author  nipkow 
Thu, 20 Jun 2013 17:43:36 +0200  
changeset 52401  56e83c57f953 
parent 52396  432777f2e372 
child 52402  c2f30ba4bb98 
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 

52394  5 
theory Denotational imports Big_Step begin 
12431  6 

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

52396  9 
definition W :: "(state \<Rightarrow> bool) \<Rightarrow> com_den \<Rightarrow> (com_den \<Rightarrow> com_den)" where 
10 
"W db dc = (\<lambda>dw. {(s,t). if db s then (s,t) \<in> dc O dw else s=t})" 

18372  11 

52389  12 
fun D :: "com \<Rightarrow> com_den" where 
13 
"D SKIP = Id"  

14 
"D (x ::= a) = {(s,t). t = s(x := aval a s)}"  

52395  15 
"D (c1;;c2) = D(c1) O D(c2)"  
52389  16 
"D (IF b THEN c1 ELSE c2) 
17 
= {(s,t). if bval b s then (s,t) \<in> D c1 else (s,t) \<in> D c2}"  

52396  18 
"D (WHILE b DO c) = lfp (W (bval b) (D c))" 
12431  19 

52387  20 
lemma W_mono: "mono (W b r)" 
21 
by (unfold W_def mono_def) auto 

12431  22 

52389  23 
lemma D_While_If: 
24 
"D(WHILE b DO c) = D(IF b THEN c;;WHILE b DO c ELSE SKIP)" 

25 
proof 

52396  26 
let ?w = "WHILE b DO c" let ?f = "W (bval b) (D c)" 
27 
have "D ?w = lfp ?f" by simp 

28 
also have "\<dots> = ?f (lfp ?f)" by(rule lfp_unfold [OF W_mono]) 

52389  29 
also have "\<dots> = D(IF b THEN c;;?w ELSE SKIP)" by (simp add: W_def) 
30 
finally show ?thesis . 

31 
qed 

12431  32 

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

52389  35 
lemma D_if_big_step: "(c,s) \<Rightarrow> t \<Longrightarrow> (s,t) \<in> D(c)" 
52387  36 
proof (induction rule: big_step_induct) 
37 
case WhileFalse 

52389  38 
with D_While_If show ?case by auto 
52387  39 
next 
40 
case WhileTrue 

52389  41 
show ?case unfolding D_While_If using WhileTrue by auto 
52387  42 
qed auto 
43 

44 
abbreviation Big_step :: "com \<Rightarrow> com_den" where 

45 
"Big_step c \<equiv> {(s,t). (c,s) \<Rightarrow> t}" 

12431  46 

52389  47 
lemma Big_step_if_D: "(s,t) \<in> D(c) \<Longrightarrow> (s,t) : Big_step c" 
52387  48 
proof (induction c arbitrary: s t) 
49 
case Seq thus ?case by fastforce 

50 
next 

51 
case (While b c) 

52396  52 
let ?B = "Big_step (WHILE b DO c)" let ?f = "W (bval b) (D c)" 
53 
have "?f ?B \<subseteq> ?B" using While.IH by (auto simp: W_def) 

54 
from lfp_lowerbound[where ?f = "?f", OF this] While.prems 

52387  55 
show ?case by auto 
56 
qed (auto split: if_splits) 

12431  57 

52387  58 
theorem denotational_is_big_step: 
52389  59 
"(s,t) \<in> D(c) = ((c,s) \<Rightarrow> t)" 
60 
by (metis D_if_big_step Big_step_if_D[simplified]) 

61 

52401  62 
corollary equiv_c_iff_equal_D: "(c1 \<sim> c2) \<longleftrightarrow> D c1 = D c2" 
63 
by(simp add: denotational_is_big_step[symmetric] set_eq_iff) 

64 

52389  65 

66 
subsection "Continuity" 

67 

68 
definition chain :: "(nat \<Rightarrow> 'a set) \<Rightarrow> bool" where 

69 
"chain S = (\<forall>i. S i \<subseteq> S(Suc i))" 

70 

71 
lemma chain_total: "chain S \<Longrightarrow> S i \<le> S j \<or> S j \<le> S i" 

72 
by (metis chain_def le_cases lift_Suc_mono_le) 

73 

74 
definition cont :: "('a set \<Rightarrow> 'a set) \<Rightarrow> bool" where 

75 
"cont f = (\<forall>S. chain S \<longrightarrow> f(UN n. S n) = (UN n. f(S n)))" 

76 

77 
lemma mono_if_cont: fixes f :: "'a set \<Rightarrow> 'a set" 

78 
assumes "cont f" shows "mono f" 

79 
proof 

80 
fix a b :: "'a set" assume "a \<subseteq> b" 

81 
let ?S = "\<lambda>n::nat. if n=0 then a else b" 

82 
have "chain ?S" using `a \<subseteq> b` by(auto simp: chain_def) 

52396  83 
hence "f(UN n. ?S n) = (UN n. f(?S n))" 
84 
using assms by(simp add: cont_def) 

52389  85 
moreover have "(UN n. ?S n) = b" using `a \<subseteq> b` by (auto split: if_splits) 
86 
moreover have "(UN n. f(?S n)) = f a \<union> f b" by (auto split: if_splits) 

87 
ultimately show "f a \<subseteq> f b" by (metis Un_upper1) 

88 
qed 

89 

90 
lemma chain_iterates: fixes f :: "'a set \<Rightarrow> 'a set" 

91 
assumes "mono f" shows "chain(\<lambda>n. (f^^n) {})" 

92 
proof 

93 
{ fix n have "(f ^^ n) {} \<subseteq> (f ^^ Suc n) {}" using assms 

94 
by(induction n) (auto simp: mono_def) } 

95 
thus ?thesis by(auto simp: chain_def) 

96 
qed 

97 

98 
theorem lfp_if_cont: 

99 
assumes "cont f" shows "lfp f = (UN n. (f^^n) {})" (is "_ = ?U") 

100 
proof 

101 
show "lfp f \<subseteq> ?U" 

102 
proof (rule lfp_lowerbound) 

103 
have "f ?U = (UN n. (f^^Suc n){})" 

104 
using chain_iterates[OF mono_if_cont[OF assms]] assms 

105 
by(simp add: cont_def) 

106 
also have "\<dots> = (f^^0){} \<union> \<dots>" by simp 

107 
also have "\<dots> = ?U" 

108 
by(auto simp del: funpow.simps) (metis not0_implies_Suc) 

109 
finally show "f ?U \<subseteq> ?U" by simp 

110 
qed 

111 
next 

112 
{ fix n p assume "f p \<subseteq> p" 

113 
have "(f^^n){} \<subseteq> p" 

114 
proof(induction n) 

115 
case 0 show ?case by simp 

116 
next 

117 
case Suc 

118 
from monoD[OF mono_if_cont[OF assms] Suc] `f p \<subseteq> p` 

119 
show ?case by simp 

120 
qed 

121 
} 

122 
thus "?U \<subseteq> lfp f" by(auto simp: lfp_def) 

123 
qed 

124 

125 
lemma cont_W: "cont(W b r)" 

126 
by(auto simp: cont_def W_def) 

127 

52392  128 

52389  129 
subsection{*The denotational semantics is deterministic*} 
130 

131 
lemma single_valued_UN_chain: 

132 
assumes "chain S" "(\<And>n. single_valued (S n))" 

133 
shows "single_valued(UN n. S n)" 

134 
proof(auto simp: single_valued_def) 

135 
fix m n x y z assume "(x, y) \<in> S m" "(x, z) \<in> S n" 

136 
with chain_total[OF assms(1), of m n] assms(2) 

137 
show "y = z" by (auto simp: single_valued_def) 

138 
qed 

139 

140 
lemma single_valued_lfp: fixes f :: "com_den \<Rightarrow> com_den" 

141 
assumes "cont f" "\<And>r. single_valued r \<Longrightarrow> single_valued (f r)" 

142 
shows "single_valued(lfp f)" 

143 
unfolding lfp_if_cont[OF assms(1)] 

144 
proof(rule single_valued_UN_chain[OF chain_iterates[OF mono_if_cont[OF assms(1)]]]) 

145 
fix n show "single_valued ((f ^^ n) {})" 

146 
by(induction n)(auto simp: assms(2)) 

147 
qed 

148 

149 
lemma single_valued_D: "single_valued (D c)" 

150 
proof(induction c) 

151 
case Seq thus ?case by(simp add: single_valued_relcomp) 

152 
next 

153 
case (While b c) 

52396  154 
let ?f = "W (bval b) (D c)" 
155 
have "single_valued (lfp ?f)" 

52389  156 
proof(rule single_valued_lfp[OF cont_W]) 
52396  157 
show "\<And>r. single_valued r \<Longrightarrow> single_valued (?f r)" 
52389  158 
using While.IH by(force simp: single_valued_def W_def) 
159 
qed 

160 
thus ?case by simp 

161 
qed (auto simp add: single_valued_def) 

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

162 

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

163 
end 