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
clasohm@1476
     1
(*  Title:      HOL/IMP/Denotation.thy
clasohm@924
     2
    ID:         $Id$
clasohm@1476
     3
    Author:     Heiko Loetzbeyer & Robert Sandner, TUM
clasohm@924
     4
    Copyright   1994 TUM
clasohm@924
     5
*)
clasohm@924
     6
kleing@12431
     7
header "Denotational Semantics of Commands"
clasohm@924
     8
kleing@12431
     9
theory Denotation = Natural:
kleing@12431
    10
kleing@12431
    11
types com_den = "(state\<times>state)set"
nipkow@1696
    12
nipkow@1696
    13
constdefs
kleing@12431
    14
  Gamma :: "[bexp,com_den] => (com_den => com_den)"
kleing@12431
    15
  "Gamma b cd == (\<lambda>phi. {(s,t). (s,t) \<in> (phi O cd) \<and> b s} \<union> 
kleing@12434
    16
                       {(s,t). s=t \<and> \<not>b s})"
nipkow@1696
    17
    
nipkow@1696
    18
consts
kleing@12431
    19
  C :: "com => com_den"
clasohm@924
    20
berghofe@5183
    21
primrec
kleing@12431
    22
  C_skip:   "C \<SKIP>   = Id"
kleing@12431
    23
  C_assign: "C (x :== a) = {(s,t). t = s[x\<mapsto>a(s)]}"
kleing@12431
    24
  C_comp:   "C (c0;c1)   = C(c1) O C(c0)"
kleing@12431
    25
  C_if:     "C (\<IF> b \<THEN> c1 \<ELSE> c2) = {(s,t). (s,t) \<in> C c1 \<and> b s} \<union>
kleing@12434
    26
                                                {(s,t). (s,t) \<in> C c2 \<and> \<not>b s}"
kleing@12431
    27
  C_while:  "C(\<WHILE> b \<DO> c) = lfp (Gamma b (C c))"
kleing@12431
    28
kleing@12431
    29
kleing@12431
    30
(**** mono (Gamma(b,c)) ****)
kleing@12431
    31
kleing@12431
    32
lemma Gamma_mono: "mono (Gamma b c)"
kleing@12431
    33
  by (unfold Gamma_def mono_def) fast
kleing@12431
    34
kleing@12431
    35
lemma C_While_If: "C(\<WHILE> b \<DO> c) = C(\<IF> b \<THEN> c;\<WHILE> b \<DO> c \<ELSE> \<SKIP>)"
kleing@12434
    36
apply (simp (no_asm)) 
kleing@12434
    37
apply (subst lfp_unfold [OF Gamma_mono]) back back
kleing@12434
    38
apply (subst Gamma_def [THEN meta_eq_to_obj_eq, THEN fun_cong]) 
kleing@12434
    39
apply simp
kleing@12431
    40
done
kleing@12431
    41
kleing@12431
    42
(* Operational Semantics implies Denotational Semantics *)
kleing@12431
    43
kleing@12431
    44
lemma com1: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t \<Longrightarrow> (s,t) \<in> C(c)"
kleing@12431
    45
kleing@12431
    46
(* start with rule induction *)
kleing@12431
    47
apply (erule evalc.induct)
kleing@12431
    48
apply auto
kleing@12431
    49
(* while *)
kleing@12431
    50
apply (unfold Gamma_def)
kleing@12431
    51
apply (subst lfp_unfold[OF Gamma_mono, simplified Gamma_def])
kleing@12431
    52
apply fast
kleing@12431
    53
apply (subst lfp_unfold[OF Gamma_mono, simplified Gamma_def])
kleing@12431
    54
apply fast
kleing@12431
    55
done
kleing@12431
    56
kleing@12431
    57
(* Denotational Semantics implies Operational Semantics *)
kleing@12431
    58
kleing@12431
    59
lemma com2 [rule_format]: "\<forall>s t. (s,t)\<in>C(c) \<longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
kleing@12431
    60
apply (induct_tac "c")
kleing@12431
    61
kleing@12431
    62
apply (simp_all (no_asm_use))
kleing@12431
    63
apply fast
kleing@12431
    64
apply fast
kleing@12431
    65
kleing@12431
    66
(* while *)
kleing@12431
    67
apply (intro strip)
kleing@12431
    68
apply (erule lfp_induct [OF _ Gamma_mono])
kleing@12431
    69
apply (unfold Gamma_def)
kleing@12431
    70
apply fast
kleing@12431
    71
done
kleing@12431
    72
kleing@12431
    73
kleing@12431
    74
(**** Proof of Equivalence ****)
kleing@12431
    75
kleing@12431
    76
lemma denotational_is_natural: "(s,t) \<in> C(c)  =  (\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t)"
kleing@12431
    77
apply (fast elim: com2 dest: com1)
kleing@12431
    78
done
clasohm@924
    79
clasohm@924
    80
end