src/HOL/IMP/Denotation.thy
author kleing
Sun Dec 09 15:26:13 2001 +0100 (2001-12-09)
changeset 12434 ff2efde4574d
parent 12431 07ec657249e5
child 15481 fc075ae929e4
permissions -rw-r--r--
tuned
     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 = Natural:
    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 (no_asm)) 
    37 apply (subst lfp_unfold [OF Gamma_mono]) back back
    38 apply (subst Gamma_def [THEN meta_eq_to_obj_eq, THEN fun_cong]) 
    39 apply simp
    40 done
    41 
    42 (* Operational Semantics implies Denotational Semantics *)
    43 
    44 lemma com1: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t \<Longrightarrow> (s,t) \<in> C(c)"
    45 
    46 (* start with rule induction *)
    47 apply (erule evalc.induct)
    48 apply auto
    49 (* while *)
    50 apply (unfold Gamma_def)
    51 apply (subst lfp_unfold[OF Gamma_mono, simplified Gamma_def])
    52 apply fast
    53 apply (subst lfp_unfold[OF Gamma_mono, simplified Gamma_def])
    54 apply fast
    55 done
    56 
    57 (* Denotational Semantics implies Operational Semantics *)
    58 
    59 lemma com2 [rule_format]: "\<forall>s t. (s,t)\<in>C(c) \<longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
    60 apply (induct_tac "c")
    61 
    62 apply (simp_all (no_asm_use))
    63 apply fast
    64 apply fast
    65 
    66 (* while *)
    67 apply (intro strip)
    68 apply (erule lfp_induct [OF _ Gamma_mono])
    69 apply (unfold Gamma_def)
    70 apply fast
    71 done
    72 
    73 
    74 (**** Proof of Equivalence ****)
    75 
    76 lemma denotational_is_natural: "(s,t) \<in> C(c)  =  (\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t)"
    77 apply (fast elim: com2 dest: com1)
    78 done
    79 
    80 end