Theory Checker_Code

(*<*)
theory Checker_Code
  imports 
    Checker Event_Data 
    "HOL-Library.Code_Target_Nat" 
    "HOL.String"
    "HOL-Library.List_Lexorder" 
    "HOL-Library.AList_Mapping"
    "HOL-Library.Cardinality"
begin
(*>*)

section ‹Code Generation›

subsection ‹Type Class Instances›

class universe =
  fixes universe :: "'a list option"
  assumes infinite: "universe = None ⟹ infinite (UNIV :: 'a set)"
  and finite: "universe = Some xs ⟹ distinct xs ∧ set xs = UNIV"
begin

lemma finite_coset: "finite (List.coset (xs :: 'a list)) = (case universe of None ⇒ False | _ ⇒ True)"
  using infinite finite
  by (auto split: option.splits dest!: equalityD2 elim!: finite_subset)

end

declare [[code drop: finite]]
declare finite_set[THEN eqTrueI, code] finite_coset[code]

instantiation bool :: universe begin
definition universe_bool :: "bool list option" where "universe_bool = Some [True, False]"
instance by standard (auto simp: universe_bool_def)
end
instantiation char :: universe begin
definition universe_char :: "char list option" where "universe_char = Some (map char_of [0::nat..<256])"
instance by standard (use UNIV_char_of_nat in ‹auto simp: universe_char_def distinct_map›)
end
instantiation nat :: universe begin
definition universe_nat :: "nat list option" where "universe_nat = None"
instance by standard (auto simp: universe_nat_def)
end
instantiation list :: (type) universe begin
definition universe_list :: "'a list list option" where "universe_list = None"
instance by standard (auto simp: universe_list_def infinite_UNIV_listI)
end
instantiation String.literal :: universe begin
definition universe_literal :: "String.literal list option" where "universe_literal = None"
instance by standard (auto simp: universe_literal_def infinite_literal)
end
instantiation string8 :: universe begin
definition universe_string8 :: "string8 list option" where "universe_string8 = None"
lemma UNIV_string8: "UNIV = Abs_string8 ` UNIV"
  by (auto simp: image_iff intro: Abs_string8_cases)
instance by standard
  (auto simp: universe_string8_def UNIV_string8 finite_image_iff Abs_string8_inject inj_on_def infinite_UNIV_listI)
end
instantiation prod :: (universe, universe) universe begin
definition universe_prod :: "('a × 'b) list option" where "universe_prod =
  (case (universe, universe) of (Some xs, Some ys) ⇒ Some (List.product xs ys) | _ ⇒ None)"
instance by standard
  (auto simp: universe_prod_def finite_prod distinct_product infinite finite split: option.splits)
end
instantiation sum :: (universe, universe) universe begin
definition universe_sum :: "('a + 'b) list option" where "universe_sum =
  (case (universe, universe) of (Some xs, Some ys) ⇒ Some (map Inl xs @ map Inr ys) | _ ⇒ None)"
instance by standard
  (use UNIV_sum in ‹auto simp: universe_sum_def distinct_map infinite finite split: option.splits›)
end
instantiation option :: (universe) universe begin
definition "universe_option = (case universe of Some xs ⇒ Some (None # map Some xs) | _ ⇒ None)"
instance by standard (auto simp: universe_option_def distinct_map finite infinite image_iff split: option.splits)
end
instantiation "fun" :: (universe, universe) universe begin
definition universe_fun :: "('a ⇒ 'b) list option" where "universe_fun = 
  (case (universe, universe) of
    (Some xs, Some ys) ⇒ Some (map (λzs. the ∘ map_of (zip xs zs)) (List.n_lists (length xs) ys))
  | (_, Some [x]) ⇒ Some [λ_. x]
  | _ ⇒ None)"
instance
proof -
  have 1: False if "infinite (UNIV::'a set)" "CARD('b) = Suc 0" "a ≠ b" for a b :: 'b
    using that by (metis (full_types) UNIV_I card_1_singleton_iff singletonD)
  have 2: "ys = zs"
    if "distinct (xs::'a list)" and "length ys = length xs" and "length zs = length xs"
    and "∀a. the (map_of (zip xs ys) a) = the (map_of (zip xs zs) a)"
    for xs :: "'a list" and ys zs :: "'b list"
    using that by (metis map_fst_zip map_of_eqI map_of_zip_inject map_of_zip_is_None option.expand)
  have 3: "∃zs. length zs = length xs ∧ set zs ⊆ set ys ∧ (∀x. f x = the (map_of (zip xs zs) x))"
    if "∀x. x ∈ set xs" "∀x. x ∈ set ys"
    for xs ys and f :: "'a ⇒ 'b"
    using that by (metis length_map map_of_zip_map option.sel subsetI)
  show "OFCLASS('a ⇒ 'b, universe_class)"
    by standard
      (auto 0 3 simp: universe_fun_def set_eq_iff fun_eq_iff image_iff set_n_lists distinct_map
        inj_on_def distinct_n_lists finite_UNIV_fun dest!: infinite finite
        split: option.splits list.splits intro: 1 2 3)
qed
end
instantiation event_data :: universe begin
definition universe_event_data :: "event_data list option" where "universe_event_data = None"  
instance by standard (simp_all add: infinite_UNIV_event_data universe_event_data_def)
end

instantiation nat :: default begin
definition default_nat :: nat where "default_nat = 0"
instance proof qed
end

instantiation list :: (type) default begin
definition default_list :: "'a list" where "default_list = []"
instance proof qed
end

instance event_data :: equal by standard

instantiation String.literal :: default begin
definition default_literal :: String.literal where "default_literal = 0"
instance proof qed
end

instantiation event_data :: card_UNIV begin
definition "finite_UNIV = Phantom(event_data) False"
definition "card_UNIV = Phantom(event_data) 0"
instance by intro_classes (simp_all add: finite_UNIV_event_data_def card_UNIV_event_data_def infinite_UNIV_event_data)
end

subsection ‹Progress›

primrec progress :: "('n, 'd) trace ⇒ ('n, 'd) Formula.formula ⇒ nat ⇒ nat" where
  "progress σ Formula.TT j = j"
| "progress σ Formula.FF j = j"
| "progress σ (Formula.Eq_Const _ _) j = j"
| "progress σ (Formula.Pred _ _) j = j"
| "progress σ (Formula.Neg φ) j = progress σ φ j"
| "progress σ (Formula.Or φ ψ) j = min (progress σ φ j) (progress σ ψ j)"
| "progress σ (Formula.And φ ψ) j = min (progress σ φ j) (progress σ ψ j)"
| "progress σ (Formula.Imp φ ψ) j = min (progress σ φ j) (progress σ ψ j)"
| "progress σ (Formula.Iff φ ψ) j = min (progress σ φ j) (progress σ ψ j)"
| "progress σ (Formula.Exists _ φ) j = progress σ φ j"
| "progress σ (Formula.Forall _ φ) j = progress σ φ j"
| "progress σ (Formula.Prev I φ) j = (if j = 0 then 0 else min (Suc (progress σ φ j)) j)"
| "progress σ (Formula.Next I φ) j = progress σ φ j - 1"
| "progress σ (Formula.Once I φ) j = progress σ φ j"
| "progress σ (Formula.Historically I φ) j = progress σ φ j"
| "progress σ (Formula.Eventually I φ) j =
    Inf {i. ∀k. k < j ∧ k ≤ (progress σ φ j) ⟶ (τ σ k - τ σ i) ≤ right I}"
| "progress σ (Formula.Always I φ) j =
    Inf {i. ∀k. k < j ∧ k ≤ (progress σ φ j) ⟶ (τ σ k - τ σ i) ≤ right I}"
| "progress σ (Formula.Since φ I ψ) j = min (progress σ φ j) (progress σ ψ j)"
| "progress σ (Formula.Until φ I ψ) j =
    Inf {i. ∀k. k < j ∧ k ≤ min (progress σ φ j) (progress σ ψ j) ⟶ (τ σ k - τ σ i) ≤ right I}"

lemma Inf_Min:
  fixes P :: "nat ⇒ bool"
  assumes "P j"
  shows "Inf (Collect P) = Min (Set.filter P {..j})"
  using Min_in[where ?A="Set.filter P {..j}"] assms
  by (auto simp: Set.filter_def intro: cInf_lower intro!: antisym[OF _ Min_le])
    (metis Inf_nat_def1 empty_iff mem_Collect_eq)

lemma progress_Eventually_code: "progress σ (Formula.Eventually I φ) j =
  (let m = min j (Suc (progress σ φ j)) - 1 in Min (Set.filter (λi. enat (δ σ m i) ≤ right I) {..j}))"
proof -
  define P where "P ≡ (λi. ∀k. k < j ∧ k ≤ (progress σ φ j) ⟶ enat (δ σ k i) ≤ right I)"
  have P_j: "P j"
    by (auto simp: P_def enat_0)
  have all_wit: "(∀k ∈ {..<m}. enat (δ σ k i) ≤ right I) ⟷ (enat (δ σ (m - 1) i) ≤ right I)" for i m
  proof (cases m)
    case (Suc ma)
    have "k < Suc ma ⟹ δ σ k i ≤ δ σ ma i" for k
      using τ_mono
      unfolding less_Suc_eq_le
      by (rule diff_le_mono)
    then show ?thesis
      by (auto simp: Suc) (meson order.trans enat_ord_simps(1))
  qed (auto simp: enat_0)
  show ?thesis
    unfolding progress.simps Let_def P_def[symmetric] Inf_Min[where ?P=P, OF P_j] all_wit[symmetric]
    by (fastforce simp: P_def intro: arg_cong[where ?f=Min])
qed

lemma progress_Always_code: "progress σ (Formula.Always I φ) j =
  (let m = min j (Suc (progress σ φ j)) - 1 in Min (Set.filter (λi. enat (δ σ m i) ≤ right I) {..j}))"
proof -
  define P where "P ≡ (λi. ∀k. k < j ∧ k ≤ (progress σ φ j) ⟶ enat (δ σ k i) ≤ right I)"
  have P_j: "P j"
    by (auto simp: P_def enat_0)
  have all_wit: "(∀k ∈ {..<m}. enat (δ σ k i) ≤ right I) ⟷ (enat (δ σ (m - 1) i) ≤ right I)" for i m
  proof (cases m)
    case (Suc ma)
    have "k < Suc ma ⟹ δ σ k i ≤ δ σ ma i" for k
      using τ_mono
      unfolding less_Suc_eq_le
      by (rule diff_le_mono)
    then show ?thesis
      by (auto simp: Suc) (meson order.trans enat_ord_simps(1))
  qed (auto simp: enat_0)
  show ?thesis
    unfolding progress.simps Let_def P_def[symmetric] Inf_Min[where ?P=P, OF P_j] all_wit[symmetric]
    by (fastforce simp: P_def intro: arg_cong[where ?f=Min])
qed

lemma progress_Until_code: "progress σ (Formula.Until φ I ψ) j =
  (let m = min j (Suc (min (progress σ φ j) (progress σ ψ j))) - 1 in Min (Set.filter (λi. enat (δ σ m i) ≤ right I) {..j}))"
proof -
  define P where "P ≡ (λi. ∀k. k < j ∧ k ≤ min (progress σ φ j) (progress σ ψ j) ⟶ enat (δ σ k i) ≤ right I)"
  have P_j: "P j"
    by (auto simp: P_def enat_0)
  have all_wit: "(∀k ∈ {..<m}. enat (δ σ k i) ≤ right I) ⟷ (enat (δ σ (m - 1) i) ≤ right I)" for i m
  proof (cases m)
    case (Suc ma)
    have "k < Suc ma ⟹ δ σ k i ≤ δ σ ma i" for k
      using τ_mono
      unfolding less_Suc_eq_le
      by (rule diff_le_mono)
    then show ?thesis
      by (auto simp: Suc) (meson order.trans enat_ord_simps(1))
  qed (auto simp: enat_0)
  show ?thesis
    unfolding progress.simps Let_def P_def[symmetric] Inf_Min[where ?P=P, OF P_j] all_wit[symmetric]
    by (fastforce simp: P_def intro: arg_cong[where ?f=Min])
qed

lemmas progress_code[code] = progress.simps(1-15) progress_Eventually_code progress_Always_code progress.simps(18) progress_Until_code

subsection ‹Trace›

lemma snth_Stream_eq: "(x ## s) !! n = (case n of 0 ⇒ x | Suc m ⇒ s !! m)"
  by (cases n) auto

lemma extend_is_stream: 
  assumes "sorted (map snd list)"
  and "⋀x. x ∈ set list ⟹ snd x ≤ m"
  and "⋀x. x ∈ set list ⟹ finite (fst x)"
  shows "ssorted (smap snd (list @- smap (λn. ({}, n + m)) nats)) ∧
    sincreasing (smap snd (list @- smap (λn. ({}, n + m)) nats)) ∧
    sfinite (smap fst (list @- smap (λn. ({}, n + m)) nats))"
proof -
  have A: "∀x∈set list. n ≤ snd x ⟹ n ≤ m ⟹
    n ≤ (map snd list @- smap (λx. x + m) nats) !! i" for n i 
    and list :: "('a set × nat) list"
  proof (induction i arbitrary: n)
    case (Suc i)
    then show ?case
      by (auto simp: shift_snth nth_tl)
  qed (auto simp add: list.map_sel(1))
  then have "ssorted (smap snd (list @- smap (λn. ({}, n + m)) nats))"
    using assms
      by (induction list) (auto simp: stream.map_comp o_def ssorted_iff_mono snth_Stream_eq
        split: nat.splits)
  moreover have "sincreasing (smap snd (list @- smap (λn. ({}, n + m)) nats))"
    using assms
  proof (induction list)
    case Nil
    then show ?case
      by (simp add: sincreasing_def) presburger
  next
    case (Cons a as)
    have IH: "⋀x. ∃i. x < smap snd (as @- smap (λn. ({}, n + m)) nats) !! i"
      using Cons
      by (simp add: sincreasing_def)
    show ?case
      using IH
      by (simp add: sincreasing_def) 
        (metis snth_Stream)
  qed
  moreover have "sfinite (smap fst (list @- smap (λn. ({}, n + m)) nats))"
    using assms(3)
  proof (induction list)
    case Nil
    then show ?case by (simp add: sfinite_def)
  next
    case (Cons a as)
    then have fin: "finite (fst a)"
      by simp
    show ?case
      using Cons 
      by (auto simp add: sfinite_def snth_Stream_eq split: nat.splits)
  qed
  ultimately show ?thesis
    by simp
qed

typedef 'a trace_mapping = "{(n, m, t) :: (nat × nat × (nat, 'a set × nat) mapping) |
  n m t. Mapping.keys t = {..<n} ∧
  sorted (map (snd ∘ (the ∘ Mapping.lookup t)) [0..<n]) ∧
  (case n of 0 ⇒ True | Suc n' ⇒ (case Mapping.lookup t n' of Some (X', t') ⇒ t' ≤ m | None ⇒ False)) ∧ 
  (∀n' < n. case Mapping.lookup t n' of Some (X', t') ⇒ finite X' | None ⇒ False)}"
  by (rule exI[of _ "(0, 0, Mapping.empty)"]) auto

setup_lifting type_definition_trace_mapping

lemma lookup_bulkload_Some: "i < length list ⟹
  Mapping.lookup (Mapping.bulkload list) i = Some (list ! i)"
  by transfer auto

lift_definition trace_mapping_of_list :: "('a set × nat) list ⇒ 'a trace_mapping" is
  "λxs. if sorted (map snd xs) ∧ (∀x ∈ set xs. finite (fst x)) then (if xs = [] then (0, 0, Mapping.empty)
  else (length xs, snd (last xs), Mapping.bulkload xs))
  else (0, 0, Mapping.empty)"
  by (auto simp: lookup_bulkload_Some sorted_iff_nth_Suc last_conv_nth
    list_all_iff in_set_conv_nth Ball_def Bex_def image_iff split: nat.splits)

lift_definition trace_mapping_nth :: "'a trace_mapping ⇒ nat ⇒ ('a set × nat)" is
  "λ(n, m, t) i. if i < n then the (Mapping.lookup t i) else ({}, (i - n) + m)" .

lift_definition Trace_Mapping :: "'a trace_mapping ⇒ 'a Trace.trace" is
  "λ(n, m, t). map (the ∘ Mapping.lookup t) [0..<n] @- smap (λn. ({} :: 'a set, n + m)) nats"
proof (goal_cases)
  case (1 prod)
  obtain n m t where prod_def: "prod = (n, m, t)"
    by (cases prod) auto
  have props: "Mapping.keys t = {..<n}"
    "sorted (map (snd ∘ (the ∘ Mapping.lookup t)) [0..<n])"
    "(case n of 0 ⇒ True | Suc n' ⇒ (case Mapping.lookup t n' of Some (X', t') ⇒ t' ≤ m | None ⇒ False))"
    "(∀n' < n. case Mapping.lookup t n' of Some (X', t') ⇒ finite X' | None ⇒ False)"
    using 1 by (auto simp add: prod_def)
  have aux: "x ∈ set (map (the ∘ Mapping.lookup t) [0..<n]) ⟹ snd x ≤ m" for x
    using props(2,3) less_Suc_eq_le
    by (fastforce simp: sorted_iff_nth_mono split: nat.splits option.splits)
  have aux2: "x ∈ set (map (the ∘ Mapping.lookup t) [0..<n]) ⟹ finite (fst x)" for x
    using props(1,4)
    by (auto split: nat.splits option.splits)
  show ?case
    unfolding prod_def prod.case
    by (rule extend_is_stream[where ?m=m]) (use props aux aux2 in ‹auto simp: prod_def›)
qed

code_datatype Trace_Mapping

definition "trace_of_list xs = Trace_Mapping (trace_mapping_of_list xs)"

lemma Γ_rbt_code[code]: "Γ (Trace_Mapping t) i = fst (trace_mapping_nth t i)"
  by transfer (auto split: prod.splits)

lemma τ_rbt_code[code]: "τ (Trace_Mapping t) i = snd (trace_mapping_nth t i)"
  by transfer (auto split: prod.splits)
                                       
lemma trace_mapping_of_list_sound: "sorted (map snd xs) ∧ (∀x ∈ set xs. finite (fst x)) ⟹ i < length xs ⟹
  xs ! i = (Γ (trace_of_list xs) i, τ (trace_of_list xs) i)"
  unfolding trace_of_list_def
  by transfer (auto simp: lookup_bulkload_Some)

subsection ‹Auxiliary results›

definition "sum_proofs f xs = sum_list (map f xs)"

lemma sum_proofs_empty[simp]: "sum_proofs f [] = 0"
  by (auto simp: sum_proofs_def)

lemma sum_proofs_fundef_cong[fundef_cong]: "(⋀x. x ∈ set xs ⟹ f x = f' x) ⟹
  sum_proofs f xs = sum_proofs f' xs"
  by (induction xs) (auto simp: sum_proofs_def)

lemma sum_proofs_Cons:
  fixes f :: "'a ⇒ nat"
  shows "sum_proofs f (p # qs) = f p + sum_proofs f qs"
  by (auto simp: sum_proofs_def split: list.splits)

lemma sum_proofs_app:
  fixes f :: "'a ⇒ nat"
  shows "sum_proofs f (qs @ [p]) = f p + sum_proofs f qs"
  by (auto simp: sum_proofs_def split: list.splits)

context
  fixes w :: "'n ⇒ nat"
begin

function (sequential) s_pred :: "('n, 'd) sproof ⇒ nat" 
  and v_pred :: "('n, 'd) vproof ⇒ nat" where
  "s_pred (STT _) = 1"
| "s_pred (SEq_Const _ _ _) = 1"
| "s_pred (SPred _ r _) = w r"
| "s_pred (SNeg vp) = (v_pred vp) + 1"
| "s_pred (SOrL sp1) = (s_pred sp1) + 1"
| "s_pred (SOrR sp2) = (s_pred sp2) + 1"
| "s_pred (SAnd sp1 sp2) = (s_pred sp1) + (s_pred sp2) + 1"
| "s_pred (SImpL vp1) = (v_pred vp1) + 1"
| "s_pred (SImpR sp2) = (s_pred sp2) + 1"
| "s_pred (SIffSS sp1 sp2) = (s_pred sp1) + (s_pred sp2) + 1"
| "s_pred (SIffVV vp1 vp2) = (v_pred vp1) + (v_pred vp2) + 1"
| "s_pred (SExists _ _ sp) = (s_pred sp) + 1"
| "s_pred (SForall _ part) = (sum_proofs s_pred (vals part)) + 1"
| "s_pred (SPrev sp) = (s_pred sp) + 1"
| "s_pred (SNext sp) = (s_pred sp) + 1"
| "s_pred (SOnce _ sp) = (s_pred sp) + 1"
| "s_pred (SEventually _ sp) = (s_pred sp) + 1"
| "s_pred (SHistorically _ _ sps) = (sum_proofs s_pred sps) + 1"
| "s_pred (SHistoricallyOut _) = 1"
| "s_pred (SAlways _ _ sps) = (sum_proofs s_pred sps) + 1"
| "s_pred (SSince sp2 sp1s) = (sum_proofs s_pred (sp2 # sp1s)) + 1"
| "s_pred (SUntil sp1s sp2) = (sum_proofs s_pred (sp1s @ [sp2])) + 1"
| "v_pred (VFF _ ) = 1"
| "v_pred (VEq_Const _ _ _) = 1"
| "v_pred (VPred _ r _) = w r"
| "v_pred (VNeg sp) = (s_pred sp) + 1"
| "v_pred (VOr vp1 vp2) = ((v_pred vp1) + (v_pred vp2)) + 1"
| "v_pred (VAndL vp1) = (v_pred vp1) + 1"
| "v_pred (VAndR vp2) = (v_pred vp2) + 1"
| "v_pred (VImp sp1 vp2) = ((s_pred sp1) + (v_pred vp2)) + 1"
| "v_pred (VIffSV sp1 vp2) = ((s_pred sp1) + (v_pred vp2)) + 1"
| "v_pred (VIffVS vp1 sp2) = ((v_pred vp1) + (s_pred sp2)) + 1"
| "v_pred (VExists _ part) = (sum_proofs v_pred (vals part)) + 1"
| "v_pred (VForall _ _ vp) = (v_pred vp) + 1"
| "v_pred (VPrev vp) = (v_pred vp) + 1"
| "v_pred (VPrevZ) = 1"
| "v_pred (VPrevOutL _) = 1"
| "v_pred (VPrevOutR _) = 1"
| "v_pred (VNext vp) = (v_pred vp) + 1"
| "v_pred (VNextOutL _) = 1"
| "v_pred (VNextOutR _) = 1"
| "v_pred (VOnceOut _) = 1"
| "v_pred (VOnce _ _ vps) = (sum_proofs v_pred vps) + 1"
| "v_pred (VEventually _ _ vps) = (sum_proofs v_pred vps) + 1"
| "v_pred (VHistorically _ vp) = (v_pred vp) + 1"
| "v_pred (VAlways _ vp) = (v_pred vp) + 1"
| "v_pred (VSinceOut _) = 1"
| "v_pred (VSince _ vp1 vp2s) = (sum_proofs v_pred (vp1 # vp2s)) + 1"
| "v_pred (VSinceInf _ _ vp2s) = (sum_proofs v_pred vp2s) + 1"
| "v_pred (VUntil _ vp2s vp1) = (sum_proofs v_pred (vp2s @ [vp1])) + 1"
| "v_pred (VUntilInf _ _ vp2s) = (sum_proofs v_pred vp2s) + 1"
  by pat_completeness auto
termination
  by (relation "measure (case_sum size size)")
    (auto simp add: termination_simp)

definition p_pred :: "('n, 'd) proof ⇒ nat" where
  "p_pred = case_sum s_pred v_pred"

end

subsection ‹\<^const>‹v_check_exec› setup›

lemma ETP_minus_le_iff: "ETP σ (τ σ i - n) ≤ j ⟷ δ σ i j ≤ n"
  by (simp add: add.commute i_ETP_tau le_diff_conv)

lemma ETP_minus_gt_iff: "j < ETP σ (τ σ i - n) ⟷ δ σ i j > n"
  by (meson ETP_minus_le_iff leD le_less_linear)

lemma nat_le_iff_less:
  fixes n :: nat
  shows "(j ≤ n) ⟷ (j = 0 ∨ j - 1 < n)"
  by auto

lemma ETP_minus_eq_iff: "j = ETP σ (τ σ i - n) ⟷ ((j = 0 ∨ n < δ σ i (j - 1)) ∧ δ σ i j ≤ n)"
  unfolding eq_iff[of j "ETP σ (τ σ i - n)"] nat_le_iff_less[of j] ETP_minus_le_iff ETP_minus_gt_iff
  by auto

lemma LTP_minus_ge_iff: "τ σ 0 + n ≤ τ σ i ⟹ j ≤ LTP σ (τ σ i - n) ⟷
  (case n of 0 ⇒ δ σ j i = 0 | _ ⇒ j ≤ i ∧ δ σ i j ≥ n)"
  using τ_mono[of i j σ]
  by (fastforce simp add: i_LTP_tau le_diff_conv2 Suc_le_eq split: nat.splits)

lemma LTP_plus_ge_iff: "j ≤ LTP σ (τ σ i + n) ⟷ δ σ j i ≤ n"
  by (simp add: add.commute i_LTP_tau le_diff_conv trans_le_add2)

lemma LTP_minus_lt_if:
  assumes "j ≤ i" "τ σ 0 + n ≤ τ σ i" "δ σ i j < n"
  shows "LTP σ (τ σ i - n) < j"
proof -
  have not_in: "k ∉ {ia. τ σ ia ≤ τ σ i - n}" if "j ≤ k" for k
    using assms τ_mono[OF that, of σ]
    by auto
  then have "{ia. τ σ ia ≤ τ σ i - n} ⊆ {0..<j}"
    using not_le_imp_less
    by (clarsimp; blast)
  then have "finite {ia. τ σ ia ≤ τ σ i - n}"
    using subset_eq_atLeast0_lessThan_finite
    by blast
  moreover have "0 ∈ {ia. τ σ ia ≤ τ σ i - n}"
    using assms(2)
    by auto
  ultimately show ?thesis
    unfolding LTP_def
    by (metis Max_in not_in empty_iff not_le_imp_less)
qed

lemma LTP_minus_lt_iff:
  assumes "τ σ 0 + n ≤ τ σ i"
  shows "LTP σ (τ σ i - n) < j ⟷ (if ¬ j ≤ i ∧ n = 0 then δ σ j i > 0 else δ σ i j < n)"
proof (cases "j ≤ i")
  case True
  then show ?thesis
    using assms i_le_LTPi_minus[of σ n i] LTP_minus_lt_if[of j i σ n]
    by (cases n)
      (auto simp add: i_LTP_tau linorder_not_less Suc_le_eq dest!: tau_LTP_k[rotated])
next
  case False
  have delta: "δ σ i j = 0"
    using False
    by auto
  show ?thesis
  proof (cases n)
    case 0
    then show ?thesis
      using False assms
      by (metis add.right_neutral diff_is_0_eq diff_zero i_LTP_tau linorder_not_less)
  next
    case (Suc n')
    then show ?thesis
      using False assms
      by (cases i)
        (auto simp: Suc_le_eq not_le elim!: order.strict_trans[rotated] intro!: i_le_LTPi_minus)
  qed
qed

lemma LTP_minus_eq_iff:
  assumes "τ σ 0 + n ≤ τ σ i"
  shows "j = LTP σ (τ σ i - n) ⟷
  (case n of 0 ⇒ i ≤ j ∧ δ σ j i = 0 ∧ δ σ (Suc j) j > 0
  | _ ⇒ j ≤ i ∧ n ≤ δ σ i j ∧ δ σ i (Suc j) < n)"
proof (cases n)
  case 0
  show ?thesis
    using assms 0 i_LTP_tau[of σ "τ σ i" "LTP σ (τ σ i)"]
      i_LTP_tau[of σ "τ σ i" "Suc (LTP σ (τ σ i))"] i_LTP_tau[of σ "τ σ i" "j"]
      less_τD[of σ "(LTP σ (τ σ i))" "Suc j"]
    by (auto simp: i_le_LTPi not_le elim!: antisym dest!:
      order_antisym_conv[of "τ σ i" "τ σ j", THEN iffD1, rotated]
      order_antisym_conv[of "τ σ i" "τ σ (LTP σ (τ σ i))", THEN iffD1, rotated])
next
  case (Suc n')
  show ?thesis
    using assms
    by (simp add: Suc eq_iff[of j "LTP σ (τ σ i - Suc n')"] less_Suc_eq_le[of "LTP σ (τ σ i - Suc n')" j, symmetric] LTP_minus_ge_iff LTP_minus_lt_iff)
qed

lemma LTP_plus_eq_iff:
  shows "j = LTP σ (τ σ i + n) ⟷ (δ σ j i ≤ n ∧ δ σ (Suc j) i > n)"
  unfolding eq_iff[of j "LTP σ (τ σ i + n)"]
  by (meson LTP_plus_ge_iff linorder_not_less not_less_eq_eq)

lemma LTP_p_def: "τ σ 0 + left I ≤ τ σ i ⟹ LTP_p σ i I = (case left I of 0 ⇒ i | _ ⇒ LTP σ (τ σ i - left I))"
  using i_le_LTPi by (auto simp: min_def i_LTP_tau split: nat.splits)

definition "check_upt_LTP_p σ I li xs i ⟷ (case xs of [] ⇒
  (case left I of 0 ⇒ i < li | Suc n ⇒
    (if ¬ li ≤ i ∧ left I = 0 then 0 < δ σ li i else δ σ i li < left I))
  | _ ⇒ xs = [li..<li + length xs] ∧
    (case left I of 0 ⇒ li + length xs - 1 = i | Suc n ⇒
      (li + length xs - 1 ≤ i ∧ left I ≤ δ σ i (li + length xs - 1) ∧ δ σ i (li + length xs) < left I)))"

lemma check_upt_l_cong:
  assumes "⋀j. j ≤ max i li ⟹ τ σ j = τ σ' j"
  shows "check_upt_LTP_p σ I li xs i = check_upt_LTP_p σ' I li xs i"
proof -
  have "li + length ys ≤ i ⟹ Suc n ≤ δ σ' i (li + length ys) ⟹
    (Suc (li + length ys)) ≤ i" for ys :: "nat list" and n
    by (cases "li + length ys = i") auto
  then show ?thesis
    using assms
    by (fastforce simp: check_upt_LTP_p_def Let_def simp del: upt.simps split: list.splits nat.splits)
qed

lemma check_upt_LTP_p_eq:
  assumes "τ σ 0 + left I ≤ τ σ i"
  shows "xs = [li..<Suc (LTP_p σ i I)] ⟷ check_upt_LTP_p σ I li xs i"
proof -
  have "li + length xs = Suc (LTP_p σ i I) ⟷ li + length xs - 1 = LTP_p σ i I" if "xs ≠ []"
    using that
    by (cases xs) auto
  then have "xs = [li..<Suc (LTP_p σ i I)] ⟷ (xs = [] ∧ LTP_p σ i I < li) ∨
    (xs ≠ [] ∧ xs = [li..<li + length xs] ∧ li + length xs - 1 = LTP_p σ i I)"
    by auto
  moreover have "… ⟷ (xs = [] ∧
    (case left I of 0 ⇒ i < li | Suc n ⇒
      (if ¬ li ≤ i ∧ left I = 0 then 0 < δ σ li i else δ σ i li < left I))) ∨
    (xs ≠ [] ∧ xs = [li..<li + length xs] ∧
    (case left I of 0 ⇒ li + length xs - 1 = i | Suc n ⇒
      (case left I of 0 ⇒ i ≤ li + length xs - 1 ∧
        δ σ (li + length xs - 1) i = 0 ∧ 0 < δ σ (Suc (li + length xs - 1)) (li + length xs - 1)
      | Suc n ⇒ li + length xs - 1 ≤ i ∧
        left I ≤ δ σ i (li + length xs - 1) ∧ δ σ i (Suc (li + length xs - 1)) < left I)))"
    using LTP_p_def[OF assms, symmetric]
    unfolding LTP_minus_lt_iff[OF assms, symmetric]
    unfolding LTP_minus_eq_iff[OF assms, symmetric]
    by (auto split: nat.splits)
  moreover have "… ⟷ (case xs of [] ⇒
    (case left I of 0 ⇒ i < li | Suc n ⇒
      (if ¬ li ≤ i ∧ left I = 0 then 0 < δ σ li i else δ σ i li < left I))
    | _ ⇒ xs = [li..<li + length xs] ∧
      (case left I of 0 ⇒ li + length xs - 1 = i | Suc n ⇒
        (li + length xs - 1 ≤ i ∧ left I ≤ δ σ i (li + length xs - 1) ∧ δ σ i (li + length xs) < left I)))"
    by (auto split: nat.splits list.splits)
  ultimately show ?thesis
    unfolding check_upt_LTP_p_def
    by simp
qed

lemma v_check_exec_Once_code[code]: "v_check_exec σ vs (Formula.Once I φ) vp = (case vp of
  VOnce i li vps ⇒
    (case right I of ∞ ⇒ li = 0 | enat b ⇒ ((li = 0 ∨ b < δ σ i (li - 1)) ∧ δ σ i li ≤ b)) 
    ∧ τ σ 0 + left I ≤ τ σ i
    ∧ check_upt_LTP_p σ I li (map v_at vps) i ∧ Ball (set vps) (v_check_exec σ vs φ)
  | VOnceOut i ⇒ τ σ i < τ σ 0 + left I 
  | _ ⇒ False)"
  by (auto simp: Let_def check_upt_LTP_p_eq ETP_minus_le_iff ETP_minus_eq_iff split: vproof.splits enat.splits simp del: upt_Suc)

lemma s_check_exec_Historically_code[code]: "s_check_exec σ vs (Formula.Historically I φ) vp = (case vp of
  SHistorically i li vps ⇒
    (case right I of ∞ ⇒ li = 0 | enat b ⇒ ((li = 0 ∨ b < δ σ i (li - 1)) ∧ δ σ i li ≤ b))
    ∧ τ σ 0 + left I ≤ τ σ i
    ∧ check_upt_LTP_p σ I li (map s_at vps) i ∧ Ball (set vps) (s_check_exec σ vs φ)
  | SHistoricallyOut i ⇒ τ σ i < τ σ 0 + left I 
  | _ ⇒ False)"
  by (auto simp: Let_def check_upt_LTP_p_eq ETP_minus_le_iff ETP_minus_eq_iff split: sproof.splits enat.splits simp del: upt_Suc)

lemma v_check_exec_Since_code[code]: "v_check_exec σ vs (Formula.Since φ I ψ) vp = (case vp of
  VSince i vp1 vp2s ⇒
    let j = v_at vp1 in
    (case right I of ∞ ⇒ True | enat b ⇒ δ σ i j ≤ b) ∧ j ≤ i
    ∧ τ σ 0 + left I ≤ τ σ i
    ∧ check_upt_LTP_p σ I j (map v_at vp2s) i
    ∧ v_check_exec σ vs φ vp1 ∧ Ball (set vp2s) (v_check_exec σ vs ψ)
  | VSinceInf i li vp2s ⇒
    (case right I of ∞ ⇒ li = 0 | enat b ⇒ ((li = 0 ∨ b < δ σ i (li - 1)) ∧ δ σ i li ≤ b)) ∧
    τ σ 0 + left I ≤ τ σ i ∧
     check_upt_LTP_p σ I li (map v_at vp2s) i ∧ Ball (set vp2s) (v_check_exec σ vs ψ)
  | VSinceOut i ⇒ τ σ i < τ σ 0 + left I 
  | _ ⇒ False)"
  by (auto simp: Let_def check_upt_LTP_p_eq ETP_minus_le_iff ETP_minus_eq_iff split: vproof.splits enat.splits simp del: upt_Suc)

lemma ETP_f_le_iff: "max i (ETP σ (τ σ i + a)) ≤ j ⟷ i ≤ j ∧ δ σ j i ≥ a"
  by (metis add.commute max.bounded_iff τ_mono i_ETP_tau le_diff_conv2)

lemma ETP_f_ge_iff: "j ≤ max i (ETP σ (τ σ i + n)) ⟷ (case n of 0 ⇒ j ≤ i
  | Suc n' ⇒ (case j of 0 ⇒ True | Suc j' ⇒ δ σ j' i < n))"
proof (cases n)
  case 0
  then show ?thesis
    by (auto simp: max_def) (metis i_ge_etpi verit_la_disequality)
next
  case (Suc n')
  have max: "max i (ETP σ (τ σ i + n)) = ETP σ (τ σ i + n)"
    by (auto simp: max_def Suc)
       (metis Groups.ab_semigroup_add_class.add.commute ETP_ge less_or_eq_imp_le plus_1_eq_Suc)
  have "j ≤ max i (ETP σ (τ σ i + n)) ⟷ (∀ia. τ σ i + n ≤ τ σ ia ⟶ j ≤ ia)"
    unfolding max
    unfolding ETP_def
    by (meson LeastI_ex Least_le order.trans ex_le_τ)
  moreover have "… ⟷ (case j of 0 ⇒ True | Suc j' ⇒ ¬τ σ i + n ≤ τ σ j')"
    by (auto split: nat.splits) (meson i_ETP_tau le_trans not_less_eq_eq)
  moreover have "… ⟷ (case j of 0 ⇒ True | Suc j' ⇒ δ σ j' i < n)"
    by (auto simp: Suc split: nat.splits)
  ultimately show ?thesis
    by (auto simp: Suc)
qed

definition "check_upt_ETP_f σ I i xs hi ⟷ (let j = Suc hi - length xs in
  (case xs of [] ⇒ (case left I of 0 ⇒ Suc hi ≤ i | Suc n' ⇒ δ σ hi i < left I)
  | _ ⇒ (xs = [j..<Suc hi] ∧
  (case left I of 0 ⇒ j ≤ i | Suc n' ⇒
  (case j of 0 ⇒ True | Suc j' ⇒ δ σ j' i < left I)) ∧
  i ≤ j ∧ left I ≤ δ σ j i)))"

lemma check_upt_lu_cong:
  assumes "⋀j. min i hi ≤ j ∧ j ≤ max i hi ⟹ τ σ j = τ σ' j"
  shows "check_upt_ETP_f σ I i xs hi = check_upt_ETP_f σ' I i xs hi"
  using assms
  unfolding check_upt_ETP_f_def
  by (auto simp add: Let_def le_Suc_eq split: list.splits nat.splits)

lemma check_upt_ETP_f_eq: "xs = [ETP_f σ i I..<Suc hi] ⟷ check_upt_ETP_f σ I i xs hi"
proof -
  have F1: "(case left I of 0 ⇒ Suc hi ≤ i | Suc n' ⇒ δ σ hi i < left I) =
    (Suc hi ≤ ETP_f σ i I)"
    unfolding ETP_f_ge_iff[where ?j="Suc hi" and ?n="left I"]
    by (auto split: nat.splits)
  have "xs = [ETP_f σ i I..<Suc hi] ⟷ (let j = Suc hi - length xs in
    (xs = [] ∧ (case left I of 0 ⇒ Suc hi ≤ i | Suc n' ⇒ δ σ hi i < left I)) ∨
    (xs ≠ [] ∧ xs = [j..<Suc hi] ∧
    (case left I of 0 ⇒ j ≤ i | Suc n' ⇒
    (case j of 0 ⇒ True | Suc j' ⇒ δ σ j' i < left I)) ∧
    i ≤ j ∧ left I ≤ δ σ j i))"
    unfolding F1
    unfolding Let_def
    unfolding ETP_f_ge_iff[where ?n="left I", symmetric]
    unfolding ETP_f_le_iff[symmetric]
    unfolding eq_iff[of _ "ETP_f σ i I", symmetric]
    by auto
  moreover have "… ⟷ (let j = Suc hi - length xs in
    (case xs of [] ⇒ (case left I of 0 ⇒ Suc hi ≤ i | Suc n' ⇒ δ σ hi i < left I)
    | _ ⇒ (xs = [j..<Suc hi] ∧
    (case left I of 0 ⇒ j ≤ i | Suc n' ⇒
    (case j of 0 ⇒ True | Suc j' ⇒ δ σ j' i < left I)) ∧
    i ≤ j ∧ left I ≤ δ σ j i)))"
    by (auto simp: Let_def split: list.splits)
  finally show ?thesis
    unfolding check_upt_ETP_f_def .
qed

lemma v_check_exec_Eventually_code[code]: "v_check_exec σ vs (Formula.Eventually I φ) vp = (case vp of
  VEventually i hi vps ⇒
    (case right I of ∞ ⇒ False | enat b ⇒ (δ σ hi i ≤ b ∧ b < δ σ (Suc hi) i)) ∧
     check_upt_ETP_f σ I i (map v_at vps) hi ∧ Ball (set vps) (v_check_exec σ vs φ)
  | _ ⇒ False)"
  by (auto simp: Let_def LTP_plus_ge_iff LTP_plus_eq_iff check_upt_ETP_f_eq simp del: upt_Suc
      split: vproof.splits enat.splits)

lemma s_check_exec_Always_code[code]: "s_check_exec σ vs (Formula.Always I φ) sp = (case sp of
  SAlways i hi sps ⇒
    (case right I of ∞ ⇒ False | enat b ⇒ (δ σ hi i ≤ b ∧ b < δ σ (Suc hi) i)) 
    ∧ check_upt_ETP_f σ I i (map s_at sps) hi ∧ Ball (set sps) (s_check_exec σ vs φ)
  | _ ⇒ False)"
  by (auto simp: Let_def LTP_plus_ge_iff LTP_plus_eq_iff check_upt_ETP_f_eq simp del: upt_Suc
      split: sproof.splits enat.splits)

lemma v_check_exec_Until_code[code]: "v_check_exec σ vs (Formula.Until φ I ψ) vp = (case vp of
  VUntil i vp2s vp1 ⇒
    let j = v_at vp1 in 
    (case right I of ∞ ⇒ True | enat b ⇒ j < LTP_f σ i b)
    ∧ i ≤ j ∧ check_upt_ETP_f σ I i (map v_at vp2s) j
    ∧ v_check_exec σ vs φ vp1 ∧ Ball (set vp2s) (v_check_exec σ vs ψ)
 | VUntilInf i hi vp2s ⇒
    (case right I of ∞ ⇒ False | enat b ⇒ (δ σ hi i ≤ b ∧ b < δ σ (Suc hi) i)) ∧
     check_upt_ETP_f σ I i (map v_at vp2s) hi ∧ Ball (set vp2s) (v_check_exec σ vs ψ)
 | _ ⇒ False)"
  by (auto simp: Let_def LTP_plus_ge_iff LTP_plus_eq_iff check_upt_ETP_f_eq simp del: upt_Suc
      split: vproof.splits enat.splits)

subsection‹ETP/LTP setup›

lemma ETP_aux: "¬ t ≤ τ σ i ⟹ i ≤ (LEAST i. t ≤ τ σ i)"
  by (meson LeastI_ex τ_mono ex_le_τ nat_le_linear order_trans)

function ETP_rec where
  "ETP_rec σ t i = (if τ σ i ≥ t then i else ETP_rec σ t (i + 1))"
  by pat_completeness auto
termination
  using ETP_aux
  by (relation "measure (λ(σ, t, i). Suc (ETP σ t) - i)")
    (fastforce simp: ETP_def)+

lemma ETP_rec_sound: "ETP_rec σ t j = (LEAST i. i ≥ j ∧ t ≤ τ σ i)"
proof (induction σ t j rule: ETP_rec.induct)
  case (1 σ t i)
  show ?case
  proof (cases "τ σ i ≥ t")
    case True
    then show ?thesis
      by simp (metis (no_types, lifting) Least_equality order_refl)
  next
    case False
    then show ?thesis
      using 1[OF False]
      by (simp add: ETP_rec.simps[of _ _ i] del: ETP_rec.simps)
         (metis Suc_leD le_antisym not_less_eq_eq)
  qed
qed

lemma ETP_code[code]: "ETP σ t = ETP_rec σ t 0"
  using ETP_rec_sound[of σ t 0]
  by (auto simp: ETP_def)

lemma LTP_aux:
  assumes "τ σ (Suc i) ≤ t"
  shows "i ≤ Max {i. τ σ i ≤ t}"
proof -
  have "finite {i. τ σ i ≤ t}"
    by (smt (verit, del_insts) τ_mono finite_nat_set_iff_bounded_le i_LTP_tau le0 le_trans mem_Collect_eq) 
  moreover have "i ∈ {i. τ σ i ≤ t}"
    using le_trans[OF τ_mono[of i "Suc i" σ] assms]
    by auto
  ultimately show ?thesis
    by (rule Max_ge)
qed

function (sequential) LTP_rec where
  "LTP_rec σ t i = (if τ σ (Suc i) ≤ t then LTP_rec σ t (i + 1) else i)"
  by pat_completeness auto
termination
  using LTP_aux
  by (relation "measure (λ(σ, t, i). Suc (LTP σ t) - i)") (fastforce simp: LTP_def)+

lemma LTP_rec_sound: "LTP_rec σ t j = Max ({i. i ≥ j ∧ (τ σ i) ≤ t} ∪ {j})"
proof (induction σ t j rule: LTP_rec.induct)
  case (1 σ t j)
  have fin: "finite {i. j ≤ i ∧ τ σ i ≤ t}"
    by (smt (verit, del_insts) τ_mono finite_nat_set_iff_bounded_le i_LTP_tau le0 le_trans
        mem_Collect_eq)
  show ?case
  proof (cases "τ σ (Suc j) ≤ t")
    case True
    have diffI: "{i. Suc j ≤ i ∧ τ σ i ≤ t} = {i. j ≤ i ∧ τ σ i ≤ t} - {j}"
      by auto
    show ?thesis
      using 1[OF True] True fin
      by (auto simp del: LTP_rec.simps simp add: LTP_rec.simps[of _ _ j] diffI intro: max_aux)
  next
    case False
    then show ?thesis
      using fin
      by (auto simp: not_le intro!: Max_insert2[symmetric]
        dest!: order.strict_trans1 less_τD)
  qed
qed

lemma LTP_code[code]: "LTP σ t = (if t < τ σ 0
  then Code.abort (STR ''LTP: undefined'') (λ_. LTP σ t)
  else LTP_rec σ t 0)"
  using LTP_rec_sound[of σ t 0]
  by (auto simp: LTP_def insert_absorb simp del: LTP_rec.simps)

lemma map_part_code[code]: "Rep_part (map_part f xs) = map (map_prod id f) (Rep_part xs)"
  using Rep_part[of xs]
  by (auto simp: map_part_def intro!: Abs_part_inverse)

lemma coset_subset_set_code[code]:
  "(List.coset (xs :: _ :: universe list) ⊆ set ys) = (case universe of None ⇒ False
  | Some zs ⇒ ∀z ∈ set zs. z ∈ set xs ∨ z ∈ set ys)"
  using finite_compl finite_subset
  by (auto split: option.splits dest!: infinite finite)

lemma is_empty_coset[code]: "Set.is_empty (List.coset (xs :: _ :: universe list)) =
  (case universe of None ⇒ False
  | Some zs ⇒ ∀z ∈ set zs. z ∈ set xs)"
  using coset_subset_set_code[of xs] by (auto simp: Set.is_empty_def split: option.splits dest: infinite finite)

subsection ‹Exported functions›

type_synonym name = string8

declare Formula.future_bounded.simps[code]

definition collect_paths :: "('n, 'd :: {default, linorder}) trace ⇒ ('n, 'd) formula ⇒ ('n, 'd) expl ⇒ 'd set list set option" where
  "collect_paths σ φ e = (if (distinct_paths e ∧ check_all_aux σ (λ_. UNIV) φ e) then None else Some (collect_paths_aux {[]} σ (λ_. UNIV) φ e))"

definition check :: "(name, event_data) trace ⇒ (name, event_data) formula ⇒ (name, event_data) expl ⇒ bool" where
  "check = check_all"

definition collect_paths_specialized :: "(name, event_data) trace ⇒ (name, event_data) formula ⇒ (name, event_data) expl ⇒ event_data set list set option" where
  "collect_paths_specialized = collect_paths"

definition trace_of_list_specialized :: "((name × event_data list) set × nat) list ⇒ (name, event_data) trace" where
  "trace_of_list_specialized xs = trace_of_list xs"

definition specialized_set :: "(name × event_data list) list ⇒ (name × event_data list) set" where
  "specialized_set = set"

definition ed_set :: "event_data list ⇒ event_data set" where
  "ed_set = set"

definition sum_nat :: "nat ⇒ nat ⇒ nat" where
  "sum_nat m n = m + n"

definition sub_nat :: "nat ⇒ nat ⇒ nat" where
  "sub_nat m n = m - n"

lift_definition abs_part :: "(event_data set × 'a) list ⇒ (event_data, 'a) part" is
  "λxs.
   let Ds = map fst xs in
   if {} ∈ set Ds
   ∨ (∃D ∈ set Ds. ∃E ∈ set Ds. D ≠ E ∧ D ∩ E ≠ {})
   ∨ ¬ distinct Ds
   ∨ (⋃D ∈ set Ds. D) ≠ UNIV then [(UNIV, undefined)] else xs"
  by (auto simp: partition_on_def disjoint_def)

export_code interval enat nat_of_integer integer_of_nat
  STT Formula.TT Inl EInt Formula.Var Leaf set part_hd sum_nat sub_nat subsvals
  check trace_of_list_specialized specialized_set ed_set abs_part 
  collect_paths_specialized
  in OCaml module_name Checker file_prefix "checker"

(*<*)
end
(*>*)