|
1 (* Title: HOL/Library/While_Combinator.thy |
|
2 Author: Tobias Nipkow |
|
3 Copyright 2000 TU Muenchen |
|
4 *) |
|
5 |
|
6 header {* An application of the While combinator *} |
|
7 |
|
8 theory While_Combinator_Example |
|
9 imports While_Combinator |
|
10 begin |
|
11 |
|
12 text {* Computation of the @{term lfp} on finite sets via |
|
13 iteration. *} |
|
14 |
|
15 theorem lfp_conv_while: |
|
16 "[| mono f; finite U; f U = U |] ==> |
|
17 lfp f = fst (while (\<lambda>(A, fA). A \<noteq> fA) (\<lambda>(A, fA). (fA, f fA)) ({}, f {}))" |
|
18 apply (rule_tac P = "\<lambda>(A, B). (A \<subseteq> U \<and> B = f A \<and> A \<subseteq> B \<and> B \<subseteq> lfp f)" and |
|
19 r = "((Pow U \<times> UNIV) \<times> (Pow U \<times> UNIV)) \<inter> |
|
20 inv_image finite_psubset (op - U o fst)" in while_rule) |
|
21 apply (subst lfp_unfold) |
|
22 apply assumption |
|
23 apply (simp add: monoD) |
|
24 apply (subst lfp_unfold) |
|
25 apply assumption |
|
26 apply clarsimp |
|
27 apply (blast dest: monoD) |
|
28 apply (fastsimp intro!: lfp_lowerbound) |
|
29 apply (blast intro: wf_finite_psubset Int_lower2 [THEN [2] wf_subset]) |
|
30 apply (clarsimp simp add: finite_psubset_def order_less_le) |
|
31 apply (blast intro!: finite_Diff dest: monoD) |
|
32 done |
|
33 |
|
34 |
|
35 subsection {* Example *} |
|
36 |
|
37 text{* Cannot use @{thm[source]set_eq_subset} because it leads to |
|
38 looping because the antisymmetry simproc turns the subset relationship |
|
39 back into equality. *} |
|
40 |
|
41 theorem "P (lfp (\<lambda>N::int set. {0} \<union> {(n + 2) mod 6 | n. n \<in> N})) = |
|
42 P {0, 4, 2}" |
|
43 proof - |
|
44 have seteq: "!!A B. (A = B) = ((!a : A. a:B) & (!b:B. b:A))" |
|
45 by blast |
|
46 have aux: "!!f A B. {f n | n. A n \<or> B n} = {f n | n. A n} \<union> {f n | n. B n}" |
|
47 apply blast |
|
48 done |
|
49 show ?thesis |
|
50 apply (subst lfp_conv_while [where ?U = "{0, 1, 2, 3, 4, 5}"]) |
|
51 apply (rule monoI) |
|
52 apply blast |
|
53 apply simp |
|
54 apply (simp add: aux set_eq_subset) |
|
55 txt {* The fixpoint computation is performed purely by rewriting: *} |
|
56 apply (simp add: while_unfold aux seteq del: subset_empty) |
|
57 done |
|
58 qed |
|
59 |
|
60 end |