# HG changeset patch
# User paulson
# Date 905441235 -7200
# Node ID d2ab1264afd4733baf3766317c75df2ec0fd2917
# Parent  6712d95c811342380b4c775d61ef2983be44b419
tidied

diff -r 6712d95c8113 -r d2ab1264afd4 src/HOL/Lex/Prefix.ML
--- a/src/HOL/Lex/Prefix.ML	Thu Sep 10 17:26:53 1998 +0200
+++ b/src/HOL/Lex/Prefix.ML	Thu Sep 10 17:27:15 1998 +0200
@@ -71,7 +71,7 @@
 qed "same_prefix_prefix";
 Addsimps [same_prefix_prefix];
 
-AddIffs
+AddIffs   (* (xs@ys <= xs) = (ys <= []) *)
  [simplify (simpset()) (read_instantiate [("zs","[]")] same_prefix_prefix)];
 
 Goalw [prefix_def] "xs <= ys ==> xs <= ys@zs";
@@ -80,13 +80,10 @@
 qed "prefix_prefix";
 Addsimps [prefix_prefix];
 
-(* nicht sehr elegant bewiesen - Induktion eigentlich ueberfluessig *)
 Goalw [prefix_def]
    "(xs <= y#ys) = (xs=[] | (? zs. xs=y#zs & zs <= ys))";
-by (induct_tac "xs" 1);
-by (Simp_tac 1);
-by (Simp_tac 1);
-by (Fast_tac 1);
+by (exhaust_tac "xs" 1);
+by Auto_tac;
 qed "prefix_Cons";
 
 Goal "(xs <= ys@zs) = (xs <= ys | (? us. xs = ys@us & us <= zs))";
@@ -94,7 +91,7 @@
  by (Simp_tac 1);
  by (Blast_tac 1);
 by (asm_full_simp_tac (simpset() delsimps [append_assoc]
-                                addsimps [append_assoc RS sym])1);
+                                 addsimps [append_assoc RS sym])1);
 by (Simp_tac 1);
 by (Blast_tac 1);
 qed "prefix_append";
diff -r 6712d95c8113 -r d2ab1264afd4 src/HOL/UNITY/WFair.ML
--- a/src/HOL/UNITY/WFair.ML	Thu Sep 10 17:26:53 1998 +0200
+++ b/src/HOL/UNITY/WFair.ML	Thu Sep 10 17:27:15 1998 +0200
@@ -521,6 +521,7 @@
 by (subgoal_tac "leadsTo acts (A Int W - C) (A' Int W Un C)" 1);
 by (simp_tac (simpset() addsimps [Int_Diff]) 2);
 by (blast_tac (claset() addIs [wlt_leadsTo, psp RS leadsTo_weaken_R]) 2);
+(** LEVEL 7 **)
 by (subgoal_tac "leadsTo acts (A' Int W Un C) (A' Int B' Un C)" 1);
 by (blast_tac (claset() addIs [wlt_leadsTo, leadsTo_Un_Un, 
                                psp2 RS leadsTo_weaken_R, 
@@ -530,8 +531,8 @@
 by (assume_tac 2);
 by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
 by (subgoal_tac "A Int B <= A Int W" 1);
-by (blast_tac (claset() addIs [leadsTo_subset, Int_mono] 
-	                delrules [subsetI]) 2);
+by (blast_tac (claset() addSDs [leadsTo_subset]
+			addSIs [subset_refl RS Int_mono]) 2);
 by (blast_tac (claset() addIs [leadsTo_Trans, subset_imp_leadsTo]) 1);
 bind_thm("completion", refl RS result());
 
diff -r 6712d95c8113 -r d2ab1264afd4 src/HOL/ex/Puzzle.ML
--- a/src/HOL/ex/Puzzle.ML	Thu Sep 10 17:26:53 1998 +0200
+++ b/src/HOL/ex/Puzzle.ML	Thu Sep 10 17:27:15 1998 +0200
@@ -3,11 +3,13 @@
     Author:     Tobias Nipkow
     Copyright   1993 TU Muenchen
 
-For puzzle.thy.  A question from "Bundeswettbewerb Mathematik"
+A question from "Bundeswettbewerb Mathematik"
 
 Proof due to Herbert Ehler
 *)
 
+AddSIs [Puzzle.f_ax];
+
 (*specialized form of induction needed below*)
 val prems = goal Nat.thy "[| P(0); !!n. P(Suc(n)) |] ==> !n. P(n)";
 by (EVERY1 [rtac (nat_induct RS allI), resolve_tac prems, resolve_tac prems]);
@@ -21,10 +23,9 @@
 by (rtac classical 1);
 by (dtac not_leE 1);
 by (subgoal_tac "f(na) <= f(f(na))" 1);
-by (fast_tac (claset() addIs [Puzzle.f_ax]) 2);
+by (Blast_tac 2);
 by (rtac Suc_leI 1);
-by (fast_tac (claset() delrules [order_refl] 
-                      addIs [Puzzle.f_ax, le_less_trans]) 1);
+by (blast_tac (claset() addSDs [spec] addIs [le_less_trans]) 1);
 val lemma = result() RS spec RS mp;
 
 Goal "n <= f(n)";
@@ -32,13 +33,16 @@
 qed "lemma1";
 
 Goal "f(n) < f(Suc(n))";
-by (deepen_tac (claset() addIs [Puzzle.f_ax, le_less_trans, lemma1]) 0 1);
+by (blast_tac (claset() addIs [le_less_trans, lemma1]) 1);
 qed "lemma2";
 
-val prems = goal Puzzle.thy "(!!n. f(n) <= f(Suc(n))) ==> m<n --> f(m) <= f(n)";
+val prems = Goal "(!!n. f(n) <= f(Suc(n))) ==> m<n --> f(m) <= f(n)";
 by (res_inst_tac[("n","n")]nat_induct 1);
 by (Simp_tac 1);
 by (simp_tac (simpset() addsimps [less_Suc_eq]) 1);
+  (*Blast_tac: PROOF FAILED.  Perhaps remove DETERM for unsafe tactics,
+    or stop rotating prems for recursive rules: the le-assumptions
+    have got out of order.*)
 by (best_tac (claset() addIs (le_trans::prems)) 1);
 qed_spec_mp "mono_lemma1";