Theory Incompleteness.Sigma

chapter ‹Sigma-Formulas and Theorem 2.5›

theory Sigma
imports Predicates
begin

section‹Ground Terms and Formulas›

definition ground_aux :: "tm ⇒ atom set ⇒ bool"
  where "ground_aux t S ≡ (supp t ⊆ S)"

abbreviation ground :: "tm ⇒ bool"
  where "ground t ≡ ground_aux t {}"

definition ground_fm_aux :: "fm ⇒ atom set ⇒ bool"
  where "ground_fm_aux A S ≡ (supp A ⊆ S)"

abbreviation ground_fm :: "fm ⇒ bool"
  where "ground_fm A ≡ ground_fm_aux A {}"

lemma ground_aux_simps[simp]:
  "ground_aux Zero S = True"
  "ground_aux (Var k) S = (if atom k ∈ S then True else False)"
  "ground_aux (Eats t u) S = (ground_aux t S ∧ ground_aux u S)"
unfolding ground_aux_def
by (simp_all add: supp_at_base)

lemma ground_fm_aux_simps[simp]:
  "ground_fm_aux Fls S = True"
  "ground_fm_aux (t IN u) S = (ground_aux t S ∧ ground_aux u S)"
  "ground_fm_aux (t EQ u) S = (ground_aux t S ∧ ground_aux u S)"
  "ground_fm_aux (A OR B) S = (ground_fm_aux A S ∧ ground_fm_aux B S)"
  "ground_fm_aux (A AND B) S = (ground_fm_aux A S ∧ ground_fm_aux B S)"
  "ground_fm_aux (A IFF B) S = (ground_fm_aux A S ∧ ground_fm_aux B S)"
  "ground_fm_aux (Neg A) S =  (ground_fm_aux A S)"
  "ground_fm_aux (Ex x A) S = (ground_fm_aux A (S ∪ {atom x}))" 
by (auto simp: ground_fm_aux_def ground_aux_def supp_conv_fresh)

lemma ground_fresh[simp]:
  "ground t ⟹ atom i ♯ t"
  "ground_fm A ⟹ atom i ♯ A"
unfolding ground_aux_def ground_fm_aux_def fresh_def
by simp_all


section‹Sigma Formulas›

text‹Section 2 material›

subsection ‹Strict Sigma Formulas›

text‹Definition 2.1›
inductive ss_fm :: "fm ⇒ bool" where
    MemI:  "ss_fm (Var i IN Var j)"
  | DisjI: "ss_fm A ⟹ ss_fm B ⟹ ss_fm (A OR B)"
  | ConjI: "ss_fm A ⟹ ss_fm B ⟹ ss_fm (A AND B)"
  | ExI:   "ss_fm A ⟹ ss_fm (Ex i A)"
  | All2I: "ss_fm A ⟹ atom j ♯ (i,A) ⟹ ss_fm (All2 i (Var j) A)"

equivariance ss_fm

nominal_inductive ss_fm
  avoids ExI: "i" | All2I: "i"
by (simp_all add: fresh_star_def)

declare ss_fm.intros [intro]


definition Sigma_fm :: "fm ⇒ bool"
  where "Sigma_fm A ⟷ (∃B. ss_fm B ∧ supp B ⊆ supp A ∧ {} ⊢ A IFF B)"

lemma Sigma_fm_Iff: "⟦{} ⊢ B IFF A; supp A ⊆ supp B; Sigma_fm A⟧ ⟹ Sigma_fm B"
  by (metis Sigma_fm_def Iff_trans order_trans)

lemma ss_fm_imp_Sigma_fm [intro]: "ss_fm A ⟹ Sigma_fm A"
  by (metis Iff_refl Sigma_fm_def order_refl)

lemma Sigma_fm_Fls [iff]: "Sigma_fm Fls"
  by (rule Sigma_fm_Iff [of _ "Ex i (Var i IN Var i)"]) auto

subsection‹Closure properties for Sigma-formulas›

lemma
  assumes "Sigma_fm A" "Sigma_fm B"  
    shows Sigma_fm_AND [intro!]: "Sigma_fm (A AND B)" 
      and Sigma_fm_OR [intro!]:  "Sigma_fm (A OR B)"
      and Sigma_fm_Ex [intro!]:  "Sigma_fm (Ex i A)"
proof -
  obtain SA SB where "ss_fm SA" "{} ⊢ A IFF SA" "supp SA ⊆ supp A"
                 and "ss_fm SB" "{} ⊢ B IFF SB" "supp SB ⊆ supp B"
    using assms by (auto simp add: Sigma_fm_def)
  then show "Sigma_fm (A AND B)"  "Sigma_fm (A OR B)"  "Sigma_fm (Ex i A)" 
    apply (auto simp: Sigma_fm_def)
    apply (metis ss_fm.ConjI Conj_cong Un_mono supp_Conj)
    apply (metis ss_fm.DisjI Disj_cong Un_mono fm.supp(3))
    apply (rule exI [where x = "Ex i SA"])
    apply (auto intro!: Ex_cong)
    done
qed

lemma Sigma_fm_All2_Var:
  assumes H0: "Sigma_fm A" and ij: "atom j ♯ (i,A)"
  shows "Sigma_fm (All2 i (Var j) A)"
proof -
  obtain SA where SA: "ss_fm SA" "{} ⊢ A IFF SA" "supp SA ⊆ supp A"
    using H0 by (auto simp add: Sigma_fm_def)
  show "Sigma_fm (All2 i (Var j) A)"
    apply (rule Sigma_fm_Iff [of _ "All2 i (Var j) SA"])
    apply (metis All2_cong Refl SA(2) emptyE)
    using SA ij
    apply (auto simp: supp_conv_fresh subset_iff)
    apply (metis ss_fm.All2I fresh_Pair ss_fm_imp_Sigma_fm)
    done
qed

  
section‹Lemma 2.2: Atomic formulas are Sigma-formulas›

lemma Eq_Eats_Iff:
   assumes [unfolded fresh_Pair, simp]: "atom i ♯ (z,x,y)"
   shows "{} ⊢ z EQ Eats x y IFF (All2 i z (Var i IN x OR Var i EQ y)) AND x SUBS z AND y IN z"
proof (rule Iff_I, auto)
  have "{Var i IN z, z EQ Eats x y} ⊢ Var i IN Eats x y"
    by (metis Assume Iff_MP_left Iff_sym Mem_cong Refl)
  then show "{Var i IN z, z EQ Eats x y} ⊢ Var i IN x OR Var i EQ y"
    by (metis Iff_MP_same Mem_Eats_Iff)
next
  show "{z EQ Eats x y} ⊢ x SUBS z"
    by (metis Iff_MP2_same Subset_cong [OF Refl Assume] Subset_Eats_I)
next
  show "{z EQ Eats x y} ⊢ y IN z"
    by (metis Iff_MP2_same Mem_cong Assume Refl Mem_Eats_I2)
next
  show "{x SUBS z, y IN z, All2 i z (Var i IN x OR Var i EQ y)} ⊢ z EQ Eats x y"
       (is "{_, _, ?allHyp} ⊢ _")
    apply (rule Eq_Eats_iff [OF assms, THEN Iff_MP2_same], auto)
    apply (rule Ex_I [where x="Var i"])
    apply (auto intro: Subset_D  Mem_cong [OF Assume Refl, THEN Iff_MP2_same])
    done
qed

lemma Subset_Zero_sf: "Sigma_fm (Var i SUBS Zero)"
proof -
  obtain j::name where j: "atom j ♯ i"
    by (rule obtain_fresh)
  hence Subset_Zero_Iff: "{} ⊢ Var i SUBS Zero IFF (All2 j (Var i) Fls)"
    by (auto intro!: Subset_I [of j] intro: Eq_Zero_D Subset_Zero_D All2_E [THEN rotate2])
  thus ?thesis using j
    by (auto simp: supp_conv_fresh 
             intro!: Sigma_fm_Iff [OF Subset_Zero_Iff] Sigma_fm_All2_Var)
qed

lemma Eq_Zero_sf: "Sigma_fm (Var i EQ Zero)"
proof -
  obtain j::name where "atom j ♯ i"
    by (rule obtain_fresh)
  thus ?thesis
    by (auto simp add: supp_conv_fresh
             intro!: Sigma_fm_Iff [OF _ _ Subset_Zero_sf] Subset_Zero_D EQ_imp_SUBS)
qed

lemma theorem_sf: assumes "{} ⊢ A" shows "Sigma_fm A"
proof -
  obtain i::name and j::name
    where ij: "atom i ♯ (j,A)" "atom j ♯ A"
    by (metis obtain_fresh)
  show ?thesis
    apply (rule Sigma_fm_Iff [where A = "Ex i (Ex j (Var i IN Var j))"])
    using ij
    apply auto
    apply (rule Ex_I [where x=Zero], simp)
    apply (rule Ex_I [where x="Eats Zero Zero"])
    apply (auto intro: Mem_Eats_I2 assms thin0)
    done
qed

text ‹The subset relation›
lemma Var_Subset_sf: "Sigma_fm (Var i SUBS Var j)"
proof -
  obtain k::name where k: "atom (k::name) ♯ (i,j)"
    by (metis obtain_fresh)
  thus ?thesis
  proof (cases "i=j")
    case True thus ?thesis using k
      by (auto intro!: theorem_sf Subset_I [where i=k])
  next
    case False thus ?thesis using k
      by (auto simp: ss_fm_imp_Sigma_fm Subset.simps [of k] ss_fm.intros)
  qed
qed

lemma Zero_Mem_sf: "Sigma_fm (Zero IN Var i)"
proof -
  obtain j::name where "atom j ♯ i"
    by (rule obtain_fresh)
  hence Zero_Mem_Iff: "{} ⊢ Zero IN Var i IFF (Ex j (Var j  EQ Zero AND Var j  IN Var i))"
    by (auto intro: Ex_I [where x = Zero]  Mem_cong [OF Assume Refl, THEN Iff_MP_same])
  show ?thesis 
    by (auto intro!: Sigma_fm_Iff [OF Zero_Mem_Iff] Eq_Zero_sf)
qed

lemma ijk: "i + k < Suc (i + j + k)"
  by arith

lemma All2_term_Iff_fresh: "i≠j ⟹ atom j' ♯ (i,j,A) ⟹
   {} ⊢ (All2 i (Var j) A) IFF Ex j' (Var j EQ Var j' AND All2 i (Var j') A)"
apply auto
apply (rule Ex_I [where x="Var j"], auto)
apply (rule Ex_I [where x="Var i"], auto intro: ContraProve Mem_cong [THEN Iff_MP_same])
done

lemma Sigma_fm_All2_fresh:
  assumes "Sigma_fm A" "i≠j"
    shows "Sigma_fm (All2 i (Var j) A)"
proof -
  obtain j'::name where j': "atom j' ♯ (i,j,A)"
    by (metis obtain_fresh)
  show "Sigma_fm (All2 i (Var j) A)"
    apply (rule Sigma_fm_Iff [OF All2_term_Iff_fresh [OF _ j']])
    using assms j'
    apply (auto simp: supp_conv_fresh Var_Subset_sf
                intro!: Sigma_fm_All2_Var Sigma_fm_Iff [OF Extensionality _ _])
    done
qed

lemma Subset_Eats_sf:
  assumes "⋀j::name. Sigma_fm (Var j IN t)"
      and "⋀k::name. Sigma_fm (Var k EQ u)"
  shows "Sigma_fm (Var i SUBS Eats t u)"
proof -
  obtain k::name where k: "atom k ♯ (t,u,Var i)"
    by (metis obtain_fresh)
  hence "{} ⊢ Var i SUBS Eats t u IFF All2 k (Var i) (Var k IN t OR Var k EQ u)"
    apply (auto simp: fresh_Pair intro: Set_MP Disj_I1 Disj_I2)
    apply (force intro!: Subset_I [where i=k] intro: All2_E' [OF Hyp] Mem_Eats_I1 Mem_Eats_I2)
    done
  thus ?thesis
    apply (rule Sigma_fm_Iff)
    using k
    apply (auto intro!: Sigma_fm_All2_fresh simp add: assms fresh_Pair supp_conv_fresh fresh_at_base)
    done
qed

lemma Eq_Eats_sf:
  assumes "⋀j::name. Sigma_fm (Var j EQ t)"
      and "⋀k::name. Sigma_fm (Var k EQ u)"
  shows "Sigma_fm (Var i EQ Eats t u)"
proof -
  obtain j::name and k::name and l::name
    where atoms: "atom j ♯ (t,u,i)" "atom k ♯ (t,u,i,j)" "atom l ♯ (t,u,i,j,k)"
    by (metis obtain_fresh)
  hence "{} ⊢ Var i EQ Eats t u IFF
              Ex j (Ex k (Var i EQ Eats (Var j) (Var k) AND Var j EQ t AND Var k EQ u))"
    apply auto
    apply (rule Ex_I [where x=t], simp)
    apply (rule Ex_I [where x=u], auto intro: Trans Eats_cong)
    done
  thus ?thesis
    apply (rule Sigma_fm_Iff)
    apply (auto simp: assms supp_at_base)
    apply (rule Sigma_fm_Iff [OF Eq_Eats_Iff [of l]])
    using atoms
    apply (auto simp: supp_conv_fresh fresh_at_base Var_Subset_sf 
                intro!: Sigma_fm_All2_Var Sigma_fm_Iff [OF Extensionality _ _])
    done
qed

lemma Eats_Mem_sf:
  assumes "⋀j::name. Sigma_fm (Var j EQ t)"
      and "⋀k::name. Sigma_fm (Var k EQ u)"
  shows "Sigma_fm (Eats t u IN Var i)"
proof -
  obtain j::name where j: "atom j ♯ (t,u,Var i)"
    by (metis obtain_fresh)
  hence "{} ⊢ Eats t u IN Var i IFF
              Ex j (Var j IN Var i AND Var j EQ Eats t u)"
    apply (auto simp: fresh_Pair intro: Ex_I [where x="Eats t u"])
    apply (metis Assume Mem_cong [OF _ Refl, THEN Iff_MP_same] rotate2)
    done
  thus ?thesis
    by (rule Sigma_fm_Iff) (auto simp: assms supp_conv_fresh Eq_Eats_sf)
qed

lemma Subset_Mem_sf_lemma:
  "size t + size u < n ⟹ Sigma_fm (t SUBS u) ∧ Sigma_fm (t IN u)"
proof (induction n arbitrary: t u rule: less_induct)
  case (less n t u)
  show ?case
  proof
    show "Sigma_fm (t SUBS u)"
      proof (cases t rule: tm.exhaust)
        case Zero thus ?thesis
          by (auto intro: theorem_sf)
      next
        case (Var i) thus ?thesis using less.prems
          apply (cases u rule: tm.exhaust)
          apply (auto simp: Subset_Zero_sf Var_Subset_sf)
          apply (force simp: supp_conv_fresh less.IH 
                       intro: Subset_Eats_sf Sigma_fm_Iff [OF Extensionality])
          done
      next
        case (Eats t1 t2) thus ?thesis using less.IH [OF _ ijk] less.prems
          by (auto intro!: Sigma_fm_Iff [OF Eats_Subset_Iff]  simp: supp_conv_fresh)
             (metis add.commute)
      qed
  next
    show "Sigma_fm (t IN u)"
      proof (cases u rule: tm.exhaust)
        case Zero show ?thesis
          by (rule Sigma_fm_Iff [where A=Fls]) (auto simp: supp_conv_fresh Zero)
      next
        case (Var i) show ?thesis
        proof (cases t rule: tm.exhaust)
          case Zero thus ?thesis using ‹u = Var i›
            by (auto intro: Zero_Mem_sf)
        next
          case (Var j)
          thus ?thesis using ‹u = Var i›
            by auto
        next
          case (Eats t1 t2) thus ?thesis using ‹u = Var i› less.prems
            by (force intro: Eats_Mem_sf Sigma_fm_Iff [OF Extensionality _ _] 
                      simp: supp_conv_fresh less.IH [THEN conjunct1])
        qed
      next
        case (Eats t1 t2) thus ?thesis  using  less.prems
          by (force intro: Sigma_fm_Iff [OF Mem_Eats_Iff] Sigma_fm_Iff [OF Extensionality _ _] 
                    simp: supp_conv_fresh less.IH)
      qed
  qed
qed

lemma Subset_sf [iff]: "Sigma_fm (t SUBS u)"
  by (metis Subset_Mem_sf_lemma [OF lessI])

lemma Mem_sf [iff]: "Sigma_fm (t IN u)"
  by (metis Subset_Mem_sf_lemma [OF lessI])

text ‹The equality relation is a Sigma-Formula›
lemma Equality_sf [iff]: "Sigma_fm (t EQ u)"
  by (auto intro: Sigma_fm_Iff [OF Extensionality] simp: supp_conv_fresh)


section‹Universal Quantification Bounded by an Arbitrary Term›

lemma All2_term_Iff: "atom i ♯ t ⟹ atom j ♯ (i,t,A) ⟹ 
                  {} ⊢ (All2 i t A) IFF Ex j (Var j EQ t AND All2 i (Var j) A)"
apply auto
apply (rule Ex_I [where x=t], auto)
apply (rule Ex_I [where x="Var i"])
apply (auto intro: ContraProve Mem_cong [THEN Iff_MP2_same])
done

lemma Sigma_fm_All2 [intro!]:
  assumes "Sigma_fm A" "atom i ♯ t"
    shows "Sigma_fm (All2 i t A)"
proof -
  obtain j::name where j: "atom j ♯ (i,t,A)"
    by (metis obtain_fresh)
  show "Sigma_fm (All2 i t A)"
    apply (rule Sigma_fm_Iff [OF All2_term_Iff [of i t j]])
    using assms j
    apply (auto simp: supp_conv_fresh Sigma_fm_All2_Var)
    done
qed


section ‹Lemma 2.3: Sequence-related concepts are Sigma-formulas›

lemma OrdP_sf [iff]: "Sigma_fm (OrdP t)"
proof -
  obtain z::name and y::name where "atom z ♯ t" "atom y ♯ (t, z)"
    by (metis obtain_fresh)
  thus ?thesis
    by (auto simp: OrdP.simps)
qed

lemma OrdNotEqP_sf [iff]: "Sigma_fm (OrdNotEqP t u)"
  by (auto simp: OrdNotEqP.simps)

lemma HDomain_Incl_sf [iff]: "Sigma_fm (HDomain_Incl t u)"
proof -
  obtain x::name and y::name and z::name
    where "atom x ♯ (t,u,y,z)" "atom y ♯ (t,u,z)" "atom z ♯ (t,u)"
    by (metis obtain_fresh)
  thus ?thesis
    by auto
qed

lemma HFun_Sigma_Iff:
  assumes "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)"
  shows
  "{} ⊢HFun_Sigma r IFF
         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 NEQ Var x') OR (Var y EQ Var y'))))))))"
  apply (simp add: HFun_Sigma.simps [OF assms])
  apply (rule Iff_refl All_cong Imp_cong Ex_cong)+
  apply (rule Conj_cong [OF Iff_refl])
  apply (rule Conj_cong [OF Iff_refl], auto)
  apply (blast intro: Disj_I1 Neg_D OrdNotEqP_I)
  apply (blast intro: Disj_I2)
  apply (blast intro: OrdNotEqP_E rotate2)
  done

lemma HFun_Sigma_sf [iff]: "Sigma_fm (HFun_Sigma t)"
proof -
  obtain x::name and y::name and z::name and x'::name and y'::name and z'::name
    where atoms: "atom z ♯ (t,z',x,y,x',y')"  "atom z' ♯ (t,x,y,x',y')"
       "atom x ♯ (t,y,x',y')"  "atom y ♯ (t,x',y')"
       "atom x' ♯ (t,y')"  "atom y' ♯ (t)"
    by (metis obtain_fresh)
  show ?thesis
    by (auto intro!: Sigma_fm_Iff [OF HFun_Sigma_Iff [OF atoms]] simp: supp_conv_fresh atoms)
qed

lemma LstSeqP_sf [iff]: "Sigma_fm (LstSeqP t u v)"
  by (auto simp: LstSeqP.simps)

  
section ‹A Key Result: Theorem 2.5›

subsection‹Preparation›
text‹To begin, we require some facts connecting quantification and ground terms.›

lemma obtain_const_tm:  obtains t where "⟦t⟧e = x" "ground t"
proof (induct x rule: hf_induct)
  case 0 thus ?case
    by (metis ground_aux_simps(1) eval_tm.simps(1))
next
  case (hinsert y x) thus ?case
    by (metis ground_aux_simps(3) eval_tm.simps(3))
qed

lemma ex_eval_fm_iff_exists_tm:
  "eval_fm e (Ex k A) ⟷ (∃t. eval_fm e (A(k::=t)) ∧ ground t)"
by (auto simp: eval_subst_fm) (metis obtain_const_tm)

text‹In a negative context, the formulation above is actually weaker than this one.›
lemma ex_eval_fm_iff_exists_tm':
  "eval_fm e (Ex k A) ⟷ (∃t. eval_fm e (A(k::=t)))"
by (auto simp: eval_subst_fm) (metis obtain_const_tm)

text‹A ground term defines a finite set of ground terms, its elements.›
nominal_function elts :: "tm ⇒ tm set" where
   "elts Zero       = {}"
 | "elts (Var k)    = {}"
 | "elts (Eats t u) = insert u (elts t)"
by (auto simp: eqvt_def elts_graph_aux_def) (metis tm.exhaust)

nominal_termination (eqvt)
  by lexicographic_order

lemma eval_fm_All2_Eats:
  "atom i ♯ (t,u) ⟹
   eval_fm e (All2 i (Eats t u) A) ⟷ eval_fm e (A(i::=u)) ∧ eval_fm e (All2 i t A)"
  by (simp only: ex_eval_fm_iff_exists_tm' eval_fm.simps) (auto simp: eval_subst_fm)

text‹The term @{term t} must be ground, since @{term elts} doesn't handle variables.›
lemma eval_fm_All2_Iff_elts:
  "ground t ⟹ eval_fm e (All2 i t A) ⟷ (∀u ∈ elts t. eval_fm e (A(i::=u)))"
proof (induct t rule: tm.induct)
  case Eats
  then show ?case by (simp add: eval_fm_All2_Eats del: eval_fm.simps)
qed auto

lemma prove_elts_imp_prove_All2:
   "ground t ⟹ (⋀u. u ∈ elts t ⟹ {} ⊢ A(i::=u)) ⟹ {} ⊢ All2 i t A"
proof (induct t rule: tm.induct)
  case (Eats t u)
  hence pt: "{} ⊢ All2 i t A" and pu: "{} ⊢ A(i::=u)"
    by auto
  have "{} ⊢ ((Var i IN t) IMP A)(i ::= Var i)"
    by (rule All_D [OF pt])
  hence "{} ⊢ ((Var i IN t) IMP A)"
    by simp
  thus ?case using pu
    by (auto intro: anti_deduction) (metis Iff_MP_same Var_Eq_subst_Iff thin1)
qed auto

subsection‹The base cases: ground atomic formulas›

lemma ground_prove:
   "⟦size t + size u < n; ground t; ground u⟧
    ⟹ (⟦t⟧e ≤ ⟦u⟧e ⟶ {} ⊢ t SUBS u) ∧ (⟦t⟧e ❙∈ ⟦u⟧e ⟶ {} ⊢ t IN u)"
proof (induction n arbitrary: t u rule: less_induct)
  case (less n t u)
  show ?case
  proof
    show "⟦t⟧e ≤ ⟦u⟧e ⟶ {} ⊢ t SUBS u" using less
      by (cases t rule: tm.exhaust) auto
  next
    { fix y t u
      have "⟦y < n; size t + size u < y; ground t; ground u; ⟦t⟧e = ⟦u⟧e⟧
           ⟹ {} ⊢ t EQ u"
        by (metis Equality_I less.IH add.commute order_refl)
    }
    thus "⟦t⟧e ❙∈ ⟦u⟧e ⟶ {} ⊢ t IN u" using less.prems
      by (cases u rule: tm.exhaust) (auto simp: Mem_Eats_I1 Mem_Eats_I2 less.IH)
  qed
qed

lemma 
  assumes "ground t" "ground u"
    shows ground_prove_SUBS: "⟦t⟧e ≤ ⟦u⟧e ⟹ {} ⊢ t SUBS u"
      and ground_prove_IN:   "⟦t⟧e ❙∈ ⟦u⟧e ⟹ {} ⊢ t IN u"
      and ground_prove_EQ:   "⟦t⟧e = ⟦u⟧e ⟹ {} ⊢ t EQ u"
  by (metis Equality_I assms ground_prove [OF lessI] order_refl)+

lemma ground_subst: 
  "ground_aux tm (insert (atom i) S) ⟹ ground t ⟹ ground_aux (subst i t tm) S"
  by (induct tm rule: tm.induct) (auto simp: ground_aux_def)

lemma ground_subst_fm: 
  "ground_fm_aux A (insert (atom i) S) ⟹ ground t ⟹ ground_fm_aux (A(i::=t)) S"
  apply (nominal_induct A avoiding: i arbitrary: S rule: fm.strong_induct)
  apply (auto simp: ground_subst Set.insert_commute)
  done

lemma elts_imp_ground: "u ∈ elts t ⟹ ground_aux t S ⟹ ground_aux u S"
  by (induct t rule: tm.induct) auto


subsection ‹Sigma-Eats Formulas›

inductive se_fm :: "fm ⇒ bool" where
    MemI:  "se_fm (t IN u)"
  | DisjI: "se_fm A ⟹ se_fm B ⟹ se_fm (A OR B)"
  | ConjI: "se_fm A ⟹ se_fm B ⟹ se_fm (A AND B)"
  | ExI:   "se_fm A ⟹ se_fm (Ex i A)"
  | All2I: "se_fm A ⟹ atom i ♯ t ⟹ se_fm (All2 i t A)"

equivariance se_fm

nominal_inductive se_fm
  avoids ExI: "i" | All2I: "i"
by (simp_all add: fresh_star_def)

declare se_fm.intros [intro]

lemma subst_fm_in_se_fm: "se_fm A ⟹ se_fm (A(k::=x))"
  by (nominal_induct avoiding: k x rule: se_fm.strong_induct) (auto)
lemma ground_se_fm_induction:
   "ground_fm α ⟹ size α < n ⟹ se_fm α ⟹ eval_fm e α ⟹ {} ⊢ α"
proof (induction n arbitrary: α rule: less_induct)
  case (less n α)
  show ?case using ‹se_fm α›
  proof (cases rule: se_fm.cases)
    case (MemI t u) thus "{} ⊢ α" using less
      by (auto intro: ground_prove_IN)
  next
    case (DisjI A B) thus "{} ⊢ α" using less
      by (auto intro: Disj_I1 Disj_I2)
  next
    case (ConjI A B) thus "{} ⊢ α" using less
      by auto
  next
    case (ExI A i)
    thus "{} ⊢ α" using less.prems
      apply (auto simp: ex_eval_fm_iff_exists_tm simp del: better_ex_eval_fm)
      apply (auto intro!: Ex_I less.IH subst_fm_in_se_fm ground_subst_fm)
      done
  next
    case (All2I A i t)
    hence t: "ground t" using less.prems
      by (auto simp: ground_aux_def fresh_def)
    hence "(∀u∈elts t. eval_fm e (A(i::=u)))"
      by (metis All2I(1) t eval_fm_All2_Iff_elts less(5))
    thus "{} ⊢ α" using less.prems All2I t
      apply (auto del: Neg_I intro!: prove_elts_imp_prove_All2 less.IH)
      apply (auto intro: subst_fm_in_se_fm ground_subst_fm elts_imp_ground)
      done
  qed
qed

lemma ss_imp_se_fm: "ss_fm A ⟹ se_fm A"
  by (erule ss_fm.induct) auto

lemma se_fm_imp_thm: "⟦se_fm A; ground_fm A; eval_fm e A⟧ ⟹ {} ⊢ A"
  by (metis ground_se_fm_induction lessI)

text‹Theorem 2.5›
theorem Sigma_fm_imp_thm: "⟦Sigma_fm A; ground_fm A; eval_fm e0 A⟧ ⟹ {} ⊢ A"
  by (metis Iff_MP2_same ss_imp_se_fm empty_iff Sigma_fm_def eval_fm_Iff ground_fm_aux_def 
            hfthm_sound se_fm_imp_thm subset_empty)

end