Fixed rulify.
authornipkow
Wed Aug 30 10:21:19 2000 +0200 (2000-08-30)
changeset 9736332fab43628f
parent 9735 203e5552496b
child 9737 7aae235675dc
Fixed rulify.
As a result ?-vars in some recdef induction schemas were renamed.
TFL/post.sml
src/HOL/Finite.ML
src/HOL/HOL.thy
src/HOL/HOL_lemmas.ML
src/HOL/Lambda/ParRed.ML
src/HOL/NumberTheory/IntFact.ML
src/HOL/Subst/Unify.ML
src/HOL/UNITY/NSP_Bad.ML
src/HOL/ex/Fib.ML
src/HOL/ex/Qsort.ML
src/HOL/ex/Recdefs.ML
src/HOL/simpdata.ML
     1.1 --- a/TFL/post.sml	Tue Aug 29 22:31:36 2000 +0200
     1.2 +++ b/TFL/post.sml	Wed Aug 30 10:21:19 2000 +0200
     1.3 @@ -198,9 +198,8 @@
     1.4  		{f = f, R = R, rules = rules,
     1.5  		 full_pats_TCs = full_pats_TCs,
     1.6  		 TCs = TCs}
     1.7 -	val rules' = map (standard o normalize_thm [RSmp]) (R.CONJUNCTS rules)
     1.8 -    in  {induct = meta_outer
     1.9 -		   (normalize_thm [RSspec,RSmp] (induction RS spec')), 
    1.10 +	val rules' = map (standard o rulify) (R.CONJUNCTS rules)
    1.11 +    in  {induct = meta_outer (rulify (induction RS spec')), 
    1.12  	 rules = ListPair.zip(rules', rows),
    1.13  	 tcs = (termination_goals rules') @ tcs}
    1.14      end
     2.1 --- a/src/HOL/Finite.ML	Tue Aug 29 22:31:36 2000 +0200
     2.2 +++ b/src/HOL/Finite.ML	Wed Aug 30 10:21:19 2000 +0200
     2.3 @@ -570,7 +570,7 @@
     2.4  
     2.5  
     2.6  Goal "[| (A, x) : foldSet f e;  (A, y) : foldSet f e |] ==> y=x";
     2.7 -by (blast_tac (claset() addIs [normalize_thm [RSspec, RSmp] lemma]) 1);
     2.8 +by (blast_tac (claset() addIs [rulify lemma]) 1);
     2.9  qed "foldSet_determ";
    2.10  
    2.11  Goalw [fold_def] "(A,y) : foldSet f e ==> fold f e A = y";
     3.1 --- a/src/HOL/HOL.thy	Tue Aug 29 22:31:36 2000 +0200
     3.2 +++ b/src/HOL/HOL.thy	Wed Aug 30 10:21:19 2000 +0200
     3.3 @@ -191,7 +191,7 @@
     3.4  
     3.5  (* theory and package setup *)
     3.6  
     3.7 -use "HOL_lemmas.ML"	setup attrib_setup
     3.8 +use "HOL_lemmas.ML"
     3.9  use "cladata.ML"	setup hypsubst_setup setup Classical.setup setup clasetup
    3.10  
    3.11  lemma all_eq: "(!!x. P x) == Trueprop (ALL x. P x)"
    3.12 @@ -219,6 +219,6 @@
    3.13  use "simpdata.ML"	setup Simplifier.setup
    3.14  			setup "Simplifier.method_setup Splitter.split_modifiers" setup simpsetup
    3.15                          setup Splitter.setup setup Clasimp.setup setup iff_attrib_setup
    3.16 -
    3.17 +			setup attrib_setup
    3.18  
    3.19  end
     4.1 --- a/src/HOL/HOL_lemmas.ML	Tue Aug 29 22:31:36 2000 +0200
     4.2 +++ b/src/HOL/HOL_lemmas.ML	Wed Aug 30 10:21:19 2000 +0200
     4.3 @@ -501,62 +501,3 @@
     4.4  
     4.5  
     4.6  fun strip_tac i = REPEAT(resolve_tac [impI,allI] i); 
     4.7 -
     4.8 -(** strip ALL and --> from proved goal while preserving ALL-bound var names **)
     4.9 -
    4.10 -(** THIS CODE IS A MESS!!! **)
    4.11 -
    4.12 -local
    4.13 -
    4.14 -(* Use XXX to avoid forall_intr failing because of duplicate variable name *)
    4.15 -val myspec = read_instantiate [("P","?XXX")] spec;
    4.16 -val _ $ (_ $ (vx as Var(_,vxT))) = concl_of myspec;
    4.17 -val cvx = cterm_of (#sign(rep_thm myspec)) vx;
    4.18 -val aspec = forall_intr cvx myspec;
    4.19 -
    4.20 -in
    4.21 -
    4.22 -fun RSspec th =
    4.23 -  (case concl_of th of
    4.24 -     _ $ (Const("All",_) $ Abs(a,_,_)) =>
    4.25 -         let val ca = cterm_of (#sign(rep_thm th)) (Var((a,0),vxT))
    4.26 -         in th RS forall_elim ca aspec end
    4.27 -  | _ => raise THM("RSspec",0,[th]));
    4.28 -
    4.29 -fun RSmp th =
    4.30 -  (case concl_of th of
    4.31 -     _ $ (Const("op -->",_)$_$_) => th RS mp
    4.32 -  | _ => raise THM("RSmp",0,[th]));
    4.33 -
    4.34 -fun normalize_thm funs =
    4.35 -  let fun trans [] th = th
    4.36 -	| trans (f::fs) th = (trans funs (f th)) handle THM _ => trans fs th
    4.37 -  in zero_var_indexes o strip_shyps_warning o trans funs end;
    4.38 -
    4.39 -fun qed_spec_mp name =
    4.40 -  let val thm = normalize_thm [RSspec,RSmp] (result())
    4.41 -  in ThmDatabase.ml_store_thm(name, thm) end;
    4.42 -
    4.43 -fun qed_goal_spec_mp name thy s p = 
    4.44 -	bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goal thy s p));
    4.45 -
    4.46 -fun qed_goalw_spec_mp name thy defs s p = 
    4.47 -	bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goalw thy defs s p));
    4.48 -
    4.49 -end;
    4.50 -
    4.51 -
    4.52 -(* attributes *)
    4.53 -
    4.54 -local
    4.55 -
    4.56 -fun gen_rulify x =
    4.57 -  Attrib.no_args (Drule.rule_attribute (fn _ => (normalize_thm [RSspec, RSmp]))) x;
    4.58 -
    4.59 -in
    4.60 -
    4.61 -val attrib_setup =
    4.62 - [Attrib.add_attributes
    4.63 -  [("rulify", (gen_rulify, gen_rulify), "put theorem into standard rule form")]];
    4.64 -
    4.65 -end;
     5.1 --- a/src/HOL/Lambda/ParRed.ML	Tue Aug 29 22:31:36 2000 +0200
     5.2 +++ b/src/HOL/Lambda/ParRed.ML	Wed Aug 30 10:21:19 2000 +0200
     5.3 @@ -83,7 +83,7 @@
     5.4  (*** cd ***)
     5.5  
     5.6  Goal "!t. s => t --> t => cd s";
     5.7 -by (res_inst_tac[("u","s")] cd.induct 1);
     5.8 +by (res_inst_tac[("x","s")] cd.induct 1);
     5.9  by (Auto_tac);
    5.10  by (fast_tac (claset() addSIs [par_beta_subst]) 1);
    5.11  qed_spec_mp "par_beta_cd";
     6.1 --- a/src/HOL/NumberTheory/IntFact.ML	Tue Aug 29 22:31:36 2000 +0200
     6.2 +++ b/src/HOL/NumberTheory/IntFact.ML	Wed Aug 30 10:21:19 2000 +0200
     6.3 @@ -60,7 +60,7 @@
     6.4  qed "d22set_le_swap";
     6.5  
     6.6  Goal "#1<b --> b<=a --> b:(d22set a)";
     6.7 -by (res_inst_tac [("u","a")] d22set.induct 1);
     6.8 +by (res_inst_tac [("x","a")] d22set.induct 1);
     6.9  by Auto_tac;
    6.10  by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [d22set_eq])));
    6.11  qed_spec_mp "d22set_mem";
    6.12 @@ -75,7 +75,7 @@
    6.13  Delsimps zfact.simps; 
    6.14  
    6.15  Goal "setprod(d22set a) = zfact a";
    6.16 -by (res_inst_tac [("u","a")] d22set.induct 1);
    6.17 +by (res_inst_tac [("x","a")] d22set.induct 1);
    6.18  by Safe_tac;
    6.19  by (asm_full_simp_tac (simpset() addsimps [d22set_eq,zfact_eq]) 1);
    6.20  by (stac d22set_eq 1);
     7.1 --- a/src/HOL/Subst/Unify.ML	Tue Aug 29 22:31:36 2000 +0200
     7.2 +++ b/src/HOL/Subst/Unify.ML	Wed Aug 30 10:21:19 2000 +0200
     7.3 @@ -128,7 +128,7 @@
     7.4   *---------------------------------------------------------------------------*)
     7.5  val wfr = tc0 RS conjunct1
     7.6  and tc  = tc0 RS conjunct2;
     7.7 -val unifyRules0 = map (normalize_thm [fn th => wfr RS th, fn th => tc RS th]) 
     7.8 +val unifyRules0 = map (rule_by_tactic (rtac wfr 1 THEN TRY(rtac tc 1)))
     7.9                       unify.simps;
    7.10  
    7.11  val unifyInduct0 = [wfr,tc] MRS unify.induct;
     8.1 --- a/src/HOL/UNITY/NSP_Bad.ML	Tue Aug 29 22:31:36 2000 +0200
     8.2 +++ b/src/HOL/UNITY/NSP_Bad.ML	Wed Aug 30 10:21:19 2000 +0200
     8.3 @@ -11,9 +11,8 @@
     8.4    Proc. Royal Soc. 426 (1989)
     8.5  *)
     8.6  
     8.7 -fun impOfAlways th = 
     8.8 -    normalize_thm [RSspec,RSmp]
     8.9 -       (th RS Always_includes_reachable RS subsetD RS CollectD);
    8.10 +fun impOfAlways th =
    8.11 +  rulify (th RS Always_includes_reachable RS subsetD RS CollectD);
    8.12  
    8.13  AddEs spies_partsEs;
    8.14  AddDs [impOfSubs analz_subset_parts];
     9.1 --- a/src/HOL/ex/Fib.ML	Tue Aug 29 22:31:36 2000 +0200
     9.2 +++ b/src/HOL/ex/Fib.ML	Wed Aug 30 10:21:19 2000 +0200
     9.3 @@ -24,7 +24,7 @@
     9.4  
     9.5  (*Concrete Mathematics, page 280*)
     9.6  Goal "fib (Suc (n + k)) = fib(Suc k) * fib(Suc n) + fib k * fib n";
     9.7 -by (res_inst_tac [("u","n")] fib.induct 1);
     9.8 +by (res_inst_tac [("x","n")] fib.induct 1);
     9.9  (*Simplify the LHS just enough to apply the induction hypotheses*)
    9.10  by (asm_full_simp_tac
    9.11      (simpset() addsimps [inst "x" "Suc(?m+?n)" fib_Suc_Suc]) 3);
    9.12 @@ -35,7 +35,7 @@
    9.13  
    9.14  
    9.15  Goal "fib (Suc n) ~= 0";
    9.16 -by (res_inst_tac [("u","n")] fib.induct 1);
    9.17 +by (res_inst_tac [("x","n")] fib.induct 1);
    9.18  by (ALLGOALS (asm_simp_tac (simpset() addsimps [fib_Suc_Suc])));
    9.19  qed "fib_Suc_neq_0";
    9.20  
    9.21 @@ -52,7 +52,7 @@
    9.22  Goal "int (fib (Suc (Suc n)) * fib n) = \
    9.23  \     (if n mod 2 = 0 then int (fib(Suc n) * fib(Suc n)) - #1 \
    9.24  \                     else int (fib(Suc n) * fib(Suc n)) + #1)";
    9.25 -by (res_inst_tac [("u","n")] fib.induct 1);
    9.26 +by (res_inst_tac [("x","n")] fib.induct 1);
    9.27  by (simp_tac (simpset() addsimps [fib_Suc_Suc, mod_Suc]) 2);
    9.28  by (simp_tac (simpset() addsimps [fib_Suc_Suc]) 1);
    9.29  by (asm_full_simp_tac
    9.30 @@ -65,7 +65,7 @@
    9.31  (** Towards Law 6.111 of Concrete Mathematics **)
    9.32  
    9.33  Goal "gcd(fib n, fib (Suc n)) = 1";
    9.34 -by (res_inst_tac [("u","n")] fib.induct 1);
    9.35 +by (res_inst_tac [("x","n")] fib.induct 1);
    9.36  by (asm_simp_tac (simpset() addsimps [fib_Suc3, gcd_commute, gcd_add2]) 3);
    9.37  by (ALLGOALS (simp_tac (simpset() addsimps [fib_Suc_Suc])));
    9.38  qed "gcd_fib_Suc_eq_1"; 
    10.1 --- a/src/HOL/ex/Qsort.ML	Tue Aug 29 22:31:36 2000 +0200
    10.2 +++ b/src/HOL/ex/Qsort.ML	Wed Aug 30 10:21:19 2000 +0200
    10.3 @@ -31,7 +31,7 @@
    10.4  (*** Version two: type classes ***)
    10.5  
    10.6  Goal "multiset (quickSort xs) z = multiset xs z";
    10.7 -by (res_inst_tac [("u","xs")] quickSort.induct 1);
    10.8 +by (res_inst_tac [("x","xs")] quickSort.induct 1);
    10.9  by Auto_tac;
   10.10  qed "quickSort_permutes";
   10.11  Addsimps [quickSort_permutes];
   10.12 @@ -43,7 +43,7 @@
   10.13  Addsimps [set_quickSort];
   10.14  
   10.15  Goal "sorted (op <=) (quickSort xs)";
   10.16 -by (res_inst_tac [("u","xs")] quickSort.induct 1);
   10.17 +by (res_inst_tac [("x","xs")] quickSort.induct 1);
   10.18  by (ALLGOALS Asm_simp_tac);
   10.19  by (blast_tac (claset() addIs [linorder_linear RS disjE, order_trans]) 1);
   10.20  qed_spec_mp "sorted_quickSort";
    11.1 --- a/src/HOL/ex/Recdefs.ML	Tue Aug 29 22:31:36 2000 +0200
    11.2 +++ b/src/HOL/ex/Recdefs.ML	Wed Aug 30 10:21:19 2000 +0200
    11.3 @@ -12,12 +12,12 @@
    11.4  Addsimps g.simps;
    11.5  
    11.6  Goal "g x < Suc x";
    11.7 -by (res_inst_tac [("u","x")] g.induct 1);
    11.8 +by (res_inst_tac [("x","x")] g.induct 1);
    11.9  by Auto_tac;
   11.10  qed "g_terminates";
   11.11  
   11.12  Goal "g x = 0";
   11.13 -by (res_inst_tac [("u","x")] g.induct 1);
   11.14 +by (res_inst_tac [("x","x")] g.induct 1);
   11.15  by (ALLGOALS (asm_simp_tac (simpset() addsimps [g_terminates])));
   11.16  qed "g_zero";
   11.17  
    12.1 --- a/src/HOL/simpdata.ML	Tue Aug 29 22:31:36 2000 +0200
    12.2 +++ b/src/HOL/simpdata.ML	Wed Aug 30 10:21:19 2000 +0200
    12.3 @@ -480,6 +480,37 @@
    12.4  val simpsetup =
    12.5    [fn thy => (simpset_ref_of thy := HOL_ss addcongs [if_weak_cong]; thy)];
    12.6  
    12.7 +(*** conversion of -->/! into ==>/!! ***)
    12.8 +
    12.9 +local
   12.10 +  val rules = [symmetric(thm"all_eq"),symmetric(thm"imp_eq"),Drule.norm_hhf_eq]
   12.11 +  val ss = HOL_basic_ss addsimps rules
   12.12 +in
   12.13 +
   12.14 +val rulify = zero_var_indexes o strip_shyps_warning o forall_elim_vars_safe o simplify ss;
   12.15 +
   12.16 +fun qed_spec_mp name = ThmDatabase.ml_store_thm(name, rulify(result()));
   12.17 +
   12.18 +fun qed_goal_spec_mp name thy s p = 
   12.19 +	bind_thm (name, rulify (prove_goal thy s p));
   12.20 +
   12.21 +fun qed_goalw_spec_mp name thy defs s p = 
   12.22 +	bind_thm (name, rulify (prove_goalw thy defs s p));
   12.23 +
   12.24 +end;
   12.25 +
   12.26 +local
   12.27 +
   12.28 +fun gen_rulify x =
   12.29 +  Attrib.no_args (Drule.rule_attribute (fn _ => rulify)) x;
   12.30 +
   12.31 +in
   12.32 +
   12.33 +val attrib_setup =
   12.34 + [Attrib.add_attributes
   12.35 +  [("rulify", (gen_rulify, gen_rulify), "put theorem into standard rule form")]];
   12.36 +
   12.37 +end;
   12.38  
   12.39  (*** integration of simplifier with classical reasoner ***)
   12.40