Theory FOL_Seq_Calc1.Sequent
section ‹Sequent Calculus›
theory Sequent imports Tableau begin
inductive SC :: ‹('a, 'b) form list ⇒ bool› (‹⊢ _› 0) where
Basic: ‹⊢ Pred i l # Neg (Pred i l) # G›
| BasicNegFF: ‹⊢ Neg ⊥ # G›
| BasicTT: ‹⊢ ⊤ # G›
| AlphaNegNeg: ‹⊢ A # G ⟹ ⊢ Neg (Neg A) # G›
| AlphaNegAnd: ‹⊢ Neg A # Neg B # G ⟹ ⊢ Neg (And A B) # G›
| AlphaOr: ‹⊢ A # B # G ⟹ ⊢ Or A B # G›
| AlphaImpl: ‹⊢ Neg A # B # G ⟹ ⊢ Impl A B # G›
| BetaAnd: ‹⊢ A # G ⟹ ⊢ B # G ⟹ ⊢ And A B # G›
| BetaNegOr: ‹⊢ Neg A # G ⟹ ⊢ Neg B # G ⟹ ⊢ Neg (Or A B) # G›
| BetaNegImpl: ‹⊢ A # G ⟹ ⊢ Neg B # G ⟹ ⊢ Neg (Impl A B) # G›
| GammaExists: ‹⊢ subst A t 0 # G ⟹ ⊢ Exists A # G›
| GammaNegForall: ‹⊢ Neg (subst A t 0) # G ⟹ ⊢ Neg (Forall A) # G›
| DeltaForall: ‹⊢ subst A (App n []) 0 # G ⟹ news n (A # G) ⟹ ⊢ Forall A # G›
| DeltaNegExists: ‹⊢ Neg (subst A (App n []) 0) # G ⟹ news n (A # G) ⟹ ⊢ Neg (Exists A) # G›
| Order: ‹⊢ G ⟹ set G = set G' ⟹ ⊢ G'›
lemma Shift: ‹⊢ rotate1 G ⟹ ⊢ G›
by (simp add: Order)
lemma Swap: ‹⊢ B # A # G ⟹ ⊢ A # B # G›
by (simp add: Order insert_commute)
lemma ‹⊢ [Neg (Pred ''A'' []), Pred ''A'' []]›
by (rule Shift, simp) (rule Basic)
lemma ‹⊢ [And (Pred ''A'' []) (Pred ''B'' []), Neg (And (Pred ''B'' []) (Pred ''A'' []))]›
apply (rule BetaAnd)
apply (rule Swap)
apply (rule AlphaNegAnd)
apply (rule Shift, simp, rule Swap)
apply (rule Basic)
apply (rule Swap)
apply (rule AlphaNegAnd)
apply (rule Shift, rule Shift, simp)
apply (rule Basic)
done
subsection ‹Soundness›
lemma SC_soundness: ‹⊢ G ⟹ ∃p ∈ set G. eval e f g p›
proof (induct G arbitrary: f rule: SC.induct)
case (DeltaForall A n G)
then consider
‹∀x. eval e (f(n := λw. x)) g (subst A (App n []) 0)› |
‹∃x. ∃p ∈ set G. eval e (f(n := λw. x)) g p›
by fastforce
then show ?case
proof cases
case 1
then have ‹∀x. eval (shift e 0 x) (f(n := λw. x)) g A›
by simp
then have ‹∀x. eval (shift e 0 x) f g A›
using ‹news n (A # G)› by simp
then show ?thesis
by simp
next
case 2
then have ‹∃p ∈ set G. eval e f g p›
using ‹news n (A # G)› using Ball_set insert_iff list.set(2) upd_lemma by metis
then show ?thesis
by simp
qed
next
case (DeltaNegExists A n G)
then consider
‹∀x. eval e (f(n := λw. x)) g (Neg (subst A (App n []) 0))› |
‹∃x. ∃p ∈ set G. eval e (f(n := λw. x)) g p›
by fastforce
then show ?case
proof cases
case 1
then have ‹∀x. eval (shift e 0 x) (f(n := λw. x)) g (Neg A)›
by simp
then have ‹∀x. eval (shift e 0 x) f g (Neg A)›
using ‹news n (A # G)› by simp
then show ?thesis
by simp
next
case 2
then have ‹∃p ∈ set G. eval e f g p›
using ‹news n (A # G)› using Ball_set insert_iff list.set(2) upd_lemma by metis
then show ?thesis
by simp
qed
qed auto
subsection ‹Tableau Calculus Equivalence›
fun compl :: ‹('a, 'b) form ⇒ ('a, 'b) form› where
‹compl (Neg p) = p›
| ‹compl p = Neg p›
lemma compl: ‹compl p = Neg p ∨ (∃q. compl p = q ∧ p = Neg q)›
by (cases p rule: compl.cases) simp_all
lemma new_compl: ‹new n p ⟹ new n (compl p)›
by (cases p rule: compl.cases) simp_all
lemma news_compl: ‹news n G ⟹ news n (map compl G)›
using new_compl by (induct G) fastforce+
theorem TC_SC: ‹⊣ G ⟹ ⊢ map compl G›
proof (induct G rule: TC.induct)
case (Basic i l G)
then show ?case
using SC.Basic Swap by fastforce
next
case (AlphaNegNeg A G)
then show ?case
using SC.AlphaNegNeg compl by (metis compl.simps(1) list.simps(9))
next
case (AlphaAnd A B G)
then have *: ‹⊢ compl A # compl B # map compl G›
by simp
then have ‹⊢ Neg A # Neg B # map compl G›
using compl AlphaNegNeg Swap by metis
then show ?case
using AlphaNegAnd by simp
next
case (AlphaNegImpl A B G)
then have ‹⊢ compl A # B # map compl G›
by simp
then have ‹⊢ Neg A # B # map compl G›
using compl AlphaNegNeg by metis
then show ?case
using AlphaImpl by simp
next
case (BetaOr A G B)
then have ‹⊢ compl A # map compl G› ‹⊢ compl B # map compl G›
by simp_all
then have ‹⊢ Neg A # map compl G› ‹⊢ Neg B # map compl G›
using compl AlphaNegNeg by metis+
then show ?case
using BetaNegOr by simp
next
case (BetaImpl A G B)
then have ‹⊢ A # map compl G› ‹⊢ compl B # map compl G›
by simp_all
then have ‹⊢ A # map compl G› ‹⊢ Neg B # map compl G›
by - (assumption, metis compl AlphaNegNeg)
then have ‹⊢ Neg (Impl A B) # map compl G›
using BetaNegImpl by blast
then have ‹⊢ compl (Impl A B) # map compl G›
using ‹⊢ A # map compl G› compl by simp
then show ?case
by simp
next
case (GammaForall A t G)
then have ‹⊢ compl (subst A t 0) # map compl G›
by simp
then have ‹⊢ Neg (subst A t 0) # map compl G›
using compl AlphaNegNeg by metis
then show ?case
using GammaNegForall by simp
next
case (DeltaExists A n G)
then have ‹⊢ compl (subst A (App n []) 0) # map compl G›
by simp
then have ‹⊢ Neg (subst A (App n []) 0) # map compl G›
using compl AlphaNegNeg by metis
moreover have ‹news n (A # map compl G)›
using DeltaExists news_compl by fastforce
ultimately show ?case
using DeltaNegExists by simp
next
case (DeltaNegForall A n G)
then have ‹⊢ subst A (App n []) 0 # map compl G›
by simp
moreover have ‹news n (A # map compl G)›
using DeltaNegForall news_compl by fastforce
ultimately show ?case
using DeltaForall by simp
qed (simp_all add: SC.intros)
subsection ‹Completeness›
theorem SC_completeness:
fixes p :: ‹(nat, nat) form›
assumes ‹∀(e :: nat ⇒ nat hterm) f g. list_all (eval e f g) ps ⟶ eval e f g p›
shows ‹⊢ p # map compl ps›
proof -
have ‹⊣ Neg p # ps›
using assms tableau_completeness unfolding tableauproof_def by simp
then show ?thesis
using TC_SC by fastforce
qed
corollary
fixes p :: ‹(nat, nat) form›
assumes ‹∀(e :: nat ⇒ nat hterm) f g. eval e f g p›
shows ‹⊢ [p]›
using assms SC_completeness list.map(1) by metis
end