src/HOL/IMP/Denotational.thy
changeset 52401 56e83c57f953
parent 52396 432777f2e372
child 52402 c2f30ba4bb98
equal deleted inserted replaced
52400:ded7b9c60dc2 52401:56e83c57f953
    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