# HG changeset patch # User nipkow # Date 1094485055 -7200 # Node ID d2c19aea17bc814718e10a68928c00252f8a8242 # Parent 66da80cad4a2ea966f67cc08985ab6901d3ba9de made mult_mono_thms generic. diff -r 66da80cad4a2 -r d2c19aea17bc src/HOL/Hyperreal/hypreal_arith.ML --- a/src/HOL/Hyperreal/hypreal_arith.ML Mon Sep 06 16:45:10 2004 +0200 +++ b/src/HOL/Hyperreal/hypreal_arith.ML Mon Sep 06 17:37:35 2004 +0200 @@ -8,26 +8,11 @@ Instantiation of the generic linear arithmetic package for type hypreal. *) -(*FIXME DELETE*) -val hypreal_mult_less_mono2 = thm"hypreal_mult_less_mono2"; - -val hypreal_mult_left_mono = - read_instantiate_sg(sign_of (the_context())) [("a","?a::hypreal")] mult_left_mono; - - (****Instantiation of the generic linear arithmetic package****) local -fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (#sign(rep_thm th)) var; - -val hypreal_mult_mono_thms = - [(rotate_prems 1 hypreal_mult_less_mono2, - cvar(hypreal_mult_less_mono2, hd(prems_of hypreal_mult_less_mono2))), - (hypreal_mult_left_mono, - cvar(hypreal_mult_left_mono, hd(tl(prems_of hypreal_mult_left_mono))))] - val real_inj_thms = [hypreal_of_real_le_iff RS iffD2, hypreal_of_real_less_iff RS iffD2, hypreal_of_real_eq_iff RS iffD2]; @@ -45,7 +30,7 @@ val hypreal_arith_setup = [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} => {add_mono_thms = add_mono_thms, - mult_mono_thms = mult_mono_thms @ hypreal_mult_mono_thms, + mult_mono_thms = mult_mono_thms, inj_thms = inj_thms @ real_inj_thms, lessD = lessD, (*Can't change LA_Data_Ref.lessD: the hypreals are dense!*) simpset = simpset}), diff -r 66da80cad4a2 -r d2c19aea17bc src/HOL/Integ/int_arith1.ML --- a/src/HOL/Integ/int_arith1.ML Mon Sep 06 16:45:10 2004 +0200 +++ b/src/HOL/Integ/int_arith1.ML Mon Sep 06 17:37:35 2004 +0200 @@ -516,7 +516,7 @@ val int_arith_setup = [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} => {add_mono_thms = add_mono_thms, - mult_mono_thms = mult_mono_thms, + mult_mono_thms = [mult_strict_left_mono,mult_left_mono] @ mult_mono_thms, inj_thms = [zle_int RS iffD2,int_int_eq RS iffD2] @ inj_thms, lessD = lessD @ [zless_imp_add1_zle], simpset = simpset addsimps add_rules diff -r 66da80cad4a2 -r d2c19aea17bc src/HOL/Real/rat_arith.ML --- a/src/HOL/Real/rat_arith.ML Mon Sep 06 16:45:10 2004 +0200 +++ b/src/HOL/Real/rat_arith.ML Mon Sep 06 17:37:35 2004 +0200 @@ -8,29 +8,12 @@ Instantiation of the generic linear arithmetic package for type rat. *) -(*FIXME: these monomorphic versions are necessary because of a bug in the arith - procedure*) -val rat_mult_strict_left_mono = - read_instantiate_sg(sign_of (the_context())) [("a","?a::rat")] mult_strict_left_mono; - -val rat_mult_left_mono = - read_instantiate_sg(sign_of (the_context())) [("a","?a::rat")] mult_left_mono; - - (****Instantiation of the generic linear arithmetic package for fields****) local val simprocs = field_cancel_numeral_factors -fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (#sign(rep_thm th)) var; - -val rat_mult_mono_thms = - [(rat_mult_strict_left_mono, - cvar(rat_mult_strict_left_mono, hd(tl(prems_of rat_mult_strict_left_mono)))), - (rat_mult_left_mono, - cvar(rat_mult_left_mono, hd(tl(prems_of rat_mult_left_mono))))] - val simps = [order_less_irrefl, neg_less_iff_less, True_implies_equals, inst "a" "(number_of ?v)" right_distrib, divide_1, divide_zero_left, @@ -57,7 +40,7 @@ val rat_arith_setup = [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} => {add_mono_thms = add_mono_thms, - mult_mono_thms = mult_mono_thms @ rat_mult_mono_thms, + mult_mono_thms = mult_mono_thms, inj_thms = int_inj_thms @ inj_thms, lessD = lessD, (*Can't change LA_Data_Ref.lessD: the rats are dense!*) simpset = simpset addsimps simps diff -r 66da80cad4a2 -r d2c19aea17bc src/HOL/Real/real_arith.ML --- a/src/HOL/Real/real_arith.ML Mon Sep 06 16:45:10 2004 +0200 +++ b/src/HOL/Real/real_arith.ML Mon Sep 06 17:37:35 2004 +0200 @@ -8,10 +8,6 @@ Instantiation of the generic linear arithmetic package for type real. *) -(*FIXME DELETE*) -val real_mult_left_mono = - read_instantiate_sg(sign_of (the_context())) [("a","?a::real")] mult_left_mono; - val real_le_def = thm "real_le_def"; val real_diff_def = thm "real_diff_def"; val real_divide_def = thm "real_divide_def"; @@ -102,14 +98,6 @@ local -fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (#sign(rep_thm th)) var; - -val real_mult_mono_thms = - [(rotate_prems 1 real_mult_less_mono2, - cvar(real_mult_less_mono2, hd(prems_of real_mult_less_mono2))), - (real_mult_left_mono, - cvar(real_mult_left_mono, hd(tl(prems_of real_mult_left_mono))))] - val simps = [real_of_nat_zero, real_of_nat_Suc, real_of_nat_add, real_of_nat_mult, real_of_int_zero, real_of_one, real_of_int_add RS sym, real_of_int_minus RS sym, real_of_int_diff RS sym, @@ -132,7 +120,7 @@ val real_arith_setup = [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} => {add_mono_thms = add_mono_thms, - mult_mono_thms = mult_mono_thms @ real_mult_mono_thms, + mult_mono_thms = mult_mono_thms, inj_thms = int_inj_thms @ nat_inj_thms @ inj_thms, lessD = lessD, (*Can't change LA_Data_Ref.lessD: the reals are dense!*) simpset = simpset addsimps simps}), diff -r 66da80cad4a2 -r d2c19aea17bc src/HOL/arith_data.ML --- a/src/HOL/arith_data.ML Mon Sep 06 16:45:10 2004 +0200 +++ b/src/HOL/arith_data.ML Mon Sep 06 17:37:35 2004 +0200 @@ -393,7 +393,8 @@ *) val add_rules = [add_zero_left,add_zero_right,Zero_not_Suc,Suc_not_Zero,le_0_eq, - One_nat_def,isolateSuc]; + One_nat_def,isolateSuc, + order_less_irrefl]; val add_mono_thms_ordered_semiring = map (fn s => prove_goal (the_context ()) s (fn prems => [cut_facts_tac prems 1, diff -r 66da80cad4a2 -r d2c19aea17bc src/HOL/simpdata.ML --- a/src/HOL/simpdata.ML Mon Sep 06 16:45:10 2004 +0200 +++ b/src/HOL/simpdata.ML Mon Sep 06 17:37:35 2004 +0200 @@ -338,17 +338,18 @@ where the Ai are atomic, i.e. no top-level &, | or EX *) -fun refute_tac test prep_tac ref_tac = - let val nnf_simps = +local + val nnf_simps = [imp_conv_disj,iff_conv_conj_imp,de_Morgan_disj,de_Morgan_conj, not_all,not_ex,not_not]; - val nnf_simpset = + val nnf_simpset = empty_ss setmkeqTrue mk_eq_True setmksimps (mksimps mksimps_pairs) addsimps nnf_simps; - val prem_nnf_tac = full_simp_tac nnf_simpset; - - val refute_prems_tac = + val prem_nnf_tac = full_simp_tac nnf_simpset +in +fun refute_tac test prep_tac ref_tac = + let val refute_prems_tac = REPEAT_DETERM (eresolve_tac [conjE, exE] 1 ORELSE filter_prems_tac test 1 ORELSE @@ -359,3 +360,4 @@ REPEAT_DETERM o etac rev_mp, prep_tac, rtac ccontr, prem_nnf_tac, SELECT_GOAL (DEPTH_SOLVE refute_prems_tac)] end; +end; \ No newline at end of file diff -r 66da80cad4a2 -r d2c19aea17bc src/Provers/Arith/fast_lin_arith.ML --- a/src/Provers/Arith/fast_lin_arith.ML Mon Sep 06 16:45:10 2004 +0200 +++ b/src/Provers/Arith/fast_lin_arith.ML Mon Sep 06 17:37:35 2004 +0200 @@ -71,9 +71,9 @@ signature FAST_LIN_ARITH = sig val setup: (theory -> theory) list - val map_data: ({add_mono_thms: thm list, mult_mono_thms: (thm*cterm)list, inj_thms: thm list, + val map_data: ({add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list, lessD: thm list, simpset: Simplifier.simpset} - -> {add_mono_thms: thm list, mult_mono_thms: (thm*cterm)list, inj_thms: thm list, + -> {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list, lessD: thm list, simpset: Simplifier.simpset}) -> theory -> theory val trace : bool ref @@ -95,7 +95,7 @@ structure DataArgs = struct val name = "Provers/fast_lin_arith"; - type T = {add_mono_thms: thm list, mult_mono_thms: (thm*cterm)list, inj_thms: thm list, + type T = {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list, lessD: thm list, simpset: Simplifier.simpset}; val empty = {add_mono_thms = [], mult_mono_thms = [], inj_thms = [], @@ -108,8 +108,7 @@ {add_mono_thms= add_mono_thms2, mult_mono_thms= mult_mono_thms2, inj_thms= inj_thms2, lessD = lessD2, simpset = simpset2}) = {add_mono_thms = Drule.merge_rules (add_mono_thms1, add_mono_thms2), - mult_mono_thms = gen_merge_lists' (Drule.eq_thm_prop o pairself fst) - mult_mono_thms1 mult_mono_thms2, + mult_mono_thms = Drule.merge_rules (mult_mono_thms1, mult_mono_thms2), inj_thms = Drule.merge_rules (inj_thms1, inj_thms2), lessD = Drule.merge_rules (lessD1, lessD2), simpset = Simplifier.merge_ss (simpset1, simpset2)}; @@ -450,12 +449,20 @@ fun multn(n,thm) = let fun mul(i,th) = if i=1 then th else mul(i-1, addthms thm th) in if n < 0 then mul(~n,thm) RS LA_Logic.sym else mul(n,thm) end; - +(* fun multn2(n,thm) = let val Some(mth,cv) = get_first (fn (th,cv) => Some(thm RS th,cv) handle THM _ => None) mult_mono_thms val ct = cterm_of sg (LA_Data.number_of(n,#T(rep_cterm cv))) in instantiate ([],[(cv,ct)]) mth end +*) + fun multn2(n,thm) = + let val Some(mth) = + get_first (fn th => Some(thm RS th) handle THM _ => None) mult_mono_thms + fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (#sign(rep_thm th)) var; + val cv = cvar(mth, hd(prems_of mth)); + val ct = cterm_of sg (LA_Data.number_of(n,#T(rep_cterm cv))) + in instantiate ([],[(cv,ct)]) mth end fun simp thm = let val thm' = trace_thm "Simplified:" (full_simplify simpset thm)