# HG changeset patch # User wenzelm # Date 964475822 -7200 # Node ID fd6866d90ec1325d6003e7a61d7b025e987b4018 # Parent 234ef8652caed1e10d37969c20a9ab564a1e2b49 avoid referencing thy value; rename_numerals: use implicit theory context; avoid some simpset_of Int.thy (why needed anyway?); diff -r 234ef8652cae -r fd6866d90ec1 src/HOL/Integ/NatBin.ML --- a/src/HOL/Integ/NatBin.ML Mon Jul 24 23:53:51 2000 +0200 +++ b/src/HOL/Integ/NatBin.ML Mon Jul 24 23:57:02 2000 +0200 @@ -16,15 +16,15 @@ (*These rewrites should one day be re-oriented...*) Goal "#0 = (0::nat)"; -by (simp_tac (simpset_of Int.thy addsimps [nat_0, nat_number_of_def]) 1); +by (simp_tac (HOL_basic_ss addsimps [nat_0, nat_number_of_def]) 1); qed "numeral_0_eq_0"; Goal "#1 = (1::nat)"; -by (simp_tac (simpset_of Int.thy addsimps [nat_1, nat_number_of_def]) 1); +by (simp_tac (HOL_basic_ss addsimps [nat_1, nat_number_of_def]) 1); qed "numeral_1_eq_1"; Goal "#2 = (2::nat)"; -by (simp_tac (simpset_of Int.thy addsimps [nat_2, nat_number_of_def]) 1); +by (simp_tac (HOL_basic_ss addsimps [nat_2, nat_number_of_def]) 1); qed "numeral_2_eq_2"; bind_thm ("zero_eq_numeral_0", numeral_0_eq_0 RS sym); @@ -229,7 +229,7 @@ eq_nat_nat_iff, eq_number_of_eq, nat_0]) 1); by (simp_tac (simpset_of Int.thy addsimps [nat_eq_iff, nat_eq_iff2, iszero_def]) 1); -by (simp_tac (simpset_of Int.thy addsimps [not_neg_eq_ge_0 RS sym]) 1); +by (simp_tac (simpset () addsimps [not_neg_eq_ge_0 RS sym]) 1); qed "eq_nat_number_of"; Addsimps [eq_nat_number_of]; @@ -262,10 +262,6 @@ (*** New versions of existing theorems involving 0, 1, 2 ***) -fun change_theory thy th = - [th, read_instantiate_sg (sign_of thy) [("t","dummyVar")] refl] - MRS (conjI RS conjunct1) |> standard; - (*Maps n to #n for n = 0, 1, 2*) val numeral_sym_ss = HOL_ss addsimps [numeral_0_eq_0 RS sym, @@ -273,7 +269,7 @@ numeral_2_eq_2 RS sym, Suc_numeral_1_eq_2, Suc_numeral_0_eq_1]; -fun rename_numerals thy th = simplify numeral_sym_ss (change_theory thy th); +fun rename_numerals th = simplify numeral_sym_ss (Thm.transfer (the_context ()) th); (*Maps #n to n for n = 0, 1, 2*) val numeral_ss = @@ -291,10 +287,9 @@ (** NatDef & Nat **) -Addsimps (map (rename_numerals thy) - [min_0L, min_0R, max_0L, max_0R]); +Addsimps (map rename_numerals [min_0L, min_0R, max_0L, max_0R]); -AddIffs (map (rename_numerals thy) +AddIffs (map rename_numerals [Suc_not_Zero, Zero_not_Suc, zero_less_Suc, not_less0, less_one, le0, le_0_eq, neq0_conv, zero_neq_conv, not_gr0]); @@ -303,19 +298,19 @@ (*Identity laws for + - * *) val basic_renamed_arith_simps = - map (rename_numerals thy) + map rename_numerals [diff_0, diff_0_eq_0, add_0, add_0_right, mult_0, mult_0_right, mult_1, mult_1_right]; (*Non-trivial simplifications*) val other_renamed_arith_simps = - map (rename_numerals thy) + map rename_numerals [add_pred, diff_is_0_eq, zero_is_diff_eq, zero_less_diff, mult_is_0, zero_is_mult, zero_less_mult_iff, mult_eq_1_iff]; Addsimps (basic_renamed_arith_simps @ other_renamed_arith_simps); -AddIffs (map (rename_numerals thy) [add_is_0, zero_is_add, add_gr_0]); +AddIffs (map rename_numerals [add_is_0, zero_is_add, add_gr_0]); Goal "Suc n = n + #1"; by (asm_simp_tac numeral_ss 1); @@ -345,26 +340,24 @@ Addsimps [inst "n" "number_of ?v" diff_less']; (*various theorems that aren't in the default simpset*) -bind_thm ("add_is_one'", rename_numerals thy add_is_1); -bind_thm ("one_is_add'", rename_numerals thy one_is_add); -bind_thm ("zero_induct'", rename_numerals thy zero_induct); -bind_thm ("diff_self_eq_0'", rename_numerals thy diff_self_eq_0); -bind_thm ("mult_eq_self_implies_10'", rename_numerals thy mult_eq_self_implies_10); -bind_thm ("le_pred_eq'", rename_numerals thy le_pred_eq); -bind_thm ("less_pred_eq'", rename_numerals thy less_pred_eq); +bind_thm ("add_is_one'", rename_numerals add_is_1); +bind_thm ("one_is_add'", rename_numerals one_is_add); +bind_thm ("zero_induct'", rename_numerals zero_induct); +bind_thm ("diff_self_eq_0'", rename_numerals diff_self_eq_0); +bind_thm ("mult_eq_self_implies_10'", rename_numerals mult_eq_self_implies_10); +bind_thm ("le_pred_eq'", rename_numerals le_pred_eq); +bind_thm ("less_pred_eq'", rename_numerals less_pred_eq); (** Divides **) -Addsimps (map (rename_numerals thy) [mod_1, mod_0, div_1, div_0]); - -AddIffs (map (rename_numerals thy) - [dvd_1_left, dvd_0_right]); +Addsimps (map rename_numerals [mod_1, mod_0, div_1, div_0]); +AddIffs (map rename_numerals [dvd_1_left, dvd_0_right]); (*useful?*) -bind_thm ("mod_self'", rename_numerals thy mod_self); -bind_thm ("div_self'", rename_numerals thy div_self); -bind_thm ("div_less'", rename_numerals thy div_less); -bind_thm ("mod_mult_self_is_zero'", rename_numerals thy mod_mult_self_is_0); +bind_thm ("mod_self'", rename_numerals mod_self); +bind_thm ("div_self'", rename_numerals div_self); +bind_thm ("div_less'", rename_numerals div_less); +bind_thm ("mod_mult_self_is_zero'", rename_numerals mod_mult_self_is_0); (** Power **) @@ -386,15 +379,14 @@ qed "zero_less_power'"; Addsimps [zero_less_power']; -bind_thm ("binomial_zero", rename_numerals thy binomial_0); -bind_thm ("binomial_Suc'", rename_numerals thy binomial_Suc); -bind_thm ("binomial_n_n'", rename_numerals thy binomial_n_n); +bind_thm ("binomial_zero", rename_numerals binomial_0); +bind_thm ("binomial_Suc'", rename_numerals binomial_Suc); +bind_thm ("binomial_n_n'", rename_numerals binomial_n_n); (*binomial_0_Suc doesn't work well on numerals*) -Addsimps (map (rename_numerals thy) - [binomial_n_0, binomial_zero, binomial_1]); +Addsimps (map rename_numerals [binomial_n_0, binomial_zero, binomial_1]); -Addsimps [rename_numerals thy card_Pow]; +Addsimps [rename_numerals card_Pow]; (*** Comparisons involving (0::nat) ***) @@ -466,7 +458,7 @@ \ (let pv = number_of (bin_pred v) in \ \ if neg pv then True else nat pv <= n)"; by (simp_tac - (simpset_of Int.thy addsimps + (simpset () addsimps [Let_def, less_Suc_number_of, linorder_not_less RS sym]) 1); qed "le_number_of_Suc"; @@ -474,7 +466,7 @@ \ (let pv = number_of (bin_pred v) in \ \ if neg pv then False else n <= nat pv)"; by (simp_tac - (simpset_of Int.thy addsimps + (simpset () addsimps [Let_def, less_number_of_Suc, linorder_not_less RS sym]) 1); qed "le_Suc_number_of";