equal
deleted
inserted
replaced
203 auto(); |
203 auto(); |
204 qed"execfrag_prefixclosed"; |
204 qed"execfrag_prefixclosed"; |
205 |
205 |
206 bind_thm ("exec_prefixclosed",conjI RS (execfrag_prefixclosed RS spec RS spec RS mp)); |
206 bind_thm ("exec_prefixclosed",conjI RS (execfrag_prefixclosed RS spec RS spec RS mp)); |
207 |
207 |
|
208 |
|
209 (* second prefix notion for Finite x *) |
|
210 |
|
211 goal thy "! y s.is_execution_fragment A (s,x@@y) --> is_execution_fragment A (s,x)"; |
|
212 by (pair_induct_tac "x" [is_execution_fragment_def] 1); |
|
213 by (strip_tac 1); |
|
214 by (Seq_case_simp_tac "s" 1); |
|
215 by (pair_tac "a" 1); |
|
216 auto(); |
|
217 qed_spec_mp"exec_prefix2closed"; |
|
218 |