src/HOLCF/IMP/Denotational.thy
author wenzelm
Fri Nov 17 02:20:03 2006 +0100 (2006-11-17)
changeset 21404 eb85850d3eb7
parent 19737 3b8920131be2
child 26438 090ced251009
permissions -rw-r--r--
more robust syntax for definition/abbreviation/notation;
     1 (*  Title:      HOLCF/IMP/Denotational.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow and Robert Sandner, TUM
     4     Copyright   1996 TUM
     5 *)
     6 
     7 header "Denotational Semantics of Commands in HOLCF"
     8 
     9 theory Denotational imports HOLCF Natural begin
    10 
    11 subsection "Definition"
    12 
    13 definition
    14   dlift :: "(('a::type) discr -> 'b::pcpo) => ('a lift -> 'b)" where
    15   "dlift f = (LAM x. case x of UU => UU | Def y => f\<cdot>(Discr y))"
    16 
    17 consts D :: "com => state discr -> state lift"
    18 
    19 primrec
    20   "D(\<SKIP>) = (LAM s. Def(undiscr s))"
    21   "D(X :== a) = (LAM s. Def((undiscr s)[X \<mapsto> a(undiscr s)]))"
    22   "D(c0 ; c1) = (dlift(D c1) oo (D c0))"
    23   "D(\<IF> b \<THEN> c1 \<ELSE> c2) =
    24         (LAM s. if b (undiscr s) then (D c1)\<cdot>s else (D c2)\<cdot>s)"
    25   "D(\<WHILE> b \<DO> c) =
    26         fix\<cdot>(LAM w s. if b (undiscr s) then (dlift w)\<cdot>((D c)\<cdot>s)
    27                       else Def(undiscr s))"
    28 
    29 subsection
    30   "Equivalence of Denotational Semantics in HOLCF and Evaluation Semantics in HOL"
    31 
    32 lemma dlift_Def [simp]: "dlift f\<cdot>(Def x) = f\<cdot>(Discr x)"
    33   by (simp add: dlift_def)
    34 
    35 lemma cont_dlift [iff]: "cont (%f. dlift f)"
    36   by (simp add: dlift_def)
    37 
    38 lemma dlift_is_Def [simp]:
    39     "(dlift f\<cdot>l = Def y) = (\<exists>x. l = Def x \<and> f\<cdot>(Discr x) = Def y)"
    40   by (simp add: dlift_def split: lift.split)
    41 
    42 lemma eval_implies_D: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t ==> D c\<cdot>(Discr s) = (Def t)"
    43   apply (induct set: evalc)
    44         apply simp_all
    45    apply (subst fix_eq)
    46    apply simp
    47   apply (subst fix_eq)
    48   apply simp
    49   done
    50 
    51 lemma D_implies_eval: "!s t. D c\<cdot>(Discr s) = (Def t) --> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
    52   apply (induct c)
    53       apply simp
    54      apply simp
    55     apply force
    56    apply (simp (no_asm))
    57    apply force
    58   apply (simp (no_asm))
    59   apply (rule fix_ind)
    60     apply (fast intro!: adm_lemmas adm_chfindom ax_flat)
    61    apply (simp (no_asm))
    62   apply (simp (no_asm))
    63   apply safe
    64   apply fast
    65   done
    66 
    67 theorem D_is_eval: "(D c\<cdot>(Discr s) = (Def t)) = (\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t)"
    68   by (fast elim!: D_implies_eval [rule_format] eval_implies_D)
    69 
    70 end