author | hoelzl |
Thu, 17 Jan 2013 11:59:12 +0100 | |
changeset 50936 | b28f258ebc1a |
parent 50577 | cfbad2d08412 |
child 53217 | 1a8673a6d669 |
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 |
Copyright 2000 TU Muenchen |
5 |
*) |
|
6 |
||
14706 | 7 |
header {* A general ``while'' combinator *} |
10251 | 8 |
|
15131 | 9 |
theory While_Combinator |
30738 | 10 |
imports Main |
15131 | 11 |
begin |
10251 | 12 |
|
37760 | 13 |
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
|
14 |
|
dc78d2d9e90a
added "while_option", which needs no well-foundedness; defined "while" in terms of "while_option"
krauss
parents:
30738
diff
changeset
|
15 |
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
|
16 |
"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
|
17 |
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
|
18 |
else None)" |
10251 | 19 |
|
37757
dc78d2d9e90a
added "while_option", which needs no well-foundedness; defined "while" in terms of "while_option"
krauss
parents:
30738
diff
changeset
|
20 |
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
|
21 |
"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
|
22 |
proof cases |
dc78d2d9e90a
added "while_option", which needs no well-foundedness; defined "while" in terms of "while_option"
krauss
parents:
30738
diff
changeset
|
23 |
assume "b s" |
dc78d2d9e90a
added "while_option", which needs no well-foundedness; defined "while" in terms of "while_option"
krauss
parents:
30738
diff
changeset
|
24 |
show ?thesis |
dc78d2d9e90a
added "while_option", which needs no well-foundedness; defined "while" in terms of "while_option"
krauss
parents:
30738
diff
changeset
|
25 |
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
|
26 |
case True |
dc78d2d9e90a
added "while_option", which needs no well-foundedness; defined "while" in terms of "while_option"
krauss
parents:
30738
diff
changeset
|
27 |
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
|
28 |
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
|
29 |
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
|
30 |
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
|
31 |
from 1 |
dc78d2d9e90a
added "while_option", which needs no well-foundedness; defined "while" in terms of "while_option"
krauss
parents:
30738
diff
changeset
|
32 |
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
|
33 |
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
|
34 |
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
|
35 |
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
|
36 |
finally |
dc78d2d9e90a
added "while_option", which needs no well-foundedness; defined "while" in terms of "while_option"
krauss
parents:
30738
diff
changeset
|
37 |
show ?thesis |
dc78d2d9e90a
added "while_option", which needs no well-foundedness; defined "while" in terms of "while_option"
krauss
parents:
30738
diff
changeset
|
38 |
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
|
39 |
next |
dc78d2d9e90a
added "while_option", which needs no well-foundedness; defined "while" in terms of "while_option"
krauss
parents:
30738
diff
changeset
|
40 |
case False |
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 ^^ 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
|
42 |
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
|
43 |
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
|
44 |
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
|
45 |
qed |
dc78d2d9e90a
added "while_option", which needs no well-foundedness; defined "while" in terms of "while_option"
krauss
parents:
30738
diff
changeset
|
46 |
next |
dc78d2d9e90a
added "while_option", which needs no well-foundedness; defined "while" in terms of "while_option"
krauss
parents:
30738
diff
changeset
|
47 |
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
|
48 |
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
|
49 |
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
|
50 |
moreover |
dc78d2d9e90a
added "while_option", which needs no well-foundedness; defined "while" in terms of "while_option"
krauss
parents:
30738
diff
changeset
|
51 |
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
|
52 |
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
|
53 |
qed |
10251 | 54 |
|
45834 | 55 |
lemma while_option_stop2: |
56 |
"while_option b c s = Some t \<Longrightarrow> EX k. t = (c^^k) s \<and> \<not> b t" |
|
57 |
apply(simp add: while_option_def split: if_splits) |
|
46365 | 58 |
by (metis (lifting) LeastI_ex) |
45834 | 59 |
|
60 |
lemma while_option_stop: "while_option b c s = Some t \<Longrightarrow> ~ b t" |
|
61 |
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
|
62 |
|
dc78d2d9e90a
added "while_option", which needs no well-foundedness; defined "while" in terms of "while_option"
krauss
parents:
30738
diff
changeset
|
63 |
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
|
64 |
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
|
65 |
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
|
66 |
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
|
67 |
shows "P t" |
dc78d2d9e90a
added "while_option", which needs no well-foundedness; defined "while" in terms of "while_option"
krauss
parents:
30738
diff
changeset
|
68 |
proof - |
dc78d2d9e90a
added "while_option", which needs no well-foundedness; defined "while" in terms of "while_option"
krauss
parents:
30738
diff
changeset
|
69 |
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
|
70 |
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
|
71 |
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
|
72 |
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
|
73 |
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
|
74 |
|
dc78d2d9e90a
added "while_option", which needs no well-foundedness; defined "while" in terms of "while_option"
krauss
parents:
30738
diff
changeset
|
75 |
{ 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
|
76 |
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
|
77 |
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
|
78 |
qed |
dc78d2d9e90a
added "while_option", which needs no well-foundedness; defined "while" in terms of "while_option"
krauss
parents:
30738
diff
changeset
|
79 |
|
50577 | 80 |
lemma funpow_commute: |
81 |
"\<lbrakk>\<forall>k' < k. f (c ((c^^k') s)) = c' (f ((c^^k') s))\<rbrakk> \<Longrightarrow> f ((c^^k) s) = (c'^^k) (f s)" |
|
82 |
by (induct k arbitrary: s) auto |
|
83 |
||
84 |
lemma while_option_commute: |
|
85 |
assumes "\<And>s. b s = b' (f s)" "\<And>s. \<lbrakk>b s\<rbrakk> \<Longrightarrow> f (c s) = c' (f s)" |
|
86 |
shows "Option.map f (while_option b c s) = while_option b' c' (f s)" |
|
87 |
unfolding while_option_def |
|
88 |
proof (rule trans[OF if_distrib if_cong], safe, unfold option.inject) |
|
89 |
fix k assume "\<not> b ((c ^^ k) s)" |
|
90 |
thus "\<exists>k. \<not> b' ((c' ^^ k) (f s))" |
|
91 |
proof (induction k arbitrary: s) |
|
92 |
case 0 thus ?case by (auto simp: assms(1) intro: exI[of _ 0]) |
|
93 |
next |
|
94 |
case (Suc k) |
|
95 |
hence "\<not> b ((c^^k) (c s))" by (auto simp: funpow_swap1) |
|
96 |
then guess k by (rule exE[OF Suc.IH[of "c s"]]) |
|
97 |
with assms show ?case by (cases "b s") (auto simp: funpow_swap1 intro: exI[of _ "Suc k"] exI[of _ "0"]) |
|
98 |
qed |
|
99 |
next |
|
100 |
fix k assume "\<not> b' ((c' ^^ k) (f s))" |
|
101 |
thus "\<exists>k. \<not> b ((c ^^ k) s)" |
|
102 |
proof (induction k arbitrary: s) |
|
103 |
case 0 thus ?case by (auto simp: assms(1) intro: exI[of _ 0]) |
|
104 |
next |
|
105 |
case (Suc k) |
|
106 |
hence *: "\<not> b' ((c'^^k) (c' (f s)))" by (auto simp: funpow_swap1) |
|
107 |
show ?case |
|
108 |
proof (cases "b s") |
|
109 |
case True |
|
110 |
with assms(2) * have "\<not> b' ((c'^^k) (f (c s)))" by simp |
|
111 |
then guess k by (rule exE[OF Suc.IH[of "c s"]]) |
|
112 |
thus ?thesis by (auto simp: funpow_swap1 intro: exI[of _ "Suc k"]) |
|
113 |
qed (auto intro: exI[of _ "0"]) |
|
114 |
qed |
|
115 |
next |
|
116 |
fix k assume k: "\<not> b' ((c' ^^ k) (f s))" |
|
117 |
have *: "(LEAST k. \<not> b' ((c' ^^ k) (f s))) = (LEAST k. \<not> b ((c ^^ k) s))" (is "?k' = ?k") |
|
118 |
proof (cases ?k') |
|
119 |
case 0 |
|
120 |
have "\<not> b' ((c'^^0) (f s))" unfolding 0[symmetric] by (rule LeastI[of _ k]) (rule k) |
|
121 |
hence "\<not> b s" unfolding assms(1) by simp |
|
122 |
hence "?k = 0" by (intro Least_equality) auto |
|
123 |
with 0 show ?thesis by auto |
|
124 |
next |
|
125 |
case (Suc k') |
|
126 |
have "\<not> b' ((c'^^Suc k') (f s))" unfolding Suc[symmetric] by (rule LeastI) (rule k) |
|
127 |
moreover |
|
128 |
{ fix k assume "k \<le> k'" |
|
129 |
hence "k < ?k'" unfolding Suc by simp |
|
130 |
hence "b' ((c' ^^ k) (f s))" by (rule iffD1[OF not_not, OF not_less_Least]) |
|
131 |
} note b' = this |
|
132 |
{ fix k assume "k \<le> k'" |
|
133 |
hence "f ((c ^^ k) s) = (c'^^k) (f s)" by (induct k) (auto simp: b' assms) |
|
134 |
with `k \<le> k'` have "b ((c^^k) s)" |
|
135 |
proof (induct k) |
|
136 |
case (Suc k) thus ?case unfolding assms(1) by (simp only: b') |
|
137 |
qed (simp add: b'[of 0, simplified] assms(1)) |
|
138 |
} note b = this |
|
139 |
hence k': "f ((c^^k') s) = (c'^^k') (f s)" by (induct k') (auto simp: assms(2)) |
|
140 |
ultimately show ?thesis unfolding Suc using b |
|
141 |
by (intro sym[OF Least_equality]) |
|
142 |
(auto simp add: assms(1) assms(2)[OF b] k' not_less_eq_eq[symmetric]) |
|
143 |
qed |
|
144 |
have "f ((c ^^ ?k) s) = (c' ^^ ?k') (f s)" unfolding * |
|
145 |
by (auto intro: funpow_commute assms(2) dest: not_less_Least) |
|
146 |
thus "\<exists>z. (c ^^ ?k) s = z \<and> f z = (c' ^^ ?k') (f s)" by blast |
|
147 |
qed |
|
37757
dc78d2d9e90a
added "while_option", which needs no well-foundedness; defined "while" in terms of "while_option"
krauss
parents:
30738
diff
changeset
|
148 |
|
37760 | 149 |
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
|
150 |
|
dc78d2d9e90a
added "while_option", which needs no well-foundedness; defined "while" in terms of "while_option"
krauss
parents:
30738
diff
changeset
|
151 |
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
|
152 |
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
|
153 |
|
50008 | 154 |
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
|
155 |
"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
|
156 |
unfolding while_def by (subst while_option_unfold) simp |
10984 | 157 |
|
18372 | 158 |
lemma def_while_unfold: |
159 |
assumes fdef: "f == while test do" |
|
160 |
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
|
161 |
unfolding fdef by (fact while_unfold) |
14300 | 162 |
|
163 |
||
10251 | 164 |
text {* |
165 |
The proof rule for @{term while}, where @{term P} is the invariant. |
|
166 |
*} |
|
167 |
||
18372 | 168 |
theorem while_rule_lemma: |
169 |
assumes invariant: "!!s. P s ==> b s ==> P (c s)" |
|
170 |
and terminate: "!!s. P s ==> \<not> b s ==> Q s" |
|
171 |
and wf: "wf {(t, s). P s \<and> b s \<and> t = c s}" |
|
172 |
shows "P s \<Longrightarrow> Q (while b c s)" |
|
19736 | 173 |
using wf |
174 |
apply (induct s) |
|
18372 | 175 |
apply simp |
176 |
apply (subst while_unfold) |
|
177 |
apply (simp add: invariant terminate) |
|
178 |
done |
|
10251 | 179 |
|
10653 | 180 |
theorem while_rule: |
10984 | 181 |
"[| P s; |
182 |
!!s. [| P s; b s |] ==> P (c s); |
|
183 |
!!s. [| P s; \<not> b s |] ==> Q s; |
|
10997 | 184 |
wf r; |
10984 | 185 |
!!s. [| P s; b s |] ==> (c s, s) \<in> r |] ==> |
186 |
Q (while b c s)" |
|
19736 | 187 |
apply (rule while_rule_lemma) |
188 |
prefer 4 apply assumption |
|
189 |
apply blast |
|
190 |
apply blast |
|
191 |
apply (erule wf_subset) |
|
192 |
apply blast |
|
193 |
done |
|
10653 | 194 |
|
41720 | 195 |
text{* Proving termination: *} |
196 |
||
197 |
theorem wf_while_option_Some: |
|
41764 | 198 |
assumes "wf {(t, s). (P s \<and> b s) \<and> t = c s}" |
199 |
and "!!s. P s \<Longrightarrow> b s \<Longrightarrow> P(c s)" and "P s" |
|
41720 | 200 |
shows "EX t. while_option b c s = Some t" |
41764 | 201 |
using assms(1,3) |
41720 | 202 |
apply (induct s) |
41764 | 203 |
using assms(2) |
41720 | 204 |
apply (subst while_option_unfold) |
205 |
apply simp |
|
206 |
done |
|
207 |
||
208 |
theorem measure_while_option_Some: fixes f :: "'s \<Rightarrow> nat" |
|
41764 | 209 |
shows "(!!s. P s \<Longrightarrow> b s \<Longrightarrow> P(c s) \<and> f(c s) < f s) |
210 |
\<Longrightarrow> P s \<Longrightarrow> EX t. while_option b c s = Some t" |
|
211 |
by(blast intro: wf_while_option_Some[OF wf_if_measure, of P b f]) |
|
10251 | 212 |
|
45834 | 213 |
text{* Kleene iteration starting from the empty set and assuming some finite |
214 |
bounding set: *} |
|
215 |
||
216 |
lemma while_option_finite_subset_Some: fixes C :: "'a set" |
|
217 |
assumes "mono f" and "!!X. X \<subseteq> C \<Longrightarrow> f X \<subseteq> C" and "finite C" |
|
218 |
shows "\<exists>P. while_option (\<lambda>A. f A \<noteq> A) f {} = Some P" |
|
219 |
proof(rule measure_while_option_Some[where |
|
220 |
f= "%A::'a set. card C - card A" and P= "%A. A \<subseteq> C \<and> A \<subseteq> f A" and s= "{}"]) |
|
221 |
fix A assume A: "A \<subseteq> C \<and> A \<subseteq> f A" "f A \<noteq> A" |
|
222 |
show "(f A \<subseteq> C \<and> f A \<subseteq> f (f A)) \<and> card C - card (f A) < card C - card A" |
|
223 |
(is "?L \<and> ?R") |
|
224 |
proof |
|
225 |
show ?L by(metis A(1) assms(2) monoD[OF `mono f`]) |
|
226 |
show ?R by (metis A assms(2,3) card_seteq diff_less_mono2 equalityI linorder_le_less_linear rev_finite_subset) |
|
227 |
qed |
|
228 |
qed simp |
|
229 |
||
230 |
lemma lfp_the_while_option: |
|
231 |
assumes "mono f" and "!!X. X \<subseteq> C \<Longrightarrow> f X \<subseteq> C" and "finite C" |
|
232 |
shows "lfp f = the(while_option (\<lambda>A. f A \<noteq> A) f {})" |
|
233 |
proof- |
|
234 |
obtain P where "while_option (\<lambda>A. f A \<noteq> A) f {} = Some P" |
|
235 |
using while_option_finite_subset_Some[OF assms] by blast |
|
236 |
with while_option_stop2[OF this] lfp_Kleene_iter[OF assms(1)] |
|
237 |
show ?thesis by auto |
|
238 |
qed |
|
239 |
||
50180 | 240 |
lemma lfp_while: |
241 |
assumes "mono f" and "!!X. X \<subseteq> C \<Longrightarrow> f X \<subseteq> C" and "finite C" |
|
242 |
shows "lfp f = while (\<lambda>A. f A \<noteq> A) f {}" |
|
243 |
unfolding while_def using assms by (rule lfp_the_while_option) blast |
|
244 |
||
10251 | 245 |
end |