| author | nipkow |
| Mon, 18 Dec 2000 14:59:05 +0100 | |
| changeset 10693 | 9e4a0e84d0d6 |
| parent 10692 | 6077fd933575 |
| child 10694 | 9a5d5df29e5c |
--- a/src/HOL/Integ/int_arith1.ML Mon Dec 18 14:57:58 2000 +0100 +++ b/src/HOL/Integ/int_arith1.ML Mon Dec 18 14:59:05 2000 +0100 @@ -79,8 +79,7 @@ (*Utilities*) -fun mk_numeral n = HOLogic.number_of_const HOLogic.intT $ - NumeralSyntax.mk_bin n; +fun mk_numeral n = HOLogic.number_of_const HOLogic.intT $ HOLogic.mk_bin n; (*Decodes a binary INTEGER*) fun dest_numeral (Const("Numeral.number_of", _) $ w) = @@ -416,8 +415,9 @@ in val int_arith_setup = - [Fast_Arith.map_data (fn {add_mono_thms, inj_thms, lessD, simpset} => + [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} => {add_mono_thms = add_mono_thms @ add_mono_thms_int, + mult_mono_thms = mult_mono_thms, inj_thms = [zle_int RS iffD2,int_int_eq RS iffD2] @ inj_thms, lessD = lessD @ [add1_zle_eq RS iffD2], simpset = simpset addsimps add_rules
--- a/src/HOL/Integ/nat_bin.ML Mon Dec 18 14:57:58 2000 +0100 +++ b/src/HOL/Integ/nat_bin.ML Mon Dec 18 14:59:05 2000 +0100 @@ -45,8 +45,8 @@ val nat_bin_arith_setup = - [Fast_Arith.map_data (fn {add_mono_thms, inj_thms, lessD, simpset} => - {add_mono_thms = add_mono_thms, + [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, inj_thms = inj_thms, lessD = lessD, simpset = simpset addsimps [int_nat_number_of,
--- a/src/HOL/Integ/nat_simprocs.ML Mon Dec 18 14:57:58 2000 +0100 +++ b/src/HOL/Integ/nat_simprocs.ML Mon Dec 18 14:59:05 2000 +0100 @@ -88,8 +88,7 @@ (*Utilities*) -fun mk_numeral n = HOLogic.number_of_const HOLogic.natT $ - NumeralSyntax.mk_bin n; +fun mk_numeral n = HOLogic.number_of_const HOLogic.natT $ HOLogic.mk_bin n; (*Decodes a unary or binary numeral to a NATURAL NUMBER*) fun dest_numeral (Const ("0", _)) = 0 @@ -466,8 +465,9 @@ in val nat_simprocs_setup = - [Fast_Arith.map_data (fn {add_mono_thms, inj_thms, lessD, simpset} => - {add_mono_thms = add_mono_thms, inj_thms = inj_thms, lessD = lessD, + [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, + inj_thms = inj_thms, lessD = lessD, simpset = simpset addsimps add_rules addsimps basic_renamed_arith_simps addsimprocs simprocs})];
--- a/src/HOL/Real/RealBin.ML Mon Dec 18 14:57:58 2000 +0100 +++ b/src/HOL/Real/RealBin.ML Mon Dec 18 14:59:05 2000 +0100 @@ -262,8 +262,7 @@ (*Utilities*) -fun mk_numeral n = HOLogic.number_of_const HOLogic.realT $ - NumeralSyntax.mk_bin n; +fun mk_numeral n = HOLogic.number_of_const HOLogic.realT $ HOLogic.mk_bin n; (*Decodes a binary real constant*) fun dest_numeral (Const("Numeral.number_of", _) $ w) =
--- a/src/HOL/Real/real_arith.ML Mon Dec 18 14:57:58 2000 +0100 +++ b/src/HOL/Real/real_arith.ML Mon Dec 18 14:59:05 2000 +0100 @@ -24,7 +24,7 @@ real_mult_minus_1, real_mult_minus_1_right]; val simprocs = [Real_Times_Assoc.conv, Real_Numeral_Simprocs.combine_numerals]@ - Real_Numeral_Simprocs.cancel_numerals; + Real_Numeral_Simprocs.cancel_numerals(* @ real_cancel_numeral_factors*); val mono_ss = simpset() addsimps [real_add_le_mono,real_add_less_mono, @@ -47,17 +47,26 @@ map (fn s => Thm.read_cterm (Theory.sign_of (the_context ())) (s, HOLogic.boolT)) ["(m::real) < n","(m::real) <= n", "(m::real) = n"]; +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_le_mono2, + cvar(real_mult_le_mono2, hd(tl(prems_of real_mult_le_mono2))))] + in val fast_real_arith_simproc = mk_simproc "fast_real_arith" real_arith_simproc_pats Fast_Arith.lin_arith_prover; val real_arith_setup = - [Fast_Arith.map_data (fn {add_mono_thms, inj_thms, lessD, simpset} => + [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} => {add_mono_thms = add_mono_thms @ add_mono_thms_real, + mult_mono_thms = mult_mono_thms @ real_mult_mono_thms, inj_thms = inj_thms, (*FIXME: add real*) lessD = lessD, (*We don't change LA_Data_Ref.lessD because the real ordering is dense!*) - simpset = simpset addsimps simps@add_rules + simpset = simpset addsimps (True_implies_equals :: add_rules @ simps) addsimprocs simprocs addcongs [if_weak_cong]}), arith_discrete ("RealDef.real",false),
--- a/src/HOL/Tools/numeral_syntax.ML Mon Dec 18 14:57:58 2000 +0100 +++ b/src/HOL/Tools/numeral_syntax.ML Mon Dec 18 14:59:05 2000 +0100 @@ -10,7 +10,6 @@ signature NUMERAL_SYNTAX = sig val dest_bin : term -> int - val mk_bin : int -> term val setup : (theory -> theory) list end; @@ -20,10 +19,6 @@ (* bits *) -fun mk_bit 0 = HOLogic.false_const - | mk_bit 1 = HOLogic.true_const - | mk_bit _ = sys_error "mk_bit"; - fun dest_bit (Const ("False", _)) = 0 | dest_bit (Const ("True", _)) = 1 | dest_bit _ = raise Match; @@ -35,17 +30,6 @@ | prefix_len pred (x :: xs) = if pred x then 1 + prefix_len pred xs else 0; -fun mk_bin n = - let - fun bin_of 0 = [] - | bin_of ~1 = [~1] - | bin_of n = (n mod 2) :: bin_of (n div 2); - - fun term_of [] = HOLogic.pls_const - | term_of [~1] = HOLogic.min_const - | term_of (b :: bs) = HOLogic.bit_const $ term_of bs $ mk_bit b; - in term_of (bin_of n) end; - (*we consider all "spellings"; Min is likely to be declared elsewhere*) fun bin_of (Const ("Pls", _)) = [] | bin_of (Const ("bin.Pls", _)) = [] @@ -74,7 +58,7 @@ (* translation of integer numeral tokens to and from bitstrings *) fun numeral_tr (*"_Numeral"*) [t as Free (str, _)] = - (Syntax.const "Numeral.number_of" $ mk_bin (Syntax.read_xnum str)) + (Syntax.const "Numeral.number_of" $ HOLogic.mk_bin (Syntax.read_xnum str)) | numeral_tr (*"_Numeral"*) ts = raise TERM ("numeral_tr", ts); fun numeral_tr' show_sorts (*"number_of"*) (Type ("fun", [_, T])) (t :: ts) =
--- a/src/HOL/arith_data.ML Mon Dec 18 14:57:58 2000 +0100 +++ b/src/HOL/arith_data.ML Mon Dec 18 14:59:05 2000 +0100 @@ -299,8 +299,14 @@ | nT _ = false; fun add_atom(t,m,(p,i)) = (case assoc(p,t) of None => ((t,m)::p,i) - | Some n => (overwrite(p,(t,n+m:int)), i)); + | Some n => (overwrite(p,(t,ratadd(n,m))), i)); + +exception Zero; +fun rat_of_term(numt,dent) = + let val num = HOLogic.dest_binum numt and den = HOLogic.dest_binum dent + in if den = 0 then raise Zero else int_ratdiv(num,den) end; + fun decomp2 inj_consts (rel,lhs,rhs) = let @@ -308,30 +314,44 @@ fun poly(Const("op +",_) $ s $ t, m, pi) = poly(s,m,poly(t,m,pi)) | poly(all as Const("op -",T) $ s $ t, m, pi) = if nT T then add_atom(all,m,pi) - else poly(s,m,poly(t,~1*m,pi)) - | poly(Const("uminus",_) $ t, m, pi) = poly(t,~1*m,pi) + else poly(s,m,poly(t,ratneg m,pi)) + | poly(Const("uminus",_) $ t, m, pi) = poly(t,ratneg m,pi) | poly(Const("0",_), _, pi) = pi - | poly(Const("Suc",_)$t, m, (p,i)) = poly(t, m, (p,i+m)) + | poly(Const("Suc",_)$t, m, (p,i)) = poly(t, m, (p,ratadd(i,m))) | poly(all as Const("op *",_) $ (Const("Numeral.number_of",_)$c) $ t, m, pi)= - (poly(t,m*HOLogic.dest_binum c,pi) + (poly(t,ratmul(m, rat_of_int(HOLogic.dest_binum c)),pi) handle TERM _ => add_atom(all,m,pi)) | poly(all as Const("op *",_) $ t $ (Const("Numeral.number_of",_)$c), m, pi)= - (poly(t,m*HOLogic.dest_binum c,pi) + (poly(t,ratmul(m, rat_of_int(HOLogic.dest_binum c)),pi) handle TERM _ => add_atom(all,m,pi)) + | poly(Const("op *",_) $ (Const("HOL.divide",_) $ (Const("Numeral.number_of",_)$numt) $ + (Const("Numeral.number_of",_)$dent)) $ t, m, pi) = + poly(t,ratmul(m,rat_of_term(numt,dent)),pi) + | poly(Const("op *",_) $ t $ (Const("HOL.divide",_) $ (Const("Numeral.number_of",_)$numt) $ + (Const("Numeral.number_of",_)$dent)), m, pi) = + poly(t,ratmul(m,rat_of_term(numt,dent)),pi) + | poly(all as Const("HOL.divide",_) $ t $ (Const("Numeral.number_of",_)$dent), m, pi) = + let val den = HOLogic.dest_binum dent + in if den = 0 then raise Zero else poly(t,ratmul(m, ratinv(rat_of_int den)),pi) end | poly(all as Const("Numeral.number_of",_)$t,m,(p,i)) = - ((p,i + m*HOLogic.dest_binum t) + ((p,ratadd(i,ratmul(m,rat_of_int(HOLogic.dest_binum t)))) handle TERM _ => add_atom(all,m,(p,i))) + | poly(Const("HOL.divide",_) $ (Const("Numeral.number_of",_)$numt) $ + (Const("Numeral.number_of",_)$dent), m, (p,i)) = + (p,ratadd(i,ratmul(m,rat_of_term(numt,dent)))) | poly(all as Const f $ x, m, pi) = if f mem inj_consts then poly(x,m,pi) else add_atom(all,m,pi) | poly x = add_atom x; - val (p,i) = poly(lhs,1,([],0)) and (q,j) = poly(rhs,1,([],0)) + val (p,i) = poly(lhs,rat_of_int 1,([],rat_of_int 0)) + and (q,j) = poly(rhs,rat_of_int 1,([],rat_of_int 0)) + in case rel of "op <" => Some(p,i,"<",q,j) | "op <=" => Some(p,i,"<=",q,j) | "op =" => Some(p,i,"=",q,j) | _ => None - end; + end handle Zero => None; fun negate(Some(x,i,rel,y,j,d)) = Some(x,i,"~"^rel,y,j,d) | negate None = None; @@ -355,6 +375,8 @@ let val {discrete, inj_consts, ...} = ArithTheoryData.get_sg sg in decomp2 (discrete,inj_consts) end +fun number_of(n,T) = HOLogic.number_of_const T $ (HOLogic.mk_bin n) + end; @@ -384,8 +406,9 @@ val init_lin_arith_data = Fast_Arith.setup @ - [Fast_Arith.map_data (fn {add_mono_thms, inj_thms, lessD, simpset = _} => + [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset = _} => {add_mono_thms = add_mono_thms @ add_mono_thms_nat, + mult_mono_thms = mult_mono_thms, inj_thms = inj_thms, lessD = lessD @ [Suc_leI], simpset = HOL_basic_ss addsimps add_rules addsimprocs nat_cancel_sums_add}),
--- a/src/HOL/hologic.ML Mon Dec 18 14:57:58 2000 +0100 +++ b/src/HOL/hologic.ML Mon Dec 18 14:59:05 2000 +0100 @@ -71,6 +71,7 @@ val number_of_const: typ -> term val int_of: int list -> int val dest_binum: term -> int + val mk_bin : int -> term end; @@ -290,4 +291,19 @@ val dest_binum = int_of o bin_of; +fun mk_bit 0 = false_const + | mk_bit 1 = true_const + | mk_bit _ = sys_error "mk_bit"; + +fun mk_bin n = + let + fun bin_of 0 = [] + | bin_of ~1 = [~1] + | bin_of n = (n mod 2) :: bin_of (n div 2); + + fun term_of [] = pls_const + | term_of [~1] = min_const + | term_of (b :: bs) = bit_const $ term_of bs $ mk_bit b; + in term_of (bin_of n) end; + end;