# HG changeset patch # User wenzelm # Date 961707874 -7200 # Node ID 9fff97d298374ddb92a68130cfd4e58316c21c19 # Parent 67202a50ee6d21fc2daadf4f5dd06a4c33b25017 bind_thm(s); diff -r 67202a50ee6d -r 9fff97d29837 src/HOL/Datatype.ML --- 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, diff -r 67202a50ee6d -r 9fff97d29837 src/HOL/Divides.ML --- 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 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 ***) diff -r 67202a50ee6d -r 9fff97d29837 src/HOL/Integ/Bin.ML --- 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; diff -r 67202a50ee6d -r 9fff97d29837 src/HOL/Integ/IntDef.ML --- 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 **) diff -r 67202a50ee6d -r 9fff97d29837 src/HOL/Integ/IntDiv.ML --- 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 diff -r 67202a50ee6d -r 9fff97d29837 src/HOL/Integ/NatBin.ML --- 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) diff -r 67202a50ee6d -r 9fff97d29837 src/HOL/List.ML --- 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; diff -r 67202a50ee6d -r 9fff97d29837 src/HOL/Nat.ML --- 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); diff -r 67202a50ee6d -r 9fff97d29837 src/HOL/NatDef.ML --- 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 i * k <= j * k"; by (asm_full_simp_tac (simpset() addsimps [pnat_le_iff_Rep_pnat_le, diff -r 67202a50ee6d -r 9fff97d29837 src/HOL/Real/PRat.ML --- 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); diff -r 67202a50ee6d -r 9fff97d29837 src/HOL/Real/PReal.ML --- 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)"; diff -r 67202a50ee6d -r 9fff97d29837 src/HOL/Real/ROOT.ML --- 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"; diff -r 67202a50ee6d -r 9fff97d29837 src/HOL/Real/RealBin.ML --- 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; diff -r 67202a50ee6d -r 9fff97d29837 src/HOL/Real/RealDef.ML --- 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. diff -r 67202a50ee6d -r 9fff97d29837 src/HOL/Relation.ML --- 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] diff -r 67202a50ee6d -r 9fff97d29837 src/HOL/Set.ML --- 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 diff -r 67202a50ee6d -r 9fff97d29837 src/HOL/Sum.ML --- 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 \ diff -r 67202a50ee6d -r 9fff97d29837 src/HOL/Trancl.ML --- 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^*"; diff -r 67202a50ee6d -r 9fff97d29837 src/HOL/Univ.ML --- 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 ***) diff -r 67202a50ee6d -r 9fff97d29837 src/HOL/WF.ML --- 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 diff -r 67202a50ee6d -r 9fff97d29837 src/HOL/WF_Rel.ML --- 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