# Theory Quote

```chapter‹Quotations of the Free Variables›

theory Quote
imports Pseudo_Coding
begin

section ‹Sequence version of the ``Special p-Function, F*''›

text‹The definition below describes a relation, not a function.
This material relates to Section 8, but omits the ordering of the universe.›

definition SeqQuote :: "hf ⇒ hf ⇒ hf ⇒ hf ⇒ bool"
where "SeqQuote x x' s k ≡
BuildSeq2 (λy y'. y=0 ∧ y' = 0)
(λu u' v v' w w'. u = v ◃ w ∧ u' = q_Eats v' w') s k x x'"

subsection ‹Defining the syntax: quantified body›

nominal_function SeqQuoteP :: "tm ⇒ tm ⇒ tm ⇒ tm ⇒ fm"
where "⟦atom l ♯ (s,k,sl,sl',m,n,sm,sm',sn,sn');
atom sl ♯ (s,sl',m,n,sm,sm',sn,sn'); atom sl' ♯ (s,m,n,sm,sm',sn,sn');
atom m ♯ (s,n,sm,sm',sn,sn');  atom n ♯ (s,sm,sm',sn,sn');
atom sm ♯ (s,sm',sn,sn');  atom sm' ♯ (s,sn,sn');
atom sn ♯ (s,sn');  atom sn' ♯ s⟧ ⟹
SeqQuoteP t u s k =
LstSeqP s k (HPair t u) AND
All2 l (SUCC k) (Ex sl (Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND
((Var sl EQ Zero AND Var sl' EQ Zero) 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 s AND
HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND
Var sl EQ Eats (Var sm) (Var sn) AND
Var sl' EQ Q_Eats (Var sm') (Var sn')))))))))))"
by (auto simp: eqvt_def SeqQuoteP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)

nominal_termination (eqvt)
by lexicographic_order

lemma
shows SeqQuoteP_fresh_iff [simp]:
"a ♯ SeqQuoteP t u s k ⟷ a ♯ t ∧ a ♯ u ∧ a ♯ s ∧ a ♯ k"  (is ?thesis1)
and eval_fm_SeqQuoteP [simp]:
"eval_fm e (SeqQuoteP t u s k) ⟷ SeqQuote ⟦t⟧e ⟦u⟧e ⟦s⟧e ⟦k⟧e"    (is ?thesis2)
and SeqQuoteP_sf [iff]:
"Sigma_fm (SeqQuoteP t u s k)"    (is ?thsf)
and SeqQuoteP_imp_OrdP:
"{ SeqQuoteP t u s k } ⊢ OrdP k"  (is ?thord)
and SeqQuoteP_imp_LstSeqP:
"{ SeqQuoteP t u s k } ⊢ LstSeqP s k (HPair t u)"  (is ?thlstseq)
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 ♯ (s,k,sl,sl',m,n,sm,sm',sn,sn')"
"atom sl ♯ (s,sl',m,n,sm,sm',sn,sn')"  "atom sl' ♯ (s,m,n,sm,sm',sn,sn')"
"atom m ♯ (s,n,sm,sm',sn,sn')"  "atom n ♯ (s,sm,sm',sn,sn')"
"atom sm ♯ (s,sm',sn,sn')"  "atom sm' ♯ (s,sn,sn')"
"atom sn ♯ (s,sn')"  "atom sn' ♯ s"
by (metis obtain_fresh)
thus ?thesis1 ?thsf ?thord ?thlstseq
by auto (auto simp: LstSeqP.simps)
show ?thesis2 using atoms
by (force simp add: LstSeq_imp_Ord SeqQuote_def
BuildSeq2_def BuildSeq_def Builds_def HBall_def q_Eats_def
Seq_iff_app [of "⟦s⟧e", OF LstSeq_imp_Seq_succ]
Ord_trans [of _ _ "succ ⟦k⟧e"]
cong: conj_cong)
qed

lemma SeqQuoteP_subst [simp]:
"(SeqQuoteP t u s k)(j::=w) =
SeqQuoteP (subst j w t) (subst j w u) (subst j w s) (subst j w 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 "atom l ♯ (s,k,w,j,sl,sl',m,n,sm,sm',sn,sn')"
"atom sl ♯ (s,w,j,sl',m,n,sm,sm',sn,sn')"  "atom sl' ♯ (s,w,j,m,n,sm,sm',sn,sn')"
"atom m ♯ (s,w,j,n,sm,sm',sn,sn')"  "atom n ♯ (s,w,j,sm,sm',sn,sn')"
"atom sm ♯ (s,w,j,sm',sn,sn')"  "atom sm' ♯ (s,w,j,sn,sn')"
"atom sn ♯ (s,w,j,sn')"  "atom sn' ♯ (s,w,j)"
by (metis obtain_fresh)
thus ?thesis
by (force simp add: SeqQuoteP.simps [of l _ _ sl sl' m n sm sm' sn sn'])
qed

declare SeqQuoteP.simps [simp del]

subsection ‹Correctness properties›

lemma SeqQuoteP_lemma:
fixes m::name and sm::name and sm'::name and n::name and sn::name and sn'::name
assumes "atom m ♯ (t,u,s,k,n,sm,sm',sn,sn')"  "atom n ♯ (t,u,s,k,sm,sm',sn,sn')"
"atom sm ♯ (t,u,s,k,sm',sn,sn')"  "atom sm' ♯ (t,u,s,k,sn,sn')"
"atom sn ♯ (t,u,s,k,sn')"  "atom sn' ♯ (t,u,s,k)"
shows "{ SeqQuoteP t u s k }
⊢ (t EQ Zero AND u EQ Zero) OR
Ex m (Ex n (Ex sm (Ex sm' (Ex sn (Ex sn' (Var m IN k AND Var n IN k AND
SeqQuoteP (Var sm) (Var sm') s (Var m) AND
SeqQuoteP (Var sn) (Var sn') s (Var n) AND
t EQ Eats (Var sm) (Var sn) AND
u EQ Q_Eats (Var sm') (Var sn')))))))"
proof -
obtain l::name and sl::name and sl'::name
where "atom l ♯ (t,u,s,k,sl,sl',m,n,sm,sm',sn,sn')"
"atom sl ♯ (t,u,s,k,sl',m,n,sm,sm',sn,sn')"
"atom sl' ♯ (t,u,s,k,m,n,sm,sm',sn,sn')"
by (metis obtain_fresh)
thus ?thesis using assms
apply (simp add: SeqQuoteP.simps [of l s k sl sl' m n sm sm' sn sn'])
apply (rule Conj_EH Ex_EH All2_SUCC_E [THEN rotate2] | simp)+
apply (rule cut_same [where A = "HPair t u EQ HPair (Var sl) (Var sl')"])
apply (metis Assume AssumeH(4) LstSeqP_EQ)
apply clarify
apply (rule Disj_EH)
apply (rule Disj_I1)
apply (rule anti_deduction)
apply (rule Var_Eq_subst_Iff [THEN Sym_L, THEN Iff_MP_same])
apply (rule rotate2)
apply (rule Var_Eq_subst_Iff [THEN Sym_L, THEN Iff_MP_same], force)
― ‹now the quantified case›
apply (rule Ex_EH Conj_EH)+
apply simp_all
apply (rule 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 sm'"], simp)
apply (rule Ex_I [where x = "Var sn"], simp)
apply (rule Ex_I [where x = "Var sn'"], simp)
apply (simp_all add: SeqQuoteP.simps [of l s _ sl sl' m n sm sm' sn sn'])
apply ((rule Conj_I)+, blast intro: LstSeqP_Mem)+
― ‹first SeqQuoteP subgoal›
apply (rule All2_Subset [OF Hyp])
apply (blast intro!: SUCC_Subset_Ord LstSeqP_OrdP)+
apply simp
― ‹next SeqQuoteP subgoal›
apply ((rule Conj_I)+, blast intro: LstSeqP_Mem)+
apply (rule All2_Subset [OF Hyp], blast)
apply (auto intro!: SUCC_Subset_Ord LstSeqP_OrdP intro: Trans)
done
qed

section ‹The ``special function'' itself›

definition Quote :: "hf ⇒ hf ⇒ bool"
where "Quote x x' ≡ ∃s k. SeqQuote x x' s k"

subsection ‹Defining the syntax›

nominal_function QuoteP :: "tm ⇒ tm ⇒ fm"
where "⟦atom s ♯ (t,u,k); atom k ♯ (t,u)⟧ ⟹
QuoteP t u = Ex s (Ex k (SeqQuoteP t u (Var s) (Var k)))"
by (auto simp: eqvt_def QuoteP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)

nominal_termination (eqvt)
by lexicographic_order

lemma
shows QuoteP_fresh_iff [simp]: "a ♯ QuoteP t u ⟷ a ♯ t ∧ a ♯ u"  (is ?thesis1)
and eval_fm_QuoteP [simp]: "eval_fm e (QuoteP t u) ⟷ Quote ⟦t⟧e ⟦u⟧e"  (is ?thesis2)
and QuoteP_sf [iff]: "Sigma_fm (QuoteP t u)"  (is ?thsf)
proof -
obtain s::name and k::name  where "atom s ♯ (t,u,k)"  "atom k ♯ (t,u)"
by (metis obtain_fresh)
thus ?thesis1 ?thesis2 ?thsf
by (auto simp: Quote_def)
qed

lemma QuoteP_subst [simp]:
"(QuoteP t u)(j::=w) = QuoteP (subst j w t) (subst j w u)"
proof -
obtain s::name and k::name  where "atom s ♯ (t,u,w,j,k)"  "atom k ♯ (t,u,w,j)"
by (metis obtain_fresh)
thus ?thesis
by (simp add: QuoteP.simps [of s _ _ k])
qed

declare QuoteP.simps [simp del]

subsection ‹Correctness properties›

lemma Quote_0: "Quote 0 0"
by (auto simp: Quote_def SeqQuote_def intro: BuildSeq2_exI)

lemma QuoteP_Zero: "{} ⊢ QuoteP Zero Zero"
by (auto intro: Sigma_fm_imp_thm [OF QuoteP_sf]
simp: ground_fm_aux_def supp_conv_fresh Quote_0)

lemma SeqQuoteP_Eats:
assumes "atom s ♯ (k,s1,s2,k1,k2,t1,t2,u1,u2)" "atom k ♯ (s1,s2,k1,k2,t1,t2,u1,u2)"
shows "{SeqQuoteP t1 u1 s1 k1, SeqQuoteP t2 u2 s2 k2} ⊢
Ex s (Ex k (SeqQuoteP (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 ♯ (kn,j,k',l,s1,s2,s,k1,k2,k,t1,t2,u1,u2,sl,sl',m,n,sm,sm',sn,sn')"
"atom kn ♯ (j,k',l,s1,s2,s,k1,k2,k,t1,t2,u1,u2,sl,sl',m,n,sm,sm',sn,sn')"
"atom j ♯ (k',l,s1,s2,s,k1,k2,k,t1,t2,u1,u2,sl,sl',m,n,sm,sm',sn,sn')"
and atoms: "atom k' ♯ (l,s1,s2,s,k1,k2,k,t1,t2,u1,u2,sl,sl',m,n,sm,sm',sn,sn')"
"atom l ♯ (s1,s2,s,k1,k2,k,t1,t2,u1,u2,sl,sl',m,n,sm,sm',sn,sn')"
"atom sl ♯ (s1,s2,s,k1,k2,k,t1,t2,u1,u2,sl',m,n,sm,sm',sn,sn')"
"atom sl' ♯ (s1,s2,s,k1,k2,k,t1,t2,u1,u2,m,n,sm,sm',sn,sn')"
"atom m ♯ (s1,s2,s,k1,k2,k,t1,t2,u1,u2,n,sm,sm',sn,sn')"
"atom n ♯ (s1,s2,s,k1,k2,k,t1,t2,u1,u2,sm,sm',sn,sn')"
"atom sm ♯ (s1,s2,s,k1,k2,k,t1,t2,u1,u2,sm',sn,sn')"
"atom sm' ♯ (s1,s2,s,k1,k2,k,t1,t2,u1,u2,sn,sn')"
"atom sn ♯ (s1,s2,s,k1,k2,k,t1,t2,u1,u2,sn')"
"atom sn' ♯ (s1,s2,s,k1,k2,k,t1,t2,u1,u2)"
by (metis obtain_fresh)
show ?thesis
using assms atoms
apply (auto simp: SeqQuoteP.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 SeqQuoteP_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 (Eats t1 t2) (Q_Eats u1 u2)))"])
apply (simp_all (no_asm_simp))
apply (rule Ex_I [where x="SUCC (SUCC (Var k'))"])
apply simp
apply (rule Conj_I [OF LstSeqP_SeqAppendP_Eats])
apply (blast intro: SeqQuoteP_imp_LstSeqP [THEN cut1])+
proof (rule All2_SUCC_I, simp_all)
show "{HaddP k1 k2 (Var k'), OrdP k1, OrdP k2, SeqAppendP s1 (SUCC k1) s2 (SUCC k2) (Var s),
SeqQuoteP t1 u1 s1 k1, SeqQuoteP t2 u2 s2 k2}
⊢ Ex sl (Ex sl'
(HPair (SUCC (SUCC (Var k'))) (HPair (Var sl) (Var sl')) IN
Eats (Var s) (HPair (SUCC (SUCC (Var k'))) (HPair (Eats t1 t2) (Q_Eats u1 u2))) AND
(Var sl EQ Zero AND Var sl' EQ Zero 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 (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 (Eats t1 t2) (Q_Eats u1 u2))) AND
Var sl EQ Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))"
― ‹verifying the final values›
apply (rule Ex_I [where x="Eats t1 t2"])
using assms atoms apply simp
apply (rule Ex_I [where x="Q_Eats u1 u2"], simp)
apply (rule Conj_I [OF Mem_Eats_I2 [OF 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 (rule Conj_I [OF Mem_SUCC_Refl])
apply (rule Conj_I)
apply (blast intro: Mem_Eats_I1 SeqAppendP_Mem1 [THEN cut3] Mem_SUCC_Refl
SeqQuoteP_imp_LstSeqP [THEN cut1] LstSeqP_imp_Mem)
apply (blast intro: Mem_Eats_I1 SeqAppendP_Mem2 [THEN cut4] Mem_SUCC_Refl
SeqQuoteP_imp_LstSeqP [THEN cut1] LstSeqP_imp_Mem  HaddP_SUCC1 [THEN cut1])
done
next
show "{HaddP k1 k2 (Var k'), OrdP k1, OrdP k2, SeqAppendP s1 (SUCC k1) s2 (SUCC k2) (Var s),
SeqQuoteP t1 u1 s1 k1, SeqQuoteP t2 u2 s2 k2}
⊢ 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 (Eats t1 t2) (Q_Eats u1 u2))) AND
(Var sl EQ Zero AND Var sl' EQ Zero 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 (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 (Eats t1 t2) (Q_Eats u1 u2))) AND
Var sl EQ Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn')))))))))))"
― ‹verifying the sequence buildup›
apply (rule cut_same [where A="HaddP (SUCC k1) (SUCC k2) (SUCC (SUCC (Var k')))"])
apply (rule All_I Imp_I)+
using assms atoms atoms2 apply simp_all
apply (rule AssumeH)
apply (blast intro: OrdP_SUCC_I)
― ‹... the sequence buildup via s1›
apply (simp add: SeqQuoteP.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 (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 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 intro: OrdP_Trans [OF OrdP_SUCC_I] Mem_Eats_I1 [OF SeqAppendP_Mem1 [THEN cut3]] Hyp)
― ‹... the sequence buildup via s2›
apply (simp add: SeqQuoteP.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 (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)
apply (rule Conj_I [OF _ Conj_I])
apply (blast intro: Hyp OrdP_SUCC_I HaddP_Mem_cancel_left [THEN Iff_MP2_same])
apply (blast intro: Hyp OrdP_SUCC_I HaddP_Mem_cancel_left [THEN Iff_MP2_same])
apply (blast intro: Hyp Mem_Eats_I1 SeqAppendP_Mem2 [THEN cut4] OrdP_Trans HaddP_imp_OrdP [THEN cut1])
done
qed
qed

lemma QuoteP_Eats: "{QuoteP t1 u1, QuoteP t2 u2} ⊢ QuoteP (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 ♯ (t1,u1,t2,u2)"             "atom k1 ♯ (t1,u1,t2,u2,s1)"
"atom s2 ♯ (t1,u1,t2,u2,k1,s1)"       "atom k2 ♯ (t1,u1,t2,u2,s2,k1,s1)"
"atom s  ♯ (t1,u1,t2,u2,k2,s2,k1,s1)" "atom k  ♯ (t1,u1,t2,u2,s,k2,s2,k1,s1)"
by (metis obtain_fresh)
thus ?thesis
by (auto simp: QuoteP.simps [of s _ "(Q_Eats u1 u2)" k]
QuoteP.simps [of s1 t1 u1 k1] QuoteP.simps [of s2 t2 u2 k2]
intro!: SeqQuoteP_Eats [THEN cut2])
qed

lemma exists_QuoteP:
assumes j: "atom j ♯ x"  shows "{} ⊢ Ex j (QuoteP x (Var j))"
proof -
obtain i::name and j'::name and k::name
where atoms: "atom i ♯ (j,x)"  "atom j' ♯ (i,j,x)"  "atom (k::name) ♯ (i,j,j',x)"
by (metis obtain_fresh)
have "{} ⊢ Ex j (QuoteP (Var i) (Var j))" (is "{} ⊢ ?scheme")
proof (rule Ind [of k])
show "atom k ♯ (i, ?scheme)" using atoms
by simp
next
show "{} ⊢ ?scheme(i::=Zero)" using j atoms
by (auto intro: Ex_I [where x=Zero] simp add: QuoteP_Zero)
next
show "{} ⊢ All i (All k (?scheme IMP ?scheme(i::=Var k) IMP ?scheme(i::=Eats (Var i) (Var k))))"
apply (rule All_I Imp_I)+
using atoms assms
apply simp_all
apply (rule Ex_E)
apply (rule Ex_E_with_renaming [where i'=j', THEN rotate2], auto)
apply (rule Ex_I [where x= "Q_Eats (Var j') (Var j)"], auto intro: QuoteP_Eats)
done
qed
hence "{} ⊢ (Ex j (QuoteP (Var i) (Var j))) (i::= x)"
by (rule Subst) auto
thus ?thesis
using atoms j by auto
qed

lemma QuoteP_imp_ConstP: "{ QuoteP x y } ⊢ ConstP y"
proof -
obtain j::name and j'::name and l::name and s::name and k::name
and m::name and n::name and sm::name and sn::name and sm'::name and sn'::name
where atoms: "atom j ♯ (x,y,s,k,j',l,m,n,sm,sm',sn,sn')"
"atom j' ♯ (x,y,s,k,l,m,n,sm,sm',sn,sn')"
"atom l ♯ (s,k,m,n,sm,sm',sn,sn')"
"atom m ♯ (s,k,n,sm,sm',sn,sn')" "atom n ♯ (s,k,sm,sm',sn,sn')"
"atom sm ♯ (s,k,sm',sn,sn')" "atom sm' ♯ (s,k,sn,sn')"
"atom sn ♯ (s,k,sn')" "atom sn' ♯ (s,k)" "atom s ♯ (k,x,y)" "atom k ♯ (x,y)"
by (metis obtain_fresh)
have "{OrdP (Var k)}
⊢ All j (All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var k) IMP ConstP (Var j')))"
(is "_ ⊢ ?scheme")
proof (rule OrdIndH [where j=l])
show "atom l ♯ (k, ?scheme)" using atoms
by simp
next
show "{} ⊢ All k (OrdP (Var k) IMP (All2 l (Var k) (?scheme(k::= Var l)) IMP ?scheme))"
apply (rule All_I Imp_I)+
using atoms
― ‹freshness finally proved!›
apply (rule cut_same)
apply (rule cut1 [OF SeqQuoteP_lemma [of m "Var j" "Var j'" "Var s" "Var k" n sm sm' sn sn']], simp_all, blast)
apply (rule Imp_I Disj_EH Conj_EH)+
― ‹case 1, Var j EQ Zero›
apply (rule thin1)
apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same], simp)
apply (metis thin0 ConstP_Zero)
― ‹case 2, @{term "Var j EQ Eats (Var sm) (Var sn)"}›
apply (rule Imp_I Conj_EH Ex_EH)+
apply simp_all
apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same, THEN rotate2], simp)
apply (rule ConstP_Eats [THEN cut2])
― ‹Operand 1. IH for sm›
apply (rule All2_E [where x="Var m", THEN rotate8], auto)
apply (rule All_E [where x="Var sm"], simp)
apply (rule All_E [where x="Var sm'"], auto)
― ‹Operand 2. IH for sm›
apply (rule All2_E [where x="Var n", THEN rotate8], auto)
apply (rule All_E [where x="Var sn"], simp)
apply (rule All_E [where x="Var sn'"], auto)
done
qed
hence "{OrdP(Var k)}
⊢ (All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var k) IMP ConstP (Var j'))) (j::=x)"
by (metis All_D)
hence "{OrdP(Var k)} ⊢ All j' (SeqQuoteP x (Var j') (Var s) (Var k) IMP ConstP (Var j'))"
using atoms by simp
hence "{OrdP(Var k)} ⊢ (SeqQuoteP x (Var j') (Var s) (Var k) IMP ConstP (Var j')) (j'::=y)"
by (metis All_D)
hence "{OrdP(Var k)} ⊢ SeqQuoteP x y (Var s) (Var k) IMP ConstP y"
using atoms by simp
hence "{ SeqQuoteP x y (Var s) (Var k) } ⊢ ConstP y"
by (metis Imp_cut SeqQuoteP_imp_OrdP anti_deduction)
thus "{ QuoteP x y } ⊢ ConstP y" using atoms
by (auto simp: QuoteP.simps [of s _ _ k])
qed

lemma SeqQuoteP_imp_QuoteP: "{SeqQuoteP t u s k} ⊢ QuoteP t u"
proof -
obtain s'::name and k'::name  where "atom s' ♯ (k',t,u,s,k)"  "atom k' ♯ (t,u,s,k)"
by (metis obtain_fresh)
thus ?thesis
apply (simp add: QuoteP.simps [of s' _ _ k'])
apply (rule Ex_I [where x = s], simp)
apply (rule Ex_I [where x = k], auto)
done
qed

lemmas QuoteP_I = SeqQuoteP_imp_QuoteP [THEN cut1]

section ‹The Operator @{term quote_all}›

subsection ‹Definition and basic properties›

definition quote_all :: "[perm, name set] ⇒ fm set"
where "quote_all p V = {QuoteP (Var i) (Var (p ∙ i)) | i. i ∈ V}"

lemma quote_all_empty [simp]: "quote_all p {} = {}"

lemma quote_all_insert [simp]:
"quote_all p (insert i V) = insert (QuoteP (Var i) (Var (p ∙ i))) (quote_all p V)"
by (auto simp: quote_all_def)

lemma finite_quote_all [simp]: "finite V ⟹ finite (quote_all p V)"
by (induct rule: finite_induct) auto

lemma fresh_quote_all [simp]: "finite V ⟹ i ♯ quote_all p V ⟷ i ♯ V ∧ i ♯ p∙V"
by (induct rule: finite_induct) (auto simp: fresh_finite_insert)

lemma fresh_quote_all_mem: "⟦A ∈ quote_all p V; finite V; i ♯ V; i ♯ p ∙ V⟧ ⟹ i ♯ A"
by (metis Set.set_insert finite_insert finite_quote_all fresh_finite_insert fresh_quote_all)

lemma quote_all_perm_eq:
assumes "finite V" "atom i ♯ (p,V)" "atom i' ♯ (p,V)"
shows "quote_all ((atom i ⇌ atom i') + p) V = quote_all p V"
proof -
{ fix W
assume w: "W ⊆ V"
have "finite W"
by (metis ‹finite V› finite_subset w)
hence "quote_all ((atom i ⇌ atom i') + p) W = quote_all p W" using w
apply induction  using assms
apply (auto simp: fresh_Pair perm_commute)
apply (metis fresh_finite_set_at_base swap_at_base_simps(3))+
done}
thus ?thesis
by (metis order_refl)
qed

subsection ‹Transferring theorems to the level of derivability›

context quote_perm
begin

lemma QuoteP_imp_ConstP_F_hyps:
assumes "Us ⊆ Vs" "{ConstP (F i) | i. i ∈ Us} ⊢ A"  shows "quote_all p Us ⊢ A"
proof -
show ?thesis using finite_V [OF ‹Us ⊆ Vs›]  assms
proof (induction arbitrary: A rule: finite_induct)
case empty thus ?case by simp
next
case (insert v Us) thus ?case
by (auto simp: Collect_disj_Un)
(metis (lifting) anti_deduction Imp_cut [OF _ QuoteP_imp_ConstP] Disj_I2 F_unfold)
qed
qed

text‹Lemma 8.3›
theorem quote_all_PfP_ssubst:
assumes β: "{} ⊢ β"
and V: "V ⊆ Vs"
and s: "supp β ⊆ atom ` Vs"
shows    "quote_all p V ⊢ PfP (ssubst ⌊β⌋V V F)"
proof -
have "{} ⊢ PfP «β»"
by (metis β proved_iff_proved_PfP)
hence "{ConstP (F i) | i. i ∈ V} ⊢ PfP (ssubst ⌊β⌋V V F)"
by (simp add: PfP_implies_PfP_ssubst V s)
thus ?thesis
by (rule QuoteP_imp_ConstP_F_hyps [OF V])
qed

text‹Lemma 8.4›
corollary quote_all_MonPon_PfP_ssubst:
assumes A: "{} ⊢ α IMP β"
and V: "V ⊆ Vs"
and s: "supp α ⊆ atom ` Vs" "supp β ⊆ atom ` Vs"
shows    "quote_all p V ⊢ PfP (ssubst ⌊α⌋V V F) IMP PfP (ssubst ⌊β⌋V V F)"
using quote_all_PfP_ssubst [OF A V] s
by (auto simp: V vquot_fm_def intro: PfP_implies_ModPon_PfP thin1)

text‹Lemma 8.4b›
corollary quote_all_MonPon2_PfP_ssubst:
assumes A: "{} ⊢ α1 IMP α2 IMP β"
and V: "V ⊆ Vs"
and s: "supp α1 ⊆ atom ` Vs" "supp α2 ⊆ atom ` Vs" "supp β ⊆ atom ` Vs"
shows "quote_all p V ⊢ PfP (ssubst ⌊α1⌋V V F) IMP PfP (ssubst ⌊α2⌋V V F) IMP PfP (ssubst ⌊β⌋V V F)"
using quote_all_PfP_ssubst [OF A V] s
by (force simp: V vquot_fm_def intro: PfP_implies_ModPon_PfP [OF PfP_implies_ModPon_PfP] thin1)

lemma quote_all_Disj_I1_PfP_ssubst:
assumes "V ⊆ Vs" "supp α ⊆ atom ` Vs" "supp β ⊆ atom ` Vs"
and prems: "H ⊢ PfP (ssubst ⌊α⌋V V F)" "quote_all p V ⊆ H"
shows "H ⊢ PfP (ssubst ⌊α OR β⌋V V F)"
proof -
have "{} ⊢ α IMP (α OR β)"
by (blast intro: Disj_I1)
hence "quote_all p V ⊢ PfP (ssubst ⌊α⌋V V F) IMP PfP (ssubst ⌊α OR β⌋V V F)"
using assms by (auto simp: quote_all_MonPon_PfP_ssubst)
thus ?thesis
by (metis MP_same prems thin)
qed

lemma quote_all_Disj_I2_PfP_ssubst:
assumes "V ⊆ Vs" "supp α ⊆ atom ` Vs" "supp β ⊆ atom ` Vs"
and prems: "H ⊢ PfP (ssubst ⌊β⌋V V F)" "quote_all p V ⊆ H"
shows "H ⊢ PfP (ssubst ⌊α OR β⌋V V F)"
proof -
have "{} ⊢ β IMP (α OR β)"
by (blast intro: Disj_I2)
hence "quote_all p V ⊢ PfP (ssubst ⌊β⌋V V F) IMP PfP (ssubst ⌊α OR β⌋V V F)"
using assms by (auto simp: quote_all_MonPon_PfP_ssubst)
thus ?thesis
by (metis MP_same prems thin)
qed

lemma quote_all_Conj_I_PfP_ssubst:
assumes "V ⊆ Vs" "supp α ⊆ atom ` Vs" "supp β ⊆ atom ` Vs"
and prems: "H ⊢ PfP (ssubst ⌊α⌋V V F)" "H ⊢ PfP (ssubst ⌊β⌋V V F)" "quote_all p V ⊆ H"
shows "H ⊢ PfP (ssubst ⌊α AND β⌋V V F)"
proof -
have "{} ⊢ α IMP β IMP (α AND β)"
by blast
hence "quote_all p V
⊢ PfP (ssubst ⌊α⌋V V F) IMP PfP (ssubst ⌊β⌋V V F) IMP PfP (ssubst ⌊α AND β⌋V V F)"
using assms by (auto simp: quote_all_MonPon2_PfP_ssubst)
thus ?thesis
by (metis MP_same prems thin)
qed

lemma quote_all_Contra_PfP_ssubst:
assumes "V ⊆ Vs" "supp α ⊆ atom ` Vs"
shows "quote_all p V
⊢ PfP (ssubst ⌊α⌋V V F) IMP PfP (ssubst ⌊Neg α⌋V V F) IMP PfP (ssubst ⌊Fls⌋V V F)"
proof -
have "{} ⊢ α IMP Neg α IMP Fls"
by blast
thus ?thesis
using assms by (auto simp: quote_all_MonPon2_PfP_ssubst supp_conv_fresh)
qed

lemma fresh_ssubst_dbtm: "⟦atom i ♯ p∙V; V ⊆ Vs⟧ ⟹ atom i ♯ ssubst (vquot_dbtm V t) V F"
by (induct t rule: dbtm.induct) (auto simp: F_unfold fresh_image permute_set_eq_image)

lemma fresh_ssubst_dbfm: "⟦atom i ♯ p∙V; V ⊆ Vs⟧ ⟹ atom i ♯ ssubst (vquot_dbfm V A) V F"
by (nominal_induct A rule: dbfm.strong_induct) (auto simp: fresh_ssubst_dbtm)

lemma fresh_ssubst_fm:
fixes A::fm shows "⟦atom i ♯ p∙V; V ⊆ Vs⟧ ⟹ atom i ♯ ssubst (⌊A⌋V) V F"

end

section ‹Star Property. Equality and Membership: Lemmas 9.3 and 9.4›

lemma SeqQuoteP_Mem_imp_QMem_and_Subset:
assumes "atom i ♯ (j,j',i',si,ki,sj,kj)" "atom i' ♯ (j,j',si,ki,sj,kj)"
"atom j ♯ (j',si,ki,sj,kj)" "atom j' ♯ (si,ki,sj,kj)"
"atom si ♯ (ki,sj,kj)" "atom sj ♯ (ki,kj)"
shows "{SeqQuoteP (Var i) (Var i') (Var si) ki, SeqQuoteP (Var j) (Var j') (Var sj) kj}
⊢ (Var i IN Var j IMP PfP (Q_Mem (Var i') (Var j')))  AND
(Var i SUBS Var j IMP PfP (Q_Subset (Var i') (Var j')))"
proof -
obtain k::name and l::name and li::name and lj::name
and m::name and n::name and sm::name and sn::name and sm'::name and sn'::name
where atoms: "atom lj ♯ (li,l,i,j,j',i',si,ki,sj,kj,i,i',k,m,n,sm,sm',sn,sn')"
"atom li ♯ (l,j,j',i,i',si,ki,sj,kj,i,i',k,m,n,sm,sm',sn,sn')"
"atom l ♯ (j,j',i,i',si,ki,sj,kj,i,i',k,m,n,sm,sm',sn,sn')"
"atom k ♯ (j,j',i,i',si,ki,sj,kj,m,n,sm,sm',sn,sn')"
"atom m ♯ (j,j',i,i',si,ki,sj,kj,n,sm,sm',sn,sn')"
"atom n ♯ (j,j',i,i',si,ki,sj,kj,sm,sm',sn,sn')"
"atom sm ♯ (j,j',i,i',si,ki,sj,kj,sm',sn,sn')"
"atom sm' ♯ (j,j',i,i',si,ki,sj,kj,sn,sn')"
"atom sn ♯ (j,j',i,i',si,ki,sj,kj,sn')"
"atom sn' ♯ (j,j',i,i',si,ki,sj,kj)"
by (metis obtain_fresh)
have "{OrdP(Var k)}
⊢ All i (All i' (All si (All li (All j (All j' (All sj (All lj
(SeqQuoteP (Var i) (Var i') (Var si) (Var li) IMP
SeqQuoteP (Var j) (Var j') (Var sj) (Var lj) IMP
HaddP (Var li) (Var lj) (Var k) IMP
( (Var i IN Var j IMP PfP (Q_Mem (Var i') (Var j')))  AND
(Var i SUBS Var j IMP PfP (Q_Subset (Var i') (Var j'))))))))))))"
(is "_ ⊢ ?scheme")
proof (rule OrdIndH [where j=l])
show "atom l ♯ (k, ?scheme)" using atoms
by simp
next
define V p where "V = {i,j,sm,sn}"
and "p = (atom i ⇌ atom i') + (atom j ⇌ atom j') +
(atom sm ⇌ atom sm') + (atom sn ⇌ atom sn')"
define F where "F ≡ make_F V p"
interpret qp: quote_perm p V F
proof unfold_locales
show "finite V" by (simp add: V_def)
show "atom ` (p ∙ V) ♯* V"
using atoms assms
by (auto simp: p_def V_def F_def make_F_def fresh_star_def fresh_finite_insert)
show "-p = p"  using assms atoms
show "F ≡ make_F V p"
by (rule F_def)
qed
have V_mem: "i ∈ V" "j ∈ V" "sm ∈ V" "sn ∈ V"
by (auto simp: V_def)  ― ‹Part of (2) from page 32›
have Mem1: "{} ⊢ (Var i IN Var sm) IMP (Var i IN Eats (Var sm) (Var sn))"
by (blast intro: Mem_Eats_I1)
have Q_Mem1: "quote_all p V
⊢ PfP (Q_Mem (Var i') (Var sm')) IMP
PfP (Q_Mem (Var i') (Q_Eats (Var sm') (Var sn')))"
using qp.quote_all_MonPon_PfP_ssubst [OF Mem1 subset_refl] assms atoms V_mem
have Mem2: "{} ⊢ (Var i EQ Var sn) IMP (Var i IN Eats (Var sm) (Var sn))"
by (blast intro: Mem_Eats_I2)
have Q_Mem2: "quote_all p V
⊢ PfP (Q_Eq (Var i') (Var sn')) IMP
PfP (Q_Mem (Var i') (Q_Eats (Var sm') (Var sn')))"
using qp.quote_all_MonPon_PfP_ssubst [OF Mem2 subset_refl] assms atoms V_mem
have Subs1: "{} ⊢ Zero SUBS Var j"
by blast
have Q_Subs1: "{QuoteP (Var j) (Var j')} ⊢ PfP (Q_Subset Zero (Var j'))"
using qp.quote_all_PfP_ssubst [OF Subs1, of "{j}"] assms atoms
by (simp add: qp.ssubst_Subset vquot_tm_def supp_conv_fresh fresh_at_base del: qp.ssubst_single)
have Subs2: "{} ⊢ Var sm SUBS Var j IMP Var sn IN Var j IMP Eats (Var sm) (Var sn) SUBS Var j"
by blast
have Q_Subs2: "quote_all p V
⊢ PfP (Q_Subset (Var sm') (Var j')) IMP
PfP (Q_Mem (Var sn') (Var j')) IMP
PfP (Q_Subset (Q_Eats (Var sm') (Var sn')) (Var j'))"
using qp.quote_all_MonPon2_PfP_ssubst [OF Subs2 subset_refl] assms atoms V_mem
by (simp add: qp.ssubst_Subset vquot_tm_def supp_conv_fresh subset_eq fresh_at_base)
(simp add: vquot_fm_def qp.F_unfold p_def V_def)
have Ext: "{} ⊢ Var i SUBS Var sn IMP Var sn SUBS Var i IMP Var i EQ Var sn"
by (blast intro: Equality_I)
have Q_Ext: "{QuoteP (Var i) (Var i'), QuoteP (Var sn) (Var sn')}
⊢ PfP (Q_Subset (Var i') (Var sn')) IMP
PfP (Q_Subset (Var sn') (Var i')) IMP
PfP (Q_Eq (Var i') (Var sn'))"
using qp.quote_all_MonPon2_PfP_ssubst [OF Ext, of "{i,sn}"] assms atoms
by (simp add: qp.ssubst_Subset vquot_tm_def supp_conv_fresh subset_eq fresh_at_base
del: qp.ssubst_single)
(simp add: vquot_fm_def qp.F_unfold p_def V_def)
show "{} ⊢ All k (OrdP (Var k) IMP (All2 l (Var k) (?scheme(k::= Var l)) IMP ?scheme))"
apply (rule All_I Imp_I)+
using atoms assms
apply simp_all
apply (rule cut_same [where A = "QuoteP (Var i) (Var i')"])
apply (blast intro: QuoteP_I)
apply (rule cut_same [where A = "QuoteP (Var j) (Var j')"])
apply (blast intro: QuoteP_I)
apply (rule rotate6)
apply (rule Conj_I)
― ‹@{term"Var i IN Var j IMP PfP (Q_Mem (Var i') (Var j'))"}›
apply (rule cut_same)
apply (rule cut1 [OF SeqQuoteP_lemma [of m "Var j" "Var j'" "Var sj" "Var lj" n sm sm' sn sn']], simp_all, blast)
apply (rule Imp_I Disj_EH Conj_EH)+
― ‹case 1, @{term "Var j EQ Zero"}›
apply (rule cut_same [where A = "Var i IN Zero"])
apply (blast intro: Mem_cong [THEN Iff_MP_same], blast)
― ‹case 2, @{term "Var j EQ Eats (Var sm) (Var sn)"}›
apply (rule Imp_I Conj_EH Ex_EH)+
apply simp_all
apply (rule Var_Eq_subst_Iff [THEN rotate2, THEN Iff_MP_same], simp)
apply (rule cut_same [where A = "QuoteP (Var sm) (Var sm')"])
apply (blast intro: QuoteP_I)
apply (rule cut_same [where A = "QuoteP (Var sn) (Var sn')"])
apply (blast intro: QuoteP_I)
apply (rule cut_same [where A = "Var i IN Eats (Var sm) (Var sn)"])
apply (rule Mem_cong [OF Refl, THEN Iff_MP_same])
apply (rule AssumeH Mem_Eats_E)+
― ‹Eats case 1. IH for sm›
apply (rule cut_same [where A = "OrdP (Var m)"])
apply (blast intro: Hyp Ord_IN_Ord SeqQuoteP_imp_OrdP [THEN cut1])
apply (rule cut_same [OF exists_HaddP [where j=l and x="Var li" and y="Var m"]])
apply auto
apply (rule All2_E [where x="Var l", THEN rotate13], simp_all)
apply (blast intro: Hyp HaddP_Mem_cancel_left [THEN Iff_MP2_same] SeqQuoteP_imp_OrdP [THEN cut1])
apply (rule All_E [where x="Var i"], simp)
apply (rule All_E [where x="Var i'"], simp)
apply (rule All_E [where x="Var si"], simp)
apply (rule All_E [where x="Var li"], simp)
apply (rule All_E [where x="Var sm"], simp)
apply (rule All_E [where x="Var sm'"], simp)
apply (rule All_E [where x="Var sj"], simp)
apply (rule All_E [where x="Var m"], simp)
apply (force intro: MP_thin [OF Q_Mem1] simp add: V_def p_def)
― ‹Eats case 2›
apply (rule rotate13)
apply (rule cut_same [where A = "OrdP (Var n)"])
apply (blast intro: Hyp Ord_IN_Ord SeqQuoteP_imp_OrdP [THEN cut1])
apply (rule cut_same [OF exists_HaddP [where j=l and x="Var li" and y="Var n"]])
apply auto
apply (rule MP_same)
apply (rule Q_Mem2 [THEN thin])
apply (rule MP_same)
apply (rule MP_same)
apply (rule Q_Ext [THEN thin])
― ‹@{term"PfP (Q_Subset (Var i') (Var sn'))"}›
apply (rule All2_E [where x="Var l", THEN rotate14], simp_all)
apply (blast intro: Hyp HaddP_Mem_cancel_left [THEN Iff_MP2_same] SeqQuoteP_imp_OrdP [THEN cut1])
apply (rule All_E [where x="Var i"], simp)
apply (rule All_E [where x="Var i'"], simp)
apply (rule All_E [where x="Var si"], simp)
apply (rule All_E [where x="Var li"], simp)
apply (rule All_E [where x="Var sn"], simp)
apply (rule All_E [where x="Var sn'"], simp)
apply (rule All_E [where x="Var sj"], simp)
apply (rule All_E [where x="Var n"], simp)
apply (rule Imp_E, blast intro: Hyp)+
apply (rule Conj_E)
apply (rule thin1)
apply (blast intro!: Imp_E EQ_imp_SUBS [THEN cut1])
― ‹@{term"PfP (Q_Subset (Var sn') (Var i'))"}›
apply (rule All2_E [where x="Var l", THEN rotate14], simp_all)
apply (blast intro: Hyp HaddP_Mem_cancel_left [THEN Iff_MP2_same] SeqQuoteP_imp_OrdP [THEN cut1])
apply (rule All_E [where x="Var sn"], simp)
apply (rule All_E [where x="Var sn'"], simp)
apply (rule All_E [where x="Var sj"], simp)
apply (rule All_E [where x="Var n"], simp)
apply (rule All_E [where x="Var i"], simp)
apply (rule All_E [where x="Var i'"], simp)
apply (rule All_E [where x="Var si"], simp)
apply (rule All_E [where x="Var li"], simp)
apply (rule Imp_E, blast intro: Hyp)+
apply (rule Imp_E)
apply (blast intro: Hyp HaddP_commute [THEN cut2] SeqQuoteP_imp_OrdP [THEN cut1])
apply (rule Conj_E)
apply (rule thin1)
apply (blast intro!: Imp_E EQ_imp_SUBS2 [THEN cut1])
― ‹@{term"Var i SUBS Var j IMP PfP (Q_Subset (Var i') (Var j'))"}›
apply (rule cut_same)
apply (rule cut1 [OF SeqQuoteP_lemma [of m "Var i" "Var i'" "Var si" "Var li" n sm sm' sn sn']], simp_all, blast)
apply (rule Imp_I Disj_EH Conj_EH)+
― ‹case 1, Var i EQ Zero›
apply (rule cut_same [where A = "PfP (Q_Subset Zero (Var j'))"])
apply (blast intro: Q_Subs1 [THEN cut1] SeqQuoteP_imp_QuoteP [THEN cut1])
apply (force intro: Var_Eq_subst_Iff [THEN Iff_MP_same, THEN rotate3])
― ‹case 2, @{term "Var i EQ Eats (Var sm) (Var sn)"}›
apply (rule Conj_EH Ex_EH)+
apply simp_all
apply (rule cut_same [where A = "OrdP (Var lj)"])
apply (blast intro: Hyp SeqQuoteP_imp_OrdP [THEN cut1])
apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same, THEN rotate3], simp)
apply (rule cut_same [where A = "QuoteP (Var sm) (Var sm')"])
apply (blast intro: QuoteP_I)
apply (rule cut_same [where A = "QuoteP (Var sn) (Var sn')"])
apply (blast intro: QuoteP_I)
apply (rule cut_same [where A = "Eats (Var sm) (Var sn) SUBS Var j"])
apply (rule Subset_cong [OF _ Refl, THEN Iff_MP_same])
apply (rule AssumeH Mem_Eats_E)+
― ‹Eats case split›
apply (rule Eats_Subset_E)
apply (rule rotate15)
apply (rule MP_same [THEN MP_same])
apply (rule Q_Subs2 [THEN thin])
― ‹Eats case 1: @{term "PfP (Q_Subset (Var sm') (Var j'))"}›
apply (rule cut_same [OF exists_HaddP [where j=l and x="Var m" and y="Var lj"]])
apply (rule AssumeH Ex_EH Conj_EH | simp)+
― ‹IH for sm›
apply (rule All2_E [where x="Var l", THEN rotate15], simp_all)
apply (blast intro: Hyp HaddP_Mem_cancel_right_Mem SeqQuoteP_imp_OrdP [THEN cut1])
apply (rule All_E [where x="Var sm"], simp)
apply (rule All_E [where x="Var sm'"], simp)
apply (rule All_E [where x="Var si"], simp)
apply (rule All_E [where x="Var m"], simp)
apply (rule All_E [where x="Var j"], simp)
apply (rule All_E [where x="Var j'"], simp)
apply (rule All_E [where x="Var sj"], simp)
apply (rule All_E [where x="Var lj"], simp)
apply (blast intro: thin1 Imp_E)
― ‹Eats case 2: @{term "PfP (Q_Mem (Var sn') (Var j'))"}›
apply (rule cut_same [OF exists_HaddP [where j=l and x="Var n" and y="Var lj"]])
apply (rule AssumeH Ex_EH Conj_EH | simp)+
― ‹IH for sn›
apply (rule All2_E [where x="Var l", THEN rotate15], simp_all)
apply (blast intro: Hyp HaddP_Mem_cancel_right_Mem SeqQuoteP_imp_OrdP [THEN cut1])
apply (rule All_E [where x="Var sn"], simp)
apply (rule All_E [where x="Var sn'"], simp)
apply (rule All_E [where x="Var si"], simp)
apply (rule All_E [where x="Var n"], simp)
apply (rule All_E [where x="Var j"], simp)
apply (rule All_E [where x="Var j'"], simp)
apply (rule All_E [where x="Var sj"], simp)
apply (rule All_E [where x="Var lj"], simp)
apply (blast intro: Hyp Imp_E)
done
qed
hence p1: "{OrdP(Var k)}
⊢ (All i' (All si (All li
(All j (All j' (All sj (All lj
(SeqQuoteP (Var i) (Var i') (Var si) (Var li) IMP
SeqQuoteP (Var j) (Var j') (Var sj) (Var lj) IMP
HaddP (Var li) (Var lj) (Var k) IMP
(Var i IN Var j IMP PfP (Q_Mem (Var i') (Var j'))) AND
(Var i SUBS Var j IMP PfP (Q_Subset (Var i') (Var j'))))))))))) (i::= Var i)"
by (metis All_D)
have p2: "{OrdP(Var k)}
⊢ (All si (All li
(All j (All j' (All sj (All lj
(SeqQuoteP (Var i) (Var i') (Var si) (Var li) IMP
SeqQuoteP (Var j) (Var j') (Var sj) (Var lj) IMP
HaddP (Var li) (Var lj) (Var k) IMP
(Var i IN Var j IMP PfP (Q_Mem (Var i') (Var j'))) AND
(Var i SUBS Var j IMP PfP (Q_Subset (Var i') (Var j'))))))))))(i'::= Var i')"
apply (rule All_D)
using atoms p1 by simp
have p3: "{OrdP(Var k)}
⊢ (All li
(All j (All j' (All sj (All lj
(SeqQuoteP (Var i) (Var i') (Var si) (Var li) IMP
SeqQuoteP (Var j) (Var j') (Var sj) (Var lj) IMP
HaddP (Var li) (Var lj) (Var k) IMP
(Var i IN Var j IMP PfP (Q_Mem (Var i') (Var j'))) AND
(Var i SUBS Var j IMP PfP (Q_Subset (Var i') (Var j'))))))))) (si::= Var si)"
apply (rule All_D)
using atoms p2 by simp
have p4: "{OrdP(Var k)}
⊢ (All j (All j' (All sj (All lj
(SeqQuoteP (Var i) (Var i') (Var si) (Var li) IMP
SeqQuoteP (Var j) (Var j') (Var sj) (Var lj) IMP
HaddP (Var li) (Var lj) (Var k) IMP
(Var i IN Var j IMP PfP (Q_Mem (Var i') (Var j'))) AND
(Var i SUBS Var j IMP PfP (Q_Subset (Var i') (Var j')))))))) (li::= ki)"
apply (rule All_D)
using atoms p3 by simp
have p5: "{OrdP(Var k)}
⊢ (All j' (All sj (All lj
(SeqQuoteP (Var i) (Var i') (Var si) ki IMP
SeqQuoteP (Var j) (Var j') (Var sj) (Var lj) IMP
HaddP ki (Var lj) (Var k) IMP
(Var i IN Var j IMP PfP (Q_Mem (Var i') (Var j'))) AND
(Var i SUBS Var j IMP PfP (Q_Subset (Var i') (Var j'))))))) (j::= Var j)"
apply (rule All_D)
using atoms assms p4 by simp
have p6: "{OrdP(Var k)}
⊢ (All sj (All lj
(SeqQuoteP (Var i) (Var i') (Var si) ki IMP
SeqQuoteP (Var j) (Var j') (Var sj) (Var lj) IMP
HaddP ki (Var lj) (Var k) IMP
(Var i IN Var j IMP PfP (Q_Mem (Var i') (Var j'))) AND
(Var i SUBS Var j IMP PfP (Q_Subset (Var i') (Var j')))))) (j'::= Var j')"
apply (rule All_D)
using atoms p5 by simp
have p7: "{OrdP(Var k)}
⊢ (All lj (SeqQuoteP (Var i) (Var i') (Var si) ki IMP
SeqQuoteP (Var j) (Var j') (Var sj) (Var lj) IMP
HaddP ki (Var lj) (Var k) IMP
(Var i IN Var j IMP PfP (Q_Mem (Var i') (Var j'))) AND
(Var i SUBS Var j IMP PfP (Q_Subset (Var i') (Var j'))))) (sj::= Var sj)"
apply (rule All_D)
using atoms p6 by simp
have p8: "{OrdP(Var k)}
⊢ (SeqQuoteP (Var i) (Var i') (Var si) ki IMP
SeqQuoteP (Var j) (Var j') (Var sj) (Var lj) IMP
HaddP ki (Var lj) (Var k) IMP
(Var i IN Var j IMP PfP (Q_Mem (Var i') (Var j'))) AND
(Var i SUBS Var j IMP PfP (Q_Subset (Var i') (Var j')))) (lj::= kj)"
apply (rule All_D)
using atoms p7 by simp
hence p9: "{OrdP(Var k)}
⊢ SeqQuoteP (Var i) (Var i') (Var si) ki IMP
SeqQuoteP (Var j) (Var j') (Var sj) kj IMP
HaddP ki kj (Var k) IMP
(Var i IN Var j IMP PfP (Q_Mem (Var i') (Var j'))) AND
(Var i SUBS Var j IMP PfP (Q_Subset (Var i') (Var j')))"
using assms atoms by simp
have p10:  "{ HaddP ki kj (Var k),
SeqQuoteP (Var i) (Var i') (Var si) ki,
SeqQuoteP (Var j) (Var j') (Var sj) kj, OrdP (Var k) }
⊢ (Var i IN Var j IMP PfP (Q_Mem (Var i') (Var j'))) AND
(Var i SUBS Var j IMP PfP (Q_Subset (Var i') (Var j')))"
apply (rule MP_same [THEN MP_same [THEN MP_same]])
apply (rule p9 [THEN thin])
apply (auto intro: MP_same)
done
show ?thesis
apply (rule cut_same [OF exists_HaddP [where j=k and x=ki and y=kj]])
apply (metis SeqQuoteP_imp_OrdP thin1)
prefer 2
apply (rule Ex_E)
apply (rule p10 [THEN cut4])
using assms atoms
apply (auto intro: HaddP_OrdP SeqQuoteP_imp_OrdP [THEN cut1])
done
qed

lemma
assumes "atom i ♯ (j,j',i')" "atom i' ♯ (j,j')" "atom j ♯ (j')"
shows QuoteP_Mem_imp_QMem:
"{QuoteP (Var i) (Var i'), QuoteP (Var j) (Var j'), Var i IN Var j}
⊢ PfP (Q_Mem (Var i') (Var j'))"     (is ?thesis1)
and QuoteP_Mem_imp_QSubset:
"{QuoteP (Var i) (Var i'), QuoteP (Var j) (Var j'), Var i SUBS Var j}
⊢ PfP (Q_Subset (Var i') (Var j'))"  (is ?thesis2)
proof -
obtain si::name and ki::name and sj::name and kj::name
where atoms: "atom si ♯ (ki,sj,kj,i,j,j',i')"  "atom ki ♯ (sj,kj,i,j,j',i')"
"atom sj ♯ (kj,i,j,j',i')"  "atom kj ♯ (i,j,j',i')"
by (metis obtain_fresh)
hence C:  "{QuoteP (Var i) (Var i'), QuoteP (Var j) (Var j')}
⊢ (Var i IN Var j IMP PfP (Q_Mem (Var i') (Var j')))  AND
(Var i SUBS Var j IMP PfP (Q_Subset (Var i') (Var j')))"
using assms
by (auto simp: QuoteP.simps [of si "Var i" _ ki] QuoteP.simps [of sj "Var j" _ kj]
intro!: SeqQuoteP_Mem_imp_QMem_and_Subset del: Conj_I)
show ?thesis1
by (best intro: Conj_E1 [OF C, THEN MP_thin])
show ?thesis2
by (best intro: Conj_E2 [OF C, THEN MP_thin])
qed

section ‹Star Property. Universal Quantifier: Lemma 9.7›

lemma (in quote_perm) SeqQuoteP_Mem_imp_All2:
assumes IH: "insert (QuoteP (Var i) (Var i')) (quote_all p Vs)
⊢ α IMP PfP (ssubst ⌊α⌋(insert i Vs) (insert i Vs) Fi)"
and sp: "supp α - {atom i} ⊆ atom ` Vs"
and j: "j ∈ Vs" and j': "p ∙ j = j'"
and pi: "pi = (atom i ⇌ atom i') + p"
and Fi: "Fi = make_F (insert i Vs) pi"
and atoms: "atom i ♯ (j,j',s,k,p)" "atom i' ♯ (i,p,α)"
"atom j ♯ (j',s,k,α)" "atom j' ♯ (s,k,α)"
"atom s ♯ (k,α)" "atom k ♯ (α,p)"
shows "insert (SeqQuoteP (Var j) (Var j') (Var s) (Var k)) (quote_all p (Vs-{j}))
⊢ All2 i (Var j) α IMP PfP (ssubst ⌊All2 i (Var j) α⌋Vs Vs F)"
proof -
have pj' [simp]: "p ∙ j' = j" using pinv j'
by (metis permute_minus_cancel(2))
have [simp]: "F j = Var j'" using j j'
by (auto simp: F_unfold)
hence i': "atom i' ♯ Vs" using atoms
by (auto simp: Vs)
have fresh_ss [simp]: "⋀i A::fm. atom i ♯ p ⟹ atom i ♯ ssubst (⌊A⌋Vs) Vs F"
obtain l::name and m::name and n::name and sm::name and sn::name and sm'::name and sn'::name
where atoms': "atom l ♯ (p,α,i,j,j',s,k,m,n,sm,sm',sn,sn')"
"atom m ♯ (p,α,i,j,j',s,k,n,sm,sm',sn,sn')" "atom n ♯ (p,α,i,j,j',s,k,sm,sm',sn,sn')"
"atom sm ♯ (p,α,i,j,j',s,k,sm',sn,sn')" "atom sm' ♯ (p,α,i,j,j',s,k,sn,sn')"
"atom sn ♯ (p,α,i,j,j',s,k,sn')" "atom sn' ♯ (p,α,i,j,j',s,k)"
by (metis obtain_fresh)
define V' p'
where "V' = {sm,sn} ∪ Vs"
and "p' = (atom sm ⇌ atom sm') + (atom sn ⇌ atom sn') + p"
define F' where "F' ≡ make_F V' p'"
interpret qp': quote_perm p' V' F'
proof unfold_locales
show "finite V'" by (simp add: V'_def)
show "atom ` (p' ∙ V') ♯* V'"
using atoms atoms' p
by (auto simp: p'_def V'_def swap_fresh_fresh fresh_at_base_permI
fresh_star_finite_insert fresh_finite_insert atom_fresh_star_atom_set_conv)
show "F' ≡ make_F V' p'"
by (rule F'_def)
show "- p' = p'" using atoms atoms' pinv
qed
have All2_Zero: "{} ⊢ All2 i Zero α"
by auto
have Q_All2_Zero:
"quote_all p Vs ⊢ PfP (Q_All (Q_Imp (Q_Mem (Q_Ind Zero) Zero)
(ssubst (vquot_dbfm Vs (trans_fm [i] α)) Vs F)))"
using quote_all_PfP_ssubst [OF All2_Zero] assms
by (force simp add: vquot_fm_def supp_conv_fresh)
have All2_Eats: "{} ⊢ All2 i (Var sm) α IMP α(i::=Var sn) IMP All2 i (Eats (Var sm) (Var sn)) α"
using atoms'  apply auto
apply (rule Ex_I [where x = "Var i"], auto)
apply (rule rotate2)
apply (blast intro: ContraProve Var_Eq_imp_subst_Iff [THEN Iff_MP_same])
done
have [simp]: "F' sm = Var sm'" "F' sn = Var sn'" using atoms'
by (auto simp: V'_def p'_def qp'.F_unfold swap_fresh_fresh fresh_at_base_permI)
have smn' [simp]: "sm ∈ V'" "sn ∈ V'" "sm ∉ Vs" "sn ∉ Vs" using atoms'
by (auto simp: V'_def fresh_finite_set_at_base [symmetric])
hence Q_All2_Eats: "quote_all p' V'
⊢ PfP (ssubst ⌊All2 i (Var sm) α⌋V' V' F') IMP
PfP (ssubst ⌊α(i::=Var sn)⌋V' V' F') IMP
PfP (ssubst ⌊All2 i (Eats (Var sm) (Var sn)) α⌋V' V' F')"
using sp  qp'.quote_all_MonPon2_PfP_ssubst [OF All2_Eats subset_refl]
by (simp add: supp_conv_fresh subset_eq V'_def)
(metis Diff_iff empty_iff fresh_ineq_at_base insertE mem_Collect_eq)
interpret qpi: quote_perm pi "insert i Vs" Fi
unfolding pi
apply (rule qp_insert) using atoms
apply (auto simp: Fi pi)
done
have F'_eq_F: "⋀name. name ∈ Vs ⟹ F' name = F name"
using atoms'
by (auto simp: F_unfold qp'.F_unfold p'_def swap_fresh_fresh V'_def fresh_pj)
{ fix t::dbtm
assume "supp t ⊆ atom ` V'" "supp t ⊆ atom ` Vs"
hence "ssubst (vquot_dbtm V' t) V' F' = ssubst (vquot_dbtm Vs t) Vs F"
by (induction t rule: dbtm.induct) (auto simp: F'_eq_F)
} note ssubst_v_tm = this
{ fix A::dbfm
assume "supp A ⊆ atom ` V'" "supp A ⊆ atom ` Vs"
hence "ssubst (vquot_dbfm V' A) V' F' = ssubst (vquot_dbfm Vs A) Vs F"
by (induction A rule: dbfm.induct) (auto simp: ssubst_v_tm F'_eq_F)
} note ssubst_v_fm = this
have ss_noprimes: "ssubst (vquot_dbfm V' (trans_fm [i] α)) V' F' =
ssubst (vquot_dbfm Vs (trans_fm [i] α)) Vs F"
apply (rule ssubst_v_fm)
using sp  apply (auto simp: V'_def supp_conv_fresh)
done
{ fix t::dbtm
assume "supp t - {atom i} ⊆ atom ` Vs"
hence "subst i' (Var sn') (ssubst (vquot_dbtm (insert i Vs) t) (insert i Vs) Fi) =
ssubst (vquot_dbtm V' (subst_dbtm (DBVar sn) i t)) V' F'"
apply (induction t rule: dbtm.induct)
using atoms atoms'
apply (auto simp: vquot_tm_def pi V'_def qpi.F_unfold qp'.F_unfold p'_def fresh_pj swap_fresh_fresh fresh_at_base_permI)
done
} note perm_v_tm = this
{ fix A::dbfm
assume "supp A - {atom i} ⊆ atom ` Vs"
hence "subst i' (Var sn') (ssubst (vquot_dbfm (insert i Vs) A) (insert i Vs) Fi) =
ssubst (vquot_dbfm V' (subst_dbfm (DBVar sn) i A)) V' F'"
by (induct A rule: dbfm.induct) (auto simp: Un_Diff perm_v_tm)
} note```