src/HOL/Library/While_Combinator.thy
author wenzelm
Thu May 06 14:14:18 2004 +0200 (2004-05-06)
changeset 14706 71590b7733b7
parent 14589 feae7b5fd425
child 15131 c69542757a4d
permissions -rw-r--r--
tuned document;
     1 (*  Title:      HOL/Library/While.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   2000 TU Muenchen
     5 *)
     6 
     7 header {* A general ``while'' combinator *}
     8 
     9 theory While_Combinator = Main:
    10 
    11 text {*
    12  We define a while-combinator @{term while} and prove: (a) an
    13  unrestricted unfolding law (even if while diverges!)  (I got this
    14  idea from Wolfgang Goerigk), and (b) the invariant rule for reasoning
    15  about @{term while}.
    16 *}
    17 
    18 consts while_aux :: "('a => bool) \<times> ('a => 'a) \<times> 'a => 'a"
    19 recdef (permissive) while_aux
    20   "same_fst (\<lambda>b. True) (\<lambda>b. same_fst (\<lambda>c. True) (\<lambda>c.
    21       {(t, s).  b s \<and> c s = t \<and>
    22         \<not> (\<exists>f. f (0::nat) = s \<and> (\<forall>i. b (f i) \<and> c (f i) = f (i + 1)))}))"
    23   "while_aux (b, c, s) =
    24     (if (\<exists>f. f (0::nat) = s \<and> (\<forall>i. b (f i) \<and> c (f i) = f (i + 1)))
    25       then arbitrary
    26       else if b s then while_aux (b, c, c s)
    27       else s)"
    28 
    29 recdef_tc while_aux_tc: while_aux
    30   apply (rule wf_same_fst)
    31   apply (rule wf_same_fst)
    32   apply (simp add: wf_iff_no_infinite_down_chain)
    33   apply blast
    34   done
    35 
    36 constdefs
    37   while :: "('a => bool) => ('a => 'a) => 'a => 'a"
    38   "while b c s == while_aux (b, c, s)"
    39 
    40 lemma while_aux_unfold:
    41   "while_aux (b, c, s) =
    42     (if \<exists>f. f (0::nat) = s \<and> (\<forall>i. b (f i) \<and> c (f i) = f (i + 1))
    43       then arbitrary
    44       else if b s then while_aux (b, c, c s)
    45       else s)"
    46   apply (rule while_aux_tc [THEN while_aux.simps [THEN trans]])
    47   apply (rule refl)
    48   done
    49 
    50 text {*
    51  The recursion equation for @{term while}: directly executable!
    52 *}
    53 
    54 theorem while_unfold [code]:
    55     "while b c s = (if b s then while b c (c s) else s)"
    56   apply (unfold while_def)
    57   apply (rule while_aux_unfold [THEN trans])
    58   apply auto
    59   apply (subst while_aux_unfold)
    60   apply simp
    61   apply clarify
    62   apply (erule_tac x = "\<lambda>i. f (Suc i)" in allE)
    63   apply blast
    64   done
    65 
    66 hide const while_aux
    67 
    68 lemma def_while_unfold: assumes fdef: "f == while test do"
    69       shows "f x = (if test x then f(do x) else x)"
    70 proof -
    71   have "f x = while test do x" using fdef by simp
    72   also have "\<dots> = (if test x then while test do (do x) else x)"
    73     by(rule while_unfold)
    74   also have "\<dots> = (if test x then f(do x) else x)" by(simp add:fdef[symmetric])
    75   finally show ?thesis .
    76 qed
    77 
    78 
    79 text {*
    80  The proof rule for @{term while}, where @{term P} is the invariant.
    81 *}
    82 
    83 theorem while_rule_lemma[rule_format]:
    84   "[| !!s. P s ==> b s ==> P (c s);
    85       !!s. P s ==> \<not> b s ==> Q s;
    86       wf {(t, s). P s \<and> b s \<and> t = c s} |] ==>
    87     P s --> Q (while b c s)"
    88 proof -
    89   case rule_context
    90   assume wf: "wf {(t, s). P s \<and> b s \<and> t = c s}"
    91   show ?thesis
    92     apply (induct s rule: wf [THEN wf_induct])
    93     apply simp
    94     apply clarify
    95     apply (subst while_unfold)
    96     apply (simp add: rule_context)
    97     done
    98 qed
    99 
   100 theorem while_rule:
   101   "[| P s;
   102       !!s. [| P s; b s  |] ==> P (c s);
   103       !!s. [| P s; \<not> b s  |] ==> Q s;
   104       wf r;
   105       !!s. [| P s; b s  |] ==> (c s, s) \<in> r |] ==>
   106    Q (while b c s)"
   107 apply (rule while_rule_lemma)
   108 prefer 4 apply assumption
   109 apply blast
   110 apply blast
   111 apply(erule wf_subset)
   112 apply blast
   113 done
   114 
   115 text {*
   116  \medskip An application: computation of the @{term lfp} on finite
   117  sets via iteration.
   118 *}
   119 
   120 theorem lfp_conv_while:
   121   "[| mono f; finite U; f U = U |] ==>
   122     lfp f = fst (while (\<lambda>(A, fA). A \<noteq> fA) (\<lambda>(A, fA). (fA, f fA)) ({}, f {}))"
   123 apply (rule_tac P = "\<lambda>(A, B). (A \<subseteq> U \<and> B = f A \<and> A \<subseteq> B \<and> B \<subseteq> lfp f)" and
   124                 r = "((Pow U \<times> UNIV) \<times> (Pow U \<times> UNIV)) \<inter>
   125                      inv_image finite_psubset (op - U o fst)" in while_rule)
   126    apply (subst lfp_unfold)
   127     apply assumption
   128    apply (simp add: monoD)
   129   apply (subst lfp_unfold)
   130    apply assumption
   131   apply clarsimp
   132   apply (blast dest: monoD)
   133  apply (fastsimp intro!: lfp_lowerbound)
   134  apply (blast intro: wf_finite_psubset Int_lower2 [THEN [2] wf_subset])
   135 apply (clarsimp simp add: inv_image_def finite_psubset_def order_less_le)
   136 apply (blast intro!: finite_Diff dest: monoD)
   137 done
   138 
   139 
   140 text {*
   141  An example of using the @{term while} combinator.
   142 *}
   143 
   144 theorem "P (lfp (\<lambda>N::int set. {0} \<union> {(n + 2) mod 6 | n. n \<in> N})) =
   145   P {0, 4, 2}"
   146 proof -
   147   have aux: "!!f A B. {f n | n. A n \<or> B n} = {f n | n. A n} \<union> {f n | n. B n}"
   148     apply blast
   149     done
   150   show ?thesis
   151     apply (subst lfp_conv_while [where ?U = "{0, 1, 2, 3, 4, 5}"])
   152        apply (rule monoI)
   153       apply blast
   154      apply simp
   155     apply (simp add: aux set_eq_subset)
   156     txt {* The fixpoint computation is performed purely by rewriting: *}
   157     apply (simp add: while_unfold aux set_eq_subset del: subset_empty)
   158     done
   159 qed
   160 
   161 end