59 apply (simp add: is_live_ref_map_def live_implements_def livetraces_def liveexecutions_def) |
59 apply (simp add: is_live_ref_map_def live_implements_def livetraces_def liveexecutions_def) |
60 apply auto |
60 apply auto |
61 apply (rule_tac x = "corresp_ex A f ex" in exI) |
61 apply (rule_tac x = "corresp_ex A f ex" in exI) |
62 apply auto |
62 apply auto |
63 (* Traces coincide, Lemma 1 *) |
63 (* Traces coincide, Lemma 1 *) |
64 apply (tactic {* pair_tac @{context} "ex" 1 *}) |
64 apply (tactic \<open>pair_tac @{context} "ex" 1\<close>) |
65 apply (erule lemma_1 [THEN spec, THEN mp]) |
65 apply (erule lemma_1 [THEN spec, THEN mp]) |
66 apply (simp (no_asm) add: externals_def) |
66 apply (simp (no_asm) add: externals_def) |
67 apply (auto)[1] |
67 apply (auto)[1] |
68 apply (simp add: executions_def reachable.reachable_0) |
68 apply (simp add: executions_def reachable.reachable_0) |
69 |
69 |
70 (* corresp_ex is execution, Lemma 2 *) |
70 (* corresp_ex is execution, Lemma 2 *) |
71 apply (tactic {* pair_tac @{context} "ex" 1 *}) |
71 apply (tactic \<open>pair_tac @{context} "ex" 1\<close>) |
72 apply (simp add: executions_def) |
72 apply (simp add: executions_def) |
73 (* start state *) |
73 (* start state *) |
74 apply (rule conjI) |
74 apply (rule conjI) |
75 apply (simp add: is_ref_map_def corresp_ex_def) |
75 apply (simp add: is_ref_map_def corresp_ex_def) |
76 (* is-execution-fragment *) |
76 (* is-execution-fragment *) |