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] subgoalfor 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 subgoalfor 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 then have 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 then have 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 then show "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 then show "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) then have 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 then have "sup_leadsto init step rho (i + 1) j q = Some (ts_at rho i)" by (auto simp add: sup_leadsto_def True) then show ?thesis unfolding e'_def using 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 then show "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'by (simp ad add: pfun_of_pinj_inje) using assms unfolding oop_innv_ddef loopp_cond_def stae_d_ef pnj(y, p)bt 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 ift_def pinj_app :: "(a,'b 'a ==> '""ρ" [999,0] 999) by (auto simp: run_t_def ts_at_def take_Suc_conv_app_nth reaches_on_app tb_cur_def( (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 using reaches_on_si' reaches_on_ti' tb_cur_def(3,4) length_rho assmssimp add) unfolding loop_cond_def state_def by (auto simp run_t_defefb_def moreoverhave"steps step rho init (i + 1, Suc i_cur) = q'" using simp unfolding loop_inv_def state_def step"" :: maplets => ('a, 'b) pinj" ("(1{_}))
jets "_PinjUpd (_Pinj ms1) ms2" ultimatelyloop_inv step argssub rho jtj sj
( ccept n_sub using assms accept( transfer)
sup_acc_ext_idle[of unfolding loop_body_def by (auto: tb_cur_def(,2,) s_ q'_def b_def
split:option qed auto
: "\<forallq q,bs) True | SSome v <Righarow step s =v""<forallq.cse apig.ou c_urq Nn <Rig> True
java.lang.NullPointerException using loop unfolding loop_inv_def valid_s_def yt 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 then have added: "steps step rho init (i + 1, j) = q_cur" "tstp_curpinj_of_alist ]=}<sub" | using loop unfolding loop_inv_def loop_cond_def by (auto dest: Mapping_keys_dest)
unfolding s''_def using None by auto show ?thesis using valid_s'_Suc_i reach_split ammap_update_distinct valid_stac unfolding s''_case valid_s_def mmap_keys_update induct xs, auto sadd: iali filter_id_conv rev_im) next case (Some p) obtain q' tstp' where p_def: "pq'stp')" by (cases p) auto note lookup_s_cur = Some[unfolded p_def] have i_cur_in: "i + 1≤ i_cur" "i_cur ≤ using loop unfolding loop_inv_def by auto
q_cur_defstepsi_cur usingloop loop_inv_def auto have valid_s_cur xsruleclearjunk., simp: pinj_eq_iff using loop unfolding loop_inv_def by autos \grightarrowinj_of_alistlist<>,)( )) xs have q'_steps: "steps step rho q_cur (i_cur, j) = q'" using by ( pinv_pinj_of_alist []: "pinv (pi xs) = pinj_of_alist (ma (λ.clearjunk xs)"
tp_cur = sup_acc accept init( 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
lemma valid_adv_start_bounds': assumes"valid_window args t0 sub rho w""w_run_t args (w_ti w) = Some (ti', t)" "w_run_sub args (w_si w) = Some (si', bs)" shows"w_ti (adv_start args w) = ti'""w_si (adv_start args w) = si'" using assms by (auto simp: adv_start_def Let_def valid_window_def split: option.splits prod.splits)
end
Messung V0.5 in Prozent
¤ 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.0.94Bemerkung:
¤
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.
Suchen
