small mods.

--- a/src/HOL/BCV/Kildall.ML	Wed Dec 13 09:30:59 2000 +0100
+++ b/src/HOL/BCV/Kildall.ML	Wed Dec 13 09:32:55 2000 +0100
@@ -152,10 +152,10 @@
 val [iter_wf,iter_tc] = iter.tcs;
 
 goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop iter_wf));
-by (REPEAT(rtac wf_same_fstI 1));
+by (REPEAT(rtac wf_same_fst 1));
 by (split_all_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [lesssub_def]) 1);
-by (REPEAT(rtac wf_same_fstI 1));
+by (REPEAT(rtac wf_same_fst 1));
 by (rtac wf_lex_prod 1);
  by (rtac wf_finite_psubset 2); (* FIXME *)
 by (Clarify_tac 1);

--- a/src/HOL/Lambda/ListBeta.thy	Wed Dec 13 09:30:59 2000 +0100
+++ b/src/HOL/Lambda/ListBeta.thy	Wed Dec 13 09:32:55 2000 +0100
@@ -47,23 +47,23 @@
      apply (case_tac r)
        apply simp
       apply (simp add: App_eq_foldl_conv)
-      apply (split (asm) split_if_asm)
+      apply (split split_if_asm)
        apply simp
        apply blast
       apply simp
      apply (simp add: App_eq_foldl_conv)
-     apply (split (asm) split_if_asm)
+     apply (split split_if_asm)
       apply simp
      apply simp
     apply (clarify del: disjCI)
     apply (drule App_eq_foldl_conv [THEN iffD1])
-    apply (split (asm) split_if_asm)
+    apply (split split_if_asm)
      apply simp
      apply blast
     apply (force intro: disjI1 [THEN append_step1I])
    apply (clarify del: disjCI)
    apply (drule App_eq_foldl_conv [THEN iffD1])
-   apply (split (asm) split_if_asm)
+   apply (split split_if_asm)
     apply simp
     apply blast
    apply (auto 0 3 intro: disjI2 [THEN append_step1I])

--- a/src/HOL/Library/While_Combinator.thy	Wed Dec 13 09:30:59 2000 +0100
+++ b/src/HOL/Library/While_Combinator.thy	Wed Dec 13 09:32:55 2000 +0100
@@ -36,8 +36,8 @@
 ML_setup {*
   goalw_cterm [] (cterm_of (sign_of (the_context ()))
     (HOLogic.mk_Trueprop (hd (RecdefPackage.tcs_of (the_context ()) "while_aux"))));
-  br wf_same_fstI 1;
-  br wf_same_fstI 1;
+  br wf_same_fst 1;
+  br wf_same_fst 1;
   by (asm_full_simp_tac (simpset() addsimps [wf_iff_no_infinite_down_chain]) 1);
   by (Blast_tac 1);
   qed "while_aux_tc";
@@ -74,7 +74,7 @@
  The proof rule for @{term while}, where @{term P} is the invariant.
 *}
 
-theorem while_rule [rule_format]:
+theorem while_rule_lemma[rule_format]:
   "(!!s. P s ==> b s ==> P (c s)) ==>
     (!!s. P s ==> \<not> b s ==> Q s) ==>
     wf {(t, s). P s \<and> b s \<and> t = c s} ==>
@@ -91,31 +91,19 @@
     done
 qed
 
+theorem while_rule:
+  "\<lbrakk> P s; \<And>s. \<lbrakk> P s; b s \<rbrakk> \<Longrightarrow> P(c s);
+    \<And>s.\<lbrakk> P s; \<not> b s \<rbrakk> \<Longrightarrow> Q s;
+    wf r;  \<And>s. \<lbrakk> P s; b s \<rbrakk> \<Longrightarrow> (c s,s) \<in> r \<rbrakk> \<Longrightarrow>
+    Q (while b c s)"
+apply (rule while_rule_lemma)
+prefer 4 apply assumption
+apply blast
+apply blast
+apply(erule wf_subset)
+apply blast
+done
+
 hide const while_aux
 
-text {*
- \medskip An application: computation of the @{term lfp} on finite
- sets via iteration.
-*}
-
-theorem lfp_conv_while:
-  "mono f ==> finite U ==> f U = U ==>
-    lfp f = fst (while (\<lambda>(A, fA). A \<noteq> fA) (\<lambda>(A, fA). (fA, f fA)) ({}, f {}))"
-  apply (rule_tac P =
-      "\<lambda>(A, B). (A \<subseteq> U \<and> B = f A \<and> A \<subseteq> B \<and> B \<subseteq> lfp f)" in while_rule)
-     apply (subst lfp_unfold)
-      apply assumption
-     apply clarsimp
-     apply (blast dest: monoD)
-    apply (fastsimp intro!: lfp_lowerbound)
-   apply (rule_tac r = "((Pow U <*> UNIV) <*> (Pow U <*> UNIV)) \<inter>
-       inv_image finite_psubset (op - U o fst)" in wf_subset)
-    apply (blast intro: wf_finite_psubset Int_lower2 [THEN [2] wf_subset])
-   apply (clarsimp simp add: inv_image_def finite_psubset_def order_less_le)
-   apply (blast intro!: finite_Diff dest: monoD)
-  apply (subst lfp_unfold)
-   apply assumption
-  apply (simp add: monoD)
-  done
-
 end

--- a/src/HOL/Library/While_Combinator_Example.thy	Wed Dec 13 09:30:59 2000 +0100
+++ b/src/HOL/Library/While_Combinator_Example.thy	Wed Dec 13 09:32:55 2000 +0100
@@ -1,9 +1,32 @@
-
 header {* \title{} *}
 
 theory While_Combinator_Example = While_Combinator:
 
 text {*
+ \medskip An application: computation of the @{term lfp} on finite
+ sets via iteration.
+*}
+
+theorem lfp_conv_while:
+  "mono f ==> finite U ==> f U = U ==>
+    lfp f = fst (while (\<lambda>(A, fA). A \<noteq> fA) (\<lambda>(A, fA). (fA, f fA)) ({}, f {}))"
+apply (rule_tac P = "\<lambda>(A, B). (A \<subseteq> U \<and> B = f A \<and> A \<subseteq> B \<and> B \<subseteq> lfp f)" and
+                r = "((Pow U <*> UNIV) <*> (Pow U <*> UNIV)) \<inter>
+                     inv_image finite_psubset (op - U o fst)" in while_rule)
+   apply (subst lfp_unfold)
+    apply assumption
+   apply (simp add: monoD)
+  apply (subst lfp_unfold)
+   apply assumption
+  apply clarsimp
+  apply (blast dest: monoD)
+ apply (fastsimp intro!: lfp_lowerbound)
+ apply (blast intro: wf_finite_psubset Int_lower2 [THEN [2] wf_subset])
+apply (clarsimp simp add: inv_image_def finite_psubset_def order_less_le)
+apply (blast intro!: finite_Diff dest: monoD)
+done
+
+text {*
  An example of using the @{term while} combinator.
 *}
 

--- a/src/HOL/Recdef.thy	Wed Dec 13 09:30:59 2000 +0100
+++ b/src/HOL/Recdef.thy	Wed Dec 13 09:32:55 2000 +0100
@@ -39,6 +39,7 @@
   wf_inv_image
   wf_measure
   wf_pred_nat
+  wf_same_fst
   wf_empty
 
 end

--- a/src/HOL/Wellfounded_Relations.ML	Wed Dec 13 09:30:59 2000 +0100
+++ b/src/HOL/Wellfounded_Relations.ML	Wed Dec 13 09:32:55 2000 +0100
@@ -223,4 +223,4 @@
  by (EVERY1[etac allE, etac allE, etac mp, rtac allI, rtac allI]);
  by(Blast_tac 1);
 by(blast_tac (claset() addIs prems) 1);
-qed "wf_same_fstI";
+qed "wf_same_fst";