--- a/src/HOL/BCV/Fixpoint.ML Thu Mar 30 19:45:18 2000 +0200
+++ b/src/HOL/BCV/Fixpoint.ML Thu Mar 30 19:45:51 2000 +0200
@@ -33,7 +33,7 @@
\ !a:A. next a : option A; s:A |] ==> \
\ fix(next,s) = (case next s of None => False \
\ | Some t => if t=s then True else fix(next,t))";
-by (stac (fix_tc RS (hd fix.rules)) 1);
+by (stac (fix_tc RS (hd fix.simps)) 1);
by (Simp_tac 1);
by (Clarify_tac 1);
by (subgoal_tac "!i. f i : A" 1);
--- a/src/HOL/Integ/IntDiv.ML Thu Mar 30 19:45:18 2000 +0200
+++ b/src/HOL/Integ/IntDiv.ML Thu Mar 30 19:45:51 2000 +0200
@@ -99,7 +99,7 @@
(* removing the termination condition from the generated theorems *)
-bind_thm ("posDivAlg_raw_eqn", lemma RS hd posDivAlg.rules);
+bind_thm ("posDivAlg_raw_eqn", lemma RS hd posDivAlg.simps);
(**use with simproc to avoid re-proving the premise*)
Goal "#0 < b ==> \
@@ -140,7 +140,7 @@
(* removing the termination condition from the generated theorems *)
-bind_thm ("negDivAlg_raw_eqn", lemma RS hd negDivAlg.rules);
+bind_thm ("negDivAlg_raw_eqn", lemma RS hd negDivAlg.simps);
(**use with simproc to avoid re-proving the premise*)
Goal "#0 < b ==> \
--- a/src/HOL/Isar_examples/Fibonacci.thy Thu Mar 30 19:45:18 2000 +0200
+++ b/src/HOL/Isar_examples/Fibonacci.thy Thu Mar 30 19:45:51 2000 +0200
@@ -30,9 +30,7 @@
recdef fib less_than
"fib 0 = 0"
"fib 1 = 1"
- "fib (Suc (Suc x)) = (fib x + fib (Suc x))";
-
-lemmas [simp] = fib.rules;
+ "fib (Suc (Suc x)) = fib x + fib(Suc x)";
lemma [simp]: "0 < fib (Suc n)";
by (induct n rule: fib.induct) (simp+);
--- a/src/HOL/Lambda/Commutation.thy Thu Mar 30 19:45:18 2000 +0200
+++ b/src/HOL/Lambda/Commutation.thy Thu Mar 30 19:45:51 2000 +0200
@@ -6,7 +6,7 @@
Abstract commutation and confluence notions.
*)
-Commutation = Trancl +
+Commutation = Main +
consts
square :: "[('a*'a)set,('a*'a)set,('a*'a)set,('a*'a)set] => bool"
--- a/src/HOL/Lambda/ParRed.ML Thu Mar 30 19:45:18 2000 +0200
+++ b/src/HOL/Lambda/ParRed.ML Thu Mar 30 19:45:51 2000 +0200
@@ -82,8 +82,6 @@
(*** cd ***)
-Addsimps cd.rules;
-
Goal "!t. s => t --> t => cd s";
by (res_inst_tac[("u","s")] cd.induct 1);
by (Auto_tac);
--- a/src/HOL/Lambda/ParRed.thy Thu Mar 30 19:45:18 2000 +0200
+++ b/src/HOL/Lambda/ParRed.thy Thu Mar 30 19:45:51 2000 +0200
@@ -6,7 +6,7 @@
Parallel reduction and a complete developments function "cd".
*)
-ParRed = Lambda + Commutation + Recdef +
+ParRed = Lambda + Commutation +
consts par_beta :: "(dB * dB) set"
--- a/src/HOL/Lex/MaxChop.ML Thu Mar 30 19:45:18 2000 +0200
+++ b/src/HOL/Lex/MaxChop.ML Thu Mar 30 19:45:51 2000 +0200
@@ -15,7 +15,7 @@
by (blast_tac (claset() addDs [sym]) 1);
val lemma = result();
-val chopr_rule = let val [chopr_rule] = chopr.rules in lemma RS chopr_rule end;
+val chopr_rule = let val [chopr_rule] = chopr.simps in lemma RS chopr_rule end;
Goalw [chop_def] "reducing splitf ==> \
\ chop splitf xs = (let (pre,post) = splitf xs \
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML Thu Mar 30 19:45:18 2000 +0200
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML Thu Mar 30 19:45:51 2000 +0200
@@ -4,7 +4,7 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-val defs1 = exec.rules@[split_def,sup_state_def,correct_state_def,
+val defs1 = exec.simps@[split_def,sup_state_def,correct_state_def,
correct_frame_def,wt_instr_def];
Goalw [correct_state_def,Let_def,correct_frame_def,split_def]
@@ -541,14 +541,14 @@
by(rename_tac "xp hp frs" 1);
by (case_tac "xp" 1);
by (case_tac "frs" 1);
- by (asm_full_simp_tac (simpset() addsimps exec.rules) 1);
+ by (asm_full_simp_tac (simpset() addsimps exec.simps) 1);
by(split_all_tac 1);
by(hyp_subst_tac 1);
by(forward_tac [correct_state_impl_Some_method] 1);
by (force_tac (claset() addIs [LS_correct,CO_correct,MO_correct,CH_correct,MI_correct,MR_correct,OS_correct,
- BR_correct], simpset() addsplits [split_if_asm,instr.split,instr.split_asm] addsimps exec.rules@[split_def]) 1);
+ BR_correct], simpset() addsplits [split_if_asm,instr.split,instr.split_asm] addsimps exec.simps@[split_def]) 1);
by (case_tac "frs" 1);
- by (ALLGOALS(asm_full_simp_tac (simpset() addsimps exec.rules)));
+ by (ALLGOALS(asm_full_simp_tac (simpset() addsimps exec.simps)));
qed_spec_mp "BV_correct_1";
(*******)
--- a/src/HOL/MicroJava/J/WellForm.ML Thu Mar 30 19:45:18 2000 +0200
+++ b/src/HOL/MicroJava/J/WellForm.ML Thu Mar 30 19:45:51 2000 +0200
@@ -99,7 +99,7 @@
\ (case class G C of None \\<Rightarrow> empty | Some (sc,fs,ms) \\<Rightarrow> \
\ (case sc of None \\<Rightarrow> empty | Some D \\<Rightarrow> method (G,D)) \\<oplus> \
\ map_of (map (\\<lambda>(s,m). (s,(C,m))) ms))";
-by( stac (method_TC RS (wf_subcls1_rel RS (hd method.rules))) 1);
+by( stac (method_TC RS (wf_subcls1_rel RS (hd method.simps))) 1);
by( clarsimp_tac (claset(), simpset() addsimps [wf_subcls1,empty_def]
addsplits [option.split]) 1);
by( case_tac "C = Object" 1);
@@ -114,7 +114,7 @@
Goal "\\<lbrakk>class G C = Some (sc,fs,ms); wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> fields (G,C) = \
\ map (\\<lambda>(fn,ft). ((fn,C),ft)) fs @ \
\ (case sc of None \\<Rightarrow> [] | Some D \\<Rightarrow> fields (G,D))";
-by( stac (fields_TC RS (wf_subcls1_rel RS (hd fields.rules))) 1);
+by( stac (fields_TC RS (wf_subcls1_rel RS (hd fields.simps))) 1);
by( asm_simp_tac (simpset() addsimps [wf_subcls1,empty_def]) 1);
by( option_case_tac2 "sc" 1);
by( Asm_simp_tac 1);
--- a/src/HOL/Subst/Unify.ML Thu Mar 30 19:45:18 2000 +0200
+++ b/src/HOL/Subst/Unify.ML Thu Mar 30 19:45:51 2000 +0200
@@ -38,7 +38,7 @@
(*---------------------------------------------------------------------------
* The non-nested TC plus the wellfoundedness of unifyRel.
*---------------------------------------------------------------------------*)
-Tfl.tgoalw Unify.thy [] unify.rules;
+Tfl.tgoalw Unify.thy [] unify.simps;
(* Wellfoundedness of unifyRel *)
by (simp_tac (simpset() addsimps [unifyRel_def,
wf_inv_image, wf_lex_prod, wf_finite_psubset,
@@ -129,7 +129,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])
- unify.rules;
+ unify.simps;
val unifyInduct0 = [wfr,tc] MRS unify.induct;
@@ -170,7 +170,7 @@
(*---------------------------------------------------------------------------
- * Now for elimination of nested TC from unify.rules and induction.
+ * Now for elimination of nested TC from unify.simps and induction.
*---------------------------------------------------------------------------*)
(*Desired rule, copied from the theory file. Could it be made available?*)
--- a/src/HOL/ex/Fib.ML Thu Mar 30 19:45:18 2000 +0200
+++ b/src/HOL/ex/Fib.ML Thu Mar 30 19:45:51 2000 +0200
@@ -17,10 +17,8 @@
selectively at first.
**)
-val [fib_0, fib_1, fib_Suc_Suc] = fib.rules;
-
-Addsimps [fib_0, fib_1];
-
+val [fib_Suc_Suc] = thms"fib.2";
+Delsimps [fib_Suc_Suc];
val fib_Suc3 = read_instantiate [("x", "(Suc ?n)")] fib_Suc_Suc;
--- a/src/HOL/ex/Primes.ML Thu Mar 30 19:45:18 2000 +0200
+++ b/src/HOL/ex/Primes.ML Thu Mar 30 19:45:51 2000 +0200
@@ -20,11 +20,11 @@
(** Prove the termination condition and remove it from the recursion equations
and induction rule **)
-Tfl.tgoalw thy [] gcd.rules;
+Tfl.tgoalw thy [] gcd.simps;
by (simp_tac (simpset() addsimps [mod_less_divisor]) 1);
val tc = result();
-val gcd_eq = tc RS hd gcd.rules;
+val gcd_eq = tc RS hd gcd.simps;
val prems = goal thy
"[| !!m. P m 0; \
--- a/src/HOL/ex/Primrec.ML Thu Mar 30 19:45:18 2000 +0200
+++ b/src/HOL/ex/Primrec.ML Thu Mar 30 19:45:51 2000 +0200
@@ -44,8 +44,6 @@
Addsimps [SC, CONST, PROJ_0, COMP_1, PREC_0, PREC_Suc];
-Addsimps ack.rules;
-
(*PROPERTY A 4*)
Goal "j < ack(i,j)";
by (res_inst_tac [("u","i"),("v","j")] ack.induct 1);
--- a/src/HOL/ex/Qsort.ML Thu Mar 30 19:45:18 2000 +0200
+++ b/src/HOL/ex/Qsort.ML Thu Mar 30 19:45:51 2000 +0200
@@ -8,8 +8,6 @@
(*** Version one: higher-order ***)
-Addsimps qsort.rules;
-
Goal "multiset (qsort(le,xs)) x = multiset xs x";
by (res_inst_tac [("v","xs"),("u","le")] qsort.induct 1);
by Auto_tac;
@@ -32,8 +30,6 @@
(*** Version two: type classes ***)
-Addsimps quickSort.rules;
-
Goal "multiset (quickSort xs) z = multiset xs z";
by (res_inst_tac [("u","xs")] quickSort.induct 1);
by Auto_tac;
--- a/src/HOL/ex/Recdefs.ML Thu Mar 30 19:45:18 2000 +0200
+++ b/src/HOL/ex/Recdefs.ML Thu Mar 30 19:45:51 2000 +0200
@@ -9,7 +9,7 @@
(** The silly g function: example of nested recursion **)
-Addsimps g.rules;
+Addsimps g.simps;
Goal "g x < Suc x";
by (res_inst_tac [("u","x")] g.induct 1);
@@ -32,7 +32,7 @@
val lemma = result();
(* removing the termination condition from the generated thms: *)
-val [mapf_0,mapf_Suc] = mapf.rules;
+val [mapf_0,mapf_Suc] = mapf.simps;
val mapf_Suc = lemma RS mapf_Suc;
val mapf_induct = lemma RS mapf.induct;