# HG changeset patch
# User nipkow
# Date 967623679 -7200
# Node ID 332fab43628f5569c157c809f387c9cde9b67943
# Parent  203e5552496b7a60711b3acd597506ef053360a0
Fixed rulify.
As a result ?-vars in some recdef induction schemas were renamed.

diff -r 203e5552496b -r 332fab43628f TFL/post.sml
--- a/TFL/post.sml	Tue Aug 29 22:31:36 2000 +0200
+++ b/TFL/post.sml	Wed Aug 30 10:21:19 2000 +0200
@@ -198,9 +198,8 @@
 		{f = f, R = R, rules = rules,
 		 full_pats_TCs = full_pats_TCs,
 		 TCs = TCs}
-	val rules' = map (standard o normalize_thm [RSmp]) (R.CONJUNCTS rules)
-    in  {induct = meta_outer
-		   (normalize_thm [RSspec,RSmp] (induction RS spec')), 
+	val rules' = map (standard o rulify) (R.CONJUNCTS rules)
+    in  {induct = meta_outer (rulify (induction RS spec')), 
 	 rules = ListPair.zip(rules', rows),
 	 tcs = (termination_goals rules') @ tcs}
     end
diff -r 203e5552496b -r 332fab43628f src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Tue Aug 29 22:31:36 2000 +0200
+++ b/src/HOL/Finite.ML	Wed Aug 30 10:21:19 2000 +0200
@@ -570,7 +570,7 @@
 
 
 Goal "[| (A, x) : foldSet f e;  (A, y) : foldSet f e |] ==> y=x";
-by (blast_tac (claset() addIs [normalize_thm [RSspec, RSmp] lemma]) 1);
+by (blast_tac (claset() addIs [rulify lemma]) 1);
 qed "foldSet_determ";
 
 Goalw [fold_def] "(A,y) : foldSet f e ==> fold f e A = y";
diff -r 203e5552496b -r 332fab43628f src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Aug 29 22:31:36 2000 +0200
+++ b/src/HOL/HOL.thy	Wed Aug 30 10:21:19 2000 +0200
@@ -191,7 +191,7 @@
 
 (* theory and package setup *)
 
-use "HOL_lemmas.ML"	setup attrib_setup
+use "HOL_lemmas.ML"
 use "cladata.ML"	setup hypsubst_setup setup Classical.setup setup clasetup
 
 lemma all_eq: "(!!x. P x) == Trueprop (ALL x. P x)"
@@ -219,6 +219,6 @@
 use "simpdata.ML"	setup Simplifier.setup
 			setup "Simplifier.method_setup Splitter.split_modifiers" setup simpsetup
                         setup Splitter.setup setup Clasimp.setup setup iff_attrib_setup
-
+			setup attrib_setup
 
 end
diff -r 203e5552496b -r 332fab43628f src/HOL/HOL_lemmas.ML
--- a/src/HOL/HOL_lemmas.ML	Tue Aug 29 22:31:36 2000 +0200
+++ b/src/HOL/HOL_lemmas.ML	Wed Aug 30 10:21:19 2000 +0200
@@ -501,62 +501,3 @@
 
 
 fun strip_tac i = REPEAT(resolve_tac [impI,allI] i); 
-
-(** strip ALL and --> from proved goal while preserving ALL-bound var names **)
-
-(** THIS CODE IS A MESS!!! **)
-
-local
-
-(* Use XXX to avoid forall_intr failing because of duplicate variable name *)
-val myspec = read_instantiate [("P","?XXX")] spec;
-val _ $ (_ $ (vx as Var(_,vxT))) = concl_of myspec;
-val cvx = cterm_of (#sign(rep_thm myspec)) vx;
-val aspec = forall_intr cvx myspec;
-
-in
-
-fun RSspec th =
-  (case concl_of th of
-     _ $ (Const("All",_) $ Abs(a,_,_)) =>
-         let val ca = cterm_of (#sign(rep_thm th)) (Var((a,0),vxT))
-         in th RS forall_elim ca aspec end
-  | _ => raise THM("RSspec",0,[th]));
-
-fun RSmp th =
-  (case concl_of th of
-     _ $ (Const("op -->",_)$_$_) => th RS mp
-  | _ => raise THM("RSmp",0,[th]));
-
-fun normalize_thm funs =
-  let fun trans [] th = th
-	| trans (f::fs) th = (trans funs (f th)) handle THM _ => trans fs th
-  in zero_var_indexes o strip_shyps_warning o trans funs end;
-
-fun qed_spec_mp name =
-  let val thm = normalize_thm [RSspec,RSmp] (result())
-  in ThmDatabase.ml_store_thm(name, thm) end;
-
-fun qed_goal_spec_mp name thy s p = 
-	bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goal thy s p));
-
-fun qed_goalw_spec_mp name thy defs s p = 
-	bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goalw thy defs s p));
-
-end;
-
-
-(* attributes *)
-
-local
-
-fun gen_rulify x =
-  Attrib.no_args (Drule.rule_attribute (fn _ => (normalize_thm [RSspec, RSmp]))) x;
-
-in
-
-val attrib_setup =
- [Attrib.add_attributes
-  [("rulify", (gen_rulify, gen_rulify), "put theorem into standard rule form")]];
-
-end;
diff -r 203e5552496b -r 332fab43628f src/HOL/Lambda/ParRed.ML
--- a/src/HOL/Lambda/ParRed.ML	Tue Aug 29 22:31:36 2000 +0200
+++ b/src/HOL/Lambda/ParRed.ML	Wed Aug 30 10:21:19 2000 +0200
@@ -83,7 +83,7 @@
 (*** cd ***)
 
 Goal "!t. s => t --> t => cd s";
-by (res_inst_tac[("u","s")] cd.induct 1);
+by (res_inst_tac[("x","s")] cd.induct 1);
 by (Auto_tac);
 by (fast_tac (claset() addSIs [par_beta_subst]) 1);
 qed_spec_mp "par_beta_cd";
diff -r 203e5552496b -r 332fab43628f src/HOL/NumberTheory/IntFact.ML
--- a/src/HOL/NumberTheory/IntFact.ML	Tue Aug 29 22:31:36 2000 +0200
+++ b/src/HOL/NumberTheory/IntFact.ML	Wed Aug 30 10:21:19 2000 +0200
@@ -60,7 +60,7 @@
 qed "d22set_le_swap";
 
 Goal "#1<b --> b<=a --> b:(d22set a)";
-by (res_inst_tac [("u","a")] d22set.induct 1);
+by (res_inst_tac [("x","a")] d22set.induct 1);
 by Auto_tac;
 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [d22set_eq])));
 qed_spec_mp "d22set_mem";
@@ -75,7 +75,7 @@
 Delsimps zfact.simps; 
 
 Goal "setprod(d22set a) = zfact a";
-by (res_inst_tac [("u","a")] d22set.induct 1);
+by (res_inst_tac [("x","a")] d22set.induct 1);
 by Safe_tac;
 by (asm_full_simp_tac (simpset() addsimps [d22set_eq,zfact_eq]) 1);
 by (stac d22set_eq 1);
diff -r 203e5552496b -r 332fab43628f src/HOL/Subst/Unify.ML
--- a/src/HOL/Subst/Unify.ML	Tue Aug 29 22:31:36 2000 +0200
+++ b/src/HOL/Subst/Unify.ML	Wed Aug 30 10:21:19 2000 +0200
@@ -128,7 +128,7 @@
  *---------------------------------------------------------------------------*)
 val wfr = tc0 RS conjunct1
 and tc  = tc0 RS conjunct2;
-val unifyRules0 = map (normalize_thm [fn th => wfr RS th, fn th => tc RS th]) 
+val unifyRules0 = map (rule_by_tactic (rtac wfr 1 THEN TRY(rtac tc 1)))
                      unify.simps;
 
 val unifyInduct0 = [wfr,tc] MRS unify.induct;
diff -r 203e5552496b -r 332fab43628f src/HOL/UNITY/NSP_Bad.ML
--- a/src/HOL/UNITY/NSP_Bad.ML	Tue Aug 29 22:31:36 2000 +0200
+++ b/src/HOL/UNITY/NSP_Bad.ML	Wed Aug 30 10:21:19 2000 +0200
@@ -11,9 +11,8 @@
   Proc. Royal Soc. 426 (1989)
 *)
 
-fun impOfAlways th = 
-    normalize_thm [RSspec,RSmp]
-       (th RS Always_includes_reachable RS subsetD RS CollectD);
+fun impOfAlways th =
+  rulify (th RS Always_includes_reachable RS subsetD RS CollectD);
 
 AddEs spies_partsEs;
 AddDs [impOfSubs analz_subset_parts];
diff -r 203e5552496b -r 332fab43628f src/HOL/ex/Fib.ML
--- a/src/HOL/ex/Fib.ML	Tue Aug 29 22:31:36 2000 +0200
+++ b/src/HOL/ex/Fib.ML	Wed Aug 30 10:21:19 2000 +0200
@@ -24,7 +24,7 @@
 
 (*Concrete Mathematics, page 280*)
 Goal "fib (Suc (n + k)) = fib(Suc k) * fib(Suc n) + fib k * fib n";
-by (res_inst_tac [("u","n")] fib.induct 1);
+by (res_inst_tac [("x","n")] fib.induct 1);
 (*Simplify the LHS just enough to apply the induction hypotheses*)
 by (asm_full_simp_tac
     (simpset() addsimps [inst "x" "Suc(?m+?n)" fib_Suc_Suc]) 3);
@@ -35,7 +35,7 @@
 
 
 Goal "fib (Suc n) ~= 0";
-by (res_inst_tac [("u","n")] fib.induct 1);
+by (res_inst_tac [("x","n")] fib.induct 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [fib_Suc_Suc])));
 qed "fib_Suc_neq_0";
 
@@ -52,7 +52,7 @@
 Goal "int (fib (Suc (Suc n)) * fib n) = \
 \     (if n mod 2 = 0 then int (fib(Suc n) * fib(Suc n)) - #1 \
 \                     else int (fib(Suc n) * fib(Suc n)) + #1)";
-by (res_inst_tac [("u","n")] fib.induct 1);
+by (res_inst_tac [("x","n")] fib.induct 1);
 by (simp_tac (simpset() addsimps [fib_Suc_Suc, mod_Suc]) 2);
 by (simp_tac (simpset() addsimps [fib_Suc_Suc]) 1);
 by (asm_full_simp_tac
@@ -65,7 +65,7 @@
 (** Towards Law 6.111 of Concrete Mathematics **)
 
 Goal "gcd(fib n, fib (Suc n)) = 1";
-by (res_inst_tac [("u","n")] fib.induct 1);
+by (res_inst_tac [("x","n")] fib.induct 1);
 by (asm_simp_tac (simpset() addsimps [fib_Suc3, gcd_commute, gcd_add2]) 3);
 by (ALLGOALS (simp_tac (simpset() addsimps [fib_Suc_Suc])));
 qed "gcd_fib_Suc_eq_1"; 
diff -r 203e5552496b -r 332fab43628f src/HOL/ex/Qsort.ML
--- a/src/HOL/ex/Qsort.ML	Tue Aug 29 22:31:36 2000 +0200
+++ b/src/HOL/ex/Qsort.ML	Wed Aug 30 10:21:19 2000 +0200
@@ -31,7 +31,7 @@
 (*** Version two: type classes ***)
 
 Goal "multiset (quickSort xs) z = multiset xs z";
-by (res_inst_tac [("u","xs")] quickSort.induct 1);
+by (res_inst_tac [("x","xs")] quickSort.induct 1);
 by Auto_tac;
 qed "quickSort_permutes";
 Addsimps [quickSort_permutes];
@@ -43,7 +43,7 @@
 Addsimps [set_quickSort];
 
 Goal "sorted (op <=) (quickSort xs)";
-by (res_inst_tac [("u","xs")] quickSort.induct 1);
+by (res_inst_tac [("x","xs")] quickSort.induct 1);
 by (ALLGOALS Asm_simp_tac);
 by (blast_tac (claset() addIs [linorder_linear RS disjE, order_trans]) 1);
 qed_spec_mp "sorted_quickSort";
diff -r 203e5552496b -r 332fab43628f src/HOL/ex/Recdefs.ML
--- a/src/HOL/ex/Recdefs.ML	Tue Aug 29 22:31:36 2000 +0200
+++ b/src/HOL/ex/Recdefs.ML	Wed Aug 30 10:21:19 2000 +0200
@@ -12,12 +12,12 @@
 Addsimps g.simps;
 
 Goal "g x < Suc x";
-by (res_inst_tac [("u","x")] g.induct 1);
+by (res_inst_tac [("x","x")] g.induct 1);
 by Auto_tac;
 qed "g_terminates";
 
 Goal "g x = 0";
-by (res_inst_tac [("u","x")] g.induct 1);
+by (res_inst_tac [("x","x")] g.induct 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [g_terminates])));
 qed "g_zero";
 
diff -r 203e5552496b -r 332fab43628f src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Tue Aug 29 22:31:36 2000 +0200
+++ b/src/HOL/simpdata.ML	Wed Aug 30 10:21:19 2000 +0200
@@ -480,6 +480,37 @@
 val simpsetup =
   [fn thy => (simpset_ref_of thy := HOL_ss addcongs [if_weak_cong]; thy)];
 
+(*** conversion of -->/! into ==>/!! ***)
+
+local
+  val rules = [symmetric(thm"all_eq"),symmetric(thm"imp_eq"),Drule.norm_hhf_eq]
+  val ss = HOL_basic_ss addsimps rules
+in
+
+val rulify = zero_var_indexes o strip_shyps_warning o forall_elim_vars_safe o simplify ss;
+
+fun qed_spec_mp name = ThmDatabase.ml_store_thm(name, rulify(result()));
+
+fun qed_goal_spec_mp name thy s p = 
+	bind_thm (name, rulify (prove_goal thy s p));
+
+fun qed_goalw_spec_mp name thy defs s p = 
+	bind_thm (name, rulify (prove_goalw thy defs s p));
+
+end;
+
+local
+
+fun gen_rulify x =
+  Attrib.no_args (Drule.rule_attribute (fn _ => rulify)) x;
+
+in
+
+val attrib_setup =
+ [Attrib.add_attributes
+  [("rulify", (gen_rulify, gen_rulify), "put theorem into standard rule form")]];
+
+end;
 
 (*** integration of simplifier with classical reasoner ***)