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.17  
    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.26  
    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.41  
    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