src/HOL/IMP/Denotation.thy
changeset 12431 07ec657249e5
parent 9241 f961c1fdff50
child 12434 ff2efde4574d
     1.1 --- a/src/HOL/IMP/Denotation.thy	Sun Dec 09 14:35:11 2001 +0100
     1.2 +++ b/src/HOL/IMP/Denotation.thy	Sun Dec 09 14:35:36 2001 +0100
     1.3 @@ -2,28 +2,79 @@
     1.4      ID:         $Id$
     1.5      Author:     Heiko Loetzbeyer & Robert Sandner, TUM
     1.6      Copyright   1994 TUM
     1.7 -
     1.8 -Denotational semantics of commands
     1.9  *)
    1.10  
    1.11 -Denotation = Natural + 
    1.12 +header "Denotational Semantics of Commands"
    1.13  
    1.14 -types com_den = "(state*state)set"
    1.15 +theory Denotation = Natural:
    1.16 +
    1.17 +types com_den = "(state\<times>state)set"
    1.18  
    1.19  constdefs
    1.20 -  Gamma :: [bexp,com_den] => (com_den => com_den)
    1.21 -           "Gamma b cd == (%phi.{(s,t). (s,t) : (phi O cd) & b(s)} Un 
    1.22 -                                 {(s,t). s=t & ~b(s)})"
    1.23 +  Gamma :: "[bexp,com_den] => (com_den => com_den)"
    1.24 +  "Gamma b cd == (\<lambda>phi. {(s,t). (s,t) \<in> (phi O cd) \<and> b s} \<union> 
    1.25 +                        {(s,t). s=t \<and> \<not>b s})"
    1.26      
    1.27  consts
    1.28 -  C     :: com => com_den
    1.29 +  C :: "com => com_den"
    1.30  
    1.31  primrec
    1.32 -  C_skip    "C(SKIP) = Id"
    1.33 -  C_assign  "C(x :== a) = {(s,t). t = s[x::=a(s)]}"
    1.34 -  C_comp    "C(c0 ; c1) = C(c1) O C(c0)"
    1.35 -  C_if      "C(IF b THEN c1 ELSE c2) = {(s,t). (s,t) : C(c1) & b(s)} Un
    1.36 -                                       {(s,t). (s,t) : C(c2) & ~ b(s)}"
    1.37 -  C_while   "C(WHILE b DO c) = lfp (Gamma b (C c))"
    1.38 +  C_skip:   "C \<SKIP>   = Id"
    1.39 +  C_assign: "C (x :== a) = {(s,t). t = s[x\<mapsto>a(s)]}"
    1.40 +  C_comp:   "C (c0;c1)   = C(c1) O C(c0)"
    1.41 +  C_if:     "C (\<IF> b \<THEN> c1 \<ELSE> c2) = {(s,t). (s,t) \<in> C c1 \<and> b s} \<union>
    1.42 +                                                 {(s,t). (s,t) \<in> C c2 \<and> \<not>b s}"
    1.43 +  C_while:  "C(\<WHILE> b \<DO> c) = lfp (Gamma b (C c))"
    1.44 +
    1.45 +
    1.46 +(**** mono (Gamma(b,c)) ****)
    1.47 +
    1.48 +lemma Gamma_mono: "mono (Gamma b c)"
    1.49 +  by (unfold Gamma_def mono_def) fast
    1.50 +
    1.51 +lemma C_While_If: "C(\<WHILE> b \<DO> c) = C(\<IF> b \<THEN> c;\<WHILE> b \<DO> c \<ELSE> \<SKIP>)"
    1.52 +apply (simp (no_asm))
    1.53 +apply (subst lfp_unfold [OF Gamma_mono],
    1.54 +       subst Gamma_def [THEN meta_eq_to_obj_eq, THEN fun_cong],
    1.55 +       simp)
    1.56 +done
    1.57 +
    1.58 +(* Operational Semantics implies Denotational Semantics *)
    1.59 +
    1.60 +lemma com1: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t \<Longrightarrow> (s,t) \<in> C(c)"
    1.61 +
    1.62 +(* start with rule induction *)
    1.63 +apply (erule evalc.induct)
    1.64 +apply auto
    1.65 +(* while *)
    1.66 +apply (unfold Gamma_def)
    1.67 +apply (subst lfp_unfold[OF Gamma_mono, simplified Gamma_def])
    1.68 +apply fast
    1.69 +apply (subst lfp_unfold[OF Gamma_mono, simplified Gamma_def])
    1.70 +apply fast
    1.71 +done
    1.72 +
    1.73 +(* Denotational Semantics implies Operational Semantics *)
    1.74 +
    1.75 +lemma com2 [rule_format]: "\<forall>s t. (s,t)\<in>C(c) \<longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
    1.76 +apply (induct_tac "c")
    1.77 +
    1.78 +apply (simp_all (no_asm_use))
    1.79 +apply fast
    1.80 +apply fast
    1.81 +
    1.82 +(* while *)
    1.83 +apply (intro strip)
    1.84 +apply (erule lfp_induct [OF _ Gamma_mono])
    1.85 +apply (unfold Gamma_def)
    1.86 +apply fast
    1.87 +done
    1.88 +
    1.89 +
    1.90 +(**** Proof of Equivalence ****)
    1.91 +
    1.92 +lemma denotational_is_natural: "(s,t) \<in> C(c)  =  (\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t)"
    1.93 +apply (fast elim: com2 dest: com1)
    1.94 +done
    1.95  
    1.96  end