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