Theory Monitor_Code

theory Monitor_Code
  imports "HOL-Library.Code_Target_Nat" "Containers.Containers" Monitor Preliminaries

derive (eq) ceq enat

instantiation enat :: ccompare begin

definition ccompare_enat :: "enat comparator option" where
  "ccompare_enat = Some (λx y. if x = y then order.Eq else if x < y then order.Lt else order.Gt)"

instance by intro_classes
    (auto simp: ccompare_enat_def split: if_splits intro!: comparator.intro)


  code_module "IArray"  (OCaml)
‹module IArray : sig
  val length' : 'a array -> Z.t
  val sub' : 'a array * Z.t -> 'a
end = struct

let length' xs = Z.of_int (Array.length xs);;

let sub' (xs, i) = Array.get xs (Z.to_int i);;

end› for type_constructor iarray constant IArray.length' IArray.sub'

code_reserved OCaml IArray

  type_constructor iarray  (OCaml) "_ array"
| constant iarray_of_list  (OCaml) "Array.of'_list"
| constant IArray.list_of  (OCaml) "'_list"
| constant IArray.length'  (OCaml) "IArray.length'"
| constant IArray.sub'  (OCaml) "IArray.sub'"

lemma iarray_list_of_inj: "IArray.list_of xs = IArray.list_of ys  xs = ys"
  by (cases xs; cases ys) auto

instantiation iarray :: (ccompare) ccompare

definition ccompare_iarray :: "('a iarray  'a iarray  order) option" where
  "ccompare_iarray = (case ID CCOMPARE('a list) of None  None
  | Some c  Some (λxs ys. c (IArray.list_of xs) (IArray.list_of ys)))"

  apply standard
  apply unfold_locales
  using comparator.sym[OF ID_ccompare'] comparator.weak_eq[OF ID_ccompare']
    comparator.comp_trans[OF ID_ccompare'] iarray_list_of_inj
    apply (auto simp: ccompare_iarray_def split: option.splits)
   apply blast+


derive (rbt) mapping_impl iarray

definition mk_db :: "String.literal list  String.literal set" where "mk_db = set"

definition init_vydra_string_enat :: "_  _  _  (String.literal, enat, 'e) vydra" where
  "init_vydra_string_enat = init_vydra"
definition run_vydra_string_enat :: " _   (String.literal, enat, 'e) vydra  _" where
  "run_vydra_string_enat = run_vydra"
definition progress_enat :: "(String.literal, enat) formula  enat list  nat" where
  "progress_enat = progress"
definition bounded_future_fmla_enat :: "(String.literal, enat) formula  bool" where
  "bounded_future_fmla_enat = bounded_future_fmla"
definition wf_fmla_enat :: "(String.literal, enat) formula  bool" where
  "wf_fmla_enat = wf_fmla"
definition mdl2mdl'_enat :: "(String.literal, enat) formula  (String.literal, enat) Preliminaries.formula" where
  "mdl2mdl'_enat = mdl2mdl'"
definition interval_enat :: "enat  enat  bool  bool  enat " where
  "interval_enat = interval"
definition rep_interval_enat :: "enat   enat × enat × bool × bool" where
  "rep_interval_enat = Rep_ℐ"

definition init_vydra_string_ereal :: "_  _  _  (String.literal, ereal, 'e) vydra" where
  "init_vydra_string_ereal = init_vydra"
definition run_vydra_string_ereal :: " _   (String.literal, ereal, 'e) vydra  _" where
  "run_vydra_string_ereal = run_vydra"
definition progress_ereal :: "(String.literal, ereal) formula  ereal list  real" where
  "progress_ereal = progress"
definition bounded_future_fmla_ereal :: "(String.literal, ereal) formula  bool" where
  "bounded_future_fmla_ereal = bounded_future_fmla"
definition wf_fmla_ereal :: "(String.literal, ereal) formula  bool" where
  "wf_fmla_ereal = wf_fmla"
definition mdl2mdl'_ereal :: "(String.literal, ereal) formula  (String.literal, ereal) Preliminaries.formula" where
  "mdl2mdl'_ereal = mdl2mdl'"
definition interval_ereal :: "ereal  ereal  bool  bool  ereal " where
  "interval_ereal = interval"
definition rep_interval_ereal :: "ereal   ereal × ereal × bool × bool" where
  "rep_interval_ereal = Rep_ℐ"

lemma tfin_enat_code[code]: "(tfin :: enat set) = Collect_set (λx. x  )"
  by (auto simp: tfin_enat_def)

lemma tfin_ereal_code[code]: "(tfin :: ereal set) = Collect_set (λx. x  -  x  )"
  by (auto simp: tfin_ereal_def)

lemma Ball_atms[code_unfold]: "Ball (atms r) P = list_all P (collect_subfmlas r [])"
  using collect_subfmlas_atms[where ?phis="[]"]
  by (auto simp: list_all_def)

lemma MIN_fold: "(MIN xset (z # zs). f x) = fold min (map f zs) (f z)"
  by (metis Min.set_eq_fold list.set_map list.simps(9))

declare progress.simps(1-8)[code]

lemma progress_matchP_code[code]:
  "progress (MatchP I r) ts = (case collect_subfmlas r [] of x # xs  fold min (map (λf. progress f ts) xs) (progress x ts))"
  using collect_subfmlas_atms[where ?r=r and ?phis="[]"] atms_nonempty[of r]
  by (auto split: list.splits) (smt (z3) MIN_fold[where ?f="λf. progress f ts"] list.simps(15))

lemma progress_matchF_code[code]:
  "progress (MatchF I r) ts = (if length ts = 0 then 0 else
  (let k = min (length ts - 1) (case collect_subfmlas r [] of x # xs  fold min (map (λf. progress f ts) xs) (progress x ts)) in
   Min {j  {..k}. memR (ts ! j) (ts ! k) I}))"
  by (auto simp: progress_matchP_code[unfolded progress.simps])

export_code init_vydra_string_enat run_vydra_string_enat progress_enat bounded_future_fmla_enat wf_fmla_enat mdl2mdl'_enat
  Bool Preliminaries.Bool enat interval_enat rep_interval_enat nat_of_integer integer_of_nat mk_db
  in OCaml module_name VYDRA file_prefix "verified"