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