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 [2] 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