author  nipkow 
Wed, 01 Jun 2011 22:47:26 +0200  
changeset 43144  631dd866b284 
parent 43143  1aeafba76f21 
child 45015  fdac1e9880eb 
permissions  rwrr 
43143  1 
(* Authors: Heiko Loetzbeyer, Robert Sandner, Tobias Nipkow *) 
924
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset

2 

12431  3 
header "Denotational Semantics of Commands" 
924
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset

4 

43143  5 
theory Denotation imports Big_Step begin 
12431  6 

42174  7 
type_synonym com_den = "(state \<times> state) set" 
1696  8 

27362  9 
definition 
43143  10 
Gamma :: "bexp \<Rightarrow> com_den \<Rightarrow> (com_den \<Rightarrow> com_den)" where 
11 
"Gamma b cd = (\<lambda>phi. {(s,t). (s,t) \<in> (cd O phi) \<and> bval b s} \<union> 

12 
{(s,t). s=t \<and> \<not>bval b s})" 

18372  13 

43143  14 
fun C :: "com \<Rightarrow> com_den" where 
15 
"C SKIP = Id"  

16 
"C (x ::= a) = {(s,t). t = s(x := aval a s)}"  

17 
"C (c0;c1) = C(c0) O C(c1)"  

18 
"C (IF b THEN c1 ELSE c2) = {(s,t). (s,t) \<in> C c1 \<and> bval b s} \<union> 

19 
{(s,t). (s,t) \<in> C c2 \<and> \<not>bval b s}"  

20 
"C(WHILE b DO c) = lfp (Gamma b (C c))" 

12431  21 

22 

23 
lemma Gamma_mono: "mono (Gamma b c)" 

43143  24 
by (unfold Gamma_def mono_def) fast 
12431  25 

43143  26 
lemma C_While_If: "C(WHILE b DO c) = C(IF b THEN c;WHILE b DO c ELSE SKIP)" 
18372  27 
apply simp 
15481  28 
apply (subst lfp_unfold [OF Gamma_mono]) {*lhs only*} 
29 
apply (simp add: Gamma_def) 

12431  30 
done 
31 

43144  32 
text{* Equivalence of denotational and bigstep semantics: *} 
12431  33 

43143  34 
lemma com1: "(c,s) \<Rightarrow> t \<Longrightarrow> (s,t) \<in> C(c)" 
35 
apply (induct rule: big_step_induct) 

12431  36 
apply auto 
37 
(* while *) 

38 
apply (unfold Gamma_def) 

39 
apply (subst lfp_unfold[OF Gamma_mono, simplified Gamma_def]) 

40 
apply fast 

41 
apply (subst lfp_unfold[OF Gamma_mono, simplified Gamma_def]) 

34055  42 
apply auto 
12431  43 
done 
44 

43143  45 
lemma com2: "(s,t) \<in> C(c) \<Longrightarrow> (c,s) \<Rightarrow> t" 
20503  46 
apply (induct c arbitrary: s t) 
34055  47 
apply auto 
48 
apply blast 

12431  49 
(* while *) 
23746  50 
apply (erule lfp_induct2 [OF _ Gamma_mono]) 
12431  51 
apply (unfold Gamma_def) 
34055  52 
apply auto 
12431  53 
done 
54 

43144  55 
lemma denotational_is_big_step: "(s,t) \<in> C(c) = ((c,s) \<Rightarrow> t)" 
43143  56 
by (fast elim: com2 dest: com1) 
924
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset

57 

806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset

58 
end 