# HG changeset patch # User nipkow # Date 954438351 -7200 # Node ID 69619f870939253d1ad973810dd867cb86eb6682 # Parent 5668aaf41c368b67d4ccaed2c1b4e575830dacaa recdef.rules -> recdef.simps diff -r 5668aaf41c36 -r 69619f870939 src/HOL/BCV/Fixpoint.ML --- 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); diff -r 5668aaf41c36 -r 69619f870939 src/HOL/Integ/IntDiv.ML --- 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 ==> \ diff -r 5668aaf41c36 -r 69619f870939 src/HOL/Isar_examples/Fibonacci.thy --- 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+); diff -r 5668aaf41c36 -r 69619f870939 src/HOL/Lambda/Commutation.thy --- 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" diff -r 5668aaf41c36 -r 69619f870939 src/HOL/Lambda/ParRed.ML --- 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); diff -r 5668aaf41c36 -r 69619f870939 src/HOL/Lambda/ParRed.thy --- 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" diff -r 5668aaf41c36 -r 69619f870939 src/HOL/Lex/MaxChop.ML --- 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 \ diff -r 5668aaf41c36 -r 69619f870939 src/HOL/MicroJava/BV/BVSpecTypeSafe.ML --- 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"; (*******) diff -r 5668aaf41c36 -r 69619f870939 src/HOL/MicroJava/J/WellForm.ML --- 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 \\ empty | Some (sc,fs,ms) \\ \ \ (case sc of None \\ empty | Some D \\ method (G,D)) \\ \ \ map_of (map (\\(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 "\\class G C = Some (sc,fs,ms); wf_prog wf_mb G\\ \\ fields (G,C) = \ \ map (\\(fn,ft). ((fn,C),ft)) fs @ \ \ (case sc of None \\ [] | Some D \\ 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); diff -r 5668aaf41c36 -r 69619f870939 src/HOL/Subst/Unify.ML --- 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?*) diff -r 5668aaf41c36 -r 69619f870939 src/HOL/ex/Fib.ML --- 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; diff -r 5668aaf41c36 -r 69619f870939 src/HOL/ex/Primes.ML --- 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; \ diff -r 5668aaf41c36 -r 69619f870939 src/HOL/ex/Primrec.ML --- 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); diff -r 5668aaf41c36 -r 69619f870939 src/HOL/ex/Qsort.ML --- 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; diff -r 5668aaf41c36 -r 69619f870939 src/HOL/ex/Recdefs.ML --- 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;