Theory BL_Chains

section‹BL-chains›

text‹BL-chains generate the variety of BL-algebras, the algebraic counterpart
 of the Basic Fuzzy Logic (see \<^cite>‹"HAJEK1998"›). As mentioned in the abstract, this formalization
 is based on the proof for BL-chains found in \<^cite>‹"BUSANICHE2005"›. We define @{text "BL-chain"} and
 @{text "bounded tower of irreducible hoops"} and formalize the main result on that paper (Theorem 3.4).›

theory BL_Chains
  imports Totally_Ordered_Hoops 

begin

subsection‹Definitions›

locale bl_chain = totally_ordered_hoop + 
  fixes zeroA :: "'a" ("0⇧^A")
  assumes zero_closed: "0⇧^A ∈ A"
  assumes zero_first: "x ∈ A ⟹ 0⇧^A ≤⇧^A x"

locale bounded_tower_of_irr_hoops = tower_of_irr_hoops +
  fixes zeroI ("0⇧^I") 
  fixes zeroS ("0⇧^S")
  assumes I_zero_closed : "0⇧^I ∈ I"
  and zero_first: "i ∈ I ⟹ 0⇧^I ≤⇧^I i"
  and first_zero_closed: "0⇧^S ∈ UNI 0⇧^I"
  and first_bounded: "x ∈ UNI 0⇧^I ⟹ IMP 0⇧^I 0⇧^S x = 1⇧^S"
begin

abbreviation (uni_zero)
  uni_zero :: "'b set"  ("𝔸⇩₀⇩_I")
  where "𝔸⇩₀⇩_I ≡ UNI 0⇧^I"

abbreviation (imp_zero)
  imp_zero :: "['b, 'b] ⇒ 'b"  ("((_)/ →⇧⁰⇧^I / (_))" [61,61] 60)
  where "x →⇧⁰⇧^I y ≡ IMP 0⇧^I x y"

end

context bl_chain
begin

subsection‹First element of @{term I}›

definition zeroI :: "'a set" ("0⇧^I")
  where "0⇧^I = π 0⇧^A"

lemma I_zero_closed: "0⇧^I ∈ I"
  using index_set_def zeroI_def zero_closed by auto

lemma I_has_first_element:
  assumes "i ∈ I" "i ≠ 0⇧^I"
  shows "0⇧^I <⇧^I i"
proof -
  have "x ≤⇧^A y" if "i <⇧^I 0⇧^I" "x ∈ i" "y ∈ 0⇧^I" for x y
    using I_zero_closed assms(1) index_order_strict_def that by fastforce
  then
  have "x ≤⇧^A 0⇧^A" if "i <⇧^I 0⇧^I" "x ∈ i" for x
    using classes_not_empty zeroI_def zero_closed that by simp
  moreover
  have "0⇧^A ≤⇧^A x" if "x ∈ i" for x
    using assms(1) that in_mono indexes_subsets zero_first by meson
  ultimately
  have "x = 0⇧^A" if "i <⇧^I 0⇧^I" "x ∈ i" for x
    using assms(1) indexes_subsets ord_antisymm zero_closed that by blast
  moreover
  have "0⇧^A ∈ 0⇧^I"
    using classes_not_empty zeroI_def zero_closed by simp
  ultimately
  have "i ∩ 0⇧^I ≠ ∅" if "i <⇧^I 0⇧^I"
    using assms(1) indexes_not_empty that by force
  moreover
  have "i <⇧^I 0⇧^I ∨ 0⇧^I <⇧^I i"
    using I_zero_closed assms trichotomy by auto
  ultimately
  show ?thesis
    using I_zero_closed assms(1) indexes_disjoint by auto
qed

subsection‹Main result for BL-chains›

definition zeroS :: "'a" ("0⇧^S")
  where "0⇧^S = 0⇧^A"

abbreviation (uniA_zero)
  uniA_zero :: "'a set" ("(𝔸⇩₀⇩_I)")
  where "𝔸⇩₀⇩_I ≡ UNI⇩_A 0⇧^I"

abbreviation (impA_zero_xy)
  impA_zero_xy :: "['a, 'a] ⇒ 'a"  ("((_)/ →⇧⁰⇧^I / (_))" [61, 61] 60)
  where "x →⇧⁰⇧^I y ≡ IMP⇩_A 0⇧^I x y"

lemma tower_is_bounded:
  shows "bounded_tower_of_irr_hoops I (≤⇧^I) (<⇧^I) UNI⇩_A MUL⇩_A IMP⇩_A 1⇧^S 0⇧^I 0⇧^S"
proof
  show "0⇧^I ∈ I"
    using I_zero_closed by simp
next
  show "0⇧^I ≤⇧^I i" if "i ∈ I" for i
    using I_has_first_element index_ord_reflex index_order_strict_def that by blast
next
  show "0⇧^S ∈ 𝔸⇩₀⇩_I"
    using classes_not_empty universes_def zeroI_def zeroS_def zero_closed by simp
next
  show "0⇧^S →⇧⁰⇧^I x = 1⇧^S" if "x ∈ 𝔸⇩₀⇩_I" for x
    using I_zero_closed universes_subsets hoop_order_def imp_map_def sum_one_def
          zeroS_def zero_first that
    by simp
qed

lemma ordinal_sum_is_bl_totally_ordered:
  shows "bl_chain A_SUM.sum_univ A_SUM.sum_mult A_SUM.sum_imp 1⇧^S 0⇧^S"
proof
  show "A_SUM.hoop_order x y ∨ A_SUM.hoop_order y x"
    if "x ∈ A_SUM.sum_univ" "y ∈ A_SUM.sum_univ" for x y
    using ordinal_sum_is_totally_ordered_hoop totally_ordered_hoop.total_order that
    by meson
next
  show "0⇧^S ∈ A_SUM.sum_univ"
    using zeroS_def zero_closed by simp
next
  show "A_SUM.hoop_order 0⇧^S x" if "x ∈ A_SUM.sum_univ" for x
    using A_SUM.hoop_order_def eq_imp hoop_order_def sum_one_def zeroS_def zero_closed
          zero_first that
    by simp
qed

theorem bl_chain_is_equal_to_ordinal_sum_of_bounded_tower_of_irr_hoops:
  shows eq_universe: "A = A_SUM.sum_univ"
  and eq_mult: "x ∈ A ⟹ y ∈ A ⟹ x *⇧^A y = A_SUM.sum_mult x y"
  and eq_imp: "x ∈ A ⟹ y ∈ A ⟹ x →⇧^A y = A_SUM.sum_imp x y"
  and eq_zero: "0⇧^A = 0⇧^S"
  and eq_one: "1⇧^A = 1⇧^S"
proof
  show "A ⊆ A_SUM.sum_univ"
    by auto
next
  show "A_SUM.sum_univ ⊆ A"
    by auto
next
  show "x *⇧^A y = A_SUM.sum_mult x y" if "x ∈ A" "y ∈ A" for x y
    using eq_mult that by blast
next
  show "x →⇧^A y = A_SUM.sum_imp x y" if "x ∈ A" "y ∈ A" for x y
    using eq_imp that by blast
next
  show "0⇧^A = 0⇧^S"
    using zeroS_def by simp
next
  show "1⇧^A = 1⇧^S"
    using sum_one_def by simp
qed

end

subsection‹Converse of main result for BL-chains›

context bounded_tower_of_irr_hoops
begin

text‹We show that the converse of the main result holds if @{term "0⇧^S ≠ 1⇧^S"}. If @{term "0⇧^S = 1⇧^S"}
then the converse may not be true. For example, take a trivial hoop @{text A} and an arbitrary
not bounded Wajsberg hoop @{text B} such that @{text "A ∩ B = {1}"}. The ordinal sum of both hoops is equal to
@{text B} and therefore not bounded.›

proposition ordinal_sum_of_bounded_tower_of_irr_hoops_is_bl_chain:
  assumes "0⇧^S ≠ 1⇧^S" 
  shows "bl_chain S (*⇧^S) (→⇧^S) 1⇧^S 0⇧^S"
proof
  show "hoop_order a b ∨ hoop_order b a" if "a ∈ S" "b ∈ S" for a b
  proof -
    from that
    consider (1) "a ∈ S-{1⇧^S}" "b ∈ S-{1⇧^S}" "floor a = floor b"
      | (2) "a ∈ S-{1⇧^S}" "b ∈ S-{1⇧^S}" "floor a <⇧^I floor b ∨ floor b <⇧^I floor a"
      | (3) "a = 1⇧^S ∨ b = 1⇧^S"
      using floor.cases floor_prop trichotomy by metis
    then
    show ?thesis
    proof(cases)
      case 1
      then
      have "a ∈ 𝔸⇩_f⇩_l⇩_o⇩_o⇩_r ⇩a ∧ b ∈ 𝔸⇩_f⇩_l⇩_o⇩_o⇩_r ⇩a"
        using "1" floor_prop by metis
      moreover
      have "totally_ordered_hoop (𝔸⇩_f⇩_l⇩_o⇩_o⇩_r ⇩a) (*⇧^f⇧^l⇧^o⇧^o⇧^r ⇧a) (→⇧^f⇧^l⇧^o⇧^o⇧^r ⇧a) 1⇧^S"
        using "1"(1) family_of_irr_hoops totally_ordered_irreducible_hoop.axioms(1)
              floor_prop
        by meson
      ultimately
      have "a →⇧^f⇧^l⇧^o⇧^o⇧^r ⇧a b = 1⇧^S ∨ b →⇧^f⇧^l⇧^o⇧^o⇧^r ⇧a a = 1⇧^S"
        using hoop.hoop_order_def totally_ordered_hoop.total_order
              totally_ordered_hoop_def
        by meson
      moreover
      have "a →⇧^S b = a →⇧^f⇧^l⇧^o⇧^o⇧^r ⇧a b ∧ b →⇧^S a = b →⇧^f⇧^l⇧^o⇧^o⇧^r ⇧a a"
        using "1" by auto
      ultimately
      show ?thesis
        using hoop_order_def by force
    next
      case 2
      then
      show ?thesis
        using sum_imp.simps(2) hoop_order_def by blast
    next
      case 3
      then
      show ?thesis
        using that ord_top by auto
    qed
  qed
next
  show "0⇧^S ∈ S"
    using first_zero_closed I_zero_closed sum_subsets by auto
next
  show "hoop_order 0⇧^S a" if "a ∈ S" for a 
  proof -
    have zero_dom: "0⇧^S ∈ 𝔸⇩₀⇩_I ∧ 0⇧^S ∈ S-{1⇧^S}"
      using I_zero_closed sum_subsets assms first_zero_closed by blast
    moreover
    have "floor 0⇧^S ≤⇧^I floor x" if "0⇧^S ∈ S-{1⇧^S}" "x ∈ S-{1⇧^S}" for x
      using I_zero_closed floor_prop floor_unique that(2) zero_dom zero_first
      by metis
    ultimately
    have "floor 0⇧^S ≤⇧^I floor x" if "x ∈ S-{1⇧^S}" for x
      using that by blast
    then
    consider (1) "0⇧^S ∈ S-{1⇧^S}" "a ∈ S-{1⇧^S}" "floor 0⇧^S = floor a"
      | (2) "0⇧^S ∈ S-{1⇧^S}" "a ∈ S-{1⇧^S}" "floor 0⇧^S <⇧^I floor a"
      | (3) "a = 1⇧^S"
      using ‹a ∈ S› floor.cases floor_prop strict_order_equiv_not_converse 
            trichotomy zero_dom
      by metis
    then
    show "hoop_order 0⇧^S a"
    proof(cases)
      case 1
      then
      have "0⇧^S ∈ 𝔸⇩₀⇩_I ∧ a ∈ 𝔸⇩₀⇩_I"
        using I_zero_closed first_zero_closed floor_prop floor_unique by metis
      then
      have "0⇧^S →⇧^S a = 0⇧^S →⇧⁰⇧^I a ∧ 0⇧^S →⇧⁰⇧^I a = 1⇧^S"
        using "1" I_zero_closed sum_imp.simps(1) first_bounded floor_prop floor_unique
        by metis
      then
      show ?thesis
        using hoop_order_def by blast
    next
      case 2
      then
      show ?thesis
        using sum_imp.simps(2,5) hoop_order_def by meson
    next
      case 3
      then
      show ?thesis
        using ord_top zero_dom by auto
    qed
  qed
qed

end

end