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