# Theory 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

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"

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
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)
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"

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

```