src/HOL/IMP/Denotation.thy
author krauss
Mon Jul 27 21:47:41 2009 +0200 (2009-07-27 ago)
changeset 32235 8f9b8d14fc9f
parent 27362 a6dc1769fdda
child 34055 fdf294ee08b2
permissions -rw-r--r--
"more standard" argument order of relation composition (op O)
clasohm@1476
     1
(*  Title:      HOL/IMP/Denotation.thy
clasohm@924
     2
    ID:         $Id$
clasohm@1476
     3
    Author:     Heiko Loetzbeyer & Robert Sandner, TUM
clasohm@924
     4
    Copyright   1994 TUM
clasohm@924
     5
*)
clasohm@924
     6
kleing@12431
     7
header "Denotational Semantics of Commands"
clasohm@924
     8
haftmann@16417
     9
theory Denotation imports Natural begin
kleing@12431
    10
kleing@12431
    11
types com_den = "(state\<times>state)set"
nipkow@1696
    12
wenzelm@27362
    13
definition
wenzelm@27362
    14
  Gamma :: "[bexp,com_den] => (com_den => com_den)" where
krauss@32235
    15
  "Gamma b cd = (\<lambda>phi. {(s,t). (s,t) \<in> (cd O phi) \<and> b s} \<union>
kleing@12434
    16
                       {(s,t). s=t \<and> \<not>b s})"
wenzelm@18372
    17
wenzelm@27362
    18
primrec C :: "com => com_den"
wenzelm@27362
    19
where
kleing@12431
    20
  C_skip:   "C \<SKIP>   = Id"
wenzelm@27362
    21
| C_assign: "C (x :== a) = {(s,t). t = s[x\<mapsto>a(s)]}"
krauss@32235
    22
| C_comp:   "C (c0;c1)   = C(c0) O C(c1)"
wenzelm@27362
    23
| C_if:     "C (\<IF> b \<THEN> c1 \<ELSE> c2) = {(s,t). (s,t) \<in> C c1 \<and> b s} \<union>
kleing@12434
    24
                                                {(s,t). (s,t) \<in> C c2 \<and> \<not>b s}"
wenzelm@27362
    25
| C_while:  "C(\<WHILE> b \<DO> c) = lfp (Gamma b (C c))"
kleing@12431
    26
kleing@12431
    27
kleing@12431
    28
(**** mono (Gamma(b,c)) ****)
kleing@12431
    29
kleing@12431
    30
lemma Gamma_mono: "mono (Gamma b c)"
kleing@12431
    31
  by (unfold Gamma_def mono_def) fast
kleing@12431
    32
kleing@12431
    33
lemma C_While_If: "C(\<WHILE> b \<DO> c) = C(\<IF> b \<THEN> c;\<WHILE> b \<DO> c \<ELSE> \<SKIP>)"
wenzelm@18372
    34
apply simp
paulson@15481
    35
apply (subst lfp_unfold [OF Gamma_mono])  --{*lhs only*}
paulson@15481
    36
apply (simp add: Gamma_def)
kleing@12431
    37
done
kleing@12431
    38
kleing@12431
    39
(* Operational Semantics implies Denotational Semantics *)
kleing@12431
    40
kleing@12431
    41
lemma com1: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t \<Longrightarrow> (s,t) \<in> C(c)"
kleing@12431
    42
(* start with rule induction *)
wenzelm@18372
    43
apply (induct set: evalc)
kleing@12431
    44
apply auto
kleing@12431
    45
(* while *)
kleing@12431
    46
apply (unfold Gamma_def)
kleing@12431
    47
apply (subst lfp_unfold[OF Gamma_mono, simplified Gamma_def])
kleing@12431
    48
apply fast
kleing@12431
    49
apply (subst lfp_unfold[OF Gamma_mono, simplified Gamma_def])
kleing@12431
    50
apply fast
kleing@12431
    51
done
kleing@12431
    52
kleing@12431
    53
(* Denotational Semantics implies Operational Semantics *)
kleing@12431
    54
wenzelm@18372
    55
lemma com2: "(s,t) \<in> C(c) \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
wenzelm@20503
    56
apply (induct c arbitrary: s t)
kleing@12431
    57
wenzelm@18372
    58
apply simp_all
kleing@12431
    59
apply fast
kleing@12431
    60
apply fast
kleing@12431
    61
kleing@12431
    62
(* while *)
berghofe@23746
    63
apply (erule lfp_induct2 [OF _ Gamma_mono])
kleing@12431
    64
apply (unfold Gamma_def)
kleing@12431
    65
apply fast
kleing@12431
    66
done
kleing@12431
    67
kleing@12431
    68
kleing@12431
    69
(**** Proof of Equivalence ****)
kleing@12431
    70
kleing@12431
    71
lemma denotational_is_natural: "(s,t) \<in> C(c)  =  (\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t)"
wenzelm@18372
    72
  by (fast elim: com2 dest: com1)
clasohm@924
    73
clasohm@924
    74
end