Quelle  RKAT.thy

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

subsection ‹Refinement Component›

theory RKAT
  imports "AVC_KAT/VC_KAT"

begin

subsubsection‹RKAT: Definition and Basic Properties›

text ‹A refinement KAT is a KAT expanded by Morgan's specification statement.›

class rkat = kat +
  fixes R :: "'a ==> 'a ==> 'a"
  assumes spec_def:  "x ≤ R p q ⟷ H p x q"

begin

lemma R1: "H p (R p q) q"
  using spec_def by blast

lemma R2: "H p x q ==> x ≤ R p q"
  by (simp add: spec_def)

subsubsection‹Propositional Refinement Calculus›

lemma R_skip: "1 ≤ R p p"
proof -
  have "H p 1 p"
    by (simp add: H_skip)
  thus ?thesis
    by (rule R2)
qed

lemma R_cons: "t p ≤ t p' ==> t q' ≤ t q ==> R p' q' ≤ R p q"
proof -
  assume h1: "t p ≤ t p'" and h2: "t q' ≤ t q"
  have "H p' (R p' q') q'"
    by (simp add: R1)
  hence "H p (R p' q') q"
    using h1 h2 H_cons_1 H_cons_2 by blast
  thus ?thesis
    by (rule R2)
qed

lemma R_seq: "(R p r) ⋅ (R r q) ≤ R p q"
proof -
  have "H p (R p r) r" and "H r (R r q) q"
    by (simp add: R1)+
  hence "H p ((R p r) ⋅ (R r q)) q"
    by (rule H_seq_swap)
  thus ?thesis
    by (rule R2)
qed

lemma R_cond: "if v then (R (t v ⋅ t p) q) else (R (n v ⋅ t p) q) fi ≤ R p q"
proof - 
  have "H (t v ⋅ t p) (R (t v ⋅ t p) q) q" and "H (n v ⋅ t p) (R (n v ⋅ t p) q) q"
    by (simp add: R1)+
  hence "H p (if v then (R (t v ⋅ t p) q) else (R (n v ⋅ t p) q) fi) q"
    by (simp add: H_cond n_mult_comm)
 thus ?thesis
    by (rule R2)
qed

lemma R_loop: "while q do (R (t p ⋅ t q) p) od ≤ R p (t p ⋅ n q)"
proof -
  have "H (t p ⋅ t q) (R (t p ⋅ t q) p) p" 
    by (simp_all add: R1)
  hence "H p (while q do (R (t p ⋅ t q) p) od) (t p ⋅ n q)"
    by (simp add: H_loop)
  thus ?thesis
    by (rule R2)
  qed

lemma R_zero_one: "x ≤ R 0 1"
proof -
  have "H 0 x 1"
    by (simp add: H_def)
  thus ?thesis
    by (rule R2)
qed

lemma R_one_zero: "R 1 0 = 0"
proof -
  have "H 1 (R 1 0) 0"
    by (simp add: R1)
  thus ?thesis
    by (simp add: H_def join.le_bot)
qed

end

end