src/HOL/IMP/Denotation.thy
 changeset 43144 631dd866b284 parent 43143 1aeafba76f21 child 45015 fdac1e9880eb
equal inserted replaced
43143:1aeafba76f21 43144:631dd866b284
`    18 "C (IF b THEN c1 ELSE c2) = {(s,t). (s,t) \<in> C c1 \<and> bval b s} \<union>`
`    18 "C (IF b THEN c1 ELSE c2) = {(s,t). (s,t) \<in> C c1 \<and> bval b s} \<union>`
`    19                             {(s,t). (s,t) \<in> C c2 \<and> \<not>bval b s}" |`
`    19                             {(s,t). (s,t) \<in> C c2 \<and> \<not>bval b s}" |`
`    20 "C(WHILE b DO c) = lfp (Gamma b (C c))"`
`    20 "C(WHILE b DO c) = lfp (Gamma b (C c))"`
`    21 `
`    21 `
`    22 `
`    22 `
`    25 lemma Gamma_mono: "mono (Gamma b c)"`
`    23 lemma Gamma_mono: "mono (Gamma b c)"`
`    26 by (unfold Gamma_def mono_def) fast`
`    24 by (unfold Gamma_def mono_def) fast`
`    27 `
`    25 `
`    28 lemma C_While_If: "C(WHILE b DO c) = C(IF b THEN c;WHILE b DO c ELSE SKIP)"`
`    26 lemma C_While_If: "C(WHILE b DO c) = C(IF b THEN c;WHILE b DO c ELSE SKIP)"`
`    29 apply simp`
`    27 apply simp`
`    30 apply (subst lfp_unfold [OF Gamma_mono])  --{*lhs only*}`
`    28 apply (subst lfp_unfold [OF Gamma_mono])  --{*lhs only*}`
`    31 apply (simp add: Gamma_def)`
`    29 apply (simp add: Gamma_def)`
`    32 done`
`    30 done`
`    33 `
`    31 `
`    34 (* Operational Semantics implies Denotational Semantics *)`
`    32 text{* Equivalence of denotational and big-step semantics: *}`
`    35 `
`    33 `
`    36 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)"`
`    38 apply (induct rule: big_step_induct)`
`    35 apply (induct rule: big_step_induct)`
`    39 apply auto`
`    36 apply auto`
`    40 (* while *)`
`    37 (* while *)`
`    41 apply (unfold Gamma_def)`
`    38 apply (unfold Gamma_def)`
`    42 apply (subst lfp_unfold[OF Gamma_mono, simplified Gamma_def])`
`    39 apply (subst lfp_unfold[OF Gamma_mono, simplified Gamma_def])`
`    43 apply fast`
`    40 apply fast`
`    44 apply (subst lfp_unfold[OF Gamma_mono, simplified Gamma_def])`
`    41 apply (subst lfp_unfold[OF Gamma_mono, simplified Gamma_def])`
`    45 apply auto `
`    42 apply auto `
`    46 done`
`    43 done`
`    49 `
`    44 `
`    50 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"`
`    51 apply (induct c arbitrary: s t)`
`    46 apply (induct c arbitrary: s t)`
`    52 apply auto `
`    47 apply auto `
`    53 apply blast`
`    48 apply blast`
`    55 apply (erule lfp_induct2 [OF _ Gamma_mono])`
`    50 apply (erule lfp_induct2 [OF _ Gamma_mono])`
`    56 apply (unfold Gamma_def)`
`    51 apply (unfold Gamma_def)`
`    57 apply auto`
`    52 apply auto`
`    58 done`
`    53 done`
`    59 `
`    54 `
`    60 `
`    55 lemma denotational_is_big_step: "(s,t) \<in> C(c)  =  ((c,s) \<Rightarrow> t)"`
`    61 (**** Proof of Equivalence ****)`
`       `
`    62 `
`       `
`    63 lemma denotational_is_natural: "(s,t) \<in> C(c)  =  ((c,s) \<Rightarrow> t)"`
`       `
`    64 by (fast elim: com2 dest: com1)`
`    56 by (fast elim: com2 dest: com1)`
`    65 `
`    57 `
`    66 end`
`    58 end`