New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
--- a/NEWS Sat Feb 16 16:52:09 2008 +0100
+++ b/NEWS Sun Feb 17 06:49:53 2008 +0100
@@ -35,6 +35,12 @@
*** HOL ***
+* Theory Int: The representation of numerals has changed. The infix operator
+BIT and the bit datatype with constructors B0 and B1 have disappeared.
+INCOMPATIBILITY, use "Int.Bit0 x" and "Int.Bit1 y" in place of "x BIT bit.B0"
+and "y BIT bit.B1", respectively. Theorems involving BIT, B0, or B1 have been
+renamed with "Bit0" or "Bit1" accordingly.
+
* Theory Nat: definition of <= and < on natural numbers no longer depend
on well-founded relations. INCOMPATIBILITY. Definitions le_def and less_def
have disappeared. Consider lemmas not_less [symmetric, where ?'a = nat]
--- a/src/HOL/Groebner_Basis.thy Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Groebner_Basis.thy Sun Feb 17 06:49:53 2008 +0100
@@ -179,7 +179,7 @@
if_True add_0 add_Suc add_number_of_left mult_number_of_left
numeral_1_eq_1[symmetric] Suc_eq_add_numeral_1
numeral_0_eq_0[symmetric] numerals[symmetric] not_iszero_1
- iszero_number_of_1 iszero_number_of_0 nonzero_number_of_Min
+ iszero_number_of_Bit1 iszero_number_of_Bit0 nonzero_number_of_Min
iszero_number_of_Pls iszero_0 not_iszero_Numeral1
lemmas semiring_norm = comp_arith
--- a/src/HOL/Import/HOL/HOL4Prob.thy Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Import/HOL/HOL4Prob.thy Sun Feb 17 06:49:53 2008 +0100
@@ -36,28 +36,24 @@
((op =::nat => nat => bool)
((op div::nat => nat => nat) (0::nat)
((number_of \<Colon> int => nat)
- ((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
- (bit.B0::bit))))
+ ((Int.Bit0 \<Colon> int => int)
+ ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))
(0::nat))
((op &::bool => bool => bool)
((op =::nat => nat => bool)
((op div::nat => nat => nat) (1::nat)
((number_of \<Colon> int => nat)
- ((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
- (bit.B0::bit))))
+ ((Int.Bit0 \<Colon> int => int)
+ ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))
(0::nat))
((op =::nat => nat => bool)
((op div::nat => nat => nat)
((number_of \<Colon> int => nat)
- ((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
- (bit.B0::bit)))
+ ((Int.Bit0 \<Colon> int => int)
+ ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
((number_of \<Colon> int => nat)
- ((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
- (bit.B0::bit))))
+ ((Int.Bit0 \<Colon> int => int)
+ ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))
(1::nat)))"
by (import prob_extra DIV_TWO_BASIC)
@@ -76,19 +72,16 @@
((op div::nat => nat => nat)
((op ^::nat => nat => nat)
((number_of \<Colon> int => nat)
- ((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
- (bit.B0::bit)))
+ ((Int.Bit0 \<Colon> int => int)
+ ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
((Suc::nat => nat) n))
((number_of \<Colon> int => nat)
- ((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
- (bit.B0::bit))))
+ ((Int.Bit0 \<Colon> int => int)
+ ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))
((op ^::nat => nat => nat)
((number_of \<Colon> int => nat)
- ((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
- (bit.B0::bit)))
+ ((Int.Bit0 \<Colon> int => int)
+ ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
n))"
by (import prob_extra EXP_DIV_TWO)
@@ -126,22 +119,19 @@
lemma HALF_POS: "(op <::real => real => bool) (0::real)
((op /::real => real => real) (1::real)
((number_of \<Colon> int => real)
- ((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
- (bit.B0::bit))))"
+ ((Int.Bit0 \<Colon> int => int)
+ ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))"
by (import prob_extra HALF_POS)
lemma HALF_CANCEL: "(op =::real => real => bool)
((op *::real => real => real)
((number_of \<Colon> int => real)
- ((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
- (bit.B0::bit)))
+ ((Int.Bit0 \<Colon> int => int)
+ ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
((op /::real => real => real) (1::real)
((number_of \<Colon> int => real)
- ((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
- (bit.B0::bit)))))
+ ((Int.Bit0 \<Colon> int => int)
+ ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))))
(1::real)"
by (import prob_extra HALF_CANCEL)
@@ -151,9 +141,8 @@
((op ^::real => nat => real)
((op /::real => real => real) (1::real)
((number_of \<Colon> int => real)
- ((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
- (bit.B0::bit))))
+ ((Int.Bit0 \<Colon> int => int)
+ ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))
n))"
by (import prob_extra POW_HALF_POS)
@@ -166,18 +155,14 @@
((op ^::real => nat => real)
((op /::real => real => real) (1::real)
((number_of \<Colon> int => real)
- ((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
- (bit.B1::bit))
- (bit.B0::bit))))
+ ((Int.Bit0 \<Colon> int => int)
+ ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))
n)
((op ^::real => nat => real)
((op /::real => real => real) (1::real)
((number_of \<Colon> int => real)
- ((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
- (bit.B1::bit))
- (bit.B0::bit))))
+ ((Int.Bit0 \<Colon> int => int)
+ ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))
m))))"
by (import prob_extra POW_HALF_MONO)
@@ -187,22 +172,18 @@
((op ^::real => nat => real)
((op /::real => real => real) (1::real)
((number_of \<Colon> int => real)
- ((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
- (bit.B0::bit))))
+ ((Int.Bit0 \<Colon> int => int)
+ ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))
n)
((op *::real => real => real)
((number_of \<Colon> int => real)
- ((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
- (bit.B0::bit)))
+ ((Int.Bit0 \<Colon> int => int)
+ ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
((op ^::real => nat => real)
((op /::real => real => real) (1::real)
((number_of \<Colon> int => real)
- ((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
- (bit.B1::bit))
- (bit.B0::bit))))
+ ((Int.Bit0 \<Colon> int => int)
+ ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))
((Suc::nat => nat) n))))"
by (import prob_extra POW_HALF_TWICE)
@@ -228,22 +209,19 @@
((op -::real => real => real) (1::real)
((op /::real => real => real) (1::real)
((number_of \<Colon> int => real)
- ((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
- (bit.B0::bit)))))
+ ((Int.Bit0 \<Colon> int => int)
+ ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))))
((op /::real => real => real) (1::real)
((number_of \<Colon> int => real)
- ((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
- (bit.B0::bit))))"
+ ((Int.Bit0 \<Colon> int => int)
+ ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))"
by (import prob_extra ONE_MINUS_HALF)
lemma HALF_LT_1: "(op <::real => real => bool)
((op /::real => real => real) (1::real)
((number_of \<Colon> int => real)
- ((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
- (bit.B0::bit))))
+ ((Int.Bit0 \<Colon> int => int)
+ ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))
(1::real)"
by (import prob_extra HALF_LT_1)
@@ -253,18 +231,15 @@
((op ^::real => nat => real)
((op /::real => real => real) (1::real)
((number_of \<Colon> int => real)
- ((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
- (bit.B0::bit))))
+ ((Int.Bit0 \<Colon> int => int)
+ ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))
n)
((inverse::real => real)
((real::nat => real)
((op ^::nat => nat => nat)
((number_of \<Colon> int => nat)
- ((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
- (bit.B1::bit))
- (bit.B0::bit)))
+ ((Int.Bit0 \<Colon> int => int)
+ ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
n))))"
by (import prob_extra POW_HALF_EXP)
@@ -1406,27 +1381,22 @@
((op ^::real => nat => real)
((op /::real => real => real) (1::real)
((number_of \<Colon> int => real)
- ((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
- (bit.B1::bit))
- (bit.B0::bit))))
+ ((Int.Bit0 \<Colon> int => int)
+ ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))
((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 \<Colon> int => real)
- ((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
- (bit.B1::bit))
- (bit.B0::bit))))
+ ((Int.Bit0 \<Colon> int => int)
+ ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))
((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 \<Colon> int => real)
- ((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
- (bit.B0::bit))))
+ ((Int.Bit0 \<Colon> int => int)
+ ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))
((size::bool list => nat) l)))"
by (import prob ALG_TWINS_MEASURE)
--- a/src/HOL/Import/HOL/HOL4Real.thy Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Import/HOL/HOL4Real.thy Sun Feb 17 06:49:53 2008 +0100
@@ -526,9 +526,8 @@
((op <=::real => real => bool) (1::real)
((op ^::real => nat => real) x
((number_of \<Colon> int => nat)
- ((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
- (bit.B0::bit))))))"
+ ((Int.Bit0 \<Colon> int => int)
+ ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))))"
by (import real REAL_LE1_POW2)
lemma REAL_LT1_POW2: "(All::(real => bool) => bool)
@@ -538,9 +537,8 @@
((op <::real => real => bool) (1::real)
((op ^::real => nat => real) x
((number_of \<Colon> int => nat)
- ((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
- (bit.B0::bit))))))"
+ ((Int.Bit0 \<Colon> int => int)
+ ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))))"
by (import real REAL_LT1_POW2)
lemma POW_POS_LT: "ALL (x::real) n::nat. 0 < x --> 0 < x ^ Suc n"
--- a/src/HOL/Import/HOL/HOL4Vec.thy Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Import/HOL/HOL4Vec.thy Sun Feb 17 06:49:53 2008 +0100
@@ -1283,9 +1283,8 @@
(op -->::bool => bool => bool)
((op <::nat => nat => bool) x
((number_of \<Colon> int => nat)
- ((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
- (bit.B0::bit))))
+ ((Int.Bit0 \<Colon> int => int)
+ ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))
((op =::nat => nat => bool) ((BV::bool => nat) ((VB::nat => bool) x))
x))"
by (import bword_num BV_VB)
@@ -1500,10 +1499,9 @@
((BV::bool => nat) cin))
((op ^::nat => nat => nat)
((number_of \<Colon> int => nat)
- ((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int)
- (Int.Pls \<Colon> int) (bit.B1::bit))
- (bit.B0::bit)))
+ ((Int.Bit0 \<Colon> int => int)
+ ((Int.Bit1 \<Colon> int => int)
+ (Int.Pls \<Colon> int))))
k)))))))"
by (import bword_arith ACARRY_EQ_ADD_DIV)
--- a/src/HOL/Import/HOL/HOL4Word32.thy Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Import/HOL/HOL4Word32.thy Sun Feb 17 06:49:53 2008 +0100
@@ -117,9 +117,8 @@
(op <::nat => nat => bool) (0::nat)
((op ^::nat => nat => nat)
((number_of \<Colon> int => nat)
- ((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
- (bit.B0::bit)))
+ ((Int.Bit0 \<Colon> int => int)
+ ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
n))"
by (import bits ZERO_LT_TWOEXP)
@@ -137,17 +136,13 @@
((op <::nat => nat => bool)
((op ^::nat => nat => nat)
((number_of \<Colon> int => nat)
- ((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
- (bit.B1::bit))
- (bit.B0::bit)))
+ ((Int.Bit0 \<Colon> int => int)
+ ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
a)
((op ^::nat => nat => nat)
((number_of \<Colon> int => nat)
- ((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
- (bit.B1::bit))
- (bit.B0::bit)))
+ ((Int.Bit0 \<Colon> int => int)
+ ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
b))))"
by (import bits TWOEXP_MONO)
@@ -159,17 +154,13 @@
((op <=::nat => nat => bool)
((op ^::nat => nat => nat)
((number_of \<Colon> int => nat)
- ((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
- (bit.B1::bit))
- (bit.B0::bit)))
+ ((Int.Bit0 \<Colon> int => int)
+ ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
a)
((op ^::nat => nat => nat)
((number_of \<Colon> int => nat)
- ((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
- (bit.B1::bit))
- (bit.B0::bit)))
+ ((Int.Bit0 \<Colon> int => int)
+ ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
b))))"
by (import bits TWOEXP_MONO2)
@@ -180,17 +171,13 @@
(op <=::nat => nat => bool)
((op ^::nat => nat => nat)
((number_of \<Colon> int => nat)
- ((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
- (bit.B1::bit))
- (bit.B0::bit)))
+ ((Int.Bit0 \<Colon> int => int)
+ ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
((op -::nat => nat => nat) a b))
((op ^::nat => nat => nat)
((number_of \<Colon> int => nat)
- ((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
- (bit.B1::bit))
- (bit.B0::bit)))
+ ((Int.Bit0 \<Colon> int => int)
+ ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
a)))"
by (import bits EXP_SUB_LESS_EQ)
@@ -349,25 +336,19 @@
(op =::nat => nat => bool)
((op ^::nat => nat => nat)
((number_of \<Colon> int => nat)
- ((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
- (bit.B1::bit))
- (bit.B0::bit)))
+ ((Int.Bit0 \<Colon> int => int)
+ ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
b)
((op *::nat => nat => nat)
((op ^::nat => nat => nat)
((number_of \<Colon> int => nat)
- ((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
- (bit.B1::bit))
- (bit.B0::bit)))
+ ((Int.Bit0 \<Colon> int => int)
+ ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
((op +::nat => nat => nat) x (1::nat)))
((op ^::nat => nat => nat)
((number_of \<Colon> int => nat)
- ((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
- (bit.B1::bit))
- (bit.B0::bit)))
+ ((Int.Bit0 \<Colon> int => int)
+ ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
a))))))"
by (import bits LESS_EXP_MULT2)
--- a/src/HOL/Int.thy Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Int.thy Sun Feb 17 06:49:53 2008 +0100
@@ -9,7 +9,7 @@
header {* The Integers as Equivalence Classes over Pairs of Natural Numbers *}
theory Int
-imports Equiv_Relations Datatype Nat Wellfounded_Relations
+imports Equiv_Relations Nat Wellfounded_Relations
uses
("Tools/numeral.ML")
("Tools/numeral_syntax.ML")
@@ -583,13 +583,6 @@
Springer LNCS 488 (240-251), 1991.
*}
-datatype bit = B0 | B1
-
-text{*
- Type @{typ bit} avoids the use of type @{typ bool}, which would make
- all of the rewrite rules higher-order.
-*}
-
definition
Pls :: int where
[code func del]: "Pls = 0"
@@ -599,8 +592,12 @@
[code func del]: "Min = - 1"
definition
- Bit :: "int \<Rightarrow> bit \<Rightarrow> int" (infixl "BIT" 90) where
- [code func del]: "k BIT b = (case b of B0 \<Rightarrow> 0 | B1 \<Rightarrow> 1) + k + k"
+ Bit0 :: "int \<Rightarrow> int" where
+ [code func del]: "Bit0 k = k + k"
+
+definition
+ Bit1 :: "int \<Rightarrow> int" where
+ [code func del]: "Bit1 k = 1 + k + k"
class number = type + -- {* for numeric types: nat, int, real, \dots *}
fixes number_of :: "int \<Rightarrow> 'a"
@@ -617,7 +614,7 @@
"Numeral0 \<equiv> number_of Pls"
abbreviation
- "Numeral1 \<equiv> number_of (Pls BIT B1)"
+ "Numeral1 \<equiv> number_of (Bit1 Pls)"
lemma Let_number_of [simp]: "Let (number_of v) f = f (number_of v)"
-- {* Unfold all @{text let}s involving constants *}
@@ -640,80 +637,80 @@
-- {* unfolding @{text minx} and @{text max} on numerals *}
lemmas numeral_simps =
- succ_def pred_def Pls_def Min_def Bit_def
+ succ_def pred_def Pls_def Min_def Bit0_def Bit1_def
text {* Removal of leading zeroes *}
-lemma Pls_0_eq [simp, code post]:
- "Pls BIT B0 = Pls"
+lemma Bit0_Pls [simp, code post]:
+ "Bit0 Pls = Pls"
unfolding numeral_simps by simp
-lemma Min_1_eq [simp, code post]:
- "Min BIT B1 = Min"
+lemma Bit1_Min [simp, code post]:
+ "Bit1 Min = Min"
unfolding numeral_simps by simp
lemmas normalize_bin_simps =
- Pls_0_eq Min_1_eq
+ Bit0_Pls Bit1_Min
subsection {* The Functions @{term succ}, @{term pred} and @{term uminus} *}
lemma succ_Pls [simp]:
- "succ Pls = Pls BIT B1"
+ "succ Pls = Bit1 Pls"
unfolding numeral_simps by simp
lemma succ_Min [simp]:
"succ Min = Pls"
unfolding numeral_simps by simp
-lemma succ_1 [simp]:
- "succ (k BIT B1) = succ k BIT B0"
+lemma succ_Bit0 [simp]:
+ "succ (Bit0 k) = Bit1 k"
unfolding numeral_simps by simp
-lemma succ_0 [simp]:
- "succ (k BIT B0) = k BIT B1"
+lemma succ_Bit1 [simp]:
+ "succ (Bit1 k) = Bit0 (succ k)"
unfolding numeral_simps by simp
lemmas succ_bin_simps =
- succ_Pls succ_Min succ_1 succ_0
+ succ_Pls succ_Min succ_Bit0 succ_Bit1
lemma pred_Pls [simp]:
"pred Pls = Min"
unfolding numeral_simps by simp
lemma pred_Min [simp]:
- "pred Min = Min BIT B0"
- unfolding numeral_simps by simp
-
-lemma pred_1 [simp]:
- "pred (k BIT B1) = k BIT B0"
+ "pred Min = Bit0 Min"
unfolding numeral_simps by simp
-lemma pred_0 [simp]:
- "pred (k BIT B0) = pred k BIT B1"
+lemma pred_Bit0 [simp]:
+ "pred (Bit0 k) = Bit1 (pred k)"
unfolding numeral_simps by simp
+lemma pred_Bit1 [simp]:
+ "pred (Bit1 k) = Bit0 k"
+ unfolding numeral_simps by simp
+
lemmas pred_bin_simps =
- pred_Pls pred_Min pred_1 pred_0
+ pred_Pls pred_Min pred_Bit0 pred_Bit1
lemma minus_Pls [simp]:
"- Pls = Pls"
unfolding numeral_simps by simp
lemma minus_Min [simp]:
- "- Min = Pls BIT B1"
+ "- Min = Bit1 Pls"
unfolding numeral_simps by simp
-lemma minus_1 [simp]:
- "- (k BIT B1) = pred (- k) BIT B1"
+lemma minus_Bit0 [simp]:
+ "- (Bit0 k) = Bit0 (- k)"
unfolding numeral_simps by simp
-lemma minus_0 [simp]:
- "- (k BIT B0) = (- k) BIT B0"
- unfolding numeral_simps by simp
+lemma minus_Bit1 [simp]:
+ "- (Bit1 k) = Bit1 (pred (- k))"
+ unfolding numeral_simps by simp
lemmas minus_bin_simps =
- minus_Pls minus_Min minus_1 minus_0
+ minus_Pls minus_Min minus_Bit0 minus_Bit1
subsection {*
@@ -729,29 +726,33 @@
"Min + k = pred k"
unfolding numeral_simps by simp
-lemma add_BIT_11 [simp]:
- "(k BIT B1) + (l BIT B1) = (k + succ l) BIT B0"
+lemma add_Bit0_Bit0 [simp]:
+ "(Bit0 k) + (Bit0 l) = Bit0 (k + l)"
+ unfolding numeral_simps by simp_all
+
+lemma add_Bit0_Bit1 [simp]:
+ "(Bit0 k) + (Bit1 l) = Bit1 (k + l)"
+ unfolding numeral_simps by simp_all
+
+lemma add_Bit1_Bit0 [simp]:
+ "(Bit1 k) + (Bit0 l) = Bit1 (k + l)"
unfolding numeral_simps by simp
-lemma add_BIT_10 [simp]:
- "(k BIT B1) + (l BIT B0) = (k + l) BIT B1"
+lemma add_Bit1_Bit1 [simp]:
+ "(Bit1 k) + (Bit1 l) = Bit0 (k + succ l)"
unfolding numeral_simps by simp
-lemma add_BIT_0 [simp]:
- "(k BIT B0) + (l BIT b) = (k + l) BIT b"
- unfolding numeral_simps by simp
-
lemma add_Pls_right [simp]:
"k + Pls = k"
unfolding numeral_simps by simp
lemma add_Min_right [simp]:
"k + Min = pred k"
- unfolding numeral_simps by simp
+ unfolding numeral_simps by simp
lemmas add_bin_simps =
- add_Pls add_Min add_BIT_0 add_BIT_10 add_BIT_11
- add_Pls_right add_Min_right
+ add_Pls add_Min add_Pls_right add_Min_right
+ add_Bit0_Bit0 add_Bit0_Bit1 add_Bit1_Bit0 add_Bit1_Bit1
lemma mult_Pls [simp]:
"Pls * w = Pls"
@@ -761,16 +762,16 @@
"Min * k = - k"
unfolding numeral_simps by simp
-lemma mult_num1 [simp]:
- "(k BIT B1) * l = ((k * l) BIT B0) + l"
- unfolding numeral_simps int_distrib by simp
+lemma mult_Bit0 [simp]:
+ "(Bit0 k) * l = Bit0 (k * l)"
+ unfolding numeral_simps int_distrib by simp
-lemma mult_num0 [simp]:
- "(k BIT B0) * l = (k * l) BIT B0"
+lemma mult_Bit1 [simp]:
+ "(Bit1 k) * l = (Bit0 (k * l)) + l"
unfolding numeral_simps int_distrib by simp
lemmas mult_bin_simps =
- mult_Pls mult_Min mult_num1 mult_num0
+ mult_Pls mult_Min mult_Bit0 mult_Bit1
subsection {* Converting Numerals to Rings: @{term number_of} *}
@@ -820,8 +821,8 @@
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)"
+lemma double_number_of_Bit0:
+ "(1 + 1) * number_of w = (number_of (Bit0 w) ::'a::number_ring)"
unfolding number_of_eq numeral_simps left_distrib by simp
text {*
@@ -877,10 +878,13 @@
"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_Bit0:
+ "number_of (Bit0 w) = (0::'a::number_ring) + (number_of w) + (number_of w)"
+ unfolding number_of_eq numeral_simps by simp
+
+lemma number_of_Bit1:
+ "number_of (Bit1 w) = (1::'a::number_ring) + (number_of w) + (number_of w)"
+ unfolding number_of_eq numeral_simps by simp
subsection {* Equality of Binary Numbers *}
@@ -979,9 +983,9 @@
qed
qed
-lemma iszero_number_of_BIT:
- "iszero (number_of (w BIT x)::'a) =
- (x = B0 \<and> iszero (number_of w::'a::{ring_char_0,number_ring}))"
+lemma iszero_number_of_Bit0:
+ "iszero (number_of (Bit0 w)::'a) =
+ iszero (number_of w::'a::{ring_char_0,number_ring})"
proof -
have "(of_int w + of_int w = (0::'a)) \<Longrightarrow> (w = 0)"
proof -
@@ -990,27 +994,24 @@
then have "w + w = 0" by (simp only: of_int_eq_iff)
then show "w = 0" by (simp only: double_eq_0_iff)
qed
- moreover have "1 + of_int w + of_int w \<noteq> (0::'a)"
+ thus ?thesis
+ by (auto simp add: iszero_def number_of_eq numeral_simps)
+qed
+
+lemma iszero_number_of_Bit1:
+ "~ iszero (number_of (Bit1 w)::'a::{ring_char_0,number_ring})"
+proof -
+ have "1 + of_int w + of_int w \<noteq> (0::'a)"
proof
assume eq: "1 + of_int w + of_int w = (0::'a)"
hence "of_int (1 + w + w) = (of_int 0 :: 'a)" by simp
hence "1 + w + w = 0" by (simp only: of_int_eq_iff)
with odd_nonzero show False by blast
qed
- ultimately show ?thesis
- by (auto simp add: iszero_def number_of_eq numeral_simps
- split: bit.split)
+ thus ?thesis
+ by (auto simp add: iszero_def number_of_eq numeral_simps)
qed
-lemma iszero_number_of_0:
- "iszero (number_of (w BIT B0) :: 'a::{ring_char_0,number_ring}) =
- iszero (number_of w :: 'a)"
- by (simp only: iszero_number_of_BIT simp_thms)
-
-lemma iszero_number_of_1:
- "~ iszero (number_of (w BIT B1)::'a::{ring_char_0,number_ring})"
- by (simp add: iszero_number_of_BIT)
-
subsection {* The Less-Than Relation *}
@@ -1056,16 +1057,20 @@
add: compare_rls of_nat_1 [symmetric] of_nat_add [symmetric])
qed
-lemma neg_number_of_BIT:
- "neg (number_of (w BIT x)::'a) =
+lemma neg_number_of_Bit0:
+ "neg (number_of (Bit0 w)::'a) =
+ neg (number_of w :: 'a::{ordered_idom,number_ring})"
+by (simp add: neg_def number_of_eq numeral_simps double_less_0_iff)
+
+lemma neg_number_of_Bit1:
+ "neg (number_of (Bit1 w)::'a) =
neg (number_of w :: 'a::{ordered_idom,number_ring})"
proof -
have "((1::'a) + of_int w + of_int w < 0) = (of_int (1 + w + w) < (of_int 0 :: 'a))"
by simp
also have "... = (w < 0)" by (simp only: of_int_less_iff odd_less_0)
finally show ?thesis
- by ( simp add: neg_def number_of_eq numeral_simps double_less_0_iff
- split: bit.split)
+ by (simp add: neg_def number_of_eq numeral_simps)
qed
@@ -1112,7 +1117,6 @@
*}
lemmas arith_simps =
- bit.distinct
normalize_bin_simps pred_bin_simps succ_bin_simps
add_bin_simps minus_bin_simps mult_bin_simps
abs_zero abs_one arith_extra_simps
@@ -1121,10 +1125,10 @@
lemmas rel_simps [simp] =
eq_number_of_eq iszero_0 nonzero_number_of_Min
- iszero_number_of_0 iszero_number_of_1
+ iszero_number_of_Bit0 iszero_number_of_Bit1
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
+ neg_number_of_Min neg_number_of_Bit0 neg_number_of_Bit1
le_number_of_eq
(* iszero_number_of_Pls would never be used
because its lhs simplifies to "iszero 0" *)
@@ -1795,7 +1799,7 @@
instance int :: eq ..
-code_datatype Pls Min Bit "number_of \<Colon> int \<Rightarrow> int"
+code_datatype Pls Min Bit0 Bit1 "number_of \<Colon> int \<Rightarrow> int"
definition
int_aux :: "nat \<Rightarrow> int \<Rightarrow> int" where
@@ -1883,7 +1887,7 @@
(*setup continues in theory Presburger*)
-hide (open) const Pls Min B0 B1 succ pred
+hide (open) const Pls Min Bit0 Bit1 succ pred
subsection {* Legacy theorems *}
--- a/src/HOL/IntDiv.thy Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/IntDiv.thy Sun Feb 17 06:49:53 2008 +0100
@@ -1062,14 +1062,18 @@
lemma not_0_le_lemma: "~ 0 \<le> x ==> x \<le> (0::int)"
by auto
-lemma zdiv_number_of_BIT[simp]:
- "number_of (v BIT b) div number_of (w BIT bit.B0) =
- (if b=bit.B0 | (0::int) \<le> number_of w
+lemma zdiv_number_of_Bit0 [simp]:
+ "number_of (Int.Bit0 v) div number_of (Int.Bit0 w) =
+ number_of v div (number_of w :: int)"
+by (simp only: number_of_eq numeral_simps) simp
+
+lemma zdiv_number_of_Bit1 [simp]:
+ "number_of (Int.Bit1 v) div number_of (Int.Bit0 w) =
+ (if (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 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)
+apply (simp add: zdiv_zmult_zmult1 pos_zdiv_mult_2 neg_zdiv_mult_2 add_ac)
done
@@ -1087,7 +1091,7 @@
apply (subst zmod_zadd1_eq)
apply (simp add: zmod_zmult_zmult2 mod_pos_pos_trivial)
apply (rule mod_pos_pos_trivial)
-apply (auto simp add: mod_pos_pos_trivial left_distrib)
+apply (auto simp add: mod_pos_pos_trivial ring_distribs)
apply (subgoal_tac "0 \<le> b mod a", arith, simp)
done
@@ -1102,14 +1106,20 @@
apply (simp only: zmod_zminus_zminus diff_minus minus_add_distrib [symmetric])
done
-lemma zmod_number_of_BIT [simp]:
- "number_of (v BIT b) mod number_of (w BIT bit.B0) =
- (case b of
- bit.B0 => 2 * (number_of v mod number_of w)
- | bit.B1 => if (0::int) \<le> number_of w
+lemma zmod_number_of_Bit0 [simp]:
+ "number_of (Int.Bit0 v) mod number_of (Int.Bit0 w) =
+ (2::int) * (number_of v mod number_of w)"
+apply (simp only: number_of_eq numeral_simps)
+apply (simp add: zmod_zmult_zmult1 pos_zmod_mult_2
+ not_0_le_lemma neg_zmod_mult_2 add_ac)
+done
+
+lemma zmod_number_of_Bit1 [simp]:
+ "number_of (Int.Bit1 v) mod number_of (Int.Bit0 w) =
+ (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 numeral_simps UNIV_I split: bit.split)
+apply (simp only: number_of_eq numeral_simps)
apply (simp add: zmod_zmult_zmult1 pos_zmod_mult_2
not_0_le_lemma neg_zmod_mult_2 add_ac)
done
--- a/src/HOL/Library/Char_nat.thy Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Library/Char_nat.thy Sun Feb 17 06:49:53 2008 +0100
@@ -76,7 +76,7 @@
unfolding nibble_of_nat_def Let_def by auto
lemmas nibble_of_nat_code [code func] = nibble_of_nat_simps
- [simplified nat_number Let_def not_neg_number_of_Pls neg_number_of_BIT if_False add_0 add_Suc]
+ [simplified nat_number Let_def not_neg_number_of_Pls neg_number_of_Bit0 neg_number_of_Bit1 if_False add_0 add_Suc]
lemma nibble_of_nat_of_nibble: "nibble_of_nat (nat_of_nibble n) = n"
by (cases n) (simp_all only: nat_of_nibble.simps nibble_of_nat_simps)
--- a/src/HOL/Library/Code_Index.thy Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Library/Code_Index.thy Sun Feb 17 06:49:53 2008 +0100
@@ -88,7 +88,7 @@
lemma one_index_code [code inline, code func]:
"(1\<Colon>index) = Numeral1"
- by (simp add: number_of_index_def Pls_def Bit_def)
+ by (simp add: number_of_index_def Pls_def Bit1_def)
lemma [code post]: "Numeral1 = (1\<Colon>index)"
using one_index_code ..
--- a/src/HOL/Library/Code_Integer.thy Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Library/Code_Integer.thy Sun Feb 17 06:49:53 2008 +0100
@@ -28,16 +28,19 @@
true true) ["SML", "OCaml", "Haskell"]
*}
-code_const "Int.Pls" and "Int.Min" and "Int.Bit"
+code_const "Int.Pls" and "Int.Min" and "Int.Bit0" and "Int.Bit1"
(SML "raise/ Fail/ \"Pls\""
and "raise/ Fail/ \"Min\""
- and "!((_);/ (_);/ raise/ Fail/ \"Bit\")")
+ and "!((_);/ raise/ Fail/ \"Bit0\")"
+ and "!((_);/ raise/ Fail/ \"Bit1\")")
(OCaml "failwith/ \"Pls\""
and "failwith/ \"Min\""
- and "!((_);/ (_);/ failwith/ \"Bit\")")
+ and "!((_);/ failwith/ \"Bit0\")"
+ and "!((_);/ failwith/ \"Bit1\")")
(Haskell "error/ \"Pls\""
and "error/ \"Min\""
- and "error/ \"Bit\"")
+ and "error/ \"Bit0\""
+ and "error/ \"Bit1\"")
code_const Int.pred
(SML "IntInf.- ((_), 1)")
--- a/src/HOL/Library/Word.thy Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Library/Word.thy Sun Feb 17 06:49:53 2008 +0100
@@ -2265,14 +2265,14 @@
primrec
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))"
+ fast_bv_to_nat_helper bs ((bit_case Int.Bit0 Int.Bit1 b) k)"
lemma fast_bv_to_nat_Cons0: "fast_bv_to_nat_helper (\<zero>#bs) bin =
- fast_bv_to_nat_helper bs (bin BIT bit.B0)"
+ fast_bv_to_nat_helper bs (Int.Bit0 bin)"
by simp
lemma fast_bv_to_nat_Cons1: "fast_bv_to_nat_helper (\<one>#bs) bin =
- fast_bv_to_nat_helper bs (bin BIT bit.B1)"
+ fast_bv_to_nat_helper bs (Int.Bit1 bin)"
by simp
lemma fast_bv_to_nat_def:
@@ -2301,8 +2301,10 @@
| is_const_bit _ = false
fun num_is_usable (Const(@{const_name Int.Pls},_)) = true
| num_is_usable (Const(@{const_name Int.Min},_)) = false
- | num_is_usable (Const(@{const_name Int.Bit},_) $ w $ b) =
- num_is_usable w andalso is_const_bool b
+ | num_is_usable (Const(@{const_name Int.Bit0},_) $ w) =
+ num_is_usable w
+ | num_is_usable (Const(@{const_name Int.Bit1},_) $ w) =
+ num_is_usable w
| num_is_usable _ = false
fun vec_is_usable (Const("List.list.Nil",_)) = true
| vec_is_usable (Const("List.list.Cons",_) $ b $ bs) =
--- a/src/HOL/NatBin.thy Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/NatBin.thy Sun Feb 17 06:49:53 2008 +0100
@@ -524,44 +524,6 @@
by (simp add: Let_def less_number_of_Suc linorder_not_less [symmetric])
-lemma lemma1: "(m+m = n+n) = (m = (n::int))"
-by auto
-
-lemma lemma2: "m+m ~= (1::int) + (n + n)"
-apply auto
-apply (drule_tac f = "%x. x mod 2" in arg_cong)
-apply (simp add: zmod_zadd1_eq)
-done
-
-lemma eq_number_of_BIT_BIT:
- "((number_of (v BIT x) ::int) = number_of (w BIT y)) =
- (x=y & (((number_of v) ::int) = number_of w))"
-apply (simp only: number_of_BIT lemma1 lemma2 eq_commute
- OrderedGroup.add_left_cancel add_assoc OrderedGroup.add_0_left
- split add: bit.split)
-apply simp
-done
-
-lemma eq_number_of_BIT_Pls:
- "((number_of (v BIT x) ::int) = Numeral0) =
- (x=bit.B0 & (((number_of v) ::int) = Numeral0))"
-apply (simp only: simp_thms add: number_of_BIT number_of_Pls eq_commute
- split add: bit.split cong: imp_cong)
-apply (rule_tac x = "number_of v" in spec, safe)
-apply (simp_all (no_asm_use))
-apply (drule_tac f = "%x. x mod 2" in arg_cong)
-apply (simp add: zmod_zadd1_eq)
-done
-
-lemma eq_number_of_BIT_Min:
- "((number_of (v BIT x) ::int) = number_of Int.Min) =
- (x=bit.B1 & (((number_of v) ::int) = number_of Int.Min))"
-apply (simp only: simp_thms add: number_of_BIT number_of_Min eq_commute
- split add: bit.split cong: imp_cong)
-apply (rule_tac x = "number_of v" in spec, auto)
-apply (drule_tac f = "%x. x mod 2" in arg_cong, auto)
-done
-
lemma eq_number_of_Pls_Min: "(Numeral0 ::int) ~= number_of Int.Min"
by auto
@@ -632,8 +594,8 @@
lemma power_number_of_even:
fixes z :: "'a::{number_ring,recpower}"
- shows "z ^ 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
+ shows "z ^ number_of (Int.Bit0 w) = (let w = z ^ (number_of w) in w * w)"
+unfolding Let_def nat_number_of_def number_of_Bit0
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)
@@ -641,9 +603,9 @@
lemma power_number_of_odd:
fixes z :: "'a::{number_ring,recpower}"
- shows "z ^ number_of (w BIT bit.B1) = (if (0::int) <= number_of w
+ shows "z ^ number_of (Int.Bit1 w) = (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
+unfolding Let_def nat_number_of_def number_of_Bit1
apply (rule_tac x = "number_of w" in spec, auto)
apply (simp only: nat_add_distrib nat_mult_distrib)
apply simp
@@ -673,7 +635,7 @@
lessD = lessD, neqE = neqE,
simpset = simpset addsimps [Suc_nat_number_of, int_nat_number_of,
@{thm not_neg_number_of_Pls}, @{thm neg_number_of_Min},
- @{thm neg_number_of_BIT}]})
+ @{thm neg_number_of_Bit0}, @{thm neg_number_of_Bit1}]})
*}
declaration {* K nat_bin_arith_setup *}
@@ -689,33 +651,32 @@
apply (simp only: number_of_Min nat_number_of_def nat_zminus_int)
done
-lemma nat_number_of_BIT_1:
- "number_of (w BIT bit.B1) =
+lemma nat_number_of_Bit0:
+ "number_of (Int.Bit0 w) = (let n::nat = number_of w in n + n)"
+ apply (simp only: nat_number_of_def Let_def)
+ apply (cases "neg (number_of w :: int)")
+ apply (simp add: neg_nat neg_number_of_Bit0)
+ apply (rule int_int_eq [THEN iffD1])
+ apply (simp only: not_neg_nat neg_number_of_Bit0 int_Suc zadd_int [symmetric] simp_thms)
+ apply (simp only: number_of_Bit0 zadd_assoc)
+ apply simp
+ done
+
+lemma nat_number_of_Bit1:
+ "number_of (Int.Bit1 w) =
(if neg (number_of w :: int) then 0
else let n = number_of w in Suc (n + n))"
apply (simp only: nat_number_of_def Let_def split: split_if)
apply (intro conjI impI)
- apply (simp add: neg_nat neg_number_of_BIT)
+ apply (simp add: neg_nat neg_number_of_Bit1)
apply (rule int_int_eq [THEN iffD1])
- apply (simp only: not_neg_nat neg_number_of_BIT int_Suc zadd_int [symmetric] simp_thms)
- apply (simp only: number_of_BIT zadd_assoc split: bit.split)
- apply simp
- done
-
-lemma nat_number_of_BIT_0:
- "number_of (w BIT bit.B0) = (let n::nat = number_of w in n + n)"
- apply (simp only: nat_number_of_def Let_def)
- apply (cases "neg (number_of w :: int)")
- apply (simp add: neg_nat neg_number_of_BIT)
- apply (rule int_int_eq [THEN iffD1])
- apply (simp only: not_neg_nat neg_number_of_BIT int_Suc zadd_int [symmetric] simp_thms)
- apply (simp only: number_of_BIT zadd_assoc)
- apply simp
+ apply (simp only: not_neg_nat neg_number_of_Bit1 int_Suc zadd_int [symmetric] simp_thms)
+ apply (simp only: number_of_Bit1 zadd_assoc)
done
lemmas nat_number =
nat_number_of_Pls nat_number_of_Min
- nat_number_of_BIT_1 nat_number_of_BIT_0
+ nat_number_of_Bit0 nat_number_of_Bit1
lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)"
by (simp add: Let_def)
--- a/src/HOL/NumberTheory/Euler.thy Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/NumberTheory/Euler.thy Sun Feb 17 06:49:53 2008 +0100
@@ -77,7 +77,7 @@
by (auto simp add: zcong_zmult_prop2)
qed
then have "[j^2 = a] (mod p)"
- by (metis number_of_is_id power2_eq_square succ_1 succ_Pls)
+ by (metis number_of_is_id power2_eq_square succ_bin_simps)
with prems show False
by (simp add: QuadRes_def)
qed
@@ -288,7 +288,7 @@
apply (auto simp add: zpower_zpower)
apply (rule zcong_trans)
apply (auto simp add: zcong_sym [of "x ^ nat ((p - 1) div 2)"])
- apply (metis Little_Fermat even_div_2_prop2 mult_num0 number_of_is_id odd_minus_one_even one_is_num_one zmult_1 aux__2)
+ apply (metis Little_Fermat even_div_2_prop2 mult_Bit0 number_of_is_id odd_minus_one_even one_is_num_one zmult_1 aux__2)
done
--- a/src/HOL/Presburger.thy Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Presburger.thy Sun Feb 17 06:49:53 2008 +0100
@@ -394,7 +394,8 @@
((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))"
by (case_tac "y \<le> x", simp_all add: zdiff_int)
-lemma number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (n BIT b)" by simp
+lemma number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (Int.Bit0 n) \<and> (0::int) <= number_of (Int.Bit1 n)"
+by simp
lemma number_of2: "(0::int) <= Numeral0" by simp
lemma Suc_plus1: "Suc n = n + 1" by simp
@@ -503,12 +504,12 @@
unfolding Pls_def Int.Min_def by presburger
lemma eq_Pls_Bit0:
- "Int.Pls = Int.Bit k bit.B0 \<longleftrightarrow> Int.Pls = k"
- unfolding Pls_def Bit_def bit.cases by presburger
+ "Int.Pls = Int.Bit0 k \<longleftrightarrow> Int.Pls = k"
+ unfolding Pls_def Bit0_def by presburger
lemma eq_Pls_Bit1:
- "Int.Pls = Int.Bit k bit.B1 \<longleftrightarrow> False"
- unfolding Pls_def Bit_def bit.cases by presburger
+ "Int.Pls = Int.Bit1 k \<longleftrightarrow> False"
+ unfolding Pls_def Bit1_def by presburger
lemma eq_Min_Pls:
"Int.Min = Int.Pls \<longleftrightarrow> False"
@@ -518,43 +519,44 @@
"Int.Min = Int.Min \<longleftrightarrow> True" by presburger
lemma eq_Min_Bit0:
- "Int.Min = Int.Bit k bit.B0 \<longleftrightarrow> False"
- unfolding Int.Min_def Bit_def bit.cases by presburger
+ "Int.Min = Int.Bit0 k \<longleftrightarrow> False"
+ unfolding Int.Min_def Bit0_def by presburger
lemma eq_Min_Bit1:
- "Int.Min = Int.Bit k bit.B1 \<longleftrightarrow> Int.Min = k"
- unfolding Int.Min_def Bit_def bit.cases by presburger
+ "Int.Min = Int.Bit1 k \<longleftrightarrow> Int.Min = k"
+ unfolding Int.Min_def Bit1_def by presburger
lemma eq_Bit0_Pls:
- "Int.Bit k bit.B0 = Int.Pls \<longleftrightarrow> Int.Pls = k"
- unfolding Pls_def Bit_def bit.cases by presburger
+ "Int.Bit0 k = Int.Pls \<longleftrightarrow> Int.Pls = k"
+ unfolding Pls_def Bit0_def by presburger
lemma eq_Bit1_Pls:
- "Int.Bit k bit.B1 = Int.Pls \<longleftrightarrow> False"
- unfolding Pls_def Bit_def bit.cases by presburger
+ "Int.Bit1 k = Int.Pls \<longleftrightarrow> False"
+ unfolding Pls_def Bit1_def by presburger
lemma eq_Bit0_Min:
- "Int.Bit k bit.B0 = Int.Min \<longleftrightarrow> False"
- unfolding Int.Min_def Bit_def bit.cases by presburger
+ "Int.Bit0 k = Int.Min \<longleftrightarrow> False"
+ unfolding Int.Min_def Bit0_def by presburger
lemma eq_Bit1_Min:
- "(Int.Bit k bit.B1) = Int.Min \<longleftrightarrow> Int.Min = k"
- unfolding Int.Min_def Bit_def bit.cases by presburger
+ "Int.Bit1 k = Int.Min \<longleftrightarrow> Int.Min = k"
+ unfolding Int.Min_def Bit1_def by presburger
+
+lemma eq_Bit0_Bit0:
+ "Int.Bit0 k1 = Int.Bit0 k2 \<longleftrightarrow> k1 = k2"
+ unfolding Bit0_def by presburger
-lemma eq_Bit_Bit:
- "Int.Bit k1 v1 = Int.Bit k2 v2 \<longleftrightarrow>
- v1 = v2 \<and> k1 = k2"
- unfolding Bit_def
- apply (cases v1)
- apply (cases v2)
- apply auto
- apply presburger
- apply (cases v2)
- apply auto
- apply presburger
- apply (cases v2)
- apply auto
- done
+lemma eq_Bit0_Bit1:
+ "Int.Bit0 k1 = Int.Bit1 k2 \<longleftrightarrow> False"
+ unfolding Bit0_def Bit1_def by presburger
+
+lemma eq_Bit1_Bit0:
+ "Int.Bit1 k1 = Int.Bit0 k2 \<longleftrightarrow> False"
+ unfolding Bit0_def Bit1_def by presburger
+
+lemma eq_Bit1_Bit1:
+ "Int.Bit1 k1 = Int.Bit1 k2 \<longleftrightarrow> k1 = k2"
+ unfolding Bit1_def by presburger
lemma eq_number_of:
"(number_of k \<Colon> int) = number_of l \<longleftrightarrow> k = l"
@@ -568,9 +570,13 @@
"Int.Pls \<le> Int.Min \<longleftrightarrow> False"
unfolding Pls_def Int.Min_def by presburger
-lemma less_eq_Pls_Bit:
- "Int.Pls \<le> Int.Bit k v \<longleftrightarrow> Int.Pls \<le> k"
- unfolding Pls_def Bit_def by (cases v) auto
+lemma less_eq_Pls_Bit0:
+ "Int.Pls \<le> Int.Bit0 k \<longleftrightarrow> Int.Pls \<le> k"
+ unfolding Pls_def Bit0_def by auto
+
+lemma less_eq_Pls_Bit1:
+ "Int.Pls \<le> Int.Bit1 k \<longleftrightarrow> Int.Pls \<le> k"
+ unfolding Pls_def Bit1_def by auto
lemma less_eq_Min_Pls:
"Int.Min \<le> Int.Pls \<longleftrightarrow> True"
@@ -580,36 +586,44 @@
"Int.Min \<le> Int.Min \<longleftrightarrow> True" by rule+
lemma less_eq_Min_Bit0:
- "Int.Min \<le> Int.Bit k bit.B0 \<longleftrightarrow> Int.Min < k"
- unfolding Int.Min_def Bit_def by auto
+ "Int.Min \<le> Int.Bit0 k \<longleftrightarrow> Int.Min < k"
+ unfolding Int.Min_def Bit0_def by auto
lemma less_eq_Min_Bit1:
- "Int.Min \<le> Int.Bit k bit.B1 \<longleftrightarrow> Int.Min \<le> k"
- unfolding Int.Min_def Bit_def by auto
+ "Int.Min \<le> Int.Bit1 k \<longleftrightarrow> Int.Min \<le> k"
+ unfolding Int.Min_def Bit1_def by auto
lemma less_eq_Bit0_Pls:
- "Int.Bit k bit.B0 \<le> Int.Pls \<longleftrightarrow> k \<le> Int.Pls"
- unfolding Pls_def Bit_def by simp
+ "Int.Bit0 k \<le> Int.Pls \<longleftrightarrow> k \<le> Int.Pls"
+ unfolding Pls_def Bit0_def by simp
lemma less_eq_Bit1_Pls:
- "Int.Bit k bit.B1 \<le> Int.Pls \<longleftrightarrow> k < Int.Pls"
- unfolding Pls_def Bit_def by auto
+ "Int.Bit1 k \<le> Int.Pls \<longleftrightarrow> k < Int.Pls"
+ unfolding Pls_def Bit1_def by auto
-lemma less_eq_Bit_Min:
- "Int.Bit k v \<le> Int.Min \<longleftrightarrow> k \<le> Int.Min"
- unfolding Int.Min_def Bit_def by (cases v) auto
+lemma less_eq_Bit0_Min:
+ "Int.Bit0 k \<le> Int.Min \<longleftrightarrow> k \<le> Int.Min"
+ unfolding Int.Min_def Bit0_def by auto
-lemma less_eq_Bit0_Bit:
- "Int.Bit k1 bit.B0 \<le> Int.Bit k2 v \<longleftrightarrow> k1 \<le> k2"
- unfolding Bit_def bit.cases by (cases v) auto
+lemma less_eq_Bit1_Min:
+ "Int.Bit1 k \<le> Int.Min \<longleftrightarrow> k \<le> Int.Min"
+ unfolding Int.Min_def Bit1_def by auto
-lemma less_eq_Bit_Bit1:
- "Int.Bit k1 v \<le> Int.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2"
- unfolding Bit_def bit.cases by (cases v) auto
+lemma less_eq_Bit0_Bit0:
+ "Int.Bit0 k1 \<le> Int.Bit0 k2 \<longleftrightarrow> k1 \<le> k2"
+ unfolding Bit0_def by auto
+
+lemma less_eq_Bit0_Bit1:
+ "Int.Bit0 k1 \<le> Int.Bit1 k2 \<longleftrightarrow> k1 \<le> k2"
+ unfolding Bit0_def Bit1_def by auto
lemma less_eq_Bit1_Bit0:
- "Int.Bit k1 bit.B1 \<le> Int.Bit k2 bit.B0 \<longleftrightarrow> k1 < k2"
- unfolding Bit_def by (auto split: bit.split)
+ "Int.Bit1 k1 \<le> Int.Bit0 k2 \<longleftrightarrow> k1 < k2"
+ unfolding Bit0_def Bit1_def by auto
+
+lemma less_eq_Bit1_Bit1:
+ "Int.Bit1 k1 \<le> Int.Bit1 k2 \<longleftrightarrow> k1 \<le> k2"
+ unfolding Bit1_def by auto
lemma less_eq_number_of:
"(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l"
@@ -624,12 +638,12 @@
unfolding Pls_def Int.Min_def by presburger
lemma less_Pls_Bit0:
- "Int.Pls < Int.Bit k bit.B0 \<longleftrightarrow> Int.Pls < k"
- unfolding Pls_def Bit_def by auto
+ "Int.Pls < Int.Bit0 k \<longleftrightarrow> Int.Pls < k"
+ unfolding Pls_def Bit0_def by auto
lemma less_Pls_Bit1:
- "Int.Pls < Int.Bit k bit.B1 \<longleftrightarrow> Int.Pls \<le> k"
- unfolding Pls_def Bit_def by auto
+ "Int.Pls < Int.Bit1 k \<longleftrightarrow> Int.Pls \<le> k"
+ unfolding Pls_def Bit1_def by auto
lemma less_Min_Pls:
"Int.Min < Int.Pls \<longleftrightarrow> True"
@@ -638,33 +652,45 @@
lemma less_Min_Min:
"Int.Min < Int.Min \<longleftrightarrow> False" by simp
-lemma less_Min_Bit:
- "Int.Min < Int.Bit k v \<longleftrightarrow> Int.Min < k"
- unfolding Int.Min_def Bit_def by (auto split: bit.split)
+lemma less_Min_Bit0:
+ "Int.Min < Int.Bit0 k \<longleftrightarrow> Int.Min < k"
+ unfolding Int.Min_def Bit0_def by auto
+
+lemma less_Min_Bit1:
+ "Int.Min < Int.Bit1 k \<longleftrightarrow> Int.Min < k"
+ unfolding Int.Min_def Bit1_def by auto
-lemma less_Bit_Pls:
- "Int.Bit k v < Int.Pls \<longleftrightarrow> k < Int.Pls"
- unfolding Pls_def Bit_def by (auto split: bit.split)
+lemma less_Bit0_Pls:
+ "Int.Bit0 k < Int.Pls \<longleftrightarrow> k < Int.Pls"
+ unfolding Pls_def Bit0_def by auto
+
+lemma less_Bit1_Pls:
+ "Int.Bit1 k < Int.Pls \<longleftrightarrow> k < Int.Pls"
+ unfolding Pls_def Bit1_def by auto
lemma less_Bit0_Min:
- "Int.Bit k bit.B0 < Int.Min \<longleftrightarrow> k \<le> Int.Min"
- unfolding Int.Min_def Bit_def by auto
+ "Int.Bit0 k < Int.Min \<longleftrightarrow> k \<le> Int.Min"
+ unfolding Int.Min_def Bit0_def by auto
lemma less_Bit1_Min:
- "Int.Bit k bit.B1 < Int.Min \<longleftrightarrow> k < Int.Min"
- unfolding Int.Min_def Bit_def by auto
+ "Int.Bit1 k < Int.Min \<longleftrightarrow> k < Int.Min"
+ unfolding Int.Min_def Bit1_def by auto
-lemma less_Bit_Bit0:
- "Int.Bit k1 v < Int.Bit k2 bit.B0 \<longleftrightarrow> k1 < k2"
- unfolding Bit_def by (auto split: bit.split)
-
-lemma less_Bit1_Bit:
- "Int.Bit k1 bit.B1 < Int.Bit k2 v \<longleftrightarrow> k1 < k2"
- unfolding Bit_def by (auto split: bit.split)
+lemma less_Bit0_Bit0:
+ "Int.Bit0 k1 < Int.Bit0 k2 \<longleftrightarrow> k1 < k2"
+ unfolding Bit0_def by auto
lemma less_Bit0_Bit1:
- "Int.Bit k1 bit.B0 < Int.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2"
- unfolding Bit_def bit.cases by arith
+ "Int.Bit0 k1 < Int.Bit1 k2 \<longleftrightarrow> k1 \<le> k2"
+ unfolding Bit0_def Bit1_def by auto
+
+lemma less_Bit1_Bit0:
+ "Int.Bit1 k1 < Int.Bit0 k2 \<longleftrightarrow> k1 < k2"
+ unfolding Bit0_def Bit1_def by auto
+
+lemma less_Bit1_Bit1:
+ "Int.Bit1 k1 < Int.Bit1 k2 \<longleftrightarrow> k1 < k2"
+ unfolding Bit1_def by auto
lemma less_number_of:
"(number_of k \<Colon> int) < number_of l \<longleftrightarrow> k < l"
@@ -689,17 +715,22 @@
lemmas eq_numeral_code [code func] =
eq_Pls_Pls eq_Pls_Min eq_Pls_Bit0 eq_Pls_Bit1
eq_Min_Pls eq_Min_Min eq_Min_Bit0 eq_Min_Bit1
- eq_Bit0_Pls eq_Bit1_Pls eq_Bit0_Min eq_Bit1_Min eq_Bit_Bit
+ eq_Bit0_Pls eq_Bit1_Pls eq_Bit0_Min eq_Bit1_Min
+ eq_Bit0_Bit0 eq_Bit0_Bit1 eq_Bit1_Bit0 eq_Bit1_Bit1
eq_number_of
-lemmas less_eq_numeral_code [code func] = less_eq_Pls_Pls less_eq_Pls_Min less_eq_Pls_Bit
+lemmas less_eq_numeral_code [code func] =
+ less_eq_Pls_Pls less_eq_Pls_Min less_eq_Pls_Bit0 less_eq_Pls_Bit1
less_eq_Min_Pls less_eq_Min_Min less_eq_Min_Bit0 less_eq_Min_Bit1
- less_eq_Bit0_Pls less_eq_Bit1_Pls less_eq_Bit_Min less_eq_Bit0_Bit less_eq_Bit_Bit1 less_eq_Bit1_Bit0
+ less_eq_Bit0_Pls less_eq_Bit1_Pls less_eq_Bit0_Min less_eq_Bit1_Min
+ less_eq_Bit0_Bit0 less_eq_Bit0_Bit1 less_eq_Bit1_Bit0 less_eq_Bit1_Bit1
less_eq_number_of
-lemmas less_numeral_code [code func] = less_Pls_Pls less_Pls_Min less_Pls_Bit0
- less_Pls_Bit1 less_Min_Pls less_Min_Min less_Min_Bit less_Bit_Pls
- less_Bit0_Min less_Bit1_Min less_Bit_Bit0 less_Bit1_Bit less_Bit0_Bit1
+lemmas less_numeral_code [code func] =
+ less_Pls_Pls less_Pls_Min less_Pls_Bit0 less_Pls_Bit1
+ less_Min_Pls less_Min_Min less_Min_Bit0 less_Min_Bit1
+ less_Bit0_Pls less_Bit1_Pls less_Bit0_Min less_Bit1_Min
+ less_Bit0_Bit0 less_Bit0_Bit1 less_Bit1_Bit0 less_Bit1_Bit1
less_number_of
context ring_1
--- a/src/HOL/Real/Float.thy Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Real/Float.thy Sun Feb 17 06:49:53 2008 +0100
@@ -518,10 +518,10 @@
lemma int_nonzero_number_of_Min: "~(iszero ((-1)::int))"
by simp
-lemma int_iszero_number_of_0: "iszero ((number_of (w BIT bit.B0))::int) = iszero ((number_of w)::int)"
+lemma int_iszero_number_of_Bit0: "iszero ((number_of (Int.Bit0 w))::int) = iszero ((number_of w)::int)"
by simp
-lemma int_iszero_number_of_1: "\<not> iszero ((number_of (w BIT bit.B1))::int)"
+lemma int_iszero_number_of_Bit1: "\<not> iszero ((number_of (Int.Bit1 w))::int)"
by simp
lemma int_less_number_of_eq_neg: "(((number_of x)::int) < number_of y) = neg ((number_of (x + (uminus y)))::int)"
@@ -533,7 +533,10 @@
lemma int_neg_number_of_Min: "neg (-1::int)"
by simp
-lemma int_neg_number_of_BIT: "neg ((number_of (w BIT x))::int) = neg ((number_of w)::int)"
+lemma int_neg_number_of_Bit0: "neg ((number_of (Int.Bit0 w))::int) = neg ((number_of w)::int)"
+ by simp
+
+lemma int_neg_number_of_Bit1: "neg ((number_of (Int.Bit1 w))::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 (y + (uminus x)))::int))"
@@ -541,9 +544,9 @@
lemmas intarithrel =
int_eq_number_of_eq
- lift_bool[OF int_iszero_number_of_Pls] nlift_bool[OF int_nonzero_number_of_Min] int_iszero_number_of_0
- 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
+ lift_bool[OF int_iszero_number_of_Pls] nlift_bool[OF int_nonzero_number_of_Min] int_iszero_number_of_Bit0
+ lift_bool[OF int_iszero_number_of_Bit1] 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_Bit0 int_neg_number_of_Bit1 int_le_number_of_eq
lemma int_number_of_add_sym: "((number_of v)::int) + number_of w = number_of (v + w)"
by simp
--- a/src/HOL/Tools/ComputeNumeral.thy Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Tools/ComputeNumeral.thy Sun Feb 17 06:49:53 2008 +0100
@@ -8,15 +8,15 @@
(* neg for bit strings *)
lemma neg1: "neg Int.Pls = False" by (simp add: Int.Pls_def)
lemma neg2: "neg Int.Min = True" apply (subst Int.Min_def) by auto
-lemma neg3: "neg (x BIT Int.B0) = neg x" apply (simp add: neg_def) apply (subst Bit_def) by auto
-lemma neg4: "neg (x BIT Int.B1) = neg x" apply (simp add: neg_def) apply (subst Bit_def) by auto
+lemma neg3: "neg (Int.Bit0 x) = neg x" apply (simp add: neg_def) apply (subst Bit0_def) by auto
+lemma neg4: "neg (Int.Bit1 x) = neg x" apply (simp add: neg_def) apply (subst Bit1_def) by auto
lemmas bitneg = neg1 neg2 neg3 neg4
(* iszero for bit strings *)
lemma iszero1: "iszero Int.Pls = True" by (simp add: Int.Pls_def iszero_def)
lemma iszero2: "iszero Int.Min = False" apply (subst Int.Min_def) apply (subst iszero_def) by simp
-lemma iszero3: "iszero (x BIT Int.B0) = iszero x" apply (subst Int.Bit_def) apply (subst iszero_def)+ by auto
-lemma iszero4: "iszero (x BIT Int.B1) = False" apply (subst Int.Bit_def) apply (subst iszero_def)+ apply simp by arith
+lemma iszero3: "iszero (Int.Bit0 x) = iszero x" apply (subst Int.Bit0_def) apply (subst iszero_def)+ by auto
+lemma iszero4: "iszero (Int.Bit1 x) = False" apply (subst Int.Bit1_def) apply (subst iszero_def)+ apply simp by arith
lemmas bitiszero = iszero1 iszero2 iszero3 iszero4
(* lezero for bit strings *)
@@ -24,66 +24,66 @@
"lezero x == (x \<le> 0)"
lemma lezero1: "lezero Int.Pls = True" unfolding Int.Pls_def lezero_def by auto
lemma lezero2: "lezero Int.Min = True" unfolding Int.Min_def lezero_def by auto
-lemma lezero3: "lezero (x BIT Int.B0) = lezero x" unfolding Int.Bit_def lezero_def by auto
-lemma lezero4: "lezero (x BIT Int.B1) = neg x" unfolding Int.Bit_def lezero_def neg_def by auto
+lemma lezero3: "lezero (Int.Bit0 x) = lezero x" unfolding Int.Bit0_def lezero_def by auto
+lemma lezero4: "lezero (Int.Bit1 x) = neg x" unfolding Int.Bit1_def lezero_def neg_def by auto
lemmas bitlezero = lezero1 lezero2 lezero3 lezero4
(* equality for bit strings *)
-lemma biteq1: "(Int.Pls = Int.Pls) = True" by auto
-lemma biteq2: "(Int.Min = Int.Min) = True" by auto
-lemma biteq3: "(Int.Pls = Int.Min) = False" unfolding Pls_def Min_def by auto
-lemma biteq4: "(Int.Min = Int.Pls) = False" unfolding Pls_def Min_def by auto
-lemma biteq5: "(x BIT Int.B0 = y BIT Int.B0) = (x = y)" unfolding Bit_def by auto
-lemma biteq6: "(x BIT Int.B1 = y BIT Int.B1) = (x = y)" unfolding Bit_def by auto
-lemma biteq7: "(x BIT Int.B0 = y BIT Int.B1) = False" unfolding Bit_def by (simp, arith)
-lemma biteq8: "(x BIT Int.B1 = y BIT Int.B0) = False" unfolding Bit_def by (simp, arith)
-lemma biteq9: "(Int.Pls = x BIT Int.B0) = (Int.Pls = x)" unfolding Bit_def Pls_def by auto
-lemma biteq10: "(Int.Pls = x BIT Int.B1) = False" unfolding Bit_def Pls_def by (simp, arith)
-lemma biteq11: "(Int.Min = x BIT Int.B0) = False" unfolding Bit_def Min_def by (simp, arith)
-lemma biteq12: "(Int.Min = x BIT Int.B1) = (Int.Min = x)" unfolding Bit_def Min_def by auto
-lemma biteq13: "(x BIT Int.B0 = Int.Pls) = (x = Int.Pls)" unfolding Bit_def Pls_def by auto
-lemma biteq14: "(x BIT Int.B1 = Int.Pls) = False" unfolding Bit_def Pls_def by (simp, arith)
-lemma biteq15: "(x BIT Int.B0 = Int.Min) = False" unfolding Bit_def Pls_def Min_def by (simp, arith)
-lemma biteq16: "(x BIT Int.B1 = Int.Min) = (x = Int.Min)" unfolding Bit_def Min_def by (simp, arith)
+lemma biteq1: "(Int.Pls = Int.Pls) = True" by (rule eq_Pls_Pls)
+lemma biteq2: "(Int.Min = Int.Min) = True" by (rule eq_Min_Min)
+lemma biteq3: "(Int.Pls = Int.Min) = False" by (rule eq_Pls_Min)
+lemma biteq4: "(Int.Min = Int.Pls) = False" by (rule eq_Min_Pls)
+lemma biteq5: "(Int.Bit0 x = Int.Bit0 y) = (x = y)" by (rule eq_Bit0_Bit0)
+lemma biteq6: "(Int.Bit1 x = Int.Bit1 y) = (x = y)" by (rule eq_Bit1_Bit1)
+lemma biteq7: "(Int.Bit0 x = Int.Bit1 y) = False" by (rule eq_Bit0_Bit1)
+lemma biteq8: "(Int.Bit1 x = Int.Bit0 y) = False" by (rule eq_Bit1_Bit0)
+lemma biteq9: "(Int.Pls = Int.Bit0 x) = (Int.Pls = x)" by (rule eq_Pls_Bit0)
+lemma biteq10: "(Int.Pls = Int.Bit1 x) = False" by (rule eq_Pls_Bit1)
+lemma biteq11: "(Int.Min = Int.Bit0 x) = False" by (rule eq_Min_Bit0)
+lemma biteq12: "(Int.Min = Int.Bit1 x) = (Int.Min = x)" by (rule eq_Min_Bit1)
+lemma biteq13: "(Int.Bit0 x = Int.Pls) = (x = Int.Pls)" by (subst eq_Bit0_Pls) auto
+lemma biteq14: "(Int.Bit1 x = Int.Pls) = False" by (rule eq_Bit1_Pls)
+lemma biteq15: "(Int.Bit0 x = Int.Min) = False" by (rule eq_Bit0_Min)
+lemma biteq16: "(Int.Bit1 x = Int.Min) = (x = Int.Min)" by (subst eq_Bit1_Min) auto
lemmas biteq = biteq1 biteq2 biteq3 biteq4 biteq5 biteq6 biteq7 biteq8 biteq9 biteq10 biteq11 biteq12 biteq13 biteq14 biteq15 biteq16
(* x < y for bit strings *)
-lemma bitless1: "(Int.Pls < Int.Min) = False" unfolding Pls_def Min_def by auto
-lemma bitless2: "(Int.Pls < Int.Pls) = False" by auto
-lemma bitless3: "(Int.Min < Int.Pls) = True" unfolding Pls_def Min_def by auto
-lemma bitless4: "(Int.Min < Int.Min) = False" unfolding Pls_def Min_def by auto
-lemma bitless5: "(x BIT Int.B0 < y BIT Int.B0) = (x < y)" unfolding Bit_def by auto
-lemma bitless6: "(x BIT Int.B1 < y BIT Int.B1) = (x < y)" unfolding Bit_def by auto
-lemma bitless7: "(x BIT Int.B0 < y BIT Int.B1) = (x \<le> y)" unfolding Bit_def by auto
-lemma bitless8: "(x BIT Int.B1 < y BIT Int.B0) = (x < y)" unfolding Bit_def by auto
-lemma bitless9: "(Int.Pls < x BIT Int.B0) = (Int.Pls < x)" unfolding Bit_def Pls_def by auto
-lemma bitless10: "(Int.Pls < x BIT Int.B1) = (Int.Pls \<le> x)" unfolding Bit_def Pls_def by auto
-lemma bitless11: "(Int.Min < x BIT Int.B0) = (Int.Pls \<le> x)" unfolding Bit_def Pls_def Min_def by auto
-lemma bitless12: "(Int.Min < x BIT Int.B1) = (Int.Min < x)" unfolding Bit_def Min_def by auto
-lemma bitless13: "(x BIT Int.B0 < Int.Pls) = (x < Int.Pls)" unfolding Bit_def Pls_def by auto
-lemma bitless14: "(x BIT Int.B1 < Int.Pls) = (x < Int.Pls)" unfolding Bit_def Pls_def by auto
-lemma bitless15: "(x BIT Int.B0 < Int.Min) = (x < Int.Pls)" unfolding Bit_def Pls_def Min_def by auto
-lemma bitless16: "(x BIT Int.B1 < Int.Min) = (x < Int.Min)" unfolding Bit_def Min_def by auto
+lemma bitless1: "(Int.Pls < Int.Min) = False" by (rule less_Pls_Min)
+lemma bitless2: "(Int.Pls < Int.Pls) = False" by (rule less_Pls_Pls)
+lemma bitless3: "(Int.Min < Int.Pls) = True" by (rule less_Min_Pls)
+lemma bitless4: "(Int.Min < Int.Min) = False" by (rule less_Min_Min)
+lemma bitless5: "(Int.Bit0 x < Int.Bit0 y) = (x < y)" by (rule less_Bit0_Bit0)
+lemma bitless6: "(Int.Bit1 x < Int.Bit1 y) = (x < y)" by (rule less_Bit1_Bit1)
+lemma bitless7: "(Int.Bit0 x < Int.Bit1 y) = (x \<le> y)" by (rule less_Bit0_Bit1)
+lemma bitless8: "(Int.Bit1 x < Int.Bit0 y) = (x < y)" by (rule less_Bit1_Bit0)
+lemma bitless9: "(Int.Pls < Int.Bit0 x) = (Int.Pls < x)" by (rule less_Pls_Bit0)
+lemma bitless10: "(Int.Pls < Int.Bit1 x) = (Int.Pls \<le> x)" by (rule less_Pls_Bit1)
+lemma bitless11: "(Int.Min < Int.Bit0 x) = (Int.Pls \<le> x)" unfolding Bit0_def Pls_def Min_def by auto
+lemma bitless12: "(Int.Min < Int.Bit1 x) = (Int.Min < x)" by (rule less_Min_Bit1)
+lemma bitless13: "(Int.Bit0 x < Int.Pls) = (x < Int.Pls)" by (rule less_Bit0_Pls)
+lemma bitless14: "(Int.Bit1 x < Int.Pls) = (x < Int.Pls)" by (rule less_Bit1_Pls)
+lemma bitless15: "(Int.Bit0 x < Int.Min) = (x < Int.Pls)" unfolding Bit0_def Pls_def Min_def by auto
+lemma bitless16: "(Int.Bit1 x < Int.Min) = (x < Int.Min)" by (rule less_Bit1_Min)
lemmas bitless = bitless1 bitless2 bitless3 bitless4 bitless5 bitless6 bitless7 bitless8
bitless9 bitless10 bitless11 bitless12 bitless13 bitless14 bitless15 bitless16
(* x \<le> y for bit strings *)
-lemma bitle1: "(Int.Pls \<le> Int.Min) = False" unfolding Pls_def Min_def by auto
-lemma bitle2: "(Int.Pls \<le> Int.Pls) = True" by auto
-lemma bitle3: "(Int.Min \<le> Int.Pls) = True" unfolding Pls_def Min_def by auto
-lemma bitle4: "(Int.Min \<le> Int.Min) = True" unfolding Pls_def Min_def by auto
-lemma bitle5: "(x BIT Int.B0 \<le> y BIT Int.B0) = (x \<le> y)" unfolding Bit_def by auto
-lemma bitle6: "(x BIT Int.B1 \<le> y BIT Int.B1) = (x \<le> y)" unfolding Bit_def by auto
-lemma bitle7: "(x BIT Int.B0 \<le> y BIT Int.B1) = (x \<le> y)" unfolding Bit_def by auto
-lemma bitle8: "(x BIT Int.B1 \<le> y BIT Int.B0) = (x < y)" unfolding Bit_def by auto
-lemma bitle9: "(Int.Pls \<le> x BIT Int.B0) = (Int.Pls \<le> x)" unfolding Bit_def Pls_def by auto
-lemma bitle10: "(Int.Pls \<le> x BIT Int.B1) = (Int.Pls \<le> x)" unfolding Bit_def Pls_def by auto
-lemma bitle11: "(Int.Min \<le> x BIT Int.B0) = (Int.Pls \<le> x)" unfolding Bit_def Pls_def Min_def by auto
-lemma bitle12: "(Int.Min \<le> x BIT Int.B1) = (Int.Min \<le> x)" unfolding Bit_def Min_def by auto
-lemma bitle13: "(x BIT Int.B0 \<le> Int.Pls) = (x \<le> Int.Pls)" unfolding Bit_def Pls_def by auto
-lemma bitle14: "(x BIT Int.B1 \<le> Int.Pls) = (x < Int.Pls)" unfolding Bit_def Pls_def by auto
-lemma bitle15: "(x BIT Int.B0 \<le> Int.Min) = (x < Int.Pls)" unfolding Bit_def Pls_def Min_def by auto
-lemma bitle16: "(x BIT Int.B1 \<le> Int.Min) = (x \<le> Int.Min)" unfolding Bit_def Min_def by auto
+lemma bitle1: "(Int.Pls \<le> Int.Min) = False" by (rule less_eq_Pls_Min)
+lemma bitle2: "(Int.Pls \<le> Int.Pls) = True" by (rule less_eq_Pls_Pls)
+lemma bitle3: "(Int.Min \<le> Int.Pls) = True" by (rule less_eq_Min_Pls)
+lemma bitle4: "(Int.Min \<le> Int.Min) = True" by (rule less_eq_Min_Min)
+lemma bitle5: "(Int.Bit0 x \<le> Int.Bit0 y) = (x \<le> y)" by (rule less_eq_Bit0_Bit0)
+lemma bitle6: "(Int.Bit1 x \<le> Int.Bit1 y) = (x \<le> y)" by (rule less_eq_Bit1_Bit1)
+lemma bitle7: "(Int.Bit0 x \<le> Int.Bit1 y) = (x \<le> y)" by (rule less_eq_Bit0_Bit1)
+lemma bitle8: "(Int.Bit1 x \<le> Int.Bit0 y) = (x < y)" by (rule less_eq_Bit1_Bit0)
+lemma bitle9: "(Int.Pls \<le> Int.Bit0 x) = (Int.Pls \<le> x)" by (rule less_eq_Pls_Bit0)
+lemma bitle10: "(Int.Pls \<le> Int.Bit1 x) = (Int.Pls \<le> x)" by (rule less_eq_Pls_Bit1)
+lemma bitle11: "(Int.Min \<le> Int.Bit0 x) = (Int.Pls \<le> x)" unfolding Bit0_def Pls_def Min_def by auto
+lemma bitle12: "(Int.Min \<le> Int.Bit1 x) = (Int.Min \<le> x)" by (rule less_eq_Min_Bit1)
+lemma bitle13: "(Int.Bit0 x \<le> Int.Pls) = (x \<le> Int.Pls)" by (rule less_eq_Bit0_Pls)
+lemma bitle14: "(Int.Bit1 x \<le> Int.Pls) = (x < Int.Pls)" by (rule less_eq_Bit1_Pls)
+lemma bitle15: "(Int.Bit0 x \<le> Int.Min) = (x < Int.Pls)" unfolding Bit0_def Pls_def Min_def by auto
+lemma bitle16: "(Int.Bit1 x \<le> Int.Min) = (x \<le> Int.Min)" by (rule less_eq_Bit1_Min)
lemmas bitle = bitle1 bitle2 bitle3 bitle4 bitle5 bitle6 bitle7 bitle8
bitle9 bitle10 bitle11 bitle12 bitle13 bitle14 bitle15 bitle16
@@ -97,15 +97,15 @@
lemmas bituminus = minus_bin_simps
(* addition for bit strings *)
-lemmas bitadd = add_Pls add_Pls_right add_Min add_Min_right add_BIT_11 add_BIT_10 add_BIT_0[where b="Int.B0"] add_BIT_0[where b="Int.B1"]
+lemmas bitadd = add_bin_simps
(* multiplication for bit strings *)
lemma mult_Pls_right: "x * Int.Pls = Int.Pls" by (simp add: Pls_def)
lemma mult_Min_right: "x * Int.Min = - x" by (subst mult_commute, simp add: mult_Min)
-lemma multb0x: "(x BIT Int.B0) * y = (x * y) BIT Int.B0" unfolding Bit_def by simp
-lemma multxb0: "x * (y BIT Int.B0) = (x * y) BIT Int.B0" unfolding Bit_def by simp
-lemma multb1: "(x BIT Int.B1) * (y BIT Int.B1) = (((x * y) BIT Int.B0) + x + y) BIT Int.B1"
- unfolding Bit_def by (simp add: ring_simps)
+lemma multb0x: "(Int.Bit0 x) * y = Int.Bit0 (x * y)" by (rule mult_Bit0)
+lemma multxb0: "x * (Int.Bit0 y) = Int.Bit0 (x * y)" unfolding Bit0_def by simp
+lemma multb1: "(Int.Bit1 x) * (Int.Bit1 y) = Int.Bit1 (Int.Bit0 (x * y) + x + y)"
+ unfolding Bit0_def Bit1_def by (simp add: ring_simps)
lemmas bitmul = mult_Pls mult_Min mult_Pls_right mult_Min_right multb0x multxb0 multb1
lemmas bitarith = bitnorm bitiszero bitneg bitlezero biteq bitless bitle bitsucc bitpred bituminus bitadd bitmul
@@ -121,7 +121,7 @@
(* Normalization of nat literals *)
lemma natnorm0: "(0::nat) = number_of (Int.Pls)" by auto
-lemma natnorm1: "(1 :: nat) = number_of (Int.Pls BIT Int.B1)" by auto
+lemma natnorm1: "(1 :: nat) = number_of (Int.Bit1 Int.Pls)" by auto
lemmas natnorm = natnorm0 natnorm1 nat_norm_number_of
(* Suc *)
@@ -228,12 +228,12 @@
apply (unfold Min_def even_def)
by simp
-lemma even_B0: "even (x BIT Int.B0) = True"
- apply (unfold Bit_def)
+lemma even_B0: "even (Int.Bit0 x) = True"
+ apply (unfold Bit0_def)
by simp
-lemma even_B1: "even (x BIT Int.B1) = False"
- apply (unfold Bit_def)
+lemma even_B1: "even (Int.Bit1 x) = False"
+ apply (unfold Bit1_def)
by simp
lemma even_number_of: "even ((number_of w)::int) = even w"
--- a/src/HOL/Tools/Qelim/cooper_data.ML Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Tools/Qelim/cooper_data.ML Sun Feb 17 06:49:53 2008 +0100
@@ -24,7 +24,7 @@
@{term "op * :: int => _"}, @{term "op * :: nat => _"},
@{term "op div :: int => _"}, @{term "op div :: nat => _"},
@{term "op mod :: int => _"}, @{term "op mod :: nat => _"},
- @{term "Int.Bit"},
+ @{term "Int.Bit0"}, @{term "Int.Bit1"},
@{term "op &"}, @{term "op |"}, @{term "op -->"},
@{term "op = :: int => _"}, @{term "op = :: nat => _"}, @{term "op = :: bool => _"},
@{term "op < :: int => _"}, @{term "op < :: nat => _"},
@@ -38,8 +38,8 @@
@{term "Ex :: (int => _) => _"}, @{term "Ex :: (nat => _) => _"},
@{term "All :: (int => _) => _"}, @{term "All :: (nat => _) => _"},
@{term "nat"}, @{term "int"},
- @{term "Int.bit.B0"},@{term "Int.bit.B1"},
- @{term "Int.Bit"}, @{term "Int.Pls"}, @{term "Int.Min"},
+ @{term "Int.Bit0"}, @{term "Int.Bit1"},
+ @{term "Int.Pls"}, @{term "Int.Min"},
@{term "Int.number_of :: int => int"}, @{term "Int.number_of :: int => nat"},
@{term "0::int"}, @{term "1::int"}, @{term "0::nat"}, @{term "1::nat"},
@{term "True"}, @{term "False"}];
--- a/src/HOL/Tools/numeral.ML Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Tools/numeral.ML Sun Feb 17 06:49:53 2008 +0100
@@ -17,15 +17,15 @@
(* numeral *)
-fun mk_cbit 0 = @{cterm "Int.bit.B0"}
- | mk_cbit 1 = @{cterm "Int.bit.B1"}
+fun mk_cbit 0 = @{cterm "Int.Bit0"}
+ | mk_cbit 1 = @{cterm "Int.Bit1"}
| mk_cbit _ = raise CTERM ("mk_cbit", []);
fun mk_cnumeral 0 = @{cterm "Int.Pls"}
| mk_cnumeral ~1 = @{cterm "Int.Min"}
| mk_cnumeral i =
let val (q, r) = Integer.div_mod i 2 in
- Thm.capply (Thm.capply @{cterm "Int.Bit"} (mk_cnumeral q)) (mk_cbit r)
+ Thm.capply (mk_cbit r) (mk_cnumeral q)
end;
@@ -57,8 +57,7 @@
fun add_code number_of negative unbounded target =
CodeTarget.add_pretty_numeral target negative unbounded number_of
- @{const_name Int.B0} @{const_name Int.B1}
@{const_name Int.Pls} @{const_name Int.Min}
- @{const_name Int.Bit};
+ @{const_name Int.Bit0} @{const_name Int.Bit1};
end;
--- a/src/HOL/Tools/numeral_syntax.ML Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Tools/numeral_syntax.ML Sun Feb 17 06:49:53 2008 +0100
@@ -20,7 +20,7 @@
fun mk_bin num =
let
val {leading_zeros = z, value, ...} = Syntax.read_xnum num;
- fun bit b bs = Syntax.const @{const_name Int.Bit} $ bs $ HOLogic.mk_bit b;
+ fun bit b bs = HOLogic.mk_bit b $ bs;
fun mk 0 = (* FIXME funpow z (bit 0) *) (Syntax.const @{const_name Int.Pls})
| mk ~1 = (* FIXME funpow z (bit 1) *) (Syntax.const @{const_name Int.Min})
| mk i = let val (q, r) = Integer.div_mod i 2 in bit r (mk q) end;
@@ -39,15 +39,10 @@
local
-fun dest_bit (Const (@{const_syntax Int.bit.B0}, _)) = 0
- | dest_bit (Const (@{const_syntax Int.bit.B1}, _)) = 1
- | dest_bit (Const ("bit.B0", _)) = 0
- | dest_bit (Const ("bit.B1", _)) = 1
- | dest_bit _ = raise Match;
-
fun dest_bin (Const (@{const_syntax "Int.Pls"}, _)) = []
| dest_bin (Const (@{const_syntax "Int.Min"}, _)) = [~1]
- | dest_bin (Const (@{const_syntax "Int.Bit"}, _) $ bs $ b) = dest_bit b :: dest_bin bs
+ | dest_bin (Const (@{const_syntax "Int.Bit0"}, _) $ bs) = 0 :: dest_bin bs
+ | dest_bin (Const (@{const_syntax "Int.Bit1"}, _) $ bs) = 1 :: dest_bin bs
| dest_bin _ = raise Match;
fun leading _ [] = 0
--- a/src/HOL/Word/BinBoolList.thy Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Word/BinBoolList.thy Sun Feb 17 06:49:53 2008 +0100
@@ -75,24 +75,30 @@
"(butlast ^ n) bl = take (length bl - n) bl"
by (induct n) (auto simp: butlast_take)
-lemma bin_to_bl_aux_Pls_minus_simp:
+lemma bin_to_bl_aux_Pls_minus_simp [simp]:
"0 < n ==> bin_to_bl_aux n Int.Pls bl =
bin_to_bl_aux (n - 1) Int.Pls (False # bl)"
by (cases n) auto
-lemma bin_to_bl_aux_Min_minus_simp:
+lemma bin_to_bl_aux_Min_minus_simp [simp]:
"0 < n ==> bin_to_bl_aux n Int.Min bl =
bin_to_bl_aux (n - 1) Int.Min (True # bl)"
by (cases n) auto
-lemma bin_to_bl_aux_Bit_minus_simp:
+lemma bin_to_bl_aux_Bit_minus_simp [simp]:
"0 < n ==> bin_to_bl_aux n (w BIT b) bl =
bin_to_bl_aux (n - 1) w ((b = bit.B1) # bl)"
by (cases n) auto
-declare bin_to_bl_aux_Pls_minus_simp [simp]
- bin_to_bl_aux_Min_minus_simp [simp]
- bin_to_bl_aux_Bit_minus_simp [simp]
+lemma bin_to_bl_aux_Bit0_minus_simp [simp]:
+ "0 < n ==> bin_to_bl_aux n (Int.Bit0 w) bl =
+ bin_to_bl_aux (n - 1) w (False # bl)"
+ by (cases n) auto
+
+lemma bin_to_bl_aux_Bit1_minus_simp [simp]:
+ "0 < n ==> bin_to_bl_aux n (Int.Bit1 w) bl =
+ bin_to_bl_aux (n - 1) w (True # bl)"
+ by (cases n) auto
(** link between bin and bool list **)
@@ -308,7 +314,7 @@
apply clarsimp
apply safe
apply (erule allE, erule xtr8 [rotated],
- simp add: Bit_def ring_simps cong add : number_of_False_cong)+
+ simp add: numeral_simps ring_simps cong add : number_of_False_cong)+
done
lemma bl_to_bin_lt2p: "bl_to_bin bs < (2 ^ length bs)"
@@ -326,7 +332,7 @@
apply clarsimp
apply safe
apply (erule allE, erule less_eq_less.order_trans [rotated],
- simp add: Bit_def ring_simps cong add : number_of_False_cong)+
+ simp add: numeral_simps ring_simps cong add : number_of_False_cong)+
done
lemma bl_to_bin_ge0: "bl_to_bin bs >= 0"
@@ -370,13 +376,13 @@
apply (case_tac "m - size list")
apply (simp add : diff_is_0_eq [THEN iffD1, THEN Suc_diff_le])
apply simp
- apply (rule_tac f = "%nat. bl_to_bin_aux (bintrunc nat w BIT bit.B1) list"
+ apply (rule_tac f = "%nat. bl_to_bin_aux (Int.Bit1 (bintrunc nat w)) list"
in arg_cong)
apply simp
apply (case_tac "m - size list")
apply (simp add: diff_is_0_eq [THEN iffD1, THEN Suc_diff_le])
apply simp
- apply (rule_tac f = "%nat. bl_to_bin_aux (bintrunc nat w BIT bit.B0) list"
+ apply (rule_tac f = "%nat. bl_to_bin_aux (Int.Bit0 (bintrunc nat w)) list"
in arg_cong)
apply simp
done
--- a/src/HOL/Word/BinGeneral.thy Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Word/BinGeneral.thy Sun Feb 17 06:49:53 2008 +0100
@@ -49,21 +49,37 @@
apply (auto intro: bin_rec'.simps [THEN trans])
done
-lemmas bin_rec_Pls = refl [THEN bin_rec_PM, THEN conjunct1, standard]
-lemmas bin_rec_Min = refl [THEN bin_rec_PM, THEN conjunct2, standard]
+lemma bin_rec_Pls: "bin_rec f1 f2 f3 Int.Pls = f1"
+ unfolding bin_rec_def by simp
+
+lemma bin_rec_Min: "bin_rec f1 f2 f3 Int.Min = f2"
+ unfolding bin_rec_def by simp
+
+lemma bin_rec_Bit0:
+ "f3 Int.Pls bit.B0 f1 = f1 \<Longrightarrow>
+ bin_rec f1 f2 f3 (Int.Bit0 w) = f3 w bit.B0 (bin_rec f1 f2 f3 w)"
+ apply (unfold bin_rec_def)
+ apply (rule bin_rec'.simps [THEN trans])
+ apply (fold bin_rec_def)
+ apply (simp add: eq_Bit0_Pls eq_Bit0_Min bin_rec_Pls)
+ done
+
+lemma bin_rec_Bit1:
+ "f3 Int.Min bit.B1 f2 = f2 \<Longrightarrow>
+ bin_rec f1 f2 f3 (Int.Bit1 w) = f3 w bit.B1 (bin_rec f1 f2 f3 w)"
+ apply (unfold bin_rec_def)
+ apply (rule bin_rec'.simps [THEN trans])
+ apply (fold bin_rec_def)
+ apply (simp add: eq_Bit1_Pls eq_Bit1_Min bin_rec_Min)
+ done
lemma bin_rec_Bit:
"f = bin_rec f1 f2 f3 ==> f3 Int.Pls bit.B0 f1 = f1 ==>
f3 Int.Min bit.B1 f2 = f2 ==> f (w BIT b) = f3 w b (f w)"
- apply clarify
- apply (unfold bin_rec_def)
- apply (rule bin_rec'.simps [THEN trans])
- apply auto
- apply (unfold Pls_def Min_def Bit_def)
- apply (cases b, auto)+
- done
+ by (cases b, simp add: bin_rec_Bit0, simp add: bin_rec_Bit1)
lemmas bin_rec_simps = refl [THEN bin_rec_Bit] bin_rec_Pls bin_rec_Min
+ bin_rec_Bit0 bin_rec_Bit1
subsection {* Destructors for binary integers *}
@@ -92,18 +108,24 @@
"bin_rest Int.Pls = Int.Pls"
"bin_rest Int.Min = Int.Min"
"bin_rest (w BIT b) = w"
+ "bin_rest (Int.Bit0 w) = w"
+ "bin_rest (Int.Bit1 w) = w"
unfolding bin_rest_def by auto
lemma bin_last_simps [simp]:
"bin_last Int.Pls = bit.B0"
"bin_last Int.Min = bit.B1"
"bin_last (w BIT b) = b"
+ "bin_last (Int.Bit0 w) = bit.B0"
+ "bin_last (Int.Bit1 w) = bit.B1"
unfolding bin_last_def by auto
-
+
lemma bin_sign_simps [simp]:
"bin_sign Int.Pls = Int.Pls"
"bin_sign Int.Min = Int.Min"
"bin_sign (w BIT b) = bin_sign w"
+ "bin_sign (Int.Bit0 w) = bin_sign w"
+ "bin_sign (Int.Bit1 w) = bin_sign w"
unfolding bin_sign_def by (auto simp: bin_rec_simps)
lemma bin_r_l_extras [simp]:
@@ -142,6 +164,12 @@
lemma Bit_div2 [simp]: "(w BIT b) div 2 = w"
unfolding bin_rest_div [symmetric] by auto
+lemma Bit0_div2 [simp]: "(Int.Bit0 w) div 2 = w"
+ using Bit_div2 [where b=bit.B0] by simp
+
+lemma Bit1_div2 [simp]: "(Int.Bit1 w) div 2 = w"
+ using Bit_div2 [where b=bit.B1] by simp
+
lemma bin_nth_lem [rule_format]:
"ALL y. bin_nth x = bin_nth y --> x = y"
apply (induct x rule: bin_induct)
@@ -191,11 +219,20 @@
lemma bin_nth_minus [simp]: "0 < n ==> bin_nth (w BIT b) n = bin_nth w (n - 1)"
by (cases n) auto
+lemma bin_nth_minus_Bit0 [simp]:
+ "0 < n ==> bin_nth (Int.Bit0 w) n = bin_nth w (n - 1)"
+ using bin_nth_minus [where b=bit.B0] by simp
+
+lemma bin_nth_minus_Bit1 [simp]:
+ "0 < n ==> bin_nth (Int.Bit1 w) n = bin_nth w (n - 1)"
+ using bin_nth_minus [where b=bit.B1] by simp
+
lemmas bin_nth_0 = bin_nth.simps(1)
lemmas bin_nth_Suc = bin_nth.simps(2)
lemmas bin_nth_simps =
bin_nth_0 bin_nth_Suc bin_nth_Pls bin_nth_Min bin_nth_minus
+ bin_nth_minus_Bit0 bin_nth_minus_Bit1
lemma bin_sign_rest [simp]:
"bin_sign (bin_rest w) = (bin_sign w)"
@@ -277,6 +314,14 @@
"bin_nth (w BIT b) n = (n = 0 & b = bit.B1 | (EX m. n = Suc m & bin_nth w m))"
by (cases n) auto
+lemma bin_nth_Bit0:
+ "bin_nth (Int.Bit0 w) n = (EX m. n = Suc m & bin_nth w m)"
+ using bin_nth_Bit [where b=bit.B0] by simp
+
+lemma bin_nth_Bit1:
+ "bin_nth (Int.Bit1 w) n = (n = 0 | (EX m. n = Suc m & bin_nth w m))"
+ using bin_nth_Bit [where b=bit.B1] by simp
+
lemma bintrunc_bintrunc_l:
"n <= m ==> (bintrunc m (bintrunc n w) = bintrunc n w)"
by (rule bin_eqI) (auto simp add : nth_bintr)
@@ -312,7 +357,16 @@
lemmas bintrunc_BIT [simp] =
bintrunc.Suc [where bin="w BIT b", simplified bin_last_simps bin_rest_simps, standard]
+lemma bintrunc_Bit0 [simp]:
+ "bintrunc (Suc n) (Int.Bit0 w) = Int.Bit0 (bintrunc n w)"
+ using bintrunc_BIT [where b=bit.B0] by simp
+
+lemma bintrunc_Bit1 [simp]:
+ "bintrunc (Suc n) (Int.Bit1 w) = Int.Bit1 (bintrunc n w)"
+ using bintrunc_BIT [where b=bit.B1] by simp
+
lemmas bintrunc_Sucs = bintrunc_Pls bintrunc_Min bintrunc_BIT
+ bintrunc_Bit0 bintrunc_Bit1
lemmas sbintrunc_Suc_Pls =
sbintrunc.Suc [where bin="Int.Pls", simplified bin_last_simps bin_rest_simps, standard]
@@ -323,7 +377,16 @@
lemmas sbintrunc_Suc_BIT [simp] =
sbintrunc.Suc [where bin="w BIT b", simplified bin_last_simps bin_rest_simps, standard]
+lemma sbintrunc_Suc_Bit0 [simp]:
+ "sbintrunc (Suc n) (Int.Bit0 w) = Int.Bit0 (sbintrunc n w)"
+ using sbintrunc_Suc_BIT [where b=bit.B0] by simp
+
+lemma sbintrunc_Suc_Bit1 [simp]:
+ "sbintrunc (Suc n) (Int.Bit1 w) = Int.Bit1 (sbintrunc n w)"
+ using sbintrunc_Suc_BIT [where b=bit.B1] by simp
+
lemmas sbintrunc_Sucs = sbintrunc_Suc_Pls sbintrunc_Suc_Min sbintrunc_Suc_BIT
+ sbintrunc_Suc_Bit0 sbintrunc_Suc_Bit1
lemmas sbintrunc_Pls =
sbintrunc.Z [where bin="Int.Pls",
@@ -341,8 +404,15 @@
sbintrunc.Z [where bin="w BIT bit.B1",
simplified bin_last_simps bin_rest_simps bit.simps, standard]
+lemma sbintrunc_0_Bit0 [simp]: "sbintrunc 0 (Int.Bit0 w) = Int.Pls"
+ using sbintrunc_0_BIT_B0 by simp
+
+lemma sbintrunc_0_Bit1 [simp]: "sbintrunc 0 (Int.Bit1 w) = Int.Min"
+ using sbintrunc_0_BIT_B1 by simp
+
lemmas sbintrunc_0_simps =
sbintrunc_Pls sbintrunc_Min sbintrunc_0_BIT_B0 sbintrunc_0_BIT_B1
+ sbintrunc_0_Bit0 sbintrunc_0_Bit1
lemmas bintrunc_simps = bintrunc.Z bintrunc_Sucs
lemmas sbintrunc_simps = sbintrunc_0_simps sbintrunc_Sucs
@@ -374,7 +444,7 @@
lemmas bintrunc_BIT_I = trans [OF bintrunc_BIT thobini1]
lemmas bintrunc_Min_I = trans [OF bintrunc_Min thobini1]
-lemmas bmsts = bintrunc_minus_simps [THEN thobini1 [THEN [2] trans], standard]
+lemmas bmsts = bintrunc_minus_simps(1-3) [THEN thobini1 [THEN [2] trans], standard]
lemmas bintrunc_Pls_minus_I = bmsts(1)
lemmas bintrunc_Min_minus_I = bmsts(2)
lemmas bintrunc_BIT_minus_I = bmsts(3)
@@ -394,10 +464,10 @@
lemmas sbintrunc_BIT_I = trans [OF sbintrunc_Suc_BIT thobini1]
lemmas sbintrunc_Suc_Is =
- sbintrunc_Sucs [THEN thobini1 [THEN [2] trans], standard]
+ sbintrunc_Sucs(1-3) [THEN thobini1 [THEN [2] trans], standard]
lemmas sbintrunc_Suc_minus_Is =
- sbintrunc_minus_simps [THEN thobini1 [THEN [2] trans], standard]
+ sbintrunc_minus_simps(1-3) [THEN thobini1 [THEN [2] trans], standard]
lemma sbintrunc_Suc_lem:
"sbintrunc (Suc n) x = y ==> m = Suc n ==> sbintrunc m x = y"
@@ -573,11 +643,11 @@
lemma sign_Pls_ge_0:
"(bin_sign bin = Int.Pls) = (number_of bin >= (0 :: int))"
- by (induct bin rule: bin_induct) auto
+ by (induct bin rule: numeral_induct) auto
lemma sign_Min_lt_0:
"(bin_sign bin = Int.Min) = (number_of bin < (0 :: int))"
- by (induct bin rule: bin_induct) auto
+ by (induct bin rule: numeral_induct) auto
lemmas sign_Min_neg = trans [OF sign_Min_lt_0 neg_def [symmetric]]
@@ -725,5 +795,4 @@
lemmas s2n_ths = n2s_ths [symmetric]
-
end
--- a/src/HOL/Word/BinOperations.thy Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Word/BinOperations.thy Sun Feb 17 06:49:53 2008 +0100
@@ -44,7 +44,9 @@
"NOT Int.Pls = Int.Min"
"NOT Int.Min = Int.Pls"
"NOT (w BIT b) = (NOT w) BIT (NOT b)"
- by (unfold int_not_def) (auto intro: bin_rec_simps)
+ "NOT (Int.Bit0 w) = Int.Bit1 (NOT w)"
+ "NOT (Int.Bit1 w) = Int.Bit0 (NOT w)"
+ unfolding int_not_def by (simp_all add: bin_rec_simps)
lemma int_xor_Pls [simp]:
"Int.Pls XOR x = x"
@@ -65,6 +67,13 @@
apply (simp add: int_not_simps [symmetric])
done
+lemma int_xor_Bits2 [simp]:
+ "(Int.Bit0 x) XOR (Int.Bit0 y) = Int.Bit0 (x XOR y)"
+ "(Int.Bit0 x) XOR (Int.Bit1 y) = Int.Bit1 (x XOR y)"
+ "(Int.Bit1 x) XOR (Int.Bit0 y) = Int.Bit1 (x XOR y)"
+ "(Int.Bit1 x) XOR (Int.Bit1 y) = Int.Bit0 (x XOR y)"
+ unfolding BIT_simps [symmetric] int_xor_Bits by simp_all
+
lemma int_xor_x_simps':
"w XOR (Int.Pls BIT bit.B0) = w"
"w XOR (Int.Min BIT bit.B1) = NOT w"
@@ -74,7 +83,10 @@
apply clarsimp+
done
-lemmas int_xor_extra_simps [simp] = int_xor_x_simps' [simplified arith_simps]
+lemma int_xor_extra_simps [simp]:
+ "w XOR Int.Pls = w"
+ "w XOR Int.Min = NOT w"
+ using int_xor_x_simps' by simp_all
lemma int_or_Pls [simp]:
"Int.Pls OR x = x"
@@ -88,6 +100,13 @@
"(x BIT b) OR (y BIT c) = (x OR y) BIT (b OR c)"
unfolding int_or_def by (simp add: bin_rec_simps)
+lemma int_or_Bits2 [simp]:
+ "(Int.Bit0 x) OR (Int.Bit0 y) = Int.Bit0 (x OR y)"
+ "(Int.Bit0 x) OR (Int.Bit1 y) = Int.Bit1 (x OR y)"
+ "(Int.Bit1 x) OR (Int.Bit0 y) = Int.Bit1 (x OR y)"
+ "(Int.Bit1 x) OR (Int.Bit1 y) = Int.Bit1 (x OR y)"
+ unfolding BIT_simps [symmetric] int_or_Bits by simp_all
+
lemma int_or_x_simps':
"w OR (Int.Pls BIT bit.B0) = w"
"w OR (Int.Min BIT bit.B1) = Int.Min"
@@ -97,8 +116,10 @@
apply clarsimp+
done
-lemmas int_or_extra_simps [simp] = int_or_x_simps' [simplified arith_simps]
-
+lemma int_or_extra_simps [simp]:
+ "w OR Int.Pls = w"
+ "w OR Int.Min = Int.Min"
+ using int_or_x_simps' by simp_all
lemma int_and_Pls [simp]:
"Int.Pls AND x = Int.Pls"
@@ -112,6 +133,13 @@
"(x BIT b) AND (y BIT c) = (x AND y) BIT (b AND c)"
unfolding int_and_def by (simp add: bin_rec_simps)
+lemma int_and_Bits2 [simp]:
+ "(Int.Bit0 x) AND (Int.Bit0 y) = Int.Bit0 (x AND y)"
+ "(Int.Bit0 x) AND (Int.Bit1 y) = Int.Bit0 (x AND y)"
+ "(Int.Bit1 x) AND (Int.Bit0 y) = Int.Bit0 (x AND y)"
+ "(Int.Bit1 x) AND (Int.Bit1 y) = Int.Bit1 (x AND y)"
+ unfolding BIT_simps [symmetric] int_and_Bits by simp_all
+
lemma int_and_x_simps':
"w AND (Int.Pls BIT bit.B0) = Int.Pls"
"w AND (Int.Min BIT bit.B1) = w"
@@ -121,7 +149,10 @@
apply clarsimp+
done
-lemmas int_and_extra_simps [simp] = int_and_x_simps' [simplified arith_simps]
+lemma int_and_extra_simps [simp]:
+ "w AND Int.Pls = Int.Pls"
+ "w AND Int.Min = w"
+ using int_and_x_simps' by simp_all
(* commutativity of the above *)
lemma bin_ops_comm:
@@ -194,7 +225,7 @@
apply (case_tac [!] z rule: bin_exhaust)
apply (case_tac [!] bit)
apply (case_tac [!] b)
- apply auto
+ apply (auto simp del: BIT_simps)
done
lemma int_and_assoc:
@@ -225,7 +256,7 @@
apply (induct x rule: bin_induct)
apply auto
apply (case_tac [!] y rule: bin_exhaust)
- apply (case_tac [!] bit, auto)
+ apply (case_tac [!] bit, auto simp del: BIT_simps)
done
lemma bbw_oa_dist:
@@ -235,7 +266,7 @@
apply auto
apply (case_tac y rule: bin_exhaust)
apply (case_tac z rule: bin_exhaust)
- apply (case_tac ba, auto)
+ apply (case_tac ba, auto simp del: BIT_simps)
done
lemma bbw_ao_dist:
@@ -245,7 +276,7 @@
apply auto
apply (case_tac y rule: bin_exhaust)
apply (case_tac z rule: bin_exhaust)
- apply (case_tac ba, auto)
+ apply (case_tac ba, auto simp del: BIT_simps)
done
(*
@@ -289,9 +320,9 @@
apply (induct n)
apply safe
apply (case_tac [!] x rule: bin_exhaust)
- apply simp_all
+ apply (simp_all del: BIT_simps)
apply (case_tac [!] y rule: bin_exhaust)
- apply simp_all
+ apply (simp_all del: BIT_simps)
apply (auto dest: not_B1_is_B0 intro: B1_ass_B0)
done
@@ -392,7 +423,7 @@
"!!w. bin_sc n bit.B0 w <= w"
apply (induct n)
apply (case_tac [!] w rule: bin_exhaust)
- apply auto
+ apply (auto simp del: BIT_simps)
apply (unfold Bit_def)
apply (simp_all split: bit.split)
done
@@ -401,7 +432,7 @@
"!!w. bin_sc n bit.B1 w >= w"
apply (induct n)
apply (case_tac [!] w rule: bin_exhaust)
- apply auto
+ apply (auto simp del: BIT_simps)
apply (unfold Bit_def)
apply (simp_all split: bit.split)
done
@@ -412,7 +443,7 @@
apply simp
apply (case_tac w rule: bin_exhaust)
apply (case_tac m)
- apply auto
+ apply (auto simp del: BIT_simps)
apply (unfold Bit_def)
apply (simp_all split: bit.split)
done
@@ -423,7 +454,7 @@
apply simp
apply (case_tac w rule: bin_exhaust)
apply (case_tac m)
- apply auto
+ apply (auto simp del: BIT_simps)
apply (unfold Bit_def)
apply (simp_all split: bit.split)
done
--- a/src/HOL/Word/BitSyntax.thy Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Word/BitSyntax.thy Sun Feb 17 06:49:53 2008 +0100
@@ -9,7 +9,7 @@
header {* Syntactic class for bitwise operations *}
theory BitSyntax
-imports Main
+imports Main Num_Lemmas
begin
class bit = type +
@@ -43,7 +43,7 @@
shiftr :: "'a::bit \<Rightarrow> nat \<Rightarrow> 'a" (infixl ">>" 55)
-subsection {* Bitwise operations on type @{typ bit} *}
+subsection {* Bitwise operations on @{typ bit} *}
instantiation bit :: bit
begin
--- a/src/HOL/Word/Examples/WordExamples.thy Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Word/Examples/WordExamples.thy Sun Feb 17 06:49:53 2008 +0100
@@ -92,7 +92,7 @@
lemma "\<not> (0b1000 :: 3 word) !! 4" by simp
lemma "(0b11000 :: 10 word) !! n = (n = 4 \<or> n = 3)"
- by (auto simp add: bin_nth_Bit)
+ by (auto simp add: bin_nth_Bit0 bin_nth_Bit1)
lemma "set_bit 55 7 True = (183::'a::len0 word)" by simp
lemma "set_bit 0b0010 7 True = (0b10000010::'a::len0 word)" by simp
--- a/src/HOL/Word/Num_Lemmas.thy Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Word/Num_Lemmas.thy Sun Feb 17 06:49:53 2008 +0100
@@ -9,6 +9,22 @@
imports Main Parity
begin
+datatype bit = B0 | B1
+
+definition
+ Bit :: "int \<Rightarrow> bit \<Rightarrow> int" (infixl "BIT" 90) where
+ [code func del]: "k BIT b = (case b of B0 \<Rightarrow> 0 | B1 \<Rightarrow> 1) + k + k"
+
+lemma BIT_B0_eq_Bit0 [simp]: "w BIT B0 = Int.Bit0 w"
+ unfolding Bit_def Bit0_def by simp
+
+lemma BIT_B1_eq_Bit1 [simp]: "w BIT B1 = Int.Bit1 w"
+ unfolding Bit_def Bit1_def by simp
+
+lemmas BIT_simps = BIT_B0_eq_Bit0 BIT_B1_eq_Bit1
+
+hide (open) const B0 B1
+
lemma contentsI: "y = {x} ==> contents y = x"
unfolding contents_def by auto
@@ -197,8 +213,13 @@
apply auto
done
-lemmas bin_rl_simps [THEN bin_rl_char [THEN iffD2], standard, simp] =
- Pls_0_eq Min_1_eq refl
+lemma bin_rl_simps [simp]:
+ "bin_rl Int.Pls = (Int.Pls, bit.B0)"
+ "bin_rl Int.Min = (Int.Min, bit.B1)"
+ "bin_rl (r BIT b) = (r, b)"
+ "bin_rl (Int.Bit0 r) = (r, bit.B0)"
+ "bin_rl (Int.Bit1 r) = (r, bit.B1)"
+ unfolding bin_rl_char by simp_all
lemma bin_abs_lem:
"bin = (w BIT b) ==> ~ bin = Int.Min --> ~ bin = Int.Pls -->
@@ -223,6 +244,24 @@
apply (auto simp add : PPls PMin PBit)
done
+lemma numeral_induct:
+ assumes Pls: "P Int.Pls"
+ assumes Min: "P Int.Min"
+ assumes Bit0: "\<And>w. \<lbrakk>P w; w \<noteq> Int.Pls\<rbrakk> \<Longrightarrow> P (Int.Bit0 w)"
+ assumes Bit1: "\<And>w. \<lbrakk>P w; w \<noteq> Int.Min\<rbrakk> \<Longrightarrow> P (Int.Bit1 w)"
+ shows "P x"
+ apply (induct x rule: bin_induct)
+ apply (rule Pls)
+ apply (rule Min)
+ apply (case_tac bit)
+ apply (case_tac "bin = Int.Pls")
+ apply simp
+ apply (simp add: Bit0)
+ apply (case_tac "bin = Int.Min")
+ apply simp
+ apply (simp add: Bit1)
+ done
+
lemma no_no [simp]: "number_of (number_of i) = i"
unfolding number_of_eq by simp
@@ -245,9 +284,12 @@
apply (simp (no_asm) only: Bit_B0 Bit_B1)
apply (simp add: z1pmod2)
done
-
-lemmas B1_mod_2 [simp] = B_mod_2' [OF refl, THEN conjunct1, standard]
-lemmas B0_mod_2 [simp] = B_mod_2' [OF refl, THEN conjunct2, standard]
+
+lemma B1_mod_2 [simp]: "(Int.Bit1 w) mod 2 = 1"
+ unfolding numeral_simps number_of_is_id by (simp add: z1pmod2)
+
+lemma B0_mod_2 [simp]: "(Int.Bit0 w) mod 2 = 0"
+ unfolding numeral_simps number_of_is_id by simp
lemma axxbyy:
"a + m + m = b + n + n ==> (a = 0 | a = 1) ==> (b = 0 | b = 1) ==>
--- a/src/HOL/Word/WordArith.thy Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Word/WordArith.thy Sun Feb 17 06:49:53 2008 +0100
@@ -395,7 +395,7 @@
lemma word_zero_neq_one: "0 < len_of TYPE ('a :: len0) ==> (0 :: 'a word) ~= 1";
unfolding word_arith_wis
- by (auto simp add: word_ubin.norm_eq_iff [symmetric] gr0_conv_Suc)
+ by (auto simp add: word_ubin.norm_eq_iff [symmetric] gr0_conv_Suc eq_Bit0_Bit1)
lemmas lenw1_zero_neq_one = len_gt_0 [THEN word_zero_neq_one]
--- a/src/HOL/Word/WordMain.thy Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Word/WordMain.thy Sun Feb 17 06:49:53 2008 +0100
@@ -10,7 +10,7 @@
theory WordMain imports WordGenLib
begin
-lemmas word_no_1 [simp] = word_1_no [symmetric]
+lemmas word_no_1 [simp] = word_1_no [symmetric, unfolded BIT_simps]
lemmas word_no_0 [simp] = word_0_no [symmetric]
declare word_0_bl [simp]
--- a/src/HOL/Word/WordShift.thy Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Word/WordShift.thy Sun Feb 17 06:49:53 2008 +0100
@@ -14,7 +14,8 @@
lemma shiftl1_number [simp] :
"shiftl1 (number_of w) = number_of (w BIT bit.B0)"
apply (unfold shiftl1_def word_number_of_def)
- apply (simp add: word_ubin.norm_eq_iff [symmetric] word_ubin.eq_norm)
+ apply (simp add: word_ubin.norm_eq_iff [symmetric] word_ubin.eq_norm
+ del: BIT_simps)
apply (subst refl [THEN bintrunc_BIT_I, symmetric])
apply (subst bintrunc_bintrunc_min)
apply simp
@@ -331,13 +332,13 @@
lemma shiftl1_2t: "shiftl1 (w :: 'a :: len word) = 2 * w"
apply (simp add: shiftl1_def_u)
- apply (simp only: double_number_of_BIT [symmetric])
+ apply (simp only: double_number_of_Bit0 [symmetric])
apply simp
done
lemma shiftl1_p: "shiftl1 (w :: 'a :: len word) = w + w"
apply (simp add: shiftl1_def_u)
- apply (simp only: double_number_of_BIT [symmetric])
+ apply (simp only: double_number_of_Bit0 [symmetric])
apply simp
done
--- a/src/HOL/hologic.ML Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/hologic.ML Sun Feb 17 06:49:53 2008 +0100
@@ -88,15 +88,13 @@
val class_size: string
val size_const: typ -> term
val indexT: typ
- val bitT: typ
- val B0_const: term
- val B1_const: term
- val mk_bit: int -> term
- val dest_bit: term -> int
val intT: typ
val pls_const: term
val min_const: term
- val bit_const: term
+ val bit0_const: term
+ val bit1_const: term
+ val mk_bit: int -> term
+ val dest_bit: term -> int
val mk_numeral: int -> term
val dest_numeral: term -> int
val number_of_const: typ -> term
@@ -452,39 +450,33 @@
val indexT = Type ("Code_Index.index", []);
-(* bit *)
-
-val bitT = Type ("Int.bit", []);
-
-val B0_const = Const ("Int.bit.B0", bitT);
-val B1_const = Const ("Int.bit.B1", bitT);
-
-fun mk_bit 0 = B0_const
- | mk_bit 1 = B1_const
- | mk_bit _ = raise TERM ("mk_bit", []);
-
-fun dest_bit (Const ("Int.bit.B0", _)) = 0
- | dest_bit (Const ("Int.bit.B1", _)) = 1
- | dest_bit t = raise TERM ("dest_bit", [t]);
-
-
(* binary numerals and int -- non-unique representation due to leading zeros/ones! *)
val intT = Type ("Int.int", []);
val pls_const = Const ("Int.Pls", intT)
and min_const = Const ("Int.Min", intT)
-and bit_const = Const ("Int.Bit", intT --> bitT --> intT);
+and bit0_const = Const ("Int.Bit0", intT --> intT)
+and bit1_const = Const ("Int.Bit1", intT --> intT);
+
+fun mk_bit 0 = bit0_const
+ | mk_bit 1 = bit1_const
+ | mk_bit _ = raise TERM ("mk_bit", []);
+
+fun dest_bit (Const ("Int.Bit0", _)) = 0
+ | dest_bit (Const ("Int.Bit1", _)) = 1
+ | dest_bit t = raise TERM ("dest_bit", [t]);
fun mk_numeral 0 = pls_const
| mk_numeral ~1 = min_const
| mk_numeral i =
let val (q, r) = Integer.div_mod i 2;
- in bit_const $ mk_numeral q $ mk_bit r end;
+ in mk_bit r $ mk_numeral q end;
fun dest_numeral (Const ("Int.Pls", _)) = 0
| dest_numeral (Const ("Int.Min", _)) = ~1
- | dest_numeral (Const ("Int.Bit", _) $ bs $ b) = 2 * dest_numeral bs + dest_bit b
+ | dest_numeral (Const ("Int.Bit0", _) $ bs) = 2 * dest_numeral bs
+ | dest_numeral (Const ("Int.Bit1", _) $ bs) = 2 * dest_numeral bs + 1
| dest_numeral t = raise TERM ("dest_numeral", [t]);
fun number_of_const T = Const ("Int.number_class.number_of", intT --> T);
--- a/src/HOL/int_arith1.ML Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/int_arith1.ML Sun Feb 17 06:49:53 2008 +0100
@@ -548,7 +548,7 @@
simp_thms @ @{thms arith_simps} @ @{thms rel_simps} @ @{thms arith_special} @
[@{thm neg_le_iff_le}, @{thm numeral_0_eq_0}, @{thm numeral_1_eq_1},
@{thm minus_zero}, @{thm diff_minus}, @{thm left_minus}, @{thm right_minus},
- @{thm mult_zero_left}, @{thm mult_zero_right}, @{thm mult_num1}, @{thm mult_1_right},
+ @{thm mult_zero_left}, @{thm mult_zero_right}, @{thm mult_Bit1}, @{thm mult_1_right},
@{thm minus_mult_left} RS sym, @{thm minus_mult_right} RS sym,
@{thm minus_add_distrib}, @{thm minus_minus}, @{thm mult_assoc},
@{thm of_nat_0}, @{thm of_nat_1}, @{thm of_nat_Suc}, @{thm of_nat_add},
--- a/src/HOL/int_factor_simprocs.ML Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/int_factor_simprocs.ML Sun Feb 17 06:49:53 2008 +0100
@@ -43,7 +43,7 @@
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
[@{thm add_0}, @{thm add_0_right}, @{thm mult_zero_left},
- @{thm mult_zero_right}, @{thm mult_num1}, @{thm mult_1_right}];
+ @{thm mult_zero_right}, @{thm mult_Bit1}, @{thm mult_1_right}];
end
(*Version for integer division*)
--- a/src/Tools/code/code_target.ML Sat Feb 16 16:52:09 2008 +0100
+++ b/src/Tools/code/code_target.ML Sun Feb 17 06:49:53 2008 +0100
@@ -23,7 +23,7 @@
val add_pretty_list_string: string -> string -> string
-> string -> string list -> theory -> theory;
val add_pretty_char: string -> string -> string list -> theory -> theory
- val add_pretty_numeral: string -> bool -> bool -> string -> string -> string -> string
+ val add_pretty_numeral: string -> bool -> bool -> string -> string -> string
-> string -> string -> theory -> theory;
val add_pretty_message: string -> string -> string list -> string
-> string -> string -> theory -> theory;
@@ -234,7 +234,7 @@
else NONE
end;
-fun implode_numeral negative c_bit0 c_bit1 c_pls c_min c_bit =
+fun implode_numeral negative c_pls c_min c_bit0 c_bit1 =
let
fun dest_bit (IConst (c, _)) = if c = c_bit0 then 0
else if c = c_bit1 then 1
@@ -244,10 +244,9 @@
else if c = c_min then
if negative then SOME ~1 else NONE
else error "Illegal numeral expression: illegal leading digit"
- | dest_numeral (IConst (c, _) `$ t1 `$ t2) =
- if c = c_bit then let val (n, b) = (dest_numeral t1, dest_bit t2)
- in case n of SOME n => SOME (2 * n + b) | NONE => NONE end
- else error "Illegal numeral expression: illegal bit shift operator"
+ | dest_numeral (t1 `$ t2) =
+ let val (n, b) = (dest_numeral t2, dest_bit t1)
+ in case n of SOME n => SOME (2 * n + b) | NONE => NONE end
| dest_numeral _ = error "Illegal numeral expression: illegal constant";
in dest_numeral #> the_default 0 end;
@@ -1825,11 +1824,11 @@
| NONE => error "Illegal character expression";
in (2, pretty) end;
-fun pretty_numeral unbounded negative c_bit0 c_bit1 c_pls c_min c_bit target =
+fun pretty_numeral unbounded negative c_pls c_min c_bit0 c_bit1 target =
let
val mk_numeral = #pretty_numeral (pr_pretty target);
fun pretty _ _ _ [(t, _)] =
- (str o mk_numeral unbounded o implode_numeral negative c_bit0 c_bit1 c_pls c_min c_bit) t;
+ (str o mk_numeral unbounded o implode_numeral negative c_pls c_min c_bit0 c_bit1) t;
in (1, pretty) end;
fun pretty_message c_char c_nibbles c_nil c_cons target =
@@ -2100,14 +2099,13 @@
|> add_syntax_const target charr (SOME pr)
end;
-fun add_pretty_numeral target unbounded negative number_of b0 b1 pls min bit thy =
+fun add_pretty_numeral target unbounded negative number_of pls min bit0 bit1 thy =
let
- val b0' = CodeName.const thy b0;
- val b1' = CodeName.const thy b1;
val pls' = CodeName.const thy pls;
val min' = CodeName.const thy min;
- val bit' = CodeName.const thy bit;
- val pr = pretty_numeral unbounded negative b0' b1' pls' min' bit' target;
+ val bit0' = CodeName.const thy bit0;
+ val bit1' = CodeName.const thy bit1;
+ val pr = pretty_numeral unbounded negative pls' min' bit0' bit1' target;
in
thy
|> add_syntax_const target number_of (SOME pr)