haftmann@22803
|
1 |
(* Title: HOL/Library/While_Combinator.thy
|
wenzelm@10251
|
2 |
Author: Tobias Nipkow
|
krauss@37756
|
3 |
Author: Alexander Krauss
|
wenzelm@10251
|
4 |
*)
|
wenzelm@10251
|
5 |
|
wenzelm@14706
|
6 |
header {* A general ``while'' combinator *}
|
wenzelm@10251
|
7 |
|
nipkow@15131
|
8 |
theory While_Combinator
|
haftmann@30738
|
9 |
imports Main
|
nipkow@15131
|
10 |
begin
|
wenzelm@10251
|
11 |
|
krauss@37759
|
12 |
subsection {* Partial version *}
|
wenzelm@10251
|
13 |
|
krauss@37756
|
14 |
definition while_option :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option" where
|
krauss@37756
|
15 |
"while_option b c s = (if (\<exists>k. ~ b ((c ^^ k) s))
|
krauss@37756
|
16 |
then Some ((c ^^ (LEAST k. ~ b ((c ^^ k) s))) s)
|
krauss@37756
|
17 |
else None)"
|
wenzelm@10251
|
18 |
|
krauss@37756
|
19 |
theorem while_option_unfold[code]:
|
krauss@37756
|
20 |
"while_option b c s = (if b s then while_option b c (c s) else Some s)"
|
krauss@37756
|
21 |
proof cases
|
krauss@37756
|
22 |
assume "b s"
|
krauss@37756
|
23 |
show ?thesis
|
krauss@37756
|
24 |
proof (cases "\<exists>k. ~ b ((c ^^ k) s)")
|
krauss@37756
|
25 |
case True
|
krauss@37756
|
26 |
then obtain k where 1: "~ b ((c ^^ k) s)" ..
|
krauss@37756
|
27 |
with `b s` obtain l where "k = Suc l" by (cases k) auto
|
krauss@37756
|
28 |
with 1 have "~ b ((c ^^ l) (c s))" by (auto simp: funpow_swap1)
|
krauss@37756
|
29 |
then have 2: "\<exists>l. ~ b ((c ^^ l) (c s))" ..
|
krauss@37756
|
30 |
from 1
|
krauss@37756
|
31 |
have "(LEAST k. ~ b ((c ^^ k) s)) = Suc (LEAST l. ~ b ((c ^^ Suc l) s))"
|
krauss@37756
|
32 |
by (rule Least_Suc) (simp add: `b s`)
|
krauss@37756
|
33 |
also have "... = Suc (LEAST l. ~ b ((c ^^ l) (c s)))"
|
krauss@37756
|
34 |
by (simp add: funpow_swap1)
|
krauss@37756
|
35 |
finally
|
krauss@37756
|
36 |
show ?thesis
|
krauss@37756
|
37 |
using True 2 `b s` by (simp add: funpow_swap1 while_option_def)
|
krauss@37756
|
38 |
next
|
krauss@37756
|
39 |
case False
|
krauss@37756
|
40 |
then have "~ (\<exists>l. ~ b ((c ^^ Suc l) s))" by blast
|
krauss@37756
|
41 |
then have "~ (\<exists>l. ~ b ((c ^^ l) (c s)))"
|
krauss@37756
|
42 |
by (simp add: funpow_swap1)
|
krauss@37756
|
43 |
with False `b s` show ?thesis by (simp add: while_option_def)
|
krauss@37756
|
44 |
qed
|
krauss@37756
|
45 |
next
|
krauss@37756
|
46 |
assume [simp]: "~ b s"
|
krauss@37756
|
47 |
have least: "(LEAST k. ~ b ((c ^^ k) s)) = 0"
|
krauss@37756
|
48 |
by (rule Least_equality) auto
|
krauss@37756
|
49 |
moreover
|
krauss@37756
|
50 |
have "\<exists>k. ~ b ((c ^^ k) s)" by (rule exI[of _ "0::nat"]) auto
|
krauss@37756
|
51 |
ultimately show ?thesis unfolding while_option_def by auto
|
krauss@37756
|
52 |
qed
|
krauss@37756
|
53 |
|
nipkow@46705
|
54 |
lemma while_option_stop2:
|
nipkow@46705
|
55 |
"while_option b c s = Some t \<Longrightarrow> EX k. t = (c^^k) s \<and> \<not> b t"
|
nipkow@46705
|
56 |
apply(simp add: while_option_def split: if_splits)
|
blanchet@47193
|
57 |
by (metis (lifting) LeastI_ex)
|
nipkow@46705
|
58 |
|
nipkow@46705
|
59 |
lemma while_option_stop: "while_option b c s = Some t \<Longrightarrow> ~ b t"
|
nipkow@46705
|
60 |
by(metis while_option_stop2)
|
krauss@37756
|
61 |
|
krauss@37756
|
62 |
theorem while_option_rule:
|
krauss@37756
|
63 |
assumes step: "!!s. P s ==> b s ==> P (c s)"
|
krauss@37756
|
64 |
and result: "while_option b c s = Some t"
|
krauss@37756
|
65 |
and init: "P s"
|
krauss@37756
|
66 |
shows "P t"
|
krauss@37756
|
67 |
proof -
|
krauss@37756
|
68 |
def k == "LEAST k. ~ b ((c ^^ k) s)"
|
krauss@37756
|
69 |
from assms have t: "t = (c ^^ k) s"
|
krauss@37756
|
70 |
by (simp add: while_option_def k_def split: if_splits)
|
krauss@37756
|
71 |
have 1: "ALL i<k. b ((c ^^ i) s)"
|
krauss@37756
|
72 |
by (auto simp: k_def dest: not_less_Least)
|
krauss@37756
|
73 |
|
krauss@37756
|
74 |
{ fix i assume "i <= k" then have "P ((c ^^ i) s)"
|
krauss@37756
|
75 |
by (induct i) (auto simp: init step 1) }
|
krauss@37756
|
76 |
thus "P t" by (auto simp: t)
|
krauss@37756
|
77 |
qed
|
krauss@37756
|
78 |
|
traytel@51592
|
79 |
lemma funpow_commute:
|
traytel@51592
|
80 |
"\<lbrakk>\<forall>k' < k. f (c ((c^^k') s)) = c' (f ((c^^k') s))\<rbrakk> \<Longrightarrow> f ((c^^k) s) = (c'^^k) (f s)"
|
traytel@51592
|
81 |
by (induct k arbitrary: s) auto
|
traytel@51592
|
82 |
|
nipkow@55187
|
83 |
lemma while_option_commute_invariant:
|
nipkow@55187
|
84 |
assumes Invariant: "\<And>s. P s \<Longrightarrow> b s \<Longrightarrow> P (c s)"
|
nipkow@55187
|
85 |
assumes TestCommute: "\<And>s. P s \<Longrightarrow> b s = b' (f s)"
|
nipkow@55187
|
86 |
assumes BodyCommute: "\<And>s. P s \<Longrightarrow> b s \<Longrightarrow> f (c s) = c' (f s)"
|
nipkow@55187
|
87 |
assumes Initial: "P s"
|
nipkow@55187
|
88 |
shows "Option.map f (while_option b c s) = while_option b' c' (f s)"
|
traytel@51592
|
89 |
unfolding while_option_def
|
traytel@51592
|
90 |
proof (rule trans[OF if_distrib if_cong], safe, unfold option.inject)
|
nipkow@55187
|
91 |
fix k
|
nipkow@55187
|
92 |
assume "\<not> b ((c ^^ k) s)"
|
nipkow@55187
|
93 |
with Initial show "\<exists>k. \<not> b' ((c' ^^ k) (f s))"
|
traytel@51592
|
94 |
proof (induction k arbitrary: s)
|
nipkow@55187
|
95 |
case 0 thus ?case by (auto simp: TestCommute intro: exI[of _ 0])
|
traytel@51592
|
96 |
next
|
nipkow@55187
|
97 |
case (Suc k) thus ?case
|
nipkow@55187
|
98 |
proof (cases "b s")
|
nipkow@55187
|
99 |
assume "b s"
|
nipkow@55187
|
100 |
with Suc.IH[of "c s"] Suc.prems show ?thesis
|
nipkow@55187
|
101 |
by (metis BodyCommute Invariant comp_apply funpow.simps(2) funpow_swap1)
|
nipkow@55187
|
102 |
next
|
nipkow@55187
|
103 |
assume "\<not> b s"
|
nipkow@55187
|
104 |
with Suc show ?thesis by (auto simp: TestCommute intro: exI [of _ 0])
|
nipkow@55187
|
105 |
qed
|
traytel@51592
|
106 |
qed
|
traytel@51592
|
107 |
next
|
nipkow@55187
|
108 |
fix k
|
nipkow@55187
|
109 |
assume "\<not> b' ((c' ^^ k) (f s))"
|
nipkow@55187
|
110 |
with Initial show "\<exists>k. \<not> b ((c ^^ k) s)"
|
traytel@51592
|
111 |
proof (induction k arbitrary: s)
|
nipkow@55187
|
112 |
case 0 thus ?case by (auto simp: TestCommute intro: exI[of _ 0])
|
traytel@51592
|
113 |
next
|
nipkow@55187
|
114 |
case (Suc k) thus ?case
|
traytel@51592
|
115 |
proof (cases "b s")
|
nipkow@55187
|
116 |
assume "b s"
|
nipkow@55187
|
117 |
with Suc.IH[of "c s"] Suc.prems show ?thesis
|
nipkow@55187
|
118 |
by (metis BodyCommute Invariant comp_apply funpow.simps(2) funpow_swap1)
|
nipkow@55187
|
119 |
next
|
nipkow@55187
|
120 |
assume "\<not> b s"
|
nipkow@55187
|
121 |
with Suc show ?thesis by (auto simp: TestCommute intro: exI [of _ 0])
|
nipkow@55187
|
122 |
qed
|
traytel@51592
|
123 |
qed
|
traytel@51592
|
124 |
next
|
nipkow@55187
|
125 |
fix k
|
nipkow@55187
|
126 |
assume k: "\<not> b' ((c' ^^ k) (f s))"
|
nipkow@55187
|
127 |
have *: "(LEAST k. \<not> b' ((c' ^^ k) (f s))) = (LEAST k. \<not> b ((c ^^ k) s))"
|
nipkow@55187
|
128 |
(is "?k' = ?k")
|
traytel@51592
|
129 |
proof (cases ?k')
|
traytel@51592
|
130 |
case 0
|
nipkow@55187
|
131 |
have "\<not> b' ((c' ^^ 0) (f s))"
|
nipkow@55187
|
132 |
unfolding 0[symmetric] by (rule LeastI[of _ k]) (rule k)
|
nipkow@55187
|
133 |
hence "\<not> b s" by (auto simp: TestCommute Initial)
|
traytel@51592
|
134 |
hence "?k = 0" by (intro Least_equality) auto
|
traytel@51592
|
135 |
with 0 show ?thesis by auto
|
traytel@51592
|
136 |
next
|
traytel@51592
|
137 |
case (Suc k')
|
nipkow@55187
|
138 |
have "\<not> b' ((c' ^^ Suc k') (f s))"
|
nipkow@55187
|
139 |
unfolding Suc[symmetric] by (rule LeastI) (rule k)
|
traytel@51592
|
140 |
moreover
|
traytel@51592
|
141 |
{ fix k assume "k \<le> k'"
|
traytel@51592
|
142 |
hence "k < ?k'" unfolding Suc by simp
|
traytel@51592
|
143 |
hence "b' ((c' ^^ k) (f s))" by (rule iffD1[OF not_not, OF not_less_Least])
|
nipkow@55187
|
144 |
}
|
nipkow@55187
|
145 |
note b' = this
|
traytel@51592
|
146 |
{ fix k assume "k \<le> k'"
|
nipkow@55187
|
147 |
hence "f ((c ^^ k) s) = (c' ^^ k) (f s)"
|
nipkow@55187
|
148 |
and "b ((c ^^ k) s) = b' ((c' ^^ k) (f s))"
|
nipkow@55187
|
149 |
and "P ((c ^^ k) s)"
|
nipkow@55187
|
150 |
by (induct k) (auto simp: b' assms)
|
nipkow@55187
|
151 |
with `k \<le> k'`
|
nipkow@55187
|
152 |
have "b ((c ^^ k) s)"
|
nipkow@55187
|
153 |
and "f ((c ^^ k) s) = (c' ^^ k) (f s)"
|
nipkow@55187
|
154 |
and "P ((c ^^ k) s)"
|
nipkow@55187
|
155 |
by (auto simp: b')
|
nipkow@55187
|
156 |
}
|
nipkow@55187
|
157 |
note b = this(1) and body = this(2) and inv = this(3)
|
nipkow@55187
|
158 |
hence k': "f ((c ^^ k') s) = (c' ^^ k') (f s)" by auto
|
traytel@51592
|
159 |
ultimately show ?thesis unfolding Suc using b
|
nipkow@55187
|
160 |
proof (intro Least_equality[symmetric])
|
nipkow@55187
|
161 |
case goal1
|
nipkow@55187
|
162 |
hence Test: "\<not> b' (f ((c ^^ Suc k') s))"
|
nipkow@55187
|
163 |
by (auto simp: BodyCommute inv b)
|
nipkow@55187
|
164 |
have "P ((c ^^ Suc k') s)" by (auto simp: Invariant inv b)
|
nipkow@55187
|
165 |
with Test show ?case by (auto simp: TestCommute)
|
nipkow@55187
|
166 |
next
|
nipkow@55187
|
167 |
case goal2 thus ?case by (metis not_less_eq_eq)
|
nipkow@55187
|
168 |
qed
|
traytel@51592
|
169 |
qed
|
traytel@51592
|
170 |
have "f ((c ^^ ?k) s) = (c' ^^ ?k') (f s)" unfolding *
|
nipkow@55187
|
171 |
proof (rule funpow_commute, clarify)
|
nipkow@55187
|
172 |
fix k assume "k < ?k"
|
nipkow@55187
|
173 |
hence TestTrue: "b ((c ^^ k) s)" by (auto dest: not_less_Least)
|
nipkow@55187
|
174 |
from `k < ?k` have "P ((c ^^ k) s)"
|
nipkow@55187
|
175 |
proof (induct k)
|
nipkow@55187
|
176 |
case 0 thus ?case by (auto simp: assms)
|
nipkow@55187
|
177 |
next
|
nipkow@55187
|
178 |
case (Suc h)
|
nipkow@55187
|
179 |
hence "P ((c ^^ h) s)" by auto
|
nipkow@55187
|
180 |
with Suc show ?case
|
nipkow@55187
|
181 |
by (auto, metis (lifting, no_types) Invariant Suc_lessD not_less_Least)
|
nipkow@55187
|
182 |
qed
|
nipkow@55187
|
183 |
with TestTrue show "f (c ((c ^^ k) s)) = c' (f ((c ^^ k) s))"
|
nipkow@55187
|
184 |
by (metis BodyCommute)
|
nipkow@55187
|
185 |
qed
|
traytel@51592
|
186 |
thus "\<exists>z. (c ^^ ?k) s = z \<and> f z = (c' ^^ ?k') (f s)" by blast
|
traytel@51592
|
187 |
qed
|
krauss@37756
|
188 |
|
nipkow@55187
|
189 |
lemma while_option_commute:
|
nipkow@55187
|
190 |
assumes "\<And>s. b s = b' (f s)" "\<And>s. \<lbrakk>b s\<rbrakk> \<Longrightarrow> f (c s) = c' (f s)"
|
nipkow@55187
|
191 |
shows "Option.map f (while_option b c s) = while_option b' c' (f s)"
|
nipkow@55187
|
192 |
by(rule while_option_commute_invariant[where P = "\<lambda>_. True"])
|
nipkow@55187
|
193 |
(auto simp add: assms)
|
nipkow@55187
|
194 |
|
krauss@37759
|
195 |
subsection {* Total version *}
|
krauss@37756
|
196 |
|
krauss@37756
|
197 |
definition while :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
|
krauss@37756
|
198 |
where "while b c s = the (while_option b c s)"
|
krauss@37756
|
199 |
|
nipkow@51023
|
200 |
lemma while_unfold [code]:
|
krauss@37756
|
201 |
"while b c s = (if b s then while b c (c s) else s)"
|
krauss@37756
|
202 |
unfolding while_def by (subst while_option_unfold) simp
|
nipkow@10984
|
203 |
|
wenzelm@18372
|
204 |
lemma def_while_unfold:
|
wenzelm@18372
|
205 |
assumes fdef: "f == while test do"
|
wenzelm@18372
|
206 |
shows "f x = (if test x then f(do x) else x)"
|
krauss@37756
|
207 |
unfolding fdef by (fact while_unfold)
|
nipkow@14300
|
208 |
|
nipkow@14300
|
209 |
|
wenzelm@10251
|
210 |
text {*
|
wenzelm@10251
|
211 |
The proof rule for @{term while}, where @{term P} is the invariant.
|
wenzelm@10251
|
212 |
*}
|
wenzelm@10251
|
213 |
|
wenzelm@18372
|
214 |
theorem while_rule_lemma:
|
wenzelm@18372
|
215 |
assumes invariant: "!!s. P s ==> b s ==> P (c s)"
|
wenzelm@18372
|
216 |
and terminate: "!!s. P s ==> \<not> b s ==> Q s"
|
wenzelm@18372
|
217 |
and wf: "wf {(t, s). P s \<and> b s \<and> t = c s}"
|
wenzelm@18372
|
218 |
shows "P s \<Longrightarrow> Q (while b c s)"
|
wenzelm@19736
|
219 |
using wf
|
wenzelm@19736
|
220 |
apply (induct s)
|
wenzelm@18372
|
221 |
apply simp
|
wenzelm@18372
|
222 |
apply (subst while_unfold)
|
wenzelm@18372
|
223 |
apply (simp add: invariant terminate)
|
wenzelm@18372
|
224 |
done
|
wenzelm@10251
|
225 |
|
nipkow@10653
|
226 |
theorem while_rule:
|
nipkow@10984
|
227 |
"[| P s;
|
nipkow@10984
|
228 |
!!s. [| P s; b s |] ==> P (c s);
|
nipkow@10984
|
229 |
!!s. [| P s; \<not> b s |] ==> Q s;
|
wenzelm@10997
|
230 |
wf r;
|
nipkow@10984
|
231 |
!!s. [| P s; b s |] ==> (c s, s) \<in> r |] ==>
|
nipkow@10984
|
232 |
Q (while b c s)"
|
wenzelm@19736
|
233 |
apply (rule while_rule_lemma)
|
wenzelm@19736
|
234 |
prefer 4 apply assumption
|
wenzelm@19736
|
235 |
apply blast
|
wenzelm@19736
|
236 |
apply blast
|
wenzelm@19736
|
237 |
apply (erule wf_subset)
|
wenzelm@19736
|
238 |
apply blast
|
wenzelm@19736
|
239 |
done
|
nipkow@10653
|
240 |
|
nipkow@42584
|
241 |
text{* Proving termination: *}
|
nipkow@42584
|
242 |
|
nipkow@42584
|
243 |
theorem wf_while_option_Some:
|
nipkow@42635
|
244 |
assumes "wf {(t, s). (P s \<and> b s) \<and> t = c s}"
|
nipkow@42635
|
245 |
and "!!s. P s \<Longrightarrow> b s \<Longrightarrow> P(c s)" and "P s"
|
nipkow@42584
|
246 |
shows "EX t. while_option b c s = Some t"
|
nipkow@42635
|
247 |
using assms(1,3)
|
nipkow@55187
|
248 |
proof (induction s)
|
nipkow@55187
|
249 |
case less thus ?case using assms(2)
|
nipkow@55187
|
250 |
by (subst while_option_unfold) simp
|
nipkow@55187
|
251 |
qed
|
nipkow@55187
|
252 |
|
nipkow@55187
|
253 |
lemma wf_rel_while_option_Some:
|
nipkow@55187
|
254 |
assumes wf: "wf R"
|
nipkow@55187
|
255 |
assumes smaller: "\<And>s. P s \<and> b s \<Longrightarrow> (c s, s) \<in> R"
|
nipkow@55187
|
256 |
assumes inv: "\<And>s. P s \<and> b s \<Longrightarrow> P(c s)"
|
nipkow@55187
|
257 |
assumes init: "P s"
|
nipkow@55187
|
258 |
shows "\<exists>t. while_option b c s = Some t"
|
nipkow@55187
|
259 |
proof -
|
nipkow@55187
|
260 |
from smaller have "{(t,s). P s \<and> b s \<and> t = c s} \<subseteq> R" by auto
|
nipkow@55187
|
261 |
with wf have "wf {(t,s). P s \<and> b s \<and> t = c s}" by (auto simp: wf_subset)
|
nipkow@55187
|
262 |
with inv init show ?thesis by (auto simp: wf_while_option_Some)
|
nipkow@55187
|
263 |
qed
|
nipkow@42584
|
264 |
|
nipkow@42584
|
265 |
theorem measure_while_option_Some: fixes f :: "'s \<Rightarrow> nat"
|
nipkow@42635
|
266 |
shows "(!!s. P s \<Longrightarrow> b s \<Longrightarrow> P(c s) \<and> f(c s) < f s)
|
nipkow@42635
|
267 |
\<Longrightarrow> P s \<Longrightarrow> EX t. while_option b c s = Some t"
|
nipkow@42635
|
268 |
by(blast intro: wf_while_option_Some[OF wf_if_measure, of P b f])
|
wenzelm@10251
|
269 |
|
nipkow@46705
|
270 |
text{* Kleene iteration starting from the empty set and assuming some finite
|
nipkow@46705
|
271 |
bounding set: *}
|
nipkow@46705
|
272 |
|
nipkow@46705
|
273 |
lemma while_option_finite_subset_Some: fixes C :: "'a set"
|
nipkow@46705
|
274 |
assumes "mono f" and "!!X. X \<subseteq> C \<Longrightarrow> f X \<subseteq> C" and "finite C"
|
nipkow@46705
|
275 |
shows "\<exists>P. while_option (\<lambda>A. f A \<noteq> A) f {} = Some P"
|
nipkow@46705
|
276 |
proof(rule measure_while_option_Some[where
|
nipkow@46705
|
277 |
f= "%A::'a set. card C - card A" and P= "%A. A \<subseteq> C \<and> A \<subseteq> f A" and s= "{}"])
|
nipkow@46705
|
278 |
fix A assume A: "A \<subseteq> C \<and> A \<subseteq> f A" "f A \<noteq> A"
|
nipkow@46705
|
279 |
show "(f A \<subseteq> C \<and> f A \<subseteq> f (f A)) \<and> card C - card (f A) < card C - card A"
|
nipkow@46705
|
280 |
(is "?L \<and> ?R")
|
nipkow@46705
|
281 |
proof
|
nipkow@46705
|
282 |
show ?L by(metis A(1) assms(2) monoD[OF `mono f`])
|
nipkow@46705
|
283 |
show ?R by (metis A assms(2,3) card_seteq diff_less_mono2 equalityI linorder_le_less_linear rev_finite_subset)
|
nipkow@46705
|
284 |
qed
|
nipkow@46705
|
285 |
qed simp
|
nipkow@46705
|
286 |
|
nipkow@46705
|
287 |
lemma lfp_the_while_option:
|
nipkow@46705
|
288 |
assumes "mono f" and "!!X. X \<subseteq> C \<Longrightarrow> f X \<subseteq> C" and "finite C"
|
nipkow@46705
|
289 |
shows "lfp f = the(while_option (\<lambda>A. f A \<noteq> A) f {})"
|
nipkow@46705
|
290 |
proof-
|
nipkow@46705
|
291 |
obtain P where "while_option (\<lambda>A. f A \<noteq> A) f {} = Some P"
|
nipkow@46705
|
292 |
using while_option_finite_subset_Some[OF assms] by blast
|
nipkow@46705
|
293 |
with while_option_stop2[OF this] lfp_Kleene_iter[OF assms(1)]
|
nipkow@46705
|
294 |
show ?thesis by auto
|
nipkow@46705
|
295 |
qed
|
nipkow@46705
|
296 |
|
nipkow@51195
|
297 |
lemma lfp_while:
|
nipkow@51195
|
298 |
assumes "mono f" and "!!X. X \<subseteq> C \<Longrightarrow> f X \<subseteq> C" and "finite C"
|
nipkow@51195
|
299 |
shows "lfp f = while (\<lambda>A. f A \<noteq> A) f {}"
|
nipkow@51195
|
300 |
unfolding while_def using assms by (rule lfp_the_while_option) blast
|
nipkow@51195
|
301 |
|
nipkow@54354
|
302 |
|
nipkow@54354
|
303 |
text{* Computing the reflexive, transitive closure by iterating a successor
|
nipkow@54354
|
304 |
function. Stops when an element is found that dos not satisfy the test.
|
nipkow@54354
|
305 |
|
nipkow@54354
|
306 |
More refined (and hence more efficient) versions can be found in ITP 2011 paper
|
nipkow@54354
|
307 |
by Nipkow (the theories are in the AFP entry Flyspeck by Nipkow)
|
nipkow@54354
|
308 |
and the AFP article Executable Transitive Closures by René Thiemann. *}
|
nipkow@54354
|
309 |
|
nipkow@54354
|
310 |
definition rtrancl_while :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a list) \<Rightarrow> 'a
|
nipkow@54354
|
311 |
\<Rightarrow> ('a list * 'a set) option"
|
nipkow@54354
|
312 |
where "rtrancl_while p f x =
|
nipkow@54354
|
313 |
while_option (%(ws,_). ws \<noteq> [] \<and> p(hd ws))
|
nipkow@54354
|
314 |
((%(ws,Z).
|
nipkow@54354
|
315 |
let x = hd ws; new = filter (\<lambda>y. y \<notin> Z) (f x)
|
nipkow@55184
|
316 |
in (new @ tl ws, set new \<union> Z)))
|
nipkow@54357
|
317 |
([x],{x})"
|
nipkow@54354
|
318 |
|
nipkow@54354
|
319 |
lemma rtrancl_while_Some: assumes "rtrancl_while p f x = Some(ws,Z)"
|
nipkow@54354
|
320 |
shows "if ws = []
|
nipkow@54354
|
321 |
then Z = {(x,y). y \<in> set(f x)}^* `` {x} \<and> (\<forall>z\<in>Z. p z)
|
nipkow@54354
|
322 |
else \<not>p(hd ws) \<and> hd ws \<in> {(x,y). y \<in> set(f x)}^* `` {x}"
|
nipkow@54354
|
323 |
proof-
|
nipkow@54354
|
324 |
let ?test = "(%(ws,_). ws \<noteq> [] \<and> p(hd ws))"
|
nipkow@54354
|
325 |
let ?step = "(%(ws,Z).
|
nipkow@54354
|
326 |
let x = hd ws; new = filter (\<lambda>y. y \<notin> Z) (f x)
|
nipkow@55184
|
327 |
in (new @ tl ws, set new \<union> Z))"
|
nipkow@54354
|
328 |
let ?R = "{(x,y). y \<in> set(f x)}"
|
nipkow@54357
|
329 |
let ?Inv = "%(ws,Z). x \<in> Z \<and> set ws \<subseteq> Z \<and> ?R `` (Z - set ws) \<subseteq> Z \<and>
|
nipkow@54357
|
330 |
Z \<subseteq> ?R^* `` {x} \<and> (\<forall>z\<in>Z - set ws. p z)"
|
nipkow@54354
|
331 |
{ fix ws Z assume 1: "?Inv(ws,Z)" and 2: "?test(ws,Z)"
|
nipkow@54354
|
332 |
from 2 obtain v vs where [simp]: "ws = v#vs" by (auto simp: neq_Nil_conv)
|
nipkow@54354
|
333 |
have "?Inv(?step (ws,Z))" using 1 2
|
nipkow@54354
|
334 |
by (auto intro: rtrancl.rtrancl_into_rtrancl)
|
nipkow@54354
|
335 |
} note inv = this
|
nipkow@54354
|
336 |
hence "!!p. ?Inv p \<Longrightarrow> ?test p \<Longrightarrow> ?Inv(?step p)"
|
nipkow@54354
|
337 |
apply(tactic {* split_all_tac @{context} 1 *})
|
nipkow@54354
|
338 |
using inv by iprover
|
nipkow@54357
|
339 |
moreover have "?Inv ([x],{x})" by (simp)
|
nipkow@54354
|
340 |
ultimately have I: "?Inv (ws,Z)"
|
nipkow@54354
|
341 |
by (rule while_option_rule[OF _ assms[unfolded rtrancl_while_def]])
|
nipkow@54354
|
342 |
{ assume "ws = []"
|
nipkow@54354
|
343 |
hence ?thesis using I
|
nipkow@54354
|
344 |
by (auto simp del:Image_Collect_split dest: Image_closed_trancl)
|
nipkow@54354
|
345 |
} moreover
|
nipkow@54354
|
346 |
{ assume "ws \<noteq> []"
|
nipkow@54354
|
347 |
hence ?thesis using I while_option_stop[OF assms[unfolded rtrancl_while_def]]
|
nipkow@54354
|
348 |
by (simp add: subset_iff)
|
nipkow@54354
|
349 |
}
|
nipkow@54354
|
350 |
ultimately show ?thesis by simp
|
nipkow@54354
|
351 |
qed
|
nipkow@54354
|
352 |
|
wenzelm@10251
|
353 |
end
|