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
     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> (cd O phi) \<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(c0) O C(c1)"
    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 auto 
    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 apply auto 
    58 apply blast
    59 
    60 (* while *)
    61 apply (erule lfp_induct2 [OF _ Gamma_mono])
    62 apply (unfold Gamma_def)
    63 apply auto
    64 done
    65 
    66 
    67 (**** Proof of Equivalence ****)
    68 
    69 lemma denotational_is_natural: "(s,t) \<in> C(c)  =  (\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t)"
    70   by (fast elim: com2 dest: com1)
    71 
    72 end