Theory Matrix.Ordered_Semiring

(*  Title:       Executable Matrix Operations on Matrices of Arbitrary Dimensions
    Author:      Christian Sternagel <christian.sternagel@uibk.ac.at>
                 René Thiemann       <rene.thiemann@uibk.ac.at>
    Maintainer:  Christian Sternagel and René Thiemann
    License:     LGPL
*)

(*
Copyright 2013 Christian Sternagel, René Thiemann

This file is part of IsaFoR/CeTA.

IsaFoR/CeTA is free software: you can redistribute it and/or modify it under the
terms of the GNU Lesser General Public License as published by the Free Software
Foundation, either version 3 of the License, or (at your option) any later
version.

IsaFoR/CeTA is distributed in the hope that it will be useful, but WITHOUT ANY
WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A
PARTICULAR PURPOSE.  See the GNU Lesser General Public License for more details.

You should have received a copy of the GNU Lesser General Public License along
with IsaFoR/CeTA. If not, see <http://www.gnu.org/licenses/>.
*)
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