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
  by (simp add: apx_antisymmetric)

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
    by (simp add: the_apx_meet_def)
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"
  by (simp add: sup_apx_left_isotone sup_commute)

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