# 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)"

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

lemma ascending_chain_directed:
"ascending_chain f ⟹ directed (range f)"

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)"

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)"

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

"descending_chain f ⟹ descending_chain (λn . x ⊔ f n)"
using descending_chain_def sup_right_isotone by blast

"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)"

lemma ascending_chain_right_mult:
"ascending_chain f ⟹ ascending_chain (λn . f n * x)"

lemma descending_chain_left_mult:
"descending_chain f ⟹ descending_chain (λn . x * f n)"

lemma descending_chain_right_mult:
"descending_chain f ⟹ descending_chain (λn . f n * x)"

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)

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)

lemma inf_INF:
"Y ≠ {} ⟹ inf x (INF y∈Y . f y) = (INF y∈Y. inf x (f y))"
apply (subst inf_Inf)

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)

lemma power_zero_id:
"f^0 = id"