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