1(* 2 * Copyright 2014, NICTA 3 * 4 * This software may be distributed and modified according to the terms of 5 * the BSD 2-Clause license. Note that NO WARRANTY is provided. 6 * See "LICENSE_BSD2.txt" for details. 7 * 8 * @TAG(NICTA_BSD) 9 *) 10 11theory GraphLangLemmas 12 13imports GraphLang CommonOpsLemmas 14 15begin 16 17definition 18 get_state_function_call :: "(string \<Rightarrow> graph_function option) 19 \<Rightarrow> (next_node \<times> state \<times> string) \<Rightarrow> string option" 20where 21 "get_state_function_call Gamma x \<equiv> case x of (NextNode nn, st, fname) \<Rightarrow> 22 (case Gamma fname of Some gf \<Rightarrow> 23 (case function_graph gf nn of Some (Call _ fname' _ _) \<Rightarrow> Some fname' | _ \<Rightarrow> None) 24 | None \<Rightarrow> None) 25 | _ \<Rightarrow> None" 26 27definition 28 exec_graph_invariant :: "(string \<Rightarrow> graph_function option) \<Rightarrow> string \<Rightarrow> stack \<Rightarrow> bool" 29where 30 "exec_graph_invariant Gamma gf xs = (xs \<noteq> [] 31 \<and> (\<forall>frame \<in> set (tl xs). get_state_function_call Gamma frame \<noteq> None) 32 \<and> map (Some o snd o snd) xs = map (get_state_function_call Gamma) (tl xs) @ [Some gf])" 33 34lemma exec_graph_invariant_Cons: 35 "exec_graph_invariant Gamma fname (x # xs) = (if xs = [] then snd (snd x) = fname 36 else (get_state_function_call Gamma (hd xs) = Some (snd (snd x)) 37 \<and> exec_graph_invariant Gamma fname xs))" 38 by (cases xs, auto simp add: exec_graph_invariant_def) 39 40lemma exec_step_invariant: 41 "(stack, stack') \<in> exec_graph_step Gamma 42 \<Longrightarrow> exec_graph_invariant Gamma gf stack 43 \<Longrightarrow> exec_graph_invariant Gamma gf stack'" 44 by (auto simp: all_exec_graph_step_cases exec_graph_invariant_Cons 45 get_state_function_call_def 46 split: graph_function.split_asm) 47 48lemma exec_trace_invariant': 49 "tr \<in> exec_trace Gamma gf 50 \<Longrightarrow> (\<forall>stack. tr i = Some stack 51 \<longrightarrow> exec_graph_invariant Gamma gf stack)" 52 apply (induct i) 53 apply (clarsimp simp: exec_trace_def exec_graph_invariant_def) 54 apply (clarsimp split: next_node.split_asm list.split_asm) 55 apply (clarsimp simp: exec_trace_def nat_trace_rel_def) 56 apply (drule_tac x=i in spec, clarsimp) 57 apply (auto elim: exec_step_invariant) 58 done 59 60lemmas exec_trace_invariant = exec_trace_invariant'[rule_format] 61 62lemma exec_trace_Nil: 63 "tr \<in> exec_trace Gamma gf \<Longrightarrow> tr i \<noteq> Some []" 64 apply safe 65 apply (drule(1) exec_trace_invariant) 66 apply (simp add: exec_graph_invariant_def) 67 done 68 69lemma exec_trace_step_cases: 70 assumes exec: "tr \<in> exec_trace Gamma gf" 71 shows "((tr i = None \<and> tr (Suc i) = None)) 72 \<or> (\<exists>state. tr i = Some [state] \<and> fst state \<in> {Ret, Err} \<and> tr (Suc i) = None) 73 \<or> (tr i \<noteq> None \<and> tr (Suc i) \<noteq> None \<and> (the (tr i), the (tr (Suc i))) \<in> exec_graph_step Gamma)" 74 using exec exec_trace_Nil[OF exec] 75 apply (clarsimp simp: exec_trace_def nat_trace_rel_def continuing_def Ball_def) 76 apply (drule_tac x=i in spec)+ 77 apply (auto split: list.split_asm option.split_asm prod.split_asm next_node.split_asm)[1] 78 done 79 80definition 81 reachable_step :: "(nat \<Rightarrow> node option) \<Rightarrow> (next_node \<times> next_node) set" 82where 83 "reachable_step graph = {(s, t). (case s of NextNode i \<Rightarrow> 84 (case graph i of None \<Rightarrow> False 85 | Some (Cond l r _) \<Rightarrow> (t = l \<or> t = r) 86 | Some (Basic c _) \<Rightarrow> t = c 87 | Some (Call c _ _ _) \<Rightarrow> t = c \<or> t = Err) | _ \<Rightarrow> False)}" 88 89abbreviation 90 "reachable_step' gf \<equiv> reachable_step (function_graph gf)" 91 92lemma exec_trace_None_dom_subset: 93 "tr n = None \<Longrightarrow> tr \<in> exec_trace Gamma f 94 \<Longrightarrow> dom tr \<subseteq> {..< n}" 95 unfolding exec_trace_def 96 by (blast elim: CollectE dest: trace_None_dom_subset) 97 98lemma trace_Some_dom_superset: 99 "tr \<in> nat_trace_rel c R 100 \<Longrightarrow> tr i = Some v 101 \<Longrightarrow> {..i} \<subseteq> dom tr" 102 apply (clarsimp, rule ccontr, clarsimp) 103 apply (drule(1) trace_None_dom_subset) 104 apply auto 105 done 106 107lemma nat_trace_rel_final: 108 "tr \<in> nat_trace_rel c R 109 \<Longrightarrow> tr i = Some v 110 \<Longrightarrow> \<not> c' v 111 \<Longrightarrow> restrict_map tr {.. i} \<in> nat_trace_rel c' R" 112 apply (frule(1) trace_Some_dom_superset) 113 apply (clarsimp simp: nat_trace_rel_def restrict_map_def Suc_le_eq) 114 apply (drule_tac c="Suc n" in subsetD, auto) 115 done 116 117lemma trace_None_dom_eq: 118 "tr n = None \<Longrightarrow> tr \<in> nat_trace_rel cont R 119 \<Longrightarrow> (\<exists>n'. n' \<le> n \<and> dom tr = {..< n'})" 120 apply (cases "\<forall>i. tr i = None") 121 apply (rule_tac x=0 in exI) 122 apply (simp add: fun_eq_iff) 123 apply clarsimp 124 apply (rule_tac x="Suc (Max (dom tr))" in exI) 125 apply (drule(1) nat_trace_Max_dom_None[rotated, simplified, OF exI]) 126 apply clarsimp 127 apply (frule(1) trace_None_dom_subset) 128 apply (rule conjI) 129 apply auto[1] 130 apply (rule equalityI) 131 apply (auto simp: less_Suc_eq_le intro!: Max_ge elim: finite_subset)[1] 132 apply (clarsimp, rule ccontr, clarsimp simp: less_Suc_eq_le) 133 apply (drule(1) trace_None_dom_subset)+ 134 apply auto 135 done 136 137lemma trace_end_eq_Some: 138 "tr \<in> nat_trace_rel c R 139 \<Longrightarrow> tr i = Some v 140 \<Longrightarrow> tr (Suc i) = None 141 \<Longrightarrow> trace_end tr = Some v" 142 apply (frule(1) trace_Some_dom_superset) 143 apply (frule(1) trace_None_dom_eq) 144 apply (clarsimp simp: le_Suc_eq lessThan_Suc_atMost[symmetric]) 145 apply (simp add: trace_end_def) 146 apply (subst Max_eqI[where x=i], simp_all) 147 apply auto 148 done 149 150lemma trace_end_cut: 151 "tr \<in> nat_trace_rel c R 152 \<Longrightarrow> tr i = Some v 153 \<Longrightarrow> trace_end (restrict_map tr {.. i}) = Some v" 154 apply (frule(1) trace_Some_dom_superset) 155 apply (simp add: trace_end_def Int_absorb1) 156 apply (subst Max_eqI[where x=i], simp_all) 157 apply (simp add: restrict_map_def) 158 apply (metis Suc_n_not_le_n) 159 done 160 161definition 162 trace_drop_n :: "nat \<Rightarrow> nat \<Rightarrow> trace \<Rightarrow> trace" 163where 164 "trace_drop_n start n_drop tr = (\<lambda>i. if (\<forall>j < i. tr (start + j) \<noteq> None 165 \<and> continuing (rev (drop n_drop (rev (the (tr (start + j))))))) 166 then option_map (rev o drop n_drop o rev) (tr (i + start)) else None)" 167 168lemma rev_drop_step: 169 "(stack, stack') \<in> exec_graph_step Gamma 170 \<Longrightarrow> continuing (rev (drop k (rev stack))) 171 \<Longrightarrow> (rev (drop k (rev stack)), rev (drop k (rev stack'))) \<in> exec_graph_step Gamma" 172 apply (subgoal_tac "\<exists>xs ys. stack = xs @ ys \<and> k = length ys") 173 apply clarsimp 174 apply (frule(1) exec_graph_step_stack_extend[THEN iffD1]) 175 apply clarsimp 176 apply (rule_tac x="take (length stack - k) stack" in exI) 177 apply (rule_tac x="drop (length stack - k) stack" in exI) 178 apply (cases "length (rev (drop k (rev stack)))") 179 apply simp 180 apply simp 181 done 182 183lemma rev_drop_continuing: 184 "continuing (rev (drop k (rev stack))) \<Longrightarrow> continuing stack" 185 by (simp add: continuing_def split: list.split next_node.split, 186 auto simp: drop_Cons split: nat.split_asm) 187 188lemma all_less_Suc_eq: 189 "(\<forall>x < Suc i. P x) = (P i \<and> (\<forall>x < i. P x))" 190 by (auto simp: less_Suc_eq) 191 192lemma exec_trace_drop_n_Cons: 193 assumes tr: "tr \<in> exec_trace Gamma fn" "Gamma fn'' = Some gf" 194 shows "tr i = Some ((NextNode n, st, fn'') # xs) 195 \<Longrightarrow> function_graph gf n = Some (Call nn fn' inps outps) 196 \<Longrightarrow> Gamma fn' = Some gf' 197 \<Longrightarrow> trace_drop_n (Suc i) (Suc (length xs)) tr \<in> exec_trace Gamma fn'" 198 using tr 199 apply (clarsimp simp: exec_trace_def) 200 apply (intro conjI) 201 apply (simp add: trace_drop_n_def) 202 apply (cut_tac exec_trace_step_cases[where i=i, OF tr(1)]) 203 apply (clarsimp simp: all_exec_graph_step_cases exec_graph_invariant_Cons 204 split: graph_function.split_asm) 205 apply (clarsimp simp: nat_trace_rel_def trace_drop_n_def 206 all_less_Suc_eq 207 split del: if_split) 208 apply (cut_tac i="Suc i + na" in exec_trace_Nil[OF tr(1)]) 209 apply (drule_tac x="Suc i + na" in spec)+ 210 apply (clarsimp simp: field_simps) 211 apply (safe, simp_all) 212 apply (safe intro!: rev_drop_step) 213 apply (auto dest!: rev_drop_continuing) 214 done 215 216lemma exec_trace_drop_n: 217 assumes tr: "tr \<in> exec_trace Gamma fn" "Gamma fn = Some gf" 218 shows "tr i = Some [(NextNode n, st, fn'')] 219 \<Longrightarrow> function_graph gf n = Some (Call nn fn' inps outps) 220 \<Longrightarrow> Gamma fn' = Some gf' 221 \<Longrightarrow> trace_drop_n (Suc i) 1 tr \<in> exec_trace Gamma fn'" 222 apply (frule exec_trace_invariant[OF tr(1)]) 223 apply (simp add: exec_graph_invariant_Cons) 224 apply (drule(2) exec_trace_drop_n_Cons[OF tr]) 225 apply simp 226 done 227 228lemma exec_trace_drop_n_rest_Cons: 229 "tr \<in> exec_trace Gamma fn 230 \<Longrightarrow> tr i = Some ((NextNode n, st, fn'') # xs) 231 \<Longrightarrow> Gamma fn'' = Some gf 232 \<Longrightarrow> function_graph gf n = Some (Call nn fn' inps outps) 233 \<Longrightarrow> Gamma fn' = Some gf' 234 \<Longrightarrow> (\<forall>stk. trace_drop_n (Suc i) (Suc (length xs)) tr k = Some stk 235 \<longrightarrow> tr (Suc i + k) = Some (stk @ (NextNode n, st, fn'') # xs))" 236proof (induct k) 237 case 0 show ?case using 0 238 apply (clarsimp simp: trace_drop_n_def) 239 apply (frule_tac i=i in exec_trace_step_cases) 240 apply (clarsimp simp: exec_graph_step_def exec_graph_invariant_Cons 241 split: graph_function.split_asm) 242 done 243next 244 case (Suc k) 245 have rev_drop_eq: "\<And>xs ys n. length ys = n 246 \<Longrightarrow> (xs = rev (drop n (rev xs)) @ ys) 247 = (\<exists>zs. xs = zs @ ys)" 248 by auto 249 show ?case using Suc.prems Suc.hyps 250 apply (clarsimp simp: trace_drop_n_def field_simps) 251 apply (frule_tac i="Suc k + i" in exec_trace_step_cases) 252 apply (clarsimp simp: field_simps all_less_Suc_eq rev_drop_eq) 253 apply (clarsimp simp: exec_graph_step_stack_extend) 254 done 255qed 256 257lemma exec_trace_drop_n_rest: 258 "tr \<in> exec_trace Gamma fn \<Longrightarrow> Gamma fn = Some gf 259 \<Longrightarrow> tr i = Some [(NextNode n, st, fn'')] 260 \<Longrightarrow> function_graph gf n = Some (Call nn fn' inps outps) 261 \<Longrightarrow> Gamma fn' = Some gf' 262 \<Longrightarrow> (\<forall>stk. trace_drop_n (Suc i) 1 tr k = Some stk 263 \<longrightarrow> tr (Suc i + k) = Some (stk @ [(NextNode n, st, fn'')]))" 264 apply (frule(1) exec_trace_invariant) 265 apply (clarsimp simp: exec_graph_invariant_Cons) 266 apply (drule(4) exec_trace_drop_n_rest_Cons) 267 apply auto 268 done 269 270lemma trace_drop_n_init: 271 "tr \<in> exec_trace Gamma fn \<Longrightarrow> Gamma fn = Some f 272 \<Longrightarrow> function_graph f n = Some (Call nn fname inputs outputs) 273 \<Longrightarrow> Gamma fname = Some f' 274 \<Longrightarrow> tr i = Some [(NextNode n, st, fn')] 275 \<Longrightarrow> trace_drop_n (Suc i) 1 tr 0 = Some [(NextNode (entry_point f'), 276 init_vars (function_inputs f') inputs st, fname)]" 277 apply (frule(1) exec_trace_invariant) 278 apply (clarsimp simp: exec_graph_invariant_Cons) 279 apply (frule_tac i=i in exec_trace_step_cases, clarsimp) 280 apply (clarsimp simp: all_exec_graph_step_cases trace_drop_n_def) 281 done 282 283lemma exec_trace_init: 284 "tr \<in> exec_trace Gamma fn 285 \<Longrightarrow> \<exists>st gf. Gamma fn = Some gf \<and> tr 0 = Some [(NextNode (entry_point gf), st, fn)]" 286 by (clarsimp simp: exec_trace_def) 287 288lemma dom_Max_None: 289 "tr \<in> exec_trace Gamma f \<Longrightarrow> (tr (Max (dom tr)) \<noteq> None)" 290 apply (rule notI) 291 apply (frule(1) exec_trace_None_dom_subset) 292 apply (cases "dom tr = {}") 293 apply (clarsimp dest!: exec_trace_init) 294 apply (drule Max_in[rotated]) 295 apply (simp add: finite_subset) 296 apply clarsimp 297 done 298 299lemma trace_end_trace_drop_n_None: 300 "trace_end (trace_drop_n i j tr) = None \<Longrightarrow> tr \<in> exec_trace Gamma f 301 \<Longrightarrow> trace_drop_n i j tr \<in> exec_trace Gamma f' 302 \<Longrightarrow> trace_end tr = None" 303 apply (clarsimp simp: trace_end_def dom_Max_None split: if_split_asm) 304 apply (rule ccontr, simp) 305 apply (drule(1) exec_trace_None_dom_subset) 306 apply (drule_tac x="n + i + 1" in spec) 307 apply (clarsimp simp: trace_drop_n_def split: if_split_asm) 308 apply auto[1] 309 done 310 311lemma trace_end_trace_drop_n_Some: 312 "trace_end (trace_drop_n (Suc i) (Suc 0) tr) = Some [(Ret, st', dontcare)] 313 \<Longrightarrow> tr \<in> exec_trace Gamma fn \<Longrightarrow> Gamma fn = Some f 314 \<Longrightarrow> function_graph f n = Some (Call nn fname inputs outputs) 315 \<Longrightarrow> Gamma fname = Some f' 316 \<Longrightarrow> tr i = Some [(NextNode n, st, fn')] 317 \<Longrightarrow> \<exists>j. tr (Suc i + j) = Some [(nn, return_vars (function_outputs f') outputs st' st, fn)] 318" 319 apply (frule(4) exec_trace_drop_n) 320 apply (drule trace_end_SomeD, fastforce simp add: exec_trace_def) 321 apply clarsimp 322 apply (frule(4) exec_trace_drop_n_rest, simp, drule spec, drule(1) mp) 323 apply simp 324 apply (frule(1) exec_trace_invariant[where stack="[a, b]" for a b]) 325 apply (clarsimp simp: exec_graph_invariant_Cons get_state_function_call_def) 326 apply (frule_tac i="Suc i + na" in exec_trace_step_cases, clarsimp) 327 apply (clarsimp simp: all_exec_graph_step_cases) 328 apply (metis add_Suc_right) 329 done 330 331end 332