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;
wenzelm@41959
     1
(*  Title:      HOL/ex/While_Combinator_Example.thy
krauss@37760
     2
    Author:     Tobias Nipkow
krauss@37760
     3
    Copyright   2000 TU Muenchen
krauss@37760
     4
*)
krauss@37760
     5
wenzelm@61343
     6
section \<open>An application of the While combinator\<close>
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
wenzelm@61343
    12
text \<open>Computation of the @{term lfp} on finite sets via 
wenzelm@61343
    13
  iteration.\<close>
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)
nipkow@44890
    28
 apply (fastforce 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
wenzelm@61343
    35
subsection \<open>Example\<close>
krauss@37760
    36
wenzelm@61343
    37
text\<open>Cannot use @{thm[source]set_eq_subset} because it leads to
krauss@37760
    38
looping because the antisymmetry simproc turns the subset relationship
wenzelm@61343
    39
back into equality.\<close>
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)
wenzelm@61343
    55
    txt \<open>The fixpoint computation is performed purely by rewriting:\<close>
krauss@37760
    56
    apply (simp add: while_unfold aux seteq del: subset_empty)
krauss@37760
    57
    done
krauss@37760
    58
qed
krauss@37760
    59
nipkow@62390
    60
end