# HG changeset patch # User haftmann # Date 1175170905 -7200 # Node ID 6ce4bddf3bcb5138bffad253db5145d6d0108ff9 # Parent c3290f4382e4a4eaee0f943041e050e32b7686fc dropped legacy ML bindings diff -r c3290f4382e4 -r 6ce4bddf3bcb src/HOL/Integ/int_arith1.ML --- 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 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 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); -*) diff -r c3290f4382e4 -r 6ce4bddf3bcb src/HOL/Integ/int_factor_simprocs.ML --- 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 diff -r c3290f4382e4 -r 6ce4bddf3bcb src/HOL/Integ/nat_simprocs.ML --- 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 diff -r c3290f4382e4 -r 6ce4bddf3bcb src/HOL/Integ/presburger.ML --- 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) diff -r c3290f4382e4 -r 6ce4bddf3bcb src/HOL/Lattices.thy --- 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 diff -r c3290f4382e4 -r 6ce4bddf3bcb src/HOL/OrderedGroup.thy --- 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 diff -r c3290f4382e4 -r 6ce4bddf3bcb src/HOL/Orderings.thy --- 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"; diff -r c3290f4382e4 -r 6ce4bddf3bcb src/HOL/Real/ferrante_rackoff.ML --- 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) diff -r c3290f4382e4 -r 6ce4bddf3bcb src/HOL/Real/ferrante_rackoff_proof.ML --- 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)] diff -r c3290f4382e4 -r 6ce4bddf3bcb src/HOL/Real/rat_arith.ML --- 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", []) diff -r c3290f4382e4 -r 6ce4bddf3bcb src/HOL/Ring_and_Field.thy --- 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 diff -r c3290f4382e4 -r 6ce4bddf3bcb src/HOL/Tools/Presburger/presburger.ML --- 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) diff -r c3290f4382e4 -r 6ce4bddf3bcb src/HOL/W0/W0.thy --- 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 \} *} - 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 \ cod s \ s l = TVar l") apply (tactic "safe_tac HOL_cs") diff -r c3290f4382e4 -r 6ce4bddf3bcb src/HOL/arith_data.ML --- 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 = diff -r c3290f4382e4 -r 6ce4bddf3bcb src/HOL/ex/MT.ML --- 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";