theory Sequent2 imports Sequent begin

section ‹Completeness Revisited›

lemma ‹∃p. q = compl p›
  by (metis compl.simps(1))

definition compl' where
  ‹compl' = (λq. (SOME p. q = compl p))›

lemma comp'_sem:
  ‹eval e f g (compl' p) ⟷ ¬ eval e f g p›
  by (smt compl'_def compl.simps(1) compl eval.simps(7) someI_ex)

lemma comp'_sem_list: ‹list_ex (λp. ¬ eval e f g p) (map compl' ps) ⟷ list_ex (eval e f g) ps›
  by (induct ps) (use comp'_sem in auto)

theorem SC_completeness':
  fixes ps :: ‹(nat, nat) form list›
  assumes ‹∀(e :: nat → nat hterm) f g. list_ex (eval e f g) (p # ps)›
  shows ‹⊨ p # ps›
proof -
  define ps' where ‹ps' = map compl' ps›
  then have ‹ps = map compl ps'›
    by (induct ps arbitrary: ps') (simp, smt (verit) compl'_def compl.simps(1) list.simps(9) someI_ex)
  from assms have ‹∀(e :: nat → nat hterm) f g. (list_ex (eval e f g) ps) ∨ eval e f g p›
    by auto
  then have ‹∀(e :: nat → nat hterm) f g. (list_ex (λp. ¬ eval e f g p) ps') ∨ eval e f g p›
    unfolding ps'_def using comp'_sem_list by blast
  then have ‹∀(e :: nat → nat hterm) f g. list_all (eval e f g) ps' ⟶ eval e f g p›
    by (metis Ball_set Bex_set)
  then have ‹⊨ p # map compl ps'›
    using SC_completeness by blast
  then show ?thesis
    using ‹ps = map compl ps'› by auto
qed

corollary
  fixes ps :: ‹(nat, nat) form list›
  assumes ‹∀(e :: nat → nat hterm) f g. list_ex (eval e f g) ps›
  shows ‹⊨ ps›
  using assms SC_completeness' by (cases ps) auto

end