src/HOL/IMP/Denotation.thy
author berghofe
Wed Jul 11 11:14:51 2007 +0200 (2007-07-11)
changeset 23746 a455e69c31cc
parent 21020 9af9ceb16d58
child 27362 a6dc1769fdda
permissions -rw-r--r--
Adapted to new inductive definition package.
     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 constdefs
    14   Gamma :: "[bexp,com_den] => (com_den => com_den)"
    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 consts
    19   C :: "com => com_den"
    20 
    21 primrec
    22   C_skip:   "C \<SKIP>   = Id"
    23   C_assign: "C (x :== a) = {(s,t). t = s[x\<mapsto>a(s)]}"
    24   C_comp:   "C (c0;c1)   = C(c1) O C(c0)"
    25   C_if:     "C (\<IF> b \<THEN> c1 \<ELSE> c2) = {(s,t). (s,t) \<in> C c1 \<and> b s} \<union>
    26                                                 {(s,t). (s,t) \<in> C c2 \<and> \<not>b s}"
    27   C_while:  "C(\<WHILE> b \<DO> c) = lfp (Gamma b (C c))"
    28 
    29 
    30 (**** mono (Gamma(b,c)) ****)
    31 
    32 lemma Gamma_mono: "mono (Gamma b c)"
    33   by (unfold Gamma_def mono_def) fast
    34 
    35 lemma C_While_If: "C(\<WHILE> b \<DO> c) = C(\<IF> b \<THEN> c;\<WHILE> b \<DO> c \<ELSE> \<SKIP>)"
    36 apply simp
    37 apply (subst lfp_unfold [OF Gamma_mono])  --{*lhs only*}
    38 apply (simp add: Gamma_def)
    39 done
    40 
    41 (* Operational Semantics implies Denotational Semantics *)
    42 
    43 lemma com1: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t \<Longrightarrow> (s,t) \<in> C(c)"
    44 (* start with rule induction *)
    45 apply (induct set: evalc)
    46 apply auto
    47 (* while *)
    48 apply (unfold Gamma_def)
    49 apply (subst lfp_unfold[OF Gamma_mono, simplified Gamma_def])
    50 apply fast
    51 apply (subst lfp_unfold[OF Gamma_mono, simplified Gamma_def])
    52 apply fast
    53 done
    54 
    55 (* Denotational Semantics implies Operational Semantics *)
    56 
    57 lemma com2: "(s,t) \<in> C(c) \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
    58 apply (induct c arbitrary: s t)
    59 
    60 apply simp_all
    61 apply fast
    62 apply fast
    63 
    64 (* while *)
    65 apply (erule lfp_induct2 [OF _ Gamma_mono])
    66 apply (unfold Gamma_def)
    67 apply fast
    68 done
    69 
    70 
    71 (**** Proof of Equivalence ****)
    72 
    73 lemma denotational_is_natural: "(s,t) \<in> C(c)  =  (\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t)"
    74   by (fast elim: com2 dest: com1)
    75 
    76 end