Theory II_Prelims
chapter‹Syntactic Preliminaries for the Second Incompleteness Theorem›
theory II_Prelims
imports Pf_Predicates
begin
declare IndP.simps [simp del]
lemma VarP_Var [intro]: "H ⊢ VarP «Var i»"
proof -
have "{} ⊢ VarP «Var i»"
by (auto simp: Sigma_fm_imp_thm [OF VarP_sf] ground_fm_aux_def supp_conv_fresh)
thus ?thesis
by (rule thin0)
qed
lemma VarP_neq_IndP: "{t EQ v, VarP v, IndP t} ⊢ Fls"
proof -
obtain m::name where "atom m ♯ (t,v)"
by (metis obtain_fresh)
thus ?thesis
apply (auto simp: VarP_def IndP.simps [of m])
apply (rule cut_same [of _ "OrdP (Q_Ind (Var m))"])
apply (blast intro: Sym Trans OrdP_cong [THEN Iff_MP_same])
by (metis OrdP_HPairE)
qed
lemma OrdP_ORD_OF [intro]: "H ⊢ OrdP (ORD_OF n)"
proof -
have "{} ⊢ OrdP (ORD_OF n)"
by (induct n) (auto simp: OrdP_SUCC_I)
thus ?thesis
by (rule thin0)
qed
lemma Mem_HFun_Sigma_OrdP: "{HPair t u IN f, HFun_Sigma f} ⊢ OrdP t"
proof -
obtain x::name and y::name and z::name and x'::name and y'::name and z'::name
where "atom z ♯ (f,t,u,z',x,y,x',y')" "atom z' ♯ (f,t,u,x,y,x',y')"
"atom x ♯ (f,t,u,y,x',y')" "atom y ♯ (f,t,u,x',y')"
"atom x' ♯ (f,t,u,y')" "atom y' ♯ (f,t,u)"
by (metis obtain_fresh)
thus ?thesis
apply (simp add: HFun_Sigma.simps [of z f z' x y x' y'])
apply (rule All2_E [where x="HPair t u", THEN rotate2], auto)
apply (rule All2_E [where x="HPair t u"], auto intro: OrdP_cong [THEN Iff_MP2_same])
done
qed
section ‹NotInDom›
nominal_function NotInDom :: "tm ⇒ tm ⇒ fm"
where "atom z ♯ (t, r) ⟹ NotInDom t r = All z (Neg (HPair t (Var z) IN r))"
by (auto simp: eqvt_def NotInDom_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)
nominal_termination (eqvt)
by lexicographic_order
lemma NotInDom_fresh_iff [simp]: "a ♯ NotInDom t r ⟷ a ♯ (t, r)"
proof -
obtain j::name where "atom j ♯ (t,r)"
by (rule obtain_fresh)
thus ?thesis
by auto
qed
lemma subst_fm_NotInDom [simp]: "(NotInDom t r)(i::=x) = NotInDom (subst i x t) (subst i x r)"
proof -
obtain j::name where "atom j ♯ (i,x,t,r)"
by (rule obtain_fresh)
thus ?thesis
by (auto simp: NotInDom.simps [of j])
qed
lemma NotInDom_cong: "H ⊢ t EQ t' ⟹ H ⊢ r EQ r' ⟹ H ⊢ NotInDom t r IFF NotInDom t' r'"
by (rule P2_cong) auto
lemma NotInDom_Zero: "H ⊢ NotInDom t Zero"
proof -
obtain z::name where "atom z ♯ t"
by (metis obtain_fresh)
hence "{} ⊢ NotInDom t Zero"
by (auto simp: fresh_Pair)
thus ?thesis
by (rule thin0)
qed
lemma NotInDom_Fls: "{HPair d d' IN r, NotInDom d r} ⊢ A"
proof -
obtain z::name where "atom z ♯ (d,r)"
by (metis obtain_fresh)
hence "{HPair d d' IN r, NotInDom d r} ⊢ Fls"
by (auto intro!: Ex_I [where x=d'])
thus ?thesis
by (metis ExFalso)
qed
lemma NotInDom_Contra: "H ⊢ NotInDom d r ⟹ H ⊢ HPair x y IN r ⟹ insert (x EQ d) H ⊢ A"
by (rule NotInDom_Fls [THEN cut2, THEN ExFalso])
(auto intro: thin1 NotInDom_cong [OF Assume Refl, THEN Iff_MP2_same])
section ‹Restriction of a Sequence to a Domain›
nominal_function RestrictedP :: "tm ⇒ tm ⇒ tm ⇒ fm"
where "⟦atom x ♯ (y,f,k,g); atom y ♯ (f,k,g)⟧ ⟹
RestrictedP f k g =
g SUBS f AND
All x (All y (HPair (Var x) (Var y) IN g IFF
(Var x) IN k AND HPair (Var x) (Var y) IN f))"
by (auto simp: eqvt_def RestrictedP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)
nominal_termination (eqvt)
by lexicographic_order
lemma RestrictedP_fresh_iff [simp]: "a ♯ RestrictedP f k g ⟷ a ♯ f ∧ a ♯ k ∧ a ♯ g"
proof -
obtain x::name and y::name where "atom x ♯ (y,f,k,g)" "atom y ♯ (f,k,g)"
by (metis obtain_fresh)
thus ?thesis
by auto
qed
lemma subst_fm_RestrictedP [simp]:
"(RestrictedP f k g)(i::=u) = RestrictedP (subst i u f) (subst i u k) (subst i u g)"
proof -
obtain x::name and y::name where "atom x ♯ (y,f,k,g,i,u)" "atom y ♯ (f,k,g,i,u)"
by (metis obtain_fresh)
thus ?thesis
by (auto simp: RestrictedP.simps [of x y])
qed
lemma RestrictedP_cong:
"⟦H ⊢ f EQ f'; H ⊢ k EQ A'; H ⊢ g EQ g'⟧
⟹ H ⊢ RestrictedP f k g IFF RestrictedP f' A' g'"
by (rule P3_cong) auto
lemma RestrictedP_Zero: "H ⊢ RestrictedP Zero k Zero"
proof -
obtain x::name and y::name where "atom x ♯ (y,k)" "atom y ♯ (k)"
by (metis obtain_fresh)
hence "{} ⊢ RestrictedP Zero k Zero"
by (auto simp: RestrictedP.simps [of x y])
thus ?thesis
by (rule thin0)
qed
lemma RestrictedP_Mem: "{ RestrictedP s k s', HPair a b IN s, a IN k } ⊢ HPair a b IN s'"
proof -
obtain x::name and y::name where "atom x ♯ (y,s,k,s',a,b)" "atom y ♯ (s,k,s',a,b)"
by (metis obtain_fresh)
thus ?thesis
apply (auto simp: RestrictedP.simps [of x y])
apply (rule All_E [where x=a, THEN rotate2], auto)
apply (rule All_E [where x=b], auto intro: Iff_E2)
done
qed
lemma RestrictedP_imp_Subset: "{RestrictedP s k s'} ⊢ s' SUBS s"
proof -
obtain x::name and y::name where "atom x ♯ (y,s,k,s')" "atom y ♯ (s,k,s')"
by (metis obtain_fresh)
thus ?thesis
by (auto simp: RestrictedP.simps [of x y])
qed
lemma RestrictedP_Mem2:
"{ RestrictedP s k s', HPair a b IN s' } ⊢ HPair a b IN s AND a IN k"
proof -
obtain x::name and y::name where "atom x ♯ (y,s,k,s',a,b)" "atom y ♯ (s,k,s',a,b)"
by (metis obtain_fresh)
thus ?thesis
apply (auto simp: RestrictedP.simps [of x y] intro: Subset_D)
apply (rule All_E [where x=a, THEN rotate2], auto)
apply (rule All_E [where x=b], auto intro: Iff_E1)
done
qed
lemma RestrictedP_Mem_D: "H ⊢ RestrictedP s k t ⟹ H ⊢ a IN t ⟹ insert (a IN s) H ⊢ A ⟹ H ⊢ A"
by (metis RestrictedP_imp_Subset Subset_E cut1)
lemma RestrictedP_Eats:
"{ RestrictedP s k s', a IN k } ⊢ RestrictedP (Eats s (HPair a b)) k (Eats s' (HPair a b))"
proof -
obtain x::name and y::name
where "atom x ♯ (y,s,k,s',a,b)" "atom y ♯ (s,k,s',a,b)"
by (metis obtain_fresh)
thus ?thesis
apply (auto simp: RestrictedP.simps [of x y])
apply (metis Assume Subset_Eats_I Subset_trans)
apply (metis Mem_Eats_I2 Refl)
apply (rule Swap, auto)
apply (rule All_E [where x="Var x", THEN rotate2], auto)
apply (rule All_E [where x="Var y"], simp)
apply (metis Assume Conj_E Iff_E1)
apply (blast intro: Subset_D)
apply (blast intro: Mem_cong [THEN Iff_MP2_same])
apply (metis Assume AssumeH(2) HPair_cong Mem_Eats_I2)
apply (rule All_E [where x="Var x", THEN rotate3], auto)
apply (rule All_E [where x="Var y"], simp)
apply (metis Assume AssumeH(2) Conj_I Iff_E2 Mem_Eats_I1)
apply (blast intro: Mem_Eats_I2 HPair_cong)
done
qed
lemma exists_RestrictedP:
assumes s: "atom s ♯ (f,k)"
shows "H ⊢ Ex s (RestrictedP f k (Var s))"
proof -
obtain j::name and x::name and y::name and z::name
where atoms: "atom j ♯ (k,z,s)" "atom x ♯ (j,k,z,s)" "atom y ♯ (x,j,k,z,s)" "atom z ♯ (s,k)"
by (metis obtain_fresh)
have "{} ⊢ Ex s (RestrictedP (Var z) k (Var s))"
apply (rule Ind [of j z]) using atoms s
apply simp_all
apply (rule Ex_I [where x=Zero], simp add: RestrictedP_Zero)
apply (rule All_I)+
apply (auto del: Ex_EH)
apply (rule thin1)
apply (rule Ex_E)
proof (rule Cases [where A="Ex x (Ex y ((Var x) IN k AND Var j EQ HPair (Var x) (Var y)))"], auto)
show "{Var x IN k, Var j EQ HPair (Var x) (Var y), RestrictedP (Var z) k (Var s)}
⊢ Ex s (RestrictedP (Eats (Var z) (Var j)) k (Var s))"
apply (rule Ex_I [where x="Eats (Var s) (HPair (Var x) (Var y))"])
using atoms s apply auto
apply (rule RestrictedP_cong [OF _ Refl Refl, THEN Iff_MP2_same])
apply (blast intro: Eats_cong [OF Refl])
apply (rule Var_Eq_subst_Iff [THEN rotate2, THEN Iff_MP_same])
apply (auto intro: RestrictedP_Eats [THEN cut2])
done
next
obtain u::name and v::name
where uv: "atom u ♯ (x,y,z,s,j,k)" "atom v ♯ (u,x,y,z,s,j,k)"
by (metis obtain_fresh)
show "{Neg (Ex x (Ex y (Var x IN k AND Var j EQ HPair (Var x) (Var y)))),
RestrictedP (Var z) k (Var s)} ⊢
Ex s (RestrictedP (Eats (Var z) (Var j)) k (Var s))"
apply (rule Ex_I [where x="Var s"])
using uv atoms
apply (auto simp: RestrictedP.simps [of u v])
apply (metis Assume Subset_Eats_I Subset_trans)
apply (rule Swap, auto)
apply (rule All_E [THEN rotate4, of _ _ "Var u"], auto)
apply (rule All_E [where x="Var v"], simp)
apply (metis Assume Conj_E Iff_E1)
apply (rule Mem_Eats_I1)
apply (metis Assume AssumeH(3) Subset_D)
apply (rule All_E [where x="Var u", THEN rotate5], auto)
apply (rule All_E [where x="Var v"], simp)
apply (metis Assume AssumeH(2) Conj_I Iff_E2)
apply (rule ContraProve [THEN rotate3])
apply (rule Ex_I [where x="Var u"], simp)
apply (rule Ex_I [where x="Var v"], auto intro: Sym)
done
qed
hence "{} ⊢ (Ex s (RestrictedP (Var z) k (Var s)))(z::=f)"
by (rule Subst) simp
thus ?thesis using atoms s
by simp (rule thin0)
qed
lemma cut_RestrictedP:
assumes s: "atom s ♯ (f,k,A)" and "∀C ∈ H. atom s ♯ C"
shows "insert (RestrictedP f k (Var s)) H ⊢ A ⟹ H ⊢ A"
apply (rule cut_same [OF exists_RestrictedP [of s]])
using assms apply auto
done
lemma RestrictedP_NotInDom: "{ RestrictedP s k s', Neg (j IN k) } ⊢ NotInDom j s'"
proof -
obtain x::name and y::name and z::name
where "atom x ♯ (y,s,j,k,s')" "atom y ♯ (s,j,k,s')" "atom z ♯ (s,j,k,s')"
by (metis obtain_fresh)
thus ?thesis
apply (auto simp: RestrictedP.simps [of x y] NotInDom.simps [of z])
apply (rule All_E [where x=j, THEN rotate3], auto)
apply (rule All_E, auto intro: Conj_E1 Iff_E1)
done
qed
declare RestrictedP.simps [simp del]
section ‹Applications to LstSeqP›
lemma HFun_Sigma_Eats:
assumes "H ⊢ HFun_Sigma r" "H ⊢ NotInDom d r" "H ⊢ OrdP d"
shows "H ⊢ HFun_Sigma (Eats r (HPair d d'))"
proof -
obtain x::name and y::name and z::name and x'::name and y'::name and z'::name and z''::name
where "atom z'' ♯ (r,d,d',z,z',x,y,x',y')"
and "atom z ♯ (r,d,d',z',x,y,x',y')" and "atom z' ♯ (r,d,d',x,y,x',y')"
and "atom x ♯ (r,d,d',y,x',y')" and "atom y ♯ (r,d,d',x',y')"
and "atom x' ♯ (r,d,d',y')" and "atom y' ♯ (r,d,d')"
by (metis obtain_fresh)
hence "{ HFun_Sigma r, NotInDom d r, OrdP d } ⊢ HFun_Sigma (Eats r (HPair d d'))"
apply (auto simp: HFun_Sigma.simps [of z _ z' x y x' y'])
apply (rule Ex_I [where x = "Var z"], simp)
apply (rule Neg_Imp_I, blast)
apply (rule All_E [where x = "Var z'"], auto)
apply (rule Ex_I [where x = "Var z"], simp)
apply (rule Neg_Imp_I, blast)
apply (rule All_E [where x = "Var z"], simp)
apply (rule Imp_E, auto del: Disj_EH)
apply (rule thin1)
apply (rule thin1)
apply (rule Ex_I [where x = "Var x"], simp)
apply (rule Ex_I [where x = "Var y"], simp)
apply (rule Ex_I [where x = d], simp)
apply (rule Ex_I [where x = d'], auto)
apply (blast intro: Disj_I1 OrdNotEqP_I NotInDom_Contra Mem_cong [THEN Iff_MP_same])
apply (rule Ex_I [where x = "Var z'"])
apply (subst subst_fm_Ex_with_renaming [where i'=z''] | subst subst_fm.simps)+
apply (auto simp add: flip_fresh_fresh)
apply (rule Ex_I [where x = "Var z'", THEN Swap], simp)
apply (rule Neg_I)
apply (rule Imp_E, auto del: Disj_EH)
apply (rule thin1)
apply (rule thin1)
apply (rule Ex_I [where x = d], simp)
apply (rule Ex_I [where x = d'], simp)
apply (rule Ex_I [where x = "Var x"], simp)
apply (rule Ex_I [where x = "Var y"], auto)
apply (blast intro: Disj_I1 Sym_L OrdNotEqP_I NotInDom_Contra Mem_cong [THEN Iff_MP_same])
apply (rule rotate2 [OF Swap])
apply (rule Ex_I [where x = d], auto)
apply (rule Ex_I [where x = d'], auto)
apply (rule Ex_I [where x = d], auto)
apply (rule Ex_I [where x = d'], auto intro: Disj_I2)
done
thus ?thesis using assms
by (rule cut3)
qed
lemma HFun_Sigma_single [iff]: "H ⊢ OrdP d ⟹ H ⊢ HFun_Sigma (Eats Zero (HPair d d'))"
by (metis HFun_Sigma_Eats HFun_Sigma_Zero NotInDom_Zero)
lemma LstSeqP_single [iff]: "H ⊢ LstSeqP (Eats Zero (HPair Zero x)) Zero x"
by (auto simp: LstSeqP.simps intro!: OrdP_SUCC_I HDomain_Incl_Eats_I Mem_Eats_I2)
lemma NotInDom_LstSeqP_Eats:
"{ NotInDom (SUCC k) s, LstSeqP s k y } ⊢ LstSeqP (Eats s (HPair (SUCC k) z)) (SUCC k) z"
by (auto simp: LstSeqP.simps intro: HDomain_Incl_Eats_I Mem_Eats_I2 OrdP_SUCC_I HFun_Sigma_Eats)
lemma RestrictedP_HDomain_Incl: "{HDomain_Incl s k, RestrictedP s k s'} ⊢ HDomain_Incl s' k"
proof -
obtain u::name and v::name and x::name and y::name and z::name
where "atom u ♯ (v,s,k,s')" "atom v ♯ (s,k,s')"
"atom x ♯ (s,k,s',u,v,y,z)" "atom y ♯ (s,k,s',u,v,z)" "atom z ♯ (s,k,s',u,v)"
by (metis obtain_fresh)
thus ?thesis
apply (auto simp: HDomain_Incl.simps [of x _ _ y z])
apply (rule Ex_I [where x="Var x"], auto)
apply (rule Ex_I [where x="Var y"], auto)
apply (rule Ex_I [where x="Var z"], simp)
apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same, THEN rotate2])
apply (auto simp: RestrictedP.simps [of u v])
apply (rule All_E [where x="Var x", THEN rotate2], auto)
apply (rule All_E [where x="Var y"])
apply (auto intro: Iff_E ContraProve Mem_cong [THEN Iff_MP_same])
done
qed
lemma RestrictedP_HFun_Sigma: "{HFun_Sigma s, RestrictedP s k s'} ⊢ HFun_Sigma s'"
by (metis Assume RestrictedP_imp_Subset Subset_HFun_Sigma rcut2)
lemma RestrictedP_LstSeqP:
"{ RestrictedP s (SUCC k) s', LstSeqP s k y } ⊢ LstSeqP s' k y"
by (auto simp: LstSeqP.simps
intro: Mem_Neg_refl cut2 [OF RestrictedP_HDomain_Incl]
cut2 [OF RestrictedP_HFun_Sigma] cut3 [OF RestrictedP_Mem])
lemma RestrictedP_LstSeqP_Eats:
"{ RestrictedP s (SUCC k) s', LstSeqP s k y }
⊢ LstSeqP (Eats s' (HPair (SUCC k) z)) (SUCC k) z"
by (blast intro: Mem_Neg_refl cut2 [OF NotInDom_LstSeqP_Eats]
cut2 [OF RestrictedP_NotInDom] cut2 [OF RestrictedP_LstSeqP])
section‹Ordinal Addition›
subsection‹Predicate form, defined on sequences›
nominal_function SeqHaddP :: "tm ⇒ tm ⇒ tm ⇒ tm ⇒ fm"
where "⟦atom l ♯ (sl,s,k,j); atom sl ♯ (s,j)⟧ ⟹
SeqHaddP s j k y = LstSeqP s k y AND
HPair Zero j IN s AND
All2 l k (Ex sl (HPair (Var l) (Var sl) IN s AND
HPair (SUCC (Var l)) (SUCC (Var sl)) IN s))"
by (auto simp: eqvt_def SeqHaddP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)
nominal_termination (eqvt)
by lexicographic_order
lemma SeqHaddP_fresh_iff [simp]: "a ♯ SeqHaddP s j k y ⟷ a ♯ s ∧ a ♯ j ∧ a ♯ k ∧ a ♯ y"
proof -
obtain l::name and sl::name where "atom l ♯ (sl,s,k,j)" "atom sl ♯ (s,j)"
by (metis obtain_fresh)
thus ?thesis
by force
qed
lemma SeqHaddP_subst [simp]:
"(SeqHaddP s j k y)(i::=t) = SeqHaddP (subst i t s) (subst i t j) (subst i t k) (subst i t y)"
proof -
obtain l::name and sl::name where "atom l ♯ (s,k,j,sl,t,i)" "atom sl ♯ (s,k,j,t,i)"
by (metis obtain_fresh)
thus ?thesis
by (auto simp: SeqHaddP.simps [where l=l and sl=sl])
qed
declare SeqHaddP.simps [simp del]
nominal_function HaddP :: "tm ⇒ tm ⇒ tm ⇒ fm"
where "⟦atom s ♯ (x,y,z)⟧ ⟹
HaddP x y z = Ex s (SeqHaddP (Var s) x y z)"
by (auto simp: eqvt_def HaddP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)
nominal_termination (eqvt)
by lexicographic_order
lemma HaddP_fresh_iff [simp]: "a ♯ HaddP x y z ⟷ a ♯ x ∧ a ♯ y ∧ a ♯ z"
proof -
obtain s::name where "atom s ♯ (x,y,z)"
by (metis obtain_fresh)
thus ?thesis
by force
qed
lemma HaddP_subst [simp]: "(HaddP x y z)(i::=t) = HaddP (subst i t x) (subst i t y) (subst i t z)"
proof -
obtain s::name where "atom s ♯ (x,y,z,t,i)"
by (metis obtain_fresh)
thus ?thesis
by (auto simp: HaddP.simps [of s])
qed
lemma HaddP_cong: "⟦H ⊢ t EQ t'; H ⊢ u EQ u'; H ⊢ v EQ v'⟧ ⟹ H ⊢ HaddP t u v IFF HaddP t' u' v'"
by (rule P3_cong) auto
declare HaddP.simps [simp del]
lemma HaddP_Zero2: "H ⊢ HaddP x Zero x"
proof -
obtain s::name and l::name and sl::name where "atom l ♯ (sl,s,x)" "atom sl ♯ (s,x)" "atom s ♯ x"
by (metis obtain_fresh)
hence "{} ⊢ HaddP x Zero x"
by (auto simp: HaddP.simps [of s] SeqHaddP.simps [of l sl]
intro!: Mem_Eats_I2 Ex_I [where x="Eats Zero (HPair Zero x)"])
thus ?thesis
by (rule thin0)
qed
lemma HaddP_imp_OrdP: "{HaddP x y z} ⊢ OrdP y"
proof -
obtain s::name and l::name and sl::name
where "atom l ♯ (sl,s,x,y,z)" "atom sl ♯ (s,x,y,z)" "atom s ♯ (x,y,z)"
by (metis obtain_fresh)
thus ?thesis
by (auto simp: HaddP.simps [of s] SeqHaddP.simps [of l sl] LstSeqP.simps)
qed
lemma HaddP_SUCC2: "{HaddP x y z} ⊢ HaddP x (SUCC y) (SUCC z)"
proof -
obtain s::name and s'::name and l::name and sl::name
where "atom s' ♯ (l,sl,s,x,y,z)" "atom l ♯ (sl,s,x,y,z)" "atom sl ♯ (s,x,y,z)" "atom s ♯ (x,y,z)"
by (metis obtain_fresh)
hence "{HaddP x y z, OrdP y} ⊢ HaddP x (SUCC y) (SUCC z)"
apply (auto simp: HaddP.simps [of s] SeqHaddP.simps [of l sl])
apply (rule cut_RestrictedP [of s' "Var s" "SUCC y"], auto)
apply (rule Ex_I [where x="Eats (Var s') (HPair (SUCC y) (SUCC z))"])
apply (auto intro!: Mem_SUCC_EH)
apply (metis rotate2 RestrictedP_LstSeqP_Eats rotate3 thin1)
apply (blast intro: Mem_Eats_I1 cut3 [OF RestrictedP_Mem] cut1 [OF Zero_In_SUCC])
apply (rule Ex_I [where x="Var l"], auto)
apply (rule Ex_I [where x="Var sl"], auto)
apply (blast intro: Mem_Eats_I1 cut3 [OF RestrictedP_Mem] Mem_SUCC_I1)
apply (blast intro: Mem_Eats_I1 cut3 [OF RestrictedP_Mem] OrdP_IN_SUCC)
apply (rule ContraProve [THEN rotate2])
apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same], simp add: LstSeqP.simps)
apply (rule Ex_I [where x=z])
apply (force intro: Mem_Eats_I1 Mem_Eats_I2 cut3 [OF RestrictedP_Mem] Mem_SUCC_I2)
done
thus ?thesis
by (metis Assume HaddP_imp_OrdP cut2)
qed
subsection‹Proving that these relations are functions›
lemma SeqHaddP_Zero_E: "{SeqHaddP s w Zero z} ⊢ w EQ z"
proof -
obtain l::name and sl::name where "atom l ♯ (s,w,z,sl)" "atom sl ♯ (s,w)"
by (metis obtain_fresh)
thus ?thesis
by (auto simp: SeqHaddP.simps [of l sl] LstSeqP.simps intro: HFun_Sigma_E)
qed
lemma SeqHaddP_SUCC_lemma:
assumes y': "atom y' ♯ (s,j,k,y)"
shows "{SeqHaddP s j (SUCC k) y} ⊢ Ex y' (SeqHaddP s j k (Var y') AND y EQ SUCC (Var y'))"
proof -
obtain l::name and sl::name where "atom l ♯ (s,j,k,y,y',sl)" "atom sl ♯ (s,j,k,y,y')"
by (metis obtain_fresh)
thus ?thesis using y'
apply (auto simp: SeqHaddP.simps [where s=s and l=l and sl=sl])
apply (rule All2_SUCC_E' [where t=k, THEN rotate2], auto)
apply (auto intro!: Ex_I [where x="Var sl"])
apply (blast intro: LstSeqP_SUCC)
apply (blast intro: LstSeqP_EQ)
done
qed
lemma SeqHaddP_SUCC:
assumes "H ⊢ SeqHaddP s j (SUCC k) y" "atom y' ♯ (s,j,k,y)"
shows "H ⊢ Ex y' (SeqHaddP s j k (Var y') AND y EQ SUCC (Var y'))"
by (metis SeqHaddP_SUCC_lemma [THEN cut1] assms)
lemma SeqHaddP_unique: "{OrdP x, SeqHaddP s w x y, SeqHaddP s' w x y'} ⊢ y' EQ y"
proof -
obtain i::name and j::name and j'::name and k::name and sl::name and sl'::name
and l::name and ji::name and ji'::name
where ij: "atom i ♯ (s,s',w,y,y')" "atom j ♯ (s,s',w,i,x,y,y')" "atom j' ♯ (s,s',w,i,j,x,y,y')"
and atoms: "atom k ♯ (s,s',w,i,j,j')" "atom sl ♯ (s,s',w,i,j,j',k)" "atom sl' ♯ (s,s',w,i,j,j',k,sl)"
"atom ji ♯ (s,s',w,i,j,j',k,sl,sl')" "atom ji' ♯ (s,s',w,i,j,j',k,sl,sl',ji)"
by (metis obtain_fresh)
have "{OrdP (Var i)}
⊢ All j (All j' (SeqHaddP s w (Var i) (Var j) IMP (SeqHaddP s' w (Var i) (Var j') IMP Var j' EQ Var j)))"
apply (rule OrdInd2H)
using ij atoms apply auto
apply (metis SeqHaddP_Zero_E [THEN cut1] Assume AssumeH(2) Sym Trans)
apply (rule cut_same [OF SeqHaddP_SUCC [where y' = ji and s=s]], auto)
apply (rule cut_same [OF SeqHaddP_SUCC [where y' = ji' and s=s']], auto)
apply (rule Ex_I [where x = "Var ji"], auto)
apply (rule All_E [where x = "Var ji'"], auto)
apply (blast intro: Trans [OF Hyp] Sym intro!: SUCC_cong)
done
hence "{OrdP (Var i)}
⊢ (All j' (SeqHaddP s w (Var i) (Var j) IMP (SeqHaddP s' w (Var i) (Var j') IMP Var j' EQ Var j)))(j::=y)"
by (metis All_D)
hence "{OrdP (Var i)}
⊢ All j' (SeqHaddP s w (Var i) y IMP (SeqHaddP s' w (Var i) (Var j') IMP Var j' EQ y))"
using ij by simp
hence "{OrdP (Var i)}
⊢ (SeqHaddP s w (Var i) y IMP (SeqHaddP s' w (Var i) (Var j') IMP Var j' EQ y))(j'::=y')"
by (metis All_D)
hence "{OrdP (Var i)} ⊢ SeqHaddP s w (Var i) y IMP (SeqHaddP s' w (Var i) y' IMP y' EQ y)"
using ij by simp
hence "{} ⊢ (OrdP (Var i) IMP SeqHaddP s w (Var i) y IMP (SeqHaddP s' w (Var i) y' IMP y' EQ y))(i::=x)"
by (metis Imp_I Subst emptyE)
thus ?thesis
using ij by simp (metis DisjAssoc2 Disj_commute anti_deduction)
qed
lemma HaddP_unique: "{HaddP w x y, HaddP w x y'} ⊢ y' EQ y"
proof -
obtain s::name and s'::name where "atom s ♯ (w,x,y,y')" "atom s' ♯ (w,x,y,y',s)"
by (metis obtain_fresh)
hence "{OrdP x, HaddP w x y, HaddP w x y'} ⊢ y' EQ y"
by (auto simp: HaddP.simps [of s _ _ y] HaddP.simps [of s' _ _ y']
intro: SeqHaddP_unique [THEN cut3])
thus ?thesis
by (metis HaddP_imp_OrdP cut_same thin1)
qed
lemma HaddP_Zero1: assumes "H ⊢ OrdP x" shows "H ⊢ HaddP Zero x x"
proof -
fix k::name
have "{ OrdP (Var k) } ⊢ HaddP Zero (Var k) (Var k)"
by (rule OrdInd2H [where i=k]) (auto intro: HaddP_Zero2 HaddP_SUCC2 [THEN cut1])
hence "{} ⊢ OrdP (Var k) IMP HaddP Zero (Var k) (Var k)"
by (metis Imp_I)
hence "{} ⊢ (OrdP (Var k) IMP HaddP Zero (Var k) (Var k))(k::=x)"
by (rule Subst) auto
hence "{} ⊢ OrdP x IMP HaddP Zero x x"
by simp
thus ?thesis using assms
by (metis MP_same thin0)
qed
lemma HaddP_Zero_D1: "insert (HaddP Zero x y) H ⊢ x EQ y"
by (metis Assume HaddP_imp_OrdP HaddP_Zero1 HaddP_unique [THEN cut2] rcut1)
lemma HaddP_Zero_D2: "insert (HaddP x Zero y) H ⊢ x EQ y"
by (metis Assume HaddP_Zero2 HaddP_unique [THEN cut2])
lemma HaddP_SUCC_Ex2:
assumes "H ⊢ HaddP x (SUCC y) z" "atom z' ♯ (x,y,z)"
shows "H ⊢ Ex z' (HaddP x y (Var z') AND z EQ SUCC (Var z'))"
proof -
obtain s::name and s'::name where "atom s ♯ (x,y,z,z')" "atom s' ♯ (x,y,z,z',s)"
by (metis obtain_fresh)
hence "{ HaddP x (SUCC y) z } ⊢ Ex z' (HaddP x y (Var z') AND z EQ SUCC (Var z'))"
using assms
apply (auto simp: HaddP.simps [of s _ _ ] HaddP.simps [of s' _ _ ])
apply (rule cut_same [OF SeqHaddP_SUCC_lemma [of z']], auto)
apply (rule Ex_I, auto)+
done
thus ?thesis
by (metis assms(1) cut1)
qed
lemma HaddP_SUCC1: "{ HaddP x y z } ⊢ HaddP (SUCC x) y (SUCC z)"
proof -
obtain i::name and j::name and z'::name
where atoms: "atom i ♯ (x,y,z)" "atom j ♯ (i,x,y,z)" "atom z' ♯ (x,i,j)"
by (metis obtain_fresh)
have "{OrdP (Var i)} ⊢ All j (HaddP x (Var i) (Var j) IMP HaddP (SUCC x) (Var i) (SUCC (Var j)))"
(is "_ ⊢ ?scheme")
proof (rule OrdInd2H)
show "{} ⊢ ?scheme(i::=Zero)"
using atoms apply auto
apply (rule cut_same [OF HaddP_Zero_D2])
apply (rule Var_Eq_subst_Iff [THEN Sym_L, THEN Iff_MP_same], auto intro: HaddP_Zero2)
done
next
show "{} ⊢ All i (OrdP (Var i) IMP ?scheme IMP ?scheme(i::=SUCC (Var i)))"
using atoms
apply auto
apply (rule cut_same [OF HaddP_SUCC_Ex2 [where z'=z']], auto)
apply (rule Ex_I [where x="Var z'"], auto)
apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same, THEN rotate3], simp)
by (metis Assume HaddP_SUCC2 cut1 thin1)
qed
hence "{OrdP (Var i)} ⊢ (HaddP x (Var i) (Var j) IMP HaddP (SUCC x) (Var i) (SUCC (Var j)))(j::=z)"
by (rule All_D)
hence "{OrdP (Var i)} ⊢ HaddP x (Var i) z IMP HaddP (SUCC x) (Var i) (SUCC z)"
using atoms by auto
hence "{} ⊢ HaddP x (Var i) z IMP HaddP (SUCC x) (Var i) (SUCC z)"
by (metis HaddP_imp_OrdP Imp_cut)
hence "{} ⊢ (HaddP x (Var i) z IMP HaddP (SUCC x) (Var i) (SUCC z))(i::=y)"
using atoms by (force intro!: Subst)
thus ?thesis
using atoms by simp (metis anti_deduction)
qed
lemma HaddP_commute: "{HaddP x y z, OrdP x} ⊢ HaddP y x z"
proof -
obtain i::name and j::name and z'::name
where atoms: "atom i ♯ (x,y,z)" "atom j ♯ (i,x,y,z)" "atom z' ♯ (x,i,j)"
by (metis obtain_fresh)
have "{OrdP (Var i), OrdP x} ⊢ All j (HaddP x (Var i) (Var j) IMP HaddP (Var i) x (Var j))"
(is "_ ⊢ ?scheme")
proof (rule OrdInd2H)
show "{OrdP x} ⊢ ?scheme(i::=Zero)"
using atoms apply auto
apply (rule cut_same [OF HaddP_Zero_D2])
apply (rule Var_Eq_subst_Iff [THEN Sym_L, THEN Iff_MP_same], auto intro: HaddP_Zero1)
done
next
show "{OrdP x} ⊢ All i (OrdP (Var i) IMP ?scheme IMP ?scheme(i::=SUCC (Var i)))"
using atoms
apply auto
apply (rule cut_same [OF HaddP_SUCC_Ex2 [where z'=z']], auto)
apply (rule Ex_I [where x="Var z'"], auto)
apply (rule rotate3)
apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same], simp)
by (metis Assume HaddP_SUCC1 cut1 thin1)
qed
hence "{OrdP (Var i), OrdP x} ⊢ (HaddP x (Var i) (Var j) IMP HaddP (Var i) x (Var j))(j::=z)"
by (rule All_D)
hence "{OrdP (Var i), OrdP x} ⊢ HaddP x (Var i) z IMP HaddP (Var i) x z"
using atoms by auto
hence "{OrdP x} ⊢ HaddP x (Var i) z IMP HaddP (Var i) x z"
by (metis HaddP_imp_OrdP Imp_cut)
hence "{OrdP x} ⊢ (HaddP x (Var i) z IMP HaddP (Var i) x z)(i::=y)"
using atoms by (force intro!: Subst)
thus ?thesis
using atoms by simp (metis anti_deduction)
qed
lemma HaddP_SUCC_Ex1:
assumes "atom i ♯ (x,y,z)"
shows "insert (HaddP (SUCC x) y z) (insert (OrdP x) H)
⊢ Ex i (HaddP x y (Var i) AND z EQ SUCC (Var i))"
proof -
have "{ HaddP (SUCC x) y z, OrdP x } ⊢ Ex i (HaddP x y (Var i) AND z EQ SUCC (Var i))"
apply (rule cut_same [OF HaddP_commute [THEN cut2]])
apply (blast intro: OrdP_SUCC_I)+
apply (rule cut_same [OF HaddP_SUCC_Ex2 [where z'=i]], blast)
using assms apply auto
apply (auto intro!: Ex_I [where x="Var i"])
by (metis AssumeH(2) HaddP_commute [THEN cut2] HaddP_imp_OrdP rotate2 thin1)
thus ?thesis
by (metis Assume AssumeH(2) cut2)
qed
lemma HaddP_inv2: "{HaddP x y z, HaddP x y' z, OrdP x} ⊢ y' EQ y"
proof -
obtain i::name and j::name and u::name and u'::name
where atoms: "atom i ♯ (x,y,y',z)" "atom j ♯ (i,x,y,y',z)"
"atom u ♯ (x,y,y',i,j)" "atom u' ♯ (x,y,y',u,i,j)"
by (metis obtain_fresh)
have "{OrdP (Var i)} ⊢ All j (HaddP (Var i) y (Var j) IMP HaddP (Var i) y' (Var j) IMP y' EQ y)"
(is "_ ⊢ ?scheme")
proof (rule OrdInd2H)
show "{} ⊢ ?scheme(i::=Zero)"
using atoms
by auto (metis HaddP_Zero_D1 Sym Trans thin1)
next
show "{} ⊢ All i (OrdP (Var i) IMP ?scheme IMP ?scheme(i::=SUCC (Var i)))"
using atoms
apply auto
apply (rule cut_same [OF HaddP_SUCC_Ex1 [where y=y and i=u, THEN cut2]], auto)
apply (rule Ex_I [where x="Var u"], auto)
apply (rule cut_same [OF HaddP_SUCC_Ex1 [where y=y' and i=u', THEN cut2]], auto)
apply (rule cut_same [where A="SUCC (Var u) EQ SUCC (Var u')"])
apply (auto intro: Sym Trans)
apply (rule rotate4 [OF ContraProve])
apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same], force)
done
qed
hence "{OrdP (Var i)} ⊢ (HaddP (Var i) y (Var j) IMP HaddP (Var i) y' (Var j) IMP y' EQ y)(j::=z)"
by (rule All_D)
hence "{OrdP (Var i)} ⊢ HaddP (Var i) y z IMP HaddP (Var i) y' z IMP y' EQ y"
using atoms by auto
hence "{} ⊢ OrdP (Var i) IMP HaddP (Var i) y z IMP HaddP (Var i) y' z IMP y' EQ y"
by (metis Imp_I)
hence "{} ⊢ (OrdP (Var i) IMP HaddP (Var i) y z IMP HaddP (Var i) y' z IMP y' EQ y)(i::=x)"
using atoms by (force intro!: Subst)
thus ?thesis
using atoms by simp (metis DisjAssoc2 Disj_commute anti_deduction)
qed
lemma Mem_imp_subtract:
assumes "H ⊢ x IN y" "H ⊢ OrdP y" and k: "atom (k::name) ♯ (x,y)"
shows "H ⊢ Ex k (HaddP x (Var k) y AND Zero IN (Var k))"
proof -
obtain i::name
where atoms: "atom i ♯ (x,y,k)"
by (metis obtain_fresh)
have "{OrdP (Var i)} ⊢ x IN Var i IMP Ex k (HaddP x (Var k) (Var i) AND Zero IN (Var k))"
(is "_ ⊢ ?scheme")
proof (rule OrdInd2H)
show "{} ⊢ ?scheme(i::=Zero)"
by auto
next
show "{} ⊢ All i (OrdP (Var i) IMP ?scheme IMP ?scheme(i::=SUCC (Var i)))"
using atoms k
apply (auto intro!: Mem_SUCC_EH)
apply (rule Ex_I [where x="SUCC (Var k)"], auto)
apply (metis AssumeH(4) HaddP_SUCC2 cut1 insert_commute)
apply (blast intro: Mem_SUCC_I1)
apply (rule Ex_I [where x="SUCC Zero"], auto)
apply (rule thin1)
apply (rule Var_Eq_subst_Iff [THEN Sym_L, THEN Iff_MP_same], simp)
apply (metis HaddP_SUCC2 HaddP_Zero2 cut1)
apply (rule Ex_I [where x="SUCC (Var k)"], auto intro: Mem_SUCC_I1)
apply (metis AssumeH(4) HaddP_SUCC2 cut1 insert_commute)
done
qed
hence "{} ⊢ OrdP (Var i) IMP x IN Var i IMP Ex k (HaddP x (Var k) (Var i) AND Zero IN (Var k))"
by (metis Imp_I)
hence "{} ⊢ (OrdP (Var i) IMP x IN Var i IMP Ex k (HaddP x (Var k) (Var i) AND Zero IN (Var k)))(i::=y)"
by (force intro!: Subst)
thus ?thesis using assms atoms
by simp (metis (no_types) anti_deduction cut2)
qed
lemma HaddP_OrdP:
assumes "H ⊢ HaddP x y z" "H ⊢ OrdP x" shows "H ⊢ OrdP z"
proof -
obtain i::name and j::name and k::name
where atoms: "atom i ♯ (x,y,z)" "atom j ♯ (i,x,y,z)" "atom k ♯ (i,j,x,y,z)"
by (metis obtain_fresh)
have "{OrdP (Var i), OrdP x} ⊢ All j (HaddP x (Var i) (Var j) IMP OrdP (Var j))"
(is "_ ⊢ ?scheme")
proof (rule OrdInd2H)
show "{OrdP x} ⊢ ?scheme(i::=Zero)"
using atoms
by (auto intro: HaddP_Zero_D2 OrdP_cong [THEN Iff_MP_same])
next
show "{OrdP x} ⊢ All i (OrdP (Var i) IMP ?scheme IMP ?scheme(i::=SUCC (Var i)))"
using atoms
apply auto
apply (rule cut_same [OF HaddP_SUCC_Ex2 [where z'=k]], auto)
apply (rule Ex_I [where x="Var k"], auto)
apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same, THEN rotate3], auto intro: OrdP_SUCC_I)
done
qed
hence "{OrdP (Var i), OrdP x} ⊢ (HaddP x (Var i) (Var j) IMP OrdP (Var j))(j::=z)"
by (rule All_D)
hence "{OrdP (Var i), OrdP x} ⊢ (HaddP x (Var i) z IMP OrdP z)"
using atoms by simp
hence "{OrdP x} ⊢ HaddP x (Var i) z IMP OrdP z"
by (metis HaddP_imp_OrdP Imp_cut)
hence "{OrdP x} ⊢ (HaddP x (Var i) z IMP OrdP z)(i::=y)"
using atoms by (force intro!: Subst)
thus ?thesis using assms atoms
by simp (metis anti_deduction cut2)
qed
lemma HaddP_Mem_cancel_left:
assumes "H ⊢ HaddP x y' z'" "H ⊢ HaddP x y z" "H ⊢ OrdP x"
shows "H ⊢ z' IN z IFF y' IN y"
proof -
obtain i::name and j::name and j'::name and k::name and k'::name
where atoms: "atom i ♯ (x,y,y',z,z')" "atom j ♯ (i,x,y,y',z,z')" "atom j' ♯ (i,j,x,y,y',z,z')"
"atom k ♯ (i,j,j',x,y,y',z,z')" "atom k' ♯ (i,j,j',k,x,y,y',z,z')"
by (metis obtain_fresh)
have "{OrdP (Var i)}
⊢ All j (All j' (HaddP (Var i) y' (Var j') IMP (HaddP (Var i) y (Var j) IMP
((Var j') IN (Var j) IFF y' IN y))))"
(is "_ ⊢ ?scheme")
proof (rule OrdInd2H)
show "{} ⊢ ?scheme(i::=Zero)"
using atoms apply simp
apply (rule All_I Imp_I Ex_EH)+
apply (rule cut_same [where A="Var j EQ y"])
apply (metis HaddP_Zero_D1 Sym)
apply (rule cut_same [where A="Var j' EQ y'"])
apply (metis HaddP_Zero_D1 Sym thin1)
apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same], simp)
apply (rule thin1)
apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same], auto)
done
next
show "{} ⊢ All i (OrdP (Var i) IMP ?scheme IMP ?scheme(i::=SUCC (Var i)))"
using atoms apply simp
apply (rule All_I Imp_I Ex_EH)+
apply (rule cut_same [OF HaddP_SUCC_Ex1 [of k "Var i" y "Var j", THEN cut2]], simp_all)
apply (rule AssumeH Conj_EH Ex_EH)+
apply (rule cut_same [OF HaddP_SUCC_Ex1 [of k' "Var i" y' "Var j'", THEN cut2]], simp_all)
apply (rule AssumeH Conj_EH Ex_EH)+
apply (rule rotate7)
apply (rule All_E [where x = "Var k"], simp)
apply (rule All_E [where x = "Var k'"], simp_all)
apply (rule Imp_E AssumeH)+
apply (rule Iff_trans)
prefer 2
apply (rule AssumeH)
apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same, THEN rotate3], simp)
apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same, THEN rotate5], simp)
apply (blast intro!: HaddP_OrdP OrdP_IN_SUCC_Iff)
done
qed
hence "{OrdP (Var i)}
⊢ (All j' (HaddP (Var i) y' (Var j') IMP (HaddP (Var i) y (Var j) IMP ((Var j') IN (Var j) IFF y' IN y))))(j::=z)"
by (metis All_D)
hence "{OrdP (Var i)}
⊢ (All j' (HaddP (Var i) y' (Var j') IMP (HaddP (Var i) y z IMP ((Var j') IN z IFF y' IN y))))"
using atoms by simp
hence "{OrdP (Var i)}
⊢ (HaddP (Var i) y' (Var j') IMP (HaddP (Var i) y z IMP ((Var j') IN z IFF y' IN y)))(j'::=z')"
by (metis All_D)
hence "{OrdP (Var i)} ⊢ HaddP (Var i) y' z' IMP (HaddP (Var i) y z IMP (z' IN z IFF y' IN y))"
using atoms by simp
hence "{} ⊢ (OrdP (Var i) IMP HaddP (Var i) y' z' IMP (HaddP (Var i) y z IMP (z' IN z IFF y' IN y)))(i::=x)"
by (metis Imp_I Subst emptyE)
thus ?thesis
using atoms by simp (metis assms MP_null MP_same)
qed
lemma HaddP_Mem_cancel_right_Mem:
assumes "H ⊢ HaddP x' y z'" "H ⊢ HaddP x y z" "H ⊢ x' IN x" "H ⊢ OrdP x"
shows "H ⊢ z' IN z"
proof -
have "H ⊢ OrdP x'"
by (metis Ord_IN_Ord assms(3) assms(4))
hence "H ⊢ HaddP y x' z'" "H ⊢ HaddP y x z"
by (blast intro: assms HaddP_commute [THEN cut2])+
thus ?thesis
by (blast intro: assms HaddP_imp_OrdP [THEN cut1] HaddP_Mem_cancel_left [THEN Iff_MP2_same])
qed
lemma HaddP_Mem_cases:
assumes "H ⊢ HaddP k1 k2 k" "H ⊢ OrdP k1"
"insert (x IN k1) H ⊢ A"
"insert (Var i IN k2) (insert (HaddP k1 (Var i) x) H) ⊢ A"
and i: "atom (i::name) ♯ (k1,k2,k,x,A)" and "∀C ∈ H. atom i ♯ C"
shows "insert (x IN k) H ⊢ A"
proof -
obtain j::name where j: "atom j ♯ (k1,k2,k,x)"
by (metis obtain_fresh)
have seq: "{HaddP k1 k2 k, x IN k, OrdP k1} ⊢ x IN k1 OR (Ex i (HaddP k1 (Var i) x AND Var i IN k2))"
apply (rule cut_same [OF HaddP_OrdP])
apply (rule AssumeH)+
apply (rule cut_same [OF Ord_IN_Ord])
apply (rule AssumeH)+
apply (rule OrdP_linear [of _ x k1], (rule AssumeH)+)
proof -
show "{x IN k1, OrdP x, OrdP k, HaddP k1 k2 k, x IN k, OrdP k1} ⊢ x IN k1 OR Ex i (HaddP k1 (Var i) x AND Var i IN k2)"
by (blast intro: Disj_I1)
next
show "{x EQ k1, OrdP x, OrdP k, HaddP k1 k2 k, x IN k, OrdP k1} ⊢ x IN k1 OR Ex i (HaddP k1 (Var i) x AND Var i IN k2)"
apply (rule cut_same [OF Zero_In_OrdP [of k2, THEN cut1]])
apply (metis AssumeH(4) HaddP_imp_OrdP cut1)
apply auto
apply (rule cut_same [where A="HaddP x Zero k"])
apply (blast intro: HaddP_cong [THEN Iff_MP_same] Sym)
apply (rule cut_same [where A="x EQ k"])
apply (metis HaddP_Zero_D2)
apply (blast intro: Mem_non_refl Mem_cong [THEN Iff_MP_same])
apply (rule Disj_I2)
apply (rule Ex_I [where x=Zero])
using i apply auto
apply (rule HaddP_cong [THEN Iff_MP_same])
apply (rule AssumeH Refl HaddP_Zero2)+
done
next
show "{k1 IN x, OrdP x, OrdP k, HaddP k1 k2 k, x IN k, OrdP k1} ⊢ x IN k1 OR Ex i (HaddP k1 (Var i) x AND Var i IN k2)"
apply (rule Disj_I2)
apply (rule cut_same [OF Mem_imp_subtract [of _ k1 x j]])
apply (rule AssumeH)+
using i j apply auto
apply (rule Ex_I [where x="Var j"], auto intro: HaddP_Mem_cancel_left [THEN Iff_MP_same])
done
qed
show ?thesis using assms
by (force intro: cut_same [OF seq [THEN cut3]] thin1 simp: insert_commute)
qed
lemma HaddP_Mem_contra:
assumes "H ⊢ HaddP x y z" "H ⊢ z IN x" "H ⊢ OrdP x"
shows "H ⊢ A"
proof -
obtain i::name and j::name and k::name
where atoms: "atom i ♯ (x,y,z)" "atom j ♯ (i,x,y,z)" "atom k ♯ (i,j,x,y,z)"
by (metis obtain_fresh)
have "{OrdP (Var i)} ⊢ All j (HaddP (Var i) y (Var j) IMP Neg ((Var j) IN (Var i)))"
(is "_ ⊢ ?scheme")
proof (rule OrdInd2H)
show "{} ⊢ ?scheme(i::=Zero)"
using atoms by auto
next
show "{} ⊢ All i (OrdP (Var i) IMP ?scheme IMP ?scheme(i::=SUCC (Var i)))"
using atoms apply auto
apply (rule cut_same [OF HaddP_SUCC_Ex1 [of k "Var i" y "Var j", THEN cut2]], auto)
apply (rule Ex_I [where x="Var k"], auto)
apply (blast intro: OrdP_IN_SUCC_D Mem_cong [OF _ Refl, THEN Iff_MP_same])
done
qed
hence "{OrdP (Var i)} ⊢ (HaddP (Var i) y (Var j) IMP Neg ((Var j) IN (Var i)))(j::=z)"
by (metis All_D)
hence "{} ⊢ OrdP (Var i) IMP HaddP (Var i) y z IMP Neg (z IN (Var i))"
using atoms by simp (metis Imp_I)
hence "{} ⊢ (OrdP (Var i) IMP HaddP (Var i) y z IMP Neg (z IN (Var i)))(i::=x)"
by (metis Subst emptyE)
thus ?thesis
using atoms by simp (metis MP_same MP_null Neg_D assms)
qed
lemma exists_HaddP:
assumes "H ⊢ OrdP y" "atom j ♯ (x,y)"
shows "H ⊢ Ex j (HaddP x y (Var j))"
proof -
obtain i::name
where atoms: "atom i ♯ (j,x,y)"
by (metis obtain_fresh)
have "{OrdP (Var i)} ⊢ Ex j (HaddP x (Var i) (Var j))"
(is "_ ⊢ ?scheme")
proof (rule OrdInd2H)
show "{} ⊢ ?scheme(i::=Zero)"
using atoms assms
by (force intro!: Ex_I [where x=x] HaddP_Zero2)
next
show "{} ⊢ All i (OrdP (Var i) IMP ?scheme IMP ?scheme(i::=SUCC (Var i)))"
using atoms assms
apply auto
apply (auto intro!: Ex_I [where x="SUCC (Var j)"] HaddP_SUCC2)
apply (metis HaddP_SUCC2 insert_commute thin1)
done
qed
hence "{} ⊢ OrdP (Var i) IMP Ex j (HaddP x (Var i) (Var j))"
by (metis Imp_I)
hence "{} ⊢ (OrdP (Var i) IMP Ex j (HaddP x (Var i) (Var j)))(i::=y)"
using atoms by (force intro!: Subst)
thus ?thesis
using atoms assms by simp (metis MP_null assms(1))
qed
lemma HaddP_Mem_I:
assumes "H ⊢ HaddP x y z" "H ⊢ OrdP x" shows "H ⊢ x IN SUCC z"
proof -
have "{HaddP x y z, OrdP x} ⊢ x IN SUCC z"
apply (rule OrdP_linear [of _ x "SUCC z"])
apply (auto intro: OrdP_SUCC_I HaddP_OrdP)
apply (rule HaddP_Mem_contra, blast)
apply (metis Assume Mem_SUCC_I2 OrdP_IN_SUCC_D Sym_L thin1 thin2, blast)
apply (blast intro: HaddP_Mem_contra Mem_SUCC_Refl OrdP_Trans)
done
thus ?thesis
by (rule cut2) (auto intro: assms)
qed
section ‹A Shifted Sequence›
nominal_function ShiftP :: "tm ⇒ tm ⇒ tm ⇒ tm ⇒ fm"
where "⟦atom x ♯ (x',y,z,f,del,k); atom x' ♯ (y,z,f,del,k); atom y ♯ (z,f,del,k); atom z ♯ (f,del,g,k)⟧ ⟹
ShiftP f k del g =
All z (Var z IN g IFF
(Ex x (Ex x' (Ex y ((Var z) EQ HPair (Var x') (Var y) AND
HaddP del (Var x) (Var x') AND
HPair (Var x) (Var y) IN f AND Var x IN k)))))"
by (auto simp: eqvt_def ShiftP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)
nominal_termination (eqvt)
by lexicographic_order
lemma ShiftP_fresh_iff [simp]: "a ♯ ShiftP f k del g ⟷ a ♯ f ∧ a ♯ k ∧ a ♯ del ∧ a ♯ g"
proof -
obtain x::name and x'::name and y::name and z::name
where "atom x ♯ (x',y,z,f,del,k)" "atom x' ♯ (y,z,f,del,k)"
"atom y ♯ (z,f,del,k)" "atom z ♯ (f,del,g,k)"
by (metis obtain_fresh)
thus ?thesis
by auto
qed
lemma subst_fm_ShiftP [simp]:
"(ShiftP f k del g)(i::=u) = ShiftP (subst i u f) (subst i u k) (subst i u del) (subst i u g)"
proof -
obtain x::name and x'::name and y::name and z::name
where "atom x ♯ (x',y,z,f,del,k,i,u)" "atom x' ♯ (y,z,f,del,k,i,u)"
"atom y ♯ (z,f,del,k,i,u)" "atom z ♯ (f,del,g,k,i,u)"
by (metis obtain_fresh)
thus ?thesis
by (auto simp: ShiftP.simps [of x x' y z])
qed
lemma ShiftP_Zero: "{} ⊢ ShiftP Zero k d Zero"
proof -
obtain x::name and x'::name and y::name and z::name
where "atom x ♯ (x',y,z,k,d)" "atom x' ♯ (y,z,k,d)" "atom y ♯ (z,k,d)" "atom z ♯ (k,d)"
by (metis obtain_fresh)
thus ?thesis
by (auto simp: ShiftP.simps [of x x' y z])
qed
lemma ShiftP_Mem1:
"{ShiftP f k del g, HPair a b IN f, HaddP del a a', a IN k} ⊢ HPair a' b IN g"
proof -
obtain x::name and x'::name and y::name and z::name
where "atom x ♯ (x',y,z,f,del,k,a,a',b)" "atom x' ♯ (y,z,f,del,k,a,a',b)"
"atom y ♯ (z,f,del,k,a,a',b)" "atom z ♯ (f,del,g,k,a,a',b)"
by (metis obtain_fresh)
thus ?thesis
apply (auto simp: ShiftP.simps [of x x' y z])
apply (rule All_E [where x="HPair a' b"], auto intro!: Iff_E2)
apply (rule Ex_I [where x=a], simp)
apply (rule Ex_I [where x="a'"], simp)
apply (rule Ex_I [where x=b], auto intro: Mem_Eats_I1)
done
qed
lemma ShiftP_Mem2:
assumes "atom u ♯ (f,k,del,a,b)"
shows "{ShiftP f k del g, HPair a b IN g} ⊢ Ex u ((Var u) IN k AND HaddP del (Var u) a AND HPair (Var u) b IN f)"
proof -
obtain x::name and x'::name and y::name and z::name
where atoms: "atom x ♯ (x',y,z,f,del,g,k,a,u,b)" "atom x' ♯ (y,z,f,del,g,k,a,u,b)"
"atom y ♯ (z,f,del,g,k,a,u,b)" "atom z ♯ (f,del,g,k,a,u,b)"
by (metis obtain_fresh)
thus ?thesis using assms
apply (auto simp: ShiftP.simps [of x x' y z])
apply (rule All_E [where x="HPair a b"])
apply (auto intro!: Iff_E1 [OF Assume])
apply (rule Ex_I [where x="Var x"])
apply (auto intro: Mem_cong [OF HPair_cong Refl, THEN Iff_MP2_same])
apply (blast intro: HaddP_cong [OF Refl Refl, THEN Iff_MP2_same])
done
qed
lemma ShiftP_Mem_D:
assumes "H ⊢ ShiftP f k del g" "H ⊢ a IN g"
"atom x ♯ (x',y,a,f,del,k)" "atom x' ♯ (y,a,f,del,k)" "atom y ♯ (a,f,del,k)"
shows "H ⊢ (Ex x (Ex x' (Ex y (a EQ HPair (Var x') (Var y) AND
HaddP del (Var x) (Var x') AND
HPair (Var x) (Var y) IN f AND Var x IN k))))"
(is "_ ⊢ ?concl")
proof -
obtain z::name where "atom z ♯ (x,x',y,f,del,g,k,a)"
by (metis obtain_fresh)
hence "{ShiftP f k del g, a IN g} ⊢ ?concl" using assms
by (auto simp: ShiftP.simps [of x x' y z]) (rule All_E [where x=a], auto intro: Iff_E1)
thus ?thesis
by (rule cut2) (rule assms)+
qed
lemma ShiftP_Eats_Eats:
"{ShiftP f k del g, HaddP del a a', a IN k}
⊢ ShiftP (Eats f (HPair a b)) k del (Eats g (HPair a' b))"
proof -
obtain x::name and x'::name and y::name and z::name
where "atom x ♯ (x',y,z,f,del,g,k,a,a',b)" "atom x' ♯ (y,z,f,del,g,k,a,a',b)"
"atom y ♯ (z,f,del,g,k,a,a',b)" "atom z ♯ (f,del,g,k,a,a',b)"
by (metis obtain_fresh)
thus ?thesis
apply (auto simp: ShiftP.simps [of x x' y z] intro!: Iff_I [THEN Swap])
apply (rule All_E [where x="Var z", THEN rotate2], simp)
apply (rule Iff_E)
apply auto [1]
apply (rule Ex_I [where x="Var x"], simp)
apply (rule Ex_I [where x="Var x'"], simp)
apply (rule Ex_I [where x="Var y"], simp)
apply (blast intro: Mem_Eats_I1, blast)
apply (rule Ex_I [where x=a], simp)
apply (rule Ex_I [where x="a'"], simp)
apply (rule Ex_I [where x=b], simp)
apply (metis Assume AssumeH(3) AssumeH(4) Conj_I Mem_Eats_I2 Refl)
apply (rule All_E [where x="Var z", THEN rotate5], auto)
apply (rule Mem_Eats_I1)
apply (rule Iff_MP2_same [OF Hyp], blast)
apply (rule Ex_I [where x="Var x"], simp)
apply (rule Ex_I [where x="Var x'"], simp)
apply (rule Ex_I [where x="Var y"], auto)
apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same, THEN rotate5], simp)
apply (blast intro: Mem_Eats_I2 HaddP_cong [THEN Iff_MP_same] HaddP_unique [THEN cut2] HPair_cong)
done
qed
lemma ShiftP_Eats_Neg:
assumes "atom u ♯ (u',v,f,k,del,g,c)" "atom u' ♯ (v,f,k,del,g,c)" "atom v ♯ (f,k,del,g,c)"
shows
"{ShiftP f k del g,
Neg (Ex u (Ex u' (Ex v (c EQ HPair (Var u) (Var v) AND Var u IN k AND HaddP del (Var u) (Var u')))))}
⊢ ShiftP (Eats f c) k del g"
proof -
obtain x::name and x'::name and y::name and z::name
where atoms: "atom x ♯ (x',y,z,u,u',v,f,k,del,g,c)" "atom x' ♯ (y,z,u,u',v,f,k,del,g,c)"
"atom y ♯ (z,u,u',v,f,k,del,g,c)" "atom z ♯ (u,u',v,f,k,del,g,c)"
by (metis obtain_fresh)
thus ?thesis using assms
apply (auto simp: ShiftP.simps [of x x' y z] intro!: Iff_I [THEN Swap])
apply (rule All_E [where x="Var z", THEN rotate3])
apply (auto intro!: Iff_E1 [OF Assume])
apply (rule Ex_I [where x="Var x"], simp)
apply (rule Ex_I [where x="Var x'"], simp)
apply (rule Ex_I [where x="Var y"], simp)
apply (blast intro: Mem_Eats_I1)
apply (rule All_E [where x="Var z", THEN rotate6], simp)
apply (rule Iff_E2)
apply (rule Ex_I [where x="Var x"], simp)
apply (rule Ex_I [where x="Var x'"], simp)
apply (rule Ex_I [where x="Var y"])
apply (auto intro: Mem_Eats_I1)
apply (rule Swap [THEN rotate5])
apply (rule Ex_I [where x="Var x"], simp)
apply (rule Ex_I [where x="Var x'"], simp)
apply (rule Ex_I [where x="Var y"], simp)
apply (blast intro: Sym Mem_Eats_I1)
done
qed
lemma exists_ShiftP:
assumes t: "atom t ♯ (s,k,del)"
shows "H ⊢ Ex t (ShiftP s k del (Var t))"
proof -
obtain i::name and j::name
where i: "atom (i::name) ♯ (s,t,k,del)" and j: "atom (j::name) ♯ (i,s,t,k,del)"
by (metis obtain_fresh)
have "{} ⊢ Ex t (ShiftP (Var i) k del (Var t))" (is "{} ⊢ ?scheme")
proof (rule Ind [of j])
show "atom j ♯ (i, ?scheme)" using j
by simp
next
show "{} ⊢ ?scheme(i::=Zero)" using i t
by (auto intro!: Ex_I [where x=Zero] simp: ShiftP_Zero)
next
obtain x::name and x'::name and y::name
where atoms: "atom x ♯ (x',y,s,k,del,t,i,j)" "atom x' ♯ (y,s,k,del,t,i,j)"
"atom y ♯ (s,k,del,t,i,j)"
by (metis obtain_fresh)
let ?caseA = "Ex x (Ex x' (Ex y ((Var j) EQ HPair (Var x) (Var y) AND Var x IN k AND
HaddP del (Var x) (Var x'))))"
show "{} ⊢ All i (All j (?scheme IMP ?scheme(i::=Var j) IMP ?scheme(i::=Eats (Var i) (Var j))))"
using i j atoms
apply (auto del: Ex_EH)
apply (rule Ex_E)
apply (auto del: Ex_EH)
apply (rule Ex_E)
apply (auto del: Ex_EH)
apply (rule thin1, auto)
proof (rule Cases [where A="?caseA"])
show "{?caseA, ShiftP (Var i) k del (Var t)}
⊢ Ex t (ShiftP (Eats (Var i) (Var j)) k del (Var t))"
using i j t atoms
apply (auto simp del: ShiftP.simps)
apply (rule Ex_I [where x="Eats (Var t) (HPair (Var x') (Var y))"], auto)
apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same, THEN rotate3])
apply (auto intro: ShiftP_Eats_Eats [THEN cut3])
done
next
show "{Neg ?caseA, ShiftP (Var i) k del (Var t)}
⊢ Ex t (ShiftP (Eats (Var i) (Var j)) k del (Var t))"
using atoms
by (auto intro!: Ex_I [where x="Var t"] ShiftP_Eats_Neg [of x x' y, THEN cut2]
simp: ShiftP_Zero)
qed
qed
hence "{} ⊢ (Ex t (ShiftP (Var i) k del (Var t)))(i::=s)"
by (blast intro: Subst)
thus ?thesis using i t
by (auto intro: thin0)
qed
section ‹Union of Two Sets›
nominal_function UnionP :: "tm ⇒ tm ⇒ tm ⇒ fm"
where "atom i ♯ (x,y,z) ⟹ UnionP x y z = All i (Var i IN z IFF (Var i IN x OR Var i IN y))"
by (auto simp: eqvt_def UnionP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)
nominal_termination (eqvt)
by lexicographic_order
lemma UnionP_fresh_iff [simp]: "a ♯ UnionP x y z ⟷ a ♯ x ∧ a ♯ y ∧ a ♯ z"
proof -
obtain i::name where "atom i ♯ (x,y,z)"
by (metis obtain_fresh)
thus ?thesis
by auto
qed
lemma subst_fm_UnionP [simp]:
"(UnionP x y z)(i::=u) = UnionP (subst i u x) (subst i u y) (subst i u z)"
proof -
obtain j::name where "atom j ♯ (x,y,z,i,u)"
by (metis obtain_fresh)
thus ?thesis
by (auto simp: UnionP.simps [of j])
qed
lemma Union_Zero1: "H ⊢ UnionP Zero x x"
proof -
obtain i::name where "atom i ♯ x"
by (metis obtain_fresh)
hence "{} ⊢ UnionP Zero x x"
by (auto simp: UnionP.simps [of i] intro: Disj_I2)
thus ?thesis
by (metis thin0)
qed
lemma Union_Eats: "{UnionP x y z} ⊢ UnionP (Eats x a) y (Eats z a)"
proof -
obtain i::name where "atom i ♯ (x,y,z,a)"
by (metis obtain_fresh)
thus ?thesis
apply (auto simp: UnionP.simps [of i])
apply (rule Ex_I [where x="Var i"])
apply (auto intro: Iff_E1 [THEN rotate2] Iff_E2 [THEN rotate2] Mem_Eats_I1 Mem_Eats_I2 Disj_I1 Disj_I2)
done
qed
lemma exists_Union_lemma:
assumes z: "atom z ♯ (i,y)" and i: "atom i ♯ y"
shows "{} ⊢ Ex z (UnionP (Var i) y (Var z))"
proof -
obtain j::name where j: "atom j ♯ (y,z,i)"
by (metis obtain_fresh)
show "{} ⊢ Ex z (UnionP (Var i) y (Var z))"
apply (rule Ind [of j i]) using j z i
apply simp_all
apply (rule Ex_I [where x=y], simp add: Union_Zero1)
apply (auto del: Ex_EH)
apply (rule Ex_E)
apply (rule NegNeg_E)
apply (rule Ex_E)
apply (auto del: Ex_EH)
apply (rule thin1, force intro: Ex_I [where x="Eats (Var z) (Var j)"] Union_Eats)
done
qed
lemma exists_UnionP:
assumes z: "atom z ♯ (x,y)" shows "H ⊢ Ex z (UnionP x y (Var z))"
proof -
obtain i::name where i: "atom i ♯ (y,z)"
by (metis obtain_fresh)
hence "{} ⊢ Ex z (UnionP (Var i) y (Var z))"
by (metis exists_Union_lemma fresh_Pair fresh_at_base(2) z)
hence "{} ⊢ (Ex z (UnionP (Var i) y (Var z)))(i::=x)"
by (metis Subst empty_iff)
thus ?thesis using i z
by (simp add: thin0)
qed
lemma UnionP_Mem1: "{ UnionP x y z, a IN x } ⊢ a IN z"
proof -
obtain i::name where "atom i ♯ (x,y,z,a)"
by (metis obtain_fresh)
thus ?thesis
by (force simp: UnionP.simps [of i] intro: All_E [where x=a] Disj_I1 Iff_E2)
qed
lemma UnionP_Mem2: "{ UnionP x y z, a IN y } ⊢ a IN z"
proof -
obtain i::name where "atom i ♯ (x,y,z,a)"
by (metis obtain_fresh)
thus ?thesis
by (force simp: UnionP.simps [of i] intro: All_E [where x=a] Disj_I2 Iff_E2)
qed
lemma UnionP_Mem: "{ UnionP x y z, a IN z } ⊢ a IN x OR a IN y"
proof -
obtain i::name where "atom i ♯ (x,y,z,a)"
by (metis obtain_fresh)
thus ?thesis
by (force simp: UnionP.simps [of i] intro: All_E [where x=a] Iff_E1)
qed
lemma UnionP_Mem_E:
assumes "H ⊢ UnionP x y z"
and "insert (a IN x) H ⊢ A"
and "insert (a IN y) H ⊢ A"
shows "insert (a IN z) H ⊢ A"
using assms
by (blast intro: rotate2 cut_same [OF UnionP_Mem [THEN cut2]] thin1)
section ‹Append on Sequences›
nominal_function SeqAppendP :: "tm ⇒ tm ⇒ tm ⇒ tm ⇒ tm ⇒ fm"
where "⟦atom g1 ♯ (g2,f1,k1,f2,k2,g); atom g2 ♯ (f1,k1,f2,k2,g)⟧ ⟹
SeqAppendP f1 k1 f2 k2 g =
(Ex g1 (Ex g2 (RestrictedP f1 k1 (Var g1) AND
ShiftP f2 k2 k1 (Var g2) AND
UnionP (Var g1) (Var g2) g)))"
by (auto simp: eqvt_def SeqAppendP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)
nominal_termination (eqvt)
by lexicographic_order
lemma SeqAppendP_fresh_iff [simp]:
"a ♯ SeqAppendP f1 k1 f2 k2 g ⟷ a ♯ f1 ∧ a ♯ k1 ∧ a ♯ f2 ∧ a ♯ k2 ∧ a ♯ g"
proof -
obtain g1::name and g2::name
where "atom g1 ♯ (g2,f1,k1,f2,k2,g)" "atom g2 ♯ (f1,k1,f2,k2,g)"
by (metis obtain_fresh)
thus ?thesis
by auto
qed
lemma subst_fm_SeqAppendP [simp]:
"(SeqAppendP f1 k1 f2 k2 g)(i::=u) =
SeqAppendP (subst i u f1) (subst i u k1) (subst i u f2) (subst i u k2) (subst i u g)"
proof -
obtain g1::name and g2::name
where "atom g1 ♯ (g2,f1,k1,f2,k2,g,i,u)" "atom g2 ♯ (f1,k1,f2,k2,g,i,u)"
by (metis obtain_fresh)
thus ?thesis
by (auto simp: SeqAppendP.simps [of g1 g2])
qed
lemma exists_SeqAppendP:
assumes "atom g ♯ (f1,k1,f2,k2)"
shows "H ⊢ Ex g (SeqAppendP f1 k1 f2 k2 (Var g))"
proof -
obtain g1::name and g2::name
where atoms: "atom g1 ♯ (g2,f1,k1,f2,k2,g)" "atom g2 ♯ (f1,k1,f2,k2,g)"
by (metis obtain_fresh)
hence "{} ⊢ Ex g (SeqAppendP f1 k1 f2 k2 (Var g))"
using assms
apply (auto simp: SeqAppendP.simps [of g1 g2])
apply (rule cut_same [OF exists_RestrictedP [of g1 f1 k1]], auto)
apply (rule cut_same [OF exists_ShiftP [of g2 f2 k2 k1]], auto)
apply (rule cut_same [OF exists_UnionP [of g "Var g1" "Var g2"]], auto)
apply (rule Ex_I [where x="Var g"], simp)
apply (rule Ex_I [where x="Var g1"], simp)
apply (rule Ex_I [where x="Var g2"], auto)
done
thus ?thesis using assms
by (metis thin0)
qed
lemma SeqAppendP_Mem1: "{SeqAppendP f1 k1 f2 k2 g, HPair x y IN f1, x IN k1} ⊢ HPair x y IN g"
proof -
obtain g1::name and g2::name
where "atom g1 ♯ (g2,f1,k1,f2,k2,g,x,y)" "atom g2 ♯ (f1,k1,f2,k2,g,x,y)"
by (metis obtain_fresh)
thus ?thesis
by (auto simp: SeqAppendP.simps [of g1 g2] intro: UnionP_Mem1 [THEN cut2] RestrictedP_Mem [THEN cut3])
qed
lemma SeqAppendP_Mem2: "{SeqAppendP f1 k1 f2 k2 g, HaddP k1 x x', x IN k2, HPair x y IN f2} ⊢ HPair x' y IN g"
proof -
obtain g1::name and g2::name
where "atom g1 ♯ (g2,f1,k1,f2,k2,g,x,x',y)" "atom g2 ♯ (f1,k1,f2,k2,g,x,x',y)"
by (metis obtain_fresh)
thus ?thesis
by (auto simp: SeqAppendP.simps [of g1 g2] intro: UnionP_Mem2 [THEN cut2] ShiftP_Mem1 [THEN cut4])
qed
lemma SeqAppendP_Mem_E:
assumes "H ⊢ SeqAppendP f1 k1 f2 k2 g"
and "insert (HPair x y IN f1) (insert (x IN k1) H) ⊢ A"
and "insert (HPair (Var u) y IN f2) (insert (HaddP k1 (Var u) x) (insert (Var u IN k2) H)) ⊢ A"
and u: "atom u ♯ (f1,k1,f2,k2,x,y,g,A)" "∀C ∈ H. atom u ♯ C"
shows "insert (HPair x y IN g) H ⊢ A"
proof -
obtain g1::name and g2::name
where atoms: "atom g1 ♯ (g2,f1,k1,f2,k2,g,x,y,u)" "atom g2 ♯ (f1,k1,f2,k2,g,x,y,u)"
by (metis obtain_fresh)
hence "{SeqAppendP f1 k1 f2 k2 g, HPair x y IN g}
⊢ (HPair x y IN f1 AND x IN k1) OR Ex u ((Var u) IN k2 AND HaddP k1 (Var u) x AND HPair (Var u) y IN f2)"
using u
apply (auto simp: SeqAppendP.simps [of g1 g2])
apply (rule UnionP_Mem_E [THEN rotate4])
apply (rule AssumeH)+
apply (blast intro: Disj_I1 cut_same [OF RestrictedP_Mem2 [THEN cut2]])
apply (rule Disj_I2)
apply (rule cut_same [OF ShiftP_Mem2 [where u=u, THEN cut2]])
defer 1
apply force+
done
thus ?thesis
apply (rule cut_same [OF _ [THEN cut2]])
using assms
apply (auto intro: thin1 rotate2 thin3 thin4)
done
qed
section ‹LstSeqP and SeqAppendP›
lemma HDomain_Incl_SeqAppendP:
"{SeqAppendP f1 k1 f2 k2 g, HDomain_Incl f1 k1 AND HDomain_Incl f2 k2,
HaddP k1 k2 k, OrdP k1} ⊢ HDomain_Incl g k"
proof -
obtain x::name and y::name and z::name and i::name
where "atom x ♯ (f1,k1,f2,k2,g,k,y,z,i)" "atom y ♯ (f1,k1,f2,k2,g,k,z,i)"
"atom z ♯ (f1,k1,f2,k2,g,k,i)" "atom i ♯ (f1,k1,f2,k2,g,k)"
by (metis obtain_fresh)
thus ?thesis
apply (auto simp: HDomain_Incl.simps [of x _ _ y z])
apply (rule HaddP_Mem_cases [where i=i, THEN rotate2], auto)
apply (rule All_E' [where x = "Var x"], blast, auto)
apply (rule ContraProve [THEN rotate4])
apply (rule Ex_I [where x = "Var y"], auto)
apply (rule Ex_I [where x = "Var z"], auto)
apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same, THEN rotate2], simp)
apply (rule SeqAppendP_Mem1 [THEN cut3], auto)
apply (rule Mem_cong [OF Assume Refl, THEN Iff_MP_same], auto)
apply (rule Ex_I [where x = "Var i"], auto)
apply (rule ContraProve [THEN rotate5])
apply (rule Ex_I [where x = "Var y"], simp)
apply (rule Ex_I [where x = "HPair (Var x) (Var y)"], auto)
apply (blast intro: SeqAppendP_Mem2 [THEN cut4] Mem_cong [OF _ Refl, THEN Iff_MP_same])
done
qed
declare SeqAppendP.simps [simp del]
lemma HFun_Sigma_SeqAppendP:
"{SeqAppendP f1 k1 f2 k2 g, HFun_Sigma f1, HFun_Sigma f2, OrdP k1} ⊢ HFun_Sigma g"
proof -
obtain x::name and y::name and z::name
and x'::name and y'::name and z'::name and g1::name and g2::name
and v::name and v'::name and w::name
where atoms:
"atom v ♯ (v',w,g1,g2,z,z',x,y,x',y',f1,k1,f2,k2,g)" "atom v' ♯ (w,g1,g2,z,z',x,y,x',y',f1,k1,f2,k2,g)"
"atom w ♯ (g1,g2,z,z',x,y,x',y',f1,k1,f2,k2,g)"
"atom g1 ♯ (g2,z,z',x,y,x',y',f1,k1,f2,k2,g)" "atom g2 ♯ (z,z',x,y,x',y',f1,k1,f2,k2,g)"
"atom z ♯ (z',x,y,x',y',f1,k1,f2,k2,g)" "atom z' ♯ (x,y,x',y',f1,k1,f2,k2,g)"
"atom x ♯ (y,x',y',f1,k1,f2,k2,g)" "atom y ♯ (x',y',f1,k1,f2,k2,g)"
"atom x' ♯ (y',f1,k1,f2,k2,g)" "atom y' ♯ (f1,k1,f2,k2,g)"
by (metis obtain_fresh)
thus ?thesis
apply (simp add: HFun_Sigma.simps [of z g z' x y x' y'] SeqAppendP.simps [of g1 g2])
apply (rule Ex_EH Conj_EH All_I Imp_I)+
apply (rule cut_same [OF UnionP_Mem [where a = "Var z", THEN cut2]])
apply (rule AssumeH)+
apply (rule Disj_E)
apply (rule cut_same [OF UnionP_Mem [where a = "Var z'", THEN cut2]])
apply (rule AssumeH)+
apply (rule thin1 [where A="UnionP (Var g1) (Var g2) g", THEN rotate6])
apply (rule Disj_E)
apply (rule thin1 [where A="ShiftP f2 k2 k1 (Var g2)", THEN rotate5])
apply (rule RestrictedP_Mem_D [where a = "Var z"])
apply (rule AssumeH)+
apply (rule RestrictedP_Mem_D [where a = "Var z'"])
apply (rule AssumeH)+
apply (simp add: HFun_Sigma.simps [of z f1 z' x y x' y'])
apply (rule All2_E [where x = "Var z", THEN rotate8], simp_all, blast)
apply (rule All2_E [where x = "Var z'"], simp_all, blast)
apply (rule Ex_EH Conj_EH)+
apply simp_all
apply (rule Ex_I [where x="Var x"], simp)
apply (rule Ex_I [where x="Var y"], simp)
apply (rule Ex_I [where x="Var x'"], simp)
apply (rule Ex_I [where x="Var y'"], simp)
apply (rule Conj_I, blast)+
apply blast
apply (rule RestrictedP_Mem_D [where a = "Var z"])
apply (rule AssumeH)+
apply (rule thin1 [where A="Var z IN g", THEN rotate5])
apply (rule thin1 [where A="Var z' IN g", THEN rotate4])
apply (rule cut_same [OF HFun_Sigma_Mem_imp_HPair [of _ f1 "Var z" x y]], simp_all)
apply (rule AssumeH)+
apply (rule cut_same [OF ShiftP_Mem_D [where x=v and x'=v' and y=w]])
apply (rule AssumeH Ex_EH Conj_EH)+
apply auto [3]
apply (rule AssumeH Ex_EH Conj_EH)+
apply simp_all
apply (rule Ex_I [where x="Var x"], simp)
apply (rule Ex_I [where x="Var y"], simp)
apply (rule Ex_I [where x="Var v'"], simp)
apply (rule Ex_I [where x="Var w"], simp)
apply auto [1]
apply (blast intro: Mem_HFun_Sigma_OrdP [THEN cut2] Mem_cong [OF _ Refl, THEN Iff_MP_same])
apply (blast intro: Hyp HaddP_OrdP)
apply (rule cut_same [OF RestrictedP_Mem2 [THEN cut2]])
apply (rule AssumeH)+
apply (blast intro: Mem_cong [OF _ Refl, THEN Iff_MP_same])
apply (blast intro: Hyp Mem_cong [OF _ Refl, THEN Iff_MP_same] HaddP_Mem_contra)
apply (rule cut_same [OF UnionP_Mem [where a = "Var z'", THEN cut2]])
apply (rule AssumeH)+
apply (rule thin1 [where A="UnionP (Var g1) (Var g2) g", THEN rotate6])
apply (rule Disj_E)
apply (rule RestrictedP_Mem_D [where a = "Var z'"])
apply (rule AssumeH)+
apply (rule thin1 [where A="Var z IN g", THEN rotate5])
apply (rule thin1 [where A="Var z' IN g", THEN rotate4])
apply (rule cut_same [OF HFun_Sigma_Mem_imp_HPair [of _ f1 "Var z'" x y]], simp_all)
apply (rule AssumeH)+
apply (rule cut_same [OF ShiftP_Mem_D [where x=v and x'=v' and y=w]])
apply (rule AssumeH Ex_EH Conj_EH)+
apply auto [3]
apply (rule AssumeH Ex_EH Conj_EH)+
apply simp_all
apply (rule Ex_I [where x="Var v'"], simp)
apply (rule Ex_I [where x="Var w"], simp)
apply (rule Ex_I [where x="Var x"], simp)
apply (rule Ex_I [where x="Var y"], simp)
apply auto [1]
apply (blast intro: Hyp HaddP_OrdP)
apply (blast intro: Mem_HFun_Sigma_OrdP [THEN cut2] Mem_cong [OF _ Refl, THEN Iff_MP_same])
apply (rule cut_same [OF RestrictedP_Mem2 [THEN cut2]])
apply (rule AssumeH)+
apply (blast intro: Mem_cong [OF _ Refl, THEN Iff_MP_same])
apply (blast intro: Mem_cong [OF _ Refl, THEN Iff_MP2_same] HaddP_Mem_contra Hyp)
apply (rule cut_same [OF ShiftP_Mem_D [where x=x and x'=x' and y=y and a = "Var z"]])
apply (rule AssumeH Ex_EH Conj_EH)+
apply simp_all
apply (rule cut_same [OF ShiftP_Mem_D [where x=v and x'=v' and y=w and a = "Var z'"]])
apply (rule AssumeH Ex_EH Conj_EH)+
apply simp_all
apply (rule thin1 [where A="ShiftP f2 k2 k1 (Var g2)", THEN rotate7])
apply (rule thin1 [where A="RestrictedP f1 k1 (Var g1)", THEN rotate7])
apply (rule AssumeH Ex_EH Conj_EH)+
apply simp_all
apply (rule Ex_I [where x="Var x'"], simp)
apply (rule Ex_I [where x="Var y"], simp)
apply (rule Ex_I [where x="Var v'"], simp)
apply (rule Ex_I [where x="Var w"], auto intro: Hyp HaddP_OrdP)
apply (rule cut_same [where A="Var x EQ Var v"])
apply (blast intro: HaddP_inv2 [THEN cut3] HaddP_cong [OF Refl Refl, THEN Iff_MP_same] Hyp)
apply (rule HFun_Sigma_E [where r=f2])
apply (auto intro: Hyp Var_Eq_subst_Iff [THEN Iff_MP_same])
done
qed
lemma LstSeqP_SeqAppendP:
assumes "H ⊢ SeqAppendP f1 (SUCC k1) f2 (SUCC k2) g"
"H ⊢ LstSeqP f1 k1 y1" "H ⊢ LstSeqP f2 k2 y2" "H ⊢ HaddP k1 k2 k"
shows "H ⊢ LstSeqP g (SUCC k) y2"
proof -
have "{SeqAppendP f1 (SUCC k1) f2 (SUCC k2) g, LstSeqP f1 k1 y1, LstSeqP f2 k2 y2, HaddP k1 k2 k}
⊢ LstSeqP g (SUCC k) y2"
apply (auto simp: LstSeqP.simps intro: HaddP_OrdP OrdP_SUCC_I)
apply (rule HDomain_Incl_SeqAppendP [THEN cut4])
apply (rule AssumeH Conj_I)+
apply (blast intro: HaddP_SUCC1 [THEN cut1] HaddP_SUCC2 [THEN cut1])
apply (blast intro: HaddP_OrdP OrdP_SUCC_I)
apply (rule HFun_Sigma_SeqAppendP [THEN cut4])
apply (auto intro: HaddP_OrdP OrdP_SUCC_I)
apply (blast intro: Mem_SUCC_Refl HaddP_SUCC1 [THEN cut1] HaddP_SUCC2 [THEN cut1]
SeqAppendP_Mem2 [THEN cut4])
done
thus ?thesis using assms
by (rule cut4)
qed
lemma SeqAppendP_NotInDom: "{SeqAppendP f1 k1 f2 k2 g, HaddP k1 k2 k, OrdP k1} ⊢ NotInDom k g"
proof -
obtain x::name and z::name
where "atom x ♯ (z,f1,k1,f2,k2,g,k)" "atom z ♯ (f1,k1,f2,k2,g,k)"
by (metis obtain_fresh)
thus ?thesis
apply (auto simp: NotInDom.simps [of z])
apply (rule SeqAppendP_Mem_E [where u=x])
apply (rule AssumeH)+
apply (blast intro: HaddP_Mem_contra, simp_all)
apply (rule cut_same [where A="(Var x) EQ k2"])
apply (blast intro: HaddP_inv2 [THEN cut3])
apply (blast intro: Mem_non_refl [where x=k2] Mem_cong [OF _ Refl, THEN Iff_MP_same])
done
qed
lemma LstSeqP_SeqAppendP_Eats:
assumes "H ⊢ SeqAppendP f1 (SUCC k1) f2 (SUCC k2) g"
"H ⊢ LstSeqP f1 k1 y1" "H ⊢ LstSeqP f2 k2 y2" "H ⊢ HaddP k1 k2 k"
shows "H ⊢ LstSeqP (Eats g (HPair (SUCC (SUCC k)) z)) (SUCC (SUCC k)) z"
proof -
have "{SeqAppendP f1 (SUCC k1) f2 (SUCC k2) g, LstSeqP f1 k1 y1, LstSeqP f2 k2 y2, HaddP k1 k2 k}
⊢ LstSeqP (Eats g (HPair (SUCC (SUCC k)) z)) (SUCC (SUCC k)) z"
apply (rule cut2 [OF NotInDom_LstSeqP_Eats])
apply (rule SeqAppendP_NotInDom [THEN cut3])
apply (rule AssumeH)
apply (metis HaddP_SUCC1 HaddP_SUCC2 cut1 thin1)
apply (metis Assume LstSeqP_OrdP OrdP_SUCC_I insert_commute)
apply (blast intro: LstSeqP_SeqAppendP)
done
thus ?thesis using assms
by (rule cut4)
qed
section ‹Substitution and Abstraction on Terms›
subsection ‹Atomic cases›
lemma SeqStTermP_Var_same:
assumes "atom s ♯ (k,v,i)" "atom k ♯ (v,i)"
shows "{VarP v} ⊢ Ex s (Ex k (SeqStTermP v i v i (Var s) (Var k)))"
proof -
obtain l::name and sl::name and sl'::name and m::name and sm::name and sm'::name
and n::name and sn::name and sn'::name
where "atom l ♯ (v,i,s,k,sl,sl',m,n,sm,sm',sn,sn')"
"atom sl ♯ (v,i,s,k,sl',m,n,sm,sm',sn,sn')"
"atom sl' ♯ (v,i,s,k,m,n,sm,sm',sn,sn')"
"atom m ♯ (v,i,s,k,n,sm,sm',sn,sn')" "atom n ♯ (v,i,s,k,sm,sm',sn,sn')"
"atom sm ♯ (v,i,s,k,sm',sn,sn')" "atom sm' ♯ (v,i,s,k,sn,sn')"
"atom sn ♯ (v,i,s,k,sn')" "atom sn' ♯ (v,i,s,k)"
by (metis obtain_fresh)
thus ?thesis using assms
apply (simp add: SeqStTermP.simps [of l _ _ v i sl sl' m n sm sm' sn sn'])
apply (rule Ex_I [where x = "Eats Zero (HPair Zero (HPair v i))"], simp)
apply (rule Ex_I [where x = Zero], auto intro!: Mem_SUCC_EH)
apply (rule Ex_I [where x = v], simp)
apply (rule Ex_I [where x = i], auto intro: Disj_I1 Mem_Eats_I2 HPair_cong)
done
qed
lemma SeqStTermP_Var_diff:
assumes "atom s ♯ (k,v,w,i)" "atom k ♯ (v,w,i)"
shows "{VarP v, VarP w, Neg (v EQ w) } ⊢ Ex s (Ex k (SeqStTermP v i w w (Var s) (Var k)))"
proof -
obtain l::name and sl::name and sl'::name and m::name and sm::name and sm'::name
and n::name and sn::name and sn'::name
where "atom l ♯ (v,w,i,s,k,sl,sl',m,n,sm,sm',sn,sn')"
"atom sl ♯ (v,w,i,s,k,sl',m,n,sm,sm',sn,sn')"
"atom sl' ♯ (v,w,i,s,k,m,n,sm,sm',sn,sn')"
"atom m ♯ (v,w,i,s,k,n,sm,sm',sn,sn')" "atom n ♯ (v,w,i,s,k,sm,sm',sn,sn')"
"atom sm ♯ (v,w,i,s,k,sm',sn,sn')" "atom sm' ♯ (v,w,i,s,k,sn,sn')"
"atom sn ♯ (v,w,i,s,k,sn')" "atom sn' ♯ (v,w,i,s,k)"
by (metis obtain_fresh)
thus ?thesis using assms
apply (simp add: SeqStTermP.simps [of l _ _ v i sl sl' m n sm sm' sn sn'])
apply (rule Ex_I [where x = "Eats Zero (HPair Zero (HPair w w))"], simp)
apply (rule Ex_I [where x = Zero], auto intro!: Mem_SUCC_EH)
apply (rule rotate2 [OF Swap])
apply (rule Ex_I [where x = w], simp)
apply (rule Ex_I [where x = w], auto simp: VarP_def)
apply (blast intro: HPair_cong Mem_Eats_I2)
apply (blast intro: Sym OrdNotEqP_I Disj_I1 Disj_I2)
done
qed
lemma SeqStTermP_Zero:
assumes "atom s ♯ (k,v,i)" "atom k ♯ (v,i)"
shows "{VarP v} ⊢ Ex s (Ex k (SeqStTermP v i Zero Zero (Var s) (Var k)))"
proof -
obtain l::name and sl::name and sl'::name and m::name and sm::name and sm'::name
and n::name and sn::name and sn'::name
where "atom l ♯ (v,i,s,k,sl,sl',m,n,sm,sm',sn,sn')"
"atom sl ♯ (v,i,s,k,sl',m,n,sm,sm',sn,sn')"
"atom sl' ♯ (v,i,s,k,m,n,sm,sm',sn,sn')"
"atom m ♯ (v,i,s,k,n,sm,sm',sn,sn')" "atom n ♯ (v,i,s,k,sm,sm',sn,sn')"
"atom sm ♯ (v,i,s,k,sm',sn,sn')" "atom sm' ♯ (v,i,s,k,sn,sn')"
"atom sn ♯ (v,i,s,k,sn')" "atom sn' ♯ (v,i,s,k)"
by (metis obtain_fresh)
thus ?thesis using assms
apply (simp add: SeqStTermP.simps [of l _ _ v i sl sl' m n sm sm' sn sn'])
apply (rule Ex_I [where x = "Eats Zero (HPair Zero (HPair Zero Zero))"], simp)
apply (rule Ex_I [where x = Zero], auto intro!: Mem_SUCC_EH)
apply (rule Ex_I [where x = Zero], simp)
apply (rule Ex_I [where x = Zero], simp)
apply (rule Conj_I)
apply (force intro: Var_Eq_subst_Iff [THEN Iff_MP_same] Mem_Eats_I2)
apply (force simp: VarP_def OrdNotEqP.simps intro: Disj_I1 Disj_I2)
done
qed
corollary SubstTermP_Zero: "{TermP t} ⊢ SubstTermP «Var v» t Zero Zero"
proof -
obtain s::name and k::name where "atom s ♯ (v,t,k)" "atom k ♯ (v,t)"
by (metis obtain_fresh)
thus ?thesis
by (auto simp: SubstTermP.simps [of s _ _ _ _ k] intro: SeqStTermP_Zero [THEN cut1])
qed
corollary SubstTermP_Var_same: "{VarP v, TermP t} ⊢ SubstTermP v t v t"
proof -
obtain s::name and k::name where "atom s ♯ (v,t,k)" "atom k ♯ (v,t)"
by (metis obtain_fresh)
thus ?thesis
by (auto simp: SubstTermP.simps [of s _ _ _ _ k] intro: SeqStTermP_Var_same [THEN cut1])
qed
corollary SubstTermP_Var_diff: "{VarP v, VarP w, Neg (v EQ w), TermP t} ⊢ SubstTermP v t w w"
proof -
obtain s::name and k::name where "atom s ♯ (v,w,t,k)" "atom k ♯ (v,w,t)"
by (metis obtain_fresh)
thus ?thesis
by (auto simp: SubstTermP.simps [of s _ _ _ _ k] intro: SeqStTermP_Var_diff [THEN cut3])
qed
lemma SeqStTermP_Ind:
assumes "atom s ♯ (k,v,t,i)" "atom k ♯ (v,t,i)"
shows "{VarP v, IndP t} ⊢ Ex s (Ex k (SeqStTermP v i t t (Var s) (Var k)))"
proof -
obtain l::name and sl::name and sl'::name and m::name and sm::name and sm'::name
and n::name and sn::name and sn'::name
where "atom l ♯ (v,t,i,s,k,sl,sl',m,n,sm,sm',sn,sn')"
"atom sl ♯ (v,t,i,s,k,sl',m,n,sm,sm',sn,sn')"
"atom sl' ♯ (v,t,i,s,k,m,n,sm,sm',sn,sn')"
"atom m ♯ (v,t,i,s,k,n,sm,sm',sn,sn')" "atom n ♯ (v,t,i,s,k,sm,sm',sn,sn')"
"atom sm ♯ (v,t,i,s,k,sm',sn,sn')" "atom sm' ♯ (v,t,i,s,k,sn,sn')"
"atom sn ♯ (v,t,i,s,k,sn')" "atom sn' ♯ (v,t,i,s,k)"
by (metis obtain_fresh)
thus ?thesis using assms
apply (simp add: SeqStTermP.simps [of l _ _ v i sl sl' m n sm sm' sn sn'])
apply (rule Ex_I [where x = "Eats Zero (HPair Zero (HPair t t))"], simp)
apply (rule Ex_I [where x = Zero], auto intro!: Mem_SUCC_EH)
apply (rule Ex_I [where x = t], simp)
apply (rule Ex_I [where x = t], auto intro: HPair_cong Mem_Eats_I2)
apply (blast intro: Disj_I1 Disj_I2 VarP_neq_IndP)
done
qed
corollary SubstTermP_Ind: "{VarP v, IndP w, TermP t} ⊢ SubstTermP v t w w"
proof -
obtain s::name and k::name where "atom s ♯ (v,w,t,k)" "atom k ♯ (v,w,t)"
by (metis obtain_fresh)
thus ?thesis
by (force simp: SubstTermP.simps [of s _ _ _ _ k]
intro: SeqStTermP_Ind [THEN cut2])
qed
subsection ‹Non-atomic cases›
lemma SeqStTermP_Eats:
assumes sk: "atom s ♯ (k,s1,s2,k1,k2,t1,t2,u1,u2,v,i)"
"atom k ♯ (t1,t2,u1,u2,v,i)"
shows "{SeqStTermP v i t1 u1 s1 k1, SeqStTermP v i t2 u2 s2 k2}
⊢ Ex s (Ex k (SeqStTermP v i (Q_Eats t1 t2) (Q_Eats u1 u2) (Var s) (Var k)))"
proof -
obtain km::name and kn::name and j::name and k'::name and l::name and sl::name and sl'::name
and m::name and n::name and sm::name and sm'::name and sn::name and sn'::name
where atoms2: "atom km ♯ (s1,s2,s,k1,k2,k,t1,t2,u1,u2,v,i,kn,j,k',l,sl,sl',m,n,sm,sm',sn,sn')"
"atom kn ♯ (s1,s2,s,k1,k2,k,t1,t2,u1,u2,v,i,j,k',l,sl,sl',m,n,sm,sm',sn,sn')"
"atom j ♯ (s1,s2,s,k1,k2,k,t1,t2,u1,u2,v,i,k',l,sl,sl',m,n,sm,sm',sn,sn')"
and atoms: "atom k' ♯ (s1,s2,s,k1,k2,k,t1,t2,u1,u2,v,i,l,sl,sl',m,n,sm,sm',sn,sn')"
"atom l ♯ (s1,s2,s,k1,k2,k,t1,t2,u1,u2,v,i,sl,sl',m,n,sm,sm',sn,sn')"
"atom sl ♯ (s1,s2,s,k1,k2,k,t1,t2,u1,u2,v,i,sl',m,n,sm,sm',sn,sn')"
"atom sl'♯ (s1,s2,s,k1,k2,k,t1,t2,u1,u2,v,i,m,n,sm,sm',sn,sn')"
"atom m ♯ (s1,s2,s,k1,k2,k,t1,t2,u1,u2,v,i,n,sm,sm',sn,sn')"
"atom n ♯ (s1,s2,s,k1,k2,k,t1,t2,u1,u2,v,i,sm,sm',sn,sn')"
"atom sm ♯ (s1,s2,s,k1,k2,k,t1,t2,u1,u2,v,i,sm',sn,sn')"
"atom sm'♯ (s1,s2,s,k1,k2,k,t1,t2,u1,u2,v,i,sn,sn')"
"atom sn ♯ (s1,s2,s,k1,k2,k,t1,t2,u1,u2,v,i,sn')"
"atom sn'♯ (s1,s2,s,k1,k2,k,t1,t2,u1,u2,v,i)"
by (metis obtain_fresh)
let ?hyp = "{HaddP k1 k2 (Var k'), OrdP k1, OrdP k2, SeqAppendP s1 (SUCC k1) s2 (SUCC k2) (Var s), SeqStTermP v i t1 u1 s1 k1, SeqStTermP v i t2 u2 s2 k2}"
show ?thesis
using sk atoms
apply (auto simp: SeqStTermP.simps [of l "Var s" _ _ _ sl sl' m n sm sm' sn sn'])
apply (rule cut_same [where A="OrdP k1 AND OrdP k2"])
apply (metis Conj_I SeqStTermP_imp_OrdP thin1 thin2)
apply (rule cut_same [OF exists_SeqAppendP [of s s1 "SUCC k1" s2 "SUCC k2"]])
apply (rule AssumeH Ex_EH Conj_EH | simp)+
apply (rule cut_same [OF exists_HaddP [where j=k' and x=k1 and y=k2]])
apply (rule AssumeH Ex_EH Conj_EH | simp)+
apply (rule Ex_I [where x="Eats (Var s) (HPair (SUCC (SUCC (Var k'))) (HPair (Q_Eats t1 t2) (Q_Eats u1 u2)))"])
apply (simp_all (no_asm_simp))
apply (rule Ex_I [where x="SUCC (SUCC (Var k'))"], simp)
apply (rule Conj_I [OF _ Conj_I])
apply (metis SeqStTermP_imp_VarP thin1)
apply (blast intro: LstSeqP_SeqAppendP_Eats SeqStTermP_imp_LstSeqP [THEN cut1])
proof (rule All2_SUCC_I, simp_all)
show "?hyp ⊢ Ex sl (Ex sl'
(HPair (SUCC (SUCC (Var k'))) (HPair (Var sl) (Var sl')) IN Eats (Var s) (HPair (SUCC (SUCC (Var k'))) (HPair (Q_Eats t1 t2) (Q_Eats u1 u2))) AND
((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR
Ex m (Ex n (Ex sm (Ex sm' (Ex sn (Ex sn'
(Var m IN SUCC (SUCC (Var k')) AND
Var n IN SUCC (SUCC (Var k')) AND
HPair (Var m) (HPair (Var sm) (Var sm')) IN Eats (Var s) (HPair (SUCC (SUCC (Var k'))) (HPair (Q_Eats t1 t2) (Q_Eats u1 u2))) AND
HPair (Var n) (HPair (Var sn) (Var sn')) IN Eats (Var s) (HPair (SUCC (SUCC (Var k'))) (HPair (Q_Eats t1 t2) (Q_Eats u1 u2))) AND
Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))"
apply (rule Ex_I [where x="Q_Eats t1 t2"])
using sk atoms apply simp
apply (rule Ex_I [where x="Q_Eats u1 u2"], simp)
apply (rule Conj_I, metis Mem_Eats_I2 Refl)
apply (rule Disj_I2)
apply (rule Ex_I [where x=k1], simp)
apply (rule Ex_I [where x="SUCC (Var k')"], simp)
apply (rule Ex_I [where x=t1], simp)
apply (rule Ex_I [where x=u1], simp)
apply (rule Ex_I [where x=t2], simp)
apply (rule Ex_I [where x=u2], simp)
apply (rule Conj_I)
apply (blast intro: HaddP_Mem_I LstSeqP_OrdP Mem_SUCC_I1)
apply (rule Conj_I [OF Mem_SUCC_Refl Conj_I])
apply (blast intro: Mem_Eats_I1 SeqAppendP_Mem1 [THEN cut3] Mem_SUCC_Refl SeqStTermP_imp_LstSeqP [THEN cut1]
LstSeqP_imp_Mem)
apply (blast intro: Mem_Eats_I1 SeqAppendP_Mem2 [THEN cut4] Mem_SUCC_Refl SeqStTermP_imp_LstSeqP [THEN cut1]
HaddP_SUCC1 [THEN cut1] LstSeqP_imp_Mem)
done
next
show "?hyp ⊢ All2 l (SUCC (SUCC (Var k')))
(Ex sl (Ex sl'
(HPair (Var l) (HPair (Var sl) (Var sl')) IN Eats (Var s) (HPair (SUCC (SUCC (Var k'))) (HPair (Q_Eats t1 t2) (Q_Eats u1 u2))) AND
((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR
Ex m (Ex n (Ex sm (Ex sm' (Ex sn (Ex sn'
(Var m IN Var l AND
Var n IN Var l AND
HPair (Var m) (HPair (Var sm) (Var sm')) IN Eats (Var s) (HPair (SUCC (SUCC (Var k'))) (HPair (Q_Eats t1 t2) (Q_Eats u1 u2))) AND
HPair (Var n) (HPair (Var sn) (Var sn')) IN Eats (Var s) (HPair (SUCC (SUCC (Var k'))) (HPair (Q_Eats t1 t2) (Q_Eats u1 u2))) AND
Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn')))))))))))"
apply (rule cut_same [where A="HaddP (SUCC k1) (SUCC k2) (SUCC (SUCC (Var k')))"])
apply (blast intro: HaddP_SUCC1 [THEN cut1] HaddP_SUCC2 [THEN cut1])
apply (rule All_I Imp_I)+
apply (rule HaddP_Mem_cases [where i=j])
using sk atoms atoms2 apply simp_all
apply (rule AssumeH)
apply (blast intro: OrdP_SUCC_I LstSeqP_OrdP)
apply (simp add: SeqStTermP.simps [of l s1 _ _ _ sl sl' m n sm sm' sn sn'])
apply (rule AssumeH Ex_EH Conj_EH)+
apply (rule All2_E [THEN rotate2])
apply (simp | rule AssumeH Ex_EH Conj_EH)+
apply (rule Ex_I [where x="Var sl"], simp)
apply (rule Ex_I [where x="Var sl'"], simp)
apply (rule Conj_I)
apply (metis Mem_Eats_I1 SeqAppendP_Mem1 rotate3 thin2 thin4)
apply (rule AssumeH Disj_IE1H Ex_EH Conj_EH)+
apply (rule Ex_I [where x="Var m"], simp)
apply (rule Ex_I [where x="Var n"], simp)
apply (rule Ex_I [where x="Var sm"], simp)
apply (rule Ex_I [where x="Var sm'"], simp)
apply (rule Ex_I [where x="Var sn"], simp)
apply (rule Ex_I [where x="Var sn'"], simp_all)
apply (rule Conj_I, rule AssumeH)+
apply (blast del: Disj_EH intro: OrdP_Trans [OF OrdP_SUCC_I] Mem_Eats_I1 [OF SeqAppendP_Mem1 [THEN cut3]] Hyp)
apply (simp add: SeqStTermP.simps [of l s2 _ _ _ sl sl' m n sm sm' sn sn'])
apply (rule AssumeH Ex_EH Conj_EH)+
apply (rule All2_E [THEN rotate2])
apply (simp | rule AssumeH Ex_EH Conj_EH)+
apply (rule Ex_I [where x="Var sl"], simp)
apply (rule Ex_I [where x="Var sl'"], simp)
apply (rule cut_same [where A="OrdP (Var j)"])
apply (metis HaddP_imp_OrdP rotate2 thin2)
apply (rule Conj_I)
apply (blast intro: Mem_Eats_I1 SeqAppendP_Mem2 [THEN cut4] del: Disj_EH)
apply (rule AssumeH Disj_IE1H Ex_EH Conj_EH)+
apply simp_all
apply (rule cut_same [OF exists_HaddP [where j=km and x="SUCC k1" and y="Var m"]])
apply (blast intro!: Ord_IN_Ord, simp)
apply (rule cut_same [OF exists_HaddP [where j=kn and x="SUCC k1" and y="Var n"]])
apply (blast intro!: Ord_IN_Ord, simp)
apply (rule AssumeH Ex_EH Conj_EH | simp)+
apply (rule Ex_I [where x="Var km"], simp)
apply (rule Ex_I [where x="Var kn"], simp)
apply (rule Ex_I [where x="Var sm"], simp)
apply (rule Ex_I [where x="Var sm'"], simp)
apply (rule Ex_I [where x="Var sn"], simp)
apply (rule Ex_I [where x="Var sn'"], simp_all)
apply (rule Conj_I [OF _ Conj_I])
apply (blast intro!: HaddP_Mem_cancel_left [THEN Iff_MP2_same] OrdP_SUCC_I intro: LstSeqP_OrdP Hyp)+
apply (blast intro: OrdP_Trans Hyp Mem_Eats_I1 SeqAppendP_Mem2 [THEN cut4] HaddP_imp_OrdP [THEN cut1])
done
qed
qed
theorem SubstTermP_Eats:
"{SubstTermP v i t1 u1, SubstTermP v i t2 u2} ⊢ SubstTermP v i (Q_Eats t1 t2) (Q_Eats u1 u2)"
proof -
obtain k1::name and s1::name and k2::name and s2::name and k::name and s::name
where "atom s1 ♯ (v,i,t1,u1,t2,u2)" "atom k1 ♯ (v,i,t1,u1,t2,u2,s1)"
"atom s2 ♯ (v,i,t1,u1,t2,u2,k1,s1)" "atom k2 ♯ (v,i,t1,u1,t2,u2,s2,k1,s1)"
"atom s ♯ (v,i,t1,u1,t2,u2,k2,s2,k1,s1)"
"atom k ♯ (v,i,t1,u1,t2,u2,s,k2,s2,k1,s1)"
by (metis obtain_fresh)
thus ?thesis
by (auto intro!: SeqStTermP_Eats [THEN cut2]
simp: SubstTermP.simps [of s _ _ _ "(Q_Eats u1 u2)" k]
SubstTermP.simps [of s1 v i t1 u1 k1]
SubstTermP.simps [of s2 v i t2 u2 k2])
qed
subsection ‹Substitution over a constant›
lemma SeqConstP_lemma:
assumes "atom m ♯ (s,k,c,n,sm,sn)" "atom n ♯ (s,k,c,sm,sn)"
"atom sm ♯ (s,k,c,sn)" "atom sn ♯ (s,k,c)"
shows "{ SeqConstP s k c }
⊢ c EQ Zero OR
Ex m (Ex n (Ex sm (Ex sn (Var m IN k AND Var n IN k AND
SeqConstP s (Var m) (Var sm) AND
SeqConstP s (Var n) (Var sn) AND
c EQ Q_Eats (Var sm) (Var sn)))))"
proof -
obtain l::name and sl::name where "atom l ♯ (s,k,c,sl,m,n,sm,sn)" "atom sl ♯ (s,k,c,m,n,sm,sn)"
by (metis obtain_fresh)
thus ?thesis using assms
apply (simp add: SeqCTermP.simps [of l s k sl m n sm sn])
apply (rule Conj_EH)+
apply (rule All2_SUCC_E [THEN rotate2], auto del: Disj_EH)
apply (rule cut_same [where A = "c EQ (Var sl)"])
apply (metis Assume AssumeH(4) LstSeqP_EQ)
apply (rule Disj_EH)
apply (blast intro: Disj_I1 Sym Trans)
apply (auto intro!: Disj_I2)
apply (rule Ex_I [where x = "Var m"], simp)
apply (rule Ex_I [where x = "Var n"], simp)
apply (rule Ex_I [where x = "Var sm"], simp)
apply (rule Ex_I [where x = "Var sn"], simp)
apply (simp_all add: SeqCTermP.simps [of l s _ sl m n sm sn])
apply ((rule Conj_I)+, blast intro: LstSeqP_Mem)+
apply (rule All2_Subset [OF Hyp], blast)
apply (blast intro!: SUCC_Subset_Ord LstSeqP_OrdP, blast, simp)
apply ((rule Conj_I)+, blast intro: LstSeqP_Mem)+
apply (rule All2_Subset [OF Hyp], blast)
apply (blast intro!: SUCC_Subset_Ord LstSeqP_OrdP, blast, simp)
apply (blast intro: Trans)
done
qed
lemma SeqConstP_imp_SubstTermP: "{SeqConstP s kk c, TermP t} ⊢ SubstTermP «Var w» t c c"
proof -
obtain j::name and k::name and l::name and sl::name and m::name and n::name and sm::name and sn::name
where atoms: "atom j ♯ (s,kk,c,t,k,l,sl,m,n,sm,sn)" "atom k ♯ (s,kk,c,t,l,sl,m,n,sm,sn)"
"atom l ♯ (s,kk,c,t,sl,m,n,sm,sn)" "atom sl ♯ (s,kk,c,t,m,n,sm,sn)"
"atom m ♯ (s,kk,c,t,n,sm,sn)" "atom n ♯ (s,kk,c,t,sm,sn)"
"atom sm ♯ (s,kk,c,t,sn)" "atom sn ♯ (s,kk,c,t)"
by (metis obtain_fresh)
have "{ OrdP (Var k), TermP t } ⊢ All j (SeqConstP s (Var k) (Var j) IMP SubstTermP «Var w» t (Var j) (Var j))"
(is "_ ⊢ ?scheme")
proof (rule OrdIndH [where j=l])
show "atom l ♯ (k, ?scheme)" using atoms
by simp
next
show "{TermP t} ⊢ All k (OrdP (Var k) IMP (All2 l (Var k) (?scheme(k::= Var l)) IMP ?scheme))"
using atoms apply auto
apply (rule Swap)
apply (rule cut_same)
apply (rule cut1 [OF SeqConstP_lemma [of m s "Var k" "Var j" n sm sn]], auto)
apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same])
apply (auto intro: SubstTermP_Zero [THEN cut1])
apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same, THEN rotate2], simp)
apply (rule SubstTermP_Eats [THEN cut2])
apply (rule All2_E' [OF Hyp, where x="Var m"], blast+, simp_all)
apply (force intro: All_E [where x="Var sm"])
apply (rule All2_E' [OF Hyp, where x="Var n"], blast+, simp_all)
apply (rule All_E [where x="Var sn"], auto)
done
qed
hence "{OrdP (Var k), TermP t} ⊢ (SeqConstP s (Var k) (Var j) IMP SubstTermP «Var w» t (Var j) (Var j))(j::=c)"
by (metis All_D)
hence "{TermP t} ⊢ (SeqConstP s (Var k) c IMP SubstTermP «Var w» t c c)"
using atoms by simp (metis Imp_cut SeqCTermP_imp_OrdP)
hence "{TermP t} ⊢ (SeqConstP s (Var k) c IMP SubstTermP «Var w» t c c)(k::=kk)"
using atoms by (force intro!: Subst)
thus ?thesis
using atoms by (simp add: anti_deduction)
qed
theorem SubstTermP_Const: "{ConstP c, TermP t} ⊢ SubstTermP «Var w» t c c"
proof -
obtain s::name and k::name where "atom s ♯ (c,t,w,k)" "atom k ♯ (c,t,w)"
by (metis obtain_fresh)
thus ?thesis
by (auto simp: CTermP.simps [of k s c] SeqConstP_imp_SubstTermP)
qed
section ‹Substitution on Formulas›
subsection ‹Membership›
lemma SubstAtomicP_Mem:
"{SubstTermP v i x x', SubstTermP v i y y'} ⊢ SubstAtomicP v i (Q_Mem x y) (Q_Mem x' y')"
proof -
obtain t::name and u::name and t'::name and u'::name
where "atom t ♯ (v,i,x,x',y,y',t',u,u')" "atom t' ♯ (v,i,x,x',y,y',u,u')"
"atom u ♯ (v,i,x,x',y,y',u')" "atom u' ♯ (v,i,x,x',y,y')"
by (metis obtain_fresh)
thus ?thesis
apply (simp add: SubstAtomicP.simps [of t _ _ _ _ t' u u'])
apply (rule Ex_I [where x = x], simp)
apply (rule Ex_I [where x = y], simp)
apply (rule Ex_I [where x = x'], simp)
apply (rule Ex_I [where x = y'], auto intro: Disj_I2)
done
qed
lemma SeqSubstFormP_Mem:
assumes "atom s ♯ (k,x,y,x',y',v,i)" "atom k ♯ (x,y,x',y',v,i)"
shows "{SubstTermP v i x x', SubstTermP v i y y'}
⊢ Ex s (Ex k (SeqSubstFormP v i (Q_Mem x y) (Q_Mem x' y') (Var s) (Var k)))"
proof -
let ?vs = "(s,k,x,y,x',y',v,i)"
obtain l::name and sl::name and sl'::name and m::name and n::name and sm::name and sm'::name and sn::name and sn'::name
where "atom l ♯ (?vs,sl,sl',m,n,sm,sm',sn,sn')"
"atom sl ♯ (?vs,sl',m,n,sm,sm',sn,sn')" "atom sl' ♯ (?vs,m,n,sm,sm',sn,sn')"
"atom m ♯ (?vs,n,sm,sm',sn,sn')" "atom n ♯ (?vs,sm,sm',sn,sn')"
"atom sm ♯ (?vs,sm',sn,sn')" "atom sm' ♯ (?vs,sn,sn')"
"atom sn ♯ (?vs,sn')" "atom sn' ♯ ?vs"
by (metis obtain_fresh)
thus ?thesis
using assms
apply (auto simp: SeqSubstFormP.simps [of l "Var s" _ _ _ sl sl' m n sm sm' sn sn'])
apply (rule Ex_I [where x = "Eats Zero (HPair Zero (HPair (Q_Mem x y) (Q_Mem x' y')))"], simp)
apply (rule Ex_I [where x = Zero], auto intro!: Mem_SUCC_EH)
apply (rule Ex_I [where x = "Q_Mem x y"], simp)
apply (rule Ex_I [where x = "Q_Mem x' y'"], auto intro: Mem_Eats_I2 HPair_cong)
apply (blast intro: SubstAtomicP_Mem [THEN cut2] Disj_I1)
done
qed
lemma SubstFormP_Mem:
"{SubstTermP v i x x', SubstTermP v i y y'} ⊢ SubstFormP v i (Q_Mem x y) (Q_Mem x' y')"
proof -
obtain k1::name and s1::name and k2::name and s2::name and k::name and s::name
where "atom s1 ♯ (v,i,x,y,x',y')" "atom k1 ♯ (v,i,x,y,x',y',s1)"
"atom s2 ♯ (v,i,x,y,x',y',k1,s1)" "atom k2 ♯ (v,i,x,y,x',y',s2,k1,s1)"
"atom s ♯ (v,i,x,y,x',y',k2,s2,k1,s1)" "atom k ♯ (v,i,x,y,x',y',s,k2,s2,k1,s1)"
by (metis obtain_fresh)
thus ?thesis
by (auto simp: SubstFormP.simps [of s v i "(Q_Mem x y)" _ k]
SubstFormP.simps [of s1 v i x x' k1]
SubstFormP.simps [of s2 v i y y' k2]
intro: SubstTermP_imp_TermP SubstTermP_imp_VarP SeqSubstFormP_Mem thin1)
qed
subsection ‹Equality›
lemma SubstAtomicP_Eq:
"{SubstTermP v i x x', SubstTermP v i y y'} ⊢ SubstAtomicP v i (Q_Eq x y) (Q_Eq x' y')"
proof -
obtain t::name and u::name and t'::name and u'::name
where "atom t ♯ (v,i,x,x',y,y',t',u,u')" "atom t' ♯ (v,i,x,x',y,y',u,u')"
"atom u ♯ (v,i,x,x',y,y',u')" "atom u' ♯ (v,i,x,x',y,y')"
by (metis obtain_fresh)
thus ?thesis
apply (simp add: SubstAtomicP.simps [of t _ _ _ _ t' u u'])
apply (rule Ex_I [where x = x], simp)
apply (rule Ex_I [where x = y], simp)
apply (rule Ex_I [where x = x'], simp)
apply (rule Ex_I [where x = y'], auto intro: Disj_I1)
done
qed
lemma SeqSubstFormP_Eq:
assumes sk: "atom s ♯ (k,x,y,x',y',v,i)" "atom k ♯ (x,y,x',y',v,i)"
shows "{SubstTermP v i x x', SubstTermP v i y y'}
⊢ Ex s (Ex k (SeqSubstFormP v i (Q_Eq x y) (Q_Eq x' y') (Var s) (Var k)))"
proof -
let ?vs = "(s,k,x,y,x',y',v,i)"
obtain l::name and sl::name and sl'::name and m::name and n::name and sm::name and sm'::name and sn::name and sn'::name
where "atom l ♯ (?vs,sl,sl',m,n,sm,sm',sn,sn')"
"atom sl ♯ (?vs,sl',m,n,sm,sm',sn,sn')" "atom sl' ♯ (?vs,m,n,sm,sm',sn,sn')"
"atom m ♯ (?vs,n,sm,sm',sn,sn')" "atom n ♯ (?vs,sm,sm',sn,sn')"
"atom sm ♯ (?vs,sm',sn,sn')" "atom sm' ♯ (?vs,sn,sn')"
"atom sn ♯ (?vs,sn')" "atom sn' ♯ ?vs"
by (metis obtain_fresh)
thus ?thesis
using sk
apply (auto simp: SeqSubstFormP.simps [of l "Var s" _ _ _ sl sl' m n sm sm' sn sn'])
apply (rule Ex_I [where x = "Eats Zero (HPair Zero (HPair (Q_Eq x y) (Q_Eq x' y')))"], simp)
apply (rule Ex_I [where x = Zero], auto intro!: Mem_SUCC_EH)
apply (rule Ex_I [where x = "Q_Eq x y"], simp)
apply (rule Ex_I [where x = "Q_Eq x' y'"], auto)
apply (metis Mem_Eats_I2 Assume HPair_cong Refl)
apply (blast intro: SubstAtomicP_Eq [THEN cut2] Disj_I1)
done
qed
lemma SubstFormP_Eq:
"{SubstTermP v i x x', SubstTermP v i y y'} ⊢ SubstFormP v i (Q_Eq x y) (Q_Eq x' y')"
proof -
obtain k1::name and s1::name and k2::name and s2::name and k::name and s::name
where "atom s1 ♯ (v,i,x,y,x',y')" "atom k1 ♯ (v,i,x,y,x',y',s1)"
"atom s2 ♯ (v,i,x,y,x',y',k1,s1)" "atom k2 ♯ (v,i,x,y,x',y',s2,k1,s1)"
"atom s ♯ (v,i,x,y,x',y',k2,s2,k1,s1)" "atom k ♯ (v,i,x,y,x',y',s,k2,s2,k1,s1)"
by (metis obtain_fresh)
thus ?thesis
by (auto simp: SubstFormP.simps [of s v i "(Q_Eq x y)" _ k]
SubstFormP.simps [of s1 v i x x' k1]
SubstFormP.simps [of s2 v i y y' k2]
intro: SeqSubstFormP_Eq SubstTermP_imp_TermP SubstTermP_imp_VarP thin1)
qed
subsection ‹Negation›
lemma SeqSubstFormP_Neg:
assumes "atom s ♯ (k,s1,k1,x,x',v,i)" "atom k ♯ (s1,k1,x,x',v,i)"
shows "{SeqSubstFormP v i x x' s1 k1, TermP i, VarP v}
⊢ Ex s (Ex k (SeqSubstFormP v i (Q_Neg x) (Q_Neg x') (Var s) (Var k)))"
proof -
let ?vs = "(s1,k1,s,k,x,x',v,i)"
obtain l::name and sl::name and sl'::name and m::name and n::name and
sm::name and sm'::name and sn::name and sn'::name
where atoms:
"atom l ♯ (?vs,sl,sl',m,n,sm,sm',sn,sn')"
"atom sl ♯ (?vs,sl',m,n,sm,sm',sn,sn')" "atom sl' ♯ (?vs,m,n,sm,sm',sn,sn')"
"atom m ♯ (?vs,n,sm,sm',sn,sn')" "atom n ♯ (?vs,sm,sm',sn,sn')"
"atom sm ♯ (?vs,sm',sn,sn')" "atom sm' ♯ (?vs,sn,sn')"
"atom sn ♯ (?vs,sn')" "atom sn' ♯ ?vs"
by (metis obtain_fresh)
let ?hyp = "{RestrictedP s1 (SUCC k1) (Var s), OrdP k1, SeqSubstFormP v i x x' s1 k1, TermP i, VarP v}"
show ?thesis
using assms atoms
apply (auto simp: SeqSubstFormP.simps [of l "Var s" _ _ _ sl sl' m n sm sm' sn sn'])
apply (rule cut_same [where A="OrdP k1"])
apply (metis SeqSubstFormP_imp_OrdP thin2)
apply (rule cut_same [OF exists_RestrictedP [of s s1 "SUCC k1"]])
apply (rule AssumeH Ex_EH Conj_EH | simp)+
apply (rule Ex_I [where x="Eats (Var s) (HPair (SUCC k1) (HPair (Q_Neg x) (Q_Neg x')))"])
apply (simp_all (no_asm_simp))
apply (rule Ex_I [where x="(SUCC k1)"])
apply (simp add: flip_fresh_fresh)
apply (rule Conj_I)
apply (blast intro: RestrictedP_LstSeqP_Eats [THEN cut2] SeqSubstFormP_imp_LstSeqP [THEN cut1])
proof (rule All2_SUCC_I, simp_all)
show "?hyp ⊢ Ex sl (Ex sl'
(HPair (SUCC k1) (HPair (Var sl) (Var sl')) IN Eats (Var s) (HPair (SUCC k1) (HPair (Q_Neg x) (Q_Neg x'))) AND
(SubstAtomicP v i (Var sl) (Var sl') OR
Ex m (Ex n
(Ex sm (Ex sm'
(Ex sn (Ex sn'
(Var m IN SUCC k1 AND
Var n IN SUCC k1 AND
HPair (Var m) (HPair (Var sm) (Var sm')) IN Eats (Var s) (HPair (SUCC k1) (HPair (Q_Neg x) (Q_Neg x'))) AND
HPair (Var n) (HPair (Var sn) (Var sn')) IN Eats (Var s) (HPair (SUCC k1) (HPair (Q_Neg x) (Q_Neg x'))) AND
(Var sl EQ Q_Disj (Var sm) (Var sn) AND Var sl' EQ Q_Disj (Var sm') (Var sn') OR
Var sl EQ Q_Neg (Var sm) AND Var sl' EQ Q_Neg (Var sm') OR Var sl EQ Q_Ex (Var sm) AND Var sl' EQ Q_Ex (Var sm')))))))))))"
apply (rule Ex_I [where x="Q_Neg x"])
using assms atoms apply simp
apply (rule Ex_I [where x="Q_Neg x'"], simp)
apply (rule Conj_I, metis Mem_Eats_I2 Refl)
apply (rule Disj_I2)
apply (rule Ex_I [where x=k1], simp)
apply (rule Ex_I [where x=k1], simp)
apply (rule Ex_I [where x=x], simp)
apply (rule_tac x=x' in Ex_I, simp)
apply (rule Ex_I [where x=x], simp)
apply (rule_tac x=x' in Ex_I, simp)
apply (rule Conj_I [OF Mem_SUCC_Refl])+
apply (blast intro: Disj_I1 Disj_I2 Mem_Eats_I1 RestrictedP_Mem [THEN cut3] Mem_SUCC_Refl
SeqSubstFormP_imp_LstSeqP [THEN cut1] LstSeqP_imp_Mem)
done
next
show "?hyp ⊢ All2 l (SUCC k1)
(Ex sl (Ex sl'
(HPair (Var l) (HPair (Var sl) (Var sl')) IN Eats (Var s) (HPair (SUCC k1) (HPair (Q_Neg x) (Q_Neg x'))) AND
(SubstAtomicP v i (Var sl) (Var sl') OR
Ex m (Ex n
(Ex sm (Ex sm'
(Ex sn (Ex sn'
(Var m IN Var l AND
Var n IN Var l AND
HPair (Var m) (HPair (Var sm) (Var sm')) IN Eats (Var s) (HPair (SUCC k1) (HPair (Q_Neg x) (Q_Neg x'))) AND
HPair (Var n) (HPair (Var sn) (Var sn')) IN Eats (Var s) (HPair (SUCC k1) (HPair (Q_Neg x) (Q_Neg x'))) AND
(Var sl EQ Q_Disj (Var sm) (Var sn) AND Var sl' EQ Q_Disj (Var sm') (Var sn') OR
Var sl EQ Q_Neg (Var sm) AND Var sl' EQ Q_Neg (Var sm') OR Var sl EQ Q_Ex (Var sm) AND Var sl' EQ Q_Ex (Var sm'))))))))))))"
apply (rule All_I Imp_I)+
using assms atoms apply simp_all
apply (simp add: SeqSubstFormP.simps [of l s1 _ _ _ sl sl' m n sm sm' sn sn'])
apply (rule AssumeH Ex_EH Conj_EH)+
apply (rule All2_E [THEN rotate2], auto del: Disj_EH)
apply (rule Ex_I [where x="Var sl"], simp)
apply (rule Ex_I [where x="Var sl'"], simp)
apply (rule Conj_I)
apply (blast intro: Mem_Eats_I1 [OF RestrictedP_Mem [THEN cut3]] del: Disj_EH)
apply (rule AssumeH Disj_IE1H Ex_EH Conj_EH)+
apply (rule Ex_I [where x="Var m"], simp)
apply (rule Ex_I [where x="Var n"], simp)
apply (rule Ex_I [where x="Var sm"], simp)
apply (rule Ex_I [where x="Var sm'"], simp)
apply (rule Ex_I [where x="Var sn"], simp)
apply (rule Ex_I [where x="Var sn'"], auto del: Disj_EH)
apply (blast intro: Mem_Eats_I1 [OF RestrictedP_Mem [THEN cut3]] OrdP_Trans [OF OrdP_SUCC_I])+
done
qed
qed
theorem SubstFormP_Neg: "{SubstFormP v i x x'} ⊢ SubstFormP v i (Q_Neg x) (Q_Neg x')"
proof -
obtain k1::name and s1::name and k::name and s::name
where "atom s1 ♯ (v,i,x,x')" "atom k1 ♯ (v,i,x,x',s1)"
"atom s ♯ (v,i,x,x',k1,s1)" "atom k ♯ (v,i,x,x',s,k1,s1)"
by (metis obtain_fresh)
thus ?thesis
by (force simp: SubstFormP.simps [of s v i "Q_Neg x" _ k] SubstFormP.simps [of s1 v i x x' k1]
intro: SeqSubstFormP_Neg [THEN cut3])
qed
subsection ‹Disjunction›
lemma SeqSubstFormP_Disj:
assumes "atom s ♯ (k,s1,s2,k1,k2,x,y,x',y',v,i)" "atom k ♯ (s1,s2,k1,k2,x,y,x',y',v,i)"
shows "{SeqSubstFormP v i x x' s1 k1,
SeqSubstFormP v i y y' s2 k2, TermP i, VarP v}
⊢ Ex s (Ex k (SeqSubstFormP v i (Q_Disj x y) (Q_Disj x' y') (Var s) (Var k)))"
proof -
let ?vs = "(s1,s2,s,k1,k2,k,x,y,x',y',v,i)"
obtain km::name and kn::name and j::name and k'::name
and l::name and sl::name and sl'::name and m::name and n::name
and sm::name and sm'::name and sn::name and sn'::name
where atoms2: "atom km ♯ (kn,j,k',l,s1,s2,s,k1,k2,k,x,y,x',y',v,i,sl,sl',m,n,sm,sm',sn,sn')"
"atom kn ♯ (j,k',l,s1,s2,s,k1,k2,k,x,y,x',y',v,i,sl,sl',m,n,sm,sm',sn,sn')"
"atom j ♯ (k',l,s1,s2,s,k1,k2,k,x,y,x',y',v,i,sl,sl',m,n,sm,sm',sn,sn')"
and atoms: "atom k' ♯ (l,s1,s2,s,k1,k2,k,x,y,x',y',v,i,sl,sl',m,n,sm,sm',sn,sn')"
"atom l ♯ (s1,s2,s,k1,k2,k,x,y,x',y',v,i,sl,sl',m,n,sm,sm',sn,sn')"
"atom sl ♯ (s1,s2,s,k1,k2,k,x,y,x',y',v,i,sl',m,n,sm,sm',sn,sn')"
"atom sl' ♯ (s1,s2,s,k1,k2,k,x,y,x',y',v,i,m,n,sm,sm',sn,sn')"
"atom m ♯ (s1,s2,s,k1,k2,k,x,y,x',y',v,i,n,sm,sm',sn,sn')"
"atom n ♯ (s1,s2,s,k1,k2,k,x,y,x',y',v,i,sm,sm',sn,sn')"
"atom sm ♯ (s1,s2,s,k1,k2,k,x,y,x',y',v,i,sm',sn,sn')"
"atom sm' ♯ (s1,s2,s,k1,k2,k,x,y,x',y',v,i,sn,sn')"
"atom sn ♯ (s1,s2,s,k1,k2,k,x,y,x',y',v,i,sn')"
"atom sn' ♯ (s1,s2,s,k1,k2,k,x,y,x',y',v,i)"
by (metis obtain_fresh)
let ?hyp = "{HaddP k1 k2 (Var k'), OrdP k1, OrdP k2, SeqAppendP s1 (SUCC k1) s2 (SUCC k2) (Var s),
SeqSubstFormP v i x x' s1 k1, SeqSubstFormP v i y y' s2 k2, TermP i, VarP v}"
show ?thesis
using assms atoms
apply (auto simp: SeqSubstFormP.simps [of l "Var s" _ _ _ sl sl' m n sm sm' sn sn'])
apply (rule cut_same [where A="OrdP k1 AND OrdP k2"])
apply (metis Conj_I SeqSubstFormP_imp_OrdP thin1 thin2)
apply (rule cut_same [OF exists_SeqAppendP [of s s1 "SUCC k1" s2 "SUCC k2"]])
apply (rule AssumeH Ex_EH Conj_EH | simp)+
apply (rule cut_same [OF exists_HaddP [where j=k' and x=k1 and y=k2]])
apply (rule AssumeH Ex_EH Conj_EH | simp)+
apply (rule Ex_I [where x="Eats (Var s) (HPair (SUCC(SUCC(Var k'))) (HPair(Q_Disj x y)(Q_Disj x' y')))"])
apply (simp_all (no_asm_simp))
apply (rule Ex_I [where x="SUCC (SUCC (Var k'))"], simp)
apply (rule Conj_I)
apply (blast intro: LstSeqP_SeqAppendP_Eats SeqSubstFormP_imp_LstSeqP [THEN cut1])
proof (rule All2_SUCC_I, simp_all)
show "?hyp ⊢ Ex sl (Ex sl'
(HPair (SUCC (SUCC (Var k'))) (HPair (Var sl) (Var sl')) IN
Eats (Var s) (HPair (SUCC (SUCC (Var k'))) (HPair (Q_Disj x y) (Q_Disj x' y'))) AND
(SubstAtomicP v i (Var sl) (Var sl') OR
Ex m (Ex n (Ex sm (Ex sm' (Ex sn (Ex sn'
(Var m IN SUCC (SUCC (Var k')) AND
Var n IN SUCC (SUCC (Var k')) AND
HPair (Var m) (HPair (Var sm) (Var sm')) IN
Eats (Var s) (HPair (SUCC (SUCC (Var k'))) (HPair (Q_Disj x y) (Q_Disj x' y'))) AND
HPair (Var n) (HPair (Var sn) (Var sn')) IN
Eats (Var s) (HPair (SUCC (SUCC (Var k'))) (HPair (Q_Disj x y) (Q_Disj x' y'))) AND
(Var sl EQ Q_Disj (Var sm) (Var sn) AND Var sl' EQ Q_Disj (Var sm') (Var sn') OR
Var sl EQ Q_Neg (Var sm) AND Var sl' EQ Q_Neg (Var sm') OR Var sl EQ Q_Ex (Var sm) AND Var sl' EQ Q_Ex (Var sm')))))))))))"
apply (rule Ex_I [where x="Q_Disj x y"])
using assms atoms apply simp
apply (rule Ex_I [where x="Q_Disj x' y'"], simp)
apply (rule Conj_I, metis Mem_Eats_I2 Refl)
apply (rule Disj_I2)
apply (rule Ex_I [where x=k1], simp)
apply (rule Ex_I [where x="SUCC (Var k')"], simp)
apply (rule Ex_I [where x=x], simp)
apply (rule_tac x=x' in Ex_I, simp)
apply (rule Ex_I [where x=y], simp)
apply (rule_tac x=y' in Ex_I, simp)
apply (rule Conj_I)
apply (blast intro: HaddP_Mem_I LstSeqP_OrdP Mem_SUCC_I1)
apply (rule Conj_I [OF Mem_SUCC_Refl])
apply (blast intro: Disj_I1 Mem_Eats_I1 Mem_SUCC_Refl SeqSubstFormP_imp_LstSeqP [THEN cut1]
LstSeqP_imp_Mem SeqAppendP_Mem1 [THEN cut3] SeqAppendP_Mem2 [THEN cut4] HaddP_SUCC1 [THEN cut1])
done
next
show "?hyp ⊢ All2 l (SUCC (SUCC (Var k')))
(Ex sl
(Ex sl'
(HPair (Var l) (HPair (Var sl) (Var sl')) IN
Eats (Var s) (HPair (SUCC (SUCC (Var k'))) (HPair (Q_Disj x y) (Q_Disj x' y'))) AND
(SubstAtomicP v i (Var sl) (Var sl') OR
Ex m (Ex n
(Ex sm (Ex sm'
(Ex sn (Ex sn'
(Var m IN Var l AND
Var n IN Var l AND
HPair (Var m) (HPair (Var sm) (Var sm')) IN
Eats (Var s) (HPair (SUCC (SUCC (Var k'))) (HPair (Q_Disj x y) (Q_Disj x' y'))) AND
HPair (Var n) (HPair (Var sn) (Var sn')) IN
Eats (Var s) (HPair (SUCC (SUCC (Var k'))) (HPair (Q_Disj x y) (Q_Disj x' y'))) AND
(Var sl EQ Q_Disj (Var sm) (Var sn) AND Var sl' EQ Q_Disj (Var sm') (Var sn') OR
Var sl EQ Q_Neg (Var sm) AND Var sl' EQ Q_Neg (Var sm') OR Var sl EQ Q_Ex (Var sm) AND Var sl' EQ Q_Ex (Var sm'))))))))))))"
apply (rule cut_same [where A="HaddP (SUCC k1) (SUCC k2) (SUCC (SUCC (Var k')))"])
apply (blast intro: HaddP_SUCC1 [THEN cut1] HaddP_SUCC2 [THEN cut1])
apply (rule All_I Imp_I)+
apply (rule HaddP_Mem_cases [where i=j])
using assms atoms atoms2 apply simp_all
apply (rule AssumeH)
apply (blast intro: OrdP_SUCC_I LstSeqP_OrdP)
apply (simp add: SeqSubstFormP.simps [of l s1 _ _ _ sl sl' m n sm sm' sn sn'])
apply (rule AssumeH Ex_EH Conj_EH)+
apply (rule All2_E [THEN rotate2])
apply (simp | rule AssumeH Ex_EH Conj_EH)+
apply (rule Ex_I [where x="Var sl"], simp)
apply (rule Ex_I [where x="Var sl'"], simp)
apply (rule Conj_I [OF Mem_Eats_I1])
apply (metis SeqAppendP_Mem1 rotate3 thin2 thin4)
apply (rule AssumeH Disj_IE1H Ex_EH Conj_EH)+
apply (rule Ex_I [where x="Var m"], simp)
apply (rule Ex_I [where x="Var n"], simp)
apply (rule Ex_I [where x="Var sm"], simp)
apply (rule Ex_I [where x="Var sm'"], simp)
apply (rule Ex_I [where x="Var sn"], simp)
apply (rule Ex_I [where x="Var sn'"], simp_all (no_asm_simp))
apply (rule Conj_I, rule AssumeH)+
apply (rule Conj_I)
apply (blast intro: OrdP_Trans [OF OrdP_SUCC_I] Mem_Eats_I1 [OF SeqAppendP_Mem1 [THEN cut3]] Hyp)
apply (blast intro: Disj_I1 Disj_I2 OrdP_Trans [OF OrdP_SUCC_I] Mem_Eats_I1 [OF SeqAppendP_Mem1 [THEN cut3]] Hyp)
apply (simp add: SeqSubstFormP.simps [of l s2 _ _ _ sl sl' m n sm sm' sn sn'])
apply (rule AssumeH Ex_EH Conj_EH)+
apply (rule All2_E [THEN rotate2])
apply (simp | rule AssumeH Ex_EH Conj_EH)+
apply (rule Ex_I [where x="Var sl"], simp)
apply (rule Ex_I [where x="Var sl'"], simp)
apply (rule cut_same [where A="OrdP (Var j)"])
apply (metis HaddP_imp_OrdP rotate2 thin2)
apply (rule Conj_I)
apply (blast intro: Mem_Eats_I1 SeqAppendP_Mem2 [THEN cut4] del: Disj_EH)
apply (rule AssumeH Disj_IE1H Ex_EH Conj_EH)+
apply (rule cut_same [OF exists_HaddP [where j=km and x="SUCC k1" and y="Var m"]])
apply (blast intro: Ord_IN_Ord, simp)
apply (rule cut_same [OF exists_HaddP [where j=kn and x="SUCC k1" and y="Var n"]])
apply (metis AssumeH(6) Ord_IN_Ord0 rotate8, simp)
apply (rule AssumeH Ex_EH Conj_EH | simp)+
apply (rule Ex_I [where x="Var km"], simp)
apply (rule Ex_I [where x="Var kn"], simp)
apply (rule Ex_I [where x="Var sm"], simp)
apply (rule Ex_I [where x="Var sm'"], simp)
apply (rule Ex_I [where x="Var sn"], simp)
apply (rule Ex_I [where x="Var sn'"], simp_all (no_asm_simp))
apply (rule Conj_I [OF _ Conj_I])
apply (blast intro!: HaddP_Mem_cancel_left [THEN Iff_MP2_same] OrdP_SUCC_I intro: LstSeqP_OrdP Hyp)+
apply (blast del: Disj_EH intro: OrdP_Trans Hyp
intro!: Mem_Eats_I1 SeqAppendP_Mem2 [THEN cut4] HaddP_imp_OrdP [THEN cut1])
done
qed
qed
theorem SubstFormP_Disj:
"{SubstFormP v i x x', SubstFormP v i y y'} ⊢ SubstFormP v i (Q_Disj x y) (Q_Disj x' y')"
proof -
obtain k1::name and s1::name and k2::name and s2::name and k::name and s::name
where "atom s1 ♯ (v,i,x,y,x',y')" "atom k1 ♯ (v,i,x,y,x',y',s1)"
"atom s2 ♯ (v,i,x,y,x',y',k1,s1)" "atom k2 ♯ (v,i,x,y,x',y',s2,k1,s1)"
"atom s ♯ (v,i,x,y,x',y',k2,s2,k1,s1)" "atom k ♯ (v,i,x,y,x',y',s,k2,s2,k1,s1)"
by (metis obtain_fresh)
thus ?thesis
by (force simp: SubstFormP.simps [of s v i "Q_Disj x y" _ k]
SubstFormP.simps [of s1 v i x x' k1]
SubstFormP.simps [of s2 v i y y' k2]
intro: SeqSubstFormP_Disj [THEN cut4])
qed
subsection ‹Existential›
lemma SeqSubstFormP_Ex:
assumes "atom s ♯ (k,s1,k1,x,x',v,i)" "atom k ♯ (s1,k1,x,x',v,i)"
shows "{SeqSubstFormP v i x x' s1 k1, TermP i, VarP v}
⊢ Ex s (Ex k (SeqSubstFormP v i (Q_Ex x) (Q_Ex x') (Var s) (Var k)))"
proof -
obtain l::name and sl::name and sl'::name and m::name and n::name
and sm::name and sm'::name and sn::name and sn'::name
where atoms:
"atom l ♯ (s1,k1,s,k,x,x',v,i,sl,sl',m,n,sm,sm',sn,sn')"
"atom sl ♯ (s1,k1,s,k,x,x',v,i,sl',m,n,sm,sm',sn,sn')"
"atom sl' ♯ (s1,k1,s,k,x,x',v,i,m,n,sm,sm',sn,sn')"
"atom m ♯ (s1,k1,s,k,x,x',v,i,n,sm,sm',sn,sn')"
"atom n ♯ (s1,k1,s,k,x,x',v,i,sm,sm',sn,sn')"
"atom sm ♯ (s1,k1,s,k,x,x',v,i,sm',sn,sn')"
"atom sm' ♯ (s1,k1,s,k,x,x',v,i,sn,sn')"
"atom sn ♯ (s1,k1,s,k,x,x',v,i,sn')"
"atom sn' ♯ (s1,k1,s,k,x,x',v,i)"
by (metis obtain_fresh)
let ?hyp = "{RestrictedP s1 (SUCC k1) (Var s), OrdP k1, SeqSubstFormP v i x x' s1 k1, TermP i, VarP v}"
show ?thesis
using assms atoms
apply (auto simp: SeqSubstFormP.simps [of l "Var s" _ _ _ sl sl' m n sm sm' sn sn'])
apply (rule cut_same [where A="OrdP k1"])
apply (metis SeqSubstFormP_imp_OrdP thin2)
apply (rule cut_same [OF exists_RestrictedP [of s s1 "SUCC k1"]])
apply (rule AssumeH Ex_EH Conj_EH | simp)+
apply (rule Ex_I [where x="Eats (Var s) (HPair (SUCC k1) (HPair (Q_Ex x) (Q_Ex x')))"], simp)
apply (rule Ex_I [where x="(SUCC k1)"], simp)
apply (rule Conj_I)
apply (blast intro: RestrictedP_LstSeqP_Eats [THEN cut2] SeqSubstFormP_imp_LstSeqP [THEN cut1])
proof (rule All2_SUCC_I, simp_all)
show "?hyp ⊢ Ex sl (Ex sl'
(HPair (SUCC k1) (HPair (Var sl) (Var sl')) IN Eats (Var s) (HPair (SUCC k1) (HPair (Q_Ex x) (Q_Ex x'))) AND
(SubstAtomicP v i (Var sl) (Var sl') OR
Ex m (Ex n
(Ex sm (Ex sm'
(Ex sn (Ex sn'
(Var m IN SUCC k1 AND
Var n IN SUCC k1 AND
HPair (Var m) (HPair (Var sm) (Var sm')) IN Eats (Var s) (HPair (SUCC k1) (HPair (Q_Ex x) (Q_Ex x'))) AND
HPair (Var n) (HPair (Var sn) (Var sn')) IN Eats (Var s) (HPair (SUCC k1) (HPair (Q_Ex x) (Q_Ex x'))) AND
(Var sl EQ Q_Disj (Var sm) (Var sn) AND Var sl' EQ Q_Disj (Var sm') (Var sn') OR
Var sl EQ Q_Neg (Var sm) AND Var sl' EQ Q_Neg (Var sm') OR Var sl EQ Q_Ex (Var sm) AND Var sl' EQ Q_Ex (Var sm')))))))))))"
apply (rule Ex_I [where x="Q_Ex x"])
using assms atoms apply simp
apply (rule Ex_I [where x="Q_Ex x'"], simp)
apply (rule Conj_I, metis Mem_Eats_I2 Refl)
apply (rule Disj_I2)
apply (rule Ex_I [where x=k1], simp)
apply (rule Ex_I [where x=k1], simp)
apply (rule Ex_I [where x=x], simp)
apply (rule_tac x=x' in Ex_I, simp)
apply (rule Ex_I [where x=x], simp)
apply (rule_tac x=x' in Ex_I, simp)
apply (rule Conj_I [OF Mem_SUCC_Refl])+
apply (blast intro: Disj_I2 Mem_Eats_I1 RestrictedP_Mem [THEN cut3] Mem_SUCC_Refl
SeqSubstFormP_imp_LstSeqP [THEN cut1] LstSeqP_imp_Mem)
done
next
show "?hyp
⊢ All2 l (SUCC k1)
(Ex sl (Ex sl'
(HPair (Var l) (HPair (Var sl) (Var sl')) IN Eats (Var s) (HPair (SUCC k1) (HPair (Q_Ex x) (Q_Ex x'))) AND
(SubstAtomicP v i (Var sl) (Var sl') OR
Ex m (Ex n
(Ex sm (Ex sm'
(Ex sn (Ex sn'
(Var m IN Var l AND
Var n IN Var l AND
HPair (Var m) (HPair (Var sm) (Var sm')) IN Eats (Var s) (HPair (SUCC k1) (HPair (Q_Ex x) (Q_Ex x'))) AND
HPair (Var n) (HPair (Var sn) (Var sn')) IN Eats (Var s) (HPair (SUCC k1) (HPair (Q_Ex x) (Q_Ex x'))) AND
(Var sl EQ Q_Disj (Var sm) (Var sn) AND Var sl' EQ Q_Disj (Var sm') (Var sn') OR
Var sl EQ Q_Neg (Var sm) AND Var sl' EQ Q_Neg (Var sm') OR Var sl EQ Q_Ex (Var sm) AND Var sl' EQ Q_Ex (Var sm'))))))))))))"
using assms atoms
apply (auto simp add: SeqSubstFormP.simps [of l s1 _ _ _ sl sl' m n sm sm' sn sn'])
apply (rule Swap)
apply (rule All2_E, auto del: Disj_EH)
apply (rule Ex_I [where x="Var sl"], simp)
apply (rule Ex_I [where x="Var sl'"], simp)
apply (rule Conj_I)
apply (blast intro: Mem_Eats_I1 [OF RestrictedP_Mem [THEN cut3]] del: Disj_EH)
apply (rule AssumeH Disj_IE1H Ex_EH Conj_EH)+
apply (rule Ex_I [where x="Var m"], simp)
apply (rule Ex_I [where x="Var n"], simp)
apply (rule Ex_I [where x="Var sm"], simp)
apply (rule Ex_I [where x="Var sm'"], simp)
apply (rule Ex_I [where x="Var sn"], simp)
apply (rule Ex_I [where x="Var sn'"])
apply (auto intro: Mem_Eats_I1 [OF RestrictedP_Mem [THEN cut3]] OrdP_Trans [OF OrdP_SUCC_I] del: Disj_EH)
done
qed
qed
theorem SubstFormP_Ex: "{SubstFormP v i x x'} ⊢ SubstFormP v i (Q_Ex x) (Q_Ex x')"
proof -
obtain k1::name and s1::name and k::name and s::name
where "atom s1 ♯ (v,i,x,x')" "atom k1 ♯ (v,i,x,x',s1)"
"atom s ♯ (v,i,x,x',k1,s1)" "atom k ♯ (v,i,x,x',s,k1,s1)"
by (metis obtain_fresh)
thus ?thesis
by (force simp: SubstFormP.simps [of s v i "Q_Ex x" _ k] SubstFormP.simps [of s1 v i x x' k1]
intro: SeqSubstFormP_Ex [THEN cut3])
qed
section ‹Constant Terms›
lemma ConstP_Zero: "{} ⊢ ConstP Zero"
by (auto intro: Sigma_fm_imp_thm [OF CTermP_sf] simp: Const_0 ground_fm_aux_def supp_conv_fresh)
lemma SeqConstP_Eats:
assumes "atom s ♯ (k,s1,s2,k1,k2,t1,t2)" "atom k ♯ (s1,s2,k1,k2,t1,t2)"
shows "{SeqConstP s1 k1 t1, SeqConstP s2 k2 t2}
⊢ Ex s (Ex k (SeqConstP (Var s) (Var k) (Q_Eats t1 t2)))"
proof -
obtain km::name and kn::name and j::name and k'::name
and l::name and sl::name and m::name and n::name and sm::name and sn::name
where atoms:
"atom km ♯ (kn,j,k',l,s1,s2,s,k1,k2,k,t1,t2,sl,m,n,sm,sn)"
"atom kn ♯ (j,k',l,s1,s2,s,k1,k2,k,t1,t2,sl,m,n,sm,sn)"
"atom j ♯ (k',l,s1,s2,s,k1,k2,k,t1,t2,sl,m,n,sm,sn)"
"atom k' ♯ (l,s1,s2,s,k1,k2,k,t1,t2,sl,m,n,sm,sn)"
"atom l ♯ (s1,s2,s,k1,k2,k,t1,t2,sl,m,n,sm,sn)"
"atom sl ♯ (s1,s2,s,k1,k2,k,t1,t2,m,n,sm,sn)"
"atom m ♯ (s1,s2,s,k1,k2,k,t1,t2,n,sm,sn)"
"atom n ♯ (s1,s2,s,k1,k2,k,t1,t2,sm,sn)"
"atom sm ♯ (s1,s2,s,k1,k2,k,t1,t2,sn)"
"atom sn ♯ (s1,s2,s,k1,k2,k,t1,t2)"
by (metis obtain_fresh)
let ?hyp = "{HaddP k1 k2 (Var k'), OrdP k1, OrdP k2, SeqAppendP s1 (SUCC k1) s2 (SUCC k2) (Var s),
SeqConstP s1 k1 t1, SeqConstP s2 k2 t2}"
show ?thesis
using assms atoms
apply (auto simp: SeqCTermP.simps [of l "Var s" _ sl m n sm sn])
apply (rule cut_same [where A="OrdP k1 AND OrdP k2"])
apply (metis Conj_I SeqCTermP_imp_OrdP thin1 thin2)
apply (rule cut_same [OF exists_SeqAppendP [of s s1 "SUCC k1" s2 "SUCC k2"]])
apply (rule AssumeH Ex_EH Conj_EH | simp)+
apply (rule cut_same [OF exists_HaddP [where j=k' and x=k1 and y=k2]])
apply (rule AssumeH Ex_EH Conj_EH | simp)+
apply (rule Ex_I [where x="Eats (Var s) (HPair (SUCC (SUCC (Var k'))) (Q_Eats t1 t2))"], simp)
apply (rule Ex_I [where x="SUCC (SUCC (Var k'))"], simp)
apply (rule Conj_I)
apply (blast intro: LstSeqP_SeqAppendP_Eats SeqCTermP_imp_LstSeqP [THEN cut1])
proof (rule All2_SUCC_I, simp_all)
show "?hyp ⊢ Ex sl (HPair (SUCC (SUCC (Var k'))) (Var sl) IN Eats (Var s)
(HPair (SUCC (SUCC (Var k'))) (Q_Eats t1 t2)) AND
(Var sl EQ Zero OR Fls OR
Ex m (Ex n(Ex sm (Ex sn
(Var m IN SUCC (SUCC (Var k')) AND
Var n IN SUCC (SUCC (Var k')) AND
HPair (Var m) (Var sm) IN Eats (Var s) (HPair (SUCC (SUCC (Var k'))) (Q_Eats t1 t2)) AND
HPair (Var n) (Var sn) IN Eats (Var s) (HPair (SUCC (SUCC (Var k'))) (Q_Eats t1 t2)) AND
Var sl EQ Q_Eats (Var sm) (Var sn)))))))"
apply (rule Ex_I [where x="Q_Eats t1 t2"])
using assms atoms apply simp
apply (rule Conj_I, metis Mem_Eats_I2 Refl)
apply (rule Disj_I2)+
apply (rule Ex_I [where x=k1], simp)
apply (rule Ex_I [where x="SUCC (Var k')"], simp)
apply (rule Ex_I [where x=t1], simp)
apply (rule Ex_I [where x=t2], simp)
apply (rule Conj_I)
apply (blast intro: HaddP_Mem_I LstSeqP_OrdP Mem_SUCC_I1)
apply (blast intro: Mem_Eats_I1 SeqAppendP_Mem1 [THEN cut3] SeqAppendP_Mem2 [THEN cut4]
Mem_SUCC_Refl SeqCTermP_imp_LstSeqP [THEN cut1] LstSeqP_imp_Mem HaddP_SUCC1 [THEN cut1])
done
next
show "?hyp ⊢ All2 l (SUCC (SUCC (Var k')))
(Ex sl
(HPair (Var l) (Var sl) IN Eats (Var s) (HPair (SUCC (SUCC (Var k'))) (Q_Eats t1 t2)) AND
(Var sl EQ Zero OR Fls OR
Ex m (Ex n (Ex sm (Ex sn
(Var m IN Var l AND
Var n IN Var l AND
HPair (Var m) (Var sm) IN Eats (Var s) (HPair (SUCC (SUCC (Var k'))) (Q_Eats t1 t2)) AND
HPair (Var n) (Var sn) IN Eats (Var s) (HPair (SUCC (SUCC (Var k'))) (Q_Eats t1 t2)) AND
Var sl EQ Q_Eats (Var sm) (Var sn))))))))"
apply (rule cut_same [where A="HaddP (SUCC k1) (SUCC k2) (SUCC (SUCC (Var k')))"])
apply (blast intro: HaddP_SUCC1 [THEN cut1] HaddP_SUCC2 [THEN cut1])
apply (rule All_I Imp_I)+
apply (rule HaddP_Mem_cases [where i=j])
using assms atoms apply simp_all
apply (rule AssumeH)
apply (blast intro: OrdP_SUCC_I LstSeqP_OrdP)
apply (simp add: SeqCTermP.simps [of l s1 _ sl m n sm sn])
apply (rule AssumeH Ex_EH Conj_EH)+
apply (rule All2_E [THEN rotate2], auto del: Disj_EH)
apply (rule Ex_I [where x="Var sl"], simp)
apply (rule Conj_I)
apply (rule Mem_Eats_I1)
apply (metis SeqAppendP_Mem1 rotate3 thin2 thin4)
apply (rule AssumeH Disj_IE1H Ex_EH Conj_EH)+
apply simp_all
apply (rule Ex_I [where x="Var m"], simp)
apply (rule Ex_I [where x="Var n"], simp)
apply (rule Ex_I [where x="Var sm"], simp)
apply (rule Ex_I [where x="Var sn"], simp)
apply (rule Conj_I, rule AssumeH)+
apply (blast del: Disj_EH intro: OrdP_Trans [OF OrdP_SUCC_I] Mem_Eats_I1 [OF SeqAppendP_Mem1 [THEN cut3]] Hyp)
apply (simp add: SeqCTermP.simps [of l s2 _ sl m n sm sn])
apply (rule AssumeH Ex_EH Conj_EH)+
apply (rule All2_E [THEN rotate2], auto del: Disj_EH)
apply (rule Ex_I [where x="Var sl"], simp)
apply (rule cut_same [where A="OrdP (Var j)"])
apply (metis HaddP_imp_OrdP rotate2 thin2)
apply (rule Conj_I)
apply (blast intro: Mem_Eats_I1 SeqAppendP_Mem2 [THEN cut4] del: Disj_EH)
apply (rule AssumeH Disj_IE1H Ex_EH Conj_EH)+
apply (rule cut_same [OF exists_HaddP [where j=km and x="SUCC k1" and y="Var m"]])
apply (blast intro: Ord_IN_Ord, simp)
apply (rule cut_same [OF exists_HaddP [where j=kn and x="SUCC k1" and y="Var n"]])
apply (metis AssumeH(6) Ord_IN_Ord0 rotate8, simp)
apply (rule AssumeH Ex_EH Conj_EH | simp)+
apply (rule Ex_I [where x="Var km"], simp)
apply (rule Ex_I [where x="Var kn"], simp)
apply (rule Ex_I [where x="Var sm"], simp)
apply (rule Ex_I [where x="Var sn"], simp_all)
apply (rule Conj_I [OF _ Conj_I])
apply (blast intro!: HaddP_Mem_cancel_left [THEN Iff_MP2_same] OrdP_SUCC_I intro: LstSeqP_OrdP Hyp)+
apply (blast del: Disj_EH intro: OrdP_Trans Hyp
intro!: Mem_Eats_I1 SeqAppendP_Mem2 [THEN cut4] HaddP_imp_OrdP [THEN cut1])
done
qed
qed
theorem ConstP_Eats: "{ConstP t1, ConstP t2} ⊢ ConstP (Q_Eats t1 t2)"
proof -
obtain k1::name and s1::name and k2::name and s2::name and k::name and s::name
where "atom s1 ♯ (t1,t2)" "atom k1 ♯ (t1,t2,s1)"
"atom s2 ♯ (t1,t2,k1,s1)" "atom k2 ♯ (t1,t2,s2,k1,s1)"
"atom s ♯ (t1,t2,k2,s2,k1,s1)" "atom k ♯ (t1,t2,s,k2,s2,k1,s1)"
by (metis obtain_fresh)
thus ?thesis
by (auto simp: CTermP.simps [of k s "(Q_Eats t1 t2)"]
CTermP.simps [of k1 s1 t1] CTermP.simps [of k2 s2 t2]
intro!: SeqConstP_Eats [THEN cut2])
qed
section ‹Proofs›
lemma PrfP_inference:
assumes "atom s ♯ (k,s1,s2,k1,k2,α1,α2,β)" "atom k ♯ (s1,s2,k1,k2,α1,α2,β)"
shows "{PrfP s1 k1 α1, PrfP s2 k2 α2, ModPonP α1 α2 β OR ExistsP α1 β OR SubstP α1 β}
⊢ Ex k (Ex s (PrfP (Var s) (Var k) β))"
proof -
obtain km::name and kn::name and j::name and k'::name
and l::name and sl::name and m::name and n::name and sm::name and sn::name
where atoms:
"atom km ♯ (kn,j,k',l,s1,s2,s,k1,k2,k,α1,α2,β,sl,m,n,sm,sn)"
"atom kn ♯ (j,k',l,s1,s2,s,k1,k2,k,α1,α2,β,sl,m,n,sm,sn)"
"atom j ♯ (k',l,s1,s2,s,k1,k2,k,α1,α2,β,sl,m,n,sm,sn)"
"atom k' ♯ (l,s1,s2,s,k1,k2,k,α1,α2,β,sl,m,n,sm,sn)"
"atom l ♯ (s1,s2,s,k1,k2,k,α1,α2,β,sl,m,n,sm,sn)"
"atom sl ♯ (s1,s2,s,k1,k2,k,α1,α2,β,m,n,sm,sn)"
"atom m ♯ (s1,s2,s,k1,k2,k,α1,α2,β,n,sm,sn)"
"atom n ♯ (s1,s2,s,k1,k2,k,α1,α2,β,sm,sn)"
"atom sm ♯ (s1,s2,s,k1,k2,k,α1,α2,β,sn)"
"atom sn ♯ (s1,s2,s,k1,k2,k,α1,α2,β)"
by (metis obtain_fresh)
let ?hyp = "{HaddP k1 k2 (Var k'), OrdP k1, OrdP k2, SeqAppendP s1 (SUCC k1) s2 (SUCC k2) (Var s),
PrfP s1 k1 α1, PrfP s2 k2 α2, ModPonP α1 α2 β OR ExistsP α1 β OR SubstP α1 β}"
show ?thesis
using assms atoms
apply (simp add: PrfP.simps [of l "Var s" sl m n sm sn])
apply (rule cut_same [where A="OrdP k1 AND OrdP k2"])
apply (metis Conj_I PrfP_imp_OrdP thin1 thin2)
apply (rule cut_same [OF exists_SeqAppendP [of s s1 "SUCC k1" s2 "SUCC k2"]])
apply (rule AssumeH Ex_EH Conj_EH | simp)+
apply (rule cut_same [OF exists_HaddP [where j=k' and x=k1 and y=k2]])
apply (rule AssumeH Ex_EH Conj_EH | simp)+
apply (rule Ex_I [where x="SUCC (SUCC (Var k'))"], simp)
apply (rule Ex_I [where x="Eats (Var s) (HPair (SUCC (SUCC (Var k'))) β)"], simp)
apply (rule Conj_I)
apply (blast intro: LstSeqP_SeqAppendP_Eats PrfP_imp_LstSeqP [THEN cut1])
proof (rule All2_SUCC_I, simp_all)
show "?hyp ⊢ Ex sn
(HPair (SUCC (SUCC (Var k'))) (Var sn) IN Eats (Var s) (HPair (SUCC (SUCC (Var k'))) β) AND
(AxiomP (Var sn) OR
Ex m (Ex l (Ex sm (Ex sl
(Var m IN SUCC (SUCC (Var k')) AND
Var l IN SUCC (SUCC (Var k')) AND
HPair (Var m) (Var sm) IN Eats (Var s) (HPair (SUCC (SUCC (Var k'))) β) AND
HPair (Var l) (Var sl) IN Eats (Var s) (HPair (SUCC (SUCC (Var k'))) β) AND
(ModPonP (Var sm) (Var sl) (Var sn) OR ExistsP (Var sm) (Var sn) OR SubstP (Var sm) (Var sn))))))))"
apply (rule Ex_I [where x="β"])
using assms atoms apply simp
apply (rule Conj_I, metis Mem_Eats_I2 Refl)
apply (rule Disj_I2)
apply (rule Ex_I [where x=k1], simp)
apply (rule Ex_I [where x="SUCC (Var k')"], simp)
apply (rule_tac x=α1 in Ex_I, simp)
apply (rule_tac x=α2 in Ex_I, simp)
apply (rule Conj_I)
apply (blast intro: HaddP_Mem_I LstSeqP_OrdP Mem_SUCC_I1)
apply (rule Conj_I [OF Mem_SUCC_Refl Conj_I])
apply (blast intro: Mem_Eats_I1 SeqAppendP_Mem1 [THEN cut3] Mem_SUCC_Refl PrfP_imp_LstSeqP [THEN cut1] LstSeqP_imp_Mem)
apply (blast del: Disj_EH intro: Mem_Eats_I1 SeqAppendP_Mem2 [THEN cut4] Mem_SUCC_Refl
PrfP_imp_LstSeqP [THEN cut1] HaddP_SUCC1 [THEN cut1] LstSeqP_imp_Mem)
done
next
show "?hyp ⊢ All2 n (SUCC (SUCC (Var k')))
(Ex sn
(HPair (Var n) (Var sn) IN Eats (Var s) (HPair (SUCC (SUCC (Var k'))) β) AND
(AxiomP (Var sn) OR
Ex m (Ex l (Ex sm (Ex sl
(Var m IN Var n AND
Var l IN Var n AND
HPair (Var m) (Var sm) IN Eats (Var s) (HPair (SUCC (SUCC (Var k'))) β) AND
HPair (Var l) (Var sl) IN Eats (Var s) (HPair (SUCC (SUCC (Var k'))) β) AND
(ModPonP (Var sm) (Var sl) (Var sn) OR ExistsP (Var sm) (Var sn) OR SubstP (Var sm) (Var sn)))))))))"
apply (rule cut_same [where A="HaddP (SUCC k1) (SUCC k2) (SUCC (SUCC (Var k')))"])
apply (blast intro: HaddP_SUCC1 [THEN cut1] HaddP_SUCC2 [THEN cut1])
apply (rule All_I Imp_I)+
apply (rule HaddP_Mem_cases [where i=j])
using assms atoms apply simp_all
apply (rule AssumeH)
apply (blast intro: OrdP_SUCC_I LstSeqP_OrdP)
apply (simp add: PrfP.simps [of l s1 sl m n sm sn])
apply (rule AssumeH Ex_EH Conj_EH)+
apply (rule All2_E [THEN rotate2])
apply (rule AssumeH Ex_EH Conj_EH | simp)+
apply (rule Ex_I [where x="Var sn"], simp)
apply (rule Conj_I)
apply (rule Mem_Eats_I1)
apply (metis SeqAppendP_Mem1 rotate3 thin2 thin4)
apply (rule AssumeH Disj_IE1H Ex_EH Conj_EH)+
apply (rule Ex_I [where x="Var m"], simp)
apply (rule Ex_I [where x="Var l"], simp)
apply (rule Ex_I [where x="Var sm"], simp)
apply (rule Ex_I [where x="Var sl"], simp_all)
apply (rule Conj_I, rule AssumeH)+
apply (blast del: Disj_EH intro: OrdP_Trans [OF OrdP_SUCC_I] Mem_Eats_I1 [OF SeqAppendP_Mem1 [THEN cut3]] Hyp)
apply (simp add: PrfP.simps [of l s2 sl m n sm sn])
apply (rule AssumeH Ex_EH Conj_EH)+
apply (rule All2_E [THEN rotate2])
apply (rule AssumeH Ex_EH Conj_EH | simp)+
apply (rule Ex_I [where x="Var sn"], simp)
apply (rule cut_same [where A="OrdP (Var j)"])
apply (metis HaddP_imp_OrdP rotate2 thin2)
apply (rule Conj_I)
apply (blast intro!: Mem_Eats_I1 SeqAppendP_Mem2 [THEN cut4] del: Disj_EH)
apply (rule AssumeH Disj_IE1H Ex_EH Conj_EH)+
apply (rule cut_same [OF exists_HaddP [where j=km and x="SUCC k1" and y="Var m"]])
apply (blast intro: Ord_IN_Ord, simp)
apply (rule cut_same [OF exists_HaddP [where j=kn and x="SUCC k1" and y="Var l"]])
apply (blast intro!: Ord_IN_Ord)
apply (rule AssumeH Ex_EH Conj_EH | simp)+
apply (rule Ex_I [where x="Var km"], simp)
apply (rule Ex_I [where x="Var kn"], simp)
apply (rule Ex_I [where x="Var sm"], simp)
apply (rule Ex_I [where x="Var sl"], simp_all)
apply (rule Conj_I [OF _ Conj_I])
apply (blast intro!: HaddP_Mem_cancel_left [THEN Iff_MP2_same] OrdP_SUCC_I intro: LstSeqP_OrdP Hyp)+
apply (blast del: Disj_EH intro: OrdP_Trans Hyp
intro!: Mem_Eats_I1 SeqAppendP_Mem2 [THEN cut4] HaddP_imp_OrdP [THEN cut1])
done
qed
qed
corollary PfP_inference: "{PfP α1, PfP α2, ModPonP α1 α2 β OR ExistsP α1 β OR SubstP α1 β} ⊢ PfP β"
proof -
obtain k1::name and s1::name and k2::name and s2::name and k::name and s::name
where "atom s1 ♯ (α1,α2,β)" "atom k1 ♯ (α1,α2,β,s1)"
"atom s2 ♯ (α1,α2,β,k1,s1)""atom k2 ♯ (α1,α2,β,s2,k1,s1)"
"atom s ♯ (α1,α2,β,k2,s2,k1,s1)"
"atom k ♯ (α1,α2,β,s,k2,s2,k1,s1)"
by (metis obtain_fresh)
thus ?thesis
apply (simp add: PfP.simps [of k s β] PfP.simps [of k1 s1 α1] PfP.simps [of k2 s2 α2])
apply (auto intro!: PrfP_inference [of s k "Var s1" "Var s2", THEN cut3] del: Disj_EH)
done
qed
theorem PfP_implies_SubstForm_PfP:
assumes "H ⊢ PfP y" "H ⊢ SubstFormP x t y z"
shows "H ⊢ PfP z"
proof -
obtain u::name and v::name
where atoms: "atom u ♯ (t,x,y,z,v)" "atom v ♯ (t,x,y,z)"
by (metis obtain_fresh)
show ?thesis
apply (rule PfP_inference [of y, THEN cut3])
apply (rule assms)+
using atoms
apply (auto simp: SubstP.simps [of u _ _ v] intro!: Disj_I2)
apply (rule Ex_I [where x=x], simp)
apply (rule Ex_I [where x=t], simp add: assms)
done
qed
theorem PfP_implies_ModPon_PfP: "⟦H ⊢ PfP (Q_Imp x y); H ⊢ PfP x⟧ ⟹ H ⊢ PfP y"
by (force intro: PfP_inference [of x, THEN cut3] Disj_I1 simp add: ModPonP_def)
corollary PfP_implies_ModPon_PfP_quot: "⟦H ⊢ PfP «α IMP β»; H ⊢ PfP «α»⟧ ⟹ H ⊢ PfP «β»"
by (auto simp: quot_fm_def intro: PfP_implies_ModPon_PfP)
end