Theory Simple_Network_Language_Model_Checking

theory Simple_Network_Language_Model_Checking
  imports Munta_Base.Temporal_Logics
    Simple_Network_Language_Impl_Refine
    Munta_Model_Checker.UPPAAL_Model_Checking
begin

section ‹Product Bisimulation›

no_notation State_Networks.step_sn ("_ ⊢ ⟨_, _, _⟩ →⇘_⇙ ⟨_, _, _⟩" [61,61,61,61,61] 61)

text ‹
  We have proved the necessary theorems already but we need to lift it to
  the case where delay and action transitions are strictly alternating.
›
inductive step_u' ::
  "('a, 's, 'c, 't :: time, 'x, 'v :: linorder) nta ⇒ 's list ⇒ ('x ⇀ 'v) ⇒ ('c, 't) cval
  ⇒ 's list ⇒ ('x ⇀ 'v) ⇒ ('c, 't) cval ⇒ bool"
("_ ⊢ ⟨_, _, _⟩ → ⟨_, _, _⟩" [61,61,61,61] 61) where
  "A ⊢ ⟨L, s, u⟩ → ⟨L'', s'', u''⟩" if
  "A ⊢ ⟨L, s, u⟩ →⇘Del⇙ ⟨L', s', u'⟩"
  "a ≠ Del"
  "A ⊢ ⟨L', s', u'⟩ →⇘a⇙ ⟨L'', s'', u''⟩"

inductive_cases step'_elims: "A ⊢' ⟨(L, s), u⟩ → ⟨(L', s'), u'⟩"

inductive_cases step_u'_elims: "A ⊢ ⟨L, s, u⟩ → ⟨L', s', u'⟩"

theorem Bisimulation_Invariant_strong_intro:
  fixes A :: "'a ⇒ 'a ⇒ bool"
    and P :: "'a ⇒ bool"
    and B :: "'a ⇒ 'a ⇒ bool"
  assumes "⋀a b. A a b ⟹ P a ⟹ B a b"
    and "⋀a b. B a b ⟹ P a ⟹ A a b"
    and "⋀a b. P a ⟹ A a b ⟹ P b"
  shows "Bisimulation_Invariant A B (=) P P"
  apply standard
  subgoal A for a b a'
    by (blast intro: assms)
  subgoal B for a b a'
    by (blast intro: assms)
  subgoal C for a b
    by (rule assms)
  subgoal D for a b
    by (rule C, assumption) (rule assms)
  done

context Prod_TA_Defs
begin

definition
  "all_prop L s = (L ∈ states ∧ bounded bounds s)"

lemma all_prop_boundedD[dest]:
  "bounded bounds s" if "all_prop L s"
  using that unfolding all_prop_def ..

lemma all_prop_statesD[dest]:
  "L ∈ states" if "all_prop L s"
  using that unfolding all_prop_def ..

end (* Prod TA Defs *)


context Prod_TA
begin

lemma prod_action_step_not_eq_delay:
  "a ≠ Del" if "prod_ta ⊢ ⟨(L, s), u⟩ →⇘a⇙ ⟨(L', s'), u'⟩"
  using that
  apply cases
  unfolding trans_of_def
  unfolding prod_ta_def trans_prod_def
  by (auto simp: trans_int_def trans_bin_def trans_broad_def)

end

locale Prod_TA_urge =
  Prod_TA + assumes urgency_removed: "∀N ∈ set (fst (snd A)). urgent N = {}"
begin

lemma prod_all_prop_inv:
  "all_prop L' s'" if "all_prop L s" "prod_ta ⊢ ⟨(L, s), u⟩ → ⟨(L', s'), u'⟩"
  using that unfolding all_prop_def
  by (auto elim: bounded_inv states_inv simp: step_iff[symmetric, OF _ _ urgency_removed])

lemma prod_all_prop_inv':
  "all_prop L' s'" if "all_prop L s" "prod_ta ⊢' ⟨(L, s), u⟩ → ⟨(L', s'), u'⟩"
  using that by (auto intro: prod_all_prop_inv elim!: step'_elims)

interpretation prod_bisim:
  Bisimulation_Invariant
  "(λ (L, s, u) (L', s', u'). prod_ta ⊢' ⟨(L, s), u⟩ → ⟨(L', s'), u'⟩)"
  "(λ (L, s, u) (L', s', u'). A ⊢ ⟨L, s, u⟩ → ⟨L', s', u'⟩)"
  "(=)"
  "(λ (L, s, u). all_prop L s)"
  "(λ (L, s, u). all_prop L s)"
  apply (rule Bisimulation_Invariant_strong_intro; clarsimp)
  subgoal
    by (auto intro: step_u'.intros simp: all_prop_def
             dest: action_sound prod_action_step_not_eq_delay delay_sound[OF _ _ _ urgency_removed]
             elim!: step'_elims)
  subgoal
    by (auto 4 4 dest: prod_all_prop_inv action_complete elim: delay_complete elim!: step_u'_elims)
  subgoal
    by (rule prod_all_prop_inv')
  done

lemmas prod_bisim_intro = prod_bisim.Bisimulation_Invariant_axioms

end (* Prod TA *)


section ‹The Final Semantics›

text ‹State formulas›
datatype ('n, 's, 'a, 'b) sexp =
  true |
  ― ‹Boolean connectives›
  not "('n, 's, 'a, 'b) sexp" | "and" "('n, 's, 'a, 'b) sexp" "('n, 's, 'a, 'b) sexp" |
  or "('n, 's, 'a, 'b) sexp" "('n, 's, 'a, 'b) sexp" | imply "('n, 's, 'a, 'b) sexp" "('n, 's, 'a, 'b) sexp" |
  ― ‹Does var ‹a› equal ‹x›?›
  eq 'a 'b |
  le 'a 'b |
  lt 'a 'b |
  ge 'a 'b |
  gt 'a 'b |
  ― ‹Is procces ‹i› in location ‹l›?›
  loc 'n 's

datatype ('n, 's, 'a, 'b) formula =
  EX "('n, 's, 'a, 'b) sexp" | EG "('n, 's, 'a, 'b) sexp"
| AX "('n, 's, 'a, 'b) sexp" | AG "('n, 's, 'a, 'b) sexp"
| Leadsto "('n, 's, 'a, 'b) sexp" "('n, 's, 'a, 'b) sexp"

fun check_sexp :: "(nat, 's, 'a, 'b :: linorder) sexp ⇒ 's list ⇒ ('a ⇒ 'b) ⇒ bool" where
  "check_sexp sexp.true _ _ ⟷ True" |
  "check_sexp (not e) L s ⟷ ¬ check_sexp e L s" |
  "check_sexp (and e1 e2) L s ⟷ check_sexp e1 L s ∧ check_sexp e2 L s" |
  "check_sexp (sexp.or e1 e2) L s ⟷ check_sexp e1 L s ∨ check_sexp e2 L s" |
  "check_sexp (imply e1 e2) L s ⟷ check_sexp e1 L s ⟶ check_sexp e2 L s" |
  "check_sexp (eq i x) L s ⟷ s i = x" |
  "check_sexp (le i x) L s ⟷ s i ≤ x" |
  "check_sexp (lt i x) L s ⟷ s i < x" |
  "check_sexp (ge i x) L s ⟷ s i ≥ x" |
  "check_sexp (gt i x) L s ⟷ s i > x" |
  "check_sexp (loc i x) L s ⟷ L ! i = x"

fun locs_of_sexp :: "('n, 's, 'a, 'b) sexp ⇒ 'n set" where
  "locs_of_sexp (not e) = locs_of_sexp e" |
  "locs_of_sexp (and e1 e2) = locs_of_sexp e1 ∪ locs_of_sexp e2" |
  "locs_of_sexp (sexp.or e1 e2) = locs_of_sexp e1 ∪ locs_of_sexp e2" |
  "locs_of_sexp (imply e1 e2) = locs_of_sexp e1 ∪ locs_of_sexp e2" |
  "locs_of_sexp (loc i x) = {i}" |
  "locs_of_sexp _ = {}"

fun vars_of_sexp :: "('n, 's, 'a, 'b) sexp ⇒ 'a set" where
  "vars_of_sexp (not e) = vars_of_sexp e" |
  "vars_of_sexp (and e1 e2) = vars_of_sexp e1 ∪ vars_of_sexp e2" |
  "vars_of_sexp (sexp.or e1 e2) = vars_of_sexp e1 ∪ vars_of_sexp e2" |
  "vars_of_sexp (imply e1 e2) = vars_of_sexp e1 ∪ vars_of_sexp e2" |
  "vars_of_sexp (eq i x) = {i}" |
  "vars_of_sexp (lt i x) = {i}" |
  "vars_of_sexp (le i x) = {i}" |
  "vars_of_sexp (ge i x) = {i}" |
  "vars_of_sexp (gt i x) = {i}" |
  "vars_of_sexp _ = {}"

fun locs_of_formula :: "('n, 's, 'a, 'b) formula ⇒ 'n set" where
  "locs_of_formula (formula.EX φ) = locs_of_sexp φ" |
  "locs_of_formula (EG φ) = locs_of_sexp φ" |
  "locs_of_formula (AX φ) = locs_of_sexp φ" |
  "locs_of_formula (AG φ) = locs_of_sexp φ" |
  "locs_of_formula (Leadsto φ ψ) = locs_of_sexp φ ∪ locs_of_sexp ψ"

fun vars_of_formula :: "('n, 's, 'a, 'b) formula ⇒ 'a set" where
  "vars_of_formula (formula.EX φ) = vars_of_sexp φ" |
  "vars_of_formula (EG φ) = vars_of_sexp φ" |
  "vars_of_formula (AX φ) = vars_of_sexp φ" |
  "vars_of_formula (AG φ) = vars_of_sexp φ" |
  "vars_of_formula (Leadsto φ ψ) = vars_of_sexp φ ∪ vars_of_sexp ψ"

fun hd_of_formula :: "(nat, 's, 'a, 'b) formula ⇒ 's list ⇒ ('a ⇒ 'b :: linorder) ⇒ bool" where
  "hd_of_formula (formula.EX φ) L s = check_sexp φ L s" |
  "hd_of_formula (EG φ) L s = check_sexp φ L s" |
  "hd_of_formula (AX φ) L s = Not (check_sexp φ L s)" |
  "hd_of_formula (AG φ) L s = Not (check_sexp φ L s)" |
  "hd_of_formula (Leadsto φ _) L s = check_sexp φ L s"

definition models ("_,_ ⊨ _" [61,61] 61) where
  "A,a0 ⊨ Φ ≡ (case Φ of
    formula.EX φ ⇒
      Graph_Defs.Ex_ev
        (λ (L, s, u) (L', s', u'). A ⊢ ⟨L, s, u⟩ → ⟨L', s', u'⟩)
        (λ (L, s, _). check_sexp φ L (the o s))
  | formula.EG φ ⇒
      Graph_Defs.Ex_alw
        (λ (L, s, u) (L', s', u'). A ⊢ ⟨L, s, u⟩ → ⟨L', s', u'⟩)
        (λ (L, s, _). check_sexp φ L (the o s))
  | formula.AX φ ⇒
      Graph_Defs.Alw_ev
        (λ (L, s, u) (L', s', u'). A ⊢ ⟨L, s, u⟩ → ⟨L', s', u'⟩)
        (λ (L, s, _). check_sexp φ L (the o s))
  | formula.AG φ ⇒
      Graph_Defs.Alw_alw
        (λ (L, s, u) (L', s', u'). A ⊢ ⟨L, s, u⟩ → ⟨L', s', u'⟩)
        (λ (L, s, _). check_sexp φ L (the o s))
  | formula.Leadsto φ ψ ⇒
      Graph_Defs.leadsto
        (λ (L, s, u) (L', s', u'). A ⊢ ⟨L, s, u⟩ → ⟨L', s', u'⟩)
        (λ (L, s, _). check_sexp φ L (the o s))
        (λ (L, s, _). check_sexp ψ L (the o s))
  ) a0"

lemmas models_iff = models_def[unfolded Graph_Defs.Ex_alw_iff Graph_Defs.Alw_alw_iff]

definition prop_of where
  "prop_of φ = PropC (λ(L, s, _). check_sexp φ L (the o s))"

fun ctl_of where
  "ctl_of (formula.EX φ) = ctl_formula.EX (prop_of φ)"
| "ctl_of (formula.EG φ) = ctl_formula.EG (prop_of φ)"
| "ctl_of (formula.AX φ) = ctl_formula.AX (prop_of φ)"
| "ctl_of (formula.AG φ) = ctl_formula.AG (prop_of φ)"
| "ctl_of (formula.Leadsto φ ψ) =
  ctl_formula.AG (ctl_formula.ImpliesC (prop_of φ) (ctl_formula.AX (prop_of ψ)))"

context
  fixes A :: "('a, 's, 'c, 't :: time, 'x, 'v :: linorder) nta"
begin

interpretation Graph_Defs "λ (L, s, u) (L', s', u'). A ⊢ ⟨L, s, u⟩ → ⟨L', s', u'⟩" .

lemma models_ctl_iff:
  "A,a0 ⊨ Φ ⟷ models_ctl (ctl_of Φ) a0"
  by (cases Φ) (simp_all add: models_def prop_of_def leadsto_def)

end

fun check_sexpi :: "(nat, 's, nat, int) sexp ⇒ 's list ⇒ int list ⇒ bool" where
  "check_sexpi sexp.true _ _ ⟷ True" |
  "check_sexpi (not e) L s ⟷ ¬ check_sexpi e L s" |
  "check_sexpi (and e1 e2) L s ⟷ check_sexpi e1 L s ∧ check_sexpi e2 L s" |
  "check_sexpi (sexp.or e1 e2) L s ⟷ check_sexpi e1 L s ∨ check_sexpi e2 L s" |
  "check_sexpi (imply e1 e2) L s ⟷ check_sexpi e1 L s ⟶ check_sexpi e2 L s" |
  "check_sexpi (eq i x) L s ⟷ s ! i = x" |
  "check_sexpi (le i x) L s ⟷ s ! i ≤ x" |
  "check_sexpi (lt i x) L s ⟷ s ! i < x" |
  "check_sexpi (ge i x) L s ⟷ s ! i ≥ x" |
  "check_sexpi (gt i x) L s ⟷ s ! i > x" |
  "check_sexpi (loc i x) L s ⟷ L ! i = x"

fun hd_of_formulai :: "(nat, 's, nat, int) formula ⇒ 's list ⇒ int list ⇒ bool" where
  "hd_of_formulai (formula.EX φ) L s = check_sexpi φ L s" |
  "hd_of_formulai (EG φ) L s = check_sexpi φ L s" |
  "hd_of_formulai (AX φ) L s = Not (check_sexpi φ L s)" |
  "hd_of_formulai (AG φ) L s = Not (check_sexpi φ L s)" |
  "hd_of_formulai (Leadsto φ _) L s = check_sexpi φ L s"



(* Stop locale constant unfolding in simplifier *)
lemma all_prop_weak_cong[cong]:
  "Prod_TA_Defs.all_prop A = Prod_TA_Defs.all_prop A" for A
  by(rule HOL.refl)
lemma equiv'_weak_cong[cong]:
  "Bisimulation_Invariant.equiv' R P Q = Bisimulation_Invariant.equiv' R P Q" for R P Q
  by (rule HOL.refl)
lemma equiv'_weak_cong2[cong]:
  "Simulation_Invariant.equiv' R P Q = Simulation_Invariant.equiv' R P Q" for R P Q
  by (rule HOL.refl)
lemma models_ctl_weak_cong[cong]:
  "Graph_Defs.models_ctl E = Graph_Defs.models_ctl E" for E
  by (rule HOL.refl)
lemma models_path_weak_cong[cong]:
  "Graph_Defs.models_path E = Graph_Defs.models_path E" for E
  by (rule HOL.refl)
lemma models_state_weak_cong[cong]:
  "Graph_Defs.models_state E = Graph_Defs.models_state E" for E
  by (rule HOL.refl)
lemma models_ltl_weak_cong[cong]:
  "Graph_Defs.models_ltlc E = Graph_Defs.models_ltlc E" for E
  by (rule HOL.refl)
lemma models_weak_cong[cong]:
  "models E = models E"
  for E by (rule HOL.refl)




section ‹Instantiating the Model Checking Locale›

locale Simple_Network_Impl_nat_urge =
  Simple_Network_Impl_nat + assumes no_urgency: "∀ (_, U, _, _) ∈ set automata. U = []"

text ‹
  This locale certifies that a given local clock ceiling is correct.
  Moreover, we certify that the vector of initial locations has outgoing transitions for
  each automaton, and that all variables of the initial state are in bounds.
›
locale Simple_Network_Impl_nat_ceiling_start_state =
  Simple_Network_Impl_nat_urge +
  fixes k :: "nat list list list"
    and L0 :: "nat list"
    and s0 :: "(nat × int) list"
    and formula :: "(nat, nat, nat, int) formula"
    and show_clock :: "nat ⇒ string"
    and show_state :: "nat list × int list ⇒ string"
  assumes k_ceiling:
    "∀i < n_ps. ∀(l, g) ∈ set ((snd o snd o snd) (automata ! i)).
      ∀(x, m) ∈ collect_clock_pairs g. m ≤ int (k ! i ! l ! x)"
    "∀i < n_ps. ∀(l, _, g, _) ∈ set ((fst o snd o snd) (automata ! i)).
      (∀(x, m) ∈ collect_clock_pairs g. m ≤ int (k ! i ! l ! x))"
  and k_resets:
    "∀i < n_ps. ∀ (l, b, g, a, upd, r, l') ∈ set ((fst o snd o snd) (automata ! i)).
       ∀c ∈ {0..<m+1} - set r. k ! i ! l' ! c ≤ k ! i ! l ! c"
  and k_length:
    "length k = n_ps" "∀ i < n_ps. length (k ! i) = num_states i"
    "∀ xs ∈ set k. ∀ xxs ∈ set xs. length xxs = m + 1"
  and k_0:
    "∀i < n_ps. ∀l < num_states i. k ! i ! l ! 0 = 0"
  and inv_unambiguous:
    "∀(_, _, _, inv) ∈ set automata. distinct (map fst inv)"
  and s0_bounded: "bounded bounds (map_of s0)"
  and L0_len: "length L0 = n_ps"
  and L0_has_trans: "∀i < n_ps. L0 ! i ∈ fst ` set ((fst o snd o snd) (automata ! i))"
  and vars_of_formula: "vars_of_formula formula ⊆ {0..<n_vs}"
  (* and num_states_length: "∀i<n_ps. num_states i = length (fst (snd (automata ! i)))" *)
begin

text ‹
The ceiling ‹k› is correct for each individual automaton in the network.
We now construct a ceiling for the product automaton:
›
definition
  "k_fun l c ≡
    if (c > 0 ∧ c ≤ m) ∧ fst l ∈ states then Max {k ! i ! (fst l ! i) ! c | i . i < n_ps} else 0"

lemma (in -) default_map_of_distinct:
  "(k, default_map_of x xs k) ∈ set xs ∪ {(k, x)}" if "distinct (map fst xs)"
  unfolding default_map_of_alt_def by clarsimp (simp add: map_of_eq_Some_iff[OF that])

lemma N_inv:
  "(L ! i, inv (N i) (L ! i)) ∈ set ((snd o snd o snd) (automata ! i)) ∪ {(L ! i, [])}"
  if "i < n_ps"
  unfolding N_def comp_def fst_conv snd_conv inv_def
  using that
  apply (subst nth_map)
   apply (simp add: n_ps_def; fail)
  apply (clarsimp split: prod.split simp: automaton_of_def)
  subgoal for _ _ _ xs
    using default_map_of_distinct[of xs "L ! i" "[]"] inv_unambiguous that
    by (auto dest!: nth_mem simp: n_ps_def)
  done

lemma (in -) subset_nat_0_atLeastLessThan_conv:
  "S ⊆ {0..<n::nat} ⟷ (∀ x ∈ S. x < n)"
  by auto

lemma k_ceiling_rule:
  "m ≤ int (k ! i ! l ! x)"
  if "i < n_ps" "(l, b, g, xx) ∈ set ((fst o snd o snd) (automata ! i))"
     "(x, m) ∈ collect_clock_pairs g"
  for i l x g xx
  using that k_ceiling(2) by fastforce

lemma k_ceiling_1:
  "∀s. ∀L ∈ states. ∀(x,m) ∈ clkp_set prod_ta (L, s). m ≤ k_fun (L, s) x"
proof safe
  fix L s c x
  assume ‹L ∈ states› ‹(c, x) ∈ Closure.clkp_set prod_ta (L, s)›
  have "0 < c" "c ≤ m"
  proof -
    from ‹(c, x) ∈ _› have "(c, x) ∈ Timed_Automata.clkp_set prod_ta"
      unfolding TA_clkp_set_unfold by auto
    with clock_range show "0 < c" "c ≤ m"
      by auto
  qed
  with ‹L ∈ _› have "k_fun (L, s) c = Max {k ! i ! (L ! i) ! c | i . i < n_ps}"
    unfolding k_fun_def by auto
  have Max_aux: "x ≤ int (Max {k ! i ! (L ! i) ! c |i. i < n_ps})"
    if "x ≤ int (k ! p ! (L ! p) ! c)" "p < n_ps" for p
  proof -
    from ‹p < n_ps › have "k ! p ! (L ! p) ! c ≤ Max {k ! i ! (L ! i) ! c |i. i < n_ps}"
      by (intro Max_ge) auto
    with ‹x ≤ _› show ?thesis
      by simp
  qed
  from ‹(c, x) ∈ _› show ‹x ≤ k_fun (L, s) c›
    unfolding clkp_set_def
  proof safe
    assume ‹(c, x) ∈ Closure.collect_clki (inv_of prod_ta) (L, s)›
    then show ‹x ≤ k_fun (L, s) c›
      using k_ceiling(1) unfolding collect_clki_def ‹k_fun (L, s) c = _›
      by (auto 0 8 dest: N_inv
          intro!: Max_aux simp: prod_inv_def collect_clock_pairs_def k_fun_def)
  next
    assume ‹(c, x) ∈ Closure.collect_clkt (trans_of prod_ta) (L, s)›
    then show ‹x ≤ k_fun (L, s) c›
      unfolding collect_clkt_def ‹k_fun (L, s) c = _›
      apply (clarsimp simp: trans_prod_def collect_clock_pairs_def k_fun_def)
      apply safe
      subgoal
        using k_ceiling(2) unfolding trans_int_def
        apply (clarsimp simp: mem_trans_N_iff L_len subset_nat_0_atLeastLessThan_conv)
        apply (fastforce intro!: Max_aux simp: collect_clock_pairs_def)
        done
      subgoal
        using k_ceiling(2) unfolding trans_bin_def
        apply (clarsimp simp: mem_trans_N_iff L_len subset_nat_0_atLeastLessThan_conv)
        apply (erule disjE)
         apply (force intro!: Max_aux simp: collect_clock_pairs_def)+
        done
      subgoal
        using k_ceiling(2) unfolding trans_broad_def
        apply (clarsimp simp: mem_trans_N_iff L_len subset_nat_0_atLeastLessThan_conv)
        apply (erule disjE)
         apply (fastforce intro!: Max_aux simp: collect_clock_pairs_def)
        apply (erule bexE)
        apply (force intro!: Max_aux simp: collect_clock_pairs_def) ― ‹slow: 60s›
        done
      done
  qed
qed

lemma k_fun_mono':
  "k_fun (L, s) c ≤ k_fun (L', s') c" if
  "∀i < n_ps. k ! i ! (L ! i) ! c ≤ k ! i ! (L' ! i) ! c" "L ∈ states" "L' ∈ states"
  using that unfolding k_fun_def
  apply clarsimp
  apply (cases "n_ps = 0")
   apply (simp; fail)
  apply (rule Max.boundedI)
    apply (simp; fail)
   apply blast
  apply safe
  subgoal for _ i
    by - (rule order.trans[where b = "k ! i ! (L' ! i) ! c"], auto intro: Max_ge)
  done

lemma k_fun_mono:
  ‹Max {k ! i ! (L ! i) ! c | i . i < n_ps} ≤ Max {k ! i ! (L' ! i) ! c | i . i < n_ps}›
  if ‹∀i < n_ps. k ! i ! (L ! i) ! c ≤ k ! i ! (L' ! i) ! c›
  apply (cases "n_ps = 0")
   apply (simp; fail)
  apply (rule Max.boundedI)
    apply (simp; fail)
   apply blast
  apply safe
  subgoal for _ i
    using that by - (rule order.trans[where b = "k ! i ! (L' ! i) ! c"], auto intro: Max_ge)
  done

lemma (in -) fold_upds_aux1:
  "fold (λp L. L[p := g p]) ps xs ! i = xs ! i" if ‹i ∉ set ps›
  using that by (induction ps arbitrary: xs) auto

lemma (in -) fold_upds_aux2:
  "fold (λp L. L[p := g p]) ps xs ! i = g i" if ‹distinct ps› ‹i ∈ set ps› ‹i < length xs›
  using that by (induction ps arbitrary: xs) (auto simp: fold_upds_aux1)

lemma (in -) fold_upds_aux_length:
  "length (fold (λp L. L[p := g p]) ps xs) = length xs"
  by (induction ps arbitrary: xs) auto

lemma prod_ta_step_statesD:
  assumes "prod_ta ⊢ (L, s) ⟶⇗g,a,r⇖ (L', s')"
  shows "L ∈ states" "L' ∈ states"
  using assms state_set_states by (fastforce dest: state_setI1 state_setI2)+

lemma k_ceiling_2:
  "∀l g a r l'. ∀ c ≤ m. prod_ta ⊢ l ⟶⇗g,a,r⇖ l' ∧ c ∉ set r ⟶ k_fun l' c ≤ k_fun l c"
proof safe
  fix L s g a r L' s' c
  assume A: ‹c ≤ m› ‹prod_ta ⊢ (L, s) ⟶⇗g,a,r⇖ (L', s')› ‹c ∉ set r›
  then have "L ∈ states" "L' ∈ states"
    by - (rule prod_ta_step_statesD, assumption)+
  from A have ‹Max {k ! i ! (L' ! i) ! c | i . i < n_ps} ≤ Max {k ! i ! (L ! i) ! c | i . i < n_ps}›
    apply simp
    unfolding trans_prod_def
    apply safe
    subgoal
      using k_resets
      unfolding trans_int_def
      apply clarsimp
      apply (rule k_fun_mono)
      apply (clarsimp simp: mem_trans_N_iff L_len subset_nat_0_atLeastLessThan_conv)
      subgoal for b f p aa l' i
        by (cases "p = i"; force simp add: L_len)
      done
    subgoal
      using k_resets
      unfolding trans_bin_def
      apply clarsimp
      apply (rule k_fun_mono)
      apply (clarsimp simp: mem_trans_N_iff L_len subset_nat_0_atLeastLessThan_conv)
      subgoal for _ _ p q b1 g1 f1 r1 l1' b2 g2 f2 r2 l2' i
        by (cases "p = i"; cases "q = i"; force simp add: L_len)
      done
    subgoal
      using k_resets
      unfolding trans_broad_def
      apply clarsimp
      apply (rule k_fun_mono)
      apply (clarsimp simp: mem_trans_N_iff L_len subset_nat_0_atLeastLessThan_conv)
      subgoal premises prems for s'a aa p b ga f ra l' bs gs fs rs ls' ps i
      proof (cases "p = i")
        case True
        with ‹p ∉ _› ‹i < _› ‹L ∈ states› have "(fold (λp L. L[p := ls' p]) ps L)[p := l'] ! i = l'"
          by (simp add: L_len fold_upds_aux_length)
        with prems ‹p = i› show ?thesis
          by (fastforce simp add: L_len)
      next
        case False
        then have *: "(fold (λp L. L[p := ls' p]) ps L)[p := l'] ! i
          = fold (λp L. L[p := ls' p]) ps L ! i"
          by simp
        show ?thesis
        proof (cases "i ∈ set ps")
          case True
          then have **: "fold (λp L. L[p := ls' p]) ps L ! i = ls' i"
            using ‹distinct ps› ‹i < n_ps› ‹L ∈ states› by (auto simp: fold_upds_aux2)
          moreover have
            "(L ! i, bs i, gs i, In aa, fs i, rs i, ls' i) ∈ set (fst (snd (snd (automata ! i))))"
            using ‹p ≠ i› True prems by fast
          moreover have "c∈{0..<Suc m} - set (rs i)"
            using ‹p ≠ i› True prems by force
          ultimately show ?thesis
            using prems(2) ‹i < n_ps› by (auto 4 3 simp add: *)
        next
          case False
          with ‹p ≠ i› show ?thesis
            by (simp add: fold_upds_aux1)
        qed
      qed
      done
    done
  with ‹L ∈ states› ‹L' ∈ states› ‹c ≤ m› show "k_fun (L', s') c ≤ k_fun (L, s) c"
    by (auto simp: k_fun_def)
qed



abbreviation F where "F ≡ λ(L, s). hd_of_formula formula L (the o s)"
abbreviation "Fi ≡ λ(L, s). hd_of_formulai formula L s"

lemma (in Simple_Network_Impl_nat) check_sexp_check_sexpi:
  "check_sexp e L (the o s) ⟷ check_sexpi e L s'"
  if "state_rel s s'" "vars_of_sexp e ⊆ {0..<n_vs}"
  using that unfolding state_rel_def by (induction e) auto

lemma (in Simple_Network_Impl_nat) hd_of_formula_hd_of_formulai:
  "hd_of_formula φ L (the o s) ⟷ hd_of_formulai φ L s'"
  if "state_rel s s'" "vars_of_formula φ ⊆ {0..<n_vs}"
  using that by (induction φ) (auto simp: check_sexp_check_sexpi)

lemma F_Fi:
  "F l ⟷ Fi l'" if "(l', l) ∈ loc_rel"
  using vars_of_formula that unfolding loc_rel_def by clarsimp (erule hd_of_formula_hd_of_formulai)


abbreviation "l0 ≡ (L0, map_of s0)"
abbreviation "s0i ≡ map (the o map_of s0) [0..<n_vs]"
abbreviation "l0i ≡ (L0, s0i)"

lemma state_rel_start:
  "state_rel (map_of s0) s0i"
  using s0_bounded unfolding state_rel_def bounded_def dom_bounds_eq by auto

lemma statesI:
  "L ∈ states" if "length L = n_ps" "∀i<n_ps. L ! i ∈ fst ` set (fst (snd (snd (automata ! i))))"
  using that unfolding states_def by (auto 4 3 simp: mem_trans_N_iff[symmetric])

lemma L0_states[simp, intro]:
  "L0 ∈ states"
  using L0_has_trans L0_len by (auto intro: statesI)

lemma l0_states'[simp, intro]:
  "l0 ∈ states'"
  using state_rel_start s0_bounded unfolding states'_def state_rel_def by auto

sublocale reach: Reachability_Problem_Defs
  prod_ta
  l0
  m
  k_fun
  F
  .

lemma (in -) collect_clkt_state_setI:
  assumes "(x, d) ∈ Closure.collect_clkt (trans_of A) l"
  shows "l ∈ state_set (trans_of A)" "l ∈ Simulation_Graphs_TA.state_set A"
  using assms unfolding collect_clkt_def by (auto simp: state_set_def)

lemma clkp_set_statesD:
  fixes x d
  assumes "(x, d)∈Closure.clkp_set prod_ta (L, s)"
  shows "L ∈ states"
  using assms
  unfolding clkp_set_def collect_clki_def
  apply safe
  subgoal
    apply simp
    unfolding prod_inv_def
    unfolding collect_clock_pairs_def
    apply auto
    done
  apply (drule collect_clkt_state_setI)
  using state_set_states by auto

sublocale reach1: Reachability_Problem
  prod_ta
  l0
  m
  k_fun
  F
  apply standard
  subgoal
    apply safe
    using k_ceiling_1
    subgoal for L s x m
      apply (cases "L ∈ states")
       apply blast
      apply (auto dest: clkp_set_statesD simp: k_fun_def)
      done
    done
  subgoal
    apply safe
    subgoal for L s g a r L' s' c
      apply (cases "c ≤ m")
      using k_ceiling_2
       apply force
      apply (auto simp: k_fun_def)
      done
    done
  subgoal
    by (simp add: k_fun_def)
  subgoal
    by (simp add: k_fun_def)
  done  ― ‹slow: 60s›

lemma states'_superset:
  "{l0} ∪ Normalized_Zone_Semantics_Impl_Refine.state_set trans_prod ⊆ states'"
  (is "{l0} ∪ ?S ⊆ states'")
proof -
  have "?S ⊆ states'"
  proof safe
    fix L s
    assume "(L, s) ∈ ?S"
    then have "L ∈ states"
      using state_set_states[unfolded trans_of_prod state_set_eq] by blast
    moreover have "bounded bounds s"
      using ‹(L, s) ∈ _›
      unfolding state_set_def
      unfolding trans_prod_def
      unfolding trans_int_def trans_bin_def trans_broad_def
      by auto
    ultimately show "(L, s) ∈ states'"
      by (auto simp: states'_alt_def)
  qed
  then show ?thesis
    by simp
qed



definition "k_i ≡ IArray (map (IArray o (map (IArray o map int))) k)"

definition
  "k_impl ≡ λ(l, _). IArray (map (λ c. Max {k_i !! i !! (l ! i) !! c | i. i < n_ps}) [0..<m+1])"

(* Duplication with UPPAAL_State_Networks_Impl_Refine *)
lemma Max_int_commute:
  "int (Max S) = Max (int ` S)" if "finite S" "S ≠ {}"
  apply (rule mono_Max_commute)
    apply rule
  using that by auto

lemma (in Simple_Network_Impl_nat) n_ps_gt_0: "n_ps > 0"
  using length_automata_eq_n_ps non_empty by auto

lemma statesD:
  "L ! i ∈ fst ` set (fst (snd (snd (automata ! i))))
 ∨ L ! i ∈ (snd o snd o snd o snd o snd o snd) ` set (fst (snd (snd (automata ! i))))"
  if "L ∈ states" "length L = n_ps" "i < n_ps"
  using that unfolding states_def
  apply safe
  apply -
  apply (elim allE impE, assumption)
  apply safe
   apply (force simp: mem_trans_N_iff)+
  done

lemma k_impl_k_fun:
  "k_impl (L, s) = IArray (map (k_fun (L, s)) [0..<m+1])" if "L ∈ states"
proof -
  define k_i2 where "k_i2 i c = k_i !! i !! (L ! i) !! c" for i c
  have k_i2_k: "k_i2 i c = k ! i ! (L ! i) ! c" if "i < n_ps" "c ≤ m" for i c
  proof -
    have "i < length k"
      by (simp add: k_length(1) that(1))
    moreover have "L ! i < length (k ! i)"
      using L_i_len[OF _ ‹L ∈ states›] k_length(2) ‹i < n_ps› by auto
    moreover have "c < length (k ! i ! (L ! i))"
      using k_length(3) ‹c ≤ m› ‹i < length k› ‹L ! i < length (k ! i)› by (auto dest: nth_mem)
    ultimately show ?thesis
      unfolding k_i2_def k_i_def by simp
  qed
  have k_impl_alt_def: "k_impl (L, s) = IArray (map (λ c. Max {k_i2 i c | i. i < n_ps}) [0..<m+1])"
    unfolding k_impl_def k_i2_def by auto
  have Max_cong: "Max {f i | i. i < n_ps} = Max {g i | i. i < n_ps}"
    if "⋀ i. i < n_ps ⟹ f i = g i" for f g :: "nat ⇒ int"
    by (rule arg_cong[where f = Max]) (force simp: that)
  from that n_ps_gt_0 show ?thesis
    unfolding k_impl_alt_def
    unfolding k_i2_def[symmetric]
    apply (clarsimp simp: k_fun_def k_i2_k cong: Max_cong)
    apply safe
    subgoal
      by (subst Max_int_commute; force simp: setcompr_eq_image image_comp comp_def)
    subgoal
      using k_0 L_i_len[OF _ ‹L ∈ states›] by (intro linorder_class.Max_eqI) auto
    subgoal
      by (subst Max_int_commute; force simp: setcompr_eq_image image_comp comp_def)
    done
qed


sublocale impl: Reachability_Problem_Impl
  where trans_fun = trans_from
  and inv_fun = inv_fun
  and F_fun = Fi
  and ceiling = k_impl
  and A = prod_ta
  and l0 = l0
  and l0i = l0i
  and F = "PR_CONST F"
  and n = m
  and k = k_fun
  and trans_impl = trans_impl
  and states' = states'
  and loc_rel = loc_rel
  apply standard

(* trans_from *)
  subgoal
    unfolding trans_of_prod by (rule trans_from_correct)

(* trans_impl *)
  subgoal
    apply (rule trans_from_refine)
    done

(* inv_fun *)
  subgoal
    unfolding trans_of_prod
    by (rule set_mp[OF _ inv_fun_inv_of'[where R = loc_rel and S = "{(s, s'). state_rel s' s}"]])
       (auto simp: loc_rel_def)

(* state set *)
  subgoal
    using states'_superset by simp

(* loc_rel l0 l0i*)
  subgoal
    using state_rel_start unfolding loc_rel_def by auto

(* loc_rel left unique *)
  subgoal for l li li'
    unfolding trans_of_prod by (rule state_rel_left_unique)

(* loc_rel right unique *)
  subgoal for l l' li
    unfolding trans_of_prod by (rule state_rel_right_unique)

(* ceiling *)
  subgoal
    unfolding inv_rel_def using L0_states
    by (auto simp: loc_rel_def state_rel_def reach.k'_def k_fun_def k_impl_k_fun)

(* F_fun *)
  subgoal
    unfolding inv_rel_def by (clarsimp dest!: F_Fi)

  done  ― ‹slow: 50s›

end (* Simple_Network_Impl_nat_ceiling_start_state *)

no_notation UPPAAL_Model_Checking.models ("_,_ ⊨⇩_ _" [61,61] 61)


context Reachability_Problem_Impl
begin

lemma F_reachable_correct:
  "op.F_reachable
  ⟷ (∃l'. ∀u0. (∀c ∈ {1..n}. u0 c = 0) ⟶ (∃ u'. conv_A A ⊢' ⟨l0, u0⟩ →* ⟨l', u'⟩ ∧ F l'))"
  using E_op''.E_from_op_reachability_check[symmetric] reachability_check_new
  unfolding E_op_F_reachable E_op''.F_reachable_def E_op''.reachable_def
  unfolding F_rel_def by auto

lemma E_op''_F_reachable_correct:
  "E_op''.F_reachable
  ⟷ (∃l'. ∀u0. (∀c ∈ {1..n}. u0 c = 0) ⟶ (∃ u'. conv_A A ⊢' ⟨l0, u0⟩ →* ⟨l', u'⟩ ∧ F l'))"
  using E_op''.E_from_op_reachability_check[symmetric] reachability_check_new
  unfolding E_op_F_reachable E_op''.F_reachable_def E_op''.reachable_def
  unfolding F_rel_def by auto

lemma Ex_ev_impl_hnr:
  assumes "∀u0. (∀c ∈ {1..n}. u0 c = 0) ⟶ ¬ deadlock (l0, u0)"
  shows
    "
  (uncurry0
    (pw_impl (return ∘ fst) state_copy_impl tracei subsumes_impl a0_impl F_impl succs_impl
      emptiness_check_impl),
   uncurry0 (SPEC (λr. (r ⟷ (∀u0. (∀c ∈ {1..n}. u0 c = 0) ⟶ Ex_ev (λ(l, _). F l) (l0, u0))))))
  ∈ unit_assnk →a bool_assn"
proof -
  interpret Bisimulation_Invariant
    "(λ(l, u) (l', u'). conv_A A ⊢' ⟨l, u⟩ → ⟨l', u'⟩)"
    "(λ(l, u) (l', u'). conv_A A ⊢' ⟨l, u⟩ → ⟨l', u'⟩)"
    "(λ(l, u) (l', u'). l' = l ∧ (∀ c. c ∈ clk_set (conv_A A) ⟶ u c = u' c))"
    "(λ_. True)" "(λ_. True)"
    apply (rule ta_bisimulation)
    done
  define spec where "spec = (∀u0. (∀c ∈ {1..n}. u0 c = 0) ⟶ Ex_ev (λ(l, _). F l) (l0, u0))"
  have *: "E_op''.F_reachable ⟷ spec"
    unfolding spec_def
    unfolding E_op''_F_reachable_correct
  proof safe
    fix l' :: ‹'s› and u0 :: ‹nat ⇒ real›
    assume
      ‹∀u0. (∀c∈{1..n}. u0 c = 0) ⟶ (∃u'. conv_A A ⊢' ⟨l0, u0⟩ →* ⟨l', u'⟩ ∧ F l')› and
      ‹∀c∈{1..n}. u0 c = 0›
    then show ‹Ex_ev (λ(l, _). F l) (l0, u0)›
      using assms by (subst Ex_ev; unfold reaches_steps'[symmetric]) blast+
  next
    assume ‹∀u0. (∀c∈{1..n}. u0 c = 0) ⟶ Ex_ev (λ(l, _). F l) (l0, u0)›
    then have "Ex_ev (λ(l, _). F l) (l0, λ_. 0)"
      by auto
    then obtain l' u' where "conv_A A ⊢' ⟨l0, (λ_. 0)⟩ →* ⟨l', u'⟩ ∧ F l'"
      apply (subst (asm) Ex_ev)
      using assms
      unfolding reaches_steps'[symmetric]
      by auto
    then show ‹∃l'. ∀u0. (∀c∈{1..n}. u0 c = 0) ⟶ (∃u'. conv_A A ⊢' ⟨l0, u0⟩ →* ⟨l', u'⟩ ∧ F l')›
    proof (inst_existentials l', safe, unfold reaches_steps'[symmetric])
      fix u0 :: ‹nat ⇒ real›
      assume ‹reaches (l0, λ_. 0) (l', u')› and ‹F l'› and ‹∀c∈{1..n}. u0 c = 0›
      then have "equiv' (l0, λ_. 0) (l0, u0)"
        unfolding equiv'_def using clocks_I[of "λ_. 0" u0] by auto
      with ‹reaches _ _› ‹F l'› show ‹∃u'. reaches (l0, u0) (l', u') ∧ F l'›
        by - (drule (1) bisim.A_B.simulation_reaches, unfold equiv'_def, auto)
    qed
  qed
  show ?thesis
    unfolding spec_def[symmetric] using pw_impl_hnr_F_reachable[to_hnr, unfolded hn_refine_def]
    by sepref_to_hoare (sep_auto simp: *)
qed

end (* Reachability Problem Impl *)


context Simple_Network_Impl_nat_urge
begin

sublocale conv: Prod_TA_urge
  "(set broadcast, map (Simple_Network_Language.conv_A o automaton_of) automata, map_of bounds')"
  by standard
     (use no_urgency in ‹auto simp: Simple_Network_Language.conv_A_def automaton_of_def urgent_def›)

abbreviation "A ≡ (set broadcast, map automaton_of automata, map_of bounds')"

interpretation conv_eq_bisim:
  Bisimulation_Invariant
  "(λ(l, u) (l', u'). conv_A prod_ta ⊢' ⟨l, u⟩ → ⟨l', u'⟩)"
  "(λ(L, s, u) (L', s', u'). conv.prod_ta   ⊢' ⟨(L, s), u⟩ → ⟨(L', s'), u'⟩)"
  "(λ((L, s), u) (L', s', u'). L = L' ∧ u = u' ∧ s = s')"
  "(λ((L, s), u). conv.all_prop L s)"
  "(λ(L, s, u). conv.all_prop L s)"
proof goal_cases
  case 1
  interpret Bisimulation_Invariant
  "(λ(L, s, u) (L', s', u'). conv_A prod_ta ⊢' ⟨(L, s), u⟩ → ⟨(L', s'), u'⟩)"
  "(λ(L, s, u) (L', s', u'). conv.prod_ta   ⊢' ⟨(L, s), u⟩ → ⟨(L', s'), u'⟩)"
  "(=)"
  "(λ(L, s, u). conv.all_prop L s)"
  "(λ(L, s, u). conv.all_prop L s)"
  by (rule Bisimulation_Invariant_strong_intro)
     (auto simp: conv_prod_ta elim: conv.prod_all_prop_inv')
  show ?case
    by standard (auto simp: conv_prod_ta elim: conv.prod_all_prop_inv')
qed

interpretation Bisimulation_Invariant
  "(λ(l, u) (l', u'). conv_A prod_ta ⊢' ⟨l, u⟩ → ⟨l', u'⟩)"
  "(λ(L, s, u) (L', s', u'). Simple_Network_Language.conv A ⊢ ⟨L, s, u⟩ → ⟨L', s', u'⟩)"
  "(λ((L, s), u) (L', s', u'). L = L' ∧ u = u' ∧ s = s')"
  "(λ((L, s), u). conv.all_prop L s)"
  "(λ(L, s, u). conv.all_prop L s)"
  unfolding conv_alt_def
  apply (rule Bisimulation_Invariant_sim_replace, rule Bisimulation_Invariant_composition)
    apply (rule conv_eq_bisim.Bisimulation_Invariant_axioms conv.prod_bisim_intro)+
  apply auto
  done

lemmas prod_bisim = Bisimulation_Invariant_axioms

lemmas deadlock_iff = deadlock_iff

lemma conv_all_prop:
  "conv.all_prop = all_prop"
  unfolding conv.all_prop_def all_prop_def by simp

definition prop_of2 where
  "prop_of2 φ = PropC (λ((L, s), _). check_sexp φ L (the o s))"

fun ctl_of2 where
  "ctl_of2 (formula.EX φ) = ctl_formula.EX (prop_of2 φ)"
| "ctl_of2 (formula.EG φ) = ctl_formula.EG (prop_of2 φ)"
| "ctl_of2 (formula.AX φ) = ctl_formula.AX (prop_of2 φ)"
| "ctl_of2 (formula.AG φ) = ctl_formula.AG (prop_of2 φ)"
| "ctl_of2 (formula.Leadsto φ ψ) =
  ctl_formula.AG (ctl_formula.ImpliesC (prop_of2 φ) (ctl_formula.AX (prop_of2 ψ)))"

lemma models_correct:
  "Simple_Network_Language.conv A,(L0, s0, u0) ⊨ Φ = (case Φ of
    formula.EX φ ⇒
      Graph_Defs.Ex_ev
        (λ (l, u) (l', u'). conv_A prod_ta ⊢' ⟨l, u⟩ → ⟨l', u'⟩)
        (λ ((L, s), _). check_sexp φ L (the o s))
  | formula.EG φ ⇒
      Not o Graph_Defs.Alw_ev
        (λ (l, u) (l', u'). conv_A prod_ta ⊢' ⟨l, u⟩ → ⟨l', u'⟩)
        (λ ((L, s), _). ¬ check_sexp φ L (the o s))
  | formula.AX φ ⇒
      Graph_Defs.Alw_ev
        (λ (l, u) (l', u'). conv_A prod_ta ⊢' ⟨l, u⟩ → ⟨l', u'⟩)
        (λ ((L, s), _). check_sexp φ L (the o s))
  | formula.AG φ ⇒
      Not o Graph_Defs.Ex_ev
        (λ (l, u) (l', u'). conv_A prod_ta ⊢' ⟨l, u⟩ → ⟨l', u'⟩)
        (λ ((L, s), _). ¬ check_sexp φ L (the o s))
  | formula.Leadsto φ ψ ⇒
      Graph_Defs.leadsto
        (λ (l, u) (l', u'). conv_A prod_ta ⊢' ⟨l, u⟩ → ⟨l', u'⟩)
        (λ ((L, s), _). check_sexp φ L (the o s))
        (λ ((L, s), _). check_sexp ψ L (the o s))
  ) ((L0, s0), u0)
  " if "L0 ∈ states" "Simple_Network_Language.bounded bounds s0"
proof -
  have *: "((Not ∘∘ case_prod) (λ(L, s) _. check_sexp φ L (the o s)))
    = (λ((L, s), _). ¬ check_sexp φ L (the o s))"
    for φ by (auto simp: comp_def)
  have "rel_ctl_formula compatible (ctl_of2 Φ) (ctl_of Φ)"
    by (cases Φ; simp add: prop_of_def prop_of2_def rel_fun_def A_B.equiv'_def)
  moreover have "A_B.equiv' ((L0, s0), u0) (L0, s0, u0)"
    unfolding A_B.equiv'_def unfolding conv_all_prop all_prop_def using that by simp
  ultimately show ?thesis
    apply (subst models_ctl_iff)
    apply (subst CTL_compatible[THEN rel_funD, symmetric])
      apply assumption+
    apply (cases Φ; simp add:
        Graph_Defs.models_ctl.simps prop_of2_def
        Graph_Defs.Ex_alw_iff Graph_Defs.Alw_alw_iff Graph_Defs.leadsto_def *)
    done
qed

end (* Simple_Network_Impl_nat *)

context Simple_Network_Impl_nat_ceiling_start_state ― ‹slow: 70s›
begin

definition Alw_ev_checker where
  "Alw_ev_checker = dfs_map_impl'
     (impl.succs_P_impl' Fi) impl.a0_impl impl.subsumes_impl (return ∘ fst)
     impl.state_copy_impl"

definition leadsto_checker where
  "leadsto_checker ψ = do {
      r ← leadsto_impl
      impl.state_copy_impl (impl.succs_P_impl' (λ (L, s). ¬ check_sexpi ψ L s))
      impl.a0_impl impl.subsumes_impl (return ∘ fst)
      impl.succs_impl' impl.emptiness_check_impl impl.F_impl
      (impl.Q_impl (λ (L, s). ¬ check_sexpi ψ L s))
      impl.tracei;
      return (¬ r)
    }"

definition
  "reachability_checker ≡
     pw_impl
      (return o fst) impl.state_copy_impl impl.tracei impl.subsumes_impl impl.a0_impl impl.F_impl
      impl.succs_impl impl.emptiness_check_impl"

definition model_checker where
  "model_checker = (
  case formula of
    formula.EX _ ⇒ reachability_checker |
    formula.AG _ ⇒ do {
      r ← reachability_checker;
      return (¬ r)
    } |
    formula.AX _ ⇒ do {
      r ← if PR_CONST F l0
      then Alw_ev_checker
      else return False;
      return (¬ r)
    } |
    formula.EG _ ⇒
      if PR_CONST F l0
      then Alw_ev_checker
      else return False |
    formula.Leadsto _ ψ ⇒ leadsto_checker ψ
  )
  "

abbreviation "u0 ≡ (λ _. 0 :: real)"

lemma all_prop_start:
  "all_prop L0 (map_of s0)"
  using L0_states s0_bounded unfolding all_prop_def ..

lemma deadlock_start_iff:
  "Graph_Defs.deadlock
   (λ(L, s, u) (L', s', u'). Simple_Network_Language.conv A ⊢ ⟨L, s, u⟩ → ⟨L', s', u'⟩) (L0, (map_of s0), u0)
  ⟷ reach.deadlock (l0, u0)"
  using all_prop_start by (subst deadlock_iff[symmetric]) (auto simp: conv_all_prop)

lemma F_Fi':
  "check_sexp ψ L (the o s) ⟷ check_sexpi ψ L' s'"
  if "((L', s'), (L, s)) ∈ loc_rel" "formula = Leadsto φ ψ"
  using vars_of_formula that unfolding loc_rel_def by (auto elim!: check_sexp_check_sexpi)

theorem model_check':
  "(uncurry0 model_checker,
    uncurry0 (
      SPEC (λr.
  ¬ Graph_Defs.deadlock
    (λ(L, s, u) (L', s', u').
      Simple_Network_Language.conv A ⊢ ⟨L, s, u⟩ → ⟨L', s', u'⟩) (L0, (map_of s0), u0)
      ⟶ r = (Simple_Network_Language.conv A,(L0, (map_of s0), u0) ⊨ formula)
      )
    )
   )
  ∈ unit_assnk →a bool_assn"
proof -
  define protect where
    "protect = ((λ(l, u) (l', u'). conv_A prod_ta ⊢' ⟨l, u⟩ → ⟨l', u'⟩))"

  have start: "l0 ∈ Normalized_Zone_Semantics_Impl_Refine.state_set trans_prod"
    if "¬ Graph_Defs.deadlock protect (l0, λ_. 0)"
    using that unfolding protect_def by (rule impl.init_state_in_state_set[simplified])

  interpret ta_bisim: Bisimulation_Invariant
    "(λ(l, u) (l', u'). conv_A prod_ta ⊢' ⟨l, u⟩ → ⟨l', u'⟩)"
    "(λ(l, u) (l', u'). conv_A prod_ta ⊢' ⟨l, u⟩ → ⟨l', u'⟩)"
    "(λ(l, u) (l', u'). l' = l ∧ (∀ c. c ∈ clk_set (conv_A prod_ta) ⟶ u c = u' c))"
    "(λ_. True)" "(λ_. True)"
    by (rule ta_bisimulation[of "conv_A prod_ta"])

  let ?φ1 = "λφ. λ(p, _). case p of (L, s) ⇒ ¬ check_sexp φ L (the ∘ s)"
  let ?φ2 = "λφ. λ(p, _). case p of (L, s) ⇒ check_sexp φ L (the ∘ s)"

  have start_sim:
    "ta_bisim.A_B.equiv' (l0, u) (l0, λ_. 0)" "ta_bisim.A_B.equiv' (l0, λ_. 0) (l0, u)"
    if "∀c∈{Suc 0..m}. u c = 0" for u
    using impl.clocks_I[of u "λ_. 0"] that unfolding ta_bisim.A_B.equiv'_def by auto

  have compatibleI: "φ a = φ b"
    if "ta_bisim.A_B.equiv' a b" "⋀ l u u'. φ (l, u) = φ (l, u')" for a b φ
    using that unfolding ta_bisim.A_B.equiv'_def by auto

  have bisims:
    "(∀u0. (∀c∈{Suc 0..m}. u0 c = 0) ⟶ reach.Ex_ev (?φ1 φ) (l0, u0))
    ⟷ reach.Ex_ev (?φ1 φ) (l0, u0)"
    "(∀u0. (∀c∈{Suc 0..m}. u0 c = 0) ⟶ reach.Ex_ev (?φ2 φ) (l0, u0))
    ⟷ reach.Ex_ev (?φ2 φ) (l0, u0)"
    "(∀u0. (∀c∈{Suc 0..m}. u0 c = 0) ⟶ reach.Alw_ev (?φ1 φ) (l0, u0))
    ⟷ reach.Alw_ev (?φ1 φ) (l0, u0)"
    "(∀u0. (∀c∈{Suc 0..m}. u0 c = 0) ⟶ reach.Alw_ev (?φ2 φ) (l0, u0))
    ⟷ reach.Alw_ev (?φ2 φ) (l0, u0)"
    "(∀u0. (∀c∈{Suc 0..m}. u0 c = 0) ⟶ reach.leadsto (?φ2 φ) (?φ2 ψ) (l0, u0))
    ⟷ reach.leadsto (?φ2 φ) (?φ2 ψ) (l0, u0)"
    for φ ψ
    apply safe
    apply (all ‹(solves auto)?›)
    subgoal for u
      using start_sim
      by (subst (asm) ta_bisim.Ex_ev_iff[of "?φ1 φ" "?φ1 φ"]) (erule compatibleI, auto)
    subgoal for u
      using start_sim
      by (subst (asm) ta_bisim.Ex_ev_iff[of "?φ2 φ" "?φ2 φ"]) (erule compatibleI, auto)
    subgoal for u
      using start_sim
      by (subst (asm) ta_bisim.Alw_ev_iff[of "?φ1 φ" "?φ1 φ"]) (erule compatibleI, auto)
    subgoal for u
      using start_sim
      by (subst (asm) ta_bisim.Alw_ev_iff[of "?φ2 φ" "?φ2 φ"]) (erule compatibleI, auto)
    subgoal for u
      using start_sim
      by (subst (asm) ta_bisim.Leadsto_iff[of "?φ2 φ" "?φ2 φ" "?φ2 ψ" "?φ2 ψ"])
        ((erule compatibleI)?; auto)+
    done

  have deadlock_bisim:
    "(∀u0. (∀c∈{1..m}. u0 c = 0) ⟶ ¬ reach.deadlock (l0, u0))
    ⟷ ¬ Graph_Defs.deadlock protect (l0, λ_. 0)"
    unfolding protect_def
    apply (safe; clarsimp)
    apply (drule start_sim(2))
    apply (subst (asm) ta_bisim.deadlock_iff)
    unfolding ta_bisim.A_B.equiv'_def
    by auto

  have *****:
    "return True = (return False ⤜ return o Not)"
    by auto

  show ?thesis
    unfolding deadlock_start_iff
    using models_correct[OF L0_states s0_bounded]
    unfolding protect_def[symmetric]
    apply (simp split del: if_split)
    apply sepref_to_hoare
    apply sep_auto
    unfolding model_checker_def Alw_ev_checker_def leadsto_checker_def reachability_checker_def
    apply (cases formula; simp)

    subgoal
      apply (cases "Graph_Defs.deadlock protect (l0, λ_. 0)")
      subgoal
        using impl.pw_impl_hnr_F_reachable[to_hnr, unfolded hn_refine_def]
        by (sep_auto elim!: cons_post_rule)
      subgoal
        using impl.Ex_ev_impl_hnr[unfolded deadlock_bisim, to_hnr, unfolded hn_refine_def]
        by (sep_auto simp: pure_def protect_def bisims)
      done

    subgoal premises prems for φ
    proof -
      have *: "(λ(l, u). ¬ F l) = ((λ(p, _). case p of (L, s) ⇒ ¬ check_sexp φ L (the ∘ s)))"
        using prems by auto
      show ?thesis
        using impl.Alw_ev_impl_hnr[to_hnr, unfolded hn_refine_def] prems start
        unfolding PR_CONST_def * protect_def
        by (sep_auto elim!: cons_post_rule simp: pure_def bisims)
    qed

    subgoal premises prems for φ
    proof -
      have *: "(λ(l, u). ¬ F l) = ((λ(p, _). case p of (L, s) ⇒ check_sexp φ L (the ∘ s)))"
        using prems by auto
      show ?thesis
        apply intros
        subgoal
          using impl.Alw_ev_impl_hnr[to_hnr, unfolded hn_refine_def] prems start
          unfolding PR_CONST_def * protect_def
          apply simp
          unfolding *****
          apply (erule bind_rule)
          apply (sep_auto simp: pure_def bisims(2-))
          done
        subgoal
          using impl.Alw_ev_impl_hnr[to_hnr, unfolded hn_refine_def] prems start
          unfolding PR_CONST_def * protect_def
          apply (sep_auto elim!: cons_post_rule simp: pure_def bisims(2-))
          done
        done
    qed

    subgoal
      apply (cases "Graph_Defs.deadlock protect (l0, λ_. 0)")
      subgoal
        using impl.pw_impl_hnr_F_reachable[to_hnr, unfolded hn_refine_def]
        by (sep_auto elim!: cons_post_rule)
      subgoal
        using impl.Ex_ev_impl_hnr[unfolded deadlock_bisim, to_hnr, unfolded hn_refine_def]
        apply (sep_auto simp: pure_def protect_def bisims)
        done
      done

    subgoal premises prems for φ ψ
    proof -
      have *: "(λ(l, u). F l) = ((λ(p, _). case p of (L, s) ⇒ check_sexp φ L (the ∘ s)))"
        using prems by auto
      have **:"(λ(L, s). ¬ check_sexpi ψ L s, λ(L, s). ¬ check_sexp ψ L (the ∘ s))
               ∈ inv_rel loc_rel states'"
        unfolding trans_of_prod using prems by (auto simp: F_Fi' inv_rel_def)
      have ****: "(λ(l, u). ¬ (case l of (L, s) ⇒ ¬ check_sexp ψ L (the ∘ s)))
      = (λ(l, u). (case l of (L, s) ⇒ check_sexp ψ L (the ∘ s)))"
        by auto
      show ?thesis
        apply (cases "reach.deadlock (l0, λ_. 0)")
        subgoal
          using impl.leadsto_impl_hnr'[OF **, to_hnr, unfolded hn_refine_def]
          unfolding protect_def ‹formula = _› by (sep_auto simp: pure_def)
        using impl.leadsto_impl_hnr[unfolded deadlock_bisim, to_hnr, unfolded hn_refine_def, OF **]
          prems start
        unfolding PR_CONST_def * protect_def by (sep_auto simp: pure_def bisims ****)
    qed
    done
qed


subsection ‹Extracting an Efficient Implementation›

lemma reachability_checker_alt_def':
  "reachability_checker ≡
    do {
      x ← do {
        let key = return ∘ fst;
        let sub = impl.subsumes_impl;
        let copy = impl.state_copy_impl;
        let start = impl.a0_impl;
        let final = impl.F_impl;
        let succs =  impl.succs_impl;
        let empty = impl.emptiness_check_impl;
        let trace = impl.tracei;
        pw_impl key copy trace sub start final succs empty
      };
      _ ← return ();
      return x
    }"
  unfolding reachability_checker_def by simp

lemma Alw_ev_checker_alt_def':
  "Alw_ev_checker ≡
    do {
      x ← let
        key = return ∘ fst;
        sub = impl.subsumes_impl;
        copy = impl.state_copy_impl;
        start = impl.a0_impl;
        succs =  impl.succs_P_impl' Fi
      in dfs_map_impl' succs start sub key copy;
      _ ← return ();
      return x
    }"
  unfolding Alw_ev_checker_def by simp

lemma leadsto_checker_alt_def':
  "leadsto_checker ψ ≡
    do {
      r ← let
        key = return ∘ fst;
        sub = impl.subsumes_impl;
        copy = impl.state_copy_impl;
        start = impl.a0_impl;
        final = impl.F_impl;
        final' = (impl.Q_impl (λ(L, s). ¬ check_sexpi ψ L s));
        succs =  impl.succs_P_impl' (λ(L, s). ¬ check_sexpi ψ L s);
        succs' =  impl.succs_impl';
        empty = impl.emptiness_check_impl;
        trace = impl.tracei
      in
        leadsto_impl copy succs start sub key succs' empty final final' trace;
      return (¬ r)
    }"
  unfolding leadsto_checker_def by simp

theorem k_impl_alt_def:
  "k_impl = (λ(l, s). IArray (map (λc. MAX i ∈ {0..<n_ps}. k_i !! i !! (l ! i) !! c) [0..<m + 1]))"
proof -
  have "{i. i < p} = {0..<p}" for p :: nat
    by auto
  then show ?thesis
    unfolding k_impl_def setcompr_eq_image by simp
qed

definition
  "trans_map_inner ≡ map (λi. union_map_of (fst (snd (snd (automata ! i))))) [0..<n_ps]"

lemma trans_map_alt_def:
  "trans_map i j = (case (IArray trans_map_inner !! i) j of None ⇒ [] | Some xs ⇒ xs)"
  if "i < n_ps"
  using that unfolding trans_map_inner_def trans_map_def by (auto simp: n_ps_def)

schematic_goal succs_impl_alt_def:
  "impl.succs_impl ≡ ?impl"
  unfolding impl.succs_impl_def
  apply (abstract_let impl.E_op''_impl E_op''_impl)
  unfolding impl.E_op''_impl_def fw_impl'_int
  apply (abstract_let trans_impl trans_impl)
  unfolding trans_impl_def
  apply (abstract_let int_trans_impl int_trans_impl)
  apply (abstract_let bin_trans_from_impl bin_trans_impl)
  apply (abstract_let broad_trans_from_impl broad_trans_impl)
  unfolding int_trans_impl_def bin_trans_from_impl_def broad_trans_from_impl_def
  apply (abstract_let trans_in_broad_grouped trans_in_broad_grouped)
  apply (abstract_let trans_out_broad_grouped trans_out_broad_grouped)
  apply (abstract_let trans_in_map trans_in_map)
  apply (abstract_let trans_out_map trans_out_map)
  apply (abstract_let int_trans_from_all_impl int_trans_from_all_impl)
  unfolding int_trans_from_all_impl_def
  apply (abstract_let int_trans_from_vec_impl int_trans_from_vec_impl)
  unfolding int_trans_from_vec_impl_def
  apply (abstract_let int_trans_from_loc_impl int_trans_from_loc_impl)
  unfolding int_trans_from_loc_impl_def
  apply (abstract_let trans_i_map trans_i_map)
  unfolding trans_out_broad_grouped_def trans_out_broad_map_def
  unfolding trans_in_broad_grouped_def trans_in_broad_map_def
  unfolding trans_in_map_def trans_out_map_def
  unfolding trans_i_map_def
  apply (abstract_let trans_map trans_map)
  apply (abstract_let "inv_fun :: nat list × int list ⇒ _" inv_fun)
  unfolding inv_fun_alt_def
  apply (abstract_let invs2 invs)
  unfolding invs2_def
  unfolding k_impl_alt_def
  apply (abstract_let k_i k_i) (* Could be killed *)
  apply (abstract_let n_ps n_ps)
  by (rule Pure.reflexive)

schematic_goal succs_P_impl_alt_def:
  "impl.succs_P_impl Pi ≡ ?impl"
  if "(Pi, P) ∈ inv_rel loc_rel states'"
  for P Pi
  unfolding impl.succs_P_impl_def[OF that]
  apply (abstract_let impl.E_op''_impl E_op''_impl)
  unfolding impl.E_op''_impl_def fw_impl'_int
  apply (abstract_let "trans_impl" trans_impl)
  unfolding trans_impl_def
  apply (abstract_let "int_trans_impl" int_trans_impl)
  apply (abstract_let "bin_trans_from_impl" bin_trans_impl)
  apply (abstract_let "broad_trans_from_impl" broad_trans_impl)
  unfolding int_trans_impl_def bin_trans_from_impl_def broad_trans_from_impl_def
  apply (abstract_let trans_in_broad_grouped trans_in_broad_grouped)
  apply (abstract_let trans_out_broad_grouped trans_out_broad_grouped)
  apply (abstract_let trans_in_map trans_in_map)
  apply (abstract_let trans_out_map trans_out_map)
  apply (abstract_let int_trans_from_all_impl int_trans_from_all_impl)
  unfolding int_trans_from_all_impl_def
  apply (abstract_let int_trans_from_vec_impl int_trans_from_vec_impl)
  unfolding int_trans_from_vec_impl_def
  apply (abstract_let int_trans_from_loc_impl int_trans_from_loc_impl)
  unfolding int_trans_from_loc_impl_def
  apply (abstract_let trans_i_map trans_i_map)
  unfolding trans_out_broad_grouped_def trans_out_broad_map_def
  unfolding trans_in_broad_grouped_def trans_in_broad_map_def
  unfolding trans_in_map_def trans_out_map_def
  unfolding trans_i_map_def
  apply (abstract_let trans_map trans_map)
  apply (abstract_let "inv_fun :: nat list × int list ⇒ _" inv_fun)
  unfolding inv_fun_alt_def
  apply (abstract_let invs2 invs)
  unfolding invs2_def
  unfolding k_impl_alt_def
  apply (abstract_let k_i k_i) (* Could be killed *)
  apply (abstract_let n_ps n_ps)
  by (rule Pure.reflexive)


(* These implementations contain unnecessary list reversals *)
lemmas succs_P'_impl_alt_def =
  impl.succs_P_impl'_def[OF impl.F_fun, unfolded succs_P_impl_alt_def[OF impl.F_fun]]

schematic_goal Alw_ev_checker_alt_def:
  "Alw_ev_checker ≡ ?impl"
  unfolding Alw_ev_checker_alt_def'
  unfolding succs_P'_impl_alt_def
  unfolding k_impl_alt_def k_i_def
  (* The following are just to unfold things that should have been defined in a defs locale *)
  unfolding impl.E_op''_impl_def impl.abstr_repair_impl_def impl.abstra_repair_impl_def
  unfolding impl.start_inv_check_impl_def unbounded_dbm_impl_def unbounded_dbm'_def
  unfolding impl.init_dbm_impl_def impl.a0_impl_def
  unfolding impl.F_impl_def
  unfolding impl.subsumes_impl_def
  unfolding impl.emptiness_check_impl_def
  unfolding impl.state_copy_impl_def
  by (rule Pure.reflexive)

lemma ψ_compatibleI:
  "(λ(L, s). ¬ check_sexpi ψ L s, λ(L, s). ¬ check_sexp ψ L (the ∘ s)) ∈ inv_rel loc_rel states'"
  if "formula = Leadsto φ ψ"
  using F_Fi'[OF _ that] unfolding inv_rel_def by auto

lemma Q_impl_alt_def:
  "impl.Q_impl (λ(L, s). ¬ check_sexpi ψ L s) ≡
  λxi. return (case xi of (a1, a2) ⇒ (λ(L, s). ¬ check_sexpi ψ L s) a1)"
  if "formula = Leadsto φ ψ"
  by (intro impl.Q_impl_def[where Q = "λ(L, s). ¬ check_sexp ψ L (the o s)"] ψ_compatibleI[OF that])

schematic_goal leadsto_checker_alt_def:
  "leadsto_checker ψ ≡ ?impl" if "formula = Leadsto φ ψ"
  unfolding leadsto_checker_alt_def'
  unfolding Q_impl_alt_def[OF that] impl.F_impl_def
  unfolding impl.succs_P_impl'_def[OF ψ_compatibleI[OF that]]
  unfolding succs_P_impl_alt_def[OF ψ_compatibleI[OF that]]
  unfolding impl.succs_impl'_def succs_impl_alt_def
  unfolding k_impl_alt_def k_i_def
  (* The following are just to unfold things that should have been defined in a defs locale *)
  unfolding impl.E_op''_impl_def impl.abstr_repair_impl_def impl.abstra_repair_impl_def
  unfolding impl.start_inv_check_impl_def unbounded_dbm_impl_def unbounded_dbm'_def
  unfolding impl.init_dbm_impl_def impl.a0_impl_def
  unfolding impl.F_impl_def
  unfolding impl.subsumes_impl_def
  unfolding impl.emptiness_check_impl_def
  unfolding impl.state_copy_impl_def
  by (rule Pure.reflexive)

schematic_goal reachability_checker_alt_def:
  "reachability_checker ≡ ?impl"
  unfolding reachability_checker_alt_def'
  unfolding succs_impl_alt_def
  unfolding k_impl_alt_def k_i_def
  (* The following are just to unfold things that should have been defined in a defs locale *)
  unfolding impl.E_op''_impl_def impl.abstr_repair_impl_def impl.abstra_repair_impl_def
  unfolding impl.start_inv_check_impl_def unbounded_dbm_impl_def unbounded_dbm'_def
  unfolding impl.init_dbm_impl_def impl.a0_impl_def
  unfolding impl.F_impl_def
  unfolding impl.subsumes_impl_def
  unfolding impl.emptiness_check_impl_def
  unfolding impl.state_copy_impl_def
  by (rule Pure.reflexive)

end (* Simple_Network_Impl_nat_ceiling_start_state *)

concrete_definition reachability_checker
  uses Simple_Network_Impl_nat_ceiling_start_state.reachability_checker_alt_def

concrete_definition Alw_ev_checker
  uses Simple_Network_Impl_nat_ceiling_start_state.Alw_ev_checker_alt_def

concrete_definition leadsto_checker
  uses Simple_Network_Impl_nat_ceiling_start_state.leadsto_checker_alt_def

context Simple_Network_Impl_nat_ceiling_start_state ― ‹slow: 100s›
begin

lemma model_checker_unfold_leadsto:
  "model_checker = (
  case formula of Simple_Network_Language_Model_Checking.formula.EX xa ⇒ reachability_checker
    | Simple_Network_Language_Model_Checking.formula.EG xa ⇒
      if PR_CONST F l0 then Alw_ev_checker else return False
    | Simple_Network_Language_Model_Checking.formula.AX xa ⇒
      (if PR_CONST F l0 then Alw_ev_checker else return False) ⤜ (λr. return (¬ r))
    | Simple_Network_Language_Model_Checking.formula.AG xa ⇒
      reachability_checker ⤜ (λr. return (¬ r))
    | Simple_Network_Language_Model_Checking.formula.Leadsto φ ψ ⇒
      Simple_Network_Language_Model_Checking.leadsto_checker
        broadcast bounds' automata m num_states num_actions k L0 s0 formula ψ show_clock show_state)
"
  unfolding model_checker_def
  using leadsto_checker.refine[OF Simple_Network_Impl_nat_ceiling_start_state_axioms]
  by (simp split: formula.split)

lemmas model_checker_def_refined = model_checker_unfold_leadsto[unfolded
    reachability_checker.refine[OF Simple_Network_Impl_nat_ceiling_start_state_axioms]
    Alw_ev_checker.refine[OF Simple_Network_Impl_nat_ceiling_start_state_axioms]
  ]

end (* Simple_Network_Impl_nat_ceiling_start_state *)

concrete_definition model_checker uses
  Simple_Network_Impl_nat_ceiling_start_state.model_checker_def_refined

definition precond_mc where
  "precond_mc
    show_clock show_state broadcast bounds' automata m num_states num_actions k L0 s0 formula ≡
    if Simple_Network_Impl_nat_ceiling_start_state
      broadcast bounds' automata m num_states num_actions k L0 s0 formula
    then
      model_checker
        broadcast bounds' automata m num_states num_actions k L0 s0 formula show_clock show_state
      ⤜ (λ x. return (Some x))
    else return None"


abbreviation N where
  "N broadcast automata bounds ≡
  Simple_Network_Language.conv
    (set broadcast, map automaton_of automata, map_of bounds)"

definition has_deadlock where
  "has_deadlock A a0 ≡
    Graph_Defs.deadlock (λ (L, s, u) (L', s', u'). A ⊢ ⟨L, s, u⟩ → ⟨L', s', u'⟩) a0"

theorem model_check:
  "<emp> precond_mc
    show_clock show_state broadcast bounds automata m num_states num_actions k L0 s0 formula
    <λ Some r ⇒ ↑(
        Simple_Network_Impl_nat_ceiling_start_state
          broadcast bounds automata m num_states num_actions k L0 s0 formula ∧
        (¬ has_deadlock (N broadcast automata bounds) (L0, map_of s0, λ_ . 0) ⟶
          r = N broadcast automata bounds,(L0, map_of s0, λ_ . 0) ⊨ formula
        ))
     | None ⇒ ↑(¬ Simple_Network_Impl_nat_ceiling_start_state
        broadcast bounds automata m num_states num_actions k L0 s0 formula)
    >t"
proof -
  define A where "A ≡ N broadcast automata bounds"
  define check where "check ≡ A,(L0, map_of s0, λ_ . 0) ⊨ formula"
  note [sep_heap_rules] =
    Simple_Network_Impl_nat_ceiling_start_state.model_check'[
      to_hnr, unfolded hn_refine_def,
      of broadcast bounds automata m num_states num_actions k L0 s0 formula,
      unfolded UPPAAL_Reachability_Problem_precompiled_defs.init_def,
      folded A_def check_def has_deadlock_def,
      simplified
      ]
  show ?thesis
    unfolding A_def[symmetric] check_def[symmetric]
    unfolding precond_mc_def
    by (sep_auto simp: model_checker.refine[symmetric] pure_def)
qed

end (* Theory *)