src/HOL/IMP/Denotation.thy
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 45015 fdac1e9880eb
child 52046 bc01725d7918
permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
nipkow@43143
     1
(* Authors: Heiko Loetzbeyer, Robert Sandner, Tobias Nipkow *)
clasohm@924
     2
kleing@12431
     3
header "Denotational Semantics of Commands"
clasohm@924
     4
nipkow@43143
     5
theory Denotation imports Big_Step begin
kleing@12431
     6
wenzelm@42174
     7
type_synonym com_den = "(state \<times> state) set"
nipkow@1696
     8
wenzelm@27362
     9
definition
nipkow@43143
    10
  Gamma :: "bexp \<Rightarrow> com_den \<Rightarrow> (com_den \<Rightarrow> com_den)" where
nipkow@43143
    11
  "Gamma b cd = (\<lambda>phi. {(s,t). (s,t) \<in> (cd O phi) \<and> bval b s} \<union>
nipkow@43143
    12
                       {(s,t). s=t \<and> \<not>bval b s})"
wenzelm@18372
    13
nipkow@43143
    14
fun C :: "com \<Rightarrow> com_den" where
nipkow@43143
    15
"C SKIP   = Id" |
nipkow@43143
    16
"C (x ::= a) = {(s,t). t = s(x := aval a s)}" |
nipkow@43143
    17
"C (c0;c1)   = C(c0) O C(c1)" |
nipkow@43143
    18
"C (IF b THEN c1 ELSE c2) = {(s,t). (s,t) \<in> C c1 \<and> bval b s} \<union>
nipkow@43143
    19
                            {(s,t). (s,t) \<in> C c2 \<and> \<not>bval b s}" |
nipkow@43143
    20
"C(WHILE b DO c) = lfp (Gamma b (C c))"
kleing@12431
    21
kleing@12431
    22
kleing@12431
    23
lemma Gamma_mono: "mono (Gamma b c)"
nipkow@43143
    24
by (unfold Gamma_def mono_def) fast
kleing@12431
    25
nipkow@43143
    26
lemma C_While_If: "C(WHILE b DO c) = C(IF b THEN c;WHILE b DO c ELSE SKIP)"
wenzelm@18372
    27
apply simp
paulson@15481
    28
apply (subst lfp_unfold [OF Gamma_mono])  --{*lhs only*}
paulson@15481
    29
apply (simp add: Gamma_def)
kleing@12431
    30
done
kleing@12431
    31
nipkow@43144
    32
text{* Equivalence of denotational and big-step semantics: *}
kleing@12431
    33
nipkow@43143
    34
lemma com1: "(c,s) \<Rightarrow> t \<Longrightarrow> (s,t) \<in> C(c)"
nipkow@45015
    35
apply (induction rule: big_step_induct)
kleing@12431
    36
apply auto
kleing@12431
    37
(* while *)
kleing@12431
    38
apply (unfold Gamma_def)
kleing@12431
    39
apply (subst lfp_unfold[OF Gamma_mono, simplified Gamma_def])
kleing@12431
    40
apply fast
kleing@12431
    41
apply (subst lfp_unfold[OF Gamma_mono, simplified Gamma_def])
paulson@34055
    42
apply auto 
kleing@12431
    43
done
kleing@12431
    44
nipkow@43143
    45
lemma com2: "(s,t) \<in> C(c) \<Longrightarrow> (c,s) \<Rightarrow> t"
nipkow@45015
    46
apply (induction c arbitrary: s t)
paulson@34055
    47
apply auto 
paulson@34055
    48
apply blast
kleing@12431
    49
(* while *)
berghofe@23746
    50
apply (erule lfp_induct2 [OF _ Gamma_mono])
kleing@12431
    51
apply (unfold Gamma_def)
paulson@34055
    52
apply auto
kleing@12431
    53
done
kleing@12431
    54
nipkow@43144
    55
lemma denotational_is_big_step: "(s,t) \<in> C(c)  =  ((c,s) \<Rightarrow> t)"
nipkow@43143
    56
by (fast elim: com2 dest: com1)
clasohm@924
    57
clasohm@924
    58
end