equal
deleted
inserted
replaced
56 qed (auto split: if_splits) |
56 qed (auto split: if_splits) |
57 |
57 |
58 theorem denotational_is_big_step: |
58 theorem denotational_is_big_step: |
59 "(s,t) \<in> D(c) = ((c,s) \<Rightarrow> t)" |
59 "(s,t) \<in> D(c) = ((c,s) \<Rightarrow> t)" |
60 by (metis D_if_big_step Big_step_if_D[simplified]) |
60 by (metis D_if_big_step Big_step_if_D[simplified]) |
|
61 |
|
62 corollary equiv_c_iff_equal_D: "(c1 \<sim> c2) \<longleftrightarrow> D c1 = D c2" |
|
63 by(simp add: denotational_is_big_step[symmetric] set_eq_iff) |
61 |
64 |
62 |
65 |
63 subsection "Continuity" |
66 subsection "Continuity" |
64 |
67 |
65 definition chain :: "(nat \<Rightarrow> 'a set) \<Rightarrow> bool" where |
68 definition chain :: "(nat \<Rightarrow> 'a set) \<Rightarrow> bool" where |