src/HOL/HOLCF/IMP/Denotational.thy
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (24 months ago)
changeset 66695 91500c024c7f
parent 66453 cc19f7ca2ed6
child 67613 ce654b0e6d69
permissions -rw-r--r--
tuned;
wenzelm@42151
     1
(*  Title:      HOL/HOLCF/IMP/Denotational.thy
wenzelm@12600
     2
    Author:     Tobias Nipkow and Robert Sandner, TUM
nipkow@2798
     3
    Copyright   1996 TUM
nipkow@2798
     4
*)
nipkow@2798
     5
wenzelm@58880
     6
section "Denotational Semantics of Commands in HOLCF"
kleing@12431
     7
wenzelm@66453
     8
theory Denotational imports HOLCF "HOL-IMP.Big_Step" begin
huffman@37085
     9
kleing@12431
    10
subsection "Definition"
nipkow@2798
    11
wenzelm@19737
    12
definition
wenzelm@21404
    13
  dlift :: "(('a::type) discr -> 'b::pcpo) => ('a lift -> 'b)" where
wenzelm@19737
    14
  "dlift f = (LAM x. case x of UU => UU | Def y => f\<cdot>(Discr y))"
nipkow@2841
    15
wenzelm@27362
    16
primrec D :: "com => state discr -> state lift"
wenzelm@27362
    17
where
nipkow@43143
    18
  "D(SKIP) = (LAM s. Def(undiscr s))"
nipkow@43143
    19
| "D(X ::= a) = (LAM s. Def((undiscr s)(X := aval a (undiscr s))))"
wenzelm@52047
    20
| "D(c0 ;; c1) = (dlift(D c1) oo (D c0))"
nipkow@43143
    21
| "D(IF b THEN c1 ELSE c2) =
nipkow@43143
    22
        (LAM s. if bval b (undiscr s) then (D c1)\<cdot>s else (D c2)\<cdot>s)"
nipkow@43143
    23
| "D(WHILE b DO c) =
nipkow@43143
    24
        fix\<cdot>(LAM w s. if bval b (undiscr s) then (dlift w)\<cdot>((D c)\<cdot>s)
nipkow@2841
    25
                      else Def(undiscr s))"
nipkow@2798
    26
kleing@12431
    27
subsection
kleing@12431
    28
  "Equivalence of Denotational Semantics in HOLCF and Evaluation Semantics in HOL"
kleing@12431
    29
wenzelm@12600
    30
lemma dlift_Def [simp]: "dlift f\<cdot>(Def x) = f\<cdot>(Discr x)"
wenzelm@12600
    31
  by (simp add: dlift_def)
wenzelm@12600
    32
wenzelm@12600
    33
lemma cont_dlift [iff]: "cont (%f. dlift f)"
wenzelm@12600
    34
  by (simp add: dlift_def)
kleing@12431
    35
wenzelm@12600
    36
lemma dlift_is_Def [simp]:
wenzelm@12600
    37
    "(dlift f\<cdot>l = Def y) = (\<exists>x. l = Def x \<and> f\<cdot>(Discr x) = Def y)"
wenzelm@12600
    38
  by (simp add: dlift_def split: lift.split)
kleing@12431
    39
nipkow@43143
    40
lemma eval_implies_D: "(c,s) \<Rightarrow> t ==> D c\<cdot>(Discr s) = (Def t)"
nipkow@43143
    41
apply (induct rule: big_step_induct)
nipkow@43143
    42
      apply (auto)
nipkow@43143
    43
 apply (subst fix_eq)
nipkow@43143
    44
 apply simp
nipkow@43143
    45
apply (subst fix_eq)
nipkow@43143
    46
apply simp
nipkow@43143
    47
done
kleing@12431
    48
nipkow@43143
    49
lemma D_implies_eval: "!s t. D c\<cdot>(Discr s) = (Def t) --> (c,s) \<Rightarrow> t"
nipkow@43143
    50
apply (induct c)
nipkow@44890
    51
    apply fastforce
nipkow@44890
    52
   apply fastforce
nipkow@43143
    53
  apply force
nipkow@43143
    54
 apply (simp (no_asm))
nipkow@43143
    55
 apply force
nipkow@43143
    56
apply (simp (no_asm))
nipkow@43143
    57
apply (rule fix_ind)
nipkow@43143
    58
  apply (fast intro!: adm_lemmas adm_chfindom ax_flat)
nipkow@43143
    59
 apply (simp (no_asm))
nipkow@43143
    60
apply (simp (no_asm))
nipkow@43143
    61
apply force
nipkow@43143
    62
done
kleing@12431
    63
nipkow@43143
    64
theorem D_is_eval: "(D c\<cdot>(Discr s) = (Def t)) = ((c,s) \<Rightarrow> t)"
nipkow@43143
    65
by (fast elim!: D_implies_eval [rule_format] eval_implies_D)
kleing@12431
    66
nipkow@2798
    67
end