Tidied some proofs

--- a/src/HOL/ex/Comb.ML	Mon Aug 19 11:17:20 1996 +0200
+++ b/src/HOL/ex/Comb.ML	Mon Aug 19 11:18:36 1996 +0200
@@ -17,7 +17,6 @@
 
 open Comb;
 
-
 (*** Reflexive/Transitive closure preserves the Church-Rosser property 
      So does the Transitive closure; use r_into_trancl instead of rtrancl_refl
 ***)
@@ -29,17 +28,17 @@
     "!!r. [| diamond(r);  (x,y):r^* |] ==> \ 
 \         ALL y'. (x,y'):r --> (EX z. (y',z): r^* & (y,z): r)";
 by (etac rtrancl_induct 1);
-by (fast_tac (!claset addIs [rtrancl_refl]) 1);
+by (Fast_tac 1);
 by (slow_best_tac (!claset addIs [r_into_rtrancl RSN (2, rtrancl_trans)]
-                          addSDs [spec_mp]) 1);
+                           addSDs [spec_mp]) 1);
 val diamond_strip_lemmaE = result() RS spec RS mp RS exE;
 
 val [major] = goal Comb.thy "diamond(r) ==> diamond(r^*)";
 by (rewtac diamond_def);  (*unfold only in goal, not in premise!*)
 by (rtac (impI RS allI RS allI) 1);
 by (etac rtrancl_induct 1);
-by (fast_tac (!claset addIs [rtrancl_refl]) 1);
-by (ALLGOALS
+by (Fast_tac 1);
+by (ALLGOALS  (*Seems to be a brittle, undirected search*)
     (slow_best_tac ((claset_of "Fun") addIs [r_into_rtrancl, rtrancl_trans]
                            addEs [major RS diamond_strip_lemmaE])));
 qed "diamond_rtrancl";
@@ -56,27 +55,26 @@
 
 AddIs  contract.intrs;
 AddSEs [K_contractE, S_contractE, Ap_contractE];
-Addss  (HOL_ss addsimps comb.simps);
+Addss  (!simpset);
 
 goalw Comb.thy [I_def] "!!z. I -1-> z ==> P";
 by (Fast_tac 1);
 qed "I_contract_E";
+AddSEs [I_contract_E];
 
-(*Unused*)
-goal Comb.thy "!!x z. K#x -1-> z ==> (EX y. z = K#y & x -1-> y)";
+goal Comb.thy "!!x z. K#x -1-> z ==> (EX x'. z = K#x' & x -1-> x')";
 by (Fast_tac 1);
 qed "K1_contractD";
+AddSEs [K1_contractD];
 
 goal Comb.thy "!!x z. x ---> y ==> x#z ---> y#z";
 by (etac rtrancl_induct 1);
-by (rtac rtrancl_refl 1);
-by (fast_tac (!claset addIs [r_into_rtrancl, rtrancl_trans]) 1);
+by (ALLGOALS (best_tac (!claset addIs [r_into_rtrancl, rtrancl_trans])));
 qed "Ap_reduce1";
 
 goal Comb.thy "!!x z. x ---> y ==> z#x ---> z#y";
 by (etac rtrancl_induct 1);
-by (rtac rtrancl_refl 1);
-by (fast_tac (!claset addIs [r_into_rtrancl, rtrancl_trans]) 1);
+by (ALLGOALS (best_tac (!claset addIs [r_into_rtrancl, rtrancl_trans])));
 qed "Ap_reduce2";
 
 (** Counterexample to the diamond property for -1-> **)
@@ -94,8 +92,7 @@
 qed "KIII_contract3";
 
 goalw Comb.thy [diamond_def] "~ diamond(contract)";
-by (fast_tac (!claset addIs [KIII_contract1,KIII_contract2,KIII_contract3]
-                     addSEs [I_contract_E]) 1);
+by (fast_tac (!claset addIs [KIII_contract1,KIII_contract2,KIII_contract3]) 1);
 qed "not_diamond_contract";
 
 
@@ -109,30 +106,34 @@
 
 AddIs  parcontract.intrs;
 AddSEs [K_parcontractE, S_parcontractE,Ap_parcontractE];
-Addss  (HOL_ss addsimps comb.simps);
+Addss  (!simpset);
 
 (*** Basic properties of parallel contraction ***)
 
 goal Comb.thy "!!x z. K#x =1=> z ==> (EX x'. z = K#x' & x =1=> x')";
 by (Fast_tac 1);
 qed "K1_parcontractD";
+AddSDs [K1_parcontractD];
 
 goal Comb.thy "!!x z. S#x =1=> z ==> (EX x'. z = S#x' & x =1=> x')";
 by (Fast_tac 1);
 qed "S1_parcontractD";
+AddSDs [S1_parcontractD];
 
 goal Comb.thy
  "!!x y z. S#x#y =1=> z ==> (EX x' y'. z = S#x'#y' & x =1=> x' & y =1=> y')";
-by (fast_tac (!claset addSDs [S1_parcontractD]) 1);
-     (*the extra rule makes the proof more than twice as fast*)
+by (Fast_tac 1);
 qed "S2_parcontractD";
+AddSDs [S2_parcontractD];
+
+(*The rules above are not essential but make proofs much faster*)
+
 
 (*Church-Rosser property for parallel contraction*)
-goalw Comb.thy [diamond_def] "diamond(parcontract)";
+goalw Comb.thy [diamond_def] "diamond parcontract";
 by (rtac (impI RS allI RS allI) 1);
 by (etac parcontract.induct 1 THEN prune_params_tac);
-by (ALLGOALS 
-    (fast_tac (!claset addSDs [K1_parcontractD,S2_parcontractD])));
+by (ALLGOALS Fast_tac);
 qed "diamond_parcontract";
 
 
@@ -142,19 +143,18 @@
 by (rtac subsetI 1);
 by (split_all_tac 1);
 by (etac contract.induct 1);
-by (ALLGOALS (Fast_tac));
+by (ALLGOALS Fast_tac);
 qed "contract_subset_parcontract";
 
 (*Reductions: simply throw together reflexivity, transitivity and
   the one-step reductions*)
 
-AddIs [rtrancl_refl, r_into_rtrancl,
-		       contract.K, contract.S, Ap_reduce1, Ap_reduce2,
-		       rtrancl_trans];
+AddSIs [contract.K, contract.S];
+AddIs [Ap_reduce1, Ap_reduce2, r_into_rtrancl, rtrancl_trans];
 
 (*Example only: not used*)
 goalw Comb.thy [I_def] "I#x ---> x";
-by (Best_tac 1);
+by (Deepen_tac 0 1);
 qed "reduce_I";
 
 goal Comb.thy "parcontract <= contract^*";
@@ -172,9 +172,8 @@
 qed "reduce_eq_parreduce";
 
 goal Comb.thy "diamond(contract^*)";
-by (simp_tac (HOL_ss addsimps [reduce_eq_parreduce, diamond_rtrancl, 
-			       diamond_parcontract]) 1);
-
+by (simp_tac (!simpset addsimps [reduce_eq_parreduce, diamond_rtrancl, 
+			         diamond_parcontract]) 1);
 qed "diamond_reduce";
 
 

--- a/src/HOL/ex/Mutil.ML	Mon Aug 19 11:17:20 1996 +0200
+++ b/src/HOL/ex/Mutil.ML	Mon Aug 19 11:18:36 1996 +0200
@@ -17,34 +17,37 @@
 by (etac tiling.induct 1);
 by (Simp_tac 1);
 by (fast_tac (!claset addIs tiling.intrs
-	             addss (HOL_ss addsimps [Un_assoc,
-					     subset_empty_iff RS sym])) 1);
-bind_thm ("tiling_UnI", result() RS mp RS mp);
+	              addss (HOL_ss addsimps [Un_assoc,
+					      subset_empty_iff RS sym])) 1);
+qed_spec_mp "tiling_UnI";
 
 
 (*** Chess boards ***)
 
 val [below_0, below_Suc] = nat_recs below_def;
-Addsimps [below_0];
-(*below_Suc should NOT be added, or Sigma_Suc1,2 cannot be used*)
+Addsimps [below_0, below_Suc];
 
-goal thy "(i: below k) = (i<k)";
-by (res_inst_tac [("x", "i")] spec 1);
+goal thy "ALL i. (i: below k) = (i<k)";
 by (nat_ind_tac "k" 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [below_Suc, less_Suc_eq])));
+by (ALLGOALS (asm_simp_tac (!simpset addsimps [less_Suc_eq])));
 by (Fast_tac 1);
-qed "below_less_iff";
+qed_spec_mp "below_less_iff";
+
+Addsimps [below_less_iff];
 
 goal thy "below(Suc n) Times B = ({n} Times B) Un ((below n) Times B)";
-by (simp_tac (!simpset addsimps [below_Suc]) 1);
-by (fast_tac (!claset addIs [equalityI]) 1);
+by (Simp_tac 1);
+by (Fast_tac 1);
 qed "Sigma_Suc1";
 
 goal thy "A Times below(Suc n) = (A Times {n}) Un (A Times (below n))";
-by (simp_tac (!simpset addsimps [below_Suc]) 1);
-by (fast_tac (!claset addIs [equalityI]) 1);
+by (Simp_tac 1);
+by (Fast_tac 1);
 qed "Sigma_Suc2";
 
+(*Deletion is essential to allow use of Sigma_Suc1,2*)
+Delsimps [below_Suc];
+
 goal thy "{i} Times below(n + n) : tiling domino";
 by (nat_ind_tac "n" 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [Un_assoc RS sym, Sigma_Suc2])));
@@ -53,7 +56,7 @@
 by (subgoal_tac    (*seems the easiest way of turning one to the other*)
     "({i} Times {Suc(n1+n1)}) Un ({i} Times {n1+n1}) = \
 \    {(i, n1+n1), (i, Suc(n1+n1))}" 1);
-by (fast_tac (!claset addIs [equalityI]) 2);
+by (Fast_tac 2);
 by (asm_simp_tac (!simpset addsimps [domino.horiz]) 1);
 by (fast_tac (!claset addIs [equalityI, lessI] addEs [less_irrefl, less_asym]
                       addDs [below_less_iff RS iffD1]) 1);
@@ -108,15 +111,15 @@
 by (res_inst_tac [("k1", "i+j")] (mod2_cases RS disjE) 1);
 by (REPEAT_FIRST assume_tac);
 (*Four similar cases: case (i+j) mod 2 = b, 2#-b, ...*)
-by (REPEAT (asm_simp_tac (!simpset addsimps
-                          [evnodd_insert, evnodd_empty, mod_Suc] 
+by (REPEAT (asm_full_simp_tac (!simpset addsimps
+                          [less_Suc_eq, evnodd_insert, evnodd_empty, mod_Suc] 
                           setloop split_tac [expand_if]) 1
            THEN Fast_tac 1));
 qed "domino_singleton";
 
 goal thy "!!d. d:domino ==> finite d";
 by (fast_tac (!claset addSIs [finite_insertI, finite_emptyI] 
-                     addEs [domino.elim]) 1);
+                      addEs [domino.elim]) 1);
 qed "domino_finite";
 
 
@@ -165,6 +168,6 @@
      THEN
      asm_simp_tac (!simpset addsimps [tiling_domino_finite, finite_evnodd]) 1 
      THEN
-     asm_simp_tac (!simpset addsimps [mod_less, evnodd_iff, below_less_iff]) 1));
+     asm_simp_tac (!simpset addsimps [mod_less, evnodd_iff]) 1));
 qed "mutil_not_tiling";