# Theory PseudoHoops

Up to index of Isabelle/HOL/LatticeProperties/PseudoHoops

theory PseudoHoops
imports RightComplementedMonoid
`header{* Pseudo-Hoops *}theory PseudoHoopsimports RightComplementedMonoidbeginlemma drop_assumption:  "p ==> True"  by simpclass pseudo_hoop_algebra = left_complemented_monoid_algebra + right_complemented_monoid_nole_algebra +  assumes left_right_impl_times: "(a l-> b) * a = a * (a r-> b)"begin  definition     "inf_rr a b  = a * (a r-> b)"  definition    "lesseq_r a b = (a r-> b = 1)"  definition    "less_r a b = (lesseq_r a b ∧ ¬ lesseq_r b a)"end(*sublocale pseudo_hoop_algebra < right!: right_complemented_monoid_algebra lesseq_r less_r 1 "op *" inf_rr "op r->";  apply unfold_locales;  apply simp_all;  apply (simp add: less_r_def);  apply (simp add: inf_rr_def);  apply (rule right_impl_times, rule right_impl_ded);  by (simp add: lesseq_r_def);*)context pseudo_hoop_algebra begin  lemma right_complemented_monoid_algebra: "class.right_complemented_monoid_algebra lesseq_r less_r 1 (op *) inf_rr (op r->)"   (* by unfold_locales;*)  apply unfold_locales  apply simp_all  apply (simp add: less_r_def)  apply (simp add: inf_rr_def)  apply (rule right_impl_times, rule right_impl_ded)  by (simp add: lesseq_r_def)  lemma inf_rr_inf [simp]: "inf_rr = op \<sqinter>"    by (unfold fun_eq_iff, simp add: inf_rr_def inf_l_def left_right_impl_times)  lemma lesseq_lesseq_r: "lesseq_r a b = (a ≤ b)"  proof -    interpret A!: right_complemented_monoid_algebra lesseq_r less_r 1 "op *" inf_rr "op r->"      by (rule right_complemented_monoid_algebra)(*    find_theorems name: le_iff_inf    thm A.dual_algebra.le_iff_inf    have "!!x y. lesseq_r x y = (inf_rr x y = x)" by fact    note `!!x y. lesseq_r x y = (inf_rr x y = x)`*)    show "lesseq_r a b = (a ≤ b)"      apply (subst  le_iff_inf)      apply (subst `lesseq_r a b = (inf_rr a b = a)`)      apply (unfold inf_rr_inf [THEN sym])      by simp  qed  lemma [simp]: "lesseq_r = op ≤"    apply (unfold fun_eq_iff, simp add: lesseq_lesseq_r) done  lemma [simp]: "less_r = op <"    by (unfold fun_eq_iff, simp add: less_r_def less_le_not_le)      subclass right_complemented_monoid_algebra     apply (cut_tac right_complemented_monoid_algebra)    by simp  endsublocale pseudo_hoop_algebra <      pseudo_hoop_dual!: pseudo_hoop_algebra "λ a b . b * a" "op \<sqinter>" "op r->" "op ≤" "op <" 1 "op l->"  apply unfold_locales  apply (simp add: inf_l_def)  apply simp  apply (simp add: left_impl_times)  apply (simp add: left_impl_ded)  by (simp add: left_right_impl_times)context pseudo_hoop_algebra beginlemma commutative_ps: "(∀ a b . a * b = b * a) = ((op l->) = (op r->))"  apply (simp add: fun_eq_iff)  apply safe  apply (rule antisym)  apply (simp add: right_residual [THEN sym])  apply (subgoal_tac "x * (x l-> xa) =  (x l-> xa) * x")  apply (drule drop_assumption)  apply simp  apply (simp add: left_residual)  apply simp  apply (simp add: left_residual [THEN sym])  apply (simp add: right_residual)  apply (rule antisym)  apply (simp add: left_residual)  apply (simp add: right_residual [THEN sym])  apply (simp add: left_residual)  by (simp add: right_residual [THEN sym])lemma lemma_2_4_5: "a l-> b ≤ (c l-> a) l-> (c l-> b)"  apply (simp add: left_residual [THEN sym] mult_assoc)  apply (rule_tac y = "(a l-> b) * a" in order_trans)  apply (rule mult_left_mono)  by (simp_all add: left_residual)endcontext pseudo_hoop_algebra beginlemma lemma_2_4_6: "a r-> b ≤ (c r-> a) r-> (c r-> b)"  by (rule pseudo_hoop_dual.lemma_2_4_5)primrec  imp_power_l:: "'a => nat => 'a => 'a" ("(_) l-(_)-> (_)" [65,0,65] 65) where    "a l-0-> b = b" |   "a l-(Suc n)-> b = (a l-> (a l-n-> b))"primrec  imp_power_r:: "'a => nat => 'a => 'a" ("(_) r-(_)-> (_)" [65,0,65] 65) where    "a r-0-> b = b" |   "a r-(Suc n)-> b = (a r-> (a r-n-> b))"lemma lemma_2_4_7_a: "a l-n-> b = a ^ n l-> b"   apply (induct_tac n)  by (simp_all add: left_impl_ded)lemma lemma_2_4_7_b: "a r-n-> b = a ^ n r-> b"   apply (induct_tac n)  by (simp_all add: right_impl_ded [THEN sym] power_commutes)lemma lemma_2_5_8_a [simp]: "a * b ≤ a"  by (rule dual_algebra.H)lemma lemma_2_5_8_b [simp]: "a * b ≤ b"  by (rule H)lemma lemma_2_5_9_a: "a ≤ b l-> a"  by (simp add: left_residual [THEN sym] dual_algebra.H)lemma lemma_2_5_9_b: "a ≤ b r-> a"  by (simp add: right_residual [THEN sym] H)lemma lemma_2_5_11: "a * b ≤ a \<sqinter> b"  by simplemma lemma_2_5_12_a: "a ≤ b ==>  c l-> a ≤ c l-> b"  apply (subst left_residual [THEN sym])  apply (subst left_impl_times)  apply (rule_tac y = "(a l-> c) * b" in order_trans)  apply (simp add: mult_left_mono)  by (rule H)lemma lemma_2_5_13_a: "a ≤ b ==>  b l-> c ≤ a l-> c"  apply (simp add: left_residual [THEN sym])  apply (rule_tac y = "(b l-> c) * b" in order_trans)  apply (simp add: mult_left_mono)  by (simp add: left_residual)lemma lemma_2_5_14: "(b l-> c) * (a l-> b) ≤ a l-> c"  apply (simp add: left_residual [THEN sym])  apply (simp add: mult_assoc)  apply (subst left_impl_times)  apply (subst mult_assoc [THEN sym])  apply (subst left_residual)  by (rule dual_algebra.H)lemma lemma_2_5_16: "(a l-> b) ≤  (b l-> c) r-> (a l-> c)"  apply (simp add: right_residual [THEN sym])  by (rule lemma_2_5_14)lemma lemma_2_5_18: "(a l-> b) ≤  a * c l-> b * c"  apply (simp add: left_residual  [THEN sym])  apply (subst mult_assoc  [THEN sym])  apply (rule mult_right_mono)  apply (subst left_impl_times)  by (rule H)endcontext pseudo_hoop_algebra beginlemma lemma_2_5_12_b: "a ≤ b ==>  c r-> a ≤ c r-> b"  by (rule pseudo_hoop_dual.lemma_2_5_12_a)lemma lemma_2_5_13_b: "a ≤ b ==>  b r-> c ≤ a r-> c"  by (rule pseudo_hoop_dual.lemma_2_5_13_a)lemma lemma_2_5_15: "(a r-> b) * (b r-> c) ≤ a r-> c"  by (rule pseudo_hoop_dual.lemma_2_5_14)lemma lemma_2_5_17: "(a r-> b) ≤  (b r-> c) l-> (a r-> c)"  by (rule pseudo_hoop_dual.lemma_2_5_16)lemma lemma_2_5_19: "(a r-> b) ≤  c * a r-> c * b"  by (rule pseudo_hoop_dual.lemma_2_5_18)definition  "lower_bound A = {a . ∀ x ∈ A . a ≤ x}"definition  "infimum A = {a ∈ lower_bound A . (∀ x ∈ lower_bound A . x ≤ a)}"lemma infimum_unique: "(infimum A = {x}) = (x ∈ infimum A)"  apply safe  apply simp  apply (rule antisym)  by (simp_all add: infimum_def)lemma lemma_2_6_20:  "a ∈ infimum A ==> b l-> a ∈ infimum ((op l-> b)`A)"  apply (subst infimum_def)  apply safe  apply (simp add: infimum_def lower_bound_def lemma_2_5_12_a)  by (simp add: infimum_def lower_bound_def left_residual  [THEN sym])endcontext pseudo_hoop_algebra beginlemma lemma_2_6_21:  "a ∈ infimum A ==> b r-> a ∈ infimum ((op r-> b)`A)"  by (rule pseudo_hoop_dual.lemma_2_6_20)lemma infimum_pair: "a ∈ infimum {x . x = b ∨ x = c} = (a = b \<sqinter> c)"  apply (simp add: infimum_def lower_bound_def)  apply safe  apply (rule antisym)  by simp_all lemma lemma_2_6_20_a:  "a l-> (b \<sqinter> c) = (a l-> b) \<sqinter> (a l-> c)"  apply (subgoal_tac "b \<sqinter> c ∈ infimum {x . x = b ∨ x = c}")  apply (drule_tac b = a in lemma_2_6_20)  apply (case_tac "(op l-> a) ` {x . ((x = b) ∨ (x = c))} = {x . x = a l-> b ∨ x = a l-> c}")  apply (simp_all add: infimum_pair)  by autoendcontext pseudo_hoop_algebra beginlemma lemma_2_6_21_a:  "a r-> (b \<sqinter> c) = (a r-> b) \<sqinter> (a r-> c)"  by (rule pseudo_hoop_dual.lemma_2_6_20_a)lemma mult_mono: "a ≤ b ==> c ≤ d ==> a * c ≤ b * d"  apply (rule_tac y = "a * d" in order_trans)  by (simp_all add: mult_right_mono mult_left_mono)lemma lemma_2_7_22: "(a l-> b) * (c l-> d) ≤ (a \<sqinter> c) l-> (b \<sqinter> d)"  apply (rule_tac y = "(a \<sqinter> c l-> b) * (a \<sqinter> c l-> d)" in order_trans)  apply (rule mult_mono)  apply (simp_all add: lemma_2_5_13_a)  apply (rule_tac y = "(a \<sqinter> c l-> b) \<sqinter> (a \<sqinter> c l-> d)" in order_trans)  apply (rule lemma_2_5_11)  by (simp add: lemma_2_6_20_a)endcontext pseudo_hoop_algebra beginlemma lemma_2_7_23: "(a r-> b) * (c r-> d) ≤ (a \<sqinter> c) r-> (b \<sqinter> d)"  apply (rule_tac y = "(c \<sqinter> a) r-> (d \<sqinter> b)" in order_trans)  apply (rule pseudo_hoop_dual.lemma_2_7_22)  by (simp add: inf_commute)definition  "upper_bound A = {a . ∀ x ∈ A . x ≤ a}"definition  "supremum A = {a ∈ upper_bound A . (∀ x ∈ upper_bound A . a ≤ x)}"lemma supremum_unique:  "a ∈ supremum A ==> b ∈ supremum A ==> a = b"  apply (simp add: supremum_def upper_bound_def)  apply (rule antisym)  by autolemma lemma_2_8_i:  "a ∈ supremum A ==> a l-> b ∈ infimum ((λ x . x l-> b)`A)"  apply (subst infimum_def)  apply safe  apply (simp add: supremum_def upper_bound_def lower_bound_def lemma_2_5_13_a)  apply (simp add: supremum_def upper_bound_def lower_bound_def left_residual  [THEN sym])  by (simp add: right_residual)endcontext pseudo_hoop_algebra beginlemma lemma_2_8_i1:  "a ∈ supremum A ==> a r-> b ∈ infimum ((λ x . x r-> b)`A)"  by (rule pseudo_hoop_dual.lemma_2_8_i, simp)definition  times_set :: "'a set => 'a set => 'a set"  (infixl "**" 70) where  "(A ** B) = {a . ∃ x ∈ A . ∃ y ∈ B . a = x * y}"lemma times_set_assoc: "A ** (B ** C) = (A ** B) ** C"  apply (simp add: times_set_def)  apply safe  apply (rule_tac x = "xa * xb" in exI)  apply safe  apply (rule_tac x = xa in bexI)  apply (rule_tac x = xb in bexI)  apply simp_all  apply (subst mult_assoc)  apply (rule_tac x = ya in bexI)  apply simp_all  apply (rule_tac x = xb in bexI)  apply simp_all  apply (rule_tac x = "ya * y" in exI)  apply (subst mult_assoc)  apply simp  by autoprimrec power_set :: "'a set => nat => 'a set" (infixr "*^" 80) where    power_set_0: "(A *^ 0) = {1}"  | power_set_Suc: "(A *^ (Suc n)) = (A ** (A *^ n))"lemma infimum_singleton [simp]: "infimum {a} = {a}"  apply (simp add: infimum_def lower_bound_def)  by auto  lemma lemma_2_8_ii:  "a ∈ supremum A ==> (a ^ n) l-> b ∈ infimum ((λ x . x l-> b)`(A *^ n))"  apply (induct_tac n)  apply simp  apply (simp add: left_impl_ded)  apply (drule_tac a = "a ^ n l-> b" and b = a in lemma_2_6_20)  apply (simp add: infimum_def lower_bound_def times_set_def)  apply safe  apply (drule_tac b = "y l-> b" in lemma_2_8_i)  apply (simp add: infimum_def lower_bound_def times_set_def left_impl_ded)  apply (rule_tac y = "a l-> y l-> b" in order_trans)  apply simp_all  apply (subgoal_tac "(∀xa ∈ A *^ n. x ≤ a l-> xa l-> b)")  apply simp  apply safe  apply (drule_tac b = "xa l-> b" in lemma_2_8_i)  apply (simp add: infimum_def lower_bound_def)  apply safe  apply (subgoal_tac "(∀xb ∈ A. x ≤ xb l-> xa l-> b)")  apply simp  apply safe  apply (subgoal_tac "x ≤ xb * xa l-> b")  apply (simp add: left_impl_ded)  apply (subgoal_tac "(∃x ∈ A. ∃y ∈ A *^ n. xb * xa = x * y)")  by autolemma power_set_Suc2:  "A *^ (Suc n) = A *^ n ** A"  apply (induct_tac n)  apply (simp add: times_set_def)  apply simp  apply (subst times_set_assoc)  by simplemma power_set_add:  "A *^ (n + m) = (A *^ n) ** (A *^ m)"  apply (induct_tac m)  apply simp  apply (simp add: times_set_def)  apply simp  apply (subst times_set_assoc)  apply (subst times_set_assoc)  apply (subst power_set_Suc2 [THEN sym])  by simpendcontext pseudo_hoop_algebra beginlemma lemma_2_8_ii1:  "a ∈ supremum A ==> (a ^ n) r-> b ∈ infimum ((λ x . x r-> b)`(A *^ n))"  apply (induct_tac n)  apply simp  apply (subst power_Suc2)  apply (subst power_set_Suc2)  apply (simp add: right_impl_ded)  apply (drule_tac a = "a ^ n r-> b" and b = a in lemma_2_6_21)  apply (simp add: infimum_def lower_bound_def times_set_def)  apply safe  apply (drule_tac b = "xa r-> b" in lemma_2_8_i1)  apply (simp add: infimum_def lower_bound_def times_set_def right_impl_ded)  apply (rule_tac y = "a r-> xa r-> b" in order_trans)  apply simp_all  apply (subgoal_tac "(∀xa ∈ A *^ n. x ≤ a r-> xa r-> b)")  apply simp  apply safe  apply (drule_tac b = "xa r-> b" in lemma_2_8_i1)  apply (simp add: infimum_def lower_bound_def)  apply safe  apply (subgoal_tac "(∀xb ∈ A. x ≤ xb r-> xa r-> b)")  apply simp  apply safe  apply (subgoal_tac "x ≤ xa * xb r-> b")  apply (simp add: right_impl_ded)  apply (subgoal_tac "(∃x ∈ A *^ n. ∃y ∈ A . xa * xb = x * y)")  by autolemma lemma_2_9_i:  "b ∈ supremum A ==> a * b ∈ supremum (op * a ` A)"  apply (simp add: supremum_def upper_bound_def)  apply safe  apply (simp add: mult_left_mono)  by (simp add: right_residual) lemma lemma_2_9_i1:  "b ∈ supremum A ==> b * a ∈ supremum ((λ x . x * a) ` A)"  apply (simp add: supremum_def upper_bound_def)  apply safe  apply (simp add: mult_right_mono)  by (simp add: left_residual)lemma lemma_2_9_ii:  "b ∈ supremum A ==> a \<sqinter> b ∈ supremum (op \<sqinter> a ` A)"  apply (subst supremum_def)  apply safe  apply (simp add: supremum_def upper_bound_def)  apply safe  apply (rule_tac y = x in order_trans)  apply simp_all  apply (subst inf_commute)  apply (subst inf_l_def)  apply (subst left_right_impl_times)  apply (frule_tac a = "(b r-> a)" in lemma_2_9_i1)  apply (simp add: right_residual)  apply (simp add: supremum_def upper_bound_def)  apply (simp add: right_residual)  apply safe  apply (subgoal_tac "(∀xa ∈ A. b r-> a ≤ xa r-> x)")  apply simp  apply safe  apply (simp add: inf_l_def)  apply (simp add: left_right_impl_times)  apply (rule_tac y = "xa r->  b * (b r-> a)" in order_trans)  apply simp  apply (rule lemma_2_5_12_b)  apply (subst left_residual)  apply (subgoal_tac "(∀xa∈A. xa ≤ (b r-> a) l-> x)")  apply simp  apply safe  apply (subst left_residual [THEN sym])  apply (rule_tac y = "xaa * (xaa r-> a)" in order_trans)  apply (rule mult_left_mono)  apply (rule lemma_2_5_13_b)  apply simp  apply (subst right_impl_times)  by simplemma lemma_2_10_24:  "a ≤ (a l-> b) r-> b"  by (simp add: right_residual [THEN sym] inf_l_def [THEN sym])lemma lemma_2_10_25:  "a ≤ (a l-> b) r-> a"  by (rule lemma_2_5_9_b)endcontext pseudo_hoop_algebra beginlemma lemma_2_10_26:  "a ≤ (a r-> b) l-> b"  by (rule pseudo_hoop_dual.lemma_2_10_24)lemma lemma_2_10_27:  "a ≤ (a r-> b) l-> a"  by (rule lemma_2_5_9_a)lemma lemma_2_10_28:  "b l-> ((a l-> b) r-> a) = b l-> a"  apply (rule antisym)  apply (subst left_residual [THEN sym])  apply (rule_tac y = "((a l-> b) r-> a) \<sqinter> a" in order_trans)  apply (subst inf_l_def)  apply (rule_tac y = "(((a l-> b) r-> a) l-> b) * ((a l-> b) r-> a)" in order_trans)  apply (subst left_impl_times)  apply simp_all  apply (rule mult_right_mono)  apply (rule_tac y = "a l-> b" in order_trans)  apply (rule lemma_2_5_13_a)   apply (fact lemma_2_10_25)  apply (fact lemma_2_10_26)  apply (rule lemma_2_5_12_a)   by (fact lemma_2_10_25)end  context pseudo_hoop_algebra beginlemma lemma_2_10_29:  "b r-> ((a r-> b) l-> a) = b r-> a"  by (rule pseudo_hoop_dual.lemma_2_10_28)lemma lemma_2_10_30:  "((b l-> a) r-> a) l-> a = b l-> a"  apply (rule antisym)  apply (simp_all add: lemma_2_10_26)  apply (rule lemma_2_5_13_a)   by (rule lemma_2_10_24)endcontext pseudo_hoop_algebra beginlemma lemma_2_10_31:  "((b r-> a) l-> a) r-> a = b r-> a"  by (rule pseudo_hoop_dual.lemma_2_10_30)lemma lemma_2_10_32:  "(((b l-> a) r-> a) l-> b) l-> (b l-> a) = b l-> a"  proof -    have "((((b l-> a) r-> a) l-> b) l-> (b l-> a) = (((b l-> a) r-> a) l-> b) l-> (((b l-> a) r-> a) l-> a))"      by (simp add: lemma_2_10_30)    also have "… = ((((b l-> a) r-> a) l-> b) * ((b l-> a) r-> a) l-> a)"      by (simp add: left_impl_ded)    also have "… = (((b l-> a) r-> a) \<sqinter> b) l-> a"      by (simp add: inf_l_def)    also have "… = b l-> a" apply (subgoal_tac "((b l-> a) r-> a) \<sqinter> b = b", simp, rule antisym)       by (simp_all add: lemma_2_10_24)    finally show ?thesis .  qedendcontext pseudo_hoop_algebra beginlemma lemma_2_10_33:  "(((b r-> a) l-> a) r-> b) r-> (b r-> a) = b r-> a"  by (rule pseudo_hoop_dual.lemma_2_10_32)endclass pseudo_hoop_sup_algebra = pseudo_hoop_algebra + sup +  assumes    sup_comute: "a \<squnion> b = b \<squnion> a"    and sup_le [simp]: "a ≤ a \<squnion> b"    and le_sup_equiv: "(a ≤ b) = (a \<squnion> b = b)"begin  lemma sup_le_2 [simp]:    "b ≤ a \<squnion> b"    by (subst sup_comute, simp)  lemma le_sup_equiv_r:    "(a \<squnion> b = b) = (a ≤ b)"    by (simp add: le_sup_equiv)  lemma sup_idemp [simp]:     "a \<squnion> a = a"    by (simp add: le_sup_equiv_r)endclass pseudo_hoop_sup1_algebra = pseudo_hoop_algebra + sup +  assumes  sup_def: "a \<squnion> b = ((a l-> b) r-> b) \<sqinter> ((b l-> a) r-> a)"beginlemma sup_comute1: "a \<squnion> b = b \<squnion> a"  apply (simp add: sup_def)  apply (rule antisym)  by simp_alllemma sup_le1 [simp]: "a ≤ a \<squnion> b"  by (simp add: sup_def lemma_2_10_24 lemma_2_5_9_b)lemma le_sup_equiv1: "(a ≤ b) = (a \<squnion> b = b)"  apply safe  apply (simp add: left_lesseq)  apply (rule antisym)  apply (simp add: sup_def)  apply (simp add: sup_def)  apply (simp_all add: lemma_2_10_24)  apply (simp add:  le_iff_inf)  apply (subgoal_tac "(a \<sqinter> b = a \<sqinter> (a \<squnion> b)) ∧ (a \<sqinter> (a \<squnion> b) = a)")  apply simp  apply safe  apply simp  apply (rule antisym)  apply simp  apply (drule drop_assumption)  by (simp add: sup_comute1)  subclass pseudo_hoop_sup_algebra  apply unfold_locales  apply (simp add: sup_comute1)  apply simp  by (simp add: le_sup_equiv1)endclass pseudo_hoop_sup2_algebra = pseudo_hoop_algebra + sup +  assumes  sup_2_def: "a \<squnion> b = ((a r-> b) l-> b) \<sqinter> ((b r-> a) l-> a)"context pseudo_hoop_sup1_algebra begin endsublocale pseudo_hoop_sup2_algebra < sup1_dual!: pseudo_hoop_sup1_algebra "op \<squnion>" "λ a b . b * a" "op \<sqinter>" "op r->" "op ≤" "op <" 1 "op l->"  apply unfold_locales  by (simp add: sup_2_def)context pseudo_hoop_sup2_algebra beginlemma sup_comute_2: "a \<squnion> b = b \<squnion> a"  by (rule  sup1_dual.sup_comute)lemma sup_le2 [simp]: "a ≤ a \<squnion> b"  by (rule sup1_dual.sup_le)lemma le_sup_equiv2: "(a ≤ b) = (a \<squnion> b = b)"  by (rule sup1_dual.le_sup_equiv)  subclass pseudo_hoop_sup_algebra  apply unfold_locales  apply (simp add: sup_comute_2)  apply simp  by (simp add: le_sup_equiv2)endclass pseudo_hoop_lattice_a = pseudo_hoop_sup_algebra +  assumes sup_inf_le_distr: "a \<squnion> (b \<sqinter> c) ≤ (a \<squnion> b) \<sqinter> (a \<squnion> c)"begin  lemma sup_lower_upper_bound [simp]:    "a ≤ c ==> b ≤ c ==> a \<squnion> b ≤ c"    apply (subst le_iff_inf)    apply (subgoal_tac "(a \<squnion> b) \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c) ∧ a \<squnion> (b \<sqinter> c) ≤ (a \<squnion> b) \<sqinter> (a \<squnion> c) ∧ a \<squnion> (b \<sqinter> c) = a \<squnion> b")    apply (rule antisym)    apply simp    apply safe    apply auto[1]    apply (simp add:  le_sup_equiv)    apply (rule sup_inf_le_distr)    by (simp add: le_iff_inf)endsublocale pseudo_hoop_lattice_a <  lattice "op \<sqinter>" "op ≤" "op <" "op \<squnion>"  by (unfold_locales, simp_all)class pseudo_hoop_lattice_b = pseudo_hoop_sup_algebra +  assumes le_sup_cong: "a ≤ b ==> a \<squnion> c ≤ b \<squnion> c"begin  lemma sup_lower_upper_bound_b [simp]:    "a ≤ c ==> b ≤ c ==> a \<squnion> b ≤ c"    proof -      assume A: "a ≤ c"      assume B: "b ≤ c"      have "a \<squnion> b ≤ c \<squnion> b" by (cut_tac A, simp add: le_sup_cong)      also have "… = b \<squnion> c" by (simp add: sup_comute)      also have "… ≤ c \<squnion> c" by (cut_tac B, rule le_sup_cong, simp)      also have "… = c"  by simp      finally show ?thesis .    qed  lemma  sup_inf_le_distr_b:    "a \<squnion> (b \<sqinter> c) ≤ (a \<squnion> b) \<sqinter> (a \<squnion> c)"    apply (rule sup_lower_upper_bound_b)    apply simp    apply simp    apply safe    apply (subst sup_comute)    apply (rule_tac y = "b" in order_trans)    apply simp_all    apply (rule_tac y = "c" in order_trans)    by simp_allendcontext pseudo_hoop_lattice_a begin endsublocale pseudo_hoop_lattice_b <  pseudo_hoop_lattice_a "op \<squnion>" "op *" "op \<sqinter>" "op l->" "op ≤" "op <" 1 "op r->"  by (unfold_locales, rule sup_inf_le_distr_b)class pseudo_hoop_lattice = pseudo_hoop_sup_algebra +  assumes sup_assoc_1: "a \<squnion> (b \<squnion> c) = (a \<squnion> b) \<squnion> c"begin  lemma le_sup_cong_c:    "a ≤ b ==> a \<squnion> c ≤ b \<squnion> c"    proof -      assume A: "a ≤ b"      have "a \<squnion> c \<squnion> (b \<squnion> c) = a \<squnion> (c \<squnion> (b \<squnion> c))" by (simp add: sup_assoc_1)      also have "… = a \<squnion> ((b \<squnion> c) \<squnion> c)" by (simp add: sup_comute)      also have "… = a \<squnion> (b \<squnion> (c \<squnion> c))" by (simp add: sup_assoc_1 [THEN sym])      also have "… = (a \<squnion> b) \<squnion> c" by (simp add: sup_assoc_1)      also have "… = b \<squnion> c" by (cut_tac A, simp add: le_sup_equiv)      finally show ?thesis by (simp add: le_sup_equiv)    qedendsublocale pseudo_hoop_lattice <  pseudo_hoop_lattice_b "op \<squnion>" "op *" "op \<sqinter>" "op l->" "op ≤" "op <" 1 "op r->"  by (unfold_locales, rule le_sup_cong_c)sublocale pseudo_hoop_lattice <  semilattice_sup "op \<squnion>" "op ≤" "op <"  by (unfold_locales, simp_all)sublocale pseudo_hoop_lattice <  lattice "op \<sqinter>" "op ≤" "op <" "op \<squnion>"  by unfold_localeslemma (in pseudo_hoop_lattice_a) supremum_pair [simp]:  "supremum {a, b} = {a \<squnion> b}"   apply (simp add: supremum_def upper_bound_def)  apply safe  apply simp_all  apply (rule antisym)  by simp_allsublocale pseudo_hoop_lattice <  distrib_lattice "op \<sqinter>" "op ≤" "op <" "op \<squnion>"  apply unfold_locales  apply (rule distrib_imp1)  apply (case_tac "xa \<sqinter> (ya \<squnion> za) ∈ supremum (op \<sqinter> xa ` {ya, za})")  apply (simp add: supremum_pair)  apply (erule notE)  apply (rule lemma_2_9_ii)  by (simp add: supremum_pair)class bounded_semilattice_inf_top = semilattice_inf + topbeginlemma inf_eq_top_iff [simp]:  "(inf x y = top) = (x = top ∧ y = top)"  by (simp add: eq_iff)endsublocale pseudo_hoop_algebra < bounded_semilattice_inf_top "op \<sqinter>" "op ≤" "op <" "1"  by unfold_locales simpdefinition (in pseudo_hoop_algebra)  sup1::"'a => 'a => 'a" (infixl "\<squnion>1" 70) where   "a \<squnion>1 b = ((a l-> b) r-> b) \<sqinter> ((b l-> a) r-> a)"sublocale pseudo_hoop_algebra < sup1!: pseudo_hoop_sup1_algebra "op \<squnion>1" "op *" "op \<sqinter>" "op l->" "op ≤" "op <" 1 "op r->"  apply unfold_locales   by (simp add: sup1_def)definition (in pseudo_hoop_algebra)  sup2::"'a => 'a => 'a" (infixl "\<squnion>2" 70) where   "a \<squnion>2 b = ((a r-> b) l-> b) \<sqinter> ((b r-> a) l-> a)"sublocale pseudo_hoop_algebra < sup2!: pseudo_hoop_sup2_algebra "op \<squnion>2" "op *" "op \<sqinter>" "op l->" "op ≤" "op <" 1 "op r->"  apply unfold_locales   by (simp add: sup2_def)context pseudo_hoop_algebrabegin  lemma lemma_2_15_i:    "1 ∈ supremum {a, b} ==> a * b = a \<sqinter> b"    apply (rule antisym)    apply (rule lemma_2_5_11)    apply (simp add: inf_l_def)    apply (subst left_impl_times)    apply (rule mult_right_mono)    apply (subst right_lesseq)    apply (subgoal_tac "a \<squnion>1 b = 1")    apply (simp add: sup1_def)    apply (rule antisym)    apply simp    by (simp add: supremum_def upper_bound_def)      lemma lemma_2_15_ii:    "1 ∈ supremum {a, b} ==> a ≤ c ==> b ≤ d ==> 1 ∈ supremum {c, d}"    apply (simp add: supremum_def upper_bound_def)    apply safe    apply (drule_tac x = x in spec)    apply safe    by simp_alllemma sup_union:  "a ∈ supremum A ==> b ∈ supremum B ==> supremum {a, b} = supremum (A ∪ B)"  apply safe  apply (simp_all add: supremum_def upper_bound_def)  apply safe  apply auto  apply (subgoal_tac "(∀x ∈ A ∪ B. x ≤ xa)")  by autolemma sup_singleton [simp]: "a ∈ supremum {a}"  by (simp add: supremum_def upper_bound_def) lemma sup_union_singleton: "a ∈ supremum X ==> supremum {a, b} = supremum (X ∪ {b})"  apply (rule_tac B = "{b}" in  sup_union)  by simp_alllemma sup_le_union [simp]: "a ≤ b ==> supremum (A ∪ {a, b}) = supremum (A ∪ {b})"  apply (simp add: supremum_def upper_bound_def)  by autolemma sup_sup_union: "a ∈ supremum A ==> b ∈ supremum (B ∪ {a}) ==> b ∈ supremum (A ∪ B)"  apply (simp add: supremum_def upper_bound_def)  by auto  end(*context monoid_multbeginlemma "a ^ 2 = a * a"  by (simp add: local.power2_eq_square)end*)lemma [simp]:  "n ≤ 2 ^ n"  apply (induct_tac n)  apply auto  apply (rule_tac y = "1 + 2 ^ n" in order_trans)  by autocontext pseudo_hoop_algebrabeginlemma sup_le_union_2:  "a ≤ b ==> a ∈ A ==> b ∈ A ==> supremum A = supremum ((A - {a}) ∪ {b})"  apply (case_tac "supremum ((A - {a , b}) ∪ {a, b}) = supremum ((A - {a, b}) ∪ {b})")  apply (case_tac "((A - {a, b}) ∪ {a, b} = A) ∧ ((A - {a, b}) ∪ {b} = (A - {a}) ∪ {b})")  apply safe[1]   apply simp  apply simp  apply (erule notE)  apply safe [1]  apply (erule notE)  apply (rule sup_le_union)  by simp  lemma lemma_2_15_iii_0:    "1 ∈ supremum {a, b} ==> 1 ∈ supremum {a ^ 2, b ^ 2}"    apply (frule_tac a = a in lemma_2_9_i)    apply simp    apply (frule_tac a = a and b = b in sup_union_singleton)    apply (subgoal_tac "supremum ({a * a, a * b} ∪ {b}) = supremum ({a * a, b})")    apply simp_all    apply (frule_tac a = b in lemma_2_9_i)    apply simp    apply (drule_tac a = b and A = "{b * (a * a), b * b}" and b = 1 and B = "{a * a}" in sup_sup_union)    apply simp    apply (case_tac "{a * a, b} = {b, a * a}")    apply simp    apply auto [1]    apply simp    apply (subgoal_tac "supremum {a * a, b * (a * a), b * b} = supremum {a * a, b * b}")    apply(simp add: power2_eq_square)    apply (case_tac "b * (a * a) = b * b")    apply auto[1]    apply (cut_tac  A = "{a * a, b * (a * a), b * b}" and a = "b * (a * a)" and b = "a * a" in  sup_le_union_2)    apply simp    apply simp    apply simp    apply (subgoal_tac "({a * a, b * (a * a), b * b} - {b * (a * a)} ∪ {a * a}) = {a * a, b * b}")    apply simp    apply auto[1]    apply (case_tac "a * a = a * b")    apply (subgoal_tac "{b, a * a, a * b} = {a * a, b}")    apply simp    apply auto[1]    apply (cut_tac  A = "{b, a * a, a * b}" and a = "a * b" and b = "b" in  sup_le_union_2)    apply simp    apply simp    apply simp    apply (subgoal_tac "{b, a * a, a * b} - {a * b} ∪ {b} = {a * a, b}")    apply simp    by auto   lemma [simp]: "m ≤ n ==> a ^ n ≤ a ^ m"  apply (subgoal_tac "a ^ n = (a ^ m) * (a ^ (n-m))")  apply simp  apply (cut_tac a = a and m = "m" and n = "n - m" in power_add)  by simplemma [simp]: "a ^ (2 ^ n) ≤ a ^ n"  by simplemma lemma_2_15_iii_1: "1 ∈ supremum {a, b} ==> 1 ∈ supremum {a ^ (2 ^ n), b ^ (2 ^ n)}"  apply (induct_tac n)  apply auto[1]  apply (drule drop_assumption)  apply (drule lemma_2_15_iii_0)  apply (subgoal_tac "!a . (a ^ (2::nat) ^ n)² = a ^ (2::nat) ^ Suc n")  apply simp  apply safe  apply (cut_tac a = aa and m = "2 ^ n" and n = 2 in  power_mult)  apply auto  apply (subgoal_tac "((2::nat) ^ n * (2::nat)) = ((2::nat) * (2::nat) ^ n)")  by simp_all  lemma lemma_2_15_iii:    "1 ∈ supremum {a, b} ==> 1 ∈ supremum {a ^ n, b ^ n}"    apply (drule_tac n = n in lemma_2_15_iii_1)    apply (simp add: supremum_def upper_bound_def)    apply safe    apply (drule_tac x = x in spec)    apply safe    apply (rule_tac y = "a ^ n" in order_trans)    apply simp_all    apply (rule_tac y = "b ^ n" in order_trans)    by simp_allendend`