Theory Sequent2

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