Theory PseudoHoopFilters

```
section‹Filters and Congruences›

theory PseudoHoopFilters
imports PseudoHoops
begin

context pseudo_hoop_algebra
begin
definition
"filters = {F . F ≠ {} ∧ (∀ a b . a ∈ F ∧ b ∈ F ⟶ a * b ∈ F) ∧ (∀ a b . a ∈ F ∧ a ≤ b ⟶ b ∈ F)}"

definition
"properfilters = {F . F ∈ filters ∧ F ≠ UNIV}"

definition
"maximalfilters = {F . F ∈ filters ∧ (∀ A . A ∈ filters ∧ F ⊆ A ⟶ A = F ∨ A = UNIV)}"

definition
"ultrafilters = properfilters ∩ maximalfilters"

lemma filter_i: "F ∈ filters ⟹ a ∈ F ⟹ b ∈ F ⟹ a * b ∈ F"

lemma filter_ii: "F ∈ filters ⟹ a ∈ F ⟹ a ≤ b ⟹ b ∈ F"

lemma filter_iii [simp]: "F ∈ filters ⟹ 1 ∈ F"

lemma filter_left_impl:
"(F ∈ filters) = ((1 ∈ F) ∧ (∀ a b . a ∈ F ∧ a l→ b ∈ F ⟶ b ∈ F))"
apply safe
apply simp
apply (frule_tac a = "a l→ b" and b = a in filter_i)
apply simp
apply simp
apply (rule_tac a = "(a l→ b) * a" in filter_ii)
apply simp
apply simp
apply (simp add: inf_l_def [THEN sym])
apply (subst filters_def)
apply safe
apply (subgoal_tac "a l→ (b l→ a * b) ∈ F")
apply blast
apply (subst left_impl_ded [THEN sym])
apply (subst left_impl_one)
apply safe
apply (subst (asm) left_lesseq)
by blast

lemma filter_right_impl:
"(F ∈ filters) = ((1 ∈ F) ∧ (∀ a b . a ∈ F ∧ a r→ b ∈ F ⟶ b ∈ F))"
apply safe
apply simp
apply (frule_tac a = a and b = "a r→ b" in filter_i)
apply simp
apply simp
apply (rule_tac a = "a * (a r→ b)" in filter_ii)
apply simp
apply simp
apply (simp add: inf_r_def [THEN sym])
apply (subst filters_def)
apply safe
apply (subgoal_tac "b r→ (a r→ a * b) ∈ F")
apply blast
apply (subst right_impl_ded [THEN sym])
apply (subst right_impl_one)
apply safe
apply (subst (asm) right_lesseq)
by blast

lemma [simp]: "A ⊆ filters ⟹ ⋂ A ∈ filters"
apply safe
apply (drule_tac x = "1" in spec)
apply safe
apply (erule notE)
apply (subgoal_tac "x ∈ filters")
apply simp
apply blast
apply (frule rev_subsetD)
apply simp
apply simp
apply (frule rev_subsetD)
apply simp
apply (subgoal_tac "a ∈ X")
apply blast
by blast

definition
"filterof X = ⋂ {F . F ∈ filters ∧ X ⊆ F}"

lemma [simp]: "filterof X ∈ filters"

lemma times_le_mono [simp]: "x ≤ y ⟹ u ≤ v ⟹ x * u ≤ y * v"
apply (rule_tac y = "x * v" in order_trans)

lemma prop_3_2_i:
"filterof X = {a . ∃ n x . x ∈ X *^ n ∧ x ≤ a}"
apply safe
apply (subgoal_tac "{a . ∃ n x . x ∈ X *^ n ∧ x ≤ a} ∈ filters")
apply (drule_tac x = "{a::'a. ∃(n::nat) x::'a. x ∈ X *^ n ∧ x ≤ a}" in spec)
apply safe
apply (rule_tac x = "1::nat" in exI)
apply (rule_tac x = "xa" in exI)
apply (drule drop_assumption)
apply safe
apply (rule_tac x = "1" in exI)
apply (rule_tac x = "0" in exI)
apply (rule_tac x = "1" in exI)
apply simp
apply (rule_tac x = "n + na" in exI)
apply (rule_tac x = "x * xa" in exI)
apply safe
apply blast
apply simp
apply (rule_tac x = "n" in exI)
apply (rule_tac x = "x" in exI)
apply simp
apply safe
apply (rule filter_ii)
apply simp_all
apply (subgoal_tac "∀x . x ∈ X *^ n ⟶ x ∈ xb")
apply simp
apply (induct_tac n)
apply safe
apply (rule filter_i)
apply simp_all
by blast

lemma ultrafilter_union:
"ultrafilters = {F . F ∈ filters ∧ F ≠ UNIV ∧ (∀ x . x ∉ F ⟶ filterof (F ∪ {x}) = UNIV)}"
apply (simp add: ultrafilters_def maximalfilters_def properfilters_def filterof_def)
by auto

lemma filterof_sub: "F ∈ filters ⟹ X ⊆ F ⟹ filterof X ⊆ F"
by blast

lemma filterof_elem [simp]: "x ∈ X ⟹ x ∈  filterof X"
by blast

lemma [simp]: "filterof X ∈ filters"
apply safe
apply (rule_tac x = 1 in exI)
apply (rule_tac x = 0 in exI)
apply (rule_tac x = 1 in exI)
apply auto [1]
apply (rule_tac x = "n + na" in exI)
apply (rule_tac x = "x * xa" in exI)
apply safe
apply auto [1]
apply (rule_tac y = "x * b" in order_trans)
apply (rule mult_left_mono)
apply simp
apply (rule_tac x = n in exI)
apply (rule_tac x = x in exI)
by simp

lemma singleton_power [simp]: "{a} *^ n = {b . b = a ^ n}"
apply (induct_tac n)
apply auto [1]

lemma power_pair: "x ∈ {a, b} *^ n ⟹ ∃ i j . i + j = n ∧ x ≤ a ^ i ∧ x ≤ b ^ j"
apply (subgoal_tac "∀ x . x ∈ {a, b} *^ n ⟶ (∃ i j . i + j = n ∧ x ≤ a ^ i ∧ x ≤ b ^ j)")
apply auto[1]
apply (drule drop_assumption)
apply (induct_tac n)
apply auto [1]
apply safe
apply safe
apply (drule_tac x = y in spec)
apply safe
apply (rule_tac x = "i + 1" in exI)
apply (rule_tac x = "j" in exI)
apply simp
apply (rule_tac y = y in order_trans)
apply simp_all
apply (drule_tac x = y in spec)
apply safe
apply (rule_tac x = "i" in exI)
apply (rule_tac x = "j+1" in exI)
apply simp
apply (rule_tac y = y in order_trans)
by simp_all

lemma filterof_supremum:
"c ∈ supremum {a, b} ⟹ filterof {c} = filterof {a} ∩ filterof {b}"
apply safe
apply (cut_tac X = "{c}" and F = "filterof {a}" in filterof_sub)
apply simp_all
apply safe
apply (rule_tac  a = a in filter_ii)
apply simp_all
apply blast
apply (cut_tac X = "{c}" and F = "filterof {b}" in filterof_sub)
apply simp_all
apply safe
apply (rule_tac  a = b in filter_ii)
apply simp_all
apply blast
apply (subst (asm) prop_3_2_i)
apply simp
apply (subst (asm) prop_3_2_i)
apply simp
apply safe
apply (cut_tac A = "{a, b}" and a = c and b = x and n = "n + na" in  lemma_2_8_ii1)
apply simp
apply (subst prop_3_2_i)
apply simp
apply (rule_tac x = "n + na" in exI)
apply (subgoal_tac "infimum ((λxa::'a. xa r→ x) ` ({a, b} *^ (n + na))) = {1}")
apply simp
apply (subst infimum_unique)
apply (subst infimum_def lower_bound_def)
apply (subst lower_bound_def)
apply safe
apply simp_all
apply (drule power_pair)
apply safe
apply (subst right_residual [THEN sym])
apply simp
apply (case_tac "n ≤ i")
apply (rule_tac y = "a ^ n" in order_trans)
apply (rule_tac y = "a ^ i" in order_trans)
apply simp_all
apply (subgoal_tac "na ≤ j")
apply (rule_tac y = "b ^ na" in order_trans)
apply (rule_tac y = "b ^ j" in order_trans)
by simp_all

definition "d1 a b = (a l→ b) * (b l→ a)"
definition "d2 a b = (a r→ b) * (b r→ a)"

definition "d3 a b = d1 b a"
definition "d4 a b = d2 b a"

lemma [simp]: "(a * b = 1) = (a = 1 ∧ b = 1)"
apply (rule iffI)
apply (rule conjI)
apply (rule order.antisym)
apply simp
apply (rule_tac y = "a*b" in order_trans)
apply simp
apply (drule drop_assumption)
apply simp
apply (rule order.antisym)
apply simp
apply (rule_tac y = "a*b" in order_trans)
apply simp
apply (drule drop_assumption)
apply simp
by simp

lemma lemma_3_5_i_1: "(d1 a b = 1) = (a = b)"
apply (simp add: d1_def left_lesseq [THEN sym])
by auto

lemma lemma_3_5_i_2: "(d2 a b = 1) = (a = b)"
apply (simp add: d2_def right_lesseq [THEN sym])
by auto

lemma lemma_3_5_i_3: "(d3 a b = 1) = (a = b)"
by auto

lemma lemma_3_5_i_4: "(d4 a b = 1) = (a = b)"
by auto

lemma lemma_3_5_ii_1 [simp]: "d1 a a = 1"
apply (subst lemma_3_5_i_1)
by simp

lemma lemma_3_5_ii_2 [simp]: "d2 a a = 1"
apply (subst lemma_3_5_i_2)
by simp

lemma lemma_3_5_ii_3 [simp]: "d3 a a = 1"
apply (subst lemma_3_5_i_3)
by simp

lemma lemma_3_5_ii_4 [simp]: "d4 a a = 1"
apply (subst lemma_3_5_i_4)
by simp

lemma [simp]: "(a l→ 1) = 1"
by (simp add: left_lesseq [THEN sym])

end

context pseudo_hoop_algebra begin

lemma [simp]: "(a r→ 1) = 1"
by simp

lemma lemma_3_5_iii_1 [simp]: "d1 a 1 = a"

lemma lemma_3_5_iii_2 [simp]: "d2 a 1 = a"

lemma lemma_3_5_iii_3 [simp]: "d3 a 1 = a"

lemma lemma_3_5_iii_4 [simp]: "d4 a 1 = a"

lemma lemma_3_5_iv_1: "(d1 b c) * (d1 a b) * (d1 b c) ≤ d1 a c"
apply (subgoal_tac "(b l→ c) * (c l→ b) * ((a l→ b) * (b l→ a)) * ((b l→ c) * (c l→ b)) =
((b l→ c) * (c l→ b) * (a l→ b)) * ((b l→ a) * (b l→ c) * (c l→ b))")
apply simp
apply (rule mult_mono)
apply (rule_tac y = "(b l→ c) * (a l→ b)" in order_trans)
apply (rule mult_right_mono)
apply simp
apply (rule_tac y = "(b l→ a) * (c l→ b)" in order_trans)
apply (rule mult_right_mono)
apply simp

lemma lemma_3_5_iv_2: "(d2 a b) * (d2 b c) * (d2 a b) ≤ d2 a c"
apply (subgoal_tac "(a r→ b) * (b r→ a) * ((b r→ c) * (c r→ b)) * ((a r→ b) * (b r→ a)) =
((a r→ b) * (b r→ a) * (b r→ c)) * ((c r→ b) * (a r→ b) * (b r→ a))")
apply simp
apply (rule mult_mono)
apply (rule_tac y = "(a r→ b) * (b r→ c)" in order_trans)
apply (rule mult_right_mono)
apply simp
apply (rule_tac y = "(c r→ b) * (b r→ a)" in order_trans)
apply (rule mult_right_mono)
apply simp

lemma lemma_3_5_iv_3: "(d3 a b) * (d3 b c) * (d3 a b) ≤ d3 a c"

lemma lemma_3_5_iv_4: "(d4 b c) * (d4 a b) * (d4 b c) ≤ d4 a c"

definition
"cong_r F a b ≡ d1 a b ∈ F"

definition
"cong_l F a b ≡ d2 a b ∈ F"

lemma cong_r_filter: "F ∈ filters ⟹ (cong_r F a b) = (a l→ b ∈ F ∧ b l→ a ∈ F)"
apply safe
apply (rule filter_ii)
apply simp_all
apply simp
apply (rule filter_ii)
apply simp_all
apply simp

lemma cong_r_symmetric: "F ∈ filters ⟹ (cong_r F a b) = (cong_r F b a)"
by blast

lemma cong_r_d3: "F ∈ filters ⟹ (cong_r F a b) = (d3 a b ∈ F)"
apply (subst cong_r_symmetric)

lemma cong_l_filter: "F ∈ filters ⟹ (cong_l F a b) = (a r→ b ∈ F ∧ b r→ a ∈ F)"
apply safe
apply (rule filter_ii)
apply simp_all
apply simp
apply (rule filter_ii)
apply simp_all
apply simp

lemma cong_l_symmetric: "F ∈ filters ⟹ (cong_l F a b) = (cong_l F b a)"
by blast

lemma cong_l_d4: "F ∈ filters ⟹ (cong_l F a b) = (d4 a b ∈ F)"
apply (subst cong_l_symmetric)

lemma cong_r_reflexive: "F ∈ filters ⟹ cong_r F a a"

lemma cong_r_transitive: "F ∈ filters ⟹ cong_r F a b ⟹ cong_r F b c ⟹ cong_r F a c"
apply safe
apply (rule_tac a = "(b l→ c) * (a l→ b)" in filter_ii)
apply simp_all
apply (rule filter_i)
apply simp_all
apply (rule_tac a = "(b l→ a) * (c l→ b)" in filter_ii)
apply simp_all
apply (rule filter_i)
apply simp_all

lemma cong_l_reflexive: "F ∈ filters ⟹ cong_l F a a"

lemma cong_l_transitive: "F ∈ filters ⟹ cong_l F a b ⟹ cong_l F b c ⟹ cong_l F a c"
apply safe
apply (rule_tac a = "(a r→ b) * (b r→ c)" in filter_ii)
apply simp_all
apply (rule filter_i)
apply simp_all
apply (rule_tac a = "(c r→ b) * (b r→ a)" in filter_ii)
apply simp_all
apply (rule filter_i)
apply simp_all

lemma lemma_3_7_i: "F ∈ filters ⟹ F = {a . cong_r F a 1}"

lemma lemma_3_7_ii: "F ∈ filters ⟹ F = {a . cong_l F a 1}"

lemma lemma_3_8_i: "F ∈ filters ⟹ (cong_r F a b) = (∃ x y . x ∈ F ∧ y ∈ F ∧ x * a = y * b)"
apply (subst cong_r_filter)
apply safe
apply (rule_tac x = "a l→ b" in exI)
apply (rule_tac x = "b l→ a" in exI)
apply (subgoal_tac "x ≤ a l→ b")
apply (simp add: left_residual [THEN sym])
apply (subgoal_tac "y ≤ b l→ a")
apply (simp add: left_residual [THEN sym])
apply (subgoal_tac "y * b = x * a")
by simp_all

lemma lemma_3_8_ii: "F ∈ filters ⟹ (cong_l F a b) = (∃ x y . x ∈ F ∧ y ∈ F ∧ a * x = b * y)"
apply (subst cong_l_filter)
apply safe
apply (rule_tac x = "a r→ b" in exI)
apply (rule_tac x = "b r→ a" in exI)
apply (subgoal_tac "x ≤ a r→ b")
apply (simp add: right_residual [THEN sym])
apply (subgoal_tac "y ≤ b r→ a")
apply (simp add: right_residual [THEN sym])
apply (subgoal_tac "b * y = a * x")
by simp_all

lemma lemma_3_9_i: "F ∈ filters ⟹ cong_r F a b  ⟹ cong_r F c d ⟹ (a l→ c ∈ F) = (b l→ d ∈ F)"
apply safe
apply (rule_tac a = "(a l→ d) * (b l→ a)" in filter_ii)
apply (rule_tac a = "((c l→ d) * (a l→ c)) * (b l→ a)" in filter_ii)
apply simp_all
apply (rule mult_right_mono)

apply (rule_tac a = "(b l→ c) * (a l→ b)" in filter_ii)
apply (rule_tac a = "((d l→ c) * (b l→ d)) * (a l→ b)" in filter_ii)
apply simp_all
apply (rule mult_right_mono)

lemma lemma_3_9_ii: "F ∈ filters ⟹ cong_l F a b  ⟹ cong_l F c d ⟹ (a r→ c ∈ F) = (b r→ d ∈ F)"
apply safe
apply (rule_tac a = "(b r→ a) * (a r→ d)" in filter_ii)
apply (rule_tac a = "(b r→ a) * ((a r→ c) * (c r→ d))" in filter_ii)
apply simp_all
apply (rule mult_left_mono)

apply (rule_tac a = "(a r→ b) * (b r→ c)" in filter_ii)
apply (rule_tac a = "(a r→ b) * ((b r→ d) * (d r→ c))" in filter_ii)
apply simp_all
apply (rule mult_left_mono)

definition
"normalfilters = {F . F ∈ filters ∧ (∀ a b . (a l→ b ∈ F) = (a r→ b ∈ F))}"

lemma normalfilter_i:
"H ∈ normalfilters ⟹ a l→ b ∈ H ⟹ a r→ b ∈ H"

lemma normalfilter_ii:
"H ∈ normalfilters ⟹ a r→ b ∈ H ⟹ a l→ b ∈ H"

lemma [simp]: "H ∈ normalfilters ⟹ H ∈ filters"

lemma lemma_3_10_i_ii:
"H ∈ normalfilters ⟹ {a} ** H = H ** {a}"
apply safe
apply simp
apply (rule_tac x = "a l→ a * y" in bexI)
apply (simp add: inf_l_def [THEN sym])
apply (rule order.antisym)
apply simp
apply simp
apply (rule normalfilter_ii)
apply simp_all
apply (rule_tac a = "y" in filter_ii)
apply simp_all
apply (simp add: right_residual [THEN sym])

apply (rule_tac x = "a r→ xa * a" in bexI)
apply (simp add: inf_r_def [THEN sym])
apply (rule order.antisym)
apply simp
apply simp
apply (rule normalfilter_i)
apply simp_all
apply (rule_tac a = "xa" in filter_ii)
apply simp_all
by (simp add: left_residual [THEN sym])

lemma lemma_3_10_ii_iii:
"H ∈ filters ⟹ (∀ a . {a} ** H = H ** {a}) ⟹ cong_r H = cong_l H"
apply (subst fun_eq_iff)
apply (subst fun_eq_iff)
apply safe
apply (subst (asm) lemma_3_8_i)
apply simp_all
apply safe
apply (subst lemma_3_8_ii)
apply simp_all
apply (subgoal_tac "xb * x ∈ {x} ** H")
apply (subgoal_tac "y * xa ∈ {xa} ** H")
apply (drule drop_assumption)
apply (drule drop_assumption)
apply safe
apply (rule_tac x = ya in exI)
apply simp
apply (rule_tac x = yb in exI)
apply simp
apply (drule_tac x = xa in spec)
apply auto[1]
apply (drule_tac x = x in spec)
apply simp
apply (rule_tac x = xb in bexI)
apply simp_all

apply (subst (asm) lemma_3_8_ii)
apply simp_all
apply safe
apply (subst lemma_3_8_i)
apply simp_all
apply (subgoal_tac "x * xb ∈ H ** {x}")
apply (subgoal_tac "xa * y ∈ H ** {xa}")
apply (drule drop_assumption)
apply (drule drop_assumption)
apply safe
apply (rule_tac x = xc in exI)
apply simp
apply (rule_tac x = xd in exI)
apply simp
apply (drule_tac x = xa in spec)
apply auto[1]
apply (drule_tac x = x in spec)
apply (subgoal_tac "x * xb ∈ {x} ** H")
apply simp
apply (subst times_set_def)
by blast

lemma lemma_3_10_i_iii:
"H ∈ normalfilters ⟹ cong_r H = cong_l H"

lemma order_impl_l [simp]: "a ≤ b ⟹ a l→ b = 1"

end

context pseudo_hoop_algebra begin

lemma impl_l_d1: "(a l→ b) = d1 a (a ⊓ b)"
by (simp add: d1_def lemma_2_6_20_a )

lemma impl_r_d2: "(a r→ b) = d2 a (a ⊓ b)"

lemma lemma_3_10_iii_i:
"H ∈ filters ⟹ cong_r H = cong_l H ⟹ H ∈ normalfilters"
apply (unfold normalfilters_def)
apply safe
apply (subgoal_tac  "cong_r H a (a ⊓ b)")
apply simp
apply (subst (asm) cong_l_def)
apply simp
apply (subst cong_r_def)
apply simp
apply (subgoal_tac  "cong_r H a (a ⊓ b)")
apply (subst (asm) cong_r_def)
apply simp
apply simp
apply (subst cong_l_def)
by simp

lemma lemma_3_10_ii_i:
"H ∈ filters ⟹  (∀ a . {a} ** H = H ** {a}) ⟹ H ∈ normalfilters"
apply (rule lemma_3_10_iii_i)
apply simp
apply (rule lemma_3_10_ii_iii)
by simp_all

definition
"allpowers x n = {y . ∃ i. i < n ∧ y = x ^ i}"

lemma times_set_in: "a ∈ A ⟹ b ∈ B ⟹ c = a * b ⟹ c ∈ A ** B"
by auto

lemma power_set_power: "a ∈ A ⟹ a ^ n ∈ A *^ n"
apply (induct_tac n)
apply simp
apply simp
apply (rule_tac a = a and b = "a ^ n" in times_set_in)
by simp_all

lemma normal_filter_union: "H ∈ normalfilters ⟹ (H ∪ {x}) *^ n = (H ** (allpowers x n)) ∪ {x ^ n} "
apply (induct_tac n)
apply safe
apply simp
apply safe
apply safe
apply (subgoal_tac "x * xa ∈ H ** {x}")
apply safe
apply (drule_tac x = "xb" in bspec)
apply simp
apply (drule_tac x = "x ^ (i + 1)" in spec)
apply simp
apply safe
apply (erule notE)
apply (rule_tac x = "i + 1" in exI)
apply simp
apply (erule notE)
apply (simp add: mult.assoc [THEN sym])
apply (drule_tac a = x in lemma_3_10_i_ii)
apply (subgoal_tac "H ** {x} = {x} ** H")
apply simp
apply auto[1]
apply simp
apply (drule_tac x = "xaa" in bspec)
apply simp
apply (drule_tac x = "x ^ n" in bspec)
apply blast
apply simp
apply (drule_tac x = "xaa * xb" in bspec)
apply (drule_tac x = "ya" in bspec)
apply safe
apply (rule_tac x = i in exI)
apply simp
apply simp
apply (subst (asm)  times_set_def)
apply (subst (asm)  times_set_def)
apply simp
apply safe
apply (subst (asm) allpowers_def)
apply (subst (asm) allpowers_def)
apply safe
apply (case_tac "i = 0")
apply simp
apply (rule_tac a = xa and b = 1 in times_set_in)
apply blast
apply safe
apply simp
apply (drule_tac x = 1 in bspec)
apply simp
apply (drule_tac x = 1 in spec)
apply simp
apply (drule_tac x = 0 in spec)
apply auto[1]
apply simp
apply (rule_tac a = xaa and b = "x ^ i" in times_set_in)
apply blast
apply (case_tac "i = n")
apply simp
apply safe
apply (subgoal_tac "x ^ i ∈  H ** {y . ∃i<n. y = x ^ i}")
apply simp
apply (rule_tac a = 1 and b = "x ^ i" in times_set_in)
apply simp
apply simp
apply (rule_tac x = i in exI)
apply simp
apply simp
apply (rule power_set_power)
by simp

lemma lemma_3_11_i: "H ∈ normalfilters ⟹ filterof (H ∪ {x}) = {a . ∃ n h . h ∈ H ∧ h * x ^ n ≤ a}"
apply (subst prop_3_2_i)
apply (subst normal_filter_union)
apply simp_all
apply safe
apply (rule_tac x = n in exI)
apply (rule_tac x = 1 in exI)
apply simp
apply safe
apply (rule_tac x = i in exI)
apply (rule_tac x = xb in exI)
apply simp
apply (rule_tac x = "n + 1" in exI)
apply (rule_tac x = "h * x ^ n" in exI)
apply safe
apply (erule notE)
apply (rule_tac x = h in bexI)
apply (rule_tac x = "x ^ n" in exI)
by auto

lemma lemma_3_11_ii: "H ∈ normalfilters ⟹ filterof (H ∪ {x}) = {a . ∃ n h . h ∈ H ∧ (x ^ n) * h ≤ a}"
apply (subst lemma_3_11_i)
apply simp_all
apply safe
apply (rule_tac x = n in exI)
apply (subgoal_tac "h * x ^ n ∈ {x ^ n} ** H")
apply auto[1]
apply (drule_tac a = "x ^ n" in lemma_3_10_i_ii)
apply simp
apply auto[1]
apply (rule_tac x = n in exI)
apply (subgoal_tac "(x ^ n) * h ∈ H ** {x ^ n}")
apply auto[1]
apply (drule_tac a = "x ^ n" in lemma_3_10_i_ii)
apply (drule_tac sym)
apply simp
by auto

lemma lemma_3_12_i_ii:
"H ∈ normalfilters ⟹ H ∈ ultrafilters ⟹ x ∉ H ⟹ (∃ n . x ^ n l→ a ∈ H)"
apply (subst (asm) ultrafilter_union)
apply clarify
apply (drule_tac x = x in spec)
apply clarify
apply (subst (asm) lemma_3_11_i)
apply assumption
apply (subgoal_tac "a ∈ {a::'a. ∃(n::nat) h::'a. h ∈ H ∧ h * x ^ n ≤ a}")
apply clarify
apply (rule_tac x = n in exI)
apply (rule filter_ii)
by simp_all

lemma lemma_3_12_ii_i:
"H ∈ normalfilters ⟹ H ∈ properfilters ⟹ (∀ x a . x ∉ H ⟶ (∃ n . x ^ n l→ a ∈ H)) ⟹ H ∈ maximalfilters"
apply (subgoal_tac "H ∈ ultrafilters")
apply (subst ultrafilter_union)
apply clarify
apply (subst (asm) properfilters_def)
apply clarify
apply (subst lemma_3_11_i)
apply simp_all
apply safe
apply simp_all
apply (drule_tac x = x in spec)
apply clarify
apply (drule_tac x = xb in spec)
apply clarify
apply (rule_tac x = n in exI)
apply (rule_tac x = "x ^ n l→ xb" in exI)
apply clarify
apply (subst inf_l_def [THEN sym])
by simp

lemma lemma_3_12_i_iii:
"H ∈ normalfilters ⟹ H ∈ ultrafilters ⟹ x ∉ H ⟹ (∃ n . x ^ n r→ a ∈ H)"
apply (subst (asm) ultrafilter_union)
apply clarify
apply (drule_tac x = x in spec)
apply clarify
apply (subst (asm) lemma_3_11_ii)
apply assumption
apply (subgoal_tac "a ∈ {a::'a. ∃(n::nat) h::'a. h ∈ H ∧ (x ^ n) * h ≤ a}")
apply clarify
apply (rule_tac x = n in exI)
apply (rule filter_ii)
by simp_all

lemma lemma_3_12_iii_i:
"H ∈ normalfilters ⟹ H ∈ properfilters ⟹ (∀ x a . x ∉ H ⟶ (∃ n . x ^ n r→ a ∈ H)) ⟹ H ∈ maximalfilters"
apply (subgoal_tac "H ∈ ultrafilters")
apply (subst ultrafilter_union)
apply clarify
apply (subst (asm) properfilters_def)
apply clarify
apply (subst lemma_3_11_ii)
apply simp_all
apply safe
apply simp_all
apply (drule_tac x = x in spec)
apply clarify
apply (drule_tac x = xb in spec)
apply clarify
apply (rule_tac x = n in exI)
apply (rule_tac x = "x ^ n r→ xb" in exI)
apply clarify
apply (subst inf_r_def [THEN sym])
by simp

definition
"cong H = (λ x y . cong_l H x y ∧ cong_r H x y)"

definition
"congruences = {R . equivp R ∧ (∀ a b c d . R a b ∧ R c d ⟶ R (a * c) (b * d) ∧  R (a l→ c) (b l→ d) ∧  R (a r→ c) (b r→ d))}"

lemma cong_l: "H ∈ normalfilters ⟹ cong H = cong_l H"

lemma cong_r: "H ∈ normalfilters ⟹ cong H = cong_r H"

lemma cong_equiv: "H ∈ normalfilters ⟹ equivp (cong H)"
apply (simp add: equivp_reflp_symp_transp reflp_def refl_on_def cong_l_reflexive cong_l_symmetric symp_def sym_def transp_def trans_def)
apply safe
apply (rule cong_l_transitive)
by simp_all

lemma cong_trans: "H ∈ normalfilters ⟹ cong H x y ⟹ cong H y z ⟹ cong H x z"
apply (drule cong_equiv)
apply (drule equivp_transp)
by simp_all

lemma lemma_3_13 [simp]:
"H ∈ normalfilters ⟹ cong H ∈ congruences"
apply (subst congruences_def)
apply safe
apply (rule_tac y = "b * c" in cong_trans)
apply simp_all
apply safe
apply (rule_tac x = x in exI)
apply simp
apply (rule_tac x = y in exI)
apply (simp add: mult.assoc [THEN sym])
apply safe
apply (rule_tac x = xa in exI)
apply simp
apply (rule_tac x = ya in exI)
apply (rule_tac y = "a l→ d" in cong_trans)
apply simp
apply safe
apply (rule_tac a = "c l→ d" in filter_ii)
apply simp_all
apply (subst left_residual [THEN sym])
apply (rule_tac a = "d l→ c" in filter_ii)
apply simp_all
apply (subst left_residual [THEN sym])
apply (subst cong_l)
apply simp
apply (simp add: cong_r cong_r_filter cong_l_filter)
apply safe
apply (rule_tac a = "b l→ a" in filter_ii)
apply simp_all
apply (subst right_residual [THEN sym])
apply (rule_tac a = "a l→ b" in filter_ii)
apply simp_all
apply (subst right_residual [THEN sym])

apply (rule_tac y = "a r→ d" in cong_trans)
apply simp
apply safe
apply (rule_tac a = "c r→ d" in filter_ii)
apply simp_all
apply (subst right_residual [THEN sym])
apply (rule_tac a = "d r→ c" in filter_ii)
apply simp_all
apply (subst right_residual [THEN sym])

apply (subst cong_r)
apply simp
apply (simp add: cong_l cong_l_filter cong_r_filter)
apply safe
apply (rule_tac a = "b r→ a" in filter_ii)
apply simp_all
apply (subst left_residual [THEN sym])
apply (rule_tac a = "a r→ b" in filter_ii)
apply simp_all
apply (subst left_residual [THEN sym])

lemma cong_times: "R ∈ congruences ⟹ R a b ⟹ R c d ⟹ R (a * c) (b * d)"

lemma cong_impl_l: "R ∈ congruences ⟹ R a b ⟹ R c d ⟹ R (a l→ c) (b l→ d)"

lemma cong_impl_r: "R ∈ congruences ⟹ R a b ⟹ R c d ⟹ R (a r→ c) (b r→ d)"

lemma cong_refl [simp]: "R ∈ congruences ⟹ R a a"

lemma cong_trans_a: "R ∈ congruences ⟹ R a b ⟹ R b c ⟹ R a c"
apply (rule_tac y = b in equivp_transp)
by simp_all

lemma cong_sym: "R ∈ congruences ⟹ R a b ⟹ R b a"

definition
"normalfilter R = {a . R a 1}"

lemma lemma_3_14 [simp]:
"R ∈ congruences ⟹ (normalfilter R) ∈ normalfilters"
apply (unfold normalfilters_def)
apply safe
apply safe
apply (drule_tac x = 1 in spec)
apply (drule_tac a = a and c = b and b = 1 and d = 1 and R = R in cong_times)
apply simp_all
apply (cut_tac R = R and a = a and b = 1 and c = b and d = b in cong_impl_l)
apply simp_all
apply (cut_tac R = R and a = "a l→ b" and b = 1 and c = a and d = a in cong_times)
apply simp_all
apply (simp add: inf_l_def [THEN sym])
apply (cut_tac R = R and a = a and b = "a ⊓ b" and c = b and d = b in cong_impl_r)
apply simp_all
apply (cut_tac R = R and c = "a r→ b" and d = 1 and a = a and b = a in cong_times)
apply simp_all
apply (simp add: inf_r_def [THEN sym])
apply (cut_tac R = R and a = a and b = "a ⊓ b" and c = b and d = b in cong_impl_l)
apply simp_all

lemma lemma_3_15_i:
"H ∈ normalfilters ⟹ normalfilter (cong H) = H"
by (simp add: normalfilter_def cong_r cong_r_filter)

lemma lemma_3_15_ii:
"R ∈ congruences ⟹ cong (normalfilter R) = R"
apply (simp add: fun_eq_iff cong_r cong_r_filter)
apply safe
apply (cut_tac R = R and a = "x l→ xa" and b = 1 and c = x and d = x in cong_times)
apply simp_all
apply (cut_tac R = R and a = "xa l→ x" and b = 1 and c = xa and d = xa in cong_times)
apply simp_all
apply (simp add: inf_l_def [THEN sym])
apply (rule_tac b = "x ⊓ xa" in cong_trans_a)
apply simp_all
apply (subst cong_sym)
apply simp_all
apply (subst inf.commute)
apply simp_all
apply (cut_tac R = R and a = x and b = xa and c = xa and d = xa in cong_impl_l)
apply simp_all
apply (cut_tac R = R and a = xa and b = xa and c = x and d = xa in cong_impl_l)
by simp_all

lemma lemma_3_15_iii: "H1 ∈ normalfilters ⟹ H2 ∈ normalfilters ⟹ (H1 ⊆ H2) = (cong H1 ≤ cong H2)"
apply safe
apply blast
apply (subgoal_tac "cong H2 x 1")
apply (subgoal_tac "cong H1 x 1")
apply blast

definition
"p x y z = ((x l→ y) r→ z) ⊓ ((z l→ y) r→ x)"

lemma lemma_3_16_i: "p x x y = y ∧ p x y y = x"
apply safe
apply (rule order.antisym)
apply (rule order.antisym)

definition "M x y z = ((y l→ x) r→ x) ⊓ ((z l→ y) r→ y) ⊓ ((x l→ z) r→ z)"

lemma "M x x y = x ∧ M x y x = x ∧ M y x x = x"