src/HOL/Library/While_Combinator.thy
author haftmann
Fri Mar 27 10:05:11 2009 +0100 (2009-03-27)
changeset 30738 0842e906300c
parent 27487 c8a6ce181805
child 37757 dc78d2d9e90a
permissions -rw-r--r--
normalized imports
haftmann@22803
     1
(*  Title:      HOL/Library/While_Combinator.thy
wenzelm@10251
     2
    Author:     Tobias Nipkow
wenzelm@10251
     3
    Copyright   2000 TU Muenchen
wenzelm@10251
     4
*)
wenzelm@10251
     5
wenzelm@14706
     6
header {* A general ``while'' combinator *}
wenzelm@10251
     7
nipkow@15131
     8
theory While_Combinator
haftmann@30738
     9
imports Main
nipkow@15131
    10
begin
wenzelm@10251
    11
krauss@23821
    12
text {* 
krauss@23821
    13
  We define the while combinator as the "mother of all tail recursive functions".
wenzelm@10251
    14
*}
wenzelm@10251
    15
krauss@23821
    16
function (tailrec) while :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
krauss@23821
    17
where
krauss@23821
    18
  while_unfold[simp del]: "while b c s = (if b s then while b c (c s) else s)"
krauss@23821
    19
by auto
wenzelm@10251
    20
krauss@23821
    21
declare while_unfold[code]
nipkow@10984
    22
wenzelm@18372
    23
lemma def_while_unfold:
wenzelm@18372
    24
  assumes fdef: "f == while test do"
wenzelm@18372
    25
  shows "f x = (if test x then f(do x) else x)"
nipkow@14300
    26
proof -
nipkow@14300
    27
  have "f x = while test do x" using fdef by simp
nipkow@14300
    28
  also have "\<dots> = (if test x then while test do (do x) else x)"
nipkow@14300
    29
    by(rule while_unfold)
nipkow@14300
    30
  also have "\<dots> = (if test x then f(do x) else x)" by(simp add:fdef[symmetric])
nipkow@14300
    31
  finally show ?thesis .
nipkow@14300
    32
qed
nipkow@14300
    33
nipkow@14300
    34
wenzelm@10251
    35
text {*
wenzelm@10251
    36
 The proof rule for @{term while}, where @{term P} is the invariant.
wenzelm@10251
    37
*}
wenzelm@10251
    38
wenzelm@18372
    39
theorem while_rule_lemma:
wenzelm@18372
    40
  assumes invariant: "!!s. P s ==> b s ==> P (c s)"
wenzelm@18372
    41
    and terminate: "!!s. P s ==> \<not> b s ==> Q s"
wenzelm@18372
    42
    and wf: "wf {(t, s). P s \<and> b s \<and> t = c s}"
wenzelm@18372
    43
  shows "P s \<Longrightarrow> Q (while b c s)"
wenzelm@19736
    44
  using wf
wenzelm@19736
    45
  apply (induct s)
wenzelm@18372
    46
  apply simp
wenzelm@18372
    47
  apply (subst while_unfold)
wenzelm@18372
    48
  apply (simp add: invariant terminate)
wenzelm@18372
    49
  done
wenzelm@10251
    50
nipkow@10653
    51
theorem while_rule:
nipkow@10984
    52
  "[| P s;
nipkow@10984
    53
      !!s. [| P s; b s  |] ==> P (c s);
nipkow@10984
    54
      !!s. [| P s; \<not> b s  |] ==> Q s;
wenzelm@10997
    55
      wf r;
nipkow@10984
    56
      !!s. [| P s; b s  |] ==> (c s, s) \<in> r |] ==>
nipkow@10984
    57
   Q (while b c s)"
wenzelm@19736
    58
  apply (rule while_rule_lemma)
wenzelm@19736
    59
     prefer 4 apply assumption
wenzelm@19736
    60
    apply blast
wenzelm@19736
    61
   apply blast
wenzelm@19736
    62
  apply (erule wf_subset)
wenzelm@19736
    63
  apply blast
wenzelm@19736
    64
  done
nipkow@10653
    65
nipkow@10984
    66
text {*
nipkow@10984
    67
 \medskip An application: computation of the @{term lfp} on finite
nipkow@10984
    68
 sets via iteration.
nipkow@10984
    69
*}
nipkow@10984
    70
nipkow@10984
    71
theorem lfp_conv_while:
nipkow@10984
    72
  "[| mono f; finite U; f U = U |] ==>
nipkow@10984
    73
    lfp f = fst (while (\<lambda>(A, fA). A \<noteq> fA) (\<lambda>(A, fA). (fA, f fA)) ({}, f {}))"
nipkow@10984
    74
apply (rule_tac P = "\<lambda>(A, B). (A \<subseteq> U \<and> B = f A \<and> A \<subseteq> B \<and> B \<subseteq> lfp f)" and
wenzelm@11047
    75
                r = "((Pow U \<times> UNIV) \<times> (Pow U \<times> UNIV)) \<inter>
nipkow@10984
    76
                     inv_image finite_psubset (op - U o fst)" in while_rule)
nipkow@10984
    77
   apply (subst lfp_unfold)
nipkow@10984
    78
    apply assumption
nipkow@10984
    79
   apply (simp add: monoD)
nipkow@10984
    80
  apply (subst lfp_unfold)
nipkow@10984
    81
   apply assumption
nipkow@10984
    82
  apply clarsimp
nipkow@10984
    83
  apply (blast dest: monoD)
nipkow@10984
    84
 apply (fastsimp intro!: lfp_lowerbound)
nipkow@10984
    85
 apply (blast intro: wf_finite_psubset Int_lower2 [THEN [2] wf_subset])
krauss@19769
    86
apply (clarsimp simp add: finite_psubset_def order_less_le)
nipkow@10984
    87
apply (blast intro!: finite_Diff dest: monoD)
nipkow@10984
    88
done
nipkow@10984
    89
nipkow@10984
    90
nipkow@10984
    91
text {*
wenzelm@14589
    92
 An example of using the @{term while} combinator.
nipkow@10984
    93
*}
nipkow@10984
    94
nipkow@15197
    95
text{* Cannot use @{thm[source]set_eq_subset} because it leads to
nipkow@15197
    96
looping because the antisymmetry simproc turns the subset relationship
nipkow@15197
    97
back into equality. *}
nipkow@15197
    98
wenzelm@14589
    99
theorem "P (lfp (\<lambda>N::int set. {0} \<union> {(n + 2) mod 6 | n. n \<in> N})) =
wenzelm@14589
   100
  P {0, 4, 2}"
wenzelm@10997
   101
proof -
wenzelm@19736
   102
  have seteq: "!!A B. (A = B) = ((!a : A. a:B) & (!b:B. b:A))"
wenzelm@19736
   103
    by blast
wenzelm@10997
   104
  have aux: "!!f A B. {f n | n. A n \<or> B n} = {f n | n. A n} \<union> {f n | n. B n}"
nipkow@10984
   105
    apply blast
wenzelm@10997
   106
    done
wenzelm@10997
   107
  show ?thesis
wenzelm@11914
   108
    apply (subst lfp_conv_while [where ?U = "{0, 1, 2, 3, 4, 5}"])
wenzelm@10997
   109
       apply (rule monoI)
wenzelm@10997
   110
      apply blast
wenzelm@10997
   111
     apply simp
wenzelm@10997
   112
    apply (simp add: aux set_eq_subset)
wenzelm@10997
   113
    txt {* The fixpoint computation is performed purely by rewriting: *}
nipkow@15197
   114
    apply (simp add: while_unfold aux seteq del: subset_empty)
wenzelm@10997
   115
    done
wenzelm@10997
   116
qed
wenzelm@10251
   117
wenzelm@10251
   118
end