Theory II_Prelims

chapter‹Syntactic Preliminaries for the Second Incompleteness Theorem›

theory II_Prelims
imports Pf_Predicates
begin

declare IndP.simps [simp del]

lemma VarP_Var [intro]: "H  VarP «Var i»"
proof -
  have "{}  VarP «Var i»"
    by (auto simp: Sigma_fm_imp_thm [OF VarP_sf] ground_fm_aux_def supp_conv_fresh)
  thus ?thesis
    by (rule thin0)
qed

lemma VarP_neq_IndP: "{t EQ v, VarP v, IndP t}  Fls"
proof -
  obtain m::name where "atom m  (t,v)"
    by (metis obtain_fresh) 
  thus ?thesis
    apply (auto simp: VarP_def IndP.simps [of m])
    apply (rule cut_same [of _ "OrdP (Q_Ind (Var m))"])
    apply (blast intro: Sym Trans OrdP_cong [THEN Iff_MP_same])
    by (metis OrdP_HPairE)
qed

lemma OrdP_ORD_OF [intro]: "H  OrdP (ORD_OF n)"
proof -
  have "{}  OrdP (ORD_OF n)"
    by (induct n) (auto simp: OrdP_SUCC_I)
  thus ?thesis
    by (rule thin0)
qed
 
lemma Mem_HFun_Sigma_OrdP: "{HPair t u IN f, HFun_Sigma f}  OrdP t"
proof -
  obtain x::name and y::name and z::name and x'::name and y'::name and z'::name
    where "atom z  (f,t,u,z',x,y,x',y')"  "atom z'  (f,t,u,x,y,x',y')"
       "atom x  (f,t,u,y,x',y')"  "atom y  (f,t,u,x',y')" 
       "atom x'  (f,t,u,y')"  "atom y'  (f,t,u)"
    by (metis obtain_fresh) 
  thus ?thesis 
  apply (simp add: HFun_Sigma.simps [of z f z' x y x' y'])
  apply (rule All2_E [where x="HPair t u", THEN rotate2], auto)
  apply (rule All2_E [where x="HPair t u"], auto intro: OrdP_cong [THEN Iff_MP2_same])
  done
qed

section ‹NotInDom›

nominal_function NotInDom :: "tm  tm  fm" 
  where "atom z  (t, r)  NotInDom t r = All z (Neg (HPair t (Var z) IN r))"
by (auto simp: eqvt_def NotInDom_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)

nominal_termination (eqvt)
  by lexicographic_order

lemma NotInDom_fresh_iff [simp]: "a  NotInDom t r  a  (t, r)"
proof -
  obtain j::name where "atom j  (t,r)"
    by (rule obtain_fresh)
  thus ?thesis
    by auto
qed

lemma subst_fm_NotInDom [simp]: "(NotInDom t r)(i::=x) = NotInDom (subst i x t) (subst i x r)"
proof -
  obtain j::name where "atom j  (i,x,t,r)"
    by (rule obtain_fresh)
  thus ?thesis
    by (auto simp: NotInDom.simps [of j])
qed

lemma NotInDom_cong: "H  t EQ t'  H  r EQ r'  H  NotInDom t r IFF NotInDom t' r'"
  by (rule P2_cong) auto

lemma NotInDom_Zero: "H  NotInDom t Zero"
proof -
  obtain z::name where "atom z  t"
    by (metis obtain_fresh) 
  hence "{}  NotInDom t Zero"
    by (auto simp: fresh_Pair)
  thus ?thesis
    by (rule thin0)
qed

lemma NotInDom_Fls: "{HPair d d' IN r, NotInDom d r}  A"
proof -
  obtain z::name where "atom z  (d,r)"
    by (metis obtain_fresh) 
  hence "{HPair d d' IN r, NotInDom d r}  Fls"
    by (auto intro!: Ex_I [where x=d'])
  thus ?thesis 
    by (metis ExFalso)
qed

lemma NotInDom_Contra: "H  NotInDom d r  H  HPair x y IN r  insert (x EQ d) H  A"
by (rule NotInDom_Fls [THEN cut2, THEN ExFalso])
   (auto intro: thin1 NotInDom_cong [OF Assume Refl, THEN Iff_MP2_same])


section ‹Restriction of a Sequence to a Domain›

nominal_function RestrictedP :: "tm  tm  tm  fm"
  where "atom x  (y,f,k,g); atom y  (f,k,g) 
    RestrictedP f k g =
      g SUBS f AND
      All x (All y (HPair (Var x) (Var y) IN g IFF 
                    (Var x) IN k AND HPair (Var x) (Var y) IN f))"
by (auto simp: eqvt_def RestrictedP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)

nominal_termination (eqvt)
  by lexicographic_order

lemma RestrictedP_fresh_iff [simp]: "a  RestrictedP f k g  a  f  a  k  a  g"       
proof -
  obtain x::name and y::name where "atom x  (y,f,k,g)" "atom y  (f,k,g)"
    by (metis obtain_fresh)
  thus ?thesis
    by auto
qed

lemma subst_fm_RestrictedP [simp]:
  "(RestrictedP f k g)(i::=u) = RestrictedP (subst i u f) (subst i u k) (subst i u g)"
proof -
  obtain x::name and y::name  where "atom x  (y,f,k,g,i,u)" "atom y  (f,k,g,i,u)"
    by (metis obtain_fresh)
  thus ?thesis
    by (auto simp: RestrictedP.simps [of x y])
qed

lemma RestrictedP_cong: 
  "H  f EQ f'; H  k EQ A'; H  g EQ g' 
    H  RestrictedP f k g IFF RestrictedP f' A' g'"
  by (rule P3_cong) auto

lemma RestrictedP_Zero: "H  RestrictedP Zero k Zero"
proof -
  obtain x::name and y::name  where "atom x  (y,k)" "atom y  (k)"
    by (metis obtain_fresh)
  hence "{}  RestrictedP Zero k Zero"
    by (auto simp: RestrictedP.simps [of x y])
  thus ?thesis
    by (rule thin0)
qed

lemma RestrictedP_Mem: "{ RestrictedP s k s', HPair a b IN s, a IN k }  HPair a b IN s'"
proof -
  obtain x::name and y::name where "atom x  (y,s,k,s',a,b)" "atom y  (s,k,s',a,b)"
    by (metis obtain_fresh)
  thus ?thesis
    apply (auto simp: RestrictedP.simps [of x y])
    apply (rule All_E [where x=a, THEN rotate2], auto)
    apply (rule All_E [where x=b], auto intro: Iff_E2)
    done
qed

lemma RestrictedP_imp_Subset: "{RestrictedP s k s'}  s' SUBS s"
proof -
  obtain x::name and y::name where "atom x  (y,s,k,s')" "atom y  (s,k,s')"
    by (metis obtain_fresh)
  thus ?thesis
    by (auto simp: RestrictedP.simps [of x y])
qed

lemma RestrictedP_Mem2: 
  "{ RestrictedP s k s', HPair a b IN s' }  HPair a b IN s AND a IN k"
proof -
  obtain x::name and y::name where "atom x  (y,s,k,s',a,b)" "atom y  (s,k,s',a,b)"
    by (metis obtain_fresh)
  thus ?thesis
    apply (auto simp: RestrictedP.simps [of x y] intro: Subset_D)
    apply (rule All_E [where x=a, THEN rotate2], auto)
    apply (rule All_E [where x=b], auto intro: Iff_E1)
    done
qed

lemma RestrictedP_Mem_D: "H  RestrictedP s k t  H  a IN t  insert (a IN s) H  A  H  A"
  by (metis RestrictedP_imp_Subset Subset_E cut1)

lemma RestrictedP_Eats:
  "{ RestrictedP s k s', a IN k }  RestrictedP (Eats s (HPair a b)) k (Eats s' (HPair a b))" (*<*)
proof -
  obtain x::name and y::name 
  where "atom x  (y,s,k,s',a,b)" "atom y  (s,k,s',a,b)"
    by (metis obtain_fresh)
  thus ?thesis
    apply (auto simp: RestrictedP.simps [of x y])
      apply (metis Assume Subset_Eats_I Subset_trans)
     apply (metis Mem_Eats_I2 Refl)
    apply (rule Swap, auto)
         apply (rule All_E [where x="Var x", THEN rotate2], auto)
         apply (rule All_E [where x="Var y"], simp)
         apply (metis Assume Conj_E Iff_E1)
        apply (blast intro: Subset_D)
       apply (blast intro: Mem_cong [THEN Iff_MP2_same])
      apply (metis Assume AssumeH(2) HPair_cong Mem_Eats_I2)
     apply (rule All_E [where x="Var x", THEN rotate3], auto)
     apply (rule All_E [where x="Var y"], simp)
     apply (metis Assume AssumeH(2) Conj_I Iff_E2 Mem_Eats_I1)
    apply (blast intro: Mem_Eats_I2 HPair_cong)
   done
qed (*>*)

lemma exists_RestrictedP: 
  assumes s: "atom s  (f,k)"
  shows  "H  Ex s (RestrictedP f k (Var s))" (*<*)
proof -
  obtain j::name and x::name and y::name and z::name
    where atoms: "atom j  (k,z,s)"  "atom x  (j,k,z,s)"  "atom y  (x,j,k,z,s)"  "atom z  (s,k)"
    by (metis obtain_fresh) 
  have "{}  Ex s (RestrictedP (Var z) k (Var s))"
    apply (rule Ind [of j z]) using atoms s
    apply simp_all
    apply (rule Ex_I [where x=Zero], simp add: RestrictedP_Zero)
    apply (rule All_I)+
    apply (auto del: Ex_EH)
    apply (rule thin1)
    apply (rule Ex_E)
    proof (rule Cases [where A="Ex x (Ex y ((Var x) IN k AND Var j EQ HPair (Var x) (Var y)))"], auto)
      show "{Var x IN k, Var j EQ HPair (Var x) (Var y), RestrictedP (Var z) k (Var s)} 
             Ex s (RestrictedP (Eats (Var z) (Var j)) k (Var s))"
        apply (rule Ex_I [where x="Eats (Var s) (HPair (Var x) (Var y))"])
        using atoms s apply auto
        apply (rule RestrictedP_cong [OF _ Refl Refl, THEN Iff_MP2_same])
        apply (blast intro: Eats_cong [OF Refl])
        apply (rule Var_Eq_subst_Iff [THEN rotate2, THEN Iff_MP_same])
        apply (auto intro: RestrictedP_Eats [THEN cut2])
        done
    next
      obtain u::name and v::name 
      where uv: "atom u  (x,y,z,s,j,k)" "atom v  (u,x,y,z,s,j,k)"
        by (metis obtain_fresh)
      show "{Neg (Ex x (Ex y (Var x IN k AND Var j EQ HPair (Var x) (Var y)))),
             RestrictedP (Var z) k (Var s)} 
             Ex s (RestrictedP (Eats (Var z) (Var j)) k (Var s))"
        apply (rule Ex_I [where x="Var s"]) 
        using uv atoms
        apply (auto simp: RestrictedP.simps [of u v])
         apply (metis Assume Subset_Eats_I Subset_trans)
        apply (rule Swap, auto)
           apply (rule All_E [THEN rotate4, of _ _ "Var u"], auto)
           apply (rule All_E [where x="Var v"], simp)
           apply (metis Assume Conj_E Iff_E1)
          apply (rule Mem_Eats_I1)
          apply (metis Assume AssumeH(3) Subset_D)
         apply (rule All_E [where x="Var u", THEN rotate5], auto)
         apply (rule All_E [where x="Var v"], simp)
         apply (metis Assume AssumeH(2) Conj_I Iff_E2)
        apply (rule ContraProve [THEN rotate3])
       apply (rule Ex_I [where x="Var u"], simp)
       apply (rule Ex_I [where x="Var v"], auto intro: Sym)
       done
    qed
  hence "{}  (Ex s (RestrictedP (Var z) k (Var s)))(z::=f)"
    by (rule Subst) simp
  thus ?thesis using atoms s
    by simp (rule thin0)
qed (*>*)    

lemma cut_RestrictedP: 
  assumes s: "atom s  (f,k,A)" and "C  H. atom s  C"
  shows  "insert (RestrictedP f k (Var s)) H  A  H  A"
  apply (rule cut_same [OF exists_RestrictedP [of s]])
  using assms apply auto
  done

lemma RestrictedP_NotInDom: "{ RestrictedP s k s', Neg (j IN k) }  NotInDom j s'"
proof -
  obtain x::name and y::name and z::name 
  where "atom x  (y,s,j,k,s')" "atom y  (s,j,k,s')" "atom z  (s,j,k,s')"
    by (metis obtain_fresh)
  thus ?thesis
    apply (auto simp: RestrictedP.simps [of x y] NotInDom.simps [of z])
    apply (rule All_E [where x=j, THEN rotate3], auto)
    apply (rule All_E, auto intro: Conj_E1 Iff_E1)
    done
qed

declare RestrictedP.simps [simp del]

section ‹Applications to LstSeqP›

lemma HFun_Sigma_Eats: 
  assumes "H  HFun_Sigma r" "H  NotInDom d r" "H  OrdP d"
    shows "H  HFun_Sigma (Eats r (HPair d d'))" (*<*)
proof -
  obtain x::name and y::name and z::name and x'::name and y'::name and z'::name and z''::name
    where "atom z''  (r,d,d',z,z',x,y,x',y')" 
      and "atom z  (r,d,d',z',x,y,x',y')" and "atom z'  (r,d,d',x,y,x',y')"
      and "atom x  (r,d,d',y,x',y')" and "atom y  (r,d,d',x',y')" 
      and "atom x'  (r,d,d',y')" and "atom y'  (r,d,d')"
    by (metis obtain_fresh) 
  hence "{ HFun_Sigma r, NotInDom d r, OrdP d }  HFun_Sigma (Eats r (HPair d d'))"
    apply (auto simp: HFun_Sigma.simps [of z _ z' x y x' y'])
      ― ‹case 1›
       apply (rule Ex_I [where x = "Var z"], simp)
       apply (rule Neg_Imp_I, blast)
      apply (rule All_E [where x = "Var z'"], auto)
      ― ‹case 2›
      apply (rule Ex_I [where x = "Var z"], simp)
      apply (rule Neg_Imp_I, blast)
      apply (rule All_E [where x = "Var z"], simp)
      apply (rule Imp_E, auto del: Disj_EH)
      apply (rule thin1)
      apply (rule thin1)
      apply (rule Ex_I [where x = "Var x"], simp)
      apply (rule Ex_I [where x = "Var y"], simp)
      apply (rule Ex_I [where x = d], simp)
      apply (rule Ex_I [where x = d'], auto)
      apply (blast intro: Disj_I1 OrdNotEqP_I NotInDom_Contra Mem_cong [THEN Iff_MP_same])
    ― ‹case 3›
    apply (rule Ex_I [where x = "Var z'"])
    apply (subst subst_fm_Ex_with_renaming [where i'=z''] | subst subst_fm.simps)+
    apply (auto simp add: flip_fresh_fresh)
    apply (rule Ex_I [where x = "Var z'", THEN Swap], simp)
    apply (rule Neg_I)
    apply (rule Imp_E, auto del: Disj_EH)
    apply (rule thin1)
    apply (rule thin1)
    apply (rule Ex_I [where x = d], simp)
    apply (rule Ex_I [where x = d'], simp)
    apply (rule Ex_I [where x = "Var x"], simp)
    apply (rule Ex_I [where x = "Var y"], auto)
    apply (blast intro: Disj_I1 Sym_L OrdNotEqP_I NotInDom_Contra Mem_cong [THEN Iff_MP_same])
    ― ‹case 4›
    apply (rule rotate2 [OF Swap])
    apply (rule Ex_I [where x = d], auto)
    apply (rule Ex_I [where x = d'], auto)
    apply (rule Ex_I [where x = d], auto)
    apply (rule Ex_I [where x = d'], auto intro: Disj_I2)
    done
  thus ?thesis using assms
    by (rule cut3)
qed (*>*)

lemma HFun_Sigma_single [iff]: "H  OrdP d  H  HFun_Sigma (Eats Zero (HPair d d'))"
  by (metis HFun_Sigma_Eats HFun_Sigma_Zero NotInDom_Zero)

lemma LstSeqP_single [iff]: "H  LstSeqP (Eats Zero (HPair Zero x)) Zero x"
  by (auto simp: LstSeqP.simps intro!: OrdP_SUCC_I HDomain_Incl_Eats_I Mem_Eats_I2)

lemma NotInDom_LstSeqP_Eats: 
  "{ NotInDom (SUCC k) s, LstSeqP s k y }  LstSeqP (Eats s (HPair (SUCC k) z)) (SUCC k) z"
by (auto simp: LstSeqP.simps intro: HDomain_Incl_Eats_I Mem_Eats_I2 OrdP_SUCC_I HFun_Sigma_Eats)

lemma RestrictedP_HDomain_Incl: "{HDomain_Incl s k, RestrictedP s k s'}  HDomain_Incl s' k"
proof -
  obtain u::name and v::name and x::name and y::name and z::name 
    where "atom u  (v,s,k,s')" "atom v  (s,k,s')" 
          "atom x  (s,k,s',u,v,y,z)" "atom y  (s,k,s',u,v,z)" "atom z  (s,k,s',u,v)"
    by (metis obtain_fresh) 
  thus ?thesis
    apply (auto simp: HDomain_Incl.simps [of x _ _ y z])
    apply (rule Ex_I [where x="Var x"], auto)
    apply (rule Ex_I [where x="Var y"], auto)
    apply (rule Ex_I [where x="Var z"], simp)
    apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same, THEN rotate2])
    apply (auto simp: RestrictedP.simps [of u v])
    apply (rule All_E [where x="Var x", THEN rotate2], auto)
    apply (rule All_E [where x="Var y"])
    apply (auto intro: Iff_E ContraProve Mem_cong [THEN Iff_MP_same])
    done
qed

lemma RestrictedP_HFun_Sigma: "{HFun_Sigma s, RestrictedP s k s'}  HFun_Sigma s'"
  by (metis Assume RestrictedP_imp_Subset Subset_HFun_Sigma rcut2)

lemma RestrictedP_LstSeqP: 
  "{ RestrictedP s (SUCC k) s', LstSeqP s k y }  LstSeqP s' k y"
  by (auto simp: LstSeqP.simps 
           intro: Mem_Neg_refl cut2 [OF RestrictedP_HDomain_Incl]  
                               cut2 [OF RestrictedP_HFun_Sigma] cut3 [OF RestrictedP_Mem])

lemma RestrictedP_LstSeqP_Eats: 
  "{ RestrictedP s (SUCC k) s', LstSeqP s k y }
    LstSeqP (Eats s' (HPair (SUCC k) z)) (SUCC k) z"
by (blast intro: Mem_Neg_refl cut2 [OF NotInDom_LstSeqP_Eats] 
                              cut2 [OF RestrictedP_NotInDom] cut2 [OF RestrictedP_LstSeqP])


section‹Ordinal Addition›

subsection‹Predicate form, defined on sequences›

nominal_function SeqHaddP :: "tm  tm  tm  tm  fm"
  where "atom l  (sl,s,k,j); atom sl  (s,j) 
    SeqHaddP s j k y = LstSeqP s k y AND
          HPair Zero j IN s AND
          All2 l k (Ex sl (HPair (Var l) (Var sl) IN s AND
                           HPair (SUCC (Var l)) (SUCC (Var sl)) IN s))"
by (auto simp: eqvt_def SeqHaddP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)

nominal_termination (eqvt)
  by lexicographic_order

lemma SeqHaddP_fresh_iff [simp]: "a  SeqHaddP s j k y  a  s  a  j  a  k  a  y"
proof -
  obtain l::name and sl::name where "atom l  (sl,s,k,j)" "atom sl  (s,j)"
    by (metis obtain_fresh)
  thus ?thesis
    by force
qed

lemma SeqHaddP_subst [simp]:
  "(SeqHaddP s j k y)(i::=t) = SeqHaddP (subst i t s) (subst i t j) (subst i t k) (subst i t y)"
proof -
  obtain l::name and sl::name where "atom l  (s,k,j,sl,t,i)" "atom sl  (s,k,j,t,i)"
    by (metis obtain_fresh)
  thus ?thesis
    by (auto simp: SeqHaddP.simps [where l=l and sl=sl])
qed

declare SeqHaddP.simps [simp del]

nominal_function HaddP :: "tm  tm  tm  fm"
  where "atom s  (x,y,z) 
    HaddP x y z = Ex s (SeqHaddP (Var s) x y z)"
by (auto simp: eqvt_def HaddP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)

nominal_termination (eqvt)
  by lexicographic_order

lemma HaddP_fresh_iff [simp]: "a  HaddP x y z  a  x  a  y  a  z" 
proof -
  obtain s::name where "atom s  (x,y,z)"
    by (metis obtain_fresh)
  thus ?thesis
    by force
qed

lemma HaddP_subst [simp]: "(HaddP x y z)(i::=t) = HaddP (subst i t x) (subst i t y) (subst i t z)"
proof -
  obtain s::name where "atom s  (x,y,z,t,i)"
    by (metis obtain_fresh)
  thus ?thesis
    by (auto simp: HaddP.simps [of s])
qed

lemma HaddP_cong: "H  t EQ t'; H  u EQ u'; H  v EQ v'  H  HaddP t u v IFF HaddP t' u' v'"
  by (rule P3_cong) auto

declare HaddP.simps [simp del]

lemma HaddP_Zero2: "H  HaddP x Zero x"
proof -
  obtain s::name and l::name and sl::name where "atom l  (sl,s,x)" "atom sl  (s,x)" "atom s  x"
    by (metis obtain_fresh)
  hence "{}  HaddP x Zero x"
    by (auto simp: HaddP.simps [of s] SeqHaddP.simps [of l sl]
          intro!: Mem_Eats_I2 Ex_I [where x="Eats Zero (HPair Zero x)"])
  thus ?thesis
    by (rule thin0)
qed

lemma HaddP_imp_OrdP: "{HaddP x y z}  OrdP y" 
proof -
  obtain s::name and l::name and sl::name
    where "atom l  (sl,s,x,y,z)" "atom sl  (s,x,y,z)" "atom s  (x,y,z)"
    by (metis obtain_fresh)
  thus ?thesis
    by (auto simp: HaddP.simps [of s] SeqHaddP.simps [of l sl] LstSeqP.simps)
qed

lemma HaddP_SUCC2: "{HaddP x y z}  HaddP x (SUCC y) (SUCC z)" (*<*)
proof -
  obtain s::name and s'::name and l::name and sl::name
    where "atom s'  (l,sl,s,x,y,z)" "atom l  (sl,s,x,y,z)" "atom sl  (s,x,y,z)" "atom s  (x,y,z)"
    by (metis obtain_fresh)
  hence "{HaddP x y z, OrdP y}  HaddP x (SUCC y) (SUCC z)"
    apply (auto simp: HaddP.simps [of s] SeqHaddP.simps [of l sl])
    apply (rule cut_RestrictedP [of s' "Var s" "SUCC y"], auto)
    apply (rule Ex_I [where x="Eats (Var s') (HPair (SUCC y) (SUCC z))"])
       apply (auto intro!: Mem_SUCC_EH)
       apply (metis rotate2 RestrictedP_LstSeqP_Eats rotate3 thin1)
      apply (blast intro: Mem_Eats_I1 cut3 [OF RestrictedP_Mem] cut1 [OF Zero_In_SUCC])
     apply (rule Ex_I [where x="Var l"], auto)
     apply (rule Ex_I [where x="Var sl"], auto)
     apply (blast intro: Mem_Eats_I1 cut3 [OF RestrictedP_Mem] Mem_SUCC_I1)
    apply (blast intro: Mem_Eats_I1 cut3 [OF RestrictedP_Mem] OrdP_IN_SUCC)
   apply (rule ContraProve [THEN rotate2])
   apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same], simp add: LstSeqP.simps)
   apply (rule Ex_I [where x=z])
   apply (force intro: Mem_Eats_I1 Mem_Eats_I2 cut3 [OF RestrictedP_Mem] Mem_SUCC_I2)
   done
 thus ?thesis
   by (metis Assume HaddP_imp_OrdP cut2)
qed (*>*)

subsection‹Proving that these relations are functions›

lemma SeqHaddP_Zero_E: "{SeqHaddP s w Zero z}  w EQ z"
proof -
  obtain l::name and sl::name where "atom l  (s,w,z,sl)" "atom sl  (s,w)"
    by (metis obtain_fresh)
  thus ?thesis
    by (auto simp: SeqHaddP.simps [of l sl] LstSeqP.simps intro: HFun_Sigma_E)
qed

lemma SeqHaddP_SUCC_lemma:
  assumes y': "atom y'  (s,j,k,y)"
  shows "{SeqHaddP s j (SUCC k) y}  Ex y' (SeqHaddP s j k (Var y') AND y EQ SUCC (Var y'))"
proof -
  obtain l::name and sl::name  where "atom l  (s,j,k,y,y',sl)" "atom sl  (s,j,k,y,y')"
    by (metis obtain_fresh)
  thus ?thesis using y'
    apply (auto simp: SeqHaddP.simps [where s=s and l=l and sl=sl])
    apply (rule All2_SUCC_E' [where t=k, THEN rotate2], auto)
    apply (auto intro!: Ex_I [where x="Var sl"])
    apply (blast intro: LstSeqP_SUCC) ― ‹showing @{term"SeqHaddP s j k (Var sl)"}
    apply (blast intro: LstSeqP_EQ)
    done
qed

lemma SeqHaddP_SUCC:
  assumes "H  SeqHaddP s j (SUCC k) y"  "atom y'  (s,j,k,y)"
  shows "H  Ex y' (SeqHaddP s j k (Var y') AND y EQ SUCC (Var y'))"
  by (metis SeqHaddP_SUCC_lemma [THEN cut1] assms)

lemma SeqHaddP_unique: "{OrdP x, SeqHaddP s w x y, SeqHaddP s' w x y'}  y' EQ y" (*<*)
proof -
  obtain i::name and j::name and j'::name and k::name and sl::name and sl'::name 
     and l::name and ji::name and ji'::name
   where ij: "atom i  (s,s',w,y,y')" "atom j  (s,s',w,i,x,y,y')" "atom j'  (s,s',w,i,j,x,y,y')"
     and atoms: "atom k  (s,s',w,i,j,j')" "atom sl  (s,s',w,i,j,j',k)" "atom sl'  (s,s',w,i,j,j',k,sl)"
                "atom ji  (s,s',w,i,j,j',k,sl,sl')"  "atom ji'  (s,s',w,i,j,j',k,sl,sl',ji)"
    by (metis obtain_fresh)
  have "{OrdP (Var i)} 
         All j (All j' (SeqHaddP s w (Var i) (Var j) IMP (SeqHaddP s' w (Var i) (Var j') IMP Var j' EQ Var j)))"
    apply (rule OrdInd2H)
    using ij atoms apply auto 
    apply (metis SeqHaddP_Zero_E [THEN cut1] Assume AssumeH(2) Sym Trans)
    ― ‹SUCC case›
    apply (rule cut_same [OF SeqHaddP_SUCC [where y' = ji and s=s]], auto)
    apply (rule cut_same [OF SeqHaddP_SUCC [where y' = ji' and s=s']], auto)
    apply (rule Ex_I [where x = "Var ji"], auto)
    apply (rule All_E [where x = "Var ji'"], auto)
    apply (blast intro: Trans [OF Hyp] Sym intro!: SUCC_cong)
    done
  hence "{OrdP (Var i)} 
          (All j' (SeqHaddP s w (Var i) (Var j) IMP (SeqHaddP s' w (Var i) (Var j') IMP Var j' EQ Var j)))(j::=y)"
    by (metis All_D)
  hence "{OrdP (Var i)} 
          All j' (SeqHaddP s w (Var i) y IMP (SeqHaddP s' w (Var i) (Var j') IMP Var j' EQ y))"
    using ij by simp
  hence "{OrdP (Var i)} 
          (SeqHaddP s w (Var i) y IMP (SeqHaddP s' w (Var i) (Var j') IMP Var j' EQ y))(j'::=y')"
    by (metis All_D)
  hence "{OrdP (Var i)}  SeqHaddP s w (Var i) y IMP (SeqHaddP s' w (Var i) y' IMP y' EQ y)"
    using ij by simp
  hence "{}  (OrdP (Var i) IMP SeqHaddP s w (Var i) y IMP (SeqHaddP s' w (Var i) y' IMP y' EQ y))(i::=x)"
    by (metis Imp_I Subst emptyE)
  thus ?thesis
    using ij by simp (metis DisjAssoc2 Disj_commute anti_deduction)
qed (*>*)

lemma HaddP_unique: "{HaddP w x y, HaddP w x y'}  y' EQ y"
proof -
  obtain s::name and s'::name  where "atom s  (w,x,y,y')" "atom s'  (w,x,y,y',s)"
    by (metis obtain_fresh)
  hence "{OrdP x, HaddP w x y, HaddP w x y'}  y' EQ y"
    by (auto simp: HaddP.simps [of s _ _ y]  HaddP.simps [of s' _ _ y'] 
             intro: SeqHaddP_unique [THEN cut3])
  thus ?thesis 
    by (metis HaddP_imp_OrdP cut_same thin1)
qed

lemma HaddP_Zero1: assumes "H  OrdP x" shows "H  HaddP Zero x x"
proof -
  fix k::name 
  have "{ OrdP (Var k) }  HaddP Zero (Var k) (Var k)"
    by (rule OrdInd2H [where i=k]) (auto intro: HaddP_Zero2 HaddP_SUCC2 [THEN cut1])
  hence "{}  OrdP (Var k) IMP HaddP Zero (Var k) (Var k)"
    by (metis Imp_I)
  hence "{}  (OrdP (Var k) IMP HaddP Zero (Var k) (Var k))(k::=x)"
    by (rule Subst) auto
  hence "{}  OrdP x IMP HaddP Zero x x"
    by simp
  thus ?thesis using assms
    by (metis MP_same thin0)
qed

lemma HaddP_Zero_D1: "insert (HaddP Zero x y) H  x EQ y"
  by (metis Assume HaddP_imp_OrdP HaddP_Zero1 HaddP_unique [THEN cut2] rcut1)

lemma HaddP_Zero_D2: "insert (HaddP x Zero y) H  x EQ y"
  by (metis Assume HaddP_Zero2 HaddP_unique [THEN cut2])

lemma HaddP_SUCC_Ex2:
  assumes "H  HaddP x (SUCC y) z" "atom z'  (x,y,z)"
    shows "H  Ex z' (HaddP x y (Var z') AND z EQ SUCC (Var z'))"
proof -
  obtain s::name and s'::name  where "atom s  (x,y,z,z')" "atom s'  (x,y,z,z',s)"
    by (metis obtain_fresh)
  hence "{ HaddP x (SUCC y) z }  Ex z' (HaddP x y (Var z') AND z EQ SUCC (Var z'))"
    using assms
    apply (auto simp: HaddP.simps [of s _ _ ]  HaddP.simps [of s' _ _ ])
    apply (rule cut_same [OF SeqHaddP_SUCC_lemma [of z']], auto)
    apply (rule Ex_I, auto)+
    done
  thus ?thesis
    by (metis assms(1) cut1)
qed

lemma HaddP_SUCC1: "{ HaddP x y z }  HaddP (SUCC x) y (SUCC z)" (*<*)
proof -
  obtain i::name and j::name and z'::name
   where atoms: "atom i  (x,y,z)"  "atom j  (i,x,y,z)"  "atom z'  (x,i,j)"
    by (metis obtain_fresh)
  have "{OrdP (Var i)}  All j (HaddP x (Var i) (Var j) IMP HaddP (SUCC x) (Var i) (SUCC (Var j)))"
       (is "_  ?scheme")
    proof (rule OrdInd2H)
      show "{}  ?scheme(i::=Zero)"
        using atoms apply auto
        apply (rule cut_same [OF HaddP_Zero_D2])
        apply (rule Var_Eq_subst_Iff [THEN Sym_L, THEN Iff_MP_same], auto intro: HaddP_Zero2)
        done
    next
      show "{}  All i (OrdP (Var i) IMP ?scheme IMP ?scheme(i::=SUCC (Var i)))"
        using atoms
        apply auto
        apply (rule cut_same [OF HaddP_SUCC_Ex2 [where z'=z']], auto)
        apply (rule Ex_I [where x="Var z'"], auto)
        apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same, THEN rotate3], simp)
        by (metis Assume HaddP_SUCC2 cut1 thin1)
    qed
  hence "{OrdP (Var i)}  (HaddP x (Var i) (Var j) IMP HaddP (SUCC x) (Var i) (SUCC (Var j)))(j::=z)"
    by (rule All_D)
  hence "{OrdP (Var i)}  HaddP x (Var i) z IMP HaddP (SUCC x) (Var i) (SUCC z)"
    using atoms by auto
  hence "{}  HaddP x (Var i) z IMP HaddP (SUCC x) (Var i) (SUCC z)"
    by (metis HaddP_imp_OrdP Imp_cut)
  hence "{}  (HaddP x (Var i) z IMP HaddP (SUCC x) (Var i) (SUCC z))(i::=y)"
    using atoms by (force intro!: Subst)
  thus ?thesis
    using atoms by simp (metis anti_deduction)
qed (*>*)

lemma HaddP_commute: "{HaddP x y z, OrdP x}  HaddP y x z" (*<*)
proof -
  obtain i::name and j::name and z'::name
   where atoms: "atom i  (x,y,z)"  "atom j  (i,x,y,z)"  "atom z'  (x,i,j)"
    by (metis obtain_fresh)
  have "{OrdP (Var i), OrdP x}  All j (HaddP x (Var i) (Var j) IMP HaddP (Var i) x (Var j))"
       (is "_  ?scheme")
    proof (rule OrdInd2H)
      show "{OrdP x}  ?scheme(i::=Zero)"
        using atoms apply auto
        apply (rule cut_same [OF HaddP_Zero_D2])
        apply (rule Var_Eq_subst_Iff [THEN Sym_L, THEN Iff_MP_same], auto intro: HaddP_Zero1)
        done
    next
      show "{OrdP x}  All i (OrdP (Var i) IMP ?scheme IMP ?scheme(i::=SUCC (Var i)))"
        using atoms
        apply auto
        apply (rule cut_same [OF HaddP_SUCC_Ex2 [where z'=z']], auto)
        apply (rule Ex_I [where x="Var z'"], auto)
        apply (rule rotate3)
        apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same], simp)
        by (metis Assume HaddP_SUCC1 cut1 thin1)
    qed
  hence "{OrdP (Var i), OrdP x}  (HaddP x (Var i) (Var j) IMP HaddP (Var i) x (Var j))(j::=z)"
    by (rule All_D)
  hence "{OrdP (Var i), OrdP x}  HaddP x (Var i) z IMP HaddP (Var i) x z"
    using atoms by auto
  hence "{OrdP x}  HaddP x (Var i) z IMP HaddP (Var i) x z"
    by (metis HaddP_imp_OrdP Imp_cut)
  hence "{OrdP x}  (HaddP x (Var i) z IMP HaddP (Var i) x z)(i::=y)"
    using atoms by (force intro!: Subst)
  thus ?thesis
    using atoms by simp (metis anti_deduction)
qed (*>*)

lemma HaddP_SUCC_Ex1:
  assumes "atom i  (x,y,z)"
    shows "insert (HaddP (SUCC x) y z) (insert (OrdP x) H)
            Ex i (HaddP x y (Var i) AND z EQ SUCC (Var i))"
proof -
  have "{ HaddP (SUCC x) y z, OrdP x }  Ex i (HaddP x y (Var i) AND z EQ SUCC (Var i))"
    apply (rule cut_same [OF HaddP_commute [THEN cut2]])
    apply (blast intro: OrdP_SUCC_I)+
    apply (rule cut_same [OF HaddP_SUCC_Ex2 [where z'=i]], blast)
    using assms apply auto
    apply (auto intro!: Ex_I [where x="Var i"])
    by (metis AssumeH(2) HaddP_commute [THEN cut2] HaddP_imp_OrdP rotate2 thin1)
  thus ?thesis
    by (metis Assume AssumeH(2) cut2)
qed

lemma HaddP_inv2: "{HaddP x y z, HaddP x y' z, OrdP x}  y' EQ y" (*<*)
proof -
  obtain i::name and j::name and u::name and u'::name
   where atoms: "atom i  (x,y,y',z)"  "atom j  (i,x,y,y',z)"  
                "atom u  (x,y,y',i,j)" "atom u'  (x,y,y',u,i,j)"
    by (metis obtain_fresh)
  have "{OrdP (Var i)}  All j (HaddP (Var i) y (Var j) IMP HaddP (Var i) y' (Var j) IMP y' EQ y)"
       (is "_  ?scheme")
    proof (rule OrdInd2H)
      show "{}  ?scheme(i::=Zero)"
        using atoms 
        by auto (metis HaddP_Zero_D1 Sym Trans thin1)
    next
      show "{}  All i (OrdP (Var i) IMP ?scheme IMP ?scheme(i::=SUCC (Var i)))"
        using atoms
        apply auto
        apply (rule cut_same [OF HaddP_SUCC_Ex1 [where y=y and i=u, THEN cut2]], auto)
        apply (rule Ex_I [where x="Var u"], auto)
        apply (rule cut_same [OF HaddP_SUCC_Ex1 [where y=y' and i=u', THEN cut2]], auto)
        apply (rule cut_same [where A="SUCC (Var u) EQ SUCC (Var u')"])
        apply (auto intro: Sym Trans)
        apply (rule rotate4 [OF ContraProve])
        apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same], force)
        done
    qed
  hence "{OrdP (Var i)}  (HaddP (Var i) y (Var j) IMP HaddP (Var i) y' (Var j) IMP y' EQ y)(j::=z)"
    by (rule All_D)
  hence "{OrdP (Var i)}  HaddP (Var i) y z IMP HaddP (Var i) y' z IMP y' EQ y"
    using atoms by auto
  hence "{}  OrdP (Var i) IMP HaddP (Var i) y z IMP HaddP (Var i) y' z IMP y' EQ y"
    by (metis Imp_I)
  hence "{}  (OrdP (Var i) IMP HaddP (Var i) y z IMP HaddP (Var i) y' z IMP y' EQ y)(i::=x)"
    using atoms by (force intro!: Subst)
  thus ?thesis
    using atoms by simp (metis DisjAssoc2 Disj_commute anti_deduction)
qed (*>*)

lemma Mem_imp_subtract: (*<*)
  assumes "H  x IN y" "H  OrdP y" and k: "atom (k::name)  (x,y)"
    shows  "H  Ex k (HaddP x (Var k) y AND Zero IN (Var k))"
proof -
  obtain i::name 
   where atoms: "atom i  (x,y,k)" 
    by (metis obtain_fresh)
  have "{OrdP (Var i)}  x IN Var i IMP Ex k (HaddP x (Var k) (Var i) AND Zero IN (Var k))"
       (is "_  ?scheme")
    proof (rule OrdInd2H)
      show "{}  ?scheme(i::=Zero)"
        by auto
    next
      show "{}  All i (OrdP (Var i) IMP ?scheme IMP ?scheme(i::=SUCC (Var i)))"
        using atoms k
        apply (auto intro!: Mem_SUCC_EH)
        apply (rule Ex_I [where x="SUCC (Var k)"], auto)
        apply (metis AssumeH(4) HaddP_SUCC2 cut1 insert_commute)
        apply (blast intro: Mem_SUCC_I1)
        apply (rule Ex_I [where x="SUCC Zero"], auto)
        apply (rule thin1)
        apply (rule Var_Eq_subst_Iff [THEN Sym_L, THEN Iff_MP_same], simp)
        apply (metis HaddP_SUCC2 HaddP_Zero2 cut1) 
        apply (rule Ex_I [where x="SUCC (Var k)"], auto intro: Mem_SUCC_I1)
        apply (metis AssumeH(4) HaddP_SUCC2 cut1 insert_commute)
        done
    qed
  hence "{}  OrdP (Var i) IMP x IN Var i IMP Ex k (HaddP x (Var k) (Var i) AND Zero IN (Var k))"
    by (metis Imp_I)
  hence "{}  (OrdP (Var i) IMP x IN Var i IMP Ex k (HaddP x (Var k) (Var i) AND Zero IN (Var k)))(i::=y)"
    by (force intro!: Subst)
  thus ?thesis using assms atoms
    by simp (metis (no_types) anti_deduction cut2)
qed (*>*)

lemma HaddP_OrdP:
  assumes "H  HaddP x y z" "H  OrdP x"  shows "H  OrdP z"  (*<*)
proof -
  obtain i::name and j::name and k::name
   where atoms: "atom i  (x,y,z)"  "atom j  (i,x,y,z)"  "atom k  (i,j,x,y,z)"  
    by (metis obtain_fresh)
  have "{OrdP (Var i), OrdP x}  All j (HaddP x (Var i) (Var j) IMP OrdP (Var j))"
       (is "_  ?scheme")
    proof (rule OrdInd2H)
      show "{OrdP x}  ?scheme(i::=Zero)"
        using atoms
        by (auto intro: HaddP_Zero_D2 OrdP_cong [THEN Iff_MP_same])
    next
      show "{OrdP x}  All i (OrdP (Var i) IMP ?scheme IMP ?scheme(i::=SUCC (Var i)))"
        using atoms 
        apply auto
        apply (rule cut_same [OF HaddP_SUCC_Ex2 [where z'=k]], auto)
        apply (rule Ex_I [where x="Var k"], auto)
        apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same, THEN rotate3], auto intro: OrdP_SUCC_I)
        done
    qed
  hence "{OrdP (Var i), OrdP x}  (HaddP x (Var i) (Var j) IMP OrdP (Var j))(j::=z)"
    by (rule All_D)
  hence "{OrdP (Var i), OrdP x}  (HaddP x (Var i) z IMP OrdP z)"
    using atoms by simp
  hence "{OrdP x}  HaddP x (Var i) z IMP OrdP z"
    by (metis HaddP_imp_OrdP Imp_cut)
  hence "{OrdP x}  (HaddP x (Var i) z IMP OrdP z)(i::=y)"
    using atoms by (force intro!: Subst)
  thus ?thesis using assms atoms
    by simp (metis anti_deduction cut2)
qed (*>*)

lemma HaddP_Mem_cancel_left: 
  assumes "H  HaddP x y' z'" "H  HaddP x y z" "H  OrdP x"
    shows "H  z' IN z IFF y' IN y" (*<*)
proof -
  obtain i::name and j::name and j'::name and k::name and k'::name 
   where atoms: "atom i  (x,y,y',z,z')" "atom j  (i,x,y,y',z,z')" "atom j'  (i,j,x,y,y',z,z')"
                 "atom k  (i,j,j',x,y,y',z,z')" "atom k'  (i,j,j',k,x,y,y',z,z')"
    by (metis obtain_fresh)
  have "{OrdP (Var i)} 
         All j (All j' (HaddP (Var i) y' (Var j') IMP (HaddP (Var i) y (Var j) IMP
                         ((Var j') IN (Var j) IFF y' IN y))))"
       (is "_  ?scheme")
    proof (rule OrdInd2H)
      show "{}  ?scheme(i::=Zero)"
        using atoms apply simp
        apply (rule All_I Imp_I Ex_EH)+
        apply (rule cut_same [where A="Var j EQ y"])
        apply (metis HaddP_Zero_D1 Sym)
        apply (rule cut_same [where A="Var j' EQ y'"])
        apply (metis HaddP_Zero_D1 Sym thin1)
        apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same], simp)
        apply (rule thin1)
        apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same], auto)
        done
    next
      show "{}  All i (OrdP (Var i) IMP ?scheme IMP ?scheme(i::=SUCC (Var i)))"
        using atoms apply simp
        apply (rule All_I Imp_I Ex_EH)+
        apply (rule cut_same [OF HaddP_SUCC_Ex1 [of k "Var i" y "Var j", THEN cut2]], simp_all)
        apply (rule AssumeH Conj_EH Ex_EH)+
        apply (rule cut_same [OF HaddP_SUCC_Ex1 [of k' "Var i" y' "Var j'", THEN cut2]], simp_all)
        apply (rule AssumeH Conj_EH Ex_EH)+
        apply (rule rotate7)
        apply (rule All_E [where x = "Var k"], simp)
        apply (rule All_E [where x = "Var k'"], simp_all)
        apply (rule Imp_E AssumeH)+
        apply (rule Iff_trans)
        prefer 2
        apply (rule AssumeH)
        apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same, THEN rotate3], simp)
        apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same, THEN rotate5], simp)
        apply (blast intro!: HaddP_OrdP OrdP_IN_SUCC_Iff)
        done
    qed
  hence "{OrdP (Var i)} 
          (All j' (HaddP (Var i) y' (Var j') IMP (HaddP (Var i) y (Var j) IMP ((Var j') IN (Var j) IFF y' IN y))))(j::=z)"
    by (metis All_D)
  hence "{OrdP (Var i)} 
          (All j' (HaddP (Var i) y' (Var j') IMP (HaddP (Var i) y z IMP ((Var j') IN z IFF y' IN y))))"
    using atoms by simp
  hence "{OrdP (Var i)} 
          (HaddP (Var i) y' (Var j') IMP (HaddP (Var i) y z IMP ((Var j') IN z IFF y' IN y)))(j'::=z')"
    by (metis All_D)
  hence "{OrdP (Var i)}  HaddP (Var i) y' z' IMP (HaddP (Var i) y z IMP (z' IN z IFF y' IN y))"
    using atoms by simp
  hence "{}  (OrdP (Var i) IMP HaddP (Var i) y' z' IMP (HaddP (Var i) y z IMP (z' IN z IFF y' IN y)))(i::=x)"
    by (metis Imp_I Subst emptyE)
  thus ?thesis
    using atoms by simp (metis assms MP_null MP_same)
qed (*>*)

lemma HaddP_Mem_cancel_right_Mem: 
  assumes "H  HaddP x' y z'" "H  HaddP x y z" "H  x' IN x" "H  OrdP x"
    shows "H  z' IN z"
proof -
  have "H  OrdP x'"
    by (metis Ord_IN_Ord assms(3) assms(4))
  hence "H  HaddP y x' z'" "H  HaddP y x z"
    by (blast intro: assms HaddP_commute [THEN cut2])+
  thus ?thesis
    by (blast intro: assms HaddP_imp_OrdP [THEN cut1] HaddP_Mem_cancel_left [THEN Iff_MP2_same])
qed

lemma HaddP_Mem_cases:
  assumes "H  HaddP k1 k2 k" "H  OrdP k1" 
          "insert (x IN k1) H  A"
          "insert (Var i IN k2) (insert (HaddP k1 (Var i) x) H)  A"
      and i: "atom (i::name)  (k1,k2,k,x,A)" and "C  H. atom i  C"
    shows "insert (x IN k) H  A" (*<*)
proof -
  obtain j::name where j: "atom j  (k1,k2,k,x)"
    by (metis obtain_fresh)
  have seq: "{HaddP k1 k2 k, x IN k, OrdP k1}  x IN k1 OR (Ex i (HaddP k1 (Var i) x AND Var i IN k2))"
    apply (rule cut_same [OF HaddP_OrdP])
    apply (rule AssumeH)+
    apply (rule cut_same [OF Ord_IN_Ord])
    apply (rule AssumeH)+
    apply (rule OrdP_linear [of _ x k1], (rule AssumeH)+)
    proof -
      show "{x IN k1, OrdP x, OrdP k, HaddP k1 k2 k, x IN k, OrdP k1}  x IN k1 OR Ex i (HaddP k1 (Var i) x AND Var i IN k2)"
        by (blast intro: Disj_I1)
    next
      show "{x EQ k1, OrdP x, OrdP k, HaddP k1 k2 k, x IN k, OrdP k1}  x IN k1 OR Ex i (HaddP k1 (Var i) x AND Var i IN k2)"
        apply (rule cut_same [OF Zero_In_OrdP [of k2, THEN cut1]])
        apply (metis AssumeH(4) HaddP_imp_OrdP cut1)
        apply auto
        apply (rule cut_same [where A="HaddP x Zero k"])
        apply (blast intro: HaddP_cong [THEN Iff_MP_same] Sym)
        apply (rule cut_same [where A="x EQ k"])
        apply (metis HaddP_Zero_D2)
        apply (blast intro: Mem_non_refl Mem_cong [THEN Iff_MP_same])
        apply (rule Disj_I2)
        apply (rule Ex_I [where x=Zero])
        using i apply auto
        apply (rule HaddP_cong [THEN Iff_MP_same])
        apply (rule AssumeH Refl HaddP_Zero2)+
        done
    next
      show "{k1 IN x, OrdP x, OrdP k, HaddP k1 k2 k, x IN k, OrdP k1}  x IN k1 OR Ex i (HaddP k1 (Var i) x AND Var i IN k2)"
        apply (rule Disj_I2)
        apply (rule cut_same [OF Mem_imp_subtract [of _ k1 x j]])
        apply (rule AssumeH)+
        using i j apply auto
        apply (rule Ex_I [where x="Var j"], auto intro: HaddP_Mem_cancel_left [THEN Iff_MP_same])
        done
    qed
  show ?thesis using assms
    by (force intro: cut_same [OF seq [THEN cut3]] thin1 simp: insert_commute)
qed (*>*)

lemma HaddP_Mem_contra: 
  assumes "H  HaddP x y z" "H  z IN x" "H  OrdP x"
    shows "H  A"
proof -
  obtain i::name and j::name and k::name
   where atoms: "atom i  (x,y,z)" "atom j  (i,x,y,z)" "atom k  (i,j,x,y,z)" 
    by (metis obtain_fresh)
  have "{OrdP (Var i)}   All j (HaddP (Var i) y (Var j) IMP Neg ((Var j) IN (Var i)))"
       (is "_  ?scheme")
    proof (rule OrdInd2H)
      show "{}  ?scheme(i::=Zero)"
        using atoms by auto
    next
      show "{}  All i (OrdP (Var i) IMP ?scheme IMP ?scheme(i::=SUCC (Var i)))"
        using  atoms apply auto
        apply (rule cut_same [OF HaddP_SUCC_Ex1 [of k "Var i" y "Var j", THEN cut2]], auto)
        apply (rule Ex_I [where x="Var k"], auto)
        apply (blast intro: OrdP_IN_SUCC_D Mem_cong [OF _ Refl, THEN Iff_MP_same])
        done
    qed
  hence "{OrdP (Var i)}  (HaddP (Var i) y (Var j) IMP Neg ((Var j) IN (Var i)))(j::=z)"
    by (metis All_D)
  hence "{}  OrdP (Var i) IMP HaddP (Var i) y z IMP Neg (z IN (Var i))"
    using atoms by simp (metis Imp_I)
  hence "{}  (OrdP (Var i) IMP HaddP (Var i) y z IMP Neg (z IN (Var i)))(i::=x)"
    by (metis Subst emptyE)
  thus ?thesis
    using atoms by simp (metis MP_same MP_null Neg_D assms)
qed (*>*)

lemma exists_HaddP:
  assumes "H  OrdP y" "atom j  (x,y)"
    shows "H  Ex j (HaddP x y (Var j))"
proof -
  obtain i::name 
   where atoms: "atom i  (j,x,y)" 
    by (metis obtain_fresh)
  have "{OrdP (Var i)}  Ex j (HaddP x (Var i) (Var j))"
       (is "_  ?scheme")
    proof (rule OrdInd2H)
      show "{}  ?scheme(i::=Zero)"
        using atoms assms
        by (force intro!: Ex_I [where x=x] HaddP_Zero2)
    next
      show "{}  All i (OrdP (Var i) IMP ?scheme IMP ?scheme(i::=SUCC (Var i)))"
        using atoms assms
        apply auto
        apply (auto intro!: Ex_I [where x="SUCC (Var j)"] HaddP_SUCC2)
        apply (metis HaddP_SUCC2 insert_commute thin1)
        done
    qed
  hence "{}  OrdP (Var i) IMP Ex j (HaddP x (Var i) (Var j))"
    by (metis Imp_I)
  hence "{}  (OrdP (Var i) IMP Ex j (HaddP x (Var i) (Var j)))(i::=y)"
    using atoms by (force intro!: Subst)
  thus ?thesis 
    using atoms assms by simp (metis MP_null assms(1))
qed

lemma HaddP_Mem_I: 
  assumes "H  HaddP x y z" "H  OrdP x" shows "H  x IN SUCC z"
proof -
  have "{HaddP x y z, OrdP x}  x IN SUCC z"
    apply (rule OrdP_linear [of _ x "SUCC z"])
    apply (auto intro: OrdP_SUCC_I HaddP_OrdP)
    apply (rule HaddP_Mem_contra, blast)
    apply (metis Assume Mem_SUCC_I2 OrdP_IN_SUCC_D Sym_L thin1 thin2, blast)
    apply (blast intro: HaddP_Mem_contra Mem_SUCC_Refl OrdP_Trans)
    done
  thus ?thesis
    by (rule cut2) (auto intro: assms)
qed


section ‹A Shifted Sequence›

nominal_function ShiftP :: "tm  tm  tm  tm  fm"
  where "atom x  (x',y,z,f,del,k); atom x'  (y,z,f,del,k); atom y  (z,f,del,k); atom z  (f,del,g,k) 
    ShiftP f k del g =
      All z (Var z IN g IFF 
      (Ex x (Ex x' (Ex y ((Var z) EQ HPair (Var x') (Var y) AND 
                          HaddP del (Var x) (Var x') AND
                          HPair (Var x) (Var y) IN f AND Var x IN k)))))"
by (auto simp: eqvt_def ShiftP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)

nominal_termination (eqvt)
  by lexicographic_order

lemma ShiftP_fresh_iff [simp]: "a  ShiftP f k del g  a  f  a  k  a  del  a  g"       
proof -
  obtain x::name and x'::name and y::name and z::name 
    where "atom x  (x',y,z,f,del,k)" "atom x'  (y,z,f,del,k)" 
          "atom y  (z,f,del,k)" "atom z  (f,del,g,k)"
    by (metis obtain_fresh)
  thus ?thesis
    by auto
qed

lemma subst_fm_ShiftP [simp]:
  "(ShiftP f k del g)(i::=u) = ShiftP (subst i u f) (subst i u k) (subst i u del) (subst i u g)"
proof -
  obtain x::name and x'::name and y::name and z::name 
  where "atom x  (x',y,z,f,del,k,i,u)" "atom x'  (y,z,f,del,k,i,u)" 
        "atom y  (z,f,del,k,i,u)" "atom z  (f,del,g,k,i,u)"
    by (metis obtain_fresh)
  thus ?thesis
    by (auto simp: ShiftP.simps [of x x' y z])
qed

lemma ShiftP_Zero: "{}  ShiftP Zero k d Zero"
proof -
  obtain x::name and x'::name and y::name and z::name 
  where "atom x  (x',y,z,k,d)" "atom x'  (y,z,k,d)" "atom y  (z,k,d)" "atom z  (k,d)"
    by (metis obtain_fresh)
  thus ?thesis
    by (auto simp: ShiftP.simps [of x x' y z])
qed

lemma ShiftP_Mem1:
  "{ShiftP f k del g, HPair a b IN f, HaddP del a a', a IN k}  HPair a' b IN g"       
proof -
  obtain x::name and x'::name and y::name and z::name 
    where "atom x  (x',y,z,f,del,k,a,a',b)" "atom x'  (y,z,f,del,k,a,a',b)" 
          "atom y  (z,f,del,k,a,a',b)" "atom z  (f,del,g,k,a,a',b)"
    by (metis obtain_fresh)
  thus ?thesis
    apply (auto simp: ShiftP.simps [of x x' y z])
    apply (rule All_E [where x="HPair a' b"], auto intro!: Iff_E2)
    apply (rule Ex_I [where x=a], simp)
    apply (rule Ex_I [where x="a'"], simp)
    apply (rule Ex_I [where x=b], auto intro: Mem_Eats_I1)
    done
qed
 
lemma ShiftP_Mem2:
  assumes "atom u  (f,k,del,a,b)"
  shows  "{ShiftP f k del g, HPair a b IN g}  Ex u ((Var u) IN k AND HaddP del (Var u) a AND HPair (Var u) b IN f)"       
proof -
  obtain x::name and x'::name and y::name and z::name 
  where atoms: "atom x  (x',y,z,f,del,g,k,a,u,b)" "atom x'  (y,z,f,del,g,k,a,u,b)" 
               "atom y  (z,f,del,g,k,a,u,b)" "atom z  (f,del,g,k,a,u,b)"
    by (metis obtain_fresh)
  thus ?thesis using assms
    apply (auto simp: ShiftP.simps [of x x' y z])
    apply (rule All_E [where x="HPair a b"])
    apply (auto intro!: Iff_E1 [OF Assume]) 
    apply (rule Ex_I [where x="Var x"])
    apply (auto intro: Mem_cong [OF HPair_cong Refl, THEN Iff_MP2_same])
    apply (blast intro: HaddP_cong [OF Refl Refl, THEN Iff_MP2_same])
    done
qed

lemma ShiftP_Mem_D:
  assumes "H  ShiftP f k del g" "H  a IN g"
          "atom x  (x',y,a,f,del,k)" "atom x'  (y,a,f,del,k)" "atom y  (a,f,del,k)"
  shows  "H  (Ex x (Ex x' (Ex y (a EQ HPair (Var x') (Var y) AND 
                                  HaddP del (Var x) (Var x') AND
                                  HPair (Var x) (Var y) IN f AND Var x IN k))))" 
         (is "_  ?concl")
proof -
  obtain z::name where "atom z  (x,x',y,f,del,g,k,a)"
    by (metis obtain_fresh)
  hence "{ShiftP f k del g, a IN g}  ?concl" using assms
    by (auto simp: ShiftP.simps [of x x' y z]) (rule All_E [where x=a], auto intro: Iff_E1)
  thus ?thesis
    by (rule cut2) (rule assms)+ 
qed

lemma ShiftP_Eats_Eats: 
  "{ShiftP f k del g, HaddP del a a', a IN k} 
    ShiftP (Eats f (HPair a b)) k del (Eats g (HPair a' b))" (*<*)
proof -
  obtain x::name and x'::name and y::name and z::name 
    where "atom x  (x',y,z,f,del,g,k,a,a',b)" "atom x'  (y,z,f,del,g,k,a,a',b)" 
          "atom y  (z,f,del,g,k,a,a',b)" "atom z  (f,del,g,k,a,a',b)"
    by (metis obtain_fresh)
  thus ?thesis
    apply (auto simp: ShiftP.simps [of x x' y z] intro!: Iff_I [THEN Swap])
    apply (rule All_E [where x="Var z", THEN rotate2], simp)
    apply (rule Iff_E)
    apply auto [1]
    apply (rule Ex_I [where x="Var x"], simp)
    apply (rule Ex_I [where x="Var x'"], simp)
    apply (rule Ex_I [where x="Var y"], simp)
    apply (blast intro: Mem_Eats_I1, blast)
    apply (rule Ex_I [where x=a], simp)
    apply (rule Ex_I [where x="a'"], simp)
    apply (rule Ex_I [where x=b], simp)
    apply (metis Assume AssumeH(3) AssumeH(4) Conj_I Mem_Eats_I2 Refl)
    apply (rule All_E [where x="Var z", THEN rotate5], auto)
    apply (rule Mem_Eats_I1)
    apply (rule Iff_MP2_same [OF Hyp], blast)
    apply (rule Ex_I [where x="Var x"], simp)
    apply (rule Ex_I [where x="Var x'"], simp)
    apply (rule Ex_I [where x="Var y"], auto)
    apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same, THEN rotate5], simp)
    apply (blast intro: Mem_Eats_I2 HaddP_cong [THEN Iff_MP_same] HaddP_unique [THEN cut2] HPair_cong)
    done
qed (*>*)

lemma ShiftP_Eats_Neg: 
  assumes "atom u  (u',v,f,k,del,g,c)" "atom u'  (v,f,k,del,g,c)" "atom v  (f,k,del,g,c)"
  shows
  "{ShiftP f k del g, 
    Neg (Ex u (Ex u' (Ex v (c EQ HPair (Var u) (Var v) AND Var u IN k AND HaddP del (Var u) (Var u')))))} 
    ShiftP (Eats f c) k del g"  (*<*)
proof -
  obtain x::name and x'::name and y::name and z::name 
  where atoms: "atom x  (x',y,z,u,u',v,f,k,del,g,c)" "atom x'  (y,z,u,u',v,f,k,del,g,c)" 
               "atom y  (z,u,u',v,f,k,del,g,c)" "atom z  (u,u',v,f,k,del,g,c)"
    by (metis obtain_fresh)
  thus ?thesis using assms
    apply (auto simp: ShiftP.simps [of x x' y z] intro!: Iff_I [THEN Swap])
    apply (rule All_E [where x="Var z", THEN rotate3])
    apply (auto intro!: Iff_E1 [OF Assume]) 
    apply (rule Ex_I [where x="Var x"], simp)
    apply (rule Ex_I [where x="Var x'"], simp)
    apply (rule Ex_I [where x="Var y"], simp)
    apply (blast intro: Mem_Eats_I1)
    apply (rule All_E [where x="Var z", THEN rotate6], simp)
    apply (rule Iff_E2)
    apply (rule Ex_I [where x="Var x"], simp)
    apply (rule Ex_I [where x="Var x'"], simp)
    apply (rule Ex_I [where x="Var y"])
    apply (auto intro: Mem_Eats_I1)
    apply (rule Swap [THEN rotate5]