src/HOL/Library/While_Combinator.thy
 changeset 10653 55f33da63366 parent 10269 cc20c9d7e682 child 10673 337c00fd385b
1.1 --- a/src/HOL/Library/While_Combinator.thy	Wed Dec 13 09:30:59 2000 +0100
1.2 +++ b/src/HOL/Library/While_Combinator.thy	Wed Dec 13 09:32:55 2000 +0100
1.3 @@ -36,8 +36,8 @@
1.4  ML_setup {*
1.5    goalw_cterm [] (cterm_of (sign_of (the_context ()))
1.6      (HOLogic.mk_Trueprop (hd (RecdefPackage.tcs_of (the_context ()) "while_aux"))));
1.7 -  br wf_same_fstI 1;
1.8 -  br wf_same_fstI 1;
1.9 +  br wf_same_fst 1;
1.10 +  br wf_same_fst 1;
1.11    by (asm_full_simp_tac (simpset() addsimps [wf_iff_no_infinite_down_chain]) 1);
1.12    by (Blast_tac 1);
1.13    qed "while_aux_tc";
1.14 @@ -74,7 +74,7 @@
1.15   The proof rule for @{term while}, where @{term P} is the invariant.
1.16  *}
1.18 -theorem while_rule [rule_format]:
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 @@ -91,31 +91,19 @@
1.24      done
1.25  qed
1.27 +theorem while_rule:
1.28 +  "\<lbrakk> P s; \<And>s. \<lbrakk> P s; b s \<rbrakk> \<Longrightarrow> P(c s);
1.29 +    \<And>s.\<lbrakk> P s; \<not> b s \<rbrakk> \<Longrightarrow> Q s;
1.30 +    wf r;  \<And>s. \<lbrakk> P s; b s \<rbrakk> \<Longrightarrow> (c s,s) \<in> r \<rbrakk> \<Longrightarrow>
1.31 +    Q (while b c s)"
1.32 +apply (rule while_rule_lemma)
1.33 +prefer 4 apply assumption
1.34 +apply blast
1.35 +apply blast
1.36 +apply(erule wf_subset)
1.37 +apply blast
1.38 +done
1.39 +
1.40  hide const while_aux
1.42 -text {*
1.43 - \medskip An application: computation of the @{term lfp} on finite
1.44 - sets via iteration.
1.45 -*}
1.46 -
1.47 -theorem lfp_conv_while:
1.48 -  "mono f ==> finite U ==> f U = U ==>
1.49 -    lfp f = fst (while (\<lambda>(A, fA). A \<noteq> fA) (\<lambda>(A, fA). (fA, f fA)) ({}, f {}))"
1.50 -  apply (rule_tac P =
1.51 -      "\<lambda>(A, B). (A \<subseteq> U \<and> B = f A \<and> A \<subseteq> B \<and> B \<subseteq> lfp f)" in while_rule)
1.52 -     apply (subst lfp_unfold)
1.53 -      apply assumption
1.54 -     apply clarsimp
1.55 -     apply (blast dest: monoD)
1.56 -    apply (fastsimp intro!: lfp_lowerbound)
1.57 -   apply (rule_tac r = "((Pow U <*> UNIV) <*> (Pow U <*> UNIV)) \<inter>
1.58 -       inv_image finite_psubset (op - U o fst)" in wf_subset)
1.59 -    apply (blast intro: wf_finite_psubset Int_lower2 [THEN [2] wf_subset])
1.60 -   apply (clarsimp simp add: inv_image_def finite_psubset_def order_less_le)
1.61 -   apply (blast intro!: finite_Diff dest: monoD)
1.62 -  apply (subst lfp_unfold)
1.63 -   apply assumption
1.64 -  apply (simp add: monoD)
1.65 -  done
1.66 -
1.67  end