src/HOL/ex/While_Combinator_Example.thy
 author wenzelm Wed Jun 22 10:09:20 2016 +0200 (2016-06-22) changeset 63343 fb5d8a50c641 parent 62390 842917225d56 child 66453 cc19f7ca2ed6 permissions -rw-r--r--
bundle lifting_syntax;
```     1 (*  Title:      HOL/ex/While_Combinator_Example.thy
```
```     2     Author:     Tobias Nipkow
```
```     3     Copyright   2000 TU Muenchen
```
```     4 *)
```
```     5
```
```     6 section \<open>An application of the While combinator\<close>
```
```     7
```
```     8 theory While_Combinator_Example
```
```     9 imports "~~/src/HOL/Library/While_Combinator"
```
```    10 begin
```
```    11
```
```    12 text \<open>Computation of the @{term lfp} on finite sets via
```
```    13   iteration.\<close>
```
```    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 (fastforce intro!: lfp_lowerbound)
```
```    29  apply (blast intro: wf_finite_psubset Int_lower2 [THEN  wf_subset])
```
```    30 apply (clarsimp simp add: finite_psubset_def order_less_le)
```
```    31 apply (blast dest: monoD)
```
```    32 done
```
```    33
```
```    34
```
```    35 subsection \<open>Example\<close>
```
```    36
```
```    37 text\<open>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.\<close>
```
```    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 \<open>The fixpoint computation is performed purely by rewriting:\<close>
```
```    56     apply (simp add: while_unfold aux seteq del: subset_empty)
```
```    57     done
```
```    58 qed
```
```    59
```
```    60 end
```