Quelle  Hoops.thy

section‹Hoops›

text‹A @{text hoop} is a naturally ordered @{text "pocrim"} (i.e., a partially ordered commutative
 residuated integral monoid). This structures have been introduced by Büchi and Owens in cite‹"BUCHI1975"›
  constitute the algebraic counterpart of fragments without negation and falsum of some nonclassical logics.›

theory Hoops
  imports Posets
begin

subsection‹Definitions›

locale hoop =
  fixes universe :: "'a set" (‹A›)
  and multiplication :: "'a ==> 'a ==> 'a" (infix ‹*^A› 60)
  and implication :: "'a ==> 'a ==> 'a" (infix ‹→^A› 60)
  and one :: 'a (‹1^A›)
  assumes mult_closed: "x ∈ A ==> y ∈ A ==> x *^A y ∈ A"
  and imp_closed: "x ∈ A ==> y ∈ A ==> x →^A y ∈ A"
  and one_closed [simp]: "1^A ∈ A"
  and mult_comm:  "x ∈ A ==> y ∈ A ==> x *^A y = y *^A x"
  and mult_assoc: "x ∈ A ==> y ∈ A ==> z ∈ A ==> x *^A (y *^A z) = (x *^A y) *^A z"
  and mult_neutr [simp]: "x ∈ A ==> x *^A 1^A = x" 
  and imp_reflex [simp]: "x ∈ A ==> x →^A x = 1^A" 
  and divisibility: "x ∈ A ==> y ∈ A ==> x *^A (x →^A y) = y *^A (y →^A x)" 
  and residuation: "x ∈ A ==> y ∈ A ==> z ∈ A ==>
                    x →^A (y →^A z) = (x *^A y) →^A z"
begin

definition hoop_order :: "'a ==> 'a ==> bool" (infix ‹≤^A› 60)
  where "x ≤^A y ≡ (x →^A y = 1^A)" 

definition hoop_order_strict :: "'a ==> 'a ==> bool" (infix ‹<\<^sup>A› 60)
  where "x <^A y ≡ (x ≤^A y ∧ x ≠ y)"

definition hoop_inf :: "'a ==> 'a ==> 'a" (infix ‹∧^A› 60)
  where "x ∧^A y = x *^A (x →^A y)"

definition hoop_pseudo_sup :: "'a ==> 'a ==> 'a" (infix ‹∨^*A› 60)
  where "x ∨^*A y = ((x →^A y) →^A y) ∧^A ((y →^A x) →^A x)" 

end

locale wajsberg_hoop = hoop +
  assumes T: "x ∈ A ==> y ∈ A ==> (x →^A y) →^A y = (y →^A x) →^A x"
begin

definition wajsberg_hoop_sup :: "'a ==> 'a ==> 'a" (infix ‹∨^A› 60)
  where "x ∨^A y = (x →^A y) →^A y"

end

subsection‹Basic properties›

context hoop
begin

lemma mult_neutr_2 [simp]: 
  assumes "a ∈ A"
  shows "1^A *^A a = a"
  using assms mult_comm by simp

lemma imp_one_A:
  assumes "a ∈ A"
  shows "(1^A →^A a) →^A 1^A = 1^A"
proof -
  have "(1^A →^A a) →^A 1^A = (1^A →^A a) →^A (1^A →^A 1^A)"
    using assms by simp
  also
  have "… = ((1^A →^A a) *^A 1^A) →^A 1^A"
    using assms imp_closed residuation by simp
  also
  have "… = ((a →^A 1^A) *^A a) →^A 1^A"
    using assms divisibility imp_closed mult_comm by simp
  also
  have "… = (a →^A 1^A) →^A (a →^A 1^A)"
    using assms imp_closed one_closed residuation by metis
  also
  have "… = 1^A"
    using assms imp_closed by simp
  finally
  show ?thesis 
    by auto
qed

lemma imp_one_B:
  assumes "a ∈ A"
  shows "(1^A →^A a) →^A a = 1^A"
proof -
  have "(1^A →^A a) →^A a = ((1^A →^A a) *^A 1^A) →^A a"
    using assms imp_closed by simp
  also
  have "… = (1^A →^A a) →^A (1^A →^A a)" 
    using assms imp_closed one_closed residuation by metis
  also
  have "… = 1^A"
    using assms imp_closed by simp
  finally
  show ?thesis
    by auto
qed

lemma imp_one_C:
  assumes "a ∈ A"
  shows "1^A →^A a = a" 
proof -
  have "1^A →^A a = (1^A →^A a) *^A 1^A" 
    using assms imp_closed by simp
  also
  have "… = (1^A →^A a) *^A ((1^A →^A a) →^A a)" 
    using assms imp_one_B by simp
  also
  have "… = a *^A (a →^A (1^A →^A a))" 
    using assms divisibility imp_closed by simp
  also
  have "… = a" 
    using assms residuation by simp
  finally
  show ?thesis
    by auto
qed

lemma imp_one_top:
  assumes "a ∈ A"
  shows "a →^A 1^A = 1^A"
proof -
  have "a →^A 1^A = (1^A →^A a) →^A 1^A"
    using assms imp_one_C by auto
  also
  have "… = 1^A"
    using assms imp_one_A by auto
  finally
  show ?thesis
    by auto
qed

text‹The proofs of @{thm [source] imp_one_A}, @{thm [source] imp_one_B}, @{thm [source] imp_one_C}
  @{thm [source] imp_one_top} are based on proofs found in cite‹"BOSBACH1969"›
 (see Section 1: (4), (6), (7) and (12)).›
 
lemma swap: 
  assumes "a ∈ A" "b ∈ A" "c ∈ A"
  shows "a →^A (b →^A c) = b →^A (a →^A c)"
proof -
  have "a →^A (b →^A c) = (a *^A b) →^A c"
    using assms residuation by auto
  also
  have "… = (b *^A a) →^A c"
    using assms mult_comm by auto
  also
  have "… = b →^A (a →^A c)"
    using assms residuation by auto
  finally
  show ?thesis
    by auto
qed

lemma imp_A:
  assumes "a ∈ A" "b ∈ A"
  shows "a →^A (b →^A a) = 1^A"
proof -
  have "a →^A (b →^A a) = b →^A (a →^A a)"
    using assms swap by blast
  then
  show ?thesis
    using assms imp_one_top by simp
qed

subsection‹Multiplication monotonicity›

lemma mult_mono:
  assumes "a ∈ A" "b ∈ A" "c ∈ A"
  shows "(a →^A b) →^A ((a *^A c) →^A (b *^A c)) = 1^A"
proof -
  have "(a →^A b) →^A ((a *^A c) →^A (b *^A c)) =
        (a →^A b) →^A (a →^A (c →^A (b *^A c)))"
    using assms mult_closed residuation by auto
  also
  have "… = ((a →^A b) *^A a) →^A (c →^A (b *^A c))"
    using assms imp_closed mult_closed residuation by metis
  also
  have "… = ((b →^A a) *^A b) →^A (c →^A (b *^A c))"
    using assms divisibility imp_closed mult_comm by simp
  also
  have "… = (b →^A a) →^A (b →^A (c →^A (b *^A c)))"
    using assms imp_closed mult_closed residuation by metis
  also
  have "… = (b →^A a) →^A ((b *^A c) →^A (b *^A c))" 
    using assms(2,3) mult_closed residuation by simp
  also
  have "… = 1^A"
    using assms imp_closed imp_one_top mult_closed by simp
  finally
  show ?thesis
    by auto
qed

subsection‹Implication monotonicity and anti-monotonicity›

lemma imp_mono:
  assumes "a ∈ A" "b ∈ A" "c ∈ A"
  shows "(a →^A b) →^A ((c →^A a) →^A (c →^A b)) = 1^A"
proof -
  have "(a →^A b) →^A ((c →^A a) →^A (c →^A b)) =
        (a →^A b) →^A (((c →^A a) *^A c) →^A b)" 
    using assms imp_closed residuation by simp
  also
  have "… = (a →^A b) →^A (((a →^A c) *^A a) →^A b)" 
    using assms divisibility imp_closed mult_comm by simp
  also
  have "… = (a →^A b) →^A ((a →^A c) →^A (a →^A b))" 
    using assms imp_closed residuation by simp
  also
  have "… = 1^A" 
    using assms imp_A imp_closed by simp
  finally
  show ?thesis
    by auto
qed

lemma imp_anti_mono:
  assumes "a ∈ A" "b ∈ A" "c ∈ A"
  shows "(a →^A b) →^A ((b →^A c) →^A (a →^A c)) = 1^A"
  using assms imp_closed imp_mono swap by metis

subsection‹@{term hoop_order} defines a partial order over @{term A}›

lemma ord_reflex: 
  assumes "a ∈ A"
  shows "a ≤^A a"
  using assms hoop_order_def by simp

lemma ord_trans:
  assumes "a ∈ A" "b ∈ A" "c ∈ A" "a ≤^A b" "b ≤^A c"
  shows "a ≤^A c"
proof -
  have "a →^A c = 1^A →^A (1^A →^A (a →^A c))"
    using assms(1,3) imp_closed imp_one_C by simp
  also
  have "… = (a →^A b) →^A ((b →^A c) →^A (a →^A c))"
    using assms(4,5) hoop_order_def by simp
  also
  have "… = 1^A"
    using assms(1-3) imp_anti_mono by simp
  finally
  show ?thesis
    using hoop_order_def by auto
qed

lemma ord_antisymm:
  assumes "a ∈ A" "b ∈ A" "a ≤^A b" "b ≤^A a"
  shows "a = b"
proof -
  have "a = a *^A (a →^A b)"
    using assms(1,3) hoop_order_def by simp
  also
  have "… = b *^A (b →^A a)" 
    using assms(1,2) divisibility by simp
  also
  have "… = b"
    using assms(2,4) hoop_order_def by simp
  finally
  show ?thesis
    by auto
qed

lemma ord_antisymm_equiv:
  assumes "a ∈ A" "b ∈ A" "a →^A b = 1^A" "b →^A a = 1^A"
  shows "a = b"
  using assms hoop_order_def ord_antisymm by auto

lemma ord_top:
  assumes "a ∈ A"
  shows "a ≤^A 1^A"
  using assms hoop_order_def imp_one_top by simp

sublocale top_poset_on "A" "(≤^A)" "(<^A)" "1^A"
proof
  show "A ≠ ∅"
    using one_closed by blast
next
  show "reflp_on A (≤^A)"
    using ord_reflex reflp_onI by blast
next
  show "antisymp_on A (≤^A)"
    using antisymp_onI ord_antisymm by blast
next 
  show "transp_on A (≤^A)"
    using ord_trans transp_onI by blast
next
  show "x <^A y = (x ≤^A y ∧ x ≠ y)" if "x ∈ A" "y ∈ A" for x y
    using hoop_order_strict_def by blast
next
  show "1^A ∈ A"
    by simp
next
  show "x ≤^A 1^A" if "x ∈ A" for x
    using ord_top that by simp
qed
 
subsection‹Order properties›

lemma ord_mult_mono_A:
  assumes "a ∈ A" "b ∈ A" "c ∈ A"
  shows "(a →^A b) ≤^A ((a *^A c) →^A (b *^A c))"
  using assms hoop_order_def mult_mono by simp

lemma ord_mult_mono_B:
  assumes "a ∈ A" "b ∈ A" "c ∈ A" "a ≤^A b"
  shows "(a *^A c) ≤^A (b *^A c)"
  using assms hoop_order_def imp_one_C swap mult_closed mult_mono top_closed
  by metis

lemma ord_residuation:
  assumes "a ∈ A" "b ∈ A" "c ∈ A"
  shows "(a *^A b) ≤^A c ⟷ a ≤^A (b →^A c)"
  using assms hoop_order_def residuation by simp

lemma ord_imp_mono_A:
  assumes "a ∈ A" "b ∈ A" "c ∈ A"
  shows "(a →^A b) ≤^A ((c →^A a) →^A (c →^A b))"
  using assms hoop_order_def imp_mono by simp

lemma ord_imp_mono_B:
  assumes "a ∈ A" "b ∈ A" "c ∈ A" "a ≤^A b"
  shows "(c →^A a) ≤^A (c →^A b)"
  using assms imp_closed ord_trans ord_reflex ord_residuation mult_closed
  by metis

lemma ord_imp_anti_mono_A:
  assumes "a ∈ A" "b ∈ A" "c ∈ A"
  shows "(a →^A b) ≤^A ((b →^A c) →^A (a →^A c))"
  using assms hoop_order_def imp_anti_mono by simp

lemma ord_imp_anti_mono_B:
  assumes "a ∈ A" "b ∈ A" "c ∈ A" "a ≤^A b"
  shows "(b →^A c) ≤^A (a →^A c)"
  using assms hoop_order_def imp_one_C swap ord_imp_mono_A top_closed
  by metis

lemma ord_A:
  assumes "a ∈ A" "b ∈ A"
  shows "b ≤^A (a →^A b)"
  using assms hoop_order_def imp_A by simp

lemma ord_B:
  assumes "a ∈ A" "b ∈ A"
  shows "b ≤^A ((a →^A b) →^A b)"
  using assms imp_closed ord_A by simp

lemma ord_C:
  assumes "a ∈ A" "b ∈ A"
  shows "a ≤^A ((a →^A b) →^A b)"
  using assms imp_one_C one_closed ord_imp_anti_mono_A by metis

lemma ord_D:
  assumes "a ∈ A" "b ∈ A" "a <^A b"
  shows "b →^A a ≠ 1^A"
  using assms hoop_order_def hoop_order_strict_def ord_antisymm by auto

subsection‹Additional multiplication properties›

lemma mult_lesseq_inf:
  assumes "a ∈ A" "b ∈ A"
  shows "(a *^A b) ≤^A (a ∧^A b)"
proof -
  have "b ≤^A (a →^A b)"
    using assms ord_A by simp
  then
  have "(a *^A b) ≤^A (a *^A (a →^A b))"
    using assms imp_closed ord_mult_mono_B mult_comm by metis
  then
  show ?thesis
    using hoop_inf_def by metis
qed

lemma mult_A:
  assumes "a ∈ A" "b ∈ A"
  shows "(a *^A b) ≤^A a"
  using assms ord_A ord_residuation by simp

lemma mult_B:
  assumes "a ∈ A" "b ∈ A"
  shows "(a *^A b) ≤^A b"
  using assms mult_A mult_comm by metis

lemma mult_C:
  assumes "a ∈ A-{1^A}" "b ∈ A-{1^A}"
  shows "a *^A b ∈ A-{1^A}"
  using assms ord_antisymm ord_top mult_A mult_closed by force

subsection‹Additional implication properties›

lemma imp_B:
  assumes "a ∈ A" "b ∈ A"
  shows "a →^A b = ((a →^A b) →^A b) →^A b"
proof -
  have "a ≤^A ((a →^A b) →^A b)"
    using assms ord_C by simp
  then 
  have "(((a →^A b) →^A b) →^A b) ≤^A (a →^A b)"
    using assms imp_closed ord_imp_anti_mono_B by simp
  moreover
  have "(a →^A b) ≤^A (((a →^A b) →^A b) →^A b)"
    using assms imp_closed ord_C by simp
  ultimately
  show ?thesis
    using assms imp_closed ord_antisymm by simp
qed

text‹The following two results can be found in cite‹"BLOK2000"› (see Proposition 1.7 and 2.2).›

lemma imp_C:
  assumes "a ∈ A" "b ∈ A"
  shows "(a →^A b) →^A (b →^A a) = b →^A a"
proof -
  have "a ≤^A ((a →^A b) →^A a)"
    using assms imp_closed ord_A by simp
  then
  have "(((a →^A b) →^A a) →^A b) ≤^A (a →^A b)"
    using assms imp_closed ord_imp_anti_mono_B by simp
  moreover 
  have "(a →^A b) ≤^A (((a →^A b) →^A a) →^A a)"
    using assms imp_closed ord_C by simp
  ultimately
  have "(((a →^A b) →^A a) →^A b) ≤^A (((a →^A b) →^A a) →^A a)"
    using assms imp_closed ord_trans by meson
  then
  have "((((a →^A b) →^A a) →^A b) *^A ((a →^A b) →^A a)) ≤^A a"
    using assms imp_closed ord_residuation by simp
  then
  have "((b →^A ((a →^A b) →^A a)) *^A b) ≤^A a"
    using assms divisibility imp_closed mult_comm by simp
  then
  have "(b →^A ((a →^A b) →^A a)) ≤^A (b →^A a)"
    using assms imp_closed ord_residuation by simp
  then 
  have "((a →^A b) →^A (b →^A a)) ≤^A (b →^A a)"
    using assms imp_closed swap by simp
  moreover
  have "(b →^A a) ≤^A ((a →^A b) →^A (b →^A a))"
    using assms imp_closed ord_A by simp
  ultimately
  show ?thesis
    using assms imp_closed ord_antisymm by auto
qed

lemma imp_D:
  assumes "a ∈ A" "b ∈ A"
  shows "(((b →^A a) →^A a) →^A b) →^A (b →^A a) = b →^A a"
proof -
  have "(((b →^A a) →^A a) →^A b) →^A (b →^A a) =
        (((b →^A a) →^A a) →^A b) →^A (((b →^A a) →^A a) →^A a)" 
    using assms imp_B by simp
  also
  have "… = ((((b →^A a) →^A a) →^A b) *^A ((b →^A a) →^A a)) →^A a" 
    using assms imp_closed residuation by simp
  also
  have "… = ((b →^A ((b →^A a) →^A a)) *^A b) →^A a" 
    using assms divisibility imp_closed mult_comm by simp
  also
  have "… = (1^A *^A b) →^A a"
    using assms hoop_order_def ord_C by simp
  also
  have "… = b →^A a"
    using assms(2) mult_neutr_2 by simp
  finally
  show ?thesis
    by auto
qed

subsection‹@{term hoop_inf} defines a semilattice over @{term A}›

lemma inf_closed:
  assumes "a ∈ A" "b ∈ A"
  shows "a ∧^A b ∈ A"
  using assms hoop_inf_def imp_closed mult_closed by simp

lemma inf_comm:
  assumes "a ∈ A" "b ∈ A"
  shows "a ∧^A b = b ∧^A a"
  using assms divisibility hoop_inf_def by simp

lemma inf_A:
  assumes "a ∈ A" "b ∈ A"
  shows "(a ∧^A b) ≤^A a"
proof -
  have "(a ∧^A b) →^A a = (a *^A (a →^A b)) →^A a"
    using hoop_inf_def by simp
  also
  have "… = (a →^A b) →^A (a →^A a)"
    using assms mult_comm imp_closed residuation by metis
  finally
  show ?thesis
    using assms hoop_order_def imp_closed imp_one_top by simp
qed

lemma inf_B:
  assumes "a ∈ A" "b ∈ A"
  shows "(a ∧^A b) ≤^A b" 
  using assms inf_comm inf_A by metis

lemma inf_C:
  assumes "a ∈ A" "b ∈ A" "c ∈ A" "a ≤^A b" "a ≤^A c"
  shows "a ≤^A (b ∧^A c)"
proof -
  have "(b →^A a) ≤^A (b →^A c)"
    using assms(1-3,5) ord_imp_mono_B by simp
  then
  have "(b *^A (b →^A a)) ≤^A (b *^A (b →^A c))"
    using assms imp_closed ord_mult_mono_B mult_comm by metis
  moreover
  have "a = b *^A (b →^A a)"
    using assms(1-3,4) divisibility hoop_order_def mult_neutr by simp
  ultimately
  show ?thesis
    using hoop_inf_def by auto
qed

lemma inf_order: 
  assumes "a ∈ A" "b ∈ A"
  shows "a ≤^A b ⟷ (a ∧^A b = a)"
  using assms hoop_inf_def hoop_order_def inf_B mult_neutr by metis

subsection‹Properties of @{term hoop_pseudo_sup}›

lemma pseudo_sup_closed:
  assumes "a ∈ A" "b ∈ A"
  shows "a ∨^*A b ∈ A"
  using assms hoop_pseudo_sup_def imp_closed inf_closed by simp

lemma pseudo_sup_comm:
  assumes "a ∈ A" "b ∈ A"
  shows "a ∨^*A b = b ∨^*A a"
  using assms hoop_pseudo_sup_def imp_closed inf_comm by auto

lemma pseudo_sup_A:
  assumes "a ∈ A" "b ∈ A"
  shows "a ≤^A (a ∨^*A b)"
  using assms hoop_pseudo_sup_def imp_closed inf_C ord_B ord_C by simp

lemma pseudo_sup_B:
  assumes "a ∈ A" "b ∈ A"
  shows "b ≤^A (a ∨^*A b)"
  using assms pseudo_sup_A pseudo_sup_comm by metis

lemma pseudo_sup_order:
  assumes "a ∈ A" "b ∈ A"
  shows "a ≤^A b ⟷ a ∨^*A b = b"
proof
  assume "a ≤^A b"
  then 
  have "a ∨^*A b = b ∧^A ((b →^A a) →^A a)"
    using assms(2) hoop_order_def hoop_pseudo_sup_def imp_one_C by simp
  also
  have "… = b"
    using assms imp_closed inf_order ord_C by meson
  finally
  show "a ∨^*A b = b"
    by auto
next
  assume "a ∨^*A b = b"
  then
  show "a ≤^A b"
    using assms pseudo_sup_A by metis
qed

end

end