author | krauss |
Fri, 09 Jul 2010 16:32:25 +0200 | |
changeset 37757 | dc78d2d9e90a |
parent 30738 | 0842e906300c |
child 37760 | 8380686be5cd |
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 |
|
37757
dc78d2d9e90a
added "while_option", which needs no well-foundedness; defined "while" in terms of "while_option"
krauss
parents:
30738
diff
changeset
|
13 |
subsection {* Option result *} |
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 |
|
37757
dc78d2d9e90a
added "while_option", which needs no well-foundedness; defined "while" in terms of "while_option"
krauss
parents:
30738
diff
changeset
|
55 |
lemma while_option_stop: |
dc78d2d9e90a
added "while_option", which needs no well-foundedness; defined "while" in terms of "while_option"
krauss
parents:
30738
diff
changeset
|
56 |
assumes "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
|
57 |
shows "~ b t" |
dc78d2d9e90a
added "while_option", which needs no well-foundedness; defined "while" in terms of "while_option"
krauss
parents:
30738
diff
changeset
|
58 |
proof - |
dc78d2d9e90a
added "while_option", which needs no well-foundedness; defined "while" in terms of "while_option"
krauss
parents:
30738
diff
changeset
|
59 |
from assms have ex: "\<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
|
60 |
and t: "t = (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
|
61 |
by (auto simp: while_option_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
|
62 |
from LeastI_ex[OF ex] |
dc78d2d9e90a
added "while_option", which needs no well-foundedness; defined "while" in terms of "while_option"
krauss
parents:
30738
diff
changeset
|
63 |
show "~ b t" unfolding t . |
dc78d2d9e90a
added "while_option", which needs no well-foundedness; defined "while" in terms of "while_option"
krauss
parents:
30738
diff
changeset
|
64 |
qed |
dc78d2d9e90a
added "while_option", which needs no well-foundedness; defined "while" in terms of "while_option"
krauss
parents:
30738
diff
changeset
|
65 |
|
dc78d2d9e90a
added "while_option", which needs no well-foundedness; defined "while" in terms of "while_option"
krauss
parents:
30738
diff
changeset
|
66 |
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
|
67 |
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
|
68 |
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
|
69 |
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
|
70 |
shows "P t" |
dc78d2d9e90a
added "while_option", which needs no well-foundedness; defined "while" in terms of "while_option"
krauss
parents:
30738
diff
changeset
|
71 |
proof - |
dc78d2d9e90a
added "while_option", which needs no well-foundedness; defined "while" in terms of "while_option"
krauss
parents:
30738
diff
changeset
|
72 |
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
|
73 |
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
|
74 |
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
|
75 |
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
|
76 |
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
|
77 |
|
dc78d2d9e90a
added "while_option", which needs no well-foundedness; defined "while" in terms of "while_option"
krauss
parents:
30738
diff
changeset
|
78 |
{ 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
|
79 |
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
|
80 |
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
|
81 |
qed |
dc78d2d9e90a
added "while_option", which needs no well-foundedness; defined "while" in terms of "while_option"
krauss
parents:
30738
diff
changeset
|
82 |
|
dc78d2d9e90a
added "while_option", which needs no well-foundedness; defined "while" in terms of "while_option"
krauss
parents:
30738
diff
changeset
|
83 |
|
dc78d2d9e90a
added "while_option", which needs no well-foundedness; defined "while" in terms of "while_option"
krauss
parents:
30738
diff
changeset
|
84 |
subsection {* Totalized version *} |
dc78d2d9e90a
added "while_option", which needs no well-foundedness; defined "while" in terms of "while_option"
krauss
parents:
30738
diff
changeset
|
85 |
|
dc78d2d9e90a
added "while_option", which needs no well-foundedness; defined "while" in terms of "while_option"
krauss
parents:
30738
diff
changeset
|
86 |
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
|
87 |
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
|
88 |
|
dc78d2d9e90a
added "while_option", which needs no well-foundedness; defined "while" in terms of "while_option"
krauss
parents:
30738
diff
changeset
|
89 |
lemma while_unfold: |
dc78d2d9e90a
added "while_option", which needs no well-foundedness; defined "while" in terms of "while_option"
krauss
parents:
30738
diff
changeset
|
90 |
"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
|
91 |
unfolding while_def by (subst while_option_unfold) simp |
10984 | 92 |
|
18372 | 93 |
lemma def_while_unfold: |
94 |
assumes fdef: "f == while test do" |
|
95 |
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
|
96 |
unfolding fdef by (fact while_unfold) |
14300 | 97 |
|
98 |
||
10251 | 99 |
text {* |
100 |
The proof rule for @{term while}, where @{term P} is the invariant. |
|
101 |
*} |
|
102 |
||
18372 | 103 |
theorem while_rule_lemma: |
104 |
assumes invariant: "!!s. P s ==> b s ==> P (c s)" |
|
105 |
and terminate: "!!s. P s ==> \<not> b s ==> Q s" |
|
106 |
and wf: "wf {(t, s). P s \<and> b s \<and> t = c s}" |
|
107 |
shows "P s \<Longrightarrow> Q (while b c s)" |
|
19736 | 108 |
using wf |
109 |
apply (induct s) |
|
18372 | 110 |
apply simp |
111 |
apply (subst while_unfold) |
|
112 |
apply (simp add: invariant terminate) |
|
113 |
done |
|
10251 | 114 |
|
10653 | 115 |
theorem while_rule: |
10984 | 116 |
"[| P s; |
117 |
!!s. [| P s; b s |] ==> P (c s); |
|
118 |
!!s. [| P s; \<not> b s |] ==> Q s; |
|
10997 | 119 |
wf r; |
10984 | 120 |
!!s. [| P s; b s |] ==> (c s, s) \<in> r |] ==> |
121 |
Q (while b c s)" |
|
19736 | 122 |
apply (rule while_rule_lemma) |
123 |
prefer 4 apply assumption |
|
124 |
apply blast |
|
125 |
apply blast |
|
126 |
apply (erule wf_subset) |
|
127 |
apply blast |
|
128 |
done |
|
10653 | 129 |
|
10984 | 130 |
text {* |
131 |
\medskip An application: computation of the @{term lfp} on finite |
|
132 |
sets via iteration. |
|
133 |
*} |
|
134 |
||
135 |
theorem lfp_conv_while: |
|
136 |
"[| mono f; finite U; f U = U |] ==> |
|
137 |
lfp f = fst (while (\<lambda>(A, fA). A \<noteq> fA) (\<lambda>(A, fA). (fA, f fA)) ({}, f {}))" |
|
138 |
apply (rule_tac P = "\<lambda>(A, B). (A \<subseteq> U \<and> B = f A \<and> A \<subseteq> B \<and> B \<subseteq> lfp f)" and |
|
11047 | 139 |
r = "((Pow U \<times> UNIV) \<times> (Pow U \<times> UNIV)) \<inter> |
10984 | 140 |
inv_image finite_psubset (op - U o fst)" in while_rule) |
141 |
apply (subst lfp_unfold) |
|
142 |
apply assumption |
|
143 |
apply (simp add: monoD) |
|
144 |
apply (subst lfp_unfold) |
|
145 |
apply assumption |
|
146 |
apply clarsimp |
|
147 |
apply (blast dest: monoD) |
|
148 |
apply (fastsimp intro!: lfp_lowerbound) |
|
149 |
apply (blast intro: wf_finite_psubset Int_lower2 [THEN [2] wf_subset]) |
|
19769
c40ce2de2020
Added [simp]-lemmas "in_inv_image" and "in_lex_prod" in the spirit of "in_measure".
krauss
parents:
19736
diff
changeset
|
150 |
apply (clarsimp simp add: finite_psubset_def order_less_le) |
10984 | 151 |
apply (blast intro!: finite_Diff dest: monoD) |
152 |
done |
|
153 |
||
154 |
||
37757
dc78d2d9e90a
added "while_option", which needs no well-foundedness; defined "while" in terms of "while_option"
krauss
parents:
30738
diff
changeset
|
155 |
subsection {* Example *} |
10984 | 156 |
|
15197 | 157 |
text{* Cannot use @{thm[source]set_eq_subset} because it leads to |
158 |
looping because the antisymmetry simproc turns the subset relationship |
|
159 |
back into equality. *} |
|
160 |
||
14589 | 161 |
theorem "P (lfp (\<lambda>N::int set. {0} \<union> {(n + 2) mod 6 | n. n \<in> N})) = |
162 |
P {0, 4, 2}" |
|
10997 | 163 |
proof - |
19736 | 164 |
have seteq: "!!A B. (A = B) = ((!a : A. a:B) & (!b:B. b:A))" |
165 |
by blast |
|
10997 | 166 |
have aux: "!!f A B. {f n | n. A n \<or> B n} = {f n | n. A n} \<union> {f n | n. B n}" |
10984 | 167 |
apply blast |
10997 | 168 |
done |
169 |
show ?thesis |
|
11914 | 170 |
apply (subst lfp_conv_while [where ?U = "{0, 1, 2, 3, 4, 5}"]) |
10997 | 171 |
apply (rule monoI) |
172 |
apply blast |
|
173 |
apply simp |
|
174 |
apply (simp add: aux set_eq_subset) |
|
175 |
txt {* The fixpoint computation is performed purely by rewriting: *} |
|
15197 | 176 |
apply (simp add: while_unfold aux seteq del: subset_empty) |
10997 | 177 |
done |
178 |
qed |
|
10251 | 179 |
|
180 |
end |