equal
deleted
inserted
replaced
399 lemma effNone: |
399 lemma effNone: |
400 "(pc', s') \<in> set (eff i G pc et None) \<Longrightarrow> s' = None" |
400 "(pc', s') \<in> set (eff i G pc et None) \<Longrightarrow> s' = None" |
401 by (auto simp add: eff_def xcpt_eff_def norm_eff_def) |
401 by (auto simp add: eff_def xcpt_eff_def norm_eff_def) |
402 |
402 |
403 |
403 |
404 text {* some helpers to make the specification directly executable: *} |
|
405 declare list_all2_Nil [code] |
|
406 declare list_all2_Cons [code] |
|
407 |
|
408 lemma xcpt_app_lemma [code]: |
404 lemma xcpt_app_lemma [code]: |
409 "xcpt_app i G pc et = list_all (is_class G) (xcpt_names (i, G, pc, et))" |
405 "xcpt_app i G pc et = list_all (is_class G) (xcpt_names (i, G, pc, et))" |
410 by (simp add: list_all_iff) |
406 by (simp add: list_all_iff) |
411 |
407 |
412 lemmas [simp del] = app_def xcpt_app_def |
408 lemmas [simp del] = app_def xcpt_app_def |