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