Theory PseudoHoops
section‹Pseudo-Hoops›
theory PseudoHoops
imports RightComplementedMonoid
begin
lemma drop_assumption:
"p ⟹ True"
by simp
class 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
context pseudo_hoop_algebra begin
lemma right_complemented_monoid_algebra: "class.right_complemented_monoid_algebra lesseq_r less_r 1 (*) inf_rr (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)
lemma inf_rr_inf [simp]: "inf_rr = (⊓)"
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 "(*)" inf_rr "(r→)"
by (rule right_complemented_monoid_algebra)
show "lesseq_r a b = (a ≤ b)"
apply (subst le_iff_inf)
apply (subst A.dual_algebra.inf.absorb_iff1 [of a b])
apply (unfold inf_rr_inf [THEN sym])
by simp
qed
lemma [simp]: "lesseq_r = (≤)"
apply (unfold fun_eq_iff, simp add: lesseq_lesseq_r) done
lemma [simp]: "less_r = (<)"
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
end
sublocale pseudo_hoop_algebra <
pseudo_hoop_dual: pseudo_hoop_algebra "λ a b . b * a" "(⊓)" "(r→)" "(≤)" "(<)" 1 "(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 begin
lemma commutative_ps: "(∀ a b . a * b = b * a) = ((l→) = (r→))"
apply (simp add: fun_eq_iff)
apply safe
apply (rule order.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 order.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)
end
context pseudo_hoop_algebra begin
lemma 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 ⊓ b"
by simp
lemma 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)
end
context pseudo_hoop_algebra begin
lemma 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 order.antisym)
by (simp_all add: infimum_def)
lemma lemma_2_6_20:
"a ∈ infimum A ⟹ b l→ a ∈ infimum (((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])
end
context pseudo_hoop_algebra begin
lemma lemma_2_6_21:
"a ∈ infimum A ⟹ b r→ a ∈ infimum (((r→) b)`A)"
by (rule pseudo_hoop_dual.lemma_2_6_20)
lemma infimum_pair: "a ∈ infimum {x . x = b ∨ x = c} = (a = b ⊓ c)"
apply (simp add: infimum_def lower_bound_def)
apply safe
apply (rule order.antisym)
by simp_all
lemma lemma_2_6_20_a:
"a l→ (b ⊓ c) = (a l→ b) ⊓ (a l→ c)"
apply (subgoal_tac "b ⊓ c ∈ infimum {x . x = b ∨ x = c}")
apply (drule_tac b = a in lemma_2_6_20)
apply (case_tac "((l→) a) ` {x . ((x = b) ∨ (x = c))} = {x . x = a l→ b ∨ x = a l→ c}")
apply (simp_all add: infimum_pair)
by auto
end
context pseudo_hoop_algebra begin
lemma lemma_2_6_21_a:
"a r→ (b ⊓ c) = (a r→ b) ⊓ (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 ⊓ c) l→ (b ⊓ d)"
apply (rule_tac y = "(a ⊓ c l→ b) * (a ⊓ c l→ d)" in order_trans)
apply (rule mult_mono)
apply (simp_all add: lemma_2_5_13_a)
apply (rule_tac y = "(a ⊓ c l→ b) ⊓ (a ⊓ c l→ d)" in order_trans)
apply (rule lemma_2_5_11)
by (simp add: lemma_2_6_20_a)
end
context pseudo_hoop_algebra begin
lemma lemma_2_7_23: "(a r→ b) * (c r→ d) ≤ (a ⊓ c) r→ (b ⊓ d)"
apply (rule_tac y = "(c ⊓ a) r→ (d ⊓ 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 order.antisym)
by auto
lemma 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)
end
context pseudo_hoop_algebra begin
lemma lemma_2_8_i1:
"a ∈ supremum A ⟹ a r→ b ∈ infimum ((λ x . x r→ b)`A)"
by (fact pseudo_hoop_dual.lemma_2_8_i)
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 auto
primrec 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 auto
lemma 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 simp
lemma 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 simp
end
context pseudo_hoop_algebra begin
lemma 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 auto
lemma lemma_2_9_i:
"b ∈ supremum A ⟹ a * b ∈ supremum ((*) 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 ⊓ b ∈ supremum ((⊓) 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 simp
lemma 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)
end
context pseudo_hoop_algebra begin
lemma 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 order.antisym)
apply (subst left_residual [THEN sym])
apply (rule_tac y = "((a l→ b) r→ a) ⊓ 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 begin
lemma 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 order.antisym)
apply (simp_all add: lemma_2_10_26)
apply (rule lemma_2_5_13_a)
by (rule lemma_2_10_24)
end
context pseudo_hoop_algebra begin
lemma 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) ⊓ b) l→ a"
by (simp add: inf_l_def)
also have "… = b l→ a" apply (subgoal_tac "((b l→ a) r→ a) ⊓ b = b", simp, rule order.antisym)
by (simp_all add: lemma_2_10_24)
finally show ?thesis .
qed
end
context pseudo_hoop_algebra begin
lemma 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)
end
class pseudo_hoop_sup_algebra = pseudo_hoop_algebra + sup +
assumes
sup_comute: "a ⊔ b = b ⊔ a"
and sup_le [simp]: "a ≤ a ⊔ b"
and le_sup_equiv: "(a ≤ b) = (a ⊔ b = b)"
begin
lemma sup_le_2 [simp]:
"b ≤ a ⊔ b"
by (subst sup_comute, simp)
lemma le_sup_equiv_r:
"(a ⊔ b = b) = (a ≤ b)"
by (simp add: le_sup_equiv)
lemma sup_idemp [simp]:
"a ⊔ a = a"
by (simp add: le_sup_equiv_r)
end
class pseudo_hoop_sup1_algebra = pseudo_hoop_algebra + sup +
assumes
sup_def: "a ⊔ b = ((a l→ b) r→ b) ⊓ ((b l→ a) r→ a)"
begin
lemma sup_comute1: "a ⊔ b = b ⊔ a"
apply (simp add: sup_def)
apply (rule order.antisym)
by simp_all
lemma sup_le1 [simp]: "a ≤ a ⊔ b"
by (simp add: sup_def lemma_2_10_24 lemma_2_5_9_b)
lemma le_sup_equiv1: "(a ≤ b) = (a ⊔ b = b)"
apply safe
apply (simp add: left_lesseq)
apply (rule order.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 ⊓ b = a ⊓ (a ⊔ b)) ∧ (a ⊓ (a ⊔ b) = a)")
apply simp
apply safe
apply simp
apply (rule order.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)
end
class pseudo_hoop_sup2_algebra = pseudo_hoop_algebra + sup +
assumes
sup_2_def: "a ⊔ b = ((a r→ b) l→ b) ⊓ ((b r→ a) l→ a)"
context pseudo_hoop_sup1_algebra begin end
sublocale pseudo_hoop_sup2_algebra < sup1_dual: pseudo_hoop_sup1_algebra "(⊔)" "λ a b . b * a" "(⊓)" "(r→)" "(≤)" "(<)" 1 "(l→)"
apply unfold_locales
by (simp add: sup_2_def)
context pseudo_hoop_sup2_algebra begin
lemma sup_comute_2: "a ⊔ b = b ⊔ a"
by (rule sup1_dual.sup_comute)
lemma sup_le2 [simp]: "a ≤ a ⊔ b"
by (rule sup1_dual.sup_le)
lemma le_sup_equiv2: "(a ≤ b) = (a ⊔ 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)
end
class pseudo_hoop_lattice_a = pseudo_hoop_sup_algebra +
assumes sup_inf_le_distr: "a ⊔ (b ⊓ c) ≤ (a ⊔ b) ⊓ (a ⊔ c)"
begin
lemma sup_lower_upper_bound [simp]:
"a ≤ c ⟹ b ≤ c ⟹ a ⊔ b ≤ c"
apply (subst le_iff_inf)
apply (subgoal_tac "(a ⊔ b) ⊓ c = (a ⊔ b) ⊓ (a ⊔ c) ∧ a ⊔ (b ⊓ c) ≤ (a ⊔ b) ⊓ (a ⊔ c) ∧ a ⊔ (b ⊓ c) = a ⊔ b")
apply (rule order.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)
end
sublocale pseudo_hoop_lattice_a < lattice "(⊓)" "(≤)" "(<)" "(⊔)"
by (unfold_locales, simp_all)
class pseudo_hoop_lattice_b = pseudo_hoop_sup_algebra +
assumes le_sup_cong: "a ≤ b ⟹ a ⊔ c ≤ b ⊔ c"
begin
lemma sup_lower_upper_bound_b [simp]:
"a ≤ c ⟹ b ≤ c ⟹ a ⊔ b ≤ c"
proof -
assume A: "a ≤ c"
assume B: "b ≤ c"
have "a ⊔ b ≤ c ⊔ b" by (cut_tac A, simp add: le_sup_cong)
also have "… = b ⊔ c" by (simp add: sup_comute)
also have "… ≤ c ⊔ 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 ⊔ (b ⊓ c) ≤ (a ⊔ b) ⊓ (a ⊔ 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_all
end
context pseudo_hoop_lattice_a begin end
sublocale pseudo_hoop_lattice_b < pseudo_hoop_lattice_a "(⊔)" "(*)" "(⊓)" "(l→)" "(≤)" "(<)" 1 "(r→)"
by (unfold_locales, rule sup_inf_le_distr_b)
class pseudo_hoop_lattice = pseudo_hoop_sup_algebra +
assumes sup_assoc_1: "a ⊔ (b ⊔ c) = (a ⊔ b) ⊔ c"
begin
lemma le_sup_cong_c:
"a ≤ b ⟹ a ⊔ c ≤ b ⊔ c"
proof -
assume A: "a ≤ b"
have "a ⊔ c ⊔ (b ⊔ c) = a ⊔ (c ⊔ (b ⊔ c))" by (simp add: sup_assoc_1)
also have "… = a ⊔ ((b ⊔ c) ⊔ c)" by (simp add: sup_comute)
also have "… = a ⊔ (b ⊔ (c ⊔ c))" by (simp add: sup_assoc_1 [THEN sym])
also have "… = (a ⊔ b) ⊔ c" by (simp add: sup_assoc_1)
also have "… = b ⊔ c" by (cut_tac A, simp add: le_sup_equiv)
finally show ?thesis by (simp add: le_sup_equiv)
qed
end
sublocale pseudo_hoop_lattice < pseudo_hoop_lattice_b "(⊔)" "(*)" "(⊓)" "(l→)" "(≤)" "(<)" 1 "(r→)"
by (unfold_locales, rule le_sup_cong_c)
sublocale pseudo_hoop_lattice < semilattice_sup "(⊔)" "(≤)" "(<)"
by (unfold_locales, simp_all)
sublocale pseudo_hoop_lattice < lattice "(⊓)" "(≤)" "(<)" "(⊔)"
by unfold_locales
lemma (in pseudo_hoop_lattice_a) supremum_pair [simp]:
"supremum {a, b} = {a ⊔ b}"
apply (simp add: supremum_def upper_bound_def)
apply safe
apply simp_all
apply (rule order.antisym)
by simp_all
sublocale pseudo_hoop_lattice < distrib_lattice "(⊓)" "(≤)" "(<)" "(⊔)"
apply unfold_locales
apply (rule distrib_imp1)
apply (case_tac "xa ⊓ (ya ⊔ za) ∈ supremum ((⊓) 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 + order_top
begin
lemma inf_eq_top_iff [simp]:
"(inf x y = top) = (x = top ∧ y = top)"
by (simp add: order.eq_iff)
end
sublocale pseudo_hoop_algebra < bounded_semilattice_inf_top "(⊓)" "(≤)" "(<)" "1"
by unfold_locales simp
definition (in pseudo_hoop_algebra)
sup1::"'a ⇒ 'a ⇒ 'a" (infixl "⊔1" 70) where
"a ⊔1 b = ((a l→ b) r→ b) ⊓ ((b l→ a) r→ a)"
sublocale pseudo_hoop_algebra < sup1: pseudo_hoop_sup1_algebra "(⊔1)" "(*)" "(⊓)" "(l→)" "(≤)" "(<)" 1 "(r→)"
apply unfold_locales
by (simp add: sup1_def)
definition (in pseudo_hoop_algebra)
sup2::"'a ⇒ 'a ⇒ 'a" (infixl "⊔2" 70) where
"a ⊔2 b = ((a r→ b) l→ b) ⊓ ((b r→ a) l→ a)"
sublocale pseudo_hoop_algebra < sup2: pseudo_hoop_sup2_algebra "(⊔2)" "(*)" "(⊓)" "(l→)" "(≤)" "(<)" 1 "(r→)"
apply unfold_locales
by (simp add: sup2_def)
context pseudo_hoop_algebra
begin
lemma lemma_2_15_i:
"1 ∈ supremum {a, b} ⟹ a * b = a ⊓ b"
apply (rule order.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 ⊔1 b = 1")
apply (simp add: sup1_def)
apply (rule order.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_all
lemma 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 auto
lemma 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_all
lemma sup_le_union [simp]: "a ≤ b ⟹ supremum (A ∪ {a, b}) = supremum (A ∪ {b})"
apply (simp add: supremum_def upper_bound_def)
by auto
lemma 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
lemma [simp]:
"n ≤ 2 ^ n"
apply (induct_tac n)
apply auto
apply (rule_tac y = "1 + 2 ^ n" in order_trans)
by auto
context pseudo_hoop_algebra
begin
lemma 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 simp
lemma [simp]: "a ^ (2 ^ n) ≤ a ^ n"
by simp
lemma 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)⇧2 = 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_all
end
end