--- a/src/HOL/Decision_Procs/Cooper.thy Wed Feb 17 21:08:18 2016 +0100
+++ b/src/HOL/Decision_Procs/Cooper.thy Wed Feb 17 21:51:55 2016 +0100
@@ -2442,9 +2442,9 @@
| num_of_term vs @{term "1::int"} = @{code C} (@{code int_of_integer} 1)
| num_of_term vs @{term "- 1::int"} = @{code C} (@{code int_of_integer} (~ 1))
| num_of_term vs (@{term "numeral :: _ \<Rightarrow> int"} $ t) =
- @{code C} (@{code int_of_integer} (HOLogic.dest_num t))
+ @{code C} (@{code int_of_integer} (HOLogic.dest_numeral t))
| num_of_term vs (@{term "- numeral :: _ \<Rightarrow> int"} $ t) =
- @{code C} (@{code int_of_integer} (~(HOLogic.dest_num t)))
+ @{code C} (@{code int_of_integer} (~(HOLogic.dest_numeral t)))
| num_of_term vs (Bound i) = @{code Bound} (@{code nat_of_integer} i)
| num_of_term vs (@{term "uminus :: int \<Rightarrow> int"} $ t') = @{code Neg} (num_of_term vs t')
| num_of_term vs (@{term "op + :: int \<Rightarrow> int \<Rightarrow> int"} $ t1 $ t2) =
--- a/src/HOL/Decision_Procs/MIR.thy Wed Feb 17 21:08:18 2016 +0100
+++ b/src/HOL/Decision_Procs/MIR.thy Wed Feb 17 21:51:55 2016 +0100
@@ -5547,17 +5547,17 @@
of @{code C} i => @{code Mul} (i, num_of_term vs t2)
| _ => error "num_of_term: unsupported Multiplication")
| num_of_term vs (@{term "of_int :: int \<Rightarrow> real"} $ (@{term "numeral :: _ \<Rightarrow> int"} $ t')) =
- mk_C (HOLogic.dest_num t')
+ mk_C (HOLogic.dest_numeral t')
| num_of_term vs (@{term "of_int :: int \<Rightarrow> real"} $ (@{term "- numeral :: _ \<Rightarrow> int"} $ t')) =
- mk_C (~ (HOLogic.dest_num t'))
+ mk_C (~ (HOLogic.dest_numeral t'))
| num_of_term vs (@{term "of_int :: int \<Rightarrow> real"} $ (@{term "floor :: real \<Rightarrow> int"} $ t')) =
@{code Floor} (num_of_term vs t')
| num_of_term vs (@{term "of_int :: int \<Rightarrow> real"} $ (@{term "ceiling :: real \<Rightarrow> int"} $ t')) =
@{code Neg} (@{code Floor} (@{code Neg} (num_of_term vs t')))
| num_of_term vs (@{term "numeral :: _ \<Rightarrow> real"} $ t') =
- mk_C (HOLogic.dest_num t')
+ mk_C (HOLogic.dest_numeral t')
| num_of_term vs (@{term "- numeral :: _ \<Rightarrow> real"} $ t') =
- mk_C (~ (HOLogic.dest_num t'))
+ mk_C (~ (HOLogic.dest_numeral t'))
| num_of_term vs t = error ("num_of_term: unknown term " ^ Syntax.string_of_term @{context} t);
fun fm_of_term vs @{term True} = @{code T}
@@ -5569,9 +5569,9 @@
| fm_of_term vs (@{term "op = :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) =
@{code Eq} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
| fm_of_term vs (@{term "op rdvd"} $ (@{term "of_int :: int \<Rightarrow> real"} $ (@{term "numeral :: _ \<Rightarrow> int"} $ t1)) $ t2) =
- mk_Dvd (HOLogic.dest_num t1, num_of_term vs t2)
+ mk_Dvd (HOLogic.dest_numeral t1, num_of_term vs t2)
| fm_of_term vs (@{term "op rdvd"} $ (@{term "of_int :: int \<Rightarrow> real"} $ (@{term "- numeral :: _ \<Rightarrow> int"} $ t1)) $ t2) =
- mk_Dvd (~ (HOLogic.dest_num t1), num_of_term vs t2)
+ mk_Dvd (~ (HOLogic.dest_numeral t1), num_of_term vs t2)
| fm_of_term vs (@{term "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t1 $ t2) =
@{code Iff} (fm_of_term vs t1, fm_of_term vs t2)
| fm_of_term vs (@{term HOL.conj} $ t1 $ t2) =
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Wed Feb 17 21:08:18 2016 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Wed Feb 17 21:51:55 2016 +0100
@@ -1672,7 +1672,7 @@
fun do_numeral depth Ts mult T some_t0 t1 t2 =
(if is_number_type ctxt T then
let
- val j = mult * HOLogic.dest_num t2
+ val j = mult * HOLogic.dest_numeral t2
in
if j = 1 then
raise SAME ()
--- a/src/HOL/Tools/hologic.ML Wed Feb 17 21:08:18 2016 +0100
+++ b/src/HOL/Tools/hologic.ML Wed Feb 17 21:51:55 2016 +0100
@@ -100,7 +100,7 @@
val mk_bit: int -> term
val dest_bit: term -> int
val mk_numeral: int -> term
- val dest_num: term -> int
+ val dest_numeral: term -> int
val numeral_const: typ -> term
val add_numerals: term -> (term * typ) list -> (term * typ) list
val mk_number: typ -> int -> term
@@ -533,10 +533,10 @@
in if i > 0 then mk i else raise TERM ("mk_numeral: " ^ string_of_int i, [])
end
-fun dest_num (Const ("Num.num.One", _)) = 1
- | dest_num (Const ("Num.num.Bit0", _) $ bs) = 2 * dest_num bs
- | dest_num (Const ("Num.num.Bit1", _) $ bs) = 2 * dest_num bs + 1
- | dest_num t = raise TERM ("dest_num", [t]);
+fun dest_numeral (Const ("Num.num.One", _)) = 1
+ | dest_numeral (Const ("Num.num.Bit0", _) $ bs) = 2 * dest_numeral bs
+ | dest_numeral (Const ("Num.num.Bit1", _) $ bs) = 2 * dest_numeral bs + 1
+ | dest_numeral t = raise TERM ("dest_num", [t]);
fun numeral_const T = Const ("Num.numeral_class.numeral", numT --> T);
@@ -554,7 +554,7 @@
fun dest_number (Const ("Groups.zero_class.zero", T)) = (T, 0)
| dest_number (Const ("Groups.one_class.one", T)) = (T, 1)
| dest_number (Const ("Num.numeral_class.numeral", Type ("fun", [_, T])) $ t) =
- (T, dest_num t)
+ (T, dest_numeral t)
| dest_number (Const ("Groups.uminus_class.uminus", Type ("fun", [_, T])) $ t) =
apsnd (op ~) (dest_number t)
| dest_number t = raise TERM ("dest_number", [t]);
--- a/src/HOL/Tools/lin_arith.ML Wed Feb 17 21:08:18 2016 +0100
+++ b/src/HOL/Tools/lin_arith.ML Wed Feb 17 21:51:55 2016 +0100
@@ -175,11 +175,11 @@
| demult (Const (@{const_name Groups.zero}, _), _) = (NONE, Rat.zero)
| demult (Const (@{const_name Groups.one}, _), m) = (NONE, m)
(*Warning: in rare cases (neg_)numeral encloses a non-numeral,
- in which case dest_num 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 ...*)
| demult (t as Const ("Num.numeral_class.numeral", _) $ n, m) =
- ((NONE, Rat.mult m (Rat.rat_of_int (HOLogic.dest_num n)))
+ ((NONE, Rat.mult m (Rat.rat_of_int (HOLogic.dest_numeral n)))
handle TERM _ => (SOME t, m))
| demult (t as Const (@{const_name Suc}, _) $ _, m) =
((NONE, Rat.mult m (Rat.rat_of_int (HOLogic.dest_nat t)))
@@ -208,7 +208,7 @@
| poly (Const (@{const_name Groups.one}, _), m, (p, i)) =
(p, Rat.add i m)
| poly (all as Const ("Num.numeral_class.numeral", Type(_,[_,_])) $ t, m, pi as (p, i)) =
- (let val k = HOLogic.dest_num t
+ (let val k = HOLogic.dest_numeral t
in (p, Rat.add i (Rat.mult m (Rat.rat_of_int k))) end
handle TERM _ => add_atom all m pi)
| poly (Const (@{const_name Suc}, _) $ t, m, (p, i)) =