Theory Incompleteness.Predicates

chapter‹Basic Predicates›

theory Predicates
imports SyntaxN
begin

section ‹The Subset Relation›

nominal_function Subset :: "tm  tm  fm"   (infixr "SUBS" 150)
  where "atom z  (t, u)  t SUBS u = All2 z t ((Var z) IN u)"
  by (auto simp: eqvt_def Subset_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)

nominal_termination (eqvt)
  by lexicographic_order

declare Subset.simps [simp del]

lemma Subset_fresh_iff [simp]: "a  t SUBS u  a  t  a  u"
  apply (rule obtain_fresh [where x="(t, u)"])
  apply (subst Subset.simps, auto)
  done

lemma eval_fm_Subset [simp]: "eval_fm e (Subset t u)  (te  ue)"
  apply (rule obtain_fresh [where x="(t, u)"])
  apply (subst Subset.simps, auto)
  done

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

lemma Subset_I:
  assumes "insert ((Var i) IN t) H  (Var i) IN u" "atom i  (t,u)" "B  H. atom i  B"
  shows "H  t SUBS u"
by (subst Subset.simps [of i]) (auto simp: assms)

lemma Subset_D:
  assumes major: "H  t SUBS u" and minor: "H  a IN t" shows "H  a IN u"
proof -
  obtain i::name where i: "atom i  (t, u)"
    by (rule obtain_fresh)
  hence "H  (Var i IN t IMP Var i IN u) (i::=a)"
    by (metis Subset.simps major All_D)
  thus ?thesis
    using i  by simp (metis MP_same minor)
qed

lemma Subset_E: "H  t SUBS u  H  a IN t  insert (a IN u) H  A  H  A"
  by (metis Subset_D cut_same)

lemma Subset_cong: "H  t EQ t'  H  u EQ u'  H  t SUBS u IFF t' SUBS u'"
  by (rule P2_cong) auto

lemma Set_MP: "x SUBS y  H  z IN x  H  insert (z IN y) H  A  H  A"
  by (metis Assume Subset_D cut_same insert_absorb)

lemma Zero_Subset_I [intro!]: "H  Zero SUBS t"
proof -
  have "{}  Zero SUBS t"
    by (rule obtain_fresh [where x="(Zero,t)"]) (auto intro: Subset_I)
  thus ?thesis
    by (auto intro: thin)
qed

lemma Zero_SubsetE: "H  A  insert (Zero SUBS X) H  A"
  by (rule thin1)

lemma Subset_Zero_D:
   assumes "H  t SUBS Zero" shows "H  t EQ Zero"
proof -
  obtain i::name where i [iff]: "atom i  t"
    by (rule obtain_fresh)
  have "{t SUBS Zero}  t EQ Zero"
  proof (rule Eq_Zero_I)
    fix A
    show "{Var i IN t, t SUBS Zero}  A"
      by (metis Hyp Subset_D insertI1 thin1 Mem_Zero_E cut1)
  qed auto
  thus ?thesis
    by (metis assms cut1)
qed

lemma Subset_refl: "H  t SUBS t"
proof -
  obtain i::name where "atom i  t"
    by (rule obtain_fresh)
  thus ?thesis
    by (metis Assume Subset_I empty_iff fresh_Pair thin0)
qed

lemma Eats_Subset_Iff: "H  Eats x y SUBS z IFF (x SUBS z) AND (y IN z)"
proof -
  obtain i::name where i: "atom i  (x,y,z)"
    by (rule obtain_fresh)
  have "{}  (Eats x y SUBS z) IFF (x SUBS z AND y IN z)"
  proof (rule Iff_I) 
    show "{Eats x y SUBS z}  x SUBS z AND y IN z"
    proof (rule Conj_I) 
      show "{Eats x y SUBS z}  x SUBS z"
        apply (rule Subset_I [where i=i]) using i
        apply (auto intro: Subset_D Mem_Eats_I1) 
        done
    next
      show "{Eats x y SUBS z}  y IN z"
        by (metis Subset_D Assume Mem_Eats_I2 Refl) 
    qed
  next
    show "{x SUBS z AND y IN z}  Eats x y SUBS z" using i
      by (auto intro!: Subset_I [where i=i] intro: Subset_D Mem_cong [THEN Iff_MP2_same])
  qed
  thus ?thesis
    by (rule thin0) 
qed

lemma Eats_Subset_I [intro!]: "H  x SUBS z  H  y IN z  H  Eats x y SUBS z"
  by (metis Conj_I Eats_Subset_Iff Iff_MP2_same)

lemma Eats_Subset_E [intro!]:
  "insert (x SUBS z) (insert (y IN z) H)  C  insert (Eats x y SUBS z) H  C"
  by (metis Conj_E Eats_Subset_Iff Iff_MP_left')

text‹A surprising proof: a consequence of @{thm Eats_Subset_Iff} and reflexivity!›
lemma Subset_Eats_I [intro!]: "H  x SUBS Eats x y"
  by (metis Conj_E1 Eats_Subset_Iff Iff_MP_same Subset_refl)

lemma SUCC_Subset_I [intro!]: "H  x SUBS z  H  x IN z  H  SUCC x SUBS z"
  by (metis Eats_Subset_I SUCC_def)

lemma SUCC_Subset_E [intro!]:
  "insert (x SUBS z) (insert (x IN z) H)  C  insert (SUCC x SUBS z) H  C"
  by (metis Eats_Subset_E SUCC_def)

lemma Subset_trans0: "{ a SUBS b, b SUBS c }  a SUBS c"
proof -
  obtain i::name where [simp]: "atom i  (a,b,c)"
    by (rule obtain_fresh)
  show ?thesis
    by (rule Subset_I [of i]) (auto intro: Subset_D)
qed

lemma Subset_trans: "H  a SUBS b  H  b SUBS c  H  a SUBS c"
  by (metis Subset_trans0 cut2)

lemma Subset_SUCC: "H  a SUBS (SUCC a)"
  by (metis SUCC_def Subset_Eats_I)

lemma All2_Subset_lemma: "atom l  (k',k)  {P}  P'  {All2 l k P, k' SUBS k}  All2 l k' P'"
  apply auto
  apply (rule Ex_I [where x = "Var l"])
  apply (auto intro: ContraProve Set_MP cut1)
  done

lemma All2_Subset: "H  All2 l k P; H  k' SUBS k; {P}  P'; atom l  (k', k)  H  All2 l k' P'"
  by (rule cut2 [OF All2_Subset_lemma]) auto


section‹Extensionality›

lemma Extensionality: "H  x EQ y IFF x SUBS y AND y SUBS x"
proof -
  obtain i::name and j::name and k::name
    where atoms: "atom i  (x,y)"  "atom j  (i,x,y)"  "atom k  (i,j,y)"
    by (metis obtain_fresh) 
  have "{}  (Var i EQ y IFF Var i SUBS y AND y SUBS Var i)" (is "{}  ?scheme")
  proof (rule Ind [of j])
    show "atom j  (i, ?scheme)" using atoms
      by simp 
  next
    show "{}  ?scheme(i::=Zero)" using atoms
    proof auto
      show "{Zero EQ y}  y SUBS Zero"
        by (rule Subset_cong [OF Assume Refl, THEN Iff_MP_same]) (rule Subset_refl)
    next
      show "{Zero SUBS y, y SUBS Zero}  Zero EQ y"
        by (metis AssumeH(2) Subset_Zero_D Sym)
    qed
  next
    show "{}  All i (All j (?scheme IMP ?scheme(i::=Var j) IMP ?scheme(i::=Eats (Var i) (Var j))))"
      using atoms
      apply auto
      apply (metis Subset_cong [OF Refl Assume, THEN Iff_MP_same] Subset_Eats_I)
      apply (metis Mem_cong [OF Refl Assume, THEN Iff_MP_same] Mem_Eats_I2 Refl)
      apply (metis Subset_cong [OF Assume Refl, THEN Iff_MP_same] Subset_refl)
      apply (rule Eq_Eats_I [of _ k, THEN Sym])
      apply (auto intro: Set_MP [where x=y] Subset_D [where t = "Var i"] Disj_I1 Disj_I2)
      apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same], auto)
      done
  qed
  hence "{}  (Var i EQ y IFF Var i SUBS y AND y SUBS Var i)(i::=x)" 
    by (metis Subst emptyE)
  thus ?thesis using atoms
    by (simp add: thin0)
qed

lemma Equality_I: "H  y SUBS x  H  x SUBS y  H  x EQ y"
  by (metis Conj_I Extensionality Iff_MP2_same)

lemma EQ_imp_SUBS: "insert (t EQ u) H  (t SUBS u)"
  by (meson Assume Iff_MP_same Refl Subset_cong Subset_refl)

lemma EQ_imp_SUBS2: "insert (u EQ t) H  (t SUBS u)"
  by (metis EQ_imp_SUBS Sym_L)

lemma Equality_E: "insert (t SUBS u) (insert (u SUBS t) H)  A  insert (t EQ u) H  A"
  by (metis Conj_E Extensionality Iff_MP_left')


section ‹The Disjointness Relation›

text‹The following predicate is defined in order to prove Lemma 2.3, Foundation›

nominal_function Disjoint :: "tm  tm  fm"
  where "atom z  (t, u)  Disjoint t u = All2 z t (Neg ((Var z) IN u))"
  by (auto simp: eqvt_def Disjoint_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)

nominal_termination (eqvt)
  by lexicographic_order

declare Disjoint.simps [simp del]

lemma Disjoint_fresh_iff [simp]: "a  Disjoint t u  a  t  a  u"
proof -
  obtain j::name where j: "atom j  (a,t,u)"
    by (rule obtain_fresh)
  thus ?thesis
    by (auto simp: Disjoint.simps [of j])
qed

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

lemma Disjoint_cong: "H  t EQ t'  H  u EQ u'  H  Disjoint t u IFF Disjoint t' u'"
  by (rule P2_cong) auto

lemma Disjoint_I:
  assumes "insert ((Var i) IN t) (insert ((Var i) IN u) H)  Fls"
          "atom i  (t,u)" "B  H. atom i  B"
  shows "H  Disjoint t u"
by (subst Disjoint.simps [of i]) (auto simp: assms insert_commute)

lemma Disjoint_E:
  assumes major: "H  Disjoint t u" and minor: "H  a IN t" "H  a IN u" shows "H  A"
proof -
  obtain i::name where i: "atom i  (t, u)"
    by (rule obtain_fresh)
  hence "H  (Var i IN t IMP Neg (Var i IN u)) (i::=a)"
    by (metis Disjoint.simps major All_D)
  thus ?thesis using i
    by simp (metis MP_same Neg_D minor)
qed

lemma Disjoint_commute: "{ Disjoint t u }  Disjoint u t"
proof -
  obtain i::name where "atom i  (t,u)"
    by (rule obtain_fresh)
  thus ?thesis
    by (auto simp: fresh_Pair intro: Disjoint_I Disjoint_E) 
qed

lemma Disjoint_commute_I: "H  Disjoint t u  H  Disjoint u t"
  by (metis Disjoint_commute cut1)

lemma Disjoint_commute_D: "insert (Disjoint t u) H  A  insert (Disjoint u t) H  A" 
  by (metis Assume Disjoint_commute_I cut_same insert_commute thin1)

lemma Zero_Disjoint_I1 [iff]: "H  Disjoint Zero t"
proof -
  obtain i::name where i: "atom i  t"
    by (rule obtain_fresh)
  hence "{}  Disjoint Zero t"
    by (auto intro: Disjoint_I [of i]) 
  thus ?thesis
    by (metis thin0)
qed

lemma Zero_Disjoint_I2 [iff]: "H  Disjoint t Zero"
  by (metis Disjoint_commute Zero_Disjoint_I1 cut1)

lemma Disjoint_Eats_D1: "{ Disjoint (Eats x y) z }  Disjoint x z"
proof -
  obtain i::name where i: "atom i  (x,y,z)"
    by (rule obtain_fresh)
  show ?thesis
    apply (rule Disjoint_I [of i])  
    apply (blast intro: Disjoint_E Mem_Eats_I1)
    using i apply auto
    done
qed

lemma Disjoint_Eats_D2: "{ Disjoint (Eats x y) z }  Neg(y IN z)"
proof -
  obtain i::name where i: "atom i  (x,y,z)"
    by (rule obtain_fresh)
  show ?thesis
    by (force intro: Disjoint_E [THEN rotate2] Mem_Eats_I2)
qed

lemma Disjoint_Eats_E: 
  "insert (Disjoint x z) (insert (Neg(y IN z)) H)  A  insert (Disjoint (Eats x y) z) H  A"
  by (meson Conj_E Conj_I Disjoint_Eats_D1 Disjoint_Eats_D2 rcut1)

lemma Disjoint_Eats_E2: 
  "insert (Disjoint z x) (insert (Neg(y IN z)) H)  A  insert (Disjoint z (Eats x y)) H  A"
  by (metis Disjoint_Eats_E Disjoint_commute_D)
    
lemma Disjoint_Eats_Imp: "{ Disjoint x z, Neg(y IN z) }  Disjoint (Eats x y) z"
proof -
  obtain i::name where"atom i  (x,y,z)"
    by (rule obtain_fresh)
  then show ?thesis 
    by (auto intro: Disjoint_I [of i]  Disjoint_E [THEN rotate3] 
                    Mem_cong [OF Assume Refl, THEN Iff_MP_same])
qed

lemma Disjoint_Eats_I [intro!]: "H  Disjoint x z  insert (y IN z) H  Fls  H  Disjoint (Eats x y) z"
  by (metis Neg_I cut2 [OF Disjoint_Eats_Imp])

lemma Disjoint_Eats_I2 [intro!]: "H  Disjoint z x  insert (y IN z) H  Fls  H  Disjoint z (Eats x y)"
  by (metis Disjoint_Eats_I Disjoint_commute cut1)


section ‹The Foundation Theorem›

lemma Foundation_lemma: 
  assumes i: "atom i  z"
  shows "{ All2 i z (Neg (Disjoint (Var i) z)) }  Neg (Var i IN z) AND Disjoint (Var i) z"
proof -
  obtain j::name  where j: "atom j  (z,i)"
    by (metis obtain_fresh) 
  show ?thesis
    apply (rule Ind [of j]) using i j
    apply auto
    apply (rule Ex_I [where x=Zero], auto)
    apply (rule Ex_I [where x="Eats (Var i) (Var j)"], auto)
    apply (metis ContraAssume insertI1 insert_commute)
    apply (metis ContraProve Disjoint_Eats_Imp rotate2 thin1)
    apply (metis Assume Disj_I1 anti_deduction rotate3)
    done
qed    

theorem Foundation: "atom i  z  {}  All2 i z (Neg (Disjoint (Var i) z)) IMP z EQ Zero"
  apply auto 
  apply (rule Eq_Zero_I)
  apply (rule cut_same [where A = "(Neg ((Var i) IN z) AND Disjoint (Var i) z)"])
  apply (rule Foundation_lemma [THEN cut1], auto)
  done

lemma Mem_Neg_refl: "{}  Neg (x IN x)"
proof -
  obtain i::name where i: "atom i  x"
    by (metis obtain_fresh)
  have "{}  Disjoint x (Eats Zero x)" 
    apply (rule cut_same [OF Foundation [where z = "Eats Zero x"]]) using i
    apply auto
    apply (rule cut_same [where A = "Disjoint x (Eats Zero x)"])    
    apply (metis Assume thin1 Disjoint_cong [OF Assume Refl, THEN Iff_MP_same])
    apply (metis Assume AssumeH(4) Disjoint_E Mem_Eats_I2 Refl) 
    done
  thus ?thesis 
    by (metis Disjoint_Eats_D2 Disjoint_commute cut_same)
qed

lemma Mem_refl_E [intro!]: "insert (x IN x) H  A"
  by (metis Disj_I1 Mem_Neg_refl anti_deduction thin0)

lemma Mem_non_refl: assumes "H  x IN x" shows "H  A"
  by (metis Mem_refl_E assms cut_same)

lemma Mem_Neg_sym: "{ x IN y, y IN x }  Fls"
proof -
  obtain i::name where i: "atom i  (x,y)"
    by (metis obtain_fresh)
  have "{}  Disjoint x (Eats Zero y) OR Disjoint y (Eats Zero x)" 
    apply (rule cut_same [OF Foundation [where i=i and z = "Eats (Eats Zero y) x"]]) using i
    apply (auto intro!: Disjoint_Eats_E2 [THEN rotate2])
    apply (rule Disj_I2, auto)
    apply (metis Assume EQ_imp_SUBS2 Subset_D insert_commute)
    apply (blast intro!: Disj_I1 Disjoint_cong [OF Hyp Refl, THEN Iff_MP_same])
    done
  thus ?thesis
    by (auto intro: cut0 Disjoint_Eats_E2)
qed

lemma Mem_not_sym: "insert (x IN y) (insert (y IN x) H)  A"
  by (rule cut_thin [OF Mem_Neg_sym]) auto

  
section ‹The Ordinal Property›

nominal_function OrdP :: "tm  fm"
  where "atom y  (x, z); atom z  x 
    OrdP x = All2 y x ((Var y) SUBS x AND  All2 z (Var y) ((Var z) SUBS (Var y)))"
  by (auto simp: eqvt_def OrdP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)

nominal_termination (eqvt)
  by lexicographic_order

lemma
 shows OrdP_fresh_iff [simp]: "a  OrdP x  a  x"       (is ?thesis1)
   and eval_fm_OrdP [simp]:  "eval_fm e (OrdP x)  Ord xe"  (is ?thesis2)
proof -
  obtain z::name and y::name where "atom z  x" "atom y  (x, z)"
    by (metis obtain_fresh)
  thus ?thesis1 ?thesis2
    by (auto simp: OrdP.simps [of y _ z] Ord_def Transset_def)
qed

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

lemma OrdP_cong: "H  x EQ x'  H  OrdP x IFF OrdP x'"
  by (rule P1_cong) auto

lemma OrdP_Mem_lemma:
  assumes z: "atom z  (k,l)" and l: "insert (OrdP k) H  l IN k"
  shows "insert (OrdP k) H  l SUBS k AND All2 z l (Var z SUBS l)"
proof -
  obtain y::name where y: "atom y  (k,l,z)"
    by (metis obtain_fresh)
  have "insert (OrdP k) H 
         (Var y IN k IMP (Var y SUBS k AND All2 z (Var y) (Var z SUBS Var y)))(y::=l)"
    by (rule All_D) (simp add: OrdP.simps [of y _ z] y z Assume) 
  also have "... = l IN k IMP (l SUBS k AND All2 z l (Var z SUBS l))" 
    using y z  by simp
  finally show ?thesis
    by (metis MP_same l) 
qed

lemma OrdP_Mem_E:
  assumes "atom z  (k,l)" 
          "insert (OrdP k) H  l IN k"
          "insert (l SUBS k) (insert (All2 z l (Var z SUBS l)) H)  A"
  shows "insert (OrdP k) H  A" 
  apply (rule OrdP_Mem_lemma [THEN cut_same])
  apply (auto simp: insert_commute)
  apply (blast intro: assms thin1)+
  done

lemma OrdP_Mem_imp_Subset:
  assumes k: "H  k IN l" and l: "H  OrdP l" shows "H  k SUBS l"
  apply (rule obtain_fresh [of "(l,k)"])
  apply (rule cut_same [OF l])
  using k  apply (auto intro: OrdP_Mem_E thin1)
  done

lemma SUCC_Subset_Ord_lemma: "{ k' IN k, OrdP k }  SUCC k' SUBS k"
  by auto (metis Assume thin1 OrdP_Mem_imp_Subset)

lemma SUCC_Subset_Ord: "H  k' IN k  H  OrdP k  H  SUCC k' SUBS k"
  by (blast intro!: cut2 [OF SUCC_Subset_Ord_lemma])

lemma OrdP_Trans_lemma: "{ OrdP k, i IN j, j IN k }  i IN k"
proof -
  obtain m::name where "atom m  (i,j,k)"
    by (metis obtain_fresh) 
  thus ?thesis
    by (auto intro: OrdP_Mem_E [of m k j] Subset_D [THEN rotate3])
qed

lemma OrdP_Trans: "H   OrdP k  H  i IN j  H  j IN k  H   i IN k"
  by (blast intro: cut3 [OF OrdP_Trans_lemma])

lemma Ord_IN_Ord0:
  assumes l: "H  l IN k"
  shows "insert (OrdP k) H  OrdP l"
proof -
  obtain z::name and y::name where z: "atom z  (k,l)" and y: "atom y  (k,l,z)"
    by (metis obtain_fresh)
  have "{Var y IN l, OrdP k, l IN k}  All2 z (Var y) (Var z SUBS Var y)"  using y z
    apply (simp add: insert_commute [of _ "OrdP k"]) 
    apply (auto intro: OrdP_Mem_E [of z k "Var y"] OrdP_Trans_lemma del: All_I Neg_I)
    done
  hence "{OrdP k, l IN k}  OrdP l" using z y
    apply (auto simp: OrdP.simps [of y l z])
    apply (simp add: insert_commute [of _ "OrdP k"]) 
    apply (rule OrdP_Mem_E [of y k l], simp_all)
    apply (metis Assume thin1)
    apply (rule All_E [where x= "Var y", THEN thin1], simp) 
    apply (metis Assume anti_deduction insert_commute) 
    done
  thus ?thesis
    by (metis (full_types) Assume l cut2 thin1) 
qed

lemma Ord_IN_Ord: "H  l IN k  H  OrdP k  H  OrdP l"
  by (metis Ord_IN_Ord0 cut_same)

lemma OrdP_I:
  assumes "insert (Var y IN x) H  (Var y) SUBS x"
      and "insert (Var z IN Var y) (insert (Var y IN x) H)  (Var z) SUBS (Var y)"
      and "atom y  (x, z)" "B  H. atom y  B"  "atom z  x" "B  H. atom z  B"
    shows "H  OrdP x"
  using assms by auto

lemma OrdP_Zero [simp]: "H  OrdP Zero"
proof -
  obtain y::name and z::name where "atom y  z"
    by (rule obtain_fresh)
  hence "{}  OrdP Zero"
    by (auto intro: OrdP_I [of y _ _ z])
  thus ?thesis 
    by (metis thin0)
qed

lemma OrdP_SUCC_I0: "{ OrdP k }  OrdP (SUCC k)"
proof -
  obtain w::name and y::name and z::name where atoms: "atom w  (k,y,z)" "atom y  (k,z)" "atom z  k"
    by (metis obtain_fresh)
  have 1: "{Var y IN SUCC k, OrdP k}  Var y SUBS SUCC k"
    apply (rule Mem_SUCC_E)
    apply (rule OrdP_Mem_E [of w _ "Var y", THEN rotate2]) using atoms
    apply auto
    apply (metis Assume Subset_SUCC Subset_trans)   
    apply (metis EQ_imp_SUBS Subset_SUCC Subset_trans)
    done
  have in_case: "{Var y IN k, Var z IN Var y, OrdP k}  Var z SUBS Var y"
    apply (rule OrdP_Mem_E [of w _ "Var y", THEN rotate3]) using atoms
    apply (auto intro:  All2_E [THEN thin1])
    done
  have "{Var y EQ k, Var z IN k, OrdP k}  Var z SUBS Var y"
    by (metis AssumeH(2) AssumeH(3) EQ_imp_SUBS2 OrdP_Mem_imp_Subset Subset_trans)
  hence eq_case: "{Var y EQ k, Var z IN Var y, OrdP k}  Var z SUBS Var y"
    by (rule cut3) (auto intro: EQ_imp_SUBS [THEN cut1] Subset_D)
  have 2: "{Var z IN Var y, Var y IN SUCC k, OrdP k}  Var z SUBS Var y"
    by (metis rotate2 Mem_SUCC_E in_case eq_case)   
  show ?thesis
    using OrdP_I [OF 1 2] atoms
    by (metis OrdP_fresh_iff SUCC_fresh_iff fresh_Pair singletonD)
qed

lemma OrdP_SUCC_I: "H  OrdP k  H  OrdP (SUCC k)"
  by (metis OrdP_SUCC_I0 cut1)

lemma Zero_In_OrdP: "{ OrdP x }  x EQ Zero OR Zero IN x"
proof -
  obtain i::name and j::name
    where i: "atom i  x" and j: "atom j  (x,i)"
    by (metis obtain_fresh)
  show ?thesis
    apply (rule cut_thin [where HB = "{OrdP x}", OF Foundation [where i=i and z = x]])
    using i j apply auto
    prefer 2 apply (metis Assume Disj_I1)
    apply (rule Disj_I2)
    apply (rule cut_same [where A = "Var i EQ Zero"])
    prefer 2 apply (blast intro: Iff_MP_same [OF Mem_cong [OF Assume Refl]])
    apply (auto intro!: Eq_Zero_I [where i=j] Ex_I [where x="Var i"])
    apply (blast intro: Disjoint_E Subset_D)
    done
qed

lemma OrdP_HPairE: "insert (OrdP (HPair x y)) H  A"
proof -
  have "{ OrdP (HPair x y) }  A"
    by (rule cut_same [OF Zero_In_OrdP]) (auto simp: HPair_def)
  thus ?thesis
    by (metis Assume cut1)
qed

lemmas OrdP_HPairEH = OrdP_HPairE OrdP_HPairE [THEN rotate2] OrdP_HPairE [THEN rotate3] OrdP_HPairE [THEN rotate4] OrdP_HPairE [THEN rotate5] 
                 OrdP_HPairE [THEN rotate6] OrdP_HPairE [THEN rotate7] OrdP_HPairE [THEN rotate8] OrdP_HPairE [THEN rotate9] OrdP_HPairE [THEN rotate10]
declare OrdP_HPairEH [intro!]

lemma Zero_Eq_HPairE: "insert (Zero EQ HPair x y) H  A"
  by (metis Eats_EQ_Zero_E2 HPair_def)

lemmas Zero_Eq_HPairEH = Zero_Eq_HPairE Zero_Eq_HPairE [THEN rotate2] Zero_Eq_HPairE [THEN rotate3] Zero_Eq_HPairE [THEN rotate4] Zero_Eq_HPairE [THEN rotate5] 
                 Zero_Eq_HPairE [THEN rotate6] Zero_Eq_HPairE [THEN rotate7] Zero_Eq_HPairE [THEN rotate8] Zero_Eq_HPairE [THEN rotate9] Zero_Eq_HPairE [THEN rotate10]
declare Zero_Eq_HPairEH [intro!]

lemma HPair_Eq_ZeroE: "insert (HPair x y EQ Zero) H  A"
  by (metis Sym_L Zero_Eq_HPairE)

lemmas HPair_Eq_ZeroEH = HPair_Eq_ZeroE HPair_Eq_ZeroE [THEN rotate2] HPair_Eq_ZeroE [THEN rotate3] HPair_Eq_ZeroE [THEN rotate4] HPair_Eq_ZeroE [THEN rotate5] 
                 HPair_Eq_ZeroE [THEN rotate6] HPair_Eq_ZeroE [THEN rotate7] HPair_Eq_ZeroE [THEN rotate8] HPair_Eq_ZeroE [THEN rotate9] HPair_Eq_ZeroE [THEN rotate10]
declare HPair_Eq_ZeroEH [intro!]

section ‹Induction on Ordinals›

lemma OrdInd_lemma:
  assumes j: "atom (j::name)  (i,A)"
  shows "{ OrdP (Var i) }  (All i (OrdP (Var i) IMP ((All2 j (Var i) (A(i::= Var j))) IMP A))) IMP A"
proof -
  obtain l::name and k::name
      where l: "atom l  (i,j,A)" and k: "atom k  (i,j,l,A)" 
      by (metis obtain_fresh)  
  have "{ (All i (OrdP (Var i) IMP ((All2 j (Var i) (A(i::= Var j))) IMP A))) } 
         (All2 l (Var i) (OrdP (Var l) IMP A(i::= Var l)))"
    apply (rule Ind [of k]) 
    using j k l apply auto
    apply (rule All_E [where x="Var l", THEN rotate5], auto)
    apply (metis Assume Disj_I1 anti_deduction thin1)
    apply (rule Ex_I [where x="Var l"], auto)
    apply (rule All_E [where x="Var j", THEN rotate6], auto)
    apply (blast intro: ContraProve Iff_MP_same [OF Mem_cong [OF Refl]])
    apply (metis Assume Ord_IN_Ord0 ContraProve insert_commute)
    apply (metis Assume Neg_D thin1)+
    done
  hence "{ (All i (OrdP (Var i) IMP ((All2 j (Var i) (A(i::= Var j))) IMP A))) } 
           (All2 l (Var i) (OrdP (Var l) IMP A(i::= Var l)))(i::= Eats Zero (Var i))"
    by (rule Subst, auto) 
  hence indlem: "{ All i (OrdP (Var i) IMP ((All2 j (Var i) (A(i::= Var j))) IMP A)) } 
              All2 l (Eats Zero (Var i)) (OrdP (Var l) IMP A(i::=Var l))" 
    using j l by simp 
  show ?thesis
    apply (rule Imp_I)
    apply (rule cut_thin [OF indlem, where HB = "{OrdP (Var i)}"])
    apply (rule All2_Eats_E) using j l
    apply auto 
    done
qed

lemma OrdInd:
  assumes j: "atom (j::name)  (i,A)"
  and x: "H  OrdP (Var i)" and step: "H  All i (OrdP (Var i) IMP (All2 j (Var i) (A(i::= Var j)) IMP A))"
  shows "H  A"
  apply (rule cut_thin [OF x, where HB=H])
  apply (rule MP_thin [OF OrdInd_lemma step])
  apply (auto simp: j)
  done

lemma OrdIndH:
  assumes "atom (j::name)  (i,A)"
      and "H  All i (OrdP (Var i) IMP (All2 j (Var i) (A(i::= Var j)) IMP A))"
    shows "insert (OrdP (Var i)) H  A"
  by (metis assms thin1 Assume OrdInd)

  
section ‹Linearity of Ordinals›

lemma OrdP_linear_lemma:
  assumes j: "atom j  i"
  shows "{ OrdP (Var i) }  All j (OrdP (Var j) IMP (Var i IN Var j OR Var i EQ Var j OR Var j IN Var i))"
         (is "_  ?scheme")
proof -
  obtain k::name and l::name and m::name
    where k: "atom k  (i,j)" and l: "atom l  (i,j,k)" and m: "atom m  (i,j)"
    by (metis obtain_fresh) 
  show ?thesis
  proof (rule OrdIndH [where i=i and j=k])
    show "atom k  (i, ?scheme)"
      using k  by (force simp add: fresh_Pair)  
  next
    show "{}  All i (OrdP (Var i) IMP (All2 k (Var i) (?scheme(i::= Var k)) IMP ?scheme))"
      using j k
      apply simp
      apply (rule All_I Imp_I)+
        defer 1
        apply auto [2]
      apply (rule OrdIndH [where i=j and j=l]) using l
        ― ‹nested induction›
       apply (force simp add: fresh_Pair)
      apply simp
      apply (rule All_I Imp_I)+
       prefer 2  apply force
      apply (rule Disj_3I)
      apply (rule Equality_I)
        ― ‹Now the opposite inclusion, @{term"Var j SUBS Var i"}
       apply (rule Subset_I [where i=m])
         apply (rule All2_E [THEN rotate4]) using l m
           apply auto
        apply (blast intro: ContraProve [THEN rotate3] OrdP_Trans)
       apply (blast intro: ContraProve [THEN rotate3] Mem_cong [OF Hyp Refl, THEN Iff_MP2_same])
        ― ‹Now the opposite inclusion, @{term"Var i SUBS Var j"}
      apply (rule Subset_I [where i=m])
        apply (rule All2_E [THEN rotate6], auto) 
      apply (rule All_E [where x = "Var j"], auto) 
       apply (blast intro: ContraProve [THEN rotate4] Mem_cong [OF Hyp Refl, THEN Iff_MP_same])
      apply (blast intro: ContraProve [THEN rotate4] OrdP_Trans)
      done
  qed
qed

lemma OrdP_linear_imp: "{}  OrdP x IMP OrdP y IMP x IN y OR x EQ y OR y IN x"
proof -
  obtain i::name and j::name
    where atoms: "atom i  (x,y)" "atom j  (x,y,i)" 
    by (metis obtain_fresh) 
  have "{ OrdP (Var i) }  (OrdP (Var j) IMP (Var i IN Var j OR Var i EQ Var j OR Var j IN Var i))(j::=y)"
    using atoms  by (metis All_D OrdP_linear_lemma fresh_Pair)
  hence "{}  OrdP (Var i) IMP OrdP y IMP (Var i IN y OR Var i EQ y OR y IN Var i)"
    using atoms by auto
  hence "{}  (OrdP (Var i) IMP OrdP y IMP (Var i IN y OR Var i EQ y OR y IN Var i))(i::=x)"
    by (metis Subst empty_iff)
  thus ?thesis
    using atoms by auto
qed
  
lemma OrdP_linear:
  assumes "H  OrdP x" "H  OrdP y" 
          "insert (x IN y) H  A" "insert (x EQ y) H  A" "insert (y IN x) H  A" 
    shows "H  A"
proof -
  have "{ OrdP x, OrdP y }  x IN y OR x EQ y OR y IN x"
    by (metis OrdP_linear_imp Imp_Imp_commute anti_deduction)
  thus ?thesis    
    using assms  by (metis cut2 Disj_E cut_same)
qed

lemma Zero_In_SUCC: "{OrdP k}  Zero IN SUCC k"
  by (rule OrdP_linear [OF OrdP_Zero OrdP_SUCC_I]) (force simp: SUCC_def)+


section ‹The predicate OrdNotEqP›

nominal_function OrdNotEqP :: "tm  tm  fm"  (infixr "NEQ" 150)
  where "OrdNotEqP x y = OrdP x AND OrdP y AND (x IN y OR y IN x)"
  by (auto simp: eqvt_def OrdNotEqP_graph_aux_def)

nominal_termination (eqvt)
  by lexicographic_order

lemma OrdNotEqP_fresh_iff [simp]: "a  OrdNotEqP x y  a  x  a  y"
  by auto

lemma eval_fm_OrdNotEqP [simp]: "eval_fm e (OrdNotEqP x y)  Ord xe  Ord ye  xe  ye"
  by (auto simp: hmem_not_refl) (metis Ord_linear)

lemma OrdNotEqP_subst [simp]: "(OrdNotEqP x y)(i::=t) = OrdNotEqP (subst i t x) (subst i t y)"
  by simp

lemma OrdNotEqP_cong: "H  x EQ x'  H  y EQ y'  H  OrdNotEqP x y IFF OrdNotEqP x' y'"
  by (rule P2_cong) auto

lemma OrdNotEqP_self_contra: "{x NEQ x}  Fls"
  by auto

lemma OrdNotEqP_OrdP_E: "insert (OrdP x) (insert (OrdP y) H)  A  insert (x NEQ y) H  A"
  by (auto intro: thin1 rotate2)

lemma OrdNotEqP_I: "insert (x EQ y) H  Fls  H  OrdP x  H  OrdP y  H  x NEQ y"
  by (rule OrdP_linear [of _ x y]) (auto intro: ExFalso thin1 Disj_I1 Disj_I2)

declare OrdNotEqP.simps [simp del]

lemma OrdNotEqP_imp_Neg_Eq: "{x NEQ y}  Neg (x EQ y)"
  by (blast intro: OrdNotEqP_cong [THEN Iff_MP2_same]  OrdNotEqP_self_contra [of x, THEN cut1])

lemma OrdNotEqP_E: "H  x EQ y  insert (x NEQ y) H  A"
  by (metis ContraProve OrdNotEqP_imp_Neg_Eq rcut1)

  
section ‹Predecessor of an Ordinal›

lemma OrdP_set_max_lemma:
  assumes j: "atom (j::name)  i" and k: "atom (k::name)  (i,j)"
  shows "{}  (Neg (Var i EQ Zero) AND (All2 j (Var i) (OrdP (Var j)))) IMP 
              (Ex j (Var j IN Var i AND (All2 k (Var i) (Var k SUBS Var j))))"
proof -
  obtain l::name where l: "atom l  (i,j,k)" 
    by (metis obtain_fresh) 
  show ?thesis
    apply (rule Ind [of l i]) using j k l 
      apply simp_all
     apply (metis Conj_E Refl Swap Imp_I)
    apply (rule All_I Imp_I)+  
      apply simp_all
    apply clarify
    apply (rule thin1)
    apply (rule thin1 [THEN rotate2])
    apply (rule Disj_EH)
     apply (rule Neg_Conj_E)
      apply (auto simp: All2_Eats_E1)   
     apply (rule Ex_I [where x="Var l"], auto intro: Mem_Eats_I2)
      apply (metis Assume Eq_Zero_D rotate3)
     apply (metis Assume EQ_imp_SUBS Neg_D thin1)
    apply (rule Cases [where A = "Var j IN Var l"])
     apply (rule Ex_I [where x="Var l"], auto intro: Mem_Eats_I2)
      apply (rule Ex_I [where x="Var l"], auto intro: Mem_Eats_I2 ContraProve)
      apply (rule Ex_I [where x="Var k"], auto)
      apply (metis Assume Subset_trans OrdP_Mem_imp_Subset thin1)
     apply (rule Ex_I [where x="Var l"], auto intro: Mem_Eats_I2 ContraProve)
     apply (metis ContraProve EQ_imp_SUBS rotate3)
      ― ‹final case›
    apply (rule All2_Eats_E [THEN rotate4], simp_all)
    apply (rule Ex_I [where x="Var j"], auto intro: Mem_Eats_I1)
     apply (rule All2_E [where x = "Var k", THEN rotate3], auto)
     apply (rule Ex_I [where x="Var k"], simp)
     apply (metis Assume NegNeg_I Neg_Disj_I rotate3)
    apply (rule cut_same [where A = "OrdP (Var j)"])
     apply (rule All2_E [where x = "Var j", THEN rotate3], auto)
    apply (rule cut_same [where A = "Var l EQ Var j OR Var l IN Var j"])
     apply (rule OrdP_linear [of _ "Var l" "Var j"], auto intro: Disj_CI)
      apply (metis Assume ContraProve rotate7)
     apply (metis ContraProve [THEN rotate4] EQ_imp_SUBS Subset_trans rotate3)
    apply (blast intro: ContraProve [THEN rotate4] OrdP_Mem_imp_Subset Iff_MP2_same [OF Mem_cong])
    done
qed

lemma OrdP_max_imp:
  assumes j: "atom j  (x)" and k: "atom k  (x,j)"
  shows  "{ OrdP x, Neg (x EQ Zero) }  Ex j (Var j IN x AND (All2 k x (Var k SUBS Var j)))"
proof -
  obtain i::name where i: "atom i  (x,j,k)" 
    by (metis obtain_fresh) 
  have "{}  ((Neg (Var i EQ Zero) AND (All2 j (Var i) (OrdP (Var j)))) IMP 
              (Ex j (Var j IN Var i AND (All2 k (Var i) (Var k SUBS Var j)))))(i::=x)"
    apply (rule Subst [OF OrdP_set_max_lemma])
    using i k apply auto
    done
  hence "{ Neg (x EQ Zero) AND (All2 j x (OrdP (Var j))) } 
          Ex j (Var j IN x AND (All2 k x (Var k SUBS Var j)))"
   using i j k by simp (metis anti_deduction)
  hence "{ All2 j x (OrdP (Var j)), Neg (x EQ Zero) } 
              Ex j (Var j IN x AND (All2 k x (Var k SUBS Var j)))"
    by (rule cut1) (metis Assume Conj_I thin1)
  moreover have "{ OrdP x }  All2 j x (OrdP (Var j))" using j
    by auto (metis Assume Ord_IN_Ord thin1)
  ultimately show ?thesis
   by (metis rcut1)
qed

declare OrdP.simps [simp del]


section ‹Case Analysis and Zero/SUCC Induction›

lemma OrdP_cases_lemma:
  assumes p: "atom p  x" 
  shows  "{ OrdP x, Neg (x EQ Zero) }  Ex p (OrdP (Var p) AND x EQ SUCC (Var p))"
proof -
  obtain j::name and k::name where j: "atom j  (x,p)" and k: "atom k  (x,j,p)" 
    by (metis obtain_fresh) 
  show ?thesis
    apply (rule cut_same [OF OrdP_max_imp [of j x k]]) 
    using p j k apply auto
    apply (rule Ex_I [where x="Var j"], auto)
     apply (metis Assume Ord_IN_Ord thin1)
    apply (rule cut_same [where A = "OrdP (SUCC (Var j))"])
    apply (metis Assume Ord_IN_Ord0 OrdP_SUCC_I rotate2 thin1)
    apply (rule OrdP_linear [where x = x, OF _ Assume], auto intro!: Mem_SUCC_EH)
    apply (metis Mem_not_sym rotate3) 
    apply (rule Mem_non_refl, blast intro: Mem_cong [OF Assume Refl, THEN Iff_MP2_same])
    apply (force intro: thin1 All2_E [where x = "SUCC (Var j)", THEN rotate4])
    done
qed

lemma OrdP_cases_disj:
  assumes p: "atom p  x" 
  shows  "insert (OrdP x) H  x EQ Zero OR Ex p (OrdP (Var p) AND x EQ SUCC (Var p))"
  by (metis Disj_CI Assume cut2 [OF OrdP_cases_lemma [OF p]] Swap thin1)

lemma OrdP_cases_E:
  "insert (x EQ Zero) H  A;
    insert (x EQ SUCC (Var k)) (insert (OrdP (Var k)) H)  A; 
    atom k  (x,A);   C  H. atom k  C
    insert (OrdP x) H  A"
  by (rule cut_same [OF OrdP_cases_disj [of k]]) (auto simp: insert_commute intro: thin1)

lemma OrdInd2_lemma:
  "{ OrdP (Var i), A(i::= Zero), (All i (OrdP (Var i) IMP A IMP (A(i::= SUCC (Var i))))) }  A"
proof -
  obtain j::name and k::name  where atoms: "atom j  (i,A)" "atom k  (i,j,A)" 
    by (metis obtain_fresh) 
  show ?thesis
    apply (rule OrdIndH [where i=i and j=j]) 
    using atoms  apply auto
    apply (rule OrdP_cases_E [where k=k, THEN rotate3])
       apply (rule ContraProve [THEN rotate2]) using Var_Eq_imp_subst_Iff
       apply (metis Assume AssumeH(3) Iff_MP_same) 
      apply (rule Ex_I [where x="Var k"], simp)
      apply (rule Neg_Imp_I, blast)
      apply (rule cut_same [where A = "A(i::=Var k)"])
       apply (rule All2_E [where x = "Var k", THEN rotate5])
         apply (auto intro: Mem_SUCC_I2 Mem_cong [OF Refl, THEN Iff_MP2_same])
    apply (rule ContraProve [THEN rotate5])
    by (metis Assume Iff_MP_left' Var_Eq_subst_Iff thin1)
qed

lemma OrdInd2:
  assumes "H  OrdP (Var i)"
      and "H  A(i::= Zero)"
      and "H  All i (OrdP (Var i) IMP A IMP (A(i::= SUCC (Var i))))"
    shows "H  A"
  by (metis cut3 [OF OrdInd2_lemma] assms)

lemma OrdInd2H:
  assumes "H  A(i::= Zero)"
      and "H  All i (OrdP (Var i) IMP A IMP (A(i::= SUCC (Var i))))"
    shows "insert (OrdP (Var i)) H  A"
  by (metis assms thin1 Assume OrdInd2)


section ‹The predicate HFun_Sigma›

text‹To characterise the concept of a function using only bounded universal quantifiers.›

text‹See the note after the proof of Lemma 2.3.›

definition hfun_sigma where
 "hfun_sigma r  z  r. z'  r. x y x' y'. z = x,y  z' = x',y'  (x=x'  y=y')"

definition hfun_sigma_ord where
 "hfun_sigma_ord r  z  r. z'  r. x y x' y'. z = x,y  z' = x',y'  Ord x  Ord x'  (x=x'  y=y')"

nominal_function HFun_Sigma :: "tm  fm"
  where "atom z  (r,z',x,y,x',y'); atom z'  (r,x,y,x',y'); 
          atom x  (r,y,x',y'); atom y  (r,x',y'); atom x'  (r,y'); atom y'  (r)  
    HFun_Sigma r = 
         All2 z r (All2 z' r (Ex x (Ex y (Ex x' (Ex y'
             (Var z EQ HPair (Var x) (Var y) AND Var z' EQ HPair (Var x') (Var y')
              AND OrdP (Var x) AND OrdP (Var x') AND 
              ((Var x EQ Var x') IMP (Var y EQ Var y'))))))))"
by (auto simp: eqvt_def HFun_Sigma_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)

nominal_termination (eqvt)
  by lexicographic_order

lemma
  shows HFun_Sigma_fresh_iff [simp]: "a  HFun_Sigma r  a  r" (is ?thesis1)
    and eval_fm_HFun_Sigma [simp]:
         "eval_fm e (HFun_Sigma r)  hfun_sigma_ord re" (is ?thesis2)
proof -
  obtain x::name and y::name and z::name and x'::name and y'::name and z'::name
    where "atom z  (r,z',x,y,x',y')"  "atom z'  (r,x,y,x',y')"
          "atom x  (r,y,x',y')"  "atom y  (r,x',y')" 
          "atom x'  (r,y')"  "atom y'  (r)"
    by (metis obtain_fresh) 
  thus ?thesis1 ?thesis2
    by (auto simp: HBall_def hfun_sigma_ord_def, metis+)
qed

lemma HFun_Sigma_subst [simp]: "(HFun_Sigma r)(i::=t) = HFun_Sigma (subst i t r)"
proof -
  obtain x::name and y::name and z::name and x'::name and y'::name and z'::name
    where "atom z  (r,t,i,z',x,y,x',y')" "atom z'  (r,t,i,x,y,x',y')"
          "atom x  (r,t,i,y,x',y')" "atom y  (r,t,i,x',y')" 
          "atom x'  (r,t,i,y')" "atom y'  (r,t,i)"
    by (metis obtain_fresh) 
  thus ?thesis 
    by (auto simp: HFun_Sigma.simps [of z _ z' x y x' y'])
qed

lemma HFun_Sigma_Zero: "H  HFun_Sigma Zero"
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''  (z,z',x,y,x',y')" "atom z  (z',x,y,x',y')" "atom z'  (x,y,x',y')"
      "atom x  (y,x',y')" "atom y  (x',y')" "atom x'  y'" 
    by (metis obtain_fresh) 
  hence "{}  HFun_Sigma Zero"
    by (auto simp: HFun_Sigma.simps [of z _ z' x y x' y'])
  thus ?thesis
    by (metis thin0)
qed

lemma Subset_HFun_Sigma: "{HFun_Sigma s, s' SUBS s}  HFun_Sigma s'"
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''  (z,z',x,y,x',y',s,s')" 
      "atom z  (z',x,y,x',y',s,s')" "atom z'  (x,y,x',y',s,s')"
      "atom x  (y,x',y',s,s')" "atom y  (x',y',s,s')" 
      "atom x'  (y',s,s')" "atom y'  (s,s')" 
    by (metis obtain_fresh) 
  thus ?thesis
    apply (auto simp: HFun_Sigma.simps [of z _ z' x y x' y'])
    apply (rule Ex_I [where x="Var z"], auto)
    apply (blast intro: Subset_D ContraProve)
    apply (rule All_E [where x="Var z'"], auto intro: Subset_D ContraProve)
    done
qed

text‹Captures the property of being a relation, using fewer variables than the full definition›
lemma HFun_Sigma_Mem_imp_HPair:
  assumes "H  HFun_Sigma r" "H  a IN r"
      and xy: "atom x  (y,a,r)" "atom y  (a,r)"
    shows "H  (Ex x (Ex y (a EQ HPair (Var x) (Var y))))"  (is "_  ?concl")
proof -
  obtain x'::name and y'::name and z::name and z'::name
    where atoms: "atom z  (z',x',y',x,y,a,r)" "atom z'  (x',y',x,y,a,r)"
                 "atom x'  (y',x,y,a,r)" "atom y'  (x,y,a,r)" 
    by (metis obtain_fresh) 
  hence "{HFun_Sigma r, a IN r}  ?concl" using xy
    apply (auto simp: HFun_Sigma.simps [of z r z' x y x' y'])
    apply (rule All_E [where x=a], auto)
    apply (rule All_E [where x=a], simp)
    apply (rule Imp_E, blast)
    apply (rule Ex_EH Conj_EH)+ apply simp_all
    apply (rule Ex_I [where x="Var x"], simp)
    apply (rule Ex_I [where x="Var y"], auto)
    done
  thus ?thesis
    by (rule cut2) (rule assms)+ 
qed

    
section ‹The predicate HDomain_Incl›

text ‹This is an internal version of @{term "x  d. y z. z  r  z = x,y"}.›

nominal_function HDomain_Incl :: "tm  tm  fm"
  where "atom x  (r,d,y,z); atom y  (r,d,z); atom z  (r,d) 
    HDomain_Incl r d = All2 x d (Ex y (Ex z (Var z IN r AND Var z EQ HPair (Var x) (Var y))))"
  by (auto simp: eqvt_def HDomain_Incl_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)

nominal_termination (eqvt)
  by lexicographic_order

lemma
  shows HDomain_Incl_fresh_iff [simp]:
      "a  HDomain_Incl r d  a  r  a  d" (is ?thesis1)
  and   eval_fm_HDomain_Incl [simp]:
      "eval_fm e (HDomain_Incl r d)  de  hdomain re" (is ?thesis2)
proof -
  obtain x::name and y::name and z::name 
    where "atom x  (r,d,y,z)" "atom y  (r,d,z)" "atom z  (r,d)"
    by (metis obtain_fresh) 
  thus ?thesis1 ?thesis2
    by (auto simp: HDomain_Incl.simps [of x _ _ y z] hdomain_def)
qed

lemma HDomain_Incl_subst [simp]:
      "(HDomain_Incl r d)(i::=t) = HDomain_Incl (subst i t r) (subst i t d)"
proof -
  obtain x::name and y::name and z::name 
    where "atom x  (r,d,y,z,t,i)"  "atom y  (r,d,z,t,i)" "atom z  (r,d,t,i)"
    by (metis obtain_fresh) 
  thus ?thesis
    by (auto simp: HDomain_Incl.simps [of x _ _ y z])
qed

lemma HDomain_Incl_Subset_lemma: "{ HDomain_Incl r k, k' SUBS k }  HDomain_Incl r k'"
proof -
  obtain x::name and y::name and z::name 
    where "atom x  (r,k,k',y,z)" "atom y  (r,k,k',z)" "atom z  (r,k,k')"
    by (metis obtain_fresh) 
  thus ?thesis
    apply (simp add: HDomain_Incl.simps [of x _ _ y z], auto)
    apply (rule Ex_I [where x = "Var x"], auto intro: ContraProve Subset_D)
    done
qed

lemma HDomain_Incl_Subset: "H  HDomain_Incl r k  H  k' SUBS k  H  HDomain_Incl r k'"
  by (metis HDomain_Incl_Subset_lemma cut2)

lemma HDomain_Incl_Mem_Ord: "H  HDomain_Incl r k  H  k' IN k  H  OrdP k  H  HDomain_Incl r k'"
  by (metis HDomain_Incl_Subset OrdP_Mem_imp_Subset)

lemma HDomain_Incl_Zero [simp]: "H  HDomain_Incl r Zero"
proof -
  obtain x::name and y::name and z::name 
    where "atom x  (r,y,z)" "atom y  (r,z)" "atom z  r"
    by (metis obtain_fresh) 
  hence "{}  HDomain_Incl r Zero"
    by (auto simp: HDomain_Incl.simps [of x _ _ y z])
  thus ?thesis
    by (metis thin0)
qed

lemma HDomain_Incl_Eats: "{ HDomain_Incl r d }  HDomain_Incl (Eats r (HPair d d')) (SUCC d)"
proof -
  obtain x::name and y::name and z::name 
    where x: "atom x  (r,d,d',y,z)" and y: "atom y  (r,d,d',z)" and z: "atom z  (r,d,d')"
    by (metis obtain_fresh) 
  thus ?thesis
    apply (auto simp: HDomain_Incl.simps [of x _ _ y z] intro!: Mem_SUCC_EH)
    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"], auto intro: Mem_Eats_I1)
    apply (rule rotate2 [OF Swap])
    apply (rule Ex_I [where x = d'], auto)
    apply (rule Ex_I [where x = "HPair d d'"], auto intro: Mem_Eats_I2 HPair_cong Sym)
    done
qed

lemma HDomain_Incl_Eats_I: "H  HDomain_Incl r d  H  HDomain_Incl (Eats r (HPair d d')) (SUCC d)"
  by (metis HDomain_Incl_Eats cut1)


section @{term HPair} is Provably Injective›

lemma Doubleton_E:
  assumes "insert (a EQ c) (insert (b EQ d) H)  A"
          "insert (a EQ d) (insert (b EQ c) H)  A"
    shows    "insert ((Eats (Eats Zero b) a) EQ (Eats (Eats Zero d) c)) H  A"
apply (rule Equality_E) using assms
apply (auto intro!: Zero_SubsetE rotate2 [of "a IN b"])
apply (rule_tac [!] rotate3) 
apply (auto intro!: Zero_SubsetE rotate2 [of "a IN b"])
apply (metis Sym_L insert_commute thin1)+
done
  
lemma HFST: "{HPair a b EQ HPair c d}  a EQ c"
  unfolding HPair_def  by (metis Assume Doubleton_E thin1)

lemma b_EQ_d_1: "{a EQ c, a EQ d, b EQ c}  b EQ d"
  by (metis Assume thin1 Sym Trans)

lemma HSND: "{HPair a b EQ HPair c d}  b EQ d"
  unfolding HPair_def
  by (metis  AssumeH(2) Doubleton_E b_EQ_d_1 rotate3 thin2) 

lemma HPair_E [intro!]:
  assumes "insert (a EQ c) (insert (b EQ d) H)  A"
    shows "insert (HPair a b EQ HPair c d) H  A"
  by (metis Conj_E [OF assms] Conj_I [OF HFST HSND] rcut1)

declare HPair_E [THEN rotate2, intro!]
declare HPair_E [THEN rotate3, intro!]
declare HPair_E [THEN rotate4, intro!]
declare HPair_E [THEN rotate5, intro!]
declare HPair_E [THEN rotate6, intro!]
declare HPair_E [THEN rotate7, intro!]
declare HPair_E [THEN rotate8, intro!]

lemma HFun_Sigma_E:
  assumes r: "H  HFun_Sigma r"
      and b: "H  HPair a b IN r"
      and b': "H  HPair a b' IN r"
    shows "H  b EQ b'"
proof -
  obtain x::name and y::name and z::name and x'::name and y'::name and z'::name
    where atoms: "atom z  (r,a,b,b',z',x,y,x',y')"  "atom z'  (r,a,b,b',x,y,x',y')"
       "atom x  (r,a,b,b',y,x',y')"  "atom y  (r,a,b,b',x',y')" 
       "atom x'  (r,a,b,b',y')"  "atom y'  (r,a,b,b')"
    by (metis obtain_fresh) 
  hence d1: "H  All2 z r (All2 z' r (Ex x (Ex y (Ex x' (Ex y'
                  (Var z EQ HPair (Var x) (Var y) AND Var z' EQ HPair (Var x') (Var y')
                   AND OrdP (Var x) AND OrdP (Var x') AND ((Var x EQ Var x') IMP (Var y EQ Var y'))))))))" 
      using r HFun_Sigma.simps [of z r z' x y x' y']
    by simp 
  have d2: "H  All2 z' r (Ex x (Ex y (Ex x' (Ex y'
             (HPair a b EQ HPair (Var x) (Var y) AND Var z' EQ HPair (Var x') (Var y')
                   AND OrdP (Var x) AND OrdP (Var x') AND ((Var x EQ Var x') IMP (Var y EQ Var y')))))))" 
    using All_D [where x = "HPair a b", OF d1]  atoms
    by simp (metis MP_same b)              
  have d4: "H  Ex x (Ex y (Ex x' (Ex y'
             (HPair a b EQ HPair (Var x) (Var y) AND HPair a b' EQ HPair (Var x') (Var y')
               AND OrdP (Var x) AND OrdP (Var x') AND ((Var x EQ Var x') IMP (Var y EQ Var y'))))))"
    using All_D [where x = "HPair a b'", OF d2]  atoms
    by simp (metis MP_same b')              
  have d': "{ Ex x (Ex y (Ex x' (Ex y'
             (HPair a b EQ HPair (Var x) (Var y) AND HPair a b' EQ HPair (Var x') (Var y')
              AND OrdP (Var x) AND OrdP (Var x') AND ((Var x EQ Var x') IMP (Var y EQ Var y')))))) }  b EQ b'" 
     using atoms
     by (auto intro: ContraProve Trans Sym)
  thus ?thesis 
    by (rule cut_thin [OF d4], auto)
qed


section @{term SUCC} is Provably Injective›

lemma SUCC_SUBS_lemma: "{SUCC x SUBS SUCC y}  x SUBS y"
  apply (rule obtain_fresh [where x="(x,y)"]) 
  apply (auto simp: SUCC_def)
  prefer 2  apply (metis Assume Conj_E1 Extensionality Iff_MP_same)
  apply (auto intro!: Subset_I)
  apply (blast intro: Set_MP cut_same [OF Mem_cong [OF Refl Assume, THEN Iff_MP2_same]] 
            Mem_not_sym thin2)
  done

lemma SUCC_SUBS: "insert (SUCC x SUBS SUCC y) H  x SUBS y"
  by (metis Assume SUCC_SUBS_lemma cut1)

lemma SUCC_inject: "insert (SUCC x EQ SUCC y) H  x EQ y"
  by (metis Equality_I EQ_imp_SUBS SUCC_SUBS Sym_L cut1)

lemma SUCC_inject_E [intro!]: "insert (x EQ y) H  A  insert (SUCC x EQ SUCC y) H  A"
  by (metis SUCC_inject cut_same insert_commute thin1)

declare SUCC_inject_E [THEN rotate2, intro!]
declare SUCC_inject_E [THEN rotate3, intro!]
declare SUCC_inject_E [THEN rotate4, intro!]
declare SUCC_inject_E [THEN rotate5, intro!]
declare SUCC_inject_E [THEN rotate6, intro!]
declare SUCC_inject_E [THEN rotate7, intro!]
declare SUCC_inject_E [THEN rotate8, intro!]

lemma OrdP_IN_SUCC_lemma: "{OrdP x, y IN x}  SUCC y IN SUCC x"
  apply (rule OrdP_linear [of _ "SUCC x" "SUCC y"])
      apply (auto intro!: Mem_SUCC_EH  intro: OrdP_SUCC_I Ord_IN_Ord0)
    apply (metis Hyp Mem_SUCC_I1 Mem_not_sym cut_same insertCI)
   apply (metis Assume EQ_imp_SUBS Mem_SUCC_I1 Mem_non_refl Subset_D thin1) 
  apply (blast intro: cut_same [OF Mem_cong [THEN Iff_MP2_same]])
  done

lemma OrdP_IN_SUCC: "H  OrdP x  H  y IN x  H  SUCC y IN SUCC x"
  by (rule cut2 [OF OrdP_IN_SUCC_lemma])

lemma OrdP_IN_SUCC_D_lemma: "{OrdP x, SUCC y IN SUCC x}  y IN x"
  apply (rule OrdP_linear [of _ "x" "y"], auto)
    apply (metis Assume AssumeH(2) Mem_SUCC_Refl OrdP_SUCC_I Ord_IN_Ord)
   apply (metis Assume EQ_imp_SUBS Mem_Eats_EH(2) Mem_SUCC_Refl OrdP_Mem_imp_Subset SUCC_def Subset_D thin1)
  by (meson Assume EQ_imp_SUBS Mem_SUCC_E Mem_SUCC_Refl OrdP_Mem_imp_Subset Subset_D rotate3)

lemma OrdP_IN_SUCC_D: "H  OrdP x  H  SUCC y IN SUCC x  H  y IN x"
  by (rule cut2 [OF OrdP_IN_SUCC_D_lemma])

lemma OrdP_IN_SUCC_Iff: "H  OrdP y  H  SUCC x IN SUCC y IFF x IN y" 
  by (metis Assume Iff_I OrdP_IN_SUCC OrdP_IN_SUCC_D thin1)


section ‹The predicate LstSeqP›

lemma hfun_sigma_ord_iff: "hfun_sigma_ord s  OrdDom s  hfun_sigma s"
  by (auto simp: hfun_sigma_ord_def OrdDom_def hfun_sigma_def HBall_def, metis+)

lemma hfun_sigma_iff: "hfun_sigma r  hfunction r  hrelation r"
  by (auto simp add: HBall_def hfun_sigma_def hfunction_def hrelation_def is_hpair_def, metis+)

lemma Seq_iff: "Seq r d  d  hdomain r  hfun_sigma r"
  by (auto simp: Seq_def hfun_sigma_iff)

lemma LstSeq_iff: "LstSeq s k y  succ k  hdomain s  k,y  s  hfun_sigma_ord s"
  by (auto simp: OrdDom_def LstSeq_def Seq_iff hfun_sigma_ord_iff)

nominal_function LstSeqP :: "tm  tm  tm  fm"
  where
    "LstSeqP s k y = OrdP k AND HDomain_Incl s (SUCC k) AND HFun_Sigma s AND HPair k y IN s"
  by (auto simp: eqvt_def LstSeqP_graph_aux_def)

nominal_termination (eqvt)
  by lexicographic_order

lemma
 shows LstSeqP_fresh_iff [simp]:
      "a  LstSeqP s k y  a  s  a  k  a  y"         (is ?thesis1)
   and eval_fm_LstSeqP [simp]: 
      "eval_fm e (LstSeqP s k y)  LstSeq se ke ye"  (is ?thesis2)
proof -
  show ?thesis1 ?thesis2
    by (auto simp: LstSeq_iff OrdDom_def hfun_sigma_ord_iff)
qed

lemma LstSeqP_subst [simp]:
  "(LstSeqP s k y)(i::=t) = LstSeqP (subst i t s) (subst i t k) (subst i t y)" 
  by (auto simp: fresh_Pair fresh_at_base)

lemma LstSeqP_E: 
  assumes "insert (HDomain_Incl s (SUCC k)) 
            (insert (OrdP k) (insert (HFun_Sigma s)
              (insert (HPair k y IN s) H)))  B" 
    shows "insert (LstSeqP s k y) H  B" 
  using assms by (auto simp: insert_commute)

declare LstSeqP.simps [simp del]

lemma LstSeqP_cong:
  assumes "H  s EQ s'" "H  k EQ k'" "H  y EQ y'" 
  shows "H  LstSeqP s k y IFF LstSeqP s' k' y'"
  by (rule P3_cong [OF _ assms], auto)

lemma LstSeqP_OrdP: "H  LstSeqP r k y  H  OrdP k"
  by (metis Conj_E1 LstSeqP.simps)

lemma LstSeqP_Mem_lemma: "{ LstSeqP r k y, HPair k' z IN r, k' IN k }  LstSeqP r k' z"
  by (auto simp: LstSeqP.simps intro: Ord_IN_Ord OrdP_SUCC_I OrdP_IN_SUCC HDomain_Incl_Mem_Ord)

lemma LstSeqP_Mem: "H  LstSeqP r k y  H  HPair k' z IN r  H  k' IN k  H  LstSeqP r k' z"
  by (rule cut3 [OF LstSeqP_Mem_lemma])

lemma LstSeqP_imp_Mem: "H  LstSeqP s k y  H  HPair k y IN s"
  by (auto simp: LstSeqP.simps) (metis Conj_E2)

lemma LstSeqP_SUCC: "H  LstSeqP r (SUCC d) y  H  HPair d z IN r  H  LstSeqP r d z"
  by (metis LstSeqP_Mem Mem_SUCC_I2 Refl)

lemma LstSeqP_EQ: "H  LstSeqP s k y; H  HPair k y' IN s  H  y EQ y'" 
  by (metis AssumeH(2) HFun_Sigma_E LstSeqP_E cut1 insert_commute)

end