Theory Ordered_Semiring
theory Ordered_Semiring
imports
"HOL-Algebra.Ring"
"Abstract-Rewriting.SN_Orders"
begin
record 'a ordered_semiring = "'a ring" +
geq :: "'a ⇒ 'a ⇒ bool" (infix "≽ı" 50)
gt :: "'a ⇒ 'a ⇒ bool" (infix "≻ı" 50)
max :: "'a ⇒ 'a ⇒ 'a" ("Maxı")
lemmas ordered_semiring_record_simps = ring_record_simps ordered_semiring.simps
locale ordered_semiring = semiring +
assumes compat: "⟦s ≽ (t :: 'a); t ≻ u; s ∈ carrier R; t ∈ carrier R; u ∈ carrier R⟧ ⟹ s ≻ u"
and compat2: "⟦s ≻ (t :: 'a); t ≽ u; s ∈ carrier R ; t ∈ carrier R; u ∈ carrier R⟧ ⟹ s ≻ u"
and plus_left_mono: "⟦x ≽ y; x ∈ carrier R; y ∈ carrier R; z ∈ carrier R⟧ ⟹ x ⊕ z ≽ y ⊕ z"
and times_left_mono: "⟦z ≽ 𝟬; x ≽ y; x ∈ carrier R; y ∈ carrier R; z ∈ carrier R⟧ ⟹ x ⊗ z ≽ y ⊗ z"
and times_right_mono: "⟦x ≽ 𝟬; y ≽ z; x ∈ carrier R; y ∈ carrier R; z ∈ carrier R⟧ ⟹ x ⊗ y ≽ x ⊗ z"
and geq_refl: "x ∈ carrier R ⟹ x ≽ x"
and geq_trans[trans]: "⟦x ≽ y; y ≽ z; x ∈ carrier R; y ∈ carrier R; z ∈ carrier R⟧ ⟹ x ≽ z"
and gt_trans[trans]: "⟦x ≻ y; y ≻ z; x ∈ carrier R; y ∈ carrier R; z ∈ carrier R⟧ ⟹ x ≻ z"
and gt_imp_ge: "x ≻ y ⟹ x ∈ carrier R ⟹ y ∈ carrier R ⟹ x ≽ y"
and max_comm: "x ∈ carrier R ⟹ y ∈ carrier R ⟹ Max x y = Max y x"
and max_ge: "x ∈ carrier R ⟹ y ∈ carrier R ⟹ Max x y ≽ x"
and max_id: "x ∈ carrier R ⟹ y ∈ carrier R ⟹ x ≽ y ⟹ Max x y = x"
and max_mono: "x ≽ y ⟹ x ∈ carrier R ⟹ y ∈ carrier R ⟹ z ∈ carrier R ⟹ Max z x ≽ Max z y"
and wf_max[simp, intro]: "x ∈ carrier R ⟹ y ∈ carrier R ⟹ Max x y ∈ carrier R"
and one_geq_zero: "𝟭 ≽ 𝟬"
begin
lemma max_ge_right: assumes x: "x ∈ carrier R" and y: "y ∈ carrier R" shows "Max x y ≽ y"
by (unfold max_comm[OF x y], rule max_ge[OF y x])
lemma wf_max0: "x ∈ carrier R ⟹ Max 𝟬 x ∈ carrier R" using wf_max[of 𝟬 x] by auto
lemma max0_id_pos: assumes x: "x ≽ 𝟬" and wf: "x ∈ carrier R"
shows "Max 𝟬 x = x" unfolding max_comm[OF zero_closed wf] by (rule max_id[OF wf zero_closed x])
end
hide_const (open) gt geq max
subsection ‹A connection between class based semirings and set based semirings›
definition class_semiring :: "'a itself ⇒ 'b ⇒ ('a :: {plus,times,one,zero},'b)ring_scheme" where
"class_semiring _ b ≡ ⦇ carrier = UNIV, mult = (*), one = 1, zero = 0, add = (+), … = b⦈"
lemma class_semiring: "semiring (class_semiring (TYPE('a :: ordered_semiring_1)) b)"
unfolding class_semiring_def
by (unfold_locales, auto simp: field_simps)
definition class_ordered_semiring :: "'a itself ⇒ ('a :: ordered_semiring_1 ⇒ 'a ⇒ bool) ⇒ 'b ⇒ ('a,'b) ordered_semiring_scheme" where
"class_ordered_semiring a gt b ≡ class_semiring a ⦇
ordered_semiring.geq = (≥),
gt = gt,
max = max,
… = b⦈"
lemma class_ordered_semiring: assumes "order_pair (gt :: ('a :: ordered_semiring_1 ⇒ 'a ⇒ bool)) d"
shows "ordered_semiring
(class_ordered_semiring (TYPE('a)) gt b)"
(is "ordered_semiring ?R")
proof -
interpret order_pair gt d by fact
interpret semiring ?R unfolding class_ordered_semiring_def by (rule class_semiring)
show ?thesis
by (unfold_locales, unfold class_ordered_semiring_def class_semiring_def, auto
intro: compat compat2 gt_imp_ge ge_trans max_comm max_id max_mono ge_refl one_ge_zero
times_left_mono times_right_mono plus_left_mono)
qed
lemma (in one_mono_ordered_semiring_1) class_ordered_semiring:
"ordered_semiring
(class_ordered_semiring (TYPE('a)) (≻) b)"
by (rule class_ordered_semiring[of _ default], unfold_locales)
lemma (in both_mono_ordered_semiring_1) class_ordered_semiring:
"ordered_semiring
(class_ordered_semiring (TYPE('a)) (≻) b)"
by (rule class_ordered_semiring[of _ default], unfold_locales)
end