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