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