Theory Refine_Imp_Hol

section ‹Refinement for Imperative-HOL Programs›
theory Refine_Imp_Hol
  imports "Hoare_Triple"
            "HOL-Eisbach.Eisbach"
begin

  subsection ‹Assertions›
    
  text ‹We add assertions that consume no time to Imperative HOL Time.
  
    Note that the original \<^const>‹assert› consumes one time unit, i.e., is designed for 
    actually being checked at runtime. On the other hand, our assertions are not executable, 
    and must be refined before code generation.
  ›
  definition [code del]: "assert' P ≡ if P then ureturn () else raise ''assert''"

  lemma execute_assert'[execute_simps]: "execute (assert' P) h = (if P then Some ((),h,0) else None)"
    by (auto simp: assert'_def execute_simps)

  
  lemma assert'_rule: "⟦⋀h. h⊨P ⟹ φ⟧ ⟹ <P> assert' φ <λ_. P>"  
    apply rule
    apply (auto simp: execute_simps in_range.simps relH_refl)
    done
    
  lemma assert'_bind_rule: 
    assumes "⋀h. h⊨P ⟹ φ"
    assumes "φ ⟹ <P> c <Q>"
    shows "<P> do {assert' φ; c} <Q>"  
    apply rule
    using assms
    apply (auto simp: execute_simps in_range.simps relH_refl elim!: hoare_tripleE)
    done    
    
  subsection ‹Refinement Predicate›  
  text ‹An imperative-HOL program ‹p› refines a program ‹q›, if either ‹q› fails, or ‹p› returns the
    same result as ‹q›. In case ‹q› is already proved correct (in particular does not fail), this
    implies correctness of ‹p›. Moreover, for the refinement proof, we can assume that ‹q› does not fail,
    in particular, that all assertions in ‹q› hold. This can be used to transfer knowledge from the 
    correctness proof (proving the assertions) to the refinement proof (assuming the assertions).
  ›
  definition "refines p q ≡ ∀h. case execute q h of None ⇒ True | Some (r,h',t) ⇒ execute p h = Some (r,h',t)"

  lemma hoare_triple_refines:
    assumes "<P> c <Q>"
    assumes "refines c' c"
    shows "<P> c' <Q>"
    apply rule
    using assms
    by (auto simp: refines_def elim!: hoare_tripleE split: option.splits)
  
    
  subsubsection ‹Admissibility›
  context begin
  
  private lemma refines_adm_aux: "option.admissible (λxa. ∀h a aa b. xa h = Some (a, aa, b) ⟶ execute (t x) h = Some (a, aa, b))"
  proof-
    have "option.admissible (λxa. ∀h y. xa h = Some y ⟶ execute (t x) h = Some y)" 
      using option_admissible by metis
    thus ?thesis by auto
  qed
  
  lemma refines_adm: "heap.admissible (λf. ∀x. refines (t x) (f x) )"
    unfolding refines_def
    apply (rule admissible_fun[OF heap_interpretation])
  
    unfolding Heap_lub_def Heap_ord_def
    apply (rule admissible_image)
    using option.partial_function_definitions_axioms partial_function_lift apply auto[1]
      apply(simp split: option.splits)
      apply auto[3]
    subgoal for x
      apply (simp add: comp_def)
      apply(rule refines_adm_aux)
      done
    subgoal for xa y 
      apply (metis Heap_execute)  
      done
    done
  
  end  

  subsection ‹Syntactic rules for \<^const>‹refines››  

  named_theorems refines_rule
  
  lemma refines_assert'[refines_rule]: "refines (ureturn ()) (assert' φ)"
    unfolding refines_def
    by (simp add: execute_simps)
  
  lemma refines_assert'_bind[refines_rule]: "refines p q ⟹ refines p (do {assert' φ; q})"  
    unfolding refines_def
    apply (cases φ)
    apply (auto simp add: execute_simps split: option.splits)
    done
    
  lemma refines_bind[refines_rule]: "refines m m' ⟹ (⋀x. refines (f x) (f' x)) ⟹ refines (do {x←m; f x}) (do {x←m'; f' x})"
    unfolding refines_def
    apply clarsimp
    subgoal for h
      apply (cases "execute m' h"; cases "execute m h")
      apply (auto simp add: execute_simps split: option.splits)
      by (smt (verit, best) option.case(2) prod.simps(2) timeFrame.elims)
    done
    
  lemma refines_If[refines_rule]: "⟦b⟹refines t t'⟧ ⟹ ⟦¬b⟹refines e e'⟧ ⟹ refines (If b t e) (If b t' e')" by auto
  lemma refines_Let[refines_rule]: "⟦ ⋀x. ⟦x=v⟧ ⟹ refines (f x) (f' x) ⟧ ⟹ refines (let x=v in f x) (let x=v in f' x)" by auto
    
  
  lemma refines_refl: "refines p p"  
    unfolding refines_def
    by (auto split: option.splits)
 
  lemma refines_empty[simp]: "refines m  (Heap.Heap Map.empty)" 
    apply(simp add: refines_def)
    done
 
  lemma refines_let_right: assumes "refines m (m' a)"
    shows "refines m (let x = a in m' x)"
    using assms by simp
  
  lemma refines_case_prod_right: assumes "⋀ a b. refines m (m' a b)"
    shows "refines m (case t of (a,b) ⇒ m' a b)"
    using assms apply(cases t)
    by simp
  
  lemma refines_option[refines_rule]: assumes "a=a'" "refines m1 m1'" "⋀ x. refines (m2 x) (m2' x)"
    shows "refines (case a of None ⇒ m1 | Some x ⇒ m2 x)  (case a' of None ⇒ m1' | Some x ⇒ m2' x)"
    using assms apply(cases a')
     apply simp_all
    done
  
  lemma prod_case_refines[refines_rule]: assumes "p= p'" " ⋀ a b. refines (f a b) (f' a b)"
    shows " refines (case p of (a, b) ⇒ f a b) (case p' of (a, b) ⇒ f' a b )" 
    using assms apply(cases p') by simp

subsection ‹Automation›    
    
  method refines_step= determ‹rule refines_rule refl refines_refl refines_let_right refines_case_prod_right 
                               | assumption | simp only:›
  
  method refines = refines_step+    
    
end