--- a/NEWS Wed Sep 06 10:01:27 2006 +0200
+++ b/NEWS Wed Sep 06 13:48:02 2006 +0200
@@ -465,6 +465,20 @@
*** HOL ***
+* Numeral syntax: type 'bin' which was a mere type copy of 'int' has been
+abandoned in favour of plain 'int'. Significant changes for setting up numeral
+syntax for types:
+
+ - new constants Numeral.pred and Numeral.succ instead
+ of former Numeral.bin_pred and Numeral.bin_succ.
+ - Use integer operations instead of bin_add, bin_mult and so on.
+ - Numeral simplification theorems named Numeral.numeral_simps instead of Bin_simps.
+ - ML structure Bin_Simprocs now named Int_Numeral_Base_Simprocs.
+
+See HOL/Integ/IntArith.thy for an example setup.
+
+INCOMPATIBILITY.
+
* New top level command 'normal_form' computes the normal form of a term
that may contain free variables. For example 'normal_form "rev[a,b,c]"'
prints '[b,c,a]'. This command is suitable for heavy-duty computations
--- a/src/HOL/Complex/Complex.thy Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Complex/Complex.thy Wed Sep 06 13:48:02 2006 +0200
@@ -830,7 +830,7 @@
instance complex :: number ..
defs (overloaded)
- complex_number_of_def: "(number_of w :: complex) == of_int (Rep_Bin w)"
+ complex_number_of_def: "(number_of w :: complex) == of_int w"
--{*the type constraint is essential!*}
instance complex :: number_ring
--- a/src/HOL/Complex/NSComplex.thy Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Complex/NSComplex.thy Wed Sep 06 13:48:02 2006 +0200
@@ -783,7 +783,7 @@
subsection{*Numerals and Arithmetic*}
-lemma hcomplex_number_of_def: "(number_of w :: hcomplex) == of_int (Rep_Bin w)"
+lemma hcomplex_number_of_def: "(number_of w :: hcomplex) == of_int w"
by (transfer, rule number_of_eq [THEN eq_reflection])
lemma hcomplex_of_hypreal_eq_hcomplex_of_complex:
--- a/src/HOL/Hyperreal/NSA.thy Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Hyperreal/NSA.thy Wed Sep 06 13:48:02 2006 +0200
@@ -547,7 +547,7 @@
in
val approx_reorient_simproc =
- Bin_Simprocs.prep_simproc
+ Int_Numeral_Base_Simprocs.prep_simproc
("reorient_simproc", ["0@=x", "1@=x", "number_of w @= x"], reorient_proc);
end;
--- a/src/HOL/Import/HOL/HOL4Prob.thy Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Import/HOL/HOL4Prob.thy Wed Sep 06 13:48:02 2006 +0200
@@ -35,28 +35,28 @@
lemma DIV_TWO_BASIC: "(op &::bool => bool => bool)
((op =::nat => nat => bool)
((op div::nat => nat => nat) (0::nat)
- ((number_of::bin => nat)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::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))
(bit.B0::bit))))
(0::nat))
((op &::bool => bool => bool)
((op =::nat => nat => bool)
((op div::nat => nat => nat) (1::nat)
- ((number_of::bin => nat)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::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))
(bit.B0::bit))))
(0::nat))
((op =::nat => nat => bool)
((op div::nat => nat => nat)
- ((number_of::bin => nat)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::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))
(bit.B0::bit)))
- ((number_of::bin => nat)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::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))
(bit.B0::bit))))
(1::nat)))"
by (import prob_extra DIV_TWO_BASIC)
@@ -75,19 +75,19 @@
(op =::nat => nat => bool)
((op div::nat => nat => nat)
((op ^::nat => nat => nat)
- ((number_of::bin => nat)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::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))
(bit.B0::bit)))
((Suc::nat => nat) n))
- ((number_of::bin => nat)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::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))
(bit.B0::bit))))
((op ^::nat => nat => nat)
- ((number_of::bin => nat)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::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))
(bit.B0::bit)))
n))"
by (import prob_extra EXP_DIV_TWO)
@@ -125,22 +125,22 @@
lemma HALF_POS: "(op <::real => real => bool) (0::real)
((op /::real => real => real) (1::real)
- ((number_of::bin => real)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+ ((number_of \<Colon> int => real)
+ ((op BIT \<Colon> int => bit => int)
+ ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
(bit.B0::bit))))"
by (import prob_extra HALF_POS)
lemma HALF_CANCEL: "(op =::real => real => bool)
((op *::real => real => real)
- ((number_of::bin => real)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+ ((number_of \<Colon> int => real)
+ ((op BIT \<Colon> int => bit => int)
+ ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
(bit.B0::bit)))
((op /::real => real => real) (1::real)
- ((number_of::bin => real)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+ ((number_of \<Colon> int => real)
+ ((op BIT \<Colon> int => bit => int)
+ ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
(bit.B0::bit)))))
(1::real)"
by (import prob_extra HALF_CANCEL)
@@ -150,9 +150,9 @@
(op <::real => real => bool) (0::real)
((op ^::real => nat => real)
((op /::real => real => real) (1::real)
- ((number_of::bin => real)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+ ((number_of \<Colon> int => real)
+ ((op BIT \<Colon> int => bit => int)
+ ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
(bit.B0::bit))))
n))"
by (import prob_extra POW_HALF_POS)
@@ -165,17 +165,17 @@
((op <=::real => real => bool)
((op ^::real => nat => real)
((op /::real => real => real) (1::real)
- ((number_of::bin => real)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ ((number_of \<Colon> int => real)
+ ((op BIT \<Colon> int => bit => int)
+ ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
(bit.B1::bit))
(bit.B0::bit))))
n)
((op ^::real => nat => real)
((op /::real => real => real) (1::real)
- ((number_of::bin => real)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ ((number_of \<Colon> int => real)
+ ((op BIT \<Colon> int => bit => int)
+ ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
(bit.B1::bit))
(bit.B0::bit))))
m))))"
@@ -186,21 +186,21 @@
(op =::real => real => bool)
((op ^::real => nat => real)
((op /::real => real => real) (1::real)
- ((number_of::bin => real)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+ ((number_of \<Colon> int => real)
+ ((op BIT \<Colon> int => bit => int)
+ ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
(bit.B0::bit))))
n)
((op *::real => real => real)
- ((number_of::bin => real)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+ ((number_of \<Colon> int => real)
+ ((op BIT \<Colon> int => bit => int)
+ ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
(bit.B0::bit)))
((op ^::real => nat => real)
((op /::real => real => real) (1::real)
- ((number_of::bin => real)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ ((number_of \<Colon> int => real)
+ ((op BIT \<Colon> int => bit => int)
+ ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
(bit.B1::bit))
(bit.B0::bit))))
((Suc::nat => nat) n))))"
@@ -227,22 +227,22 @@
lemma ONE_MINUS_HALF: "(op =::real => real => bool)
((op -::real => real => real) (1::real)
((op /::real => real => real) (1::real)
- ((number_of::bin => real)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+ ((number_of \<Colon> int => real)
+ ((op BIT \<Colon> int => bit => int)
+ ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
(bit.B0::bit)))))
((op /::real => real => real) (1::real)
- ((number_of::bin => real)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+ ((number_of \<Colon> int => real)
+ ((op BIT \<Colon> int => bit => int)
+ ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
(bit.B0::bit))))"
by (import prob_extra ONE_MINUS_HALF)
lemma HALF_LT_1: "(op <::real => real => bool)
((op /::real => real => real) (1::real)
- ((number_of::bin => real)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+ ((number_of \<Colon> int => real)
+ ((op BIT \<Colon> int => bit => int)
+ ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
(bit.B0::bit))))
(1::real)"
by (import prob_extra HALF_LT_1)
@@ -252,17 +252,17 @@
(op =::real => real => bool)
((op ^::real => nat => real)
((op /::real => real => real) (1::real)
- ((number_of::bin => real)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+ ((number_of \<Colon> int => real)
+ ((op BIT \<Colon> int => bit => int)
+ ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
(bit.B0::bit))))
n)
((inverse::real => real)
((real::nat => real)
((op ^::nat => nat => nat)
- ((number_of::bin => nat)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ ((number_of \<Colon> int => nat)
+ ((op BIT \<Colon> int => bit => int)
+ ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
(bit.B1::bit))
(bit.B0::bit)))
n))))"
@@ -1405,27 +1405,27 @@
((op +::real => real => real)
((op ^::real => nat => real)
((op /::real => real => real) (1::real)
- ((number_of::bin => real)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ ((number_of \<Colon> int => real)
+ ((op BIT \<Colon> int => bit => int)
+ ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
(bit.B1::bit))
(bit.B0::bit))))
((size::bool list => nat)
((SNOC::bool => bool list => bool list) (True::bool) l)))
((op ^::real => nat => real)
((op /::real => real => real) (1::real)
- ((number_of::bin => real)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ ((number_of \<Colon> int => real)
+ ((op BIT \<Colon> int => bit => int)
+ ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
(bit.B1::bit))
(bit.B0::bit))))
((size::bool list => nat)
((SNOC::bool => bool list => bool list) (False::bool) l))))
((op ^::real => nat => real)
((op /::real => real => real) (1::real)
- ((number_of::bin => real)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+ ((number_of \<Colon> int => real)
+ ((op BIT \<Colon> int => bit => int)
+ ((op BIT \<Colon> int => bit => int) (Numeral.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 Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Import/HOL/HOL4Real.thy Wed Sep 06 13:48:02 2006 +0200
@@ -525,9 +525,9 @@
((op <=::real => real => bool) (1::real) x)
((op <=::real => real => bool) (1::real)
((op ^::real => nat => real) x
- ((number_of::bin => nat)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::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))
(bit.B0::bit))))))"
by (import real REAL_LE1_POW2)
@@ -537,9 +537,9 @@
((op <::real => real => bool) (1::real) x)
((op <::real => real => bool) (1::real)
((op ^::real => nat => real) x
- ((number_of::bin => nat)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::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))
(bit.B0::bit))))))"
by (import real REAL_LT1_POW2)
--- a/src/HOL/Import/HOL/HOL4Vec.thy Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Import/HOL/HOL4Vec.thy Wed Sep 06 13:48:02 2006 +0200
@@ -1282,9 +1282,9 @@
(%x::nat.
(op -->::bool => bool => bool)
((op <::nat => nat => bool) x
- ((number_of::bin => nat)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::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))
(bit.B0::bit))))
((op =::nat => nat => bool) ((BV::bool => nat) ((VB::nat => bool) x))
x))"
@@ -1499,10 +1499,10 @@
k (0::nat) w2)))
((BV::bool => nat) cin))
((op ^::nat => nat => nat)
- ((number_of::bin => nat)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin)
- (Numeral.Pls::bin) (bit.B1::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))
(bit.B0::bit)))
k)))))))"
by (import bword_arith ACARRY_EQ_ADD_DIV)
--- a/src/HOL/Import/HOL/HOL4Word32.thy Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Import/HOL/HOL4Word32.thy Wed Sep 06 13:48:02 2006 +0200
@@ -116,9 +116,9 @@
(%n::nat.
(op <::nat => nat => bool) (0::nat)
((op ^::nat => nat => nat)
- ((number_of::bin => nat)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::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))
(bit.B0::bit)))
n))"
by (import bits ZERO_LT_TWOEXP)
@@ -136,16 +136,16 @@
(op -->::bool => bool => bool) ((op <::nat => nat => bool) a b)
((op <::nat => nat => bool)
((op ^::nat => nat => nat)
- ((number_of::bin => nat)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ ((number_of \<Colon> int => nat)
+ ((op BIT \<Colon> int => bit => int)
+ ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
(bit.B1::bit))
(bit.B0::bit)))
a)
((op ^::nat => nat => nat)
- ((number_of::bin => nat)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ ((number_of \<Colon> int => nat)
+ ((op BIT \<Colon> int => bit => int)
+ ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
(bit.B1::bit))
(bit.B0::bit)))
b))))"
@@ -158,16 +158,16 @@
(op -->::bool => bool => bool) ((op <=::nat => nat => bool) a b)
((op <=::nat => nat => bool)
((op ^::nat => nat => nat)
- ((number_of::bin => nat)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ ((number_of \<Colon> int => nat)
+ ((op BIT \<Colon> int => bit => int)
+ ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
(bit.B1::bit))
(bit.B0::bit)))
a)
((op ^::nat => nat => nat)
- ((number_of::bin => nat)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ ((number_of \<Colon> int => nat)
+ ((op BIT \<Colon> int => bit => int)
+ ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
(bit.B1::bit))
(bit.B0::bit)))
b))))"
@@ -179,16 +179,16 @@
(%b::nat.
(op <=::nat => nat => bool)
((op ^::nat => nat => nat)
- ((number_of::bin => nat)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ ((number_of \<Colon> int => nat)
+ ((op BIT \<Colon> int => bit => int)
+ ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
(bit.B1::bit))
(bit.B0::bit)))
((op -::nat => nat => nat) a b))
((op ^::nat => nat => nat)
- ((number_of::bin => nat)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ ((number_of \<Colon> int => nat)
+ ((op BIT \<Colon> int => bit => int)
+ ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
(bit.B1::bit))
(bit.B0::bit)))
a)))"
@@ -348,24 +348,24 @@
(%x::nat.
(op =::nat => nat => bool)
((op ^::nat => nat => nat)
- ((number_of::bin => nat)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ ((number_of \<Colon> int => nat)
+ ((op BIT \<Colon> int => bit => int)
+ ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
(bit.B1::bit))
(bit.B0::bit)))
b)
((op *::nat => nat => nat)
((op ^::nat => nat => nat)
- ((number_of::bin => nat)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ ((number_of \<Colon> int => nat)
+ ((op BIT \<Colon> int => bit => int)
+ ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
(bit.B1::bit))
(bit.B0::bit)))
((op +::nat => nat => nat) x (1::nat)))
((op ^::nat => nat => nat)
- ((number_of::bin => nat)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ ((number_of \<Colon> int => nat)
+ ((op BIT \<Colon> int => bit => int)
+ ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
(bit.B1::bit))
(bit.B0::bit)))
a))))))"
--- a/src/HOL/Integ/IntArith.thy Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Integ/IntArith.thy Wed Sep 06 13:48:02 2006 +0200
@@ -20,7 +20,7 @@
int :: number ..
defs (overloaded)
- int_number_of_def: "(number_of w :: int) == of_int (Rep_Bin w)"
+ int_number_of_def: "(number_of w :: int) == of_int w"
--{*the type constraint is essential!*}
instance int :: number_ring
@@ -365,12 +365,9 @@
subsection {* code generator setup *}
code_typename
- "Numeral.bin" "IntDef.bin"
"Numeral.bit" "IntDef.bit"
code_constname
- "Numeral.Abs_Bin" "IntDef.bin"
- "Numeral.Rep_Bin" "IntDef.int_of_bin"
"Numeral.Pls" "IntDef.pls"
"Numeral.Min" "IntDef.min"
"Numeral.Bit" "IntDef.bit"
@@ -387,36 +384,29 @@
lemma
Numeral_Bit_refl [code fun]: "Numeral.Bit = Numeral.Bit" ..
-lemma
- number_of_is_rep_bin [code inline]: "number_of = Rep_Bin"
-proof
- fix b
- show "number_of b = Rep_Bin b"
- unfolding int_number_of_def by simp
-qed
+lemma zero_is_num_zero [code fun, code inline]:
+ "(0::int) = Numeral.Pls"
+ unfolding Pls_def ..
-lemma zero_is_num_zero [code, code inline]:
- "(0::int) = Rep_Bin Numeral.Pls"
- unfolding Pls_def Abs_Bin_inverse' ..
+lemma one_is_num_one [code fun, code inline]:
+ "(1::int) = Numeral.Pls BIT bit.B1"
+ unfolding Pls_def Bit_def by simp
-lemma one_is_num_one [code, code inline]:
- "(1::int) = Rep_Bin (Numeral.Pls BIT bit.B1)"
- unfolding Pls_def Bit_def Abs_Bin_inverse' by simp
+lemma number_of_is_id [code fun, code inline]:
+ "number_of (k::int) = k"
+ unfolding int_number_of_def by simp
-lemma negate_bin_minus:
- "(Rep_Bin b :: int) = - Rep_Bin (bin_minus b)"
- unfolding bin_minus_def Abs_Bin_inverse' by simp
-
-lemmas [code inline] =
- bin_minus_Pls bin_minus_Min bin_minus_1 bin_minus_0
- bin_pred_Pls bin_pred_Min bin_pred_1 bin_pred_0
+lemma number_of_minus:
+ "number_of (b :: int) = (- number_of (- b) :: int)"
+ unfolding int_number_of_def by simp
ML {*
structure Numeral =
struct
-val negate_bin_minus_thm = eq_reflection OF [thm "negate_bin_minus"];
-val number_of_is_rep_bin_thm = eq_reflection OF [thm "number_of_is_rep_bin"];
+val number_of_minus_thm = eq_reflection OF [thm "number_of_minus"];
+val minus_rewrites = map (fn thm => eq_reflection OF [thm])
+ [minus_1, minus_0, minus_Pls, minus_Min, pred_1, pred_0, pred_Pls, pred_Min];
fun int_of_numeral thy num = HOLogic.dest_binum num
handle TERM _
@@ -424,7 +414,6 @@
fun elim_negate thy thms =
let
- val thms' = map (CodegenTheorems.rewrite_fun [number_of_is_rep_bin_thm]) thms;
fun bins_of (Const _) =
I
| bins_of (Var _) =
@@ -437,28 +426,32 @@
bins_of t
| bins_of (t as _ $ _) =
case strip_comb t
- of (Const ("Numeral.Rep_Bin", _), [bin]) => cons bin
+ of (Const ("Numeral.Bit", _), _) => cons t
| (t', ts) => bins_of t' #> fold bins_of ts;
- fun is_negative bin = case try HOLogic.dest_binum bin
+ fun is_negative num = case try HOLogic.dest_binum num
of SOME i => i < 0
| _ => false;
fun instantiate_with bin =
- Drule.instantiate' [] [(SOME o cterm_of thy) bin] negate_bin_minus_thm;
+ Drule.instantiate' [] [(SOME o cterm_of thy) bin] number_of_minus_thm;
val rewrites =
[]
- |> fold (bins_of o prop_of) thms'
+ |> fold (bins_of o prop_of) thms
|> filter is_negative
|> map instantiate_with
- in if null rewrites then thms' else
- map (CodegenTheorems.rewrite_fun rewrites) thms'
+ in if null rewrites then thms else
+ map (CodegenTheorems.rewrite_fun (rewrites @ minus_rewrites)) thms
end;
end;
*}
+code_const "Numeral.Pls" and "Numeral.Min"
+ (SML target_atom "(0 : IntInf.int)" and target_atom "(~1 : IntInf.int)")
+ (Haskell target_atom "0" and target_atom "(negate ~1)")
+
setup {*
CodegenTheorems.add_preproc Numeral.elim_negate
- #> CodegenPackage.add_appconst ("Numeral.Rep_Bin", CodegenPackage.appgen_rep_bin Numeral.int_of_numeral)
+ #> CodegenPackage.add_appconst ("Numeral.Bit", CodegenPackage.appgen_rep_bin Numeral.int_of_numeral)
*}
--- a/src/HOL/Integ/IntDef.thy Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Integ/IntDef.thy Wed Sep 06 13:48:02 2006 +0200
@@ -935,7 +935,7 @@
Type ("fun", [_, Type ("nat", [])])) $ bin) =
SOME (Codegen.invoke_codegen thy defs s thyname b (gr,
Const ("IntDef.nat", HOLogic.intT --> HOLogic.natT) $
- (Const ("Numeral.number_of", HOLogic.binT --> HOLogic.intT) $ bin)))
+ (Const ("Numeral.number_of", HOLogic.intT --> HOLogic.intT) $ bin)))
| number_of_codegen _ _ _ _ _ _ _ = NONE;
*}
--- a/src/HOL/Integ/IntDiv.thy Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Integ/IntDiv.thy Wed Sep 06 13:48:02 2006 +0200
@@ -9,7 +9,7 @@
header{*The Division Operators div and mod; the Divides Relation dvd*}
theory IntDiv
-imports SetInterval Recdef
+imports "../SetInterval" "../Recdef"
uses ("IntDiv_setup.ML")
begin
@@ -959,7 +959,7 @@
(if b=bit.B0 | (0::int) \<le> number_of w
then number_of v div (number_of w)
else (number_of v + (1::int)) div (number_of w))"
-apply (simp only: number_of_eq Bin_simps UNIV_I split: split_if)
+apply (simp only: number_of_eq numeral_simps UNIV_I split: split_if)
apply (simp add: zdiv_zmult_zmult1 pos_zdiv_mult_2 neg_zdiv_mult_2 add_ac
split: bit.split)
done
@@ -1001,7 +1001,7 @@
| bit.B1 => if (0::int) \<le> number_of w
then 2 * (number_of v mod number_of w) + 1
else 2 * ((number_of v + (1::int)) mod number_of w) - 1)"
-apply (simp only: number_of_eq Bin_simps UNIV_I split: bit.split)
+apply (simp only: number_of_eq numeral_simps UNIV_I split: bit.split)
apply (simp add: zmod_zmult_zmult1 pos_zmod_mult_2
not_0_le_lemma neg_zmod_mult_2 add_ac)
done
--- a/src/HOL/Integ/NatBin.thy Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Integ/NatBin.thy Wed Sep 06 13:48:02 2006 +0200
@@ -17,8 +17,7 @@
instance nat :: number ..
defs (overloaded)
- nat_number_of_def:
- "(number_of::bin => nat) v == nat ((number_of :: bin => int) v)"
+ nat_number_of_def: "number_of v == nat (number_of (v\<Colon>int))"
abbreviation (xsymbols)
square :: "'a::power => 'a" ("(_\<twosuperior>)" [1000] 999)
@@ -113,14 +112,14 @@
lemma Suc_nat_number_of_add:
"Suc (number_of v + n) =
- (if neg (number_of v :: int) then 1+n else number_of (bin_succ v) + n)"
+ (if neg (number_of v :: int) then 1+n else number_of (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 (bin_succ v))"
+ (if neg (number_of v :: int) then 1 else number_of (succ v))"
apply (cut_tac n = 0 in Suc_nat_number_of_add)
apply (simp cong del: if_weak_cong)
done
@@ -133,7 +132,7 @@
"(number_of v :: nat) + number_of v' =
(if neg (number_of v :: int) then number_of v'
else if neg (number_of v' :: int) then number_of v
- else number_of (bin_add v v'))"
+ else number_of (v + v'))"
by (force dest!: neg_nat
simp del: nat_number_of
simp add: nat_number_of_def nat_add_distrib [symmetric])
@@ -152,7 +151,7 @@
lemma diff_nat_number_of [simp]:
"(number_of v :: nat) - number_of v' =
(if neg (number_of v' :: int) then number_of v
- else let d = number_of (bin_add v (bin_minus v')) in
+ else let d = number_of (v + uminus v') in
if neg d then 0 else nat d)"
by (simp del: nat_number_of add: diff_nat_eq_if nat_number_of_def)
@@ -162,7 +161,7 @@
lemma mult_nat_number_of [simp]:
"(number_of v :: nat) * number_of v' =
- (if neg (number_of v :: int) then 0 else number_of (bin_mult v v'))"
+ (if neg (number_of v :: int) then 0 else number_of (v * v'))"
by (force dest!: neg_nat
simp del: nat_number_of
simp add: nat_number_of_def nat_mult_distrib [symmetric])
@@ -246,7 +245,7 @@
"((number_of v :: nat) = number_of v') =
(if neg (number_of v :: int) then (iszero (number_of v' :: int) | neg (number_of v' :: int))
else if neg (number_of v' :: int) then iszero (number_of v :: int)
- else iszero (number_of (bin_add v (bin_minus v')) :: int))"
+ else iszero (number_of (v + uminus v') :: int))"
apply (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def
eq_nat_nat_iff eq_number_of_eq nat_0 iszero_def
split add: split_if cong add: imp_cong)
@@ -260,13 +259,11 @@
(*"neg" is used in rewrite rules for binary comparisons*)
lemma less_nat_number_of [simp]:
"((number_of v :: nat) < number_of v') =
- (if neg (number_of v :: int) then neg (number_of (bin_minus v') :: int)
- else neg (number_of (bin_add v (bin_minus v')) :: int))"
+ (if neg (number_of v :: int) then neg (number_of (uminus v') :: int)
+ else neg (number_of (v + uminus v') :: int))"
by (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def
nat_less_eq_zless less_number_of_eq_neg zless_nat_eq_int_zless
- cong add: imp_cong, simp)
-
-
+ cong add: imp_cong, simp add: Pls_def)
(*Maps #n to n for n = 0, 1, 2*)
@@ -437,8 +434,8 @@
by (rule trans [OF eq_sym_conv eq_number_of_0])
lemma less_0_number_of [simp]:
- "((0::nat) < number_of v) = neg (number_of (bin_minus v) :: int)"
-by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric])
+ "((0::nat) < number_of v) = neg (number_of (uminus v) :: int)"
+by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric] Pls_def)
lemma neg_imp_number_of_eq_0: "neg (number_of v :: int) ==> number_of v = (0::nat)"
@@ -450,7 +447,7 @@
lemma eq_number_of_Suc [simp]:
"(number_of v = Suc n) =
- (let pv = number_of (bin_pred v) in
+ (let pv = number_of (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
@@ -461,13 +458,13 @@
lemma Suc_eq_number_of [simp]:
"(Suc n = number_of v) =
- (let pv = number_of (bin_pred v) in
+ (let pv = number_of (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 (bin_pred v) in
+ (let pv = number_of (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
@@ -478,7 +475,7 @@
lemma less_Suc_number_of [simp]:
"(Suc n < number_of v) =
- (let pv = number_of (bin_pred v) in
+ (let pv = number_of (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
@@ -489,13 +486,13 @@
lemma le_number_of_Suc [simp]:
"(number_of v <= Suc n) =
- (let pv = number_of (bin_pred v) in
+ (let pv = number_of (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 (bin_pred v) in
+ (let pv = number_of (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])
@@ -568,23 +565,20 @@
text{*For the integers*}
lemma zpower_number_of_even:
- "(z::int) ^ number_of (w BIT bit.B0) =
- (let w = z ^ (number_of w) in w*w)"
-apply (simp del: nat_number_of add: nat_number_of_def number_of_BIT Let_def)
-apply (simp only: number_of_add)
+ "(z::int) ^ number_of (w BIT bit.B0) = (let w = z ^ (number_of w) in w * w)"
+unfolding Let_def nat_number_of_def number_of_BIT bit.cases
apply (rule_tac x = "number_of w" in spec, clarify)
apply (case_tac " (0::int) <= x")
apply (auto simp add: nat_mult_distrib power_even_eq power2_eq_square)
done
lemma zpower_number_of_odd:
- "(z::int) ^ number_of (w BIT bit.B1) =
- (if (0::int) <= number_of w
- then (let w = z ^ (number_of w) in z*w*w)
- else 1)"
-apply (simp del: nat_number_of add: nat_number_of_def number_of_BIT Let_def)
-apply (simp only: number_of_add nat_numeral_1_eq_1 not_neg_eq_ge_0 neg_eq_less_0)
-apply (rule_tac x = "number_of w" in spec, clarify)
+ "(z::int) ^ number_of (w BIT bit.B1) = (if (0::int) <= number_of w
+ then (let w = z ^ (number_of w) in z * w * w) else 1)"
+unfolding Let_def nat_number_of_def number_of_BIT bit.cases
+apply (rule_tac x = "number_of w" in spec, auto)
+apply (simp only: nat_add_distrib nat_mult_distrib)
+apply simp
apply (auto simp add: nat_add_distrib nat_mult_distrib power_even_eq power2_eq_square neg_nat)
done
@@ -695,13 +689,13 @@
"number_of v + (number_of v' + (k::nat)) =
(if neg (number_of v :: int) then number_of v' + k
else if neg (number_of v' :: int) then number_of v + k
- else number_of (bin_add v v') + k)"
+ else number_of (v + v') + k)"
by simp
lemma nat_number_of_mult_left:
"number_of v * (number_of v' * (k::nat)) =
(if neg (number_of v :: int) then 0
- else number_of (bin_mult v v') * k)"
+ else number_of (v * v') * k)"
by simp
@@ -780,7 +774,7 @@
subsection {* code generator setup *}
lemma number_of_is_nat_rep_bin [code inline]:
- "(number_of b :: nat) = nat (Rep_Bin b)"
+ "(number_of b :: nat) = nat (number_of b)"
unfolding nat_number_of_def int_number_of_def by simp
--- a/src/HOL/Integ/NatSimprocs.thy Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Integ/NatSimprocs.thy Wed Sep 06 13:48:02 2006 +0200
@@ -22,9 +22,9 @@
text {*Now just instantiating @{text n} to @{text "number_of v"} does
the right simplification, but with some redundant inequality
tests.*}
-lemma neg_number_of_bin_pred_iff_0:
- "neg (number_of (bin_pred v)::int) = (number_of v = (0::nat))"
-apply (subgoal_tac "neg (number_of (bin_pred v)) = (number_of v < Suc 0) ")
+lemma neg_number_of_pred_iff_0:
+ "neg (number_of (pred v)::int) = (number_of v = (0::nat))"
+apply (subgoal_tac "neg (number_of (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
@@ -32,13 +32,13 @@
text{*No longer required as a simprule because of the @{text inverse_fold}
simproc*}
lemma Suc_diff_number_of:
- "neg (number_of (bin_minus v)::int) ==>
- Suc m - (number_of v) = m - (number_of (bin_pred v))"
+ "neg (number_of (uminus v)::int) ==>
+ Suc m - (number_of v) = m - (number_of (pred v))"
apply (subst Suc_diff_eq_diff_pred)
apply simp
apply (simp del: nat_numeral_1_eq_1)
apply (auto simp only: diff_nat_number_of less_0_number_of [symmetric]
- neg_number_of_bin_pred_iff_0)
+ neg_number_of_pred_iff_0)
done
lemma diff_Suc_eq_diff_pred: "m - Suc n = (m - 1) - n"
@@ -49,40 +49,40 @@
lemma nat_case_number_of [simp]:
"nat_case a f (number_of v) =
- (let pv = number_of (bin_pred v) in
+ (let pv = number_of (pred v) in
if neg pv then a else f (nat pv))"
-by (simp split add: nat.split add: Let_def neg_number_of_bin_pred_iff_0)
+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 (bin_pred v) in
+ (let pv = number_of (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
del: nat_numeral_1_eq_1
add: numeral_1_eq_Suc_0 [symmetric] Let_def
- neg_imp_number_of_eq_0 neg_number_of_bin_pred_iff_0)
+ neg_imp_number_of_eq_0 neg_number_of_pred_iff_0)
done
lemma nat_rec_number_of [simp]:
"nat_rec a f (number_of v) =
- (let pv = number_of (bin_pred v) in
+ (let pv = number_of (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_bin_pred_iff_0)
+apply (simp_all (no_asm_simp) add: Let_def neg_number_of_pred_iff_0)
apply (simp split add: split_if_asm)
done
lemma nat_rec_add_eq_if [simp]:
"nat_rec a f (number_of v + n) =
- (let pv = number_of (bin_pred v) in
+ (let pv = number_of (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)
apply (simp split add: nat.split
del: nat_numeral_1_eq_1
add: numeral_1_eq_Suc_0 [symmetric] Let_def neg_imp_number_of_eq_0
- neg_number_of_bin_pred_iff_0)
+ neg_number_of_pred_iff_0)
done
--- a/src/HOL/Integ/Numeral.thy Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Integ/Numeral.thy Wed Sep 06 13:48:02 2006 +0200
@@ -1,292 +1,315 @@
-(* Title: HOL/Integ/Numeral.thy
+(* Title: HOL/Integ/Numeral.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1994 University of Cambridge
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1994 University of Cambridge
*)
-header{*Arithmetic on Binary Integers*}
+header {* Arithmetic on Binary Integers *}
theory Numeral
imports IntDef Datatype
uses "../Tools/numeral_syntax.ML"
begin
-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/Integ/twos-compl.ML"}, function @{text
-int_of_binary}, for the numerical interpretation.
+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/Integ/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"}.
+ 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"}.
*}
+text{*
+ This datatype avoids the use of type @{typ bool}, which would make
+ all of the rewrite rules higher-order.
+*}
-typedef (Bin)
- bin = "UNIV::int set"
- by (auto)
-
-text{*This datatype avoids the use of type @{typ bool}, which would make
-all of the rewrite rules higher-order. If the use of datatype causes
-problems, this two-element type can easily be formalized using typedef.*}
datatype bit = B0 | B1
constdefs
- Pls :: "bin"
- "Pls == Abs_Bin 0"
-
- Min :: "bin"
- "Min == Abs_Bin (- 1)"
-
- Bit :: "[bin,bit] => bin" (infixl "BIT" 90)
- --{*That is, 2w+b*}
- "w BIT b == Abs_Bin ((case b of B0 => 0 | B1 => 1) + Rep_Bin w + Rep_Bin w)"
-
+ Pls :: int
+ "Pls == 0"
+ Min :: int
+ "Min == - 1"
+ Bit :: "int \<Rightarrow> bit \<Rightarrow> int" (infixl "BIT" 90)
+ "k BIT b == (case b of B0 \<Rightarrow> 0 | B1 \<Rightarrow> 1) + k + k"
axclass
number < type -- {* for numeric types: nat, int, real, \dots *}
consts
- number_of :: "bin => 'a::number"
+ number_of :: "int \<Rightarrow> 'a::number"
syntax
- "_Numeral" :: "num_const => 'a" ("_")
+ "_Numeral" :: "num_const \<Rightarrow> 'a" ("_")
setup NumeralSyntax.setup
abbreviation
- "Numeral0 == number_of Pls"
- "Numeral1 == number_of (Pls BIT B1)"
+ "Numeral0 \<equiv> number_of Pls"
+ "Numeral1 \<equiv> number_of (Pls BIT B1)"
-lemma Let_number_of [simp]: "Let (number_of v) f == f (number_of v)"
+lemma Let_number_of [simp]: "Let (number_of v) f = f (number_of v)"
-- {* Unfold all @{text let}s involving constants *}
- by (simp add: Let_def)
+ unfolding Let_def ..
+
+lemma Let_0 [simp]: "Let 0 f = f 0"
+ unfolding Let_def ..
+
+lemma Let_1 [simp]: "Let 1 f = f 1"
+ unfolding Let_def ..
-lemma Let_0 [simp]: "Let 0 f == f 0"
- by (simp add: Let_def)
+definition
+ succ :: "int \<Rightarrow> int"
+ "succ k = k + 1"
+ pred :: "int \<Rightarrow> int"
+ "pred k = k - 1"
+
+lemmas numeral_simps =
+ succ_def pred_def Pls_def Min_def Bit_def
-lemma Let_1 [simp]: "Let 1 f == f 1"
- by (simp add: Let_def)
+text {* Removal of leading zeroes *}
+
+lemma Pls_0_eq [simp]:
+ "Pls BIT B0 = Pls"
+ unfolding numeral_simps by simp
+
+lemma Min_1_eq [simp]:
+ "Min BIT B1 = Min"
+ unfolding numeral_simps by simp
-constdefs
- bin_succ :: "bin=>bin"
- "bin_succ w == Abs_Bin(Rep_Bin w + 1)"
-
- bin_pred :: "bin=>bin"
- "bin_pred w == Abs_Bin(Rep_Bin w - 1)"
+subsection {* The Functions @{term succ}, @{term pred} and @{term uminus} *}
- bin_minus :: "bin=>bin"
- "bin_minus w == Abs_Bin(- (Rep_Bin w))"
+lemma succ_Pls [simp]:
+ "succ Pls = Pls BIT B1"
+ unfolding numeral_simps by simp
- bin_add :: "[bin,bin]=>bin"
- "bin_add v w == Abs_Bin(Rep_Bin v + Rep_Bin w)"
-
- bin_mult :: "[bin,bin]=>bin"
- "bin_mult v w == Abs_Bin(Rep_Bin v * Rep_Bin w)"
+lemma succ_Min [simp]:
+ "succ Min = Pls"
+ unfolding numeral_simps by simp
-lemma Abs_Bin_inverse':
- "Rep_Bin (Abs_Bin x) = x"
-by (rule Abs_Bin_inverse) (auto simp add: Bin_def)
-
-lemmas Bin_simps =
- bin_succ_def bin_pred_def bin_minus_def bin_add_def bin_mult_def
- Pls_def Min_def Bit_def Abs_Bin_inverse Rep_Bin_inverse Bin_def
+lemma succ_1 [simp]:
+ "succ (k BIT B1) = succ k BIT B0"
+ unfolding numeral_simps by simp
-text{*Removal of leading zeroes*}
-lemma Pls_0_eq [simp]: "Pls BIT B0 = Pls"
-by (simp add: Bin_simps)
+lemma succ_0 [simp]:
+ "succ (k BIT B0) = k BIT B1"
+ unfolding numeral_simps by simp
-lemma Min_1_eq [simp]: "Min BIT B1 = Min"
-by (simp add: Bin_simps)
-
-subsection{*The Functions @{term bin_succ}, @{term bin_pred} and @{term bin_minus}*}
+lemma pred_Pls [simp]:
+ "pred Pls = Min"
+ unfolding numeral_simps by simp
-lemma bin_succ_Pls [simp]: "bin_succ Pls = Pls BIT B1"
-by (simp add: Bin_simps)
-
-lemma bin_succ_Min [simp]: "bin_succ Min = Pls"
-by (simp add: Bin_simps)
-
-lemma bin_succ_1 [simp]: "bin_succ(w BIT B1) = (bin_succ w) BIT B0"
-by (simp add: Bin_simps add_ac)
+lemma pred_Min [simp]:
+ "pred Min = Min BIT B0"
+ unfolding numeral_simps by simp
-lemma bin_succ_0 [simp]: "bin_succ(w BIT B0) = w BIT B1"
-by (simp add: Bin_simps add_ac)
+lemma pred_1 [simp]:
+ "pred (k BIT B1) = k BIT B0"
+ unfolding numeral_simps by simp
-lemma bin_pred_Pls [simp]: "bin_pred Pls = Min"
-by (simp add: Bin_simps)
-
-lemma bin_pred_Min [simp]: "bin_pred Min = Min BIT B0"
-by (simp add: Bin_simps diff_minus)
+lemma pred_0 [simp]:
+ "pred (k BIT B0) = pred k BIT B1"
+ unfolding numeral_simps by simp
-lemma bin_pred_1 [simp]: "bin_pred(w BIT B1) = w BIT B0"
-by (simp add: Bin_simps)
+lemma minus_Pls [simp]:
+ "- Pls = Pls"
+ unfolding numeral_simps by simp
-lemma bin_pred_0 [simp]: "bin_pred(w BIT B0) = (bin_pred w) BIT B1"
-by (simp add: Bin_simps diff_minus add_ac)
-
-lemma bin_minus_Pls [simp]: "bin_minus Pls = Pls"
-by (simp add: Bin_simps)
+lemma minus_Min [simp]:
+ "- Min = Pls BIT B1"
+ unfolding numeral_simps by simp
-lemma bin_minus_Min [simp]: "bin_minus Min = Pls BIT B1"
-by (simp add: Bin_simps)
+lemma minus_1 [simp]:
+ "- (k BIT B1) = pred (- k) BIT B1"
+ unfolding numeral_simps by simp
-lemma bin_minus_1 [simp]:
- "bin_minus (w BIT B1) = bin_pred (bin_minus w) BIT B1"
-by (simp add: Bin_simps add_ac diff_minus)
-
- lemma bin_minus_0 [simp]: "bin_minus(w BIT B0) = (bin_minus w) BIT B0"
-by (simp add: Bin_simps)
+lemma minus_0 [simp]:
+ "- (k BIT B0) = (- k) BIT B0"
+ unfolding numeral_simps by simp
-subsection{*Binary Addition and Multiplication:
- @{term bin_add} and @{term bin_mult}*}
+subsection {*
+ Binary Addition and Multiplication: @{term "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"}
+ and @{term "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int"}
+*}
-lemma bin_add_Pls [simp]: "bin_add Pls w = w"
-by (simp add: Bin_simps)
+lemma add_Pls [simp]:
+ "Pls + k = k"
+ unfolding numeral_simps by simp
-lemma bin_add_Min [simp]: "bin_add Min w = bin_pred w"
-by (simp add: Bin_simps diff_minus add_ac)
+lemma add_Min [simp]:
+ "Min + k = pred k"
+ unfolding numeral_simps by simp
-lemma bin_add_BIT_11 [simp]:
- "bin_add (v BIT B1) (w BIT B1) = bin_add v (bin_succ w) BIT B0"
-by (simp add: Bin_simps add_ac)
+lemma add_BIT_11 [simp]:
+ "(k BIT B1) + (l BIT B1) = (k + succ l) BIT B0"
+ unfolding numeral_simps by simp
-lemma bin_add_BIT_10 [simp]:
- "bin_add (v BIT B1) (w BIT B0) = (bin_add v w) BIT B1"
-by (simp add: Bin_simps add_ac)
+lemma add_BIT_10 [simp]:
+ "(k BIT B1) + (l BIT B0) = (k + l) BIT B1"
+ unfolding numeral_simps by simp
-lemma bin_add_BIT_0 [simp]:
- "bin_add (v BIT B0) (w BIT y) = bin_add v w BIT y"
-by (simp add: Bin_simps add_ac)
+lemma add_BIT_0 [simp]:
+ "(k BIT B0) + (l BIT b) = (k + l) BIT b"
+ unfolding numeral_simps by simp
-lemma bin_add_Pls_right [simp]: "bin_add w Pls = w"
-by (simp add: Bin_simps)
+lemma add_Pls_right [simp]:
+ "k + Pls = k"
+ unfolding numeral_simps by simp
-lemma bin_add_Min_right [simp]: "bin_add w Min = bin_pred w"
-by (simp add: Bin_simps diff_minus)
+lemma add_Min_right [simp]:
+ "k + Min = pred k"
+ unfolding numeral_simps by simp
-lemma bin_mult_Pls [simp]: "bin_mult Pls w = Pls"
-by (simp add: Bin_simps)
+lemma mult_Pls [simp]:
+ "Pls * w = Pls"
+ unfolding numeral_simps by simp
-lemma bin_mult_Min [simp]: "bin_mult Min w = bin_minus w"
-by (simp add: Bin_simps)
+lemma mult_Min [simp]:
+ "Min * k = - k"
+ unfolding numeral_simps by simp
-lemma bin_mult_1 [simp]:
- "bin_mult (v BIT B1) w = bin_add ((bin_mult v w) BIT B0) w"
-by (simp add: Bin_simps add_ac left_distrib)
+lemma mult_num1 [simp]:
+ "(k BIT B1) * l = ((k * l) BIT B0) + l"
+ unfolding numeral_simps int_distrib by simp
-lemma bin_mult_0 [simp]: "bin_mult (v BIT B0) w = (bin_mult v w) BIT B0"
-by (simp add: Bin_simps left_distrib)
+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}*}
+subsection {* Converting Numerals to Rings: @{term number_of} *}
axclass number_ring \<subseteq> number, comm_ring_1
- number_of_eq: "number_of w = of_int (Rep_Bin w)"
+ number_of_eq: "number_of k = of_int k"
lemma number_of_succ:
- "number_of(bin_succ w) = (1 + number_of w ::'a::number_ring)"
-by (simp add: number_of_eq Bin_simps)
+ "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(bin_pred w) = (- 1 + number_of w ::'a::number_ring)"
-by (simp add: number_of_eq Bin_simps)
+ "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(bin_minus w) = (- (number_of w)::'a::number_ring)"
-by (simp add: number_of_eq Bin_simps)
+ "number_of (uminus w) = (- (number_of w)::'a::number_ring)"
+ unfolding number_of_eq numeral_simps by simp
lemma number_of_add:
- "number_of(bin_add v w) = (number_of v + number_of w::'a::number_ring)"
-by (simp add: number_of_eq Bin_simps)
+ "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(bin_mult v w) = (number_of v * number_of w::'a::number_ring)"
-by (simp add: number_of_eq Bin_simps)
+ "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.*}
+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)"
-by (simp add: number_of_eq Bin_simps left_distrib)
+ "(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)"
-by (simp add: number_of_eq Bin_simps)
+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)"
-by (simp add: number_of_eq Bin_simps)
+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 {*
+ 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"
-by (simp add: number_of_eq Bin_simps)
-
+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 mult_minus1 [simp]: "-1 * z = -(z::'a::number_ring)"
-by (simp add: numeral_m1_eq_minus_1)
+lemma numeral_m1_eq_minus_1:
+ "(-1::'a::number_ring) = - 1"
+ unfolding number_of_eq numeral_simps by simp
-lemma mult_minus1_right [simp]: "z * -1 = -(z::'a::number_ring)"
-by (simp add: numeral_m1_eq_minus_1)
+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(bin_minus w) * (z::'a::number_ring)"
-by (simp add: number_of_minus)
+ "- (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
-text{*Subtraction*}
-lemma diff_number_of_eq:
- "number_of v - number_of w =
- (number_of(bin_add v (bin_minus w))::'a::number_ring)"
-by (simp add: diff_minus number_of_add number_of_minus)
+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)
-lemma number_of_Pls: "number_of Pls = (0::'a::number_ring)"
-by (simp add: number_of_eq Bin_simps)
-
-lemma number_of_Min: "number_of Min = (- 1::'a::number_ring)"
-by (simp add: number_of_eq Bin_simps)
+subsection {* Equality of Binary Numbers *}
-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)"
-by (simp add: number_of_eq Bin_simps split: bit.split)
-
-
-
-subsection{*Equality of Binary Numbers*}
-
-text{*First version by Norbert Voelker*}
+text {* First version by Norbert Voelker *}
lemma eq_number_of_eq:
"((number_of x::'a::number_ring) = number_of y) =
- iszero (number_of (bin_add x (bin_minus y)) :: 'a)"
-by (simp add: iszero_def compare_rls number_of_add number_of_minus)
+ 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)"
-by (simp add: iszero_def numeral_0_eq_0)
+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)"
-by (simp add: iszero_def numeral_m1_eq_minus_1 eq_commute)
+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*}
+subsection {* Comparisons, for Ordered Rings *}
-lemma double_eq_0_iff: "(a + a = 0) = (a = (0::'a::ordered_idom))"
+lemma double_eq_0_iff:
+ "(a + a = 0) = (a = (0::'a::ordered_idom))"
proof -
- have "a + a = (1+1)*a" by (simp add: left_distrib)
+ have "a + a = (1 + 1) * a" unfolding left_distrib by simp
with zero_less_two [where 'a = 'a]
show ?thesis by force
qed
lemma le_imp_0_less:
- assumes le: "0 \<le> z" shows "(0::int) < 1 + z"
+ assumes le: "0 \<le> z"
+ shows "(0::int) < 1 + z"
proof -
have "0 \<le> z" .
also have "... < z + 1" by (rule less_add_one)
@@ -294,7 +317,8 @@
finally show "0 < 1 + z" .
qed
-lemma odd_nonzero: "1 + z + z \<noteq> (0::int)";
+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)
@@ -315,11 +339,13 @@
qed
qed
+text {* The premise involving @{term Ints} prevents @{term "a = 1/2"}. *}
-text{*The premise involving @{term Ints} prevents @{term "a = 1/2"}.*}
-lemma Ints_odd_nonzero: "a \<in> Ints ==> 1 + a + a \<noteq> (0::'a::ordered_idom)"
-proof (unfold Ints_def)
- assume "a \<in> range of_int"
+lemma Ints_odd_nonzero:
+ assumes in_Ints: "a \<in> Ints"
+ shows "1 + a + a \<noteq> (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" ..
show ?thesis
proof
@@ -330,46 +356,50 @@
qed
qed
-lemma Ints_number_of: "(number_of w :: 'a::number_ring) \<in> Ints"
-by (simp add: number_of_eq Ints_def)
-
+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 & iszero (number_of w::'a::{ordered_idom,number_ring}))"
-by (simp add: iszero_def number_of_eq Bin_simps double_eq_0_iff
- Ints_odd_nonzero Ints_def split: bit.split)
+ "iszero (number_of (w BIT x)::'a) =
+ (x = B0 \<and> iszero (number_of w::'a::{ordered_idom,number_ring}))"
+ by (simp add: iszero_def number_of_eq numeral_simps double_eq_0_iff
+ Ints_odd_nonzero Ints_def split: bit.split)
lemma iszero_number_of_0:
- "iszero (number_of (w BIT B0) :: 'a::{ordered_idom,number_ring}) =
- iszero (number_of w :: 'a)"
-by (simp only: iszero_number_of_BIT simp_thms)
+ "iszero (number_of (w BIT B0) :: 'a::{ordered_idom,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::{ordered_idom,number_ring})"
-by (simp add: iszero_number_of_BIT)
+ "~ iszero (number_of (w BIT B1)::'a::{ordered_idom,number_ring})"
+ by (simp add: iszero_number_of_BIT)
-subsection{*The Less-Than Relation*}
+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 (bin_add x (bin_minus y)) :: 'a)"
+ "((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"} *}
+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)
+ "~ 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)
+ "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))"
+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)"
@@ -378,7 +408,8 @@
finally show ?thesis .
qed
-lemma odd_less_0: "(1 + z + z < 0) = (z < (0::int))";
+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
@@ -386,14 +417,16 @@
next
case (neg n)
thus ?thesis by (simp del: int_Suc
- add: int_Suc0_eq_1 [symmetric] zadd_int compare_rls)
+ add: int_Suc0_eq_1 [symmetric] zadd_int compare_rls)
qed
-text{*The premise involving @{term Ints} prevents @{term "a = 1/2"}.*}
+text {* The premise involving @{term Ints} prevents @{term "a = 1/2"}. *}
+
lemma Ints_odd_less_0:
- "a \<in> Ints ==> (1 + a + a < 0) = (a < (0::'a::ordered_idom))";
-proof (unfold Ints_def)
- assume "a \<in> range of_int"
+ 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)
@@ -403,93 +436,98 @@
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 Bin_simps double_less_0_iff
- Ints_odd_less_0 Ints_def split: bit.split)
-
+ "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 {* Less-Than or Equals *}
+
+text {* Reduces @{term "a\<le>b"} to @{term "~ (b<a)"} for ALL numerals. *}
-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]
+ 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 (bin_add y (bin_minus x)) :: 'a)))"
+ = (~ (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})*}
+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)
+ "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
+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.*}
+subsection {* Simplification of arithmetic operations on integer constants. *}
-lemmas bin_arith_extra_simps =
- 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
+lemmas arith_extra_simps =
+ 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}.
+*}
-text{*For making a minimal simpset, one must include these default simprules.
- Also include @{text simp_thms} *}
-lemmas bin_arith_simps =
- Numeral.bit.distinct
- Pls_0_eq Min_1_eq
- bin_pred_Pls bin_pred_Min bin_pred_1 bin_pred_0
- bin_succ_Pls bin_succ_Min bin_succ_1 bin_succ_0
- bin_add_Pls bin_add_Min bin_add_BIT_0 bin_add_BIT_10 bin_add_BIT_11
- bin_minus_Pls bin_minus_Min bin_minus_1 bin_minus_0
- bin_mult_Pls bin_mult_Min bin_mult_1 bin_mult_0
- bin_add_Pls_right bin_add_Min_right
- abs_zero abs_one bin_arith_extra_simps
+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 bin_rel_simps =
- eq_number_of_eq iszero_number_of_Pls 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
+text {* Simplification of relational operations *}
-declare bin_arith_extra_simps [simp]
-declare bin_rel_simps [simp]
+lemmas rel_simps =
+ eq_number_of_eq iszero_number_of_Pls 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
+
+declare arith_extra_simps [simp]
+declare rel_simps [simp]
-subsection{*Simplification of arithmetic when nested to the right*}
+subsection {* Simplification of arithmetic when nested to the right. *}
lemma add_number_of_left [simp]:
- "number_of v + (number_of w + z) =
- (number_of(bin_add v w) + z::'a::number_ring)"
-by (simp add: add_assoc [symmetric])
+ "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(bin_mult v w) * z::'a::number_ring)"
-by (simp add: mult_assoc [symmetric])
+ "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(bin_add v w) - (c::'a::number_ring)"
-by (simp add: diff_minus add_number_of_left)
+ "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 (bin_add v (bin_minus w)) + (c::'a::number_ring)"
+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
--- a/src/HOL/Integ/Presburger.thy Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Integ/Presburger.thy Wed Sep 06 13:48:02 2006 +0200
@@ -992,7 +992,8 @@
lemma not_true_eq_false: "(~ True) = False" by simp
-lemma int_eq_number_of_eq: "(((number_of v)::int)=(number_of w)) = iszero ((number_of (bin_add v (bin_minus w)))::int)"
+lemma int_eq_number_of_eq:
+ "(((number_of v)::int) = (number_of w)) = iszero ((number_of (v + (uminus w)))::int)"
by simp
lemma int_iszero_number_of_Pls: "iszero (Numeral0::int)"
by (simp only: iszero_number_of_Pls)
@@ -1006,7 +1007,7 @@
lemma int_iszero_number_of_1: "\<not> iszero ((number_of (w BIT bit.B1))::int)"
by simp
-lemma int_less_number_of_eq_neg: "(((number_of x)::int) < number_of y) = neg ((number_of (bin_add x (bin_minus y)))::int)"
+lemma int_less_number_of_eq_neg: "(((number_of x)::int) < number_of y) = neg ((number_of (x + (uminus y)))::int)"
by simp
lemma int_not_neg_number_of_Pls: "\<not> (neg (Numeral0::int))"
@@ -1018,18 +1019,20 @@
lemma int_neg_number_of_BIT: "neg ((number_of (w BIT x))::int) = neg ((number_of w)::int)"
by simp
-lemma int_le_number_of_eq: "(((number_of x)::int) \<le> number_of y) = (\<not> neg ((number_of (bin_add y (bin_minus x)))::int))"
+lemma int_le_number_of_eq: "(((number_of x)::int) \<le> number_of y) = (\<not> neg ((number_of (y + (uminus x)))::int))"
by simp
-lemma int_number_of_add_sym: "((number_of v)::int) + number_of w = number_of (bin_add v w)"
+lemma int_number_of_add_sym: "((number_of v)::int) + number_of w = number_of (v + w)"
by simp
-lemma int_number_of_diff_sym: "((number_of v)::int) - number_of w = number_of (bin_add v (bin_minus w))"
+lemma int_number_of_diff_sym:
+ "((number_of v)::int) - number_of w = number_of (v + (uminus w))"
by simp
-lemma int_number_of_mult_sym: "((number_of v)::int) * number_of w = number_of (bin_mult v w)"
+lemma int_number_of_mult_sym:
+ "((number_of v)::int) * number_of w = number_of (v * w)"
by simp
-lemma int_number_of_minus_sym: "- ((number_of v)::int) = number_of (bin_minus v)"
+lemma int_number_of_minus_sym: "- ((number_of v)::int) = number_of (uminus v)"
by simp
lemma add_left_zero: "0 + a = (a::'a::comm_monoid_add)"
by simp
--- a/src/HOL/Integ/int_arith1.ML Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Integ/int_arith1.ML Wed Sep 06 13:48:02 2006 +0200
@@ -7,90 +7,90 @@
(** Misc ML bindings **)
-val bin_succ_Pls = thm"bin_succ_Pls";
-val bin_succ_Min = thm"bin_succ_Min";
-val bin_succ_1 = thm"bin_succ_1";
-val bin_succ_0 = thm"bin_succ_0";
+val succ_Pls = thm "succ_Pls";
+val succ_Min = thm "succ_Min";
+val succ_1 = thm "succ_1";
+val succ_0 = thm "succ_0";
-val bin_pred_Pls = thm"bin_pred_Pls";
-val bin_pred_Min = thm"bin_pred_Min";
-val bin_pred_1 = thm"bin_pred_1";
-val bin_pred_0 = thm"bin_pred_0";
+val pred_Pls = thm "pred_Pls";
+val pred_Min = thm "pred_Min";
+val pred_1 = thm "pred_1";
+val pred_0 = thm "pred_0";
-val bin_minus_Pls = thm"bin_minus_Pls";
-val bin_minus_Min = thm"bin_minus_Min";
-val bin_minus_1 = thm"bin_minus_1";
-val bin_minus_0 = thm"bin_minus_0";
+val minus_Pls = thm "minus_Pls";
+val minus_Min = thm "minus_Min";
+val minus_1 = thm "minus_1";
+val minus_0 = thm "minus_0";
-val bin_add_Pls = thm"bin_add_Pls";
-val bin_add_Min = thm"bin_add_Min";
-val bin_add_BIT_11 = thm"bin_add_BIT_11";
-val bin_add_BIT_10 = thm"bin_add_BIT_10";
-val bin_add_BIT_0 = thm"bin_add_BIT_0";
-val bin_add_Pls_right = thm"bin_add_Pls_right";
-val bin_add_Min_right = thm"bin_add_Min_right";
+val add_Pls = thm "add_Pls";
+val add_Min = thm "add_Min";
+val add_BIT_11 = thm "add_BIT_11";
+val add_BIT_10 = thm "add_BIT_10";
+val add_BIT_0 = thm "add_BIT_0";
+val add_Pls_right = thm "add_Pls_right";
+val add_Min_right = thm "add_Min_right";
-val bin_mult_Pls = thm"bin_mult_Pls";
-val bin_mult_Min = thm"bin_mult_Min";
-val bin_mult_1 = thm"bin_mult_1";
-val bin_mult_0 = thm"bin_mult_0";
+val mult_Pls = thm "mult_Pls";
+val mult_Min = thm "mult_Min";
+val mult_num1 = thm "mult_num1";
+val mult_num0 = thm "mult_num0";
val neg_def = thm "neg_def";
val iszero_def = thm "iszero_def";
-val number_of_succ = thm"number_of_succ";
-val number_of_pred = thm"number_of_pred";
-val number_of_minus = thm"number_of_minus";
-val number_of_add = thm"number_of_add";
-val diff_number_of_eq = thm"diff_number_of_eq";
-val number_of_mult = thm"number_of_mult";
-val double_number_of_BIT = thm"double_number_of_BIT";
-val numeral_0_eq_0 = thm"numeral_0_eq_0";
-val numeral_1_eq_1 = thm"numeral_1_eq_1";
-val numeral_m1_eq_minus_1 = thm"numeral_m1_eq_minus_1";
-val mult_minus1 = thm"mult_minus1";
-val mult_minus1_right = thm"mult_minus1_right";
-val minus_number_of_mult = thm"minus_number_of_mult";
-val zero_less_nat_eq = thm"zero_less_nat_eq";
-val eq_number_of_eq = thm"eq_number_of_eq";
-val iszero_number_of_Pls = thm"iszero_number_of_Pls";
-val nonzero_number_of_Min = thm"nonzero_number_of_Min";
-val iszero_number_of_BIT = thm"iszero_number_of_BIT";
-val iszero_number_of_0 = thm"iszero_number_of_0";
-val iszero_number_of_1 = thm"iszero_number_of_1";
-val less_number_of_eq_neg = thm"less_number_of_eq_neg";
-val le_number_of_eq = thm"le_number_of_eq";
-val not_neg_number_of_Pls = thm"not_neg_number_of_Pls";
-val neg_number_of_Min = thm"neg_number_of_Min";
-val neg_number_of_BIT = thm"neg_number_of_BIT";
-val le_number_of_eq_not_less = thm"le_number_of_eq_not_less";
-val abs_number_of = thm"abs_number_of";
-val number_of_reorient = thm"number_of_reorient";
-val add_number_of_left = thm"add_number_of_left";
-val mult_number_of_left = thm"mult_number_of_left";
-val add_number_of_diff1 = thm"add_number_of_diff1";
-val add_number_of_diff2 = thm"add_number_of_diff2";
-val less_iff_diff_less_0 = thm"less_iff_diff_less_0";
-val eq_iff_diff_eq_0 = thm"eq_iff_diff_eq_0";
-val le_iff_diff_le_0 = thm"le_iff_diff_le_0";
+val number_of_succ = thm "number_of_succ";
+val number_of_pred = thm "number_of_pred";
+val number_of_minus = thm "number_of_minus";
+val number_of_add = thm "number_of_add";
+val diff_number_of_eq = thm "diff_number_of_eq";
+val number_of_mult = thm "number_of_mult";
+val double_number_of_BIT = thm "double_number_of_BIT";
+val numeral_0_eq_0 = thm "numeral_0_eq_0";
+val numeral_1_eq_1 = thm "numeral_1_eq_1";
+val numeral_m1_eq_minus_1 = thm "numeral_m1_eq_minus_1";
+val mult_minus1 = thm "mult_minus1";
+val mult_minus1_right = thm "mult_minus1_right";
+val minus_number_of_mult = thm "minus_number_of_mult";
+val zero_less_nat_eq = thm "zero_less_nat_eq";
+val eq_number_of_eq = thm "eq_number_of_eq";
+val iszero_number_of_Pls = thm "iszero_number_of_Pls";
+val nonzero_number_of_Min = thm "nonzero_number_of_Min";
+val iszero_number_of_BIT = thm "iszero_number_of_BIT";
+val iszero_number_of_0 = thm "iszero_number_of_0";
+val iszero_number_of_1 = thm "iszero_number_of_1";
+val less_number_of_eq_neg = thm "less_number_of_eq_neg";
+val le_number_of_eq = thm "le_number_of_eq";
+val not_neg_number_of_Pls = thm "not_neg_number_of_Pls";
+val neg_number_of_Min = thm "neg_number_of_Min";
+val neg_number_of_BIT = thm "neg_number_of_BIT";
+val le_number_of_eq_not_less = thm "le_number_of_eq_not_less";
+val abs_number_of = thm "abs_number_of";
+val number_of_reorient = thm "number_of_reorient";
+val add_number_of_left = thm "add_number_of_left";
+val mult_number_of_left = thm "mult_number_of_left";
+val add_number_of_diff1 = thm "add_number_of_diff1";
+val add_number_of_diff2 = thm "add_number_of_diff2";
+val less_iff_diff_less_0 = thm "less_iff_diff_less_0";
+val eq_iff_diff_eq_0 = thm "eq_iff_diff_eq_0";
+val le_iff_diff_le_0 = thm "le_iff_diff_le_0";
-val bin_arith_extra_simps = thms"bin_arith_extra_simps";
-val bin_arith_simps = thms"bin_arith_simps";
-val bin_rel_simps = thms"bin_rel_simps";
+val arith_extra_simps = thms "arith_extra_simps";
+val arith_simps = thms "arith_simps";
+val rel_simps = thms "rel_simps";
val zless_imp_add1_zle = thm "zless_imp_add1_zle";
-val combine_common_factor = thm"combine_common_factor";
-val eq_add_iff1 = thm"eq_add_iff1";
-val eq_add_iff2 = thm"eq_add_iff2";
-val less_add_iff1 = thm"less_add_iff1";
-val less_add_iff2 = thm"less_add_iff2";
-val le_add_iff1 = thm"le_add_iff1";
-val le_add_iff2 = thm"le_add_iff2";
+val combine_common_factor = thm "combine_common_factor";
+val eq_add_iff1 = thm "eq_add_iff1";
+val eq_add_iff2 = thm "eq_add_iff2";
+val less_add_iff1 = thm "less_add_iff1";
+val less_add_iff2 = thm "less_add_iff2";
+val le_add_iff1 = thm "le_add_iff1";
+val le_add_iff2 = thm "le_add_iff2";
-val arith_special = thms"arith_special";
+val arith_special = thms "arith_special";
-structure Bin_Simprocs =
+structure Int_Numeral_Base_Simprocs =
struct
fun prove_conv tacs ctxt (_: thm list) (t, u) =
if t aconv u then NONE
@@ -133,13 +133,13 @@
Addsimps arith_special;
-Addsimprocs [Bin_Simprocs.reorient_simproc];
+Addsimprocs [Int_Numeral_Base_Simprocs.reorient_simproc];
structure Int_Numeral_Simprocs =
struct
-(*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic in simprocs
+(*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic in Int_Numeral_Base_Simprocs
isn't complicated by the abstract 0 and 1.*)
val numeral_syms = [numeral_0_eq_0 RS sym, numeral_1_eq_1 RS sym];
@@ -175,7 +175,7 @@
fun numtermless tu = (numterm_ord tu = LESS);
-(*Defined in this file, but perhaps needed only for simprocs of type nat.*)
+(*Defined in this file, but perhaps needed only for Int_Numeral_Base_Simprocs of type nat.*)
val num_ss = HOL_ss settermless numtermless;
@@ -273,20 +273,20 @@
val mult_1s = thms "mult_1s";
(*To perform binary arithmetic. The "left" rewriting handles patterns
- created by the simprocs, such as 3 * (5 * x). *)
-val bin_simps = [numeral_0_eq_0 RS sym, numeral_1_eq_1 RS sym,
+ created by the Int_Numeral_Base_Simprocs, such as 3 * (5 * x). *)
+val simps = [numeral_0_eq_0 RS sym, numeral_1_eq_1 RS sym,
add_number_of_left, mult_number_of_left] @
- bin_arith_simps @ bin_rel_simps;
+ arith_simps @ rel_simps;
(*Binary arithmetic BUT NOT ADDITION since it may collapse adjacent terms
during re-arrangement*)
-val non_add_bin_simps =
- subtract Thm.eq_thm [add_number_of_left, number_of_add RS sym] bin_simps;
+val non_add_simps =
+ subtract Thm.eq_thm [add_number_of_left, number_of_add RS sym] simps;
(*To evaluate binary negations of coefficients*)
val minus_simps = [numeral_m1_eq_minus_1 RS sym, number_of_minus RS sym,
- bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min,
- bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min];
+ minus_1, minus_0, minus_Pls, minus_Min,
+ pred_1, pred_0, pred_Pls, pred_Min];
(*To let us treat subtraction as addition*)
val diff_simps = [diff_minus, minus_add_distrib, minus_minus];
@@ -322,14 +322,14 @@
val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
diff_simps @ minus_simps @ add_ac
- val norm_ss2 = num_ss addsimps non_add_bin_simps @ mult_minus_simps
+ val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps
val norm_ss3 = num_ss addsimps minus_from_mult_simps @ add_ac @ mult_ac
fun norm_tac ss =
ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3))
- val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps
+ val numeral_simp_ss = HOL_ss addsimps add_0s @ simps
fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
val simplify_meta_eq = simplify_meta_eq (add_0s @ mult_1s)
end;
@@ -337,7 +337,7 @@
structure EqCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
- val prove_conv = Bin_Simprocs.prove_conv
+ val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
val mk_bal = HOLogic.mk_eq
val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
val bal_add1 = eq_add_iff1 RS trans
@@ -346,7 +346,7 @@
structure LessCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
- val prove_conv = Bin_Simprocs.prove_conv
+ val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binrel "Orderings.less"
val dest_bal = HOLogic.dest_bin "Orderings.less" Term.dummyT
val bal_add1 = less_add_iff1 RS trans
@@ -355,7 +355,7 @@
structure LeCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
- val prove_conv = Bin_Simprocs.prove_conv
+ val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binrel "Orderings.less_eq"
val dest_bal = HOLogic.dest_bin "Orderings.less_eq" Term.dummyT
val bal_add1 = le_add_iff1 RS trans
@@ -363,7 +363,7 @@
);
val cancel_numerals =
- map Bin_Simprocs.prep_simproc
+ map Int_Numeral_Base_Simprocs.prep_simproc
[("inteq_cancel_numerals",
["(l::'a::number_ring) + m = n",
"(l::'a::number_ring) = m + n",
@@ -398,19 +398,19 @@
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff 1
val left_distrib = combine_common_factor RS trans
- val prove_conv = Bin_Simprocs.prove_conv_nohyps
+ val prove_conv = Int_Numeral_Base_Simprocs.prove_conv_nohyps
val trans_tac = fn _ => trans_tac
val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
diff_simps @ minus_simps @ add_ac
- val norm_ss2 = num_ss addsimps non_add_bin_simps @ mult_minus_simps
+ val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps
val norm_ss3 = num_ss addsimps minus_from_mult_simps @ add_ac @ mult_ac
fun norm_tac ss =
ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3))
- val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps
+ val numeral_simp_ss = HOL_ss addsimps add_0s @ simps
fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
val simplify_meta_eq = simplify_meta_eq (add_0s @ mult_1s)
end;
@@ -418,7 +418,7 @@
structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
val combine_numerals =
- Bin_Simprocs.prep_simproc
+ Int_Numeral_Base_Simprocs.prep_simproc
("int_combine_numerals",
["(i::'a::number_ring) + j", "(i::'a::number_ring) - j"],
K CombineNumerals.proc);
@@ -479,7 +479,7 @@
structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data);
val assoc_fold_simproc =
- Bin_Simprocs.prep_simproc
+ Int_Numeral_Base_Simprocs.prep_simproc
("semiring_assoc_fold", ["(a::'a::comm_semiring_1_cancel) * b"],
K Semiring_Times_Assoc.proc);
@@ -503,10 +503,10 @@
(* reduce contradictory <= to False *)
val add_rules =
- simp_thms @ bin_arith_simps @ bin_rel_simps @ arith_special @
+ simp_thms @ arith_simps @ rel_simps @ arith_special @
[neg_le_iff_le, numeral_0_eq_0, numeral_1_eq_1,
minus_zero, diff_minus, left_minus, right_minus,
- mult_zero_left, mult_zero_right, mult_1, mult_1_right,
+ mult_zero_left, mult_zero_right, mult_num1, mult_1_right,
minus_mult_left RS sym, minus_mult_right RS sym,
minus_add_distrib, minus_minus, mult_assoc,
of_nat_0, of_nat_1, of_nat_Suc, of_nat_add, of_nat_mult,
@@ -515,7 +515,7 @@
val nat_inj_thms = [zle_int RS iffD2,
int_int_eq RS iffD2]
-val simprocs = [assoc_fold_simproc, Int_Numeral_Simprocs.combine_numerals]@
+val Int_Numeral_Base_Simprocs = [assoc_fold_simproc, Int_Numeral_Simprocs.combine_numerals]@
Int_Numeral_Simprocs.cancel_numerals
in
@@ -528,7 +528,7 @@
lessD = lessD @ [zless_imp_add1_zle],
neqE = neqE,
simpset = simpset addsimps add_rules
- addsimprocs simprocs
+ addsimprocs Int_Numeral_Base_Simprocs
addcongs [if_weak_cong]}) #>
arith_inj_const ("NatArith.of_nat", HOLogic.natT --> HOLogic.intT) #>
arith_inj_const ("IntDef.int", HOLogic.natT --> HOLogic.intT) #>
--- a/src/HOL/Integ/int_factor_simprocs.ML Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Integ/int_factor_simprocs.ML Wed Sep 06 13:48:02 2006 +0200
@@ -45,25 +45,25 @@
val trans_tac = fn _ => trans_tac
val norm_ss1 = HOL_ss addsimps minus_from_mult_simps @ mult_1s
- val norm_ss2 = HOL_ss addsimps bin_simps@mult_minus_simps
+ val norm_ss2 = HOL_ss addsimps simps @ mult_minus_simps
val norm_ss3 = HOL_ss addsimps mult_ac
fun norm_tac ss =
ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3))
- val numeral_simp_ss = HOL_ss addsimps rel_number_of @ bin_simps
+ val numeral_simp_ss = HOL_ss addsimps rel_number_of @ simps
fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
val simplify_meta_eq =
Int_Numeral_Simprocs.simplify_meta_eq
[add_0, add_0_right,
- mult_zero_left, mult_zero_right, mult_1, mult_1_right];
+ mult_zero_left, mult_zero_right, mult_num1, mult_1_right];
end
(*Version for integer division*)
structure DivCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
- val prove_conv = Bin_Simprocs.prove_conv
+ val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binop "Divides.op div"
val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.intT
val cancel = int_mult_div_cancel1 RS trans
@@ -73,7 +73,7 @@
(*Version for fields*)
structure FieldDivCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
- val prove_conv = Bin_Simprocs.prove_conv
+ val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binop "HOL.divide"
val dest_bal = HOLogic.dest_bin "HOL.divide" Term.dummyT
val cancel = mult_divide_cancel_left RS trans
@@ -83,7 +83,7 @@
(*Version for ordered rings: mult_cancel_left requires an ordering*)
structure EqCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
- val prove_conv = Bin_Simprocs.prove_conv
+ val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
val mk_bal = HOLogic.mk_eq
val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
val cancel = mult_cancel_left RS trans
@@ -93,7 +93,7 @@
(*Version for (unordered) fields*)
structure FieldEqCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
- val prove_conv = Bin_Simprocs.prove_conv
+ val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
val mk_bal = HOLogic.mk_eq
val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
val cancel = field_mult_cancel_left RS trans
@@ -102,7 +102,7 @@
structure LessCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
- val prove_conv = Bin_Simprocs.prove_conv
+ val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binrel "Orderings.less"
val dest_bal = HOLogic.dest_bin "Orderings.less" Term.dummyT
val cancel = mult_less_cancel_left RS trans
@@ -111,7 +111,7 @@
structure LeCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
- val prove_conv = Bin_Simprocs.prove_conv
+ val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binrel "Orderings.less_eq"
val dest_bal = HOLogic.dest_bin "Orderings.less_eq" Term.dummyT
val cancel = mult_le_cancel_left RS trans
@@ -119,7 +119,7 @@
)
val ring_cancel_numeral_factors =
- map Bin_Simprocs.prep_simproc
+ map Int_Numeral_Base_Simprocs.prep_simproc
[("ring_eq_cancel_numeral_factor",
["(l::'a::{ordered_idom,number_ring}) * m = n",
"(l::'a::{ordered_idom,number_ring}) = m * n"],
@@ -138,7 +138,7 @@
val field_cancel_numeral_factors =
- map Bin_Simprocs.prep_simproc
+ map Int_Numeral_Base_Simprocs.prep_simproc
[("field_eq_cancel_numeral_factor",
["(l::'a::{field,number_ring}) * m = n",
"(l::'a::{field,number_ring}) = m * n"],
@@ -261,7 +261,7 @@
rat_arith.ML works for all fields.*)
structure EqCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
- val prove_conv = Bin_Simprocs.prove_conv
+ val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
val mk_bal = HOLogic.mk_eq
val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT
val simplify_meta_eq = cancel_simplify_meta_eq mult_cancel_left
@@ -271,14 +271,14 @@
rat_arith.ML works for all fields, using real division (/).*)
structure DivideCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
- val prove_conv = Bin_Simprocs.prove_conv
+ val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binop "Divides.op div"
val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.intT
val simplify_meta_eq = cancel_simplify_meta_eq int_mult_div_cancel_disj
);
val int_cancel_factor =
- map Bin_Simprocs.prep_simproc
+ map Int_Numeral_Base_Simprocs.prep_simproc
[("ring_eq_cancel_factor", ["(l::int) * m = n", "(l::int) = m * n"],
K EqCancelFactor.proc),
("int_divide_cancel_factor", ["((l::int) * m) div n", "(l::int) div (m*n)"],
@@ -288,7 +288,7 @@
structure FieldEqCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
- val prove_conv = Bin_Simprocs.prove_conv
+ val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
val mk_bal = HOLogic.mk_eq
val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
val simplify_meta_eq = cancel_simplify_meta_eq field_mult_cancel_left
@@ -296,7 +296,7 @@
structure FieldDivideCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
- val prove_conv = Bin_Simprocs.prove_conv
+ val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binop "HOL.divide"
val dest_bal = HOLogic.dest_bin "HOL.divide" Term.dummyT
val simplify_meta_eq = cancel_simplify_meta_eq mult_divide_cancel_eq_if
@@ -305,7 +305,7 @@
(*The number_ring class is necessary because the simprocs refer to the
binary number 1. FIXME: probably they could use 1 instead.*)
val field_cancel_factor =
- map Bin_Simprocs.prep_simproc
+ map Int_Numeral_Base_Simprocs.prep_simproc
[("field_eq_cancel_factor",
["(l::'a::{field,number_ring}) * m = n",
"(l::'a::{field,number_ring}) = m * n"],
--- a/src/HOL/Integ/nat_simprocs.ML Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Integ/nat_simprocs.ML Wed Sep 06 13:48:02 2006 +0200
@@ -64,7 +64,7 @@
mult_nat_number_of, nat_number_of_mult_left,
less_nat_number_of,
Let_number_of, nat_number_of] @
- bin_arith_simps @ bin_rel_simps;
+ arith_simps @ rel_simps;
fun prep_simproc (name, pats, proc) =
Simplifier.simproc (Theory.sign_of (the_context ())) name pats proc;
@@ -182,7 +182,7 @@
structure EqCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
- val prove_conv = Bin_Simprocs.prove_conv
+ val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
val mk_bal = HOLogic.mk_eq
val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
val bal_add1 = nat_eq_add_iff1 RS trans
@@ -191,7 +191,7 @@
structure LessCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
- val prove_conv = Bin_Simprocs.prove_conv
+ val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binrel "Orderings.less"
val dest_bal = HOLogic.dest_bin "Orderings.less" HOLogic.natT
val bal_add1 = nat_less_add_iff1 RS trans
@@ -200,7 +200,7 @@
structure LeCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
- val prove_conv = Bin_Simprocs.prove_conv
+ val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binrel "Orderings.less_eq"
val dest_bal = HOLogic.dest_bin "Orderings.less_eq" HOLogic.natT
val bal_add1 = nat_le_add_iff1 RS trans
@@ -209,7 +209,7 @@
structure DiffCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
- val prove_conv = Bin_Simprocs.prove_conv
+ val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binop "HOL.minus"
val dest_bal = HOLogic.dest_bin "HOL.minus" HOLogic.natT
val bal_add1 = nat_diff_add_eq1 RS trans
@@ -251,7 +251,7 @@
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff
val left_distrib = left_add_mult_distrib RS trans
- val prove_conv = Bin_Simprocs.prove_conv_nohyps
+ val prove_conv = Int_Numeral_Base_Simprocs.prove_conv_nohyps
val trans_tac = fn _ => trans_tac
val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [Suc_eq_add_numeral_1] @ add_ac
@@ -293,7 +293,7 @@
structure DivCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
- val prove_conv = Bin_Simprocs.prove_conv
+ val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binop "Divides.op div"
val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.natT
val cancel = nat_mult_div_cancel1 RS trans
@@ -302,7 +302,7 @@
structure EqCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
- val prove_conv = Bin_Simprocs.prove_conv
+ val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
val mk_bal = HOLogic.mk_eq
val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
val cancel = nat_mult_eq_cancel1 RS trans
@@ -311,7 +311,7 @@
structure LessCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
- val prove_conv = Bin_Simprocs.prove_conv
+ val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binrel "Orderings.less"
val dest_bal = HOLogic.dest_bin "Orderings.less" HOLogic.natT
val cancel = nat_mult_less_cancel1 RS trans
@@ -320,7 +320,7 @@
structure LeCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
- val prove_conv = Bin_Simprocs.prove_conv
+ val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binrel "Orderings.less_eq"
val dest_bal = HOLogic.dest_bin "Orderings.less_eq" HOLogic.natT
val cancel = nat_mult_le_cancel1 RS trans
@@ -379,7 +379,7 @@
structure EqCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
- val prove_conv = Bin_Simprocs.prove_conv
+ val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
val mk_bal = HOLogic.mk_eq
val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
val simplify_meta_eq = cancel_simplify_meta_eq nat_mult_eq_cancel_disj
@@ -387,7 +387,7 @@
structure LessCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
- val prove_conv = Bin_Simprocs.prove_conv
+ val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binrel "Orderings.less"
val dest_bal = HOLogic.dest_bin "Orderings.less" HOLogic.natT
val simplify_meta_eq = cancel_simplify_meta_eq nat_mult_less_cancel_disj
@@ -395,7 +395,7 @@
structure LeCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
- val prove_conv = Bin_Simprocs.prove_conv
+ val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binrel "Orderings.less_eq"
val dest_bal = HOLogic.dest_bin "Orderings.less_eq" HOLogic.natT
val simplify_meta_eq = cancel_simplify_meta_eq nat_mult_le_cancel_disj
@@ -403,7 +403,7 @@
structure DivideCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
- val prove_conv = Bin_Simprocs.prove_conv
+ val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binop "Divides.op div"
val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.natT
val simplify_meta_eq = cancel_simplify_meta_eq nat_mult_div_cancel_disj
--- a/src/HOL/Integ/presburger.ML Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Integ/presburger.ML Wed Sep 06 13:48:02 2006 +0200
@@ -33,12 +33,12 @@
val presburger_ss = simpset ();
val binarith = map thm
["Pls_0_eq", "Min_1_eq",
- "bin_pred_Pls","bin_pred_Min","bin_pred_1","bin_pred_0",
- "bin_succ_Pls", "bin_succ_Min", "bin_succ_1", "bin_succ_0",
- "bin_add_Pls", "bin_add_Min", "bin_add_BIT_0", "bin_add_BIT_10",
- "bin_add_BIT_11", "bin_minus_Pls", "bin_minus_Min", "bin_minus_1",
- "bin_minus_0", "bin_mult_Pls", "bin_mult_Min", "bin_mult_1", "bin_mult_0",
- "bin_add_Pls_right", "bin_add_Min_right"];
+ "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"];
val intarithrel =
(map thm ["int_eq_number_of_eq","int_neg_number_of_BIT",
"int_le_number_of_eq","int_iszero_number_of_0",
@@ -116,7 +116,6 @@
val bT = HOLogic.boolT;
val bitT = HOLogic.bitT;
val iT = HOLogic.intT;
-val binT = HOLogic.binT;
val nT = HOLogic.natT;
(* Allowed Consts in formulae for presburger tactic*)
@@ -162,11 +161,11 @@
("Numeral.bit.B0", bitT),
("Numeral.bit.B1", bitT),
- ("Numeral.Bit", binT --> bitT --> binT),
- ("Numeral.Pls", binT),
- ("Numeral.Min", binT),
- ("Numeral.number_of", binT --> iT),
- ("Numeral.number_of", binT --> nT),
+ ("Numeral.Bit", iT --> bitT --> iT),
+ ("Numeral.Pls", iT),
+ ("Numeral.Min", iT),
+ ("Numeral.number_of", iT --> iT),
+ ("Numeral.number_of", iT --> nT),
("0", nT),
("0", iT),
("1", nT),
--- a/src/HOL/Library/Word.thy Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Library/Word.thy Wed Sep 06 13:48:02 2006 +0200
@@ -2513,92 +2513,12 @@
lemma "nat_to_bv (number_of Numeral.Pls) = []"
by simp
-(***NO LONGER WORKS
consts
- fast_nat_to_bv_helper :: "bin => bit list => bit list"
+ fast_bv_to_nat_helper :: "[bit list, int] => int"
primrec
- fast_nat_to_bv_Pls: "fast_nat_to_bv_helper Numeral.Pls res = res"
- fast_nat_to_bv_Bit: "fast_nat_to_bv_helper (w BIT b) res = fast_nat_to_bv_helper w ((if b then \<one> else \<zero>) # res)"
-
-lemma fast_nat_to_bv_def:
- assumes pos_w: "(0::int) \<le> number_of w"
- shows "nat_to_bv (number_of w) == norm_unsigned (fast_nat_to_bv_helper w [])"
-proof -
- have h [rule_format]: "(0::int) \<le> number_of w ==> \<forall> l. norm_unsigned (nat_to_bv_helper (number_of w) l) = norm_unsigned (fast_nat_to_bv_helper w l)"
- proof (induct w,simp add: nat_to_bv_helper.simps,simp)
- fix bin b
- assume ind: "(0::int) \<le> number_of bin ==> \<forall> l. norm_unsigned (nat_to_bv_helper (number_of bin) l) = norm_unsigned (fast_nat_to_bv_helper bin l)"
- def qq == "number_of bin::int"
- assume posbb: "(0::int) \<le> number_of (bin BIT b)"
- hence indq [rule_format]: "\<forall> l. norm_unsigned (nat_to_bv_helper qq l) = norm_unsigned (fast_nat_to_bv_helper bin l)"
- apply (unfold qq_def)
- apply (rule ind)
- apply simp
- done
- from posbb
- have "0 \<le> qq"
- by (simp add: qq_def)
- with posbb
- show "\<forall> l. norm_unsigned (nat_to_bv_helper (number_of (bin BIT b)) l) = norm_unsigned (fast_nat_to_bv_helper (bin BIT b) l)"
- apply (subst pos_number_of)
- apply safe
- apply (fold qq_def)
- apply (cases "qq = 0")
- apply (simp add: nat_to_bv_helper.simps)
- apply (subst indq [symmetric])
- apply (subst indq [symmetric])
- apply (simp add: nat_to_bv_helper.simps)
- apply (subgoal_tac "0 < qq")
- prefer 2
- apply simp
- apply simp
- apply (subst indq [symmetric])
- apply (subst indq [symmetric])
- apply auto
- apply (simp only: nat_to_bv_helper.simps [of "2 * qq + 1"])
- apply simp
- apply safe
- apply (subgoal_tac "2 * qq + 1 ~= 2 * q")
- apply simp
- apply arith
- apply (subgoal_tac "(2 * qq + 1) div 2 = qq")
- apply simp
- apply (subst zdiv_zadd1_eq,simp)
- apply (simp only: nat_to_bv_helper.simps [of "2 * qq"])
- apply simp
- done
- qed
- from pos_w
- have "nat_to_bv (number_of w) = norm_unsigned (nat_to_bv (number_of w))"
- by simp
- also have "... = norm_unsigned (fast_nat_to_bv_helper w [])"
- apply (unfold nat_to_bv_def)
- apply (rule h)
- apply (rule pos_w)
- done
- finally show "nat_to_bv (number_of w) == norm_unsigned (fast_nat_to_bv_helper w [])"
- by simp
-qed
-
-lemma fast_nat_to_bv_Bit0: "fast_nat_to_bv_helper (w BIT False) res = fast_nat_to_bv_helper w (\<zero> # res)"
- by simp
-
-lemma fast_nat_to_bv_Bit1: "fast_nat_to_bv_helper (w BIT True) res = fast_nat_to_bv_helper w (\<one> # res)"
- by simp
-
-declare fast_nat_to_bv_Bit [simp del]
-declare fast_nat_to_bv_Bit0 [simp]
-declare fast_nat_to_bv_Bit1 [simp]
-****)
-
-
-consts
- fast_bv_to_nat_helper :: "[bit list, bin] => bin"
-
-primrec
- fast_bv_to_nat_Nil: "fast_bv_to_nat_helper [] bin = bin"
- fast_bv_to_nat_Cons: "fast_bv_to_nat_helper (b#bs) bin = fast_bv_to_nat_helper bs (bin BIT (bit_case bit.B0 bit.B1 b))"
+ fast_bv_to_nat_Nil: "fast_bv_to_nat_helper [] k = k"
+ fast_bv_to_nat_Cons: "fast_bv_to_nat_helper (b#bs) k = fast_bv_to_nat_helper bs (k BIT (bit_case bit.B0 bit.B1 b))"
lemma fast_bv_to_nat_Cons0: "fast_bv_to_nat_helper (\<zero>#bs) bin = fast_bv_to_nat_helper bs (bin BIT bit.B0)"
by simp
--- a/src/HOL/Library/word_setup.ML Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Library/word_setup.ML Wed Sep 06 13:48:02 2006 +0200
@@ -27,7 +27,7 @@
val fast2_th = PureThy.get_thm thy (Name "Word.fast_bv_to_nat_def")
(*lcp** fun f sg thms (Const("Word.nat_to_bv",_) $ (Const("Numeral.number_of",_) $ t)) =
if num_is_usable t
- then SOME (Drule.cterm_instantiate [(cterm_of sg (Var(("w",0),Type("Numeral.bin",[]))),cterm_of sg t)] fast1_th)
+ then SOME (Drule.cterm_instantiate [(cterm_of sg (Var(("w",0),Type("IntDef.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/Matrix/cplex/FloatSparseMatrixBuilder.ML Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML Wed Sep 06 13:48:02 2006 +0200
@@ -32,7 +32,7 @@
val v_only_elem : vector -> int option
val v_fold : ('a * (int * string) -> 'a) -> 'a -> vector -> 'a
val m_fold : ('a * (int * vector) -> 'a) -> 'a -> matrix -> 'a
-
+
val transpose_matrix : matrix -> matrix
val cut_vector : int -> vector -> vector
@@ -80,53 +80,27 @@
val Cons_spvec_const = Const (term_Cons, spvec_elemT --> spvecT --> spvecT)
val Cons_spmat_const = Const (term_Cons, spmat_elemT --> spmatT --> spmatT)
-
+
val float_const = Float.float_const
-(*val float_const = Const (readterm "float", HOLogic.mk_prodT (HOLogic.intT, HOLogic.intT) --> HOLogic.realT)*)
-
val zero = IntInf.fromInt 0
val minus_one = IntInf.fromInt ~1
val two = IntInf.fromInt 2
-
+
val mk_intinf = Float.mk_intinf
-(* let
- fun mk_bit n = if n = zero then HOLogic.false_const else HOLogic.true_const
-
- fun bin_of n =
- if n = zero then HOLogic.pls_const
- else if n = minus_one then HOLogic.min_const
- else
- let
- (*val (q,r) = IntInf.divMod (n, two): doesn't work in SML 10.0.7, but in newer versions!!!*)
- val q = IntInf.div (n, two)
- val r = IntInf.mod (n, two)
- in
- HOLogic.bit_const $ bin_of q $ mk_bit r
- end
- in
- HOLogic.number_of_const ty $ (bin_of n)
- end*)
val mk_float = Float.mk_float
-(* float_const $ (HOLogic.mk_prod ((mk_intinf HOLogic.intT a), (mk_intinf HOLogic.intT b)))*)
fun float2cterm (a,b) = cterm_of sg (mk_float (a,b))
fun approx_value_term prec f = Float.approx_float prec (fn (x, y) => (f x, f y))
-(* let
- val (flower, fupper) = ExactFloatingPoint.approx_decstr_by_bin prec value
- val (flower, fupper) = (f flower, f fupper)
- in
- (mk_float flower, mk_float fupper)
- end*)
fun approx_value prec pprt value =
- let
- val (flower, fupper) = approx_value_term prec pprt value
- in
- (cterm_of sg flower, cterm_of sg fupper)
- end
+ let
+ val (flower, fupper) = approx_value_term prec pprt value
+ in
+ (cterm_of sg flower, cterm_of sg fupper)
+ end
fun sign_term t = cterm_of sg t
--- a/src/HOL/Matrix/cplex/MatrixLP.ML Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Matrix/cplex/MatrixLP.ML Wed Sep 06 13:48:02 2006 +0200
@@ -16,15 +16,15 @@
structure MatrixLP : MATRIX_LP =
struct
-val sg = sign_of (theory "MatrixLP")
+val thy = theory "MatrixLP";
-fun inst_real thm = standard (Thm.instantiate ([(ctyp_of sg (TVar (hd (term_tvars (prop_of thm)))),
- ctyp_of sg HOLogic.realT)], []) thm)
+fun inst_real thm = standard (Thm.instantiate ([(ctyp_of thy (TVar (hd (term_tvars (prop_of thm)))),
+ ctyp_of thy HOLogic.realT)], []) thm)
fun lp_dual_estimate_prt_primitive (y, (A1, A2), (c1, c2), b, (r1, r2)) =
let
val th = inst_real (thm "SparseMatrix.spm_mult_le_dual_prts_no_let")
- fun var s x = (cterm_of sg (Var ((s,0), FloatSparseMatrixBuilder.real_spmatT)), x)
+ fun var s x = (cterm_of thy (Var ((s,0), FloatSparseMatrixBuilder.real_spmatT)), x)
val th = Thm.instantiate ([], [var "A1" A1, var "A2" A2, var "y" y, var "c1" c1, var "c2" c2,
var "r1" r1, var "r2" r2, var "b" b]) th
in
@@ -43,8 +43,8 @@
in
lp_dual_estimate_prt_primitive certificate
end
-
-fun read_ct s = read_cterm sg (s, TypeInfer.logicT);
+
+fun read_ct s = read_cterm thy (s, TypeInfer.logicT);
fun is_meta_eq th =
let
@@ -56,19 +56,19 @@
fun prep ths = (Library.filter is_meta_eq ths) @ (map (standard o mk_meta_eq) (Library.filter (not o is_meta_eq) ths))
-fun make ths = Compute.basic_make sg ths
+fun make ths = Compute.basic_make thy ths
fun inst_tvar ty thm =
let
val ord = prod_ord (prod_ord string_ord int_ord) (list_ord string_ord)
val v = TVar (hd (sort ord (term_tvars (prop_of thm))))
in
- standard (Thm.instantiate ([(ctyp_of sg v, ctyp_of sg ty)], []) thm)
+ standard (Thm.instantiate ([(ctyp_of thy v, ctyp_of thy ty)], []) thm)
end
fun inst_tvars [] thms = thms
| inst_tvars (ty::tys) thms = inst_tvars tys (map (inst_tvar ty) thms)
-
+
val matrix_compute =
let
val spvecT = FloatSparseMatrixBuilder.real_spvecT
@@ -117,8 +117,8 @@
matrix_simplify th
end
-fun realFromStr s = valOf (Real.fromString s)
-fun float2real (x,y) = (realFromStr x) * (Math.pow (2.0, realFromStr y))
+val realFromStr = the o Real.fromString;
+fun float2real (x, y) = realFromStr x * Math.pow (2.0, realFromStr y);
end
--- a/src/HOL/Presburger.thy Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Presburger.thy Wed Sep 06 13:48:02 2006 +0200
@@ -992,7 +992,8 @@
lemma not_true_eq_false: "(~ True) = False" by simp
-lemma int_eq_number_of_eq: "(((number_of v)::int)=(number_of w)) = iszero ((number_of (bin_add v (bin_minus w)))::int)"
+lemma int_eq_number_of_eq:
+ "(((number_of v)::int) = (number_of w)) = iszero ((number_of (v + (uminus w)))::int)"
by simp
lemma int_iszero_number_of_Pls: "iszero (Numeral0::int)"
by (simp only: iszero_number_of_Pls)
@@ -1006,7 +1007,7 @@
lemma int_iszero_number_of_1: "\<not> iszero ((number_of (w BIT bit.B1))::int)"
by simp
-lemma int_less_number_of_eq_neg: "(((number_of x)::int) < number_of y) = neg ((number_of (bin_add x (bin_minus y)))::int)"
+lemma int_less_number_of_eq_neg: "(((number_of x)::int) < number_of y) = neg ((number_of (x + (uminus y)))::int)"
by simp
lemma int_not_neg_number_of_Pls: "\<not> (neg (Numeral0::int))"
@@ -1018,18 +1019,20 @@
lemma int_neg_number_of_BIT: "neg ((number_of (w BIT x))::int) = neg ((number_of w)::int)"
by simp
-lemma int_le_number_of_eq: "(((number_of x)::int) \<le> number_of y) = (\<not> neg ((number_of (bin_add y (bin_minus x)))::int))"
+lemma int_le_number_of_eq: "(((number_of x)::int) \<le> number_of y) = (\<not> neg ((number_of (y + (uminus x)))::int))"
by simp
-lemma int_number_of_add_sym: "((number_of v)::int) + number_of w = number_of (bin_add v w)"
+lemma int_number_of_add_sym: "((number_of v)::int) + number_of w = number_of (v + w)"
by simp
-lemma int_number_of_diff_sym: "((number_of v)::int) - number_of w = number_of (bin_add v (bin_minus w))"
+lemma int_number_of_diff_sym:
+ "((number_of v)::int) - number_of w = number_of (v + (uminus w))"
by simp
-lemma int_number_of_mult_sym: "((number_of v)::int) * number_of w = number_of (bin_mult v w)"
+lemma int_number_of_mult_sym:
+ "((number_of v)::int) * number_of w = number_of (v * w)"
by simp
-lemma int_number_of_minus_sym: "- ((number_of v)::int) = number_of (bin_minus v)"
+lemma int_number_of_minus_sym: "- ((number_of v)::int) = number_of (uminus v)"
by simp
lemma add_left_zero: "0 + a = (a::'a::comm_monoid_add)"
by simp
--- a/src/HOL/Real/Float.ML Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Real/Float.ML Wed Sep 06 13:48:02 2006 +0200
@@ -7,9 +7,9 @@
sig
exception Destruct_floatstr of string
val destruct_floatstr : (char -> bool) -> (char -> bool) -> string -> bool * string * string * bool * string
-
+
exception Floating_point of string
-
+
type floatrep = IntInf.int * IntInf.int
val approx_dec_by_bin : IntInf.int -> floatrep -> floatrep * floatrep
val approx_decstr_by_bin : int -> string -> floatrep * floatrep
@@ -351,23 +351,19 @@
exception Dest_float;
fun mk_intinf ty n =
- let
- fun mk_bit n = if n = zero then HOLogic.B0_const else HOLogic.B1_const
-
- fun bin_of n =
- if n = zero then HOLogic.pls_const
- else if n = minus_one then HOLogic.min_const
- else
- let
- (*val (q,r) = IntInf.divMod (n, two): doesn't work in SML 10.0.7, but in newer versions!!!*)
- val q = IntInf.div (n, two)
- val r = IntInf.mod (n, two)
- in
- HOLogic.bit_const $ bin_of q $ mk_bit r
- end
- in
- HOLogic.number_of_const ty $ (bin_of n)
- end
+ let
+ fun mk_bit n = if n = zero then HOLogic.B0_const else HOLogic.B1_const
+ fun bin_of n =
+ if n = zero then HOLogic.pls_const
+ else if n = minus_one then HOLogic.min_const
+ else let
+ val (q,r) = IntInf.divMod (n, two)
+ in
+ HOLogic.bit_const $ bin_of q $ mk_bit r
+ end
+ in
+ HOLogic.number_of_const ty $ (bin_of n)
+ end
fun dest_intinf n =
let
--- a/src/HOL/Real/Float.thy Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Real/Float.thy Wed Sep 06 13:48:02 2006 +0200
@@ -3,7 +3,9 @@
Author: Steven Obua
*)
-theory Float imports Real begin
+theory Float
+imports Real
+begin
definition
pow2 :: "int \<Rightarrow> real"
@@ -177,7 +179,7 @@
ultimately show ?thesis by auto
qed
-lemma real_is_int_number_of[simp]: "real_is_int ((number_of::bin\<Rightarrow>real) x)"
+lemma real_is_int_number_of[simp]: "real_is_int ((number_of \<Colon> int \<Rightarrow> real) x)"
proof -
have neg1: "real_is_int (-1::real)"
proof -
@@ -187,11 +189,9 @@
qed
{
- fix x::int
- have "!! y. real_is_int ((number_of::bin\<Rightarrow>real) (Abs_Bin x))"
- apply (simp add: number_of_eq)
- apply (subst Abs_Bin_inverse)
- apply (simp add: Bin_def)
+ fix x :: int
+ have "real_is_int ((number_of \<Colon> int \<Rightarrow> real) x)"
+ unfolding number_of_eq
apply (induct x)
apply (induct_tac n)
apply (simp)
@@ -212,13 +212,13 @@
}
note Abs_Bin = this
{
- fix x :: bin
- have "? u. x = Abs_Bin u"
- apply (rule exI[where x = "Rep_Bin x"])
- apply (simp add: Rep_Bin_inverse)
+ fix x :: int
+ have "? u. x = u"
+ apply (rule exI[where x = "x"])
+ apply (simp)
done
}
- then obtain u::int where "x = Abs_Bin u" by auto
+ then obtain u::int where "x = u" by auto
with Abs_Bin show ?thesis by auto
qed
@@ -448,17 +448,17 @@
lemma not_true_eq_false: "(~ True) = False" by simp
-
lemmas binarith =
Pls_0_eq Min_1_eq
- bin_pred_Pls bin_pred_Min bin_pred_1 bin_pred_0
- bin_succ_Pls bin_succ_Min bin_succ_1 bin_succ_0
- bin_add_Pls bin_add_Min bin_add_BIT_0 bin_add_BIT_10
- bin_add_BIT_11 bin_minus_Pls bin_minus_Min bin_minus_1
- bin_minus_0 bin_mult_Pls bin_mult_Min bin_mult_1 bin_mult_0
- bin_add_Pls_right bin_add_Min_right
+ 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
-lemma int_eq_number_of_eq: "(((number_of v)::int)=(number_of w)) = iszero ((number_of (bin_add v (bin_minus w)))::int)"
+lemma int_eq_number_of_eq:
+ "(((number_of v)::int)=(number_of w)) = iszero ((number_of (v + uminus w))::int)"
by simp
lemma int_iszero_number_of_Pls: "iszero (Numeral0::int)"
@@ -473,7 +473,7 @@
lemma int_iszero_number_of_1: "\<not> iszero ((number_of (w BIT bit.B1))::int)"
by simp
-lemma int_less_number_of_eq_neg: "(((number_of x)::int) < number_of y) = neg ((number_of (bin_add x (bin_minus y)))::int)"
+lemma int_less_number_of_eq_neg: "(((number_of x)::int) < number_of y) = neg ((number_of (x + (uminus y)))::int)"
by simp
lemma int_not_neg_number_of_Pls: "\<not> (neg (Numeral0::int))"
@@ -485,7 +485,7 @@
lemma int_neg_number_of_BIT: "neg ((number_of (w BIT x))::int) = neg ((number_of w)::int)"
by simp
-lemma int_le_number_of_eq: "(((number_of x)::int) \<le> number_of y) = (\<not> neg ((number_of (bin_add y (bin_minus x)))::int))"
+lemma int_le_number_of_eq: "(((number_of x)::int) \<le> number_of y) = (\<not> neg ((number_of (y + (uminus x)))::int))"
by simp
lemmas intarithrel =
@@ -494,16 +494,16 @@
lift_bool[OF int_iszero_number_of_1] int_less_number_of_eq_neg nlift_bool[OF int_not_neg_number_of_Pls] lift_bool[OF int_neg_number_of_Min]
int_neg_number_of_BIT int_le_number_of_eq
-lemma int_number_of_add_sym: "((number_of v)::int) + number_of w = number_of (bin_add v w)"
+lemma int_number_of_add_sym: "((number_of v)::int) + number_of w = number_of (v + w)"
by simp
-lemma int_number_of_diff_sym: "((number_of v)::int) - number_of w = number_of (bin_add v (bin_minus w))"
+lemma int_number_of_diff_sym: "((number_of v)::int) - number_of w = number_of (v + (uminus w))"
by simp
-lemma int_number_of_mult_sym: "((number_of v)::int) * number_of w = number_of (bin_mult v w)"
+lemma int_number_of_mult_sym: "((number_of v)::int) * number_of w = number_of (v * w)"
by simp
-lemma int_number_of_minus_sym: "- ((number_of v)::int) = number_of (bin_minus v)"
+lemma int_number_of_minus_sym: "- ((number_of v)::int) = number_of (uminus v)"
by simp
lemmas intarith = int_number_of_add_sym int_number_of_minus_sym int_number_of_diff_sym int_number_of_mult_sym
--- a/src/HOL/Real/Rational.thy Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Real/Rational.thy Wed Sep 06 13:48:02 2006 +0200
@@ -451,7 +451,7 @@
instance rat :: number ..
defs (overloaded)
- rat_number_of_def: "(number_of w :: rat) == of_int (Rep_Bin w)"
+ rat_number_of_def: "(number_of w :: rat) == of_int w"
--{*the type constraint is essential!*}
instance rat :: number_ring
--- a/src/HOL/Real/RealDef.thy Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Real/RealDef.thy Wed Sep 06 13:48:02 2006 +0200
@@ -922,7 +922,7 @@
instance real :: number ..
defs (overloaded)
- real_number_of_def: "(number_of w :: real) == of_int (Rep_Bin w)"
+ real_number_of_def: "(number_of w :: real) == of_int w"
--{*the type constraint is essential!*}
instance real :: number_ring
--- a/src/HOL/Real/ferrante_rackoff.ML Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Real/ferrante_rackoff.ML Wed Sep 06 13:48:02 2006 +0200
@@ -21,12 +21,12 @@
val nT = HOLogic.natT;
val binarith = map thm
["Pls_0_eq", "Min_1_eq",
- "bin_pred_Pls","bin_pred_Min","bin_pred_1","bin_pred_0",
- "bin_succ_Pls", "bin_succ_Min", "bin_succ_1", "bin_succ_0",
- "bin_add_Pls", "bin_add_Min", "bin_add_BIT_0", "bin_add_BIT_10",
- "bin_add_BIT_11", "bin_minus_Pls", "bin_minus_Min", "bin_minus_1",
- "bin_minus_0", "bin_mult_Pls", "bin_mult_Min", "bin_mult_1", "bin_mult_0",
- "bin_add_Pls_right", "bin_add_Min_right"];
+ "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_1", "mult_0",
+ "add_Pls_right", "add_Min_right"];
val intarithrel =
(map thm ["int_eq_number_of_eq","int_neg_number_of_BIT",
"int_le_number_of_eq","int_iszero_number_of_0",
--- a/src/HOL/Tools/Presburger/presburger.ML Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Tools/Presburger/presburger.ML Wed Sep 06 13:48:02 2006 +0200
@@ -33,12 +33,12 @@
val presburger_ss = simpset ();
val binarith = map thm
["Pls_0_eq", "Min_1_eq",
- "bin_pred_Pls","bin_pred_Min","bin_pred_1","bin_pred_0",
- "bin_succ_Pls", "bin_succ_Min", "bin_succ_1", "bin_succ_0",
- "bin_add_Pls", "bin_add_Min", "bin_add_BIT_0", "bin_add_BIT_10",
- "bin_add_BIT_11", "bin_minus_Pls", "bin_minus_Min", "bin_minus_1",
- "bin_minus_0", "bin_mult_Pls", "bin_mult_Min", "bin_mult_1", "bin_mult_0",
- "bin_add_Pls_right", "bin_add_Min_right"];
+ "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"];
val intarithrel =
(map thm ["int_eq_number_of_eq","int_neg_number_of_BIT",
"int_le_number_of_eq","int_iszero_number_of_0",
@@ -116,7 +116,6 @@
val bT = HOLogic.boolT;
val bitT = HOLogic.bitT;
val iT = HOLogic.intT;
-val binT = HOLogic.binT;
val nT = HOLogic.natT;
(* Allowed Consts in formulae for presburger tactic*)
@@ -162,11 +161,11 @@
("Numeral.bit.B0", bitT),
("Numeral.bit.B1", bitT),
- ("Numeral.Bit", binT --> bitT --> binT),
- ("Numeral.Pls", binT),
- ("Numeral.Min", binT),
- ("Numeral.number_of", binT --> iT),
- ("Numeral.number_of", binT --> nT),
+ ("Numeral.Bit", iT --> bitT --> iT),
+ ("Numeral.Pls", iT),
+ ("Numeral.Min", iT),
+ ("Numeral.number_of", iT --> iT),
+ ("Numeral.number_of", iT --> nT),
("0", nT),
("0", iT),
("1", nT),
--- a/src/HOL/arith_data.ML Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/arith_data.ML Wed Sep 06 13:48:02 2006 +0200
@@ -680,7 +680,7 @@
end
(* "?P ((?n::int) mod (number_of ?k)) =
((iszero (number_of ?k) --> ?P ?n) &
- (neg (number_of (bin_minus ?k)) -->
+ (neg (number_of (uminus ?k)) -->
(ALL i j. 0 <= j & j < number_of ?k & ?n = number_of ?k * i + j --> ?P j)) &
(neg (number_of ?k) -->
(ALL i j. number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j --> ?P j))) *)
@@ -699,8 +699,8 @@
val iszero_t2 = Const ("IntDef.iszero", split_type --> HOLogic.boolT) $ t2
val neg_minus_k = Const ("IntDef.neg", split_type --> HOLogic.boolT) $
(number_of $
- (Const ("Numeral.bin_minus",
- HOLogic.binT --> HOLogic.binT) $ k'))
+ (Const ("HOL.uminus",
+ HOLogic.intT --> HOLogic.intT) $ k'))
val zero_leq_j = Const ("Orderings.less_eq",
split_type --> split_type --> HOLogic.boolT) $ zero $ j
val j_lt_t2 = Const ("Orderings.less",
@@ -732,7 +732,7 @@
end
(* "?P ((?n::int) div (number_of ?k)) =
((iszero (number_of ?k) --> ?P 0) &
- (neg (number_of (bin_minus ?k)) -->
+ (neg (number_of (uminus ?k)) -->
(ALL i. (EX j. 0 <= j & j < number_of ?k & ?n = number_of ?k * i + j) --> ?P i)) &
(neg (number_of ?k) -->
(ALL i. (EX j. number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j) --> ?P i))) *)
@@ -751,8 +751,8 @@
val iszero_t2 = Const ("IntDef.iszero", split_type --> HOLogic.boolT) $ t2
val neg_minus_k = Const ("IntDef.neg", split_type --> HOLogic.boolT) $
(number_of $
- (Const ("Numeral.bin_minus",
- HOLogic.binT --> HOLogic.binT) $ k'))
+ (Const ("Numeral.uminus",
+ HOLogic.intT --> HOLogic.intT) $ k'))
val zero_leq_j = Const ("Orderings.less_eq",
split_type --> split_type --> HOLogic.boolT) $ zero $ j
val j_lt_t2 = Const ("Orderings.less",
--- a/src/HOL/ex/Abstract_NAT.thy Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/ex/Abstract_NAT.thy Wed Sep 06 13:48:02 2006 +0200
@@ -11,6 +11,8 @@
text {* Axiomatic Natural Numbers (Peano) -- a monomorphic theory. *}
+hide (open) const succ
+
locale NAT =
fixes zero :: 'n
and succ :: "'n \<Rightarrow> 'n"
--- a/src/HOL/hologic.ML Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/hologic.ML Wed Sep 06 13:48:02 2006 +0200
@@ -76,7 +76,6 @@
val bitT: typ
val B0_const: term
val B1_const: term
- val binT: typ
val pls_const: term
val min_const: term
val bit_const: term
@@ -280,26 +279,25 @@
| dest_nat t = raise TERM ("dest_nat", [t]);
-(* binary numerals *)
+(* binary numerals and int *)
-val binT = Type ("Numeral.bin", []);
-
+val intT = Type ("IntDef.int", []);
val bitT = Type ("Numeral.bit", []);
val B0_const = Const ("Numeral.bit.B0", bitT);
val B1_const = Const ("Numeral.bit.B1", bitT);
-val pls_const = Const ("Numeral.Pls", binT)
-and min_const = Const ("Numeral.Min", binT)
-and bit_const = Const ("Numeral.Bit", [binT, bitT] ---> binT);
+val pls_const = Const ("Numeral.Pls", intT)
+and min_const = Const ("Numeral.Min", intT)
+and bit_const = Const ("Numeral.Bit", [intT, bitT] ---> intT);
-fun number_of_const T = Const ("Numeral.number_of", binT --> T);
+fun number_of_const T = Const ("Numeral.number_of", intT --> T);
fun int_of [] = 0
| int_of (b :: bs) = IntInf.fromInt b + (2 * int_of bs);
(*When called from a print translation, the Numeral qualifier will probably have
- been removed from Bit, bin.B0, etc.*)
+ been removed from Bit, bit.B0, etc.*)
fun dest_bit (Const ("Numeral.bit.B0", _)) = 0
| dest_bit (Const ("Numeral.bit.B1", _)) = 1
| dest_bit (Const ("bit.B0", _)) = 0
@@ -334,11 +332,6 @@
in bit_const $ bin_of q $ mk_bit r end;
in bin_of n end;
-
-(* int *)
-
-val intT = Type ("IntDef.int", []);
-
fun mk_int 0 = Const ("0", intT)
| mk_int 1 = Const ("1", intT)
| mk_int i = number_of_const intT $ mk_binum i;
--- a/src/Pure/Tools/codegen_package.ML Wed Sep 06 10:01:27 2006 +0200
+++ b/src/Pure/Tools/codegen_package.ML Wed Sep 06 13:48:02 2006 +0200
@@ -609,19 +609,18 @@
(* parametrized application generators, for instantiation in object logic *)
(* (axiomatic extensions of extraction kernel *)
-fun appgen_rep_bin int_of_numeral thy algbr thmtab strct (app as (c as (_, ty), [bin])) trns =
- case try (int_of_numeral thy) bin
+fun appgen_rep_bin int_of_numeral thy algbr thmtab strct (app as (c, ts)) trns =
+ case try (int_of_numeral thy) (list_comb (Const c, ts))
of SOME i => if i < 0 then (*preprocessor eliminates negative numerals*)
trns
|> appgen_default thy algbr thmtab (no_strict strct) app
else
trns
- |> exprgen_term thy algbr thmtab (no_strict strct) (Const c)
- ||>> exprgen_term thy algbr thmtab (no_strict strct) bin
- |-> (fn (e1, e2) => pair (CodegenThingol.INum (i, e1 `$ e2)))
+ |> appgen_default thy algbr thmtab (no_strict strct) app
+ |-> (fn e => pair (CodegenThingol.INum (i, e)))
| NONE =>
trns
- |> appgen_default thy algbr thmtab strct app;
+ |> appgen_default thy algbr thmtab (no_strict strct) app;
fun appgen_char char_to_index thy algbr thmtab strct (app as ((_, ty), _)) trns =
case (char_to_index o list_comb o apfst Const) app