src/HOL/Library/While_Combinator.thy
 changeset 18372 2bffdf62fe7f parent 15197 19e735596e51 child 19736 d8d0f8f51d69
```     1.1 --- a/src/HOL/Library/While_Combinator.thy	Thu Dec 08 20:15:41 2005 +0100
1.2 +++ b/src/HOL/Library/While_Combinator.thy	Thu Dec 08 20:15:50 2005 +0100
1.3 @@ -67,8 +67,9 @@
1.4
1.5  hide const while_aux
1.6
1.7 -lemma def_while_unfold: assumes fdef: "f == while test do"
1.8 -      shows "f x = (if test x then f(do x) else x)"
1.9 +lemma def_while_unfold:
1.10 +  assumes fdef: "f == while test do"
1.11 +  shows "f x = (if test x then f(do x) else x)"
1.12  proof -
1.13    have "f x = while test do x" using fdef by simp
1.14    also have "\<dots> = (if test x then while test do (do x) else x)"
1.15 @@ -82,22 +83,16 @@
1.16   The proof rule for @{term while}, where @{term P} is the invariant.
1.17  *}
1.18
1.19 -theorem while_rule_lemma[rule_format]:
1.20 -  "[| !!s. P s ==> b s ==> P (c s);
1.21 -      !!s. P s ==> \<not> b s ==> Q s;
1.22 -      wf {(t, s). P s \<and> b s \<and> t = c s} |] ==>
1.23 -    P s --> Q (while b c s)"
1.24 -proof -
1.25 -  case rule_context
1.26 -  assume wf: "wf {(t, s). P s \<and> b s \<and> t = c s}"
1.27 -  show ?thesis
1.28 -    apply (induct s rule: wf [THEN wf_induct])
1.29 -    apply simp
1.30 -    apply clarify
1.31 -    apply (subst while_unfold)
1.32 -    apply (simp add: rule_context)
1.33 -    done
1.34 -qed
1.35 +theorem while_rule_lemma:
1.36 +  assumes invariant: "!!s. P s ==> b s ==> P (c s)"
1.37 +    and terminate: "!!s. P s ==> \<not> b s ==> Q s"
1.38 +    and wf: "wf {(t, s). P s \<and> b s \<and> t = c s}"
1.39 +  shows "P s \<Longrightarrow> Q (while b c s)"
1.40 +  apply (induct s rule: wf [THEN wf_induct])
1.41 +  apply simp
1.42 +  apply (subst while_unfold)
1.43 +  apply (simp add: invariant terminate)
1.44 +  done
1.45
1.46  theorem while_rule:
1.47    "[| P s;
1.48 @@ -148,7 +143,7 @@
1.49  back into equality. *}
1.50
1.51  lemma seteq: "(A = B) = ((!a : A. a:B) & (!b:B. b:A))"
1.52 -by blast
1.53 +  by blast
1.54
1.55  theorem "P (lfp (\<lambda>N::int set. {0} \<union> {(n + 2) mod 6 | n. n \<in> N})) =
1.56    P {0, 4, 2}"
```