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}"