src/HOL/Library/While_Combinator.thy
changeset 19736 d8d0f8f51d69
parent 18372 2bffdf62fe7f
child 19769 c40ce2de2020
     1.1 --- a/src/HOL/Library/While_Combinator.thy	Sat May 27 17:42:00 2006 +0200
     1.2 +++ b/src/HOL/Library/While_Combinator.thy	Sat May 27 17:42:02 2006 +0200
     1.3 @@ -35,7 +35,7 @@
     1.4    apply blast
     1.5    done
     1.6  
     1.7 -constdefs
     1.8 +definition
     1.9    while :: "('a => bool) => ('a => 'a) => 'a => 'a"
    1.10    "while b c s == while_aux (b, c, s)"
    1.11  
    1.12 @@ -88,7 +88,8 @@
    1.13      and terminate: "!!s. P s ==> \<not> b s ==> Q s"
    1.14      and wf: "wf {(t, s). P s \<and> b s \<and> t = c s}"
    1.15    shows "P s \<Longrightarrow> Q (while b c s)"
    1.16 -  apply (induct s rule: wf [THEN wf_induct])
    1.17 +  using wf
    1.18 +  apply (induct s)
    1.19    apply simp
    1.20    apply (subst while_unfold)
    1.21    apply (simp add: invariant terminate)
    1.22 @@ -101,13 +102,13 @@
    1.23        wf r;
    1.24        !!s. [| P s; b s  |] ==> (c s, s) \<in> r |] ==>
    1.25     Q (while b c s)"
    1.26 -apply (rule while_rule_lemma)
    1.27 -prefer 4 apply assumption
    1.28 -apply blast
    1.29 -apply blast
    1.30 -apply(erule wf_subset)
    1.31 -apply blast
    1.32 -done
    1.33 +  apply (rule while_rule_lemma)
    1.34 +     prefer 4 apply assumption
    1.35 +    apply blast
    1.36 +   apply blast
    1.37 +  apply (erule wf_subset)
    1.38 +  apply blast
    1.39 +  done
    1.40  
    1.41  text {*
    1.42   \medskip An application: computation of the @{term lfp} on finite
    1.43 @@ -142,12 +143,11 @@
    1.44  looping because the antisymmetry simproc turns the subset relationship
    1.45  back into equality. *}
    1.46  
    1.47 -lemma seteq: "(A = B) = ((!a : A. a:B) & (!b:B. b:A))"
    1.48 -  by blast
    1.49 -
    1.50  theorem "P (lfp (\<lambda>N::int set. {0} \<union> {(n + 2) mod 6 | n. n \<in> N})) =
    1.51    P {0, 4, 2}"
    1.52  proof -
    1.53 +  have seteq: "!!A B. (A = B) = ((!a : A. a:B) & (!b:B. b:A))"
    1.54 +    by blast
    1.55    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.56      apply blast
    1.57      done