1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory GraphProof 8imports TailrecPre GraphLangLemmas "Lib.SplitRule" 9begin 10 11declare sep_false_def[symmetric, simp del] 12 13lemma exec_graph_step_Gamma_deterministic: 14 assumes stacks: "(stack, stack') \<in> exec_graph_step Gamma" 15 "(stack, stack'') \<in> exec_graph_step (adds ++ Gamma)" 16 and adds: "\<forall>gf \<in> ran Gamma. \<forall>nn fname inps outps. 17 (Call nn fname inps outps) \<in> ran (function_graph gf) \<longrightarrow> fname \<notin> dom adds" 18 shows "stack'' = stack'" 19proof - 20 have adds': "\<And>fname fn fname' fn'. adds fname = Some fn \<Longrightarrow> Gamma fname' = Some fn' 21 \<Longrightarrow> \<forall>x nn inps outps. function_graph fn' x \<noteq> Some (Call nn fname inps outps)" 22 using adds 23 by (metis ranI domI) 24 show ?thesis using stacks 25 by (auto simp: all_exec_graph_step_cases 26 split: graph_function.split_asm dest: adds') 27qed 28 29lemmas exec_graph_step_deterministic 30 = exec_graph_step_Gamma_deterministic[where adds=Map.empty, simplified] 31 32lemma exec_graph_n_Gamma_deterministic: 33 "(stack, stack') \<in> exec_graph_n Gamma n 34 \<Longrightarrow> (stack, stack'') \<in> exec_graph_n (adds ++ Gamma) n 35 \<Longrightarrow> \<forall>gf \<in> ran Gamma. \<forall>nn fname inps outps. 36 (Call nn fname inps outps) \<in> ran (function_graph gf) \<longrightarrow> fname \<notin> dom adds 37 \<Longrightarrow> stack'' = stack'" 38 using exec_graph_step_Gamma_deterministic 39 apply (induct n arbitrary: stack' stack'', simp_all add: exec_graph_n_def) 40 apply blast 41 done 42 43lemmas exec_graph_n_deterministic 44 = exec_graph_n_Gamma_deterministic[where adds=Map.empty, simplified] 45 46lemma step_implies_continuing: 47 "(stack, stack') \<in> exec_graph_step Gamma 48 \<Longrightarrow> continuing stack" 49 by (simp add: exec_graph_step_def continuing_def 50 split: list.split_asm prod.split_asm next_node.split_asm) 51 52lemma exec_trace_Gamma_deterministic: 53 "trace \<in> exec_trace Gamma f 54 \<Longrightarrow> trace' \<in> exec_trace (adds ++ Gamma) f 55 \<Longrightarrow> \<forall>gf \<in> ran Gamma. \<forall>nn fname inps outps. 56 (Call nn fname inps outps) \<in> ran (function_graph gf) \<longrightarrow> fname \<notin> dom adds 57 \<Longrightarrow> trace 0 = trace' 0 58 \<Longrightarrow> trace n = trace' n" 59 apply (induct n) 60 apply simp 61 apply (clarsimp simp: exec_trace_def nat_trace_rel_def) 62 apply (drule_tac x=n in spec)+ 63 apply (case_tac "trace' n", clarsimp+) 64 apply (case_tac "trace (Suc n)", simp_all) 65 apply (auto dest: step_implies_continuing)[1] 66 apply (clarsimp simp: step_implies_continuing) 67 apply (metis exec_graph_step_Gamma_deterministic) 68 done 69 70lemmas exec_trace_deterministic 71 = exec_trace_Gamma_deterministic[where adds=Map.empty, simplified] 72 73lemma exec_trace_nat_trace: 74 "tr \<in> exec_trace Gamma f \<Longrightarrow> tr \<in> nat_trace_rel continuing (exec_graph_step Gamma)" 75 by (clarsimp simp add: exec_trace_def) 76 77abbreviation(input) 78 "exec_double_trace Gamma1 f1 Gamma2 f2 trace1 trace2 79 \<equiv> (trace1 \<in> exec_trace Gamma1 f1 \<and> trace2 \<in> exec_trace Gamma2 f2)" 80 81definition 82 trace_refine :: "bool \<Rightarrow> (state \<Rightarrow> state \<Rightarrow> bool) \<Rightarrow> trace \<Rightarrow> trace \<Rightarrow> bool" 83where 84 "trace_refine precise rel tr tr' = (case (trace_end tr, trace_end tr') of 85 (None, None) \<Rightarrow> True 86 | (_, None) \<Rightarrow> \<not> precise 87 | (_, Some [(Err, _, _)]) \<Rightarrow> True 88 | (Some [(Ret, st, _)], Some [(Ret, st', _)]) \<Rightarrow> rel st st' 89 | _ \<Rightarrow> False)" 90 91definition 92 "switch_val f x y = (\<lambda>z. if f z then y z else x z)" 93 94definition 95 "tuple_switch vs = switch_val id (\<lambda>_. fst vs) (\<lambda>_. snd vs)" 96 97lemma tuple_switch_simps[simp]: 98 "tuple_switch vs True = snd vs" 99 "tuple_switch vs False = fst vs" 100 by (auto simp: tuple_switch_def switch_val_def) 101 102definition 103 "function_outputs_st f st = acc_vars (function_outputs f) st" 104 105definition 106 trace_refine2 :: "bool \<Rightarrow> graph_function \<times> graph_function 107 \<Rightarrow> ((bool \<times> bool \<Rightarrow> variable list) \<Rightarrow> bool) \<Rightarrow> trace \<Rightarrow> trace \<Rightarrow> bool" 108where 109 "trace_refine2 precise gfs orel tr tr' = trace_refine precise (\<lambda>st st'. 110 orel (switch_val fst 111 (tuple_switch (acc_vars (function_inputs (fst gfs)) (fst (snd (hd (the (tr 0))))), 112 function_outputs_st (fst gfs) st) o snd) 113 (tuple_switch (acc_vars (function_inputs (snd gfs)) (fst (snd (hd (the (tr' 0))))), 114 function_outputs_st (snd gfs) st') o snd) 115 )) tr tr'" 116 117definition 118 graph_function_refine :: "bool \<Rightarrow> (string \<Rightarrow> graph_function option) \<Rightarrow> string 119 \<Rightarrow> (string \<Rightarrow> graph_function option) \<Rightarrow> string 120 \<Rightarrow> ((bool \<Rightarrow> variable list) \<Rightarrow> bool) 121 \<Rightarrow> ((bool \<times> bool \<Rightarrow> variable list) \<Rightarrow> bool) 122 \<Rightarrow> bool" 123where 124 "graph_function_refine precise Gamma1 f1 Gamma2 f2 irel orel 125 = (\<forall>xs ys tr tr' gf gf'. tr \<in> exec_trace Gamma1 f1 \<and> tr' \<in> exec_trace Gamma2 f2 126 \<and> Gamma1 f1 = Some gf \<and> tr 0 = Some [init_state f1 gf xs] 127 \<and> Gamma2 f2 = Some gf' \<and> tr' 0 = Some [init_state f2 gf' ys] 128 \<and> length xs = length (function_inputs gf) \<and> length ys = length (function_inputs gf') 129 \<and> irel (tuple_switch (xs, ys)) 130 \<longrightarrow> trace_refine precise (\<lambda>st st'. orel (switch_val fst 131 (tuple_switch (xs, function_outputs_st gf st) o snd) 132 (tuple_switch (ys, function_outputs_st gf' st') o snd) 133 )) tr tr')" 134 135lemma graph_function_refine_trace: 136 "graph_function_refine prec Gamma1 f1 Gamma2 f2 irel orel 137 = (\<forall>tr tr' xs ys gf gf'. exec_double_trace Gamma1 f1 Gamma2 f2 tr tr' 138 \<and> tr 0 \<noteq> None \<and> tr' 0 \<noteq> None \<and> Gamma1 f1 = Some gf \<and> Gamma2 f2 = Some gf' 139 \<and> the (tr 0) = [init_state f1 gf xs] \<and> the (tr' 0) = [init_state f2 gf' ys] 140 \<and> length xs = length (function_inputs gf) \<and> length ys = length (function_inputs gf') 141 \<and> irel (tuple_switch (xs, ys)) 142 \<longrightarrow> trace_refine prec (\<lambda>st st'. orel (switch_val fst 143 (tuple_switch (xs, function_outputs_st gf st) o snd) 144 (tuple_switch (ys, function_outputs_st gf' st') o snd) 145 )) tr tr')" 146 apply (clarsimp simp: graph_function_refine_def) 147 apply (simp only: ex_simps[symmetric] all_simps[symmetric] 148 cong: conj_cong) 149 apply auto 150 done 151 152definition 153 trace_addr :: "trace \<Rightarrow> nat \<Rightarrow> next_node option" 154where 155 "trace_addr tr n = (case tr n of Some [(nn, _, _)] \<Rightarrow> Some nn | _ \<Rightarrow> None)" 156 157lemma trace_addr_SomeD: 158 "trace_addr tr n = Some nn \<Longrightarrow> \<exists>st g. tr n = Some [(nn, st, g)]" 159 by (simp add: trace_addr_def split: option.split_asm list.split_asm prod.split_asm) 160 161lemma trace_addr_SomeI: 162 "\<exists>x. tr n = Some [(nn, x)] \<Longrightarrow> trace_addr tr n = Some nn" 163 by (clarsimp simp add: trace_addr_def) 164 165type_synonym restrs = "nat \<Rightarrow> nat set" 166 167definition 168 restrs_condition :: "trace \<Rightarrow> restrs \<Rightarrow> nat \<Rightarrow> bool" 169where 170 "restrs_condition tr restrs n = (\<forall>m. card {i. i < n \<and> trace_addr tr i = Some (NextNode m)} \<in> restrs m)" 171 172definition 173 succ_restrs :: "next_node \<Rightarrow> restrs \<Rightarrow> restrs" 174where 175 "succ_restrs nn rs = (case nn of NextNode n \<Rightarrow> rs (n := {x. x - 1 \<in> rs n}) | _ \<Rightarrow> rs)" 176 177abbreviation 178 "succ_restrs' n \<equiv> succ_restrs (NextNode n)" 179 180definition 181 pred_restrs :: "next_node \<Rightarrow> restrs \<Rightarrow> restrs" 182where 183 "pred_restrs nn rs = (case nn of NextNode n \<Rightarrow> rs (n := {x. Suc x \<in> rs n}) | _ \<Rightarrow> rs)" 184 185abbreviation 186 "pred_restrs' n \<equiv> pred_restrs (NextNode n)" 187 188definition 189 trace_bottom_addr :: "trace \<Rightarrow> nat \<Rightarrow> next_node option" 190where 191 "trace_bottom_addr tr n = (case tr n of Some [] \<Rightarrow> None 192 | Some xs \<Rightarrow> Some (fst (List.last xs)) | None \<Rightarrow> None)" 193 194definition 195 double_trace_imp :: "(trace \<times> trace \<Rightarrow> bool) \<Rightarrow> (trace \<times> trace \<Rightarrow> bool) 196 \<Rightarrow> (trace \<times> trace \<Rightarrow> bool)" 197where "double_trace_imp P Q = (\<lambda>(tr, tr'). P (tr, tr') \<longrightarrow> Q (tr, tr'))" 198 199type_synonym visit_addr = "bool \<times> next_node \<times> restrs" 200 201definition 202 restrs_eventually_condition :: "trace \<Rightarrow> restrs \<Rightarrow> bool" 203where 204 "restrs_eventually_condition tr restrs = (\<exists>n. tr n \<noteq> None 205 \<and> (\<forall>m \<ge> n. restrs_condition tr restrs m))" 206 207definition 208 visit :: "trace \<Rightarrow> next_node \<Rightarrow> restrs \<Rightarrow> state option" 209where 210 "visit tr n restrs = (if \<exists>i. restrs_condition tr restrs i \<and> trace_addr tr i = Some n 211 then Some (fst (snd (hd (the (tr (LEAST i. restrs_condition tr restrs i \<and> trace_addr tr i = Some n)))))) 212 else None)" 213 214definition 215 pc :: "next_node \<Rightarrow> restrs \<Rightarrow> trace \<Rightarrow> bool" 216where 217 "pc n restrs tr = (visit tr n restrs \<noteq> None)" 218 219abbreviation 220 "pc' n \<equiv> pc (NextNode n)" 221 222definition 223 double_visit :: "visit_addr \<Rightarrow> trace \<times> trace \<Rightarrow> state option" 224where 225 "double_visit = (\<lambda>(side, nn, restrs) (tr, tr'). 226 visit (if side then tr' else tr) nn restrs)" 227 228definition 229 double_pc :: "visit_addr \<Rightarrow> trace \<times> trace \<Rightarrow> bool" 230where 231 "double_pc = (\<lambda>(side, nn, restrs) (tr, tr'). 232 (visit (if side then tr' else tr) nn restrs) \<noteq> None)" 233 234definition 235 related_pair :: "visit_addr \<Rightarrow> (state \<Rightarrow> 'a) 236 \<Rightarrow> visit_addr \<Rightarrow> (state \<Rightarrow> 'b) 237 \<Rightarrow> ('a \<times> 'b \<Rightarrow> bool) 238 \<Rightarrow> (trace \<times> trace) \<Rightarrow> bool" 239where 240 "related_pair v1 expr1 v2 expr2 rel trs 241 = rel (expr1 (the (double_visit v1 trs)), expr2 (the (double_visit v2 trs)))" 242 243abbreviation 244 "equals v1 expr1 v2 expr2 245 \<equiv> related_pair v1 expr1 v2 expr2 (split (=))" 246 247abbreviation 248 "equals' n1 restrs1 expr1 n2 restrs2 expr2 249 \<equiv> equals (False, NextNode n1, restrs1) expr1 (True, NextNode n2, restrs2) expr2" 250 251definition 252 restr_trace_refine :: "bool \<Rightarrow> (string \<Rightarrow> graph_function option) \<Rightarrow> string 253 \<Rightarrow> (string \<Rightarrow> graph_function option) \<Rightarrow> string 254 \<Rightarrow> restrs \<Rightarrow> restrs 255 \<Rightarrow> ((bool \<times> bool \<Rightarrow> variable list) \<Rightarrow> bool) \<Rightarrow> trace \<Rightarrow> trace \<Rightarrow> bool" 256where 257 "restr_trace_refine precise Gamma1 f1 Gamma2 f2 restrs1 restrs2 orel 258 tr tr' = (\<forall>gf gf'. exec_double_trace Gamma1 f1 Gamma2 f2 tr tr' 259 \<and> Gamma1 f1 = Some gf \<and> Gamma2 f2 = Some gf' 260 \<and> (\<exists>xs. the (tr 0) = [init_state f1 gf xs] 261 \<and> length xs = length (function_inputs gf)) 262 \<and> (\<exists>ys. the (tr' 0) = [init_state f2 gf' ys] 263 \<and> length ys = length (function_inputs gf')) 264 \<and> restrs_eventually_condition tr restrs1 265 \<and> restrs_eventually_condition tr' restrs2 266 \<longrightarrow> trace_refine2 precise (gf, gf') orel tr tr')" 267 268definition 269 restrs_list :: "(nat \<times> nat list) list \<Rightarrow> restrs" 270where 271 "restrs_list rs = (\<lambda>i. fold (\<lambda>(n, xs) S. 272 if i = n then set xs \<inter> S else S) rs UNIV)" 273 274definition 275 fill_in_below :: "nat list \<Rightarrow> nat list" 276where 277 "fill_in_below xs = [0 ..< fold max (map Suc xs) 0]" 278 279definition 280 restrs_visit :: "(nat \<times> nat list) list 281 \<Rightarrow> next_node \<Rightarrow> graph_function 282 \<Rightarrow> (nat \<times> nat list) list" 283where 284 "restrs_visit xs nn gf = map (\<lambda>(m, xsf). if (nn, NextNode m) \<in> rtrancl (reachable_step' gf) 285 then (m, (fill_in_below xsf)) else (m, xsf)) xs" 286 287definition 288 eqs :: "(('a \<times> (variable list \<Rightarrow> variable)) \<times> ('a \<times> (variable list \<Rightarrow> variable))) list 289 \<Rightarrow> ('a \<Rightarrow> nat option) \<Rightarrow> ('a \<Rightarrow> variable list) \<Rightarrow> bool" 290where 291 "eqs xs lens vs = ((\<forall>((laddr, lval), (raddr, rval)) \<in> set xs. lval (vs laddr) = rval (vs raddr)) 292 \<and> (\<forall>addr. lens addr \<noteq> None \<longrightarrow> length (vs addr) = the (lens addr)))" 293 294definition 295 visit_restrs_preds_raw :: "next_node \<Rightarrow> restrs 296 \<Rightarrow> (next_node \<times> restrs) list \<Rightarrow> bool" 297where 298 "visit_restrs_preds_raw nn restrs preds = 299 (\<forall>tr i. trace_addr tr i = Some nn \<and> restrs_condition tr restrs i 300 \<longrightarrow> (\<forall>j. trace_addr tr j = Some nn \<and> restrs_condition tr restrs j \<longrightarrow> j = i) 301 \<and> (\<exists>j nn' restrs'. j < i 302 \<and> (nn', restrs') \<in> set preds \<and> trace_addr tr j = Some nn' 303 \<and> restrs_condition tr restrs' j))" 304 305definition 306 visit_restrs_preds :: "visit_addr \<Rightarrow> visit_addr list \<Rightarrow> bool" 307where 308 "visit_restrs_preds vis preds = (case vis of (side, nn, restrs) 309 \<Rightarrow> (fst ` set preds \<subseteq> {side}) 310 \<and> visit_restrs_preds_raw nn restrs (map snd preds))" 311 312lemma visit_known: 313 "tr i = Some [(nn, st, g)] 314 \<Longrightarrow> restrs_condition tr restrs i 315 \<Longrightarrow> (\<forall>j < i. trace_addr tr j = Some nn \<longrightarrow> \<not> restrs_condition tr restrs j) 316 \<Longrightarrow> visit tr nn restrs = Some st" 317 apply (clarsimp simp: visit_def) 318 apply (subst Least_equality, blast intro: trace_addr_SomeI) 319 apply (blast intro: linorder_not_le[THEN iffD1]) 320 apply (auto simp: trace_addr_SomeI) 321 done 322 323lemma fold_invariant: 324 "(\<forall>x \<in> set xs. \<forall> s. g (f x s) = g s) \<Longrightarrow> g s = v \<Longrightarrow> g (fold f xs s) = v" 325 by (induct xs arbitrary: s, simp_all) 326 327lemma var_acc_var_upd: 328 "var_acc s (var_upd s' v st) 329 = (if s = s' then v else var_acc s st)" 330 by (cases st, simp add: var_acc_def var_upd_def) 331 332lemma var_acc_save_vals_distinct: 333 "distinct xs \<Longrightarrow> length xs = length vs 334 \<Longrightarrow> map (\<lambda>i. var_acc i (save_vals xs vs st)) xs = vs" 335 apply (induct xs arbitrary: vs st) 336 apply simp 337 apply (case_tac vs, simp_all add: save_vals_def) 338 apply (rule fold_invariant) 339 apply (clarsimp simp: var_acc_var_upd elim!: in_set_zipE) 340 apply (simp add: var_acc_var_upd) 341 done 342 343definition 344 wf_graph_function :: "graph_function \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" 345where 346 "wf_graph_function f ilen olen = (case f of GraphFunction inputs outputs graph ep 347 \<Rightarrow> distinct inputs \<and> distinct outputs \<and> length inputs = ilen \<and> length outputs = olen 348 \<and> (\<forall>nn i. (nn, NextNode i) \<in> reachable_step' f \<longrightarrow> i \<in> dom graph) 349 \<and> ep \<in> dom graph)" 350 351lemma wf_graph_function_acc_vars_save_vals: 352 "\<lbrakk> wf_graph_function f ilen olen; xs = function_inputs f; length vs = ilen \<rbrakk> 353 \<Longrightarrow> acc_vars xs (save_vals xs vs st) = vs" 354 by (cases f, simp add: acc_vars_def wf_graph_function_def 355 var_acc_save_vals_distinct) 356 357lemma wf_graph_function_length_function_inputs: 358 "wf_graph_function f ilen olen \<Longrightarrow> length (function_inputs f) = ilen" 359 by (cases f, simp_all add: wf_graph_function_def) 360 361lemma graph_function_refine_trace2: 362 "Gamma1 f1 = Some gf \<Longrightarrow> wf_graph_function gf ilen1 olen1 363 \<Longrightarrow> Gamma2 f2 = Some gf' \<Longrightarrow> wf_graph_function gf' ilen2 olen2 364 \<Longrightarrow> graph_function_refine prec Gamma1 f1 Gamma2 f2 irel orel 365 = (\<forall>tr tr'. exec_double_trace Gamma1 f1 Gamma2 f2 tr tr' 366 \<and> Gamma1 f1 = Some gf \<and> Gamma2 f2 = Some gf' 367 \<and> (\<exists>xs ys. the (tr 0) = [init_state f1 gf xs] 368 \<and> length xs = length (function_inputs gf) 369 \<and> the (tr' 0) = [init_state f2 gf' ys] 370 \<and> length ys = length (function_inputs gf') 371 \<and> irel (tuple_switch (xs, ys))) 372 \<longrightarrow> trace_refine2 prec (gf, gf') orel tr tr')" 373 apply (clarsimp simp: graph_function_refine_trace trace_refine2_def) 374 apply (frule wf_graph_function_length_function_inputs[where f=gf]) 375 apply (frule wf_graph_function_length_function_inputs[where f=gf']) 376 apply (simp add: imp_conjL) 377 apply (rule arg_cong[where f=All] ext imp_cong[OF refl])+ 378 apply (clarsimp dest!: exec_trace_init) 379 apply (safe, simp_all add: init_state_def wf_graph_function_acc_vars_save_vals) 380 done 381 382lemma exec_trace_step_reachable_induct: 383 "tr \<in> exec_trace Gamma fn \<Longrightarrow> Gamma fn = Some gf 384 \<Longrightarrow> trace_bottom_addr tr (Suc i) = Some addr 385 \<Longrightarrow> (\<forall>n. trace_bottom_addr tr i = Some (NextNode n) \<longrightarrow> n \<in> dom (function_graph gf)) 386 \<longrightarrow> trace_bottom_addr tr i \<noteq> None 387 \<and> (trace_bottom_addr tr i = Some addr \<and> trace_addr tr (Suc i) = None 388 \<or> trace_addr tr (Suc i) = Some addr 389 \<and> (the (trace_bottom_addr tr i), addr) \<in> reachable_step' gf)" 390 apply (frule_tac i=i in exec_trace_invariant') 391 apply (frule_tac i=i in exec_trace_step_cases) 392 apply (simp add: all_exec_graph_step_cases, safe dest!: trace_addr_SomeD, 393 simp_all add: trace_bottom_addr_def del: last.simps) 394 apply (auto simp: exec_graph_invariant_Cons reachable_step_def 395 get_state_function_call_def 396 split: graph_function.split_asm, 397 auto split: next_node.splits option.split node.splits if_split_asm 398 simp: trace_addr_def neq_Nil_conv) 399 done 400 401lemma exec_trace_step_reachable_induct2: 402 "tr \<in> exec_trace Gamma fn \<Longrightarrow> Gamma fn = Some gf 403 \<Longrightarrow> wf_graph_function gf ilen olen 404 \<Longrightarrow> trace_bottom_addr tr (Suc i) = Some addr 405 \<Longrightarrow> (\<forall>n. trace_bottom_addr tr i = Some (NextNode n) \<longrightarrow> n \<in> dom (function_graph gf)) 406 \<and> trace_bottom_addr tr i \<noteq> None 407 \<and> (trace_bottom_addr tr i = Some addr \<and> trace_addr tr (Suc i) = None 408 \<or> trace_addr tr (Suc i) = Some addr 409 \<and> (the (trace_bottom_addr tr i), addr) \<in> reachable_step' gf)" 410 apply (induct i arbitrary: addr) 411 apply (frule(2) exec_trace_step_reachable_induct) 412 apply (clarsimp simp: exec_trace_def trace_bottom_addr_def 413 wf_graph_function_def split: graph_function.split_asm) 414 apply (frule(2) exec_trace_step_reachable_induct) 415 apply atomize 416 apply (case_tac "trace_bottom_addr tr (Suc i)", simp_all) 417 apply clarsimp 418 apply (frule_tac i=i in exec_trace_step_reachable_induct, simp) 419 apply clarsimp 420 apply (erule disjE, simp_all) 421 apply (simp add: wf_graph_function_def split: graph_function.split_asm) 422 apply auto 423 done 424 425lemma Collect_less_Suc: 426 "{i. i < Suc n \<and> P i} = {i. i < n \<and> P i} \<union> (if P n then {n} else {})" 427 by (auto simp: less_Suc_eq) 428 429lemma trace_addr_trace_bottom_addr_eq: 430 "trace_addr tr i = Some addr \<Longrightarrow> trace_bottom_addr tr i = Some addr" 431 by (clarsimp simp: trace_bottom_addr_def dest!: trace_addr_SomeD) 432 433lemma reachable_trace_induct: 434 "tr \<in> exec_trace Gamma fname \<Longrightarrow> Gamma fname = Some f 435 \<Longrightarrow> wf_graph_function f ilen olen 436 \<Longrightarrow> trace_addr tr i = Some nn 437 \<Longrightarrow> i + k \<le> j 438 \<Longrightarrow> (\<forall>nn'. trace_bottom_addr tr (i + k) = Some nn' 439 \<longrightarrow> (Some nn' \<in> trace_addr tr ` {i .. i + k}) 440 \<and> (nn, nn') \<in> rtrancl (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i ..< j}}) 441 \<and> (k \<noteq> 0 \<and> trace_addr tr (i + k) \<noteq> None 442 \<longrightarrow> (nn, nn') \<in> trancl (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i ..< j}})))" 443 apply (induct k) 444 apply (clarsimp simp: trace_bottom_addr_def dest!: trace_addr_SomeD) 445 apply clarsimp 446 apply (frule(3) exec_trace_step_reachable_induct2) 447 apply clarsimp 448 apply (subgoal_tac "i + k \<in> {i ..< j} \<and> Suc (i + k) \<in> {i .. Suc (i + k)}") 449 apply (rule conjI) 450 apply (elim disjE conjE) 451 apply simp 452 apply (blast intro: sym) 453 apply (rule conjI) 454 apply (elim disjE conjE) 455 apply simp 456 apply (erule rtrancl_into_rtrancl) 457 apply simp 458 apply clarify 459 apply (elim disjE conjE) 460 apply simp 461 apply (erule rtrancl_into_trancl1) 462 apply simp 463 apply simp 464 done 465 466lemma reachable_trace: 467 "tr \<in> exec_trace Gamma fname \<Longrightarrow> Gamma fname = Some f 468 \<Longrightarrow> wf_graph_function f ilen olen 469 \<Longrightarrow> trace_addr tr i = Some nn 470 \<Longrightarrow> trace_addr tr j = Some nn' 471 \<Longrightarrow> i < j 472 \<Longrightarrow> (nn, nn') \<in> trancl (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i ..< j}})" 473 apply (frule(3) reachable_trace_induct[where k="j - i" and j=j]) 474 apply simp 475 apply (clarsimp simp: trace_bottom_addr_def dest!: trace_addr_SomeD) 476 done 477 478lemma reachable_trace_eq: 479 "tr \<in> exec_trace Gamma fname \<Longrightarrow> Gamma fname = Some f 480 \<Longrightarrow> wf_graph_function f ilen olen 481 \<Longrightarrow> trace_addr tr i = Some nn 482 \<Longrightarrow> trace_addr tr j = Some nn' 483 \<Longrightarrow> i \<le> j 484 \<Longrightarrow> (nn, nn') \<in> rtrancl (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i ..< j}})" 485 apply (cases "i = j", simp_all) 486 apply (rule trancl_into_rtrancl) 487 apply (fastforce elim: reachable_trace) 488 done 489 490lemma restrs_single_visit_neq: 491 "tr \<in> exec_trace Gamma fname \<Longrightarrow> Gamma fname = Some f 492 \<Longrightarrow> wf_graph_function f ilen olen 493 \<Longrightarrow> trace_addr tr i = Some nn 494 \<Longrightarrow> restrs_condition tr restrs i 495 \<Longrightarrow> trace_addr tr j = Some nn 496 \<Longrightarrow> restrs_condition tr restrs j 497 \<Longrightarrow> \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}) 498 \<Longrightarrow> (nn, nn) \<notin> trancl (reachable_step' f \<inter> {(x, y). x \<notin> set cuts}) 499 \<Longrightarrow> i < j \<Longrightarrow> False" 500 apply (frule(5) reachable_trace) 501 apply (erule notE, erule trancl_mono) 502 apply clarsimp 503 apply (case_tac a, simp_all) 504 apply (drule spec, drule(1) mp, clarsimp) 505 apply (clarsimp simp: restrs_condition_def) 506 apply (drule spec, drule(1) subsetD[rotated])+ 507 apply clarsimp 508 apply (frule card_seteq[rotated -1, OF eq_imp_le], simp, clarsimp)[1] 509 apply (blast dest: linorder_not_less[THEN iffD2]) 510 apply (simp add: reachable_step_def)+ 511 done 512 513lemma restrs_single_visit: 514 "tr \<in> exec_trace Gamma fname \<Longrightarrow> Gamma fname = Some f 515 \<Longrightarrow> wf_graph_function f ilen olen 516 \<Longrightarrow> trace_addr tr i = Some nn 517 \<Longrightarrow> restrs_condition tr restrs i 518 \<Longrightarrow> trace_addr tr j = Some nn 519 \<Longrightarrow> restrs_condition tr restrs j 520 \<Longrightarrow> \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}) 521 \<Longrightarrow> (nn, nn) \<notin> trancl (reachable_step' f \<inter> {(x, y). x \<notin> set cuts}) 522 \<Longrightarrow> i = j" 523 by (metis restrs_single_visit_neq linorder_neq_iff) 524 525lemma restrs_single_visit2: 526 "trace_addr tr i = Some nn 527 \<Longrightarrow> trace_addr tr j = Some nn 528 \<Longrightarrow> tr \<in> exec_trace Gamma fname 529 \<Longrightarrow> Gamma fname = Some f 530 \<Longrightarrow> wf_graph_function f ilen olen 531 \<Longrightarrow> restrs_condition tr restrs i 532 \<Longrightarrow> restrs_condition tr restrs j 533 \<Longrightarrow> \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}) 534 \<Longrightarrow> (nn, nn) \<notin> trancl (reachable_step' f \<inter> {(x, y). x \<notin> set cuts}) 535 \<Longrightarrow> i = j" 536 by (metis restrs_single_visit) 537 538lemma not_trancl_converse_step: 539 "converse stp `` {y} \<subseteq> S 540 \<Longrightarrow> \<forall>z \<in> S. (x, z) \<notin> rtrancl (stp \<inter> constraint) 541 \<Longrightarrow> (x, y) \<notin> trancl (stp \<inter> constraint)" 542 using tranclD2 by fastforce 543 544lemma reachable_order_mono: 545 "(nn, nn') \<in> rtrancl R 546 \<Longrightarrow> (\<forall>(nn, nn') \<in> R. order nn \<le> order nn') 547 \<Longrightarrow> order nn \<le> (order nn' :: 'a :: linorder)" 548 apply (induct rule: rtrancl.induct) 549 apply simp 550 apply (blast intro: order_trans) 551 done 552 553lemma not_reachable_by_order: 554 "(\<forall>(nn, nn') \<in> R. order nn \<le> order nn') 555 \<Longrightarrow> order nn > (order nn' :: 'a :: linorder) 556 \<Longrightarrow> (nn, nn') \<notin> rtrancl R" 557 by (metis reachable_order_mono linorder_not_less) 558 559lemma Collect_less_nat: 560 "(n :: nat) - 1 = m 561 \<Longrightarrow> {i. i < n \<and> P i} = (if n = 0 then {} else {i. i < m \<and> P i} \<union> (if P m then {m} else {}))" 562 by (cases n, simp_all add: Collect_less_Suc) 563 564lemma test_restrs_condition: 565 "\<lbrakk> graph = [ 1 \<mapsto> Call (NextNode 2) ''foo'' [] [], 2 \<mapsto> Basic (NextNode 3) [], 3 \<mapsto> Basic Ret [] ]; 566 Gamma ''bar'' = Some (GraphFunction [] [] graph 1); 567 tr \<in> exec_trace Gamma ''bar''; 568 Gamma ''foo'' = Some (GraphFunction [] [] [ 1 \<mapsto> Basic Ret []] 1) \<rbrakk> 569 \<Longrightarrow> restrs_condition tr (restrs_list [(1, [1])]) 5" 570 apply (frule exec_trace_init, elim exE conjE) 571 apply (frule_tac i=0 in exec_trace_step_cases, clarsimp) 572 apply (clarsimp simp: all_exec_graph_step_cases) 573 apply (frule_tac i=1 in exec_trace_step_cases, clarsimp) 574 apply (clarsimp simp: all_exec_graph_step_cases upd_vars_def save_vals_def init_vars_def) 575 apply (frule_tac i=2 in exec_trace_step_cases, clarsimp) 576 apply (clarsimp simp: all_exec_graph_step_cases upd_vars_def save_vals_def init_vars_def TWO return_vars_def) 577 apply (frule_tac i=3 in exec_trace_step_cases, clarsimp) 578 apply (clarsimp simp: all_exec_graph_step_cases upd_vars_def save_vals_def init_vars_def) 579 apply (frule_tac i=4 in exec_trace_step_cases, clarsimp) 580 apply (clarsimp simp: all_exec_graph_step_cases upd_vars_def save_vals_def init_vars_def) 581 apply (frule_tac i=5 in exec_trace_step_cases, clarsimp) 582 apply (clarsimp simp: all_exec_graph_step_cases upd_vars_def save_vals_def init_vars_def) 583 584 apply (simp add: restrs_condition_def Collect_less_nat Collect_conv_if trace_addr_def 585 restrs_list_def) 586 done 587 588primrec 589 first_reached_prop :: "visit_addr list 590 \<Rightarrow> (visit_addr \<Rightarrow> (trace \<times> trace) \<Rightarrow> bool) 591 \<Rightarrow> (trace \<times> trace) \<Rightarrow> bool" 592where 593 "first_reached_prop [] p trs = False" 594 | "first_reached_prop (v # vs) p trs = 595 (if double_pc v trs then p v trs 596 else first_reached_prop vs p trs)" 597 598definition 599 get_function_call :: "(graph_function \<times> graph_function) 600 \<Rightarrow> visit_addr 601 \<Rightarrow> (next_node \<times> string \<times> (state \<Rightarrow> variable) list \<times> string list) option" 602where 603 "get_function_call gfs x = (case x of (side, NextNode n, restrs) 604 \<Rightarrow> (case function_graph (tuple_switch gfs side) n of 605 Some (Call nn fname inputs outputs) \<Rightarrow> Some (nn, fname, inputs, outputs) 606 | _ \<Rightarrow> None) | _ \<Rightarrow> None)" 607 608definition 609 func_inputs_match :: "(graph_function \<times> graph_function) 610 \<Rightarrow> ((bool \<Rightarrow> variable list) \<Rightarrow> bool) 611 \<Rightarrow> visit_addr \<Rightarrow> visit_addr 612 \<Rightarrow> (trace \<times> trace) \<Rightarrow> bool" 613where 614 "func_inputs_match gfs rel vis1 vis2 trs = (case (get_function_call gfs vis1, 615 get_function_call gfs vis2) of (Some (_, _, inputs1, _), Some (_, _, inputs2, _)) 616 \<Rightarrow> rel (\<lambda>x. map (\<lambda>f. f (the (double_visit (tuple_switch (vis1, vis2) x) trs))) 617 (tuple_switch (inputs1, inputs2) x)) 618 | _ \<Rightarrow> False)" 619 620definition 621 succ_visit :: "next_node \<Rightarrow> visit_addr \<Rightarrow> visit_addr" 622where 623 "succ_visit nn vis = (case vis of (side, nn', restrs) 624 \<Rightarrow> (side, nn', succ_restrs nn restrs))" 625 626lemma fst_succ_visit[simp]: 627 "fst (succ_visit nn v) = fst v" 628 by (simp add: succ_visit_def split_def split: next_node.split) 629 630lemma wf_graph_function_init_extract: 631 "\<lbrakk> wf_graph_function f ilen olen; tr \<in> exec_trace Gamma fn; Gamma fn = Some f; 632 the (tr 0) = [init_state fn f xs]; 633 \<forall>n. 0 \<in> restrs n; length xs = ilen \<rbrakk> \<Longrightarrow> 634 acc_vars (function_inputs f) (the (visit tr (NextNode (entry_point f)) restrs)) = xs" 635 apply (cases f) 636 apply (frule wf_graph_function_length_function_inputs) 637 apply (frule exec_trace_init) 638 apply (clarsimp simp: visit_known restrs_condition_def init_state_def 639 wf_graph_function_acc_vars_save_vals) 640 done 641 642lemma exec_trace_reachable_step: 643 "tr \<in> exec_trace Gamma fn \<Longrightarrow> Gamma fn = Some f 644 \<Longrightarrow> trace_addr tr (Suc i) = Some nn' 645 \<Longrightarrow> nn' \<noteq> Err 646 \<Longrightarrow> \<exists>nn. (nn, nn') \<in> reachable_step' f" 647 apply (clarsimp dest!: trace_addr_SomeD) 648 apply (frule(1) exec_trace_invariant) 649 apply (subgoal_tac "\<forall>stack. tr i = Some stack \<longrightarrow> exec_graph_invariant Gamma fn stack") 650 prefer 2 651 apply (metis exec_trace_invariant) 652 apply (frule_tac i=i in exec_trace_step_cases) 653 apply (rule_tac x="the (trace_bottom_addr tr i)" in exI) 654 apply (clarsimp simp: all_exec_graph_step_cases) 655 apply (safe, simp_all add: reachable_step_def)[1] 656 apply (auto simp: exec_graph_invariant_def trace_addr_def 657 get_state_function_call_def trace_bottom_addr_def 658 split: graph_function.split_asm next_node.split option.splits node.splits 659 next_node.split) 660 done 661 662lemma init_pc: 663 "tr \<in> exec_trace Gamma fn \<Longrightarrow> Gamma fn = Some f 664 \<Longrightarrow> tr 0 = Some [init_state fn f xs] 665 \<Longrightarrow> \<forall>n. 0 \<in> restrs n 666 \<Longrightarrow> wf_graph_function f ilen olen 667 \<Longrightarrow> pc' (entry_point f) restrs tr" 668 apply (clarsimp simp: pc_def visit_def) 669 apply (rule_tac x=0 in exI) 670 apply (simp add: trace_addr_SomeI init_state_def restrs_condition_def 671 split: graph_function.split) 672 done 673 674lemma eqs_eq_conj_len_assert: 675 "(eqs xs lens vs) = ((eqs xs lens $ vs) 676 \<and> (\<forall>addr. lens addr \<noteq> None \<longrightarrow> length (vs addr) = the (lens addr)))" 677 by (auto simp: eqs_def) 678 679lemma length_acc_vars[simp]: 680 "length (acc_vars vs st) = length vs" 681 by (simp add: acc_vars_def) 682 683lemma restrs_eventually_init: 684 "tr \<in> exec_trace Gamma fn 685 \<Longrightarrow> Gamma fn = Some f 686 \<Longrightarrow> converse (reachable_step' f) `` {NextNode (entry_point f)} \<subseteq> set [] 687 \<Longrightarrow> rs = (restrs_list [(entry_point f, [1])]) 688 \<Longrightarrow> restrs_eventually_condition tr rs" 689 apply (clarsimp simp: restrs_eventually_condition_def) 690 apply (rule_tac x=1 in exI) 691 apply (rule conjI) 692 apply (clarsimp simp: exec_trace_def nat_trace_rel_def) 693 apply (clarsimp simp: restrs_condition_def restrs_list_def) 694 apply (subst arg_cong[where f=card and y="{0}"], simp_all) 695 apply (safe, simp_all) 696 apply (case_tac x, simp_all) 697 apply (drule(2) exec_trace_reachable_step, simp) 698 apply auto[1] 699 apply (clarsimp simp: exec_trace_def trace_addr_def) 700 done 701 702lemma graph_function_restr_trace_refine: 703 assumes wfs: "wf_graph_function f1 il1 ol1" "wf_graph_function f2 il2 ol2" 704 and inps: "converse (reachable_step' f1) `` {NextNode (entry_point f1)} \<subseteq> set []" 705 "converse (reachable_step' f2) `` {NextNode (entry_point f2)} \<subseteq> set []" 706 and gfs: "Gamma1 fn1 = Some f1" "Gamma2 fn2 = Some f2" 707 notes wf_facts = wf_graph_function_init_extract 708 wf_graph_function_init_extract 709 wf_graph_function_length_function_inputs 710 shows "graph_function_refine prec Gamma1 fn1 Gamma2 fn2 711 (eqs ieqs (Some o ils)) orel 712 = (\<forall>tr tr'. related_pair (False, NextNode (entry_point f1), restrs_list []) 713 (acc_vars (function_inputs f1)) 714 (True, NextNode (entry_point f2), restrs_list []) 715 (acc_vars (function_inputs f2)) 716 (eqs ieqs (Some o ils) o tuple_switch) (tr, tr') 717 \<and> exec_double_trace Gamma1 fn1 Gamma2 fn2 tr tr' 718 \<longrightarrow> restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 719 (restrs_list [(entry_point f1, [1])]) (restrs_list [(entry_point f2, [1])]) 720 orel tr tr')" 721 using wfs 722 apply (simp add: graph_function_refine_trace2 gfs) 723 apply (simp add: restr_trace_refine_def gfs 724 restrs_eventually_init 725 restrs_list_def split_def related_pair_def double_visit_def 726 wf_graph_function_init_extract) 727 apply (rule arg_cong[where f=All] ext)+ 728 apply (auto simp: wf_graph_function_init_extract 729 wf_graph_function_length_function_inputs gfs 730 restrs_list_def 731 cong: if_cong 732 elim!: restrs_eventually_init[where Gamma=Gamma1, OF _ _ inps(1)] 733 restrs_eventually_init[where Gamma=Gamma2, OF _ _ inps(2)]; 734 metis) 735 done 736 737lemma restrs_list_Int: 738 "restrs_list rs = (\<lambda>j. \<Inter>(n, xsf) \<in> set rs. (if j = n then set xsf else UNIV))" 739 apply (induct rs rule: rev_induct) 740 apply (simp add: restrs_list_def) 741 apply (clarsimp simp add: restrs_list_def fun_eq_iff) 742 done 743 744lemma restrs_list_Int2: 745 "restrs_list rs = (\<lambda>j. \<Inter>(_, xsf) \<in> {x \<in> set rs. fst x = j}. set xsf)" 746 by (auto simp add: restrs_list_Int fun_eq_iff set_eq_iff) 747 748lemma restrs_list_Cons: 749 "restrs_list ((n, xs) # rs) = (\<lambda>j. 750 if j = n then set xs \<inter> restrs_list rs j else restrs_list rs j)" 751 by (simp add: restrs_list_Int fun_eq_iff) 752 753lemma restrs_eventually_Cons: 754 "restrs_eventually_condition tr ((K UNIV) (n := set xs)) 755 \<Longrightarrow> restrs_eventually_condition tr (restrs_list rs) 756 \<Longrightarrow> restrs_eventually_condition tr (restrs_list ((n, xs) # rs))" 757 apply (clarsimp simp: restrs_eventually_condition_def) 758 apply (rule_tac x="max na naa" in exI) 759 apply (simp add: restrs_condition_def restrs_list_Cons split: if_split_asm) 760 apply (simp add: max_def) 761 done 762 763lemma ex_greatest_nat_le: 764 "P j \<Longrightarrow> j \<le> n \<Longrightarrow> \<exists>k \<le> n. (\<forall>i \<in> {Suc k .. n}. \<not> P i) \<and> P k" 765 apply (cases "P n") 766 apply (rule_tac x=n in exI, simp) 767 apply (cut_tac P="\<lambda>j. P (n - j)" and n = "n - j" in ex_least_nat_le, simp+) 768 apply (clarify, rule_tac x="n - k" in exI) 769 apply clarsimp 770 apply (drule_tac x="n - i" in spec, simp) 771 done 772 773lemma neq_counting_le: 774 assumes neq: "\<forall>i. f i \<noteq> bound" 775 assumes mono: "\<forall>i. f (Suc i) \<le> Suc (f i)" 776 shows "f 0 < bound \<Longrightarrow> f i < bound" 777proof (induct i) 778 case 0 779 show ?case using 0 by simp 780next 781 case (Suc n) 782 show ?case using neq[rule_format, of n] neq[rule_format, of "Suc n"] 783 mono[rule_format, of n] Suc 784 by simp 785qed 786 787lemma restrs_eventually_upt: 788 "\<exists>m. card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} = i \<and> tr m \<noteq> None 789 \<Longrightarrow> \<forall>m. card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} \<noteq> j 790 \<Longrightarrow> restrs_eventually_condition tr ((\<lambda>_. UNIV) (n := {i ..< j}))" 791 apply (clarsimp simp: restrs_eventually_condition_def restrs_condition_def) 792 apply (rule exI, rule conjI, erule exI) 793 apply (clarsimp simp: Suc_le_eq) 794 apply (intro conjI impI allI) 795 apply (rule card_mono) 796 apply simp 797 apply clarsimp 798 apply (frule neq_counting_le, simp_all) 799 apply (clarsimp simp: Collect_less_Suc) 800 apply (drule_tac x=0 in spec, simp) 801 done 802 803lemma set_fill_in_below: 804 "set (fill_in_below xs) = {k. \<exists>l. l : set xs \<and> k \<le> l}" 805 apply (induct xs rule: rev_induct, simp_all add: fill_in_below_def) 806 apply (simp add: set_eq_iff less_max_iff_disj less_Suc_eq_le) 807 apply auto 808 done 809 810lemma restrs_visit_abstract: 811 assumes dist: "distinct (map fst rs)" 812 shows "restrs_list (restrs_visit rs nn gf) 813 = (\<lambda>j. if (nn, NextNode j) \<in> rtrancl (reachable_step' gf) 814 then {k. \<exists>l. l \<in> restrs_list rs j \<and> k \<le> l} 815 else restrs_list rs j)" 816proof - 817 have P: "\<And>j. {x \<in> set (restrs_visit rs nn gf). fst x = j} 818 = (if (nn, NextNode j) \<in> rtrancl (reachable_step' gf) 819 then (\<lambda>(k, xsf). (k, fill_in_below xsf)) 820 ` {x \<in> set rs. fst x = j} 821 else {x \<in> set rs. fst x = j})" 822 by (force simp: restrs_visit_def elim: image_eqI[rotated]) 823 show ?thesis 824 apply (rule ext, clarsimp simp: restrs_list_Int2 split_def P) 825 apply (cut_tac dist[THEN set_map_of_compr]) 826 apply (case_tac "\<exists>b. (j, b) \<in> set rs") 827 apply (auto simp: set_fill_in_below) 828 done 829qed 830 831lemma last_upd_stack: 832 "List.last (upd_stack nn stf xs) 833 = (if length xs = 1 then (nn, stf (fst (snd (hd xs))), snd (snd (hd xs))) 834 else List.last xs)" 835 by (cases xs, simp_all) 836 837lemma not_reachable_visits_same: 838 "tr \<in> exec_trace Gamma fn \<Longrightarrow> Gamma fn = Some gf 839 \<Longrightarrow> trace_addr tr i = Some n 840 \<Longrightarrow> (n, m) \<notin> rtrancl (reachable_step' gf) 841 \<Longrightarrow> wf_graph_function gf ilen olen 842 \<Longrightarrow> j > i 843 \<Longrightarrow> {k. k < j \<and> trace_addr tr k = Some m} = {k. k < i \<and> trace_addr tr k = Some m}" 844 using reachable_trace_eq[THEN subsetD[OF rtrancl_mono, OF Int_lower1]] 845 apply (safe, simp_all) 846 apply (rule ccontr, clarsimp simp: linorder_not_less) 847 done 848 849lemma not_reachable_visits_same_symm: 850 "tr \<in> exec_trace Gamma fn \<Longrightarrow> Gamma fn = Some gf 851 \<Longrightarrow> trace_addr tr i = Some n 852 \<Longrightarrow> trace_addr tr j = Some n 853 \<Longrightarrow> (n, m) \<notin> rtrancl (reachable_step' gf) 854 \<Longrightarrow> wf_graph_function gf ilen olen 855 \<Longrightarrow> {k. k < j \<and> trace_addr tr k = Some m} = {k. k < i \<and> trace_addr tr k = Some m}" 856 using linorder_neq_iff[where x=i and y=j] not_reachable_visits_same 857 by blast 858 859lemma restrs_eventually_at_visit: 860 "restrs_eventually_condition tr (restrs_list rs) 861 \<Longrightarrow> trace_addr tr i = Some nn 862 \<Longrightarrow> tr \<in> exec_trace Gamma fn \<Longrightarrow> Gamma fn = Some gf 863 \<Longrightarrow> distinct (map fst rs) 864 \<Longrightarrow> wf_graph_function gf ilen olen 865 \<Longrightarrow> restrs_condition tr (restrs_list (restrs_visit rs nn gf)) i" 866 apply (clarsimp simp: restrs_eventually_condition_def 867 restrs_condition_def restrs_visit_abstract) 868 apply (case_tac "i \<ge> n") 869 apply (drule spec, drule(1) mp) 870 apply auto[1] 871 apply (simp add: linorder_not_le) 872 apply (drule spec, drule mp, rule order_refl) 873 apply safe 874 apply (fastforce intro: card_mono) 875 apply (simp add: not_reachable_visits_same[symmetric]) 876 done 877 878lemma fold_double_trace_imp: 879 "fold double_trace_imp hyps hyp trs 880 = ((\<forall>h \<in> set hyps. h trs) \<longrightarrow> hyp trs)" 881 apply (induct hyps arbitrary: hyp, simp_all) 882 apply (auto simp add: double_trace_imp_def) 883 done 884 885lemma exec_trace_addr_Suc: 886 "tr \<in> exec_trace Gamma f \<Longrightarrow> trace_addr tr n = Some (NextNode m) \<Longrightarrow> tr (Suc n) \<noteq> None" 887 apply (drule_tac i=n in exec_trace_step_cases) 888 apply (auto dest!: trace_addr_SomeD) 889 done 890 891lemma num_visits_equals_j_first: 892 "card {i. i < m \<and> trace_addr tr i = Some n} = j 893 \<Longrightarrow> j \<noteq> 0 894 \<Longrightarrow> \<exists>m'. trace_addr tr m' = Some n \<and> card {i. i < m' \<and> trace_addr tr i = Some n} = j - 1" 895 apply (frule_tac P="\<lambda>m. card {i. i < m \<and> trace_addr tr i = Some n} = j" 896 in ex_least_nat_le[rotated]) 897 apply simp 898 apply clarify 899 apply (rule_tac x="k - 1" in exI) 900 apply (case_tac k) 901 apply (simp del: Collect_empty_eq) 902 apply (simp add: Collect_less_Suc split: if_split_asm) 903 done 904 905lemma ex_least_nat: 906 "\<exists>n. P n \<Longrightarrow> \<exists>n :: nat. P n \<and> (\<forall>i < n. \<not> P i)" 907 apply clarsimp 908 apply (case_tac "n = 0") 909 apply fastforce 910 apply (cut_tac P="\<lambda>i. i \<noteq> 0 \<and> P i" in ex_least_nat_le, auto) 911 done 912 913lemma visit_eqs: 914 "(visit trace nn restrs = None) 915 = (\<forall>i. trace_addr trace i = Some nn \<longrightarrow> \<not> restrs_condition trace restrs i)" 916 "(visit trace nn restrs = Some st) 917 = (\<exists>i. restrs_condition trace restrs i \<and> trace_addr trace i = Some nn 918 \<and> st = fst (snd (hd (the (trace i)))) 919 \<and> (\<forall>j < i. restrs_condition trace restrs j \<longrightarrow> trace_addr trace j \<noteq> Some nn))" 920 apply (simp_all add: visit_def) 921 apply auto[1] 922 apply (safe elim!: exE[OF ex_least_nat] del: exE, simp_all) 923 apply (rule exI, rule conjI, assumption, simp) 924 apply (rule arg_cong[OF Least_equality], simp) 925 apply (blast intro: linorder_not_le[THEN iffD1]) 926 apply (rule arg_cong[OF Least_equality], simp) 927 apply (blast intro: linorder_not_le[THEN iffD1]) 928 done 929 930lemmas visit_eqs' = visit_eqs(1) arg_cong[where f=Not, OF visit_eqs(1), simplified] 931 932theorem restr_trace_refine_Restr1: 933 "j \<noteq> 0 934 \<Longrightarrow> distinct (map fst rs1) 935 \<Longrightarrow> wf_graph_function f1 ilen olen \<Longrightarrow> Gamma1 fn1 = Some f1 936 \<Longrightarrow> i \<noteq> 0 \<longrightarrow> 937 pc' n (restrs_list ((n, [i - 1]) # (restrs_visit rs1 (NextNode n) f1))) tr 938 \<Longrightarrow> \<not> pc' n (restrs_list ((n, [j - 1]) # (restrs_visit rs1 (NextNode n) f1))) tr 939 \<Longrightarrow> restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 (restrs_list ((n, [i ..< j]) # rs1)) rs2 orel tr tr' 940 \<Longrightarrow> restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 (restrs_list rs1) rs2 orel tr tr'" 941 apply (clarsimp simp: restr_trace_refine_def) 942 apply (subst(asm) restrs_eventually_Cons, simp_all add: K_def) 943 prefer 2 944 apply auto[1] 945 apply (rule restrs_eventually_upt) 946 apply (clarsimp simp: fold_double_trace_imp double_trace_imp_def pc_def) 947 apply (case_tac "i = 0") 948 apply (rule_tac x=0 in exI) 949 apply (clarsimp simp: dest!: exec_trace_init) 950 apply simp 951 apply (clarsimp simp: visit_eqs) 952 apply (simp(no_asm_use) add: restrs_list_Cons restrs_condition_def) 953 apply (drule_tac x=n in spec)+ 954 apply simp 955 apply (rule_tac x="Suc ia" in exI, simp add: Collect_less_Suc) 956 apply (rule exec_trace_addr_Suc[simplified], assumption) 957 apply simp 958 apply (clarsimp simp: fold_double_trace_imp double_trace_imp_def pc_def) 959 apply (thin_tac "0 < i \<longrightarrow> q" for q) 960 apply (clarsimp simp: visit_eqs) 961 apply (frule num_visits_equals_j_first[OF refl, simplified neq0_conv]) 962 apply clarsimp 963 apply (drule(5) restrs_eventually_at_visit) 964 apply (drule_tac x=m' in spec, clarsimp) 965 apply (clarsimp simp: restrs_list_Cons restrs_condition_def split: if_split_asm) 966 done 967 968theorem restr_trace_refine_Restr2: 969 "j \<noteq> 0 970 \<Longrightarrow> distinct (map fst rs2) 971 \<Longrightarrow> wf_graph_function f2 ilen olen \<Longrightarrow> Gamma2 fn2 = Some f2 972 \<Longrightarrow> i \<noteq> 0 \<longrightarrow> pc' n (restrs_list ((n, [i - 1]) # (restrs_visit rs2 (NextNode n) f2))) tr' 973 \<Longrightarrow> \<not> pc' n (restrs_list ((n, [j - 1]) # (restrs_visit rs2 (NextNode n) f2))) tr' 974 \<Longrightarrow> restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 rs1 (restrs_list ((n, [i ..< j]) # rs2)) orel tr tr' 975 \<Longrightarrow> restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 rs1 (restrs_list rs2) orel tr tr'" 976 apply (clarsimp simp: restr_trace_refine_def) 977 apply (subst(asm) restrs_eventually_Cons, simp_all add: K_def) 978 prefer 2 979 apply auto[1] 980 apply (rule restrs_eventually_upt) 981 apply (clarsimp simp: fold_double_trace_imp double_trace_imp_def pc_def) 982 apply (case_tac "i = 0") 983 apply (rule_tac x=0 in exI) 984 apply (clarsimp dest!: exec_trace_init) 985 apply simp 986 apply (clarsimp simp: visit_eqs restrs_list_Cons restrs_condition_def) 987 apply (drule_tac x=n in spec)+ 988 apply simp 989 apply (rule_tac x="Suc ia" in exI, simp add: Collect_less_Suc) 990 apply (rule exec_trace_addr_Suc[simplified], assumption) 991 apply simp 992 apply (clarsimp simp: fold_double_trace_imp double_trace_imp_def pc_def) 993 apply (thin_tac "0 < i \<longrightarrow> q" for q) 994 apply (clarsimp simp: visit_eqs) 995 apply (frule num_visits_equals_j_first[OF refl, simplified neq0_conv]) 996 apply clarsimp 997 apply (drule(5) restrs_eventually_at_visit) 998 apply (drule_tac x=m' in spec, clarsimp) 999 apply (clarsimp simp: restrs_list_Cons restrs_condition_def split: if_split_asm) 1000 done 1001 1002lemma pc_Ret_Err_trace_end: 1003 "er \<in> {Ret, Err} \<Longrightarrow> pc er restrs tr 1004 \<Longrightarrow> tr \<in> exec_trace Gamma f 1005 \<Longrightarrow> \<exists>st g. trace_end tr = Some [(er, st, g)]" 1006 apply (clarsimp simp: pc_def visit_eqs trace_end_def dest!: trace_addr_SomeD) 1007 apply (frule_tac i=i in exec_trace_step_cases, simp add: all_exec_graph_step_cases) 1008 apply (cut_tac tr=tr and n="Suc i" in trace_None_dom_subset) 1009 apply (auto simp add: exec_trace_def)[2] 1010 apply (subst Max_eqI[rotated 2], erule domI) 1011 apply (simp add: finite_subset) 1012 apply (simp add: subset_iff less_Suc_eq_le) 1013 apply auto[1] 1014 done 1015 1016lemmas pc_Ret_trace_end = pc_Ret_Err_trace_end[where er=Ret, simplified] 1017 1018lemma exec_trace_end_SomeD: 1019 "trace_end tr = Some v \<Longrightarrow> tr \<in> exec_trace Gamma f 1020 \<Longrightarrow> \<exists>n. tr n = Some v \<and> tr (Suc n) = None 1021 \<and> (\<exists>nn st g. v = [(nn, st, g)] \<and> nn \<in> {Ret, Err})" 1022 apply (frule exec_trace_nat_trace) 1023 apply (drule(1) trace_end_SomeD) 1024 apply clarsimp 1025 apply (frule_tac i=n in exec_trace_Nil) 1026 apply (case_tac "fst (hd v)", auto simp add: continuing_def split: list.split_asm) 1027 done 1028 1029lemma reachable_from_Ret: 1030 "((Ret, nn) \<notin> reachable_step' gf)" 1031 by (simp add: reachable_step_def) 1032 1033lemma trace_end_visit_Ret: 1034 "tr n = Some [(Ret, st, g)] \<Longrightarrow> tr (Suc n) = None 1035 \<Longrightarrow> tr \<in> exec_trace Gamma gf 1036 \<Longrightarrow> restrs_eventually_condition tr rs 1037 \<Longrightarrow> visit tr Ret rs = Some st" 1038 apply (rule visit_known, assumption) 1039 apply (clarsimp simp: restrs_eventually_condition_def) 1040 apply (drule spec, erule mp) 1041 apply (clarsimp simp: exec_trace_def) 1042 apply (drule(1) trace_None_dom_subset) 1043 apply auto[1] 1044 apply (clarsimp dest!: trace_addr_SomeD) 1045 apply (frule_tac i=j in exec_trace_step_cases, simp add: all_exec_graph_step_cases) 1046 apply (clarsimp simp: exec_trace_def) 1047 apply (auto dest!: trace_None_dom_subset) 1048 done 1049 1050definition 1051 "output_rel orel gfs restrs trs = 1052 orel (\<lambda>(x, y). acc_vars (tuple_switch (function_inputs, function_outputs) y 1053 (tuple_switch gfs x)) 1054 (the (double_visit (x, tuple_switch (NextNode (entry_point (tuple_switch gfs x)), Ret) y, 1055 tuple_switch (restrs_list [], tuple_switch restrs x) y) trs)))" 1056 1057theorem restr_trace_refine_Leaf: 1058 "wf_graph_function f1 ilen1 olen1 \<Longrightarrow> Gamma1 fn1 = Some f1 1059 \<Longrightarrow> wf_graph_function f2 ilen2 olen2 \<Longrightarrow> Gamma2 fn2 = Some f2 1060 \<Longrightarrow> pc Ret rs1 tr \<Longrightarrow> prec \<longrightarrow> pc Ret rs2 tr' 1061 \<Longrightarrow> output_rel orel (f1, f2) (rs1, rs2) (tr, tr') 1062 \<Longrightarrow> restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 rs1 rs2 orel tr tr'" 1063 apply (clarsimp simp only: restr_trace_refine_def) 1064 apply (clarsimp simp: trace_refine2_def trace_refine_def) 1065 apply (frule(1) pc_Ret_trace_end) 1066 apply (case_tac "trace_end tr'") 1067 apply (clarsimp split: option.split) 1068 apply (cut_tac tr=tr' in pc_Ret_trace_end, blast, assumption+) 1069 apply clarsimp 1070 apply (clarsimp simp: output_rel_def) 1071 apply (drule(1) exec_trace_end_SomeD)+ 1072 apply (safe del: impCE, simp_all) 1073 apply (erule rsubst[where P=orel], rule ext) 1074 apply (clarsimp simp: tuple_switch_def switch_val_def double_visit_def 1075 wf_graph_function_init_extract restrs_list_def 1076 wf_graph_function_length_function_inputs 1077 function_outputs_st_def trace_end_visit_Ret 1078 init_state_def wf_graph_function_acc_vars_save_vals) 1079 done 1080 1081lemma first_reached_propD: 1082 "first_reached_prop addrs propn trs 1083 \<Longrightarrow> \<exists>addr \<in> set addrs. propn addr trs 1084 \<and> (\<forall>propn. first_reached_prop addrs propn trs = propn addr trs)" 1085 by (induct addrs, simp_all split: if_split_asm) 1086 1087lemma double_pc_reds: 1088 "double_pc (False, nn, restrs) trs = pc nn restrs (fst trs)" 1089 "double_pc (True, nn, restrs) trs = pc nn restrs (snd trs)" 1090 by (simp_all add: double_pc_def pc_def split_def) 1091 1092definition 1093 merge_opt :: "'a option \<Rightarrow> 'a option \<Rightarrow> 'a option" 1094where 1095 "merge_opt opt opt' = case_option opt' Some opt" 1096 1097lemma merge_opt_simps[simp]: 1098 "merge_opt (Some x) v = Some x" 1099 "merge_opt None v = v" 1100 by (simp_all add: merge_opt_def) 1101 1102lemma fold_merge_opt_Nones_eq: 1103 "(\<forall>v \<in> set xs. v = None) \<Longrightarrow> fold merge_opt xs v = v" 1104 by (induct xs, simp_all) 1105 1106lemma set_zip_rev: 1107 "length xs = length ys \<Longrightarrow> set (zip xs ys) = set (zip (rev xs) (rev ys))" 1108 by (simp add: zip_rev) 1109 1110lemma exec_trace_non_Call: 1111 "\<lbrakk> tr \<in> exec_trace Gamma fn; Gamma fn = Some f; 1112 trace_bottom_addr tr i = Some (NextNode n); 1113 function_graph f n = Some node; 1114 case node of Call _ _ _ _ \<Rightarrow> False | _ \<Rightarrow> True 1115 \<rbrakk> \<Longrightarrow> trace_addr tr i = Some (NextNode n)" 1116 apply (clarsimp simp: trace_bottom_addr_def split: option.split_asm) 1117 apply (frule(1) exec_trace_invariant) 1118 apply (clarsimp simp: exec_graph_invariant_def neq_Nil_conv) 1119 apply (case_tac "tl (the (tr i))" rule: rev_cases) 1120 apply (clarsimp simp: trace_addr_SomeI) 1121 apply (clarsimp simp: get_state_function_call_def split: node.split_asm) 1122 done 1123 1124lemma visit_immediate_pred: 1125 "\<lbrakk> tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; 1126 trace_addr tr i = Some nn; nn \<noteq> NextNode (entry_point f); 1127 converse (reachable_step' f) `` {nn} \<subseteq> S \<rbrakk> 1128 \<Longrightarrow> \<exists>i' nn'. i = Suc i' \<and> nn' \<in> S \<and> trace_bottom_addr tr i' = Some nn'" 1129 apply (case_tac i) 1130 apply (clarsimp dest!: exec_trace_init trace_addr_SomeD) 1131 apply (rename_tac i') 1132 apply (frule trace_addr_SomeD, clarsimp) 1133 apply (frule(1) exec_trace_invariant) 1134 apply (frule_tac i=i' in exec_trace_step_reachable_induct2, assumption+) 1135 apply (simp add: trace_bottom_addr_def) 1136 apply auto 1137 done 1138 1139 1140 1141lemma pred_restrs: 1142 "\<lbrakk> tr \<in> exec_trace Gamma f; trace_bottom_addr tr i = Some nn \<rbrakk> 1143 \<Longrightarrow> restrs_condition tr restrs (Suc i) 1144 = restrs_condition tr (if trace_addr tr i = None then restrs 1145 else pred_restrs nn restrs) i" 1146 apply (clarsimp simp: restrs_condition_def Collect_less_Suc all_conj_distrib 1147 pred_restrs_def 1148 split: if_split_asm next_node.split) 1149 apply (auto simp: trace_addr_trace_bottom_addr_eq) 1150 done 1151 1152lemma visit_merge: 1153 assumes tr: "tr \<in> exec_trace Gamma fn" "Gamma fn = Some f" 1154 and wf: "wf_graph_function f ilen olen" 1155 and ns: "nn \<noteq> NextNode (entry_point f)" 1156 "\<forall>n \<in> set ns. graph n = Some (Basic nn [])" 1157 "converse (reachable_step graph) `` {nn} \<subseteq> NextNode ` set ns" 1158 and geq: "function_graph f = graph" 1159 and cut: "\<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y})" 1160 "\<forall>n \<in> set ns. (nn, NextNode n) \<notin> rtrancl 1161 (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})" 1162 shows "visit tr nn restrs = fold merge_opt (map (\<lambda>n. visit tr (NextNode n) 1163 (pred_restrs' n restrs)) ns) None" 1164proof - 1165 note ns = ns[folded geq] 1166 note cut = cut[folded geq] 1167 1168 have step_after: 1169 "\<And>n i. n \<in> set ns \<Longrightarrow> trace_bottom_addr tr i = Some (NextNode n) 1170 \<Longrightarrow> \<exists>st. tr i = Some [(NextNode n, st, fn)] 1171 \<and> tr (Suc i) = Some [(nn, st, fn)] 1172 \<and> trace_addr tr (Suc i) = Some nn 1173 \<and> restrs_condition tr restrs (Suc i) 1174 = restrs_condition tr (pred_restrs' n restrs) i" 1175 apply (drule exec_trace_non_Call[OF tr], (simp add: ns)+) 1176 apply (frule ns[rule_format], cut_tac tr(2)) 1177 apply (frule trace_addr_SomeD, clarsimp) 1178 apply (frule exec_trace_invariant[OF tr(1)]) 1179 apply (cut_tac i=i in exec_trace_step_cases[OF tr(1)]) 1180 apply (clarsimp simp: all_exec_graph_step_cases exec_graph_invariant_Cons 1181 upd_vars_def save_vals_def) 1182 apply (simp add: pred_restrs[OF tr(1)] trace_addr_SomeI trace_bottom_addr_def K_def) 1183 done 1184 have step_after_single: 1185 "\<And>n i. n \<in> set ns \<Longrightarrow> trace_bottom_addr tr i = Some (NextNode n) 1186 \<Longrightarrow> restrs_condition tr restrs (Suc i) 1187 \<Longrightarrow> (\<forall>n' j. n' \<in> set ns \<longrightarrow> trace_addr tr j = Some (NextNode n') 1188 \<longrightarrow> restrs_condition tr (pred_restrs' n' restrs) j \<longrightarrow> j = i)" 1189 apply clarsimp 1190 apply (frule step_after, erule trace_addr_trace_bottom_addr_eq) 1191 apply (frule(1) step_after) 1192 apply clarsimp 1193 apply (drule(2) restrs_single_visit[OF tr wf _ _ _ _ cut(1)], simp_all) 1194 apply (rule not_trancl_converse_step, rule ns) 1195 apply (simp add: cut) 1196 done 1197 have visit_after: 1198 "\<And>n v. n \<in> set ns \<Longrightarrow> visit tr (NextNode n) (pred_restrs' n restrs) = Some v 1199 \<Longrightarrow> visit tr nn restrs \<noteq> None" 1200 apply (clarsimp simp: visit_eqs) 1201 apply (drule_tac i=i in step_after, simp add: trace_addr_trace_bottom_addr_eq) 1202 apply (rule_tac x="Suc i" in exI) 1203 apply clarsimp 1204 done 1205 show ?thesis 1206 apply (rule sym, cases "visit tr nn restrs", simp_all) 1207 apply (rule fold_merge_opt_Nones_eq) 1208 apply (rule ccontr, clarsimp simp: visit_after) 1209 apply (clarsimp simp: visit_eqs) 1210 apply (frule visit_immediate_pred[OF tr wf _ ns(1, 3)]) 1211 apply clarsimp 1212 apply (frule(1) step_after, clarsimp) 1213 apply (frule(2) step_after_single) 1214 apply (drule in_set_conv_decomp_last[THEN iffD1]) 1215 apply clarsimp 1216 apply (rule trans, rule fold_merge_opt_Nones_eq) 1217 apply (rule ccontr, clarsimp simp: visit_eqs pc_def ball_Un) 1218 apply (simp add: trace_addr_SomeI) 1219 apply (subst visit_known, assumption, simp_all) 1220 apply clarsimp 1221 done 1222qed 1223 1224lemma visit_merge_restrs: 1225 assumes tr: "tr \<in> exec_trace Gamma fn" "Gamma fn = Some gf" 1226 and geq: "function_graph gf = graph" 1227 assumes indep: "opt \<notin> set (opt2 # opts)" 1228 assumes reach: "(nn, NextNode addr) \<notin> rtrancl (reachable_step graph)" 1229 and wf: "wf_graph_function gf ilen olen" 1230 fixes rs 1231 defines "rs1 \<equiv> restrs_list ((addr, [opt]) # rs)" 1232 and "rs2 \<equiv> restrs_list ((addr, opt2 # opts) # rs)" 1233 and "rs3 \<equiv> restrs_list ((addr, opt # opt2 # opts) # rs)" 1234 shows 1235 "visit tr nn rs3 1236 = merge_opt (visit tr nn rs1) (visit tr nn rs2)" 1237proof - 1238 let ?card = "\<lambda>i. card {j. j < i \<and> trace_addr tr j = Some (NextNode addr)}" 1239 obtain n where vis: "\<forall>i. trace_addr tr i = Some nn \<longrightarrow> ?card i = n" 1240 apply (case_tac "\<exists>i. trace_addr tr i = Some nn") 1241 apply clarsimp 1242 apply (erule_tac x="?card i" in meta_allE) 1243 apply (erule meta_mp) 1244 apply clarsimp 1245 apply (auto dest: not_reachable_visits_same_symm[OF tr _ _ reach[folded geq] wf]) 1246 done 1247 have indep2: "\<forall>i. restrs_condition tr rs1 i 1248 \<longrightarrow> \<not> restrs_condition tr rs2 i" 1249 using indep 1250 apply (clarsimp, clarsimp simp: restrs_condition_def rs1_def rs2_def restrs_list_Cons) 1251 apply (drule_tac x=addr in spec)+ 1252 apply (clarsimp simp: restrs_list_def) 1253 done 1254 have disj: 1255 "\<forall>i. restrs_condition tr rs3 i 1256 = (restrs_condition tr rs1 i \<or> restrs_condition tr rs2 i)" 1257 apply (clarsimp simp: restrs_condition_def rs1_def rs2_def rs3_def restrs_list_Cons) 1258 apply blast 1259 done 1260 have indep3: "\<forall>j i. trace_addr tr i = Some nn \<longrightarrow> restrs_condition tr rs1 i 1261 \<longrightarrow> trace_addr tr j = Some nn \<longrightarrow> \<not> restrs_condition tr rs2 j" 1262 using indep 1263 apply (clarsimp, clarsimp simp: restrs_condition_def rs1_def rs2_def restrs_list_Cons) 1264 apply (drule_tac x=addr in spec)+ 1265 apply (clarsimp simp: restrs_list_def vis) 1266 done 1267 show ?thesis 1268 unfolding visit_def 1269 by (auto simp: disj dest: indep3[rule_format]; metis) 1270qed 1271 1272theorem visit_explode_restr: 1273 assumes gf1: "tr \<in> exec_trace Gamma fn" 1274 "Gamma fn = Some gf" 1275 "function_graph gf = graph" 1276 and gf2: "(nn, NextNode addr) \<notin> (reachable_step graph)\<^sup>*" 1277 "wf_graph_function gf ilen olen" 1278 and rs: "restrs_list rs addr = set xs" 1279 "filter (\<lambda>(addr', xs). addr' \<noteq> addr) rs = rs'" 1280 and xs: "distinct xs" 1281 shows "visit tr nn (restrs_list rs) = 1282 fold (\<lambda>x. merge_opt (visit tr nn (restrs_list ((addr, [x]) # rs')))) xs None" 1283proof - 1284 from rs have Q1: "restrs_list rs addr = restrs_list ((addr, rev xs) # rs') addr" 1285 apply (clarsimp simp: restrs_list_def fun_eq_iff) 1286 apply (rule fold_invariant[where g="\<lambda>x. x", symmetric], auto) 1287 done 1288 1289 { fix addr' from rs(2) have "addr \<noteq> addr' 1290 \<Longrightarrow> restrs_list rs addr' = restrs_list ((addr, rev xs) # rs') addr'" 1291 apply clarsimp 1292 apply hypsubst_thin 1293 apply (induct rs, simp_all add: restrs_list_Cons) 1294 apply (clarsimp simp: restrs_list_Cons) 1295 done 1296 } 1297 hence Q: "restrs_list rs = restrs_list ((addr, rev xs) # rs')" 1298 using Q1 1299 apply (simp add: fun_eq_iff) 1300 apply metis 1301 done 1302 1303 show "?thesis" using xs unfolding Q 1304 apply (induct xs rule: rev_induct) 1305 apply (simp add: restrs_list_Cons visit_def restrs_condition_def) 1306 apply metis 1307 apply (case_tac xs rule: rev_cases) 1308 apply (simp add: merge_opt_def) 1309 apply (clarsimp simp: visit_merge_restrs[OF gf1 _ gf2]) 1310 done 1311qed 1312 1313lemma visit_impossible: 1314 "tr \<in> exec_trace Gamma fn \<Longrightarrow> Gamma fn = Some gf 1315 \<Longrightarrow> function_graph gf = graph 1316 \<Longrightarrow> wf_graph_function gf ilen olen 1317 \<Longrightarrow> 0 \<notin> restrs n 1318 \<Longrightarrow> (NextNode n, nn) \<notin> rtrancl (reachable_step graph) 1319 \<Longrightarrow> visit tr nn restrs = None" 1320 apply (clarsimp simp: visit_eqs restrs_condition_def) 1321 apply (rule_tac x=n in exI) 1322 apply (subst arg_cong[where f=card and y="{}"], simp_all) 1323 apply clarsimp 1324 apply (drule(5) reachable_trace) 1325 apply (drule trancl_mono[OF _ Int_lower1]) 1326 apply (simp add: trancl_into_rtrancl) 1327 done 1328 1329lemma visit_inconsistent: 1330 "restrs i = {} \<Longrightarrow> visit tr nn restrs = None" 1331 by (auto simp add: visit_def restrs_condition_def) 1332 1333lemma visit_immediate_pred_step: 1334 "tr i = Some [(nn, st, fn')] 1335 \<Longrightarrow> tr \<in> exec_trace Gamma fn \<Longrightarrow> Gamma fn = Some gf 1336 \<Longrightarrow> wf_graph_function gf ilen olen 1337 \<Longrightarrow> converse (reachable_step (function_graph gf)) `` {nn} \<subseteq> {NextNode n} 1338 \<Longrightarrow> nn \<noteq> NextNode (entry_point gf) 1339 \<Longrightarrow> (case (function_graph gf n) of None \<Rightarrow> False | Some (Call _ _ _ _) \<Rightarrow> False | _ \<Rightarrow> True) 1340 \<Longrightarrow> \<exists>i' st'. i = Suc i' \<and> fn' = fn \<and> tr i' = Some [(NextNode n, st', fn)] 1341 \<and> (([(NextNode n, st', fn)], [(nn, st, fn)]) \<in> exec_graph_step Gamma)" 1342 apply (frule(2) visit_immediate_pred[where i=i], simp_all) 1343 apply (simp add: trace_addr_def) 1344 apply (clarsimp split: option.split_asm) 1345 apply (frule(4) exec_trace_non_Call) 1346 apply (clarsimp dest!: trace_addr_SomeD) 1347 apply (frule_tac i=i' in exec_trace_step_cases, clarsimp) 1348 apply (frule_tac i=i' in exec_trace_invariant') 1349 apply (frule_tac i=i in exec_trace_invariant') 1350 apply (clarsimp simp: exec_graph_invariant_def) 1351 done 1352 1353lemma visit_Basic: 1354 "tr \<in> exec_trace Gamma fn \<Longrightarrow> Gamma fn = Some gf 1355 \<Longrightarrow> function_graph gf = graph 1356 \<Longrightarrow> wf_graph_function gf ilen olen 1357 \<Longrightarrow> graph n = Some (Basic nn upds) 1358 \<Longrightarrow> converse (reachable_step graph) `` {nn} \<subseteq> {NextNode n} 1359 \<Longrightarrow> nn \<noteq> NextNode (entry_point gf) 1360 \<Longrightarrow> visit tr nn restrs = option_map (upd_vars upds) 1361 (visit tr (NextNode n) (pred_restrs' n restrs))" 1362 apply (cases "visit tr (NextNode n) (pred_restrs' n restrs)", simp_all) 1363 apply (clarsimp simp: visit_eqs) 1364 apply (frule(5) visit_immediate_pred) 1365 apply (clarsimp simp: pred_restrs) 1366 apply (frule(3) exec_trace_non_Call, simp) 1367 apply simp 1368 apply (clarsimp simp: visit_eqs) 1369 apply (frule trace_addr_SomeD, clarsimp) 1370 apply (frule_tac i=i in exec_trace_step_cases) 1371 apply (frule(1) exec_trace_invariant) 1372 apply (rule_tac x="Suc i" in exI) 1373 apply (clarsimp simp: all_exec_graph_step_cases exec_graph_invariant_Cons K_def) 1374 apply (simp add: pred_restrs[unfolded trace_bottom_addr_def] trace_addr_SomeI) 1375 apply clarsimp 1376 apply (frule(2) visit_immediate_pred, simp+) 1377 apply clarsimp 1378 apply (frule(2) exec_trace_non_Call, simp+) 1379 apply (clarsimp simp: pred_restrs split: if_split_asm) 1380 done 1381 1382definition 1383 "option_guard guard opt = (case opt of None \<Rightarrow> None | Some v \<Rightarrow> if guard v then Some v else None)" 1384 1385lemmas option_guard_simps[simp] = option_guard_def[split_simps option.split] 1386 1387lemma visit_Cond: 1388 "tr \<in> exec_trace Gamma fn \<Longrightarrow> Gamma fn = Some gf 1389 \<Longrightarrow> function_graph gf = graph 1390 \<Longrightarrow> wf_graph_function gf ilen olen 1391 \<Longrightarrow> graph n = Some (Cond l r cond) 1392 \<Longrightarrow> converse (reachable_step graph) `` {nn} \<subseteq> {NextNode n} 1393 \<Longrightarrow> nn \<noteq> NextNode (entry_point gf) 1394 \<Longrightarrow> \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}) 1395 \<Longrightarrow> (l, NextNode n) \<notin> rtrancl (reachable_step graph \<inter> {(x, y). x \<notin> set cuts}) 1396 \<Longrightarrow> (r, NextNode n) \<notin> rtrancl (reachable_step graph \<inter> {(x, y). x \<notin> set cuts}) 1397 \<Longrightarrow> visit tr nn restrs = option_guard (\<lambda>st. (nn = l \<and> cond st) \<or> (nn = r \<and> \<not> cond st)) 1398 (visit tr (NextNode n) (pred_restrs' n restrs))" 1399 apply (cases "visit tr (NextNode n) (pred_restrs' n restrs)"; simp) 1400 apply (clarsimp simp: visit_eqs) 1401 apply (frule(5) visit_immediate_pred) 1402 apply (clarsimp simp: pred_restrs) 1403 apply (frule(3) exec_trace_non_Call, simp) 1404 apply simp 1405 apply (clarsimp simp: visit_eqs simp del: imp_disjL) 1406 apply (frule trace_addr_SomeD, clarsimp simp del: imp_disjL) 1407 apply (frule_tac i=i in exec_trace_step_cases) 1408 apply (frule(1) exec_trace_invariant) 1409 apply (clarsimp simp: all_exec_graph_step_cases exec_graph_invariant_Cons 1410 simp del: imp_disjL) 1411 apply (intro conjI impI) 1412 apply (rule_tac x="Suc i" in exI) 1413 apply (clarsimp simp: pred_restrs trace_bottom_addr_def) 1414 apply (rule conjI, simp add: trace_addr_def) 1415 apply clarsimp 1416 apply (frule(3) visit_immediate_pred, simp, simp) 1417 apply (clarsimp simp: pred_restrs) 1418 apply (frule(2) exec_trace_non_Call, simp+)[1] 1419 apply (rule_tac x="Suc i" in exI) 1420 apply (clarsimp simp: pred_restrs trace_bottom_addr_def) 1421 apply (rule conjI, simp add: trace_addr_def) 1422 apply clarsimp 1423 apply (frule(3) visit_immediate_pred, simp, simp) 1424 apply (clarsimp simp: pred_restrs) 1425 apply (frule(2) exec_trace_non_Call, simp+)[1] 1426 apply clarsimp 1427 apply (frule(3) visit_immediate_pred, simp, simp) 1428 apply (clarsimp simp: pred_restrs) 1429 apply (frule(2) exec_trace_non_Call, simp+) 1430 apply (drule(3) restrs_single_visit2, simp+) 1431 apply (clarsimp simp: reachable_step_def[THEN eqset_imp_iff] dest!: tranclD) 1432 apply auto[1] 1433 apply (clarsimp dest!: trace_addr_SomeD split: if_split_asm) 1434 done 1435 1436lemma exec_trace_pc_Call: 1437 "pc' n restrs tr 1438 \<Longrightarrow> tr \<in> exec_trace Gamma fn \<Longrightarrow> Gamma fn = Some f 1439 \<Longrightarrow> function_graph f n = Some (node.Call nn fname inps outps) 1440 \<Longrightarrow> Gamma fname = Some g 1441 \<Longrightarrow> (\<exists>x. restrs_condition tr restrs x \<and> trace_addr tr x = Some (NextNode n) 1442 \<and> (trace_drop_n (Suc x) 1 tr \<in> exec_trace Gamma fname) 1443 \<and> visit tr (NextNode n) restrs = Some (fst (snd (hd (the (tr x))))))" 1444 apply (clarsimp simp: pc_def visit_eqs elim!: exE[OF ex_least_nat] del: exE) 1445 apply (rule exI, rule conjI, assumption, simp) 1446 apply (rule conjI[rotated], blast) 1447 apply (clarsimp dest!: trace_addr_SomeD) 1448 apply (frule(1) exec_trace_invariant) 1449 apply (simp add: exec_graph_invariant_def) 1450 apply (erule(4) exec_trace_drop_n[simplified]) 1451 done 1452 1453lemma exec_trace_step: 1454 "tr \<in> exec_trace Gamma f 1455 \<Longrightarrow> tr i = Some stack 1456 \<Longrightarrow> continuing stack 1457 \<Longrightarrow> \<exists>stack'. tr (Suc i) = Some stack' \<and> (stack, stack') \<in> exec_graph_step Gamma" 1458 apply (frule_tac i=i in exec_trace_step_cases) 1459 apply auto 1460 done 1461 1462lemma trace_bottom_addr_trace_addr_prev: 1463 "\<lbrakk> trace_bottom_addr tr i = Some addr; restrs_condition tr restrs i; 1464 tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen \<rbrakk> 1465 \<Longrightarrow> \<exists>j. trace_addr tr j = Some addr 1466 \<and> (i = j \<or> trace_addr tr i = None) 1467 \<and> (trace_addr tr ` {Suc j .. i} \<subseteq> {None}) 1468 \<and> (trace_bottom_addr tr ` {Suc j .. i} \<subseteq> {Some addr}) 1469 \<and> j \<le> i \<and> restrs_condition tr (if i = j then restrs else pred_restrs addr restrs) j" 1470 apply (induct i) 1471 apply (clarsimp dest!: exec_trace_init) 1472 apply (simp add: trace_addr_def trace_bottom_addr_def) 1473 apply clarsimp 1474 apply (case_tac "trace_addr tr (Suc i)") 1475 defer 1476 apply (auto simp: trace_addr_trace_bottom_addr_eq)[1] 1477 apply (subgoal_tac "trace_bottom_addr tr i = Some addr") 1478 apply (case_tac "trace_addr tr i") 1479 apply simp 1480 apply (drule meta_mp) 1481 apply (simp add: restrs_condition_def Collect_less_Suc) 1482 apply (clarsimp, clarsimp split: if_split_asm) 1483 apply (fastforce simp add: atLeastAtMostSuc_conv) 1484 apply (simp add: trace_addr_trace_bottom_addr_eq pred_restrs) 1485 apply (rule_tac x=i in exI, simp) 1486 apply (frule_tac i=i in exec_trace_step_cases) 1487 apply (elim disjE conjE) 1488 apply (simp add: trace_bottom_addr_def) 1489 apply (clarsimp simp: trace_bottom_addr_def) 1490 apply (clarsimp simp: all_exec_graph_step_cases) 1491 apply (elim disjE conjE exE, simp_all add: trace_addr_def trace_bottom_addr_def 1492 split: list.split_asm graph_function.split_asm if_split_asm) 1493 done 1494 1495lemma visit_extended_pred: 1496 "\<lbrakk> trace_addr tr i = Some addr; restrs_condition tr restrs i; 1497 tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; 1498 converse (reachable_step' f) `` {addr} \<subseteq> S; 1499 addr \<noteq> NextNode (entry_point f) \<rbrakk> 1500 \<Longrightarrow> \<exists>j nn'. trace_addr tr j = Some nn' \<and> nn' \<in> S 1501 \<and> j < i 1502 \<and> (trace_addr tr ` {Suc j ..< i} \<subseteq> {None}) 1503 \<and> (trace_bottom_addr tr ` {Suc j ..< i} \<subseteq> {Some nn'}) 1504 \<and> restrs_condition tr (pred_restrs nn' restrs) j" 1505 apply (frule(5) visit_immediate_pred) 1506 apply (clarsimp simp: pred_restrs) 1507 apply (frule(4) trace_bottom_addr_trace_addr_prev) 1508 apply clarsimp 1509 apply (rule_tac x=j in exI, simp) 1510 apply (clarsimp split: if_split_asm) 1511 apply (simp add: atLeastLessThanSuc_atLeastAtMost) 1512 done 1513 1514lemma if_x_None_eq_Some: 1515 "((if P then x else None) = Some y) = (P \<and> x = Some y)" 1516 by simp 1517 1518lemma subtract_le_nat: 1519 "((a :: nat) \<le> a - b) = (a = 0 \<or> b = 0)" 1520 by arith 1521 1522lemma bottom_addr_only: 1523 "trace_addr tr i = None \<Longrightarrow> trace_bottom_addr tr i = Some nn 1524 \<Longrightarrow> \<exists>x x' xs. tr i = Some (x # x' # xs) \<and> nn = fst (last (x' # xs))" 1525 apply (clarsimp simp: trace_addr_def trace_bottom_addr_def 1526 split: option.split_asm list.split_asm) 1527 apply blast 1528 done 1529 1530lemma extended_pred_trace_drop_n: 1531 "trace_addr tr i = Some (NextNode n) 1532 \<Longrightarrow> trace_addr tr j = Some nn 1533 \<Longrightarrow> tr \<in> exec_trace Gamma fn \<Longrightarrow> Gamma fn = Some f 1534 \<Longrightarrow> wf_graph_function f ilen olen 1535 \<Longrightarrow> function_graph f n = Some (Call nn fname inputs outputs) 1536 \<Longrightarrow> Gamma fname = Some f' 1537 \<Longrightarrow> i < j \<Longrightarrow> nn \<noteq> Err 1538 \<Longrightarrow> trace_addr tr ` {Suc i ..< j} \<subseteq> {None} 1539 \<Longrightarrow> trace_bottom_addr tr ` {Suc i ..< j} \<subseteq> {Some (NextNode n)} 1540 \<Longrightarrow> trace_drop_n (Suc i) 1 tr \<in> exec_trace Gamma fname 1541 \<and> Suc i < j 1542 \<and> (\<exists>st g. trace_drop_n (Suc i) 1 tr (j - Suc (Suc i)) = Some [(Ret, st, g)]) 1543 \<and> trace_drop_n (Suc i) 1 tr (j - Suc i) = None" 1544 apply (clarsimp dest!: trace_addr_SomeD) 1545 apply (frule_tac i=i in exec_trace_invariant, simp) 1546 apply (simp add: exec_graph_invariant_Cons) 1547 apply (frule(3) exec_trace_drop_n, simp+) 1548 apply (rule context_conjI) 1549 apply (rule ccontr, simp add: linorder_not_less le_Suc_eq) 1550 apply (frule_tac i=i in exec_trace_step_cases, simp) 1551 apply (clarsimp simp: all_exec_graph_step_cases) 1552 apply (subgoal_tac "Suc (j - 2) = j - 1", simp_all) 1553 apply (rule context_conjI) 1554 prefer 2 1555 apply (clarsimp simp: trace_drop_n_def if_x_None_eq_Some) 1556 apply (rule_tac x="j - Suc (Suc i)" in exI, simp) 1557 apply (frule subsetD, rule_tac x="j - 1" and f="trace_addr tr" in imageI, simp) 1558 apply (frule subsetD, rule_tac x="j - 1" and f="trace_bottom_addr tr" in imageI, simp) 1559 apply (frule_tac i="j - 1" in exec_trace_step_cases) 1560 apply clarsimp 1561 apply (simp add: all_exec_graph_step_cases, safe; (solves \<open>simp add: trace_addr_def\<close>)?) 1562 apply (simp(no_asm) add: trace_drop_n_def if_x_None_eq_Some) 1563 apply clarsimp 1564 apply (cut_tac tr=tr and i="Suc (i + ja)" in bottom_addr_only) 1565 apply (simp add: image_subset_iff) 1566 apply (simp add: image_subset_iff) 1567 apply (cut_tac tr=tr and i="Suc (Suc (i + ja))" in bottom_addr_only) 1568 apply (simp add: image_subset_iff) 1569 apply (simp add: image_subset_iff) 1570 apply (clarsimp simp: continuing_def split: list.split next_node.split) 1571 apply (case_tac "drop 2 (the (tr (Suc (i + ja))))", simp_all) 1572 apply (frule_tac i="Suc (i + ja)" in exec_trace_step_cases) 1573 apply (frule_tac i="Suc (i + ja)" in exec_trace_invariant, simp) 1574 apply (auto simp: all_exec_graph_step_cases exec_graph_invariant_Cons 1575 split: graph_function.split_asm) 1576 done 1577 1578lemma restrs_condition_no_change: 1579 "restrs_condition tr restrs i 1580 \<Longrightarrow> j \<ge> i 1581 \<Longrightarrow> (\<forall>k \<in> {i ..< j}. trace_addr tr k = None) 1582 \<Longrightarrow> restrs_condition tr restrs j" 1583 apply (clarsimp simp: restrs_condition_def) 1584 apply (rule_tac P="\<lambda>S. card S \<in> SS" for SS in subst[rotated]) 1585 apply (erule spec) 1586 apply (auto intro: linorder_not_le[THEN iffD1, OF notI]) 1587 done 1588 1589lemma trace_end_exec_SomeI: 1590 "tr \<in> exec_trace Gamma fn 1591 \<Longrightarrow> tr i = Some stk 1592 \<Longrightarrow> tr (Suc i) = None 1593 \<Longrightarrow> trace_end tr = Some stk" 1594 apply (clarsimp simp: trace_end_def exI[where x="Suc i"]) 1595 apply (drule(1) exec_trace_None_dom_subset) 1596 apply (subst Max_eqI[where x=i], auto elim: finite_subset) 1597 done 1598 1599definition 1600 function_call_trace :: "nat \<Rightarrow> restrs \<Rightarrow> trace \<Rightarrow> trace option" 1601where 1602 "function_call_trace n restrs tr 1603 = (if pc' n restrs tr then Some (trace_drop_n 1604 (Suc (Least (\<lambda>i. trace_addr tr i = Some (NextNode n) \<and> restrs_condition tr restrs i))) 1 tr) 1605 else None)" 1606 1607lemma function_call_trace_eq: 1608 assumes tr: "tr \<in> exec_trace Gamma fname" 1609 "Gamma fname = Some f" 1610 "wf_graph_function f ilen olen" 1611 and i: "trace_addr tr i = Some (NextNode n)" 1612 "restrs_condition tr restrs i" 1613 and cut: "\<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y})" 1614 "(NextNode n, NextNode n) \<notin> trancl (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})" 1615 shows "function_call_trace n restrs tr = Some (trace_drop_n (Suc i) 1 tr)" 1616proof - 1617 1618 have P: "\<forall>j < i. trace_addr tr j = Some (NextNode n) 1619 \<longrightarrow> \<not> restrs_condition tr restrs j" 1620 using restrs_single_visit[OF tr _ _ i cut] 1621 by clarsimp 1622 1623 note eq = Least_equality[where x=i, OF _ ccontr, unfolded linorder_not_le] 1624 1625 show ?thesis using i 1626 apply (clarsimp simp: function_call_trace_def pc_def visit_known P 1627 dest!: trace_addr_SomeD) 1628 apply (subst eq, auto simp: i P) 1629 done 1630qed 1631 1632definition function_call_trace_embed :: "state option \<Rightarrow> trace \<Rightarrow> trace option 1633 \<Rightarrow> (string \<Rightarrow> graph_function option) \<Rightarrow> string \<Rightarrow> (state \<Rightarrow> variable) list \<Rightarrow> bool" 1634 where "function_call_trace_embed vis tr tr' Gamma f inps 1635 = (((vis = None) = (tr' = None)) \<and> (\<forall>tr''. tr' = Some tr'' 1636 \<longrightarrow> tr'' \<in> exec_trace Gamma f 1637 \<and> (trace_end tr'' = None \<longrightarrow> trace_end tr = None) 1638 \<and> (option_map (fst o hd) (trace_end tr'') = Some Err 1639 \<longrightarrow> option_map (fst o hd) (trace_end tr) = Some Err) 1640 \<and> length inps = length (function_inputs (the (Gamma f))) 1641 \<and> tr'' 0 = Some [init_state f (the (Gamma f)) (map (\<lambda>i. i (the vis)) inps)]))" 1642 1643lemma exec_trace_Err_propagate: 1644 "tr \<in> exec_trace Gamma f 1645 \<Longrightarrow> tr i = Some ((Err, st, fname) # xs) 1646 \<Longrightarrow> j \<le> length xs \<Longrightarrow> tr (i + j) = Some (upd_stack Err id (drop j ((Err, st, fname) # xs)))" 1647 apply (induct j arbitrary: xs) 1648 apply simp 1649 apply atomize 1650 apply clarsimp 1651 apply (cut_tac xs="drop j ((Err, st, fname) # xs)" in neq_Nil_conv) 1652 apply clarsimp 1653 apply (frule_tac i="i + j" in exec_trace_step_cases) 1654 apply (auto simp: exec_graph_step_def drop_eq_Cons Cons_eq_append_conv 1655 split: list.split_asm) 1656 done 1657 1658lemma trace_end_trace_drop_n_Err: 1659 "option_map (fst o hd) (trace_end (trace_drop_n i j tr)) = Some Err 1660 \<Longrightarrow> tr \<in> exec_trace Gamma f 1661 \<Longrightarrow> trace_drop_n i j tr \<in> exec_trace Gamma f' 1662 \<Longrightarrow> option_map (fst o hd) (trace_end tr) = Some Err" 1663 apply clarsimp 1664 apply (drule(1) exec_trace_end_SomeD) 1665 apply (clarsimp simp: trace_drop_n_def[THEN fun_cong] if_x_None_eq_Some 1666 drop_eq_Cons rev_swap) 1667 apply (frule(1) exec_trace_Err_propagate[OF _ _ order_refl]) 1668 apply (case_tac "tl (the (tr (n + i)))" rule: rev_cases) 1669 apply (frule_tac i="n + i" in exec_trace_step_cases) 1670 apply (clarsimp simp: exec_graph_step_def trace_end_exec_SomeI) 1671 apply (simp add: rev_swap) 1672 apply (frule_tac i="n + i + length (the (tr (n + i))) - 2" in exec_trace_step_cases) 1673 apply (frule_tac i="n + i + length (the (tr (n + i))) - 1" in exec_trace_step_cases) 1674 apply (clarsimp simp: exec_graph_step_def trace_end_exec_SomeI) 1675 done 1676 1677lemma trace_end_Nil: 1678 "tr \<in> exec_trace Gamma f 1679 \<Longrightarrow> trace_end tr \<noteq> Some []" 1680 by (auto dest: exec_trace_end_SomeD simp: exec_trace_Nil) 1681 1682lemma visit_Call_loop_lemma: 1683 "(nn, NextNode n) \<notin> rtrancl (reachable_step' f \<inter> S) 1684 \<Longrightarrow> function_graph f n = Some (Call nn fname inputs outputs) 1685 \<Longrightarrow> converse (reachable_step' f) `` {nn} \<subseteq> {NextNode n} 1686 \<Longrightarrow> (nn, nn) \<notin> trancl (reachable_step' f \<inter> S) 1687 \<and> (NextNode n, NextNode n) \<notin> trancl (reachable_step' f \<inter> S)" 1688 apply (simp add: not_trancl_converse_step) 1689 apply (clarsimp simp: reachable_step_def[THEN eqset_imp_iff] dest!: tranclD) 1690 apply (erule disjE, simp_all) 1691 apply (erule converse_rtranclE, simp_all add: reachable_step_def) 1692 done 1693 1694lemma pred_restrs_list: 1695 "pred_restrs nn (restrs_list xs) 1696 = restrs_list (map (\<lambda>(i, ns). (i, if nn = NextNode i 1697 then map (\<lambda>x. x - 1) (filter ((\<noteq>) 0) ns) else ns)) xs)" 1698 apply (clarsimp simp: pred_restrs_def split: next_node.split) 1699 apply (rule sym) 1700 apply (induct xs; simp, rule ext) 1701 apply (simp add: restrs_list_def) 1702 apply (clarsimp simp: restrs_list_Cons split del: if_split cong: if_cong) 1703 apply (auto intro: image_eqI[rotated]) 1704 done 1705 1706lemma pred_restrs_cut: 1707 "(\<exists>y. restrs x \<subseteq> {y}) \<Longrightarrow> (\<exists>y. pred_restrs nn restrs x \<subseteq> {y})" 1708 apply (clarsimp simp: pred_restrs_def split: next_node.split) 1709 apply blast 1710 done 1711 1712lemma pred_restrs_cut2: 1713 "\<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}) 1714 \<Longrightarrow> \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs nn restrs x \<subseteq> {y})" 1715 by (metis pred_restrs_cut) 1716 1717lemma visit_Call: 1718 "tr \<in> exec_trace Gamma fn \<Longrightarrow> Gamma fn = Some f 1719 \<Longrightarrow> wf_graph_function f ilen olen 1720 \<Longrightarrow> function_graph f n = Some (Call nn fname inputs outputs) 1721 \<Longrightarrow> Gamma fname = Some f' 1722 \<Longrightarrow> length inputs = length (function_inputs f') 1723 \<Longrightarrow> converse (reachable_step' f) `` {nn} \<subseteq> {NextNode n} 1724 \<Longrightarrow> nn \<noteq> NextNode (entry_point f) \<Longrightarrow> nn \<noteq> Err 1725 \<Longrightarrow> (nn, NextNode n) \<notin> rtrancl (reachable_step' f \<inter> {(x, y). x \<notin> set cuts}) 1726 \<Longrightarrow> \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}) 1727 \<Longrightarrow> let v = visit tr nn restrs; v' = visit tr (NextNode n) (pred_restrs' n restrs); 1728 tr' = function_call_trace n (pred_restrs' n restrs) tr 1729 in function_call_trace_embed v' tr tr' Gamma fname inputs 1730 \<and> v = option_map (\<lambda>st. return_vars (function_outputs f') outputs 1731 (fst (snd (hd (the (trace_end (the tr')))))) st) 1732 (option_guard (\<lambda>_. tr' \<noteq> None \<and> trace_end (the tr') \<noteq> None 1733 \<and> fst (hd (the (trace_end (the tr')))) = Ret) v')" 1734 apply (cases "visit tr (NextNode n) (pred_restrs' n restrs)", 1735 simp_all split del: if_split) 1736 apply (clarsimp simp: visit_eqs function_call_trace_embed_def) 1737 apply (rule context_conjI) 1738 apply (clarsimp simp: function_call_trace_def pc_def visit_eqs) 1739 apply clarsimp 1740 apply (frule(6) visit_extended_pred) 1741 apply clarsimp 1742 apply (drule visit_eqs[THEN iffD1]) 1743 apply (drule(2) visit_Call_loop_lemma) 1744 apply (frule_tac nn="NextNode n" in pred_restrs_cut2) 1745 apply (clarsimp simp: Let_def split del: if_split) 1746 apply (frule trace_addr_SomeD, clarsimp split del: if_split) 1747 apply (frule(1) exec_trace_invariant) 1748 apply (clarsimp simp: exec_graph_invariant_Cons split del: if_split) 1749 apply (frule(4) exec_trace_drop_n) 1750 apply (clarsimp simp: function_call_trace_eq visit_eqs Let_def 1751 simp del: imp_disjL split del: if_split) 1752 apply (rule conjI) 1753 apply (clarsimp simp: function_call_trace_embed_def simp del: map_option_eq_Some) 1754 apply (rule conjI, blast intro: trace_end_trace_drop_n_None) 1755 apply (rule conjI, metis trace_end_trace_drop_n_Err) 1756 apply (clarsimp simp: trace_drop_n_def) 1757 apply (frule_tac i=i in exec_trace_step_cases) 1758 apply (clarsimp simp: exec_graph_step_def init_state_def init_vars_def 1759 split: graph_function.split_asm dest!: trace_addr_SomeD) 1760 apply (simp del: imp_disjL) 1761 apply (rule conjI) 1762 apply (clarsimp simp: visit_eqs) 1763 apply (drule(1) exec_trace_end_SomeD, clarsimp) 1764 apply (frule(4) exec_trace_drop_n_rest[rule_format], simp) 1765 apply (frule_tac i="Suc i + na" in exec_trace_step_cases) 1766 apply (clarsimp simp: exec_graph_step_def split: graph_function.split_asm) 1767 apply (subgoal_tac "restrs_condition tr restrs (Suc (Suc i + na))") 1768 apply (rule exI, rule conjI, assumption) 1769 apply (clarsimp simp: trace_addr_SomeI) 1770 apply (drule(2) restrs_single_visit2[OF trace_addr_SomeI, OF exI], simp+)[1] 1771 apply (rule_tac i="Suc i" in restrs_condition_no_change) 1772 apply (simp add: pred_restrs[unfolded trace_bottom_addr_def]) 1773 apply simp 1774 apply clarsimp 1775 apply (rule ccontr, clarsimp dest!: trace_addr_SomeD) 1776 apply (case_tac "trace_drop_n (Suc i) 1 tr (k - Suc i)") 1777 apply simp 1778 apply (drule(1) exec_trace_None_dom_subset)+ 1779 apply auto[1] 1780 apply (frule(2) exec_trace_drop_n_rest[rule_format], fastforce, assumption+) 1781 apply (clarsimp simp: exec_trace_Nil) 1782 apply (intro impI allI notI conjI) 1783 1784 apply (clarsimp simp: visit_eqs) 1785 apply (rename_tac k) 1786 apply (frule(6) visit_extended_pred) 1787 apply clarsimp 1788 apply (drule(8) restrs_single_visit[rotated 3]) 1789 apply clarsimp 1790 apply (frule(10) extended_pred_trace_drop_n) 1791 apply (clarsimp simp: trace_end_exec_SomeI Suc_diff_Suc) 1792 done 1793 1794definition 1795 "double_function_call_trace vis trs = (case vis of (side, NextNode n, restrs) 1796 \<Rightarrow> function_call_trace n restrs (tuple_switch trs side) 1797 | _ \<Rightarrow> None)" 1798 1799lemma double_visit_None: 1800 "(double_visit vis trs = None) = (\<not> double_pc vis trs)" 1801 by (simp add: double_pc_def double_visit_def split: prod.split) 1802 1803lemma restr_trace_refine_Call_single: 1804 "\<not> fst ccall \<and> (\<exists>nn outps. get_function_call gfs ccall = Some (nn, cfname, cinps, outps)) 1805 \<Longrightarrow> Gamma1 cfname = Some cf \<Longrightarrow> wf_graph_function cf cilen colen 1806 \<Longrightarrow> fst acall \<and> (\<exists>nn outps. get_function_call gfs acall = Some (nn, afname, ainps, outps)) 1807 \<Longrightarrow> Gamma2 afname = Some af \<Longrightarrow> wf_graph_function af ailen aolen 1808 \<Longrightarrow> graph_function_refine prec Gamma1 cfname Gamma2 afname irel orel' 1809 \<Longrightarrow> double_pc ccall (tr, tr') \<longrightarrow> func_inputs_match gfs irel ccall acall (tr, tr') 1810 \<Longrightarrow> double_pc ccall (tr, tr') \<longrightarrow> double_pc acall (tr, tr') 1811 \<Longrightarrow> function_call_trace_embed (double_visit ccall (tr, tr')) tr 1812 (ctr (tr, tr')) Gamma1 cfname cinps 1813 \<Longrightarrow> function_call_trace_embed (double_visit acall (tr, tr')) tr' 1814 (ctr' (tr, tr')) Gamma2 afname ainps 1815 \<Longrightarrow> (double_pc ccall (tr, tr') \<longrightarrow> ctr (tr, tr') \<noteq> None \<and> ctr' (tr, tr') \<noteq> None 1816 \<and> trace_end (the (ctr (tr, tr'))) \<noteq> None 1817 \<and> trace_refine2 prec (cf, af) orel' 1818 (the (ctr (tr, tr'))) (the (ctr' (tr, tr')))) 1819 \<longrightarrow> restr_trace_refine prec Gamma1 f1 Gamma2 f2 rs1 rs2 orel tr tr' 1820 \<Longrightarrow> restr_trace_refine prec Gamma1 f1 Gamma2 f2 rs1 rs2 orel tr tr'" 1821 apply (clarsimp simp: restr_trace_refine_def) 1822 apply (case_tac "\<not> double_pc ccall (tr, tr')") 1823 apply (auto simp: double_trace_imp_def)[1] 1824 apply (clarsimp simp: function_call_trace_embed_def double_trace_imp_def double_visit_None) 1825 apply (drule(4) graph_function_refine_trace2[THEN iffD1, rotated -1, rule_format]) 1826 apply simp 1827 apply (rule conjI, assumption)+ 1828 apply simp 1829 apply (rule exI, rule conjI, rule refl, simp)+ 1830 apply (clarsimp simp: func_inputs_match_def) 1831 apply (erule rsubst[where P=irel]) 1832 apply (rule ext, simp add: tuple_switch_def switch_val_def) 1833 apply (case_tac "trace_end (the (ctr (tr, tr')))") 1834 apply (case_tac "trace_end (the (ctr' (tr, tr')))") 1835 apply (clarsimp simp: trace_refine2_def trace_refine_def) 1836 apply (clarsimp simp: trace_refine2_def trace_refine_def) 1837 apply (clarsimp simp: list.split[where P="Not", THEN consume_Not_eq] 1838 next_node.split[where P="Not", THEN consume_Not_eq] 1839 trace_end_Nil) 1840 apply (drule(1) exec_trace_end_SomeD)+ 1841 apply clarsimp 1842 apply clarsimp 1843 apply fastforce 1844 done 1845 1846definition split_visit_rel 1847 where "split_visit_rel rel ccall acall j trs 1848 = (double_pc (ccall j) trs \<and> double_pc (acall j) trs 1849 \<and> rel j (\<lambda>(x, y). the (double_visit ((tuple_switch (ccall, acall) x) 1850 (tuple_switch (0, j) y)) trs)))" 1851 1852lemma not_finite_two: 1853 "\<not> finite S \<Longrightarrow> \<exists>x y. x \<in> S \<and> y \<in> S \<and> x \<noteq> y" 1854 apply (case_tac "\<exists>x. x \<in> S") 1855 apply (rule ccontr, clarsimp) 1856 apply (erule notE, rule_tac B="{x}" in finite_subset) 1857 apply auto 1858 done 1859 1860definition 1861 induct_var :: "next_node \<Rightarrow> nat \<Rightarrow> bool" 1862where 1863 "induct_var nn n = True" 1864 1865lemma infinite_subset: 1866 "\<not> finite S \<Longrightarrow> S \<subseteq> T \<Longrightarrow> \<not> finite T" 1867 by (metis finite_subset) 1868 1869lemma restr_trace_refine_Split_orig: 1870 fixes rs1 rs2 hyps Gamma1 f1 Gamma2 f2 1871 defines "H trs \<equiv> 1872 exec_double_trace Gamma1 f1 Gamma2 f2 (fst trs) (snd trs) 1873 \<and> restrs_eventually_condition (fst trs) (restrs_list rs1) 1874 \<and> restrs_eventually_condition (snd trs) (restrs_list rs2)" 1875 assumes Suc: "\<forall>i. double_pc (ccall (Suc i)) (tr, tr') \<longrightarrow> double_pc (ccall i) (tr, tr')" 1876 and init: "\<forall>i. i < k \<longrightarrow> H (tr, tr') 1877 \<longrightarrow> double_pc (ccall i) (tr, tr') \<longrightarrow> split_visit_rel rel ccall acall i (tr, tr')" 1878 and induct: "\<forall>i. H (tr, tr') 1879 \<longrightarrow> double_pc (ccall (i + k)) (tr, tr') 1880 \<longrightarrow> (\<forall>j < k. split_visit_rel rel ccall acall (i + j) (tr, tr')) 1881 \<longrightarrow> split_visit_rel rel ccall acall (i + k) (tr, tr')" 1882 and distinct: "\<forall>tr i j k. restrs_condition tr (snd (snd (ccall i))) k 1883 \<longrightarrow> restrs_condition tr (snd (snd (ccall j))) k \<longrightarrow> i = j" 1884 "\<forall>tr i j k. restrs_condition tr (snd (snd (acall i))) k 1885 \<longrightarrow> restrs_condition tr (snd (snd (acall j))) k \<longrightarrow> i = j" 1886 and sides: "\<forall>i. \<not> fst (ccall i) \<and> fst (acall i)" 1887 and k: "k \<noteq> 0" 1888 and init_case: "\<not> double_pc (ccall k) (tr, tr') 1889 \<Longrightarrow> restr_trace_refine prec Gamma1 f1 Gamma2 f2 (restrs_list rs1) (restrs_list rs2) 1890 orel tr tr'" 1891 and induct_case: "\<And>i. induct_var (fst (snd (ccall 0))) i 1892 \<Longrightarrow> induct_var (fst (snd (acall 0))) i 1893 \<Longrightarrow> \<not> double_pc (ccall (i + k)) (tr, tr') 1894 \<Longrightarrow> \<forall>j < k. split_visit_rel rel ccall acall (i + j) (tr, tr') 1895 \<Longrightarrow> restr_trace_refine prec Gamma1 f1 Gamma2 f2 (restrs_list rs1) (restrs_list rs2) 1896 orel tr tr'" 1897 shows "restr_trace_refine prec Gamma1 f1 Gamma2 f2 (restrs_list rs1) (restrs_list rs2) orel tr tr'" 1898proof - 1899 have pc_ccall_less: "double_pc (ccall n) (tr, tr') 1900 \<longrightarrow> m \<le> n \<longrightarrow> double_pc (ccall m) (tr, tr')" for n m 1901 apply (induct_tac n, simp_all) 1902 apply clarsimp 1903 apply (frule Suc[rule_format]) 1904 apply (clarsimp simp: linorder_not_le Suc_le_eq[symmetric]) 1905 done 1906 1907 {fix i assume le[simp]: "i \<ge> k" 1908 note induct[rule_format, where i="i - k", simplified] 1909 } 1910 note induct_minus = this 1911 1912 {fix j 1913 have "double_pc (ccall j) (tr, tr') \<and> H (tr, tr') 1914 \<longrightarrow> split_visit_rel rel ccall acall j (tr, tr')" 1915 apply (induct j rule: nat_less_induct) 1916 apply (case_tac "n < k") 1917 apply (simp add: init) 1918 apply clarsimp 1919 apply (rule induct_minus, simp+) 1920 apply (simp add: field_simps pc_ccall_less) 1921 done 1922 } 1923 note rel_induct = this 1924 1925 note H_intro = H_def[THEN meta_eq_to_obj_eq, THEN iffD2, OF conjI] 1926 1927 have Suc_Max: "finite S \<Longrightarrow> Suc (Max S) \<notin> S" for S 1928 by (auto dest: Max_ge) 1929 1930 have unreached: 1931 "finite {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')} 1932 \<Longrightarrow> x \<in> {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')} 1933 \<Longrightarrow> \<not> double_pc (ccall (Max {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')} + k)) (tr, tr')" 1934 for x 1935 apply (frule Suc_Max) 1936 apply (frule Max_in, rule notI, clarsimp) 1937 apply clarsimp 1938 apply (case_tac k, simp_all) 1939 apply (auto dest!: less_Suc_eq[THEN iffD1]) 1940 done 1941 1942 have infinite_helper: 1943 "tr \<in> exec_trace G f 1944 \<Longrightarrow> \<forall>i j k. restrs_condition tr (snd (vis i)) k 1945 \<longrightarrow> restrs_condition tr (snd (vis j)) k \<longrightarrow> i = j 1946 \<Longrightarrow> \<not> finite {n. pc (fst (vis n)) (snd (vis n)) tr} 1947 \<Longrightarrow> trace_end tr = None" 1948 for tr G f and vis :: "'b \<Rightarrow> next_node \<times> (nat \<Rightarrow> nat set)" 1949 apply (clarsimp simp: trace_end_def) 1950 apply (drule(1) exec_trace_None_dom_subset) 1951 apply (drule_tac R="\<lambda>n i. restrs_condition tr (snd (vis n)) i" 1952 in pigeonhole_infinite_rel) 1953 apply (erule finite_subset, simp) 1954 apply (auto simp: pc_def visit_eqs dest!: trace_addr_SomeD)[1] 1955 apply (auto dest!: not_finite_two) 1956 done 1957 1958 have infinite: 1959 "exec_double_trace Gamma1 f1 Gamma2 f2 tr tr' 1960 \<Longrightarrow> H (tr, tr') 1961 \<Longrightarrow> \<not> finite {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')} 1962 \<Longrightarrow> trace_end tr = None \<and> trace_end tr' = None" 1963 apply (case_tac "\<exists>n. \<not> double_pc (ccall n) (tr, tr')") 1964 apply clarsimp 1965 apply (erule notE, rule_tac k1=n in finite_subset[OF _ finite_lessThan]) 1966 apply clarsimp 1967 apply (drule_tac x=0 in spec, simp add: k[simplified]) 1968 apply (rule ccontr, simp add: pc_ccall_less) 1969 apply clarsimp 1970 apply (rule conjI) 1971 apply (erule_tac vis="\<lambda>i. snd (ccall i)" in infinite_helper) 1972 apply (simp add: distinct) 1973 apply (simp add: double_pc_def[folded pc_def] split_def sides) 1974 apply (erule_tac vis="\<lambda>i. snd (acall i)" in infinite_helper) 1975 apply (simp add: distinct) 1976 apply clarsimp 1977 apply (drule_tac A="UNIV" in finite_subset[rotated]) 1978 apply clarsimp 1979 apply (rename_tac n, drule_tac x="n" in spec) 1980 apply (drule(1) rel_induct[rule_format, OF conjI]) 1981 apply (clarsimp simp: split_visit_rel_def) 1982 apply (simp add: double_pc_def[folded pc_def] sides split_def) 1983 apply simp 1984 done 1985 1986 show ?thesis 1987 apply (clarsimp simp: restr_trace_refine_def) 1988 apply (case_tac "\<not> double_pc (ccall k) (tr, tr')") 1989 apply (rule init_case[unfolded restr_trace_refine_def, rule_format], 1990 auto)[1] 1991 apply (case_tac "finite {n. \<forall>j < k. double_pc (ccall (n + j)) (tr, tr')}") 1992 apply (frule Max_in) 1993 apply simp 1994 apply (rule_tac x="0" in exI) 1995 apply (simp add: pc_ccall_less) 1996 apply (rule_tac i="Max {n. \<forall>j < k. double_pc (ccall (n + j)) (tr, tr')}" 1997 in induct_case[unfolded restr_trace_refine_def, rule_format]) 1998 apply (simp add: induct_var_def)+ 1999 apply (simp add: rel_induct unreached) 2000 apply (simp add: rel_induct unreached H_intro) 2001 apply auto[1] 2002 apply clarsimp 2003 apply (drule infinite[rotated -1], simp) 2004 apply (simp add: H_def) 2005 apply (simp add: trace_refine2_def trace_refine_def) 2006 done 2007qed 2008 2009lemma restrs_condition_unique: 2010 "restrs_condition tr (restrs_list ((n, [x]) # rs)) k 2011 \<Longrightarrow> restrs_condition tr (restrs_list ((n, [y]) # rs)) k 2012 \<Longrightarrow> x = y" 2013 by (clarsimp simp: restrs_condition_def restrs_list_Cons 2014 split: if_split_asm) 2015 2016abbreviation(input) 2017 "split_restr split_seq restrs i \<equiv> (restrs_list ((fst split_seq, 2018 [fst (snd split_seq) + i * snd (snd split_seq)]) # restrs))" 2019 2020abbreviation(input) 2021 "split_pc split_seq restrs tr i 2022 \<equiv> pc' (fst split_seq) (split_restr split_seq restrs i) tr" 2023 2024abbreviation(input) 2025 "split_visit split_seq restrs i tr 2026 \<equiv> visit tr (NextNode (fst split_seq)) (split_restr split_seq restrs i)" 2027 2028definition 2029 split_visit_rel' 2030 where "split_visit_rel' rel conc_seq abs_seq restrs trs j 2031 = (split_pc conc_seq (fst restrs) (fst trs) j \<and> split_pc abs_seq (snd restrs) (snd trs) j 2032 \<and> rel j (\<lambda>(x, y). the (split_visit (tuple_switch (conc_seq, abs_seq) x) 2033 (tuple_switch restrs x) 2034 (tuple_switch (0, j) y) (tuple_switch trs x))))" 2035 2036lemma split_visit_rel': 2037 "split_visit_rel rel (\<lambda>i. (False, NextNode (fst cseq), split_restr cseq rs1 i)) 2038 (\<lambda>i. (True, NextNode (fst aseq), split_restr aseq rs2 i)) j trs 2039 = split_visit_rel' rel cseq aseq (rs1, rs2) trs j" 2040 apply (simp add: split_visit_rel_def split_visit_rel'_def 2041 double_pc_def[folded pc_def] split_def double_visit_def) 2042 apply (auto elim!: rsubst[where P="rel j", OF _ ext]) 2043 apply (auto simp: tuple_switch_def switch_val_def) 2044 done 2045 2046theorem restr_trace_refine_Split: 2047 assumes Suc: "\<forall>i. split_pc conc_seq rs1 tr (Suc i) \<longrightarrow> split_pc conc_seq rs1 tr i" 2048 and init: "\<forall>i. i < k \<longrightarrow> split_pc conc_seq rs1 tr i 2049 \<longrightarrow> split_visit_rel' rel conc_seq abs_seq (rs1, rs2) (tr, tr') i" 2050 and induct: "\<forall>i. split_pc conc_seq rs1 tr (i + k) 2051 \<longrightarrow> (\<forall>j < k. split_visit_rel' rel conc_seq abs_seq (rs1, rs2) (tr, tr') (i + j)) 2052 \<longrightarrow> split_visit_rel' rel conc_seq abs_seq (rs1, rs2) (tr, tr') (i + k)" 2053 and zero: "k \<noteq> 0" "snd (snd conc_seq) \<noteq> 0" "snd (snd abs_seq) \<noteq> 0" 2054 and init_case: "\<not> split_pc conc_seq rs1 tr k 2055 \<Longrightarrow> restr_trace_refine prec Gamma1 f1 Gamma2 f2 (restrs_list rs1) (restrs_list rs2) 2056 orel tr tr'" 2057 and induct_case: "\<And>i. induct_var (NextNode (fst conc_seq)) i 2058 \<Longrightarrow> induct_var (NextNode (fst abs_seq)) i 2059 \<Longrightarrow> \<not> split_pc conc_seq rs1 tr (i + k) 2060 \<Longrightarrow> \<forall>j < k. split_visit_rel' rel conc_seq abs_seq (rs1, rs2) (tr, tr') (i + j) 2061 \<Longrightarrow> restr_trace_refine prec Gamma1 f1 Gamma2 f2 (restrs_list rs1) (restrs_list rs2) 2062 orel tr tr'" 2063 shows "restr_trace_refine prec Gamma1 f1 Gamma2 f2 (restrs_list rs1) (restrs_list rs2) orel tr tr'" 2064 apply (rule restr_trace_refine_Split_orig[where 2065 ccall="\<lambda>i. (False, NextNode (fst conc_seq), split_restr conc_seq rs1 i)" 2066 and acall="\<lambda>i. (True, NextNode (fst abs_seq), split_restr abs_seq rs2 i)" 2067 and k=k and rel=rel], 2068 simp_all add: Suc init induct init_case induct_case zero[simplified] 2069 double_pc_def[folded pc_def] split_visit_rel') 2070 apply (clarsimp, drule(1) restrs_condition_unique) 2071 apply (simp add: zero) 2072 apply (clarsimp, drule(1) restrs_condition_unique) 2073 apply (simp add: zero) 2074 done 2075 2076theorem restr_trace_refine_Split': 2077 "let cpc = split_pc conc_seq rs1 tr; 2078 rel = split_visit_rel' rel conc_seq abs_seq (rs1, rs2) (tr, tr') 2079 in (\<forall>i. cpc (Suc i) --> cpc i) 2080 --> (\<forall>i. i < k --> cpc i --> rel i) 2081 --> (\<forall>i. cpc (i + k) --> (\<forall>j < k. rel (i + j)) --> rel (i + k)) 2082 --> k \<noteq> 0 --> snd (snd conc_seq) \<noteq> 0 --> snd (snd abs_seq) \<noteq> 0 2083 --> (~ cpc k --> restr_trace_refine prec Gamma1 f1 Gamma2 f2 2084 (restrs_list rs1) (restrs_list rs2) orel tr tr') 2085 --> (\<forall>i. ~ cpc (i + k) --> (\<forall>j < k. rel (i + j)) 2086 --> restr_trace_refine prec Gamma1 f1 Gamma2 f2 2087 (restrs_list rs1) (restrs_list rs2) orel tr tr') 2088 --> restr_trace_refine prec Gamma1 f1 Gamma2 f2 2089 (restrs_list rs1) (restrs_list rs2) orel tr tr'" 2090 apply (clarsimp simp only: Let_def) 2091 apply (erule notE, rule restr_trace_refine_Split[where conc_seq=conc_seq and abs_seq=abs_seq 2092 and k=k and rel=rel], simp_all) 2093 apply blast 2094 done 2095 2096lemma restr_trace_refine_Restr1_offset: 2097 "induct_var (NextNode n) iv 2098 \<Longrightarrow> restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 (restrs_list ((n, [iv + 1 ..< iv + j]) # rs1)) rs2 orel tr tr' 2099 \<Longrightarrow> j \<noteq> 0 2100 \<Longrightarrow> distinct (map fst rs1) 2101 \<Longrightarrow> wf_graph_function f1 ilen olen \<Longrightarrow> Gamma1 fn1 = Some f1 2102 \<Longrightarrow> pc' n (restrs_list ((n, [iv]) # (restrs_visit rs1 (NextNode n) f1))) tr 2103 \<Longrightarrow> \<not> pc' n (restrs_list ((n, [iv + (j - 1)]) # (restrs_visit rs1 (NextNode n) f1))) tr 2104 \<Longrightarrow> restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 (restrs_list rs1) rs2 orel tr tr'" 2105 by (rule restr_trace_refine_Restr1[where i="iv + 1" and j="iv + j"], simp_all) 2106 2107lemma restr_trace_refine_Restr2_offset: 2108 "induct_var (NextNode n) iv 2109 \<Longrightarrow> restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 rs1 (restrs_list ((n, [iv + 1 ..< iv + j]) # rs2)) orel tr tr' 2110 \<Longrightarrow> j \<noteq> 0 2111 \<Longrightarrow> distinct (map fst rs2) 2112 \<Longrightarrow> wf_graph_function f2 ilen olen \<Longrightarrow> Gamma2 fn2 = Some f2 2113 \<Longrightarrow> pc' n (restrs_list ((n, [iv]) # (restrs_visit rs2 (NextNode n) f2))) tr' 2114 \<Longrightarrow> \<not> pc' n (restrs_list ((n, [iv + (j - 1)]) # (restrs_visit rs2 (NextNode n) f2))) tr' 2115 \<Longrightarrow> restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 rs1 (restrs_list rs2) orel tr tr'" 2116 by (rule restr_trace_refine_Restr2[where i="iv + 1" and j="iv + j"], simp_all) 2117 2118lemma restr_trace_refine_PCCases1: 2119 "pc nn rs1 tr 2120 \<longrightarrow> restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 rs1 rs2 orel tr tr' 2121 \<Longrightarrow> \<not> pc nn rs1 tr 2122 \<longrightarrow> restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 rs1 rs2 orel tr tr' 2123 \<Longrightarrow> restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 rs1 rs2 orel tr tr'" 2124 by metis 2125 2126lemma restr_trace_refine_PCCases2: 2127 "pc nn rs2 tr' 2128 \<longrightarrow> restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 rs1 rs2 orel tr tr' 2129 \<Longrightarrow> \<not> pc nn rs2 tr' 2130 \<longrightarrow> restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 rs1 rs2 orel tr tr' 2131 \<Longrightarrow> restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 rs1 rs2 orel tr tr'" 2132 by metis 2133 2134lemma restr_trace_refine_Err: 2135 "(\<not> pc Err restrs tr' 2136 \<longrightarrow> restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 rs1 rs2 orel tr tr') 2137 \<Longrightarrow> restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 rs1 rs2 orel tr tr'" 2138 apply (clarsimp simp: restr_trace_refine_def) 2139 apply (erule impCE) 2140 apply simp 2141 apply (clarsimp simp: trace_refine2_def trace_refine_def) 2142 apply (drule(1) pc_Ret_Err_trace_end[where er=Err, simplified]) 2143 apply clarsimp 2144 apply (simp split: option.split list.split next_node.split) 2145 apply auto 2146 done 2147 2148definition 2149 stepwise_graph_refine :: "(string \<Rightarrow> graph_function option) 2150 \<Rightarrow> (string list \<times> string list) 2151 \<Rightarrow> (next_node list \<times> next_node list) 2152 \<Rightarrow> (state list \<times> state list \<Rightarrow> bool) 2153 \<Rightarrow> ((next_node \<times> state \<times> string) \<times> (next_node \<times> state \<times> string) \<Rightarrow> bool) 2154 \<Rightarrow> (trace \<times> trace) option 2155 \<Rightarrow> nat \<Rightarrow> bool" 2156where 2157 "stepwise_graph_refine Gamma fnames nns irel orel trs n 2158 = (\<forall>tr tr' i j. i \<ge> n \<and> j \<ge> n \<and> tr i \<noteq> None \<and> tr' j \<noteq> None 2159 \<and> (map fst (the (tr i)), map fst (the (tr' j))) = nns 2160 \<and> (map (snd o snd) (the (tr i)), map (snd o snd) (the (tr' j))) = fnames 2161 \<and> irel (map (fst o snd) (the (tr i)), map (fst o snd) (the (tr' j))) 2162 \<and> (trs \<noteq> None \<longrightarrow> trs = Some (tr, tr')) 2163 \<and> tr \<in> exec_trace Gamma (last (fst fnames)) \<and> tr' \<in> exec_trace Gamma (last (snd fnames)) 2164 \<longrightarrow> (trace_end tr = None) = (trace_end tr' = None) 2165 \<and> (trace_end tr \<noteq> None \<longrightarrow> orel (hd (the (trace_end tr)), hd (the (trace_end tr')))))" 2166 2167lemmas stepwise_graph_refineI = stepwise_graph_refine_def[THEN iffD2, rule_format] 2168lemmas stepwise_graph_refineD = stepwise_graph_refine_def[THEN iffD1, rule_format] 2169 2170lemma stepwise_graph_refine_Basic: 2171 "stepwise_graph_refine Gamma (f1 # fns, f2 # fns') (nn # nns, nn' # nns') rel orel otr (Suc N) 2172 \<Longrightarrow> Gamma f1 = Some gf1 \<Longrightarrow> Gamma f2 = Some gf2 2173 \<Longrightarrow> function_graph gf1 n = Some (Basic nn upds) 2174 \<Longrightarrow> function_graph gf2 n' = Some (Basic nn' upds') 2175 \<Longrightarrow> \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> rel (upd_vars upds x # xs, upd_vars upds' y # ys) 2176 \<Longrightarrow> stepwise_graph_refine Gamma (f1 # fns, f2 # fns') 2177 (NextNode n # nns, NextNode n' # nns') rel orel otr N" 2178 apply (rule stepwise_graph_refineI) 2179 apply (erule_tac i="Suc i" and j="Suc j" in stepwise_graph_refineD) 2180 apply clarsimp 2181 apply (frule_tac i=i and tr=tr in exec_trace_step_cases) 2182 apply (frule_tac i=j and tr=tr' in exec_trace_step_cases) 2183 apply (clarsimp simp: exec_graph_step_def exec_graph_invariant_Cons split: graph_function.split_asm) 2184 apply (simp add: K_def) 2185 done 2186 2187lemma stepwise_graph_refine_Cond: 2188 "stepwise_graph_refine Gamma (f1 # fns, f2 # fns') (l # nns, l' # nns') rel orel otr (Suc N) 2189 \<Longrightarrow> stepwise_graph_refine Gamma (f1 # fns, f2 # fns') (r # nns, r' # nns') rel orel otr (Suc N) 2190 \<Longrightarrow> Gamma f1 = Some gf1 \<Longrightarrow> Gamma f2 = Some gf2 2191 \<Longrightarrow> function_graph gf1 n = Some (Cond l r cond) 2192 \<Longrightarrow> function_graph gf2 n' = Some (Cond l' r' cond') 2193 \<Longrightarrow> \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> cond x = cond' y 2194 \<Longrightarrow> stepwise_graph_refine Gamma (f1 # fns, f2 # fns') 2195 (NextNode n # nns, NextNode n' # nns') rel orel otr N" 2196 apply (rule stepwise_graph_refineI) 2197 apply (clarsimp simp del: last.simps not_None_eq) 2198 apply (frule_tac i=i and tr=tr in exec_trace_step_cases) 2199 apply (frule_tac i=j and tr=tr' in exec_trace_step_cases) 2200 apply (clarsimp simp: exec_graph_step_def exec_graph_invariant_Cons 2201 split: graph_function.split_asm split: if_split_asm 2202 simp del: last.simps not_None_eq) 2203 apply (simp_all only: exI all_simps[symmetric] simp_thms) 2204 apply (erule_tac i="Suc i" and j="Suc j" 2205 and nns="(l # xs, ys)" for xs ys in stepwise_graph_refineD, simp) 2206 apply (erule_tac i="Suc i" and j="Suc j" 2207 and nns="(r # xs, ys)" for xs ys in stepwise_graph_refineD, simp) 2208 done 2209 2210lemma stepwise_graph_refine_Call_same: 2211 "stepwise_graph_refine Gamma (f1 # fns, f2 # fns') (nn # nns, nn' # nns') rel orel otr (Suc N) 2212 \<Longrightarrow> Gamma f1 = Some gf1 \<Longrightarrow> Gamma f2 = Some gf2 2213 \<Longrightarrow> function_graph gf1 n = Some (Call nn fname inputs outputs) 2214 \<Longrightarrow> function_graph gf2 n' = Some (Call nn' fname inputs' outputs') 2215 \<Longrightarrow> Gamma fname = Some gf3 2216 \<Longrightarrow> \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs' 2217 \<Longrightarrow> \<forall>x xs y ys zs st. rel (x # xs, y # ys) 2218 \<longrightarrow> rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys) 2219 \<Longrightarrow> \<forall>sts. fst (fst sts) = Err \<longrightarrow> fst (snd sts) = Err \<longrightarrow> orel sts 2220 \<Longrightarrow> stepwise_graph_refine Gamma (f1 # fns, f2 # fns') 2221 (NextNode n # nns, NextNode n' # nns') rel orel otr N" 2222 apply (rule stepwise_graph_refineI, clarsimp) 2223 apply (simp only: all_simps[symmetric]) 2224 apply (frule(4) exec_trace_drop_n_Cons[where gf=gf1]) 2225 apply (frule(4) exec_trace_drop_n_Cons[where gf=gf2]) 2226 apply (frule_tac i=i and tr=tr in exec_trace_step_cases) 2227 apply (frule_tac i=j and tr=tr' in exec_trace_step_cases) 2228 apply (clarsimp simp: exec_graph_step_def init_vars_def 2229 split: graph_function.split_asm) 2230 apply (subgoal_tac "trace_drop_n (Suc i) (length (the (tr i))) tr 2231 = trace_drop_n (Suc j) (length (the (tr' j))) tr'") 2232 apply (frule_tac f=trace_end in arg_cong) 2233 apply (drule fun_eq_iff[THEN iffD1]) 2234 apply (case_tac "trace_end (trace_drop_n (Suc i) (length (the (tr i))) tr)") 2235 apply simp 2236 apply (drule(1) trace_end_trace_drop_n_None, simp)+ 2237 apply simp 2238 apply clarsimp 2239 apply (drule(1) exec_trace_end_SomeD)+ 2240 apply clarsimp 2241 apply (erule disjE) 2242 apply (frule_tac tr=tr and i=i and k=na in exec_trace_drop_n_rest_Cons[rule_format], 2243 (simp only: function_graph.simps)+) 2244 apply (frule_tac tr=tr' and i=j and k=na in exec_trace_drop_n_rest_Cons[rule_format], 2245 (simp only: function_graph.simps)+) 2246 apply (frule_tac i="Suc i + na" and tr=tr in exec_trace_step_cases) 2247 apply (frule_tac i="Suc j + na" and tr=tr' in exec_trace_step_cases) 2248 apply (clarsimp simp: field_simps exec_graph_step_def) 2249 apply (drule_tac tr=tr and tr'=tr' and i="i + na + 2" and j="j + na + 2" 2250 in stepwise_graph_refineD) 2251 apply (simp add: ) 2252 apply auto[1] 2253 apply auto[1] 2254 apply (drule(1) trace_end_trace_drop_n_Err[rotated], simp add: trace_end_exec_SomeI)+ 2255 apply (case_tac "hd (the (trace_end tr))") 2256 apply (case_tac "hd (the (trace_end tr'))") 2257 apply clarsimp 2258 apply (rule ext) 2259 apply (rule exec_trace_deterministic, simp+) 2260 apply (simp add: trace_drop_n_def) 2261 apply (simp only: all_simps[symmetric]) 2262 done 2263 2264lemma stepwise_graph_refine_nop_left: 2265 "stepwise_graph_refine Gamma (f1 # fns, fns') (nn # nns, nns') rel orel otr N 2266 \<Longrightarrow> Gamma f1 = Some gf1 2267 \<Longrightarrow> function_graph gf1 n = Some (Basic nn []) 2268 \<Longrightarrow> stepwise_graph_refine Gamma (f1 # fns, fns') 2269 (NextNode n # nns, nns') rel orel otr N" 2270 apply (rule stepwise_graph_refineI) 2271 apply (erule_tac i="Suc i" and j="j" in stepwise_graph_refineD) 2272 apply clarsimp 2273 apply (frule_tac i=i and tr=tr in exec_trace_step_cases) 2274 apply (clarsimp simp: exec_graph_step_def exec_graph_invariant_Cons split: graph_function.split_asm) 2275 apply (simp add: K_def upd_vars_def save_vals_def) 2276 done 2277 2278lemma stepwise_graph_refine_flip: 2279 "stepwise_graph_refine Gamma (fns', fns) (nns', nns) 2280 (\<lambda>x. rel (snd x, fst x)) (\<lambda>x. orel (snd x, fst x)) (option_map (\<lambda>x. (snd x, fst x)) otr) N 2281 = stepwise_graph_refine Gamma (fns, fns') (nns, nns') rel orel otr N" 2282 apply (intro iffI stepwise_graph_refineI) 2283 apply (frule_tac i=j and j=i and tr=tr' and tr'=tr in stepwise_graph_refineD) 2284 apply simp 2285 apply auto[1] 2286 apply (frule_tac i=j and j=i and tr=tr' and tr'=tr in stepwise_graph_refineD) 2287 apply simp 2288 apply auto[1] 2289 done 2290 2291lemma stepwise_graph_refine_nop_right: 2292 "stepwise_graph_refine Gamma (fns, f2 # fns') (nns, nn' # nns') rel orel otr N 2293 \<Longrightarrow> Gamma f2 = Some gf2 2294 \<Longrightarrow> function_graph gf2 n' = Some (Basic nn' []) 2295 \<Longrightarrow> stepwise_graph_refine Gamma (fns, f2 # fns') 2296 (nns, NextNode n' # nns') rel orel otr N" 2297 apply (rule stepwise_graph_refineI) 2298 apply (erule_tac i="i" and j="Suc j" in stepwise_graph_refineD) 2299 apply clarsimp 2300 apply (frule_tac i=j and tr=tr' in exec_trace_step_cases) 2301 apply (clarsimp simp: exec_graph_step_def exec_graph_invariant_Cons split: graph_function.split_asm) 2302 apply (simp add: K_def upd_vars_def save_vals_def) 2303 done 2304 2305lemma stepwise_graph_refine_inline_left: 2306 "stepwise_graph_refine Gamma (fname # f1 # fns, f2 # fns') 2307 (NextNode (entry_point gf3) # NextNode n # nns, nn' # nns') 2308 rel' orel otr (Suc N) 2309 \<Longrightarrow> Gamma f1 = Some gf1 \<Longrightarrow> Gamma f2 = Some gf2 2310 \<Longrightarrow> function_graph gf1 n = Some (Call nn fname inputs outputs) 2311 \<Longrightarrow> function_graph gf2 n' = Some (Basic nn' upds) 2312 \<Longrightarrow> Gamma fname = Some gf3 2313 \<Longrightarrow> \<forall>x xs y ys. rel (x # xs, y # ys) 2314 \<longrightarrow> rel' (init_vars (function_inputs gf3) inputs x # x # xs, upd_vars upds y # ys) 2315 \<Longrightarrow> stepwise_graph_refine Gamma (f1 # fns, f2 # fns') 2316 (NextNode n # nns, NextNode n' # nns') rel orel otr N" 2317 apply (rule stepwise_graph_refineI) 2318 apply (erule_tac i="Suc i" and j="Suc j" in stepwise_graph_refineD) 2319 apply clarsimp 2320 apply (frule_tac i=i and tr=tr in exec_trace_step_cases) 2321 apply (frule_tac i=j and tr=tr' in exec_trace_step_cases) 2322 apply (clarsimp simp: exec_graph_step_def exec_graph_invariant_Cons split: graph_function.split_asm) 2323 apply (simp add: K_def) 2324 done 2325 2326lemma stepwise_graph_refine_end_inline_left: 2327 "stepwise_graph_refine Gamma (f1 # fns, f2 # fns') 2328 (nn # nns, nn' # nns') 2329 rel' orel otr (Suc N) 2330 \<Longrightarrow> Gamma f1 = Some gf1 \<Longrightarrow> Gamma f2 = Some gf2 2331 \<Longrightarrow> function_graph gf1 n = Some (Call nn fname inputs outputs) 2332 \<Longrightarrow> function_graph gf2 n' = Some (Basic nn' upds) 2333 \<Longrightarrow> Gamma fname = Some gf3 2334 \<Longrightarrow> \<forall>x x' xs y ys. rel (x # x' # xs, y # ys) 2335 \<longrightarrow> rel' (return_vars (function_outputs gf3) outputs x x' # xs, upd_vars upds y # ys) 2336 \<Longrightarrow> stepwise_graph_refine Gamma (fname # f1 # fns, f2 # fns') 2337 (Ret # NextNode n # nns, NextNode n' # nns') rel orel otr N" 2338 apply (rule stepwise_graph_refineI) 2339 apply (erule_tac i="Suc i" and j="Suc j" in stepwise_graph_refineD) 2340 apply clarsimp 2341 apply (frule_tac i=i and tr=tr in exec_trace_step_cases) 2342 apply (frule_tac i=j and tr=tr' in exec_trace_step_cases) 2343 apply (clarsimp simp: exec_graph_step_def exec_graph_invariant_Cons split: graph_function.split_asm) 2344 apply (simp add: K_def) 2345 done 2346 2347lemma stepwise_graph_refine_inline_right: 2348 "stepwise_graph_refine Gamma (f1 # fns, fname # f2 # fns') 2349 (nn # nns, NextNode (entry_point gf3) # NextNode n' # nns') 2350 rel' orel otr (Suc N) 2351 \<Longrightarrow> Gamma f1 = Some gf1 \<Longrightarrow> Gamma f2 = Some gf2 2352 \<Longrightarrow> function_graph gf1 n = Some (Basic nn upds) 2353 \<Longrightarrow> function_graph gf2 n' = Some (Call nn' fname inputs outputs) 2354 \<Longrightarrow> Gamma fname = Some gf3 2355 \<Longrightarrow> \<forall>x xs y ys. rel (x # xs, y # ys) 2356 \<longrightarrow> rel' (upd_vars upds x # xs, init_vars (function_inputs gf3) inputs y # y # ys) 2357 \<Longrightarrow> stepwise_graph_refine Gamma (f1 # fns, f2 # fns') 2358 (NextNode n # nns, NextNode n' # nns') rel orel otr N" 2359 apply (rule stepwise_graph_refineI) 2360 apply (erule_tac i="Suc i" and j="Suc j" in stepwise_graph_refineD) 2361 apply clarsimp 2362 apply (frule_tac i=i and tr=tr in exec_trace_step_cases) 2363 apply (frule_tac i=j and tr=tr' in exec_trace_step_cases) 2364 apply (clarsimp simp: exec_graph_step_def exec_graph_invariant_Cons split: graph_function.split_asm) 2365 apply (simp add: K_def) 2366 done 2367 2368lemma stepwise_graph_refine_end_inline_right: 2369 "stepwise_graph_refine Gamma (f1 # fns, f2 # fns') 2370 (nn # nns, nn' # nns') 2371 rel' orel otr (Suc N) 2372 \<Longrightarrow> Gamma f1 = Some gf1 \<Longrightarrow> Gamma f2 = Some gf2 2373 \<Longrightarrow> function_graph gf1 n = Some (Basic nn upds) 2374 \<Longrightarrow> function_graph gf2 n' = Some (Call nn' fname inputs outputs) 2375 \<Longrightarrow> Gamma fname = Some gf3 2376 \<Longrightarrow> \<forall>x xs y y' ys. rel (x # xs, y # y' # ys) 2377 \<longrightarrow> rel' (upd_vars upds x # xs, return_vars (function_outputs gf3) outputs y y' # ys) 2378 \<Longrightarrow> stepwise_graph_refine Gamma (f1 # fns, fname # f2 # fns') 2379 (NextNode n # nns, Ret # NextNode n' # nns') rel orel otr N" 2380 apply (rule stepwise_graph_refineI) 2381 apply (erule_tac i="Suc i" and j="Suc j" in stepwise_graph_refineD) 2382 apply clarsimp 2383 apply (frule_tac i=i and tr=tr in exec_trace_step_cases) 2384 apply (frule_tac i=j and tr=tr' in exec_trace_step_cases) 2385 apply (clarsimp simp: exec_graph_step_def exec_graph_invariant_Cons split: graph_function.split_asm) 2386 apply (simp add: K_def) 2387 done 2388 2389lemma stepwise_graph_refine_induct: 2390 assumes Suc: "\<And>n otr. stepwise_graph_refine Gamma fns nns rel orel otr (Suc n) 2391 \<Longrightarrow> stepwise_graph_refine Gamma fns nns rel orel otr n" 2392 shows "stepwise_graph_refine Gamma fns nns rel orel otr n" 2393proof - 2394 have induct: "\<And>n m otr. n \<ge> m 2395 \<Longrightarrow> stepwise_graph_refine Gamma fns nns rel orel otr n 2396 \<Longrightarrow> stepwise_graph_refine Gamma fns nns rel orel otr m" 2397 by (erule(1) inc_induct, erule Suc) 2398 2399 show ?thesis 2400 apply (rule stepwise_graph_refineI) 2401 apply (simp add: prod_eq_iff) 2402 apply (case_tac "\<exists>N. (\<forall>i \<ge> N. tr i = None) \<or> (\<forall>i \<ge> N. tr' i = None)") 2403 apply clarsimp 2404 apply (cut_tac n="Suc N" and m="n" and otr="Some (tr, tr')" in induct) 2405 apply (rule ccontr, auto)[1] 2406 apply (auto simp add: stepwise_graph_refine_def)[1] 2407 apply (drule_tac tr=tr and tr'=tr' in stepwise_graph_refineD, (erule conjI)+) 2408 apply simp 2409 apply simp 2410 apply (case_tac "trace_end tr") 2411 apply (rule ccontr, clarsimp) 2412 apply (frule(1) exec_trace_end_SomeD, clarsimp) 2413 apply (frule(1) exec_trace_None_dom_subset) 2414 apply (drule_tac x="Suc na" in spec) 2415 apply auto[1] 2416 apply clarsimp 2417 apply (frule(1) exec_trace_end_SomeD, clarsimp) 2418 apply (frule(1) exec_trace_None_dom_subset) 2419 apply (drule_tac x="Suc na" in spec) 2420 apply auto[1] 2421 done 2422qed 2423 2424end 2425