Theory CAVA_Base

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

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

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

(* 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}"

  text {* Cleaning up the namespace a bit *}
  
  hide_type (open) Word.word
  no_notation bits_class.test_bit (infixl "!!" 100)

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


  (* TODO: Should be contained in Isabelle since de0a4a76d7aa under 
    Option.bind_split{s,_asm}*)
  lemma option_bind_split: "P (Option.bind m f) 
  <-> (m = None --> P None) ∧ (∀v. m=Some v --> P (f v))"
    by (cases m) auto

  lemma option_bind_split_asm: "P (Option.bind m f) = (¬(
      m=None ∧ ¬P None 
    ∨ (∃x. m=Some x ∧ ¬P (f x))))"
    by (cases m) auto

  lemmas option_bind_splits = option_bind_split option_bind_split_asm

end