theory Window imports"HOL-Library.AList""HOL-Library.Mapping""HOL-Library.While_Combinator" Timestamp begin
type_synonym ('a, 'b) mmap = "('a × 'b) list"
(* 'b is a polymorphic input symbol; 'c is a polymorphic DFA state;
'd is a timestamp; 'e is a submonitor state *)
inductive chain_le :: "'d :: timestamp list ==> bool"where
chain_le_Nil: "chain_le []"
| chain_le_singleton: "chain_le [x]"
| chain_le_cons: "chain_le (y # xs) ==> x ≤ y ==> chain_le (x # y # xs)"
lemma chain_le_app: "chain_le (zs @ [z]) ==> z ≤ w ==> chain_le ((zs @ [z]) @ [w])" apply (induction"zs @ [z]" arbitrary: zs rule: chain_le.induct) apply (auto intro: chain_le.intros)[2]
subgoal for y xs x zs apply (cases zs) apply (auto) apply (metis append.assoc append_Cons append_Nil chain_le_cons) done done
inductive reaches_on :: "('e ==> ('e × 'f) option) ==> 'e ==> 'f list ==> 'e ==> bool" for run :: "'e ==> ('e × 'f) option"where "reaches_on run s [] s"
| "run s = Some (s', v) ==> reaches_on run s' vs s'' ==> reaches_on run s (v # vs) s''"
lemma reaches_on_init_Some: "reaches_on r s xs s' ==> r s' ≠ None ==> r s ≠ None" by (auto elim: reaches_on.cases)
lemma reaches_on_split: "reaches_on run s vs s' ==> i < length vs ==> ∃s'' s'''. reaches_on run s (take i vs) s'' ∧ run s'' = Some (s''', vs ! i) ∧ reaches_on run s''' (drop (Suc i) vs) s'" proof (induction s vs s' arbitrary: i rule: reaches_on.induct) case (2 s s' v vs s'') show ?case using2(1,2) proof (cases i) case (Suc n) show ?thesis using2 by (fastforce simp: Suc intro: reaches_on.intros) qed (auto intro: reaches_on.intros) qed auto
lemma reaches_on_split': "reaches_on run s vs s' ==> i ≤ length vs ==> ∃s'' . reaches_on run s (take i vs) s'' ∧ reaches_on run s'' (drop i vs) s'" proof (induction s vs s' arbitrary: i rule: reaches_on.induct) case (2 s s' v vs s'') show ?case using2(1,2) proof (cases i) case (Suc n) show ?thesis using2 by (fastforce simp: Suc intro: reaches_on.intros) qed (auto intro: reaches_on.intros) qed (auto intro: reaches_on.intros)
lemma reaches_on_split_app: "reaches_on run s (vs @ vs') s' ==> ∃s''. reaches_on run s vs s'' ∧ reaches_on run s'' vs' s'" using reaches_on_split'[where i="length vs", of run s "vs @ vs'" s'] by auto
lemma reaches_on_inj: "reaches_on run s vs t ==> reaches_on run s vs' t' ==> length vs = length vs' ==> vs = vs' ∧ t = t'" apply (induction s vs t arbitrary: vs' t' rule: reaches_on.induct) apply (auto elim: reaches_on.cases)[1]
subgoal for s s' v vs s'' vs' t' apply (rule reaches_on.cases[of run s' vs s'']; rule reaches_on.cases[of run s vs' t']) apply assumption+ apply auto[2] apply fastforce apply (metis length_0_conv list.discI) apply (metis Pair_inject length_Cons nat.inject option.inject) done done
lemma reaches_on_split_last: "reaches_on run s (xs @ [x]) s'' ==> ∃s'. reaches_on run s xs s' ∧ run s' = Some (s'', x)" apply (induction s "xs @ [x]" s'' arbitrary: xs x rule: reaches_on.induct) apply simp
subgoal for s s' v vs s'' xs x by (cases vs rule: rev_cases) (fastforce elim: reaches_on.cases intro: reaches_on.intros)+ done
lemma reaches_on_rev_induct[consumes 1]: "reaches_on run s vs s' ==> (∧s. P s [] s) ==> (∧s s' v vs s''. reaches_on run s vs s' ==> P s vs s' ==> run s' = Some (s'', v)==> P s (vs @ [v]) s'') ==> P s vs s'" proof (induction vs arbitrary: s s' rule: rev_induct) case (snoc x xs) from snoc(2) obtain s'' where s''_def: "reaches_on run s xs s''""run s'' = Some (s', x)" using reaches_on_split_last by fast show ?case using snoc(4)[OF s''_def(1) _ s''_def(2)] snoc(1)[OF s''_def(1) snoc(3,4)] by auto qed (auto elim: reaches_on.cases)
lemma reaches_on_app: "reaches_on run s vs s' ==> run s' = Some (s'', v) ==> reaches_on run s (vs @ [v]) s''" by (induction s vs s' rule: reaches_on.induct) (auto intro: reaches_on.intros)
lemma reaches_on_trans: "reaches_on run s vs s' ==> reaches_on run s' vs' s'' ==> reaches_on run s (vs @ vs') s''" by (induction s vs s' rule: reaches_on.induct) (auto intro: reaches_on.intros)
lemma reaches_onD: "reaches_on run s ((t, b) # vs) s' ==> ∃s''. run s = Some (s'', (t, b)) ∧ reaches_on run s'' vs s'" by (auto elim: reaches_on.cases)
lemma reaches_on_setD: "reaches_on run s vs s' ==> x ∈ set vs ==> ∃vs' vs'' s''. reaches_on run s (vs' @ [x]) s'' ∧ reaches_on run s'' vs'' s' ∧ vs = vs' @ x # vs''" proof (induction s vs s' rule: reaches_on_rev_induct) case (2 s s' v vs s'') show ?case proof (cases "x ∈ set vs") case True obtain vs' vs'' s''' where split_def: "reaches_on run s (vs' @ [x]) s'''" "reaches_on run s''' vs'' s'""vs = vs' @ x # vs''" using2(3)[OF True] by auto show ?thesis using split_def(1,3) reaches_on_app[OF split_def(2) 2(2)] by auto next case False have x_v: "x = v" using2(4) False by auto show ?thesis unfolding x_v using reaches_on_app[OF 2(1,2)] reaches_on.intros(1)[of run s''] by auto qed qed auto
lemma reaches_on_len: "∃vs s'. reaches_on run s vs s' ∧ (length vs = n ∨ run s' = None)" proof (induction n arbitrary: s) case (Suc n) show ?case proof (cases "run s") case (Some x) obtain s' v where x_def: "x = (s', v)" by (cases x) auto obtain vs s'' where s''_def: "reaches_on run s' vs s''""length vs = n ∨ run s'' = None" using Suc[of s'] by auto show ?thesis using reaches_on.intros(2)[OF Some[unfolded x_def] s''_def(1)] s''_def(2) by fastforce qed (auto intro: reaches_on.intros) qed (auto intro: reaches_on.intros)
lemma reaches_on_NilD: "reaches_on run q [] q' ==> q = q'" by (auto elim: reaches_on.cases)
lemma reaches_on_ConsD: "reaches_on run q (x # xs) q' ==>∃q''. run q = Some (q'', x) ∧ reaches_on run q'' xs q'" by (auto elim: reaches_on.cases)
inductive reaches :: "('e ==> ('e × 'f) option) ==> 'e ==> nat ==> 'e ==> bool" for run :: "'e ==> ('e × 'f) option"where "reaches run s 0 s"
| "run s = Some (s', v) ==> reaches run s' n s'' ==> reaches run s (Suc n) s''"
lemma reaches_Suc_split_last: "reaches run s (Suc n) s' ==>∃s'' x. reaches run s n s'' ∧ run s'' = Some (s', x)" proof (induction n arbitrary: s) case (Suc n) obtain s'' x where s''_def: "run s = Some (s'', x)""reaches run s'' (Suc n) s'" using Suc(2) by (auto elim: reaches.cases) show ?case using s''_def(1) Suc(1)[OF s''_def(2)] by (auto intro: reaches.intros) qed (auto elim!: reaches.cases intro: reaches.intros)
lemma reaches_invar: "reaches f x n y ==> P x ==> (∧z z' v. P z ==> f z = Some (z', v) ==> P z') ==> P y" by (induction x n y rule: reaches.induct) auto
lemma reaches_cong: "reaches f x n y ==> P x ==> (∧z z' v. P z ==> f z = Some (z', v) ==> P z') ==> (∧z. P z ==> f' (g z) = map_option (apfst g) (f z)) ==> reaches f' (g x) n (g y)" by (induction x n y rule: reaches.induct) (auto intro: reaches.intros)
lemma reaches_on_n: "reaches_on run s vs s' ==> reaches run s (length vs) s'" by (induction s vs s' rule: reaches_on.induct) (auto intro: reaches.intros)
lemma reaches_on: "reaches run s n s' ==>∃vs. reaches_on run s vs s' ∧ length vs = n" by (induction s n s' rule: reaches.induct) (auto intro: reaches_on.intros)
definition ts_at :: "('d × 'b) list ==> nat ==> 'd"where "ts_at rho i = fst (rho ! i)"
definition bs_at :: "('d × 'b) list ==> nat ==> 'b"where "bs_at rho i = snd (rho ! i)"
definition sup_acc :: "('c ==> 'b ==> 'c) ==> ('c ==> bool) ==> ('d × 'b) list ==> 'c ==> nat ==> nat ==> ('d × nat) option"where "sup_acc step accept rho q i j = (let L' = {l ∈ {i..<j}. acc step accept rho q (i, Suc l)}; m = Max L' in if L' = {} then None else Some (ts_at rho m, m))"
definition sup_leadsto :: "'c ==> ('c ==> 'b ==> 'c) ==> ('d × 'b) list ==> nat ==> nat ==> 'c ==> 'd option"where "sup_leadsto init step rho i j q = (let L' = {l. l < i ∧ steps step rho init (l, j) = q}; m = Max L' in if L' = {} then None else Some (ts_at rho m))"
definition mmap_keys :: "('a, 'b) mmap ==> 'a set"where "mmap_keys kvs = set (map fst kvs)"
lemma sup_acc_ext_idle: "i ≤ j ==>¬acc step accept rho q (i, Suc j) ==> sup_acc step accept rho q i (Suc j) = sup_acc step accept rho q i j" proof - assume assms: "i ≤ j""¬acc step accept rho q (i, Suc j)"
define L where"L = {l ∈ {i..<j}. acc step accept rho q (i, Suc l)}"
define L' where"L' = {l ∈ {i..<Suc j}. acc step accept rho q (i, Suc l)}" have L_L': "L = L'" unfolding L_def L'_defusing assms(2) less_antisym by fastforce show"sup_acc step accept rho q i (Suc j) = sup_acc step accept rho q i j" using L_def L'_def L_L' by (auto simp add: sup_acc_def) qed
lemma sup_acc_comp_Some_ge: "i ≤ l ==> l ≤ j ==> tp ≥ l ==> sup_acc step accept rho (steps step rho q (i, l)) l j = Some (ts, tp) ==> sup_acc step accept rho q i j = sup_acc step accept rho (steps step rho q (i, l)) l j" proof - assume assms: "i ≤ l""l ≤ j""sup_acc step accept rho (steps step rho q (i, l)) l j = Some (ts, tp)""tp ≥ l"
define L where"L = {l ∈ {i..<j}. acc step accept rho q (i, Suc l)}"
define L' where"L' = {l' ∈ {l..<j}. acc step accept rho (steps step rho q (i, l)) (l, Suc l')}" have L'_props: "finite L'""L' ≠ {}""tp = Max L'""ts = ts_at rho tp" using assms(3) unfolding L'_def by (auto simp add: sup_acc_def Let_def split: if_splits) have tp_in_L': "tp ∈ L'" using Max_in[OF L'_props(1,2)] unfolding L'_props(3) . thenhave tp_in_L: "tp ∈ L" unfolding L_def L'_defusing assms(1) steps_comp[OF assms(1,2), of step rho] apply (auto simp add: acc_def) using steps_comp by (metis le_SucI) have L_props: "finite L""L ≠ {}" using L_def tp_in_L by auto have"∧l'. l' ∈ L ==> l' ≤ tp" proof - fix l' assume assm: "l' ∈ L" show"l' ≤ tp" proof (cases "l' < l") case True thenshow ?thesis using assms(4) by auto next case False thenhave"l' ∈ L'" using assm unfolding L_def L'_def by (auto simp add: acc_def) (metis assms(1) less_imp_le_nat not_less_eq steps_comp) thenshow ?thesis using Max_eq_iff[OF L'_props(1,2)] L'_props(3) by auto qed qed thenhave"Max L = tp" using Max_eq_iff[OF L_props] tp_in_L by auto thenhave"sup_acc step accept rho q i j = Some (ts, tp)" using L_def L_props(2) unfolding L'_props(4) by (auto simp add: sup_acc_def) thenshow"sup_acc step accept rho q i j = sup_acc step accept rho (steps step rho q (i, l)) l j" using assms(3) by auto qed
lemma sup_acc_comp_None: "i ≤ l ==> l ≤ j ==> sup_acc step accept rho (steps step rho q (i, l)) l j = None ==> sup_acc step accept rho q i j = sup_acc step accept rho q i l" proof (induction"j - l" arbitrary: l) case (Suc n) have i_lt_j: "i < j" using Suc by auto have l_lt_j: "l < j" using Suc by auto have"¬acc step accept rho q (i, Suc l)" using sup_acc_NoneE[of l l j step accept rho "steps step rho q (i, l)"] Suc(2-) by (auto simp add: acc_def steps_def) thenhave"sup_acc step accept rho q i (l + 1) = sup_acc step accept rho q i l" using sup_acc_ext_idle[OF Suc(3)] by auto moreoverhave"sup_acc step accept rho (steps step rho q (i, l + 1)) (l + 1) j = None" using sup_acc_None_restrict[OF Suc(4,5)] steps_app[OF Suc(3), of step rho] by auto ultimatelyshow ?case using Suc(1)[of "l + 1"] Suc(2,3,4,5) by auto qed (auto simp add: sup_acc_same)
lemma sup_acc_ext: "i ≤ j ==> acc step accept rho q (i, Suc j) ==> sup_acc step accept rho q i (Suc j) = Some (ts_at rho j, j)" proof - assume assms: "i ≤ j""acc step accept rho q (i, Suc j)"
define L' where"L' = {l ∈ {i..<j + 1}. acc step accept rho q (i, Suc l)}" have j_in_L': "finite L'""L' ≠ {}""j ∈ L'" using assms unfolding L'_defby auto have j_is_Max: "Max L' = j" using Max_eq_iff[OF j_in_L'(1,2)] j_in_L'(3) by (auto simp add: L'_def) show"sup_acc step accept rho q i (Suc j) = Some (ts_at rho j, j)" using L'_def j_is_Max j_in_L'(2) by (auto simp add: sup_acc_def) qed
lemma sup_acc_None: "i < j ==> sup_acc step accept rho q i j = None ==> sup_acc step accept rho (step q (bs_at rho i)) (i + 1) j = None" using steps_split[of _ _ step rho] by (auto simp add: sup_acc_def Let_def acc_def split: if_splits)
lemma sup_acc_i: "i < j ==> sup_acc step accept rho q i j = Some (ts, i) ==> sup_acc step accept rho (step q (bs_at rho i)) (Suc i) j = None" proof (rule ccontr) assume assms: "i < j""sup_acc step accept rho q i j = Some (ts, i)" "sup_acc step accept rho (step q (bs_at rho i)) (Suc i) j ≠ None" from assms(3) obtain l where l_def: "l ∈ {Suc i..<j}" "acc step accept rho (step q (bs_at rho i)) (Suc i, Suc l)" by (auto simp add: sup_acc_def Let_def split: if_splits)
define L' where"L' = {l ∈ {i..<j}. acc step accept rho q (i, Suc l)}" from assms(2) have L'_props: "finite L'""L' ≠ {}""Max L' = i" by (auto simp add: sup_acc_def L'_def Let_def split: if_splits) have i_lt_l: "i < l" using l_def(1) by auto from l_def have"l ∈ L'" unfolding L'_def acc_def using steps_split[OF i_lt_l, of step rho] by (auto simp: steps_def) thenshow"False" using l_def(1) L'_props Max_ge i_lt_l not_le by auto qed
lemma sup_acc_l: "i < j ==> i ≠ l ==> sup_acc step accept rho q i j = Some (ts, l) ==> sup_acc step accept rho q i j = sup_acc step accept rho (step q (bs_at rho i)) (Suc i) j" proof - assume assms: "i < j""i ≠ l""sup_acc step accept rho q i j = Some (ts, l)"
define L where"L = {l ∈ {i..<j}. acc step accept rho q (i, Suc l)}"
define L' where"L' = {l ∈ {Suc i..<j}. acc step accept rho (step q (bs_at rho i)) (Suc i, Suc l)}" from assms(3) have L_props: "finite L""L ≠ {}""l = Max L" "sup_acc step accept rho q i j = Some (ts_at rho l, l)" by (auto simp add: sup_acc_def L_def Let_def split: if_splits) have l_in_L: "l ∈ L" using Max_in[OF L_props(1,2)] L_props(3) by auto thenhave i_lt_l: "i < l" unfolding L_def using assms(2) by auto have l_in_L': "finite L'""L' ≠ {}""l ∈ L'" using steps_split[OF i_lt_l, of step rho q] l_in_L assms(2) unfolding L_def L'_def acc_def by (auto simp: steps_def) have"∧l'. l' ∈ L' ==> l' ≤ l" proof - fix l' assume assms: "l' ∈ L'" have i_lt_l': "i < l'" using assms unfolding L'_defby auto have"l' ∈ L" using steps_split[OF i_lt_l', of step rho] assms unfolding L_def L'_def acc_def by (auto simp: steps_def) thenshow"l' ≤ l" using L_props by simp qed thenhave l_sup_L': "Max L' = l" using Max_eq_iff[OF l_in_L'(1,2)] l_in_L'(3) by auto thenshow"sup_acc step accept rho q i j = sup_acc step accept rho (step q (bs_at rho i)) (Suc i) j" unfolding L_props(4) unfolding sup_acc_def Let_def using L'_def l_in_L'(2,3) L_props unfolding Suc_eq_plus1 by auto qed
lemma sup_leadsto_idle: "i < j ==> steps step rho init (i, j) ≠ q ==> sup_leadsto init step rho i j q = sup_leadsto init step rho (i + 1) j q" proof - assume assms: "i < j""steps step rho init (i, j) ≠ q"
define L where"L = {l. l < i ∧ steps step rho init (l, j) = q}"
define L' where"L' = {l. l < i + 1 ∧ steps step rho init (l, j) = q}" have L_L': "L = L'" unfolding L_def L'_defusing assms(2) less_antisym by fastforce show"sup_leadsto init step rho i j q = sup_leadsto init step rho (i + 1) j q" using L_def L'_def L_L' by (auto simp add: sup_leadsto_def) qed
lemma sup_leadsto_SomeI: "l < i ==> steps step rho init (l, j) = q ==> ∃l'. sup_leadsto init step rho i j q = Some (ts_at rho l') ∧ l ≤ l' ∧ l' < i" proof - assume assms: "l < i""steps step rho init (l, j) = q"
define L' where"L' = {l. l < i ∧ steps step rho init (l, j) = q}" have fin_L': "finite L'" unfolding L'_defby auto moreoverhave L_nonempty: "L' ≠ {}" using assms unfolding L'_def by (auto simp add: sup_leadsto_def split: if_splits) ultimatelyhave"Max L' ∈ L'" using Max_in by auto thenshow"∃l'. sup_leadsto init step rho i j q = Some (ts_at rho l') ∧ l ≤ l' ∧ l' < i" using L'_def L_nonempty assms by (fastforce simp add: sup_leadsto_def split: if_splits) qed
lemma sup_leadsto_SomeE: "i ≤ j ==> sup_leadsto init step rho i j q = Some ts ==> ∃l < i. steps step rho init (l, j) = q ∧ ts_at rho l = ts" proof - assume assms: "i ≤ j""sup_leadsto init step rho i j q = Some ts"
define L' where"L' = {l. l < i ∧ steps step rho init (l, j) = q}" have fin_L': "finite L'" unfolding L'_defby auto moreoverhave L_nonempty: "L' ≠ {}" using assms(2) unfolding L'_def by (auto simp add: sup_leadsto_def split: if_splits) ultimatelyhave"Max L' ∈ L'" using Max_in by auto thenshow"∃l < i. steps step rho init (l, j) = q ∧ ts_at rho l = ts" using assms(2) L'_def apply (auto simp add: sup_leadsto_def split: if_splits) using‹Max L' ∈ L'›by blast qed
lemma Mapping_keys_dest: "x ∈ mmap_keys f ==>∃y. mmap_lookup f x = Some y" by (auto simp add: mmap_keys_def mmap_lookup_def weak_map_of_SomeI)
lemma Mapping_keys_intro: "mmap_lookup f x ≠ None ==> x ∈ mmap_keys f" by (auto simp add: mmap_keys_def mmap_lookup_def)
(metis map_of_eq_None_iff option.distinct(1))
lemma Mapping_not_keys_intro: "mmap_lookup f x = None ==> x ∉ mmap_keys f" unfolding mmap_lookup_def mmap_keys_def using weak_map_of_SomeI by force
lemma Mapping_lookup_None_intro: "x ∉ mmap_keys f ==> mmap_lookup f x = None" unfolding mmap_lookup_def mmap_keys_def by (simp add: map_of_eq_None_iff)
primrec mmap_combine :: "'key ==> 'val ==> ('val ==> 'val ==> 'val) ==> ('key × 'val) list ==> ('key × 'val) list" where "mmap_combine k v c [] = [(k, v)]"
| "mmap_combine k v c (p # ps) = (case p of (k', v') ==> if k = k' then (k, c v' v) # ps else p # mmap_combine k v c ps)"
lemma mmap_combine_distinct_set: "distinct (map fst r) ==> distinct (map fst (mmap_combine k v c r)) ∧ set (map fst (mmap_combine k v c r)) = set (map fst r) ∪ {k}" by (induction r) force+
lemma mmap_combine_lookup: "distinct (map fst r) ==> mmap_lookup (mmap_combine k v c r) z = (if k = z then (case mmap_lookup r k of None ==> Some v | Some v' ==> Some (c v' v)) else mmap_lookup r z)" using eq_key_imp_eq_value by (induction r) (fastforce simp: mmap_lookup_def split: option.splits)+
definition mmap_fold :: "('c, 'd) mmap ==> (('c × 'd) ==> ('c × 'd)) ==> ('d ==> 'd==> 'd) ==> ('c, 'd) mmap ==> ('c, 'd) mmap"where "mmap_fold m f c r = foldl (λr p. case f p of (k, v) ==> mmap_combine k v c r) r m"
definition mmap_fold' :: "('c, 'd) mmap ==> 'e ==> (('c × 'd) × 'e ==> ('c × 'd) ×'e) ==> ('d ==> 'd ==> 'd) ==> ('c, 'd) mmap ==> ('c, 'd) mmap × 'e"where "mmap_fold' m e f c r = foldl (λ(r, e) p. case f (p, e) of ((k, v), e') ==> (mmap_combine k v c r, e')) (r, e) m"
lemma mmap_fold'_eq: "mmap_fold' m e f' c r = (m', e') ==> P e ==> (∧p e p' e'. P e ==> f' (p, e) = (p', e') ==> p' = f p ∧ P e') ==> m' = mmap_fold m f c r ∧ P e'" proof (induction m arbitrary: e r m' e') case (Cons p m) obtain k v e'' where kv_def: "f' (p, e) = ((k, v), e'')""P e''" using Cons by (cases "f' (p, e)") fastforce have mmap_fold: "mmap_fold m f c (mmap_combine k v c r) = mmap_fold (p # m) f c r" using Cons(1)[OF _ kv_def(2), where ?r="mmap_combine k v c r"] Cons(2,3,4) by (simp add: mmap_fold_def mmap_fold'_def kv_def(1)) have mmap_fold': "mmap_fold' m e'' f' c (mmap_combine k v c r) = (m', e')" using Cons(2) by (auto simp: mmap_fold'_def kv_def) show ?case using Cons(1)[OF mmap_fold' kv_def(2) Cons(4)] unfolding mmap_fold by auto qed (auto simp: mmap_fold_def mmap_fold'_def)
lemma foldl_mmap_combine_distinct_set: "distinct (map fst r) ==> distinct (map fst (mmap_fold m f c r)) ∧ set (map fst (mmap_fold m f c r)) = set (map fst r) ∪ set (map (fst ∘ f) m)" apply (induction m arbitrary: r) using mmap_combine_distinct_set apply (auto simp: mmap_fold_def split: prod.splits) apply force apply (smt Un_iff fst_conv imageI insert_iff) using mk_disjoint_insert apply fastforce+ done
lemma mmap_fold_lookup_rec: "distinct (map fst r) ==> mmap_lookup (mmap_fold m f c r) z = (case map (snd ∘ f) (filter (λ(k, v). fst (f (k, v)) = z) m) of [] ==> mmap_lookup r z | v # vs ==> (case mmap_lookup r z of None ==> Some (foldl c v vs) | Some w ==> Some (foldl c w (v # vs))))" proof (induction m arbitrary: r) case (Cons p ps) obtain k v where kv_def: "f p = (k, v)" by fastforce have distinct: "distinct (map fst (mmap_combine k v c r))" using mmap_combine_distinct_set[OF Cons(2)] by auto show ?case using Cons(1)[OF distinct, unfolded mmap_combine_lookup[OF Cons(2)]] by (auto simp: mmap_lookup_def kv_def mmap_fold_def split: list.splits option.splits) qed (auto simp: mmap_fold_def)
lemma mmap_fold_distinct: "distinct (map fst m) ==> distinct (map fst (mmap_fold m f c []))" using foldl_mmap_combine_distinct_set[of "[]"] by auto
lemma mmap_fold_set: "distinct (map fst m) ==> set (map fst (mmap_fold m f c [])) = (fst ∘ f) ` set m" using foldl_mmap_combine_distinct_set[of "[]"] by force
lemma mmap_lookup_empty: "mmap_lookup [] z = None" by (auto simp: mmap_lookup_def)
lemma mmap_fold_lookup: "distinct (map fst m) ==> mmap_lookup (mmap_fold m f c []) z = (case map (snd ∘ f) (filter (λ(k, v). fst (f (k, v)) = z) m) of [] ==> None | v # vs ==> Some (foldl c v vs))" using mmap_fold_lookup_rec[of "[]" _ f c] by (auto simp: mmap_lookup_empty split: list.splits)
definition fold_sup :: "('c, 'd :: timestamp) mmap ==> ('c ==> 'c) ==> ('c, 'd) mmap"where "fold_sup m f = mmap_fold m (λ(x, y). (f x, y)) sup []"
lemma mmap_lookup_distinct: "distinct (map fst m) ==> (k, v) ∈ set m ==> mmap_lookup m k = Some v" by (auto simp: mmap_lookup_def)
lemma fold_sup_distinct: "distinct (map fst m) ==> distinct (map fst (fold_sup m f))" using mmap_fold_distinct by (auto simp: fold_sup_def)
lemma fold_sup: fixes v :: "'d :: timestamp" shows"foldl sup v vs = fold sup vs v" by (induction vs arbitrary: v) (auto simp: sup.commute)
lemma lookup_fold_sup: assumes distinct: "distinct (map fst m)" shows"mmap_lookup (fold_sup m f) z = (let Z = {x ∈ mmap_keys m. f x = z} in if Z = {} then None else Some (Sup_fin ((the ∘ mmap_lookup m) ` Z)))" proof (cases "{x ∈ mmap_keys m. f x = z} = {}") case True have"z ∉ mmap_keys (mmap_fold m (λ(x, y). (f x, y)) sup [])" using True[unfolded mmap_keys_def] mmap_fold_set[OF distinct] by (auto simp: mmap_keys_def) thenhave"mmap_lookup (fold_sup m f) z = None" unfolding fold_sup_def by (meson Mapping_keys_intro) thenshow ?thesis unfolding True by auto next case False have z_in_keys: "z ∈ mmap_keys (mmap_fold m (λ(x, y). (f x, y)) sup [])" using False[unfolded mmap_keys_def] mmap_fold_set[OF distinct] by (force simp: mmap_keys_def) obtain v vs where vs_def: "mmap_lookup (fold_sup m f) z = Some (foldl sup v vs)" "v # vs = map snd (filter (λ(k, v). f k = z) m)" using mmap_fold_lookup[OF distinct, of "(λ(x, y). (f x, y))" sup z]
Mapping_keys_dest[OF z_in_keys] by (force simp: fold_sup_def mmap_keys_def comp_def split: list.splits prod.splits) have"set (v # vs) = (the ∘ mmap_lookup m) ` {x ∈ mmap_keys m. f x = z}" proof (rule set_eqI, rule iffI) fix w assume"w ∈ set (v # vs)" thenobtain x where x_def: "x ∈ mmap_keys m""f x = z""(x, w) ∈ set m" using vs_def(2) by (auto simp add: mmap_keys_def rev_image_eqI) show"w ∈ (the ∘ mmap_lookup m) ` {x ∈ mmap_keys m. f x = z}" using x_def(1,2) mmap_lookup_distinct[OF distinct x_def(3)] by force next fix w assume"w ∈ (the ∘ mmap_lookup m) ` {x ∈ mmap_keys m. f x = z}" thenobtain x where x_def: "x ∈ mmap_keys m""f x = z""(x, w) ∈ set m" using mmap_lookup_distinct[OF distinct] by (auto simp add: Mapping_keys_intro distinct mmap_lookup_def dest: Mapping_keys_dest) show"w ∈ set (v # vs)" using x_def by (force simp: vs_def(2)) qed thenhave"foldl sup v vs = Sup_fin ((the ∘ mmap_lookup m) ` {x ∈ mmap_keys m. f x = z})" unfolding fold_sup by (metis Sup_fin.set_eq_fold) thenshow ?thesis using False by (auto simp: vs_def(1)) qed
definition mmap_map :: "('a ==> 'b ==> 'c) ==> ('a, 'b) mmap ==> ('a, 'c) mmap"where "mmap_map f m = map (λ(k, v). (k, f k v)) m"
lemma mmap_map_keys: "mmap_keys (mmap_map f m) = mmap_keys m" by (force simp: mmap_map_def mmap_keys_def)
lemma mmap_map_fst: "map fst (mmap_map f m) = map fst m" by (auto simp: mmap_map_def)
definition cstep :: "('c ==> 'b ==> 'c) ==> ('c × 'b, 'c) mapping ==> 'c ==> 'b ==> ('c × ('c × 'b, 'c) mapping)"where "cstep step st q bs = (case Mapping.lookup st (q, bs) of None ==> (let res = step q bs in (res, Mapping.update (q, bs) res st)) | Some v ==> (v, st))"
definition cac :: "('c ==> bool) ==> ('c, bool) mapping ==> 'c ==> (bool × ('c, bool) mapping)"where "cac accept ac q = (case Mapping.lookup ac q of None ==> (let res = accept q in (res, Mapping.update q res ac)) | Some v ==> (v, ac))"
fun mmap_fold_s :: "('c ==> 'b ==> 'c) ==> ('c × 'b, 'c) mapping ==> ('c ==> bool) ==> ('c, bool) mapping ==> 'b ==> 'd ==> nat ==> ('c, 'c × ('d × nat) option) mmap ==> (('c, 'c × ('d × nat) option) mmap × ('c × 'b, 'c) mapping × ('c, bool) mapping)"where "mmap_fold_s step st accept ac bs t j [] = ([], st, ac)"
| "mmap_fold_s step st accept ac bs t j ((q, (q', tstp)) # qbss) = (let (q'', st') = cstep step st q' bs; (β, ac') = cac accept ac q''; (qbss', st'', ac'') = mmap_fold_s step st' accept ac' bs t j qbss in ((q, (q'', if β then Some (t, j) else tstp)) # qbss', st'', ac''))"
lemma mmap_fold_s_sound: "mmap_fold_s step st accept ac bs t j qbss = (qbss', st', ac') ==> (∧q bs. case Mapping.lookup st (q, bs) of None ==> True | Some v ==> step q bs = v) ==> (∧q bs. case Mapping.lookup ac q of None ==> True | Some v ==> accept q = v) ==> qbss' = mmap_map (λq (q', tstp). (step q' bs, if accept (step q' bs) then Some (t, j) else tstp)) qbss ∧ (∀q bs. case Mapping.lookup st' (q, bs) of None ==> True | Some v ==> step q bs = v) ∧ (∀q bs. case Mapping.lookup ac' q of None ==> True | Some v ==> accept q = v)" proof (induction qbss arbitrary: st ac qbss') case (Cons a qbss) obtain q q' tstp where a_def: "a = (q, (q', tstp))" by (cases a) auto obtain q'' st'' where q''_def: "cstep step st q' bs = (q'', st'')" "q'' = step q' bs" using Cons(3) by (cases "cstep step st q' bs")
(auto simp: cstep_def Let_def option.case_eq_if split: option.splits if_splits) obtain b ac'' where b_def: "cac accept ac q'' = (b, ac'')" "b = accept q''" using Cons(4) by (cases "cac accept ac q''")
(auto simp: cac_def Let_def option.case_eq_if split: option.splits if_splits) obtain qbss'' where qbss''_def: "mmap_fold_s step st'' accept ac'' bs t j qbss = (qbss'', st', ac')""qbss' = (q, q'', if b then Some (t, j) else tstp) # qbss''" using Cons(2)[unfolded a_def mmap_fold_s.simps q''_def(1) b_def(1)] unfolding Let_def by (auto simp: b_def(1) split: prod.splits) have ih: "∧q bs. case Mapping.lookup st'' (q, bs) of None ==> True | Some a ==> step q bs = a" "∧q bs. case Mapping.lookup ac'' q of None ==> True | Some a ==> accept q = a" using q''_def b_def Cons(3,4) by (auto simp: cstep_def cac_def Let_def Mapping.lookup_update' option.case_eq_if
split: option.splits if_splits) show ?case using Cons(1)[OF qbss''_def(1) ih] unfolding a_def q''_def(2) b_def(2) qbss''_def(2) by (auto simp: mmap_map_def) qed (auto simp: mmap_map_def)
definition adv_end :: "('b, 'c, 'd :: timestamp, 't, 'e) args ==> ('b, 'c, 'd, 't, 'e) window ==> ('b, 'c, 'd, 't, 'e) window option"where "adv_end args w = (let step = w_step args; accept = w_accept args; run_t = w_run_t args; run_sub = w_run_sub args; st = w_st w; ac = w_ac w; j = w_j w; tj = w_tj w; sj = w_sj w; s = w_s w; e = w_e w in (case run_t tj of None ==> None | Some (tj', t) ==> (case run_sub sj of None ==> None | Some (sj', bs) ==> let (s', st', ac') = mmap_fold_s step st accept ac bs t j s; (e', st'') = mmap_fold' e st' (λ((x, y), st). let (q', st') = cstep step st x bs in ((q', y), st')) sup [] in Some (w(w_st := st'', w_ac := ac', w_j := Suc j, w_tj := tj', w_sj := sj', w_s := s', w_e := e')))))"
lemma map_values_lookup: "mmap_lookup (mmap_map f m) z = Some v' ==> ∃v. mmap_lookup m z = Some v ∧ v' = f z v" by (induction m) (auto simp: mmap_lookup_def mmap_map_def)
lemma acc_app: assumes"i ≤ j""steps step rho q (i, Suc j) = q'""accept q'" shows"sup_acc step accept rho q i (Suc j) = Some (ts_at rho j, j)" proof -
define L where"L = {l ∈ {i..<Suc j}. accept (steps step rho q (i, Suc l))}" have nonempty: "finite L""L ≠ {}" using assms unfolding L_def by auto moreoverhave"Max {l ∈ {i..<Suc j}. accept (steps step rho q (i, Suc l))} = j" unfolding L_def[symmetric] Max_eq_iff[OF nonempty, of j] unfolding L_def using assms by auto ultimatelyshow ?thesis by (auto simp add: sup_acc_def acc_def L_def) qed
lemma sup_fin_closed: "finite A ==> A ≠ {} ==> (∧x y. x ∈ A ==> y ∈ A ==> sup x y ∈ {x, y}) ==>⊔fin A ∈ A" apply (induct A rule: finite.induct) using Sup_fin.insert by auto fastforce
lemma valid_adv_end: assumes"valid_window args t0 sub rho w""w_run_t args (w_tj w) = Some (tj', t)" "w_run_sub args (w_sj w) = Some (sj', bs)" "∧t'. t' ∈ set (map fst rho) ==> t' ≤ t" shows"case adv_end args w of None ==> False | Some w' ==> valid_window args t0 sub (rho @ [(t, bs)]) w'" proof -
define init where"init = w_init args"
define step where"step = w_step args"
define accept where"accept = w_accept args"
define run_t where"run_t = w_run_t args"
define run_sub where"run_sub = w_run_sub args"
define st where"st = w_st w"
define ac where"ac = w_ac w"
define i where"i = w_i w"
define ti where"ti = w_ti w"
define si where"si = w_si w"
define j where"j = w_j w"
define tj where"tj = w_tj w"
define sj where"sj = w_sj w"
define s where"s = w_s w"
define e where"e = w_e w" have valid_before: "reach_window args t0 sub rho (i, ti, si, j, tj, sj)" "∧i j. i ≤ j ==> j < length rho ==> ts_at rho i ≤ ts_at rho j" "(∧q bs. case Mapping.lookup st (q, bs) of None ==> True | Some v ==> step q bs = v)" "(∧q bs. case Mapping.lookup ac q of None ==> True | Some v ==> accept q = v)" "∀q. mmap_lookup e q = sup_leadsto init step rho i j q""distinct (map fst e)" "valid_s init step st accept rho i i j s" using assms(1) unfolding valid_window_def valid_s_def Let_def init_def step_def accept_def run_t_def
run_sub_def st_def ac_def i_def ti_def si_def j_def tj_def sj_def s_def e_def by auto have i_j: "i ≤ j" using valid_before(1) by auto have distinct_before: "distinct (map fst s)""distinct (map fst e)" using valid_before by (auto simp: valid_s_def) note run_tj = assms(2)[folded run_t_def tj_def] note run_sj = assms(3)[folded run_sub_def sj_def]
define rho' where"rho' = rho @ [(t, bs)]" have ts_at_mono: "∧i j. i ≤ j ==> j < length rho' ==> ts_at rho' i ≤ ts_at rho' j" using valid_before(2) assms(4) by (auto simp: rho'_def ts_at_def nth_append split: option.splits list.splits if_splits) obtain s' st' ac' where s'_def: "mmap_fold_s step st accept ac bs t j s = (s', st', ac')" apply (cases "mmap_fold_s step st accept ac bs t j s") apply (auto) done have s'_mmap_map: "s' = mmap_map (λq (q', tstp). (step q' bs, if accept (step q' bs) then Some (t, j) else tstp)) s" "(∧q bs. case Mapping.lookup st' (q, bs) of None ==> True | Some v ==> step q bs = v)" "(∧q bs. case Mapping.lookup ac' q of None ==> True | Some v ==> accept q = v)" using mmap_fold_s_sound[OF s'_def valid_before(3,4)] by auto obtain e' st'' where e'_def: "mmap_fold' e st' (λ((x, y), st). let (q', st') = cstep step st x bs in ((q', y), st')) sup [] = (e', st'')" by (metis old.prod.exhaust)
define inv where"inv ≡ λst'. ∀q bs. case Mapping.lookup st' (q, bs) of None ==> True | Some v ==> step q bs = v" have inv_st': "inv st'" using s'_mmap_map(2) by (auto simp: inv_def) have"∧p e p' e'. inv e ==> (case (p, e) of (x, xa) ==> (case x of (x, y) ==> λst. let (q', st') = cstep step st x bs in ((q', y), st')) xa) = (p', e') ==> p' = (case p of (x, y) ==> (step x bs, y)) ∧ inv e'" by (auto simp: inv_def cstep_def Let_def Mapping.lookup_update' split: option.splits if_splits) thenhave e'_fold_sup_st'': "e' = fold_sup e (λq. step q bs)" "(∧q bs. case Mapping.lookup st'' (q, bs) of None ==> True | Some v ==> step q bs = v)" using mmap_fold'_eq[OF e'_def, of inv "λ(x, y). (step x bs, y)", OF inv_st'] by (fastforce simp: fold_sup_def inv_def)+ have adv_end: "adv_end args w = Some (w(w_st := st'', w_ac := ac', w_j := Suc j, w_tj := tj', w_sj := sj', w_s := s', w_e := e'))" using run_tj run_sj e'_def[unfolded st_def] unfolding adv_end_def init_def step_def accept_def run_t_def run_sub_def
i_def ti_def si_def j_def tj_def sj_def s_def e_def s'_def e'_def by (auto simp: Let_def s'_def[unfolded step_def st_def accept_def ac_def j_def s_def]) have keys_s': "mmap_keys s' = mmap_keys s" by (force simp: mmap_keys_def mmap_map_def s'_mmap_map(1)) have lookup_s: "∧q q' tstp. mmap_lookup s q = Some (q', tstp) ==> steps step rho' q (i, j) = q' ∧ tstp = sup_acc step accept rho' q i j" using valid_before Mapping_keys_intro by (force simp add: Let_def rho'_def valid_s_def steps_app_cong sup_acc_app_cong
split: option.splits) have bs_at_rho'_j: "bs_at rho' j = bs" using valid_before by (auto simp: rho'_def bs_at_def nth_append) have ts_at_rho'_j: "ts_at rho' j = t" using valid_before by (auto simp: rho'_def ts_at_def nth_append) have lookup_s': "∧q q' tstp. mmap_lookup s' q = Some (q', tstp) ==> steps step rho' q (i, Suc j) = q' ∧ tstp = sup_acc step accept rho' q i (Suc j)" proof - fix q q'' tstp' assume assm: "mmap_lookup s' q = Some (q'', tstp')" obtain q' tstp where"mmap_lookup s q = Some (q', tstp)""q'' = step q' bs" "tstp' = (if accept (step q' bs) then Some (t, j) else tstp)" using map_values_lookup[OF assm[unfolded s'_mmap_map]] by auto thenshow"steps step rho' q (i, Suc j) = q'' ∧ tstp' = sup_acc step accept rho' q i (Suc j)" using lookup_s apply (auto simp: bs_at_rho'_j ts_at_rho'_j) apply (metis Suc_eq_plus1 bs_at_rho'_j i_j steps_app) apply (metis acc_app bs_at_rho'_j i_j steps_appE ts_at_rho'_j) apply (metis Suc_eq_plus1 bs_at_rho'_j i_j steps_app) apply (metis (no_types, lifting) acc_app_idle bs_at_rho'_j i_j steps_appE) done qed have lookup_e: "∧q. mmap_lookup e q = sup_leadsto init step rho' i j q" using valid_before sup_leadsto_app_cong[of _ _ rho init step] by (auto simp: rho'_def) have keys_e_alt: "mmap_keys e = {q. ∃l < i. steps step rho' init (l, j) = q}" using valid_before apply (auto simp add: sup_leadsto_def rho'_def) apply (metis (no_types, lifting) Mapping_keys_dest lookup_e rho'_def sup_leadsto_SomeE) apply (metis (no_types, lifting) Mapping_keys_intro option.simps(3) order_refl steps_app_cong) done have finite_keys_e: "finite (mmap_keys e)" unfolding keys_e_alt by (rule finite_surj[of "{l. l < i}"]) auto have"reaches_on run_sub sub (map snd rho) sj" using valid_before reaches_on_trans unfolding run_sub_def sub_def by fastforce thenhave reaches_on': "reaches_on run_sub sub (map snd rho @ [bs]) sj'" using reaches_on_app run_sj by fast have"reaches_on run_t t0 (map fst rho) tj" using valid_before reaches_on_trans unfolding run_t_def by fastforce thenhave reach_t': "reaches_on run_t t0 (map fst rho') tj'" using reaches_on_app run_tj unfolding rho'_def by fastforce have lookup_e': "∧q. mmap_lookup e' q = sup_leadsto init step rho' i (Suc j) q" proof - fix q
define Z where"Z = {x ∈ mmap_keys e. step x bs = q}" show"mmap_lookup e' q = sup_leadsto init step rho' i (Suc j) q" proof (cases "Z = {}") case True thenhave"mmap_lookup e' q = None" using Z_def lookup_fold_sup[OF distinct_before(2)] unfolding e'_fold_sup_st'' by (auto simp: Let_def) moreoverhave"sup_leadsto init step rho' i (Suc j) q = None" proof (rule ccontr) assume assm: "sup_leadsto init step rho' i (Suc j) q ≠ None" obtain l where l_def: "l < i""steps step rho' init (l, Suc j) = q" using i_j sup_leadsto_SomeE[of i "Suc j"] assm by force have l_j: "l ≤ j" using less_le_trans[OF l_def(1) i_j] by auto obtain q'' where q''_def: "steps step rho' init (l, j) = q''""step q'' bs = q" using steps_appE[OF _ l_def(2)] l_j by (auto simp: bs_at_rho'_j) thenhave"q'' ∈ mmap_keys e" using keys_e_alt l_def(1) by auto thenshow"False" using Z_def q''_def(2) True by auto qed ultimatelyshow ?thesis by auto next case False thenhave lookup_e': "mmap_lookup e' q = Some (Sup_fin ((the ∘ mmap_lookup e) ` Z))" using Z_def lookup_fold_sup[OF distinct_before(2)] unfolding e'_fold_sup_st'' by (auto simp: Let_def)
define L where"L = {l. l < i ∧ steps step rho' init (l, Suc j) = q}" have fin_L: "finite L" unfolding L_def by auto have Z_alt: "Z = {x. ∃l < i. steps step rho' init (l, j) = x ∧ step x bs = q}" using Z_def[unfolded keys_e_alt] by auto have fin_Z: "finite Z" unfolding Z_alt by auto have L_nonempty: "L ≠ {}" using L_def Z_alt False i_j steps_app[of _ _ step rho q] by (auto simp: bs_at_rho'_j)
(smt Suc_eq_plus1 bs_at_rho'_j less_irrefl_nat less_le_trans nat_le_linear steps_app) have sup_leadsto: "sup_leadsto init step rho' i (Suc j) q = Some (ts_at rho' (Max L))" using L_nonempty L_def by (auto simp add: sup_leadsto_def) have j_lt_rho': "j < length rho'" using valid_before by (auto simp: rho'_def) have"Sup_fin ((the ∘ mmap_lookup e) ` Z) = ts_at rho' (Max L)" proof (rule antisym) obtain z ts where zts_def: "z ∈ Z""(the ∘ mmap_lookup e) z = ts" "Sup_fin ((the ∘ mmap_lookup e) ` Z) = ts" proof - assume lassm: "∧z ts. z ∈ Z ==> (the ∘ mmap_lookup e) z = ts ==> ⊔fin ((the ∘ mmap_lookup e) ` Z) = ts ==> thesis"
define T where"T = (the ∘ mmap_lookup e) ` Z" have T_sub: "T ⊆ ts_at rho' ` {..j}" using lookup_e keys_e_alt i_j by (auto simp add: T_def Z_def sup_leadsto_def) have"finite T""T ≠ {}" using fin_Z False by (auto simp add: T_def) thenhave sup_in: "⊔fin T ∈ T" proof (rule sup_fin_closed) fix x y assume xy: "x ∈ T""y ∈ T" thenobtain a c where"x = ts_at rho' a""y = ts_at rho' c""a ≤ j""c ≤ j" using T_sub by (meson atMost_iff imageE subsetD) thenshow"sup x y ∈ {x, y}" using ts_at_mono j_lt_rho' by (cases "a ≤ c") (auto simp add: sup.absorb1 sup.absorb2) qed thenshow ?thesis using lassm by (auto simp add: T_def) qed from zts_def(2) have lookup_e_z: "mmap_lookup e z = Some ts" using zts_def(1) Z_def by (auto dest: Mapping_keys_dest) have"sup_leadsto init step rho' i j z = Some ts" using lookup_e_z lookup_e by auto thenobtain l where l_def: "l < i""steps step rho' init (l, j) = z""ts_at rho' l = ts" using sup_leadsto_SomeE[OF i_j] by (fastforce simp: rho'_def ts_at_def nth_append) have l_j: "l ≤ j" using less_le_trans[OF l_def(1) i_j] by auto have"l ∈ L" unfolding L_def using l_def zts_def(1) Z_alt by auto (metis (no_types, lifting) Suc_eq_plus1 bs_at_rho'_j l_j steps_app) thenhave"l ≤ Max L""Max L < i" using L_nonempty fin_L by (auto simp add: L_def) thenshow"Sup_fin ((the ∘ mmap_lookup e) ` Z) ≤ ts_at rho' (Max L)" unfolding zts_def(3) l_def(3)[symmetric] using ts_at_mono i_j j_lt_rho' by (auto simp: rho'_def) next obtain l where l_def: "Max L = l""l < i""steps step rho' init (l, Suc j) = q" using Max_in[OF fin_L L_nonempty] L_def by auto obtain z where z_def: "steps step rho' init (l, j) = z""step z bs = q" using l_def(2,3) i_j bs_at_rho'_j by (metis less_imp_le_nat less_le_trans steps_appE) have z_in_Z: "z ∈ Z" unfolding Z_alt using l_def(2) z_def i_j by fastforce have lookup_e_z: "mmap_lookup e z = sup_leadsto init step rho' i j z" using lookup_e z_in_Z Z_alt by auto obtain l' where l'_def: "sup_leadsto init step rho' i j z = Some (ts_at rho' l')" "l ≤ l'""l' < i" using sup_leadsto_SomeI[OF l_def(2) z_def(1)] by auto have"ts_at rho' l' ∈ (the ∘ mmap_lookup e) ` Z" using lookup_e_z l'_def(1) z_in_Z by force thenhave"ts_at rho' l' ≤ Sup_fin ((the ∘ mmap_lookup e) ` Z)" using Inf_fin_le_Sup_fin fin_Z z_in_Z by (simp add: Sup_fin.coboundedI) thenshow"ts_at rho' (Max L) ≤ Sup_fin ((the ∘ mmap_lookup e) ` Z)" unfolding l_def(1) using ts_at_mono l'_def(2,3) i_j j_lt_rho' by (fastforce simp: rho'_def) qed thenshow ?thesis unfolding lookup_e' sup_leadsto by auto qed qed have"distinct (map fst s')""distinct (map fst e')" using distinct_before mmap_fold_distinct unfolding s'_mmap_map mmap_map_fst e'_fold_sup_st'' fold_sup_def by auto moreoverhave"mmap_keys s' = {q. ∃l≤i. steps step rho' init (l, i) = q}" unfolding keys_s' rho'_def using valid_before(1,7) valid_s_def[of init step st accept rho i i j s] by (auto simp: steps_app_cong[of _ rho step]) moreoverhave"reaches_on run_t ti (drop i (map fst rho')) tj'" "reaches_on run_sub si (drop i (map snd rho')) sj'" using valid_before reaches_on_app run_tj run_sj by (auto simp: rho'_def run_t_def run_sub_def) ultimatelyshow ?thesis unfolding adv_end using valid_before lookup_e' lookup_s' ts_at_mono s'_mmap_map(3) e'_fold_sup_st''(2) by (fastforce simp: valid_window_def Let_def init_def step_def accept_def run_t_def
run_sub_def i_def ti_def si_def j_def tj_def sj_def s_def e'_def
rho'_def valid_s_def intro!: exI[of _ rho'] split: option.splits) qed
lemma adv_end_bounds: assumes"w_run_t args (w_tj w) = Some (tj', t)" "w_run_sub args (w_sj w) = Some (sj', bs)" "adv_end args w = Some w'" shows"w_i w' = w_i w""w_ti w' = w_ti w""w_si w' = w_si w" "w_j w' = Suc (w_j w)""w_tj w' = tj'""w_sj w' = sj'" using assms by (auto simp: adv_end_def Let_def split: prod.splits)
definition drop_cur :: "nat ==> ('c × ('d × nat) option) ==> ('c × ('d × nat) option)"where "drop_cur i = (λ(q', tstp). (q', case tstp of Some (ts, tp) ==> if tp = i then None else tstp | None ==> tstp))"
definition adv_d :: "('c ==> 'b ==> 'c) ==> ('c × 'b, 'c) mapping ==> nat ==> 'b ==> ('c, 'c × ('d × nat) option) mmap ==> (('c, 'c × ('d × nat) option) mmap × ('c × 'b, 'c) mapping)"where "adv_d step st i b s = (mmap_fold' s st (λ((x, v), st). case cstep step st x b of (x', st') ==> ((x', drop_cur i v), st')) (λx y. x) [])"
lemma adv_d_mmap_fold: assumes inv: "∧q bs. case Mapping.lookup st (q, bs) of None ==> True | Some v ==>step q bs = v" and fold': "mmap_fold' s st (λ((x, v), st). case cstep step st x bs of (x', st') ==> ((x', drop_cur i v), st')) (λx y. x) r = (s', st')" shows"s' = mmap_fold s (λ(x, v). (step x bs, drop_cur i v)) (λx y. x) r ∧ (∀q bs. case Mapping.lookup st' (q, bs) of None ==> True | Some v ==> step q bs = v)" proof -
define inv where"inv ≡ λst. ∀q bs. case Mapping.lookup st (q, bs) of None ==> True | Some v ==> step q bs = v" have inv_st: "inv st" using inv by (auto simp: inv_def) show ?thesis by (rule mmap_fold'_eq[OF fold', of inv "λ(x, v). (step x bs, drop_cur i v)",
OF inv_st, unfolded inv_def])
(auto simp: cstep_def Let_def Mapping.lookup_update'
split: prod.splits option.splits if_splits) qed
definition keys_idem :: "('c ==> 'b ==> 'c) ==> nat ==> 'b ==> ('c, 'c × ('d × nat) option) mmap ==> bool"where "keys_idem step i b s = (∀x ∈ mmap_keys s. ∀x' ∈ mmap_keys s. step x b = step x' b ⟶ drop_cur i (the (mmap_lookup s x)) = drop_cur i (the (mmap_lookup s x')))"
lemma adv_d_keys: assumes inv: "∧q bs. case Mapping.lookup st (q, bs) of None ==> True | Some v ==>step q bs = v" and distinct: "distinct (map fst s)" and adv_d: "adv_d step st i bs s = (s', st')" shows"mmap_keys s' = (λq. step q bs) ` (mmap_keys s)" using adv_d_mmap_fold[OF inv adv_d[unfolded adv_d_def]]
mmap_fold_set[OF distinct] unfolding mmap_keys_def by fastforce
lemma lookup_adv_d_None: assumes inv: "∧q bs. case Mapping.lookup st (q, bs) of None ==> True | Some v ==>step q bs = v" and distinct: "distinct (map fst s)" and adv_d: "adv_d step st i bs s = (s', st')" and Z_empty: "{x ∈ mmap_keys s. step x bs = z} = {}" shows"mmap_lookup s' z = None" proof - have"z ∉ mmap_keys (mmap_fold s (λ(x, v). (step x bs, drop_cur i v)) (λx y. x) [])" using Z_empty[unfolded mmap_keys_def] mmap_fold_set[OF distinct] by (auto simp: mmap_keys_def) thenshow ?thesis using adv_d adv_d_mmap_fold[OF inv adv_d[unfolded adv_d_def]] unfolding adv_d_def by (simp add: Mapping_lookup_None_intro) qed
lemma lookup_adv_d_Some: assumes inv: "∧q bs. case Mapping.lookup st (q, bs) of None ==> True | Some v ==>step q bs = v" and distinct: "distinct (map fst s)"and idem: "keys_idem step i bs s" and wit: "x ∈ mmap_keys s""step x bs = z" and adv_d: "adv_d step st i bs s = (s', st')" shows"mmap_lookup s' z = Some (drop_cur i (the (mmap_lookup s x)))" proof - have z_in_keys: "z ∈ mmap_keys (mmap_fold s (λ(x, v). (step x bs, drop_cur i v)) (λx y. x) [])" using wit(1,2)[unfolded mmap_keys_def] mmap_fold_set[OF distinct] by (force simp: mmap_keys_def) obtain v vs where vs_def: "mmap_lookup s' z = Some (foldl (λx y. x) v vs)" "v # vs = map (λ(x, v). drop_cur i v) (filter (λ(k, v). step k bs = z) s)" using adv_d adv_d_mmap_fold[OF inv adv_d[unfolded adv_d_def]] unfolding adv_d_def using mmap_fold_lookup[OF distinct, of "(λ(x, v). (step x bs, drop_cur i v))""λx y. x"z]
Mapping_keys_dest[OF z_in_keys] by (force simp: adv_d_def mmap_keys_def split: list.splits) have"set (v # vs) = drop_cur i ` (the ∘ mmap_lookup s) ` {x ∈ mmap_keys s. step x bs = z}" proof (rule set_eqI, rule iffI) fix w assume"w ∈ set (v # vs)" thenobtain x y where xy_def: "x ∈ mmap_keys s""step x bs = z""(x, y) ∈ set s" "w = drop_cur i y" using vs_def(2) by (auto simp add: mmap_keys_def rev_image_eqI) show"w ∈ drop_cur i ` (the ∘ mmap_lookup s) ` {x ∈ mmap_keys s. step x bs = z}" using xy_def(1,2,4) mmap_lookup_distinct[OF distinct xy_def(3)] by force next fix w assume"w ∈ drop_cur i ` (the ∘ mmap_lookup s) ` {x ∈ mmap_keys s. step x bs = z}" thenobtain x y where xy_def: "x ∈ mmap_keys s""step x bs = z""(x, y) ∈ set s" "w = drop_cur i y" using mmap_lookup_distinct[OF distinct] by (auto simp add: Mapping_keys_intro distinct mmap_lookup_def dest: Mapping_keys_dest) show"w ∈ set (v # vs)" using xy_def by (force simp: vs_def(2)) qed thenhave"foldl (λx y. x) v vs = drop_cur i (the (mmap_lookup s x))" using wit apply (induction vs arbitrary: v) apply (auto) apply (metis (mono_tags, lifting) emptyE imageI insertE mem_Collect_eq) apply (smt Collect_cong idem imageE insert_compr keys_idem_def mem_Collect_eq) done thenshow ?thesis using wit by (auto simp: vs_def(1)) qed
definition"loop_cond j = (λ(st, ac, i, ti, si, q, s, tstp). i < j ∧ q ∉ mmap_keys s)" definition"loop_body step accept run_t run_sub = (λ(st, ac, i, ti, si, q, s, tstp). case run_t ti of Some (ti', t) ==> case run_sub si of Some (si', b) ==> case adv_d step st i b s of (s', st') ==> case cstep step st' q b of (q', st'') ==> case cac accept ac q' of (β, ac') ==> (st'', ac', Suc i, ti', si', q', s', if β then Some (t, i) else tstp))" definition"loop_inv init step accept args t0 sub rho u j tj sj = (λ(st, ac, i, ti, si, q, s, tstp). u + 1 ≤ i ∧ reach_window args t0 sub rho (i, ti, si, j, tj, sj) ∧ steps step rho init (u + 1, i) = q ∧ (∀q. case Mapping.lookup ac q of None ==> True | Some v ==> accept q = v) ∧ valid_s init step st accept rho u i j s ∧ tstp = sup_acc step accept rho init (u + 1) i)"
lemma mmap_update_distinct: "distinct (map fst m) ==> distinct (map fst (mmap_update k v m))" by (auto simp: mmap_update_def distinct_update)
definition adv_start :: "('b, 'c, 'd :: timestamp, 't, 'e) args ==> ('b, 'c, 'd, 't, 'e) window ==> ('b, 'c, 'd, 't, 'e) window"where "adv_start args w = (let init = w_init args; step = w_step args; accept = w_accept args; run_t = w_run_t args; run_sub = w_run_sub args; st = w_st w; ac = w_ac w; i = w_i w; ti = w_ti w; si = w_si w; j = w_j w; s = w_s w; e = w_e w in (case run_t ti of Some (ti', t) ==> (case run_sub si of Some (si', bs) ==> let (s', st') = adv_d step st i bs s; e' = mmap_update (fst (the (mmap_lookup s init))) t e; (st_cur, ac_cur, i_cur, ti_cur, si_cur, q_cur, s_cur, tstp_cur) = while (loop_cond j) (loop_body step accept run_t run_sub) (st', ac, Suc i, ti', si', init, s', None); s'' = mmap_update init (case mmap_lookup s_cur q_cur of Some (q', tstp') ==> (case tstp' of Some (ts, tp) ==> (q', tstp') | None ==> (q', tstp_cur)) | None ==> (q_cur, tstp_cur)) s' in w(w_st := st_cur, w_ac := ac_cur, w_i := Suc i, w_ti := ti', w_si := si', w_s := s'', w_e := e'))))"
lemma valid_adv_d: assumes valid_before: "valid_s init step st accept rho u i j s" and u_le_i: "u ≤ i"and i_lt_j: "i < j"and b_def: "b = bs_at rho i" and adv_d: "adv_d step st i b s = (s', st')" shows"valid_s init step st' accept rho u (i + 1) j s'" proof - have inv_st: "∧q bs. case Mapping.lookup st (q, bs) of None ==> True | Some v ==>step q bs = v" using valid_before by (auto simp add: valid_s_def) have keys_s: "mmap_keys s = {q. (∃l ≤ u. steps step rho init (l, i) = q)}" using valid_before by (auto simp add: valid_s_def) have fin_keys_s: "finite (mmap_keys s)" using valid_before by (auto simp add: valid_s_def) have lookup_s: "∧q q' tstp. mmap_lookup s q = Some (q', tstp) ==> steps step rho q (i, j) = q' ∧ tstp = sup_acc step accept rho q i j" using valid_before Mapping_keys_intro by (auto simp add: valid_s_def) (smt case_prodD option.simps(5))+ have drop_cur_i: "∧x. x ∈ mmap_keys s ==> drop_cur i (the (mmap_lookup s x)) = (steps step rho (step x (bs_at rho i)) (i + 1, j), sup_acc step accept rho (step x (bs_at rho i)) (i + 1) j)" proof - fix x assume assms: "x ∈ mmap_keys s" obtain q tstp where q_def: "mmap_lookup s x = Some (q, tstp)" using assms(1) by (auto dest: Mapping_keys_dest) have q_q': "q = steps step rho (step x (bs_at rho i)) (i + 1, j)" "tstp = sup_acc step accept rho x i j" using lookup_s[OF q_def] steps_split[OF i_lt_j] assms(1) by auto show"drop_cur i (the (mmap_lookup s x)) = (steps step rho (step x (bs_at rho i)) (i + 1, j), sup_acc step accept rho (step x (bs_at rho i)) (i + 1) j)" using q_def sup_acc_None[OF i_lt_j, of step accept rho]
sup_acc_i[OF i_lt_j, of step accept rho] sup_acc_l[OF i_lt_j, of _ step accept rho] unfolding q_q' by (auto simp add: drop_cur_def split: option.splits) qed have valid_drop_cur: "∧x x'. x ∈ mmap_keys s ==> x' ∈ mmap_keys s ==> step x (bs_at rho i) = step x' (bs_at rho i) ==> drop_cur i (the (mmap_lookup s x)) = drop_cur i (the (mmap_lookup s x'))" using drop_cur_i by auto thenhave keys_idem: "keys_idem step i b s" unfolding keys_idem_def b_def by blast have distinct: "distinct (map fst s)" using valid_before by (auto simp: valid_s_def) have"(λq. step q (bs_at rho i)) ` {q. ∃l≤u. steps step rho init (l, i) = q} = {q. ∃l≤u. steps step rho init (l, i + 1) = q}" using steps_app[of _ i step rho init] u_le_i by auto thenhave keys_s': "mmap_keys s' = {q. ∃l≤u. steps step rho init (l, i + 1) = q}" using adv_d_keys[OF _ distinct adv_d] inv_st unfolding keys_s b_def by auto have lookup_s': "∧q q' tstp. mmap_lookup s' q = Some (q', tstp) ==> steps step rho q (i + 1, j) = q' ∧ tstp = sup_acc step accept rho q (i + 1) j" proof - fix q q' tstp assume assm: "mmap_lookup s' q = Some (q', tstp)" obtain x where wit: "x ∈ mmap_keys s""step x (bs_at rho i) = q" using assm lookup_adv_d_None[OF _ distinct adv_d] inv_st by (fastforce simp: b_def) have lookup_s'_q: "mmap_lookup s' q = Some (drop_cur i (the (mmap_lookup s x)))" using lookup_adv_d_Some[OF _ distinct keys_idem wit[folded b_def] adv_d] inv_st by auto thenshow"steps step rho q (i + 1, j) = q' ∧ tstp = sup_acc step accept rho q (i + 1) j" using assm by (simp add: drop_cur_i wit) qed have"distinct (map fst s')" using mmap_fold_distinct[OF distinct] adv_d_mmap_fold[OF inv_st adv_d[unfolded adv_d_def]] unfolding adv_d_def mmap_map_fst by auto thenshow"valid_s init step st' accept rho u (i + 1) j s'" unfolding valid_s_def using keys_s' lookup_s' u_le_i inv_st adv_d[unfolded adv_d_def]
adv_d_mmap_fold[OF inv_st adv_d[unfolded adv_d_def]] by (auto split: option.splits dest: Mapping_keys_dest) qed
lemma mmap_lookup_update': "mmap_lookup (mmap_update k v kvs) z = (if k = z then Some v else mmap_lookup kvs z)" unfolding mmap_lookup_def mmap_update_def by (auto simp add: update_conv')
lemma mmap_keys_update: "mmap_keys (mmap_update k v kvs) = mmap_keys kvs ∪ {k}" by (induction kvs) (auto simp: mmap_keys_def mmap_update_def)
lemma valid_adv_start: assumes"valid_window args t0 sub rho w""w_i w < w_j w" shows"valid_window args t0 sub rho (adv_start args w)" proof -
define init where"init = w_init args"
define step where"step = w_step args"
define accept where"accept = w_accept args"
define run_t where"run_t = w_run_t args"
define run_sub where"run_sub = w_run_sub args"
define st where"st = w_st w"
define ac where"ac = w_ac w"
define i where"i = w_i w"
define ti where"ti = w_ti w"
define si where"si = w_si w"
define j where"j = w_j w"
define tj where"tj = w_tj w"
define sj where"sj = w_sj w"
define s where"s = w_s w"
define e where"e = w_e w" have valid_before: "reach_window args t0 sub rho (i, ti, si, j, tj, sj)" "∧i j. i ≤ j ==> j < length rho ==> ts_at rho i ≤ ts_at rho j" "(∧q bs. case Mapping.lookup st (q, bs) of None ==> True | Some v ==> step q bs = v)" "(∧q bs. case Mapping.lookup ac q of None ==> True | Some v ==> accept q = v)" "∀q. mmap_lookup e q = sup_leadsto init step rho i j q""distinct (map fst e)" "valid_s init step st accept rho i i j s" using assms(1) unfolding valid_window_def valid_s_def Let_def init_def step_def accept_def run_t_def
run_sub_def st_def ac_def i_def ti_def si_def j_def tj_def sj_def s_def e_def by auto have distinct_before: "distinct (map fst s)""distinct (map fst e)" using valid_before by (auto simp: valid_s_def) note i_lt_j = assms(2)[folded i_def j_def] obtain ti' si' t b where tb_def: "run_t ti = Some (ti', t)" "run_sub si = Some (si', b)" "reaches_on run_t ti' (drop (Suc i) (map fst rho)) tj" "reaches_on run_sub si' (drop (Suc i) (map snd rho)) sj" "t = ts_at rho i""b = bs_at rho i" using valid_before i_lt_j apply (auto simp: ts_at_def bs_at_def run_t_def[symmetric] run_sub_def[symmetric]
elim!: reaches_on.cases[of run_t ti "drop i (map fst rho)" tj]
reaches_on.cases[of run_sub si "drop i (map snd rho)" sj]) by (metis Cons_nth_drop_Suc length_map list.inject nth_map) have reaches_on_si': "reaches_on run_sub sub (take (Suc i) (map snd rho)) si'" using valid_before tb_def(2,3,4) i_lt_j reaches_on_app tb_def(1) by (auto simp: run_sub_def sub_def bs_at_def take_Suc_conv_app_nth reaches_on_app tb_def(6)) have reaches_on_ti': "reaches_on run_t t0 (take (Suc i) (map fst rho)) ti'" using valid_before tb_def(2,3,4) i_lt_j reaches_on_app tb_def(1) by (auto simp: run_t_def ts_at_def take_Suc_conv_app_nth reaches_on_app tb_def(5))
define e' where"e' = mmap_update (fst (the (mmap_lookup s init))) t e" obtain st' s' where s'_def: "adv_d step st i b s = (s', st')" by (metis old.prod.exhaust) obtain st_cur ac_cur i_cur ti_cur si_cur q_cur s_cur tstp_cur where loop_def: "(st_cur, ac_cur, i_cur, ti_cur, si_cur, q_cur, s_cur, tstp_cur) = while (loop_cond j) (loop_body step accept run_t run_sub) (st', ac, Suc i, ti', si', init, s', None)" by (cases "while (loop_cond j) (loop_body step accept run_t run_sub) (st', ac, Suc i, ti', si', init, s', None)") auto
define s'' where"s'' = mmap_update init (case mmap_lookup s_cur q_cur of Some (q', tstp') ==> (case tstp' of Some (ts, tp) ==> (q', tstp') | None ==> (q', tstp_cur)) | None ==> (q_cur, tstp_cur)) s'" have i_le_j: "i ≤ j" using i_lt_j by auto have length_rho: "length rho = j" using valid_before by auto have lookup_s: "∧q q' tstp. mmap_lookup s q = Some (q', tstp) ==> steps step rho q (i, j) = q' ∧ tstp = sup_acc step accept rho q i j" using valid_before Mapping_keys_intro by (auto simp: valid_s_def) (smt case_prodD option.simps(5))+ have init_in_keys_s: "init ∈ mmap_keys s" using valid_before by (auto simp add: valid_s_def) thenhave run_init_i_j: "steps step rho init (i, j) = fst (the (mmap_lookup s init))" using lookup_s by (auto dest: Mapping_keys_dest) have lookup_e: "∧q. mmap_lookup e q = sup_leadsto init step rho i j q" using valid_before by auto have lookup_e': "∧q. mmap_lookup e' q = sup_leadsto init step rho (i + 1) j q" proof - fix q show"mmap_lookup e' q = sup_leadsto init step rho (i + 1) j q" proof (cases "steps step rho init (i, j) = q") case True have"Max {l. l < Suc i ∧ steps step rho init (l, j) = steps step rho init (i, j)} = i" by (rule iffD2[OF Max_eq_iff]) auto thenhave"sup_leadsto init step rho (i + 1) j q = Some (ts_at rho i)" by (auto simp add: sup_leadsto_def True) thenshow ?thesis unfolding e'_defusing run_init_i_j tb_def by (auto simp add: mmap_lookup_update' True) next case False show ?thesis using run_init_i_j sup_leadsto_idle[OF i_lt_j False] lookup_e[of q] False by (auto simp add: e'_def mmap_lookup_update') qed qed have reach_split: "{q. ∃l≤i + 1. steps step rho init (l, i + 1) = q} = {q. ∃l≤i. steps step rho init (l, i + 1) = q} ∪ {init}" using le_Suc_eq by auto have valid_s_i: "valid_s init step st accept rho i i j s" using valid_before by auto have valid_s'_Suc_i: "valid_s init step st' accept rho i (i + 1) j s'" using valid_adv_d[OF valid_s_i order.refl i_lt_j, OF tb_def(6) s'_def] unfolding s'_def . have loop: "loop_inv init step accept args t0 sub rho i j tj sj (st_cur, ac_cur, i_cur, ti_cur, si_cur, q_cur, s_cur, tstp_cur) ∧ ¬loop_cond j (st_cur, ac_cur, i_cur, ti_cur, si_cur, q_cur, s_cur, tstp_cur)" unfolding loop_def proof (rule while_rule_lemma[of "loop_inv init step accept args t0 sub rho i j tj sj" "loop_cond j""loop_body step accept run_t run_sub" "λs. loop_inv init step accept args t0 sub rho i j tj sj s ∧¬ loop_cond j s"]) show"loop_inv init step accept args t0 sub rho i j tj sj (st', ac, Suc i, ti', si', init, s', None)" unfolding loop_inv_def using i_lt_j valid_s'_Suc_i sup_acc_same[of step accept rho]
length_rho reaches_on_si' reaches_on_ti' tb_def(3,4) valid_before(4) by (auto simp: run_t_def run_sub_def split: prod.splits) next have"{(t, s). loop_inv init step accept args t0 sub rho i j tj sj s ∧ loop_cond j s ∧ t = loop_body step accept run_t run_sub s} ⊆ measure (λ(st, ac, i_cur, ti, si, q, s, tstp). j - i_cur)" unfolding loop_inv_def loop_cond_def loop_body_def apply (auto simp: run_t_def run_sub_def split: option.splits) apply (metis drop_eq_Nil length_map not_less option.distinct(1) reaches_on.simps) apply (metis (no_types, lifting) drop_eq_Nil length_map not_less option.distinct(1)
reaches_on.simps) apply (auto split: prod.splits) done thenshow"wf {(t, s). loop_inv init step accept args t0 sub rho i j tj sj s ∧ loop_cond j s ∧ t = loop_body step accept run_t run_sub s}" using wf_measure wf_subset by auto next fix state assume assms: "loop_inv init step accept args t0 sub rho i j tj sj state" "loop_cond j state" obtain st_cur ac_cur i_cur ti_cur si_cur q_cur s_cur tstp_cur where state_def: "state = (st_cur, ac_cur, i_cur, ti_cur, si_cur, q_cur, s_cur, tstp_cur)" by (cases state) auto obtain ti'_cur si'_cur t_cur b_cur where tb_cur_def: "run_t ti_cur = Some (ti'_cur, t_cur)" "run_sub si_cur = Some (si'_cur, b_cur)" "reaches_on run_t ti'_cur (drop (Suc i_cur) (map fst rho)) tj" "reaches_on run_sub si'_cur (drop (Suc i_cur) (map snd rho)) sj" "t_cur = ts_at rho i_cur""b_cur = bs_at rho i_cur" using assms unfolding loop_inv_def loop_cond_def state_def apply (auto simp: ts_at_def bs_at_def run_t_def[symmetric] run_sub_def[symmetric]
elim!: reaches_on.cases[of run_t ti_cur "drop i_cur (map fst rho)" tj]
reaches_on.cases[of run_sub si_cur "drop i_cur (map snd rho)" sj]) by (metis Cons_nth_drop_Suc length_map list.inject nth_map) obtain s'_cur st'_cur where s'_cur_def: "adv_d step st_cur i_cur b_cur s_cur = (s'_cur, st'_cur)" by fastforce have valid_s'_cur: "valid_s init step st'_cur accept rho i (i_cur + 1) j s'_cur" using assms valid_adv_d[of init step st_cur accept rho] tb_cur_def(6) s'_cur_def unfolding loop_inv_def loop_cond_def state_def by auto obtain q' st''_cur where q'_def: "cstep step st'_cur q_cur b_cur = (q', st''_cur)" by fastforce obtain β ac'_cur where b_def: "cac accept ac_cur q' = (β, ac'_cur)" by fastforce have step: "q' = step q_cur b_cur""∧q bs. case Mapping.lookup st''_cur (q, bs) of None ==> True | Some v ==> step q bs = v" using valid_s'_cur q'_def unfolding valid_s_def by (auto simp: cstep_def Let_def Mapping.lookup_update' split: option.splits if_splits) have accept: "β = accept q'""∧q. case Mapping.lookup ac'_cur q of None ==> True | Some v ==> accept q = v" using assms b_def unfolding loop_inv_def state_def by (auto simp: cac_def Let_def Mapping.lookup_update' split: option.splits if_splits) have steps_q': "steps step rho init (i + 1, Suc i_cur) = q'" using assms unfolding loop_inv_def state_def by auto (metis local.step(1) steps_appE tb_cur_def(6)) have b_acc: "β = acc step accept rho init (i + 1, Suc i_cur)" unfolding accept(1) acc_def steps_q' by (auto simp: tb_cur_def) have valid_s''_cur: "valid_s init step st''_cur accept rho i (i_cur + 1) j s'_cur" using valid_s'_cur step(2) unfolding valid_s_def by auto have reaches_on_si': "reaches_on run_sub sub (take (Suc i_cur) (map snd rho)) si'_cur" using assms unfolding loop_inv_def loop_cond_def state_def by (auto simp: run_sub_def sub_def bs_at_def take_Suc_conv_app_nth reaches_on_app
tb_cur_def(2,4,6))
(metis bs_at_def reaches_on_app run_sub_def tb_cur_def(2) tb_cur_def(6)) have reaches_on_ti': "reaches_on run_t t0 (take (Suc i_cur) (map fst rho)) ti'_cur" using assms unfolding loop_inv_def loop_cond_def state_def by (auto simp: run_t_def ts_at_def take_Suc_conv_app_nth reaches_on_app tb_cur_def(1,3,5))
(metis reaches_on_app run_t_def tb_cur_def(1) tb_cur_def(5) ts_at_def) have"reach_window args t0 sub rho (Suc i_cur, ti'_cur, si'_cur, j, tj, sj)" using reaches_on_si' reaches_on_ti' tb_cur_def(3,4) length_rho assms(2) unfolding loop_cond_def state_def by (auto simp: run_t_def run_sub_def) moreoverhave"steps step rho init (i + 1, Suc i_cur) = q'" using assms steps_app unfolding loop_inv_def state_def step(1) by (auto simp: tb_cur_def(6)) ultimatelyshow"loop_inv init step accept args t0 sub rho i j tj sj (loop_body step accept run_t run_sub state)" using assms accept(2) valid_s''_cur sup_acc_ext[of _ _ step accept rho]
sup_acc_ext_idle[of _ _ step accept rho] unfolding loop_inv_def loop_body_def state_def by (auto simp: tb_cur_def(1,2,5) s'_cur_def q'_def b_def b_acc
split: option.splits prod.splits) qed auto have valid_stac_cur: "∀q bs. case Mapping.lookup st_cur (q, bs) of None ==> True | Some v ==> step q bs = v""∀q. case Mapping.lookup ac_cur q of None ==> True | Some v ==> accept q = v" using loop unfolding loop_inv_def valid_s_def by auto have valid_s'': "valid_s init step st_cur accept rho (i + 1) (i + 1) j s''" proof (cases "mmap_lookup s_cur q_cur") case None thenhave added: "steps step rho init (i + 1, j) = q_cur" "tstp_cur = sup_acc step accept rho init (i + 1) j" using loop unfolding loop_inv_def loop_cond_def by (auto dest: Mapping_keys_dest) have s''_case: "s'' = mmap_update init (q_cur, tstp_cur) s'" unfolding s''_defusing None by auto show ?thesis using valid_s'_Suc_i reach_split added mmap_update_distinct valid_stac_cur unfolding s''_case valid_s_def mmap_keys_update by (auto simp add: mmap_lookup_update' split: option.splits) next case (Some p) obtain q' tstp' where p_def: "p = (q', tstp')" by (cases p) auto note lookup_s_cur = Some[unfolded p_def] have i_cur_in: "i + 1 ≤ i_cur""i_cur ≤ j" using loop unfolding loop_inv_def by auto have q_cur_def: "steps step rho init (i + 1, i_cur) = q_cur" using loop unfolding loop_inv_def by auto have valid_s_cur: "valid_s init step st_cur accept rho i i_cur j s_cur" using loop unfolding loop_inv_def by auto have q'_steps: "steps step rho q_cur (i_cur, j) = q'" using Some valid_s_cur unfolding valid_s_def p_def by (auto intro: Mapping_keys_intro) (smt case_prodD option.simps(5)) have tstp_cur: "tstp_cur = sup_acc step accept rho init (i + 1) i_cur" using loop unfolding loop_inv_def by auto have tstp': "tstp' = sup_acc step accept rho q_cur i_cur j" using loop Some unfolding loop_inv_def p_def valid_s_def by (auto intro: Mapping_keys_intro) (smt case_prodD option.simps(5)) have added: "steps step rho init (i + 1, j) = q'" using steps_comp[OF i_cur_in q_cur_def q'_steps] . show ?thesis proof (cases tstp') case None have s''_case: "s'' = mmap_update init (q', tstp_cur) s'" unfolding s''_def lookup_s_cur None by auto have tstp_cur_opt: "tstp_cur = sup_acc step accept rho init (i + 1) j" using sup_acc_comp_None[OF i_cur_in, of step accept rho init, unfolded q_cur_def,
OF tstp'[unfolded None, symmetric]] unfolding tstp_cur by auto thenshow ?thesis using valid_s'_Suc_i reach_split added mmap_update_distinct valid_stac_cur unfolding s''_case valid_s_def mmap_keys_update by (auto simp add: mmap_lookup_update' split: option.splits) next case (Some p') obtain ts tp where p'_def: "p' = (ts, tp)" by (cases p') auto have True: "tp ≥ i_cur" using sup_acc_SomeE[OF tstp'[unfolded Some p'_def, symmetric]] by auto have s''_case: "s'' = mmap_update init (q', tstp') s'" unfolding s''_def lookup_s_cur Some p'_defusing True by auto have tstp'_opt: "tstp' = sup_acc step accept rho init (i + 1) j" using sup_acc_comp_Some_ge[OF i_cur_in True
tstp'[unfolded Some p'_def q_cur_def[symmetric], symmetric]] unfolding tstp' by (auto simp: q_cur_def[symmetric]) thenshow ?thesis using valid_s'_Suc_i reach_split added mmap_update_distinct valid_stac_cur unfolding s''_case valid_s_def mmap_keys_update by (auto simp add: mmap_lookup_update' split: option.splits) qed qed have"distinct (map fst e')" using mmap_update_distinct[OF distinct_before(2), unfolded e'_def] unfolding e'_def . thenhave"valid_window args t0 sub rho (w(w_st := st_cur, w_ac := ac_cur, w_i := Suc i, w_ti := ti', w_si := si', w_s := s'', w_e := e'))" using i_lt_j lookup_e' valid_s'' length_rho tb_def(3,4) reaches_on_si' reaches_on_ti'
valid_before[unfolded step_def accept_def] valid_stac_cur(2)[unfolded accept_def] by (auto simp: valid_window_def Let_def init_def step_def accept_def run_t_def
run_sub_def st_def ac_def i_def ti_def si_def j_def tj_def sj_def s_def e_def) moreoverhave"adv_start args w = w(w_st := st_cur, w_ac := ac_cur, w_i := Suc i, w_ti := ti', w_si := si', w_s := s'', w_e := e')" unfolding adv_start_def Let_def s''_def e'_def using tb_def(1,2) s'_def i_lt_j loop_def valid_before(3) by (auto simp: valid_window_def Let_def init_def step_def accept_def run_t_def
run_sub_def st_def ac_def i_def ti_def si_def j_def tj_def sj_def s_def e_def
split: prod.splits) ultimatelyshow ?thesis by auto qed
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
