Theory WordRefine

section ‹Machine Words›
theory WordRefine
imports "../Refine_Monadic" "HOL-Library.Word"
begin

text ‹This theory provides a simple example to show refinement of natural
  numbers to machine words. The setup is not yet very elaborated, but shows 
  the direction to go.
›

subsection ‹Setup›
definition [simp]: "word_nat_rel ≡ build_rel (unat) (λ_. True)"
lemma word_nat_RELEATES[refine_dref_RELATES]: 
  "RELATES word_nat_rel" by (simp add: RELATES_def)

lemma [simp, relator_props]: 
  "single_valued word_nat_rel" unfolding word_nat_rel_def
  by blast

lemma [simp]: "single_valuedp (λc a. a = unat c)" 
  by (rule single_valuedpI) blast

lemma [simp, relator_props]: "single_valued (converse word_nat_rel)" 
  by (auto intro: injI)

lemmas [refine_hsimp] = 
  word_less_nat_alt word_le_nat_alt unat_sub iffD1[OF unat_add_lem]

subsection ‹Example›
type_synonym word32 = "32 word"

definition test :: "nat ⇒ nat ⇒ nat set nres" where "test x0 y0 ≡ do {
  let S={};
  (S,_,_) ← WHILE (λ(S,x,y). x>0) (λ(S,x,y). do {
    let S=S∪{y};
    let x=x - 1;
    ASSERT (y<x0+y0);
    let y=y + 1;
    RETURN (S,x,y)
  }) (S,x0,y0);
  RETURN S
}"

lemma "y0>0 ⟹ test x0 y0 ≤ SPEC (λS. S={y0 .. y0 + x0 - 1})"
  ― ‹Choosen pre-condition to get least trouble when proving›
  unfolding test_def
  apply (intro WHILE_rule[where I="λ(S,x,y). 
    x+y=x0+y0 ∧ x≤x0 ∧
    S={y0 .. y0 + (x0-x) - 1}"] 
    refine_vcg)
  by auto

definition test_impl :: "word32 ⇒ word32 ⇒ word32 set nres" where 
  "test_impl x y ≡ do {
    let S={};
    (S,_,_) ← WHILE (λ(S,x,y). x>0) (λ(S,x,y). do {
      let S=S∪{y}; 
      let x=x - 1;
      let y=y + 1;
      RETURN (S,x,y)
    }) (S,x,y);
    RETURN S
  }"

lemma test_impl_refine: 
  assumes "x'+y'<2^LENGTH(32)"
  assumes "(x,x')∈word_nat_rel" 
  assumes "(y,y')∈word_nat_rel" 
  shows "test_impl x y ≤ ⇓(⟨word_nat_rel⟩set_rel) (test x' y')"
proof -
  from assms show ?thesis
    unfolding test_impl_def test_def
    apply (refine_rcg)
    apply (refine_dref_type)
    apply (auto simp: refine_hsimp refine_rel_defs)
  done
qed

end