author | paulson <lp15@cam.ac.uk> |
Tue, 22 Jan 2019 12:00:16 +0000 | |
changeset 69712 | dc85b5b3a532 |
parent 69597 | ff784d5a5bfb |
permissions | -rw-r--r-- |
45812 | 1 |
(* Author: Tobias Nipkow *) |
2 |
||
68776
403dd13cf6e9
avoid session qualification because no tex is generated when used;
nipkow
parents:
68484
diff
changeset
|
3 |
subsection "True Liveness Analysis" |
403dd13cf6e9
avoid session qualification because no tex is generated when used;
nipkow
parents:
68484
diff
changeset
|
4 |
|
45812 | 5 |
theory Live_True |
66453
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
53015
diff
changeset
|
6 |
imports "HOL-Library.While_Combinator" Vars Big_Step |
45812 | 7 |
begin |
8 |
||
68776
403dd13cf6e9
avoid session qualification because no tex is generated when used;
nipkow
parents:
68484
diff
changeset
|
9 |
subsubsection "Analysis" |
45812 | 10 |
|
11 |
fun L :: "com \<Rightarrow> vname set \<Rightarrow> vname set" where |
|
12 |
"L SKIP X = X" | |
|
51436 | 13 |
"L (x ::= a) X = (if x \<in> X then vars a \<union> (X - {x}) else X)" | |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52072
diff
changeset
|
14 |
"L (c\<^sub>1;; c\<^sub>2) X = L c\<^sub>1 (L c\<^sub>2 X)" | |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52072
diff
changeset
|
15 |
"L (IF b THEN c\<^sub>1 ELSE c\<^sub>2) X = vars b \<union> L c\<^sub>1 X \<union> L c\<^sub>2 X" | |
50009 | 16 |
"L (WHILE b DO c) X = lfp(\<lambda>Y. vars b \<union> X \<union> L c Y)" |
45812 | 17 |
|
18 |
lemma L_mono: "mono (L c)" |
|
19 |
proof- |
|
67019
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
66453
diff
changeset
|
20 |
have "X \<subseteq> Y \<Longrightarrow> L c X \<subseteq> L c Y" for X Y |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
66453
diff
changeset
|
21 |
proof(induction c arbitrary: X Y) |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
66453
diff
changeset
|
22 |
case (While b c) |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
66453
diff
changeset
|
23 |
show ?case |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
66453
diff
changeset
|
24 |
proof(simp, rule lfp_mono) |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
66453
diff
changeset
|
25 |
fix Z show "vars b \<union> X \<union> L c Z \<subseteq> vars b \<union> Y \<union> L c Z" |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
66453
diff
changeset
|
26 |
using While by auto |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
66453
diff
changeset
|
27 |
qed |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
66453
diff
changeset
|
28 |
next |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
66453
diff
changeset
|
29 |
case If thus ?case by(auto simp: subset_iff) |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
66453
diff
changeset
|
30 |
qed auto |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
66453
diff
changeset
|
31 |
thus ?thesis by(rule monoI) |
45812 | 32 |
qed |
33 |
||
34 |
lemma mono_union_L: |
|
50009 | 35 |
"mono (\<lambda>Y. X \<union> L c Y)" |
45812 | 36 |
by (metis (no_types) L_mono mono_def order_eq_iff set_eq_subset sup_mono) |
37 |
||
38 |
lemma L_While_unfold: |
|
39 |
"L (WHILE b DO c) X = vars b \<union> X \<union> L c (L (WHILE b DO c) X)" |
|
40 |
by(metis lfp_unfold[OF mono_union_L] L.simps(5)) |
|
41 |
||
51468
0e8012983c4e
proofs depend only on constraints, not on def of L WHILE
nipkow
parents:
51464
diff
changeset
|
42 |
lemma L_While_pfp: "L c (L (WHILE b DO c) X) \<subseteq> L (WHILE b DO c) X" |
0e8012983c4e
proofs depend only on constraints, not on def of L WHILE
nipkow
parents:
51464
diff
changeset
|
43 |
using L_While_unfold by blast |
0e8012983c4e
proofs depend only on constraints, not on def of L WHILE
nipkow
parents:
51464
diff
changeset
|
44 |
|
0e8012983c4e
proofs depend only on constraints, not on def of L WHILE
nipkow
parents:
51464
diff
changeset
|
45 |
lemma L_While_vars: "vars b \<subseteq> L (WHILE b DO c) X" |
0e8012983c4e
proofs depend only on constraints, not on def of L WHILE
nipkow
parents:
51464
diff
changeset
|
46 |
using L_While_unfold by blast |
0e8012983c4e
proofs depend only on constraints, not on def of L WHILE
nipkow
parents:
51464
diff
changeset
|
47 |
|
0e8012983c4e
proofs depend only on constraints, not on def of L WHILE
nipkow
parents:
51464
diff
changeset
|
48 |
lemma L_While_X: "X \<subseteq> L (WHILE b DO c) X" |
0e8012983c4e
proofs depend only on constraints, not on def of L WHILE
nipkow
parents:
51464
diff
changeset
|
49 |
using L_While_unfold by blast |
0e8012983c4e
proofs depend only on constraints, not on def of L WHILE
nipkow
parents:
51464
diff
changeset
|
50 |
|
69505 | 51 |
text\<open>Disable \<open>L WHILE\<close> equation and reason only with \<open>L WHILE\<close> constraints:\<close> |
51468
0e8012983c4e
proofs depend only on constraints, not on def of L WHILE
nipkow
parents:
51464
diff
changeset
|
52 |
declare L.simps(5)[simp del] |
0e8012983c4e
proofs depend only on constraints, not on def of L WHILE
nipkow
parents:
51464
diff
changeset
|
53 |
|
45812 | 54 |
|
68776
403dd13cf6e9
avoid session qualification because no tex is generated when used;
nipkow
parents:
68484
diff
changeset
|
55 |
subsubsection "Correctness" |
45812 | 56 |
|
51975 | 57 |
theorem L_correct: |
45812 | 58 |
"(c,s) \<Rightarrow> s' \<Longrightarrow> s = t on L c X \<Longrightarrow> |
59 |
\<exists> t'. (c,t) \<Rightarrow> t' & s' = t' on X" |
|
60 |
proof (induction arbitrary: X t rule: big_step_induct) |
|
61 |
case Skip then show ?case by auto |
|
62 |
next |
|
63 |
case Assign then show ?case |
|
64 |
by (auto simp: ball_Un) |
|
65 |
next |
|
47818 | 66 |
case (Seq c1 s1 s2 c2 s3 X t1) |
67 |
from Seq.IH(1) Seq.prems obtain t2 where |
|
45812 | 68 |
t12: "(c1, t1) \<Rightarrow> t2" and s2t2: "s2 = t2 on L c2 X" |
69 |
by simp blast |
|
47818 | 70 |
from Seq.IH(2)[OF s2t2] obtain t3 where |
45812 | 71 |
t23: "(c2, t2) \<Rightarrow> t3" and s3t3: "s3 = t3 on X" |
72 |
by auto |
|
73 |
show ?case using t12 t23 s3t3 by auto |
|
74 |
next |
|
75 |
case (IfTrue b s c1 s' c2) |
|
50009 | 76 |
hence "s = t on vars b" and "s = t on L c1 X" by auto |
45812 | 77 |
from bval_eq_if_eq_on_vars[OF this(1)] IfTrue(1) have "bval b t" by simp |
67406 | 78 |
from IfTrue.IH[OF \<open>s = t on L c1 X\<close>] obtain t' where |
45812 | 79 |
"(c1, t) \<Rightarrow> t'" "s' = t' on X" by auto |
67406 | 80 |
thus ?case using \<open>bval b t\<close> by auto |
45812 | 81 |
next |
82 |
case (IfFalse b s c2 s' c1) |
|
83 |
hence "s = t on vars b" "s = t on L c2 X" by auto |
|
84 |
from bval_eq_if_eq_on_vars[OF this(1)] IfFalse(1) have "~bval b t" by simp |
|
67406 | 85 |
from IfFalse.IH[OF \<open>s = t on L c2 X\<close>] obtain t' where |
45812 | 86 |
"(c2, t) \<Rightarrow> t'" "s' = t' on X" by auto |
67406 | 87 |
thus ?case using \<open>~bval b t\<close> by auto |
45812 | 88 |
next |
89 |
case (WhileFalse b s c) |
|
90 |
hence "~ bval b t" |
|
69712 | 91 |
by (metis L_While_vars bval_eq_if_eq_on_vars subsetD) |
51468
0e8012983c4e
proofs depend only on constraints, not on def of L WHILE
nipkow
parents:
51464
diff
changeset
|
92 |
thus ?case using WhileFalse.prems L_While_X[of X b c] by auto |
45812 | 93 |
next |
94 |
case (WhileTrue b s1 c s2 s3 X t1) |
|
95 |
let ?w = "WHILE b DO c" |
|
67406 | 96 |
from \<open>bval b s1\<close> WhileTrue.prems have "bval b t1" |
69712 | 97 |
by (metis L_While_vars bval_eq_if_eq_on_vars subsetD) |
51468
0e8012983c4e
proofs depend only on constraints, not on def of L WHILE
nipkow
parents:
51464
diff
changeset
|
98 |
have "s1 = t1 on L c (L ?w X)" using L_While_pfp WhileTrue.prems |
45812 | 99 |
by (blast) |
100 |
from WhileTrue.IH(1)[OF this] obtain t2 where |
|
101 |
"(c, t1) \<Rightarrow> t2" "s2 = t2 on L ?w X" by auto |
|
102 |
from WhileTrue.IH(2)[OF this(2)] obtain t3 where "(?w,t2) \<Rightarrow> t3" "s3 = t3 on X" |
|
103 |
by auto |
|
67406 | 104 |
with \<open>bval b t1\<close> \<open>(c, t1) \<Rightarrow> t2\<close> show ?case by auto |
45812 | 105 |
qed |
106 |
||
50009 | 107 |
|
68776
403dd13cf6e9
avoid session qualification because no tex is generated when used;
nipkow
parents:
68484
diff
changeset
|
108 |
subsubsection "Executability" |
45812 | 109 |
|
52072 | 110 |
lemma L_subset_vars: "L c X \<subseteq> rvars c \<union> X" |
45812 | 111 |
proof(induction c arbitrary: X) |
112 |
case (While b c) |
|
52072 | 113 |
have "lfp(\<lambda>Y. vars b \<union> X \<union> L c Y) \<subseteq> vars b \<union> rvars c \<union> X" |
114 |
using While.IH[of "vars b \<union> rvars c \<union> X"] |
|
45812 | 115 |
by (auto intro!: lfp_lowerbound) |
51468
0e8012983c4e
proofs depend only on constraints, not on def of L WHILE
nipkow
parents:
51464
diff
changeset
|
116 |
thus ?case by (simp add: L.simps(5)) |
45812 | 117 |
qed auto |
118 |
||
69597 | 119 |
text\<open>Make \<^const>\<open>L\<close> executable by replacing \<^const>\<open>lfp\<close> with the \<^const>\<open>while\<close> combinator from theory \<^theory>\<open>HOL-Library.While_Combinator\<close>. The \<^const>\<open>while\<close> |
50007
56f269baae76
executable true liveness analysis incl an approximating version
nipkow
parents:
48256
diff
changeset
|
120 |
combinator obeys the recursion equation |
56f269baae76
executable true liveness analysis incl an approximating version
nipkow
parents:
48256
diff
changeset
|
121 |
@{thm[display] While_Combinator.while_unfold[no_vars]} |
67406 | 122 |
and is thus executable.\<close> |
50007
56f269baae76
executable true liveness analysis incl an approximating version
nipkow
parents:
48256
diff
changeset
|
123 |
|
45812 | 124 |
lemma L_While: fixes b c X |
51464 | 125 |
assumes "finite X" defines "f == \<lambda>Y. vars b \<union> X \<union> L c Y" |
126 |
shows "L (WHILE b DO c) X = while (\<lambda>Y. f Y \<noteq> Y) f {}" (is "_ = ?r") |
|
45812 | 127 |
proof - |
52072 | 128 |
let ?V = "vars b \<union> rvars c \<union> X" |
45812 | 129 |
have "lfp f = ?r" |
50007
56f269baae76
executable true liveness analysis incl an approximating version
nipkow
parents:
48256
diff
changeset
|
130 |
proof(rule lfp_while[where C = "?V"]) |
45812 | 131 |
show "mono f" by(simp add: f_def mono_union_L) |
132 |
next |
|
133 |
fix Y show "Y \<subseteq> ?V \<Longrightarrow> f Y \<subseteq> ?V" |
|
134 |
unfolding f_def using L_subset_vars[of c] by blast |
|
135 |
next |
|
67406 | 136 |
show "finite ?V" using \<open>finite X\<close> by simp |
45812 | 137 |
qed |
51468
0e8012983c4e
proofs depend only on constraints, not on def of L WHILE
nipkow
parents:
51464
diff
changeset
|
138 |
thus ?thesis by (simp add: f_def L.simps(5)) |
45812 | 139 |
qed |
140 |
||
51464 | 141 |
lemma L_While_let: "finite X \<Longrightarrow> L (WHILE b DO c) X = |
142 |
(let f = (\<lambda>Y. vars b \<union> X \<union> L c Y) |
|
143 |
in while (\<lambda>Y. f Y \<noteq> Y) f {})" |
|
51468
0e8012983c4e
proofs depend only on constraints, not on def of L WHILE
nipkow
parents:
51464
diff
changeset
|
144 |
by(simp add: L_While) |
51464 | 145 |
|
50007
56f269baae76
executable true liveness analysis incl an approximating version
nipkow
parents:
48256
diff
changeset
|
146 |
lemma L_While_set: "L (WHILE b DO c) (set xs) = |
51464 | 147 |
(let f = (\<lambda>Y. vars b \<union> set xs \<union> L c Y) |
148 |
in while (\<lambda>Y. f Y \<noteq> Y) f {})" |
|
149 |
by(rule L_While_let, simp) |
|
50007
56f269baae76
executable true liveness analysis incl an approximating version
nipkow
parents:
48256
diff
changeset
|
150 |
|
69505 | 151 |
text\<open>Replace the equation for \<open>L (WHILE \<dots>)\<close> by the executable @{thm[source] L_While_set}:\<close> |
50007
56f269baae76
executable true liveness analysis incl an approximating version
nipkow
parents:
48256
diff
changeset
|
152 |
lemmas [code] = L.simps(1-4) L_While_set |
67406 | 153 |
text\<open>Sorry, this syntax is odd.\<close> |
45812 | 154 |
|
67406 | 155 |
text\<open>A test:\<close> |
52046
bc01725d7918
replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time
nipkow
parents:
51975
diff
changeset
|
156 |
lemma "(let b = Less (N 0) (V ''y''); c = ''y'' ::= V ''x'';; ''x'' ::= V ''z'' |
50007
56f269baae76
executable true liveness analysis incl an approximating version
nipkow
parents:
48256
diff
changeset
|
157 |
in L (WHILE b DO c) {''y''}) = {''x'', ''y'', ''z''}" |
56f269baae76
executable true liveness analysis incl an approximating version
nipkow
parents:
48256
diff
changeset
|
158 |
by eval |
56f269baae76
executable true liveness analysis incl an approximating version
nipkow
parents:
48256
diff
changeset
|
159 |
|
56f269baae76
executable true liveness analysis incl an approximating version
nipkow
parents:
48256
diff
changeset
|
160 |
|
68776
403dd13cf6e9
avoid session qualification because no tex is generated when used;
nipkow
parents:
68484
diff
changeset
|
161 |
subsubsection "Limiting the number of iterations" |
50007
56f269baae76
executable true liveness analysis incl an approximating version
nipkow
parents:
48256
diff
changeset
|
162 |
|
67406 | 163 |
text\<open>The final parameter is the default value:\<close> |
50007
56f269baae76
executable true liveness analysis incl an approximating version
nipkow
parents:
48256
diff
changeset
|
164 |
|
56f269baae76
executable true liveness analysis incl an approximating version
nipkow
parents:
48256
diff
changeset
|
165 |
fun iter :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" where |
45812 | 166 |
"iter f 0 p d = d" | |
167 |
"iter f (Suc n) p d = (if f p = p then p else iter f n (f p) d)" |
|
168 |
||
69597 | 169 |
text\<open>A version of \<^const>\<open>L\<close> with a bounded number of iterations (here: 2) |
67406 | 170 |
in the WHILE case:\<close> |
45812 | 171 |
|
50007
56f269baae76
executable true liveness analysis incl an approximating version
nipkow
parents:
48256
diff
changeset
|
172 |
fun Lb :: "com \<Rightarrow> vname set \<Rightarrow> vname set" where |
56f269baae76
executable true liveness analysis incl an approximating version
nipkow
parents:
48256
diff
changeset
|
173 |
"Lb SKIP X = X" | |
50009 | 174 |
"Lb (x ::= a) X = (if x \<in> X then X - {x} \<union> vars a else X)" | |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52072
diff
changeset
|
175 |
"Lb (c\<^sub>1;; c\<^sub>2) X = (Lb c\<^sub>1 \<circ> Lb c\<^sub>2) X" | |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52072
diff
changeset
|
176 |
"Lb (IF b THEN c\<^sub>1 ELSE c\<^sub>2) X = vars b \<union> Lb c\<^sub>1 X \<union> Lb c\<^sub>2 X" | |
52072 | 177 |
"Lb (WHILE b DO c) X = iter (\<lambda>A. vars b \<union> X \<union> Lb c A) 2 {} (vars b \<union> rvars c \<union> X)" |
50007
56f269baae76
executable true liveness analysis incl an approximating version
nipkow
parents:
48256
diff
changeset
|
178 |
|
69597 | 179 |
text\<open>\<^const>\<open>Lb\<close> (and \<^const>\<open>iter\<close>) is not monotone!\<close> |
52046
bc01725d7918
replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time
nipkow
parents:
51975
diff
changeset
|
180 |
lemma "let w = WHILE Bc False DO (''x'' ::= V ''y'';; ''z'' ::= V ''x'') |
50009 | 181 |
in \<not> (Lb w {''z''} \<subseteq> Lb w {''y'',''z''})" |
182 |
by eval |
|
183 |
||
50007
56f269baae76
executable true liveness analysis incl an approximating version
nipkow
parents:
48256
diff
changeset
|
184 |
lemma lfp_subset_iter: |
56f269baae76
executable true liveness analysis incl an approximating version
nipkow
parents:
48256
diff
changeset
|
185 |
"\<lbrakk> mono f; !!X. f X \<subseteq> f' X; lfp f \<subseteq> D \<rbrakk> \<Longrightarrow> lfp f \<subseteq> iter f' n A D" |
56f269baae76
executable true liveness analysis incl an approximating version
nipkow
parents:
48256
diff
changeset
|
186 |
proof(induction n arbitrary: A) |
56f269baae76
executable true liveness analysis incl an approximating version
nipkow
parents:
48256
diff
changeset
|
187 |
case 0 thus ?case by simp |
56f269baae76
executable true liveness analysis incl an approximating version
nipkow
parents:
48256
diff
changeset
|
188 |
next |
56f269baae76
executable true liveness analysis incl an approximating version
nipkow
parents:
48256
diff
changeset
|
189 |
case Suc thus ?case by simp (metis lfp_lowerbound) |
45812 | 190 |
qed |
191 |
||
50007
56f269baae76
executable true liveness analysis incl an approximating version
nipkow
parents:
48256
diff
changeset
|
192 |
lemma "L c X \<subseteq> Lb c X" |
56f269baae76
executable true liveness analysis incl an approximating version
nipkow
parents:
48256
diff
changeset
|
193 |
proof(induction c arbitrary: X) |
56f269baae76
executable true liveness analysis incl an approximating version
nipkow
parents:
48256
diff
changeset
|
194 |
case (While b c) |
56f269baae76
executable true liveness analysis incl an approximating version
nipkow
parents:
48256
diff
changeset
|
195 |
let ?f = "\<lambda>A. vars b \<union> X \<union> L c A" |
56f269baae76
executable true liveness analysis incl an approximating version
nipkow
parents:
48256
diff
changeset
|
196 |
let ?fb = "\<lambda>A. vars b \<union> X \<union> Lb c A" |
56f269baae76
executable true liveness analysis incl an approximating version
nipkow
parents:
48256
diff
changeset
|
197 |
show ?case |
51468
0e8012983c4e
proofs depend only on constraints, not on def of L WHILE
nipkow
parents:
51464
diff
changeset
|
198 |
proof (simp add: L.simps(5), rule lfp_subset_iter[OF mono_union_L]) |
50007
56f269baae76
executable true liveness analysis incl an approximating version
nipkow
parents:
48256
diff
changeset
|
199 |
show "!!X. ?f X \<subseteq> ?fb X" using While.IH by blast |
52072 | 200 |
show "lfp ?f \<subseteq> vars b \<union> rvars c \<union> X" |
201 |
by (metis (full_types) L.simps(5) L_subset_vars rvars.simps(5)) |
|
50007
56f269baae76
executable true liveness analysis incl an approximating version
nipkow
parents:
48256
diff
changeset
|
202 |
qed |
56f269baae76
executable true liveness analysis incl an approximating version
nipkow
parents:
48256
diff
changeset
|
203 |
next |
56f269baae76
executable true liveness analysis incl an approximating version
nipkow
parents:
48256
diff
changeset
|
204 |
case Seq thus ?case by simp (metis (full_types) L_mono monoD subset_trans) |
56f269baae76
executable true liveness analysis incl an approximating version
nipkow
parents:
48256
diff
changeset
|
205 |
qed auto |
56f269baae76
executable true liveness analysis incl an approximating version
nipkow
parents:
48256
diff
changeset
|
206 |
|
45812 | 207 |
end |