(* Title: HOLCF/IMP/Denotational.thy ID: $Id$ Author: Tobias Nipkow and Robert Sandner, TUM Copyright 1996 TUM *) header "Denotational Semantics of Commands in HOLCF" theory Denotational imports HOLCF Natural begin subsection "Definition" definition dlift :: "(('a::type) discr -> 'b::pcpo) => ('a lift -> 'b)" where "dlift f = (LAM x. case x of UU => UU | Def y => f\(Discr y))" consts D :: "com => state discr -> state lift" primrec "D(\) = (LAM s. Def(undiscr s))" "D(X :== a) = (LAM s. Def((undiscr s)[X \ a(undiscr s)]))" "D(c0 ; c1) = (dlift(D c1) oo (D c0))" "D(\ b \ c1 \ c2) = (LAM s. if b (undiscr s) then (D c1)\s else (D c2)\s)" "D(\ b \ c) = fix\(LAM w s. if b (undiscr s) then (dlift w)\((D c)\s) else Def(undiscr s))" subsection "Equivalence of Denotational Semantics in HOLCF and Evaluation Semantics in HOL" lemma dlift_Def [simp]: "dlift f\(Def x) = f\(Discr x)" by (simp add: dlift_def) lemma cont_dlift [iff]: "cont (%f. dlift f)" by (simp add: dlift_def) lemma dlift_is_Def [simp]: "(dlift f\l = Def y) = (\x. l = Def x \ f\(Discr x) = Def y)" by (simp add: dlift_def split: lift.split) lemma eval_implies_D: "\c,s\ \\<^sub>c t ==> D c\(Discr s) = (Def t)" apply (induct set: evalc) apply simp_all apply (subst fix_eq) apply simp apply (subst fix_eq) apply simp done lemma D_implies_eval: "!s t. D c\(Discr s) = (Def t) --> \c,s\ \\<^sub>c t" apply (induct c) apply simp apply simp apply force apply (simp (no_asm)) apply force apply (simp (no_asm)) apply (rule fix_ind) apply (fast intro!: adm_lemmas adm_chfindom ax_flat) apply (simp (no_asm)) apply (simp (no_asm)) apply safe apply fast done theorem D_is_eval: "(D c\(Discr s) = (Def t)) = (\c,s\ \\<^sub>c t)" by (fast elim!: D_implies_eval [rule_format] eval_implies_D) end