Theory CAVA_Base.CAVA_Base

section "Setup of Environment for CAVA Model Checker"
theory CAVA_Base
  imports 
  Collections.CollectionsV1  (*-- {* Compatibility with ICF 1.0 *}*)
  Collections.Refine_Dflt      

  Statistics (*-- {* Collecting statistics by instrumenting the formalization *}*)

  CAVA_Code_Target (*-- {* Code Generator Setup *}*)
begin

hide_const (open) CollectionsV1.ahs_rel

(*
(* Select-function that selects element from set *)
(* TODO: Move! Is select properly integrated into autoref? *)
  definition select where
    "select S ≡ if S={} then RETURN None else RES {Some s | s. s∈S}"

lemma select_correct: 
  "select X ≤ SPEC (λr. case r of None ⇒ X={} | Some x ⇒ x∈X)"
  unfolding select_def
  apply (refine_rcg refine_vcg)
  by auto
*)
  
  text ‹Cleaning up the namespace a bit›
  
  hide_type (open) Word.word

  text ‹Some custom setup in cava, that does not match HOL defaults:›
  declare Let_def[simp add]

end