--- a/src/HOL/Integ/int_arith1.ML Thu Mar 29 11:59:54 2007 +0200
+++ b/src/HOL/Integ/int_arith1.ML Thu Mar 29 14:21:45 2007 +0200
@@ -280,19 +280,19 @@
pred_1, pred_0, pred_Pls, pred_Min];
(*To let us treat subtraction as addition*)
-val diff_simps = [diff_minus, minus_add_distrib, minus_minus];
+val diff_simps = [@{thm diff_minus}, @{thm minus_add_distrib}, @{thm minus_minus}];
(*push the unary minus down: - x * y = x * - y *)
val minus_mult_eq_1_to_2 =
- [minus_mult_left RS sym, minus_mult_right] MRS trans |> standard;
+ [@{thm minus_mult_left} RS sym, @{thm minus_mult_right}] MRS trans |> standard;
(*to extract again any uncancelled minuses*)
val minus_from_mult_simps =
- [minus_minus, minus_mult_left RS sym, minus_mult_right RS sym];
+ [@{thm minus_minus}, @{thm minus_mult_left} RS sym, @{thm minus_mult_right} RS sym];
(*combine unary minus with numeric literals, however nested within a product*)
val mult_minus_simps =
- [mult_assoc, minus_mult_left, minus_mult_eq_1_to_2];
+ [@{thm mult_assoc}, @{thm minus_mult_left}, minus_mult_eq_1_to_2];
(*Apply the given rewrite (if present) just once*)
fun trans_tac NONE = all_tac
@@ -495,26 +495,26 @@
(* reduce contradictory <= to False *)
val add_rules =
simp_thms @ arith_simps @ rel_simps @ arith_special @
- [neg_le_iff_le, numeral_0_eq_0, numeral_1_eq_1,
- minus_zero, diff_minus, left_minus, right_minus,
- mult_zero_left, mult_zero_right, mult_num1, mult_1_right,
- minus_mult_left RS sym, minus_mult_right RS sym,
- minus_add_distrib, minus_minus, mult_assoc,
+ [@{thm neg_le_iff_le}, @{thm numeral_0_eq_0}, @{thm numeral_1_eq_1},
+ @{thm minus_zero}, @{thm diff_minus}, @{thm left_minus}, @{thm right_minus},
+ @{thm mult_zero_left}, @{thm mult_zero_right}, @{thm mult_num1}, @{thm mult_1_right},
+ @{thm minus_mult_left} RS sym, @{thm minus_mult_right} RS sym,
+ @{thm minus_add_distrib}, @{thm minus_minus}, @{thm mult_assoc},
of_nat_0, of_nat_1, of_nat_Suc, of_nat_add, of_nat_mult,
of_int_0, of_int_1, of_int_add, of_int_mult, int_eq_of_nat]
-val nat_inj_thms = [zle_int RS iffD2,
- int_int_eq RS iffD2]
+val nat_inj_thms = [zle_int RS iffD2, int_int_eq RS iffD2]
-val Int_Numeral_Base_Simprocs = [assoc_fold_simproc, Int_Numeral_Simprocs.combine_numerals]@
- Int_Numeral_Simprocs.cancel_numerals
+val Int_Numeral_Base_Simprocs = assoc_fold_simproc
+ :: Int_Numeral_Simprocs.combine_numerals
+ :: Int_Numeral_Simprocs.cancel_numerals;
in
val int_arith_setup =
Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
{add_mono_thms = add_mono_thms,
- mult_mono_thms = [mult_strict_left_mono,mult_left_mono] @ mult_mono_thms,
+ mult_mono_thms = @{thm mult_strict_left_mono} :: @{thm mult_left_mono} :: mult_mono_thms,
inj_thms = nat_inj_thms @ inj_thms,
lessD = lessD @ [zless_imp_add1_zle],
neqE = neqE,
@@ -528,45 +528,10 @@
end;
val fast_int_arith_simproc =
- Simplifier.simproc (Theory.sign_of (the_context()))
+ Simplifier.simproc @{theory}
"fast_int_arith"
["(m::'a::{ordered_idom,number_ring}) < n",
"(m::'a::{ordered_idom,number_ring}) <= n",
"(m::'a::{ordered_idom,number_ring}) = n"] Fast_Arith.lin_arith_prover;
Addsimprocs [fast_int_arith_simproc];
-
-
-(* Some test data
-Goal "!!a::int. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d";
-by (fast_arith_tac 1);
-Goal "!!a::int. [| a < b; c < d |] ==> a-d+ 2 <= b+(-c)";
-by (fast_arith_tac 1);
-Goal "!!a::int. [| a < b; c < d |] ==> a+c+ 1 < b+d";
-by (fast_arith_tac 1);
-Goal "!!a::int. [| a <= b; b+b <= c |] ==> a+a <= c";
-by (fast_arith_tac 1);
-Goal "!!a::int. [| a+b <= i+j; a<=b; i<=j |] \
-\ ==> a+a <= j+j";
-by (fast_arith_tac 1);
-Goal "!!a::int. [| a+b < i+j; a<b; i<j |] \
-\ ==> a+a - - -1 < j+j - 3";
-by (fast_arith_tac 1);
-Goal "!!a::int. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k";
-by (arith_tac 1);
-Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
-\ ==> a <= l";
-by (fast_arith_tac 1);
-Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
-\ ==> a+a+a+a <= l+l+l+l";
-by (fast_arith_tac 1);
-Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
-\ ==> a+a+a+a+a <= l+l+l+l+i";
-by (fast_arith_tac 1);
-Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
-\ ==> a+a+a+a+a+a <= l+l+l+l+i+l";
-by (fast_arith_tac 1);
-Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
-\ ==> 6*a <= 5*l+i";
-by (fast_arith_tac 1);
-*)
--- a/src/HOL/Integ/int_factor_simprocs.ML Thu Mar 29 11:59:54 2007 +0200
+++ b/src/HOL/Integ/int_factor_simprocs.ML Thu Mar 29 14:21:45 2007 +0200
@@ -54,10 +54,9 @@
val numeral_simp_ss = HOL_ss addsimps rel_number_of @ simps
fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
- val simplify_meta_eq =
- Int_Numeral_Simprocs.simplify_meta_eq
- [add_0, add_0_right,
- mult_zero_left, mult_zero_right, mult_num1, mult_1_right];
+ val simplify_meta_eq = Int_Numeral_Simprocs.simplify_meta_eq
+ [@{thm add_0}, @{thm add_0_right}, @{thm mult_zero_left},
+ @{thm mult_zero_right}, @{thm mult_num1}, @{thm mult_1_right}];
end
(*Version for integer division*)
@@ -76,7 +75,7 @@
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binop "HOL.divide"
val dest_bal = HOLogic.dest_bin "HOL.divide" Term.dummyT
- val cancel = mult_divide_cancel_left RS trans
+ val cancel = @{thm mult_divide_cancel_left} RS trans
val neg_exchanges = false
)
@@ -86,7 +85,7 @@
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
val mk_bal = HOLogic.mk_eq
val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
- val cancel = mult_cancel_left RS trans
+ val cancel = @{thm mult_cancel_left} RS trans
val neg_exchanges = false
)
@@ -96,7 +95,7 @@
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
val mk_bal = HOLogic.mk_eq
val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
- val cancel = field_mult_cancel_left RS trans
+ val cancel = @{thm field_mult_cancel_left} RS trans
val neg_exchanges = false
)
@@ -105,7 +104,7 @@
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binrel "Orderings.less"
val dest_bal = HOLogic.dest_bin "Orderings.less" Term.dummyT
- val cancel = mult_less_cancel_left RS trans
+ val cancel = @{thm mult_less_cancel_left} RS trans
val neg_exchanges = true
)
@@ -114,7 +113,7 @@
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binrel "Orderings.less_eq"
val dest_bal = HOLogic.dest_bin "Orderings.less_eq" Term.dummyT
- val cancel = mult_le_cancel_left RS trans
+ val cancel = @{thm mult_le_cancel_left} RS trans
val neg_exchanges = true
)
@@ -236,9 +235,8 @@
handle TERM _ => find_first_t (t::past) u terms;
(** Final simplification for the CancelFactor simprocs **)
-val simplify_one =
- Int_Numeral_Simprocs.simplify_meta_eq
- [mult_1_left, mult_1_right, zdiv_1, numeral_1_eq_1];
+val simplify_one = Int_Numeral_Simprocs.simplify_meta_eq
+ [@{thm mult_1_left}, mult_1_right, zdiv_1, numeral_1_eq_1];
fun cancel_simplify_meta_eq cancel_th ss th =
simplify_one ss (([th, cancel_th]) MRS trans);
@@ -264,7 +262,7 @@
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
val mk_bal = HOLogic.mk_eq
val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT
- val simplify_meta_eq = cancel_simplify_meta_eq mult_cancel_left
+ val simplify_meta_eq = cancel_simplify_meta_eq @{thm mult_cancel_left}
);
(*int_mult_div_cancel_disj is for integer division (div). The version in
@@ -291,7 +289,7 @@
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
val mk_bal = HOLogic.mk_eq
val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
- val simplify_meta_eq = cancel_simplify_meta_eq field_mult_cancel_left
+ val simplify_meta_eq = cancel_simplify_meta_eq @{thm field_mult_cancel_left}
);
structure FieldDivideCancelFactor = ExtractCommonTermFun
@@ -299,7 +297,7 @@
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binop "HOL.divide"
val dest_bal = HOLogic.dest_bin "HOL.divide" Term.dummyT
- val simplify_meta_eq = cancel_simplify_meta_eq mult_divide_cancel_eq_if
+ val simplify_meta_eq = cancel_simplify_meta_eq @{thm mult_divide_cancel_eq_if}
);
(*The number_ring class is necessary because the simprocs refer to the
--- a/src/HOL/Integ/nat_simprocs.ML Thu Mar 29 11:59:54 2007 +0200
+++ b/src/HOL/Integ/nat_simprocs.ML Thu Mar 29 14:21:45 2007 +0200
@@ -351,9 +351,8 @@
handle TERM _ => find_first_t (t::past) u terms;
(** Final simplification for the CancelFactor simprocs **)
-val simplify_one =
- Int_Numeral_Simprocs.simplify_meta_eq
- [mult_1_left, mult_1_right, div_1, numeral_1_eq_Suc_0];
+val simplify_one = Int_Numeral_Simprocs.simplify_meta_eq
+ [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_1}, @{thm numeral_1_eq_Suc_0}];
fun cancel_simplify_meta_eq cancel_th ss th =
simplify_one ss (([th, cancel_th]) MRS trans);
@@ -538,8 +537,8 @@
eq_number_of_0, eq_0_number_of, less_0_number_of,
of_int_number_of_eq, of_nat_number_of_eq, nat_number_of, if_True, if_False];
-val simprocs = [Nat_Numeral_Simprocs.combine_numerals]@
- Nat_Numeral_Simprocs.cancel_numerals;
+val simprocs = Nat_Numeral_Simprocs.combine_numerals
+ :: Nat_Numeral_Simprocs.cancel_numerals;
in
--- a/src/HOL/Integ/presburger.ML Thu Mar 29 11:59:54 2007 +0200
+++ b/src/HOL/Integ/presburger.ML Thu Mar 29 14:21:45 2007 +0200
@@ -301,9 +301,9 @@
addsimps add_ac
addsimprocs [cancel_div_mod_proc]
val simpset0 = HOL_basic_ss
- addsimps [mod_div_equality', Suc_plus1]
+ addsimps [@{thm mod_div_equality'}, @{thm Suc_plus1}]
addsimps comp_arith
- addsplits [split_zdiv, split_zmod, split_div', split_min, split_max]
+ addsplits [split_zdiv, split_zmod, split_div', @{thm split_min}, @{thm split_max}]
(* Simp rules for changing (n::int) to int n *)
val simpset1 = HOL_basic_ss
addsimps [nat_number_of_def, zdvd_int] @ map (fn r => r RS sym)
--- a/src/HOL/Lattices.thy Thu Mar 29 11:59:54 2007 +0200
+++ b/src/HOL/Lattices.thy Thu Mar 29 14:21:45 2007 +0200
@@ -327,30 +327,4 @@
lemmas inf_aci = inf_ACI
lemmas sup_aci = sup_ACI
-
-text {* ML legacy bindings *}
-
-ML {*
-val Least_def = @{thm Least_def}
-val Least_equality = @{thm Least_equality}
-val min_def = @{thm min_def}
-val min_of_mono = @{thm min_of_mono}
-val max_def = @{thm max_def}
-val max_of_mono = @{thm max_of_mono}
-val min_leastL = @{thm min_leastL}
-val max_leastL = @{thm max_leastL}
-val min_leastR = @{thm min_leastR}
-val max_leastR = @{thm max_leastR}
-val le_max_iff_disj = @{thm le_max_iff_disj}
-val le_maxI1 = @{thm le_maxI1}
-val le_maxI2 = @{thm le_maxI2}
-val less_max_iff_disj = @{thm less_max_iff_disj}
-val max_less_iff_conj = @{thm max_less_iff_conj}
-val min_less_iff_conj = @{thm min_less_iff_conj}
-val min_le_iff_disj = @{thm min_le_iff_disj}
-val min_less_iff_disj = @{thm min_less_iff_disj}
-val split_min = @{thm split_min}
-val split_max = @{thm split_max}
-*}
-
end
--- a/src/HOL/OrderedGroup.thy Thu Mar 29 11:59:54 2007 +0200
+++ b/src/HOL/OrderedGroup.thy Thu Mar 29 14:21:45 2007 +0200
@@ -1088,13 +1088,13 @@
@{thm right_minus}, @{thm left_minus}, @{thm add_minus_cancel},
@{thm minus_add_cancel}];
-val eq_reflection = @{thm eq_reflection}
+val eq_reflection = @{thm eq_reflection};
-val thy_ref = Theory.self_ref @{theory}
+val thy_ref = Theory.self_ref @{theory};
-val T = TFree("'a", ["OrderedGroup.ab_group_add"])
+val T = TFree("'a", ["OrderedGroup.ab_group_add"]);
-val eqI_rules = [@{thm less_eqI}, @{thm le_eqI}, @{thm eq_eqI}]
+val eqI_rules = [@{thm less_eqI}, @{thm le_eqI}, @{thm eq_eqI}];
val dest_eqI =
fst o HOLogic.dest_bin "op =" HOLogic.boolT o HOLogic.dest_Trueprop o concl_of;
@@ -1106,140 +1106,4 @@
Addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv];
*}
-ML {*
-val add_assoc = thm "add_assoc";
-val add_commute = thm "add_commute";
-val add_left_commute = thm "add_left_commute";
-val add_ac = thms "add_ac";
-val mult_assoc = thm "mult_assoc";
-val mult_commute = thm "mult_commute";
-val mult_left_commute = thm "mult_left_commute";
-val mult_ac = thms "mult_ac";
-val add_0 = thm "add_0";
-val mult_1_left = thm "mult_1_left";
-val mult_1_right = thm "mult_1_right";
-val mult_1 = thm "mult_1";
-val add_left_imp_eq = thm "add_left_imp_eq";
-val add_right_imp_eq = thm "add_right_imp_eq";
-val add_imp_eq = thm "add_imp_eq";
-val left_minus = thm "left_minus";
-val diff_minus = thm "diff_minus";
-val add_0_right = thm "add_0_right";
-val add_left_cancel = thm "add_left_cancel";
-val add_right_cancel = thm "add_right_cancel";
-val right_minus = thm "right_minus";
-val right_minus_eq = thm "right_minus_eq";
-val minus_minus = thm "minus_minus";
-val equals_zero_I = thm "equals_zero_I";
-val minus_zero = thm "minus_zero";
-val diff_self = thm "diff_self";
-val diff_0 = thm "diff_0";
-val diff_0_right = thm "diff_0_right";
-val diff_minus_eq_add = thm "diff_minus_eq_add";
-val neg_equal_iff_equal = thm "neg_equal_iff_equal";
-val neg_equal_0_iff_equal = thm "neg_equal_0_iff_equal";
-val neg_0_equal_iff_equal = thm "neg_0_equal_iff_equal";
-val equation_minus_iff = thm "equation_minus_iff";
-val minus_equation_iff = thm "minus_equation_iff";
-val minus_add_distrib = thm "minus_add_distrib";
-val minus_diff_eq = thm "minus_diff_eq";
-val add_left_mono = thm "add_left_mono";
-val add_le_imp_le_left = thm "add_le_imp_le_left";
-val add_right_mono = thm "add_right_mono";
-val add_mono = thm "add_mono";
-val add_strict_left_mono = thm "add_strict_left_mono";
-val add_strict_right_mono = thm "add_strict_right_mono";
-val add_strict_mono = thm "add_strict_mono";
-val add_less_le_mono = thm "add_less_le_mono";
-val add_le_less_mono = thm "add_le_less_mono";
-val add_less_imp_less_left = thm "add_less_imp_less_left";
-val add_less_imp_less_right = thm "add_less_imp_less_right";
-val add_less_cancel_left = thm "add_less_cancel_left";
-val add_less_cancel_right = thm "add_less_cancel_right";
-val add_le_cancel_left = thm "add_le_cancel_left";
-val add_le_cancel_right = thm "add_le_cancel_right";
-val add_le_imp_le_right = thm "add_le_imp_le_right";
-val add_increasing = thm "add_increasing";
-val le_imp_neg_le = thm "le_imp_neg_le";
-val neg_le_iff_le = thm "neg_le_iff_le";
-val neg_le_0_iff_le = thm "neg_le_0_iff_le";
-val neg_0_le_iff_le = thm "neg_0_le_iff_le";
-val neg_less_iff_less = thm "neg_less_iff_less";
-val neg_less_0_iff_less = thm "neg_less_0_iff_less";
-val neg_0_less_iff_less = thm "neg_0_less_iff_less";
-val less_minus_iff = thm "less_minus_iff";
-val minus_less_iff = thm "minus_less_iff";
-val le_minus_iff = thm "le_minus_iff";
-val minus_le_iff = thm "minus_le_iff";
-val add_diff_eq = thm "add_diff_eq";
-val diff_add_eq = thm "diff_add_eq";
-val diff_eq_eq = thm "diff_eq_eq";
-val eq_diff_eq = thm "eq_diff_eq";
-val diff_diff_eq = thm "diff_diff_eq";
-val diff_diff_eq2 = thm "diff_diff_eq2";
-val diff_add_cancel = thm "diff_add_cancel";
-val add_diff_cancel = thm "add_diff_cancel";
-val less_iff_diff_less_0 = thm "less_iff_diff_less_0";
-val diff_less_eq = thm "diff_less_eq";
-val less_diff_eq = thm "less_diff_eq";
-val diff_le_eq = thm "diff_le_eq";
-val le_diff_eq = thm "le_diff_eq";
-val compare_rls = thms "compare_rls";
-val eq_iff_diff_eq_0 = thm "eq_iff_diff_eq_0";
-val le_iff_diff_le_0 = thm "le_iff_diff_le_0";
-val add_inf_distrib_left = thm "add_inf_distrib_left";
-val add_sup_distrib_left = thm "add_sup_distrib_left";
-val add_sup_distrib_right = thm "add_sup_distrib_right";
-val add_inf_distrib_right = thm "add_inf_distrib_right";
-val add_sup_inf_distribs = thms "add_sup_inf_distribs";
-val sup_eq_neg_inf = thm "sup_eq_neg_inf";
-val inf_eq_neg_sup = thm "inf_eq_neg_sup";
-val add_eq_inf_sup = thm "add_eq_inf_sup";
-val prts = thm "prts";
-val zero_le_pprt = thm "zero_le_pprt";
-val nprt_le_zero = thm "nprt_le_zero";
-val le_eq_neg = thm "le_eq_neg";
-val sup_0_imp_0 = thm "sup_0_imp_0";
-val inf_0_imp_0 = thm "inf_0_imp_0";
-val sup_0_eq_0 = thm "sup_0_eq_0";
-val inf_0_eq_0 = thm "inf_0_eq_0";
-val zero_le_double_add_iff_zero_le_single_add = thm "zero_le_double_add_iff_zero_le_single_add";
-val double_add_le_zero_iff_single_add_le_zero = thm "double_add_le_zero_iff_single_add_le_zero";
-val double_add_less_zero_iff_single_less_zero = thm "double_add_less_zero_iff_single_less_zero";
-val abs_lattice = thm "abs_lattice";
-val abs_zero = thm "abs_zero";
-val abs_eq_0 = thm "abs_eq_0";
-val abs_0_eq = thm "abs_0_eq";
-val neg_inf_eq_sup = thm "neg_inf_eq_sup";
-val neg_sup_eq_inf = thm "neg_sup_eq_inf";
-val sup_eq_if = thm "sup_eq_if";
-val abs_if_lattice = thm "abs_if_lattice";
-val abs_ge_zero = thm "abs_ge_zero";
-val abs_le_zero_iff = thm "abs_le_zero_iff";
-val zero_less_abs_iff = thm "zero_less_abs_iff";
-val abs_not_less_zero = thm "abs_not_less_zero";
-val abs_ge_self = thm "abs_ge_self";
-val abs_ge_minus_self = thm "abs_ge_minus_self";
-val le_imp_join_eq = thm "sup_absorb2";
-val ge_imp_join_eq = thm "sup_absorb1";
-val le_imp_meet_eq = thm "inf_absorb1";
-val ge_imp_meet_eq = thm "inf_absorb2";
-val abs_prts = thm "abs_prts";
-val abs_minus_cancel = thm "abs_minus_cancel";
-val abs_idempotent = thm "abs_idempotent";
-val zero_le_iff_zero_nprt = thm "zero_le_iff_zero_nprt";
-val le_zero_iff_zero_pprt = thm "le_zero_iff_zero_pprt";
-val le_zero_iff_pprt_id = thm "le_zero_iff_pprt_id";
-val zero_le_iff_nprt_id = thm "zero_le_iff_nprt_id";
-val iff2imp = thm "iff2imp";
-val abs_leI = thm "abs_leI";
-val le_minus_self_iff = thm "le_minus_self_iff";
-val minus_le_self_iff = thm "minus_le_self_iff";
-val abs_le_D1 = thm "abs_le_D1";
-val abs_le_D2 = thm "abs_le_D2";
-val abs_le_iff = thm "abs_le_iff";
-val abs_triangle_ineq = thm "abs_triangle_ineq";
-val abs_diff_triangle_ineq = thm "abs_diff_triangle_ineq";
-*}
-
end
--- a/src/HOL/Orderings.thy Thu Mar 29 11:59:54 2007 +0200
+++ b/src/HOL/Orderings.thy Thu Mar 29 14:21:45 2007 +0200
@@ -901,26 +901,12 @@
"(!!x y. (f x <= f y) = (x <= y)) ==> max (f m) (f n) = f (max m n)"
by (simp add: max_def)
-subsection {* Basic ML bindings *}
+
+subsection {* legacy ML bindings *}
ML {*
-val leD = thm "leD";
-val leI = thm "leI";
-val linorder_neqE = thm "linorder_neqE";
-val linorder_neq_iff = thm "linorder_neq_iff";
-val linorder_not_le = thm "linorder_not_le";
-val linorder_not_less = thm "linorder_not_less";
-val monoD = thm "monoD";
-val monoI = thm "monoI";
-val order_antisym = thm "order_antisym";
-val order_less_irrefl = thm "order_less_irrefl";
-val order_refl = thm "order_refl";
-val order_trans = thm "order_trans";
-val split_max = thm "split_max";
-val split_min = thm "split_min";
-*}
+val monoI = @{thm monoI};
-ML {*
structure HOL =
struct
val thy = theory "HOL";
--- a/src/HOL/Real/ferrante_rackoff.ML Thu Mar 29 11:59:54 2007 +0200
+++ b/src/HOL/Real/ferrante_rackoff.ML Thu Mar 29 14:21:45 2007 +0200
@@ -72,7 +72,7 @@
val context_ss = simpset_of (the_context ());
fun ferrack_tac q i = ObjectLogic.atomize_tac i
- THEN REPEAT_DETERM (split_tac [split_min, split_max,abs_split] i)
+ THEN REPEAT_DETERM (split_tac [@{thm split_min}, @{thm split_max}, abs_split] i)
THEN (fn st =>
let
val g = nth (prems_of st) (i - 1)
@@ -80,7 +80,7 @@
(* Transform the term*)
val (t,np,nh) = prepare_for_linr q g
(* Some simpsets for dealing with mod div abs and nat*)
- val simpset0 = HOL_basic_ss addsimps comp_arith addsplits [split_min, split_max]
+ val simpset0 = HOL_basic_ss addsimps comp_arith addsplits [@{thm split_min}, @{thm split_max}]
(* simp rules for elimination of abs *)
val simpset3 = HOL_basic_ss addsplits [abs_split]
val ct = cterm_of thy (HOLogic.mk_Trueprop t)
--- a/src/HOL/Real/ferrante_rackoff_proof.ML Thu Mar 29 11:59:54 2007 +0200
+++ b/src/HOL/Real/ferrante_rackoff_proof.ML Thu Mar 29 14:21:45 2007 +0200
@@ -319,7 +319,7 @@
val ncmul_congh = thm "ncmul_congh";
val ncmul_cong = thm "ncmul_cong";
fun decomp_ncmulh thy c t =
- if c = 0 then ([],fn _ => instantiate' [SOME crT] [SOME (cterm_of thy t)] mult_zero_left) else
+ if c = 0 then ([],fn _ => instantiate' [SOME crT] [SOME (cterm_of thy t)] @{thm mult_zero_left}) else
case t of
Const("HOL.plus",_)$(Const("HOL.times",_)$c'$v)$b =>
([b],FWD (instantiate' [] [NONE, NONE, SOME (cterm_of thy v)]
--- a/src/HOL/Real/rat_arith.ML Thu Mar 29 11:59:54 2007 +0200
+++ b/src/HOL/Real/rat_arith.ML Thu Mar 29 14:21:45 2007 +0200
@@ -12,11 +12,11 @@
val simprocs = field_cancel_numeral_factors
-val simps = [order_less_irrefl, neg_less_iff_less, True_implies_equals,
- inst "a" "(number_of ?v)" right_distrib,
- divide_1, divide_zero_left,
- times_divide_eq_right, times_divide_eq_left,
- minus_divide_left RS sym, minus_divide_right RS sym,
+val simps = [@{thm order_less_irrefl}, @{thm neg_less_iff_less}, @{thm True_implies_equals},
+ inst "a" "(number_of ?v)" @{thm right_distrib},
+ @{thm divide_1}, @{thm divide_zero_left},
+ @{thm times_divide_eq_right}, @{thm times_divide_eq_left},
+ @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym,
of_int_0, of_int_1, of_int_add, of_int_minus, of_int_diff,
of_int_mult, of_int_of_nat_eq]
@@ -32,10 +32,9 @@
in
-val fast_rat_arith_simproc =
- Simplifier.simproc (the_context ())
+val fast_rat_arith_simproc = Simplifier.simproc @{theory}
"fast_rat_arith" ["(m::rat) < n","(m::rat) <= n", "(m::rat) = n"]
- Fast_Arith.lin_arith_prover
+ Fast_Arith.lin_arith_prover
val ratT = Type ("Rational.rat", [])
--- a/src/HOL/Ring_and_Field.thy Thu Mar 29 11:59:54 2007 +0200
+++ b/src/HOL/Ring_and_Field.thy Thu Mar 29 14:21:45 2007 +0200
@@ -2067,210 +2067,4 @@
then show ?thesis by simp
qed
-ML {*
-val left_distrib = thm "left_distrib";
-val right_distrib = thm "right_distrib";
-val mult_commute = thm "mult_commute";
-val distrib = thm "distrib";
-val zero_neq_one = thm "zero_neq_one";
-val no_zero_divisors = thm "no_zero_divisors";
-val left_inverse = thm "left_inverse";
-val divide_inverse = thm "divide_inverse";
-val mult_zero_left = thm "mult_zero_left";
-val mult_zero_right = thm "mult_zero_right";
-val field_mult_eq_0_iff = thm "field_mult_eq_0_iff";
-val inverse_zero = thm "inverse_zero";
-val ring_distrib = thms "ring_distrib";
-val combine_common_factor = thm "combine_common_factor";
-val minus_mult_left = thm "minus_mult_left";
-val minus_mult_right = thm "minus_mult_right";
-val minus_mult_minus = thm "minus_mult_minus";
-val minus_mult_commute = thm "minus_mult_commute";
-val right_diff_distrib = thm "right_diff_distrib";
-val left_diff_distrib = thm "left_diff_distrib";
-val mult_left_mono = thm "mult_left_mono";
-val mult_right_mono = thm "mult_right_mono";
-val mult_strict_left_mono = thm "mult_strict_left_mono";
-val mult_strict_right_mono = thm "mult_strict_right_mono";
-val mult_mono = thm "mult_mono";
-val mult_strict_mono = thm "mult_strict_mono";
-val abs_if = thm "abs_if";
-val zero_less_one = thm "zero_less_one";
-val eq_add_iff1 = thm "eq_add_iff1";
-val eq_add_iff2 = thm "eq_add_iff2";
-val less_add_iff1 = thm "less_add_iff1";
-val less_add_iff2 = thm "less_add_iff2";
-val le_add_iff1 = thm "le_add_iff1";
-val le_add_iff2 = thm "le_add_iff2";
-val mult_left_le_imp_le = thm "mult_left_le_imp_le";
-val mult_right_le_imp_le = thm "mult_right_le_imp_le";
-val mult_left_less_imp_less = thm "mult_left_less_imp_less";
-val mult_right_less_imp_less = thm "mult_right_less_imp_less";
-val mult_strict_left_mono_neg = thm "mult_strict_left_mono_neg";
-val mult_left_mono_neg = thm "mult_left_mono_neg";
-val mult_strict_right_mono_neg = thm "mult_strict_right_mono_neg";
-val mult_right_mono_neg = thm "mult_right_mono_neg";
-(*
-val mult_pos = thm "mult_pos";
-val mult_pos_le = thm "mult_pos_le";
-val mult_pos_neg = thm "mult_pos_neg";
-val mult_pos_neg_le = thm "mult_pos_neg_le";
-val mult_pos_neg2 = thm "mult_pos_neg2";
-val mult_pos_neg2_le = thm "mult_pos_neg2_le";
-val mult_neg = thm "mult_neg";
-val mult_neg_le = thm "mult_neg_le";
-*)
-val zero_less_mult_pos = thm "zero_less_mult_pos";
-val zero_less_mult_pos2 = thm "zero_less_mult_pos2";
-val zero_less_mult_iff = thm "zero_less_mult_iff";
-val mult_eq_0_iff = thm "mult_eq_0_iff";
-val zero_le_mult_iff = thm "zero_le_mult_iff";
-val mult_less_0_iff = thm "mult_less_0_iff";
-val mult_le_0_iff = thm "mult_le_0_iff";
-val split_mult_pos_le = thm "split_mult_pos_le";
-val split_mult_neg_le = thm "split_mult_neg_le";
-val zero_le_square = thm "zero_le_square";
-val zero_le_one = thm "zero_le_one";
-val not_one_le_zero = thm "not_one_le_zero";
-val not_one_less_zero = thm "not_one_less_zero";
-val mult_left_mono_neg = thm "mult_left_mono_neg";
-val mult_right_mono_neg = thm "mult_right_mono_neg";
-val mult_strict_mono = thm "mult_strict_mono";
-val mult_strict_mono' = thm "mult_strict_mono'";
-val mult_mono = thm "mult_mono";
-val less_1_mult = thm "less_1_mult";
-val mult_less_cancel_right_disj = thm "mult_less_cancel_right_disj";
-val mult_less_cancel_left_disj = thm "mult_less_cancel_left_disj";
-val mult_less_cancel_right = thm "mult_less_cancel_right";
-val mult_less_cancel_left = thm "mult_less_cancel_left";
-val mult_le_cancel_right = thm "mult_le_cancel_right";
-val mult_le_cancel_left = thm "mult_le_cancel_left";
-val mult_less_imp_less_left = thm "mult_less_imp_less_left";
-val mult_less_imp_less_right = thm "mult_less_imp_less_right";
-val mult_cancel_right = thm "mult_cancel_right";
-val mult_cancel_left = thm "mult_cancel_left";
-val ring_eq_simps = thms "ring_eq_simps";
-val right_inverse = thm "right_inverse";
-val right_inverse_eq = thm "right_inverse_eq";
-val nonzero_inverse_eq_divide = thm "nonzero_inverse_eq_divide";
-val divide_self = thm "divide_self";
-val divide_zero = thm "divide_zero";
-val divide_zero_left = thm "divide_zero_left";
-val inverse_eq_divide = thm "inverse_eq_divide";
-val add_divide_distrib = thm "add_divide_distrib";
-val field_mult_eq_0_iff = thm "field_mult_eq_0_iff";
-val field_mult_cancel_right_lemma = thm "field_mult_cancel_right_lemma";
-val field_mult_cancel_right = thm "field_mult_cancel_right";
-val field_mult_cancel_left = thm "field_mult_cancel_left";
-val nonzero_imp_inverse_nonzero = thm "nonzero_imp_inverse_nonzero";
-val inverse_zero_imp_zero = thm "inverse_zero_imp_zero";
-val inverse_nonzero_imp_nonzero = thm "inverse_nonzero_imp_nonzero";
-val inverse_nonzero_iff_nonzero = thm "inverse_nonzero_iff_nonzero";
-val nonzero_inverse_minus_eq = thm "nonzero_inverse_minus_eq";
-val inverse_minus_eq = thm "inverse_minus_eq";
-val nonzero_inverse_eq_imp_eq = thm "nonzero_inverse_eq_imp_eq";
-val inverse_eq_imp_eq = thm "inverse_eq_imp_eq";
-val inverse_eq_iff_eq = thm "inverse_eq_iff_eq";
-val nonzero_inverse_inverse_eq = thm "nonzero_inverse_inverse_eq";
-val inverse_inverse_eq = thm "inverse_inverse_eq";
-val inverse_1 = thm "inverse_1";
-val nonzero_inverse_mult_distrib = thm "nonzero_inverse_mult_distrib";
-val inverse_mult_distrib = thm "inverse_mult_distrib";
-val inverse_add = thm "inverse_add";
-val inverse_divide = thm "inverse_divide";
-val nonzero_mult_divide_cancel_left = thm "nonzero_mult_divide_cancel_left";
-val mult_divide_cancel_left = thm "mult_divide_cancel_left";
-val nonzero_mult_divide_cancel_right = thm "nonzero_mult_divide_cancel_right";
-val mult_divide_cancel_right = thm "mult_divide_cancel_right";
-val mult_divide_cancel_eq_if = thm "mult_divide_cancel_eq_if";
-val divide_1 = thm "divide_1";
-val times_divide_eq_right = thm "times_divide_eq_right";
-val times_divide_eq_left = thm "times_divide_eq_left";
-val divide_divide_eq_right = thm "divide_divide_eq_right";
-val divide_divide_eq_left = thm "divide_divide_eq_left";
-val nonzero_minus_divide_left = thm "nonzero_minus_divide_left";
-val nonzero_minus_divide_right = thm "nonzero_minus_divide_right";
-val nonzero_minus_divide_divide = thm "nonzero_minus_divide_divide";
-val minus_divide_left = thm "minus_divide_left";
-val minus_divide_right = thm "minus_divide_right";
-val minus_divide_divide = thm "minus_divide_divide";
-val diff_divide_distrib = thm "diff_divide_distrib";
-val positive_imp_inverse_positive = thm "positive_imp_inverse_positive";
-val negative_imp_inverse_negative = thm "negative_imp_inverse_negative";
-val inverse_le_imp_le = thm "inverse_le_imp_le";
-val inverse_positive_imp_positive = thm "inverse_positive_imp_positive";
-val inverse_positive_iff_positive = thm "inverse_positive_iff_positive";
-val inverse_negative_imp_negative = thm "inverse_negative_imp_negative";
-val inverse_negative_iff_negative = thm "inverse_negative_iff_negative";
-val inverse_nonnegative_iff_nonnegative = thm "inverse_nonnegative_iff_nonnegative";
-val inverse_nonpositive_iff_nonpositive = thm "inverse_nonpositive_iff_nonpositive";
-val less_imp_inverse_less = thm "less_imp_inverse_less";
-val inverse_less_imp_less = thm "inverse_less_imp_less";
-val inverse_less_iff_less = thm "inverse_less_iff_less";
-val le_imp_inverse_le = thm "le_imp_inverse_le";
-val inverse_le_iff_le = thm "inverse_le_iff_le";
-val inverse_le_imp_le_neg = thm "inverse_le_imp_le_neg";
-val less_imp_inverse_less_neg = thm "less_imp_inverse_less_neg";
-val inverse_less_imp_less_neg = thm "inverse_less_imp_less_neg";
-val inverse_less_iff_less_neg = thm "inverse_less_iff_less_neg";
-val le_imp_inverse_le_neg = thm "le_imp_inverse_le_neg";
-val inverse_le_iff_le_neg = thm "inverse_le_iff_le_neg";
-val one_less_inverse_iff = thm "one_less_inverse_iff";
-val inverse_eq_1_iff = thm "inverse_eq_1_iff";
-val one_le_inverse_iff = thm "one_le_inverse_iff";
-val inverse_less_1_iff = thm "inverse_less_1_iff";
-val inverse_le_1_iff = thm "inverse_le_1_iff";
-val zero_less_divide_iff = thm "zero_less_divide_iff";
-val divide_less_0_iff = thm "divide_less_0_iff";
-val zero_le_divide_iff = thm "zero_le_divide_iff";
-val divide_le_0_iff = thm "divide_le_0_iff";
-val divide_eq_0_iff = thm "divide_eq_0_iff";
-val pos_le_divide_eq = thm "pos_le_divide_eq";
-val neg_le_divide_eq = thm "neg_le_divide_eq";
-val le_divide_eq = thm "le_divide_eq";
-val pos_divide_le_eq = thm "pos_divide_le_eq";
-val neg_divide_le_eq = thm "neg_divide_le_eq";
-val divide_le_eq = thm "divide_le_eq";
-val pos_less_divide_eq = thm "pos_less_divide_eq";
-val neg_less_divide_eq = thm "neg_less_divide_eq";
-val less_divide_eq = thm "less_divide_eq";
-val pos_divide_less_eq = thm "pos_divide_less_eq";
-val neg_divide_less_eq = thm "neg_divide_less_eq";
-val divide_less_eq = thm "divide_less_eq";
-val nonzero_eq_divide_eq = thm "nonzero_eq_divide_eq";
-val eq_divide_eq = thm "eq_divide_eq";
-val nonzero_divide_eq_eq = thm "nonzero_divide_eq_eq";
-val divide_eq_eq = thm "divide_eq_eq";
-val divide_cancel_right = thm "divide_cancel_right";
-val divide_cancel_left = thm "divide_cancel_left";
-val divide_eq_1_iff = thm "divide_eq_1_iff";
-val one_eq_divide_iff = thm "one_eq_divide_iff";
-val zero_eq_1_divide_iff = thm "zero_eq_1_divide_iff";
-val one_divide_eq_0_iff = thm "one_divide_eq_0_iff";
-val divide_strict_right_mono = thm "divide_strict_right_mono";
-val divide_right_mono = thm "divide_right_mono";
-val divide_strict_left_mono = thm "divide_strict_left_mono";
-val divide_left_mono = thm "divide_left_mono";
-val divide_strict_left_mono_neg = thm "divide_strict_left_mono_neg";
-val divide_strict_right_mono_neg = thm "divide_strict_right_mono_neg";
-val less_add_one = thm "less_add_one";
-val zero_less_two = thm "zero_less_two";
-val less_half_sum = thm "less_half_sum";
-val gt_half_sum = thm "gt_half_sum";
-val dense = thm "dense";
-val abs_one = thm "abs_one";
-val abs_le_mult = thm "abs_le_mult";
-val abs_eq_mult = thm "abs_eq_mult";
-val abs_mult = thm "abs_mult";
-val abs_mult_self = thm "abs_mult_self";
-val nonzero_abs_inverse = thm "nonzero_abs_inverse";
-val abs_inverse = thm "abs_inverse";
-val nonzero_abs_divide = thm "nonzero_abs_divide";
-val abs_divide = thm "abs_divide";
-val abs_mult_less = thm "abs_mult_less";
-val eq_minus_self_iff = thm "eq_minus_self_iff";
-val less_minus_self_iff = thm "less_minus_self_iff";
-val abs_less_iff = thm "abs_less_iff";
-*}
-
end
--- a/src/HOL/Tools/Presburger/presburger.ML Thu Mar 29 11:59:54 2007 +0200
+++ b/src/HOL/Tools/Presburger/presburger.ML Thu Mar 29 14:21:45 2007 +0200
@@ -301,9 +301,9 @@
addsimps add_ac
addsimprocs [cancel_div_mod_proc]
val simpset0 = HOL_basic_ss
- addsimps [mod_div_equality', Suc_plus1]
+ addsimps [@{thm mod_div_equality'}, @{thm Suc_plus1}]
addsimps comp_arith
- addsplits [split_zdiv, split_zmod, split_div', split_min, split_max]
+ addsplits [split_zdiv, split_zmod, split_div', @{thm split_min}, @{thm split_max}]
(* Simp rules for changing (n::int) to int n *)
val simpset1 = HOL_basic_ss
addsimps [nat_number_of_def, zdvd_int] @ map (fn r => r RS sym)
--- a/src/HOL/W0/W0.thy Thu Mar 29 11:59:54 2007 +0200
+++ b/src/HOL/W0/W0.thy Thu Mar 29 14:21:45 2007 +0200
@@ -196,7 +196,7 @@
apply (unfold new_tv_def)
apply (tactic "safe_tac HOL_cs")
-- {* @{text \<Longrightarrow>} *}
- apply (tactic {* fast_tac (HOL_cs addDs [leD] addss (simpset()
+ apply (tactic {* fast_tac (HOL_cs addDs [@{thm leD}] addss (simpset()
addsimps [thm "free_tv_subst", thm "dom_def"])) 1 *})
apply (subgoal_tac "m \<in> cod s \<or> s l = TVar l")
apply (tactic "safe_tac HOL_cs")
--- a/src/HOL/arith_data.ML Thu Mar 29 11:59:54 2007 +0200
+++ b/src/HOL/arith_data.ML Thu Mar 29 14:21:45 2007 +0200
@@ -89,7 +89,7 @@
val dest_sum = dest_sum;
val prove_conv = prove_conv;
val norm_tac1 = simp_all_tac add_rules;
- val norm_tac2 = simp_all_tac add_ac;
+ val norm_tac2 = simp_all_tac @{thms add_ac};
fun norm_tac ss = norm_tac1 ss THEN norm_tac2 ss;
end;
@@ -172,8 +172,8 @@
val conjI = conjI;
val notI = notI;
val sym = sym;
-val not_lessD = linorder_not_less RS iffD1;
-val not_leD = linorder_not_le RS iffD1;
+val not_lessD = @{thm linorder_not_less} RS iffD1;
+val not_leD = @{thm linorder_not_le} RS iffD1;
val le0 = thm "le0";
fun mk_Eq thm = (thm RS Eq_FalseI) handle THM _ => (thm RS Eq_TrueI);
@@ -937,7 +937,7 @@
val add_mono_thms_ordered_semiring = map (fn s => prove_goal (the_context ()) s
(fn prems => [cut_facts_tac prems 1,
- blast_tac (claset() addIs [add_mono]) 1]))
+ blast_tac (claset() addIs [@{thm add_mono}]) 1]))
["(i <= j) & (k <= l) ==> i + k <= j + (l::'a::pordered_ab_semigroup_add)",
"(i = j) & (k <= l) ==> i + k <= j + (l::'a::pordered_ab_semigroup_add)",
"(i <= j) & (k = l) ==> i + k <= j + (l::'a::pordered_ab_semigroup_add)",
@@ -945,7 +945,8 @@
];
val mono_ss = simpset() addsimps
- [add_mono,add_strict_mono,add_less_le_mono,add_le_less_mono];
+ [@{thm add_mono}, @{thm add_strict_mono},
+ @{thm add_less_le_mono}, @{thm add_le_less_mono}];
val add_mono_thms_ordered_field =
map (fn s => prove_goal (the_context ()) s
@@ -966,7 +967,7 @@
mult_mono_thms = mult_mono_thms,
inj_thms = inj_thms,
lessD = lessD @ [thm "Suc_leI"],
- neqE = [thm "linorder_neqE_nat",
+ neqE = [@{thm linorder_neqE_nat},
get_thm (theory "Ring_and_Field") (Name "linorder_neqE_ordered_idom")],
simpset = HOL_basic_ss addsimps add_rules
addsimprocs [ab_group_add_cancel.sum_conv,
@@ -1041,7 +1042,7 @@
local
val antisym = mk_meta_eq order_antisym
-val not_lessD = linorder_not_less RS iffD1
+val not_lessD = @{thm linorder_not_less} RS iffD1
fun prp t thm = (#prop(rep_thm thm) = t)
in
fun antisym_eq prems thm =
--- a/src/HOL/ex/MT.ML Thu Mar 29 11:59:54 2007 +0200
+++ b/src/HOL/ex/MT.ML Thu Mar 29 14:21:45 2007 +0200
@@ -81,11 +81,11 @@
val [cih,monoh] = goal (the_context ()) "[| x:f({x} Un gfp(f)); mono(f) |] ==> x:gfp(f)";
by (rtac (cih RSN (2,gfp_upperbound RS subsetD)) 1);
-by (rtac (monoh RS monoD) 1);
+by (rtac (monoh RS @{thm monoD}) 1);
by (rtac (UnE RS subsetI) 1);
by (assume_tac 1);
by (blast_tac (claset() addSIs [cih]) 1);
-by (rtac (monoh RS monoD RS subsetD) 1);
+by (rtac (monoh RS @{thm monoD} RS subsetD) 1);
by (rtac (thm "Un_upper2") 1);
by (etac (monoh RS gfp_lemma2 RS subsetD) 1);
qed "gfp_coind2";