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

end

```