Theory Base

(* Title:      Base
   Author:     Walter Guttmann
   Maintainer: Walter Guttmann <walter.guttmann at canterbury.ac.nz>
*)

section Base

theory Base

imports Stone_Relation_Algebras.Semirings

begin

nitpick_params [timeout = 600]

class while =
  fixes while :: "'a  'a  'a" (infixr "" 59)

class n =
  fixes n :: "'a  'a"

class diamond =
  fixes diamond :: "'a  'a  'a" ("| _ > _" [50,90] 95)

class box =
  fixes box :: "'a  'a  'a" ("| _ ] _" [50,90] 95)

context ord
begin

definition ascending_chain :: "(nat  'a)  bool"
  where "ascending_chain f  n . f n  f (Suc n)"

definition descending_chain :: "(nat  'a)  bool"
  where "descending_chain f  n . f (Suc n)  f n"

definition directed :: "'a set  bool"
  where "directed X  X  {}  (xX . yX . zX . x  z  y  z)"

definition co_directed :: "'a set  bool"
  where "co_directed X  X  {}  (xX . yX . zX . z  x  z  y)"

definition chain :: "'a set  bool"
  where "chain X  xX . yX . x  y  y  x"

end

context order
begin

lemma ascending_chain_k:
  "ascending_chain f  f m  f (m + k)"
  apply (induct k)
  apply simp
  using le_add1 lift_Suc_mono_le ord.ascending_chain_def by blast

lemma ascending_chain_isotone:
  "ascending_chain f  m  k  f m  f k"
  using lift_Suc_mono_le ord.ascending_chain_def by blast

lemma ascending_chain_comparable:
  "ascending_chain f  f k  f m  f m  f k"
  by (meson ascending_chain_isotone linear)

lemma ascending_chain_chain:
  "ascending_chain f  chain (range f)"
  by (simp add: ascending_chain_comparable chain_def)

lemma chain_directed:
  "X  {}  chain X  directed X"
  by (metis chain_def directed_def)

lemma ascending_chain_directed:
  "ascending_chain f  directed (range f)"
  by (simp add: ascending_chain_chain chain_directed)

lemma descending_chain_k:
  "descending_chain f  f (m + k)  f m"
  apply (induct k)
  apply simp
  using le_add1 lift_Suc_antimono_le ord.descending_chain_def by blast

lemma descending_chain_antitone:
  "descending_chain f  m  k  f k  f m"
  using descending_chain_def lift_Suc_antimono_le by blast

lemma descending_chain_comparable:
  "descending_chain f  f k  f m  f m  f k"
  by (meson descending_chain_antitone nat_le_linear)

lemma descending_chain_chain:
  "descending_chain f  chain (range f)"
  by (simp add: descending_chain_comparable chain_def)

lemma chain_co_directed:
  "X  {}  chain X  co_directed X"
  by (metis chain_def co_directed_def)

lemma descending_chain_codirected:
  "descending_chain f  co_directed (range f)"
  by (simp add: chain_co_directed descending_chain_chain)

end

context semilattice_sup
begin

lemma ascending_chain_left_sup:
  "ascending_chain f  ascending_chain (λn . x  f n)"
  using ascending_chain_def sup_right_isotone by blast

lemma ascending_chain_right_sup:
  "ascending_chain f  ascending_chain (λn . f n  x)"
  using ascending_chain_def sup_left_isotone by auto

lemma descending_chain_left_add:
  "descending_chain f  descending_chain (λn . x  f n)"
  using descending_chain_def sup_right_isotone by blast

lemma descending_chain_right_add:
  "descending_chain f  descending_chain (λn . f n  x)"
  using descending_chain_def sup_left_isotone by auto

primrec pSum0 :: "(nat  'a)  nat  'a"
  where "pSum0 f 0 = f 0"
      | "pSum0 f (Suc m) = pSum0 f m  f m"

lemma pSum0_below:
 "i . f i  x  pSum0 f m  x"
  apply (induct m)
  by auto

end

context non_associative_left_semiring
begin

lemma ascending_chain_left_mult:
  "ascending_chain f  ascending_chain (λn . x * f n)"
  by (simp add: mult_right_isotone ord.ascending_chain_def)

lemma ascending_chain_right_mult:
  "ascending_chain f  ascending_chain (λn . f n * x)"
  by (simp add: mult_left_isotone ord.ascending_chain_def)

lemma descending_chain_left_mult:
  "descending_chain f  descending_chain (λn . x * f n)"
  by (simp add: descending_chain_def mult_right_isotone)

lemma descending_chain_right_mult:
  "descending_chain f  descending_chain (λn . f n * x)"
  by (simp add: descending_chain_def mult_left_isotone)

end

context complete_lattice
begin

lemma sup_Sup:
  "A  {}  sup x (Sup A) = Sup ((sup x) ` A)"
  apply (rule order.antisym)
  apply (meson ex_in_conv imageI SUP_upper2 Sup_mono sup.boundedI sup_left_divisibility sup_right_divisibility)
  by (meson SUP_least Sup_upper sup_right_isotone)

lemma sup_SUP:
  "Y  {}  sup x (SUP yY . f y) = (SUP yY. sup x (f y))"
  apply (subst sup_Sup)
  by (simp_all add: image_image)

lemma inf_Inf:
  "A  {}  inf x (Inf A) = Inf ((inf x) ` A)"
  apply (rule order.antisym)
  apply (meson INF_greatest Inf_lower inf.sup_right_isotone)
  by (simp add: INF_inf_const1)

lemma inf_INF:
  "Y  {}  inf x (INF yY . f y) = (INF yY. inf x (f y))"
  apply (subst inf_Inf)
  by (simp_all add: image_image)

lemma SUP_image_id[simp]:
  "(SUP xf`A . x) = (SUP xA . f x)"
  by simp

lemma INF_image_id[simp]:
  "(INF xf`A . x) = (INF xA . f x)"
  by simp

end

lemma image_Collect_2:
  "f ` { g x | x . P x } = { f (g x) | x . P x }"
  by auto

text The following instantiation and four lemmas are from Jose Divason Mallagaray.

instantiation "fun" :: (type, type) power
begin

definition one_fun :: "'a  'a"
  where one_fun_def: "one_fun  id"

definition times_fun :: "('a  'a)  ('a  'a)  ('a  'a)"
  where times_fun_def: "times_fun  comp"

instance
  by intro_classes

end

lemma id_power:
  "id^m = id"
  apply (induct m)
  apply (simp add: one_fun_def)
  by (simp add: times_fun_def)

lemma power_zero_id:
  "f^0 = id"
  by (simp add: one_fun_def)

lemma power_succ_unfold:
  "f^Suc m = f  f^m"
  by (simp add: times_fun_def)

lemma power_succ_unfold_ext:
  "(f^Suc m) x = f ((f^m) x)"
  by (simp add: times_fun_def)

end