Theory 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