# Theory Approximation

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

section ‹Approximation›

theory Approximation

imports Stone_Kleene_Relation_Algebras.Iterings

begin

nitpick_params [timeout = 600]

class apx =
fixes apx :: "'a ⇒ 'a ⇒ bool" (infix "⊑" 50)

class apx_order = apx +
assumes apx_reflexive: "x ⊑ x"
assumes apx_antisymmetric: "x ⊑ y ∧ y ⊑ x ⟶ x = y"
assumes apx_transitive: "x ⊑ y ∧ y ⊑ z ⟶ x ⊑ z"

sublocale apx_order < apx: order where less_eq = apx and less = "λx y . x ⊑ y ∧ ¬ y ⊑ x"
apply unfold_locales
apply simp
apply (rule apx_reflexive)
using apx_transitive apply blast

context apx_order
begin

abbreviation the_apx_least_fixpoint    :: "('a ⇒ 'a) ⇒ 'a" ("κ _" [201] 200)  where "κ  f ≡ apx.the_least_fixpoint f"
abbreviation the_apx_least_prefixpoint :: "('a ⇒ 'a) ⇒ 'a" ("pκ _" [201] 200) where "pκ f ≡ apx.the_least_prefixpoint f"

definition is_apx_meet  :: "'a ⇒ 'a ⇒ 'a ⇒ bool"          where "is_apx_meet x y z ≡ z ⊑ x ∧ z ⊑ y ∧ (∀w . w ⊑ x ∧ w ⊑ y ⟶ w ⊑ z)"
definition has_apx_meet :: "'a ⇒ 'a ⇒ bool"                where "has_apx_meet x y ≡ ∃z . is_apx_meet x y z"
definition the_apx_meet :: "'a ⇒ 'a ⇒ 'a" (infixl "△" 66) where "x △ y ≡ THE z . is_apx_meet x y z"

lemma apx_meet_unique:
"has_apx_meet x y ⟹ ∃!z . is_apx_meet x y z"
by (meson apx_antisymmetric has_apx_meet_def is_apx_meet_def)

lemma apx_meet:
assumes "has_apx_meet x y"
shows "is_apx_meet x y (x △ y)"
proof -
have "is_apx_meet x y (THE z . is_apx_meet x y z)"
by (metis apx_meet_unique assms theI)
thus ?thesis
qed

lemma apx_greatest_lower_bound:
"has_apx_meet x y ⟹ (w ⊑ x ∧ w ⊑ y ⟷ w ⊑ x △ y)"
by (meson apx_meet apx_transitive is_apx_meet_def)

lemma apx_meet_same:
"is_apx_meet x y z ⟹ z = x △ y"
using apx_meet apx_meet_unique has_apx_meet_def by blast

lemma apx_meet_char:
"is_apx_meet x y z ⟷ has_apx_meet x y ∧ z = x △ y"
using apx_meet_same has_apx_meet_def by auto

end

class apx_biorder = apx_order + order
begin

lemma mu_below_kappa:
"has_least_fixpoint f ⟹ apx.has_least_fixpoint f ⟹ μ f ≤ κ f"
using apx.mu_unfold is_least_fixpoint_def least_fixpoint by auto

lemma kappa_below_nu:
"has_greatest_fixpoint f ⟹ apx.has_least_fixpoint f ⟹ κ f ≤ ν f"
by (meson apx.mu_unfold greatest_fixpoint is_greatest_fixpoint_def)

lemma kappa_apx_below_mu:
"has_least_fixpoint f ⟹ apx.has_least_fixpoint f ⟹ κ f ⊑ μ f"
using apx.is_least_fixpoint_def apx.least_fixpoint mu_unfold by auto

lemma kappa_apx_below_nu:
"has_greatest_fixpoint f ⟹ apx.has_least_fixpoint f ⟹ κ f ⊑ ν f"
by (metis apx.is_least_fixpoint_def apx.least_fixpoint nu_unfold)

end

class apx_semiring = apx_biorder + idempotent_left_semiring + L +
assumes apx_L_least: "L ⊑ x"
assumes sup_apx_left_isotone: "x ⊑ y ⟶ x ⊔ z ⊑ y ⊔ z"
assumes mult_apx_left_isotone: "x ⊑ y ⟶ x * z ⊑ y * z"
assumes mult_apx_right_isotone: "x ⊑ y ⟶ z * x ⊑ z * y"
begin

lemma sup_apx_right_isotone:
"x ⊑ y ⟹ z ⊔ x ⊑ z ⊔ y"

lemma sup_apx_isotone:
"w ⊑ y ⟹ x ⊑ z ⟹ w ⊔ x ⊑ y ⊔ z"
by (meson apx_transitive sup_apx_left_isotone sup_apx_right_isotone)

lemma mult_apx_isotone:
"w ⊑ y ⟹ x ⊑ z ⟹ w * x ⊑ y * z"
by (meson apx_transitive mult_apx_left_isotone mult_apx_right_isotone)

lemma affine_apx_isotone:
"apx.isotone (λx . y * x ⊔ z)"
by (simp add: apx.isotone_def mult_apx_right_isotone sup_apx_left_isotone)

end

end

```