Theory Ordinal_Sums

section‹Ordinal sums›

text‹We define @{text "tower of hoops"}, a family of almost disjoint hoops indexed by a total order.
 This is based on the definition of @{text "bounded tower of irreducible hoops"} in \<^cite>‹"BUSANICHE2005"›
 (see paragraph after Lemma 3.3). Parting from a tower of hoops we can define a hoop known as @{text "ordinal sum"}.
 Ordinal sums are a fundamental tool in the study of totally ordered hoops.›

theory Ordinal_Sums
  imports Hoops 
begin

subsection‹Tower of hoops›

locale tower_of_hoops =
  fixes index_set :: "'b set" ("I")
  fixes index_lesseq :: "'b ⇒ 'b ⇒ bool" (infix "≤⇧I" 60)
  fixes index_less :: "'b ⇒ 'b ⇒ bool" (infix "<⇧I" 60)
  fixes universes :: "'b ⇒ ('a set)" ("UNI")
  fixes multiplications :: "'b ⇒ ('a ⇒ 'a ⇒ 'a)" ("MUL")
  fixes implications :: "'b ⇒ ('a ⇒ 'a ⇒ 'a)" ("IMP")
  fixes sum_one :: 'a ("1⇧S")
  assumes index_set_total_order: "total_poset_on I (≤⇧I) (<⇧I)"
  and almost_disjoint: "i ∈ I ⟹ j ∈ I ⟹ i ≠ j ⟹ UNI i ∩ UNI j = {1⇧S}"
  and family_of_hoops: "i ∈ I ⟹ hoop (UNI i) (MUL i) (IMP i) 1⇧S"
begin

sublocale total_poset_on "I" "(≤⇧I)" "(<⇧I)"
  using index_set_total_order by simp                   

abbreviation (uni_i)
  uni_i :: "['b] ⇒ ('a set)" ("(𝔸(⇩_))" [61] 60)
  where "𝔸⇩i ≡ UNI i"

abbreviation (mult_i)
  mult_i :: "['b] ⇒ ('a ⇒ 'a ⇒ 'a)" ("(*(⇧_))" [61] 60)
  where "*⇧i ≡ MUL i"

abbreviation (imp_i)
  imp_i :: "['b] ⇒ ('a ⇒ 'a ⇒ 'a)" ("(→(⇧_))" [61] 60)
  where "→⇧i ≡ IMP i"

abbreviation (mult_i_xy)
  mult_i_xy :: "['a, 'b, 'a] ⇒ 'a"  ("((_)/ *(⇧_) / (_))" [61, 50, 61] 60)
  where "x *⇧i y ≡ MUL i x y"

abbreviation (imp_i_xy)
  imp_i_xy :: "['a, 'b, 'a] ⇒ 'a"  ("((_)/ →(⇧_) / (_))" [61, 50, 61] 60)
  where "x →⇧i y ≡ IMP i x y"

subsection‹Ordinal sum universe›

definition sum_univ :: "'a set" ("S")
  where "S = {x. ∃ i ∈ I. x ∈ 𝔸⇩i}"

lemma sum_one_closed [simp]: "1⇧S ∈ S"
  using family_of_hoops hoop.one_closed not_empty sum_univ_def by fastforce

lemma sum_subsets: 
  assumes "i ∈ I"
  shows "𝔸⇩i ⊆ S"
  using sum_univ_def assms by blast

subsection‹Floor function: definition and properties›

lemma floor_unique:
  assumes "a ∈ S-{1⇧S}"
  shows "∃! i. i ∈ I ∧ a ∈ 𝔸⇩i"
  using assms sum_univ_def almost_disjoint by blast

function floor :: "'a ⇒ 'b" where
  "floor x = (THE i. i ∈ I ∧ x ∈ 𝔸⇩i)" if "x ∈ S-{1⇧S}"
| "floor x = undefined" if "x = 1⇧S ∨ x ∉ S"
  by auto
termination by lexicographic_order

abbreviation (uni_floor)
  uni_floor :: "['a] ⇒ ('a set)" ("(𝔸⇩f⇩l⇩o⇩o⇩r (⇩_))" [61] 60)
  where "𝔸⇩f⇩l⇩o⇩o⇩r ⇩x ≡ UNI (floor x)"

abbreviation (mult_floor)
  mult_floor :: "['a] ⇒ ('a ⇒ 'a ⇒ 'a)"  ("(*⇧f⇧l⇧o⇧o⇧r (⇧_))" [61] 60)
  where "*⇧f⇧l⇧o⇧o⇧r ⇧a ≡ MUL (floor a)"

abbreviation (imp_floor)
  imp_floor :: "['a] ⇒ ('a ⇒ 'a ⇒ 'a)"  ("(→⇧f⇧l⇧o⇧o⇧r (⇧_))" [61] 60)
  where "→⇧f⇧l⇧o⇧o⇧r ⇧a ≡ IMP (floor a)"

abbreviation (mult_floor_xy)
  mult_floor_xy :: "['a, 'a, 'a] ⇒ 'a"  ("((_)/ *⇧f⇧l⇧o⇧o⇧r (⇧_) / (_))" [61, 50, 61] 60)
  where "x *⇧f⇧l⇧o⇧o⇧r ⇧y z ≡ MUL (floor y) x z"

abbreviation (imp_floor_xy)
  imp_floor_xy :: "['a, 'a, 'a] ⇒ 'a"  ("((_)/ →⇧f⇧l⇧o⇧o⇧r (⇧_) / (_))" [61, 50, 61] 60)
  where "x →⇧f⇧l⇧o⇧o⇧r ⇧y z ≡ IMP (floor y) x z"

lemma floor_prop:
  assumes "a ∈ S-{1⇧S}"
  shows "floor a ∈ I ∧ a ∈ 𝔸⇩f⇩l⇩o⇩o⇩r ⇩a"
proof -
  have "floor a = (THE i. i ∈ I ∧ a ∈ 𝔸⇩i)"
    using assms by auto
  then
  show ?thesis
    using assms theI_unique floor_unique by (metis (mono_tags, lifting))
qed

lemma floor_one_closed:
  assumes "i ∈ I"
  shows "1⇧S ∈ 𝔸⇩i"
  using assms floor_prop family_of_hoops hoop.one_closed by metis

lemma floor_mult_closed:
  assumes "i ∈ I" "a ∈ 𝔸⇩i" "b ∈ 𝔸⇩i" 
  shows "a *⇧i b ∈ 𝔸⇩i"
  using assms family_of_hoops hoop.mult_closed by meson

lemma floor_imp_closed:
  assumes "i ∈ I" "a ∈ 𝔸⇩i" "b ∈ 𝔸⇩i" 
  shows "a →⇧i b ∈ 𝔸⇩i"
  using assms family_of_hoops hoop.imp_closed by meson

subsection‹Ordinal sum multiplication and implication›

function sum_mult :: "'a ⇒ 'a ⇒ 'a" (infix "*⇧S" 60) where
  "x *⇧S y = x *⇧f⇧l⇧o⇧o⇧r ⇧x y" if  "x ∈ S-{1⇧S}" "y ∈ S-{1⇧S}" "floor x = floor y"
| "x *⇧S y = x" if "x ∈ S-{1⇧S}" "y ∈ S-{1⇧S}" "floor x <⇧I floor y"
| "x *⇧S y = y" if "x ∈ S-{1⇧S}" "y ∈ S-{1⇧S}" "floor y <⇧I floor x"
| "x *⇧S y = y" if "x = 1⇧S" "y ∈ S-{1⇧S}"
| "x *⇧S y = x" if "x ∈ S-{1⇧S}" "y = 1⇧S"
| "x *⇧S y = 1⇧S" if "x = 1⇧S" "y = 1⇧S"
| "x *⇧S y = undefined" if "x ∉ S ∨ y ∉ S"
  apply auto
  using floor.cases floor.simps(1) floor_prop trichotomy apply (smt (verit))
  using floor_prop strict_iff_order apply force
  using floor_prop strict_iff_order apply force
  using floor_prop trichotomy by auto
termination by lexicographic_order

function sum_imp :: "'a ⇒ 'a ⇒ 'a" (infix "→⇧S" 60) where
  "x →⇧S y = x →⇧f⇧l⇧o⇧o⇧r ⇧x y" if "x ∈ S-{1⇧S}" "y ∈ S-{1⇧S}" "floor x = floor y"
| "x →⇧S y = 1⇧S" if "x ∈ S-{1⇧S}" "y ∈ S-{1⇧S}" "floor x <⇧I floor y"
| "x →⇧S y = y" if "x ∈ S-{1⇧S}" "y ∈ S-{1⇧S}" "floor y <⇧I floor x"
| "x →⇧S y = y" if "x = 1⇧S" "y ∈ S-{1⇧S}"
| "x →⇧S y = 1⇧S" if "x ∈ S-{1⇧S}" "y = 1⇧S"
| "x →⇧S y = 1⇧S" if "x = 1⇧S" "y = 1⇧S"
| "x →⇧S y = undefined" if "x ∉ S ∨ y ∉ S"
  apply auto
  using floor.cases floor.simps(1) floor_prop trichotomy apply (smt (verit))
  using floor_prop strict_iff_order apply force
  using floor_prop strict_iff_order apply force
  using floor_prop trichotomy by auto
termination by lexicographic_order

subsubsection‹Some multiplication properties›

lemma sum_mult_not_one_aux:
  assumes "a ∈ S-{1⇧S}" "b ∈ 𝔸⇩f⇩l⇩o⇩o⇩r ⇩a"
  shows "a *⇧S b ∈ (𝔸⇩f⇩l⇩o⇩o⇩r ⇩a)-{1⇧S}"
proof -
  consider (1) "b ∈ S-{1⇧S}"
    | (2) "b = 1⇧S"
    using sum_subsets assms floor_prop by blast
  then
  show ?thesis
  proof(cases)
    case 1
    then
    have same_floor: "floor a = floor b"
      using assms floor_prop floor_unique by metis
    moreover
    have "a *⇧S b = a *⇧f⇧l⇧o⇧o⇧r ⇧a b"
      using "1" assms(1) same_floor by simp
    moreover
    have "a ∈ (𝔸⇩f⇩l⇩o⇩o⇩r ⇩a)-{1⇧S} ∧ b ∈ (𝔸⇩f⇩l⇩o⇩o⇩r ⇩a)-{1⇧S}"
      using "1" assms floor_prop by simp
    ultimately
    show ?thesis
      using assms(1) family_of_hoops floor_prop hoop.mult_C by metis
  next
    case 2
    then
    show ?thesis
      using assms(1) floor_prop by auto
  qed
qed

corollary sum_mult_not_one:
  assumes "a ∈ S-{1⇧S}" "b ∈ 𝔸⇩f⇩l⇩o⇩o⇩r ⇩a"
  shows "a *⇧S b ∈ S-{1⇧S} ∧ floor (a *⇧S b) = floor a"
proof -
  have "a *⇧S b ∈ (𝔸⇩f⇩l⇩o⇩o⇩r ⇩a)-{1⇧S}"
    using sum_mult_not_one_aux assms by meson
  then 
  have "a *⇧S b ∈ S-{1⇧S} ∧ a *⇧S b ∈ 𝔸⇩f⇩l⇩o⇩o⇩r ⇩a"
    using sum_subsets assms(1) floor_prop by fastforce
  then
  show ?thesis
    using assms(1) floor_prop floor_unique by metis
qed
   
lemma sum_mult_A: 
  assumes "a ∈ S-{1⇧S}" "b ∈ 𝔸⇩f⇩l⇩o⇩o⇩r ⇩a"
  shows "a *⇧S b = a *⇧f⇧l⇧o⇧o⇧r ⇧a b  ∧ b *⇧S a = b *⇧f⇧l⇧o⇧o⇧r ⇧a a"
proof -
  consider (1) "b ∈ S-{1⇧S}"
    | (2) "b = 1⇧S"
    using sum_subsets assms floor_prop by blast
  then
  show ?thesis
  proof(cases)
    case 1
    then
    have "floor a = floor b"
      using assms floor.cases floor_prop floor_unique by metis
    then
    show ?thesis
      using "1" assms by auto
  next
    case 2
    then
    show ?thesis
      using assms(1) family_of_hoops floor_prop hoop.mult_neutr hoop.mult_neutr_2
      by fastforce
  qed
qed

subsubsection‹Some implication properties›

lemma sum_imp_floor:
  assumes "a ∈ S-{1⇧S}" "b ∈ S-{1⇧S}" "floor a = floor b" "a →⇧S b ∈ S-{1⇧S}" 
  shows "floor (a →⇧S b) = floor a"
proof -
  have "a →⇧S b ∈ 𝔸⇩f⇩l⇩o⇩o⇩r ⇩a"
    using sum_imp.simps(1) assms(1-3) floor_imp_closed floor_prop
    by metis
  then 
  show ?thesis
    using assms(1,4) floor_prop floor_unique by blast
qed

lemma sum_imp_A:
  assumes "a ∈ S-{1⇧S}" "b ∈ 𝔸⇩f⇩l⇩o⇩o⇩r ⇩a"
  shows "a →⇧S b = a →⇧f⇧l⇧o⇧o⇧r ⇧a b"
proof -
  consider (1) "b ∈ S-{1⇧S}"
    | (2) "b = 1⇧S"
    using sum_subsets assms floor_prop by blast
  then
  show ?thesis
  proof(cases)
    case 1
    then 
    show ?thesis
      using sum_imp.simps(1) assms floor_prop floor_unique by metis
  next
    case 2
    then
    show ?thesis
      using sum_imp.simps(5) assms(1) family_of_hoops floor_prop
            hoop.imp_one_top
      by metis
  qed
qed

lemma sum_imp_B:
  assumes "a ∈ S-{1⇧S}" "b ∈ 𝔸⇩f⇩l⇩o⇩o⇩r ⇩a"
  shows "b →⇧S a = b →⇧f⇧l⇧o⇧o⇧r ⇧a a"
proof -
  consider (1) "b ∈ S-{1⇧S}"
    | (2) "b = 1⇧S"
    using sum_subsets assms floor_prop by blast
  then
  show ?thesis
  proof(cases)
    case 1
    then 
    show ?thesis
      using sum_imp.simps(1) assms floor_prop floor_unique by metis
  next
    case 2
    then
    show ?thesis
      using sum_imp.simps(4) assms(1) family_of_hoops floor_prop
            hoop.imp_one_C
      by metis
  qed
qed

lemma sum_imp_floor_antisymm:
  assumes "a ∈ S-{1⇧S}" "b ∈ S-{1⇧S}" "floor a = floor b"
          "a →⇧S b = 1⇧S" "b →⇧S a = 1⇧S"
  shows "a = b"
proof -
  have "a ∈ 𝔸⇩f⇩l⇩o⇩o⇩r ⇩a ∧ b ∈ 𝔸⇩f⇩l⇩o⇩o⇩r ⇩a ∧ floor a ∈ I"
    using floor_prop assms by metis
  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 assms by auto
  ultimately
  show ?thesis
    using assms(4,5) family_of_hoops hoop.ord_antisymm_equiv by metis
qed

corollary sum_imp_C:
  assumes "a ∈ S-{1⇧S}" "b ∈ S-{1⇧S}" "a ≠ b" "floor a = floor b" "a →⇧S b = 1⇧S"
  shows "b →⇧S a ≠ 1⇧S"
  using sum_imp_floor_antisymm assms by blast

lemma sum_imp_D:
  assumes "a ∈ S"
  shows "1⇧S →⇧S a = a"
  using sum_imp.simps(4,6) assms by blast

lemma sum_imp_E:
  assumes "a ∈ S"
  shows "a →⇧S 1⇧S = 1⇧S"
  using sum_imp.simps(5,6) assms by blast

subsection‹The ordinal sum of a tower of hoops is a hoop›

subsubsection‹@{term S} is not empty›

lemma sum_not_empty: "S ≠ ∅"
  using sum_one_closed by blast

subsubsection‹@{term sum_mult} and @{term sum_imp} are well defined›

lemma sum_mult_closed_one: 
  assumes "a ∈ S" "b ∈ S" "a = 1⇧S ∨ b = 1⇧S"
  shows "a *⇧S b ∈ S"
  using sum_mult.simps(4-6) assms floor.cases by metis

lemma sum_mult_closed_not_one:
  assumes "a ∈ S-{1⇧S}" "b ∈ S-{1⇧S}"
  shows "a *⇧S b ∈ S-{1⇧S}"
proof -
  from assms
  consider (1) "floor a = floor b"
    | (2) "floor a <⇧I floor b ∨ floor b <⇧I floor a"
    using trichotomy floor_prop by blast
  then
  show ?thesis
  proof(cases)
    case 1 
    then 
    show ?thesis
      using sum_mult_not_one assms floor_prop by metis
  next 
    case 2
    then
    show ?thesis
      using assms by auto
  qed
qed

lemma sum_mult_closed:
  assumes "a ∈ S" "b ∈ S"
  shows "a *⇧S b ∈ S"
  using sum_mult_closed_not_one sum_mult_closed_one assms by auto

lemma sum_imp_closed_one:
  assumes "a ∈ S" "b ∈ S" "a = 1⇧S ∨ b = 1⇧S"
  shows "a →⇧S b ∈ S"
  using sum_imp.simps(4-6) assms floor.cases by metis

lemma sum_imp_closed_not_one:
  assumes "a ∈ S-{1⇧S}" "b ∈ S-{1⇧S}"
  shows "a →⇧S b ∈ S"
proof -
  from assms
  consider (1) "floor a = floor b"
    | (2) "floor a <⇧I floor b ∨ floor b <⇧I floor a"
    using trichotomy floor_prop by blast
  then
  show "a →⇧S b ∈ S"
  proof(cases)
    case 1 
    then
    have "a →⇧S b = a →⇧f⇧l⇧o⇧o⇧r ⇧a b" 
      using assms by auto
    moreover
    have "a →⇧f⇧l⇧o⇧o⇧r ⇧a b ∈ 𝔸⇩f⇩l⇩o⇩o⇩r ⇩a"
      using "1" assms floor_imp_closed floor_prop by metis
    ultimately
    show ?thesis
      using sum_subsets assms(1) floor_prop by auto
  next
    case 2
    then
    show ?thesis
      using assms by auto
  qed
qed

lemma sum_imp_closed:
  assumes "a ∈ S" "b ∈ S"
  shows "a →⇧S b ∈ S"
  using sum_imp_closed_one sum_imp_closed_not_one assms by auto

subsubsection‹Neutrality of @{term sum_one}›

lemma sum_mult_neutr:
  assumes "a ∈ S"
  shows "a *⇧S 1⇧S = a ∧ 1⇧S *⇧S a = a"
  using assms sum_mult.simps(4-6) by blast

subsubsection‹Commutativity of @{term sum_mult}›

text‹Now we prove @{term "x *⇧S y = y *⇧S x"} by showing
that it holds when one of the variables is equal to @{term "1⇧S"}. Then
we consider when none of them is @{term "1⇧S"}.›

lemma sum_mult_comm_one: 
  assumes "a ∈ S" "b ∈ S" "a = 1⇧S ∨ b = 1⇧S" 
  shows "a *⇧S b = b *⇧S a"
  using sum_mult_neutr assms by auto

lemma sum_mult_comm_not_one: 
  assumes "a ∈ S-{1⇧S}" "b ∈ S-{1⇧S}"
  shows "a *⇧S b = b *⇧S a"
proof -
  from assms
  consider (1) "floor a = floor b"
    | (2) "floor a <⇧I floor b ∨ floor b <⇧I floor a"
    using trichotomy floor_prop by blast
  then
  show ?thesis
  proof(cases)
    case 1
    then 
    have same_floor: "b ∈ 𝔸⇩f⇩l⇩o⇩o⇩r ⇩a"
      using assms(2) floor_prop by simp
    then
    have "a *⇧S b = a *⇧f⇧l⇧o⇧o⇧r ⇧a b"
      using sum_mult_A assms(1) by blast
    also
    have "… = b *⇧f⇧l⇧o⇧o⇧r ⇧a a"
      using assms(1) family_of_hoops floor_prop hoop.mult_comm same_floor
      by meson
    also
    have "… = b *⇧S a"
      using sum_mult_A assms(1) same_floor by simp
    finally 
    show ?thesis
      by auto
  next
    case 2
    then
    show ?thesis
      using assms by auto
  qed
qed

lemma sum_mult_comm:
  assumes "a ∈ S" "b ∈ S"
  shows "a *⇧S b = b *⇧S a"
  using assms sum_mult_comm_one sum_mult_comm_not_one by auto

subsubsection‹Associativity of @{term sum_mult}›

text‹Next we prove @{term "x *⇧S (y *⇧S z) = (x *⇧S y) *⇧S z"}.›

lemma sum_mult_assoc_one:
  assumes "a ∈ S" "b ∈ S" "c ∈ S" "a = 1⇧S ∨ b = 1⇧S ∨ c = 1⇧S"
  shows "a *⇧S (b *⇧S c) = (a *⇧S b) *⇧S c" 
  using  sum_mult_neutr assms sum_mult_closed by metis

lemma sum_mult_assoc_not_one:
  assumes "a ∈ S-{1⇧S}" "b ∈ S-{1⇧S}" "c ∈ S-{1⇧S}"
  shows "a *⇧S (b *⇧S c) = (a *⇧S b) *⇧S c"
proof -
  from assms
  consider (1) "floor a = floor b" "floor b = floor c"
    | (2) "floor a = floor b" "floor b <⇧I floor c"
    | (3) "floor a = floor b" "floor c <⇧I floor b"
    | (4) "floor a <⇧I floor b" "floor b = floor c"
    | (5) "floor a <⇧I floor b" "floor b <⇧I floor c"
    | (6) "floor a <⇧I floor b" "floor c <⇧I floor b"
    | (7) "floor b <⇧I floor a" "floor b = floor c"
    | (8) "floor b <⇧I floor a" "floor b <⇧I floor c"
    | (9) "floor b <⇧I floor a" "floor c <⇧I floor b"
     using trichotomy floor_prop by meson
  then
  show ?thesis
  proof(cases)
    case 1
    then
    have "a *⇧S (b *⇧S c) = a *⇧f⇧l⇧o⇧o⇧r ⇧a (b *⇧f⇧l⇧o⇧o⇧r ⇧a c)"
      using sum_mult_A assms floor_mult_closed floor_prop by metis
    also
    have "… = (a *⇧f⇧l⇧o⇧o⇧r ⇧a b) *⇧f⇧l⇧o⇧o⇧r ⇧a c"
      using "1" assms family_of_hoops floor_prop hoop.mult_assoc by metis
    also 
    have "… = (a *⇧f⇧l⇧o⇧o⇧r ⇧b b) *⇧f⇧l⇧o⇧o⇧r ⇧b c"
      using "1" by simp
    also
    have "… = (a *⇧S b) *⇧S c"
      using "1" sum_mult_A assms floor_mult_closed floor_prop by metis
    finally
    show ?thesis 
      by auto
  next
    case 2 
    then
    show ?thesis
      using sum_mult.simps(2,3) sum_mult_not_one assms floor_prop by metis
  next
    case 3
    then
    show ?thesis
      using sum_mult.simps(3) sum_mult_not_one assms floor_prop by metis
  next
    case 4
    then
    show ?thesis
      using sum_mult.simps(2) sum_mult_not_one assms floor_prop by metis
  next
    case 5
    then
    show ?thesis
      using sum_mult.simps(2) assms floor_prop strict_trans by metis
  next
    case 6
    then
    show ?thesis
      using sum_mult.simps(2,3) assms by metis
  next
    case 7
    then
    show ?thesis
      using sum_mult.simps(3) sum_mult_not_one assms floor_prop by metis
  next
    case 8
    then
    show ?thesis
      using sum_mult.simps(2,3) assms by metis
  next
    case 9
    then 
    show ?thesis
      using sum_mult.simps(3) assms floor_prop strict_trans by metis
  qed
qed

lemma sum_mult_assoc:
  assumes "a ∈ S" "b ∈ S" "c ∈ S"
  shows "a *⇧S (b *⇧S c) = (a *⇧S b) *⇧S c"
  using assms sum_mult_assoc_one sum_mult_assoc_not_one by blast

subsubsection‹Reflexivity of @{term sum_imp}›

lemma sum_imp_reflex:
  assumes "a ∈ S"
  shows "a →⇧S a = 1⇧S"
proof -
  consider (1) "a ∈ S-{1⇧S}"
    | (2) "a = 1⇧S"
    using assms by blast
  then
  show ?thesis
  proof(cases)
    case 1
    then 
    have "a →⇧S a = a →⇧f⇧l⇧o⇧o⇧r ⇧a a"
      by simp
    then
    show ?thesis
      using "1" family_of_hoops floor_prop hoop.imp_reflex by metis
  next
    case 2
    then 
    show ?thesis
      by simp
  qed
qed

subsubsection‹Divisibility›

text‹We prove @{term "x *⇧S (x →⇧S y) = y *⇧S (y →⇧S x)"} using the same methods as before.›

lemma sum_divisibility_one:
  assumes "a ∈ S" "b ∈ S" "a = 1⇧S ∨ b = 1⇧S"
  shows  "a *⇧S (a →⇧S b) = b *⇧S (b →⇧S a)"
proof -
  have "x →⇧S y = y ∧ y →⇧S x = 1⇧S" if "x = 1⇧S" "y ∈ S" for x y
    using sum_imp_D sum_imp_E that by simp
  then
  show ?thesis
    using assms sum_mult_neutr by metis
qed

lemma sum_divisibility_aux:
  assumes "a ∈ S-{1⇧S}" "b ∈ 𝔸⇩f⇩l⇩o⇩o⇩r ⇩a"
  shows "a *⇧S (a →⇧S b) = a *⇧f⇧l⇧o⇧o⇧r ⇧a (a →⇧f⇧l⇧o⇧o⇧r ⇧a b)"
  using sum_imp_A sum_mult_A assms floor_imp_closed floor_prop by metis

lemma sum_divisibility_not_one:
  assumes "a ∈ S-{1⇧S}" "b ∈ S-{1⇧S}"
  shows "a *⇧S (a →⇧S b) = b *⇧S (b →⇧S a)"
proof -
  from assms
  consider (1) "floor a = floor b"
    | (2) "floor a <⇧I floor b ∨ floor b <⇧I floor a"
    using trichotomy floor_prop by blast
  then
  show ?thesis
  proof(cases)
    case 1
    then
    have "a *⇧S (a →⇧S b) =  a *⇧f⇧l⇧o⇧o⇧r ⇧a (a →⇧f⇧l⇧o⇧o⇧r ⇧a b)"
      using "1" sum_divisibility_aux assms floor_prop by metis
    also
    have "… = b *⇧f⇧l⇧o⇧o⇧r ⇧a (b →⇧f⇧l⇧o⇧o⇧r ⇧a a)"
      using "1" assms family_of_hoops floor_prop hoop.divisibility by metis
    also
    have "… = b *⇧f⇧l⇧o⇧o⇧r ⇧b (b →⇧f⇧l⇧o⇧o⇧r ⇧b a)"
      using "1" by simp
    also
    have "… = b *⇧S (b →⇧S a)"
      using "1" sum_divisibility_aux assms floor_prop by metis
    finally
    show ?thesis
      by auto
  next 
    case 2
    then
    show ?thesis
      using assms by auto
  qed
qed

lemma sum_divisibility:
  assumes "a ∈ S" "b ∈ S"
  shows "a *⇧S (a →⇧S b) = b *⇧S (b →⇧S a)"
  using assms sum_divisibility_one sum_divisibility_not_one by auto

subsubsection‹Residuation›

text‹Finally we prove @{term "(x *⇧S y) →⇧S z = (x →⇧S (y →⇧S z))"}.›

lemma sum_residuation_one:
  assumes "a ∈ S" "b ∈ S" "c ∈ S" "a = 1⇧S ∨ b = 1⇧S ∨ c = 1⇧S"
  shows "(a *⇧S b) →⇧S c = a →⇧S (b →⇧S c)"
  using sum_imp_D sum_imp_E sum_imp_closed sum_mult_closed sum_mult_neutr
        assms
  by metis

lemma sum_residuation_not_one:
  assumes "a ∈ S-{1⇧S}" "b ∈ S-{1⇧S}" "c ∈ S-{1⇧S}"
  shows "(a *⇧S b) →⇧S c = a →⇧S (b →⇧S c)"
proof -
  from assms
   consider (1) "floor a = floor b" "floor b = floor c"
    | (2) "floor a = floor b" "floor b <⇧I floor c"
    | (3) "floor a = floor b" "floor c <⇧I floor b"
    | (4) "floor a <⇧I floor b" "floor b = floor c"
    | (5) "floor a <⇧I floor b" "floor b <⇧I floor c"
    | (6) "floor a <⇧I floor b" "floor c <⇧I floor b"
    | (7) "floor b <⇧I floor a" "floor b = floor c"
    | (8) "floor b <⇧I floor a" "floor b <⇧I floor c"
    | (9) "floor b <⇧I floor a" "floor c <⇧I floor b"
     using trichotomy floor_prop by meson
  then
  show ?thesis
  proof(cases)
    case 1
    then
    have "(a *⇧S b) →⇧S c = (a *⇧f⇧l⇧o⇧o⇧r ⇧a b) →⇧f⇧l⇧o⇧o⇧r ⇧a c"
      using sum_imp_B sum_mult_A assms floor_mult_closed floor_prop by metis
    also
    have "… = a →⇧f⇧l⇧o⇧o⇧r ⇧a (b →⇧f⇧l⇧o⇧o⇧r ⇧a c)"
      using "1" assms family_of_hoops floor_prop hoop.residuation by metis
    also
    have "… = a →⇧f⇧l⇧o⇧o⇧r ⇧b (b →⇧f⇧l⇧o⇧o⇧r ⇧b c)"
      using "1" by simp
    also
    have "… = a →⇧S (b →⇧S c)"
      using "1" sum_imp_A assms floor_imp_closed floor_prop by metis
    finally
    show ?thesis
      by auto
  next
    case 2
    then
    show ?thesis
      using sum_imp.simps(2,5) sum_mult_not_one assms floor_prop by metis
  next
    case 3
    then
    show ?thesis
      using sum_imp.simps(3) sum_mult_not_one assms floor_prop by metis
  next
    case 4
    then
    have "(a *⇧S b) →⇧S c = 1⇧S"
      using "4" sum_imp.simps(2) sum_mult.simps(2) assms by metis
    moreover
    have "b →⇧S c = 1⇧S ∨ (b →⇧S c ∈ S-{1⇧S} ∧ floor (b →⇧S c) = floor b)"
      using "4"(2) sum_imp_closed_not_one sum_imp_floor assms(2,3) by blast
    ultimately 
    show ?thesis
      using "4"(1) sum_imp.simps(2,5) assms(1) by metis
  next
    case 5
    then
    show ?thesis  
      using sum_imp.simps(2,5) sum_mult.simps(2) assms floor_prop strict_trans
      by metis
  next
    case 6
    then
    show ?thesis
      using assms by auto
  next
    case 7
    then
    have "(a *⇧S b) →⇧S c = (b →⇧S c)"
      using assms(1,2) by auto
    moreover
    have "b →⇧S c = 1⇧S ∨ (b →⇧S c ∈ S-{1⇧S} ∧ floor (b →⇧S c) = floor b)"
      using "7"(2) sum_imp_closed_not_one sum_imp_floor assms(2,3) by blast
    ultimately
    show ?thesis
      using "7"(1) sum_imp.simps(3,5) assms(1) by metis
  next
    case 8
    then
    show ?thesis
      using assms by auto
  next
    case 9
    then
    show ?thesis
      using sum_imp.simps(3) sum_mult.simps(3) assms floor_prop strict_trans 
      by metis
  qed
qed

lemma sum_residuation:
  assumes "a ∈ S" "b ∈ S" "c ∈ S"
  shows "(a *⇧S b) →⇧S c = a →⇧S (b →⇧S c)"
  using assms sum_residuation_one sum_residuation_not_one by blast

subsubsection‹Main result›

sublocale hoop "S" "(*⇧S)" "(→⇧S)" "1⇧S"
proof
  show "x *⇧S y ∈ S" if "x ∈ S" "y ∈ S" for x y
    using that sum_mult_closed by simp
next
  show "x →⇧S y ∈ S" if "x ∈ S" "y ∈ S" for x y
    using that sum_imp_closed by simp
next
  show "1⇧S ∈ S"
    by simp
next
  show "x *⇧S y = y *⇧S x" if "x ∈ S" "y ∈ S" for x y
    using that sum_mult_comm by simp
next
  show "x *⇧S (y *⇧S z) = (x *⇧S y) *⇧S z" if "x ∈ S" "y ∈ S" "z ∈ S" for x y z 
    using that sum_mult_assoc by simp
next
  show "x *⇧S 1⇧S = x" if "x ∈ S" for x
    using that sum_mult_neutr by simp
next
  show "x →⇧S x = 1⇧S" if "x ∈ S" for x
    using that sum_imp_reflex by simp
next
  show "x *⇧S (x →⇧S y) = y *⇧S (y →⇧S x)" if "x ∈ S" "y ∈ S" for x y
    using that sum_divisibility by simp
next
  show "x →⇧S (y →⇧S z) = (x *⇧S y) →⇧S z" if "x ∈ S" "y ∈ S" "z ∈ S" for x y z
    using that sum_residuation by simp
qed

end
                                         
end