Theory Refine_Monadic_Thin

section ‹The Monadic Refinement Framework --- Naked›
(* TODO: Move to Refine_Monadic entry! *)
theory Refine_Monadic_Thin
imports 
  "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); r←body 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 ("while⇩T")
    notation WHILEI ("while⇗_⇖")
    notation WHILET ("while⇩T")
    notation WHILEIT ("while⇩T⇗_⇖")

    notation RECT (binder "rec⇩T " 10)
    notation REC (binder "rec " 10)

    notation SELECT (binder "select " 10)
      
  end
    
end