src/HOL/Library/While_Combinator.thy
 changeset 10997 e14029f92770 parent 10984 8f49dcbec859 child 11047 10c51288b00d
```     1.1 --- a/src/HOL/Library/While_Combinator.thy	Mon Jan 29 23:02:21 2001 +0100
1.2 +++ b/src/HOL/Library/While_Combinator.thy	Mon Jan 29 23:54:56 2001 +0100
1.3 @@ -94,7 +94,7 @@
1.4    "[| P s;
1.5        !!s. [| P s; b s  |] ==> P (c s);
1.6        !!s. [| P s; \<not> b s  |] ==> Q s;
1.7 -      wf r;
1.8 +      wf r;
1.9        !!s. [| P s; b s  |] ==> (c s, s) \<in> r |] ==>
1.10     Q (while b c s)"
1.11  apply (rule while_rule_lemma)
1.12 @@ -130,25 +130,27 @@
1.13  done
1.14
1.15
1.16 -(*
1.17  text {*
1.18 - An example of using the @{term while} combinator.
1.19 + An example of using the @{term while} combinator.\footnote{It is safe
1.20 + to keep the example here, since there is no effect on the current
1.21 + theory.}
1.22  *}
1.23
1.24 -lemma aux: "{f n | n. A n \<or> B n} = {f n | n. A n} \<union> {f n | n. B n}"
1.25 -  apply blast
1.26 -  done
1.27 -
1.28  theorem "P (lfp (\<lambda>N::int set. {#0} \<union> {(n + #2) mod #6 | n. n \<in> N})) =
1.29      P {#0, #4, #2}"
1.30 -  apply (subst lfp_conv_while [where ?U = "{#0, #1, #2, #3, #4, #5}"])
1.31 -     apply (rule monoI)
1.32 +proof -
1.33 +  have aux: "!!f A B. {f n | n. A n \<or> B n} = {f n | n. A n} \<union> {f n | n. B n}"
1.34      apply blast
1.35 -   apply simp
1.36 -  apply (simp add: aux set_eq_subset)
1.37 -  txt {* The fixpoint computation is performed purely by rewriting: *}
1.38 -  apply (simp add: while_unfold aux set_eq_subset del: subset_empty)
1.39 -  done
1.40 -*)
1.41 +    done
1.42 +  show ?thesis
1.43 +    apply (subst lfp_conv_while [where ?U = "{#0, #1, #2, #3, #4, #5}"])
1.44 +       apply (rule monoI)
1.45 +      apply blast
1.46 +     apply simp
1.47 +    apply (simp add: aux set_eq_subset)
1.48 +    txt {* The fixpoint computation is performed purely by rewriting: *}
1.49 +    apply (simp add: while_unfold aux set_eq_subset del: subset_empty)
1.50 +    done
1.51 +qed
1.52
1.53  end
```