1.1 --- a/src/HOL/Library/While_Combinator.thy	Fri Jan 26 15:50:28 2001 +0100
     1.2 +++ b/src/HOL/Library/While_Combinator.thy	Fri Jan 26 15:50:52 2001 +0100
     1.3 @@ -67,14 +67,16 @@
     1.4    apply blast
     1.5    done
     1.6  
     1.7 +hide const while_aux
     1.8 +
     1.9  text {*
    1.10   The proof rule for @{term while}, where @{term P} is the invariant.
    1.11  *}
    1.12  
    1.13  theorem while_rule_lemma[rule_format]:
    1.14 -  "(!!s. P s ==> b s ==> P (c s)) ==>
    1.15 -    (!!s. P s ==> \<not> b s ==> Q s) ==>
    1.16 -    wf {(t, s). P s \<and> b s \<and> t = c s} ==>
    1.17 +  "[| !!s. P s ==> b s ==> P (c s);
    1.18 +      !!s. P s ==> \<not> b s ==> Q s;
    1.19 +      wf {(t, s). P s \<and> b s \<and> t = c s} |] ==>
    1.20      P s --> Q (while b c s)"
    1.21  proof -
    1.22    case antecedent
    1.23 @@ -89,10 +91,12 @@
    1.24  qed
    1.25  
    1.26  theorem while_rule:
    1.27 -  "[| P s; !!s. [| P s; b s  |] ==> P (c s);
    1.28 -    !!s. [| P s; \<not> b s  |] ==> Q s;
    1.29 -    wf r;  !!s. [| P s; b s  |] ==> (c s, s) \<in> r |] ==>
    1.30 -    Q (while b c s)"
    1.31 +  "[| P s;
    1.32 +      !!s. [| P s; b s  |] ==> P (c s);
    1.33 +      !!s. [| P s; \<not> b s  |] ==> Q s;
    1.34 +      wf r; 
    1.35 +      !!s. [| P s; b s  |] ==> (c s, s) \<in> r |] ==>
    1.36 +   Q (while b c s)"
    1.37  apply (rule while_rule_lemma)
    1.38  prefer 4 apply assumption
    1.39  apply blast
    1.40 @@ -101,6 +105,50 @@
    1.41  apply blast
    1.42  done
    1.43  
    1.44 -hide const while_aux
    1.45 +text {*
    1.46 + \medskip An application: computation of the @{term lfp} on finite
    1.47 + sets via iteration.
    1.48 +*}
    1.49 +
    1.50 +theorem lfp_conv_while:
    1.51 +  "[| mono f; finite U; f U = U |] ==>
    1.52 +    lfp f = fst (while (\<lambda>(A, fA). A \<noteq> fA) (\<lambda>(A, fA). (fA, f fA)) ({}, f {}))"
    1.53 +apply (rule_tac P = "\<lambda>(A, B). (A \<subseteq> U \<and> B = f A \<and> A \<subseteq> B \<and> B \<subseteq> lfp f)" and
    1.54 +                r = "((Pow U <*> UNIV) <*> (Pow U <*> UNIV)) \<inter>
    1.55 +                     inv_image finite_psubset (op - U o fst)" in while_rule)
    1.56 +   apply (subst lfp_unfold)
    1.57 +    apply assumption
    1.58 +   apply (simp add: monoD)
    1.59 +  apply (subst lfp_unfold)
    1.60 +   apply assumption
    1.61 +  apply clarsimp
    1.62 +  apply (blast dest: monoD)
    1.63 + apply (fastsimp intro!: lfp_lowerbound)
    1.64 + apply (blast intro: wf_finite_psubset Int_lower2 [THEN [2] wf_subset])
    1.65 +apply (clarsimp simp add: inv_image_def finite_psubset_def order_less_le)
    1.66 +apply (blast intro!: finite_Diff dest: monoD)
    1.67 +done
    1.68 +
    1.69 +
    1.70 +(*
    1.71 +text {*
    1.72 + An example of using the @{term while} combinator.
    1.73 +*}
    1.74 +
    1.75 +lemma aux: "{f n | n. A n \<or> B n} = {f n | n. A n} \<union> {f n | n. B n}"
    1.76 +  apply blast
    1.77 +  done
    1.78 +
    1.79 +theorem "P (lfp (\<lambda>N::int set. {#0} \<union> {(n + #2) mod #6 | n. n \<in> N})) =
    1.80 +    P {#0, #4, #2}"
    1.81 +  apply (subst lfp_conv_while [where ?U = "{#0, #1, #2, #3, #4, #5}"])
    1.82 +     apply (rule monoI)
    1.83 +    apply blast
    1.84 +   apply simp
    1.85 +  apply (simp add: aux set_eq_subset)
    1.86 +  txt {* The fixpoint computation is performed purely by rewriting: *}
    1.87 +  apply (simp add: while_unfold aux set_eq_subset del: subset_empty)
    1.88 +  done
    1.89 +*)
    1.90  
    1.91  end