src/HOL/IMP/Denotation.thy
author wenzelm
Fri Mar 28 19:43:54 2008 +0100 (2008-03-28)
changeset 26462 dac4e2bce00d
parent 23746 a455e69c31cc
child 27362 a6dc1769fdda
permissions -rw-r--r--
avoid rebinding of existing facts;
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
nipkow@1696
    13
constdefs
kleing@12431
    14
  Gamma :: "[bexp,com_den] => (com_den => com_den)"
wenzelm@18372
    15
  "Gamma b cd == (\<lambda>phi. {(s,t). (s,t) \<in> (phi O cd) \<and> b s} \<union>
kleing@12434
    16
                       {(s,t). s=t \<and> \<not>b s})"
wenzelm@18372
    17
nipkow@1696
    18
consts
kleing@12431
    19
  C :: "com => com_den"
clasohm@924
    20
berghofe@5183
    21
primrec
kleing@12431
    22
  C_skip:   "C \<SKIP>   = Id"
kleing@12431
    23
  C_assign: "C (x :== a) = {(s,t). t = s[x\<mapsto>a(s)]}"
kleing@12431
    24
  C_comp:   "C (c0;c1)   = C(c1) O C(c0)"
kleing@12431
    25
  C_if:     "C (\<IF> b \<THEN> c1 \<ELSE> c2) = {(s,t). (s,t) \<in> C c1 \<and> b s} \<union>
kleing@12434
    26
                                                {(s,t). (s,t) \<in> C c2 \<and> \<not>b s}"
kleing@12431
    27
  C_while:  "C(\<WHILE> b \<DO> c) = lfp (Gamma b (C c))"
kleing@12431
    28
kleing@12431
    29
kleing@12431
    30
(**** mono (Gamma(b,c)) ****)
kleing@12431
    31
kleing@12431
    32
lemma Gamma_mono: "mono (Gamma b c)"
kleing@12431
    33
  by (unfold Gamma_def mono_def) fast
kleing@12431
    34
kleing@12431
    35
lemma C_While_If: "C(\<WHILE> b \<DO> c) = C(\<IF> b \<THEN> c;\<WHILE> b \<DO> c \<ELSE> \<SKIP>)"
wenzelm@18372
    36
apply simp
paulson@15481
    37
apply (subst lfp_unfold [OF Gamma_mono])  --{*lhs only*}
paulson@15481
    38
apply (simp add: Gamma_def)
kleing@12431
    39
done
kleing@12431
    40
kleing@12431
    41
(* Operational Semantics implies Denotational Semantics *)
kleing@12431
    42
kleing@12431
    43
lemma com1: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t \<Longrightarrow> (s,t) \<in> C(c)"
kleing@12431
    44
(* start with rule induction *)
wenzelm@18372
    45
apply (induct set: evalc)
kleing@12431
    46
apply auto
kleing@12431
    47
(* while *)
kleing@12431
    48
apply (unfold Gamma_def)
kleing@12431
    49
apply (subst lfp_unfold[OF Gamma_mono, simplified Gamma_def])
kleing@12431
    50
apply fast
kleing@12431
    51
apply (subst lfp_unfold[OF Gamma_mono, simplified Gamma_def])
kleing@12431
    52
apply fast
kleing@12431
    53
done
kleing@12431
    54
kleing@12431
    55
(* Denotational Semantics implies Operational Semantics *)
kleing@12431
    56
wenzelm@18372
    57
lemma com2: "(s,t) \<in> C(c) \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
wenzelm@20503
    58
apply (induct c arbitrary: s t)
kleing@12431
    59
wenzelm@18372
    60
apply simp_all
kleing@12431
    61
apply fast
kleing@12431
    62
apply fast
kleing@12431
    63
kleing@12431
    64
(* while *)
berghofe@23746
    65
apply (erule lfp_induct2 [OF _ Gamma_mono])
kleing@12431
    66
apply (unfold Gamma_def)
kleing@12431
    67
apply fast
kleing@12431
    68
done
kleing@12431
    69
kleing@12431
    70
kleing@12431
    71
(**** Proof of Equivalence ****)
kleing@12431
    72
kleing@12431
    73
lemma denotational_is_natural: "(s,t) \<in> C(c)  =  (\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t)"
wenzelm@18372
    74
  by (fast elim: com2 dest: com1)
clasohm@924
    75
clasohm@924
    76
end