src/HOL/IMP/Denotation.thy
changeset 45015 fdac1e9880eb
parent 43144 631dd866b284
child 52046 bc01725d7918
equal deleted inserted replaced
45014:0e847655b2d8 45015:fdac1e9880eb
    30 done
    30 done
    31 
    31 
    32 text{* Equivalence of denotational and big-step semantics: *}
    32 text{* Equivalence of denotational and big-step semantics: *}
    33 
    33 
    34 lemma com1: "(c,s) \<Rightarrow> t \<Longrightarrow> (s,t) \<in> C(c)"
    34 lemma com1: "(c,s) \<Rightarrow> t \<Longrightarrow> (s,t) \<in> C(c)"
    35 apply (induct rule: big_step_induct)
    35 apply (induction rule: big_step_induct)
    36 apply auto
    36 apply auto
    37 (* while *)
    37 (* while *)
    38 apply (unfold Gamma_def)
    38 apply (unfold Gamma_def)
    39 apply (subst lfp_unfold[OF Gamma_mono, simplified Gamma_def])
    39 apply (subst lfp_unfold[OF Gamma_mono, simplified Gamma_def])
    40 apply fast
    40 apply fast
    41 apply (subst lfp_unfold[OF Gamma_mono, simplified Gamma_def])
    41 apply (subst lfp_unfold[OF Gamma_mono, simplified Gamma_def])
    42 apply auto 
    42 apply auto 
    43 done
    43 done
    44 
    44 
    45 lemma com2: "(s,t) \<in> C(c) \<Longrightarrow> (c,s) \<Rightarrow> t"
    45 lemma com2: "(s,t) \<in> C(c) \<Longrightarrow> (c,s) \<Rightarrow> t"
    46 apply (induct c arbitrary: s t)
    46 apply (induction c arbitrary: s t)
    47 apply auto 
    47 apply auto 
    48 apply blast
    48 apply blast
    49 (* while *)
    49 (* while *)
    50 apply (erule lfp_induct2 [OF _ Gamma_mono])
    50 apply (erule lfp_induct2 [OF _ Gamma_mono])
    51 apply (unfold Gamma_def)
    51 apply (unfold Gamma_def)