# Theory PseudoHoopFilters

Up to index of Isabelle/HOL/LatticeProperties/PseudoHoops

theory PseudoHoopFilters
imports PseudoHoops
`header{* Filters and Congruences *}theory PseudoHoopFiltersimports PseudoHoopsbegincontext pseudo_hoop_algebrabegindefinition  "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"  by (simp add: filters_def)lemma filter_ii: "F ∈ filters ==> a ∈ F ==> a ≤ b ==> b ∈ F" apply (simp add: filters_def) by blastlemma filter_iii [simp]: "F ∈ filters ==> 1 ∈ F" apply (simp add: filters_def) by autolemma 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 blastlemma 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 blastlemma [simp]: "A ⊆ filters ==> \<Inter> A ∈ filters"  apply (simp add: filters_def)  apply safe  apply (simp add: Inter_eq)  apply (drule_tac x = "1" in spec)  apply safe  apply (erule notE)  apply (subgoal_tac "x ∈ filters")  apply simp  apply (simp add: filters_def)  apply blast  apply (frule set_rev_mp)  apply simp  apply simp  apply (frule set_rev_mp)  apply simp  apply (subgoal_tac "a ∈ X")  apply blast  by blastdefinition  "filterof X = \<Inter> {F . F ∈ filters ∧ X ⊆ F}"lemma [simp]: "filterof X ∈ filters"  apply (simp add: filterof_def)  apply (subgoal_tac "{F ∈ filters. X ⊆ F} ⊆ filters")  apply simp  by blastlemma times_le_mono [simp]: "x ≤ y ==> u ≤ v ==> x * u ≤ y * v"  apply (rule_tac y = "x * v" in order_trans)  by (simp_all add: mult_left_mono mult_right_mono)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 (simp add: filterof_def)  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 (simp add: times_set_def)  apply (drule drop_assumption)  apply (simp add: filters_def)  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 (simp add: power_set_add times_set_def)  apply blast  apply simp  apply (rule_tac x = "n" in exI)  apply (rule_tac x = "x" in exI)  apply simp  apply (simp add: filterof_def)  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 (simp add: power_set_0)  apply (simp add: power_set_Suc times_set_def)  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 autolemma filterof_sub: "F ∈ filters ==> X ⊆ F ==> filterof X ⊆ F"  apply (simp add: filterof_def)  by blastlemma filterof_elem [simp]: "x ∈ X ==> x ∈  filterof X"  apply (simp add: filterof_def)  by blastlemma [simp]: "filterof X ∈ filters"  apply (simp add: filters_def  prop_3_2_i)  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 (unfold power_set_add)  apply (simp add: times_set_def)  apply auto [1]  apply (rule_tac y = "x * b" in order_trans)  apply (rule mult_left_mono)  apply simp  apply (simp add: mult_right_mono)  apply (rule_tac x = n in exI)  apply (rule_tac x = x in exI)  by simplemma singleton_power [simp]: "{a} *^ n = {b . b = a ^ n}"  apply (induct_tac n)  apply auto [1]  by (simp add: times_set_def)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 (simp add: times_set_def)  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_alllemma 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 (simp add: supremum_def upper_bound_def)  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 (simp add: supremum_def upper_bound_def)  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 (simp add: right_lesseq)  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_alldefinition "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 antisym)  apply simp  apply (rule_tac y = "a*b" in order_trans)  apply simp  apply (drule drop_assumption)  apply simp  apply (rule antisym)  apply simp  apply (rule_tac y = "a*b" in order_trans)  apply simp  apply (drule drop_assumption)  apply simp  by simplemma lemma_3_5_i_1: "(d1 a b = 1) = (a = b)"  apply (simp add: d1_def left_lesseq [THEN sym])  by autolemma lemma_3_5_i_2: "(d2 a b = 1) = (a = b)"  apply (simp add: d2_def right_lesseq [THEN sym])  by autolemma lemma_3_5_i_3: "(d3 a b = 1) = (a = b)"  apply (simp add: d3_def lemma_3_5_i_1)  by autolemma lemma_3_5_i_4: "(d4 a b = 1) = (a = b)"  apply (simp add: d4_def lemma_3_5_i_2)  by autolemma lemma_3_5_ii_1 [simp]: "d1 a a = 1"  apply (subst lemma_3_5_i_1)  by simplemma lemma_3_5_ii_2 [simp]: "d2 a a = 1"  apply (subst lemma_3_5_i_2)  by simplemma lemma_3_5_ii_3 [simp]: "d3 a a = 1"  apply (subst lemma_3_5_i_3)  by simplemma lemma_3_5_ii_4 [simp]: "d4 a a = 1"  apply (subst lemma_3_5_i_4)  by simplemma [simp]: "(a l-> 1) = 1"  by (simp add: left_lesseq [THEN sym])endcontext pseudo_hoop_algebra beginlemma [simp]: "(a r-> 1) = 1"  by simplemma lemma_3_5_iii_1 [simp]: "d1 a 1 = a"  by (simp add: d1_def)lemma lemma_3_5_iii_2 [simp]: "d2 a 1 = a"  by (simp add: d2_def)lemma lemma_3_5_iii_3 [simp]: "d3 a 1 = a"  by (simp add: d3_def d1_def)lemma lemma_3_5_iii_4 [simp]: "d4 a 1 = a"  by (simp add: d4_def d2_def)lemma lemma_3_5_iv_1: "(d1 b c) * (d1 a b) * (d1 b c) ≤ d1 a c"  apply (simp add: d1_def)  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 (simp add: lemma_2_5_14)  apply (rule_tac y = "(b l-> a) * (c l-> b)" in order_trans)  apply (rule mult_right_mono)  apply simp  apply (simp add: lemma_2_5_14)  by (simp add: mult_assoc)lemma lemma_3_5_iv_2: "(d2 a b) * (d2 b c) * (d2 a b) ≤ d2 a c"  apply (simp add: d2_def)  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 (simp add: lemma_2_5_15)  apply (rule_tac y = "(c r-> b) * (b r-> a)" in order_trans)  apply (rule mult_right_mono)  apply simp  apply (simp add: lemma_2_5_15)  by (simp add: mult_assoc)lemma lemma_3_5_iv_3: "(d3 a b) * (d3 b c) * (d3 a b) ≤ d3 a c"  by (simp add: d3_def lemma_3_5_iv_1)lemma lemma_3_5_iv_4: "(d4 b c) * (d4 a b) * (d4 b c) ≤ d4 a c"  by (simp add: d4_def lemma_3_5_iv_2)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 (simp add: cong_r_def d1_def)  apply safe  apply (rule filter_ii)  apply simp_all  apply simp  apply (rule filter_ii)  apply simp_all  apply simp  by (simp add: filter_i)lemma cong_r_symmetric: "F ∈ filters ==> (cong_r F a b) = (cong_r F b a)"  apply (simp add: cong_r_filter)  by blastlemma cong_r_d3: "F ∈ filters ==> (cong_r F a b) = (d3 a b ∈ F)"  apply (simp add: d3_def)  apply (subst cong_r_symmetric)  by (simp_all add: cong_r_def)lemma cong_l_filter: "F ∈ filters ==> (cong_l F a b) = (a r-> b ∈ F ∧ b r-> a ∈ F)"  apply (simp add: cong_l_def d2_def)  apply safe  apply (rule filter_ii)  apply simp_all  apply simp  apply (rule filter_ii)  apply simp_all  apply simp  by (simp add: filter_i)lemma cong_l_symmetric: "F ∈ filters ==> (cong_l F a b) = (cong_l F b a)"  apply (simp add: cong_l_filter)  by blastlemma cong_l_d4: "F ∈ filters ==> (cong_l F a b) = (d4 a b ∈ F)"  apply (simp add: d4_def)  apply (subst cong_l_symmetric)  by (simp_all add: cong_l_def)lemma cong_r_reflexive: "F ∈ filters ==> cong_r F a a"  by (simp add: cong_r_def)lemma cong_r_transitive: "F ∈ filters ==> cong_r F a b ==> cong_r F b c ==> cong_r F a c"  apply (simp add: cong_r_filter)  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 (simp add: lemma_2_5_14)  apply (rule_tac a = "(b l-> a) * (c l-> b)" in filter_ii)  apply simp_all  apply (rule filter_i)  apply simp_all  by (simp add: lemma_2_5_14)lemma cong_l_reflexive: "F ∈ filters ==> cong_l F a a"  by (simp add: cong_l_def)lemma cong_l_transitive: "F ∈ filters ==> cong_l F a b ==> cong_l F b c ==> cong_l F a c"  apply (simp add: cong_l_filter)  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 (simp add: lemma_2_5_15)  apply (rule_tac a = "(c r-> b) * (b r-> a)" in filter_ii)  apply simp_all  apply (rule filter_i)  apply simp_all  by (simp add: lemma_2_5_15)lemma lemma_3_7_i: "F ∈ filters ==> F = {a . cong_r F a 1}"  by (simp add: cong_r_def)lemma lemma_3_7_ii: "F ∈ filters ==> F = {a . cong_l F a 1}"  by (simp add: cong_l_def)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 (simp add: left_impl_times)  apply (subgoal_tac "x ≤ a l-> b")  apply (simp add: filter_ii)  apply (simp add: left_residual [THEN sym])  apply (subgoal_tac "y ≤ b l-> a")  apply (simp add: filter_ii)  apply (simp add: left_residual [THEN sym])  apply (subgoal_tac "y * b = x * a")  by simp_alllemma 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 (simp add: right_impl_times)  apply (subgoal_tac "x ≤ a r-> b")  apply (simp add: filter_ii)  apply (simp add: right_residual [THEN sym])  apply (subgoal_tac "y ≤ b r-> a")  apply (simp add: filter_ii)  apply (simp add: right_residual [THEN sym])  apply (subgoal_tac "b * y = a * x")  by simp_alllemma 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 (simp add: cong_r_filter)  apply safe  apply (rule_tac a = "(a l-> d) * (b l-> a)" in filter_ii)  apply (simp_all add: lemma_2_5_14)  apply (rule_tac a = "((c l-> d) * (a l-> c)) * (b l-> a)" in filter_ii)  apply simp_all  apply (simp add: filter_i)  apply (rule mult_right_mono)  apply (simp_all add: lemma_2_5_14)  apply (rule_tac a = "(b l-> c) * (a l-> b)" in filter_ii)  apply (simp_all add: lemma_2_5_14)  apply (rule_tac a = "((d l-> c) * (b l-> d)) * (a l-> b)" in filter_ii)  apply simp_all  apply (simp add: filter_i)  apply (rule mult_right_mono)  by (simp_all add: lemma_2_5_14)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 (simp add: cong_l_filter)  apply safe  apply (rule_tac a = "(b r-> a) * (a r-> d)" in filter_ii)  apply (simp_all add: lemma_2_5_15)  apply (rule_tac a = "(b r-> a) * ((a r-> c) * (c r-> d))" in filter_ii)  apply simp_all  apply (simp add: filter_i)  apply (rule mult_left_mono)  apply (simp_all add: lemma_2_5_15)  apply (rule_tac a = "(a r-> b) * (b r-> c)" in filter_ii)  apply (simp_all add: lemma_2_5_15)  apply (rule_tac a = "(a r-> b) * ((b r-> d) * (d r-> c))" in filter_ii)  apply simp_all  apply (simp add: filter_i)  apply (rule mult_left_mono)  by (simp_all add: lemma_2_5_15)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"  by (simp add: normalfilters_def)lemma normalfilter_ii:  "H ∈ normalfilters ==> a r-> b ∈ H ==> a l-> b ∈ H"  by (simp add: normalfilters_def)lemma [simp]: "H ∈ normalfilters ==> H ∈ filters"   by (simp add: normalfilters_def)lemma lemma_3_10_i_ii:  "H ∈ normalfilters ==> {a} ** H = H ** {a}"  apply (simp add: times_set_def)  apply safe  apply simp  apply (rule_tac x = "a l-> a * y" in bexI)  apply (simp add: inf_l_def [THEN sym])  apply (rule 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 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 (simp add: times_set_def)  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 (simp add: times_set_def)  apply auto[1]  apply (drule_tac x = x in spec)  apply simp  apply (simp add: times_set_def)  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 (simp add: times_set_def)  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 (simp add: times_set_def)  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 blastlemma lemma_3_10_i_iii:   "H ∈ normalfilters ==> cong_r H = cong_l H"  by (simp add: lemma_3_10_i_ii lemma_3_10_ii_iii)lemma order_impl_l [simp]: "a ≤ b ==> a l-> b = 1"  by (simp add: left_lesseq)endcontext pseudo_hoop_algebra beginlemma impl_l_d1: "(a l-> b) = d1 a (a \<sqinter> b)"  by (simp add: d1_def lemma_2_6_20_a ) lemma impl_r_d2: "(a r-> b) = d2 a (a \<sqinter> b)"  by (simp add: d2_def lemma_2_6_21_a)lemma lemma_3_10_iii_i:  "H ∈ filters ==> cong_r H = cong_l H ==> H ∈ normalfilters"  apply (unfold normalfilters_def)  apply (simp add: impl_l_d1 impl_r_d2)  apply safe  apply (subgoal_tac  "cong_r H a (a \<sqinter> 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 \<sqinter> b)")  apply (subst (asm) cong_r_def)  apply simp  apply simp  apply (subst cong_l_def)  by simplemma 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_alldefinition  "allpowers x n = {y . ∃ i. i < n ∧ y = x ^ i}"lemma times_set_in: "a ∈ A ==> b ∈ B ==> c = a * b ==> c ∈ A ** B"   apply (simp add: times_set_def)  by autolemma 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_alllemma normal_filter_union: "H ∈ normalfilters ==> (H ∪ {x}) *^ n = (H ** (allpowers x n)) ∪ {x ^ n} "  apply (induct_tac n)  apply (simp add: times_set_def allpowers_def)  apply safe  apply simp  apply (simp add:  times_set_def)  apply safe  apply (simp add:  allpowers_def)  apply safe  apply (subgoal_tac "x * xa ∈ H ** {x}")  apply (simp add: times_set_def)  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 (simp add: times_set_def)  apply auto[1]  apply simp  apply (drule_tac x = "xaa" in bspec)  apply simp  apply (drule_tac x = "x ^ n" in bspec)  apply (simp add: allpowers_def)  apply blast  apply simp  apply (drule_tac x = "xaa * xb" in bspec)  apply (simp add: filter_i)  apply (simp add: mult_assoc)  apply (drule_tac x = "ya" in bspec)  apply (simp add: allpowers_def)  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 (simp add: allpowers_def times_set_def)  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 (simp add: allpowers_def)  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 simplemma 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 (simp_all add: allpowers_def times_set_def)  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 autolemma 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 (simp add: times_set_def)  apply auto[1]  apply (drule_tac a = "x ^ n" in lemma_3_10_i_ii)  apply simp  apply (simp add: times_set_def)  apply auto[1]  apply (rule_tac x = n in exI)  apply (subgoal_tac "(x ^ n) * h ∈ H ** {x ^ n}")  apply (simp add: times_set_def)  apply auto[1]  apply (drule_tac a = "x ^ n" in lemma_3_10_i_ii)  apply (drule_tac sym)  apply simp  apply (simp add: times_set_def)  by autolemma 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 (simp add: left_residual)  apply (rule filter_ii)  by simp_alllemma 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 (simp add: ultrafilters_def)  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 simplemma 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 (simp add: right_residual)  apply (rule filter_ii)  by simp_alllemma 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 (simp add: ultrafilters_def)  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 simpdefinition  "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"  by (simp add: cong_def lemma_3_10_i_iii)  lemma cong_r: "H ∈ normalfilters ==> cong H = cong_r H"  by (simp add: cong_def lemma_3_10_i_iii)lemma cong_equiv: "H ∈ normalfilters ==> equivp (cong H)"  apply (simp add: cong_l)  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_alllemma lemma_3_13 [simp]:   "H ∈ normalfilters ==> cong H ∈ congruences"  apply (subst congruences_def)  apply safe  apply (simp add: cong_equiv)  apply (rule_tac y = "b * c" in cong_trans)  apply simp_all  apply (simp add: cong_r lemma_3_8_i)  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 (simp add: cong_l lemma_3_8_ii)  apply safe  apply (rule_tac x = xa in exI)  apply simp  apply (rule_tac x = ya in exI)  apply (simp add: mult_assoc)  apply (rule_tac y = "a l-> d" in cong_trans)  apply simp  apply (simp add: cong_r cong_r_filter)  apply safe  apply (rule_tac a = "c l-> d" in filter_ii)  apply simp_all  apply (subst left_residual [THEN sym])  apply (simp add: lemma_2_5_14)  apply (rule_tac a = "d l-> c" in filter_ii)  apply simp_all  apply (subst left_residual [THEN sym])  apply (simp add: lemma_2_5_14)  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 (simp add: lemma_2_5_14)  apply (rule_tac a = "a l-> b" in filter_ii)  apply simp_all  apply (subst right_residual [THEN sym])  apply (simp add: lemma_2_5_14)  apply (rule_tac y = "a r-> d" in cong_trans)  apply simp  apply (simp add: cong_l cong_l_filter)  apply safe  apply (rule_tac a = "c r-> d" in filter_ii)  apply simp_all  apply (subst right_residual [THEN sym])  apply (simp add: lemma_2_5_15)  apply (rule_tac a = "d r-> c" in filter_ii)  apply simp_all  apply (subst right_residual [THEN sym])  apply (simp add: lemma_2_5_15)  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 (simp add: lemma_2_5_15)  apply (rule_tac a = "a r-> b" in filter_ii)  apply simp_all  apply (subst left_residual [THEN sym])  by (simp add: lemma_2_5_15)lemma cong_times: "R ∈ congruences ==> R a b ==> R c d ==> R (a * c) (b * d)"  by (simp add: congruences_def)lemma cong_impl_l: "R ∈ congruences ==> R a b ==> R c d ==> R (a l-> c) (b l-> d)"  by (simp add: congruences_def)lemma cong_impl_r: "R ∈ congruences ==> R a b ==> R c d ==> R (a r-> c) (b r-> d)"  by (simp add: congruences_def)lemma cong_refl [simp]: "R ∈ congruences ==> R a a"  by (simp add: congruences_def equivp_reflp)lemma cong_trans_a: "R ∈ congruences ==> R a b ==> R b c ==> R a c"  apply (simp add: congruences_def)  apply (rule_tac y = b in equivp_transp)  by simp_alllemma cong_sym: "R ∈ congruences ==> R a b ==> R b a"  by (simp add: congruences_def equivp_symp)definition  "normalfilter R = {a . R a 1}"lemma lemma_3_14 [simp]:  "R ∈ congruences ==> (normalfilter R) ∈ normalfilters"  apply (unfold normalfilters_def)  apply safe  apply (simp add: filters_def)  apply safe  apply (simp add: normalfilter_def)  apply (drule_tac x = 1 in spec)  apply (simp add: congruences_def  equivp_reflp)  apply (simp add: normalfilter_def)  apply (drule_tac a = a and c = b and b = 1 and d = 1 and R = R in cong_times)  apply simp_all  apply (simp add: normalfilter_def)  apply (simp add: left_lesseq)  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 (simp add: cong_sym)  apply (simp_all add: normalfilter_def)  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 \<sqinter> b" and c = b and d = b in cong_impl_r)  apply simp_all  apply (simp add: cong_sym)  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 \<sqinter> b" and c = b and d = b in cong_impl_l)  apply simp_all  by (simp add: cong_sym) 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 (simp add: normalfilter_def)  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 \<sqinter> 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_alllemma lemma_3_15_iii: "H1 ∈ normalfilters ==> H2 ∈ normalfilters ==> (H1 ⊆ H2) = (cong H1 ≤ cong H2)"  apply safe  apply (simp add: cong_l cong_l_filter)  apply blast  apply (subgoal_tac "cong H2 x 1")  apply (simp add: cong_l cong_l_def)  apply (subgoal_tac "cong H1 x 1")  apply blast  by (simp add: cong_l cong_l_def)definition  "p x y z = ((x l-> y) r-> z) \<sqinter> ((z l-> y) r-> x)"lemma lemma_3_16_i: "p x x y = y ∧ p x y y = x"  apply safe  apply (simp_all add: p_def)  apply (rule antisym)  apply (simp_all add: lemma_2_10_24)  apply (rule antisym)  by (simp_all add: lemma_2_10_24)definition "M x y z = ((y l-> x) r-> x) \<sqinter> ((z l-> y) r-> y) \<sqinter> ((x l-> z) r-> z)"lemma "M x x y = x ∧ M x y x = x ∧ M y x x = x"  apply (simp add: M_def)  apply safe  apply (rule antisym)  apply (simp_all add: lemma_2_10_24 lemma_2_5_9_b)   apply (rule antisym)  apply (simp_all add: lemma_2_10_24 lemma_2_5_9_b)   apply (rule antisym)  by (simp_all add: lemma_2_10_24 lemma_2_5_9_b) endend`