Theory Refinement_Lattice

section ‹Refinement Lattice \label{S:lattice}›

theory Refinement_Lattice
imports
  Main
begin

unbundle lattice_syntax

text ‹
  The underlying lattice of commands is complete and distributive.
  We follow the refinement calculus tradition so that $\nondet$ 
  is non-deterministic choice and $c \refsto d$ means $c$ is refined 
  (or implemented) by $d$.
›

declare [[show_sorts]]

text ‹Remove existing notation for quotient as it interferes with the rely quotient›
no_notation Equiv_Relations.quotient  (infixl ‹'/'/› 90)

class refinement_lattice = complete_distrib_lattice
begin

text ‹The refinement lattice infimum corresponds to non-deterministic choice for commands.›

abbreviation
  refine :: "'a ⇒ 'a ⇒ bool" (infix ‹⊑› 50)
where
  "c ⊑ d ≡ less_eq c d"

abbreviation
  refine_strict :: "'a ⇒ 'a ⇒ bool" (infix ‹⊏› 50)
where
  "c ⊏ d ≡ less c d"

text ‹Non-deterministic choice is monotonic in both arguments›
lemma inf_mono_left: "a ⊑ b ⟹ a ⊓ c ⊑ b ⊓ c"
  using inf_mono by auto

lemma inf_mono_right: "c ⊑ d ⟹ a ⊓ c ⊑ a ⊓ d"
  using inf_mono by auto

text ‹Binary choice is a special case of choice over a set.›
lemma Inf2_inf: "⨅{ f x | x. x ∈ {c, d}} = f c ⊓ f d"
proof -
  have "{ f x | x. x ∈ {c, d}} = {f c, f d}" by blast
  then have "⨅{ f x | x. x ∈ {c, d}} = ⨅{f c, f d}" by simp
  also have "... = f c ⊓ f d" by simp
  finally show ?thesis .
qed

text ‹Helper lemma for choice over indexed set.›
lemma INF_Inf: "(⨅x∈X. f x) = (⨅{f x |x. x ∈ X})"
  by (simp add: Setcompr_eq_image)

lemma (in -) INF_absorb_args: "(⨅i j. (f::nat ⇒ 'c::complete_lattice) (i + j)) = (⨅k. f k)"
proof (rule order_class.order.antisym)
  show "(⨅k. f k) ≤ (⨅i j. f (i + j))"
    by (simp add: complete_lattice_class.INF_lower complete_lattice_class.le_INF_iff)
next
  have "⋀k. ∃i j. f (i + j) ≤ f k"
    by (metis Nat.add_0_right order_refl)
  then have "⋀k. ∃i. (⨅j. f (i + j)) ≤ f k"
    by (meson UNIV_I complete_lattice_class.INF_lower2)
  then show "(⨅i j. f (i + j)) ≤ (⨅k. f k)"
    by (simp add: complete_lattice_class.INF_mono)
qed

lemma (in -) nested_Collect: "{f y |y. y ∈ {g x |x. x ∈ X}} = {f (g x) |x. x ∈ X}"
  by blast

text ‹A transition lemma for INF distributivity properties, going from Inf to INF,
  qualified version followed by a straightforward one.›

lemma Inf_distrib_INF_qual:
  fixes f :: "'a ⇒ 'a ⇒ 'a"
  assumes qual: "P {d x |x. x ∈ X}"
  assumes f_Inf_distrib: "⋀c D. P D ⟹ f c (⨅ D) = ⨅ {f c d | d . d ∈ D }"
  shows "f c (⨅x∈X. d x) = (⨅x∈X. f c (d x))"
proof -
  have "f c (⨅x∈X. d x) = f c (⨅{d x |x. x ∈ X})" by (simp add: INF_Inf)
  also have "... = (⨅{f c dx |dx. dx ∈ {d x | x. x ∈ X}})" by (simp add: qual f_Inf_distrib)
  also have "... = (⨅{f c (d x) |x. x ∈ X})" by (simp only: nested_Collect)
  also have "... = (⨅x∈X. f c (d x))" by (simp add: INF_Inf)
  finally show ?thesis .
qed

lemma Inf_distrib_INF:
  fixes f :: "'a ⇒ 'a ⇒ 'a"
  assumes f_Inf_distrib: "⋀c D. f c (⨅ D) = ⨅ {f c d | d . d ∈ D }"
  shows "f c (⨅x∈X. d x) = (⨅x∈X. f c (d x))"
  by (simp add: Setcompr_eq_image f_Inf_distrib image_comp)

    
end

lemmas refine_trans = order.trans

text ‹More transitivity rules to make calculational reasoning smoother›
declare ord_eq_le_trans[trans]
declare ord_le_eq_trans[trans]
declare dual_order.trans[trans]


abbreviation
  dist_over_sup :: "('a::refinement_lattice ⇒ 'a) ⇒ bool"
where
  "dist_over_sup F ≡ (∀ X . F (⨆ X) = (⨆x∈X. F (x)))"

abbreviation
  dist_over_inf :: "('a::refinement_lattice ⇒ 'a) ⇒ bool"
where
  "dist_over_inf F ≡ (∀ X . F (⨅ X) = (⨅x∈X. F (x)))"

end