Theory RKAT_Models

(* Title: Models of Refinement KAT
   Author: Victor Gomes, Georg Struth
   Maintainer: Victor Gomes <victor.gomes@cl.cam.ac.uk>
               Georg Struth <g.struth@sheffield.ac.uk> 
*)

subsubsection ‹Models of Refinement KAT›

theory RKAT_Models
  imports RKAT
   
begin

text ‹So far only the relational model is developed.›

definition rel_R :: "'a rel ⇒ 'a rel ⇒ 'a rel" where 
  "rel_R P Q = ⋃{X. rel_kat.H P X Q}"

interpretation rel_rkat: rkat "(∪)" "(;)" Id "{}" "(⊆)" "(⊂)" rtrancl "(λX. Id ∩ - X)" rel_R
  by (standard, auto simp: rel_R_def rel_kat.H_def)

end