--- a/src/HOL/Datatype.ML Thu Jun 22 11:37:13 2000 +0200
+++ b/src/HOL/Datatype.ML Thu Jun 22 23:04:34 2000 +0200
@@ -8,6 +8,8 @@
(*compatibility*)
val [sum_case_Inl, sum_case_Inr] = sum.cases;
+bind_thm ("sum_case_Inl", sum_case_Inl);
+bind_thm ("sum_case_Inr", sum_case_Inr);
Goal "sum_case (%x::'a. f(Inl x)) (%y::'b. f(Inr y)) s = f(s)";
by (EVERY1 [res_inst_tac [("s","s")] sumE,
--- a/src/HOL/Divides.ML Thu Jun 22 11:37:13 2000 +0200
+++ b/src/HOL/Divides.ML Thu Jun 22 23:04:34 2000 +0200
@@ -9,8 +9,8 @@
(** Less-then properties **)
-val wf_less_trans = [eq_reflection, wf_pred_nat RS wf_trancl] MRS
- def_wfrec RS trans;
+bind_thm ("wf_less_trans", [eq_reflection, wf_pred_nat RS wf_trancl] MRS
+ def_wfrec RS trans);
Goal "(%m. m mod n) = wfrec (trancl pred_nat) \
\ (%f j. if j<n | n=0 then j else f (j-n))";
--- a/src/HOL/Finite.ML Thu Jun 22 11:37:13 2000 +0200
+++ b/src/HOL/Finite.ML Thu Jun 22 23:04:34 2000 +0200
@@ -245,8 +245,8 @@
section "Finite cardinality -- 'card'";
-val cardR_emptyE = cardR.mk_cases "({},n) : cardR";
-val cardR_insertE = cardR.mk_cases "(insert a A,n) : cardR";
+bind_thm ("cardR_emptyE", cardR.mk_cases "({},n) : cardR");
+bind_thm ("cardR_insertE", cardR.mk_cases "(insert a A,n) : cardR");
AddSEs [cardR_emptyE];
AddSIs cardR.intrs;
@@ -491,7 +491,7 @@
(*** foldSet ***)
-val empty_foldSetE = foldSet.mk_cases "({}, x) : foldSet f e";
+bind_thm ("empty_foldSetE", foldSet.mk_cases "({}, x) : foldSet f e");
AddSEs [empty_foldSetE];
AddIs foldSet.intrs;
--- a/src/HOL/Fun.ML Thu Jun 22 11:37:13 2000 +0200
+++ b/src/HOL/Fun.ML Thu Jun 22 23:04:34 2000 +0200
@@ -151,7 +151,7 @@
"(!! x y. [| f(x) = f(y); x:A; y:A |] ==> x=y) ==> inj_on f A";
by (blast_tac (claset() addIs prems) 1);
qed "inj_onI";
-val injI = inj_onI; (*for compatibility*)
+bind_thm ("injI", inj_onI); (*for compatibility*)
val [major] = Goal
"(!!x. x:A ==> g(f(x)) = x) ==> inj_on f A";
@@ -159,7 +159,7 @@
by (etac (apply_inverse RS trans) 1);
by (REPEAT (eresolve_tac [asm_rl,major] 1));
qed "inj_on_inverseI";
-val inj_inverseI = inj_on_inverseI; (*for compatibility*)
+bind_thm ("inj_inverseI", inj_on_inverseI); (*for compatibility*)
Goal "(inj f) = (inv f o f = id)";
by (asm_simp_tac (simpset() addsimps [o_def, expand_fun_eq]) 1);
@@ -483,7 +483,7 @@
Goalw [Pi_def] "[| f: Pi A B; g: Pi A B; ! x: A. f x = g x |] ==> f = g";
by (rtac ext 1);
by Auto_tac;
-val Pi_extensionality = ballI RSN (3, result());
+bind_thm ("Pi_extensionality", ballI RSN (3, result()));
(*** compose ***)
--- a/src/HOL/Integ/Bin.ML Thu Jun 22 11:37:13 2000 +0200
+++ b/src/HOL/Integ/Bin.ML Thu Jun 22 23:04:34 2000 +0200
@@ -128,7 +128,7 @@
qed "number_of_minus";
-val bin_add_simps = [bin_add_BIT_BIT, number_of_succ, number_of_pred];
+bind_thms ("bin_add_simps", [bin_add_BIT_BIT, number_of_succ, number_of_pred]);
(*This proof is complicated by the mutual recursion*)
Goal "! w. number_of(bin_add v w) = (number_of v + number_of w::int)";
@@ -147,7 +147,7 @@
by (simp_tac (simpset() addsimps [number_of_add, number_of_minus]) 1);
qed "diff_number_of_eq";
-val bin_mult_simps = [zmult_zminus, number_of_minus, number_of_add];
+bind_thms ("bin_mult_simps", [zmult_zminus, number_of_minus, number_of_add]);
Goal "number_of(bin_mult v w) = (number_of v * number_of w::int)";
by (induct_tac "v" 1);
@@ -407,10 +407,9 @@
(*Simplification of arithmetic operations on integer constants.
Note that bin_pred_Pls, etc. were added to the simpset by primrec.*)
-val NCons_simps = [NCons_Pls_0, NCons_Pls_1, NCons_Min_0, NCons_Min_1,
- NCons_BIT];
+bind_thms ("NCons_simps", [NCons_Pls_0, NCons_Pls_1, NCons_Min_0, NCons_Min_1, NCons_BIT]);
-val bin_arith_extra_simps =
+bind_thms ("bin_arith_extra_simps",
[number_of_add RS sym,
number_of_minus RS sym,
number_of_mult RS sym,
@@ -420,24 +419,24 @@
bin_add_Pls_right, bin_add_Min_right,
bin_add_BIT_0, bin_add_BIT_10, bin_add_BIT_11,
diff_number_of_eq,
- bin_mult_1, bin_mult_0] @ NCons_simps;
+ bin_mult_1, bin_mult_0] @ NCons_simps);
(*For making a minimal simpset, one must include these default simprules
of thy. Also include simp_thms, or at least (~False)=True*)
-val bin_arith_simps =
+bind_thms ("bin_arith_simps",
[bin_pred_Pls, bin_pred_Min,
bin_succ_Pls, bin_succ_Min,
bin_add_Pls, bin_add_Min,
bin_minus_Pls, bin_minus_Min,
- bin_mult_Pls, bin_mult_Min] @ bin_arith_extra_simps;
+ bin_mult_Pls, bin_mult_Min] @ bin_arith_extra_simps);
(*Simplification of relational operations*)
-val bin_rel_simps =
+bind_thms ("bin_rel_simps",
[eq_number_of_eq, iszero_number_of_Pls, nonzero_number_of_Min,
iszero_number_of_0, iszero_number_of_1,
less_number_of_eq_neg,
not_neg_number_of_Pls, neg_number_of_Min, neg_number_of_BIT,
- le_number_of_eq_not_less];
+ le_number_of_eq_not_less]);
Addsimps bin_arith_extra_simps;
Addsimps bin_rel_simps;
--- a/src/HOL/Integ/IntDef.ML Thu Jun 22 11:37:13 2000 +0200
+++ b/src/HOL/Integ/IntDef.ML Thu Jun 22 23:04:34 2000 +0200
@@ -61,7 +61,7 @@
addSEs [sym, integ_trans_lemma]) 1);
qed "equiv_intrel";
-val equiv_intrel_iff = [equiv_intrel, UNIV_I, UNIV_I] MRS eq_equiv_class_iff;
+bind_thm ("equiv_intrel_iff", [equiv_intrel, UNIV_I, UNIV_I] MRS eq_equiv_class_iff);
Goalw [Integ_def,intrel_def,quotient_def] "intrel^^{(x,y)}:Integ";
by (Fast_tac 1);
@@ -586,11 +586,11 @@
(*This list of rewrites simplifies (in)equalities by bringing subtractions
to the top and then moving negative terms to the other side.
Use with zadd_ac*)
-val zcompare_rls =
+bind_thms ("zcompare_rls",
[symmetric zdiff_def,
zadd_zdiff_eq, zdiff_zadd_eq, zdiff_zdiff_eq, zdiff_zdiff_eq2,
zdiff_zless_eq, zless_zdiff_eq, zdiff_zle_eq, zle_zdiff_eq,
- zdiff_eq_eq, eq_zdiff_eq];
+ zdiff_eq_eq, eq_zdiff_eq]);
(** Cancellation laws **)
--- a/src/HOL/Integ/IntDiv.ML Thu Jun 22 11:37:13 2000 +0200
+++ b/src/HOL/Integ/IntDiv.ML Thu Jun 22 23:04:34 2000 +0200
@@ -108,7 +108,7 @@
by (Asm_simp_tac 1);
qed "posDivAlg_eqn";
-val posDivAlg_induct = lemma RS posDivAlg.induct;
+bind_thm ("posDivAlg_induct", lemma RS posDivAlg.induct);
(*Correctness of posDivAlg: it computes quotients correctly*)
@@ -146,7 +146,7 @@
by (Asm_simp_tac 1);
qed "negDivAlg_eqn";
-val negDivAlg_induct = lemma RS negDivAlg.induct;
+bind_thm ("negDivAlg_induct", lemma RS negDivAlg.induct);
(*Correctness of negDivAlg: it computes quotients correctly
--- a/src/HOL/Integ/NatBin.ML Thu Jun 22 11:37:13 2000 +0200
+++ b/src/HOL/Integ/NatBin.ML Thu Jun 22 23:04:34 2000 +0200
@@ -345,13 +345,13 @@
Addsimps [inst "n" "number_of ?v" diff_less'];
(*various theorems that aren't in the default simpset*)
-val add_is_one' = rename_numerals thy add_is_1;
-val one_is_add' = rename_numerals thy one_is_add;
-val zero_induct' = rename_numerals thy zero_induct;
-val diff_self_eq_0' = rename_numerals thy diff_self_eq_0;
-val mult_eq_self_implies_10' = rename_numerals thy mult_eq_self_implies_10;
-val le_pred_eq' = rename_numerals thy le_pred_eq;
-val less_pred_eq' = rename_numerals thy less_pred_eq;
+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);
(** Divides **)
@@ -361,10 +361,10 @@
[dvd_1_left, dvd_0_right]);
(*useful?*)
-val mod_self' = rename_numerals thy mod_self;
-val div_self' = rename_numerals thy div_self;
-val div_less' = rename_numerals thy div_less;
-val mod_mult_self_is_zero' = rename_numerals thy mod_mult_self_is_0;
+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);
(** Power **)
@@ -386,9 +386,9 @@
qed "zero_less_power'";
Addsimps [zero_less_power'];
-val binomial_zero = rename_numerals thy binomial_0;
-val binomial_Suc' = rename_numerals thy binomial_Suc;
-val binomial_n_n' = rename_numerals thy binomial_n_n;
+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);
(*binomial_0_Suc doesn't work well on numerals*)
Addsimps (map (rename_numerals thy)
--- a/src/HOL/List.ML Thu Jun 22 11:37:13 2000 +0200
+++ b/src/HOL/List.ML Thu Jun 22 23:04:34 2000 +0200
@@ -32,7 +32,7 @@
by (REPEAT (ares_tac basic_monos 1));
qed "lists_mono";
-val listsE = lists.mk_cases "x#l : lists A";
+bind_thm ("listsE", lists.mk_cases "x#l : lists A");
AddSEs [listsE];
AddSIs lists.intrs;
--- a/src/HOL/Nat.ML Thu Jun 22 11:37:13 2000 +0200
+++ b/src/HOL/Nat.ML Thu Jun 22 23:04:34 2000 +0200
@@ -7,6 +7,8 @@
(** conversion rules for nat_rec **)
val [nat_rec_0, nat_rec_Suc] = nat.recs;
+bind_thm ("nat_rec_0", nat_rec_0);
+bind_thm ("nat_rec_Suc", nat_rec_Suc);
(*These 2 rules ease the use of primitive recursion. NOTE USE OF == *)
val prems = Goal
@@ -20,6 +22,8 @@
qed "def_nat_rec_Suc";
val [nat_case_0, nat_case_Suc] = nat.cases;
+bind_thm ("nat_case_0", nat_case_0);
+bind_thm ("nat_case_Suc", nat_case_Suc);
Goal "n ~= 0 ==> EX m. n = Suc m";
by (case_tac "n" 1);
--- a/src/HOL/NatDef.ML Thu Jun 22 11:37:13 2000 +0200
+++ b/src/HOL/NatDef.ML Thu Jun 22 23:04:34 2000 +0200
@@ -8,7 +8,7 @@
by (REPEAT (ares_tac [monoI, subset_refl, image_mono, Un_mono] 1));
qed "Nat_fun_mono";
-val Nat_unfold = Nat_fun_mono RS (Nat_def RS def_lfp_Tarski);
+bind_thm ("Nat_unfold", Nat_fun_mono RS (Nat_def RS def_lfp_Tarski));
(* Zero is a natural number -- this also justifies the type definition*)
Goal "Zero_Rep: Nat";
@@ -85,7 +85,7 @@
AddIffs [Suc_not_Zero,Zero_not_Suc];
bind_thm ("Suc_neq_Zero", (Suc_not_Zero RS notE));
-val Zero_neq_Suc = sym RS Suc_neq_Zero;
+bind_thm ("Zero_neq_Suc", sym RS Suc_neq_Zero);
(** Injectiveness of Suc **)
@@ -97,7 +97,7 @@
by (etac (inj_Rep_Nat RS injD) 1);
qed "inj_Suc";
-val Suc_inject = inj_Suc RS injD;
+bind_thm ("Suc_inject", inj_Suc RS injD);
Goal "(Suc(m)=Suc(n)) = (m=n)";
by (EVERY1 [rtac iffI, etac Suc_inject, etac arg_cong]);
@@ -339,7 +339,7 @@
by (assume_tac 1);
qed "leD";
-val leE = make_elim leD;
+bind_thm ("leE", make_elim leD);
Goal "(~n<m) = (m<=(n::nat))";
by (blast_tac (claset() addIs [leI] addEs [leE]) 1);
@@ -384,7 +384,7 @@
qed "less_imp_le";
(*For instance, (Suc m < Suc n) = (Suc m <= n) = (m<n) *)
-val le_simps = [less_imp_le, less_Suc_eq_le, Suc_le_eq];
+bind_thms ("le_simps", [less_imp_le, less_Suc_eq_le, Suc_le_eq]);
(** Equivalence of m<=n and m<n | m=n **)
@@ -461,7 +461,7 @@
(*Rewrite (n < Suc m) to (n=m) if ~ n<m or m<=n hold.
Not suitable as default simprules because they often lead to looping*)
-val not_less_simps = [not_less_less_Suc_eq, leD RS not_less_less_Suc_eq];
+bind_thms ("not_less_simps", [not_less_less_Suc_eq, leD RS not_less_less_Suc_eq]);
(** LEAST -- the least number operator **)
--- a/src/HOL/Real/Hyperreal/Filter.ML Thu Jun 22 11:37:13 2000 +0200
+++ b/src/HOL/Real/Hyperreal/Filter.ML Thu Jun 22 23:04:34 2000 +0200
@@ -549,6 +549,6 @@
by (Blast_tac 1);
qed "FreeUltrafilter_ex";
-val FreeUltrafilter_Ex = export FreeUltrafilter_ex;
+bind_thm ("FreeUltrafilter_Ex", export FreeUltrafilter_ex);
Close_locale "UFT";
--- a/src/HOL/Real/Hyperreal/HyperDef.ML Thu Jun 22 11:37:13 2000 +0200
+++ b/src/HOL/Real/Hyperreal/HyperDef.ML Thu Jun 22 23:04:34 2000 +0200
@@ -210,10 +210,10 @@
simpset() addsimps [FreeUltrafilterNat_Nat_set]));
qed "equiv_hyprel";
-val equiv_hyprel_iff =
+bind_thm ("equiv_hyprel_iff",
[TrueI, TrueI] MRS
([CollectI, CollectI] MRS
- (equiv_hyprel RS eq_equiv_class_iff));
+ (equiv_hyprel RS eq_equiv_class_iff)));
Goalw [hypreal_def,hyprel_def,quotient_def] "hyprel^^{x}:hypreal";
by (Blast_tac 1);
@@ -228,7 +228,7 @@
hyprel_iff, hyprel_in_hypreal, Abs_hypreal_inverse];
Addsimps [equiv_hyprel RS eq_equiv_class_iff];
-val eq_hyprelD = equiv_hyprel RSN (2,eq_equiv_class);
+bind_thm ("eq_hyprelD", equiv_hyprel RSN (2,eq_equiv_class));
Goal "inj(Rep_hypreal)";
by (rtac inj_inverseI 1);
@@ -400,8 +400,8 @@
qed "hypreal_add_left_commute";
(* hypreal addition is an AC operator *)
-val hypreal_add_ac = [hypreal_add_assoc,hypreal_add_commute,
- hypreal_add_left_commute];
+bind_thms ("hypreal_add_ac", [hypreal_add_assoc,hypreal_add_commute,
+ hypreal_add_left_commute]);
Goalw [hypreal_zero_def] "(0::hypreal) + z = z";
by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
@@ -560,8 +560,8 @@
rtac (hypreal_mult_commute RS arg_cong) 1]);
(* hypreal multiplication is an AC operator *)
-val hypreal_mult_ac = [hypreal_mult_assoc, hypreal_mult_commute,
- hypreal_mult_left_commute];
+bind_thms ("hypreal_mult_ac", [hypreal_mult_assoc, hypreal_mult_commute,
+ hypreal_mult_left_commute]);
Goalw [hypreal_one_def] "1hr * z = z";
by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
@@ -634,7 +634,7 @@
by (simp_tac (simpset() addsimps [hypreal_mult_commute',hypreal_add_mult_distrib]) 1);
qed "hypreal_add_mult_distrib2";
-val hypreal_mult_simps = [hypreal_mult_1, hypreal_mult_1_right];
+bind_thms ("hypreal_mult_simps", [hypreal_mult_1, hypreal_mult_1_right]);
Addsimps hypreal_mult_simps;
(*** one and zero are distinct ***)
@@ -1002,7 +1002,7 @@
by (assume_tac 1);
qed "hypreal_leD";
-val hypreal_leE = make_elim hypreal_leD;
+bind_thm ("hypreal_leE", make_elim hypreal_leD);
Goal "(~(w < z)) = (z <= (w::hypreal))";
by (fast_tac (claset() addSIs [hypreal_leI,hypreal_leD]) 1);
--- a/src/HOL/Real/Hyperreal/Zorn.ML Thu Jun 22 11:37:13 2000 +0200
+++ b/src/HOL/Real/Hyperreal/Zorn.ML Thu Jun 22 23:04:34 2000 +0200
@@ -14,10 +14,10 @@
qed "Union_lemma0";
(*-- similar to subset_cs in ZF/subset.thy --*)
-val thissubset_SIs =
+bind_thms ("thissubset_SIs",
[subset_refl,Union_least, UN_least, Un_least,
Inter_greatest, Int_greatest,
- Un_upper1, Un_upper2, Int_lower1, Int_lower2];
+ Un_upper1, Un_upper2, Int_lower1, Int_lower2]);
(*A claset for subset reasoning*)
@@ -38,6 +38,9 @@
val [TFin_succI, Pow_TFin_UnionI] = TFin.intrs;
val TFin_UnionI = PowI RS Pow_TFin_UnionI;
+bind_thm ("TFin_succI", TFin_succI);
+bind_thm ("Pow_TFin_UnionI", Pow_TFin_UnionI);
+bind_thm ("TFin_UnionI", TFin_UnionI);
val major::prems = Goal
"[| n : TFin S; \
--- a/src/HOL/Real/PNat.ML Thu Jun 22 11:37:13 2000 +0200
+++ b/src/HOL/Real/PNat.ML Thu Jun 22 23:04:34 2000 +0200
@@ -10,7 +10,7 @@
by (REPEAT (ares_tac [monoI, subset_refl, image_mono, Un_mono] 1));
qed "pnat_fun_mono";
-val pnat_unfold = pnat_fun_mono RS (pnat_def RS def_lfp_Tarski);
+bind_thm ("pnat_unfold", pnat_fun_mono RS (pnat_def RS def_lfp_Tarski));
Goal "1 : pnat";
by (stac pnat_unfold 1);
@@ -144,7 +144,7 @@
AddIffs [pSuc_not_one,one_not_pSuc];
bind_thm ("pSuc_neq_one", (pSuc_not_one RS notE));
-val one_neq_pSuc = sym RS pSuc_neq_one;
+bind_thm ("one_neq_pSuc", pSuc_neq_one RS pSuc_neq_one);
(** Injectiveness of pSuc **)
@@ -156,7 +156,7 @@
by (etac (inj_Rep_pnat RS injD) 1);
qed "inj_pSuc";
-val pSuc_inject = inj_pSuc RS injD;
+bind_thm ("pSuc_inject", inj_pSuc RS injD);
Goal "(pSuc(m)=pSuc(n)) = (m=n)";
by (EVERY1 [rtac iffI, etac pSuc_inject, etac arg_cong]);
@@ -209,7 +209,7 @@
qed "pnat_add_left_commute";
(*Addition is an AC-operator*)
-val pnat_add_ac = [pnat_add_assoc, pnat_add_commute, pnat_add_left_commute];
+bind_thms ("pnat_add_ac", [pnat_add_assoc, pnat_add_commute, pnat_add_left_commute]);
Goalw [pnat_add_def] "((x::pnat) + y = x + z) = (y = z)";
by (auto_tac (claset() addDs [inj_on_Abs_pnat RS inj_onD,
@@ -306,7 +306,7 @@
by (assume_tac 1);
qed "pnat_leD";
-val pnat_leE = make_elim pnat_leD;
+bind_thm ("pnat_leE", make_elim pnat_leD);
Goal "(~ (x::pnat) < y) = (y <= x)";
by (blast_tac (claset() addIs [pnat_leI] addEs [pnat_leE]) 1);
@@ -594,7 +594,7 @@
qed "pnat_mult_1_left";
(*Multiplication is an AC-operator*)
-val pnat_mult_ac = [pnat_mult_assoc, pnat_mult_commute, pnat_mult_left_commute];
+bind_thms ("pnat_mult_ac", [pnat_mult_assoc, pnat_mult_commute, pnat_mult_left_commute]);
Goal "!!i j k::pnat. i<=j ==> i * k <= j * k";
by (asm_full_simp_tac (simpset() addsimps [pnat_le_iff_Rep_pnat_le,
--- a/src/HOL/Real/PRat.ML Thu Jun 22 11:37:13 2000 +0200
+++ b/src/HOL/Real/PRat.ML Thu Jun 22 23:04:34 2000 +0200
@@ -59,7 +59,7 @@
addSEs [sym, prat_trans_lemma]) 1);
qed "equiv_ratrel";
-val equiv_ratrel_iff = [equiv_ratrel, UNIV_I, UNIV_I] MRS eq_equiv_class_iff;
+bind_thm ("equiv_ratrel_iff", [equiv_ratrel, UNIV_I, UNIV_I] MRS eq_equiv_class_iff);
Goalw [prat_def,ratrel_def,quotient_def] "ratrel^^{(x,y)}:prat";
by (Blast_tac 1);
@@ -74,7 +74,7 @@
ratrel_iff, ratrel_in_prat, Abs_prat_inverse];
Addsimps [equiv_ratrel RS eq_equiv_class_iff];
-val eq_ratrelD = equiv_ratrel RSN (2,eq_equiv_class);
+bind_thm ("eq_ratrelD", equiv_ratrel RSN (2,eq_equiv_class));
Goal "inj(Rep_prat)";
by (rtac inj_inverseI 1);
@@ -182,7 +182,7 @@
qed "prat_add_left_commute";
(* Positive Rational addition is an AC operator *)
-val prat_add_ac = [prat_add_assoc, prat_add_commute, prat_add_left_commute];
+bind_thms ("prat_add_ac", [prat_add_assoc, prat_add_commute, prat_add_left_commute]);
(*** Congruence property for multiplication ***)
@@ -228,8 +228,8 @@
qed "prat_mult_left_commute";
(*Positive Rational multiplication is an AC operator*)
-val prat_mult_ac = [prat_mult_assoc,
- prat_mult_commute,prat_mult_left_commute];
+bind_thms ("prat_mult_ac", [prat_mult_assoc,
+ prat_mult_commute,prat_mult_left_commute]);
Goalw [prat_of_pnat_def]
"(prat_of_pnat (Abs_pnat 1)) * z = z";
@@ -572,7 +572,7 @@
by (assume_tac 1);
qed "prat_leD";
-val prat_leE = make_elim prat_leD;
+bind_thm ("prat_leE", make_elim prat_leD);
Goal "(~(w < z)) = (z <= (w::prat))";
by (fast_tac (claset() addSIs [prat_leI,prat_leD]) 1);
--- a/src/HOL/Real/PReal.ML Thu Jun 22 11:37:13 2000 +0200
+++ b/src/HOL/Real/PReal.ML Thu Jun 22 23:04:34 2000 +0200
@@ -281,7 +281,7 @@
rtac (preal_add_commute RS arg_cong) 1]);
(* Positive Reals addition is an AC operator *)
-val preal_add_ac = [preal_add_assoc, preal_add_commute, preal_add_left_commute];
+bind_thms ("preal_add_ac", [preal_add_assoc, preal_add_commute, preal_add_left_commute]);
(*** Properties of multiplication ***)
@@ -367,9 +367,9 @@
rtac (preal_mult_commute RS arg_cong) 1]);
(* Positive Reals multiplication is an AC operator *)
-val preal_mult_ac = [preal_mult_assoc,
+bind_thms ("preal_mult_ac", [preal_mult_assoc,
preal_mult_commute,
- preal_mult_left_commute];
+ preal_mult_left_commute]);
(* Positive Real 1 is the multiplicative identity element *)
(* long *)
@@ -746,7 +746,7 @@
by (auto_tac (claset() addDs [equalityI],simpset()));
qed "preal_leD";
-val preal_leE = make_elim preal_leD;
+bind_thm ("preal_leE", make_elim preal_leD);
Goalw [preal_le_def,psubset_def,preal_less_def]
"~ z <= w ==> w<(z::preal)";
--- a/src/HOL/Real/ROOT.ML Thu Jun 22 11:37:13 2000 +0200
+++ b/src/HOL/Real/ROOT.ML Thu Jun 22 23:04:34 2000 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Real/ROOT
+(* Title: HOL/Real/ROOT.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
@@ -8,5 +8,4 @@
Linear real arithmetic is installed in RealBin.ML.
*)
-time_use_thy "Real";
-time_use_thy "Hyperreal/HyperDef";
+with_path "Hyperreal" use_thy "HyperDef";
--- a/src/HOL/Real/RealBin.ML Thu Jun 22 11:37:13 2000 +0200
+++ b/src/HOL/Real/RealBin.ML Thu Jun 22 23:04:34 2000 +0200
@@ -349,7 +349,7 @@
real_mult_minus_1, real_mult_minus_1_right];
(*To perform binary arithmetic*)
-val bin_simps =
+val bin_simps =
[add_real_number_of, real_add_number_of_left, minus_real_number_of,
diff_real_number_of] @
bin_arith_simps @ bin_rel_simps;
--- a/src/HOL/Real/RealDef.ML Thu Jun 22 11:37:13 2000 +0200
+++ b/src/HOL/Real/RealDef.ML Thu Jun 22 23:04:34 2000 +0200
@@ -56,10 +56,10 @@
addSEs [sym,preal_trans_lemma]) 1);
qed "equiv_realrel";
-val equiv_realrel_iff =
+bind_thm ("equiv_realrel_iff",
[TrueI, TrueI] MRS
([CollectI, CollectI] MRS
- (equiv_realrel RS eq_equiv_class_iff));
+ (equiv_realrel RS eq_equiv_class_iff)));
Goalw [real_def,realrel_def,quotient_def] "realrel^^{(x,y)}:real";
by (Blast_tac 1);
@@ -74,7 +74,7 @@
realrel_iff, realrel_in_real, Abs_real_inverse];
Addsimps [equiv_realrel RS eq_equiv_class_iff];
-val eq_realrelD = equiv_realrel RSN (2,eq_equiv_class);
+bind_thm ("eq_realrelD", equiv_realrel RSN (2,eq_equiv_class));
Goal "inj(Rep_real)";
by (rtac inj_inverseI 1);
@@ -1081,11 +1081,11 @@
(*This list of rewrites simplifies (in)equalities by bringing subtractions
to the top and then moving negative terms to the other side.
Use with real_add_ac*)
-val real_compare_rls =
+bind_thms ("real_compare_rls",
[symmetric real_diff_def,
real_add_diff_eq, real_diff_add_eq, real_diff_diff_eq, real_diff_diff_eq2,
real_diff_less_eq, real_less_diff_eq, real_diff_le_eq, real_le_diff_eq,
- real_diff_eq_eq, real_eq_diff_eq];
+ real_diff_eq_eq, real_eq_diff_eq]);
(** For the cancellation simproc.
--- a/src/HOL/Relation.ML Thu Jun 22 11:37:13 2000 +0200
+++ b/src/HOL/Relation.ML Thu Jun 22 23:04:34 2000 +0200
@@ -45,7 +45,7 @@
by (Blast_tac 1);
qed "diag_eqI";
-val diagI = refl RS diag_eqI |> standard;
+bind_thm ("diagI", refl RS diag_eqI |> standard);
(*The general elimination rule*)
val major::prems = Goalw [diag_def]
--- a/src/HOL/Set.ML Thu Jun 22 11:37:13 2000 +0200
+++ b/src/HOL/Set.ML Thu Jun 22 23:04:34 2000 +0200
@@ -31,7 +31,7 @@
by (rtac (prem RS ext RS arg_cong) 1);
qed "Collect_cong";
-val CollectE = make_elim CollectD;
+bind_thm ("CollectE", make_elim CollectD);
AddSIs [CollectI];
AddSEs [CollectE];
@@ -191,7 +191,7 @@
by (rtac set_ext 1);
by (blast_tac (claset() addIs [subsetD]) 1);
qed "subset_antisym";
-val equalityI = subset_antisym;
+bind_thm ("equalityI", subset_antisym);
AddSIs [equalityI];
@@ -325,8 +325,8 @@
qed "PowD";
-val Pow_bottom = empty_subsetI RS PowI; (* {}: Pow(B) *)
-val Pow_top = subset_refl RS PowI; (* A : Pow(A) *)
+bind_thm ("Pow_bottom", empty_subsetI RS PowI); (* {}: Pow(B) *)
+bind_thm ("Pow_top", subset_refl RS PowI); (* A : Pow(A) *)
section "Set complement";
@@ -348,7 +348,7 @@
by (etac CollectD 1);
qed "ComplD";
-val ComplE = make_elim ComplD;
+bind_thm ("ComplE", make_elim ComplD);
AddSIs [ComplI];
AddSEs [ComplE];
@@ -720,13 +720,13 @@
bind_thm ("split_if_mem2",
read_instantiate_sg (Theory.sign_of Set.thy) [("P", "%x. ?a : x")] split_if);
-val split_ifs = [if_bool_eq_conj, split_if_eq1, split_if_eq2,
- split_if_mem1, split_if_mem2];
+bind_thms ("split_ifs", [if_bool_eq_conj, split_if_eq1, split_if_eq2,
+ split_if_mem1, split_if_mem2]);
(*Each of these has ALREADY been added to simpset() above.*)
-val mem_simps = [insert_iff, empty_iff, Un_iff, Int_iff, Compl_iff, Diff_iff,
- mem_Collect_eq, UN_iff, Union_iff, INT_iff, Inter_iff];
+bind_thms ("mem_simps", [insert_iff, empty_iff, Un_iff, Int_iff, Compl_iff, Diff_iff,
+ mem_Collect_eq, UN_iff, Union_iff, INT_iff, Inter_iff]);
(*Would like to add these, but the existing code only searches for the
outer-level constant, which in this case is just "op :"; we instead need
--- a/src/HOL/Sum.ML Thu Jun 22 11:37:13 2000 +0200
+++ b/src/HOL/Sum.ML Thu Jun 22 23:04:34 2000 +0200
@@ -43,8 +43,7 @@
AddIffs [Inl_not_Inr, Inr_not_Inl];
bind_thm ("Inl_neq_Inr", Inl_not_Inr RS notE);
-
-val Inr_neq_Inl = sym RS Inl_neq_Inr;
+bind_thm ("Inr_neq_Inl", sym RS Inl_neq_Inr);
(** Injectiveness of Inl and Inr **)
@@ -65,7 +64,7 @@
by (rtac Inl_RepI 1);
by (rtac Inl_RepI 1);
qed "inj_Inl";
-val Inl_inject = inj_Inl RS injD;
+bind_thm ("Inl_inject", inj_Inl RS injD);
Goalw [Inr_def] "inj(Inr)";
by (rtac injI 1);
@@ -73,7 +72,7 @@
by (rtac Inr_RepI 1);
by (rtac Inr_RepI 1);
qed "inj_Inr";
-val Inr_inject = inj_Inr RS injD;
+bind_thm ("Inr_inject", inj_Inr RS injD);
Goal "(Inl(x)=Inl(y)) = (x=y)";
by (blast_tac (claset() addSDs [Inl_inject]) 1);
@@ -138,7 +137,7 @@
by (Blast_tac 1);
qed "Part_eqI";
-val PartI = refl RSN (2,Part_eqI);
+bind_thm ("PartI", refl RSN (2,Part_eqI));
val major::prems = Goalw [Part_def]
"[| a : Part A h; !!z. [| a : A; a=h(z) |] ==> P \
--- a/src/HOL/Trancl.ML Thu Jun 22 11:37:13 2000 +0200
+++ b/src/HOL/Trancl.ML Thu Jun 22 23:04:34 2000 +0200
@@ -15,7 +15,7 @@
by (REPEAT (ares_tac [monoI, subset_refl, comp_mono, Un_mono] 1));
qed "rtrancl_fun_mono";
-val rtrancl_unfold = rtrancl_fun_mono RS (rtrancl_def RS def_lfp_Tarski);
+bind_thm ("rtrancl_unfold", rtrancl_fun_mono RS (rtrancl_def RS def_lfp_Tarski));
(*Reflexivity of rtrancl*)
Goal "(a,a) : r^*";
--- a/src/HOL/Univ.ML Thu Jun 22 11:37:13 2000 +0200
+++ b/src/HOL/Univ.ML Thu Jun 22 23:04:34 2000 +0200
@@ -61,7 +61,7 @@
by (etac Abs_Node_inverse 1);
qed "inj_on_Abs_Node";
-val Abs_Node_inject = inj_on_Abs_Node RS inj_onD;
+bind_thm ("Abs_Node_inject", inj_on_Abs_Node RS inj_onD);
(*** Introduction rules for Node ***)
@@ -98,7 +98,7 @@
Goalw [Atom_def] "inj(Atom)";
by (blast_tac (claset() addSIs [injI, Node_K0_I] addSDs [Abs_Node_inject]) 1);
qed "inj_Atom";
-val Atom_inject = inj_Atom RS injD;
+bind_thm ("Atom_inject", inj_Atom RS injD);
Goal "(Atom(a)=Atom(b)) = (a=b)";
by (blast_tac (claset() addSDs [Atom_inject]) 1);
@@ -118,7 +118,7 @@
by (etac (Atom_inject RS Inr_inject) 1);
qed "inj_Numb";
-val Numb_inject = inj_Numb RS injD;
+bind_thm ("Numb_inject", inj_Numb RS injD);
AddSDs [Numb_inject];
(** Injectiveness of Push_Node **)
@@ -586,7 +586,7 @@
by (Blast_tac 1);
qed "dprod_Sigma";
-val dprod_subset_Sigma = [dprod_mono, dprod_Sigma] MRS subset_trans |>standard;
+bind_thm ("dprod_subset_Sigma", [dprod_mono, dprod_Sigma] MRS subset_trans |> standard);
(*Dependent version*)
Goal "(dprod (Sigma A B) (Sigma C D)) <= Sigma (uprod A C) (Split (%x y. uprod (B x) (D y)))";
@@ -599,7 +599,7 @@
by (Blast_tac 1);
qed "dsum_Sigma";
-val dsum_subset_Sigma = [dsum_mono, dsum_Sigma] MRS subset_trans |> standard;
+bind_thm ("dsum_subset_Sigma", [dsum_mono, dsum_Sigma] MRS subset_trans |> standard);
(*** Domain ***)
--- a/src/HOL/WF.ML Thu Jun 22 11:37:13 2000 +0200
+++ b/src/HOL/WF.ML Thu Jun 22 23:04:34 2000 +0200
@@ -68,6 +68,8 @@
"!!X. wf (r^-1) ==> wf ((r^+)^-1)" (K [
stac (trancl_converse RS sym) 1,
etac wf_trancl 1]);
+bind_thm ("wf_converse_trancl", wf_converse_trancl);
+
(*----------------------------------------------------------------------------
* Minimal-element characterization of well-foundedness
--- a/src/HOL/WF_Rel.ML Thu Jun 22 11:37:13 2000 +0200
+++ b/src/HOL/WF_Rel.ML Thu Jun 22 23:04:34 2000 +0200
@@ -66,7 +66,7 @@
val measure_induct = standard
(asm_full_simplify (simpset() addsimps [measure_def,inv_image_def])
(wf_measure RS wf_induct));
-store_thm("measure_induct",measure_induct);
+bind_thm ("measure_induct", measure_induct);
(*----------------------------------------------------------------------------
* Wellfoundedness of lexicographic combinations