src/HOL/IMP/Denotation.thy
author hoelzl
Thu Sep 02 10:14:32 2010 +0200 (2010-09-02)
changeset 39072 1030b1a166ef
parent 34055 fdf294ee08b2
child 41589 bbd861837ebc
permissions -rw-r--r--
Add lessThan_Suc_eq_insert_0
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])
paulson@34055
    50
apply auto 
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)
paulson@34055
    57
apply auto 
paulson@34055
    58
apply blast
kleing@12431
    59
kleing@12431
    60
(* while *)
berghofe@23746
    61
apply (erule lfp_induct2 [OF _ Gamma_mono])
kleing@12431
    62
apply (unfold Gamma_def)
paulson@34055
    63
apply auto
kleing@12431
    64
done
kleing@12431
    65
kleing@12431
    66
kleing@12431
    67
(**** Proof of Equivalence ****)
kleing@12431
    68
kleing@12431
    69
lemma denotational_is_natural: "(s,t) \<in> C(c)  =  (\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t)"
wenzelm@18372
    70
  by (fast elim: com2 dest: com1)
clasohm@924
    71
clasohm@924
    72
end