equal
deleted
inserted
replaced
154 |
154 |
155 (* ------------------------------------------------------ |
155 (* ------------------------------------------------------ |
156 Lemma 1 :Traces coincide |
156 Lemma 1 :Traces coincide |
157 ------------------------------------------------------- *) |
157 ------------------------------------------------------- *) |
158 |
158 |
|
159 Delsplits[expand_if]; |
159 goal thy |
160 goal thy |
160 "!!f.[|is_simulation R C A; ext C = ext A|] ==> \ |
161 "!!f.[|is_simulation R C A; ext C = ext A|] ==> \ |
161 \ !s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'): R --> \ |
162 \ !s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'): R --> \ |
162 \ mk_trace C`ex = mk_trace A`((corresp_ex_simC A R`ex) s')"; |
163 \ mk_trace C`ex = mk_trace A`((corresp_ex_simC A R`ex) s')"; |
163 |
164 |
176 by (asm_full_simp_tac (simpset() addsimps |
177 by (asm_full_simp_tac (simpset() addsimps |
177 [rewrite_rule [Let_def] move_subprop5_sim, |
178 [rewrite_rule [Let_def] move_subprop5_sim, |
178 rewrite_rule [Let_def] move_subprop4_sim] |
179 rewrite_rule [Let_def] move_subprop4_sim] |
179 setloop split_tac [expand_if] ) 1); |
180 setloop split_tac [expand_if] ) 1); |
180 qed_spec_mp"traces_coincide_sim"; |
181 qed_spec_mp"traces_coincide_sim"; |
|
182 Addsplits[expand_if]; |
181 |
183 |
182 |
184 |
183 (* ----------------------------------------------------------- *) |
185 (* ----------------------------------------------------------- *) |
184 (* Lemma 2 : corresp_ex_sim is execution *) |
186 (* Lemma 2 : corresp_ex_sim is execution *) |
185 (* ----------------------------------------------------------- *) |
187 (* ----------------------------------------------------------- *) |