# HG changeset patch # User clasohm # Date 812808603 -3600 # Node ID 3eb91524b9382aca0dda5c2378edf61d43c3bfda # Parent 290c4dfc34bae00ae4c61878aedad92d1498f43f added local simpsets; removed IOA from 'make test' diff -r 290c4dfc34ba -r 3eb91524b938 src/HOL/Arith.ML --- a/src/HOL/Arith.ML Wed Oct 04 13:01:05 1995 +0100 +++ b/src/HOL/Arith.ML Wed Oct 04 13:10:03 1995 +0100 @@ -21,42 +21,40 @@ qed_goalw "diff_0_eq_0" Arith.thy [diff_def, pred_def] "0 - n = 0" - (fn _ => [nat_ind_tac "n" 1, ALLGOALS(asm_simp_tac nat_ss)]); + (fn _ => [nat_ind_tac "n" 1, ALLGOALS Asm_simp_tac]); (*Must simplify BEFORE the induction!! (Else we get a critical pair) Suc(m) - Suc(n) rewrites to pred(Suc(m) - n) *) qed_goalw "diff_Suc_Suc" Arith.thy [diff_def, pred_def] "Suc(m) - Suc(n) = m - n" (fn _ => - [simp_tac nat_ss 1, nat_ind_tac "n" 1, ALLGOALS(asm_simp_tac nat_ss)]); + [Simp_tac 1, nat_ind_tac "n" 1, ALLGOALS Asm_simp_tac]); (*** Simplification over add, mult, diff ***) -val arith_simps = - [pred_0, pred_Suc, add_0, add_Suc, mult_0, mult_Suc, - diff_0, diff_0_eq_0, diff_Suc_Suc]; +Addsimps [pred_0, pred_Suc, add_0, add_Suc, mult_0, mult_Suc, diff_0, + diff_0_eq_0, diff_Suc_Suc]; -val arith_ss = nat_ss addsimps arith_simps; (**** Inductive properties of the operators ****) (*** Addition ***) qed_goal "add_0_right" Arith.thy "m + 0 = m" - (fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]); + (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]); qed_goal "add_Suc_right" Arith.thy "m + Suc(n) = Suc(m+n)" - (fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]); + (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]); -val arith_ss = arith_ss addsimps [add_0_right,add_Suc_right]; +Addsimps [add_0_right,add_Suc_right]; (*Associative law for addition*) qed_goal "add_assoc" Arith.thy "(m + n) + k = m + ((n + k)::nat)" - (fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]); + (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]); (*Commutative law for addition*) qed_goal "add_commute" Arith.thy "m + n = n + (m::nat)" - (fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]); + (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]); qed_goal "add_left_commute" Arith.thy "x+(y+z)=y+((x+z)::nat)" (fn _ => [rtac (add_commute RS trans) 1, rtac (add_assoc RS trans) 1, @@ -67,59 +65,59 @@ goal Arith.thy "!!k::nat. (k + m = k + n) = (m=n)"; by (nat_ind_tac "k" 1); -by (simp_tac arith_ss 1); -by (asm_simp_tac arith_ss 1); +by (Simp_tac 1); +by (Asm_simp_tac 1); qed "add_left_cancel"; goal Arith.thy "!!k::nat. (m + k = n + k) = (m=n)"; by (nat_ind_tac "k" 1); -by (simp_tac arith_ss 1); -by (asm_simp_tac arith_ss 1); +by (Simp_tac 1); +by (Asm_simp_tac 1); qed "add_right_cancel"; goal Arith.thy "!!k::nat. (k + m <= k + n) = (m<=n)"; by (nat_ind_tac "k" 1); -by (simp_tac arith_ss 1); -by (asm_simp_tac (arith_ss addsimps [Suc_le_mono]) 1); +by (Simp_tac 1); +by (Asm_simp_tac 1); qed "add_left_cancel_le"; goal Arith.thy "!!k::nat. (k + m < k + n) = (m [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]); + (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]); (*right Sucessor law for multiplication*) qed_goal "mult_Suc_right" Arith.thy "m * Suc(n) = m + (m * n)" (fn _ => [nat_ind_tac "m" 1, - ALLGOALS(asm_simp_tac (arith_ss addsimps add_ac))]); + ALLGOALS(asm_simp_tac (!simpset addsimps add_ac))]); -val arith_ss = arith_ss addsimps [mult_0_right,mult_Suc_right]; +Addsimps [mult_0_right,mult_Suc_right]; (*Commutative law for multiplication*) qed_goal "mult_commute" Arith.thy "m * n = n * (m::nat)" - (fn _ => [nat_ind_tac "m" 1, ALLGOALS (asm_simp_tac arith_ss)]); + (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]); (*addition distributes over multiplication*) qed_goal "add_mult_distrib" Arith.thy "(m + n)*k = (m*k) + ((n*k)::nat)" (fn _ => [nat_ind_tac "m" 1, - ALLGOALS(asm_simp_tac (arith_ss addsimps add_ac))]); + ALLGOALS(asm_simp_tac (!simpset addsimps add_ac))]); qed_goal "add_mult_distrib2" Arith.thy "k*(m + n) = (k*m) + ((k*n)::nat)" (fn _ => [nat_ind_tac "m" 1, - ALLGOALS(asm_simp_tac (arith_ss addsimps add_ac))]); + ALLGOALS(asm_simp_tac (!simpset addsimps add_ac))]); -val arith_ss = arith_ss addsimps [add_mult_distrib,add_mult_distrib2]; +Addsimps [add_mult_distrib,add_mult_distrib2]; (*Associative law for multiplication*) qed_goal "mult_assoc" Arith.thy "(m * n) * k = m * ((n * k)::nat)" - (fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]); + (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]); qed_goal "mult_left_commute" Arith.thy "x*(y*z) = y*((x*z)::nat)" (fn _ => [rtac trans 1, rtac mult_commute 1, rtac trans 1, @@ -130,13 +128,13 @@ (*** Difference ***) qed_goal "diff_self_eq_0" Arith.thy "m - m = 0" - (fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]); + (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]); (*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *) val [prem] = goal Arith.thy "[| ~ m n+(m-n) = (m::nat)"; by (rtac (prem RS rev_mp) 1); by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); -by (ALLGOALS(asm_simp_tac arith_ss)); +by (ALLGOALS Asm_simp_tac); qed "add_diff_inverse"; @@ -145,24 +143,24 @@ goal Arith.thy "m - n < Suc(m)"; by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); by (etac less_SucE 3); -by (ALLGOALS(asm_simp_tac arith_ss)); +by (ALLGOALS Asm_simp_tac); qed "diff_less_Suc"; goal Arith.thy "!!m::nat. m - n <= m"; by (res_inst_tac [("m","m"), ("n","n")] diff_induct 1); -by (ALLGOALS (asm_simp_tac arith_ss)); +by (ALLGOALS Asm_simp_tac); by (etac le_trans 1); -by (simp_tac (HOL_ss addsimps [le_eq_less_or_eq, lessI]) 1); +by (simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1); qed "diff_le_self"; goal Arith.thy "!!n::nat. (n+m) - n = m"; by (nat_ind_tac "n" 1); -by (ALLGOALS (asm_simp_tac arith_ss)); +by (ALLGOALS Asm_simp_tac); qed "diff_add_inverse"; goal Arith.thy "!!n::nat. n - (n+m) = 0"; by (nat_ind_tac "n" 1); -by (ALLGOALS (asm_simp_tac arith_ss)); +by (ALLGOALS Asm_simp_tac); qed "diff_add_0"; (*In ordinary notation: if 0 ~ m m - n < m" 1); by (fast_tac HOL_cs 1); by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); -by (ALLGOALS(asm_simp_tac(arith_ss addsimps [diff_less_Suc]))); +by (ALLGOALS(asm_simp_tac(!simpset addsimps [diff_less_Suc]))); qed "div_termination"; val wf_less_trans = wf_pred_nat RS wf_trancl RSN (2, def_wfrec RS trans); @@ -181,12 +179,12 @@ goal Arith.thy "!!m. m m mod n = m"; by (rtac (mod_def RS wf_less_trans) 1); -by(asm_simp_tac HOL_ss 1); +by(Asm_simp_tac 1); qed "mod_less"; goal Arith.thy "!!m. [| 0 m mod n = (m-n) mod n"; by (rtac (mod_def RS wf_less_trans) 1); -by(asm_simp_tac (nat_ss addsimps [div_termination, cut_apply, less_eq]) 1); +by(asm_simp_tac (!simpset addsimps [div_termination, cut_apply, less_eq]) 1); qed "mod_geq"; @@ -194,12 +192,12 @@ goal Arith.thy "!!m. m m div n = 0"; by (rtac (div_def RS wf_less_trans) 1); -by(asm_simp_tac nat_ss 1); +by(Asm_simp_tac 1); qed "div_less"; goal Arith.thy "!!M. [| 0 m div n = Suc((m-n) div n)"; by (rtac (div_def RS wf_less_trans) 1); -by(asm_simp_tac (nat_ss addsimps [div_termination, cut_apply, less_eq]) 1); +by(asm_simp_tac (!simpset addsimps [div_termination, cut_apply, less_eq]) 1); qed "div_geq"; (*Main Result about quotient and remainder.*) @@ -207,7 +205,7 @@ by (res_inst_tac [("n","m")] less_induct 1); by (rename_tac "k" 1); (*Variable name used in line below*) by (case_tac "k m-n = 0"; by (rtac (prem RS rev_mp) 1); by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); -by (ALLGOALS (asm_simp_tac arith_ss)); +by (ALLGOALS Asm_simp_tac); qed "less_imp_diff_is_0"; val prems = goal Arith.thy "m-n = 0 --> n-m = 0 --> m=n"; by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); -by (REPEAT(simp_tac arith_ss 1 THEN TRY(atac 1))); +by (REPEAT(Simp_tac 1 THEN TRY(atac 1))); qed "diffs0_imp_equal_lemma"; (* [| m-n = 0; n-m = 0 |] ==> m=n *) @@ -232,23 +230,23 @@ val [prem] = goal Arith.thy "m 0 Suc(m)-n = Suc(m-n)"; by (rtac (prem RS rev_mp) 1); by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); -by (ALLGOALS(asm_simp_tac arith_ss)); +by (ALLGOALS Asm_simp_tac); qed "Suc_diff_n"; goal Arith.thy "Suc(m)-n = (if m (!n. P(Suc(n))--> P(n)) --> P(k-i)"; by (res_inst_tac [("m","k"),("n","i")] diff_induct 1); -by (ALLGOALS (strip_tac THEN' simp_tac arith_ss THEN' TRY o fast_tac HOL_cs)); +by (ALLGOALS (strip_tac THEN' Simp_tac THEN' TRY o fast_tac HOL_cs)); qed "zero_induct_lemma"; val prems = goal Arith.thy "[| P(k); !!n. P(Suc(n)) ==> P(n) |] ==> P(0)"; @@ -263,13 +261,13 @@ goal Arith.thy "!!m. m (? k. n=Suc(m+k))"; by (nat_ind_tac "n" 1); -by (ALLGOALS(simp_tac arith_ss)); +by (ALLGOALS(Simp_tac)); by (REPEAT_FIRST (ares_tac [conjI, impI])); by (res_inst_tac [("x","0")] exI 2); -by (simp_tac arith_ss 2); +by (Simp_tac 2); by (safe_tac HOL_cs); by (res_inst_tac [("x","Suc(k)")] exI 1); -by (simp_tac arith_ss 1); +by (Simp_tac 1); val less_eq_Suc_add_lemma = result(); (*"m ? k. n = Suc(m+k)"*) @@ -278,13 +276,13 @@ goal Arith.thy "n <= ((m + n)::nat)"; by (nat_ind_tac "m" 1); -by (ALLGOALS(simp_tac arith_ss)); +by (ALLGOALS Simp_tac); by (etac le_trans 1); by (rtac (lessI RS less_imp_le) 1); qed "le_add2"; goal Arith.thy "n <= ((n + m)::nat)"; -by (simp_tac (arith_ss addsimps add_ac) 1); +by (simp_tac (!simpset addsimps add_ac) 1); by (rtac le_add2 1); qed "le_add1"; @@ -306,7 +304,7 @@ goal Arith.thy "!!i. i+j < (k::nat) ==> i m<=(n::nat)"; by (nat_ind_tac "k" 1); -by (ALLGOALS (asm_simp_tac arith_ss)); +by (ALLGOALS Asm_simp_tac); by (fast_tac (HOL_cs addDs [Suc_leD]) 1); val add_leD1_lemma = result(); -bind_thm ("add_leD1", add_leD1_lemma RS mp);; +bind_thm ("add_leD1", add_leD1_lemma RS mp); goal Arith.thy "!!k l::nat. [| k m i + k < j + k"; by (nat_ind_tac "k" 1); -by (ALLGOALS (asm_simp_tac arith_ss)); +by (ALLGOALS Asm_simp_tac); qed "add_less_mono1"; (*strict, in both arguments*) @@ -351,7 +350,7 @@ by (rtac (add_less_mono1 RS less_trans) 1); by (REPEAT (assume_tac 1)); by (nat_ind_tac "j" 1); -by (ALLGOALS (asm_simp_tac arith_ss)); +by (ALLGOALS Asm_simp_tac); qed "add_less_mono"; (*A [clumsy] way of lifting < monotonicity to <= monotonicity *) @@ -360,7 +359,7 @@ \ i <= j \ \ |] ==> f(i) <= (f(j)::nat)"; by (cut_facts_tac [le] 1); -by (asm_full_simp_tac (HOL_ss addsimps [le_eq_less_or_eq]) 1); +by (asm_full_simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1); by (fast_tac (HOL_cs addSIs [lt_mono]) 1); qed "less_mono_imp_le_mono"; @@ -374,7 +373,7 @@ (*non-strict, in both arguments*) goal Arith.thy "!!k l::nat. [|i<=j; k<=l |] ==> i + k <= j + l"; by (etac (add_le_mono1 RS le_trans) 1); -by (simp_tac (HOL_ss addsimps [add_commute]) 1); +by (simp_tac (!simpset addsimps [add_commute]) 1); (*j moves to the end because it is free while k, l are bound*) by (eresolve_tac [add_le_mono1] 1); qed "add_le_mono"; diff -r 290c4dfc34ba -r 3eb91524b938 src/HOL/Finite.ML --- a/src/HOL/Finite.ML Wed Oct 04 13:01:05 1995 +0100 +++ b/src/HOL/Finite.ML Wed Oct 04 13:10:03 1995 +0100 @@ -33,13 +33,13 @@ (** Simplification for Fin **) -val Fin_ss = set_ss addsimps Fin.intrs; +Addsimps Fin.intrs; (*The union of two finite sets is finite*) val major::prems = goal Finite.thy "[| F: Fin(A); G: Fin(A) |] ==> F Un G : Fin(A)"; by (rtac (major RS Fin_induct) 1); -by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[Un_insert_left])))); +by (ALLGOALS (asm_simp_tac (!simpset addsimps (prems @ [Un_insert_left])))); qed "Fin_UnI"; (*Every subset of a finite set is finite*) @@ -48,18 +48,19 @@ rtac mp, etac spec, rtac subs]); by (rtac (fin RS Fin_induct) 1); -by (simp_tac (Fin_ss addsimps [subset_Un_eq]) 1); +by (simp_tac (!simpset addsimps [subset_Un_eq]) 1); by (safe_tac (set_cs addSDs [subset_insert_iff RS iffD1])); by (eres_inst_tac [("t","C")] (insert_Diff RS subst) 2); -by (ALLGOALS (asm_simp_tac Fin_ss)); +by (ALLGOALS Asm_simp_tac); qed "Fin_subset"; (*The image of a finite set is finite*) val major::_ = goal Finite.thy "F: Fin(A) ==> h``F : Fin(h``A)"; by (rtac (major RS Fin_induct) 1); -by (simp_tac Fin_ss 1); -by (asm_simp_tac (set_ss addsimps [image_eqI RS Fin.insertI, image_insert]) 1); +by (Simp_tac 1); +by (asm_simp_tac + (!simpset addsimps [image_eqI RS Fin.insertI, image_insert]) 1); qed "Fin_imageI"; val major::prems = goal Finite.thy @@ -70,7 +71,7 @@ by (rtac (major RS Fin_induct) 1); by (rtac (Diff_insert RS ssubst) 2); by (ALLGOALS (asm_simp_tac - (Fin_ss addsimps (prems@[Diff_subset RS Fin_subset])))); + (!simpset addsimps (prems@[Diff_subset RS Fin_subset])))); qed "Fin_empty_induct_lemma"; val prems = goal Finite.thy diff -r 290c4dfc34ba -r 3eb91524b938 src/HOL/Fun.ML --- a/src/HOL/Fun.ML Wed Oct 04 13:01:05 1995 +0100 +++ b/src/HOL/Fun.ML Wed Oct 04 13:10:03 1995 +0100 @@ -6,10 +6,12 @@ Lemmas about functions. *) +simpset := HOL_ss; + goal Fun.thy "(f = g) = (!x. f(x)=g(x))"; by (rtac iffI 1); -by(asm_simp_tac HOL_ss 1); -by(rtac ext 1 THEN asm_simp_tac HOL_ss 1); +by (Asm_simp_tac 1); +by (rtac ext 1 THEN Asm_simp_tac 1); qed "expand_fun_eq"; val prems = goal Fun.thy @@ -194,7 +196,6 @@ val mksimps_pairs = ("Ball",[bspec]) :: mksimps_pairs; -val set_ss = - HOL_ss addsimps mem_simps - addcongs [ball_cong,bex_cong] - setmksimps (mksimps mksimps_pairs); +simpset := !simpset addsimps mem_simps + addcongs [ball_cong,bex_cong] + setmksimps (mksimps mksimps_pairs); diff -r 290c4dfc34ba -r 3eb91524b938 src/HOL/Lfp.ML --- a/src/HOL/Lfp.ML Wed Oct 04 13:01:05 1995 +0100 +++ b/src/HOL/Lfp.ML Wed Oct 04 13:10:03 1995 +0100 @@ -59,7 +59,7 @@ brs prems 1; by(res_inst_tac[("p","x")]PairE 1); by(hyp_subst_tac 1); -by(asm_simp_tac (prod_ss addsimps prems) 1); +by(asm_simp_tac (!simpset addsimps prems) 1); qed"induct2"; (*** Fixpoint induction a la David Park ***) diff -r 290c4dfc34ba -r 3eb91524b938 src/HOL/Lfp.thy --- a/src/HOL/Lfp.thy Wed Oct 04 13:01:05 1995 +0100 +++ b/src/HOL/Lfp.thy Wed Oct 04 13:10:03 1995 +0100 @@ -1,4 +1,4 @@ -(* Title: HOL/lfp.thy +(* Title: HOL/Lfp.thy ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge diff -r 290c4dfc34ba -r 3eb91524b938 src/HOL/List.ML --- a/src/HOL/List.ML Wed Oct 04 13:01:05 1995 +0100 +++ b/src/HOL/List.ML Wed Oct 04 13:10:03 1995 +0100 @@ -15,53 +15,39 @@ bind_thm("Cons_inject", (hd list.inject) RS iffD1 RS conjE); -val list_ss = HOL_ss addsimps list.simps; - goal List.thy "!x. xs ~= x#xs"; by (list.induct_tac "xs" 1); -by (ALLGOALS (asm_simp_tac list_ss)); +by (ALLGOALS Asm_simp_tac); qed "not_Cons_self"; goal List.thy "(xs ~= []) = (? y ys. xs = y#ys)"; by (list.induct_tac "xs" 1); -by (simp_tac list_ss 1); -by (asm_simp_tac list_ss 1); +by (Simp_tac 1); +by (Asm_simp_tac 1); by (REPEAT(resolve_tac [exI,refl,conjI] 1)); qed "neq_Nil_conv"; -val list_ss = arith_ss addsimps list.simps @ - [null_Nil, null_Cons, hd_Cons, tl_Cons, ttl_Nil, ttl_Cons, - mem_Nil, mem_Cons, - append_Nil, append_Cons, - rev_Nil, rev_Cons, - map_Nil, map_Cons, - flat_Nil, flat_Cons, - list_all_Nil, list_all_Cons, - filter_Nil, filter_Cons, - foldl_Nil, foldl_Cons, - length_Nil, length_Cons]; - (** @ - append **) goal List.thy "(xs@ys)@zs = xs@(ys@zs)"; by (list.induct_tac "xs" 1); -by (ALLGOALS (asm_simp_tac list_ss)); +by (ALLGOALS Asm_simp_tac); qed "append_assoc"; goal List.thy "xs @ [] = xs"; by (list.induct_tac "xs" 1); -by (ALLGOALS (asm_simp_tac list_ss)); +by (ALLGOALS Asm_simp_tac); qed "append_Nil2"; goal List.thy "(xs@ys = []) = (xs=[] & ys=[])"; by (list.induct_tac "xs" 1); -by (ALLGOALS (asm_simp_tac list_ss)); +by (ALLGOALS Asm_simp_tac); qed "append_is_Nil"; goal List.thy "(xs @ ys = xs @ zs) = (ys=zs)"; by (list.induct_tac "xs" 1); -by (ALLGOALS (asm_simp_tac list_ss)); +by (ALLGOALS Asm_simp_tac); qed "same_append_eq"; @@ -69,12 +55,12 @@ goal List.thy "rev(xs@ys) = rev(ys) @ rev(xs)"; by (list.induct_tac "xs" 1); -by (ALLGOALS (asm_simp_tac (list_ss addsimps [append_Nil2,append_assoc]))); +by (ALLGOALS (asm_simp_tac (!simpset addsimps [append_Nil2,append_assoc]))); qed "rev_append"; goal List.thy "rev(rev l) = l"; by (list.induct_tac "l" 1); -by (ALLGOALS (asm_simp_tac (list_ss addsimps [rev_append]))); +by (ALLGOALS (asm_simp_tac (!simpset addsimps [rev_append]))); qed "rev_rev_ident"; @@ -82,29 +68,29 @@ goal List.thy "x mem (xs@ys) = (x mem xs | x mem ys)"; by (list.induct_tac "xs" 1); -by (ALLGOALS (asm_simp_tac (list_ss setloop (split_tac [expand_if])))); +by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if])))); qed "mem_append"; goal List.thy "x mem [x:xs.P(x)] = (x mem xs & P(x))"; by (list.induct_tac "xs" 1); -by (ALLGOALS (asm_simp_tac (list_ss setloop (split_tac [expand_if])))); +by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if])))); qed "mem_filter"; (** list_all **) goal List.thy "(Alls x:xs.True) = True"; by (list.induct_tac "xs" 1); -by (ALLGOALS (asm_simp_tac list_ss)); +by (ALLGOALS Asm_simp_tac); qed "list_all_True"; goal List.thy "list_all p (xs@ys) = (list_all p xs & list_all p ys)"; by (list.induct_tac "xs" 1); -by (ALLGOALS (asm_simp_tac list_ss)); +by (ALLGOALS Asm_simp_tac); qed "list_all_conj"; goal List.thy "(Alls x:xs.P(x)) = (!x. x mem xs --> P(x))"; by (list.induct_tac "xs" 1); -by (ALLGOALS (asm_simp_tac (list_ss setloop (split_tac [expand_if])))); +by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if])))); by (fast_tac HOL_cs 1); qed "list_all_mem_conv"; @@ -115,7 +101,7 @@ "P(list_case a f xs) = ((xs=[] --> P(a)) & \ \ (!y ys. xs=y#ys --> P(f y ys)))"; by (list.induct_tac "xs" 1); -by (ALLGOALS (asm_simp_tac list_ss)); +by (ALLGOALS Asm_simp_tac); by (fast_tac HOL_cs 1); qed "expand_list_case"; @@ -130,19 +116,19 @@ goal List.thy "flat(xs@ys) = flat(xs)@flat(ys)"; by (list.induct_tac "xs" 1); -by (ALLGOALS (asm_simp_tac (list_ss addsimps [append_assoc]))); +by (ALLGOALS (asm_simp_tac (!simpset addsimps [append_assoc]))); qed"flat_append"; (** length **) goal List.thy "length(xs@ys) = length(xs)+length(ys)"; by (list.induct_tac "xs" 1); -by (ALLGOALS (asm_simp_tac list_ss)); +by (ALLGOALS Asm_simp_tac); qed"length_append"; goal List.thy "length(rev xs) = length(xs)"; by (list.induct_tac "xs" 1); -by (ALLGOALS (asm_simp_tac (list_ss addsimps [length_append]))); +by (ALLGOALS (asm_simp_tac (!simpset addsimps [length_append]))); qed "length_rev"; (** nth **) @@ -156,31 +142,31 @@ goal List.thy "map (%x.x) = (%xs.xs)"; by (rtac ext 1); by (list.induct_tac "xs" 1); -by (ALLGOALS (asm_simp_tac list_ss)); +by (ALLGOALS Asm_simp_tac); qed "map_ident"; goal List.thy "map f (xs@ys) = map f xs @ map f ys"; by (list.induct_tac "xs" 1); -by (ALLGOALS (asm_simp_tac list_ss)); +by (ALLGOALS Asm_simp_tac); qed "map_append"; goalw List.thy [o_def] "map (f o g) xs = map f (map g xs)"; by (list.induct_tac "xs" 1); -by (ALLGOALS (asm_simp_tac list_ss)); +by (ALLGOALS Asm_simp_tac); qed "map_compose"; goal List.thy "rev(map f l) = map f (rev l)"; by (list.induct_tac "l" 1); -by (ALLGOALS (asm_simp_tac (list_ss addsimps [map_append]))); +by (ALLGOALS (asm_simp_tac (!simpset addsimps [map_append]))); qed "rev_map_distrib"; goal List.thy "rev(flat ls) = flat (map rev (rev ls))"; by (list.induct_tac "ls" 1); -by (ALLGOALS (asm_simp_tac (list_ss addsimps +by (ALLGOALS (asm_simp_tac (!simpset addsimps [map_append, flat_append, rev_append, append_Nil2]))); qed "rev_flat"; -val list_ss = list_ss addsimps +Addsimps [not_Cons_self, append_assoc, append_Nil2, append_is_Nil, same_append_eq, mem_append, mem_filter, rev_append, rev_rev_ident, diff -r 290c4dfc34ba -r 3eb91524b938 src/HOL/Makefile --- a/src/HOL/Makefile Wed Oct 04 13:01:05 1995 +0100 +++ b/src/HOL/Makefile Wed Oct 04 13:10:03 1995 +0100 @@ -88,7 +88,7 @@ IOA: $(BIN)/HOL $(IOA_FILES) echo 'exit_use"IOA/ROOT_NTP.ML";quit();' | $(LOGIC) - echo 'exit_use"IOA/ROOT_ABP.ML";quit();' | $(LOGIC) +# echo 'exit_use"IOA/ROOT_ABP.ML";quit();' | $(LOGIC) ##Properties of substitutions SUBST_NAMES = AList Setplus Subst Unifier UTerm UTLemmas @@ -118,8 +118,8 @@ ex: $(BIN)/HOL $(EX_FILES) echo 'exit_use"ex/ROOT.ML";quit();' | $(LOGIC) -#Full test. -test: $(BIN)/HOL IMP Integ IOA Subst Lambda ex +#Full test. (IOA has been removed temporarily) +test: $(BIN)/HOL IMP Integ Subst Lambda ex echo 'Test examples ran successfully' > test .PRECIOUS: $(BIN)/Pure $(BIN)/HOL diff -r 290c4dfc34ba -r 3eb91524b938 src/HOL/Nat.ML --- a/src/HOL/Nat.ML Wed Oct 04 13:01:05 1995 +0100 +++ b/src/HOL/Nat.ML Wed Oct 04 13:10:03 1995 +0100 @@ -110,7 +110,7 @@ by (etac (inj_Rep_Nat RS injD) 1); qed "inj_Suc"; -val Suc_inject = inj_Suc RS injD;; +val Suc_inject = inj_Suc RS injD; goal Nat.thy "(Suc(m)=Suc(n)) = (m=n)"; by (EVERY1 [rtac iffI, etac Suc_inject, etac arg_cong]); @@ -118,7 +118,7 @@ goal Nat.thy "n ~= Suc(n)"; by (nat_ind_tac "n" 1); -by (ALLGOALS(asm_simp_tac (HOL_ss addsimps [Zero_not_Suc,Suc_Suc_eq]))); +by (ALLGOALS(asm_simp_tac (!simpset addsimps [Zero_not_Suc,Suc_Suc_eq]))); qed "n_not_Suc_n"; val Suc_n_not_n = n_not_Suc_n RS not_sym; @@ -164,12 +164,12 @@ goal Nat.thy "nat_rec 0 c h = c"; by (rtac (nat_rec_unfold RS trans) 1); -by (simp_tac (HOL_ss addsimps [nat_case_0]) 1); +by (simp_tac (!simpset addsimps [nat_case_0]) 1); qed "nat_rec_0"; goal Nat.thy "nat_rec (Suc n) c h = h n (nat_rec n c h)"; by (rtac (nat_rec_unfold RS trans) 1); -by (simp_tac (HOL_ss addsimps [nat_case_Suc, pred_natI, cut_apply]) 1); +by (simp_tac (!simpset addsimps [nat_case_Suc, pred_natI, cut_apply]) 1); qed "nat_rec_Suc"; (*These 2 rules ease the use of primitive recursion. NOTE USE OF == *) @@ -328,7 +328,7 @@ (*Can be used with less_Suc_eq to get n=m | n Suc(m) <= n"; -by(simp_tac nat_ss0 1); +by(Simp_tac 1); by (fast_tac (HOL_cs addEs [less_anti_refl,less_asym]) 1); qed "lessD"; goalw Nat.thy [le_def] "!!m. Suc(m) <= n ==> m <= n"; -by(asm_full_simp_tac nat_ss0 1); +by(Asm_full_simp_tac 1); by(fast_tac HOL_cs 1); qed "Suc_leD"; @@ -407,7 +405,7 @@ qed "le_eq_less_or_eq"; goal Nat.thy "n <= (n::nat)"; -by(simp_tac (HOL_ss addsimps [le_eq_less_or_eq]) 1); +by(simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1); qed "le_refl"; val prems = goal Nat.thy "!!i. [| i <= j; j < k |] ==> i < (k::nat)"; @@ -431,7 +429,7 @@ qed "le_anti_sym"; goal Nat.thy "(Suc(n) <= Suc(m)) = (n <= m)"; -by (simp_tac (nat_ss0 addsimps [le_eq_less_or_eq]) 1); +by (simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1); qed "Suc_le_mono"; -val nat_ss = nat_ss0 addsimps [le_refl,Suc_le_mono]; +Addsimps [le_refl,Suc_le_mono]; diff -r 290c4dfc34ba -r 3eb91524b938 src/HOL/Prod.ML --- a/src/HOL/Prod.ML Wed Oct 04 13:01:05 1995 +0100 +++ b/src/HOL/Prod.ML Wed Oct 04 13:10:03 1995 +0100 @@ -58,12 +58,12 @@ by (rtac refl 1); qed "split"; -val prod_ss = set_ss addsimps [fst_conv, snd_conv, split, Pair_eq]; +Addsimps [fst_conv, snd_conv, split, Pair_eq]; goal Prod.thy "(s=t) = (fst(s)=fst(t) & snd(s)=snd(t))"; by (res_inst_tac[("p","s")] PairE 1); by (res_inst_tac[("p","t")] PairE 1); -by (asm_simp_tac prod_ss 1); +by (Asm_simp_tac 1); qed "Pair_fst_snd_eq"; (*Prevents simplification of c: much faster*) @@ -74,12 +74,12 @@ (* Do not add as rewrite rule: invalidates some proofs in IMP *) goal Prod.thy "p = (fst(p),snd(p))"; by (res_inst_tac [("p","p")] PairE 1); -by (asm_simp_tac prod_ss 1); +by (Asm_simp_tac 1); qed "surjective_pairing"; goal Prod.thy "p = split (%x y.(x,y)) p"; by (res_inst_tac [("p","p")] PairE 1); -by (asm_simp_tac prod_ss 1); +by (Asm_simp_tac 1); qed "surjective_pairing2"; (*For use with split_tac and the simplifier*) @@ -95,7 +95,7 @@ Could instead call simp_tac/asm_full_simp_tac using split as rewrite.*) goal Prod.thy "!!a b c. c a b ==> split c (a,b)"; -by (asm_simp_tac prod_ss 1); +by (Asm_simp_tac 1); qed "splitI"; val prems = goalw Prod.thy [split_def] @@ -108,7 +108,7 @@ qed "splitD"; goal Prod.thy "!!a b c. z: c a b ==> z: split c (a,b)"; -by (asm_simp_tac prod_ss 1); +by (Asm_simp_tac 1); qed "mem_splitI"; val prems = goalw Prod.thy [split_def] @@ -126,13 +126,13 @@ "prod_fun (f1 o f2) (g1 o g2) = ((prod_fun f1 g1) o (prod_fun f2 g2))"; by (rtac ext 1); by (res_inst_tac [("p","x")] PairE 1); -by (asm_simp_tac (prod_ss addsimps [prod_fun,o_def]) 1); +by (asm_simp_tac (!simpset addsimps [prod_fun,o_def]) 1); qed "prod_fun_compose"; goal Prod.thy "prod_fun (%x.x) (%y.y) = (%z.z)"; by (rtac ext 1); by (res_inst_tac [("p","z")] PairE 1); -by (asm_simp_tac (prod_ss addsimps [prod_fun]) 1); +by (asm_simp_tac (!simpset addsimps [prod_fun]) 1); qed "prod_fun_ident"; val prems = goal Prod.thy "(a,b):r ==> (f(a),g(b)) : (prod_fun f g)``r"; diff -r 290c4dfc34ba -r 3eb91524b938 src/HOL/ROOT.ML --- a/src/HOL/ROOT.ML Wed Oct 04 13:01:05 1995 +0100 +++ b/src/HOL/ROOT.ML Wed Oct 04 13:10:03 1995 +0100 @@ -1,4 +1,4 @@ -(* Title: CHOL/ROOT.ML +(* Title: HOL/ROOT.ML ID: $Id$ Author: Tobias Nipkow Copyright 1993 University of Cambridge @@ -18,7 +18,6 @@ use "thy_syntax.ML"; use_thy "HOL"; -use "../Provers/simplifier.ML"; use "../Provers/splitter.ML"; use "../Provers/hypsubst.ML"; use "../Provers/classical.ML"; @@ -64,7 +63,6 @@ use "simpdata.ML"; use_thy "Ord"; use_thy "subset"; -use_thy "equalities"; use "hologic.ML"; use "subtype.ML"; use_thy "Prod"; diff -r 290c4dfc34ba -r 3eb91524b938 src/HOL/Relation.ML --- a/src/HOL/Relation.ML Wed Oct 04 13:01:05 1995 +0100 +++ b/src/HOL/Relation.ML Wed Oct 04 13:10:03 1995 +0100 @@ -83,7 +83,7 @@ (** Natural deduction for converse(r) **) goalw Relation.thy [converse_def] "!!a b r. (a,b):r ==> (b,a):converse(r)"; -by (simp_tac prod_ss 1); +by (Simp_tac 1); by (fast_tac set_cs 1); qed "converseI"; @@ -170,4 +170,4 @@ val rel_eq_cs = rel_cs addSIs [equalityI]; -val rel_ss = prod_ss addsimps [pair_in_id_conv]; +Addsimps [pair_in_id_conv]; diff -r 290c4dfc34ba -r 3eb91524b938 src/HOL/Sexp.ML --- a/src/HOL/Sexp.ML Wed Oct 04 13:01:05 1995 +0100 +++ b/src/HOL/Sexp.ML Wed Oct 04 13:10:03 1995 +0100 @@ -87,11 +87,8 @@ and pred_sexp_trans2 = pred_sexp_t2 RSN (2, trans_trancl RS transD); (*Proves goals of the form (M,N):pred_sexp^+ provided M,N:sexp*) -val pred_sexp_simps = - sexp.intrs @ - [pred_sexp_t1, pred_sexp_t2, - pred_sexp_trans1, pred_sexp_trans2, cut_apply]; -val pred_sexp_ss = HOL_ss addsimps pred_sexp_simps; +Addsimps (sexp.intrs @ [pred_sexp_t1, pred_sexp_t2, + pred_sexp_trans1, pred_sexp_trans2, cut_apply]); val major::prems = goalw Sexp.thy [pred_sexp_def] "[| p : pred_sexp; \ @@ -130,6 +127,6 @@ goal Sexp.thy "!!M. [| M: sexp; N: sexp |] ==> \ \ sexp_rec (M$N) c d h = h M N (sexp_rec M c d h) (sexp_rec N c d h)"; by (rtac (sexp_rec_unfold RS trans) 1); -by (asm_simp_tac(HOL_ss addsimps - [sexp_case_Scons,pred_sexpI1,pred_sexpI2,cut_apply])1); +by (asm_simp_tac (!simpset addsimps [sexp_case_Scons,pred_sexpI1,pred_sexpI2]) + 1); qed "sexp_rec_Scons"; diff -r 290c4dfc34ba -r 3eb91524b938 src/HOL/Sum.ML --- a/src/HOL/Sum.ML Wed Oct 04 13:01:05 1995 +0100 +++ b/src/HOL/Sum.ML Wed Oct 04 13:10:03 1995 +0100 @@ -44,11 +44,11 @@ val Inr_neq_Inl = sym RS Inl_neq_Inr; goal Sum.thy "(Inl(a)=Inr(b)) = False"; -by (simp_tac (HOL_ss addsimps [Inl_not_Inr]) 1); +by (simp_tac (!simpset addsimps [Inl_not_Inr]) 1); qed "Inl_Inr_eq"; goal Sum.thy "(Inr(b)=Inl(a)) = False"; -by (simp_tac (HOL_ss addsimps [Inl_not_Inr RS not_sym]) 1); +by (simp_tac (!simpset addsimps [Inl_not_Inr RS not_sym]) 1); qed "Inr_Inl_eq"; @@ -157,8 +157,7 @@ by (fast_tac (set_cs addSEs [make_elim Inr_inject, Inr_neq_Inl]) 1); qed "expand_sum_case"; -val sum_ss = prod_ss addsimps [Inl_eq, Inr_eq, Inl_Inr_eq, Inr_Inl_eq, - sum_case_Inl, sum_case_Inr]; +Addsimps [Inl_eq, Inr_eq, Inl_Inr_eq, Inr_Inl_eq, sum_case_Inl, sum_case_Inr]; (*Prevents simplification of f and g: much faster*) qed_goal "sum_case_weak_cong" Sum.thy diff -r 290c4dfc34ba -r 3eb91524b938 src/HOL/Univ.ML --- a/src/HOL/Univ.ML Wed Oct 04 13:01:05 1995 +0100 +++ b/src/HOL/Univ.ML Wed Oct 04 13:10:03 1995 +0100 @@ -242,7 +242,7 @@ (** Leaf vs Numb **) goalw Univ.thy [Leaf_def,Numb_def] "Leaf(a) ~= Numb(k)"; -by (simp_tac (HOL_ss addsimps [Atom_Atom_eq,Inl_not_Inr]) 1); +by (simp_tac (!simpset addsimps [Atom_Atom_eq,Inl_not_Inr]) 1); qed "Leaf_not_Numb"; bind_thm ("Numb_not_Leaf", (Leaf_not_Numb RS not_sym)); @@ -252,8 +252,7 @@ (*** ndepth -- the depth of a node ***) -val univ_simps = [apfst_conv,Scons_not_Atom,Atom_not_Scons,Scons_Scons_eq]; -val univ_ss = nat_ss addsimps univ_simps; +Addsimps [apfst_conv,Scons_not_Atom,Atom_not_Scons,Scons_Scons_eq]; goalw Univ.thy [ndepth_def] "ndepth (Abs_Node((%k.0, x))) = 0"; @@ -265,7 +264,7 @@ goal Univ.thy "k < Suc(LEAST x. f(x)=0) --> nat_case (Suc i) f k ~= 0"; by (nat_ind_tac "k" 1); -by (ALLGOALS (simp_tac nat_ss)); +by (ALLGOALS Simp_tac); by (rtac impI 1); by (etac not_less_Least 1); qed "ndepth_Push_lemma"; @@ -276,7 +275,7 @@ by (cut_facts_tac [rewrite_rule [Node_def] Rep_Node] 1); by (safe_tac set_cs); be ssubst 1; (*instantiates type variables!*) -by (simp_tac univ_ss 1); +by (Simp_tac 1); by (rtac Least_equality 1); by (rewtac Push_def); by (rtac (nat_case_Suc RS trans) 1); @@ -317,25 +316,25 @@ (** Injection nodes **) goalw Univ.thy [In0_def] "ntrunc (Suc 0) (In0 M) = {}"; -by (simp_tac (univ_ss addsimps [ntrunc_Scons,ntrunc_0]) 1); +by (simp_tac (!simpset addsimps [ntrunc_Scons,ntrunc_0]) 1); by (rewtac Scons_def); by (safe_tac (set_cs addSIs [equalityI])); qed "ntrunc_one_In0"; goalw Univ.thy [In0_def] "ntrunc (Suc (Suc k)) (In0 M) = In0 (ntrunc (Suc k) M)"; -by (simp_tac (univ_ss addsimps [ntrunc_Scons,ntrunc_Numb]) 1); +by (simp_tac (!simpset addsimps [ntrunc_Scons,ntrunc_Numb]) 1); qed "ntrunc_In0"; goalw Univ.thy [In1_def] "ntrunc (Suc 0) (In1 M) = {}"; -by (simp_tac (univ_ss addsimps [ntrunc_Scons,ntrunc_0]) 1); +by (simp_tac (!simpset addsimps [ntrunc_Scons,ntrunc_0]) 1); by (rewtac Scons_def); by (safe_tac (set_cs addSIs [equalityI])); qed "ntrunc_one_In1"; goalw Univ.thy [In1_def] "ntrunc (Suc (Suc k)) (In1 M) = In1 (ntrunc (Suc k) M)"; -by (simp_tac (univ_ss addsimps [ntrunc_Scons,ntrunc_Numb]) 1); +by (simp_tac (!simpset addsimps [ntrunc_Scons,ntrunc_Numb]) 1); qed "ntrunc_In1"; @@ -611,5 +610,4 @@ addSEs [usumE, dsumE]) 1); qed "fst_image_dsum"; -val fst_image_simps = [fst_image_diag, fst_image_dprod, fst_image_dsum]; -val fst_image_ss = univ_ss addsimps fst_image_simps; +Addsimps [fst_image_diag, fst_image_dprod, fst_image_dsum]; diff -r 290c4dfc34ba -r 3eb91524b938 src/HOL/WF.ML --- a/src/HOL/WF.ML Wed Oct 04 13:01:05 1995 +0100 +++ b/src/HOL/WF.ML Wed Oct 04 13:10:03 1995 +0100 @@ -69,12 +69,12 @@ H_cong to expose the equality*) goalw WF.thy [cut_def] "(cut f r x = cut g r x) = (!y. (y,x):r --> f(y)=g(y))"; -by(simp_tac (HOL_ss addsimps [expand_fun_eq] - setloop (split_tac [expand_if])) 1); +by(simp_tac (!simpset addsimps [expand_fun_eq] + setloop (split_tac [expand_if])) 1); qed "cut_cut_eq"; goalw WF.thy [cut_def] "!!x. (x,a):r ==> (cut f r a)(x) = f(x)"; -by(asm_simp_tac HOL_ss 1); +by(Asm_simp_tac 1); qed "cut_apply"; @@ -83,7 +83,7 @@ goalw WF.thy [is_recfun_def,cut_def] "!!f. [| is_recfun r a H f; ~(b,a):r |] ==> f(b) = (@z.True)"; by (etac ssubst 1); -by(asm_simp_tac HOL_ss 1); +by(Asm_simp_tac 1); qed "is_recfun_undef"; (*eresolve_tac transD solves (a,b):r using transitivity AT MOST ONCE @@ -100,7 +100,7 @@ (cut_facts_tac hyps THEN' DEPTH_SOLVE_1 o (ares_tac [TrueI] ORELSE' eresolve_tac [transD, mp, allE])); -val wf_super_ss = HOL_ss setsolver indhyp_tac; +val wf_super_ss = !simpset setsolver indhyp_tac; val prems = goalw WF.thy [is_recfun_def,cut_def] "[| wf(r); trans(r); is_recfun r a H f; is_recfun r b H g |] ==> \ @@ -168,7 +168,7 @@ \ wftrec r a H = H a (cut (%x.wftrec r x H) r a)"; by (EVERY1 [stac (rewrite_rule [is_recfun_def] unfold_the_recfun), REPEAT o atac, rtac H_cong1]); -by (asm_simp_tac (HOL_ss addsimps [cut_cut_eq,the_recfun_cut]) 1); +by (asm_simp_tac (!simpset addsimps [cut_cut_eq,the_recfun_cut]) 1); qed "wftrec"; (*Unused but perhaps interesting*) @@ -186,7 +186,7 @@ by (etac (wf_trancl RS wftrec RS ssubst) 1); by (rtac trans_trancl 1); by (rtac (refl RS H_cong) 1); (*expose the equality of cuts*) -by (simp_tac (HOL_ss addsimps [cut_cut_eq, cut_apply, r_into_trancl]) 1); +by (simp_tac (!simpset addsimps [cut_cut_eq, cut_apply, r_into_trancl]) 1); qed "wfrec"; (*This form avoids giant explosions in proofs. NOTE USE OF == *) diff -r 290c4dfc34ba -r 3eb91524b938 src/HOL/equalities.ML --- a/src/HOL/equalities.ML Wed Oct 04 13:01:05 1995 +0100 +++ b/src/HOL/equalities.ML Wed Oct 04 13:10:03 1995 +0100 @@ -337,7 +337,7 @@ by (fast_tac eq_cs 1); qed "Diff_Int"; -val set_ss = set_ss addsimps +Addsimps [in_empty,in_insert,insert_subset, insert_not_empty,empty_not_insert, Int_absorb,Int_empty_left,Int_empty_right, diff -r 290c4dfc34ba -r 3eb91524b938 src/HOL/indrule.ML --- a/src/HOL/indrule.ML Wed Oct 04 13:01:05 1995 +0100 +++ b/src/HOL/indrule.ML Wed Oct 04 13:10:03 1995 +0100 @@ -87,7 +87,7 @@ (fn prems => [rtac (impI RS allI) 1, DETERM (etac raw_induct 1), - asm_full_simp_tac (HOL_ss addsimps [Part_Collect]) 1, + asm_full_simp_tac (!simpset addsimps [Part_Collect]) 1, REPEAT (FIRSTGOAL (eresolve_tac [IntE, CollectE, exE, conjE, disjE] ORELSE' hyp_subst_tac)), ind_tac (rev prems) (length prems)]) @@ -141,7 +141,8 @@ (*Simplification largely reduces the mutual induction rule to the standard rule*) -val mut_ss = set_ss addsimps [Inl_Inr_eq, Inr_Inl_eq, Inl_eq, Inr_eq]; +val mut_ss = simpset_of "Fun" + addsimps [Inl_Inr_eq, Inr_Inl_eq, Inl_eq, Inr_eq]; val all_defs = con_defs@part_rec_defs; diff -r 290c4dfc34ba -r 3eb91524b938 src/HOL/intr_elim.ML --- a/src/HOL/intr_elim.ML Wed Oct 04 13:01:05 1995 +0100 +++ b/src/HOL/intr_elim.ML Wed Oct 04 13:10:03 1995 +0100 @@ -126,7 +126,7 @@ fun con_elim_tac simps = let val elim_tac = REPEAT o (eresolve_tac (elim_rls@sumprod_free_SEs)) in ALLGOALS(EVERY'[elim_tac, - asm_full_simp_tac (nat_ss addsimps simps), + asm_full_simp_tac (simpset_of "Nat" addsimps simps), elim_tac, REPEAT o bound_hyp_subst_tac]) THEN prune_params_tac diff -r 290c4dfc34ba -r 3eb91524b938 src/HOL/mono.ML --- a/src/HOL/mono.ML Wed Oct 04 13:01:05 1995 +0100 +++ b/src/HOL/mono.ML Wed Oct 04 13:10:03 1995 +0100 @@ -1,4 +1,4 @@ -(* Title: HOL/mono +(* Title: HOL/mono.ML ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1991 University of Cambridge diff -r 290c4dfc34ba -r 3eb91524b938 src/HOL/mono.thy --- a/src/HOL/mono.thy Wed Oct 04 13:01:05 1995 +0100 +++ b/src/HOL/mono.thy Wed Oct 04 13:10:03 1995 +0100 @@ -1,8 +1,8 @@ -(* Title: HOL/mono +(* Title: HOL/mono.thy ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1991 University of Cambridge *) -mono = subset +mono = equalities diff -r 290c4dfc34ba -r 3eb91524b938 src/HOL/simpdata.ML --- a/src/HOL/simpdata.ML Wed Oct 04 13:01:05 1995 +0100 +++ b/src/HOL/simpdata.ML Wed Oct 04 13:10:03 1995 +0100 @@ -98,6 +98,8 @@ infix 4 addcongs; fun ss addcongs congs = ss addeqcongs (congs RL [eq_reflection]); +fun Addcongs congs = (simpset := !simpset addcongs congs); + (*Add a simpset to a classical set!*) infix 4 addss; fun cs addss ss = cs addbefore asm_full_simp_tac ss 1; diff -r 290c4dfc34ba -r 3eb91524b938 src/HOL/subtype.ML --- a/src/HOL/subtype.ML Wed Oct 04 13:01:05 1995 +0100 +++ b/src/HOL/subtype.ML Wed Oct 04 13:10:03 1995 +0100 @@ -45,7 +45,7 @@ fun ext_subtype prep_term name (t, vs, mx) raw_set axms thms usr_tac thy = let - val _ = require_thy thy "Set" "subtype definitions"; + val dummy = require_thy thy "Set" "subtype definitions"; val sign = sign_of thy; (*rhs*) diff -r 290c4dfc34ba -r 3eb91524b938 src/HOL/thy_syntax.ML --- a/src/HOL/thy_syntax.ML Wed Oct 04 13:01:05 1995 +0100 +++ b/src/HOL/thy_syntax.ML Wed Oct 04 13:10:03 1995 +0100 @@ -134,7 +134,8 @@ \ val recs =" ^ mk_rules tname cons "_rec_" ^ ";\n\ \ val simps = inject @ distinct @ cases @ recs;\n\ \ fun induct_tac a = res_inst_tac [(" ^ quote tname ^ ", a)] induct;\n\ - \end;\n"); + \end;\n\ + \val dummy = Addsimps " ^ tname ^ ".simps;\n"); (*parsers*) val tvars = type_args >> map (cat "dtVar"); @@ -159,11 +160,14 @@ fun mk_primrec_decl ((fname, tname), axms) = let fun mk_prove (name, eqn) = - "val " ^ name ^ " = store_thm (" ^ quote name ^ ", prove_goalw thy [get_def thy " - ^ fname ^ "] " ^ eqn ^ "\n\ - \ (fn _ => [simp_tac (HOL_ss addsimps " ^ tname ^ ".recs) 1]));"; + "val " ^ name ^ " = store_thm (" ^ quote name + ^ ", prove_goalw thy [get_def thy " ^ fname ^ "] " ^ eqn ^ "\n\ + \ (fn _ => [Simp_tac 1]));"; + val axs = mk_list (map (fn (n, a) => mk_pair (quote n, a)) axms); - in ("|> " ^ tname ^ "_add_primrec " ^ axs, cat_lines (map mk_prove axms)) end; + in ("|> " ^ tname ^ "_add_primrec " ^ axs, cat_lines (map mk_prove axms) + ^ "\nval dummy = Addsimps " ^ mk_list (map fst axms) ^ ";") + end; val primrec_decl = name -- long_id -- repeat1 (ident -- string) >> mk_primrec_decl; diff -r 290c4dfc34ba -r 3eb91524b938 src/HOL/typedef.ML --- a/src/HOL/typedef.ML Wed Oct 04 13:01:05 1995 +0100 +++ b/src/HOL/typedef.ML Wed Oct 04 13:10:03 1995 +0100 @@ -45,7 +45,7 @@ fun ext_subtype prep_term name (t, vs, mx) raw_set axms thms usr_tac thy = let - val _ = require_thy thy "Set" "subtype definitions"; + val dummy = require_thy thy "Set" "subtype definitions"; val sign = sign_of thy; (*rhs*)