Theory Incompleteness.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 (blast intro: HaddP_Mem_I Mem_SUCC_I1)
       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 (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)
     ― ‹... 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 (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)
     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
        apply (simp_all add: fresh_at_base fresh_finite_set_at_base)
        ― ‹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 {} = {}"
  by (simp add: quote_all_def)

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"
  by (simp add: fresh_ssubst_dbfm vquot_fm_def) 

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
            by (simp add: p_def add.assoc perm_self_inverseI fresh_swap fresh_plus_perm)
          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
         by (simp add: vquot_fm_def qp.Vs) (simp add: qp.F_unfold p_def)
      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
         by (simp add: vquot_fm_def qp.Vs) (simp add: qp.F_unfold p_def)
      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)
            (simp add: qp.F_unfold p_def V_def)
      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 (simp add: V_def p_def)
        apply (rule MP_same)
        apply (rule MP_same)
        apply (rule Q_Ext [THEN thin])
        apply (simp add: V_def p_def)
        ― ‹@{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])
        apply (simp add: V_def p_def)
        ― ‹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"
    by (simp add: vquot_fm_def fresh_ssubst_dbfm)
  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
        by (simp add: p'_def add.assoc perm_self_inverseI fresh_swap fresh_plus_perm)
    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 perm_v_fm = this
  have "quote_all p Vs ⊢ QuoteP (Var i) (Var i') IMP 
                 (α IMP PfP (ssubst ⌊α⌋(insert i Vs) (insert i Vs) Fi))"
    using IH by auto
  hence "quote_all p Vs 
         ⊢ (QuoteP (Var i) (Var i') IMP 
                 (α IMP PfP (ssubst ⌊α⌋(insert i Vs) (insert i Vs) Fi))) (i'::=Var sn')"
    using atoms IH
    by (force intro!: Subst elim!: fresh_quote_all_mem)
  hence "quote_all p Vs 
         ⊢ QuoteP (Var i) (Var sn') IMP 
           (α IMP PfP (subst i' (Var sn') (ssubst ⌊α⌋(insert i Vs) (insert i Vs) Fi)))"
    using atoms by simp
  moreover have "subst i' (Var sn') (ssubst ⌊α⌋(insert i Vs) (insert i Vs) Fi)
                 = ssubst ⌊α(i::=Var sn)⌋V' V' F'"
    using sp
    by (auto simp: vquot_fm_def perm_v_fm supp_conv_fresh subst_fm_trans_commute [symmetric])
  ultimately 
  have "quote_all p Vs 
         ⊢ QuoteP (Var i) (Var sn') IMP (α IMP PfP (ssubst ⌊α(i::=Var sn)⌋V' V' F'))"
    by simp
  hence "quote_all p Vs 
         ⊢ (QuoteP (Var i) (Var sn') IMP (α IMP PfP (ssubst ⌊α(i::=Var sn)⌋V' V' F'))) (i::=Var sn)"
    using ‹atom i ♯ _›
    by (force intro!: Subst elim!: fresh_quote_all_mem)
  hence "quote_all p Vs 
         ⊢ (QuoteP (Var sn) (Var sn') IMP 
           (α(i::=Var sn) IMP PfP (subst i (Var sn) (ssubst ⌊α(i::=Var sn)⌋V' V' F'))))"
    using atoms atoms' by simp
  moreover have "subst i (Var sn) (ssubst ⌊α(i::=Var sn)⌋V' V' F')
                 = ssubst ⌊α(i::=Var sn)⌋V' V' F'"
    using atoms atoms' i'
    by (auto simp: swap_fresh_fresh fresh_at_base_permI p'_def 
             intro!: forget_subst_tm [OF qp'.fresh_ssubst'])
  ultimately 
  have "quote_all p Vs 
         ⊢ QuoteP (Var sn) (Var sn') IMP (α(i::=Var sn) IMP PfP (ssubst ⌊α(i::=Var sn)⌋V' V' F'))"
    using atoms atoms' by simp
  hence star0: "insert (QuoteP (Var sn) (Var sn')) (quote_all p Vs) 
                ⊢ α(i::=Var sn) IMP PfP (ssubst ⌊α(i::=Var sn)⌋V' V' F')"
    by (rule anti_deduction)
  have subst_i_star: "quote_all p' V' ⊢ α(i::=Var sn) IMP PfP (ssubst ⌊α(i::=Var sn)⌋V' V' F')"
    apply (rule thin [OF star0])
    using atoms'
    apply (force simp: V'_def p'_def fresh_swap fresh_plus_perm fresh_at_base_permI add.assoc 
                       quote_all_perm_eq)
    done
  have "insert (OrdP (Var k)) (quote_all p (Vs-{j}))
        ⊢ All j (All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var k) IMP
                         All2 i (Var j) α IMP PfP (ssubst ⌊All2 i (Var j) α⌋Vs Vs F)))"
        (is "_ ⊢ ?scheme")
    proof (rule OrdIndH [where j=l])
      show "atom l ♯ (k, ?scheme)" using atoms atoms' j j' fresh_pVs
        by (simp add: fresh_Pair F_unfold)
    next
      have substj: "⋀t j. atom j ♯ α ⟹ atom (p ∙ j) ♯ α ⟹ 
                           subst j t (ssubst (vquot_dbfm Vs (trans_fm [i] α)) Vs F) = 
                           ssubst (vquot_dbfm Vs (trans_fm [i] α)) Vs F"
        by (auto simp: fresh_ssubst')
      { fix W 
        assume W: "W ⊆ Vs"
        hence "finite W" by (metis Vs infinite_super)
        hence "quote_all p' W = quote_all p W" using W
        proof (induction)
          case empty thus ?case
            by simp
        next
          case (insert w W) 
          hence "w ∈ Vs" "atom sm ♯ p ∙ Vs" "atom sm' ♯ p ∙ Vs" "atom sn ♯ p ∙ Vs" "atom sn' ♯ p ∙ Vs"
            using atoms' Vs by (auto simp: fresh_pVs)
          hence "atom sm ♯ p ∙ w" "atom sm' ♯ p ∙ w" "atom sn ♯ p ∙ w" "atom sn' ♯ p ∙ w"
            by (metis Vs fresh_at_base(2) fresh_finite_set_at_base fresh_permute_left)+
          thus ?case using insert 
          by (simp add: p'_def swap_fresh_fresh)
        qed 
      }
      hence "quote_all p' Vs = quote_all p Vs"
        by (metis subset_refl)
      also have "... = insert (QuoteP (Var j) (Var j')) (quote_all p (Vs - {j}))"
        using j j' by (auto simp: quote_all_def)
      finally have "quote_all p' V' = 
                    {QuoteP (Var sn) (Var sn'), QuoteP (Var sm) (Var sm')} ∪ 
                    insert (QuoteP (Var j) (Var j')) (quote_all p (Vs - {j}))"
        using atoms'
        by (auto simp: p'_def V'_def fresh_at_base_permI Collect_disj_Un)
      also have "... = {QuoteP (Var sn) (Var sn'), QuoteP (Var sm) (Var sm'), QuoteP (Var j) (Var j')}
                       ∪ quote_all p (Vs - {j})"
        by blast
      finally have quote_all'_eq: 
            "quote_all p' V' = 
              {QuoteP (Var sn) (Var sn'), QuoteP (Var sm) (Var sm'), QuoteP (Var j) (Var j')}
              ∪ quote_all p (Vs - {j})" .
      have pjV: "p ∙ j ∉ Vs" 
        by (metis j perm_exits_Vs) 
      hence jpV: "atom j ♯ p ∙ Vs" 
        by (simp add: fresh_permute_left pinv fresh_finite_set_at_base)
      show "quote_all p (Vs-{j}) ⊢ All k (OrdP (Var k) IMP (All2 l (Var k) (?scheme(k::= Var l)) IMP ?scheme))"
        apply (rule All_I Imp_I)+
        using atoms atoms' j jpV pjV
        apply (auto simp: fresh_at_base fresh_finite_set_at_base j' elim!: fresh_quote_all_mem)
        apply (rule cut_same [where A = "QuoteP (Var j) (Var j')"])
        apply (blast intro: QuoteP_I)
        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 (simp add: vquot_fm_def)
        apply (rule thin1)
        apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same], simp)
        apply (simp add: substj)
        apply (rule Q_All2_Zero [THEN thin])
        using assms
        apply (simp add: quote_all_def, blast)
        ― ‹case 2, @{term "Var j EQ Eats (Var sm) (Var sn)"}›
        apply (rule Imp_I Conj_EH Ex_EH)+
        using atoms  apply (auto elim!: fresh_quote_all_mem)
        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)
        ― ‹Eats case. IH for sm›
        apply (rule All2_E [where x="Var m", THEN rotate12], simp_all, blast)
        apply (rule All_E [where x="Var sm"], simp)
        apply (rule All_E [where x="Var sm'"], simp)
        apply (rule Imp_E, blast)
        ― ‹Setting up the subgoal›
        apply (rule cut_same [where A = "PfP (ssubst ⌊All2 i (Eats (Var sm) (Var sn)) α⌋V' V' F')"])
         defer 1
         apply (rule rotate6)
         apply (simp add: vquot_fm_def)
         apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same], force simp add: substj ss_noprimes j')
        apply (rule cut_same [where A = "All2 i (Eats (Var sm) (Var sn)) α"])
         apply (rule All2_cong [OF Hyp Iff_refl, THEN Iff_MP_same], blast)
          apply (force elim!: fresh_quote_all_mem 
                       simp add: fresh_at_base fresh_finite_set_at_base, blast)
        apply (rule All2_Eats_E, simp)
        apply (rule MP_same [THEN MP_same])
        apply (rule Q_All2_Eats [THEN thin])
        apply (force simp add: quote_all'_eq)
        ― ‹Proving @{term "PfP (ssubst ⌊All2 i (Var sm) α⌋V' V' F')"}›
        apply (force intro!: Imp_E [THEN rotate3] simp add: vquot_fm_def substj j' ss_noprimes)
        ― ‹Proving @{term "PfP (ssubst ⌊α(i::=Var sn)⌋V' V' F')"}›
        apply (rule MP_same [OF subst_i_star [THEN thin]])
        apply (force simp add: quote_all'_eq, blast)
        done
    qed
  hence p1: "insert (OrdP (Var k)) (quote_all p (Vs-{j}))
             ⊢ (All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var k) IMP
                All2 i (Var j) α IMP PfP (ssubst ⌊All2 i (Var j) α⌋Vs Vs F))) (j::=Var j)"
    by (metis All_D)
  have "insert (OrdP (Var k)) (quote_all p (Vs-{j}))
        ⊢ (SeqQuoteP (Var j) (Var j') (Var s) (Var k) IMP
            All2 i (Var j) α IMP PfP (ssubst ⌊All2 i (Var j) α⌋Vs Vs F)) (j'::=Var j')"
    apply (rule All_D)
    using p1 atoms by simp
  thus ?thesis
    using atoms 
    by simp (metis SeqQuoteP_imp_OrdP Imp_cut anti_deduction)
qed

lemma (in quote_perm) quote_all_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 "supp (All2 i (Var j) α) ⊆ atom ` Vs" 
      and j: "atom j ♯ (i,α)" and i: "atom i ♯ p" and i': "atom i' ♯ (i,p,α)" 
      and pi: "pi = (atom i ⇌ atom i') + p" 
      and Fi: "Fi = make_F (insert i Vs) pi"
  shows "insert (All2 i (Var j) α) (quote_all p Vs) ⊢ PfP (ssubst ⌊All2 i (Var j) α⌋Vs Vs F)"
proof -
  have sp: "supp α - {atom i} ⊆ atom ` Vs" and jV: "j ∈ Vs"
    using assms
    by (auto simp: fresh_def supp_Pair)
  obtain s::name and k::name
    where atoms: "atom s ♯ (k,i,j,p∙j,α,p)" "atom k ♯ (i,j,p∙j,α,p)" 
    by (metis obtain_fresh)
  hence ii: "atom i ♯ (j, p ∙ j, s, k, p)" using i j
    by (simp add: fresh_Pair) (metis fresh_at_base(2) fresh_perm fresh_permute_left pinv)
  have jj: "atom j ♯ (p ∙ j, s, k, α)" using atoms j
    by (auto simp: fresh_Pair) (metis atom_fresh_perm jV)
  have pj: "atom (p ∙ j) ♯ (s, k, α)" using atoms ii sp jV
    by (simp add: fresh_Pair) (auto simp: fresh_def perm_exits_Vs dest!: subsetD)
  show ?thesis
    apply (rule cut_same [where A = "QuoteP (Var j) (Var (p ∙ j))"])
    apply (force intro: jV Hyp simp add: quote_all_def)
    using atoms 
    apply (auto simp: QuoteP.simps [of s _ _ k] elim!: fresh_quote_all_mem)
    apply (rule MP_same)
    apply (rule SeqQuoteP_Mem_imp_All2 [OF IH sp jV refl pi Fi ii i' jj pj, THEN thin])
    apply (auto simp: fresh_at_base_permI quote_all_def intro!: fresh_ssubst')
    done
qed


section ‹The Derivability Condition, Theorem 9.1›

lemma SpecI: "H ⊢ A IMP Ex i A"
  by (metis Imp_I Assume Ex_I subst_fm_id)

lemma star:
  fixes p :: perm and F :: "name ⇒ tm"
  assumes C: "ss_fm α" 
      and p: "atom ` (p ∙ V) ♯* V" "-p = p"
      and V: "finite V" "supp α ⊆ atom ` V"
      and F: "F = make_F V p"
    shows "insert α (quote_all p V) ⊢ PfP (ssubst ⌊α⌋V V F)"
using C V p F
proof (nominal_induct avoiding: p arbitrary: V F rule: ss_fm.strong_induct)
    case (MemI i j) show ?case
    proof (cases "i=j")
      case True thus ?thesis
        by auto
    next
      case False
      hence ij: "atom i ♯ j" "{i, j} ⊆ V" using MemI
        by auto  
      interpret qp: quote_perm p V F
        by unfold_locales (auto simp: image_iff F make_F_def p MemI)
      have "insert (Var i IN Var j) (quote_all p V) ⊢ PfP (Q_Mem (Var (p ∙ i)) (Var (p ∙ j)))"
        apply (rule QuoteP_Mem_imp_QMem [of i j, THEN cut3]) 
        using ij  apply (auto simp: quote_all_def qp.atom_fresh_perm intro: Hyp)
        apply (metis atom_eqvt fresh_Pair fresh_at_base(2) fresh_permute_iff qp.atom_fresh_perm)
        done
      thus ?thesis
        apply (simp add: vquot_fm_def) 
        using MemI  apply (auto simp: make_F_def)
        done
    qed
  next
    case (DisjI A B) 
      interpret qp: quote_perm p V F
        by unfold_locales (auto simp: image_iff DisjI)
    show ?case 
      apply auto
      apply (rule_tac [2] qp.quote_all_Disj_I2_PfP_ssubst)
      apply (rule qp.quote_all_Disj_I1_PfP_ssubst)
      using DisjI by auto
  next
    case (ConjI A B) 
      interpret qp: quote_perm p V F
        by unfold_locales (auto simp: image_iff ConjI)
    show ?case 
      apply (rule qp.quote_all_Conj_I_PfP_ssubst)
      using ConjI  by (auto intro: thin1 thin2)
  next
    case (ExI A i)
    interpret qp: quote_perm p V F 
      by unfold_locales (auto simp: image_iff ExI)
    obtain i'::name where i': "atom i' ♯ (i,p,A)"
      by (metis obtain_fresh)
    define p' where "p' = (atom i ⇌ atom i') + p" 
    define F' where "F' = make_F (insert i V) p'"
    have p'_apply [simp]: "!!v. p' ∙ v = (if v=i then i' else if v=i' then i else p ∙ v)"
      using  ‹atom i ♯ p›  i'
      by (auto simp: p'_def fresh_Pair fresh_at_base_permI) 
         (metis atom_eq_iff fresh_at_base_permI permute_eq_iff swap_at_base_simps(3)) 
    have p'V: "p' ∙ V = p ∙ V"
      by (metis i' p'_def permute_plus fresh_Pair qp.fresh_pVs swap_fresh_fresh ‹atom i ♯ p›)
    have i: "i ∉ V" "i ∉ p ∙ V"  "atom i ♯ V" "atom i ♯ p ∙ V"  "atom i ♯ p' ∙ V" using ExI
      by (auto simp: p'V fresh_finite_set_at_base notin_V)
    interpret qp': quote_perm p' "insert i V" F' 
      by (auto simp: qp.qp_insert i' p'_def F'_def  ‹atom i ♯ p›)
    { fix W t assume W: "W ⊆ V" "i∉W" "i'∉W"
      hence "finite W" by (metis ‹finite V› infinite_super)
      hence "ssubst t W F' = ssubst t W F" using W
        by induct (auto simp: qp.ssubst_insert_if qp'.ssubst_insert_if qp.F_unfold qp'.F_unfold)
    }
    hence ss_simp: "ssubst ⌊Ex i A⌋(insert i V) (insert i V) F' = ssubst ⌊Ex i A⌋V V F" using i
      by (metis equalityE insertCI p'_apply qp'.perm_exits_Vs qp'.ssubst_vquot_Ex qp.Vs) 
    have qa_p': "quote_all p' V = quote_all p V" using i i' ExI.hyps(1) 
      by (auto simp: p'_def quote_all_perm_eq)
    have ss: "(quote_all p' (insert i V))
              ⊢ PfP (ssubst ⌊A⌋(insert i V) (insert i V) F') IMP 
                PfP (ssubst ⌊Ex i A⌋(insert i V) (insert i V) F')" 
      apply (rule qp'.quote_all_MonPon_PfP_ssubst [OF SpecI])
      using ExI  apply auto
      done
    hence "insert A (quote_all p' (insert i V)) 
           ⊢ PfP (ssubst ⌊Ex i A⌋(insert i V) (insert i V) F')"
      apply (rule MP_thin)
      apply (rule ExI(3) [of "insert i V" p' F'])
      apply (metis ‹finite V› finite_insert)
      using ‹supp (Ex i A) ⊆ _› qp'.p qp'.pinv i'
      apply (auto simp: F'_def fresh_finite_insert)
      done
    hence "insert (QuoteP (Var i) (Var i')) (insert A (quote_all p V)) 
           ⊢ PfP (ssubst ⌊Ex i A⌋V V F)"
      by (auto simp: insert_commute ss_simp qa_p')
    hence Exi': "insert (Ex i' (QuoteP (Var i) (Var i'))) (insert A (quote_all p V)) 
                 ⊢ PfP (ssubst ⌊Ex i A⌋V V F)"
      by (auto intro!: qp.fresh_ssubst_fm) (auto simp: ExI i' fresh_quote_all_mem)
    have "insert A (quote_all p V) ⊢ PfP (ssubst ⌊Ex i A⌋V V F)" 
      using i'  by (auto intro: cut0 [OF exists_QuoteP Exi']) 
    thus "insert (Ex i A) (quote_all p V) ⊢ PfP (ssubst ⌊Ex i A⌋V V F)"
      apply (rule Ex_E, simp)
      apply (rule qp.fresh_ssubst_fm)  using i ExI
      apply (auto simp: fresh_quote_all_mem)
      done
   next
    case (All2I A j i p V F)
    interpret qp: quote_perm p V F 
      by unfold_locales (auto simp: image_iff All2I)
    obtain i'::name where i': "atom i' ♯ (i,p,A)"
      by (metis obtain_fresh)
    define p' where "p' = (atom i ⇌ atom i') + p" 
    define F' where "F' = make_F (insert i V) p'"
    interpret qp': quote_perm p' "insert i V" F' 
      using ‹atom i ♯ p› i'
      by (auto simp: qp.qp_insert p'_def F'_def)
    have p'_apply [simp]: "p' ∙ i = i'"
      using ‹atom i ♯ p› by (auto simp: p'_def fresh_at_base_permI)
    have qa_p': "quote_all p' V = quote_all p V" using i' All2I
      by (auto simp: p'_def quote_all_perm_eq)
    have "insert A (quote_all p' (insert i V)) 
          ⊢ PfP (ssubst ⌊A⌋(insert i V) (insert i V) F')"
      apply (rule All2I.hyps)
      using ‹supp (All2 i _ A) ⊆ _›   qp'.p qp'.pinv
      apply (auto simp: F'_def fresh_finite_insert)
      done
    hence "insert (QuoteP (Var i) (Var i')) (quote_all p V) 
           ⊢ A IMP PfP (ssubst ⌊A⌋(insert i V) (insert i V) (make_F (insert i V) p'))"
      by (auto simp: insert_commute qa_p' F'_def)
    thus "insert (All2 i (Var j) A) (quote_all p V) ⊢ PfP (ssubst ⌊All2 i (Var j) A⌋V V F)" 
      using All2I i' qp.quote_all_Mem_imp_All2 by (simp add: p'_def)
qed

theorem Provability: 
  assumes "Sigma_fm α" "ground_fm α" 
    shows "{α} ⊢ PfP «α»"
proof -
  obtain β where β: "ss_fm β" "ground_fm β" "{} ⊢ α IFF β" using assms
    by (auto simp: Sigma_fm_def ground_fm_aux_def)
  hence "{β} ⊢ PfP «β»" using star [of β 0 "{}"]
    by (auto simp: ground_fm_aux_def fresh_star_def)
  then have "{α} ⊢ PfP «β»" using β
    by (metis Iff_MP_left')
  moreover have "{} ⊢ PfP «β IMP α»" using β
    by (metis Conj_E2 Iff_def proved_imp_proved_PfP)
  ultimately show ?thesis
    by (metis PfP_implies_ModPon_PfP_quot thin0)
qed

end