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 ≠ {} ∧ (∀x∈X . ∀y∈X . ∃z∈X . x ≤ z ∧ y ≤ z)"

definition co_directed :: "'a set ⇒ bool"
  where "co_directed X ≡ X ≠ {} ∧ (∀x∈X . ∀y∈X . ∃z∈X . z ≤ x ∧ z ≤ y)"

definition chain :: "'a set ⇒ bool"
  where "chain X ≡ ∀x∈X . ∀y∈X . 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 y∈Y . f y) = (SUP y∈Y. 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 y∈Y . f y) = (INF y∈Y. inf x (f y))"
  apply (subst inf_Inf)
  by (simp_all add: image_image)

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

lemma INF_image_id[simp]:
  "(INF x∈f`A . x) = (INF x∈A . 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