Theory Refine_Monadic_Thin

section The Monadic Refinement Framework --- Naked
(* TODO: Move to Refine_Monadic entry! *)
theory Refine_Monadic_Thin
imports 
  "Refine_Monadic.Refine_Chapter"
  "Refine_Monadic.Refine_Basic"
  "Refine_Monadic.Refine_Leof"
  "Refine_Monadic.Refine_Heuristics"
  "Refine_Monadic.Refine_More_Comb"
  "Refine_Monadic.Refine_While"
  "Refine_Monadic.Refine_Foreach" 
  "Refine_Monadic.Refine_Transfer"
  "Refine_Monadic.Refine_Pfun"
begin
  text 
    Monadic Refinement Framework, without Autoref.
    

  subsection Adaptations  
  declare is_None_def[simp del]  
  lemma is_None_alt[simp]: "is_None x  x=None" 
    by (auto simp: fun_eq_iff is_None_def split: option.splits)
  
    
  subsection Convenience Constructs

  definition "REC_annot pre post body x  
    REC (λD x. do {ASSERT (pre x); rbody D x; ASSERT (post x r); RETURN r}) x"
  
  theorem REC_annot_rule[refine_vcg]:
    assumes M: "trimono body"
    and P: "pre x"
    and S: "f x. x. pre x  f x  SPEC (post x); pre x 
             body f x  SPEC (post x)"
    and C: "r. post x r  Φ r"
    shows "REC_annot pre post body x  SPEC Φ"
  proof -
    from `trimono body` have [refine_mono]:
      "f g x xa. (x. flat_ge (f x) (g x))  flat_ge (body f x) (body g x)"
      "f g x xa. (x. f x  g x)  body f x  body g x"
      apply -
      unfolding trimono_def monotone_def fun_ord_def mono_def le_fun_def
      apply (auto)
      done
  
    show ?thesis
      unfolding REC_annot_def
      apply (rule order_trans[where y="SPEC (post x)"])
      apply (refine_rcg 
        refine_vcg 
        REC_rule[where pre=pre and M="λx. SPEC (post x)"]
        order_trans[OF S]
      )
      apply fact
      apply simp
      using C apply (auto) []
      done
  qed
  
  subsection Syntax Sugar
  locale Refine_Monadic_Syntax begin
  
    notation SPEC (binder "spec " 10)
    notation ASSERT ("assert")
    notation RETURN ("return")
    notation FOREACH ("foreach")
    notation WHILE ("while")
    notation WHILET ("whileT")
    notation WHILEI ("while⇗_")
    notation WHILET ("whileT")
    notation WHILEIT ("whileT_")

    notation RECT (binder "recT " 10)
    notation REC (binder "rec " 10)

    notation SELECT (binder "select " 10)
      
  end
    
end