Theory Approximation

(* Title:      Approximation
   Author:     Walter Guttmann
   Maintainer: Walter Guttmann <walter.guttmann at>

section ‹Approximation›

theory Approximation

imports Stone_Kleene_Relation_Algebras.Iterings


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

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" (" _" [201] 200) where " 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)

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


class apx_biorder = apx_order + order

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)


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"

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)