introduced mk/dest_numeral/number for mk/dest_binum etc.
--- a/src/HOL/Integ/IntArith.thy Wed Dec 13 15:45:30 2006 +0100
+++ b/src/HOL/Integ/IntArith.thy Wed Dec 13 15:45:31 2006 +0100
@@ -16,15 +16,9 @@
subsection{*Instantiating Binary Arithmetic for the Integers*}
-instance
- int :: number ..
-
-defs (overloaded)
- int_number_of_def: "(number_of w :: int) == of_int w"
- --{*the type constraint is essential!*}
-
instance int :: number_ring
-by (intro_classes, simp add: int_number_of_def)
+ int_number_of_def: "number_of w \<equiv> of_int w"
+ by intro_classes (simp only: int_number_of_def)
subsection{*Inequality Reasoning for the Arithmetic Simproc*}
@@ -400,17 +394,6 @@
declare int_code_rewrites [code func]
-ML {*
-structure Numeral =
-struct
-
-fun int_of_numeral thy num = HOLogic.dest_binum num
- handle TERM _
- => error ("not a number: " ^ Sign.string_of_term thy num);
-
-end;
-*}
-
code_type bit
(SML "bool")
(Haskell "Bool")
@@ -435,7 +418,7 @@
and "(-)/ _/ 1")
setup {*
- CodegenPackage.add_appconst ("Numeral.Bit", CodegenPackage.appgen_numeral Numeral.int_of_numeral)
+ CodegenPackage.add_appconst ("Numeral.Bit", CodegenPackage.appgen_numeral (try HOLogic.dest_numeral))
*}
--- a/src/HOL/Integ/IntDef.thy Wed Dec 13 15:45:30 2006 +0100
+++ b/src/HOL/Integ/IntDef.thy Wed Dec 13 15:45:31 2006 +0100
@@ -863,7 +863,7 @@
types_code
"int" ("int")
attach (term_of) {*
-val term_of_int = HOLogic.mk_int o IntInf.fromInt;
+val term_of_int = HOLogic.mk_number HOLogic.intT o IntInf.fromInt;
*}
attach (test) {*
fun gen_int i = one_of [~1, 1] * random_range 0 i;
@@ -955,15 +955,15 @@
IntDef Integer
ML {*
-fun number_of_codegen thy defs gr dep module b (Const ("Numeral.number_of",
- Type ("fun", [_, T as Type ("IntDef.int", [])])) $ bin) =
+fun number_of_codegen thy defs gr dep module b (Const ("Numeral.number_of", Type ("fun", [_, T])) $ t) =
+ if T = HOLogic.intT then
(SOME (fst (Codegen.invoke_tycodegen thy defs dep module false (gr, T)),
- Pretty.str (IntInf.toString (HOLogic.dest_binum bin))) handle TERM _ => NONE)
- | number_of_codegen thy defs gr s thyname b (Const ("Numeral.number_of",
- Type ("fun", [_, Type ("nat", [])])) $ bin) =
- SOME (Codegen.invoke_codegen thy defs s thyname b (gr,
+ (Pretty.str o IntInf.toString o HOLogic.dest_numeral) t) handle TERM _ => NONE)
+ else if T = HOLogic.natT then
+ SOME (Codegen.invoke_codegen thy defs dep module b (gr,
Const ("IntDef.nat", HOLogic.intT --> HOLogic.natT) $
- (Const ("Numeral.number_of", HOLogic.intT --> HOLogic.intT) $ bin)))
+ (Const ("Numeral.number_of", HOLogic.intT --> HOLogic.intT) $ t)))
+ else NONE
| number_of_codegen _ _ _ _ _ _ _ = NONE;
*}
--- a/src/HOL/Integ/Numeral.thy Wed Dec 13 15:45:30 2006 +0100
+++ b/src/HOL/Integ/Numeral.thy Wed Dec 13 15:45:31 2006 +0100
@@ -31,20 +31,19 @@
datatype bit = B0 | B1
definition
- Pls :: int where "Pls == 0"
+ Pls :: int where
+ "Pls = 0"
definition
- Min :: int where "Min == - 1"
+ Min :: int where
+ "Min = - 1"
definition
Bit :: "int \<Rightarrow> bit \<Rightarrow> int" (infixl "BIT" 90) where
- "k BIT b == (case b of B0 \<Rightarrow> 0 | B1 \<Rightarrow> 1) + k + k"
+ "k BIT b = (case b of B0 \<Rightarrow> 0 | B1 \<Rightarrow> 1) + k + k"
-axclass
- number < type -- {* for numeric types: nat, int, real, \dots *}
-
-consts
- number_of :: "int \<Rightarrow> 'a::number"
+class number = -- {* for numeric types: nat, int, real, \dots *}
+ fixes number_of :: "int \<Rightarrow> 'a"
syntax
"_Numeral" :: "num_const \<Rightarrow> 'a" ("_")
--- a/src/HOL/Integ/cooper_dec.ML Wed Dec 13 15:45:30 2006 +0100
+++ b/src/HOL/Integ/cooper_dec.ML Wed Dec 13 15:45:31 2006 +0100
@@ -11,8 +11,8 @@
sig
exception COOPER
val is_arith_rel : term -> bool
- val mk_numeral : IntInf.int -> term
- val dest_numeral : term -> IntInf.int
+ val mk_number : IntInf.int -> term
+ val dest_number : term -> IntInf.int
val is_numeral : term -> bool
val zero : term
val one : term
@@ -76,32 +76,32 @@
(*Transform a natural number to a term*)
-fun mk_numeral 0 = Const("HOL.zero",HOLogic.intT)
- |mk_numeral 1 = Const("HOL.one",HOLogic.intT)
- |mk_numeral n = (HOLogic.number_of_const HOLogic.intT) $ (HOLogic.mk_binum n);
+fun mk_number 0 = Const("HOL.zero",HOLogic.intT)
+ |mk_number 1 = Const("HOL.one",HOLogic.intT)
+ |mk_number n = (HOLogic.number_of_const HOLogic.intT) $ (HOLogic.mk_numeral n);
(*Transform an Term to an natural number*)
-fun dest_numeral (Const("HOL.zero",Type ("IntDef.int", []))) = 0
- |dest_numeral (Const("HOL.one",Type ("IntDef.int", []))) = 1
- |dest_numeral (Const ("Numeral.number_of",_) $ n) =
- HOLogic.dest_binum n;
+fun dest_number (Const("HOL.zero",Type ("IntDef.int", []))) = 0
+ |dest_number (Const("HOL.one",Type ("IntDef.int", []))) = 1
+ |dest_number (Const ("Numeral.number_of",_) $ n) =
+ HOLogic.dest_numeral n;
(*Some terms often used for pattern matching*)
-val zero = mk_numeral 0;
-val one = mk_numeral 1;
+val zero = mk_number 0;
+val one = mk_number 1;
(*Tests if a Term is representing a number*)
-fun is_numeral t = (t = zero) orelse (t = one) orelse (can dest_numeral t);
+fun is_numeral t = (t = zero) orelse (t = one) orelse (can dest_number t);
(*maps a unary natural function on a term containing an natural number*)
-fun numeral1 f n = mk_numeral (f(dest_numeral n));
+fun numeral1 f n = mk_number (f(dest_number n));
(*maps a binary natural function on 2 term containing natural numbers*)
-fun numeral2 f m n = mk_numeral(f(dest_numeral m) (dest_numeral n));
+fun numeral2 f m n = mk_number(f(dest_number m) (dest_number n));
(* ------------------------------------------------------------------------- *)
(* Operations on canonical linear terms c1 * x1 + ... + cn * xn + k *)
@@ -178,9 +178,9 @@
Free(x,T)*)
fun lint vars tm = if is_numeral tm then tm else case tm of
- (Free (x,T)) => (HOLogic.mk_binop "HOL.plus" ((HOLogic.mk_binop "HOL.times" ((mk_numeral 1),Free (x,T))), zero))
+ (Free (x,T)) => (HOLogic.mk_binop "HOL.plus" ((HOLogic.mk_binop "HOL.times" ((mk_number 1),Free (x,T))), zero))
|(Bound i) => (Const("HOL.plus",HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $
- (Const("HOL.times",HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ (mk_numeral 1) $ (Bound i)) $ zero)
+ (Const("HOL.times",HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ (mk_number 1) $ (Bound i)) $ zero)
|(Const("HOL.uminus",_) $ t ) => (linear_neg (lint vars t))
|(Const("HOL.plus",_) $ s $ t) => (linear_add vars (lint vars s) (lint vars t))
|(Const("HOL.minus",_) $ s $ t) => (linear_sub vars (lint vars s) (lint vars t))
@@ -188,8 +188,8 @@
let val s' = lint vars s
val t' = lint vars t
in
- if is_numeral s' then (linear_cmul (dest_numeral s') t')
- else if is_numeral t' then (linear_cmul (dest_numeral t') s')
+ if is_numeral s' then (linear_cmul (dest_number s') t')
+ else if is_numeral t' then (linear_cmul (dest_number t') s')
else raise COOPER
end
@@ -205,7 +205,7 @@
fun linform vars (Const ("Divides.dvd",_) $ c $ t) =
if is_numeral c then
- let val c' = (mk_numeral(abs(dest_numeral c)))
+ let val c' = (mk_number(abs(dest_number c)))
in (HOLogic.mk_binrel "Divides.dvd" (c,lint vars t))
end
else (warning "Nonlinear term --- Non numeral leftside at dvd"
@@ -214,11 +214,11 @@
|linform vars (Const("Orderings.less",_)$ s $t ) = (mkatom vars "Orderings.less" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s))
|linform vars (Const("op >",_) $ s $ t ) = (mkatom vars "Orderings.less" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ s $ t))
|linform vars (Const("Orderings.less_eq",_)$ s $ t ) =
- (mkatom vars "Orderings.less" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ (Const("HOL.plus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $t $(mk_numeral 1)) $ s))
+ (mkatom vars "Orderings.less" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ (Const("HOL.plus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $t $(mk_number 1)) $ s))
|linform vars (Const("op >=",_)$ s $ t ) =
(mkatom vars "Orderings.less" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT -->
HOLogic.intT) $ (Const("HOL.plus",HOLogic.intT --> HOLogic.intT -->
- HOLogic.intT) $s $(mk_numeral 1)) $ t))
+ HOLogic.intT) $s $(mk_number 1)) $ t))
|linform vars fm = fm;
@@ -228,7 +228,7 @@
fun posineq fm = case fm of
(Const ("Not",_)$(Const("Orderings.less",_)$ c $ t)) =>
- (HOLogic.mk_binrel "Orderings.less" (zero , (linear_sub [] (mk_numeral 1) (linear_add [] c t ) )))
+ (HOLogic.mk_binrel "Orderings.less" (zero , (linear_sub [] (mk_number 1) (linear_add [] c t ) )))
| ( Const ("op &",_) $ p $ q) => HOLogic.mk_conj (posineq p,posineq q)
| ( Const ("op |",_) $ p $ q ) => HOLogic.mk_disj (posineq p,posineq q)
| _ => fm;
@@ -245,7 +245,7 @@
fun formlcm x fm = case fm of
(Const (p,_)$ _ $(Const ("HOL.plus", _)$(Const ("HOL.times",_)$ c $ y ) $z ) ) => if
- (is_arith_rel fm) andalso (x = y) then (abs(dest_numeral c)) else 1
+ (is_arith_rel fm) andalso (x = y) then (abs(dest_number c)) else 1
| ( Const ("Not", _) $p) => formlcm x p
| ( Const ("op &",_) $ p $ q) => lcm_num (formlcm x p) (formlcm x q)
| ( Const ("op |",_) $ p $ q )=> lcm_num (formlcm x p) (formlcm x q)
@@ -259,9 +259,9 @@
case fm of
(Const(p,_) $d $( Const ("HOL.plus", _)$(Const ("HOL.times",_) $
c $ y ) $z )) => if (is_arith_rel fm) andalso (x = y) then
- let val m = l div (dest_numeral c)
+ let val m = l div (dest_number c)
val n = (if p = "Orderings.less" then abs(m) else m)
- val xtm = HOLogic.mk_binop "HOL.times" ((mk_numeral (m div n)), x)
+ val xtm = HOLogic.mk_binop "HOL.times" ((mk_number (m div n)), x)
in
(HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) ))))
end
@@ -281,9 +281,9 @@
if l = 1 then fm'
else
let val xp = (HOLogic.mk_binop "HOL.plus"
- ((HOLogic.mk_binop "HOL.times" ((mk_numeral 1), x )), zero))
+ ((HOLogic.mk_binop "HOL.times" ((mk_number 1), x )), zero))
in
- HOLogic.conj $(HOLogic.mk_binrel "Divides.dvd" ((mk_numeral l) , xp )) $ (adjustcoeff x l fm)
+ HOLogic.conj $(HOLogic.mk_binrel "Divides.dvd" ((mk_number l) , xp )) $ (adjustcoeff x l fm)
end
end;
@@ -294,9 +294,9 @@
case fm of
(Const(p,_) $d $( Const ("HOL.plus", _)$(Const ("HOL.times",_) $
c $ y ) $z )) => if (is_arith_rel fm) andalso (x = y) then
- let val m = l div (dest_numeral c)
+ let val m = l div (dest_number c)
val n = (if p = "Orderings.less" then abs(m) else m)
- val xtm = (HOLogic.mk_binop "HOL.times" ((mk_numeral ((m div n)*l) ), x))
+ val xtm = (HOLogic.mk_binop "HOL.times" ((mk_number ((m div n)*l) ), x))
in (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) ))))
end
else fm
@@ -320,7 +320,7 @@
|(Const("Orderings.less",_) $ c $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z
)) => if (x = y)
then if (pm1 = one) andalso (c = zero) then HOLogic.false_const
- else if (dest_numeral pm1 = ~1) andalso (c = zero) then HOLogic.true_const
+ else if (dest_number pm1 = ~1) andalso (c = zero) then HOLogic.true_const
else error "minusinf : term not in normal form!!!"
else fm
@@ -341,7 +341,7 @@
|(Const("Orderings.less",_) $ c $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z
)) => if (x = y)
then if (pm1 = one) andalso (c = zero) then HOLogic.true_const
- else if (dest_numeral pm1 = ~1) andalso (c = zero) then HOLogic.false_const
+ else if (dest_number pm1 = ~1) andalso (c = zero) then HOLogic.false_const
else error "plusinf : term not in normal form!!!"
else fm
@@ -355,7 +355,7 @@
(* ------------------------------------------------------------------------- *)
fun divlcm x (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z ) ) =
- if x = y then abs(dest_numeral d) else 1
+ if x = y then abs(dest_number d) else 1
|divlcm x ( Const ("Not", _) $ p) = divlcm x p
|divlcm x ( Const ("op &",_) $ p $ q) = lcm_num (divlcm x p) (divlcm x q)
|divlcm x ( Const ("op |",_) $ p $ q ) = lcm_num (divlcm x p) (divlcm x q)
@@ -375,7 +375,7 @@
|_ =>[])
else bset x p
- |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_neg(linear_add [] a (mk_numeral 1))] else []
+ |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_neg(linear_add [] a (mk_number 1))] else []
|(Const ("Orderings.less",_) $ c1$ (Const ("HOL.plus",_) $(Const ("HOL.times",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_neg a] else []
|(Const ("op &",_) $ p $ q) => (bset x p) union (bset x q)
|(Const ("op |",_) $ p $ q) => (bset x p) union (bset x q)
@@ -395,8 +395,8 @@
|_ =>[])
else aset x p
- |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_sub [] (mk_numeral 1) a] else []
- |(Const ("Orderings.less",_) $ c1$ (Const ("HOL.plus",_) $(Const ("HOL.times",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = (mk_numeral (~1))) then [a] else []
+ |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_sub [] (mk_number 1) a] else []
+ |(Const ("Orderings.less",_) $ c1$ (Const ("HOL.plus",_) $(Const ("HOL.times",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = (mk_number (~1))) then [a] else []
|(Const ("op &",_) $ p $ q) => (aset x p) union (aset x q)
|(Const ("op |",_) $ p $ q) => (aset x p) union (aset x q)
|_ => [];
@@ -410,7 +410,7 @@
((Const(p,_)$ d $ (Const("HOL.plus",_)$(Const("HOL.times",_)$ c $ y) $ z))) =>
if (x = y) andalso (is_arith_rel fm)
then
- let val ct = linear_cmul (dest_numeral c) t
+ let val ct = linear_cmul (dest_number c) t
in (HOLogic.mk_binrel p (d, linear_add vars ct z))
end
else fm
@@ -430,16 +430,16 @@
fun dvd_op (d, t) =
if not(is_numeral d) then raise DVD_UNKNOWN
else let
- val dn = dest_numeral d
+ val dn = dest_number d
fun coeffs_of x = case x of
Const(p,_) $ tl $ tr =>
if p = "HOL.plus" then (coeffs_of tl) union (coeffs_of tr)
else if p = "HOL.times"
then if (is_numeral tr)
- then [(dest_numeral tr) * (dest_numeral tl)]
- else [dest_numeral tl]
+ then [(dest_number tr) * (dest_number tl)]
+ else [dest_number tl]
else []
- |_ => if (is_numeral t) then [dest_numeral t] else []
+ |_ => if (is_numeral t) then [dest_number t] else []
val ts = coeffs_of t
in case ts of
[] => raise DVD_UNKNOWN
@@ -466,12 +466,12 @@
handle _ => at)
else
case AList.lookup (op =) operations p of
- SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const else HOLogic.false_const)
+ SOME f => ((if (f ((dest_number s),(dest_number t))) then HOLogic.true_const else HOLogic.false_const)
handle _ => at)
| _ => at)
|Const("Not",_)$(Const (p,_) $ s $ t) =>(
case AList.lookup (op =) operations p of
- SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then
+ SOME f => ((if (f ((dest_number s),(dest_number t))) then
HOLogic.false_const else HOLogic.true_const)
handle _ => at)
| _ => at)
@@ -482,13 +482,13 @@
fun evalc_atom at = case at of
(Const (p,_) $ s $ t) =>
( case AList.lookup (op =) operations p of
- SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const
+ SOME f => ((if (f ((dest_number s),(dest_number t))) then HOLogic.true_const
else HOLogic.false_const)
handle _ => at)
| _ => at)
|Const("Not",_)$(Const (p,_) $ s $ t) =>(
case AList.lookup (op =) operations p of
- SOME f => ((if (f ((dest_numeral s),(dest_numeral t)))
+ SOME f => ((if (f ((dest_number s),(dest_number t)))
then HOLogic.false_const else HOLogic.true_const)
handle _ => at)
| _ => at)
@@ -659,8 +659,8 @@
|mk_uni_vars T (Free (v,_)) = Free (v,T)
|mk_uni_vars T tm = tm;
-fun mk_uni_int T (Const ("HOL.zero",T2)) = if T = T2 then (mk_numeral 0) else (Const ("HOL.zero",T2))
- |mk_uni_int T (Const ("HOL.one",T2)) = if T = T2 then (mk_numeral 1) else (Const ("HOL.one",T2))
+fun mk_uni_int T (Const ("HOL.zero",T2)) = if T = T2 then (mk_number 0) else (Const ("HOL.zero",T2))
+ |mk_uni_int T (Const ("HOL.one",T2)) = if T = T2 then (mk_number 1) else (Const ("HOL.one",T2))
|mk_uni_int T (node $ rest) = (mk_uni_int T node) $ (mk_uni_int T rest )
|mk_uni_int T (Abs(AV,AT,p)) = Abs(AV,AT,mk_uni_int T p)
|mk_uni_int T tm = tm;
@@ -680,8 +680,8 @@
val p_inf = simpl (minusinf x p)
val bset = bset x p
val js = myupto 1 (divlcm x p)
- fun p_element j b = linrep vars x (linear_add vars b (mk_numeral j)) p
- fun stage j = list_disj (linrep vars x (mk_numeral j) p_inf :: map (p_element j) bset)
+ fun p_element j b = linrep vars x (linear_add vars b (mk_number j)) p
+ fun stage j = list_disj (linrep vars x (mk_number j) p_inf :: map (p_element j) bset)
in (list_disj (map stage js))
end
| _ => error "cooper: not an existential formula";
@@ -699,8 +699,8 @@
val p_inf = simpl (plusinf x p)
val aset = aset x p
val js = myupto 1 (divlcm x p)
- fun p_element j a = linrep vars x (linear_sub vars a (mk_numeral j)) p
- fun stage j = list_disj (linrep vars x (mk_numeral j) p_inf :: map (p_element j) aset)
+ fun p_element j a = linrep vars x (linear_sub vars a (mk_number j)) p
+ fun stage j = list_disj (linrep vars x (mk_number j) p_inf :: map (p_element j) aset)
in (list_disj (map stage js))
end
| _ => error "cooper: not an existential formula";
@@ -711,13 +711,13 @@
fun inf_w mi d vars x p =
let val f = if mi then minusinf else plusinf in
case (simpl (minusinf x p)) of
- Const("True",_) => (SOME (mk_numeral 1), HOLogic.true_const)
+ Const("True",_) => (SOME (mk_number 1), HOLogic.true_const)
|Const("False",_) => (NONE,HOLogic.false_const)
|F =>
let
fun h n =
- case ((simpl o evalc) (linrep vars x (mk_numeral n) F)) of
- Const("True",_) => (SOME (mk_numeral n),HOLogic.true_const)
+ case ((simpl o evalc) (linrep vars x (mk_number n) F)) of
+ Const("True",_) => (SOME (mk_number n),HOLogic.true_const)
|F' => if n=1 then (NONE,F')
else let val (rw,rf) = h (n-1) in
(rw,HOLogic.mk_disj(F',rf))
@@ -736,7 +736,7 @@
in (rw,HOLogic.mk_disj(F',rf))
end)
val f = if b then linear_add else linear_sub
- val p_elements = fold_rev (fn i => fn l => l union (map (fn e => f [] e (mk_numeral i)) st)) (myupto 1 d) []
+ val p_elements = fold_rev (fn i => fn l => l union (map (fn e => f [] e (mk_number i)) st)) (myupto 1 d) []
in h p_elements
end;
@@ -769,8 +769,8 @@
if (length bst) <= (length ast)
then (simpl (minusinf x p),linear_add,bst)
else (simpl (plusinf x p), linear_sub,ast)
- fun p_element j a = linrep vars x (f vars a (mk_numeral j)) p
- fun stage j = list_disj (linrep vars x (mk_numeral j) p_inf :: map (p_element j) S)
+ fun p_element j a = linrep vars x (f vars a (mk_number j)) p
+ fun stage j = list_disj (linrep vars x (mk_number j) p_inf :: map (p_element j) S)
fun stageh n = ((if n = 0 then []
else
let
@@ -805,8 +805,8 @@
then (true,bst)
else (false,ast)
in withness d p_inf S vars x p
-(* fun p_element j a = linrep vars x (f vars a (mk_numeral j)) p
- fun stage j = list_disj (linrep vars x (mk_numeral j) p_inf :: map (p_element j) S)
+(* fun p_element j a = linrep vars x (f vars a (mk_number j)) p
+ fun stage j = list_disj (linrep vars x (mk_number j) p_inf :: map (p_element j) S)
in (list_disj (map stage js))
*)
end
--- a/src/HOL/Integ/cooper_proof.ML Wed Dec 13 15:45:30 2006 +0100
+++ b/src/HOL/Integ/cooper_proof.ML Wed Dec 13 15:45:31 2006 +0100
@@ -33,7 +33,7 @@
val presburger_ss = simpset ()
addsimps [diff_int_def] delsimps [thm "diff_int_def_symmetric"];
-val cboolT = ctyp_of (sign_of HOL.thy) HOLogic.boolT;
+val cboolT = ctyp_of HOL.thy HOLogic.boolT;
(*Theorems that will be used later for the proofgeneration*)
@@ -163,7 +163,7 @@
fun norm_zero_one fm = case fm of
(Const ("HOL.times",_) $ c $ t) =>
if c = one then (norm_zero_one t)
- else if (dest_numeral c = ~1)
+ else if (dest_number c = ~1)
then (Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $ (norm_zero_one t))
else (HOLogic.mk_binop "HOL.times" (norm_zero_one c,norm_zero_one t))
|(node $ rest) => ((norm_zero_one node)$(norm_zero_one rest))
@@ -253,18 +253,18 @@
fun decomp_adjustcoeffeq sg x l fm = case fm of
(Const("Not",_)$(Const("Orderings.less",_) $(Const("HOL.zero",_)) $(rt as (Const ("HOL.plus", _)$(Const ("HOL.times",_) $ c $ y ) $z )))) =>
let
- val m = l div (dest_numeral c)
+ val m = l div (dest_number c)
val n = if (x = y) then abs (m) else 1
- val xtm = (HOLogic.mk_binop "HOL.times" ((mk_numeral ((m div n)*l) ), x))
+ val xtm = (HOLogic.mk_binop "HOL.times" ((mk_number ((m div n)*l) ), x))
val rs = if (x = y)
- then (HOLogic.mk_binrel "Orderings.less" (zero,linear_sub [] (mk_numeral n) (HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) ))))
+ then (HOLogic.mk_binrel "Orderings.less" (zero,linear_sub [] (mk_number n) (HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) ))))
else HOLogic.mk_binrel "Orderings.less" (zero,linear_sub [] one rt )
- val ck = cterm_of sg (mk_numeral n)
+ val ck = cterm_of sg (mk_number n)
val cc = cterm_of sg c
val ct = cterm_of sg z
val cx = cterm_of sg y
val pre = prove_elementar sg "lf"
- (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),(mk_numeral n)))
+ (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),(mk_number n)))
val th1 = (pre RS (instantiate' [] [SOME ck,SOME cc, SOME cx, SOME ct] (ac_pi_eq)))
in ([], fn [] => [th1,(prove_elementar sg "sa" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
end
@@ -273,12 +273,12 @@
c $ y ) $t )) =>
if (is_arith_rel fm) andalso (x = y)
then
- let val m = l div (dest_numeral c)
+ let val m = l div (dest_number c)
val k = (if p = "Orderings.less" then abs(m) else m)
- val xtm = (HOLogic.mk_binop "HOL.times" ((mk_numeral ((m div k)*l) ), x))
+ val xtm = (HOLogic.mk_binop "HOL.times" ((mk_number ((m div k)*l) ), x))
val rs = (HOLogic.mk_binrel p ((linear_cmul k a),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul k t) ))))
- val ck = cterm_of sg (mk_numeral k)
+ val ck = cterm_of sg (mk_number k)
val cc = cterm_of sg c
val ct = cterm_of sg t
val cx = cterm_of sg x
@@ -288,21 +288,21 @@
case p of
"Orderings.less" =>
let val pre = prove_elementar sg "lf"
- (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),(mk_numeral k)))
+ (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),(mk_number k)))
val th1 = (pre RS (instantiate' [] [SOME ck,SOME ca,SOME cc, SOME cx, SOME ct] (ac_lt_eq)))
in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
end
|"op =" =>
let val pre = prove_elementar sg "lf"
- (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("HOL.zero",HOLogic.intT),(mk_numeral k))))
+ (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("HOL.zero",HOLogic.intT),(mk_number k))))
val th1 = (pre RS(instantiate' [] [SOME ck,SOME ca,SOME cc, SOME cx, SOME ct] (ac_eq_eq)))
in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
end
|"Divides.dvd" =>
let val pre = prove_elementar sg "lf"
- (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("HOL.zero",HOLogic.intT),(mk_numeral k))))
+ (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("HOL.zero",HOLogic.intT),(mk_number k))))
val th1 = (pre RS (instantiate' [] [SOME ck,SOME ca,SOME cc, SOME cx, SOME ct]) (ac_dvd_eq))
in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
@@ -574,7 +574,7 @@
|(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", T) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
if (is_arith_rel at) andalso (x=y)
- then let val bst_z = norm_zero_one (linear_neg (linear_add [] z (mk_numeral 1)))
+ then let val bst_z = norm_zero_one (linear_neg (linear_add [] z (mk_number 1)))
in let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ bst_z $ B)
val th2 = prove_elementar sg "ss" (HOLogic.mk_eq (bst_z,Const("HOL.minus",T) $ (Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ (Const("HOL.one",HOLogic.intT))))
val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),dlcm))
@@ -675,7 +675,7 @@
|(Const("Orderings.less",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
if (y=x) andalso (c1 =zero) then
- if pm1 = (mk_numeral ~1) then
+ if pm1 = (mk_number ~1) then
let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one z) $ A)
val th2 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (zero,dlcm))
in (instantiate' [] [SOME cfma]([th2,th1] MRS (not_ast_p_lt)))
@@ -734,7 +734,7 @@
(Const (p,_) $ s $ t) =>(
case AList.lookup (op =) operations p of
SOME f =>
- ((if (f ((dest_numeral s),(dest_numeral t)))
+ ((if (f ((dest_number s),(dest_number t)))
then prove_elementar sg "ss" (HOLogic.mk_eq(at,HOLogic.true_const))
else prove_elementar sg "ss" (HOLogic.mk_eq(at, HOLogic.false_const)))
handle _ => instantiate' [SOME cboolT] [SOME (cterm_of sg at)] refl)
@@ -742,7 +742,7 @@
|Const("Not",_)$(Const (p,_) $ s $ t) =>(
case AList.lookup (op =) operations p of
SOME f =>
- ((if (f ((dest_numeral s),(dest_numeral t)))
+ ((if (f ((dest_number s),(dest_number t)))
then prove_elementar sg "ss" (HOLogic.mk_eq(at, HOLogic.false_const))
else prove_elementar sg "ss" (HOLogic.mk_eq(at,HOLogic.true_const)))
handle _ => instantiate' [SOME cboolT] [SOME (cterm_of sg at)] refl)
@@ -842,14 +842,14 @@
val ss = presburger_ss addsimps
[simp_from_to] delsimps [P_eqtrue, P_eqfalse, bex_triv, insert_iff]
(* uth : EX x.P(l*x) = EX x. l dvd x & P x*)
- val uth = instantiate' [] [SOME (cterm_of sg P) , SOME (cterm_of sg (mk_numeral l))] (unity_coeff_ex)
+ val uth = instantiate' [] [SOME (cterm_of sg P) , SOME (cterm_of sg (mk_number l))] (unity_coeff_ex)
(* e_ac_thm : Ex x. efm = EX x. fm*)
val e_ac_thm = (forall_intr (cterm_of sg x) ac_thm) COMP (qe_exI)
(* A and B set of the formula*)
val A = aset x cfm
val B = bset x cfm
(* the divlcm (delta) of the formula*)
- val dlcm = mk_numeral (divlcm x cfm)
+ val dlcm = mk_number (divlcm x cfm)
(* Which set is smaller to generate the (hoepfully) shorter proof*)
val cms = if ((length A) < (length B )) then "pi" else "mi"
(* val _ = if cms = "pi" then writeln "Plusinfinity" else writeln "Minusinfinity"*)
@@ -906,7 +906,7 @@
val ss = presburger_ss addsimps
[simp_from_to] delsimps [P_eqtrue, P_eqfalse, bex_triv, insert_iff]
(* uth : EX x.P(l*x) = EX x. l dvd x & P x*)
- val uth = instantiate' [] [SOME (cterm_of sg P) , SOME (cterm_of sg (mk_numeral l))] (unity_coeff_ex)
+ val uth = instantiate' [] [SOME (cterm_of sg P) , SOME (cterm_of sg (mk_number l))] (unity_coeff_ex)
(* e_ac_thm : Ex x. efm = EX x. fm*)
val e_ac_thm = (forall_intr (cterm_of sg x) ac_thm) COMP (qe_exI)
(* lsuth = EX.P(l*x) ; rsuth = EX x. l dvd x & P x*)
@@ -923,7 +923,7 @@
val A = aset x cfm
val B = bset x cfm
(* the divlcm (delta) of the formula*)
- val dlcm = mk_numeral (divlcm x cfm)
+ val dlcm = mk_number (divlcm x cfm)
(* Which set is smaller to generate the (hoepfully) shorter proof*)
val cms = if ((length A) < (length B )) then "pi" else "mi"
(* synthesize the proof of cooper's theorem*)
--- a/src/HOL/Integ/int_arith1.ML Wed Dec 13 15:45:30 2006 +0100
+++ b/src/HOL/Integ/int_arith1.ML Wed Dec 13 15:45:31 2006 +0100
@@ -160,7 +160,7 @@
(case numterm_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
| numterm_ord
(Const("Numeral.number_of", _) $ v, Const("Numeral.number_of", _) $ w) =
- num_ord (HOLogic.dest_binum v, HOLogic.dest_binum w)
+ num_ord (HOLogic.dest_numeral v, HOLogic.dest_numeral w)
| numterm_ord (Const("Numeral.number_of", _) $ _, _) = LESS
| numterm_ord (_, Const("Numeral.number_of", _) $ _) = GREATER
| numterm_ord (t, u) =
@@ -181,18 +181,18 @@
(** Utilities **)
-fun mk_numeral T n = HOLogic.number_of_const T $ HOLogic.mk_binum n;
+fun mk_number T n = HOLogic.number_of_const T $ HOLogic.mk_numeral n;
(*Decodes a binary INTEGER*)
-fun dest_numeral (Const("HOL.zero", _)) = 0
- | dest_numeral (Const("HOL.one", _)) = 1
- | dest_numeral (Const("Numeral.number_of", _) $ w) =
- (HOLogic.dest_binum w
- handle TERM _ => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w]))
- | dest_numeral t = raise TERM("Int_Numeral_Simprocs.dest_numeral:2", [t]);
+fun dest_number (Const("HOL.zero", _)) = 0
+ | dest_number (Const("HOL.one", _)) = 1
+ | dest_number (Const("Numeral.number_of", _) $ w) =
+ (HOLogic.dest_numeral w
+ handle TERM _ => raise TERM("Int_Numeral_Simprocs.dest_number:1", [w]))
+ | dest_number t = raise TERM("Int_Numeral_Simprocs.dest_number:2", [t]);
fun find_first_numeral past (t::terms) =
- ((dest_numeral t, rev past @ terms)
+ ((dest_number t, rev past @ terms)
handle TERM _ => find_first_numeral (t::past) terms)
| find_first_numeral past [] = raise TERM("find_first_numeral", []);
@@ -204,12 +204,12 @@
end;
(*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)
-fun mk_sum T [] = mk_numeral T 0
+fun mk_sum T [] = mk_number T 0
| mk_sum T [t,u] = mk_plus (t, u)
| mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts);
(*this version ALWAYS includes a trailing zero*)
-fun long_mk_sum T [] = mk_numeral T 0
+fun long_mk_sum T [] = mk_number T 0
| long_mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts);
val dest_plus = HOLogic.dest_bin "HOL.plus" Term.dummyT;
@@ -230,14 +230,14 @@
val mk_times = HOLogic.mk_binop "HOL.times";
fun mk_prod T =
- let val one = mk_numeral T 1
+ let val one = mk_number T 1
fun mk [] = one
| mk [t] = t
| mk (t :: ts) = if t = one then mk ts else mk_times (t, mk ts)
in mk end;
(*This version ALWAYS includes a trailing one*)
-fun long_mk_prod T [] = mk_numeral T 1
+fun long_mk_prod T [] = mk_number T 1
| long_mk_prod T (t :: ts) = mk_times (t, mk_prod T ts);
val dest_times = HOLogic.dest_bin "HOL.times" Term.dummyT;
@@ -248,7 +248,7 @@
handle TERM _ => [t];
(*DON'T do the obvious simplifications; that would create special cases*)
-fun mk_coeff (k, t) = mk_times (mk_numeral (Term.fastype_of t) k, t);
+fun mk_coeff (k, t) = mk_times (mk_number (Term.fastype_of t) k, t);
(*Express t as a product of (possibly) a numeral with other sorted terms*)
fun dest_coeff sign (Const ("HOL.uminus", _) $ t) = dest_coeff (~sign) t
--- a/src/HOL/Integ/nat_simprocs.ML Wed Dec 13 15:45:30 2006 +0100
+++ b/src/HOL/Integ/nat_simprocs.ML Wed Dec 13 15:45:31 2006 +0100
@@ -23,22 +23,22 @@
(*Utilities*)
-fun mk_numeral n = HOLogic.number_of_const HOLogic.natT $ HOLogic.mk_binum n;
+fun mk_number n = HOLogic.number_of_const HOLogic.natT $ HOLogic.mk_numeral n;
(*Decodes a unary or binary numeral to a NATURAL NUMBER*)
-fun dest_numeral (Const ("HOL.zero", _)) = 0
- | dest_numeral (Const ("Suc", _) $ t) = 1 + dest_numeral t
- | dest_numeral (Const("Numeral.number_of", _) $ w) =
- (IntInf.max (0, HOLogic.dest_binum w)
- handle TERM _ => raise TERM("Nat_Numeral_Simprocs.dest_numeral:1", [w]))
- | dest_numeral t = raise TERM("Nat_Numeral_Simprocs.dest_numeral:2", [t]);
+fun dest_number (Const ("HOL.zero", _)) = 0
+ | dest_number (Const ("Suc", _) $ t) = 1 + dest_number t
+ | dest_number (Const("Numeral.number_of", _) $ w) =
+ (IntInf.max (0, HOLogic.dest_numeral w)
+ handle TERM _ => raise TERM("Nat_Numeral_Simprocs.dest_number:1", [w]))
+ | dest_number t = raise TERM("Nat_Numeral_Simprocs.dest_number:2", [t]);
fun find_first_numeral past (t::terms) =
- ((dest_numeral t, t, rev past @ terms)
+ ((dest_number t, t, rev past @ terms)
handle TERM _ => find_first_numeral (t::past) terms)
| find_first_numeral past [] = raise TERM("find_first_numeral", []);
-val zero = mk_numeral 0;
+val zero = mk_number 0;
val mk_plus = HOLogic.mk_binop "HOL.plus";
(*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)
@@ -72,7 +72,7 @@
(*** CancelNumerals simprocs ***)
-val one = mk_numeral 1;
+val one = mk_number 1;
val mk_times = HOLogic.mk_binop "HOL.times";
fun mk_prod [] = one
@@ -88,7 +88,7 @@
handle TERM _ => [t];
(*DON'T do the obvious simplifications; that would create special cases*)
-fun mk_coeff (k,t) = mk_times (mk_numeral k, t);
+fun mk_coeff (k,t) = mk_times (mk_number k, t);
(*Express t as a product of (possibly) a numeral with other factors, sorted*)
fun dest_coeff t =
@@ -130,7 +130,7 @@
in
if relaxed orelse exists prod_has_numeral ts then
if k=0 then ts
- else mk_numeral (IntInf.fromInt k) :: ts
+ else mk_number (IntInf.fromInt k) :: ts
else raise TERM("Nat_Numeral_Simprocs.dest_Sucs_sum", [t])
end;
--- a/src/HOL/Integ/reflected_cooper.ML Wed Dec 13 15:45:30 2006 +0100
+++ b/src/HOL/Integ/reflected_cooper.ML Wed Dec 13 15:45:31 2006 +0100
@@ -20,7 +20,7 @@
| Const ("HOL.plus",_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
| Const ("HOL.minus",_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
| Const ("HOL.times",_)$t1$t2 => Mult (i_of_term vs t1,i_of_term vs t2)
- | Const ("Numeral.number_of",_)$t' => Cst (HOLogic.dest_binum t')
+ | Const ("Numeral.number_of",_)$t' => Cst (HOLogic.dest_numeral t')
| _ => error "i_of_term: unknown term";
@@ -75,7 +75,7 @@
fun term_of_i vs t =
case t of
- Cst i => CooperDec.mk_numeral i
+ Cst i => CooperDec.mk_number i
| Var n => valOf (myassoc2 vs n)
| Neg t' => Const("HOL.uminus",iT --> iT)$(term_of_i vs t')
| Add(t1,t2) => Const("HOL.plus",[iT,iT] ---> iT)$
--- a/src/HOL/Library/EfficientNat.thy Wed Dec 13 15:45:30 2006 +0100
+++ b/src/HOL/Library/EfficientNat.thy Wed Dec 13 15:45:31 2006 +0100
@@ -140,10 +140,7 @@
types_code
nat ("int")
attach (term_of) {*
-fun term_of_nat 0 = Const ("HOL.zero", HOLogic.natT)
- | term_of_nat 1 = Const ("HOL.one", HOLogic.natT)
- | term_of_nat i = HOLogic.number_of_const HOLogic.natT $
- HOLogic.mk_binum (IntInf.fromInt i);
+val term_of_nat = HOLogic.mk_number HOLogic.natT o InfInf.fromInt;
*}
attach (test) {*
fun gen_nat i = random_range 0 i;
--- a/src/HOL/Real/ferrante_rackoff_proof.ML Wed Dec 13 15:45:30 2006 +0100
+++ b/src/HOL/Real/ferrante_rackoff_proof.ML Wed Dec 13 15:45:31 2006 +0100
@@ -289,15 +289,8 @@
(* Normalization of arithmetical expressions *)
val rzero = Const("HOL.zero",rT);
val rone = Const("HOL.one",rT);
-fun mk_real i =
- case i of
- 0 => rzero
- | 1 => rone
- | _ => (HOLogic.number_of_const rT)$(HOLogic.mk_binum i);
-
-fun dest_real (Const("HOL.zero",_)) = 0
- | dest_real (Const("HOL.one",_)) = 1
- | dest_real (Const("Numeral.number_of",_)$b) = HOLogic.dest_binum b;
+fun mk_real i = HOLogic.mk_number rT i;
+val dest_real = snd o HOLogic.dest_number;
(* Normal form for terms is:
(c0*x0 + ... + cn*xn + k) / c , where ci!=0 and x0<..<xn ordered according to vs*)
--- a/src/HOL/Real/float.ML Wed Dec 13 15:45:30 2006 +0100
+++ b/src/HOL/Real/float.ML Wed Dec 13 15:45:31 2006 +0100
@@ -13,35 +13,35 @@
type floatrep = IntInf.int * IntInf.int
val approx_dec_by_bin : IntInf.int -> floatrep -> floatrep * floatrep
val approx_decstr_by_bin : int -> string -> floatrep * floatrep
-end
+end
=
struct
exception Destruct_floatstr of string;
-fun destruct_floatstr isDigit isExp number =
+fun destruct_floatstr isDigit isExp number =
let
val numlist = filter (not o Char.isSpace) (String.explode number)
-
+
fun countsigns ((#"+")::cs) = countsigns cs
- | countsigns ((#"-")::cs) =
- let
- val (positive, rest) = countsigns cs
+ | countsigns ((#"-")::cs) =
+ let
+ val (positive, rest) = countsigns cs
in
(not positive, rest)
end
| countsigns cs = (true, cs)
fun readdigits [] = ([], [])
- | readdigits (q as c::cs) =
- if (isDigit c) then
+ | readdigits (q as c::cs) =
+ if (isDigit c) then
let
val (digits, rest) = readdigits cs
in
(c::digits, rest)
end
else
- ([], q)
+ ([], q)
fun readfromexp_helper cs =
let
@@ -51,27 +51,27 @@
case rest' of
[] => (positive, digits)
| _ => raise (Destruct_floatstr number)
- end
+ end
fun readfromexp [] = (true, [])
- | readfromexp (c::cs) =
+ | readfromexp (c::cs) =
if isExp c then
readfromexp_helper cs
- else
- raise (Destruct_floatstr number)
+ else
+ raise (Destruct_floatstr number)
fun readfromdot [] = ([], readfromexp [])
- | readfromdot ((#".")::cs) =
- let
+ | readfromdot ((#".")::cs) =
+ let
val (digits, rest) = readdigits cs
val exp = readfromexp rest
in
(digits, exp)
- end
+ end
| readfromdot cs = readfromdot ((#".")::cs)
-
- val (positive, numlist) = countsigns numlist
- val (digits1, numlist) = readdigits numlist
+
+ val (positive, numlist) = countsigns numlist
+ val (digits1, numlist) = readdigits numlist
val (digits2, exp) = readfromdot numlist
in
(positive, String.implode digits1, String.implode digits2, fst exp, String.implode (snd exp))
@@ -82,10 +82,10 @@
exception Floating_point of string;
val ln2_10 = (Math.ln 10.0)/(Math.ln 2.0)
-
+
fun intmul a b = IntInf.* (a,b)
-fun intsub a b = IntInf.- (a,b)
-fun intadd a b = IntInf.+ (a,b)
+fun intsub a b = IntInf.- (a,b)
+fun intadd a b = IntInf.+ (a,b)
fun intpow a b = IntInf.pow (a, IntInf.toInt b);
fun intle a b = IntInf.<= (a, b);
fun intless a b = IntInf.< (a, b);
@@ -96,33 +96,33 @@
val ten = IntInf.fromInt 10;
val five = IntInf.fromInt 5;
-fun find_most_significant q r =
- let
- fun int2real i =
- case Real.fromString (IntInf.toString i) of
- SOME r => r
- | NONE => raise (Floating_point "int2real")
- fun subtract (q, r) (q', r') =
+fun find_most_significant q r =
+ let
+ fun int2real i =
+ case Real.fromString (IntInf.toString i) of
+ SOME r => r
+ | NONE => raise (Floating_point "int2real")
+ fun subtract (q, r) (q', r') =
if intle r r' then
(intsub q (intmul q' (intpow ten (intsub r' r))), r)
else
(intsub (intmul q (intpow ten (intsub r r'))) q', r')
fun bin2dec d =
- if intle zero d then
+ if intle zero d then
(intpow two d, zero)
else
- (intpow five (intneg d), d)
-
- val L = IntInf.fromInt (Real.floor (int2real (IntInf.fromInt (IntInf.log2 q)) + (int2real r) * ln2_10))
+ (intpow five (intneg d), d)
+
+ val L = IntInf.fromInt (Real.floor (int2real (IntInf.fromInt (IntInf.log2 q)) + (int2real r) * ln2_10))
val L1 = intadd L one
- val (q1, r1) = subtract (q, r) (bin2dec L1)
+ val (q1, r1) = subtract (q, r) (bin2dec L1)
in
- if intle zero q1 then
+ if intle zero q1 then
let
val (q2, r2) = subtract (q, r) (bin2dec (intadd L1 one))
in
- if intle zero q2 then
+ if intle zero q2 then
raise (Floating_point "find_most_significant")
else
(L1, (q1, r1))
@@ -135,76 +135,76 @@
(L, (q0, r0))
else
raise (Floating_point "find_most_significant")
- end
+ end
end
fun approx_dec_by_bin n (q,r) =
- let
+ let
fun addseq acc d' [] = acc
| addseq acc d' (d::ds) = addseq (intadd acc (intpow two (intsub d d'))) d' ds
fun seq2bin [] = (zero, zero)
| seq2bin (d::ds) = (intadd (addseq zero d ds) one, d)
- fun approx d_seq d0 precision (q,r) =
- if q = zero then
+ fun approx d_seq d0 precision (q,r) =
+ if q = zero then
let val x = seq2bin d_seq in
(x, x)
end
- else
- let
+ else
+ let
val (d, (q', r')) = find_most_significant q r
- in
- if intless precision (intsub d0 d) then
- let
+ in
+ if intless precision (intsub d0 d) then
+ let
val d' = intsub d0 precision
val x1 = seq2bin (d_seq)
- val x2 = (intadd (intmul (fst x1) (intpow two (intsub (snd x1) d'))) one, d') (* = seq2bin (d'::d_seq) *)
+ val x2 = (intadd (intmul (fst x1) (intpow two (intsub (snd x1) d'))) one, d') (* = seq2bin (d'::d_seq) *)
in
(x1, x2)
end
else
- approx (d::d_seq) d0 precision (q', r')
- end
-
+ approx (d::d_seq) d0 precision (q', r')
+ end
+
fun approx_start precision (q, r) =
- if q = zero then
+ if q = zero then
((zero, zero), (zero, zero))
else
- let
+ let
val (d, (q', r')) = find_most_significant q r
- in
- if intle precision zero then
+ in
+ if intle precision zero then
let
val x1 = seq2bin [d]
in
- if q' = zero then
+ if q' = zero then
(x1, x1)
else
(x1, seq2bin [intadd d one])
end
else
approx [d] d precision (q', r')
- end
+ end
in
- if intle zero q then
+ if intle zero q then
approx_start n (q,r)
else
- let
- val ((a1,b1), (a2, b2)) = approx_start n (intneg q, r)
+ let
+ val ((a1,b1), (a2, b2)) = approx_start n (intneg q, r)
in
((intneg a2, b2), (intneg a1, b1))
- end
+ end
end
fun approx_decstr_by_bin n decstr =
- let
- fun str2int s = case IntInf.fromString s of SOME x => x | NONE => zero
+ let
+ fun str2int s = case IntInf.fromString s of SOME x => x | NONE => zero
fun signint p x = if p then x else intneg x
val (p, d1, d2, ep, e) = destruct_floatstr Char.isDigit (fn e => e = #"e" orelse e = #"E") decstr
val s = IntInf.fromInt (size d2)
-
+
val q = signint p (intadd (intmul (str2int d1) (intpow ten s)) (str2int d2))
val r = intsub (signint ep (str2int e)) s
in
@@ -213,10 +213,10 @@
end;
-structure FloatArith =
+structure FloatArith =
struct
-type float = IntInf.int * IntInf.int
+type float = IntInf.int * IntInf.int
val izero = IntInf.fromInt 0
val ione = IntInf.fromInt 1
@@ -228,30 +228,30 @@
val floatzero = (izero, izero)
-fun positive_part (a,b) =
+fun positive_part (a,b) =
(if IntInf.< (a,izero) then izero else a, b)
-fun negative_part (a,b) =
+fun negative_part (a,b) =
(if IntInf.< (a,izero) then a else izero, b)
-fun is_negative (a,b) =
+fun is_negative (a,b) =
if IntInf.< (a, izero) then true else false
-fun is_positive (a,b) =
+fun is_positive (a,b) =
if IntInf.< (izero, a) then true else false
-fun is_zero (a,b) =
+fun is_zero (a,b) =
if a = izero then true else false
fun ipow2 a = IntInf.pow ((IntInf.fromInt 2), IntInf.toInt a)
-fun add (a1, b1) (a2, b2) =
+fun add (a1, b1) (a2, b2) =
if IntInf.< (b1, b2) then
(iadd a1 (imul a2 (ipow2 (isub b2 b1))), b1)
else
(iadd (imul a1 (ipow2 (isub b1 b2))) a2, b2)
-fun sub (a1, b1) (a2, b2) =
+fun sub (a1, b1) (a2, b2) =
if IntInf.< (b1, b2) then
(isub a1 (imul a2 (ipow2 (isub b2 b1))), b1)
else
@@ -285,7 +285,7 @@
exception Dest_intinf;
val dest_intinf : term -> IntInf.int
val dest_nat : term -> IntInf.int
-
+
exception Dest_float;
val dest_float : term -> float
@@ -297,7 +297,7 @@
val float_pprt_const : term
val float_nprt_const : term
val float_abs_const : term
- val float_mult_const : term
+ val float_mult_const : term
val float_le_const : term
val nat_le_const : term
@@ -314,8 +314,8 @@
val invoke_float_op : term -> thm
val invoke_nat_op : term -> thm*)
-end
-=
+end
+=
struct
structure Inttab = TableFun(type key = int val ord = (rev_order o int_ord));
@@ -337,64 +337,31 @@
val nat_le_const = Const ("Orderings.less_eq", HOLogic.natT --> HOLogic.natT --> HOLogic.boolT)
val nat_less_const = Const ("Orderings.less", HOLogic.natT --> HOLogic.natT --> HOLogic.boolT)
val nat_eq_const = Const ("op =", HOLogic.natT --> HOLogic.natT --> HOLogic.boolT)
-
+
val zero = FloatArith.izero
val minus_one = FloatArith.imone
val two = FloatArith.itwo
-
+
exception Dest_intinf;
exception Dest_float;
-fun mk_intinf ty n =
- let
- fun mk_bit n = if n = zero then HOLogic.B0_const else HOLogic.B1_const
- fun bin_of n =
- if n = zero then HOLogic.pls_const
- else if n = minus_one then HOLogic.min_const
- else let
- val (q,r) = IntInf.divMod (n, two)
- in
- HOLogic.bit_const $ bin_of q $ mk_bit r
- end
- in
- HOLogic.number_of_const ty $ (bin_of n)
- end
+fun mk_intinf ty n = HOLogic.number_of_const ty $ HOLogic.mk_numeral n;
-fun dest_intinf n =
- let
- fun dest_bit n =
- case n of
- Const ("Numeral.bit.B0", _) => FloatArith.izero
- | Const ("Numeral.bit.B1", _) => FloatArith.ione
- | _ => raise Dest_intinf
-
- fun int_of n =
- case n of
- Const ("Numeral.Pls", _) => FloatArith.izero
- | Const ("Numeral.Min", _) => FloatArith.imone
- | Const ("Numeral.Bit", _) $ q $ r => FloatArith.iadd (FloatArith.imul (int_of q) FloatArith.itwo) (dest_bit r)
- | _ => raise Dest_intinf
- in
- case n of
- Const ("Numeral.number_of", _) $ n' => int_of n'
- | Const ("Numeral0", _) => FloatArith.izero
- | Const ("Numeral1", _) => FloatArith.ione
- | _ => raise Dest_intinf
- end
+val dest_intinf = snd o HOLogic.dest_number
-fun mk_float (a,b) =
+fun mk_float (a,b) =
float_const $ (HOLogic.mk_prod ((mk_intinf HOLogic.intT a), (mk_intinf HOLogic.intT b)))
-fun dest_float f =
- case f of
+fun dest_float f =
+ case f of
(Const ("Float.float", _) $ (Const ("Pair", _) $ a $ b)) => (dest_intinf a, dest_intinf b)
| Const ("Numeral.number_of",_) $ a => (dest_intinf f, 0)
| Const ("Numeral0", _) => (FloatArith.izero, FloatArith.izero)
| Const ("Numeral1", _) => (FloatArith.ione, FloatArith.izero)
| _ => raise Dest_float
-fun dest_nat n =
- let
+fun dest_nat n =
+ let
val v = dest_intinf n
in
if IntInf.< (v, FloatArith.izero) then
@@ -403,7 +370,7 @@
v
end
-fun approx_float prec f value =
+fun approx_float prec f value =
let
val interval = ExactFloatingPoint.approx_decstr_by_bin prec value
val (flower, fupper) = f interval
@@ -415,26 +382,26 @@
fun float_op_oracle (sg, exn as Float_op_oracle_data t) =
Logic.mk_equals (t,
- case t of
- f $ a $ b =>
- let
- val a' = dest_float a
+ case t of
+ f $ a $ b =>
+ let
+ val a' = dest_float a
val b' = dest_float b
in
if f = float_add_const then
- mk_float (FloatArith.add a' b')
+ mk_float (FloatArith.add a' b')
else if f = float_diff_const then
mk_float (FloatArith.sub a' b')
else if f = float_mult_const then
- mk_float (FloatArith.mul a' b')
+ mk_float (FloatArith.mul a' b')
else if f = float_le_const then
(if FloatArith.is_less b' a' then
HOLogic.false_const
else
HOLogic.true_const)
- else raise exn
+ else raise exn
end
- | f $ a =>
+ | f $ a =>
let
val a' = dest_float a
in
@@ -454,7 +421,7 @@
val th = ref ([]: theory list)
val sg = ref ([]: Sign.sg list)
-fun invoke_float_op c =
+fun invoke_float_op c =
let
val th = (if length(!th) = 0 then th := [theory "MatrixLP"] else (); hd (!th))
val sg = (if length(!sg) = 0 then sg := [sign_of th] else (); hd (!sg))
@@ -466,10 +433,10 @@
fun nat_op_oracle (sg, exn as Nat_op_oracle_data t) =
Logic.mk_equals (t,
- case t of
- f $ a $ b =>
- let
- val a' = dest_nat a
+ case t of
+ f $ a $ b =>
+ let
+ val a' = dest_nat a
val b' = dest_nat b
in
if f = nat_le_const then
@@ -478,7 +445,7 @@
else
HOLogic.false_const)
else if f = nat_eq_const then
- (if a' = b' then
+ (if a' = b' then
HOLogic.true_const
else
HOLogic.false_const)
@@ -487,12 +454,13 @@
HOLogic.true_const
else
HOLogic.false_const)
- else
- raise exn
+ else
+ raise exn
+
end
| _ => raise exn)
-fun invoke_nat_op c =
+fun invoke_nat_op c =
let
val th = (if length (!th) = 0 then th := [theory "MatrixLP"] else (); hd (!th))
val sg = (if length (!sg) = 0 then sg := [sign_of th] else (); hd (!sg))
--- a/src/HOL/Tools/Presburger/cooper_dec.ML Wed Dec 13 15:45:30 2006 +0100
+++ b/src/HOL/Tools/Presburger/cooper_dec.ML Wed Dec 13 15:45:31 2006 +0100
@@ -11,8 +11,8 @@
sig
exception COOPER
val is_arith_rel : term -> bool
- val mk_numeral : IntInf.int -> term
- val dest_numeral : term -> IntInf.int
+ val mk_number : IntInf.int -> term
+ val dest_number : term -> IntInf.int
val is_numeral : term -> bool
val zero : term
val one : term
@@ -76,32 +76,32 @@
(*Transform a natural number to a term*)
-fun mk_numeral 0 = Const("HOL.zero",HOLogic.intT)
- |mk_numeral 1 = Const("HOL.one",HOLogic.intT)
- |mk_numeral n = (HOLogic.number_of_const HOLogic.intT) $ (HOLogic.mk_binum n);
+fun mk_number 0 = Const("HOL.zero",HOLogic.intT)
+ |mk_number 1 = Const("HOL.one",HOLogic.intT)
+ |mk_number n = (HOLogic.number_of_const HOLogic.intT) $ (HOLogic.mk_numeral n);
(*Transform an Term to an natural number*)
-fun dest_numeral (Const("HOL.zero",Type ("IntDef.int", []))) = 0
- |dest_numeral (Const("HOL.one",Type ("IntDef.int", []))) = 1
- |dest_numeral (Const ("Numeral.number_of",_) $ n) =
- HOLogic.dest_binum n;
+fun dest_number (Const("HOL.zero",Type ("IntDef.int", []))) = 0
+ |dest_number (Const("HOL.one",Type ("IntDef.int", []))) = 1
+ |dest_number (Const ("Numeral.number_of",_) $ n) =
+ HOLogic.dest_numeral n;
(*Some terms often used for pattern matching*)
-val zero = mk_numeral 0;
-val one = mk_numeral 1;
+val zero = mk_number 0;
+val one = mk_number 1;
(*Tests if a Term is representing a number*)
-fun is_numeral t = (t = zero) orelse (t = one) orelse (can dest_numeral t);
+fun is_numeral t = (t = zero) orelse (t = one) orelse (can dest_number t);
(*maps a unary natural function on a term containing an natural number*)
-fun numeral1 f n = mk_numeral (f(dest_numeral n));
+fun numeral1 f n = mk_number (f(dest_number n));
(*maps a binary natural function on 2 term containing natural numbers*)
-fun numeral2 f m n = mk_numeral(f(dest_numeral m) (dest_numeral n));
+fun numeral2 f m n = mk_number(f(dest_number m) (dest_number n));
(* ------------------------------------------------------------------------- *)
(* Operations on canonical linear terms c1 * x1 + ... + cn * xn + k *)
@@ -178,9 +178,9 @@
Free(x,T)*)
fun lint vars tm = if is_numeral tm then tm else case tm of
- (Free (x,T)) => (HOLogic.mk_binop "HOL.plus" ((HOLogic.mk_binop "HOL.times" ((mk_numeral 1),Free (x,T))), zero))
+ (Free (x,T)) => (HOLogic.mk_binop "HOL.plus" ((HOLogic.mk_binop "HOL.times" ((mk_number 1),Free (x,T))), zero))
|(Bound i) => (Const("HOL.plus",HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $
- (Const("HOL.times",HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ (mk_numeral 1) $ (Bound i)) $ zero)
+ (Const("HOL.times",HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ (mk_number 1) $ (Bound i)) $ zero)
|(Const("HOL.uminus",_) $ t ) => (linear_neg (lint vars t))
|(Const("HOL.plus",_) $ s $ t) => (linear_add vars (lint vars s) (lint vars t))
|(Const("HOL.minus",_) $ s $ t) => (linear_sub vars (lint vars s) (lint vars t))
@@ -188,8 +188,8 @@
let val s' = lint vars s
val t' = lint vars t
in
- if is_numeral s' then (linear_cmul (dest_numeral s') t')
- else if is_numeral t' then (linear_cmul (dest_numeral t') s')
+ if is_numeral s' then (linear_cmul (dest_number s') t')
+ else if is_numeral t' then (linear_cmul (dest_number t') s')
else raise COOPER
end
@@ -205,7 +205,7 @@
fun linform vars (Const ("Divides.dvd",_) $ c $ t) =
if is_numeral c then
- let val c' = (mk_numeral(abs(dest_numeral c)))
+ let val c' = (mk_number(abs(dest_number c)))
in (HOLogic.mk_binrel "Divides.dvd" (c,lint vars t))
end
else (warning "Nonlinear term --- Non numeral leftside at dvd"
@@ -214,11 +214,11 @@
|linform vars (Const("Orderings.less",_)$ s $t ) = (mkatom vars "Orderings.less" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s))
|linform vars (Const("op >",_) $ s $ t ) = (mkatom vars "Orderings.less" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ s $ t))
|linform vars (Const("Orderings.less_eq",_)$ s $ t ) =
- (mkatom vars "Orderings.less" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ (Const("HOL.plus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $t $(mk_numeral 1)) $ s))
+ (mkatom vars "Orderings.less" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ (Const("HOL.plus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $t $(mk_number 1)) $ s))
|linform vars (Const("op >=",_)$ s $ t ) =
(mkatom vars "Orderings.less" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT -->
HOLogic.intT) $ (Const("HOL.plus",HOLogic.intT --> HOLogic.intT -->
- HOLogic.intT) $s $(mk_numeral 1)) $ t))
+ HOLogic.intT) $s $(mk_number 1)) $ t))
|linform vars fm = fm;
@@ -228,7 +228,7 @@
fun posineq fm = case fm of
(Const ("Not",_)$(Const("Orderings.less",_)$ c $ t)) =>
- (HOLogic.mk_binrel "Orderings.less" (zero , (linear_sub [] (mk_numeral 1) (linear_add [] c t ) )))
+ (HOLogic.mk_binrel "Orderings.less" (zero , (linear_sub [] (mk_number 1) (linear_add [] c t ) )))
| ( Const ("op &",_) $ p $ q) => HOLogic.mk_conj (posineq p,posineq q)
| ( Const ("op |",_) $ p $ q ) => HOLogic.mk_disj (posineq p,posineq q)
| _ => fm;
@@ -245,7 +245,7 @@
fun formlcm x fm = case fm of
(Const (p,_)$ _ $(Const ("HOL.plus", _)$(Const ("HOL.times",_)$ c $ y ) $z ) ) => if
- (is_arith_rel fm) andalso (x = y) then (abs(dest_numeral c)) else 1
+ (is_arith_rel fm) andalso (x = y) then (abs(dest_number c)) else 1
| ( Const ("Not", _) $p) => formlcm x p
| ( Const ("op &",_) $ p $ q) => lcm_num (formlcm x p) (formlcm x q)
| ( Const ("op |",_) $ p $ q )=> lcm_num (formlcm x p) (formlcm x q)
@@ -259,9 +259,9 @@
case fm of
(Const(p,_) $d $( Const ("HOL.plus", _)$(Const ("HOL.times",_) $
c $ y ) $z )) => if (is_arith_rel fm) andalso (x = y) then
- let val m = l div (dest_numeral c)
+ let val m = l div (dest_number c)
val n = (if p = "Orderings.less" then abs(m) else m)
- val xtm = HOLogic.mk_binop "HOL.times" ((mk_numeral (m div n)), x)
+ val xtm = HOLogic.mk_binop "HOL.times" ((mk_number (m div n)), x)
in
(HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) ))))
end
@@ -281,9 +281,9 @@
if l = 1 then fm'
else
let val xp = (HOLogic.mk_binop "HOL.plus"
- ((HOLogic.mk_binop "HOL.times" ((mk_numeral 1), x )), zero))
+ ((HOLogic.mk_binop "HOL.times" ((mk_number 1), x )), zero))
in
- HOLogic.conj $(HOLogic.mk_binrel "Divides.dvd" ((mk_numeral l) , xp )) $ (adjustcoeff x l fm)
+ HOLogic.conj $(HOLogic.mk_binrel "Divides.dvd" ((mk_number l) , xp )) $ (adjustcoeff x l fm)
end
end;
@@ -294,9 +294,9 @@
case fm of
(Const(p,_) $d $( Const ("HOL.plus", _)$(Const ("HOL.times",_) $
c $ y ) $z )) => if (is_arith_rel fm) andalso (x = y) then
- let val m = l div (dest_numeral c)
+ let val m = l div (dest_number c)
val n = (if p = "Orderings.less" then abs(m) else m)
- val xtm = (HOLogic.mk_binop "HOL.times" ((mk_numeral ((m div n)*l) ), x))
+ val xtm = (HOLogic.mk_binop "HOL.times" ((mk_number ((m div n)*l) ), x))
in (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) ))))
end
else fm
@@ -320,7 +320,7 @@
|(Const("Orderings.less",_) $ c $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z
)) => if (x = y)
then if (pm1 = one) andalso (c = zero) then HOLogic.false_const
- else if (dest_numeral pm1 = ~1) andalso (c = zero) then HOLogic.true_const
+ else if (dest_number pm1 = ~1) andalso (c = zero) then HOLogic.true_const
else error "minusinf : term not in normal form!!!"
else fm
@@ -341,7 +341,7 @@
|(Const("Orderings.less",_) $ c $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z
)) => if (x = y)
then if (pm1 = one) andalso (c = zero) then HOLogic.true_const
- else if (dest_numeral pm1 = ~1) andalso (c = zero) then HOLogic.false_const
+ else if (dest_number pm1 = ~1) andalso (c = zero) then HOLogic.false_const
else error "plusinf : term not in normal form!!!"
else fm
@@ -355,7 +355,7 @@
(* ------------------------------------------------------------------------- *)
fun divlcm x (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z ) ) =
- if x = y then abs(dest_numeral d) else 1
+ if x = y then abs(dest_number d) else 1
|divlcm x ( Const ("Not", _) $ p) = divlcm x p
|divlcm x ( Const ("op &",_) $ p $ q) = lcm_num (divlcm x p) (divlcm x q)
|divlcm x ( Const ("op |",_) $ p $ q ) = lcm_num (divlcm x p) (divlcm x q)
@@ -375,7 +375,7 @@
|_ =>[])
else bset x p
- |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_neg(linear_add [] a (mk_numeral 1))] else []
+ |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_neg(linear_add [] a (mk_number 1))] else []
|(Const ("Orderings.less",_) $ c1$ (Const ("HOL.plus",_) $(Const ("HOL.times",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_neg a] else []
|(Const ("op &",_) $ p $ q) => (bset x p) union (bset x q)
|(Const ("op |",_) $ p $ q) => (bset x p) union (bset x q)
@@ -395,8 +395,8 @@
|_ =>[])
else aset x p
- |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_sub [] (mk_numeral 1) a] else []
- |(Const ("Orderings.less",_) $ c1$ (Const ("HOL.plus",_) $(Const ("HOL.times",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = (mk_numeral (~1))) then [a] else []
+ |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_sub [] (mk_number 1) a] else []
+ |(Const ("Orderings.less",_) $ c1$ (Const ("HOL.plus",_) $(Const ("HOL.times",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = (mk_number (~1))) then [a] else []
|(Const ("op &",_) $ p $ q) => (aset x p) union (aset x q)
|(Const ("op |",_) $ p $ q) => (aset x p) union (aset x q)
|_ => [];
@@ -410,7 +410,7 @@
((Const(p,_)$ d $ (Const("HOL.plus",_)$(Const("HOL.times",_)$ c $ y) $ z))) =>
if (x = y) andalso (is_arith_rel fm)
then
- let val ct = linear_cmul (dest_numeral c) t
+ let val ct = linear_cmul (dest_number c) t
in (HOLogic.mk_binrel p (d, linear_add vars ct z))
end
else fm
@@ -430,16 +430,16 @@
fun dvd_op (d, t) =
if not(is_numeral d) then raise DVD_UNKNOWN
else let
- val dn = dest_numeral d
+ val dn = dest_number d
fun coeffs_of x = case x of
Const(p,_) $ tl $ tr =>
if p = "HOL.plus" then (coeffs_of tl) union (coeffs_of tr)
else if p = "HOL.times"
then if (is_numeral tr)
- then [(dest_numeral tr) * (dest_numeral tl)]
- else [dest_numeral tl]
+ then [(dest_number tr) * (dest_number tl)]
+ else [dest_number tl]
else []
- |_ => if (is_numeral t) then [dest_numeral t] else []
+ |_ => if (is_numeral t) then [dest_number t] else []
val ts = coeffs_of t
in case ts of
[] => raise DVD_UNKNOWN
@@ -466,12 +466,12 @@
handle _ => at)
else
case AList.lookup (op =) operations p of
- SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const else HOLogic.false_const)
+ SOME f => ((if (f ((dest_number s),(dest_number t))) then HOLogic.true_const else HOLogic.false_const)
handle _ => at)
| _ => at)
|Const("Not",_)$(Const (p,_) $ s $ t) =>(
case AList.lookup (op =) operations p of
- SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then
+ SOME f => ((if (f ((dest_number s),(dest_number t))) then
HOLogic.false_const else HOLogic.true_const)
handle _ => at)
| _ => at)
@@ -482,13 +482,13 @@
fun evalc_atom at = case at of
(Const (p,_) $ s $ t) =>
( case AList.lookup (op =) operations p of
- SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const
+ SOME f => ((if (f ((dest_number s),(dest_number t))) then HOLogic.true_const
else HOLogic.false_const)
handle _ => at)
| _ => at)
|Const("Not",_)$(Const (p,_) $ s $ t) =>(
case AList.lookup (op =) operations p of
- SOME f => ((if (f ((dest_numeral s),(dest_numeral t)))
+ SOME f => ((if (f ((dest_number s),(dest_number t)))
then HOLogic.false_const else HOLogic.true_const)
handle _ => at)
| _ => at)
@@ -659,8 +659,8 @@
|mk_uni_vars T (Free (v,_)) = Free (v,T)
|mk_uni_vars T tm = tm;
-fun mk_uni_int T (Const ("HOL.zero",T2)) = if T = T2 then (mk_numeral 0) else (Const ("HOL.zero",T2))
- |mk_uni_int T (Const ("HOL.one",T2)) = if T = T2 then (mk_numeral 1) else (Const ("HOL.one",T2))
+fun mk_uni_int T (Const ("HOL.zero",T2)) = if T = T2 then (mk_number 0) else (Const ("HOL.zero",T2))
+ |mk_uni_int T (Const ("HOL.one",T2)) = if T = T2 then (mk_number 1) else (Const ("HOL.one",T2))
|mk_uni_int T (node $ rest) = (mk_uni_int T node) $ (mk_uni_int T rest )
|mk_uni_int T (Abs(AV,AT,p)) = Abs(AV,AT,mk_uni_int T p)
|mk_uni_int T tm = tm;
@@ -680,8 +680,8 @@
val p_inf = simpl (minusinf x p)
val bset = bset x p
val js = myupto 1 (divlcm x p)
- fun p_element j b = linrep vars x (linear_add vars b (mk_numeral j)) p
- fun stage j = list_disj (linrep vars x (mk_numeral j) p_inf :: map (p_element j) bset)
+ fun p_element j b = linrep vars x (linear_add vars b (mk_number j)) p
+ fun stage j = list_disj (linrep vars x (mk_number j) p_inf :: map (p_element j) bset)
in (list_disj (map stage js))
end
| _ => error "cooper: not an existential formula";
@@ -699,8 +699,8 @@
val p_inf = simpl (plusinf x p)
val aset = aset x p
val js = myupto 1 (divlcm x p)
- fun p_element j a = linrep vars x (linear_sub vars a (mk_numeral j)) p
- fun stage j = list_disj (linrep vars x (mk_numeral j) p_inf :: map (p_element j) aset)
+ fun p_element j a = linrep vars x (linear_sub vars a (mk_number j)) p
+ fun stage j = list_disj (linrep vars x (mk_number j) p_inf :: map (p_element j) aset)
in (list_disj (map stage js))
end
| _ => error "cooper: not an existential formula";
@@ -711,13 +711,13 @@
fun inf_w mi d vars x p =
let val f = if mi then minusinf else plusinf in
case (simpl (minusinf x p)) of
- Const("True",_) => (SOME (mk_numeral 1), HOLogic.true_const)
+ Const("True",_) => (SOME (mk_number 1), HOLogic.true_const)
|Const("False",_) => (NONE,HOLogic.false_const)
|F =>
let
fun h n =
- case ((simpl o evalc) (linrep vars x (mk_numeral n) F)) of
- Const("True",_) => (SOME (mk_numeral n),HOLogic.true_const)
+ case ((simpl o evalc) (linrep vars x (mk_number n) F)) of
+ Const("True",_) => (SOME (mk_number n),HOLogic.true_const)
|F' => if n=1 then (NONE,F')
else let val (rw,rf) = h (n-1) in
(rw,HOLogic.mk_disj(F',rf))
@@ -736,7 +736,7 @@
in (rw,HOLogic.mk_disj(F',rf))
end)
val f = if b then linear_add else linear_sub
- val p_elements = fold_rev (fn i => fn l => l union (map (fn e => f [] e (mk_numeral i)) st)) (myupto 1 d) []
+ val p_elements = fold_rev (fn i => fn l => l union (map (fn e => f [] e (mk_number i)) st)) (myupto 1 d) []
in h p_elements
end;
@@ -769,8 +769,8 @@
if (length bst) <= (length ast)
then (simpl (minusinf x p),linear_add,bst)
else (simpl (plusinf x p), linear_sub,ast)
- fun p_element j a = linrep vars x (f vars a (mk_numeral j)) p
- fun stage j = list_disj (linrep vars x (mk_numeral j) p_inf :: map (p_element j) S)
+ fun p_element j a = linrep vars x (f vars a (mk_number j)) p
+ fun stage j = list_disj (linrep vars x (mk_number j) p_inf :: map (p_element j) S)
fun stageh n = ((if n = 0 then []
else
let
@@ -805,8 +805,8 @@
then (true,bst)
else (false,ast)
in withness d p_inf S vars x p
-(* fun p_element j a = linrep vars x (f vars a (mk_numeral j)) p
- fun stage j = list_disj (linrep vars x (mk_numeral j) p_inf :: map (p_element j) S)
+(* fun p_element j a = linrep vars x (f vars a (mk_number j)) p
+ fun stage j = list_disj (linrep vars x (mk_number j) p_inf :: map (p_element j) S)
in (list_disj (map stage js))
*)
end
--- a/src/HOL/Tools/Presburger/cooper_proof.ML Wed Dec 13 15:45:30 2006 +0100
+++ b/src/HOL/Tools/Presburger/cooper_proof.ML Wed Dec 13 15:45:31 2006 +0100
@@ -33,7 +33,7 @@
val presburger_ss = simpset ()
addsimps [diff_int_def] delsimps [thm "diff_int_def_symmetric"];
-val cboolT = ctyp_of (sign_of HOL.thy) HOLogic.boolT;
+val cboolT = ctyp_of HOL.thy HOLogic.boolT;
(*Theorems that will be used later for the proofgeneration*)
@@ -163,7 +163,7 @@
fun norm_zero_one fm = case fm of
(Const ("HOL.times",_) $ c $ t) =>
if c = one then (norm_zero_one t)
- else if (dest_numeral c = ~1)
+ else if (dest_number c = ~1)
then (Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $ (norm_zero_one t))
else (HOLogic.mk_binop "HOL.times" (norm_zero_one c,norm_zero_one t))
|(node $ rest) => ((norm_zero_one node)$(norm_zero_one rest))
@@ -253,18 +253,18 @@
fun decomp_adjustcoeffeq sg x l fm = case fm of
(Const("Not",_)$(Const("Orderings.less",_) $(Const("HOL.zero",_)) $(rt as (Const ("HOL.plus", _)$(Const ("HOL.times",_) $ c $ y ) $z )))) =>
let
- val m = l div (dest_numeral c)
+ val m = l div (dest_number c)
val n = if (x = y) then abs (m) else 1
- val xtm = (HOLogic.mk_binop "HOL.times" ((mk_numeral ((m div n)*l) ), x))
+ val xtm = (HOLogic.mk_binop "HOL.times" ((mk_number ((m div n)*l) ), x))
val rs = if (x = y)
- then (HOLogic.mk_binrel "Orderings.less" (zero,linear_sub [] (mk_numeral n) (HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) ))))
+ then (HOLogic.mk_binrel "Orderings.less" (zero,linear_sub [] (mk_number n) (HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) ))))
else HOLogic.mk_binrel "Orderings.less" (zero,linear_sub [] one rt )
- val ck = cterm_of sg (mk_numeral n)
+ val ck = cterm_of sg (mk_number n)
val cc = cterm_of sg c
val ct = cterm_of sg z
val cx = cterm_of sg y
val pre = prove_elementar sg "lf"
- (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),(mk_numeral n)))
+ (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),(mk_number n)))
val th1 = (pre RS (instantiate' [] [SOME ck,SOME cc, SOME cx, SOME ct] (ac_pi_eq)))
in ([], fn [] => [th1,(prove_elementar sg "sa" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
end
@@ -273,12 +273,12 @@
c $ y ) $t )) =>
if (is_arith_rel fm) andalso (x = y)
then
- let val m = l div (dest_numeral c)
+ let val m = l div (dest_number c)
val k = (if p = "Orderings.less" then abs(m) else m)
- val xtm = (HOLogic.mk_binop "HOL.times" ((mk_numeral ((m div k)*l) ), x))
+ val xtm = (HOLogic.mk_binop "HOL.times" ((mk_number ((m div k)*l) ), x))
val rs = (HOLogic.mk_binrel p ((linear_cmul k a),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul k t) ))))
- val ck = cterm_of sg (mk_numeral k)
+ val ck = cterm_of sg (mk_number k)
val cc = cterm_of sg c
val ct = cterm_of sg t
val cx = cterm_of sg x
@@ -288,21 +288,21 @@
case p of
"Orderings.less" =>
let val pre = prove_elementar sg "lf"
- (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),(mk_numeral k)))
+ (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),(mk_number k)))
val th1 = (pre RS (instantiate' [] [SOME ck,SOME ca,SOME cc, SOME cx, SOME ct] (ac_lt_eq)))
in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
end
|"op =" =>
let val pre = prove_elementar sg "lf"
- (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("HOL.zero",HOLogic.intT),(mk_numeral k))))
+ (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("HOL.zero",HOLogic.intT),(mk_number k))))
val th1 = (pre RS(instantiate' [] [SOME ck,SOME ca,SOME cc, SOME cx, SOME ct] (ac_eq_eq)))
in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
end
|"Divides.dvd" =>
let val pre = prove_elementar sg "lf"
- (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("HOL.zero",HOLogic.intT),(mk_numeral k))))
+ (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("HOL.zero",HOLogic.intT),(mk_number k))))
val th1 = (pre RS (instantiate' [] [SOME ck,SOME ca,SOME cc, SOME cx, SOME ct]) (ac_dvd_eq))
in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
@@ -574,7 +574,7 @@
|(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", T) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
if (is_arith_rel at) andalso (x=y)
- then let val bst_z = norm_zero_one (linear_neg (linear_add [] z (mk_numeral 1)))
+ then let val bst_z = norm_zero_one (linear_neg (linear_add [] z (mk_number 1)))
in let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ bst_z $ B)
val th2 = prove_elementar sg "ss" (HOLogic.mk_eq (bst_z,Const("HOL.minus",T) $ (Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ (Const("HOL.one",HOLogic.intT))))
val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),dlcm))
@@ -675,7 +675,7 @@
|(Const("Orderings.less",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
if (y=x) andalso (c1 =zero) then
- if pm1 = (mk_numeral ~1) then
+ if pm1 = (mk_number ~1) then
let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one z) $ A)
val th2 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (zero,dlcm))
in (instantiate' [] [SOME cfma]([th2,th1] MRS (not_ast_p_lt)))
@@ -734,7 +734,7 @@
(Const (p,_) $ s $ t) =>(
case AList.lookup (op =) operations p of
SOME f =>
- ((if (f ((dest_numeral s),(dest_numeral t)))
+ ((if (f ((dest_number s),(dest_number t)))
then prove_elementar sg "ss" (HOLogic.mk_eq(at,HOLogic.true_const))
else prove_elementar sg "ss" (HOLogic.mk_eq(at, HOLogic.false_const)))
handle _ => instantiate' [SOME cboolT] [SOME (cterm_of sg at)] refl)
@@ -742,7 +742,7 @@
|Const("Not",_)$(Const (p,_) $ s $ t) =>(
case AList.lookup (op =) operations p of
SOME f =>
- ((if (f ((dest_numeral s),(dest_numeral t)))
+ ((if (f ((dest_number s),(dest_number t)))
then prove_elementar sg "ss" (HOLogic.mk_eq(at, HOLogic.false_const))
else prove_elementar sg "ss" (HOLogic.mk_eq(at,HOLogic.true_const)))
handle _ => instantiate' [SOME cboolT] [SOME (cterm_of sg at)] refl)
@@ -842,14 +842,14 @@
val ss = presburger_ss addsimps
[simp_from_to] delsimps [P_eqtrue, P_eqfalse, bex_triv, insert_iff]
(* uth : EX x.P(l*x) = EX x. l dvd x & P x*)
- val uth = instantiate' [] [SOME (cterm_of sg P) , SOME (cterm_of sg (mk_numeral l))] (unity_coeff_ex)
+ val uth = instantiate' [] [SOME (cterm_of sg P) , SOME (cterm_of sg (mk_number l))] (unity_coeff_ex)
(* e_ac_thm : Ex x. efm = EX x. fm*)
val e_ac_thm = (forall_intr (cterm_of sg x) ac_thm) COMP (qe_exI)
(* A and B set of the formula*)
val A = aset x cfm
val B = bset x cfm
(* the divlcm (delta) of the formula*)
- val dlcm = mk_numeral (divlcm x cfm)
+ val dlcm = mk_number (divlcm x cfm)
(* Which set is smaller to generate the (hoepfully) shorter proof*)
val cms = if ((length A) < (length B )) then "pi" else "mi"
(* val _ = if cms = "pi" then writeln "Plusinfinity" else writeln "Minusinfinity"*)
@@ -906,7 +906,7 @@
val ss = presburger_ss addsimps
[simp_from_to] delsimps [P_eqtrue, P_eqfalse, bex_triv, insert_iff]
(* uth : EX x.P(l*x) = EX x. l dvd x & P x*)
- val uth = instantiate' [] [SOME (cterm_of sg P) , SOME (cterm_of sg (mk_numeral l))] (unity_coeff_ex)
+ val uth = instantiate' [] [SOME (cterm_of sg P) , SOME (cterm_of sg (mk_number l))] (unity_coeff_ex)
(* e_ac_thm : Ex x. efm = EX x. fm*)
val e_ac_thm = (forall_intr (cterm_of sg x) ac_thm) COMP (qe_exI)
(* lsuth = EX.P(l*x) ; rsuth = EX x. l dvd x & P x*)
@@ -923,7 +923,7 @@
val A = aset x cfm
val B = bset x cfm
(* the divlcm (delta) of the formula*)
- val dlcm = mk_numeral (divlcm x cfm)
+ val dlcm = mk_number (divlcm x cfm)
(* Which set is smaller to generate the (hoepfully) shorter proof*)
val cms = if ((length A) < (length B )) then "pi" else "mi"
(* synthesize the proof of cooper's theorem*)
--- a/src/HOL/Tools/Presburger/reflected_cooper.ML Wed Dec 13 15:45:30 2006 +0100
+++ b/src/HOL/Tools/Presburger/reflected_cooper.ML Wed Dec 13 15:45:31 2006 +0100
@@ -20,7 +20,7 @@
| Const ("HOL.plus",_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
| Const ("HOL.minus",_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
| Const ("HOL.times",_)$t1$t2 => Mult (i_of_term vs t1,i_of_term vs t2)
- | Const ("Numeral.number_of",_)$t' => Cst (HOLogic.dest_binum t')
+ | Const ("Numeral.number_of",_)$t' => Cst (HOLogic.dest_numeral t')
| _ => error "i_of_term: unknown term";
@@ -75,7 +75,7 @@
fun term_of_i vs t =
case t of
- Cst i => CooperDec.mk_numeral i
+ Cst i => CooperDec.mk_number i
| Var n => valOf (myassoc2 vs n)
| Neg t' => Const("HOL.uminus",iT --> iT)$(term_of_i vs t')
| Add(t1,t2) => Const("HOL.plus",[iT,iT] ---> iT)$
--- a/src/HOL/arith_data.ML Wed Dec 13 15:45:30 2006 +0100
+++ b/src/HOL/arith_data.ML Wed Dec 13 15:45:31 2006 +0100
@@ -268,16 +268,16 @@
exception Zero;
-fun rat_of_term (numt : term, dent : term) : Rat.rat =
-let
- val num = HOLogic.dest_binum numt
- val den = HOLogic.dest_binum dent
-in
- if den = 0 then raise Zero else Rat.rat_of_quotient (num, den)
-end;
+fun rat_of_term (numt, dent) =
+ let
+ val num = HOLogic.dest_numeral numt
+ val den = HOLogic.dest_numeral dent
+ in
+ if den = 0 then raise Zero else Rat.rat_of_quotient (num, den)
+ end;
(* Warning: in rare cases number_of encloses a non-numeral,
- in which case dest_binum raises TERM; hence all the handles below.
+ in which case dest_numeral raises TERM; hence all the handles below.
Same for Suc-terms that turn out not to be numerals -
although the simplifier should eliminate those anyway ...
*)
@@ -294,16 +294,16 @@
fun demult ((mC as Const ("HOL.times", _)) $ s $ t, m) = (
(case s of
Const ("Numeral.number_of", _) $ n =>
- demult (t, Rat.mult (m, Rat.rat_of_intinf (HOLogic.dest_binum n)))
+ demult (t, Rat.mult (m, Rat.rat_of_intinf (HOLogic.dest_numeral n)))
| Const ("HOL.uminus", _) $ (Const ("Numeral.number_of", _) $ n) =>
- demult (t, Rat.mult (m, Rat.rat_of_intinf (~(HOLogic.dest_binum n))))
+ demult (t, Rat.mult (m, Rat.rat_of_intinf (~(HOLogic.dest_numeral n))))
| Const("Suc", _) $ _ =>
demult (t, Rat.mult (m, Rat.rat_of_int (number_of_Sucs s)))
| Const ("HOL.times", _) $ s1 $ s2 =>
demult (mC $ s1 $ (mC $ s2 $ t), m)
| Const ("HOL.divide", _) $ numt $ (Const ("Numeral.number_of", _) $ dent) =>
let
- val den = HOLogic.dest_binum dent
+ val den = HOLogic.dest_numeral dent
in
if den = 0 then
raise Zero
@@ -316,7 +316,7 @@
)
| demult (atom as Const("HOL.divide", _) $ t $ (Const ("Numeral.number_of", _) $ dent), m) =
(let
- val den = HOLogic.dest_binum dent
+ val den = HOLogic.dest_numeral dent
in
if den = 0 then
raise Zero
@@ -327,7 +327,7 @@
| demult (Const ("HOL.zero", _), m) = (NONE, Rat.rat_of_int 0)
| demult (Const ("HOL.one", _), m) = (NONE, m)
| demult (t as Const ("Numeral.number_of", _) $ n, m) =
- ((NONE, Rat.mult (m, Rat.rat_of_intinf (HOLogic.dest_binum n)))
+ ((NONE, Rat.mult (m, Rat.rat_of_intinf (HOLogic.dest_numeral n)))
handle TERM _ => (SOME t,m))
| demult (Const ("HOL.uminus", _) $ t, m) = demult(t,Rat.mult(m,Rat.rat_of_int(~1)))
| demult (t as Const f $ x, m) =
@@ -365,7 +365,7 @@
(NONE, m') => (p, Rat.add (i, m'))
| (SOME u, m') => add_atom u m' pi)
| poly (all as Const ("Numeral.number_of", Type(_,[_,T])) $ t, m, pi as (p, i)) =
- (let val k = HOLogic.dest_binum t
+ (let val k = HOLogic.dest_numeral t
val k2 = if k < 0 andalso T = HOLogic.natT then 0 else k
in (p, Rat.add (i, Rat.mult (m, Rat.rat_of_intinf k2))) end
handle TERM _ => add_atom all m pi)
@@ -427,8 +427,7 @@
| domain_is_nat (_ $ (Const ("Not", _) $ (Const (_, T) $ _ $ _))) = nT T
| domain_is_nat _ = false;
-fun number_of (n : IntInf.int, T : typ) =
- HOLogic.number_of_const T $ (HOLogic.mk_binum n);
+fun number_of (n, T) = HOLogic.mk_number T n;
(*---------------------------------------------------------------------------*)
(* code that performs certain goal transformations for linear arithmetic *)
--- a/src/HOL/ex/svc_funcs.ML Wed Dec 13 15:45:30 2006 +0100
+++ b/src/HOL/ex/svc_funcs.ML Wed Dec 13 15:45:31 2006 +0100
@@ -149,10 +149,7 @@
become part of the Var's name*)
| var (t,_) = fail t;
(*translation of a literal*)
- fun lit (Const("Numeral.number_of", _) $ w) =
- (HOLogic.dest_binum w handle TERM _ => raise Match)
- | lit (Const("0", _)) = 0
- | lit (Const("1", _)) = 1
+ val lit = snd o HOLogic.dest_number;
(*translation of a literal expression [no variables]*)
fun litExp (Const("HOL.plus", T) $ x $ y) =
if is_numeric_op T then (litExp x) + (litExp y)
--- a/src/HOL/hologic.ML Wed Dec 13 15:45:30 2006 +0100
+++ b/src/HOL/hologic.ML Wed Dec 13 15:45:31 2006 +0100
@@ -78,27 +78,28 @@
val B1_const: term
val mk_bit: int -> term
val dest_bit: term -> int
- val intT: typ
val pls_const: term
val min_const: term
val bit_const: term
val number_of_const: typ -> term
- val mk_binum: IntInf.int -> term
- val dest_binum: term -> IntInf.int
- val mk_int: IntInf.int -> term
+ val mk_numeral: IntInf.int -> term
+ val dest_numeral: term -> IntInf.int
+ val mk_number: typ -> IntInf.int -> term
+ val dest_number: term -> typ * IntInf.int
+ val intT: typ
val realT: typ
+ val listT: typ -> typ
+ val mk_list: typ -> term list -> term
+ val dest_list: term -> term list
val nibbleT: typ
val mk_nibble: int -> term
val dest_nibble: term -> int
val charT: typ
val mk_char: int -> term
val dest_char: term -> int
- val listT : typ -> typ
- val mk_list: typ -> term list -> term
- val dest_list: term -> term list
val stringT: typ
- val mk_string : string -> term
- val dest_string : term -> string
+ val mk_string: string -> term
+ val dest_string: term -> string
end;
structure HOLogic: HOLOGIC =
@@ -323,24 +324,34 @@
and min_const = Const ("Numeral.Min", intT)
and bit_const = Const ("Numeral.Bit", [intT, bitT] ---> intT);
-fun mk_binum 0 = pls_const
- | mk_binum ~1 = min_const
- | mk_binum i =
- let val (q, r) = IntInf.divMod (i, 2)
- in bit_const $ mk_binum q $ mk_bit (IntInf.toInt r) end;
-
-fun dest_binum (Const ("Numeral.Pls", _)) = 0
- | dest_binum (Const ("Numeral.Min", _)) = ~1
- | dest_binum (Const ("Numeral.Bit", _) $ bs $ b) =
- 2 * dest_binum bs + IntInf.fromInt (dest_bit b)
- | dest_binum t = raise TERM ("dest_binum", [t]);
-
fun number_of_const T = Const ("Numeral.number_of", intT --> T);
-fun mk_int 0 = Const ("HOL.zero", intT)
- | mk_int 1 = Const ("HOL.one", intT)
- | mk_int i = number_of_const intT $ mk_binum i;
+val mk_numeral =
+ let
+ fun mk_bit n = if n = 0 then B0_const else B1_const;
+ fun bin_of n =
+ if n = 0 then pls_const
+ else if n = ~1 then min_const
+ else
+ let
+ val (q, r) = IntInf.divMod (n, 2);
+ in bit_const $ bin_of q $ mk_bit r end;
+ in bin_of end;
+fun dest_numeral (Const ("Numeral.Pls", _)) = IntInf.fromInt 0
+ | dest_numeral (Const ("Numeral.Min", _)) = IntInf.fromInt ~1
+ | dest_numeral (Const ("Numeral.Bit", _) $ bs $ b) =
+ IntInf.fromInt (dest_bit b) + (2 * dest_numeral bs)
+ | dest_numeral t = raise TERM ("dest_numeral", [t]);
+
+fun mk_number T 0 = Const ("HOL.zero", T)
+ | mk_number T 1 = Const ("HOL.one", T)
+ | mk_number T i = number_of_const T $ mk_numeral i;
+
+fun dest_number (Const ("HOL.zero", T)) = (T, 0)
+ | dest_number (Const ("HOL.one", T)) = (T, 1)
+ | dest_number (Const ("Numeral.number_of", Type ("fun", [_, T])) $ t) = (T, dest_numeral t)
+ | dest_number t = raise TERM ("dest_number", [t]);
(* real *)
@@ -403,7 +414,7 @@
(* string *)
-val stringT = listT charT;
+val stringT = Type ("List.string", []);
val mk_string = mk_list charT o map (mk_char o ord) o explode;
val dest_string = implode o map (chr o dest_char) o dest_list;
--- a/src/Pure/Tools/codegen_package.ML Wed Dec 13 15:45:30 2006 +0100
+++ b/src/Pure/Tools/codegen_package.ML Wed Dec 13 15:45:31 2006 +0100
@@ -15,7 +15,7 @@
type appgen;
val add_appconst: string * appgen -> theory -> theory;
- val appgen_numeral: (theory -> term -> IntInf.int) -> appgen;
+ val appgen_numeral: (term -> IntInf.int option) -> appgen;
val appgen_char: (term -> int option) -> appgen;
val appgen_case: (theory -> term
-> ((string * typ) list * ((term * typ) * (term * term) list)) option)
@@ -397,7 +397,7 @@
(* (axiomatic extensions of extraction kernel *)
fun appgen_numeral int_of_numeral thy algbr funcgr strct (app as (c, ts)) trns =
- case try (int_of_numeral thy) (list_comb (Const c, ts))
+ case int_of_numeral (list_comb (Const c, ts))
of SOME i =>
trns
|> pair (CodegenThingol.INum i)