--- a/NEWS Tue Jan 15 16:19:21 2008 +0100
+++ b/NEWS Tue Jan 15 16:19:23 2008 +0100
@@ -25,8 +25,14 @@
*** HOL ***
+* Merged theories IntDef, Numeral and IntArith into unified theory Int.
+INCOMPATIBILITY.
+
+* Theory Library/Code_Index: type "index" now represents natural numbers rather
+than integers. INCOMPATIBILITY.
+
* New class "uminus" with operation "uminus" (split of from class "minus"
-which now only has operation "minus", binary).
+which now only has operation "minus", binary). INCOMPATIBILITY.
* New primrec package. Specification syntax conforms in style to
definition/function/.... No separate induction rule is provided.
@@ -40,14 +46,14 @@
* Library/ListSpace: new theory of arithmetic vector operations.
* Constants "card", "internal_split", "option_map" now with authentic
-syntax.
+syntax. INCOMPATIBILITY.
* Definitions subset_def, psubset_def, set_diff_def, Compl_def,
le_bool_def, less_bool_def, le_fun_def, less_fun_def, inf_bool_def,
sup_bool_def, Inf_bool_def, Sup_bool_def, inf_fun_def, sup_fun_def,
Inf_fun_def, Sup_fun_def, inf_set_def, sup_set_def, Inf_set_def,
Sup_set_def, le_def, less_def, option_map_def now with object
-equality.
+equality. INCOMPATIBILITY.
* New method "induction_scheme" derives user-specified induction rules
from wellfounded induction and completeness of patterns. This factors
--- a/src/HOL/Algebra/IntRing.thy Tue Jan 15 16:19:21 2008 +0100
+++ b/src/HOL/Algebra/IntRing.thy Tue Jan 15 16:19:23 2008 +0100
@@ -5,7 +5,7 @@
*)
theory IntRing
-imports QuotRing IntDef
+imports QuotRing Int
begin
--- a/src/HOL/Arith_Tools.thy Tue Jan 15 16:19:21 2008 +0100
+++ b/src/HOL/Arith_Tools.thy Tue Jan 15 16:19:23 2008 +0100
@@ -30,8 +30,8 @@
the right simplification, but with some redundant inequality
tests.*}
lemma neg_number_of_pred_iff_0:
- "neg (number_of (Numeral.pred v)::int) = (number_of v = (0::nat))"
-apply (subgoal_tac "neg (number_of (Numeral.pred v)) = (number_of v < Suc 0) ")
+ "neg (number_of (Int.pred v)::int) = (number_of v = (0::nat))"
+apply (subgoal_tac "neg (number_of (Int.pred v)) = (number_of v < Suc 0) ")
apply (simp only: less_Suc_eq_le le_0_eq)
apply (subst less_number_of_Suc, simp)
done
@@ -40,7 +40,7 @@
simproc*}
lemma Suc_diff_number_of:
"neg (number_of (uminus v)::int) ==>
- Suc m - (number_of v) = m - (number_of (Numeral.pred v))"
+ Suc m - (number_of v) = m - (number_of (Int.pred v))"
apply (subst Suc_diff_eq_diff_pred)
apply simp
apply (simp del: nat_numeral_1_eq_1)
@@ -56,13 +56,13 @@
lemma nat_case_number_of [simp]:
"nat_case a f (number_of v) =
- (let pv = number_of (Numeral.pred v) in
+ (let pv = number_of (Int.pred v) in
if neg pv then a else f (nat pv))"
by (simp split add: nat.split add: Let_def neg_number_of_pred_iff_0)
lemma nat_case_add_eq_if [simp]:
"nat_case a f ((number_of v) + n) =
- (let pv = number_of (Numeral.pred v) in
+ (let pv = number_of (Int.pred v) in
if neg pv then nat_case a f n else f (nat pv + n))"
apply (subst add_eq_if)
apply (simp split add: nat.split
@@ -73,7 +73,7 @@
lemma nat_rec_number_of [simp]:
"nat_rec a f (number_of v) =
- (let pv = number_of (Numeral.pred v) in
+ (let pv = number_of (Int.pred v) in
if neg pv then a else f (nat pv) (nat_rec a f (nat pv)))"
apply (case_tac " (number_of v) ::nat")
apply (simp_all (no_asm_simp) add: Let_def neg_number_of_pred_iff_0)
@@ -82,7 +82,7 @@
lemma nat_rec_add_eq_if [simp]:
"nat_rec a f (number_of v + n) =
- (let pv = number_of (Numeral.pred v) in
+ (let pv = number_of (Int.pred v) in
if neg pv then nat_rec a f n
else f (nat pv + n) (nat_rec a f (nat pv + n)))"
apply (subst add_eq_if)
--- a/src/HOL/Complex/ex/linreif.ML Tue Jan 15 16:19:21 2008 +0100
+++ b/src/HOL/Complex/ex/linreif.ML Tue Jan 15 16:19:23 2008 +0100
@@ -33,8 +33,8 @@
| Const (@{const_name "HOL.times"},_)$t1$t2 => (case (num_of_term vs t1) of C i =>
Mul (i,num_of_term vs t2)
| _ => error "num_of_term: unsupported Multiplication")
- | Const("RealDef.real",_) $ Const (@{const_name "Numeral.number_of"},_)$t' => C (HOLogic.dest_numeral t')
- | Const (@{const_name "Numeral.number_of"},_)$t' => C (HOLogic.dest_numeral t')
+ | Const("RealDef.real",_) $ Const (@{const_name "Int.number_of"},_)$t' => C (HOLogic.dest_numeral t')
+ | Const (@{const_name "Int.number_of"},_)$t' => C (HOLogic.dest_numeral t')
| _ => error ("num_of_term: unknown term " ^ (Display.raw_string_of_term t));
(* pseudo reification : term -> fm *)
--- a/src/HOL/Complex/ex/mireif.ML Tue Jan 15 16:19:21 2008 +0100
+++ b/src/HOL/Complex/ex/mireif.ML Tue Jan 15 16:19:23 2008 +0100
@@ -32,8 +32,8 @@
| _ => error "num_of_term: unsupported Multiplication")
| Const("RealDef.real",_)$ (Const (@{const_name "RComplete.floor"},_)$ t') => Floor (num_of_term vs t')
| Const("RealDef.real",_)$ (Const (@{const_name "RComplete.ceiling"},_)$ t') => Neg(Floor (Neg (num_of_term vs t')))
- | Const("RealDef.real",_) $ Const (@{const_name "Numeral.number_of"},_)$t' => C (HOLogic.dest_numeral t')
- | Const (@{const_name "Numeral.number_of"},_)$t' => C (HOLogic.dest_numeral t')
+ | Const("RealDef.real",_) $ Const (@{const_name "Int.number_of"},_)$t' => C (HOLogic.dest_numeral t')
+ | Const (@{const_name "Int.number_of"},_)$t' => C (HOLogic.dest_numeral t')
| _ => error ("num_of_term: unknown term " ^ (Display.raw_string_of_term t));
@@ -44,7 +44,7 @@
| Const("False",_) => F
| Const(@{const_name HOL.less},_)$t1$t2 => Lt (Sub (num_of_term vs t1,num_of_term vs t2))
| Const(@{const_name HOL.less_eq},_)$t1$t2 => Le (Sub (num_of_term vs t1,num_of_term vs t2))
- | Const (@{const_name "MIR.rdvd"},_ )$ (Const("RealDef.real",_) $ (Const(@{const_name "Numeral.number_of"},_)$t1))$t2 =>
+ | Const (@{const_name "MIR.rdvd"},_ )$ (Const("RealDef.real",_) $ (Const(@{const_name "Int.number_of"},_)$t1))$t2 =>
Dvd (HOLogic.dest_numeral t1, num_of_term vs t2)
| Const("op =",eqT)$t1$t2 =>
if (domain_type eqT = @{typ real})
--- a/src/HOL/Hyperreal/NSA.thy Tue Jan 15 16:19:21 2008 +0100
+++ b/src/HOL/Hyperreal/NSA.thy Tue Jan 15 16:19:23 2008 +0100
@@ -678,11 +678,11 @@
case u of
Const(@{const_name HOL.zero}, _) => NONE
| Const(@{const_name HOL.one}, _) => NONE
- | Const(@{const_name Numeral.number_of}, _) $ _ => NONE
+ | Const(@{const_name Int.number_of}, _) $ _ => NONE
| _ => SOME (case t of
Const(@{const_name HOL.zero}, _) => meta_zero_approx_reorient
| Const(@{const_name HOL.one}, _) => meta_one_approx_reorient
- | Const(@{const_name Numeral.number_of}, _) $ _ =>
+ | Const(@{const_name Int.number_of}, _) $ _ =>
meta_number_of_approx_reorient);
in
--- a/src/HOL/Import/HOL/HOL4Prob.thy Tue Jan 15 16:19:21 2008 +0100
+++ b/src/HOL/Import/HOL/HOL4Prob.thy Tue Jan 15 16:19:23 2008 +0100
@@ -37,7 +37,7 @@
((op div::nat => nat => nat) (0::nat)
((number_of \<Colon> int => nat)
((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
+ ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
(bit.B0::bit))))
(0::nat))
((op &::bool => bool => bool)
@@ -45,18 +45,18 @@
((op div::nat => nat => nat) (1::nat)
((number_of \<Colon> int => nat)
((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
+ ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
(bit.B0::bit))))
(0::nat))
((op =::nat => nat => bool)
((op div::nat => nat => nat)
((number_of \<Colon> int => nat)
((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
+ ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
(bit.B0::bit)))
((number_of \<Colon> int => nat)
((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
+ ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
(bit.B0::bit))))
(1::nat)))"
by (import prob_extra DIV_TWO_BASIC)
@@ -77,17 +77,17 @@
((op ^::nat => nat => nat)
((number_of \<Colon> int => nat)
((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
+ ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
(bit.B0::bit)))
((Suc::nat => nat) n))
((number_of \<Colon> int => nat)
((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
+ ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
(bit.B0::bit))))
((op ^::nat => nat => nat)
((number_of \<Colon> int => nat)
((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
+ ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
(bit.B0::bit)))
n))"
by (import prob_extra EXP_DIV_TWO)
@@ -127,7 +127,7 @@
((op /::real => real => real) (1::real)
((number_of \<Colon> int => real)
((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
+ ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
(bit.B0::bit))))"
by (import prob_extra HALF_POS)
@@ -135,12 +135,12 @@
((op *::real => real => real)
((number_of \<Colon> int => real)
((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
+ ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
(bit.B0::bit)))
((op /::real => real => real) (1::real)
((number_of \<Colon> int => real)
((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
+ ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
(bit.B0::bit)))))
(1::real)"
by (import prob_extra HALF_CANCEL)
@@ -152,7 +152,7 @@
((op /::real => real => real) (1::real)
((number_of \<Colon> int => real)
((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
+ ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
(bit.B0::bit))))
n))"
by (import prob_extra POW_HALF_POS)
@@ -167,7 +167,7 @@
((op /::real => real => real) (1::real)
((number_of \<Colon> int => real)
((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
+ ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
(bit.B1::bit))
(bit.B0::bit))))
n)
@@ -175,7 +175,7 @@
((op /::real => real => real) (1::real)
((number_of \<Colon> int => real)
((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
+ ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
(bit.B1::bit))
(bit.B0::bit))))
m))))"
@@ -188,19 +188,19 @@
((op /::real => real => real) (1::real)
((number_of \<Colon> int => real)
((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
+ ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
(bit.B0::bit))))
n)
((op *::real => real => real)
((number_of \<Colon> int => real)
((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
+ ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
(bit.B0::bit)))
((op ^::real => nat => real)
((op /::real => real => real) (1::real)
((number_of \<Colon> int => real)
((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
+ ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
(bit.B1::bit))
(bit.B0::bit))))
((Suc::nat => nat) n))))"
@@ -229,12 +229,12 @@
((op /::real => real => real) (1::real)
((number_of \<Colon> int => real)
((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
+ ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
(bit.B0::bit)))))
((op /::real => real => real) (1::real)
((number_of \<Colon> int => real)
((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
+ ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
(bit.B0::bit))))"
by (import prob_extra ONE_MINUS_HALF)
@@ -242,7 +242,7 @@
((op /::real => real => real) (1::real)
((number_of \<Colon> int => real)
((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
+ ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
(bit.B0::bit))))
(1::real)"
by (import prob_extra HALF_LT_1)
@@ -254,7 +254,7 @@
((op /::real => real => real) (1::real)
((number_of \<Colon> int => real)
((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
+ ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
(bit.B0::bit))))
n)
((inverse::real => real)
@@ -262,7 +262,7 @@
((op ^::nat => nat => nat)
((number_of \<Colon> int => nat)
((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
+ ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
(bit.B1::bit))
(bit.B0::bit)))
n))))"
@@ -1407,7 +1407,7 @@
((op /::real => real => real) (1::real)
((number_of \<Colon> int => real)
((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
+ ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
(bit.B1::bit))
(bit.B0::bit))))
((size::bool list => nat)
@@ -1416,7 +1416,7 @@
((op /::real => real => real) (1::real)
((number_of \<Colon> int => real)
((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
+ ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
(bit.B1::bit))
(bit.B0::bit))))
((size::bool list => nat)
@@ -1425,7 +1425,7 @@
((op /::real => real => real) (1::real)
((number_of \<Colon> int => real)
((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
+ ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
(bit.B0::bit))))
((size::bool list => nat) l)))"
by (import prob ALG_TWINS_MEASURE)
--- a/src/HOL/Import/HOL/HOL4Real.thy Tue Jan 15 16:19:21 2008 +0100
+++ b/src/HOL/Import/HOL/HOL4Real.thy Tue Jan 15 16:19:23 2008 +0100
@@ -527,7 +527,7 @@
((op ^::real => nat => real) x
((number_of \<Colon> int => nat)
((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
+ ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
(bit.B0::bit))))))"
by (import real REAL_LE1_POW2)
@@ -539,7 +539,7 @@
((op ^::real => nat => real) x
((number_of \<Colon> int => nat)
((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
+ ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
(bit.B0::bit))))))"
by (import real REAL_LT1_POW2)
--- a/src/HOL/Import/HOL/HOL4Vec.thy Tue Jan 15 16:19:21 2008 +0100
+++ b/src/HOL/Import/HOL/HOL4Vec.thy Tue Jan 15 16:19:23 2008 +0100
@@ -1284,7 +1284,7 @@
((op <::nat => nat => bool) x
((number_of \<Colon> int => nat)
((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
+ ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
(bit.B0::bit))))
((op =::nat => nat => bool) ((BV::bool => nat) ((VB::nat => bool) x))
x))"
@@ -1502,7 +1502,7 @@
((number_of \<Colon> int => nat)
((op BIT \<Colon> int => bit => int)
((op BIT \<Colon> int => bit => int)
- (Numeral.Pls \<Colon> int) (bit.B1::bit))
+ (Int.Pls \<Colon> int) (bit.B1::bit))
(bit.B0::bit)))
k)))))))"
by (import bword_arith ACARRY_EQ_ADD_DIV)
--- a/src/HOL/Import/HOL/HOL4Word32.thy Tue Jan 15 16:19:21 2008 +0100
+++ b/src/HOL/Import/HOL/HOL4Word32.thy Tue Jan 15 16:19:23 2008 +0100
@@ -118,7 +118,7 @@
((op ^::nat => nat => nat)
((number_of \<Colon> int => nat)
((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
+ ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
(bit.B0::bit)))
n))"
by (import bits ZERO_LT_TWOEXP)
@@ -138,14 +138,14 @@
((op ^::nat => nat => nat)
((number_of \<Colon> int => nat)
((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
+ ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
(bit.B1::bit))
(bit.B0::bit)))
a)
((op ^::nat => nat => nat)
((number_of \<Colon> int => nat)
((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
+ ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
(bit.B1::bit))
(bit.B0::bit)))
b))))"
@@ -160,14 +160,14 @@
((op ^::nat => nat => nat)
((number_of \<Colon> int => nat)
((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
+ ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
(bit.B1::bit))
(bit.B0::bit)))
a)
((op ^::nat => nat => nat)
((number_of \<Colon> int => nat)
((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
+ ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
(bit.B1::bit))
(bit.B0::bit)))
b))))"
@@ -181,14 +181,14 @@
((op ^::nat => nat => nat)
((number_of \<Colon> int => nat)
((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
+ ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
(bit.B1::bit))
(bit.B0::bit)))
((op -::nat => nat => nat) a b))
((op ^::nat => nat => nat)
((number_of \<Colon> int => nat)
((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
+ ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
(bit.B1::bit))
(bit.B0::bit)))
a)))"
@@ -350,7 +350,7 @@
((op ^::nat => nat => nat)
((number_of \<Colon> int => nat)
((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
+ ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
(bit.B1::bit))
(bit.B0::bit)))
b)
@@ -358,14 +358,14 @@
((op ^::nat => nat => nat)
((number_of \<Colon> int => nat)
((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
+ ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
(bit.B1::bit))
(bit.B0::bit)))
((op +::nat => nat => nat) x (1::nat)))
((op ^::nat => nat => nat)
((number_of \<Colon> int => nat)
((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
+ ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
(bit.B1::bit))
(bit.B0::bit)))
a))))))"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Int.thy Tue Jan 15 16:19:23 2008 +0100
@@ -0,0 +1,1897 @@
+(* Title: Int.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Tobias Nipkow, Florian Haftmann, TU Muenchen
+ Copyright 1994 University of Cambridge
+
+*)
+
+header {* The Integers as Equivalence Classes over Pairs of Natural Numbers *}
+
+theory Int
+imports Equiv_Relations Wellfounded_Relations Datatype Nat
+uses
+ ("Tools/numeral.ML")
+ ("Tools/numeral_syntax.ML")
+ ("~~/src/Provers/Arith/assoc_fold.ML")
+ "~~/src/Provers/Arith/cancel_numerals.ML"
+ "~~/src/Provers/Arith/combine_numerals.ML"
+ ("int_arith1.ML")
+begin
+
+subsection {* The equivalence relation underlying the integers *}
+
+definition
+ intrel :: "((nat \<times> nat) \<times> (nat \<times> nat)) set"
+where
+ "intrel = {((x, y), (u, v)) | x y u v. x + v = u +y }"
+
+typedef (Integ)
+ int = "UNIV//intrel"
+ by (auto simp add: quotient_def)
+
+instantiation int :: "{zero, one, plus, minus, uminus, times, ord, abs, sgn}"
+begin
+
+definition
+ Zero_int_def [code func del]: "0 = Abs_Integ (intrel `` {(0, 0)})"
+
+definition
+ One_int_def [code func del]: "1 = Abs_Integ (intrel `` {(1, 0)})"
+
+definition
+ add_int_def [code func del]: "z + w = Abs_Integ
+ (\<Union>(x, y) \<in> Rep_Integ z. \<Union>(u, v) \<in> Rep_Integ w.
+ intrel `` {(x + u, y + v)})"
+
+definition
+ minus_int_def [code func del]:
+ "- z = Abs_Integ (\<Union>(x, y) \<in> Rep_Integ z. intrel `` {(y, x)})"
+
+definition
+ diff_int_def [code func del]: "z - w = z + (-w \<Colon> int)"
+
+definition
+ mult_int_def [code func del]: "z * w = Abs_Integ
+ (\<Union>(x, y) \<in> Rep_Integ z. \<Union>(u,v ) \<in> Rep_Integ w.
+ intrel `` {(x*u + y*v, x*v + y*u)})"
+
+definition
+ le_int_def [code func del]:
+ "z \<le> w \<longleftrightarrow> (\<exists>x y u v. x+v \<le> u+y \<and> (x, y) \<in> Rep_Integ z \<and> (u, v) \<in> Rep_Integ w)"
+
+definition
+ less_int_def [code func del]: "(z\<Colon>int) < w \<longleftrightarrow> z \<le> w \<and> z \<noteq> w"
+
+definition
+ zabs_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"
+
+definition
+ zsgn_def: "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
+
+instance ..
+
+end
+
+
+subsection{*Construction of the Integers*}
+
+lemma intrel_iff [simp]: "(((x,y),(u,v)) \<in> intrel) = (x+v = u+y)"
+by (simp add: intrel_def)
+
+lemma equiv_intrel: "equiv UNIV intrel"
+by (simp add: intrel_def equiv_def refl_def sym_def trans_def)
+
+text{*Reduces equality of equivalence classes to the @{term intrel} relation:
+ @{term "(intrel `` {x} = intrel `` {y}) = ((x,y) \<in> intrel)"} *}
+lemmas equiv_intrel_iff [simp] = eq_equiv_class_iff [OF equiv_intrel UNIV_I UNIV_I]
+
+text{*All equivalence classes belong to set of representatives*}
+lemma [simp]: "intrel``{(x,y)} \<in> Integ"
+by (auto simp add: Integ_def intrel_def quotient_def)
+
+text{*Reduces equality on abstractions to equality on representatives:
+ @{prop "\<lbrakk>x \<in> Integ; y \<in> Integ\<rbrakk> \<Longrightarrow> (Abs_Integ x = Abs_Integ y) = (x=y)"} *}
+declare Abs_Integ_inject [simp,noatp] Abs_Integ_inverse [simp,noatp]
+
+text{*Case analysis on the representation of an integer as an equivalence
+ class of pairs of naturals.*}
+lemma eq_Abs_Integ [case_names Abs_Integ, cases type: int]:
+ "(!!x y. z = Abs_Integ(intrel``{(x,y)}) ==> P) ==> P"
+apply (rule Abs_Integ_cases [of z])
+apply (auto simp add: Integ_def quotient_def)
+done
+
+
+subsection {* Arithmetic Operations *}
+
+lemma minus: "- Abs_Integ(intrel``{(x,y)}) = Abs_Integ(intrel `` {(y,x)})"
+proof -
+ have "(\<lambda>(x,y). intrel``{(y,x)}) respects intrel"
+ by (simp add: congruent_def)
+ thus ?thesis
+ by (simp add: minus_int_def UN_equiv_class [OF equiv_intrel])
+qed
+
+lemma add:
+ "Abs_Integ (intrel``{(x,y)}) + Abs_Integ (intrel``{(u,v)}) =
+ Abs_Integ (intrel``{(x+u, y+v)})"
+proof -
+ have "(\<lambda>z w. (\<lambda>(x,y). (\<lambda>(u,v). intrel `` {(x+u, y+v)}) w) z)
+ respects2 intrel"
+ by (simp add: congruent2_def)
+ thus ?thesis
+ by (simp add: add_int_def UN_UN_split_split_eq
+ UN_equiv_class2 [OF equiv_intrel equiv_intrel])
+qed
+
+text{*Congruence property for multiplication*}
+lemma mult_congruent2:
+ "(%p1 p2. (%(x,y). (%(u,v). intrel``{(x*u + y*v, x*v + y*u)}) p2) p1)
+ respects2 intrel"
+apply (rule equiv_intrel [THEN congruent2_commuteI])
+ apply (force simp add: mult_ac, clarify)
+apply (simp add: congruent_def mult_ac)
+apply (rename_tac u v w x y z)
+apply (subgoal_tac "u*y + x*y = w*y + v*y & u*z + x*z = w*z + v*z")
+apply (simp add: mult_ac)
+apply (simp add: add_mult_distrib [symmetric])
+done
+
+lemma mult:
+ "Abs_Integ((intrel``{(x,y)})) * Abs_Integ((intrel``{(u,v)})) =
+ Abs_Integ(intrel `` {(x*u + y*v, x*v + y*u)})"
+by (simp add: mult_int_def UN_UN_split_split_eq mult_congruent2
+ UN_equiv_class2 [OF equiv_intrel equiv_intrel])
+
+text{*The integers form a @{text comm_ring_1}*}
+instance int :: comm_ring_1
+proof
+ fix i j k :: int
+ show "(i + j) + k = i + (j + k)"
+ by (cases i, cases j, cases k) (simp add: add add_assoc)
+ show "i + j = j + i"
+ by (cases i, cases j) (simp add: add_ac add)
+ show "0 + i = i"
+ by (cases i) (simp add: Zero_int_def add)
+ show "- i + i = 0"
+ by (cases i) (simp add: Zero_int_def minus add)
+ show "i - j = i + - j"
+ by (simp add: diff_int_def)
+ show "(i * j) * k = i * (j * k)"
+ by (cases i, cases j, cases k) (simp add: mult ring_simps)
+ show "i * j = j * i"
+ by (cases i, cases j) (simp add: mult ring_simps)
+ show "1 * i = i"
+ by (cases i) (simp add: One_int_def mult)
+ show "(i + j) * k = i * k + j * k"
+ by (cases i, cases j, cases k) (simp add: add mult ring_simps)
+ show "0 \<noteq> (1::int)"
+ by (simp add: Zero_int_def One_int_def)
+qed
+
+lemma int_def: "of_nat m = Abs_Integ (intrel `` {(m, 0)})"
+by (induct m, simp_all add: Zero_int_def One_int_def add)
+
+
+subsection {* The @{text "\<le>"} Ordering *}
+
+lemma le:
+ "(Abs_Integ(intrel``{(x,y)}) \<le> Abs_Integ(intrel``{(u,v)})) = (x+v \<le> u+y)"
+by (force simp add: le_int_def)
+
+lemma less:
+ "(Abs_Integ(intrel``{(x,y)}) < Abs_Integ(intrel``{(u,v)})) = (x+v < u+y)"
+by (simp add: less_int_def le order_less_le)
+
+instance int :: linorder
+proof
+ fix i j k :: int
+ show "(i < j) = (i \<le> j \<and> i \<noteq> j)"
+ by (simp add: less_int_def)
+ show "i \<le> i"
+ by (cases i) (simp add: le)
+ show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k"
+ by (cases i, cases j, cases k) (simp add: le)
+ show "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j"
+ by (cases i, cases j) (simp add: le)
+ show "i \<le> j \<or> j \<le> i"
+ by (cases i, cases j) (simp add: le linorder_linear)
+qed
+
+instantiation int :: distrib_lattice
+begin
+
+definition
+ "(inf \<Colon> int \<Rightarrow> int \<Rightarrow> int) = min"
+
+definition
+ "(sup \<Colon> int \<Rightarrow> int \<Rightarrow> int) = max"
+
+instance
+ by intro_classes
+ (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1)
+
+end
+
+instance int :: pordered_cancel_ab_semigroup_add
+proof
+ fix i j k :: int
+ show "i \<le> j \<Longrightarrow> k + i \<le> k + j"
+ by (cases i, cases j, cases k) (simp add: le add)
+qed
+
+text{*Strict Monotonicity of Multiplication*}
+
+text{*strict, in 1st argument; proof is by induction on k>0*}
+lemma zmult_zless_mono2_lemma:
+ "(i::int)<j ==> 0<k ==> of_nat k * i < of_nat k * j"
+apply (induct "k", simp)
+apply (simp add: left_distrib)
+apply (case_tac "k=0")
+apply (simp_all add: add_strict_mono)
+done
+
+lemma zero_le_imp_eq_int: "(0::int) \<le> k ==> \<exists>n. k = of_nat n"
+apply (cases k)
+apply (auto simp add: le add int_def Zero_int_def)
+apply (rule_tac x="x-y" in exI, simp)
+done
+
+lemma zero_less_imp_eq_int: "(0::int) < k ==> \<exists>n>0. k = of_nat n"
+apply (cases k)
+apply (simp add: less int_def Zero_int_def)
+apply (rule_tac x="x-y" in exI, simp)
+done
+
+lemma zmult_zless_mono2: "[| i<j; (0::int) < k |] ==> k*i < k*j"
+apply (drule zero_less_imp_eq_int)
+apply (auto simp add: zmult_zless_mono2_lemma)
+done
+
+text{*The integers form an ordered integral domain*}
+instance int :: ordered_idom
+proof
+ fix i j k :: int
+ show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"
+ by (rule zmult_zless_mono2)
+ show "\<bar>i\<bar> = (if i < 0 then -i else i)"
+ by (simp only: zabs_def)
+ show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
+ by (simp only: zsgn_def)
+qed
+
+lemma zless_imp_add1_zle: "w < z \<Longrightarrow> w + (1\<Colon>int) \<le> z"
+apply (cases w, cases z)
+apply (simp add: less le add One_int_def)
+done
+
+lemma zless_iff_Suc_zadd:
+ "(w \<Colon> int) < z \<longleftrightarrow> (\<exists>n. z = w + of_nat (Suc n))"
+apply (cases z, cases w)
+apply (auto simp add: less add int_def)
+apply (rename_tac a b c d)
+apply (rule_tac x="a+d - Suc(c+b)" in exI)
+apply arith
+done
+
+lemmas int_distrib =
+ left_distrib [of "z1::int" "z2" "w", standard]
+ right_distrib [of "w::int" "z1" "z2", standard]
+ left_diff_distrib [of "z1::int" "z2" "w", standard]
+ right_diff_distrib [of "w::int" "z1" "z2", standard]
+
+
+subsection {* Embedding of the Integers into any @{text ring_1}: @{text of_int}*}
+
+context ring_1
+begin
+
+definition
+ of_int :: "int \<Rightarrow> 'a"
+where
+ [code func del]: "of_int z = contents (\<Union>(i, j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
+
+lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j"
+proof -
+ have "(\<lambda>(i,j). { of_nat i - (of_nat j :: 'a) }) respects intrel"
+ by (simp add: congruent_def compare_rls of_nat_add [symmetric]
+ del: of_nat_add)
+ thus ?thesis
+ by (simp add: of_int_def UN_equiv_class [OF equiv_intrel])
+qed
+
+lemma of_int_0 [simp]: "of_int 0 = 0"
+ by (simp add: of_int Zero_int_def)
+
+lemma of_int_1 [simp]: "of_int 1 = 1"
+ by (simp add: of_int One_int_def)
+
+lemma of_int_add [simp]: "of_int (w+z) = of_int w + of_int z"
+ by (cases w, cases z, simp add: compare_rls of_int OrderedGroup.compare_rls add)
+
+lemma of_int_minus [simp]: "of_int (-z) = - (of_int z)"
+ by (cases z, simp add: compare_rls of_int minus)
+
+lemma of_int_diff [simp]: "of_int (w - z) = of_int w - of_int z"
+ by (simp add: OrderedGroup.diff_minus diff_minus)
+
+lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z"
+apply (cases w, cases z)
+apply (simp add: compare_rls of_int left_diff_distrib right_diff_distrib
+ mult add_ac of_nat_mult)
+done
+
+text{*Collapse nested embeddings*}
+lemma of_int_of_nat_eq [simp]: "of_int (of_nat n) = of_nat n"
+ by (induct n) auto
+
+end
+
+context ordered_idom
+begin
+
+lemma of_int_le_iff [simp]:
+ "of_int w \<le> of_int z \<longleftrightarrow> w \<le> z"
+ by (cases w, cases z, simp add: of_int le minus compare_rls of_nat_add [symmetric] del: of_nat_add)
+
+text{*Special cases where either operand is zero*}
+lemmas of_int_0_le_iff [simp] = of_int_le_iff [of 0, simplified]
+lemmas of_int_le_0_iff [simp] = of_int_le_iff [of _ 0, simplified]
+
+lemma of_int_less_iff [simp]:
+ "of_int w < of_int z \<longleftrightarrow> w < z"
+ by (simp add: not_le [symmetric] linorder_not_le [symmetric])
+
+text{*Special cases where either operand is zero*}
+lemmas of_int_0_less_iff [simp] = of_int_less_iff [of 0, simplified]
+lemmas of_int_less_0_iff [simp] = of_int_less_iff [of _ 0, simplified]
+
+end
+
+text{*Class for unital rings with characteristic zero.
+ Includes non-ordered rings like the complex numbers.*}
+class ring_char_0 = ring_1 + semiring_char_0
+begin
+
+lemma of_int_eq_iff [simp]:
+ "of_int w = of_int z \<longleftrightarrow> w = z"
+apply (cases w, cases z, simp add: of_int)
+apply (simp only: diff_eq_eq diff_add_eq eq_diff_eq)
+apply (simp only: of_nat_add [symmetric] of_nat_eq_iff)
+done
+
+text{*Special cases where either operand is zero*}
+lemmas of_int_0_eq_iff [simp] = of_int_eq_iff [of 0, simplified]
+lemmas of_int_eq_0_iff [simp] = of_int_eq_iff [of _ 0, simplified]
+
+end
+
+text{*Every @{text ordered_idom} has characteristic zero.*}
+subclass (in ordered_idom) ring_char_0 by intro_locales
+
+lemma of_int_eq_id [simp]: "of_int = id"
+proof
+ fix z show "of_int z = id z"
+ by (cases z) (simp add: of_int add minus int_def diff_minus)
+qed
+
+
+subsection {* Magnitude of an Integer, as a Natural Number: @{text nat} *}
+
+definition
+ nat :: "int \<Rightarrow> nat"
+where
+ [code func del]: "nat z = contents (\<Union>(x, y) \<in> Rep_Integ z. {x-y})"
+
+lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y"
+proof -
+ have "(\<lambda>(x,y). {x-y}) respects intrel"
+ by (simp add: congruent_def) arith
+ thus ?thesis
+ by (simp add: nat_def UN_equiv_class [OF equiv_intrel])
+qed
+
+lemma nat_int [simp]: "nat (of_nat n) = n"
+by (simp add: nat int_def)
+
+lemma nat_zero [simp]: "nat 0 = 0"
+by (simp add: Zero_int_def nat)
+
+lemma int_nat_eq [simp]: "of_nat (nat z) = (if 0 \<le> z then z else 0)"
+by (cases z, simp add: nat le int_def Zero_int_def)
+
+corollary nat_0_le: "0 \<le> z ==> of_nat (nat z) = z"
+by simp
+
+lemma nat_le_0 [simp]: "z \<le> 0 ==> nat z = 0"
+by (cases z, simp add: nat le Zero_int_def)
+
+lemma nat_le_eq_zle: "0 < w | 0 \<le> z ==> (nat w \<le> nat z) = (w\<le>z)"
+apply (cases w, cases z)
+apply (simp add: nat le linorder_not_le [symmetric] Zero_int_def, arith)
+done
+
+text{*An alternative condition is @{term "0 \<le> w"} *}
+corollary nat_mono_iff: "0 < z ==> (nat w < nat z) = (w < z)"
+by (simp add: nat_le_eq_zle linorder_not_le [symmetric])
+
+corollary nat_less_eq_zless: "0 \<le> w ==> (nat w < nat z) = (w<z)"
+by (simp add: nat_le_eq_zle linorder_not_le [symmetric])
+
+lemma zless_nat_conj [simp]: "(nat w < nat z) = (0 < z & w < z)"
+apply (cases w, cases z)
+apply (simp add: nat le Zero_int_def linorder_not_le [symmetric], arith)
+done
+
+lemma nonneg_eq_int:
+ fixes z :: int
+ assumes "0 \<le> z" and "\<And>m. z = of_nat m \<Longrightarrow> P"
+ shows P
+ using assms by (blast dest: nat_0_le sym)
+
+lemma nat_eq_iff: "(nat w = m) = (if 0 \<le> w then w = of_nat m else m=0)"
+by (cases w, simp add: nat le int_def Zero_int_def, arith)
+
+corollary nat_eq_iff2: "(m = nat w) = (if 0 \<le> w then w = of_nat m else m=0)"
+by (simp only: eq_commute [of m] nat_eq_iff)
+
+lemma nat_less_iff: "0 \<le> w ==> (nat w < m) = (w < of_nat m)"
+apply (cases w)
+apply (simp add: nat le int_def Zero_int_def linorder_not_le [symmetric], arith)
+done
+
+lemma int_eq_iff: "(of_nat m = z) = (m = nat z & 0 \<le> z)"
+by (auto simp add: nat_eq_iff2)
+
+lemma zero_less_nat_eq [simp]: "(0 < nat z) = (0 < z)"
+by (insert zless_nat_conj [of 0], auto)
+
+lemma nat_add_distrib:
+ "[| (0::int) \<le> z; 0 \<le> z' |] ==> nat (z+z') = nat z + nat z'"
+by (cases z, cases z', simp add: nat add le Zero_int_def)
+
+lemma nat_diff_distrib:
+ "[| (0::int) \<le> z'; z' \<le> z |] ==> nat (z-z') = nat z - nat z'"
+by (cases z, cases z',
+ simp add: nat add minus diff_minus le Zero_int_def)
+
+lemma nat_zminus_int [simp]: "nat (- (of_nat n)) = 0"
+by (simp add: int_def minus nat Zero_int_def)
+
+lemma zless_nat_eq_int_zless: "(m < nat z) = (of_nat m < z)"
+by (cases z, simp add: nat less int_def, arith)
+
+context ring_1
+begin
+
+lemma of_nat_nat: "0 \<le> z \<Longrightarrow> of_nat (nat z) = of_int z"
+ by (cases z rule: eq_Abs_Integ)
+ (simp add: nat le of_int Zero_int_def of_nat_diff)
+
+end
+
+
+subsection{*Lemmas about the Function @{term of_nat} and Orderings*}
+
+lemma negative_zless_0: "- (of_nat (Suc n)) < (0 \<Colon> int)"
+by (simp add: order_less_le del: of_nat_Suc)
+
+lemma negative_zless [iff]: "- (of_nat (Suc n)) < (of_nat m \<Colon> int)"
+by (rule negative_zless_0 [THEN order_less_le_trans], simp)
+
+lemma negative_zle_0: "- of_nat n \<le> (0 \<Colon> int)"
+by (simp add: minus_le_iff)
+
+lemma negative_zle [iff]: "- of_nat n \<le> (of_nat m \<Colon> int)"
+by (rule order_trans [OF negative_zle_0 of_nat_0_le_iff])
+
+lemma not_zle_0_negative [simp]: "~ (0 \<le> - (of_nat (Suc n) \<Colon> int))"
+by (subst le_minus_iff, simp del: of_nat_Suc)
+
+lemma int_zle_neg: "((of_nat n \<Colon> int) \<le> - of_nat m) = (n = 0 & m = 0)"
+by (simp add: int_def le minus Zero_int_def)
+
+lemma not_int_zless_negative [simp]: "~ ((of_nat n \<Colon> int) < - of_nat m)"
+by (simp add: linorder_not_less)
+
+lemma negative_eq_positive [simp]: "((- of_nat n \<Colon> int) = of_nat m) = (n = 0 & m = 0)"
+by (force simp add: order_eq_iff [of "- of_nat n"] int_zle_neg)
+
+lemma zle_iff_zadd: "(w\<Colon>int) \<le> z \<longleftrightarrow> (\<exists>n. z = w + of_nat n)"
+proof -
+ have "(w \<le> z) = (0 \<le> z - w)"
+ by (simp only: le_diff_eq add_0_left)
+ also have "\<dots> = (\<exists>n. z - w = of_nat n)"
+ by (auto elim: zero_le_imp_eq_int)
+ also have "\<dots> = (\<exists>n. z = w + of_nat n)"
+ by (simp only: group_simps)
+ finally show ?thesis .
+qed
+
+lemma zadd_int_left: "of_nat m + (of_nat n + z) = of_nat (m + n) + (z\<Colon>int)"
+by simp
+
+lemma int_Suc0_eq_1: "of_nat (Suc 0) = (1\<Colon>int)"
+by simp
+
+text{*This version is proved for all ordered rings, not just integers!
+ It is proved here because attribute @{text arith_split} is not available
+ in theory @{text Ring_and_Field}.
+ But is it really better than just rewriting with @{text abs_if}?*}
+lemma abs_split [arith_split,noatp]:
+ "P(abs(a::'a::ordered_idom)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
+by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
+
+lemma negD: "(x \<Colon> int) < 0 \<Longrightarrow> \<exists>n. x = - (of_nat (Suc n))"
+apply (cases x)
+apply (auto simp add: le minus Zero_int_def int_def order_less_le)
+apply (rule_tac x="y - Suc x" in exI, arith)
+done
+
+
+subsection {* Cases and induction *}
+
+text{*Now we replace the case analysis rule by a more conventional one:
+whether an integer is negative or not.*}
+
+theorem int_cases [cases type: int, case_names nonneg neg]:
+ "[|!! n. (z \<Colon> int) = of_nat n ==> P; !! n. z = - (of_nat (Suc n)) ==> P |] ==> P"
+apply (cases "z < 0", blast dest!: negD)
+apply (simp add: linorder_not_less del: of_nat_Suc)
+apply auto
+apply (blast dest: nat_0_le [THEN sym])
+done
+
+theorem int_induct [induct type: int, case_names nonneg neg]:
+ "[|!! n. P (of_nat n \<Colon> int); !!n. P (- (of_nat (Suc n))) |] ==> P z"
+ by (cases z rule: int_cases) auto
+
+text{*Contributed by Brian Huffman*}
+theorem int_diff_cases:
+ obtains (diff) m n where "(z\<Colon>int) = of_nat m - of_nat n"
+apply (cases z rule: eq_Abs_Integ)
+apply (rule_tac m=x and n=y in diff)
+apply (simp add: int_def diff_def minus add)
+done
+
+
+subsection {* Binary representation *}
+
+text {*
+ This formalization defines binary arithmetic in terms of the integers
+ rather than using a datatype. This avoids multiple representations (leading
+ zeroes, etc.) See @{text "ZF/Tools/twos-compl.ML"}, function @{text
+ int_of_binary}, for the numerical interpretation.
+
+ The representation expects that @{text "(m mod 2)"} is 0 or 1,
+ even if m is negative;
+ For instance, @{text "-5 div 2 = -3"} and @{text "-5 mod 2 = 1"}; thus
+ @{text "-5 = (-3)*2 + 1"}.
+
+ This two's complement binary representation derives from the paper
+ "An Efficient Representation of Arithmetic for Term Rewriting" by
+ Dave Cohen and Phil Watson, Rewriting Techniques and Applications,
+ Springer LNCS 488 (240-251), 1991.
+*}
+
+datatype bit = B0 | B1
+
+text{*
+ Type @{typ bit} avoids the use of type @{typ bool}, which would make
+ all of the rewrite rules higher-order.
+*}
+
+definition
+ Pls :: int where
+ [code func del]: "Pls = 0"
+
+definition
+ Min :: int where
+ [code func del]: "Min = - 1"
+
+definition
+ Bit :: "int \<Rightarrow> bit \<Rightarrow> int" (infixl "BIT" 90) where
+ [code func del]: "k BIT b = (case b of B0 \<Rightarrow> 0 | B1 \<Rightarrow> 1) + k + k"
+
+class number = type + -- {* for numeric types: nat, int, real, \dots *}
+ fixes number_of :: "int \<Rightarrow> 'a"
+
+use "Tools/numeral.ML"
+
+syntax
+ "_Numeral" :: "num_const \<Rightarrow> 'a" ("_")
+
+use "Tools/numeral_syntax.ML"
+setup NumeralSyntax.setup
+
+abbreviation
+ "Numeral0 \<equiv> number_of Pls"
+
+abbreviation
+ "Numeral1 \<equiv> number_of (Pls BIT B1)"
+
+lemma Let_number_of [simp]: "Let (number_of v) f = f (number_of v)"
+ -- {* Unfold all @{text let}s involving constants *}
+ unfolding Let_def ..
+
+definition
+ succ :: "int \<Rightarrow> int" where
+ [code func del]: "succ k = k + 1"
+
+definition
+ pred :: "int \<Rightarrow> int" where
+ [code func del]: "pred k = k - 1"
+
+lemmas
+ max_number_of [simp] = max_def
+ [of "number_of u" "number_of v", standard, simp]
+and
+ min_number_of [simp] = min_def
+ [of "number_of u" "number_of v", standard, simp]
+ -- {* unfolding @{text minx} and @{text max} on numerals *}
+
+lemmas numeral_simps =
+ succ_def pred_def Pls_def Min_def Bit_def
+
+text {* Removal of leading zeroes *}
+
+lemma Pls_0_eq [simp, code post]:
+ "Pls BIT B0 = Pls"
+ unfolding numeral_simps by simp
+
+lemma Min_1_eq [simp, code post]:
+ "Min BIT B1 = Min"
+ unfolding numeral_simps by simp
+
+
+subsection {* The Functions @{term succ}, @{term pred} and @{term uminus} *}
+
+lemma succ_Pls [simp]:
+ "succ Pls = Pls BIT B1"
+ unfolding numeral_simps by simp
+
+lemma succ_Min [simp]:
+ "succ Min = Pls"
+ unfolding numeral_simps by simp
+
+lemma succ_1 [simp]:
+ "succ (k BIT B1) = succ k BIT B0"
+ unfolding numeral_simps by simp
+
+lemma succ_0 [simp]:
+ "succ (k BIT B0) = k BIT B1"
+ unfolding numeral_simps by simp
+
+lemma pred_Pls [simp]:
+ "pred Pls = Min"
+ unfolding numeral_simps by simp
+
+lemma pred_Min [simp]:
+ "pred Min = Min BIT B0"
+ unfolding numeral_simps by simp
+
+lemma pred_1 [simp]:
+ "pred (k BIT B1) = k BIT B0"
+ unfolding numeral_simps by simp
+
+lemma pred_0 [simp]:
+ "pred (k BIT B0) = pred k BIT B1"
+ unfolding numeral_simps by simp
+
+lemma minus_Pls [simp]:
+ "- Pls = Pls"
+ unfolding numeral_simps by simp
+
+lemma minus_Min [simp]:
+ "- Min = Pls BIT B1"
+ unfolding numeral_simps by simp
+
+lemma minus_1 [simp]:
+ "- (k BIT B1) = pred (- k) BIT B1"
+ unfolding numeral_simps by simp
+
+lemma minus_0 [simp]:
+ "- (k BIT B0) = (- k) BIT B0"
+ unfolding numeral_simps by simp
+
+
+subsection {*
+ Binary Addition and Multiplication: @{term "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"}
+ and @{term "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int"}
+*}
+
+lemma add_Pls [simp]:
+ "Pls + k = k"
+ unfolding numeral_simps by simp
+
+lemma add_Min [simp]:
+ "Min + k = pred k"
+ unfolding numeral_simps by simp
+
+lemma add_BIT_11 [simp]:
+ "(k BIT B1) + (l BIT B1) = (k + succ l) BIT B0"
+ unfolding numeral_simps by simp
+
+lemma add_BIT_10 [simp]:
+ "(k BIT B1) + (l BIT B0) = (k + l) BIT B1"
+ unfolding numeral_simps by simp
+
+lemma add_BIT_0 [simp]:
+ "(k BIT B0) + (l BIT b) = (k + l) BIT b"
+ unfolding numeral_simps by simp
+
+lemma add_Pls_right [simp]:
+ "k + Pls = k"
+ unfolding numeral_simps by simp
+
+lemma add_Min_right [simp]:
+ "k + Min = pred k"
+ unfolding numeral_simps by simp
+
+lemma mult_Pls [simp]:
+ "Pls * w = Pls"
+ unfolding numeral_simps by simp
+
+lemma mult_Min [simp]:
+ "Min * k = - k"
+ unfolding numeral_simps by simp
+
+lemma mult_num1 [simp]:
+ "(k BIT B1) * l = ((k * l) BIT B0) + l"
+ unfolding numeral_simps int_distrib by simp
+
+lemma mult_num0 [simp]:
+ "(k BIT B0) * l = (k * l) BIT B0"
+ unfolding numeral_simps int_distrib by simp
+
+
+subsection {* Converting Numerals to Rings: @{term number_of} *}
+
+class number_ring = number + comm_ring_1 +
+ assumes number_of_eq: "number_of k = of_int k"
+
+text {* self-embedding of the integers *}
+
+instantiation int :: number_ring
+begin
+
+definition
+ int_number_of_def [code func del]: "number_of w = (of_int w \<Colon> int)"
+
+instance
+ by intro_classes (simp only: int_number_of_def)
+
+end
+
+lemma number_of_is_id:
+ "number_of (k::int) = k"
+ unfolding int_number_of_def by simp
+
+lemma number_of_succ:
+ "number_of (succ k) = (1 + number_of k ::'a::number_ring)"
+ unfolding number_of_eq numeral_simps by simp
+
+lemma number_of_pred:
+ "number_of (pred w) = (- 1 + number_of w ::'a::number_ring)"
+ unfolding number_of_eq numeral_simps by simp
+
+lemma number_of_minus:
+ "number_of (uminus w) = (- (number_of w)::'a::number_ring)"
+ unfolding number_of_eq numeral_simps by simp
+
+lemma number_of_add:
+ "number_of (v + w) = (number_of v + number_of w::'a::number_ring)"
+ unfolding number_of_eq numeral_simps by simp
+
+lemma number_of_mult:
+ "number_of (v * w) = (number_of v * number_of w::'a::number_ring)"
+ unfolding number_of_eq numeral_simps by simp
+
+text {*
+ The correctness of shifting.
+ But it doesn't seem to give a measurable speed-up.
+*}
+
+lemma double_number_of_BIT:
+ "(1 + 1) * number_of w = (number_of (w BIT B0) ::'a::number_ring)"
+ unfolding number_of_eq numeral_simps left_distrib by simp
+
+text {*
+ Converting numerals 0 and 1 to their abstract versions.
+*}
+
+lemma numeral_0_eq_0 [simp]:
+ "Numeral0 = (0::'a::number_ring)"
+ unfolding number_of_eq numeral_simps by simp
+
+lemma numeral_1_eq_1 [simp]:
+ "Numeral1 = (1::'a::number_ring)"
+ unfolding number_of_eq numeral_simps by simp
+
+text {*
+ Special-case simplification for small constants.
+*}
+
+text{*
+ Unary minus for the abstract constant 1. Cannot be inserted
+ as a simprule until later: it is @{text number_of_Min} re-oriented!
+*}
+
+lemma numeral_m1_eq_minus_1:
+ "(-1::'a::number_ring) = - 1"
+ unfolding number_of_eq numeral_simps by simp
+
+lemma mult_minus1 [simp]:
+ "-1 * z = -(z::'a::number_ring)"
+ unfolding number_of_eq numeral_simps by simp
+
+lemma mult_minus1_right [simp]:
+ "z * -1 = -(z::'a::number_ring)"
+ unfolding number_of_eq numeral_simps by simp
+
+(*Negation of a coefficient*)
+lemma minus_number_of_mult [simp]:
+ "- (number_of w) * z = number_of (uminus w) * (z::'a::number_ring)"
+ unfolding number_of_eq by simp
+
+text {* Subtraction *}
+
+lemma diff_number_of_eq:
+ "number_of v - number_of w =
+ (number_of (v + uminus w)::'a::number_ring)"
+ unfolding number_of_eq by simp
+
+lemma number_of_Pls:
+ "number_of Pls = (0::'a::number_ring)"
+ unfolding number_of_eq numeral_simps by simp
+
+lemma number_of_Min:
+ "number_of Min = (- 1::'a::number_ring)"
+ unfolding number_of_eq numeral_simps by simp
+
+lemma number_of_BIT:
+ "number_of(w BIT x) = (case x of B0 => 0 | B1 => (1::'a::number_ring))
+ + (number_of w) + (number_of w)"
+ unfolding number_of_eq numeral_simps by (simp split: bit.split)
+
+
+subsection {* Equality of Binary Numbers *}
+
+text {* First version by Norbert Voelker *}
+
+definition
+ neg :: "'a\<Colon>ordered_idom \<Rightarrow> bool"
+where
+ "neg Z \<longleftrightarrow> Z < 0"
+
+definition (*for simplifying equalities*)
+ iszero :: "'a\<Colon>semiring_1 \<Rightarrow> bool"
+where
+ "iszero z \<longleftrightarrow> z = 0"
+
+lemma not_neg_int [simp]: "~ neg (of_nat n)"
+by (simp add: neg_def)
+
+lemma neg_zminus_int [simp]: "neg (- (of_nat (Suc n)))"
+by (simp add: neg_def neg_less_0_iff_less del: of_nat_Suc)
+
+lemmas neg_eq_less_0 = neg_def
+
+lemma not_neg_eq_ge_0: "(~neg x) = (0 \<le> x)"
+by (simp add: neg_def linorder_not_less)
+
+text{*To simplify inequalities when Numeral1 can get simplified to 1*}
+
+lemma not_neg_0: "~ neg 0"
+by (simp add: One_int_def neg_def)
+
+lemma not_neg_1: "~ neg 1"
+by (simp add: neg_def linorder_not_less zero_le_one)
+
+lemma iszero_0: "iszero 0"
+by (simp add: iszero_def)
+
+lemma not_iszero_1: "~ iszero 1"
+by (simp add: iszero_def eq_commute)
+
+lemma neg_nat: "neg z ==> nat z = 0"
+by (simp add: neg_def order_less_imp_le)
+
+lemma not_neg_nat: "~ neg z ==> of_nat (nat z) = z"
+by (simp add: linorder_not_less neg_def)
+
+lemma eq_number_of_eq:
+ "((number_of x::'a::number_ring) = number_of y) =
+ iszero (number_of (x + uminus y) :: 'a)"
+ unfolding iszero_def number_of_add number_of_minus
+ by (simp add: compare_rls)
+
+lemma iszero_number_of_Pls:
+ "iszero ((number_of Pls)::'a::number_ring)"
+ unfolding iszero_def numeral_0_eq_0 ..
+
+lemma nonzero_number_of_Min:
+ "~ iszero ((number_of Min)::'a::number_ring)"
+ unfolding iszero_def numeral_m1_eq_minus_1 by simp
+
+
+subsection {* Comparisons, for Ordered Rings *}
+
+lemmas double_eq_0_iff = double_zero
+
+lemma le_imp_0_less:
+ assumes le: "0 \<le> z"
+ shows "(0::int) < 1 + z"
+proof -
+ have "0 \<le> z" by fact
+ also have "... < z + 1" by (rule less_add_one)
+ also have "... = 1 + z" by (simp add: add_ac)
+ finally show "0 < 1 + z" .
+qed
+
+lemma odd_nonzero:
+ "1 + z + z \<noteq> (0::int)";
+proof (cases z rule: int_cases)
+ case (nonneg n)
+ have le: "0 \<le> z+z" by (simp add: nonneg add_increasing)
+ thus ?thesis using le_imp_0_less [OF le]
+ by (auto simp add: add_assoc)
+next
+ case (neg n)
+ show ?thesis
+ proof
+ assume eq: "1 + z + z = 0"
+ have "(0::int) < 1 + (of_nat n + of_nat n)"
+ by (simp add: le_imp_0_less add_increasing)
+ also have "... = - (1 + z + z)"
+ by (simp add: neg add_assoc [symmetric])
+ also have "... = 0" by (simp add: eq)
+ finally have "0<0" ..
+ thus False by blast
+ qed
+qed
+
+lemma iszero_number_of_BIT:
+ "iszero (number_of (w BIT x)::'a) =
+ (x = B0 \<and> iszero (number_of w::'a::{ring_char_0,number_ring}))"
+proof -
+ have "(of_int w + of_int w = (0::'a)) \<Longrightarrow> (w = 0)"
+ proof -
+ assume eq: "of_int w + of_int w = (0::'a)"
+ then have "of_int (w + w) = (of_int 0 :: 'a)" by simp
+ then have "w + w = 0" by (simp only: of_int_eq_iff)
+ then show "w = 0" by (simp only: double_eq_0_iff)
+ qed
+ moreover have "1 + of_int w + of_int w \<noteq> (0::'a)"
+ proof
+ assume eq: "1 + of_int w + of_int w = (0::'a)"
+ hence "of_int (1 + w + w) = (of_int 0 :: 'a)" by simp
+ hence "1 + w + w = 0" by (simp only: of_int_eq_iff)
+ with odd_nonzero show False by blast
+ qed
+ ultimately show ?thesis
+ by (auto simp add: iszero_def number_of_eq numeral_simps
+ split: bit.split)
+qed
+
+lemma iszero_number_of_0:
+ "iszero (number_of (w BIT B0) :: 'a::{ring_char_0,number_ring}) =
+ iszero (number_of w :: 'a)"
+ by (simp only: iszero_number_of_BIT simp_thms)
+
+lemma iszero_number_of_1:
+ "~ iszero (number_of (w BIT B1)::'a::{ring_char_0,number_ring})"
+ by (simp add: iszero_number_of_BIT)
+
+
+subsection {* The Less-Than Relation *}
+
+lemma less_number_of_eq_neg:
+ "((number_of x::'a::{ordered_idom,number_ring}) < number_of y)
+ = neg (number_of (x + uminus y) :: 'a)"
+apply (subst less_iff_diff_less_0)
+apply (simp add: neg_def diff_minus number_of_add number_of_minus)
+done
+
+text {*
+ If @{term Numeral0} is rewritten to 0 then this rule can't be applied:
+ @{term Numeral0} IS @{term "number_of Pls"}
+*}
+
+lemma not_neg_number_of_Pls:
+ "~ neg (number_of Pls ::'a::{ordered_idom,number_ring})"
+ by (simp add: neg_def numeral_0_eq_0)
+
+lemma neg_number_of_Min:
+ "neg (number_of Min ::'a::{ordered_idom,number_ring})"
+ by (simp add: neg_def zero_less_one numeral_m1_eq_minus_1)
+
+lemma double_less_0_iff:
+ "(a + a < 0) = (a < (0::'a::ordered_idom))"
+proof -
+ have "(a + a < 0) = ((1+1)*a < 0)" by (simp add: left_distrib)
+ also have "... = (a < 0)"
+ by (simp add: mult_less_0_iff zero_less_two
+ order_less_not_sym [OF zero_less_two])
+ finally show ?thesis .
+qed
+
+lemma odd_less_0:
+ "(1 + z + z < 0) = (z < (0::int))";
+proof (cases z rule: int_cases)
+ case (nonneg n)
+ thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing
+ le_imp_0_less [THEN order_less_imp_le])
+next
+ case (neg n)
+ thus ?thesis by (simp del: of_nat_Suc of_nat_add
+ add: compare_rls of_nat_1 [symmetric] of_nat_add [symmetric])
+qed
+
+lemma neg_number_of_BIT:
+ "neg (number_of (w BIT x)::'a) =
+ neg (number_of w :: 'a::{ordered_idom,number_ring})"
+proof -
+ have "((1::'a) + of_int w + of_int w < 0) = (of_int (1 + w + w) < (of_int 0 :: 'a))"
+ by simp
+ also have "... = (w < 0)" by (simp only: of_int_less_iff odd_less_0)
+ finally show ?thesis
+ by ( simp add: neg_def number_of_eq numeral_simps double_less_0_iff
+ split: bit.split)
+qed
+
+
+text {* Less-Than or Equals *}
+
+text {* Reduces @{term "a\<le>b"} to @{term "~ (b<a)"} for ALL numerals. *}
+
+lemmas le_number_of_eq_not_less =
+ linorder_not_less [of "number_of w" "number_of v", symmetric,
+ standard]
+
+lemma le_number_of_eq:
+ "((number_of x::'a::{ordered_idom,number_ring}) \<le> number_of y)
+ = (~ (neg (number_of (y + uminus x) :: 'a)))"
+by (simp add: le_number_of_eq_not_less less_number_of_eq_neg)
+
+
+text {* Absolute value (@{term abs}) *}
+
+lemma abs_number_of:
+ "abs(number_of x::'a::{ordered_idom,number_ring}) =
+ (if number_of x < (0::'a) then -number_of x else number_of x)"
+ by (simp add: abs_if)
+
+
+text {* Re-orientation of the equation nnn=x *}
+
+lemma number_of_reorient:
+ "(number_of w = x) = (x = number_of w)"
+ by auto
+
+
+subsection {* Simplification of arithmetic operations on integer constants. *}
+
+lemmas arith_extra_simps [standard, simp] =
+ number_of_add [symmetric]
+ number_of_minus [symmetric] numeral_m1_eq_minus_1 [symmetric]
+ number_of_mult [symmetric]
+ diff_number_of_eq abs_number_of
+
+text {*
+ For making a minimal simpset, one must include these default simprules.
+ Also include @{text simp_thms}.
+*}
+
+lemmas arith_simps =
+ bit.distinct
+ Pls_0_eq Min_1_eq
+ pred_Pls pred_Min pred_1 pred_0
+ succ_Pls succ_Min succ_1 succ_0
+ add_Pls add_Min add_BIT_0 add_BIT_10 add_BIT_11
+ minus_Pls minus_Min minus_1 minus_0
+ mult_Pls mult_Min mult_num1 mult_num0
+ add_Pls_right add_Min_right
+ abs_zero abs_one arith_extra_simps
+
+text {* Simplification of relational operations *}
+
+lemmas rel_simps [simp] =
+ eq_number_of_eq iszero_0 nonzero_number_of_Min
+ iszero_number_of_0 iszero_number_of_1
+ less_number_of_eq_neg
+ not_neg_number_of_Pls not_neg_0 not_neg_1 not_iszero_1
+ neg_number_of_Min neg_number_of_BIT
+ le_number_of_eq
+(* iszero_number_of_Pls would never be used
+ because its lhs simplifies to "iszero 0" *)
+
+
+subsection {* Simplification of arithmetic when nested to the right. *}
+
+lemma add_number_of_left [simp]:
+ "number_of v + (number_of w + z) =
+ (number_of(v + w) + z::'a::number_ring)"
+ by (simp add: add_assoc [symmetric])
+
+lemma mult_number_of_left [simp]:
+ "number_of v * (number_of w * z) =
+ (number_of(v * w) * z::'a::number_ring)"
+ by (simp add: mult_assoc [symmetric])
+
+lemma add_number_of_diff1:
+ "number_of v + (number_of w - c) =
+ number_of(v + w) - (c::'a::number_ring)"
+ by (simp add: diff_minus add_number_of_left)
+
+lemma add_number_of_diff2 [simp]:
+ "number_of v + (c - number_of w) =
+ number_of (v + uminus w) + (c::'a::number_ring)"
+apply (subst diff_number_of_eq [symmetric])
+apply (simp only: compare_rls)
+done
+
+
+subsection {* The Set of Integers *}
+
+context ring_1
+begin
+
+definition
+ Ints :: "'a set"
+where
+ "Ints = range of_int"
+
+end
+
+notation (xsymbols)
+ Ints ("\<int>")
+
+context ring_1
+begin
+
+lemma Ints_0 [simp]: "0 \<in> \<int>"
+apply (simp add: Ints_def)
+apply (rule range_eqI)
+apply (rule of_int_0 [symmetric])
+done
+
+lemma Ints_1 [simp]: "1 \<in> \<int>"
+apply (simp add: Ints_def)
+apply (rule range_eqI)
+apply (rule of_int_1 [symmetric])
+done
+
+lemma Ints_add [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a + b \<in> \<int>"
+apply (auto simp add: Ints_def)
+apply (rule range_eqI)
+apply (rule of_int_add [symmetric])
+done
+
+lemma Ints_minus [simp]: "a \<in> \<int> \<Longrightarrow> -a \<in> \<int>"
+apply (auto simp add: Ints_def)
+apply (rule range_eqI)
+apply (rule of_int_minus [symmetric])
+done
+
+lemma Ints_mult [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a * b \<in> \<int>"
+apply (auto simp add: Ints_def)
+apply (rule range_eqI)
+apply (rule of_int_mult [symmetric])
+done
+
+lemma Ints_cases [cases set: Ints]:
+ assumes "q \<in> \<int>"
+ obtains (of_int) z where "q = of_int z"
+ unfolding Ints_def
+proof -
+ from `q \<in> \<int>` have "q \<in> range of_int" unfolding Ints_def .
+ then obtain z where "q = of_int z" ..
+ then show thesis ..
+qed
+
+lemma Ints_induct [case_names of_int, induct set: Ints]:
+ "q \<in> \<int> \<Longrightarrow> (\<And>z. P (of_int z)) \<Longrightarrow> P q"
+ by (rule Ints_cases) auto
+
+end
+
+lemma Ints_diff [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a-b \<in> \<int>"
+apply (auto simp add: Ints_def)
+apply (rule range_eqI)
+apply (rule of_int_diff [symmetric])
+done
+
+text {* The premise involving @{term Ints} prevents @{term "a = 1/2"}. *}
+
+lemma Ints_double_eq_0_iff:
+ assumes in_Ints: "a \<in> Ints"
+ shows "(a + a = 0) = (a = (0::'a::ring_char_0))"
+proof -
+ from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
+ then obtain z where a: "a = of_int z" ..
+ show ?thesis
+ proof
+ assume "a = 0"
+ thus "a + a = 0" by simp
+ next
+ assume eq: "a + a = 0"
+ hence "of_int (z + z) = (of_int 0 :: 'a)" by (simp add: a)
+ hence "z + z = 0" by (simp only: of_int_eq_iff)
+ hence "z = 0" by (simp only: double_eq_0_iff)
+ thus "a = 0" by (simp add: a)
+ qed
+qed
+
+lemma Ints_odd_nonzero:
+ assumes in_Ints: "a \<in> Ints"
+ shows "1 + a + a \<noteq> (0::'a::ring_char_0)"
+proof -
+ from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
+ then obtain z where a: "a = of_int z" ..
+ show ?thesis
+ proof
+ assume eq: "1 + a + a = 0"
+ hence "of_int (1 + z + z) = (of_int 0 :: 'a)" by (simp add: a)
+ hence "1 + z + z = 0" by (simp only: of_int_eq_iff)
+ with odd_nonzero show False by blast
+ qed
+qed
+
+lemma Ints_number_of:
+ "(number_of w :: 'a::number_ring) \<in> Ints"
+ unfolding number_of_eq Ints_def by simp
+
+lemma Ints_odd_less_0:
+ assumes in_Ints: "a \<in> Ints"
+ shows "(1 + a + a < 0) = (a < (0::'a::ordered_idom))";
+proof -
+ from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
+ then obtain z where a: "a = of_int z" ..
+ hence "((1::'a) + a + a < 0) = (of_int (1 + z + z) < (of_int 0 :: 'a))"
+ by (simp add: a)
+ also have "... = (z < 0)" by (simp only: of_int_less_iff odd_less_0)
+ also have "... = (a < 0)" by (simp add: a)
+ finally show ?thesis .
+qed
+
+
+subsection {* @{term setsum} and @{term setprod} *}
+
+text {*By Jeremy Avigad*}
+
+lemma of_nat_setsum: "of_nat (setsum f A) = (\<Sum>x\<in>A. of_nat(f x))"
+ apply (cases "finite A")
+ apply (erule finite_induct, auto)
+ done
+
+lemma of_int_setsum: "of_int (setsum f A) = (\<Sum>x\<in>A. of_int(f x))"
+ apply (cases "finite A")
+ apply (erule finite_induct, auto)
+ done
+
+lemma of_nat_setprod: "of_nat (setprod f A) = (\<Prod>x\<in>A. of_nat(f x))"
+ apply (cases "finite A")
+ apply (erule finite_induct, auto simp add: of_nat_mult)
+ done
+
+lemma of_int_setprod: "of_int (setprod f A) = (\<Prod>x\<in>A. of_int(f x))"
+ apply (cases "finite A")
+ apply (erule finite_induct, auto)
+ done
+
+lemma setprod_nonzero_nat:
+ "finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::nat)) ==> setprod f A \<noteq> 0"
+ by (rule setprod_nonzero, auto)
+
+lemma setprod_zero_eq_nat:
+ "finite A ==> (setprod f A = (0::nat)) = (\<exists>x \<in> A. f x = 0)"
+ by (rule setprod_zero_eq, auto)
+
+lemma setprod_nonzero_int:
+ "finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::int)) ==> setprod f A \<noteq> 0"
+ by (rule setprod_nonzero, auto)
+
+lemma setprod_zero_eq_int:
+ "finite A ==> (setprod f A = (0::int)) = (\<exists>x \<in> A. f x = 0)"
+ by (rule setprod_zero_eq, auto)
+
+lemmas int_setsum = of_nat_setsum [where 'a=int]
+lemmas int_setprod = of_nat_setprod [where 'a=int]
+
+
+subsection{*Inequality Reasoning for the Arithmetic Simproc*}
+
+lemma add_numeral_0: "Numeral0 + a = (a::'a::number_ring)"
+by simp
+
+lemma add_numeral_0_right: "a + Numeral0 = (a::'a::number_ring)"
+by simp
+
+lemma mult_numeral_1: "Numeral1 * a = (a::'a::number_ring)"
+by simp
+
+lemma mult_numeral_1_right: "a * Numeral1 = (a::'a::number_ring)"
+by simp
+
+lemma divide_numeral_1: "a / Numeral1 = (a::'a::{number_ring,field})"
+by simp
+
+lemma inverse_numeral_1:
+ "inverse Numeral1 = (Numeral1::'a::{number_ring,field})"
+by simp
+
+text{*Theorem lists for the cancellation simprocs. The use of binary numerals
+for 0 and 1 reduces the number of special cases.*}
+
+lemmas add_0s = add_numeral_0 add_numeral_0_right
+lemmas mult_1s = mult_numeral_1 mult_numeral_1_right
+ mult_minus1 mult_minus1_right
+
+
+subsection{*Special Arithmetic Rules for Abstract 0 and 1*}
+
+text{*Arithmetic computations are defined for binary literals, which leaves 0
+and 1 as special cases. Addition already has rules for 0, but not 1.
+Multiplication and unary minus already have rules for both 0 and 1.*}
+
+
+lemma binop_eq: "[|f x y = g x y; x = x'; y = y'|] ==> f x' y' = g x' y'"
+by simp
+
+
+lemmas add_number_of_eq = number_of_add [symmetric]
+
+text{*Allow 1 on either or both sides*}
+lemma one_add_one_is_two: "1 + 1 = (2::'a::number_ring)"
+by (simp del: numeral_1_eq_1 add: numeral_1_eq_1 [symmetric] add_number_of_eq)
+
+lemmas add_special =
+ one_add_one_is_two
+ binop_eq [of "op +", OF add_number_of_eq numeral_1_eq_1 refl, standard]
+ binop_eq [of "op +", OF add_number_of_eq refl numeral_1_eq_1, standard]
+
+text{*Allow 1 on either or both sides (1-1 already simplifies to 0)*}
+lemmas diff_special =
+ binop_eq [of "op -", OF diff_number_of_eq numeral_1_eq_1 refl, standard]
+ binop_eq [of "op -", OF diff_number_of_eq refl numeral_1_eq_1, standard]
+
+text{*Allow 0 or 1 on either side with a binary numeral on the other*}
+lemmas eq_special =
+ binop_eq [of "op =", OF eq_number_of_eq numeral_0_eq_0 refl, standard]
+ binop_eq [of "op =", OF eq_number_of_eq numeral_1_eq_1 refl, standard]
+ binop_eq [of "op =", OF eq_number_of_eq refl numeral_0_eq_0, standard]
+ binop_eq [of "op =", OF eq_number_of_eq refl numeral_1_eq_1, standard]
+
+text{*Allow 0 or 1 on either side with a binary numeral on the other*}
+lemmas less_special =
+ binop_eq [of "op <", OF less_number_of_eq_neg numeral_0_eq_0 refl, standard]
+ binop_eq [of "op <", OF less_number_of_eq_neg numeral_1_eq_1 refl, standard]
+ binop_eq [of "op <", OF less_number_of_eq_neg refl numeral_0_eq_0, standard]
+ binop_eq [of "op <", OF less_number_of_eq_neg refl numeral_1_eq_1, standard]
+
+text{*Allow 0 or 1 on either side with a binary numeral on the other*}
+lemmas le_special =
+ binop_eq [of "op \<le>", OF le_number_of_eq numeral_0_eq_0 refl, standard]
+ binop_eq [of "op \<le>", OF le_number_of_eq numeral_1_eq_1 refl, standard]
+ binop_eq [of "op \<le>", OF le_number_of_eq refl numeral_0_eq_0, standard]
+ binop_eq [of "op \<le>", OF le_number_of_eq refl numeral_1_eq_1, standard]
+
+lemmas arith_special[simp] =
+ add_special diff_special eq_special less_special le_special
+
+
+lemma min_max_01: "min (0::int) 1 = 0 & min (1::int) 0 = 0 &
+ max (0::int) 1 = 1 & max (1::int) 0 = 1"
+by(simp add:min_def max_def)
+
+lemmas min_max_special[simp] =
+ min_max_01
+ max_def[of "0::int" "number_of v", standard, simp]
+ min_def[of "0::int" "number_of v", standard, simp]
+ max_def[of "number_of u" "0::int", standard, simp]
+ min_def[of "number_of u" "0::int", standard, simp]
+ max_def[of "1::int" "number_of v", standard, simp]
+ min_def[of "1::int" "number_of v", standard, simp]
+ max_def[of "number_of u" "1::int", standard, simp]
+ min_def[of "number_of u" "1::int", standard, simp]
+
+text {* Legacy theorems *}
+
+lemmas zle_int = of_nat_le_iff [where 'a=int]
+lemmas int_int_eq = of_nat_eq_iff [where 'a=int]
+
+use "~~/src/Provers/Arith/assoc_fold.ML"
+use "int_arith1.ML"
+declaration {* K int_arith_setup *}
+
+
+subsection{*Lemmas About Small Numerals*}
+
+lemma of_int_m1 [simp]: "of_int -1 = (-1 :: 'a :: number_ring)"
+proof -
+ have "(of_int -1 :: 'a) = of_int (- 1)" by simp
+ also have "... = - of_int 1" by (simp only: of_int_minus)
+ also have "... = -1" by simp
+ finally show ?thesis .
+qed
+
+lemma abs_minus_one [simp]: "abs (-1) = (1::'a::{ordered_idom,number_ring})"
+by (simp add: abs_if)
+
+lemma abs_power_minus_one [simp]:
+ "abs(-1 ^ n) = (1::'a::{ordered_idom,number_ring,recpower})"
+by (simp add: power_abs)
+
+lemma of_int_number_of_eq:
+ "of_int (number_of v) = (number_of v :: 'a :: number_ring)"
+by (simp add: number_of_eq)
+
+text{*Lemmas for specialist use, NOT as default simprules*}
+lemma mult_2: "2 * z = (z+z::'a::number_ring)"
+proof -
+ have "2*z = (1 + 1)*z" by simp
+ also have "... = z+z" by (simp add: left_distrib)
+ finally show ?thesis .
+qed
+
+lemma mult_2_right: "z * 2 = (z+z::'a::number_ring)"
+by (subst mult_commute, rule mult_2)
+
+
+subsection{*More Inequality Reasoning*}
+
+lemma zless_add1_eq: "(w < z + (1::int)) = (w<z | w=z)"
+by arith
+
+lemma add1_zle_eq: "(w + (1::int) \<le> z) = (w<z)"
+by arith
+
+lemma zle_diff1_eq [simp]: "(w \<le> z - (1::int)) = (w<z)"
+by arith
+
+lemma zle_add1_eq_le [simp]: "(w < z + (1::int)) = (w\<le>z)"
+by arith
+
+lemma int_one_le_iff_zero_less: "((1::int) \<le> z) = (0 < z)"
+by arith
+
+
+subsection{*The Functions @{term nat} and @{term int}*}
+
+text{*Simplify the terms @{term "int 0"}, @{term "int(Suc 0)"} and
+ @{term "w + - z"}*}
+declare Zero_int_def [symmetric, simp]
+declare One_int_def [symmetric, simp]
+
+lemmas diff_int_def_symmetric = diff_int_def [symmetric, simp]
+
+lemma nat_0: "nat 0 = 0"
+by (simp add: nat_eq_iff)
+
+lemma nat_1: "nat 1 = Suc 0"
+by (subst nat_eq_iff, simp)
+
+lemma nat_2: "nat 2 = Suc (Suc 0)"
+by (subst nat_eq_iff, simp)
+
+lemma one_less_nat_eq [simp]: "(Suc 0 < nat z) = (1 < z)"
+apply (insert zless_nat_conj [of 1 z])
+apply (auto simp add: nat_1)
+done
+
+text{*This simplifies expressions of the form @{term "int n = z"} where
+ z is an integer literal.*}
+lemmas int_eq_iff_number_of [simp] = int_eq_iff [of _ "number_of v", standard]
+
+lemma split_nat [arith_split]:
+ "P(nat(i::int)) = ((\<forall>n. i = of_nat n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
+ (is "?P = (?L & ?R)")
+proof (cases "i < 0")
+ case True thus ?thesis by auto
+next
+ case False
+ have "?P = ?L"
+ proof
+ assume ?P thus ?L using False by clarsimp
+ next
+ assume ?L thus ?P using False by simp
+ qed
+ with False show ?thesis by simp
+qed
+
+context ring_1
+begin
+
+lemma of_int_of_nat:
+ "of_int k = (if k < 0 then - of_nat (nat (- k)) else of_nat (nat k))"
+proof (cases "k < 0")
+ case True then have "0 \<le> - k" by simp
+ then have "of_nat (nat (- k)) = of_int (- k)" by (rule of_nat_nat)
+ with True show ?thesis by simp
+next
+ case False then show ?thesis by (simp add: not_less of_nat_nat)
+qed
+
+end
+
+lemma nat_mult_distrib:
+ fixes z z' :: int
+ assumes "0 \<le> z"
+ shows "nat (z * z') = nat z * nat z'"
+proof (cases "0 \<le> z'")
+ case False with assms have "z * z' \<le> 0"
+ by (simp add: not_le mult_le_0_iff)
+ then have "nat (z * z') = 0" by simp
+ moreover from False have "nat z' = 0" by simp
+ ultimately show ?thesis by simp
+next
+ case True with assms have ge_0: "z * z' \<ge> 0" by (simp add: zero_le_mult_iff)
+ show ?thesis
+ by (rule injD [of "of_nat :: nat \<Rightarrow> int", OF inj_of_nat])
+ (simp only: of_nat_mult of_nat_nat [OF True]
+ of_nat_nat [OF assms] of_nat_nat [OF ge_0], simp)
+qed
+
+lemma nat_mult_distrib_neg: "z \<le> (0::int) ==> nat(z*z') = nat(-z) * nat(-z')"
+apply (rule trans)
+apply (rule_tac [2] nat_mult_distrib, auto)
+done
+
+lemma nat_abs_mult_distrib: "nat (abs (w * z)) = nat (abs w) * nat (abs z)"
+apply (cases "z=0 | w=0")
+apply (auto simp add: abs_if nat_mult_distrib [symmetric]
+ nat_mult_distrib_neg [symmetric] mult_less_0_iff)
+done
+
+
+subsection "Induction principles for int"
+
+text{*Well-founded segments of the integers*}
+
+definition
+ int_ge_less_than :: "int => (int * int) set"
+where
+ "int_ge_less_than d = {(z',z). d \<le> z' & z' < z}"
+
+theorem wf_int_ge_less_than: "wf (int_ge_less_than d)"
+proof -
+ have "int_ge_less_than d \<subseteq> measure (%z. nat (z-d))"
+ by (auto simp add: int_ge_less_than_def)
+ thus ?thesis
+ by (rule wf_subset [OF wf_measure])
+qed
+
+text{*This variant looks odd, but is typical of the relations suggested
+by RankFinder.*}
+
+definition
+ int_ge_less_than2 :: "int => (int * int) set"
+where
+ "int_ge_less_than2 d = {(z',z). d \<le> z & z' < z}"
+
+theorem wf_int_ge_less_than2: "wf (int_ge_less_than2 d)"
+proof -
+ have "int_ge_less_than2 d \<subseteq> measure (%z. nat (1+z-d))"
+ by (auto simp add: int_ge_less_than2_def)
+ thus ?thesis
+ by (rule wf_subset [OF wf_measure])
+qed
+
+abbreviation
+ int :: "nat \<Rightarrow> int"
+where
+ "int \<equiv> of_nat"
+
+(* `set:int': dummy construction *)
+theorem int_ge_induct [case_names base step, induct set: int]:
+ fixes i :: int
+ assumes ge: "k \<le> i" and
+ base: "P k" and
+ step: "\<And>i. k \<le> i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)"
+ shows "P i"
+proof -
+ { fix n have "\<And>i::int. n = nat(i-k) \<Longrightarrow> k \<le> i \<Longrightarrow> P i"
+ proof (induct n)
+ case 0
+ hence "i = k" by arith
+ thus "P i" using base by simp
+ next
+ case (Suc n)
+ then have "n = nat((i - 1) - k)" by arith
+ moreover
+ have ki1: "k \<le> i - 1" using Suc.prems by arith
+ ultimately
+ have "P(i - 1)" by(rule Suc.hyps)
+ from step[OF ki1 this] show ?case by simp
+ qed
+ }
+ with ge show ?thesis by fast
+qed
+
+ (* `set:int': dummy construction *)
+theorem int_gr_induct[case_names base step,induct set:int]:
+ assumes gr: "k < (i::int)" and
+ base: "P(k+1)" and
+ step: "\<And>i. \<lbrakk>k < i; P i\<rbrakk> \<Longrightarrow> P(i+1)"
+ shows "P i"
+apply(rule int_ge_induct[of "k + 1"])
+ using gr apply arith
+ apply(rule base)
+apply (rule step, simp+)
+done
+
+theorem int_le_induct[consumes 1,case_names base step]:
+ assumes le: "i \<le> (k::int)" and
+ base: "P(k)" and
+ step: "\<And>i. \<lbrakk>i \<le> k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
+ shows "P i"
+proof -
+ { fix n have "\<And>i::int. n = nat(k-i) \<Longrightarrow> i \<le> k \<Longrightarrow> P i"
+ proof (induct n)
+ case 0
+ hence "i = k" by arith
+ thus "P i" using base by simp
+ next
+ case (Suc n)
+ hence "n = nat(k - (i+1))" by arith
+ moreover
+ have ki1: "i + 1 \<le> k" using Suc.prems by arith
+ ultimately
+ have "P(i+1)" by(rule Suc.hyps)
+ from step[OF ki1 this] show ?case by simp
+ qed
+ }
+ with le show ?thesis by fast
+qed
+
+theorem int_less_induct [consumes 1,case_names base step]:
+ assumes less: "(i::int) < k" and
+ base: "P(k - 1)" and
+ step: "\<And>i. \<lbrakk>i < k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
+ shows "P i"
+apply(rule int_le_induct[of _ "k - 1"])
+ using less apply arith
+ apply(rule base)
+apply (rule step, simp+)
+done
+
+subsection{*Intermediate value theorems*}
+
+lemma int_val_lemma:
+ "(\<forall>i<n::nat. abs(f(i+1) - f i) \<le> 1) -->
+ f 0 \<le> k --> k \<le> f n --> (\<exists>i \<le> n. f i = (k::int))"
+apply (induct_tac "n", simp)
+apply (intro strip)
+apply (erule impE, simp)
+apply (erule_tac x = n in allE, simp)
+apply (case_tac "k = f (n+1) ")
+ apply force
+apply (erule impE)
+ apply (simp add: abs_if split add: split_if_asm)
+apply (blast intro: le_SucI)
+done
+
+lemmas nat0_intermed_int_val = int_val_lemma [rule_format (no_asm)]
+
+lemma nat_intermed_int_val:
+ "[| \<forall>i. m \<le> i & i < n --> abs(f(i + 1::nat) - f i) \<le> 1; m < n;
+ f m \<le> k; k \<le> f n |] ==> ? i. m \<le> i & i \<le> n & f i = (k::int)"
+apply (cut_tac n = "n-m" and f = "%i. f (i+m) " and k = k
+ in int_val_lemma)
+apply simp
+apply (erule exE)
+apply (rule_tac x = "i+m" in exI, arith)
+done
+
+
+subsection{*Products and 1, by T. M. Rasmussen*}
+
+lemma zabs_less_one_iff [simp]: "(\<bar>z\<bar> < 1) = (z = (0::int))"
+by arith
+
+lemma abs_zmult_eq_1: "(\<bar>m * n\<bar> = 1) ==> \<bar>m\<bar> = (1::int)"
+apply (cases "\<bar>n\<bar>=1")
+apply (simp add: abs_mult)
+apply (rule ccontr)
+apply (auto simp add: linorder_neq_iff abs_mult)
+apply (subgoal_tac "2 \<le> \<bar>m\<bar> & 2 \<le> \<bar>n\<bar>")
+ prefer 2 apply arith
+apply (subgoal_tac "2*2 \<le> \<bar>m\<bar> * \<bar>n\<bar>", simp)
+apply (rule mult_mono, auto)
+done
+
+lemma pos_zmult_eq_1_iff_lemma: "(m * n = 1) ==> m = (1::int) | m = -1"
+by (insert abs_zmult_eq_1 [of m n], arith)
+
+lemma pos_zmult_eq_1_iff: "0 < (m::int) ==> (m * n = 1) = (m = 1 & n = 1)"
+apply (auto dest: pos_zmult_eq_1_iff_lemma)
+apply (simp add: mult_commute [of m])
+apply (frule pos_zmult_eq_1_iff_lemma, auto)
+done
+
+lemma zmult_eq_1_iff: "(m*n = (1::int)) = ((m = 1 & n = 1) | (m = -1 & n = -1))"
+apply (rule iffI)
+ apply (frule pos_zmult_eq_1_iff_lemma)
+ apply (simp add: mult_commute [of m])
+ apply (frule pos_zmult_eq_1_iff_lemma, auto)
+done
+
+(* Could be simplified but Presburger only becomes available too late *)
+lemma infinite_UNIV_int: "~finite(UNIV::int set)"
+proof
+ assume "finite(UNIV::int set)"
+ moreover have "~(EX i::int. 2*i = 1)"
+ by (auto simp: pos_zmult_eq_1_iff)
+ ultimately show False using finite_UNIV_inj_surj[of "%n::int. n+n"]
+ by (simp add:inj_on_def surj_def) (blast intro:sym)
+qed
+
+
+subsection {* Configuration of the code generator *}
+
+instance int :: eq ..
+
+code_datatype Pls Min Bit "number_of \<Colon> int \<Rightarrow> int"
+
+definition
+ int_aux :: "nat \<Rightarrow> int \<Rightarrow> int" where
+ "int_aux n i = int n + i"
+
+lemma [code]:
+ "int_aux 0 i = i"
+ "int_aux (Suc n) i = int_aux n (i + 1)" -- {* tail recursive *}
+ by (simp add: int_aux_def)+
+
+lemma [code, code unfold, code inline del]:
+ "int n = int_aux n 0"
+ by (simp add: int_aux_def)
+
+definition
+ nat_aux :: "int \<Rightarrow> nat \<Rightarrow> nat" where
+ "nat_aux i n = nat i + n"
+
+lemma [code]:
+ "nat_aux i n = (if i \<le> 0 then n else nat_aux (i - 1) (Suc n))" -- {* tail recursive *}
+ by (auto simp add: nat_aux_def nat_eq_iff linorder_not_le order_less_imp_le
+ dest: zless_imp_add1_zle)
+
+lemma [code]: "nat i = nat_aux i 0"
+ by (simp add: nat_aux_def)
+
+lemma zero_is_num_zero [code func, code inline, symmetric, code post]:
+ "(0\<Colon>int) = Numeral0"
+ by simp
+
+lemma one_is_num_one [code func, code inline, symmetric, code post]:
+ "(1\<Colon>int) = Numeral1"
+ by simp
+
+code_modulename SML
+ IntDef Integer
+
+code_modulename OCaml
+ IntDef Integer
+
+code_modulename Haskell
+ IntDef Integer
+
+code_modulename SML
+ Numeral Integer
+
+code_modulename OCaml
+ Numeral Integer
+
+code_modulename Haskell
+ Numeral Integer
+
+types_code
+ "int" ("int")
+attach (term_of) {*
+val term_of_int = HOLogic.mk_number HOLogic.intT;
+*}
+attach (test) {*
+fun gen_int i =
+ let val j = one_of [~1, 1] * random_range 0 i
+ in (j, fn () => term_of_int j) end;
+*}
+
+setup {*
+let
+
+fun strip_number_of (@{term "Int.number_of :: int => int"} $ t) = t
+ | strip_number_of t = t;
+
+fun numeral_codegen thy defs gr dep module b t =
+ let val i = HOLogic.dest_numeral (strip_number_of t)
+ in
+ SOME (fst (Codegen.invoke_tycodegen thy defs dep module false (gr, HOLogic.intT)),
+ Pretty.str (string_of_int i))
+ end handle TERM _ => NONE;
+
+in
+
+Codegen.add_codegen "numeral_codegen" numeral_codegen
+
+end
+*}
+
+consts_code
+ "number_of :: int \<Rightarrow> int" ("(_)")
+ "0 :: int" ("0")
+ "1 :: int" ("1")
+ "uminus :: int => int" ("~")
+ "op + :: int => int => int" ("(_ +/ _)")
+ "op * :: int => int => int" ("(_ */ _)")
+ "op \<le> :: int => int => bool" ("(_ <=/ _)")
+ "op < :: int => int => bool" ("(_ </ _)")
+
+quickcheck_params [default_type = int]
+
+(*setup continues in theory Presburger*)
+
+hide (open) const Pls Min B0 B1 succ pred
+
+
+subsection {* Legacy theorems *}
+
+lemmas zminus_zminus = minus_minus [of "z::int", standard]
+lemmas zminus_0 = minus_zero [where 'a=int]
+lemmas zminus_zadd_distrib = minus_add_distrib [of "z::int" "w", standard]
+lemmas zadd_commute = add_commute [of "z::int" "w", standard]
+lemmas zadd_assoc = add_assoc [of "z1::int" "z2" "z3", standard]
+lemmas zadd_left_commute = add_left_commute [of "x::int" "y" "z", standard]
+lemmas zadd_ac = zadd_assoc zadd_commute zadd_left_commute
+lemmas zmult_ac = OrderedGroup.mult_ac
+lemmas zadd_0 = OrderedGroup.add_0_left [of "z::int", standard]
+lemmas zadd_0_right = OrderedGroup.add_0_left [of "z::int", standard]
+lemmas zadd_zminus_inverse2 = left_minus [of "z::int", standard]
+lemmas zmult_zminus = mult_minus_left [of "z::int" "w", standard]
+lemmas zmult_commute = mult_commute [of "z::int" "w", standard]
+lemmas zmult_assoc = mult_assoc [of "z1::int" "z2" "z3", standard]
+lemmas zadd_zmult_distrib = left_distrib [of "z1::int" "z2" "w", standard]
+lemmas zadd_zmult_distrib2 = right_distrib [of "w::int" "z1" "z2", standard]
+lemmas zdiff_zmult_distrib = left_diff_distrib [of "z1::int" "z2" "w", standard]
+lemmas zdiff_zmult_distrib2 = right_diff_distrib [of "w::int" "z1" "z2", standard]
+
+lemmas int_distrib =
+ zadd_zmult_distrib zadd_zmult_distrib2
+ zdiff_zmult_distrib zdiff_zmult_distrib2
+
+lemmas zmult_1 = mult_1_left [of "z::int", standard]
+lemmas zmult_1_right = mult_1_right [of "z::int", standard]
+
+lemmas zle_refl = order_refl [of "w::int", standard]
+lemmas zle_trans = order_trans [where 'a=int and x="i" and y="j" and z="k", standard]
+lemmas zle_anti_sym = order_antisym [of "z::int" "w", standard]
+lemmas zle_linear = linorder_linear [of "z::int" "w", standard]
+lemmas zless_linear = linorder_less_linear [where 'a = int]
+
+lemmas zadd_left_mono = add_left_mono [of "i::int" "j" "k", standard]
+lemmas zadd_strict_right_mono = add_strict_right_mono [of "i::int" "j" "k", standard]
+lemmas zadd_zless_mono = add_less_le_mono [of "w'::int" "w" "z'" "z", standard]
+
+lemmas int_0_less_1 = zero_less_one [where 'a=int]
+lemmas int_0_neq_1 = zero_neq_one [where 'a=int]
+
+lemmas inj_int = inj_of_nat [where 'a=int]
+lemmas zadd_int = of_nat_add [where 'a=int, symmetric]
+lemmas int_mult = of_nat_mult [where 'a=int]
+lemmas zmult_int = of_nat_mult [where 'a=int, symmetric]
+lemmas int_eq_0_conv = of_nat_eq_0_iff [where 'a=int and m="n", standard]
+lemmas zless_int = of_nat_less_iff [where 'a=int]
+lemmas int_less_0_conv = of_nat_less_0_iff [where 'a=int and m="k", standard]
+lemmas zero_less_int_conv = of_nat_0_less_iff [where 'a=int]
+lemmas zero_zle_int = of_nat_0_le_iff [where 'a=int]
+lemmas int_le_0_conv = of_nat_le_0_iff [where 'a=int and m="n", standard]
+lemmas int_0 = of_nat_0 [where 'a=int]
+lemmas int_1 = of_nat_1 [where 'a=int]
+lemmas int_Suc = of_nat_Suc [where 'a=int]
+lemmas abs_int_eq = abs_of_nat [where 'a=int and n="m", standard]
+lemmas of_int_int_eq = of_int_of_nat_eq [where 'a=int]
+lemmas zdiff_int = of_nat_diff [where 'a=int, symmetric]
+lemmas zless_le = less_int_def
+lemmas int_eq_of_nat = TrueI
+
+end
--- a/src/HOL/IntArith.thy Tue Jan 15 16:19:21 2008 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,422 +0,0 @@
-(* Title: HOL/IntArith.thy
- ID: $Id$
- Authors: Larry Paulson and Tobias Nipkow
-*)
-
-header {* Integer arithmetic *}
-
-theory IntArith
-imports Numeral Wellfounded_Relations
-uses
- "~~/src/Provers/Arith/assoc_fold.ML"
- "~~/src/Provers/Arith/cancel_numerals.ML"
- "~~/src/Provers/Arith/combine_numerals.ML"
- ("int_arith1.ML")
-begin
-
-subsection{*Inequality Reasoning for the Arithmetic Simproc*}
-
-lemma add_numeral_0: "Numeral0 + a = (a::'a::number_ring)"
-by simp
-
-lemma add_numeral_0_right: "a + Numeral0 = (a::'a::number_ring)"
-by simp
-
-lemma mult_numeral_1: "Numeral1 * a = (a::'a::number_ring)"
-by simp
-
-lemma mult_numeral_1_right: "a * Numeral1 = (a::'a::number_ring)"
-by simp
-
-lemma divide_numeral_1: "a / Numeral1 = (a::'a::{number_ring,field})"
-by simp
-
-lemma inverse_numeral_1:
- "inverse Numeral1 = (Numeral1::'a::{number_ring,field})"
-by simp
-
-text{*Theorem lists for the cancellation simprocs. The use of binary numerals
-for 0 and 1 reduces the number of special cases.*}
-
-lemmas add_0s = add_numeral_0 add_numeral_0_right
-lemmas mult_1s = mult_numeral_1 mult_numeral_1_right
- mult_minus1 mult_minus1_right
-
-
-subsection{*Special Arithmetic Rules for Abstract 0 and 1*}
-
-text{*Arithmetic computations are defined for binary literals, which leaves 0
-and 1 as special cases. Addition already has rules for 0, but not 1.
-Multiplication and unary minus already have rules for both 0 and 1.*}
-
-
-lemma binop_eq: "[|f x y = g x y; x = x'; y = y'|] ==> f x' y' = g x' y'"
-by simp
-
-
-lemmas add_number_of_eq = number_of_add [symmetric]
-
-text{*Allow 1 on either or both sides*}
-lemma one_add_one_is_two: "1 + 1 = (2::'a::number_ring)"
-by (simp del: numeral_1_eq_1 add: numeral_1_eq_1 [symmetric] add_number_of_eq)
-
-lemmas add_special =
- one_add_one_is_two
- binop_eq [of "op +", OF add_number_of_eq numeral_1_eq_1 refl, standard]
- binop_eq [of "op +", OF add_number_of_eq refl numeral_1_eq_1, standard]
-
-text{*Allow 1 on either or both sides (1-1 already simplifies to 0)*}
-lemmas diff_special =
- binop_eq [of "op -", OF diff_number_of_eq numeral_1_eq_1 refl, standard]
- binop_eq [of "op -", OF diff_number_of_eq refl numeral_1_eq_1, standard]
-
-text{*Allow 0 or 1 on either side with a binary numeral on the other*}
-lemmas eq_special =
- binop_eq [of "op =", OF eq_number_of_eq numeral_0_eq_0 refl, standard]
- binop_eq [of "op =", OF eq_number_of_eq numeral_1_eq_1 refl, standard]
- binop_eq [of "op =", OF eq_number_of_eq refl numeral_0_eq_0, standard]
- binop_eq [of "op =", OF eq_number_of_eq refl numeral_1_eq_1, standard]
-
-text{*Allow 0 or 1 on either side with a binary numeral on the other*}
-lemmas less_special =
- binop_eq [of "op <", OF less_number_of_eq_neg numeral_0_eq_0 refl, standard]
- binop_eq [of "op <", OF less_number_of_eq_neg numeral_1_eq_1 refl, standard]
- binop_eq [of "op <", OF less_number_of_eq_neg refl numeral_0_eq_0, standard]
- binop_eq [of "op <", OF less_number_of_eq_neg refl numeral_1_eq_1, standard]
-
-text{*Allow 0 or 1 on either side with a binary numeral on the other*}
-lemmas le_special =
- binop_eq [of "op \<le>", OF le_number_of_eq numeral_0_eq_0 refl, standard]
- binop_eq [of "op \<le>", OF le_number_of_eq numeral_1_eq_1 refl, standard]
- binop_eq [of "op \<le>", OF le_number_of_eq refl numeral_0_eq_0, standard]
- binop_eq [of "op \<le>", OF le_number_of_eq refl numeral_1_eq_1, standard]
-
-lemmas arith_special[simp] =
- add_special diff_special eq_special less_special le_special
-
-
-lemma min_max_01: "min (0::int) 1 = 0 & min (1::int) 0 = 0 &
- max (0::int) 1 = 1 & max (1::int) 0 = 1"
-by(simp add:min_def max_def)
-
-lemmas min_max_special[simp] =
- min_max_01
- max_def[of "0::int" "number_of v", standard, simp]
- min_def[of "0::int" "number_of v", standard, simp]
- max_def[of "number_of u" "0::int", standard, simp]
- min_def[of "number_of u" "0::int", standard, simp]
- max_def[of "1::int" "number_of v", standard, simp]
- min_def[of "1::int" "number_of v", standard, simp]
- max_def[of "number_of u" "1::int", standard, simp]
- min_def[of "number_of u" "1::int", standard, simp]
-
-use "int_arith1.ML"
-declaration {* K int_arith_setup *}
-
-
-subsection{*Lemmas About Small Numerals*}
-
-lemma of_int_m1 [simp]: "of_int -1 = (-1 :: 'a :: number_ring)"
-proof -
- have "(of_int -1 :: 'a) = of_int (- 1)" by simp
- also have "... = - of_int 1" by (simp only: of_int_minus)
- also have "... = -1" by simp
- finally show ?thesis .
-qed
-
-lemma abs_minus_one [simp]: "abs (-1) = (1::'a::{ordered_idom,number_ring})"
-by (simp add: abs_if)
-
-lemma abs_power_minus_one [simp]:
- "abs(-1 ^ n) = (1::'a::{ordered_idom,number_ring,recpower})"
-by (simp add: power_abs)
-
-lemma of_int_number_of_eq:
- "of_int (number_of v) = (number_of v :: 'a :: number_ring)"
-by (simp add: number_of_eq)
-
-text{*Lemmas for specialist use, NOT as default simprules*}
-lemma mult_2: "2 * z = (z+z::'a::number_ring)"
-proof -
- have "2*z = (1 + 1)*z" by simp
- also have "... = z+z" by (simp add: left_distrib)
- finally show ?thesis .
-qed
-
-lemma mult_2_right: "z * 2 = (z+z::'a::number_ring)"
-by (subst mult_commute, rule mult_2)
-
-
-subsection{*More Inequality Reasoning*}
-
-lemma zless_add1_eq: "(w < z + (1::int)) = (w<z | w=z)"
-by arith
-
-lemma add1_zle_eq: "(w + (1::int) \<le> z) = (w<z)"
-by arith
-
-lemma zle_diff1_eq [simp]: "(w \<le> z - (1::int)) = (w<z)"
-by arith
-
-lemma zle_add1_eq_le [simp]: "(w < z + (1::int)) = (w\<le>z)"
-by arith
-
-lemma int_one_le_iff_zero_less: "((1::int) \<le> z) = (0 < z)"
-by arith
-
-
-subsection{*The Functions @{term nat} and @{term int}*}
-
-text{*Simplify the terms @{term "int 0"}, @{term "int(Suc 0)"} and
- @{term "w + - z"}*}
-declare Zero_int_def [symmetric, simp]
-declare One_int_def [symmetric, simp]
-
-lemmas diff_int_def_symmetric = diff_int_def [symmetric, simp]
-
-lemma nat_0: "nat 0 = 0"
-by (simp add: nat_eq_iff)
-
-lemma nat_1: "nat 1 = Suc 0"
-by (subst nat_eq_iff, simp)
-
-lemma nat_2: "nat 2 = Suc (Suc 0)"
-by (subst nat_eq_iff, simp)
-
-lemma one_less_nat_eq [simp]: "(Suc 0 < nat z) = (1 < z)"
-apply (insert zless_nat_conj [of 1 z])
-apply (auto simp add: nat_1)
-done
-
-text{*This simplifies expressions of the form @{term "int n = z"} where
- z is an integer literal.*}
-lemmas int_eq_iff_number_of [simp] = int_eq_iff [of _ "number_of v", standard]
-
-lemma split_nat [arith_split]:
- "P(nat(i::int)) = ((\<forall>n. i = int n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
- (is "?P = (?L & ?R)")
-proof (cases "i < 0")
- case True thus ?thesis by auto
-next
- case False
- have "?P = ?L"
- proof
- assume ?P thus ?L using False by clarsimp
- next
- assume ?L thus ?P using False by simp
- qed
- with False show ?thesis by simp
-qed
-
-context ring_1
-begin
-
-lemma of_int_of_nat:
- "of_int k = (if k < 0 then - of_nat (nat (- k)) else of_nat (nat k))"
-proof (cases "k < 0")
- case True then have "0 \<le> - k" by simp
- then have "of_nat (nat (- k)) = of_int (- k)" by (rule of_nat_nat)
- with True show ?thesis by simp
-next
- case False then show ?thesis by (simp add: not_less of_nat_nat)
-qed
-
-end
-
-lemma nat_mult_distrib: "(0::int) \<le> z ==> nat (z*z') = nat z * nat z'"
-apply (cases "0 \<le> z'")
-apply (rule inj_int [THEN injD])
-apply (simp add: int_mult zero_le_mult_iff)
-apply (simp add: mult_le_0_iff)
-done
-
-lemma nat_mult_distrib_neg: "z \<le> (0::int) ==> nat(z*z') = nat(-z) * nat(-z')"
-apply (rule trans)
-apply (rule_tac [2] nat_mult_distrib, auto)
-done
-
-lemma nat_abs_mult_distrib: "nat (abs (w * z)) = nat (abs w) * nat (abs z)"
-apply (cases "z=0 | w=0")
-apply (auto simp add: abs_if nat_mult_distrib [symmetric]
- nat_mult_distrib_neg [symmetric] mult_less_0_iff)
-done
-
-
-subsection "Induction principles for int"
-
-text{*Well-founded segments of the integers*}
-
-definition
- int_ge_less_than :: "int => (int * int) set"
-where
- "int_ge_less_than d = {(z',z). d \<le> z' & z' < z}"
-
-theorem wf_int_ge_less_than: "wf (int_ge_less_than d)"
-proof -
- have "int_ge_less_than d \<subseteq> measure (%z. nat (z-d))"
- by (auto simp add: int_ge_less_than_def)
- thus ?thesis
- by (rule wf_subset [OF wf_measure])
-qed
-
-text{*This variant looks odd, but is typical of the relations suggested
-by RankFinder.*}
-
-definition
- int_ge_less_than2 :: "int => (int * int) set"
-where
- "int_ge_less_than2 d = {(z',z). d \<le> z & z' < z}"
-
-theorem wf_int_ge_less_than2: "wf (int_ge_less_than2 d)"
-proof -
- have "int_ge_less_than2 d \<subseteq> measure (%z. nat (1+z-d))"
- by (auto simp add: int_ge_less_than2_def)
- thus ?thesis
- by (rule wf_subset [OF wf_measure])
-qed
-
-(* `set:int': dummy construction *)
-theorem int_ge_induct [case_names base step, induct set:int]:
- fixes i :: int
- assumes ge: "k \<le> i" and
- base: "P k" and
- step: "\<And>i. k \<le> i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)"
- shows "P i"
-proof -
- { fix n have "\<And>i::int. n = nat(i-k) \<Longrightarrow> k \<le> i \<Longrightarrow> P i"
- proof (induct n)
- case 0
- hence "i = k" by arith
- thus "P i" using base by simp
- next
- case (Suc n)
- then have "n = nat((i - 1) - k)" by arith
- moreover
- have ki1: "k \<le> i - 1" using Suc.prems by arith
- ultimately
- have "P(i - 1)" by(rule Suc.hyps)
- from step[OF ki1 this] show ?case by simp
- qed
- }
- with ge show ?thesis by fast
-qed
-
- (* `set:int': dummy construction *)
-theorem int_gr_induct[case_names base step,induct set:int]:
- assumes gr: "k < (i::int)" and
- base: "P(k+1)" and
- step: "\<And>i. \<lbrakk>k < i; P i\<rbrakk> \<Longrightarrow> P(i+1)"
- shows "P i"
-apply(rule int_ge_induct[of "k + 1"])
- using gr apply arith
- apply(rule base)
-apply (rule step, simp+)
-done
-
-theorem int_le_induct[consumes 1,case_names base step]:
- assumes le: "i \<le> (k::int)" and
- base: "P(k)" and
- step: "\<And>i. \<lbrakk>i \<le> k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
- shows "P i"
-proof -
- { fix n have "\<And>i::int. n = nat(k-i) \<Longrightarrow> i \<le> k \<Longrightarrow> P i"
- proof (induct n)
- case 0
- hence "i = k" by arith
- thus "P i" using base by simp
- next
- case (Suc n)
- hence "n = nat(k - (i+1))" by arith
- moreover
- have ki1: "i + 1 \<le> k" using Suc.prems by arith
- ultimately
- have "P(i+1)" by(rule Suc.hyps)
- from step[OF ki1 this] show ?case by simp
- qed
- }
- with le show ?thesis by fast
-qed
-
-theorem int_less_induct [consumes 1,case_names base step]:
- assumes less: "(i::int) < k" and
- base: "P(k - 1)" and
- step: "\<And>i. \<lbrakk>i < k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
- shows "P i"
-apply(rule int_le_induct[of _ "k - 1"])
- using less apply arith
- apply(rule base)
-apply (rule step, simp+)
-done
-
-subsection{*Intermediate value theorems*}
-
-lemma int_val_lemma:
- "(\<forall>i<n::nat. abs(f(i+1) - f i) \<le> 1) -->
- f 0 \<le> k --> k \<le> f n --> (\<exists>i \<le> n. f i = (k::int))"
-apply (induct_tac "n", simp)
-apply (intro strip)
-apply (erule impE, simp)
-apply (erule_tac x = n in allE, simp)
-apply (case_tac "k = f (n+1) ")
- apply force
-apply (erule impE)
- apply (simp add: abs_if split add: split_if_asm)
-apply (blast intro: le_SucI)
-done
-
-lemmas nat0_intermed_int_val = int_val_lemma [rule_format (no_asm)]
-
-lemma nat_intermed_int_val:
- "[| \<forall>i. m \<le> i & i < n --> abs(f(i + 1::nat) - f i) \<le> 1; m < n;
- f m \<le> k; k \<le> f n |] ==> ? i. m \<le> i & i \<le> n & f i = (k::int)"
-apply (cut_tac n = "n-m" and f = "%i. f (i+m) " and k = k
- in int_val_lemma)
-apply simp
-apply (erule exE)
-apply (rule_tac x = "i+m" in exI, arith)
-done
-
-
-subsection{*Products and 1, by T. M. Rasmussen*}
-
-lemma zabs_less_one_iff [simp]: "(\<bar>z\<bar> < 1) = (z = (0::int))"
-by arith
-
-lemma abs_zmult_eq_1: "(\<bar>m * n\<bar> = 1) ==> \<bar>m\<bar> = (1::int)"
-apply (cases "\<bar>n\<bar>=1")
-apply (simp add: abs_mult)
-apply (rule ccontr)
-apply (auto simp add: linorder_neq_iff abs_mult)
-apply (subgoal_tac "2 \<le> \<bar>m\<bar> & 2 \<le> \<bar>n\<bar>")
- prefer 2 apply arith
-apply (subgoal_tac "2*2 \<le> \<bar>m\<bar> * \<bar>n\<bar>", simp)
-apply (rule mult_mono, auto)
-done
-
-lemma pos_zmult_eq_1_iff_lemma: "(m * n = 1) ==> m = (1::int) | m = -1"
-by (insert abs_zmult_eq_1 [of m n], arith)
-
-lemma pos_zmult_eq_1_iff: "0 < (m::int) ==> (m * n = 1) = (m = 1 & n = 1)"
-apply (auto dest: pos_zmult_eq_1_iff_lemma)
-apply (simp add: mult_commute [of m])
-apply (frule pos_zmult_eq_1_iff_lemma, auto)
-done
-
-lemma zmult_eq_1_iff: "(m*n = (1::int)) = ((m = 1 & n = 1) | (m = -1 & n = -1))"
-apply (rule iffI)
- apply (frule pos_zmult_eq_1_iff_lemma)
- apply (simp add: mult_commute [of m])
- apply (frule pos_zmult_eq_1_iff_lemma, auto)
-done
-
-(* Could be simplified but Presburger only becomes available too late *)
-lemma infinite_UNIV_int: "~finite(UNIV::int set)"
-proof
- assume "finite(UNIV::int set)"
- moreover have "~(EX i::int. 2*i = 1)"
- by (auto simp: pos_zmult_eq_1_iff)
- ultimately show False using finite_UNIV_inj_surj[of "%n::int. n+n"]
- by (simp add:inj_on_def surj_def) (blast intro:sym)
-qed
-
-end
--- a/src/HOL/IntDef.thy Tue Jan 15 16:19:21 2008 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,773 +0,0 @@
-(* Title: IntDef.thy
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1996 University of Cambridge
-
-*)
-
-header{*The Integers as Equivalence Classes over Pairs of Natural Numbers*}
-
-theory IntDef
-imports Equiv_Relations Nat
-begin
-
-text {* the equivalence relation underlying the integers *}
-
-definition
- intrel :: "((nat \<times> nat) \<times> (nat \<times> nat)) set"
-where
- "intrel = {((x, y), (u, v)) | x y u v. x + v = u +y }"
-
-typedef (Integ)
- int = "UNIV//intrel"
- by (auto simp add: quotient_def)
-
-instantiation int :: "{zero, one, plus, minus, uminus, times, ord, abs, sgn}"
-begin
-
-definition
- Zero_int_def [code func del]: "0 = Abs_Integ (intrel `` {(0, 0)})"
-
-definition
- One_int_def [code func del]: "1 = Abs_Integ (intrel `` {(1, 0)})"
-
-definition
- add_int_def [code func del]: "z + w = Abs_Integ
- (\<Union>(x, y) \<in> Rep_Integ z. \<Union>(u, v) \<in> Rep_Integ w.
- intrel `` {(x + u, y + v)})"
-
-definition
- minus_int_def [code func del]:
- "- z = Abs_Integ (\<Union>(x, y) \<in> Rep_Integ z. intrel `` {(y, x)})"
-
-definition
- diff_int_def [code func del]: "z - w = z + (-w \<Colon> int)"
-
-definition
- mult_int_def [code func del]: "z * w = Abs_Integ
- (\<Union>(x, y) \<in> Rep_Integ z. \<Union>(u,v ) \<in> Rep_Integ w.
- intrel `` {(x*u + y*v, x*v + y*u)})"
-
-definition
- le_int_def [code func del]:
- "z \<le> w \<longleftrightarrow> (\<exists>x y u v. x+v \<le> u+y \<and> (x, y) \<in> Rep_Integ z \<and> (u, v) \<in> Rep_Integ w)"
-
-definition
- less_int_def [code func del]: "(z\<Colon>int) < w \<longleftrightarrow> z \<le> w \<and> z \<noteq> w"
-
-definition
- zabs_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"
-
-definition
- zsgn_def: "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
-
-instance ..
-
-end
-
-
-subsection{*Construction of the Integers*}
-
-lemma intrel_iff [simp]: "(((x,y),(u,v)) \<in> intrel) = (x+v = u+y)"
-by (simp add: intrel_def)
-
-lemma equiv_intrel: "equiv UNIV intrel"
-by (simp add: intrel_def equiv_def refl_def sym_def trans_def)
-
-text{*Reduces equality of equivalence classes to the @{term intrel} relation:
- @{term "(intrel `` {x} = intrel `` {y}) = ((x,y) \<in> intrel)"} *}
-lemmas equiv_intrel_iff [simp] = eq_equiv_class_iff [OF equiv_intrel UNIV_I UNIV_I]
-
-text{*All equivalence classes belong to set of representatives*}
-lemma [simp]: "intrel``{(x,y)} \<in> Integ"
-by (auto simp add: Integ_def intrel_def quotient_def)
-
-text{*Reduces equality on abstractions to equality on representatives:
- @{prop "\<lbrakk>x \<in> Integ; y \<in> Integ\<rbrakk> \<Longrightarrow> (Abs_Integ x = Abs_Integ y) = (x=y)"} *}
-declare Abs_Integ_inject [simp,noatp] Abs_Integ_inverse [simp,noatp]
-
-text{*Case analysis on the representation of an integer as an equivalence
- class of pairs of naturals.*}
-lemma eq_Abs_Integ [case_names Abs_Integ, cases type: int]:
- "(!!x y. z = Abs_Integ(intrel``{(x,y)}) ==> P) ==> P"
-apply (rule Abs_Integ_cases [of z])
-apply (auto simp add: Integ_def quotient_def)
-done
-
-
-subsection{*Arithmetic Operations*}
-
-lemma minus: "- Abs_Integ(intrel``{(x,y)}) = Abs_Integ(intrel `` {(y,x)})"
-proof -
- have "(\<lambda>(x,y). intrel``{(y,x)}) respects intrel"
- by (simp add: congruent_def)
- thus ?thesis
- by (simp add: minus_int_def UN_equiv_class [OF equiv_intrel])
-qed
-
-lemma add:
- "Abs_Integ (intrel``{(x,y)}) + Abs_Integ (intrel``{(u,v)}) =
- Abs_Integ (intrel``{(x+u, y+v)})"
-proof -
- have "(\<lambda>z w. (\<lambda>(x,y). (\<lambda>(u,v). intrel `` {(x+u, y+v)}) w) z)
- respects2 intrel"
- by (simp add: congruent2_def)
- thus ?thesis
- by (simp add: add_int_def UN_UN_split_split_eq
- UN_equiv_class2 [OF equiv_intrel equiv_intrel])
-qed
-
-text{*Congruence property for multiplication*}
-lemma mult_congruent2:
- "(%p1 p2. (%(x,y). (%(u,v). intrel``{(x*u + y*v, x*v + y*u)}) p2) p1)
- respects2 intrel"
-apply (rule equiv_intrel [THEN congruent2_commuteI])
- apply (force simp add: mult_ac, clarify)
-apply (simp add: congruent_def mult_ac)
-apply (rename_tac u v w x y z)
-apply (subgoal_tac "u*y + x*y = w*y + v*y & u*z + x*z = w*z + v*z")
-apply (simp add: mult_ac)
-apply (simp add: add_mult_distrib [symmetric])
-done
-
-lemma mult:
- "Abs_Integ((intrel``{(x,y)})) * Abs_Integ((intrel``{(u,v)})) =
- Abs_Integ(intrel `` {(x*u + y*v, x*v + y*u)})"
-by (simp add: mult_int_def UN_UN_split_split_eq mult_congruent2
- UN_equiv_class2 [OF equiv_intrel equiv_intrel])
-
-text{*The integers form a @{text comm_ring_1}*}
-instance int :: comm_ring_1
-proof
- fix i j k :: int
- show "(i + j) + k = i + (j + k)"
- by (cases i, cases j, cases k) (simp add: add add_assoc)
- show "i + j = j + i"
- by (cases i, cases j) (simp add: add_ac add)
- show "0 + i = i"
- by (cases i) (simp add: Zero_int_def add)
- show "- i + i = 0"
- by (cases i) (simp add: Zero_int_def minus add)
- show "i - j = i + - j"
- by (simp add: diff_int_def)
- show "(i * j) * k = i * (j * k)"
- by (cases i, cases j, cases k) (simp add: mult ring_simps)
- show "i * j = j * i"
- by (cases i, cases j) (simp add: mult ring_simps)
- show "1 * i = i"
- by (cases i) (simp add: One_int_def mult)
- show "(i + j) * k = i * k + j * k"
- by (cases i, cases j, cases k) (simp add: add mult ring_simps)
- show "0 \<noteq> (1::int)"
- by (simp add: Zero_int_def One_int_def)
-qed
-
-lemma int_def: "of_nat m = Abs_Integ (intrel `` {(m, 0)})"
-by (induct m, simp_all add: Zero_int_def One_int_def add)
-
-
-subsection{*The @{text "\<le>"} Ordering*}
-
-lemma le:
- "(Abs_Integ(intrel``{(x,y)}) \<le> Abs_Integ(intrel``{(u,v)})) = (x+v \<le> u+y)"
-by (force simp add: le_int_def)
-
-lemma less:
- "(Abs_Integ(intrel``{(x,y)}) < Abs_Integ(intrel``{(u,v)})) = (x+v < u+y)"
-by (simp add: less_int_def le order_less_le)
-
-instance int :: linorder
-proof
- fix i j k :: int
- show "(i < j) = (i \<le> j \<and> i \<noteq> j)"
- by (simp add: less_int_def)
- show "i \<le> i"
- by (cases i) (simp add: le)
- show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k"
- by (cases i, cases j, cases k) (simp add: le)
- show "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j"
- by (cases i, cases j) (simp add: le)
- show "i \<le> j \<or> j \<le> i"
- by (cases i, cases j) (simp add: le linorder_linear)
-qed
-
-instance int :: pordered_cancel_ab_semigroup_add
-proof
- fix i j k :: int
- show "i \<le> j \<Longrightarrow> k + i \<le> k + j"
- by (cases i, cases j, cases k) (simp add: le add)
-qed
-
-text{*Strict Monotonicity of Multiplication*}
-
-text{*strict, in 1st argument; proof is by induction on k>0*}
-lemma zmult_zless_mono2_lemma:
- "(i::int)<j ==> 0<k ==> of_nat k * i < of_nat k * j"
-apply (induct "k", simp)
-apply (simp add: left_distrib)
-apply (case_tac "k=0")
-apply (simp_all add: add_strict_mono)
-done
-
-lemma zero_le_imp_eq_int: "(0::int) \<le> k ==> \<exists>n. k = of_nat n"
-apply (cases k)
-apply (auto simp add: le add int_def Zero_int_def)
-apply (rule_tac x="x-y" in exI, simp)
-done
-
-lemma zero_less_imp_eq_int: "(0::int) < k ==> \<exists>n>0. k = of_nat n"
-apply (cases k)
-apply (simp add: less int_def Zero_int_def)
-apply (rule_tac x="x-y" in exI, simp)
-done
-
-lemma zmult_zless_mono2: "[| i<j; (0::int) < k |] ==> k*i < k*j"
-apply (drule zero_less_imp_eq_int)
-apply (auto simp add: zmult_zless_mono2_lemma)
-done
-
-instantiation int :: distrib_lattice
-begin
-
-definition
- "(inf \<Colon> int \<Rightarrow> int \<Rightarrow> int) = min"
-
-definition
- "(sup \<Colon> int \<Rightarrow> int \<Rightarrow> int) = max"
-
-instance
- by intro_classes
- (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1)
-
-end
-
-text{*The integers form an ordered integral domain*}
-instance int :: ordered_idom
-proof
- fix i j k :: int
- show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"
- by (rule zmult_zless_mono2)
- show "\<bar>i\<bar> = (if i < 0 then -i else i)"
- by (simp only: zabs_def)
- show "sgn(i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
- by (simp only: zsgn_def)
-qed
-
-lemma zless_imp_add1_zle: "w<z ==> w + (1::int) \<le> z"
-apply (cases w, cases z)
-apply (simp add: less le add One_int_def)
-done
-
-
-subsection{*Magnitude of an Integer, as a Natural Number: @{term nat}*}
-
-definition
- nat :: "int \<Rightarrow> nat"
-where
- [code func del]: "nat z = contents (\<Union>(x, y) \<in> Rep_Integ z. {x-y})"
-
-lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y"
-proof -
- have "(\<lambda>(x,y). {x-y}) respects intrel"
- by (simp add: congruent_def) arith
- thus ?thesis
- by (simp add: nat_def UN_equiv_class [OF equiv_intrel])
-qed
-
-lemma nat_int [simp]: "nat (of_nat n) = n"
-by (simp add: nat int_def)
-
-lemma nat_zero [simp]: "nat 0 = 0"
-by (simp add: Zero_int_def nat)
-
-lemma int_nat_eq [simp]: "of_nat (nat z) = (if 0 \<le> z then z else 0)"
-by (cases z, simp add: nat le int_def Zero_int_def)
-
-corollary nat_0_le: "0 \<le> z ==> of_nat (nat z) = z"
-by simp
-
-lemma nat_le_0 [simp]: "z \<le> 0 ==> nat z = 0"
-by (cases z, simp add: nat le Zero_int_def)
-
-lemma nat_le_eq_zle: "0 < w | 0 \<le> z ==> (nat w \<le> nat z) = (w\<le>z)"
-apply (cases w, cases z)
-apply (simp add: nat le linorder_not_le [symmetric] Zero_int_def, arith)
-done
-
-text{*An alternative condition is @{term "0 \<le> w"} *}
-corollary nat_mono_iff: "0 < z ==> (nat w < nat z) = (w < z)"
-by (simp add: nat_le_eq_zle linorder_not_le [symmetric])
-
-corollary nat_less_eq_zless: "0 \<le> w ==> (nat w < nat z) = (w<z)"
-by (simp add: nat_le_eq_zle linorder_not_le [symmetric])
-
-lemma zless_nat_conj [simp]: "(nat w < nat z) = (0 < z & w < z)"
-apply (cases w, cases z)
-apply (simp add: nat le Zero_int_def linorder_not_le [symmetric], arith)
-done
-
-lemma nonneg_eq_int:
- fixes z :: int
- assumes "0 \<le> z" and "\<And>m. z = of_nat m \<Longrightarrow> P"
- shows P
- using assms by (blast dest: nat_0_le sym)
-
-lemma nat_eq_iff: "(nat w = m) = (if 0 \<le> w then w = of_nat m else m=0)"
-by (cases w, simp add: nat le int_def Zero_int_def, arith)
-
-corollary nat_eq_iff2: "(m = nat w) = (if 0 \<le> w then w = of_nat m else m=0)"
-by (simp only: eq_commute [of m] nat_eq_iff)
-
-lemma nat_less_iff: "0 \<le> w ==> (nat w < m) = (w < of_nat m)"
-apply (cases w)
-apply (simp add: nat le int_def Zero_int_def linorder_not_le [symmetric], arith)
-done
-
-lemma int_eq_iff: "(of_nat m = z) = (m = nat z & 0 \<le> z)"
-by (auto simp add: nat_eq_iff2)
-
-lemma zero_less_nat_eq [simp]: "(0 < nat z) = (0 < z)"
-by (insert zless_nat_conj [of 0], auto)
-
-lemma nat_add_distrib:
- "[| (0::int) \<le> z; 0 \<le> z' |] ==> nat (z+z') = nat z + nat z'"
-by (cases z, cases z', simp add: nat add le Zero_int_def)
-
-lemma nat_diff_distrib:
- "[| (0::int) \<le> z'; z' \<le> z |] ==> nat (z-z') = nat z - nat z'"
-by (cases z, cases z',
- simp add: nat add minus diff_minus le Zero_int_def)
-
-lemma nat_zminus_int [simp]: "nat (- (of_nat n)) = 0"
-by (simp add: int_def minus nat Zero_int_def)
-
-lemma zless_nat_eq_int_zless: "(m < nat z) = (of_nat m < z)"
-by (cases z, simp add: nat less int_def, arith)
-
-
-subsection{*Lemmas about the Function @{term of_nat} and Orderings*}
-
-lemma negative_zless_0: "- (of_nat (Suc n)) < (0 \<Colon> int)"
-by (simp add: order_less_le del: of_nat_Suc)
-
-lemma negative_zless [iff]: "- (of_nat (Suc n)) < (of_nat m \<Colon> int)"
-by (rule negative_zless_0 [THEN order_less_le_trans], simp)
-
-lemma negative_zle_0: "- of_nat n \<le> (0 \<Colon> int)"
-by (simp add: minus_le_iff)
-
-lemma negative_zle [iff]: "- of_nat n \<le> (of_nat m \<Colon> int)"
-by (rule order_trans [OF negative_zle_0 of_nat_0_le_iff])
-
-lemma not_zle_0_negative [simp]: "~ (0 \<le> - (of_nat (Suc n) \<Colon> int))"
-by (subst le_minus_iff, simp del: of_nat_Suc)
-
-lemma int_zle_neg: "((of_nat n \<Colon> int) \<le> - of_nat m) = (n = 0 & m = 0)"
-by (simp add: int_def le minus Zero_int_def)
-
-lemma not_int_zless_negative [simp]: "~ ((of_nat n \<Colon> int) < - of_nat m)"
-by (simp add: linorder_not_less)
-
-lemma negative_eq_positive [simp]: "((- of_nat n \<Colon> int) = of_nat m) = (n = 0 & m = 0)"
-by (force simp add: order_eq_iff [of "- of_nat n"] int_zle_neg)
-
-lemma zle_iff_zadd: "(w\<Colon>int) \<le> z \<longleftrightarrow> (\<exists>n. z = w + of_nat n)"
-proof -
- have "(w \<le> z) = (0 \<le> z - w)"
- by (simp only: le_diff_eq add_0_left)
- also have "\<dots> = (\<exists>n. z - w = of_nat n)"
- by (auto elim: zero_le_imp_eq_int)
- also have "\<dots> = (\<exists>n. z = w + of_nat n)"
- by (simp only: group_simps)
- finally show ?thesis .
-qed
-
-lemma zadd_int_left: "of_nat m + (of_nat n + z) = of_nat (m + n) + (z\<Colon>int)"
-by simp
-
-lemma int_Suc0_eq_1: "of_nat (Suc 0) = (1\<Colon>int)"
-by simp
-
-text{*This version is proved for all ordered rings, not just integers!
- It is proved here because attribute @{text arith_split} is not available
- in theory @{text Ring_and_Field}.
- But is it really better than just rewriting with @{text abs_if}?*}
-lemma abs_split [arith_split,noatp]:
- "P(abs(a::'a::ordered_idom)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
-by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
-
-
-subsection {* Constants @{term neg} and @{term iszero} *}
-
-definition
- neg :: "'a\<Colon>ordered_idom \<Rightarrow> bool"
-where
- "neg Z \<longleftrightarrow> Z < 0"
-
-definition (*for simplifying equalities*)
- iszero :: "'a\<Colon>semiring_1 \<Rightarrow> bool"
-where
- "iszero z \<longleftrightarrow> z = 0"
-
-lemma not_neg_int [simp]: "~ neg (of_nat n)"
-by (simp add: neg_def)
-
-lemma neg_zminus_int [simp]: "neg (- (of_nat (Suc n)))"
-by (simp add: neg_def neg_less_0_iff_less del: of_nat_Suc)
-
-lemmas neg_eq_less_0 = neg_def
-
-lemma not_neg_eq_ge_0: "(~neg x) = (0 \<le> x)"
-by (simp add: neg_def linorder_not_less)
-
-
-text{*To simplify inequalities when Numeral1 can get simplified to 1*}
-
-lemma not_neg_0: "~ neg 0"
-by (simp add: One_int_def neg_def)
-
-lemma not_neg_1: "~ neg 1"
-by (simp add: neg_def linorder_not_less zero_le_one)
-
-lemma iszero_0: "iszero 0"
-by (simp add: iszero_def)
-
-lemma not_iszero_1: "~ iszero 1"
-by (simp add: iszero_def eq_commute)
-
-lemma neg_nat: "neg z ==> nat z = 0"
-by (simp add: neg_def order_less_imp_le)
-
-lemma not_neg_nat: "~ neg z ==> of_nat (nat z) = z"
-by (simp add: linorder_not_less neg_def)
-
-
-subsection{*Embedding of the Integers into any @{text ring_1}: @{term of_int}*}
-
-context ring_1
-begin
-
-term of_nat
-
-definition
- of_int :: "int \<Rightarrow> 'a"
-where
- "of_int z = contents (\<Union>(i, j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
-lemmas [code func del] = of_int_def
-
-lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j"
-proof -
- have "(\<lambda>(i,j). { of_nat i - (of_nat j :: 'a) }) respects intrel"
- by (simp add: congruent_def compare_rls of_nat_add [symmetric]
- del: of_nat_add)
- thus ?thesis
- by (simp add: of_int_def UN_equiv_class [OF equiv_intrel])
-qed
-
-lemma of_int_0 [simp]: "of_int 0 = 0"
-by (simp add: of_int Zero_int_def)
-
-lemma of_int_1 [simp]: "of_int 1 = 1"
-by (simp add: of_int One_int_def)
-
-lemma of_int_add [simp]: "of_int (w+z) = of_int w + of_int z"
-by (cases w, cases z, simp add: compare_rls of_int add)
-
-lemma of_int_minus [simp]: "of_int (-z) = - (of_int z)"
-by (cases z, simp add: compare_rls of_int minus)
-
-lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z"
-apply (cases w, cases z)
-apply (simp add: compare_rls of_int left_diff_distrib right_diff_distrib
- mult add_ac of_nat_mult)
-done
-
-text{*Collapse nested embeddings*}
-lemma of_int_of_nat_eq [simp]: "of_int (Nat.of_nat n) = of_nat n"
- by (induct n, auto)
-
-end
-
-lemma of_int_diff [simp]: "of_int (w-z) = of_int w - of_int z"
-by (simp add: diff_minus)
-
-lemma of_int_le_iff [simp]:
- "(of_int w \<le> (of_int z::'a::ordered_idom)) = (w \<le> z)"
-apply (cases w)
-apply (cases z)
-apply (simp add: compare_rls of_int le diff_int_def add minus
- of_nat_add [symmetric] del: of_nat_add)
-done
-
-text{*Special cases where either operand is zero*}
-lemmas of_int_0_le_iff [simp] = of_int_le_iff [of 0, simplified]
-lemmas of_int_le_0_iff [simp] = of_int_le_iff [of _ 0, simplified]
-
-lemma of_int_less_iff [simp]:
- "(of_int w < (of_int z::'a::ordered_idom)) = (w < z)"
-by (simp add: linorder_not_le [symmetric])
-
-text{*Special cases where either operand is zero*}
-lemmas of_int_0_less_iff [simp] = of_int_less_iff [of 0, simplified]
-lemmas of_int_less_0_iff [simp] = of_int_less_iff [of _ 0, simplified]
-
-text{*Class for unital rings with characteristic zero.
- Includes non-ordered rings like the complex numbers.*}
-class ring_char_0 = ring_1 + semiring_char_0
-begin
-
-lemma of_int_eq_iff [simp]:
- "of_int w = of_int z \<longleftrightarrow> w = z"
-apply (cases w, cases z, simp add: of_int)
-apply (simp only: diff_eq_eq diff_add_eq eq_diff_eq)
-apply (simp only: of_nat_add [symmetric] of_nat_eq_iff)
-done
-
-text{*Special cases where either operand is zero*}
-lemmas of_int_0_eq_iff [simp] = of_int_eq_iff [of 0, simplified]
-lemmas of_int_eq_0_iff [simp] = of_int_eq_iff [of _ 0, simplified]
-
-end
-
-text{*Every @{text ordered_idom} has characteristic zero.*}
-instance ordered_idom \<subseteq> ring_char_0 ..
-
-lemma of_int_eq_id [simp]: "of_int = id"
-proof
- fix z show "of_int z = id z"
- by (cases z) (simp add: of_int add minus int_def diff_minus)
-qed
-
-context ring_1
-begin
-
-lemma of_nat_nat: "0 \<le> z \<Longrightarrow> of_nat (nat z) = of_int z"
- by (cases z rule: eq_Abs_Integ)
- (simp add: nat le of_int Zero_int_def of_nat_diff)
-
-end
-
-
-subsection{*The Set of Integers*}
-
-context ring_1
-begin
-
-definition
- Ints :: "'a set"
-where
- "Ints = range of_int"
-
-end
-
-notation (xsymbols)
- Ints ("\<int>")
-
-context ring_1
-begin
-
-lemma Ints_0 [simp]: "0 \<in> \<int>"
-apply (simp add: Ints_def)
-apply (rule range_eqI)
-apply (rule of_int_0 [symmetric])
-done
-
-lemma Ints_1 [simp]: "1 \<in> \<int>"
-apply (simp add: Ints_def)
-apply (rule range_eqI)
-apply (rule of_int_1 [symmetric])
-done
-
-lemma Ints_add [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a + b \<in> \<int>"
-apply (auto simp add: Ints_def)
-apply (rule range_eqI)
-apply (rule of_int_add [symmetric])
-done
-
-lemma Ints_minus [simp]: "a \<in> \<int> \<Longrightarrow> -a \<in> \<int>"
-apply (auto simp add: Ints_def)
-apply (rule range_eqI)
-apply (rule of_int_minus [symmetric])
-done
-
-lemma Ints_mult [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a * b \<in> \<int>"
-apply (auto simp add: Ints_def)
-apply (rule range_eqI)
-apply (rule of_int_mult [symmetric])
-done
-
-lemma Ints_cases [cases set: Ints]:
- assumes "q \<in> \<int>"
- obtains (of_int) z where "q = of_int z"
- unfolding Ints_def
-proof -
- from `q \<in> \<int>` have "q \<in> range of_int" unfolding Ints_def .
- then obtain z where "q = of_int z" ..
- then show thesis ..
-qed
-
-lemma Ints_induct [case_names of_int, induct set: Ints]:
- "q \<in> \<int> \<Longrightarrow> (\<And>z. P (of_int z)) \<Longrightarrow> P q"
- by (rule Ints_cases) auto
-
-end
-
-lemma Ints_diff [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a-b \<in> \<int>"
-apply (auto simp add: Ints_def)
-apply (rule range_eqI)
-apply (rule of_int_diff [symmetric])
-done
-
-
-subsection {* @{term setsum} and @{term setprod} *}
-
-text {*By Jeremy Avigad*}
-
-lemma of_nat_setsum: "of_nat (setsum f A) = (\<Sum>x\<in>A. of_nat(f x))"
- apply (cases "finite A")
- apply (erule finite_induct, auto)
- done
-
-lemma of_int_setsum: "of_int (setsum f A) = (\<Sum>x\<in>A. of_int(f x))"
- apply (cases "finite A")
- apply (erule finite_induct, auto)
- done
-
-lemma of_nat_setprod: "of_nat (setprod f A) = (\<Prod>x\<in>A. of_nat(f x))"
- apply (cases "finite A")
- apply (erule finite_induct, auto simp add: of_nat_mult)
- done
-
-lemma of_int_setprod: "of_int (setprod f A) = (\<Prod>x\<in>A. of_int(f x))"
- apply (cases "finite A")
- apply (erule finite_induct, auto)
- done
-
-lemma setprod_nonzero_nat:
- "finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::nat)) ==> setprod f A \<noteq> 0"
- by (rule setprod_nonzero, auto)
-
-lemma setprod_zero_eq_nat:
- "finite A ==> (setprod f A = (0::nat)) = (\<exists>x \<in> A. f x = 0)"
- by (rule setprod_zero_eq, auto)
-
-lemma setprod_nonzero_int:
- "finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::int)) ==> setprod f A \<noteq> 0"
- by (rule setprod_nonzero, auto)
-
-lemma setprod_zero_eq_int:
- "finite A ==> (setprod f A = (0::int)) = (\<exists>x \<in> A. f x = 0)"
- by (rule setprod_zero_eq, auto)
-
-lemmas int_setsum = of_nat_setsum [where 'a=int]
-lemmas int_setprod = of_nat_setprod [where 'a=int]
-
-
-subsection {* Further properties *}
-
-text{*Now we replace the case analysis rule by a more conventional one:
-whether an integer is negative or not.*}
-
-lemma zless_iff_Suc_zadd:
- "(w \<Colon> int) < z \<longleftrightarrow> (\<exists>n. z = w + of_nat (Suc n))"
-apply (cases z, cases w)
-apply (auto simp add: less add int_def)
-apply (rename_tac a b c d)
-apply (rule_tac x="a+d - Suc(c+b)" in exI)
-apply arith
-done
-
-lemma negD: "(x \<Colon> int) < 0 \<Longrightarrow> \<exists>n. x = - (of_nat (Suc n))"
-apply (cases x)
-apply (auto simp add: le minus Zero_int_def int_def order_less_le)
-apply (rule_tac x="y - Suc x" in exI, arith)
-done
-
-theorem int_cases [cases type: int, case_names nonneg neg]:
- "[|!! n. (z \<Colon> int) = of_nat n ==> P; !! n. z = - (of_nat (Suc n)) ==> P |] ==> P"
-apply (cases "z < 0", blast dest!: negD)
-apply (simp add: linorder_not_less del: of_nat_Suc)
-apply (blast dest: nat_0_le [THEN sym])
-done
-
-theorem int_induct [induct type: int, case_names nonneg neg]:
- "[|!! n. P (of_nat n \<Colon> int); !!n. P (- (of_nat (Suc n))) |] ==> P z"
- by (cases z rule: int_cases) auto
-
-text{*Contributed by Brian Huffman*}
-theorem int_diff_cases:
- obtains (diff) m n where "(z\<Colon>int) = of_nat m - of_nat n"
-apply (cases z rule: eq_Abs_Integ)
-apply (rule_tac m=x and n=y in diff)
-apply (simp add: int_def diff_def minus add)
-done
-
-
-subsection {* Legacy theorems *}
-
-lemmas zminus_zminus = minus_minus [of "z::int", standard]
-lemmas zminus_0 = minus_zero [where 'a=int]
-lemmas zminus_zadd_distrib = minus_add_distrib [of "z::int" "w", standard]
-lemmas zadd_commute = add_commute [of "z::int" "w", standard]
-lemmas zadd_assoc = add_assoc [of "z1::int" "z2" "z3", standard]
-lemmas zadd_left_commute = add_left_commute [of "x::int" "y" "z", standard]
-lemmas zadd_ac = zadd_assoc zadd_commute zadd_left_commute
-lemmas zmult_ac = OrderedGroup.mult_ac
-lemmas zadd_0 = OrderedGroup.add_0_left [of "z::int", standard]
-lemmas zadd_0_right = OrderedGroup.add_0_left [of "z::int", standard]
-lemmas zadd_zminus_inverse2 = left_minus [of "z::int", standard]
-lemmas zmult_zminus = mult_minus_left [of "z::int" "w", standard]
-lemmas zmult_commute = mult_commute [of "z::int" "w", standard]
-lemmas zmult_assoc = mult_assoc [of "z1::int" "z2" "z3", standard]
-lemmas zadd_zmult_distrib = left_distrib [of "z1::int" "z2" "w", standard]
-lemmas zadd_zmult_distrib2 = right_distrib [of "w::int" "z1" "z2", standard]
-lemmas zdiff_zmult_distrib = left_diff_distrib [of "z1::int" "z2" "w", standard]
-lemmas zdiff_zmult_distrib2 = right_diff_distrib [of "w::int" "z1" "z2", standard]
-
-lemmas int_distrib =
- zadd_zmult_distrib zadd_zmult_distrib2
- zdiff_zmult_distrib zdiff_zmult_distrib2
-
-lemmas zmult_1 = mult_1_left [of "z::int", standard]
-lemmas zmult_1_right = mult_1_right [of "z::int", standard]
-
-lemmas zle_refl = order_refl [of "w::int", standard]
-lemmas zle_trans = order_trans [where 'a=int and x="i" and y="j" and z="k", standard]
-lemmas zle_anti_sym = order_antisym [of "z::int" "w", standard]
-lemmas zle_linear = linorder_linear [of "z::int" "w", standard]
-lemmas zless_linear = linorder_less_linear [where 'a = int]
-
-lemmas zadd_left_mono = add_left_mono [of "i::int" "j" "k", standard]
-lemmas zadd_strict_right_mono = add_strict_right_mono [of "i::int" "j" "k", standard]
-lemmas zadd_zless_mono = add_less_le_mono [of "w'::int" "w" "z'" "z", standard]
-
-lemmas int_0_less_1 = zero_less_one [where 'a=int]
-lemmas int_0_neq_1 = zero_neq_one [where 'a=int]
-
-lemmas inj_int = inj_of_nat [where 'a=int]
-lemmas int_int_eq = of_nat_eq_iff [where 'a=int]
-lemmas zadd_int = of_nat_add [where 'a=int, symmetric]
-lemmas int_mult = of_nat_mult [where 'a=int]
-lemmas zmult_int = of_nat_mult [where 'a=int, symmetric]
-lemmas int_eq_0_conv = of_nat_eq_0_iff [where 'a=int and m="n", standard]
-lemmas zless_int = of_nat_less_iff [where 'a=int]
-lemmas int_less_0_conv = of_nat_less_0_iff [where 'a=int and m="k", standard]
-lemmas zero_less_int_conv = of_nat_0_less_iff [where 'a=int]
-lemmas zle_int = of_nat_le_iff [where 'a=int]
-lemmas zero_zle_int = of_nat_0_le_iff [where 'a=int]
-lemmas int_le_0_conv = of_nat_le_0_iff [where 'a=int and m="n", standard]
-lemmas int_0 = of_nat_0 [where 'a=int]
-lemmas int_1 = of_nat_1 [where 'a=int]
-lemmas int_Suc = of_nat_Suc [where 'a=int]
-lemmas abs_int_eq = abs_of_nat [where 'a=int and n="m", standard]
-lemmas of_int_int_eq = of_int_of_nat_eq [where 'a=int]
-lemmas zdiff_int = of_nat_diff [where 'a=int, symmetric]
-lemmas zless_le = less_int_def
-lemmas int_eq_of_nat = TrueI
-
-abbreviation
- int :: "nat \<Rightarrow> int"
-where
- "int \<equiv> of_nat"
-
-end
--- a/src/HOL/IntDiv.thy Tue Jan 15 16:19:21 2008 +0100
+++ b/src/HOL/IntDiv.thy Tue Jan 15 16:19:23 2008 +0100
@@ -8,7 +8,7 @@
header{*The Division Operators div and mod; the Divides Relation dvd*}
theory IntDiv
-imports IntArith Divides FunDef
+imports Int Divides FunDef
begin
constdefs
--- a/src/HOL/IsaMakefile Tue Jan 15 16:19:21 2008 +0100
+++ b/src/HOL/IsaMakefile Tue Jan 15 16:19:23 2008 +0100
@@ -95,9 +95,9 @@
Accessible_Part.thy Arith_Tools.thy Code_Setup.thy Datatype.thy \
Dense_Linear_Order.thy Divides.thy Equiv_Relations.thy Extraction.thy \
Finite_Set.thy Fun.thy FunDef.thy HOL.thy \
- Hilbert_Choice.thy Inductive.thy IntArith.thy IntDef.thy IntDiv.thy \
+ Hilbert_Choice.thy Inductive.thy Int.thy IntDiv.thy \
Lattices.thy List.thy Main.thy Map.thy Nat.thy NatBin.thy \
- Numeral.thy OrderedGroup.thy Orderings.thy Power.thy PreList.thy \
+ OrderedGroup.thy Orderings.thy Power.thy PreList.thy \
Predicate.thy Product_Type.thy ROOT.ML Recdef.thy \
Record.thy Refute.thy Relation.thy Relation_Power.thy \
Ring_and_Field.thy SAT.thy Set.thy SetInterval.thy Sum_Type.thy \
--- a/src/HOL/Library/Code_Integer.thy Tue Jan 15 16:19:21 2008 +0100
+++ b/src/HOL/Library/Code_Integer.thy Tue Jan 15 16:19:23 2008 +0100
@@ -6,7 +6,7 @@
header {* Pretty integer literals for code generation *}
theory Code_Integer
-imports IntArith Code_Index
+imports Int
begin
text {*
@@ -26,13 +26,13 @@
setup {*
fold (fn target => CodeTarget.add_pretty_numeral target true
@{const_name number_int_inst.number_of_int}
- @{const_name Numeral.B0} @{const_name Numeral.B1}
- @{const_name Numeral.Pls} @{const_name Numeral.Min}
- @{const_name Numeral.Bit}
+ @{const_name Int.B0} @{const_name Int.B1}
+ @{const_name Int.Pls} @{const_name Int.Min}
+ @{const_name Int.Bit}
) ["SML", "OCaml", "Haskell"]
*}
-code_const "Numeral.Pls" and "Numeral.Min" and "Numeral.Bit"
+code_const "Int.Pls" and "Int.Min" and "Int.Bit"
(SML "raise/ Fail/ \"Pls\""
and "raise/ Fail/ \"Min\""
and "!((_);/ (_);/ raise/ Fail/ \"Bit\")")
@@ -43,12 +43,12 @@
and "error/ \"Min\""
and "error/ \"Bit\"")
-code_const Numeral.pred
+code_const Int.pred
(SML "IntInf.- ((_), 1)")
(OCaml "Big'_int.pred'_big'_int")
(Haskell "!(_/ -/ 1)")
-code_const Numeral.succ
+code_const Int.succ
(SML "IntInf.+ ((_), 1)")
(OCaml "Big'_int.succ'_big'_int")
(Haskell "!(_/ +/ 1)")
@@ -88,11 +88,6 @@
(OCaml "Big'_int.lt'_big'_int")
(Haskell infix 4 "<")
-(*code_const index_of_int and int_of_index
- (SML "IntInf.toInt" and "IntInf.fromInt")
- (OCaml "Big'_int.int'_of'_big'_int" and "Big'_int.big'_int'_of'_int")
- (Haskell "_" and "_") FIXME perhaps recover this if neccessary *)
-
code_reserved SML IntInf
code_reserved OCaml Big_int
--- a/src/HOL/Library/Efficient_Nat.thy Tue Jan 15 16:19:21 2008 +0100
+++ b/src/HOL/Library/Efficient_Nat.thy Tue Jan 15 16:19:23 2008 +0100
@@ -6,7 +6,7 @@
header {* Implementation of natural numbers by integers *}
theory Efficient_Nat
-imports Main Code_Integer
+imports Main Code_Integer Code_Index
begin
text {*
@@ -55,7 +55,7 @@
lemma nat_of_int_of_number_of_aux:
fixes k
- assumes "Numeral.Pls \<le> k \<equiv> True"
+ assumes "Int.Pls \<le> k \<equiv> True"
shows "k \<ge> 0"
using assms unfolding Pls_def by simp
@@ -259,7 +259,7 @@
(HOL_basic_ss addsimps (@{thms less_numeral_code} @ @{thms less_eq_numeral_code}));
fun mk_rew (t, ty) =
if ty = HOLogic.natT andalso 0 <= HOLogic.dest_numeral t then
- Thm.capply @{cterm "(op \<le>) Numeral.Pls"} (Thm.cterm_of thy t)
+ Thm.capply @{cterm "(op \<le>) Int.Pls"} (Thm.cterm_of thy t)
|> simplify_less
|> (fn thm => @{thm nat_of_int_of_number_of_aux} OF [thm])
|> (fn thm => @{thm nat_of_int_of_number_of} OF [thm])
@@ -415,16 +415,19 @@
subsection {* Module names *}
code_modulename SML
+ Int Integer
Nat Integer
Divides Integer
Efficient_Nat Integer
code_modulename OCaml
+ Int Integer
Nat Integer
Divides Integer
Efficient_Nat Integer
code_modulename Haskell
+ Int Integer
Nat Integer
Divides Integer
Efficient_Nat Integer
--- a/src/HOL/Library/Eval.thy Tue Jan 15 16:19:21 2008 +0100
+++ b/src/HOL/Library/Eval.thy Tue Jan 15 16:19:23 2008 +0100
@@ -295,21 +295,21 @@
abbreviation (in pure_term_syntax) (input)
intT :: "typ"
where
- "intT \<equiv> Type (STR ''IntDef.int'') []"
+ "intT \<equiv> Type (STR ''Int.int'') []"
abbreviation (in pure_term_syntax) (input)
bitT :: "typ"
where
- "bitT \<equiv> Type (STR ''Numeral.bit'') []"
+ "bitT \<equiv> Type (STR ''Int.bit'') []"
function (in pure_term_syntax)
mk_int :: "int \<Rightarrow> term"
where
- "mk_int k = (if k = 0 then STR ''Numeral.Pls'' \<Colon>\<subseteq> intT
- else if k = -1 then STR ''Numeral.Min'' \<Colon>\<subseteq> intT
+ "mk_int k = (if k = 0 then STR ''Int.Pls'' \<Colon>\<subseteq> intT
+ else if k = -1 then STR ''Int.Min'' \<Colon>\<subseteq> intT
else let (l, m) = divAlg (k, 2)
- in STR ''Numeral.Bit'' \<Colon>\<subseteq> intT \<rightarrow> bitT \<rightarrow> intT \<bullet> mk_int l \<bullet>
- (if m = 0 then STR ''Numeral.bit.B0'' \<Colon>\<subseteq> bitT else STR ''Numeral.bit.B1'' \<Colon>\<subseteq> bitT))"
+ in STR ''Int.Bit'' \<Colon>\<subseteq> intT \<rightarrow> bitT \<rightarrow> intT \<bullet> mk_int l \<bullet>
+ (if m = 0 then STR ''Int.bit.B0'' \<Colon>\<subseteq> bitT else STR ''Int.bit.B1'' \<Colon>\<subseteq> bitT))"
by pat_completeness auto
termination (in pure_term_syntax)
by (relation "measure (nat o abs)") (auto simp add: divAlg_mod_div)
@@ -317,7 +317,7 @@
declare pure_term_syntax.mk_int.simps [code func]
definition (in pure_term_syntax)
- "term_of_int_aux k = STR ''Numeral.number_class.number_of'' \<Colon>\<subseteq> intT \<rightarrow> intT \<bullet> mk_int k"
+ "term_of_int_aux k = STR ''Int.number_class.number_of'' \<Colon>\<subseteq> intT \<rightarrow> intT \<bullet> mk_int k"
declare pure_term_syntax.term_of_int_aux_def [code func]
--- a/src/HOL/Library/Word.thy Tue Jan 15 16:19:21 2008 +0100
+++ b/src/HOL/Library/Word.thy Tue Jan 15 16:19:23 2008 +0100
@@ -2257,7 +2257,7 @@
lemmas [simp] = length_nat_non0
-lemma "nat_to_bv (number_of Numeral.Pls) = []"
+lemma "nat_to_bv (number_of Int.Pls) = []"
by simp
consts
@@ -2276,13 +2276,13 @@
by simp
lemma fast_bv_to_nat_def:
- "bv_to_nat bs == number_of (fast_bv_to_nat_helper bs Numeral.Pls)"
+ "bv_to_nat bs == number_of (fast_bv_to_nat_helper bs Int.Pls)"
proof (simp add: bv_to_nat_def)
have "\<forall> bin. \<not> (neg (number_of bin :: int)) \<longrightarrow> (foldl (%bn b. 2 * bn + bitval b) (number_of bin) bs) = number_of (fast_bv_to_nat_helper bs bin)"
apply (induct bs,simp)
apply (case_tac a,simp_all)
done
- thus "foldl (\<lambda>bn b. 2 * bn + bitval b) 0 bs \<equiv> number_of (fast_bv_to_nat_helper bs Numeral.Pls)"
+ thus "foldl (\<lambda>bn b. 2 * bn + bitval b) 0 bs \<equiv> number_of (fast_bv_to_nat_helper bs Int.Pls)"
by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric])
qed
@@ -2299,9 +2299,9 @@
fun is_const_bit (Const("Word.bit.Zero",_)) = true
| is_const_bit (Const("Word.bit.One",_)) = true
| is_const_bit _ = false
- fun num_is_usable (Const("Numeral.Pls",_)) = true
- | num_is_usable (Const("Numeral.Min",_)) = false
- | num_is_usable (Const("Numeral.Bit",_) $ w $ b) =
+ fun num_is_usable (Const(@{const_name Int.Pls},_)) = true
+ | num_is_usable (Const(@{const_name Int.Min},_)) = false
+ | num_is_usable (Const(@{const_name Int.Bit},_) $ w $ b) =
num_is_usable w andalso is_const_bool b
| num_is_usable _ = false
fun vec_is_usable (Const("List.list.Nil",_)) = true
@@ -2310,9 +2310,9 @@
| vec_is_usable _ = false
(*lcp** val fast1_th = PureThy.get_thm thy "Word.fast_nat_to_bv_def"*)
val fast2_th = @{thm "Word.fast_bv_to_nat_def"};
- (*lcp** fun f sg thms (Const("Word.nat_to_bv",_) $ (Const(@{const_name Numeral.number_of},_) $ t)) =
+ (*lcp** fun f sg thms (Const("Word.nat_to_bv",_) $ (Const(@{const_name Int.number_of},_) $ t)) =
if num_is_usable t
- then SOME (Drule.cterm_instantiate [(cterm_of sg (Var(("w",0),Type("IntDef.int",[]))),cterm_of sg t)] fast1_th)
+ then SOME (Drule.cterm_instantiate [(cterm_of sg (Var (("w", 0), @{typ int})), cterm_of sg t)] fast1_th)
else NONE
| f _ _ _ = NONE *)
fun g sg thms (Const("Word.bv_to_nat",_) $ (t as (Const("List.list.Cons",_) $ _ $ _))) =
--- a/src/HOL/NatBin.thy Tue Jan 15 16:19:21 2008 +0100
+++ b/src/HOL/NatBin.thy Tue Jan 15 16:19:23 2008 +0100
@@ -120,14 +120,14 @@
lemma Suc_nat_number_of_add:
"Suc (number_of v + n) =
- (if neg (number_of v :: int) then 1+n else number_of (Numeral.succ v) + n)"
+ (if neg (number_of v :: int) then 1+n else number_of (Int.succ v) + n)"
by (simp del: nat_number_of
add: nat_number_of_def neg_nat
Suc_nat_eq_nat_zadd1 number_of_succ)
lemma Suc_nat_number_of [simp]:
"Suc (number_of v) =
- (if neg (number_of v :: int) then 1 else number_of (Numeral.succ v))"
+ (if neg (number_of v :: int) then 1 else number_of (Int.succ v))"
apply (cut_tac n = 0 in Suc_nat_number_of_add)
apply (simp cong del: if_weak_cong)
done
@@ -470,7 +470,7 @@
lemma eq_number_of_Suc [simp]:
"(number_of v = Suc n) =
- (let pv = number_of (Numeral.pred v) in
+ (let pv = number_of (Int.pred v) in
if neg pv then False else nat pv = n)"
apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less
number_of_pred nat_number_of_def
@@ -481,13 +481,13 @@
lemma Suc_eq_number_of [simp]:
"(Suc n = number_of v) =
- (let pv = number_of (Numeral.pred v) in
+ (let pv = number_of (Int.pred v) in
if neg pv then False else nat pv = n)"
by (rule trans [OF eq_sym_conv eq_number_of_Suc])
lemma less_number_of_Suc [simp]:
"(number_of v < Suc n) =
- (let pv = number_of (Numeral.pred v) in
+ (let pv = number_of (Int.pred v) in
if neg pv then True else nat pv < n)"
apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less
number_of_pred nat_number_of_def
@@ -498,7 +498,7 @@
lemma less_Suc_number_of [simp]:
"(Suc n < number_of v) =
- (let pv = number_of (Numeral.pred v) in
+ (let pv = number_of (Int.pred v) in
if neg pv then False else n < nat pv)"
apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less
number_of_pred nat_number_of_def
@@ -509,13 +509,13 @@
lemma le_number_of_Suc [simp]:
"(number_of v <= Suc n) =
- (let pv = number_of (Numeral.pred v) in
+ (let pv = number_of (Int.pred v) in
if neg pv then True else nat pv <= n)"
by (simp add: Let_def less_Suc_number_of linorder_not_less [symmetric])
lemma le_Suc_number_of [simp]:
"(Suc n <= number_of v) =
- (let pv = number_of (Numeral.pred v) in
+ (let pv = number_of (Int.pred v) in
if neg pv then False else n <= nat pv)"
by (simp add: Let_def less_number_of_Suc linorder_not_less [symmetric])
@@ -550,15 +550,15 @@
done
lemma eq_number_of_BIT_Min:
- "((number_of (v BIT x) ::int) = number_of Numeral.Min) =
- (x=bit.B1 & (((number_of v) ::int) = number_of Numeral.Min))"
+ "((number_of (v BIT x) ::int) = number_of Int.Min) =
+ (x=bit.B1 & (((number_of v) ::int) = number_of Int.Min))"
apply (simp only: simp_thms add: number_of_BIT number_of_Min eq_commute
split add: bit.split cong: imp_cong)
apply (rule_tac x = "number_of v" in spec, auto)
apply (drule_tac f = "%x. x mod 2" in arg_cong, auto)
done
-lemma eq_number_of_Pls_Min: "(Numeral0 ::int) ~= number_of Numeral.Min"
+lemma eq_number_of_Pls_Min: "(Numeral0 ::int) ~= number_of Int.Min"
by auto
@@ -567,7 +567,7 @@
lemma max_number_of_Suc [simp]:
"max (Suc n) (number_of v) =
- (let pv = number_of (Numeral.pred v) in
+ (let pv = number_of (Int.pred v) in
if neg pv then Suc n else Suc(max n (nat pv)))"
apply (simp only: Let_def neg_eq_less_0 number_of_pred nat_number_of_def
split add: split_if nat.split)
@@ -577,7 +577,7 @@
lemma max_Suc_number_of [simp]:
"max (number_of v) (Suc n) =
- (let pv = number_of (Numeral.pred v) in
+ (let pv = number_of (Int.pred v) in
if neg pv then Suc n else Suc(max (nat pv) n))"
apply (simp only: Let_def neg_eq_less_0 number_of_pred nat_number_of_def
split add: split_if nat.split)
@@ -587,7 +587,7 @@
lemma min_number_of_Suc [simp]:
"min (Suc n) (number_of v) =
- (let pv = number_of (Numeral.pred v) in
+ (let pv = number_of (Int.pred v) in
if neg pv then 0 else Suc(min n (nat pv)))"
apply (simp only: Let_def neg_eq_less_0 number_of_pred nat_number_of_def
split add: split_if nat.split)
@@ -597,7 +597,7 @@
lemma min_Suc_number_of [simp]:
"min (number_of v) (Suc n) =
- (let pv = number_of (Numeral.pred v) in
+ (let pv = number_of (Int.pred v) in
if neg pv then 0 else Suc(min (nat pv) n))"
apply (simp only: Let_def neg_eq_less_0 number_of_pred nat_number_of_def
split add: split_if nat.split)
@@ -681,7 +681,7 @@
lemma nat_number_of_Pls: "Numeral0 = (0::nat)"
by (simp add: number_of_Pls nat_number_of_def)
-lemma nat_number_of_Min: "number_of Numeral.Min = (0::nat)"
+lemma nat_number_of_Min: "number_of Int.Min = (0::nat)"
apply (simp only: number_of_Min nat_number_of_def nat_zminus_int)
done
--- a/src/HOL/Nominal/nominal_atoms.ML Tue Jan 15 16:19:21 2008 +0100
+++ b/src/HOL/Nominal/nominal_atoms.ML Tue Jan 15 16:19:23 2008 +0100
@@ -717,9 +717,9 @@
|> discrete_pt_inst "bool" @{thm "perm_bool"}
|> discrete_fs_inst "bool" @{thm "perm_bool"}
|> discrete_cp_inst "bool" @{thm "perm_bool"}
- |> discrete_pt_inst "IntDef.int" @{thm "perm_int_def"}
- |> discrete_fs_inst "IntDef.int" @{thm "perm_int_def"}
- |> discrete_cp_inst "IntDef.int" @{thm "perm_int_def"}
+ |> discrete_pt_inst @{type_name "Int.int"} @{thm "perm_int_def"}
+ |> discrete_fs_inst @{type_name "Int.int"} @{thm "perm_int_def"}
+ |> discrete_cp_inst @{type_name "Int.int"} @{thm "perm_int_def"}
|> discrete_pt_inst "List.char" @{thm "perm_char_def"}
|> discrete_fs_inst "List.char" @{thm "perm_char_def"}
|> discrete_cp_inst "List.char" @{thm "perm_char_def"}
--- a/src/HOL/Numeral.thy Tue Jan 15 16:19:21 2008 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,688 +0,0 @@
-(* Title: HOL/Numeral.thy
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1994 University of Cambridge
-*)
-
-header {* Arithmetic on Binary Integers *}
-
-theory Numeral
-imports Datatype IntDef
-uses
- ("Tools/numeral.ML")
- ("Tools/numeral_syntax.ML")
-begin
-
-subsection {* Binary representation *}
-
-text {*
- This formalization defines binary arithmetic in terms of the integers
- rather than using a datatype. This avoids multiple representations (leading
- zeroes, etc.) See @{text "ZF/Tools/twos-compl.ML"}, function @{text
- int_of_binary}, for the numerical interpretation.
-
- The representation expects that @{text "(m mod 2)"} is 0 or 1,
- even if m is negative;
- For instance, @{text "-5 div 2 = -3"} and @{text "-5 mod 2 = 1"}; thus
- @{text "-5 = (-3)*2 + 1"}.
-
- This two's complement binary representation derives from the paper
- "An Efficient Representation of Arithmetic for Term Rewriting" by
- Dave Cohen and Phil Watson, Rewriting Techniques and Applications,
- Springer LNCS 488 (240-251), 1991.
-*}
-
-datatype bit = B0 | B1
-
-text{*
- Type @{typ bit} avoids the use of type @{typ bool}, which would make
- all of the rewrite rules higher-order.
-*}
-
-definition
- Pls :: int where
- [code func del]: "Pls = 0"
-
-definition
- Min :: int where
- [code func del]: "Min = - 1"
-
-definition
- Bit :: "int \<Rightarrow> bit \<Rightarrow> int" (infixl "BIT" 90) where
- [code func del]: "k BIT b = (case b of B0 \<Rightarrow> 0 | B1 \<Rightarrow> 1) + k + k"
-
-class number = type + -- {* for numeric types: nat, int, real, \dots *}
- fixes number_of :: "int \<Rightarrow> 'a"
-
-use "Tools/numeral.ML"
-
-syntax
- "_Numeral" :: "num_const \<Rightarrow> 'a" ("_")
-
-use "Tools/numeral_syntax.ML"
-setup NumeralSyntax.setup
-
-abbreviation
- "Numeral0 \<equiv> number_of Pls"
-
-abbreviation
- "Numeral1 \<equiv> number_of (Pls BIT B1)"
-
-lemma Let_number_of [simp]: "Let (number_of v) f = f (number_of v)"
- -- {* Unfold all @{text let}s involving constants *}
- unfolding Let_def ..
-
-definition
- succ :: "int \<Rightarrow> int" where
- [code func del]: "succ k = k + 1"
-
-definition
- pred :: "int \<Rightarrow> int" where
- [code func del]: "pred k = k - 1"
-
-lemmas
- max_number_of [simp] = max_def
- [of "number_of u" "number_of v", standard, simp]
-and
- min_number_of [simp] = min_def
- [of "number_of u" "number_of v", standard, simp]
- -- {* unfolding @{text minx} and @{text max} on numerals *}
-
-lemmas numeral_simps =
- succ_def pred_def Pls_def Min_def Bit_def
-
-text {* Removal of leading zeroes *}
-
-lemma Pls_0_eq [simp, code post]:
- "Pls BIT B0 = Pls"
- unfolding numeral_simps by simp
-
-lemma Min_1_eq [simp, code post]:
- "Min BIT B1 = Min"
- unfolding numeral_simps by simp
-
-
-subsection {* The Functions @{term succ}, @{term pred} and @{term uminus} *}
-
-lemma succ_Pls [simp]:
- "succ Pls = Pls BIT B1"
- unfolding numeral_simps by simp
-
-lemma succ_Min [simp]:
- "succ Min = Pls"
- unfolding numeral_simps by simp
-
-lemma succ_1 [simp]:
- "succ (k BIT B1) = succ k BIT B0"
- unfolding numeral_simps by simp
-
-lemma succ_0 [simp]:
- "succ (k BIT B0) = k BIT B1"
- unfolding numeral_simps by simp
-
-lemma pred_Pls [simp]:
- "pred Pls = Min"
- unfolding numeral_simps by simp
-
-lemma pred_Min [simp]:
- "pred Min = Min BIT B0"
- unfolding numeral_simps by simp
-
-lemma pred_1 [simp]:
- "pred (k BIT B1) = k BIT B0"
- unfolding numeral_simps by simp
-
-lemma pred_0 [simp]:
- "pred (k BIT B0) = pred k BIT B1"
- unfolding numeral_simps by simp
-
-lemma minus_Pls [simp]:
- "- Pls = Pls"
- unfolding numeral_simps by simp
-
-lemma minus_Min [simp]:
- "- Min = Pls BIT B1"
- unfolding numeral_simps by simp
-
-lemma minus_1 [simp]:
- "- (k BIT B1) = pred (- k) BIT B1"
- unfolding numeral_simps by simp
-
-lemma minus_0 [simp]:
- "- (k BIT B0) = (- k) BIT B0"
- unfolding numeral_simps by simp
-
-
-subsection {*
- Binary Addition and Multiplication: @{term "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"}
- and @{term "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int"}
-*}
-
-lemma add_Pls [simp]:
- "Pls + k = k"
- unfolding numeral_simps by simp
-
-lemma add_Min [simp]:
- "Min + k = pred k"
- unfolding numeral_simps by simp
-
-lemma add_BIT_11 [simp]:
- "(k BIT B1) + (l BIT B1) = (k + succ l) BIT B0"
- unfolding numeral_simps by simp
-
-lemma add_BIT_10 [simp]:
- "(k BIT B1) + (l BIT B0) = (k + l) BIT B1"
- unfolding numeral_simps by simp
-
-lemma add_BIT_0 [simp]:
- "(k BIT B0) + (l BIT b) = (k + l) BIT b"
- unfolding numeral_simps by simp
-
-lemma add_Pls_right [simp]:
- "k + Pls = k"
- unfolding numeral_simps by simp
-
-lemma add_Min_right [simp]:
- "k + Min = pred k"
- unfolding numeral_simps by simp
-
-lemma mult_Pls [simp]:
- "Pls * w = Pls"
- unfolding numeral_simps by simp
-
-lemma mult_Min [simp]:
- "Min * k = - k"
- unfolding numeral_simps by simp
-
-lemma mult_num1 [simp]:
- "(k BIT B1) * l = ((k * l) BIT B0) + l"
- unfolding numeral_simps int_distrib by simp
-
-lemma mult_num0 [simp]:
- "(k BIT B0) * l = (k * l) BIT B0"
- unfolding numeral_simps int_distrib by simp
-
-
-subsection {* Converting Numerals to Rings: @{term number_of} *}
-
-class number_ring = number + comm_ring_1 +
- assumes number_of_eq: "number_of k = of_int k"
-
-text {* self-embedding of the integers *}
-
-instantiation int :: number_ring
-begin
-
-definition
- int_number_of_def [code func del]: "number_of w = (of_int w \<Colon> int)"
-
-instance
- by intro_classes (simp only: int_number_of_def)
-
-end
-
-lemma number_of_is_id:
- "number_of (k::int) = k"
- unfolding int_number_of_def by simp
-
-lemma number_of_succ:
- "number_of (succ k) = (1 + number_of k ::'a::number_ring)"
- unfolding number_of_eq numeral_simps by simp
-
-lemma number_of_pred:
- "number_of (pred w) = (- 1 + number_of w ::'a::number_ring)"
- unfolding number_of_eq numeral_simps by simp
-
-lemma number_of_minus:
- "number_of (uminus w) = (- (number_of w)::'a::number_ring)"
- unfolding number_of_eq numeral_simps by simp
-
-lemma number_of_add:
- "number_of (v + w) = (number_of v + number_of w::'a::number_ring)"
- unfolding number_of_eq numeral_simps by simp
-
-lemma number_of_mult:
- "number_of (v * w) = (number_of v * number_of w::'a::number_ring)"
- unfolding number_of_eq numeral_simps by simp
-
-text {*
- The correctness of shifting.
- But it doesn't seem to give a measurable speed-up.
-*}
-
-lemma double_number_of_BIT:
- "(1 + 1) * number_of w = (number_of (w BIT B0) ::'a::number_ring)"
- unfolding number_of_eq numeral_simps left_distrib by simp
-
-text {*
- Converting numerals 0 and 1 to their abstract versions.
-*}
-
-lemma numeral_0_eq_0 [simp]:
- "Numeral0 = (0::'a::number_ring)"
- unfolding number_of_eq numeral_simps by simp
-
-lemma numeral_1_eq_1 [simp]:
- "Numeral1 = (1::'a::number_ring)"
- unfolding number_of_eq numeral_simps by simp
-
-text {*
- Special-case simplification for small constants.
-*}
-
-text{*
- Unary minus for the abstract constant 1. Cannot be inserted
- as a simprule until later: it is @{text number_of_Min} re-oriented!
-*}
-
-lemma numeral_m1_eq_minus_1:
- "(-1::'a::number_ring) = - 1"
- unfolding number_of_eq numeral_simps by simp
-
-lemma mult_minus1 [simp]:
- "-1 * z = -(z::'a::number_ring)"
- unfolding number_of_eq numeral_simps by simp
-
-lemma mult_minus1_right [simp]:
- "z * -1 = -(z::'a::number_ring)"
- unfolding number_of_eq numeral_simps by simp
-
-(*Negation of a coefficient*)
-lemma minus_number_of_mult [simp]:
- "- (number_of w) * z = number_of (uminus w) * (z::'a::number_ring)"
- unfolding number_of_eq by simp
-
-text {* Subtraction *}
-
-lemma diff_number_of_eq:
- "number_of v - number_of w =
- (number_of (v + uminus w)::'a::number_ring)"
- unfolding number_of_eq by simp
-
-lemma number_of_Pls:
- "number_of Pls = (0::'a::number_ring)"
- unfolding number_of_eq numeral_simps by simp
-
-lemma number_of_Min:
- "number_of Min = (- 1::'a::number_ring)"
- unfolding number_of_eq numeral_simps by simp
-
-lemma number_of_BIT:
- "number_of(w BIT x) = (case x of B0 => 0 | B1 => (1::'a::number_ring))
- + (number_of w) + (number_of w)"
- unfolding number_of_eq numeral_simps by (simp split: bit.split)
-
-
-subsection {* Equality of Binary Numbers *}
-
-text {* First version by Norbert Voelker *}
-
-lemma eq_number_of_eq:
- "((number_of x::'a::number_ring) = number_of y) =
- iszero (number_of (x + uminus y) :: 'a)"
- unfolding iszero_def number_of_add number_of_minus
- by (simp add: compare_rls)
-
-lemma iszero_number_of_Pls:
- "iszero ((number_of Pls)::'a::number_ring)"
- unfolding iszero_def numeral_0_eq_0 ..
-
-lemma nonzero_number_of_Min:
- "~ iszero ((number_of Min)::'a::number_ring)"
- unfolding iszero_def numeral_m1_eq_minus_1 by simp
-
-
-subsection {* Comparisons, for Ordered Rings *}
-
-lemmas double_eq_0_iff = double_zero
-
-lemma le_imp_0_less:
- assumes le: "0 \<le> z"
- shows "(0::int) < 1 + z"
-proof -
- have "0 \<le> z" by fact
- also have "... < z + 1" by (rule less_add_one)
- also have "... = 1 + z" by (simp add: add_ac)
- finally show "0 < 1 + z" .
-qed
-
-lemma odd_nonzero:
- "1 + z + z \<noteq> (0::int)";
-proof (cases z rule: int_cases)
- case (nonneg n)
- have le: "0 \<le> z+z" by (simp add: nonneg add_increasing)
- thus ?thesis using le_imp_0_less [OF le]
- by (auto simp add: add_assoc)
-next
- case (neg n)
- show ?thesis
- proof
- assume eq: "1 + z + z = 0"
- have "0 < 1 + (int n + int n)"
- by (simp add: le_imp_0_less add_increasing)
- also have "... = - (1 + z + z)"
- by (simp add: neg add_assoc [symmetric])
- also have "... = 0" by (simp add: eq)
- finally have "0<0" ..
- thus False by blast
- qed
-qed
-
-text {* The premise involving @{term Ints} prevents @{term "a = 1/2"}. *}
-
-lemma Ints_double_eq_0_iff:
- assumes in_Ints: "a \<in> Ints"
- shows "(a + a = 0) = (a = (0::'a::ring_char_0))"
-proof -
- from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
- then obtain z where a: "a = of_int z" ..
- show ?thesis
- proof
- assume "a = 0"
- thus "a + a = 0" by simp
- next
- assume eq: "a + a = 0"
- hence "of_int (z + z) = (of_int 0 :: 'a)" by (simp add: a)
- hence "z + z = 0" by (simp only: of_int_eq_iff)
- hence "z = 0" by (simp only: double_eq_0_iff)
- thus "a = 0" by (simp add: a)
- qed
-qed
-
-lemma Ints_odd_nonzero:
- assumes in_Ints: "a \<in> Ints"
- shows "1 + a + a \<noteq> (0::'a::ring_char_0)"
-proof -
- from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
- then obtain z where a: "a = of_int z" ..
- show ?thesis
- proof
- assume eq: "1 + a + a = 0"
- hence "of_int (1 + z + z) = (of_int 0 :: 'a)" by (simp add: a)
- hence "1 + z + z = 0" by (simp only: of_int_eq_iff)
- with odd_nonzero show False by blast
- qed
-qed
-
-lemma Ints_number_of:
- "(number_of w :: 'a::number_ring) \<in> Ints"
- unfolding number_of_eq Ints_def by simp
-
-lemma iszero_number_of_BIT:
- "iszero (number_of (w BIT x)::'a) =
- (x = B0 \<and> iszero (number_of w::'a::{ring_char_0,number_ring}))"
- by (simp add: iszero_def number_of_eq numeral_simps Ints_double_eq_0_iff
- Ints_odd_nonzero Ints_def split: bit.split)
-
-lemma iszero_number_of_0:
- "iszero (number_of (w BIT B0) :: 'a::{ring_char_0,number_ring}) =
- iszero (number_of w :: 'a)"
- by (simp only: iszero_number_of_BIT simp_thms)
-
-lemma iszero_number_of_1:
- "~ iszero (number_of (w BIT B1)::'a::{ring_char_0,number_ring})"
- by (simp add: iszero_number_of_BIT)
-
-
-subsection {* The Less-Than Relation *}
-
-lemma less_number_of_eq_neg:
- "((number_of x::'a::{ordered_idom,number_ring}) < number_of y)
- = neg (number_of (x + uminus y) :: 'a)"
-apply (subst less_iff_diff_less_0)
-apply (simp add: neg_def diff_minus number_of_add number_of_minus)
-done
-
-text {*
- If @{term Numeral0} is rewritten to 0 then this rule can't be applied:
- @{term Numeral0} IS @{term "number_of Pls"}
-*}
-
-lemma not_neg_number_of_Pls:
- "~ neg (number_of Pls ::'a::{ordered_idom,number_ring})"
- by (simp add: neg_def numeral_0_eq_0)
-
-lemma neg_number_of_Min:
- "neg (number_of Min ::'a::{ordered_idom,number_ring})"
- by (simp add: neg_def zero_less_one numeral_m1_eq_minus_1)
-
-lemma double_less_0_iff:
- "(a + a < 0) = (a < (0::'a::ordered_idom))"
-proof -
- have "(a + a < 0) = ((1+1)*a < 0)" by (simp add: left_distrib)
- also have "... = (a < 0)"
- by (simp add: mult_less_0_iff zero_less_two
- order_less_not_sym [OF zero_less_two])
- finally show ?thesis .
-qed
-
-lemma odd_less_0:
- "(1 + z + z < 0) = (z < (0::int))";
-proof (cases z rule: int_cases)
- case (nonneg n)
- thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing
- le_imp_0_less [THEN order_less_imp_le])
-next
- case (neg n)
- thus ?thesis by (simp del: of_nat_Suc of_nat_add
- add: compare_rls of_nat_1 [symmetric] of_nat_add [symmetric])
-qed
-
-text {* The premise involving @{term Ints} prevents @{term "a = 1/2"}. *}
-
-lemma Ints_odd_less_0:
- assumes in_Ints: "a \<in> Ints"
- shows "(1 + a + a < 0) = (a < (0::'a::ordered_idom))";
-proof -
- from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
- then obtain z where a: "a = of_int z" ..
- hence "((1::'a) + a + a < 0) = (of_int (1 + z + z) < (of_int 0 :: 'a))"
- by (simp add: a)
- also have "... = (z < 0)" by (simp only: of_int_less_iff odd_less_0)
- also have "... = (a < 0)" by (simp add: a)
- finally show ?thesis .
-qed
-
-lemma neg_number_of_BIT:
- "neg (number_of (w BIT x)::'a) =
- neg (number_of w :: 'a::{ordered_idom,number_ring})"
- by (simp add: neg_def number_of_eq numeral_simps double_less_0_iff
- Ints_odd_less_0 Ints_def split: bit.split)
-
-
-text {* Less-Than or Equals *}
-
-text {* Reduces @{term "a\<le>b"} to @{term "~ (b<a)"} for ALL numerals. *}
-
-lemmas le_number_of_eq_not_less =
- linorder_not_less [of "number_of w" "number_of v", symmetric,
- standard]
-
-lemma le_number_of_eq:
- "((number_of x::'a::{ordered_idom,number_ring}) \<le> number_of y)
- = (~ (neg (number_of (y + uminus x) :: 'a)))"
-by (simp add: le_number_of_eq_not_less less_number_of_eq_neg)
-
-
-text {* Absolute value (@{term abs}) *}
-
-lemma abs_number_of:
- "abs(number_of x::'a::{ordered_idom,number_ring}) =
- (if number_of x < (0::'a) then -number_of x else number_of x)"
- by (simp add: abs_if)
-
-
-text {* Re-orientation of the equation nnn=x *}
-
-lemma number_of_reorient:
- "(number_of w = x) = (x = number_of w)"
- by auto
-
-
-subsection {* Simplification of arithmetic operations on integer constants. *}
-
-lemmas arith_extra_simps [standard, simp] =
- number_of_add [symmetric]
- number_of_minus [symmetric] numeral_m1_eq_minus_1 [symmetric]
- number_of_mult [symmetric]
- diff_number_of_eq abs_number_of
-
-text {*
- For making a minimal simpset, one must include these default simprules.
- Also include @{text simp_thms}.
-*}
-
-lemmas arith_simps =
- bit.distinct
- Pls_0_eq Min_1_eq
- pred_Pls pred_Min pred_1 pred_0
- succ_Pls succ_Min succ_1 succ_0
- add_Pls add_Min add_BIT_0 add_BIT_10 add_BIT_11
- minus_Pls minus_Min minus_1 minus_0
- mult_Pls mult_Min mult_num1 mult_num0
- add_Pls_right add_Min_right
- abs_zero abs_one arith_extra_simps
-
-text {* Simplification of relational operations *}
-
-lemmas rel_simps [simp] =
- eq_number_of_eq iszero_0 nonzero_number_of_Min
- iszero_number_of_0 iszero_number_of_1
- less_number_of_eq_neg
- not_neg_number_of_Pls not_neg_0 not_neg_1 not_iszero_1
- neg_number_of_Min neg_number_of_BIT
- le_number_of_eq
-(* iszero_number_of_Pls would never be used
- because its lhs simplifies to "iszero 0" *)
-
-
-subsection {* Simplification of arithmetic when nested to the right. *}
-
-lemma add_number_of_left [simp]:
- "number_of v + (number_of w + z) =
- (number_of(v + w) + z::'a::number_ring)"
- by (simp add: add_assoc [symmetric])
-
-lemma mult_number_of_left [simp]:
- "number_of v * (number_of w * z) =
- (number_of(v * w) * z::'a::number_ring)"
- by (simp add: mult_assoc [symmetric])
-
-lemma add_number_of_diff1:
- "number_of v + (number_of w - c) =
- number_of(v + w) - (c::'a::number_ring)"
- by (simp add: diff_minus add_number_of_left)
-
-lemma add_number_of_diff2 [simp]:
- "number_of v + (c - number_of w) =
- number_of (v + uminus w) + (c::'a::number_ring)"
-apply (subst diff_number_of_eq [symmetric])
-apply (simp only: compare_rls)
-done
-
-
-subsection {* Configuration of the code generator *}
-
-instance int :: eq ..
-
-code_datatype Pls Min Bit "number_of \<Colon> int \<Rightarrow> int"
-
-definition
- int_aux :: "nat \<Rightarrow> int \<Rightarrow> int" where
- "int_aux n i = int n + i"
-
-lemma [code]:
- "int_aux 0 i = i"
- "int_aux (Suc n) i = int_aux n (i + 1)" -- {* tail recursive *}
- by (simp add: int_aux_def)+
-
-lemma [code, code unfold, code inline del]:
- "int n = int_aux n 0"
- by (simp add: int_aux_def)
-
-definition
- nat_aux :: "int \<Rightarrow> nat \<Rightarrow> nat" where
- "nat_aux i n = nat i + n"
-
-lemma [code]:
- "nat_aux i n = (if i \<le> 0 then n else nat_aux (i - 1) (Suc n))" -- {* tail recursive *}
- by (auto simp add: nat_aux_def nat_eq_iff linorder_not_le order_less_imp_le
- dest: zless_imp_add1_zle)
-
-lemma [code]: "nat i = nat_aux i 0"
- by (simp add: nat_aux_def)
-
-lemma zero_is_num_zero [code func, code inline, symmetric, code post]:
- "(0\<Colon>int) = Numeral0"
- by simp
-
-lemma one_is_num_one [code func, code inline, symmetric, code post]:
- "(1\<Colon>int) = Numeral1"
- by simp
-
-code_modulename SML
- IntDef Integer
-
-code_modulename OCaml
- IntDef Integer
-
-code_modulename Haskell
- IntDef Integer
-
-code_modulename SML
- Numeral Integer
-
-code_modulename OCaml
- Numeral Integer
-
-code_modulename Haskell
- Numeral Integer
-
-types_code
- "int" ("int")
-attach (term_of) {*
-val term_of_int = HOLogic.mk_number HOLogic.intT;
-*}
-attach (test) {*
-fun gen_int i =
- let val j = one_of [~1, 1] * random_range 0 i
- in (j, fn () => term_of_int j) end;
-*}
-
-setup {*
-let
-
-fun strip_number_of (@{term "Numeral.number_of :: int => int"} $ t) = t
- | strip_number_of t = t;
-
-fun numeral_codegen thy defs gr dep module b t =
- let val i = HOLogic.dest_numeral (strip_number_of t)
- in
- SOME (fst (Codegen.invoke_tycodegen thy defs dep module false (gr, HOLogic.intT)),
- Pretty.str (string_of_int i))
- end handle TERM _ => NONE;
-
-in
-
-Codegen.add_codegen "numeral_codegen" numeral_codegen
-
-end
-*}
-
-consts_code
- "number_of :: int \<Rightarrow> int" ("(_)")
- "0 :: int" ("0")
- "1 :: int" ("1")
- "uminus :: int => int" ("~")
- "op + :: int => int => int" ("(_ +/ _)")
- "op * :: int => int => int" ("(_ */ _)")
- "op \<le> :: int => int => bool" ("(_ <=/ _)")
- "op < :: int => int => bool" ("(_ </ _)")
-
-quickcheck_params [default_type = int]
-
-(*setup continues in theory Presburger*)
-
-hide (open) const Pls Min B0 B1 succ pred
-
-end
--- a/src/HOL/Presburger.thy Tue Jan 15 16:19:21 2008 +0100
+++ b/src/HOL/Presburger.thy Tue Jan 15 16:19:23 2008 +0100
@@ -496,53 +496,53 @@
*}
lemma eq_Pls_Pls:
- "Numeral.Pls = Numeral.Pls \<longleftrightarrow> True" by presburger
+ "Int.Pls = Int.Pls \<longleftrightarrow> True" by presburger
lemma eq_Pls_Min:
- "Numeral.Pls = Numeral.Min \<longleftrightarrow> False"
- unfolding Pls_def Numeral.Min_def by presburger
+ "Int.Pls = Int.Min \<longleftrightarrow> False"
+ unfolding Pls_def Int.Min_def by presburger
lemma eq_Pls_Bit0:
- "Numeral.Pls = Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Pls = k"
+ "Int.Pls = Int.Bit k bit.B0 \<longleftrightarrow> Int.Pls = k"
unfolding Pls_def Bit_def bit.cases by presburger
lemma eq_Pls_Bit1:
- "Numeral.Pls = Numeral.Bit k bit.B1 \<longleftrightarrow> False"
+ "Int.Pls = Int.Bit k bit.B1 \<longleftrightarrow> False"
unfolding Pls_def Bit_def bit.cases by presburger
lemma eq_Min_Pls:
- "Numeral.Min = Numeral.Pls \<longleftrightarrow> False"
- unfolding Pls_def Numeral.Min_def by presburger
+ "Int.Min = Int.Pls \<longleftrightarrow> False"
+ unfolding Pls_def Int.Min_def by presburger
lemma eq_Min_Min:
- "Numeral.Min = Numeral.Min \<longleftrightarrow> True" by presburger
+ "Int.Min = Int.Min \<longleftrightarrow> True" by presburger
lemma eq_Min_Bit0:
- "Numeral.Min = Numeral.Bit k bit.B0 \<longleftrightarrow> False"
- unfolding Numeral.Min_def Bit_def bit.cases by presburger
+ "Int.Min = Int.Bit k bit.B0 \<longleftrightarrow> False"
+ unfolding Int.Min_def Bit_def bit.cases by presburger
lemma eq_Min_Bit1:
- "Numeral.Min = Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Min = k"
- unfolding Numeral.Min_def Bit_def bit.cases by presburger
+ "Int.Min = Int.Bit k bit.B1 \<longleftrightarrow> Int.Min = k"
+ unfolding Int.Min_def Bit_def bit.cases by presburger
lemma eq_Bit0_Pls:
- "Numeral.Bit k bit.B0 = Numeral.Pls \<longleftrightarrow> Numeral.Pls = k"
+ "Int.Bit k bit.B0 = Int.Pls \<longleftrightarrow> Int.Pls = k"
unfolding Pls_def Bit_def bit.cases by presburger
lemma eq_Bit1_Pls:
- "Numeral.Bit k bit.B1 = Numeral.Pls \<longleftrightarrow> False"
+ "Int.Bit k bit.B1 = Int.Pls \<longleftrightarrow> False"
unfolding Pls_def Bit_def bit.cases by presburger
lemma eq_Bit0_Min:
- "Numeral.Bit k bit.B0 = Numeral.Min \<longleftrightarrow> False"
- unfolding Numeral.Min_def Bit_def bit.cases by presburger
+ "Int.Bit k bit.B0 = Int.Min \<longleftrightarrow> False"
+ unfolding Int.Min_def Bit_def bit.cases by presburger
lemma eq_Bit1_Min:
- "(Numeral.Bit k bit.B1) = Numeral.Min \<longleftrightarrow> Numeral.Min = k"
- unfolding Numeral.Min_def Bit_def bit.cases by presburger
+ "(Int.Bit k bit.B1) = Int.Min \<longleftrightarrow> Int.Min = k"
+ unfolding Int.Min_def Bit_def bit.cases by presburger
lemma eq_Bit_Bit:
- "Numeral.Bit k1 v1 = Numeral.Bit k2 v2 \<longleftrightarrow>
+ "Int.Bit k1 v1 = Int.Bit k2 v2 \<longleftrightarrow>
v1 = v2 \<and> k1 = k2"
unfolding Bit_def
apply (cases v1)
@@ -562,53 +562,53 @@
lemma less_eq_Pls_Pls:
- "Numeral.Pls \<le> Numeral.Pls \<longleftrightarrow> True" by rule+
+ "Int.Pls \<le> Int.Pls \<longleftrightarrow> True" by rule+
lemma less_eq_Pls_Min:
- "Numeral.Pls \<le> Numeral.Min \<longleftrightarrow> False"
- unfolding Pls_def Numeral.Min_def by presburger
+ "Int.Pls \<le> Int.Min \<longleftrightarrow> False"
+ unfolding Pls_def Int.Min_def by presburger
lemma less_eq_Pls_Bit:
- "Numeral.Pls \<le> Numeral.Bit k v \<longleftrightarrow> Numeral.Pls \<le> k"
+ "Int.Pls \<le> Int.Bit k v \<longleftrightarrow> Int.Pls \<le> k"
unfolding Pls_def Bit_def by (cases v) auto
lemma less_eq_Min_Pls:
- "Numeral.Min \<le> Numeral.Pls \<longleftrightarrow> True"
- unfolding Pls_def Numeral.Min_def by presburger
+ "Int.Min \<le> Int.Pls \<longleftrightarrow> True"
+ unfolding Pls_def Int.Min_def by presburger
lemma less_eq_Min_Min:
- "Numeral.Min \<le> Numeral.Min \<longleftrightarrow> True" by rule+
+ "Int.Min \<le> Int.Min \<longleftrightarrow> True" by rule+
lemma less_eq_Min_Bit0:
- "Numeral.Min \<le> Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Min < k"
- unfolding Numeral.Min_def Bit_def by auto
+ "Int.Min \<le> Int.Bit k bit.B0 \<longleftrightarrow> Int.Min < k"
+ unfolding Int.Min_def Bit_def by auto
lemma less_eq_Min_Bit1:
- "Numeral.Min \<le> Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Min \<le> k"
- unfolding Numeral.Min_def Bit_def by auto
+ "Int.Min \<le> Int.Bit k bit.B1 \<longleftrightarrow> Int.Min \<le> k"
+ unfolding Int.Min_def Bit_def by auto
lemma less_eq_Bit0_Pls:
- "Numeral.Bit k bit.B0 \<le> Numeral.Pls \<longleftrightarrow> k \<le> Numeral.Pls"
+ "Int.Bit k bit.B0 \<le> Int.Pls \<longleftrightarrow> k \<le> Int.Pls"
unfolding Pls_def Bit_def by simp
lemma less_eq_Bit1_Pls:
- "Numeral.Bit k bit.B1 \<le> Numeral.Pls \<longleftrightarrow> k < Numeral.Pls"
+ "Int.Bit k bit.B1 \<le> Int.Pls \<longleftrightarrow> k < Int.Pls"
unfolding Pls_def Bit_def by auto
lemma less_eq_Bit_Min:
- "Numeral.Bit k v \<le> Numeral.Min \<longleftrightarrow> k \<le> Numeral.Min"
- unfolding Numeral.Min_def Bit_def by (cases v) auto
+ "Int.Bit k v \<le> Int.Min \<longleftrightarrow> k \<le> Int.Min"
+ unfolding Int.Min_def Bit_def by (cases v) auto
lemma less_eq_Bit0_Bit:
- "Numeral.Bit k1 bit.B0 \<le> Numeral.Bit k2 v \<longleftrightarrow> k1 \<le> k2"
+ "Int.Bit k1 bit.B0 \<le> Int.Bit k2 v \<longleftrightarrow> k1 \<le> k2"
unfolding Bit_def bit.cases by (cases v) auto
lemma less_eq_Bit_Bit1:
- "Numeral.Bit k1 v \<le> Numeral.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2"
+ "Int.Bit k1 v \<le> Int.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2"
unfolding Bit_def bit.cases by (cases v) auto
lemma less_eq_Bit1_Bit0:
- "Numeral.Bit k1 bit.B1 \<le> Numeral.Bit k2 bit.B0 \<longleftrightarrow> k1 < k2"
+ "Int.Bit k1 bit.B1 \<le> Int.Bit k2 bit.B0 \<longleftrightarrow> k1 < k2"
unfolding Bit_def by (auto split: bit.split)
lemma less_eq_number_of:
@@ -617,53 +617,53 @@
lemma less_Pls_Pls:
- "Numeral.Pls < Numeral.Pls \<longleftrightarrow> False" by simp
+ "Int.Pls < Int.Pls \<longleftrightarrow> False" by simp
lemma less_Pls_Min:
- "Numeral.Pls < Numeral.Min \<longleftrightarrow> False"
- unfolding Pls_def Numeral.Min_def by presburger
+ "Int.Pls < Int.Min \<longleftrightarrow> False"
+ unfolding Pls_def Int.Min_def by presburger
lemma less_Pls_Bit0:
- "Numeral.Pls < Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Pls < k"
+ "Int.Pls < Int.Bit k bit.B0 \<longleftrightarrow> Int.Pls < k"
unfolding Pls_def Bit_def by auto
lemma less_Pls_Bit1:
- "Numeral.Pls < Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Pls \<le> k"
+ "Int.Pls < Int.Bit k bit.B1 \<longleftrightarrow> Int.Pls \<le> k"
unfolding Pls_def Bit_def by auto
lemma less_Min_Pls:
- "Numeral.Min < Numeral.Pls \<longleftrightarrow> True"
- unfolding Pls_def Numeral.Min_def by presburger
+ "Int.Min < Int.Pls \<longleftrightarrow> True"
+ unfolding Pls_def Int.Min_def by presburger
lemma less_Min_Min:
- "Numeral.Min < Numeral.Min \<longleftrightarrow> False" by simp
+ "Int.Min < Int.Min \<longleftrightarrow> False" by simp
lemma less_Min_Bit:
- "Numeral.Min < Numeral.Bit k v \<longleftrightarrow> Numeral.Min < k"
- unfolding Numeral.Min_def Bit_def by (auto split: bit.split)
+ "Int.Min < Int.Bit k v \<longleftrightarrow> Int.Min < k"
+ unfolding Int.Min_def Bit_def by (auto split: bit.split)
lemma less_Bit_Pls:
- "Numeral.Bit k v < Numeral.Pls \<longleftrightarrow> k < Numeral.Pls"
+ "Int.Bit k v < Int.Pls \<longleftrightarrow> k < Int.Pls"
unfolding Pls_def Bit_def by (auto split: bit.split)
lemma less_Bit0_Min:
- "Numeral.Bit k bit.B0 < Numeral.Min \<longleftrightarrow> k \<le> Numeral.Min"
- unfolding Numeral.Min_def Bit_def by auto
+ "Int.Bit k bit.B0 < Int.Min \<longleftrightarrow> k \<le> Int.Min"
+ unfolding Int.Min_def Bit_def by auto
lemma less_Bit1_Min:
- "Numeral.Bit k bit.B1 < Numeral.Min \<longleftrightarrow> k < Numeral.Min"
- unfolding Numeral.Min_def Bit_def by auto
+ "Int.Bit k bit.B1 < Int.Min \<longleftrightarrow> k < Int.Min"
+ unfolding Int.Min_def Bit_def by auto
lemma less_Bit_Bit0:
- "Numeral.Bit k1 v < Numeral.Bit k2 bit.B0 \<longleftrightarrow> k1 < k2"
+ "Int.Bit k1 v < Int.Bit k2 bit.B0 \<longleftrightarrow> k1 < k2"
unfolding Bit_def by (auto split: bit.split)
lemma less_Bit1_Bit:
- "Numeral.Bit k1 bit.B1 < Numeral.Bit k2 v \<longleftrightarrow> k1 < k2"
+ "Int.Bit k1 bit.B1 < Int.Bit k2 v \<longleftrightarrow> k1 < k2"
unfolding Bit_def by (auto split: bit.split)
lemma less_Bit0_Bit1:
- "Numeral.Bit k1 bit.B0 < Numeral.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2"
+ "Int.Bit k1 bit.B0 < Int.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2"
unfolding Bit_def bit.cases by arith
lemma less_number_of:
--- a/src/HOL/SetInterval.thy Tue Jan 15 16:19:21 2008 +0100
+++ b/src/HOL/SetInterval.thy Tue Jan 15 16:19:23 2008 +0100
@@ -10,7 +10,7 @@
header {* Set intervals *}
theory SetInterval
-imports IntArith
+imports Int
begin
context ord
--- a/src/HOL/Tools/ComputeNumeral.thy Tue Jan 15 16:19:21 2008 +0100
+++ b/src/HOL/Tools/ComputeNumeral.thy Tue Jan 15 16:19:23 2008 +0100
@@ -6,84 +6,84 @@
lemmas bitnorm = Pls_0_eq Min_1_eq
(* neg for bit strings *)
-lemma neg1: "neg Numeral.Pls = False" by (simp add: Numeral.Pls_def)
-lemma neg2: "neg Numeral.Min = True" apply (subst Numeral.Min_def) by auto
-lemma neg3: "neg (x BIT Numeral.B0) = neg x" apply (simp add: neg_def) apply (subst Bit_def) by auto
-lemma neg4: "neg (x BIT Numeral.B1) = neg x" apply (simp add: neg_def) apply (subst Bit_def) by auto
+lemma neg1: "neg Int.Pls = False" by (simp add: Int.Pls_def)
+lemma neg2: "neg Int.Min = True" apply (subst Int.Min_def) by auto
+lemma neg3: "neg (x BIT Int.B0) = neg x" apply (simp add: neg_def) apply (subst Bit_def) by auto
+lemma neg4: "neg (x BIT Int.B1) = neg x" apply (simp add: neg_def) apply (subst Bit_def) by auto
lemmas bitneg = neg1 neg2 neg3 neg4
(* iszero for bit strings *)
-lemma iszero1: "iszero Numeral.Pls = True" by (simp add: Numeral.Pls_def iszero_def)
-lemma iszero2: "iszero Numeral.Min = False" apply (subst Numeral.Min_def) apply (subst iszero_def) by simp
-lemma iszero3: "iszero (x BIT Numeral.B0) = iszero x" apply (subst Numeral.Bit_def) apply (subst iszero_def)+ by auto
-lemma iszero4: "iszero (x BIT Numeral.B1) = False" apply (subst Numeral.Bit_def) apply (subst iszero_def)+ apply simp by arith
+lemma iszero1: "iszero Int.Pls = True" by (simp add: Int.Pls_def iszero_def)
+lemma iszero2: "iszero Int.Min = False" apply (subst Int.Min_def) apply (subst iszero_def) by simp
+lemma iszero3: "iszero (x BIT Int.B0) = iszero x" apply (subst Int.Bit_def) apply (subst iszero_def)+ by auto
+lemma iszero4: "iszero (x BIT Int.B1) = False" apply (subst Int.Bit_def) apply (subst iszero_def)+ apply simp by arith
lemmas bitiszero = iszero1 iszero2 iszero3 iszero4
(* lezero for bit strings *)
constdefs
"lezero x == (x \<le> 0)"
-lemma lezero1: "lezero Numeral.Pls = True" unfolding Numeral.Pls_def lezero_def by auto
-lemma lezero2: "lezero Numeral.Min = True" unfolding Numeral.Min_def lezero_def by auto
-lemma lezero3: "lezero (x BIT Numeral.B0) = lezero x" unfolding Numeral.Bit_def lezero_def by auto
-lemma lezero4: "lezero (x BIT Numeral.B1) = neg x" unfolding Numeral.Bit_def lezero_def neg_def by auto
+lemma lezero1: "lezero Int.Pls = True" unfolding Int.Pls_def lezero_def by auto
+lemma lezero2: "lezero Int.Min = True" unfolding Int.Min_def lezero_def by auto
+lemma lezero3: "lezero (x BIT Int.B0) = lezero x" unfolding Int.Bit_def lezero_def by auto
+lemma lezero4: "lezero (x BIT Int.B1) = neg x" unfolding Int.Bit_def lezero_def neg_def by auto
lemmas bitlezero = lezero1 lezero2 lezero3 lezero4
(* equality for bit strings *)
-lemma biteq1: "(Numeral.Pls = Numeral.Pls) = True" by auto
-lemma biteq2: "(Numeral.Min = Numeral.Min) = True" by auto
-lemma biteq3: "(Numeral.Pls = Numeral.Min) = False" unfolding Pls_def Min_def by auto
-lemma biteq4: "(Numeral.Min = Numeral.Pls) = False" unfolding Pls_def Min_def by auto
-lemma biteq5: "(x BIT Numeral.B0 = y BIT Numeral.B0) = (x = y)" unfolding Bit_def by auto
-lemma biteq6: "(x BIT Numeral.B1 = y BIT Numeral.B1) = (x = y)" unfolding Bit_def by auto
-lemma biteq7: "(x BIT Numeral.B0 = y BIT Numeral.B1) = False" unfolding Bit_def by (simp, arith)
-lemma biteq8: "(x BIT Numeral.B1 = y BIT Numeral.B0) = False" unfolding Bit_def by (simp, arith)
-lemma biteq9: "(Numeral.Pls = x BIT Numeral.B0) = (Numeral.Pls = x)" unfolding Bit_def Pls_def by auto
-lemma biteq10: "(Numeral.Pls = x BIT Numeral.B1) = False" unfolding Bit_def Pls_def by (simp, arith)
-lemma biteq11: "(Numeral.Min = x BIT Numeral.B0) = False" unfolding Bit_def Min_def by (simp, arith)
-lemma biteq12: "(Numeral.Min = x BIT Numeral.B1) = (Numeral.Min = x)" unfolding Bit_def Min_def by auto
-lemma biteq13: "(x BIT Numeral.B0 = Numeral.Pls) = (x = Numeral.Pls)" unfolding Bit_def Pls_def by auto
-lemma biteq14: "(x BIT Numeral.B1 = Numeral.Pls) = False" unfolding Bit_def Pls_def by (simp, arith)
-lemma biteq15: "(x BIT Numeral.B0 = Numeral.Min) = False" unfolding Bit_def Pls_def Min_def by (simp, arith)
-lemma biteq16: "(x BIT Numeral.B1 = Numeral.Min) = (x = Numeral.Min)" unfolding Bit_def Min_def by (simp, arith)
+lemma biteq1: "(Int.Pls = Int.Pls) = True" by auto
+lemma biteq2: "(Int.Min = Int.Min) = True" by auto
+lemma biteq3: "(Int.Pls = Int.Min) = False" unfolding Pls_def Min_def by auto
+lemma biteq4: "(Int.Min = Int.Pls) = False" unfolding Pls_def Min_def by auto
+lemma biteq5: "(x BIT Int.B0 = y BIT Int.B0) = (x = y)" unfolding Bit_def by auto
+lemma biteq6: "(x BIT Int.B1 = y BIT Int.B1) = (x = y)" unfolding Bit_def by auto
+lemma biteq7: "(x BIT Int.B0 = y BIT Int.B1) = False" unfolding Bit_def by (simp, arith)
+lemma biteq8: "(x BIT Int.B1 = y BIT Int.B0) = False" unfolding Bit_def by (simp, arith)
+lemma biteq9: "(Int.Pls = x BIT Int.B0) = (Int.Pls = x)" unfolding Bit_def Pls_def by auto
+lemma biteq10: "(Int.Pls = x BIT Int.B1) = False" unfolding Bit_def Pls_def by (simp, arith)
+lemma biteq11: "(Int.Min = x BIT Int.B0) = False" unfolding Bit_def Min_def by (simp, arith)
+lemma biteq12: "(Int.Min = x BIT Int.B1) = (Int.Min = x)" unfolding Bit_def Min_def by auto
+lemma biteq13: "(x BIT Int.B0 = Int.Pls) = (x = Int.Pls)" unfolding Bit_def Pls_def by auto
+lemma biteq14: "(x BIT Int.B1 = Int.Pls) = False" unfolding Bit_def Pls_def by (simp, arith)
+lemma biteq15: "(x BIT Int.B0 = Int.Min) = False" unfolding Bit_def Pls_def Min_def by (simp, arith)
+lemma biteq16: "(x BIT Int.B1 = Int.Min) = (x = Int.Min)" unfolding Bit_def Min_def by (simp, arith)
lemmas biteq = biteq1 biteq2 biteq3 biteq4 biteq5 biteq6 biteq7 biteq8 biteq9 biteq10 biteq11 biteq12 biteq13 biteq14 biteq15 biteq16
(* x < y for bit strings *)
-lemma bitless1: "(Numeral.Pls < Numeral.Min) = False" unfolding Pls_def Min_def by auto
-lemma bitless2: "(Numeral.Pls < Numeral.Pls) = False" by auto
-lemma bitless3: "(Numeral.Min < Numeral.Pls) = True" unfolding Pls_def Min_def by auto
-lemma bitless4: "(Numeral.Min < Numeral.Min) = False" unfolding Pls_def Min_def by auto
-lemma bitless5: "(x BIT Numeral.B0 < y BIT Numeral.B0) = (x < y)" unfolding Bit_def by auto
-lemma bitless6: "(x BIT Numeral.B1 < y BIT Numeral.B1) = (x < y)" unfolding Bit_def by auto
-lemma bitless7: "(x BIT Numeral.B0 < y BIT Numeral.B1) = (x \<le> y)" unfolding Bit_def by auto
-lemma bitless8: "(x BIT Numeral.B1 < y BIT Numeral.B0) = (x < y)" unfolding Bit_def by auto
-lemma bitless9: "(Numeral.Pls < x BIT Numeral.B0) = (Numeral.Pls < x)" unfolding Bit_def Pls_def by auto
-lemma bitless10: "(Numeral.Pls < x BIT Numeral.B1) = (Numeral.Pls \<le> x)" unfolding Bit_def Pls_def by auto
-lemma bitless11: "(Numeral.Min < x BIT Numeral.B0) = (Numeral.Pls \<le> x)" unfolding Bit_def Pls_def Min_def by auto
-lemma bitless12: "(Numeral.Min < x BIT Numeral.B1) = (Numeral.Min < x)" unfolding Bit_def Min_def by auto
-lemma bitless13: "(x BIT Numeral.B0 < Numeral.Pls) = (x < Numeral.Pls)" unfolding Bit_def Pls_def by auto
-lemma bitless14: "(x BIT Numeral.B1 < Numeral.Pls) = (x < Numeral.Pls)" unfolding Bit_def Pls_def by auto
-lemma bitless15: "(x BIT Numeral.B0 < Numeral.Min) = (x < Numeral.Pls)" unfolding Bit_def Pls_def Min_def by auto
-lemma bitless16: "(x BIT Numeral.B1 < Numeral.Min) = (x < Numeral.Min)" unfolding Bit_def Min_def by auto
+lemma bitless1: "(Int.Pls < Int.Min) = False" unfolding Pls_def Min_def by auto
+lemma bitless2: "(Int.Pls < Int.Pls) = False" by auto
+lemma bitless3: "(Int.Min < Int.Pls) = True" unfolding Pls_def Min_def by auto
+lemma bitless4: "(Int.Min < Int.Min) = False" unfolding Pls_def Min_def by auto
+lemma bitless5: "(x BIT Int.B0 < y BIT Int.B0) = (x < y)" unfolding Bit_def by auto
+lemma bitless6: "(x BIT Int.B1 < y BIT Int.B1) = (x < y)" unfolding Bit_def by auto
+lemma bitless7: "(x BIT Int.B0 < y BIT Int.B1) = (x \<le> y)" unfolding Bit_def by auto
+lemma bitless8: "(x BIT Int.B1 < y BIT Int.B0) = (x < y)" unfolding Bit_def by auto
+lemma bitless9: "(Int.Pls < x BIT Int.B0) = (Int.Pls < x)" unfolding Bit_def Pls_def by auto
+lemma bitless10: "(Int.Pls < x BIT Int.B1) = (Int.Pls \<le> x)" unfolding Bit_def Pls_def by auto
+lemma bitless11: "(Int.Min < x BIT Int.B0) = (Int.Pls \<le> x)" unfolding Bit_def Pls_def Min_def by auto
+lemma bitless12: "(Int.Min < x BIT Int.B1) = (Int.Min < x)" unfolding Bit_def Min_def by auto
+lemma bitless13: "(x BIT Int.B0 < Int.Pls) = (x < Int.Pls)" unfolding Bit_def Pls_def by auto
+lemma bitless14: "(x BIT Int.B1 < Int.Pls) = (x < Int.Pls)" unfolding Bit_def Pls_def by auto
+lemma bitless15: "(x BIT Int.B0 < Int.Min) = (x < Int.Pls)" unfolding Bit_def Pls_def Min_def by auto
+lemma bitless16: "(x BIT Int.B1 < Int.Min) = (x < Int.Min)" unfolding Bit_def Min_def by auto
lemmas bitless = bitless1 bitless2 bitless3 bitless4 bitless5 bitless6 bitless7 bitless8
bitless9 bitless10 bitless11 bitless12 bitless13 bitless14 bitless15 bitless16
(* x \<le> y for bit strings *)
-lemma bitle1: "(Numeral.Pls \<le> Numeral.Min) = False" unfolding Pls_def Min_def by auto
-lemma bitle2: "(Numeral.Pls \<le> Numeral.Pls) = True" by auto
-lemma bitle3: "(Numeral.Min \<le> Numeral.Pls) = True" unfolding Pls_def Min_def by auto
-lemma bitle4: "(Numeral.Min \<le> Numeral.Min) = True" unfolding Pls_def Min_def by auto
-lemma bitle5: "(x BIT Numeral.B0 \<le> y BIT Numeral.B0) = (x \<le> y)" unfolding Bit_def by auto
-lemma bitle6: "(x BIT Numeral.B1 \<le> y BIT Numeral.B1) = (x \<le> y)" unfolding Bit_def by auto
-lemma bitle7: "(x BIT Numeral.B0 \<le> y BIT Numeral.B1) = (x \<le> y)" unfolding Bit_def by auto
-lemma bitle8: "(x BIT Numeral.B1 \<le> y BIT Numeral.B0) = (x < y)" unfolding Bit_def by auto
-lemma bitle9: "(Numeral.Pls \<le> x BIT Numeral.B0) = (Numeral.Pls \<le> x)" unfolding Bit_def Pls_def by auto
-lemma bitle10: "(Numeral.Pls \<le> x BIT Numeral.B1) = (Numeral.Pls \<le> x)" unfolding Bit_def Pls_def by auto
-lemma bitle11: "(Numeral.Min \<le> x BIT Numeral.B0) = (Numeral.Pls \<le> x)" unfolding Bit_def Pls_def Min_def by auto
-lemma bitle12: "(Numeral.Min \<le> x BIT Numeral.B1) = (Numeral.Min \<le> x)" unfolding Bit_def Min_def by auto
-lemma bitle13: "(x BIT Numeral.B0 \<le> Numeral.Pls) = (x \<le> Numeral.Pls)" unfolding Bit_def Pls_def by auto
-lemma bitle14: "(x BIT Numeral.B1 \<le> Numeral.Pls) = (x < Numeral.Pls)" unfolding Bit_def Pls_def by auto
-lemma bitle15: "(x BIT Numeral.B0 \<le> Numeral.Min) = (x < Numeral.Pls)" unfolding Bit_def Pls_def Min_def by auto
-lemma bitle16: "(x BIT Numeral.B1 \<le> Numeral.Min) = (x \<le> Numeral.Min)" unfolding Bit_def Min_def by auto
+lemma bitle1: "(Int.Pls \<le> Int.Min) = False" unfolding Pls_def Min_def by auto
+lemma bitle2: "(Int.Pls \<le> Int.Pls) = True" by auto
+lemma bitle3: "(Int.Min \<le> Int.Pls) = True" unfolding Pls_def Min_def by auto
+lemma bitle4: "(Int.Min \<le> Int.Min) = True" unfolding Pls_def Min_def by auto
+lemma bitle5: "(x BIT Int.B0 \<le> y BIT Int.B0) = (x \<le> y)" unfolding Bit_def by auto
+lemma bitle6: "(x BIT Int.B1 \<le> y BIT Int.B1) = (x \<le> y)" unfolding Bit_def by auto
+lemma bitle7: "(x BIT Int.B0 \<le> y BIT Int.B1) = (x \<le> y)" unfolding Bit_def by auto
+lemma bitle8: "(x BIT Int.B1 \<le> y BIT Int.B0) = (x < y)" unfolding Bit_def by auto
+lemma bitle9: "(Int.Pls \<le> x BIT Int.B0) = (Int.Pls \<le> x)" unfolding Bit_def Pls_def by auto
+lemma bitle10: "(Int.Pls \<le> x BIT Int.B1) = (Int.Pls \<le> x)" unfolding Bit_def Pls_def by auto
+lemma bitle11: "(Int.Min \<le> x BIT Int.B0) = (Int.Pls \<le> x)" unfolding Bit_def Pls_def Min_def by auto
+lemma bitle12: "(Int.Min \<le> x BIT Int.B1) = (Int.Min \<le> x)" unfolding Bit_def Min_def by auto
+lemma bitle13: "(x BIT Int.B0 \<le> Int.Pls) = (x \<le> Int.Pls)" unfolding Bit_def Pls_def by auto
+lemma bitle14: "(x BIT Int.B1 \<le> Int.Pls) = (x < Int.Pls)" unfolding Bit_def Pls_def by auto
+lemma bitle15: "(x BIT Int.B0 \<le> Int.Min) = (x < Int.Pls)" unfolding Bit_def Pls_def Min_def by auto
+lemma bitle16: "(x BIT Int.B1 \<le> Int.Min) = (x \<le> Int.Min)" unfolding Bit_def Min_def by auto
lemmas bitle = bitle1 bitle2 bitle3 bitle4 bitle5 bitle6 bitle7 bitle8
bitle9 bitle10 bitle11 bitle12 bitle13 bitle14 bitle15 bitle16
@@ -97,14 +97,14 @@
lemmas bituminus = minus_Pls minus_Min minus_1 minus_0
(* addition for bit strings *)
-lemmas bitadd = add_Pls add_Pls_right add_Min add_Min_right add_BIT_11 add_BIT_10 add_BIT_0[where b="Numeral.B0"] add_BIT_0[where b="Numeral.B1"]
+lemmas bitadd = add_Pls add_Pls_right add_Min add_Min_right add_BIT_11 add_BIT_10 add_BIT_0[where b="Int.B0"] add_BIT_0[where b="Int.B1"]
(* multiplication for bit strings *)
-lemma mult_Pls_right: "x * Numeral.Pls = Numeral.Pls" by (simp add: Pls_def)
-lemma mult_Min_right: "x * Numeral.Min = - x" by (subst mult_commute, simp add: mult_Min)
-lemma multb0x: "(x BIT Numeral.B0) * y = (x * y) BIT Numeral.B0" unfolding Bit_def by simp
-lemma multxb0: "x * (y BIT Numeral.B0) = (x * y) BIT Numeral.B0" unfolding Bit_def by simp
-lemma multb1: "(x BIT Numeral.B1) * (y BIT Numeral.B1) = (((x * y) BIT Numeral.B0) + x + y) BIT Numeral.B1"
+lemma mult_Pls_right: "x * Int.Pls = Int.Pls" by (simp add: Pls_def)
+lemma mult_Min_right: "x * Int.Min = - x" by (subst mult_commute, simp add: mult_Min)
+lemma multb0x: "(x BIT Int.B0) * y = (x * y) BIT Int.B0" unfolding Bit_def by simp
+lemma multxb0: "x * (y BIT Int.B0) = (x * y) BIT Int.B0" unfolding Bit_def by simp
+lemma multb1: "(x BIT Int.B1) * (y BIT Int.B1) = (((x * y) BIT Int.B0) + x + y) BIT Int.B1"
unfolding Bit_def by (simp add: ring_simps)
lemmas bitmul = mult_Pls mult_Min mult_Pls_right mult_Min_right multb0x multxb0 multb1
@@ -120,12 +120,12 @@
done
(* Normalization of nat literals *)
-lemma natnorm0: "(0::nat) = number_of (Numeral.Pls)" by auto
-lemma natnorm1: "(1 :: nat) = number_of (Numeral.Pls BIT Numeral.B1)" by auto
+lemma natnorm0: "(0::nat) = number_of (Int.Pls)" by auto
+lemma natnorm1: "(1 :: nat) = number_of (Int.Pls BIT Int.B1)" by auto
lemmas natnorm = natnorm0 natnorm1 nat_norm_number_of
(* Suc *)
-lemma natsuc: "Suc (number_of x) = (if neg x then 1 else number_of (Numeral.succ x))" by (auto simp add: number_of_is_id)
+lemma natsuc: "Suc (number_of x) = (if neg x then 1 else number_of (Int.succ x))" by (auto simp add: number_of_is_id)
(* Addition for nat *)
lemma natadd: "number_of x + ((number_of y)::nat) = (if neg x then (number_of y) else (if neg y then number_of x else (number_of (x + y))))"
@@ -220,19 +220,19 @@
(* collecting all the theorems *)
-lemma even_Pls: "even (Numeral.Pls) = True"
+lemma even_Pls: "even (Int.Pls) = True"
apply (unfold Pls_def even_def)
by simp
-lemma even_Min: "even (Numeral.Min) = False"
+lemma even_Min: "even (Int.Min) = False"
apply (unfold Min_def even_def)
by simp
-lemma even_B0: "even (x BIT Numeral.B0) = True"
+lemma even_B0: "even (x BIT Int.B0) = True"
apply (unfold Bit_def)
by simp
-lemma even_B1: "even (x BIT Numeral.B1) = False"
+lemma even_B1: "even (x BIT Int.B1) = False"
apply (unfold Bit_def)
by simp
--- a/src/HOL/Tools/Qelim/cooper_data.ML Tue Jan 15 16:19:21 2008 +0100
+++ b/src/HOL/Tools/Qelim/cooper_data.ML Tue Jan 15 16:19:23 2008 +0100
@@ -24,7 +24,7 @@
@{term "op * :: int => _"}, @{term "op * :: nat => _"},
@{term "op div :: int => _"}, @{term "op div :: nat => _"},
@{term "op mod :: int => _"}, @{term "op mod :: nat => _"},
- @{term "Numeral.Bit"},
+ @{term "Int.Bit"},
@{term "op &"}, @{term "op |"}, @{term "op -->"},
@{term "op = :: int => _"}, @{term "op = :: nat => _"}, @{term "op = :: bool => _"},
@{term "op < :: int => _"}, @{term "op < :: nat => _"},
@@ -38,9 +38,9 @@
@{term "Ex :: (int => _) => _"}, @{term "Ex :: (nat => _) => _"},
@{term "All :: (int => _) => _"}, @{term "All :: (nat => _) => _"},
@{term "nat"}, @{term "int"},
- @{term "Numeral.bit.B0"},@{term "Numeral.bit.B1"},
- @{term "Numeral.Bit"}, @{term "Numeral.Pls"}, @{term "Numeral.Min"},
- @{term "Numeral.number_of :: int => int"}, @{term "Numeral.number_of :: int => nat"},
+ @{term "Int.bit.B0"},@{term "Int.bit.B1"},
+ @{term "Int.Bit"}, @{term "Int.Pls"}, @{term "Int.Min"},
+ @{term "Int.number_of :: int => int"}, @{term "Int.number_of :: int => nat"},
@{term "0::int"}, @{term "1::int"}, @{term "0::nat"}, @{term "1::nat"},
@{term "True"}, @{term "False"}];
--- a/src/HOL/Tools/lin_arith.ML Tue Jan 15 16:19:21 2008 +0100
+++ b/src/HOL/Tools/lin_arith.ML Tue Jan 15 16:19:23 2008 +0100
@@ -203,7 +203,7 @@
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 ("Numeral.number_class.number_of", _) $ n, m) =
+ | demult (t as Const ("Int.number_class.number_of", _) $ n, m) =
((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) =
@@ -242,7 +242,7 @@
(case demult inj_consts (all, m) of
(NONE, m') => (p, Rat.add i m')
| (SOME u, m') => add_atom u m' pi)
- | poly (all as Const ("Numeral.number_class.number_of", Type(_,[_,T])) $ t, m, pi as (p, i)) =
+ | poly (all as Const ("Int.number_class.number_of", Type(_,[_,T])) $ t, m, pi as (p, i)) =
(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_int k2))) end
@@ -324,7 +324,7 @@
@{const_name Orderings.min},
@{const_name HOL.abs},
@{const_name HOL.minus},
- "IntDef.nat",
+ "Int.nat",
"Divides.div_class.mod",
"Divides.div_class.div"] a
| _ => (warning ("Lin. Arith.: wrong format for split rule " ^
@@ -462,7 +462,7 @@
SOME [(Ts, subgoal1), (split_type :: Ts, subgoal2)]
end
(* ?P (nat ?i) = ((ALL n. ?i = int n --> ?P n) & (?i < 0 --> ?P 0)) *)
- | (Const ("IntDef.nat", _), [t1]) =>
+ | (Const ("Int.nat", _), [t1]) =>
let
val rev_terms = rev terms
val zero_int = Const (@{const_name HOL.zero}, HOLogic.intT)
@@ -553,7 +553,7 @@
(neg (number_of ?k) -->
(ALL i j. number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j --> ?P j))) *)
| (Const ("Divides.div_class.mod",
- Type ("fun", [Type ("IntDef.int", []), _])), [t1, t2 as (number_of $ k)]) =>
+ Type ("fun", [Type ("Int.int", []), _])), [t1, t2 as (number_of $ k)]) =>
let
val rev_terms = rev terms
val zero = Const (@{const_name HOL.zero}, split_type)
@@ -564,8 +564,8 @@
(map (incr_boundvars 2) rev_terms)
val t1' = incr_boundvars 2 t1
val (t2' as (_ $ k')) = incr_boundvars 2 t2
- val iszero_t2 = Const ("IntDef.iszero", split_type --> HOLogic.boolT) $ t2
- val neg_minus_k = Const ("IntDef.neg", split_type --> HOLogic.boolT) $
+ val iszero_t2 = Const ("Int.iszero", split_type --> HOLogic.boolT) $ t2
+ val neg_minus_k = Const ("Int.neg", split_type --> HOLogic.boolT) $
(number_of $
(Const (@{const_name HOL.uminus},
HOLogic.intT --> HOLogic.intT) $ k'))
@@ -577,7 +577,7 @@
(Const (@{const_name HOL.plus}, split_type --> split_type --> split_type) $
(Const (@{const_name HOL.times},
split_type --> split_type --> split_type) $ t2' $ i) $ j)
- val neg_t2 = Const ("IntDef.neg", split_type --> HOLogic.boolT) $ t2'
+ val neg_t2 = Const ("Int.neg", split_type --> HOLogic.boolT) $ t2'
val t2_lt_j = Const (@{const_name HOL.less},
split_type --> split_type--> HOLogic.boolT) $ t2' $ j
val j_leq_zero = Const (@{const_name HOL.less_eq},
@@ -605,7 +605,7 @@
(neg (number_of ?k) -->
(ALL i. (EX j. number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j) --> ?P i))) *)
| (Const ("Divides.div_class.div",
- Type ("fun", [Type ("IntDef.int", []), _])), [t1, t2 as (number_of $ k)]) =>
+ Type ("fun", [Type ("Int.int", []), _])), [t1, t2 as (number_of $ k)]) =>
let
val rev_terms = rev terms
val zero = Const (@{const_name HOL.zero}, split_type)
@@ -616,8 +616,8 @@
(map (incr_boundvars 2) rev_terms)
val t1' = incr_boundvars 2 t1
val (t2' as (_ $ k')) = incr_boundvars 2 t2
- val iszero_t2 = Const ("IntDef.iszero", split_type --> HOLogic.boolT) $ t2
- val neg_minus_k = Const ("IntDef.neg", split_type --> HOLogic.boolT) $
+ val iszero_t2 = Const ("Int.iszero", split_type --> HOLogic.boolT) $ t2
+ val neg_minus_k = Const ("Int.neg", split_type --> HOLogic.boolT) $
(number_of $
(Const (@{const_name HOL.uminus},
HOLogic.intT --> HOLogic.intT) $ k'))
@@ -630,7 +630,7 @@
(Const (@{const_name HOL.plus}, split_type --> split_type --> split_type) $
(Const (@{const_name HOL.times},
split_type --> split_type --> split_type) $ t2' $ i) $ j)
- val neg_t2 = Const ("IntDef.neg", split_type --> HOLogic.boolT) $ t2'
+ val neg_t2 = Const ("Int.neg", split_type --> HOLogic.boolT) $ t2'
val t2_lt_j = Const (@{const_name HOL.less},
split_type --> split_type--> HOLogic.boolT) $ t2' $ j
val j_leq_zero = Const (@{const_name HOL.less_eq},
--- a/src/HOL/Tools/numeral.ML Tue Jan 15 16:19:21 2008 +0100
+++ b/src/HOL/Tools/numeral.ML Tue Jan 15 16:19:23 2008 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/Tools/numeral.ML
+(* Title: HOL/Tools/Int.ML
ID: $Id$
Author: Makarius
@@ -16,15 +16,15 @@
(* numeral *)
-fun mk_cbit 0 = @{cterm "Numeral.bit.B0"}
- | mk_cbit 1 = @{cterm "Numeral.bit.B1"}
+fun mk_cbit 0 = @{cterm "Int.bit.B0"}
+ | mk_cbit 1 = @{cterm "Int.bit.B1"}
| mk_cbit _ = raise CTERM ("mk_cbit", []);
-fun mk_cnumeral 0 = @{cterm "Numeral.Pls"}
- | mk_cnumeral ~1 = @{cterm "Numeral.Min"}
+fun mk_cnumeral 0 = @{cterm "Int.Pls"}
+ | mk_cnumeral ~1 = @{cterm "Int.Min"}
| mk_cnumeral i =
let val (q, r) = Integer.div_mod i 2 in
- Thm.capply (Thm.capply @{cterm "Numeral.Bit"} (mk_cnumeral q)) (mk_cbit r)
+ Thm.capply (Thm.capply @{cterm "Int.Bit"} (mk_cnumeral q)) (mk_cbit r)
end;
--- a/src/HOL/Tools/numeral_syntax.ML Tue Jan 15 16:19:21 2008 +0100
+++ b/src/HOL/Tools/numeral_syntax.ML Tue Jan 15 16:19:23 2008 +0100
@@ -20,16 +20,16 @@
fun mk_bin num =
let
val {leading_zeros = z, value, ...} = Syntax.read_xnum num;
- fun bit b bs = Syntax.const @{const_name Numeral.Bit} $ bs $ HOLogic.mk_bit b;
- fun mk 0 = (* FIXME funpow z (bit 0) *) (Syntax.const @{const_name Numeral.Pls})
- | mk ~1 = (* FIXME funpow z (bit 1) *) (Syntax.const @{const_name Numeral.Min})
+ fun bit b bs = Syntax.const @{const_name Int.Bit} $ bs $ HOLogic.mk_bit b;
+ fun mk 0 = (* FIXME funpow z (bit 0) *) (Syntax.const @{const_name Int.Pls})
+ | mk ~1 = (* FIXME funpow z (bit 1) *) (Syntax.const @{const_name Int.Min})
| mk i = let val (q, r) = Integer.div_mod i 2 in bit r (mk q) end;
in mk value end;
in
fun numeral_tr (*"_Numeral"*) [t as Const (num, _)] =
- Syntax.const @{const_name Numeral.number_of} $ mk_bin num
+ Syntax.const @{const_name Int.number_of} $ mk_bin num
| numeral_tr (*"_Numeral"*) ts = raise TERM ("numeral_tr", ts);
end;
@@ -39,15 +39,15 @@
local
-fun dest_bit (Const (@{const_syntax Numeral.bit.B0}, _)) = 0
- | dest_bit (Const (@{const_syntax Numeral.bit.B1}, _)) = 1
+fun dest_bit (Const (@{const_syntax Int.bit.B0}, _)) = 0
+ | dest_bit (Const (@{const_syntax Int.bit.B1}, _)) = 1
| dest_bit (Const ("bit.B0", _)) = 0
| dest_bit (Const ("bit.B1", _)) = 1
| dest_bit _ = raise Match;
-fun dest_bin (Const (@{const_syntax "Numeral.Pls"}, _)) = []
- | dest_bin (Const (@{const_syntax "Numeral.Min"}, _)) = [~1]
- | dest_bin (Const (@{const_syntax "Numeral.Bit"}, _) $ bs $ b) = dest_bit b :: dest_bin bs
+fun dest_bin (Const (@{const_syntax "Int.Pls"}, _)) = []
+ | dest_bin (Const (@{const_syntax "Int.Min"}, _)) = [~1]
+ | dest_bin (Const (@{const_syntax "Int.Bit"}, _) $ bs $ b) = dest_bit b :: dest_bin bs
| dest_bin _ = raise Match;
fun leading _ [] = 0
@@ -89,6 +89,6 @@
val setup =
Sign.add_trfuns ([], [("_Numeral", numeral_tr)], [], []) #>
- Sign.add_trfunsT [(@{const_syntax Numeral.number_of}, numeral_tr')];
+ Sign.add_trfunsT [(@{const_syntax Int.number_of}, numeral_tr')];
end;
--- a/src/HOL/Word/BinBoolList.thy Tue Jan 15 16:19:21 2008 +0100
+++ b/src/HOL/Word/BinBoolList.thy Tue Jan 15 16:19:23 2008 +0100
@@ -76,13 +76,13 @@
by (induct n) (auto simp: butlast_take)
lemma bin_to_bl_aux_Pls_minus_simp:
- "0 < n ==> bin_to_bl_aux n Numeral.Pls bl =
- bin_to_bl_aux (n - 1) Numeral.Pls (False # bl)"
+ "0 < n ==> bin_to_bl_aux n Int.Pls bl =
+ bin_to_bl_aux (n - 1) Int.Pls (False # bl)"
by (cases n) auto
lemma bin_to_bl_aux_Min_minus_simp:
- "0 < n ==> bin_to_bl_aux n Numeral.Min bl =
- bin_to_bl_aux (n - 1) Numeral.Min (True # bl)"
+ "0 < n ==> bin_to_bl_aux n Int.Min bl =
+ bin_to_bl_aux (n - 1) Int.Min (True # bl)"
by (cases n) auto
lemma bin_to_bl_aux_Bit_minus_simp:
@@ -166,21 +166,21 @@
lemma bl_to_bin_False: "bl_to_bin (False # bl) = bl_to_bin bl"
unfolding bl_to_bin_def by auto
-lemma bl_to_bin_Nil: "bl_to_bin [] = Numeral.Pls"
+lemma bl_to_bin_Nil: "bl_to_bin [] = Int.Pls"
unfolding bl_to_bin_def by auto
lemma bin_to_bl_Pls_aux [rule_format] :
- "ALL bl. bin_to_bl_aux n Numeral.Pls bl = replicate n False @ bl"
+ "ALL bl. bin_to_bl_aux n Int.Pls bl = replicate n False @ bl"
by (induct n) (auto simp: replicate_app_Cons_same)
-lemma bin_to_bl_Pls: "bin_to_bl n Numeral.Pls = replicate n False"
+lemma bin_to_bl_Pls: "bin_to_bl n Int.Pls = replicate n False"
unfolding bin_to_bl_def by (simp add : bin_to_bl_Pls_aux)
lemma bin_to_bl_Min_aux [rule_format] :
- "ALL bl. bin_to_bl_aux n Numeral.Min bl = replicate n True @ bl"
+ "ALL bl. bin_to_bl_aux n Int.Min bl = replicate n True @ bl"
by (induct n) (auto simp: replicate_app_Cons_same)
-lemma bin_to_bl_Min: "bin_to_bl n Numeral.Min = replicate n True"
+lemma bin_to_bl_Min: "bin_to_bl n Int.Min = replicate n True"
unfolding bin_to_bl_def by (simp add : bin_to_bl_Min_aux)
lemma bl_to_bin_rep_F:
@@ -214,7 +214,7 @@
lemmas bin_to_bl_bintr =
bin_to_bl_aux_bintr [where bl = "[]", folded bin_to_bl_def]
-lemma bl_to_bin_rep_False: "bl_to_bin (replicate n False) = Numeral.Pls"
+lemma bl_to_bin_rep_False: "bl_to_bin (replicate n False) = Int.Pls"
by (induct n) auto
lemma len_bin_to_bl_aux [rule_format] :
@@ -228,12 +228,12 @@
"ALL w. bin_sign (bl_to_bin_aux w bs) = bin_sign w"
by (induct bs) auto
-lemma sign_bl_bin: "bin_sign (bl_to_bin bs) = Numeral.Pls"
+lemma sign_bl_bin: "bin_sign (bl_to_bin bs) = Int.Pls"
unfolding bl_to_bin_def by (simp add : sign_bl_bin')
lemma bl_sbin_sign_aux [rule_format] :
"ALL w bs. hd (bin_to_bl_aux (Suc n) w bs) =
- (bin_sign (sbintrunc n w) = Numeral.Min)"
+ (bin_sign (sbintrunc n w) = Int.Min)"
apply (induct "n")
apply clarsimp
apply (case_tac w rule: bin_exhaust)
@@ -242,7 +242,7 @@
done
lemma bl_sbin_sign:
- "hd (bin_to_bl (Suc n) w) = (bin_sign (sbintrunc n w) = Numeral.Min)"
+ "hd (bin_to_bl (Suc n) w) = (bin_sign (sbintrunc n w) = Int.Min)"
unfolding bin_to_bl_def by (rule bl_sbin_sign_aux)
lemma bin_nth_of_bl_aux [rule_format] :
@@ -658,7 +658,7 @@
by (induct nw) auto
lemmas bl_to_bin_aux_alt =
- bl_to_bin_aux_cat [where nv = "0" and v = "Numeral.Pls",
+ bl_to_bin_aux_cat [where nv = "0" and v = "Int.Pls",
simplified bl_to_bin_def [symmetric], simplified]
lemmas bin_to_bl_cat =
@@ -671,7 +671,7 @@
trans [OF bin_to_bl_aux_cat bin_to_bl_aux_alt]
lemmas bl_to_bin_app_cat = bl_to_bin_aux_app_cat
- [where w = "Numeral.Pls", folded bl_to_bin_def]
+ [where w = "Int.Pls", folded bl_to_bin_def]
lemmas bin_to_bl_cat_app = bin_to_bl_aux_cat_app
[where bs = "[]", folded bin_to_bl_def]
@@ -682,7 +682,7 @@
by (simp add : bl_to_bin_app_cat)
lemma mask_lem: "(bl_to_bin (True # replicate n False)) =
- Numeral.succ (bl_to_bin (replicate n True))"
+ Int.succ (bl_to_bin (replicate n True))"
apply (unfold bl_to_bin_def)
apply (induct n)
apply simp
@@ -745,7 +745,7 @@
rbl_pred.Nil rbl_succ.Nil rbl_add.Nil rbl_mult.Nil
lemma rbl_pred:
- "!!bin. rbl_pred (rev (bin_to_bl n bin)) = rev (bin_to_bl n (Numeral.pred bin))"
+ "!!bin. rbl_pred (rev (bin_to_bl n bin)) = rev (bin_to_bl n (Int.pred bin))"
apply (induct n, simp)
apply (unfold bin_to_bl_def)
apply clarsimp
@@ -755,7 +755,7 @@
done
lemma rbl_succ:
- "!!bin. rbl_succ (rev (bin_to_bl n bin)) = rev (bin_to_bl n (Numeral.succ bin))"
+ "!!bin. rbl_succ (rev (bin_to_bl n bin)) = rev (bin_to_bl n (Int.succ bin))"
apply (induct n, simp)
apply (unfold bin_to_bl_def)
apply clarsimp
@@ -1011,7 +1011,7 @@
lemma bin_split_pred_simp [simp]:
"(0::nat) < number_of bin \<Longrightarrow>
bin_split (number_of bin) w =
- (let (w1, w2) = bin_split (number_of (Numeral.pred bin)) (bin_rest w)
+ (let (w1, w2) = bin_split (number_of (Int.pred bin)) (bin_rest w)
in (w1, w2 BIT bin_last w))"
by (simp only: nobm1 bin_split_minus_simp)
--- a/src/HOL/Word/BinGeneral.thy Tue Jan 15 16:19:21 2008 +0100
+++ b/src/HOL/Word/BinGeneral.thy Tue Jan 15 16:19:23 2008 +0100
@@ -15,14 +15,14 @@
subsection {* Recursion combinator for binary integers *}
-lemma brlem: "(bin = Numeral.Min) = (- bin + Numeral.pred 0 = 0)"
+lemma brlem: "(bin = Int.Min) = (- bin + Int.pred 0 = 0)"
unfolding Min_def pred_def by arith
function
bin_rec' :: "int * 'a * 'a * (int => bit => 'a => 'a) => 'a"
where
- "bin_rec' (bin, f1, f2, f3) = (if bin = Numeral.Pls then f1
- else if bin = Numeral.Min then f2
+ "bin_rec' (bin, f1, f2, f3) = (if bin = Int.Pls then f1
+ else if bin = Int.Min then f2
else case bin_rl bin of (w, b) => f3 w b (bin_rec' (w, f1, f2, f3)))"
by pat_completeness auto
@@ -43,7 +43,7 @@
"bin_rec f1 f2 f3 bin == bin_rec' (bin, f1, f2, f3)"
lemma bin_rec_PM:
- "f = bin_rec f1 f2 f3 ==> f Numeral.Pls = f1 & f Numeral.Min = f2"
+ "f = bin_rec f1 f2 f3 ==> f Int.Pls = f1 & f Int.Min = f2"
apply safe
apply (unfold bin_rec_def)
apply (auto intro: bin_rec'.simps [THEN trans])
@@ -53,8 +53,8 @@
lemmas bin_rec_Min = refl [THEN bin_rec_PM, THEN conjunct2, standard]
lemma bin_rec_Bit:
- "f = bin_rec f1 f2 f3 ==> f3 Numeral.Pls bit.B0 f1 = f1 ==>
- f3 Numeral.Min bit.B1 f2 = f2 ==> f (w BIT b) = f3 w b (f w)"
+ "f = bin_rec f1 f2 f3 ==> f3 Int.Pls bit.B0 f1 = f1 ==>
+ f3 Int.Min bit.B1 f2 = f2 ==> f (w BIT b) = f3 w b (f w)"
apply clarify
apply (unfold bin_rec_def)
apply (rule bin_rec'.simps [THEN trans])
@@ -81,7 +81,7 @@
defs
bin_rest_def : "bin_rest w == fst (bin_rl w)"
bin_last_def : "bin_last w == snd (bin_rl w)"
- bin_sign_def : "bin_sign == bin_rec Numeral.Pls Numeral.Min (%w b s. s)"
+ bin_sign_def : "bin_sign == bin_rec Int.Pls Int.Min (%w b s. s)"
lemma bin_rl: "bin_rl w = (bin_rest w, bin_last w)"
unfolding bin_rest_def bin_last_def by auto
@@ -89,20 +89,20 @@
lemmas bin_rl_simp [simp] = iffD1 [OF bin_rl_char bin_rl]
lemma bin_rest_simps [simp]:
- "bin_rest Numeral.Pls = Numeral.Pls"
- "bin_rest Numeral.Min = Numeral.Min"
+ "bin_rest Int.Pls = Int.Pls"
+ "bin_rest Int.Min = Int.Min"
"bin_rest (w BIT b) = w"
unfolding bin_rest_def by auto
lemma bin_last_simps [simp]:
- "bin_last Numeral.Pls = bit.B0"
- "bin_last Numeral.Min = bit.B1"
+ "bin_last Int.Pls = bit.B0"
+ "bin_last Int.Min = bit.B1"
"bin_last (w BIT b) = b"
unfolding bin_last_def by auto
lemma bin_sign_simps [simp]:
- "bin_sign Numeral.Pls = Numeral.Pls"
- "bin_sign Numeral.Min = Numeral.Min"
+ "bin_sign Int.Pls = Int.Pls"
+ "bin_sign Int.Min = Int.Min"
"bin_sign (w BIT b) = bin_sign w"
unfolding bin_sign_def by (auto simp: bin_rec_simps)
@@ -176,10 +176,10 @@
lemmas bin_eqI = ext [THEN bin_nth_eq_iff [THEN iffD1], standard]
-lemma bin_nth_Pls [simp]: "~ bin_nth Numeral.Pls n"
+lemma bin_nth_Pls [simp]: "~ bin_nth Int.Pls n"
by (induct n) auto
-lemma bin_nth_Min [simp]: "bin_nth Numeral.Min n"
+lemma bin_nth_Min [simp]: "bin_nth Int.Min n"
by (induct n) auto
lemma bin_nth_0_BIT: "bin_nth (w BIT b) 0 = (b = bit.B1)"
@@ -206,18 +206,18 @@
consts
bintrunc :: "nat => int => int"
primrec
- Z : "bintrunc 0 bin = Numeral.Pls"
+ Z : "bintrunc 0 bin = Int.Pls"
Suc : "bintrunc (Suc n) bin = bintrunc n (bin_rest bin) BIT (bin_last bin)"
consts
sbintrunc :: "nat => int => int"
primrec
Z : "sbintrunc 0 bin =
- (case bin_last bin of bit.B1 => Numeral.Min | bit.B0 => Numeral.Pls)"
+ (case bin_last bin of bit.B1 => Int.Min | bit.B0 => Int.Pls)"
Suc : "sbintrunc (Suc n) bin = sbintrunc n (bin_rest bin) BIT (bin_last bin)"
lemma sign_bintr:
- "!!w. bin_sign (bintrunc n w) = Numeral.Pls"
+ "!!w. bin_sign (bintrunc n w) = Int.Pls"
by (induct n) auto
lemma bintrunc_mod2p:
@@ -253,7 +253,7 @@
lemmas bit_bool1 [simp] = refl [THEN bit_bool [THEN iffD1], symmetric]
lemma bin_sign_lem:
- "!!bin. (bin_sign (sbintrunc n bin) = Numeral.Min) = bin_nth bin n"
+ "!!bin. (bin_sign (sbintrunc n bin) = Int.Min) = bin_nth bin n"
apply (induct n)
apply (case_tac bin rule: bin_exhaust, case_tac b, auto)+
done
@@ -304,10 +304,10 @@
done
lemmas bintrunc_Pls =
- bintrunc.Suc [where bin="Numeral.Pls", simplified bin_last_simps bin_rest_simps, standard]
+ bintrunc.Suc [where bin="Int.Pls", simplified bin_last_simps bin_rest_simps, standard]
lemmas bintrunc_Min [simp] =
- bintrunc.Suc [where bin="Numeral.Min", simplified bin_last_simps bin_rest_simps, standard]
+ bintrunc.Suc [where bin="Int.Min", simplified bin_last_simps bin_rest_simps, standard]
lemmas bintrunc_BIT [simp] =
bintrunc.Suc [where bin="w BIT b", simplified bin_last_simps bin_rest_simps, standard]
@@ -315,10 +315,10 @@
lemmas bintrunc_Sucs = bintrunc_Pls bintrunc_Min bintrunc_BIT
lemmas sbintrunc_Suc_Pls =
- sbintrunc.Suc [where bin="Numeral.Pls", simplified bin_last_simps bin_rest_simps, standard]
+ sbintrunc.Suc [where bin="Int.Pls", simplified bin_last_simps bin_rest_simps, standard]
lemmas sbintrunc_Suc_Min =
- sbintrunc.Suc [where bin="Numeral.Min", simplified bin_last_simps bin_rest_simps, standard]
+ sbintrunc.Suc [where bin="Int.Min", simplified bin_last_simps bin_rest_simps, standard]
lemmas sbintrunc_Suc_BIT [simp] =
sbintrunc.Suc [where bin="w BIT b", simplified bin_last_simps bin_rest_simps, standard]
@@ -326,11 +326,11 @@
lemmas sbintrunc_Sucs = sbintrunc_Suc_Pls sbintrunc_Suc_Min sbintrunc_Suc_BIT
lemmas sbintrunc_Pls =
- sbintrunc.Z [where bin="Numeral.Pls",
+ sbintrunc.Z [where bin="Int.Pls",
simplified bin_last_simps bin_rest_simps bit.simps, standard]
lemmas sbintrunc_Min =
- sbintrunc.Z [where bin="Numeral.Min",
+ sbintrunc.Z [where bin="Int.Min",
simplified bin_last_simps bin_rest_simps bit.simps, standard]
lemmas sbintrunc_0_BIT_B0 [simp] =
@@ -361,12 +361,12 @@
sbintrunc_Sucs [THEN [2] sbintrunc_minus [symmetric, THEN trans], standard]
lemma bintrunc_n_Pls [simp]:
- "bintrunc n Numeral.Pls = Numeral.Pls"
+ "bintrunc n Int.Pls = Int.Pls"
by (induct n) auto
lemma sbintrunc_n_PM [simp]:
- "sbintrunc n Numeral.Pls = Numeral.Pls"
- "sbintrunc n Numeral.Min = Numeral.Min"
+ "sbintrunc n Int.Pls = Int.Pls"
+ "sbintrunc n Int.Min = Int.Min"
by (induct n) auto
lemmas thobini1 = arg_cong [where f = "%w. w BIT b", standard]
@@ -379,9 +379,9 @@
lemmas bintrunc_Min_minus_I = bmsts(2)
lemmas bintrunc_BIT_minus_I = bmsts(3)
-lemma bintrunc_0_Min: "bintrunc 0 Numeral.Min = Numeral.Pls"
+lemma bintrunc_0_Min: "bintrunc 0 Int.Min = Int.Pls"
by auto
-lemma bintrunc_0_BIT: "bintrunc 0 (w BIT b) = Numeral.Pls"
+lemma bintrunc_0_BIT: "bintrunc 0 (w BIT b) = Int.Pls"
by auto
lemma bintrunc_Suc_lem:
@@ -558,7 +558,7 @@
by (simp add : no_bintr m2pths)
lemma bintr_Min:
- "number_of (bintrunc n Numeral.Min) = (2 ^ n :: int) - 1"
+ "number_of (bintrunc n Int.Min) = (2 ^ n :: int) - 1"
by (simp add : no_bintr m1mod2k)
lemma sbintr_ge: "(- (2 ^ n) :: int) <= number_of (sbintrunc n w)"
@@ -572,11 +572,11 @@
by (case_tac bin rule: bin_exhaust) auto
lemma sign_Pls_ge_0:
- "(bin_sign bin = Numeral.Pls) = (number_of bin >= (0 :: int))"
+ "(bin_sign bin = Int.Pls) = (number_of bin >= (0 :: int))"
by (induct bin rule: bin_induct) auto
lemma sign_Min_lt_0:
- "(bin_sign bin = Numeral.Min) = (number_of bin < (0 :: int))"
+ "(bin_sign bin = Int.Min) = (number_of bin < (0 :: int))"
by (induct bin rule: bin_induct) auto
lemmas sign_Min_neg = trans [OF sign_Min_lt_0 neg_def [symmetric]]
@@ -647,7 +647,7 @@
consts
bin_split :: "nat => int => int * int"
primrec
- Z : "bin_split 0 w = (w, Numeral.Pls)"
+ Z : "bin_split 0 w = (w, Int.Pls)"
Suc : "bin_split (Suc n) w = (let (w1, w2) = bin_split n (bin_rest w)
in (w1, w2 BIT bin_last w))"
@@ -702,7 +702,7 @@
by auto
lemma size_Cons_lem_eq_bin:
- "y = xa # list ==> size y = number_of (Numeral.succ k) ==>
+ "y = xa # list ==> size y = number_of (Int.succ k) ==>
size list = number_of k"
by (auto simp: pred_def succ_def split add : split_if_asm)
--- a/src/HOL/Word/BinOperations.thy Tue Jan 15 16:19:21 2008 +0100
+++ b/src/HOL/Word/BinOperations.thy Tue Jan 15 16:19:23 2008 +0100
@@ -21,15 +21,15 @@
begin
definition
- int_not_def: "bitNOT = bin_rec Numeral.Min Numeral.Pls
+ int_not_def: "bitNOT = bin_rec Int.Min Int.Pls
(\<lambda>w b s. s BIT (NOT b))"
definition
- int_and_def: "bitAND = bin_rec (\<lambda>x. Numeral.Pls) (\<lambda>y. y)
+ int_and_def: "bitAND = bin_rec (\<lambda>x. Int.Pls) (\<lambda>y. y)
(\<lambda>w b s y. s (bin_rest y) BIT (b AND bin_last y))"
definition
- int_or_def: "bitOR = bin_rec (\<lambda>x. x) (\<lambda>y. Numeral.Min)
+ int_or_def: "bitOR = bin_rec (\<lambda>x. x) (\<lambda>y. Int.Min)
(\<lambda>w b s y. s (bin_rest y) BIT (b OR bin_last y))"
definition
@@ -41,17 +41,17 @@
end
lemma int_not_simps [simp]:
- "NOT Numeral.Pls = Numeral.Min"
- "NOT Numeral.Min = Numeral.Pls"
+ "NOT Int.Pls = Int.Min"
+ "NOT Int.Min = Int.Pls"
"NOT (w BIT b) = (NOT w) BIT (NOT b)"
by (unfold int_not_def) (auto intro: bin_rec_simps)
lemma int_xor_Pls [simp]:
- "Numeral.Pls XOR x = x"
+ "Int.Pls XOR x = x"
unfolding int_xor_def by (simp add: bin_rec_PM)
lemma int_xor_Min [simp]:
- "Numeral.Min XOR x = NOT x"
+ "Int.Min XOR x = NOT x"
unfolding int_xor_def by (simp add: bin_rec_PM)
lemma int_xor_Bits [simp]:
@@ -66,8 +66,8 @@
done
lemma int_xor_x_simps':
- "w XOR (Numeral.Pls BIT bit.B0) = w"
- "w XOR (Numeral.Min BIT bit.B1) = NOT w"
+ "w XOR (Int.Pls BIT bit.B0) = w"
+ "w XOR (Int.Min BIT bit.B1) = NOT w"
apply (induct w rule: bin_induct)
apply simp_all[4]
apply (unfold int_xor_Bits)
@@ -77,11 +77,11 @@
lemmas int_xor_extra_simps [simp] = int_xor_x_simps' [simplified arith_simps]
lemma int_or_Pls [simp]:
- "Numeral.Pls OR x = x"
+ "Int.Pls OR x = x"
by (unfold int_or_def) (simp add: bin_rec_PM)
lemma int_or_Min [simp]:
- "Numeral.Min OR x = Numeral.Min"
+ "Int.Min OR x = Int.Min"
by (unfold int_or_def) (simp add: bin_rec_PM)
lemma int_or_Bits [simp]:
@@ -89,8 +89,8 @@
unfolding int_or_def by (simp add: bin_rec_simps)
lemma int_or_x_simps':
- "w OR (Numeral.Pls BIT bit.B0) = w"
- "w OR (Numeral.Min BIT bit.B1) = Numeral.Min"
+ "w OR (Int.Pls BIT bit.B0) = w"
+ "w OR (Int.Min BIT bit.B1) = Int.Min"
apply (induct w rule: bin_induct)
apply simp_all[4]
apply (unfold int_or_Bits)
@@ -101,11 +101,11 @@
lemma int_and_Pls [simp]:
- "Numeral.Pls AND x = Numeral.Pls"
+ "Int.Pls AND x = Int.Pls"
unfolding int_and_def by (simp add: bin_rec_PM)
lemma int_and_Min [simp]:
- "Numeral.Min AND x = x"
+ "Int.Min AND x = x"
unfolding int_and_def by (simp add: bin_rec_PM)
lemma int_and_Bits [simp]:
@@ -113,8 +113,8 @@
unfolding int_and_def by (simp add: bin_rec_simps)
lemma int_and_x_simps':
- "w AND (Numeral.Pls BIT bit.B0) = Numeral.Pls"
- "w AND (Numeral.Min BIT bit.B1) = w"
+ "w AND (Int.Pls BIT bit.B0) = Int.Pls"
+ "w AND (Int.Min BIT bit.B1) = w"
apply (induct w rule: bin_induct)
apply simp_all[4]
apply (unfold int_and_Bits)
@@ -137,7 +137,7 @@
lemma bin_ops_same [simp]:
"(x::int) AND x = x"
"(x::int) OR x = x"
- "(x::int) XOR x = Numeral.Pls"
+ "(x::int) XOR x = Int.Pls"
by (induct x rule: bin_induct) auto
lemma int_not_not [simp]: "NOT (NOT (x::int)) = x"
@@ -268,7 +268,7 @@
done
lemma le_int_or:
- "!!x. bin_sign y = Numeral.Pls ==> x <= x OR y"
+ "!!x. bin_sign y = Int.Pls ==> x <= x OR y"
apply (induct y rule: bin_induct)
apply clarsimp
apply clarsimp
@@ -297,7 +297,7 @@
(* interaction between bit-wise and arithmetic *)
(* good example of bin_induction *)
-lemma bin_add_not: "x + NOT x = Numeral.Min"
+lemma bin_add_not: "x + NOT x = Int.Min"
apply (induct x rule: bin_induct)
apply clarsimp
apply clarsimp
@@ -428,10 +428,10 @@
apply (simp_all split: bit.split)
done
-lemma bin_sc_FP [simp]: "bin_sc n bit.B0 Numeral.Pls = Numeral.Pls"
+lemma bin_sc_FP [simp]: "bin_sc n bit.B0 Int.Pls = Int.Pls"
by (induct n) auto
-lemma bin_sc_TM [simp]: "bin_sc n bit.B1 Numeral.Min = Numeral.Min"
+lemma bin_sc_TM [simp]: "bin_sc n bit.B1 Int.Min = Int.Min"
by (induct n) auto
lemmas bin_sc_simps = bin_sc.Z bin_sc.Suc bin_sc_TM bin_sc_FP
@@ -468,7 +468,7 @@
defs
bin_to_bl_def : "bin_to_bl n w == bin_to_bl_aux n w []"
- bl_to_bin_def : "bl_to_bin bs == bl_to_bin_aux Numeral.Pls bs"
+ bl_to_bin_def : "bl_to_bin bs == bl_to_bin_aux Int.Pls bs"
primrec
Suc : "bl_of_nth (Suc n) f = f n # bl_of_nth n f"
@@ -512,7 +512,7 @@
in bin_rsplitl_aux (n, b # bs, (m - n, a)))"
defs
- bin_rcat_def : "bin_rcat n bs == foldl (%u v. bin_cat u n v) Numeral.Pls bs"
+ bin_rcat_def : "bin_rcat n bs == foldl (%u v. bin_cat u n v) Int.Pls bs"
bin_rsplit_def : "bin_rsplit n w == bin_rsplit_aux (n, [], w)"
bin_rsplitl_def : "bin_rsplitl n w == bin_rsplitl_aux (n, [], w)"
@@ -559,7 +559,7 @@
done
lemma bin_cat_Pls [simp]:
- "!!w. bin_cat Numeral.Pls n w = bintrunc n w"
+ "!!w. bin_cat Int.Pls n w = bintrunc n w"
by (induct n) auto
lemma bintr_cat1:
@@ -591,11 +591,11 @@
by (induct n) auto
lemma bin_split_Pls [simp]:
- "bin_split n Numeral.Pls = (Numeral.Pls, Numeral.Pls)"
+ "bin_split n Int.Pls = (Int.Pls, Int.Pls)"
by (induct n) (auto simp: Let_def split: ls_splits)
lemma bin_split_Min [simp]:
- "bin_split n Numeral.Min = (Numeral.Min, bintrunc n Numeral.Min)"
+ "bin_split n Int.Min = (Int.Min, bintrunc n Int.Min)"
by (induct n) (auto simp: Let_def split: ls_splits)
lemma bin_split_trunc:
--- a/src/HOL/Word/Num_Lemmas.thy Tue Jan 15 16:19:21 2008 +0100
+++ b/src/HOL/Word/Num_Lemmas.thy Tue Jan 15 16:19:23 2008 +0100
@@ -50,7 +50,7 @@
lemmas xtr8 = xtrans(8)
lemma Min_ne_Pls [iff]:
- "Numeral.Min ~= Numeral.Pls"
+ "Int.Min ~= Int.Pls"
unfolding Min_def Pls_def by auto
lemmas Pls_ne_Min [iff] = Min_ne_Pls [symmetric]
@@ -72,7 +72,7 @@
lemma nobm1:
"0 < (number_of w :: nat) ==>
- number_of w - (1 :: nat) = number_of (Numeral.pred w)"
+ number_of w - (1 :: nat) = number_of (Int.pred w)"
apply (unfold nat_number_of_def One_nat_def nat_1 [symmetric] pred_def)
apply (simp add: number_of_eq nat_diff_distrib [symmetric])
done
@@ -201,7 +201,7 @@
Pls_0_eq Min_1_eq refl
lemma bin_abs_lem:
- "bin = (w BIT b) ==> ~ bin = Numeral.Min --> ~ bin = Numeral.Pls -->
+ "bin = (w BIT b) ==> ~ bin = Int.Min --> ~ bin = Int.Pls -->
nat (abs w) < nat (abs bin)"
apply (clarsimp simp add: bin_rl_char)
apply (unfold Pls_def Min_def Bit_def)
@@ -211,8 +211,8 @@
done
lemma bin_induct:
- assumes PPls: "P Numeral.Pls"
- and PMin: "P Numeral.Min"
+ assumes PPls: "P Int.Pls"
+ and PMin: "P Int.Min"
and PBit: "!!bin bit. P bin ==> P (bin BIT bit)"
shows "P bin"
apply (rule_tac P=P and a=bin and f1="nat o abs"
--- a/src/HOL/Word/WordArith.thy Tue Jan 15 16:19:21 2008 +0100
+++ b/src/HOL/Word/WordArith.thy Tue Jan 15 16:19:23 2008 +0100
@@ -61,17 +61,17 @@
lemmas word_0_wi_Pls = word_0_wi [folded Pls_def]
lemmas word_0_no = word_0_wi_Pls [folded word_no_wi]
-lemma int_one_bin: "(1 :: int) == (Numeral.Pls BIT bit.B1)"
+lemma int_one_bin: "(1 :: int) == (Int.Pls BIT bit.B1)"
unfolding Pls_def Bit_def by auto
lemma word_1_no:
- "(1 :: 'a :: len0 word) == number_of (Numeral.Pls BIT bit.B1)"
+ "(1 :: 'a :: len0 word) == number_of (Int.Pls BIT bit.B1)"
unfolding word_1_wi word_number_of_def int_one_bin by auto
lemma word_m1_wi: "-1 == word_of_int -1"
by (rule word_number_of_alt)
-lemma word_m1_wi_Min: "-1 = word_of_int Numeral.Min"
+lemma word_m1_wi_Min: "-1 = word_of_int Int.Min"
by (simp add: word_m1_wi number_of_eq)
lemma word_0_bl: "of_bl [] = 0"
@@ -169,8 +169,8 @@
wi_hom_add: "word_of_int a + word_of_int b = word_of_int (a + b)" and
wi_hom_mult: "word_of_int a * word_of_int b = word_of_int (a * b)" and
wi_hom_neg: "- word_of_int a = word_of_int (- a)" and
- wi_hom_succ: "word_succ (word_of_int a) = word_of_int (Numeral.succ a)" and
- wi_hom_pred: "word_pred (word_of_int a) = word_of_int (Numeral.pred a)"
+ wi_hom_succ: "word_succ (word_of_int a) = word_of_int (Int.succ a)" and
+ wi_hom_pred: "word_pred (word_of_int a) = word_of_int (Int.pred a)"
by (auto simp: word_arith_wis arths)
lemmas wi_hom_syms = wi_homs [symmetric]
@@ -255,15 +255,15 @@
unfolding word_pred_def number_of_eq
by (simp add : pred_def word_no_wi)
-lemma word_pred_0_Min: "word_pred 0 = word_of_int Numeral.Min"
+lemma word_pred_0_Min: "word_pred 0 = word_of_int Int.Min"
by (simp add: word_pred_0_n1 number_of_eq)
-lemma word_m1_Min: "- 1 = word_of_int Numeral.Min"
+lemma word_m1_Min: "- 1 = word_of_int Int.Min"
unfolding Min_def by (simp only: word_of_int_hom_syms)
lemma succ_pred_no [simp]:
- "word_succ (number_of bin) = number_of (Numeral.succ bin) &
- word_pred (number_of bin) = number_of (Numeral.pred bin)"
+ "word_succ (number_of bin) = number_of (Int.succ bin) &
+ word_pred (number_of bin) = number_of (Int.pred bin)"
unfolding word_number_of_def by (simp add : new_word_of_int_homs)
lemma word_sp_01 [simp] :
@@ -797,7 +797,7 @@
which requires word length >= 1, ie 'a :: len word *)
lemma zero_bintrunc:
"iszero (number_of x :: 'a :: len word) =
- (bintrunc (len_of TYPE('a)) x = Numeral.Pls)"
+ (bintrunc (len_of TYPE('a)) x = Int.Pls)"
apply (unfold iszero_def word_0_wi word_no_wi)
apply (rule word_ubin.norm_eq_iff [symmetric, THEN trans])
apply (simp add : Pls_def [symmetric])
--- a/src/HOL/Word/WordDefinition.thy Tue Jan 15 16:19:21 2008 +0100
+++ b/src/HOL/Word/WordDefinition.thy Tue Jan 15 16:19:23 2008 +0100
@@ -160,12 +160,12 @@
definition
word_succ :: "'a :: len0 word => 'a word"
where
- "word_succ a = word_of_int (Numeral.succ (uint a))"
+ "word_succ a = word_of_int (Int.succ (uint a))"
definition
word_pred :: "'a :: len0 word => 'a word"
where
- "word_pred a = word_of_int (Numeral.pred (uint a))"
+ "word_pred a = word_of_int (Int.pred (uint a))"
constdefs
udvd :: "'a::len word => 'a::len word => bool" (infixl "udvd" 50)
@@ -195,7 +195,7 @@
"lsb (a::'a::len0 word) == bin_last (uint a) = bit.B1"
word_msb_def:
- "msb (a::'a::len word) == bin_sign (sint a) = Numeral.Min"
+ "msb (a::'a::len word) == bin_sign (sint a) = Int.Min"
constdefs
@@ -475,7 +475,7 @@
lemmas sint_lt = sint_lem [THEN conjunct2, standard]
lemma sign_uint_Pls [simp]:
- "bin_sign (uint x) = Numeral.Pls"
+ "bin_sign (uint x) = Int.Pls"
by (simp add: sign_Pls_ge_0 number_of_eq)
lemmas uint_m2p_neg = iffD2 [OF diff_less_0_iff_less uint_lt2p, standard]
@@ -498,7 +498,7 @@
by (simp only: int_word_uint)
lemma unat_number_of:
- "bin_sign b = Numeral.Pls ==>
+ "bin_sign b = Int.Pls ==>
unat (number_of b::'a::len0 word) = number_of b mod 2 ^ len_of TYPE ('a)"
apply (unfold unat_def)
apply (clarsimp simp only: uint_number_of)
@@ -643,7 +643,7 @@
length_bl_gt_0 [THEN length_greater_0_conv [THEN iffD1], standard]
lemmas length_bl_neq_0 [iff] = length_bl_gt_0 [THEN gr_implies_not0]
-lemma hd_bl_sign_sint: "hd (to_bl w) = (bin_sign (sint w) = Numeral.Min)"
+lemma hd_bl_sign_sint: "hd (to_bl w) = (bin_sign (sint w) = Int.Min)"
apply (unfold to_bl_def sint_uint)
apply (rule trans [OF _ bl_sbin_sign])
apply simp
--- a/src/HOL/Word/WordShift.thy Tue Jan 15 16:19:21 2008 +0100
+++ b/src/HOL/Word/WordShift.thy Tue Jan 15 16:19:23 2008 +0100
@@ -483,7 +483,7 @@
lemma mask_bl: "mask n = of_bl (replicate n True)"
by (auto simp add : test_bit_of_bl word_size intro: word_eqI)
-lemma mask_bin: "mask n = number_of (bintrunc n Numeral.Min)"
+lemma mask_bin: "mask n = number_of (bintrunc n Int.Min)"
by (auto simp add: nth_bintr word_size intro: word_eqI)
lemma and_mask_bintr: "w AND mask n = number_of (bintrunc n (uint w))"
--- a/src/HOL/ex/SVC_Oracle.thy Tue Jan 15 16:19:21 2008 +0100
+++ b/src/HOL/ex/SVC_Oracle.thy Tue Jan 15 16:19:23 2008 +0100
@@ -64,7 +64,7 @@
(*abstraction of a numeric literal*)
fun lit (t as Const(@{const_name HOL.zero}, _)) = t
| lit (t as Const(@{const_name HOL.one}, _)) = t
- | lit (t as Const(@{const_name Numeral.number_of}, _) $ w) = t
+ | lit (t as Const(@{const_name Int.number_of}, _) $ w) = t
| lit t = replace t
(*abstraction of a real/rational expression*)
fun rat ((c as Const(@{const_name HOL.plus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
--- a/src/HOL/hologic.ML Tue Jan 15 16:19:21 2008 +0100
+++ b/src/HOL/hologic.ML Tue Jan 15 16:19:23 2008 +0100
@@ -448,27 +448,27 @@
(* bit *)
-val bitT = Type ("Numeral.bit", []);
+val bitT = Type ("Int.bit", []);
-val B0_const = Const ("Numeral.bit.B0", bitT);
-val B1_const = Const ("Numeral.bit.B1", bitT);
+val B0_const = Const ("Int.bit.B0", bitT);
+val B1_const = Const ("Int.bit.B1", bitT);
fun mk_bit 0 = B0_const
| mk_bit 1 = B1_const
| mk_bit _ = raise TERM ("mk_bit", []);
-fun dest_bit (Const ("Numeral.bit.B0", _)) = 0
- | dest_bit (Const ("Numeral.bit.B1", _)) = 1
+fun dest_bit (Const ("Int.bit.B0", _)) = 0
+ | dest_bit (Const ("Int.bit.B1", _)) = 1
| dest_bit t = raise TERM ("dest_bit", [t]);
(* binary numerals and int -- non-unique representation due to leading zeros/ones! *)
-val intT = Type ("IntDef.int", []);
+val intT = Type ("Int.int", []);
-val pls_const = Const ("Numeral.Pls", intT)
-and min_const = Const ("Numeral.Min", intT)
-and bit_const = Const ("Numeral.Bit", intT --> bitT --> intT);
+val pls_const = Const ("Int.Pls", intT)
+and min_const = Const ("Int.Min", intT)
+and bit_const = Const ("Int.Bit", intT --> bitT --> intT);
fun mk_numeral 0 = pls_const
| mk_numeral ~1 = min_const
@@ -476,14 +476,14 @@
let val (q, r) = Integer.div_mod i 2;
in bit_const $ mk_numeral q $ mk_bit r end;
-fun dest_numeral (Const ("Numeral.Pls", _)) = 0
- | dest_numeral (Const ("Numeral.Min", _)) = ~1
- | dest_numeral (Const ("Numeral.Bit", _) $ bs $ b) = 2 * dest_numeral bs + dest_bit b
+fun dest_numeral (Const ("Int.Pls", _)) = 0
+ | dest_numeral (Const ("Int.Min", _)) = ~1
+ | dest_numeral (Const ("Int.Bit", _) $ bs $ b) = 2 * dest_numeral bs + dest_bit b
| dest_numeral t = raise TERM ("dest_numeral", [t]);
-fun number_of_const T = Const ("Numeral.number_class.number_of", intT --> T);
+fun number_of_const T = Const ("Int.number_class.number_of", intT --> T);
-fun add_numerals (Const ("Numeral.number_class.number_of", Type (_, [_, T])) $ t) = cons (t, T)
+fun add_numerals (Const ("Int.number_class.number_of", Type (_, [_, T])) $ t) = cons (t, T)
| add_numerals (t $ u) = add_numerals t #> add_numerals u
| add_numerals (Abs (_, _, t)) = add_numerals t
| add_numerals _ = I;
@@ -494,7 +494,7 @@
fun dest_number (Const ("HOL.zero_class.zero", T)) = (T, 0)
| dest_number (Const ("HOL.one_class.one", T)) = (T, 1)
- | dest_number (Const ("Numeral.number_class.number_of", Type ("fun", [_, T])) $ t) =
+ | dest_number (Const ("Int.number_class.number_of", Type ("fun", [_, T])) $ t) =
(T, dest_numeral t)
| dest_number t = raise TERM ("dest_number", [t]);
--- a/src/HOL/int_arith1.ML Tue Jan 15 16:19:21 2008 +0100
+++ b/src/HOL/int_arith1.ML Tue Jan 15 16:19:23 2008 +0100
@@ -18,7 +18,7 @@
fun prep_simproc (name, pats, proc) =
Simplifier.simproc (the_context()) name pats proc;
- fun is_numeral (Const(@{const_name Numeral.number_of}, _) $ w) = true
+ fun is_numeral (Const(@{const_name Int.number_of}, _) $ w) = true
| is_numeral _ = false
fun simplify_meta_eq f_number_of_eq f_eq =
@@ -30,16 +30,16 @@
val meta_number_of_reorient = @{thm number_of_reorient} RS eq_reflection
(*reorientation simplification procedure: reorients (polymorphic)
- 0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*)
+ 0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a Int.*)
fun reorient_proc sg _ (_ $ t $ u) =
case u of
Const(@{const_name HOL.zero}, _) => NONE
| Const(@{const_name HOL.one}, _) => NONE
- | Const(@{const_name Numeral.number_of}, _) $ _ => NONE
+ | Const(@{const_name Int.number_of}, _) $ _ => NONE
| _ => SOME (case t of
Const(@{const_name HOL.zero}, _) => meta_zero_reorient
| Const(@{const_name HOL.one}, _) => meta_one_reorient
- | Const(@{const_name Numeral.number_of}, _) $ _ => meta_number_of_reorient)
+ | Const(@{const_name Int.number_of}, _) $ _ => meta_number_of_reorient)
val reorient_simproc =
prep_simproc ("reorient_simproc", ["0=x", "1=x", "number_of w = x"], reorient_proc)
@@ -73,10 +73,10 @@
fun numterm_ord (Abs (_, T, t), Abs(_, U, u)) =
(case numterm_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
| numterm_ord
- (Const(@{const_name Numeral.number_of}, _) $ v, Const(@{const_name Numeral.number_of}, _) $ w) =
+ (Const(@{const_name Int.number_of}, _) $ v, Const(@{const_name Int.number_of}, _) $ w) =
num_ord (HOLogic.dest_numeral v, HOLogic.dest_numeral w)
- | numterm_ord (Const(@{const_name Numeral.number_of}, _) $ _, _) = LESS
- | numterm_ord (_, Const(@{const_name Numeral.number_of}, _) $ _) = GREATER
+ | numterm_ord (Const(@{const_name Int.number_of}, _) $ _, _) = LESS
+ | numterm_ord (_, Const(@{const_name Int.number_of}, _) $ _) = GREATER
| numterm_ord (t, u) =
(case int_ord (size_of_term t, size_of_term u) of
EQUAL =>
@@ -575,7 +575,7 @@
addsimprocs Int_Numeral_Base_Simprocs
addcongs [if_weak_cong]}) #>
arith_inj_const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) #>
- arith_discrete "IntDef.int"
+ arith_discrete @{type_name Int.int}
end;
--- a/src/HOL/nat_simprocs.ML Tue Jan 15 16:19:21 2008 +0100
+++ b/src/HOL/nat_simprocs.ML Tue Jan 15 16:19:23 2008 +0100
@@ -105,7 +105,7 @@
handle TERM _ => (k, t::ts);
(*Code for testing whether numerals are already used in the goal*)
-fun is_numeral (Const(@{const_name Numeral.number_of}, _) $ w) = true
+fun is_numeral (Const(@{const_name Int.number_of}, _) $ w) = true
| is_numeral _ = false;
fun prod_has_numeral t = exists is_numeral (dest_prod t);
--- a/src/Provers/Arith/assoc_fold.ML Tue Jan 15 16:19:21 2008 +0100
+++ b/src/Provers/Arith/assoc_fold.ML Tue Jan 15 16:19:23 2008 +0100
@@ -30,7 +30,7 @@
(*Separate the literals from the other terms being combined*)
fun sift_terms plus (t, (lits,others)) =
(case t of
- Const (@{const_name Numeral.number_of}, _) $ _ => (* FIXME logic dependent *)
+ Const (@{const_name Int.number_of}, _) $ _ => (* FIXME logic dependent *)
(t::lits, others) (*new literal*)
| (f as Const _) $ x $ y =>
if f = plus