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