author | paulson <lp15@cam.ac.uk> |
Thu, 12 Sep 2019 15:32:39 +0100 | |
changeset 70690 | 8518a750f7bb |
parent 69661 | a03a63b81f44 |
permissions | -rw-r--r-- |
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 |
|
58889 | 3 |
section "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 |
|
67406 | 33 |
text\<open>Equivalence of denotational and big-step semantics:\<close> |
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 |
|
67613 | 47 |
lemma Big_step_if_D: "(s,t) \<in> D(c) \<Longrightarrow> (s,t) \<in> 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 |
||
52402 | 74 |
definition cont :: "('a set \<Rightarrow> 'b set) \<Rightarrow> bool" where |
52389 | 75 |
"cont f = (\<forall>S. chain S \<longrightarrow> f(UN n. S n) = (UN n. f(S n)))" |
76 |
||
52402 | 77 |
lemma mono_if_cont: fixes f :: "'a set \<Rightarrow> 'b set" |
52389 | 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" |
|
67406 | 82 |
have "chain ?S" using \<open>a \<subseteq> b\<close> by(auto simp: chain_def) |
52396 | 83 |
hence "f(UN n. ?S n) = (UN n. f(?S n))" |
69661 | 84 |
using assms by (simp add: cont_def del: if_image_distrib) |
67406 | 85 |
moreover have "(UN n. ?S n) = b" using \<open>a \<subseteq> b\<close> by (auto split: if_splits) |
52389 | 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- |
|
67019
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
62343
diff
changeset
|
93 |
have "(f ^^ n) {} \<subseteq> (f ^^ Suc n) {}" for n |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
62343
diff
changeset
|
94 |
proof (induction n) |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
62343
diff
changeset
|
95 |
case 0 show ?case by simp |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
62343
diff
changeset
|
96 |
next |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
62343
diff
changeset
|
97 |
case (Suc n) thus ?case using assms by (auto simp: mono_def) |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
62343
diff
changeset
|
98 |
qed |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
62343
diff
changeset
|
99 |
thus ?thesis by(auto simp: chain_def assms) |
52389 | 100 |
qed |
101 |
||
102 |
theorem lfp_if_cont: |
|
103 |
assumes "cont f" shows "lfp f = (UN n. (f^^n) {})" (is "_ = ?U") |
|
104 |
proof |
|
62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
62217
diff
changeset
|
105 |
from assms mono_if_cont |
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
62217
diff
changeset
|
106 |
have mono: "(f ^^ n) {} \<subseteq> (f ^^ Suc n) {}" for n |
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
62217
diff
changeset
|
107 |
using funpow_decreasing [of n "Suc n"] by auto |
52389 | 108 |
show "lfp f \<subseteq> ?U" |
109 |
proof (rule lfp_lowerbound) |
|
110 |
have "f ?U = (UN n. (f^^Suc n){})" |
|
111 |
using chain_iterates[OF mono_if_cont[OF assms]] assms |
|
112 |
by(simp add: cont_def) |
|
113 |
also have "\<dots> = (f^^0){} \<union> \<dots>" by simp |
|
114 |
also have "\<dots> = ?U" |
|
62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
62217
diff
changeset
|
115 |
using mono by auto (metis funpow_simps_right(2) funpow_swap1 o_apply) |
52389 | 116 |
finally show "f ?U \<subseteq> ?U" by simp |
117 |
qed |
|
118 |
next |
|
67019
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
62343
diff
changeset
|
119 |
have "(f^^n){} \<subseteq> p" if "f p \<subseteq> p" for n p |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
62343
diff
changeset
|
120 |
proof - |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
62343
diff
changeset
|
121 |
show ?thesis |
52389 | 122 |
proof(induction n) |
123 |
case 0 show ?case by simp |
|
124 |
next |
|
125 |
case Suc |
|
67406 | 126 |
from monoD[OF mono_if_cont[OF assms] Suc] \<open>f p \<subseteq> p\<close> |
52389 | 127 |
show ?case by simp |
128 |
qed |
|
67019
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
62343
diff
changeset
|
129 |
qed |
52389 | 130 |
thus "?U \<subseteq> lfp f" by(auto simp: lfp_def) |
131 |
qed |
|
132 |
||
133 |
lemma cont_W: "cont(W b r)" |
|
134 |
by(auto simp: cont_def W_def) |
|
135 |
||
52392 | 136 |
|
67406 | 137 |
subsection\<open>The denotational semantics is deterministic\<close> |
52389 | 138 |
|
139 |
lemma single_valued_UN_chain: |
|
140 |
assumes "chain S" "(\<And>n. single_valued (S n))" |
|
141 |
shows "single_valued(UN n. S n)" |
|
142 |
proof(auto simp: single_valued_def) |
|
143 |
fix m n x y z assume "(x, y) \<in> S m" "(x, z) \<in> S n" |
|
144 |
with chain_total[OF assms(1), of m n] assms(2) |
|
145 |
show "y = z" by (auto simp: single_valued_def) |
|
146 |
qed |
|
147 |
||
148 |
lemma single_valued_lfp: fixes f :: "com_den \<Rightarrow> com_den" |
|
149 |
assumes "cont f" "\<And>r. single_valued r \<Longrightarrow> single_valued (f r)" |
|
150 |
shows "single_valued(lfp f)" |
|
151 |
unfolding lfp_if_cont[OF assms(1)] |
|
152 |
proof(rule single_valued_UN_chain[OF chain_iterates[OF mono_if_cont[OF assms(1)]]]) |
|
153 |
fix n show "single_valued ((f ^^ n) {})" |
|
154 |
by(induction n)(auto simp: assms(2)) |
|
155 |
qed |
|
156 |
||
157 |
lemma single_valued_D: "single_valued (D c)" |
|
158 |
proof(induction c) |
|
159 |
case Seq thus ?case by(simp add: single_valued_relcomp) |
|
160 |
next |
|
161 |
case (While b c) |
|
52396 | 162 |
let ?f = "W (bval b) (D c)" |
163 |
have "single_valued (lfp ?f)" |
|
52389 | 164 |
proof(rule single_valued_lfp[OF cont_W]) |
52396 | 165 |
show "\<And>r. single_valued r \<Longrightarrow> single_valued (?f r)" |
52389 | 166 |
using While.IH by(force simp: single_valued_def W_def) |
167 |
qed |
|
168 |
thus ?case by simp |
|
169 |
qed (auto simp add: single_valued_def) |
|
924
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
170 |
|
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
171 |
end |