Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants

--- a/src/HOL/Integ/Bin.ML	Fri Sep 25 13:18:07 1998 +0200
+++ b/src/HOL/Integ/Bin.ML	Fri Sep 25 13:57:01 1998 +0200
@@ -393,35 +393,59 @@
 		neg_eq_less_0, iszero_def] @ zcompare_rls;
 
 
-(*** nat_of ***)
+(*** nat ***)
 
-Goal "#0 <= z ==> $# (nat_of z) = z"; 
+Goal "#0 <= z ==> $# (nat z) = z"; 
 by (asm_full_simp_tac
-    (simpset() addsimps [neg_eq_less_0, zle_def, not_neg_nat_of]) 1); 
-qed "nat_of_0_le"; 
+    (simpset() addsimps [neg_eq_less_0, zle_def, not_neg_nat]) 1); 
+qed "nat_0_le"; 
 
-Goal "z < #0 ==> nat_of z = 0"; 
+Goal "z < #0 ==> nat z = 0"; 
 by (asm_full_simp_tac
-    (simpset() addsimps [neg_eq_less_0, zle_def, neg_nat_of]) 1); 
-qed "nat_of_less_0"; 
+    (simpset() addsimps [neg_eq_less_0, zle_def, neg_nat]) 1); 
+qed "nat_less_0"; 
 
-Addsimps [nat_of_0_le, nat_of_less_0];
+Addsimps [nat_0_le, nat_less_0];
 
-Goal "#0 <= w ==> (nat_of w = m) = (w = $# m)";
+Goal "#0 <= w ==> (nat w = m) = (w = $# m)";
 by Auto_tac;
-qed "nat_of_eq_iff";
+qed "nat_eq_iff";
 
-Goal "#0 <= w ==> (nat_of w < m) = (w < $# m)";
+Goal "#0 <= w ==> (nat w < m) = (w < $# m)";
 by (rtac iffI 1);
 by (asm_full_simp_tac 
     (simpset() delsimps [zless_eq_less] addsimps [zless_eq_less RS sym]) 2);
-by (etac (nat_of_0_le RS subst) 1);
+by (etac (nat_0_le RS subst) 1);
 by (Simp_tac 1);
-qed "nat_of_less_iff";
+qed "nat_less_iff";
 
-Goal "#0 <= w ==> (nat_of w < nat_of z) = (w<z)";
+Goal "#0 <= w ==> (nat w < nat z) = (w<z)";
 by (case_tac "neg z" 1);
-by (auto_tac (claset(), simpset() addsimps [nat_of_less_iff]));
+by (auto_tac (claset(), simpset() addsimps [nat_less_iff]));
 by (auto_tac (claset() addIs [zless_trans], 
 	      simpset() addsimps [neg_eq_less_0, integ_of_Pls, zle_def]));
-qed "nat_of_less_eq_zless";
+qed "nat_less_eq_zless";
+
+Goal "#0 <= w ==> (nat w < nat z) = (w<z)";
+by (stac nat_less_iff 1);
+ba 1;
+by (case_tac "neg z" 1);
+by (auto_tac (claset(), simpset() addsimps [not_neg_nat, neg_nat]));
+by (auto_tac (claset(), 
+	      simpset() addsimps [neg_eq_less_0, integ_of_Pls, zle_def]));
+by (blast_tac (claset() addIs [zless_trans]) 1);
+qed "nat_less_eq_zless";
+
+
+(**Can these be generalized without evaluating large numbers?**)
+Goal "($# k = #0) = (k=0)";
+by (simp_tac (simpset() addsimps [integ_of_Pls]) 1);
+qed "nat_eq_0_conv";
+
+Goal "(#0 = $# k) = (k=0)";
+by (auto_tac (claset(), simpset() addsimps [integ_of_Pls]));
+qed "nat_eq_0_conv'";
+
+Addsimps [nat_eq_0_conv, nat_eq_0_conv'];
+
+

--- a/src/HOL/Integ/Bin.thy	Fri Sep 25 13:18:07 1998 +0200
+++ b/src/HOL/Integ/Bin.thy	Fri Sep 25 13:57:01 1998 +0200
@@ -22,7 +22,7 @@
 quoting the previously computed values.  (Or code an oracle...)
 *)
 
-Bin = Integ + Datatype +
+Bin = Int + Datatype +
 
 syntax
   "_Int"           :: xnum => int        ("_")

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Integ/Int.ML	Fri Sep 25 13:57:01 1998 +0200
@@ -0,0 +1,200 @@
+(*  Title:      HOL/Integ/Int.ML
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+Type "int" is a linear order
+*)
+
+Goal "(w<z) = neg(w-z)";
+by (simp_tac (simpset() addsimps [zless_def]) 1);
+qed "zless_eq_neg";
+
+Goal "(w=z) = iszero(w-z)";
+by (simp_tac (simpset() addsimps [iszero_def, zdiff_eq_eq]) 1);
+qed "eq_eq_iszero";
+
+Goal "(w<=z) = (~ neg(z-w))";
+by (simp_tac (simpset() addsimps [zle_def, zless_def]) 1);
+qed "zle_eq_not_neg";
+
+(*This list of rewrites simplifies (in)equalities by subtracting the RHS
+  from the LHS, then using the cancellation simproc.  Use with zadd_ac.*)
+val zcompare_0_rls = 
+    [zdiff_def, zless_eq_neg, eq_eq_iszero, zle_eq_not_neg];
+
+
+(*** Monotonicity results ***)
+
+Goal "(v+z < w+z) = (v < (w::int))";
+by (full_simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1);
+qed "zadd_right_cancel_zless";
+
+Goal "(z+v < z+w) = (v < (w::int))";
+by (full_simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1);
+qed "zadd_left_cancel_zless";
+
+Addsimps [zadd_right_cancel_zless, zadd_left_cancel_zless];
+
+Goal "(v+z <= w+z) = (v <= (w::int))";
+by (full_simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1);
+qed "zadd_right_cancel_zle";
+
+Goal "(z+v <= z+w) = (v <= (w::int))";
+by (full_simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1);
+qed "zadd_left_cancel_zle";
+
+Addsimps [zadd_right_cancel_zle, zadd_left_cancel_zle];
+
+(*"v<=w ==> v+z <= w+z"*)
+bind_thm ("zadd_zless_mono1", zadd_right_cancel_zless RS iffD2);
+
+(*"v<=w ==> v+z <= w+z"*)
+bind_thm ("zadd_zle_mono1", zadd_right_cancel_zle RS iffD2);
+
+Goal "!!z z'::int. [| w'<=w; z'<=z |] ==> w' + z' <= w + z";
+by (etac (zadd_zle_mono1 RS zle_trans) 1);
+by (Simp_tac 1);
+qed "zadd_zle_mono";
+
+Goal "!!z z'::int. [| w'<w; z'<=z |] ==> w' + z' < w + z";
+by (etac (zadd_zless_mono1 RS zless_zle_trans) 1);
+by (Simp_tac 1);
+qed "zadd_zless_mono";
+
+
+(*** Comparison laws ***)
+
+Goal "(- x < - y) = (y < (x::int))";
+by (simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1);
+qed "zminus_zless_zminus"; 
+Addsimps [zminus_zless_zminus];
+
+Goal "(- x <= - y) = (y <= (x::int))";
+by (simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1);
+qed "zminus_zle_zminus"; 
+Addsimps [zminus_zle_zminus];
+
+(** The next several equations can make the simplifier loop! **)
+
+Goal "(x < - y) = (y < - (x::int))";
+by (simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1);
+qed "zless_zminus"; 
+
+Goal "(- x < y) = (- y < (x::int))";
+by (simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1);
+qed "zminus_zless"; 
+
+Goal "(x <= - y) = (y <= - (x::int))";
+by (simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1);
+qed "zle_zminus"; 
+
+Goal "(- x <= y) = (- y <= (x::int))";
+by (simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1);
+qed "zminus_zle"; 
+
+Goal "- $# Suc n < $# 0";
+by (simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1);
+qed "negative_zless_0"; 
+
+Goal "- $# Suc n < $# m";
+by (rtac (negative_zless_0 RS zless_zle_trans) 1);
+by (Simp_tac 1); 
+qed "negative_zless"; 
+AddIffs [negative_zless]; 
+
+Goal "- $# n <= $#0";
+by (simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1);
+qed "negative_zle_0"; 
+
+Goal "- $# n <= $# m";
+by (simp_tac (simpset() addsimps add_nat :: zcompare_0_rls @ zadd_ac) 1);
+qed "negative_zle"; 
+AddIffs [negative_zle]; 
+
+Goal "~($# 0 <= - $# Suc n)";
+by (stac zle_zminus 1);
+by (Simp_tac 1);
+qed "not_zle_0_negative"; 
+Addsimps [not_zle_0_negative]; 
+
+Goal "($# n <= - $# m) = (n = 0 & m = 0)"; 
+by Safe_tac; 
+by (Simp_tac 3); 
+by (dtac (zle_zminus RS iffD1) 2); 
+by (ALLGOALS (dtac (negative_zle_0 RSN(2,zle_trans)))); 
+by (ALLGOALS Asm_full_simp_tac); 
+qed "int_zle_neg"; 
+
+Goal "~($# n < - $# m)";
+by (simp_tac (simpset() addsimps [symmetric zle_def]) 1); 
+qed "not_int_zless_negative"; 
+
+Goal "(- $# n = $# m) = (n = 0 & m = 0)"; 
+by (rtac iffI 1);
+by (rtac (int_zle_neg RS iffD1) 1); 
+by (dtac sym 1); 
+by (ALLGOALS Asm_simp_tac); 
+qed "negative_eq_positive"; 
+
+Addsimps [negative_eq_positive, not_int_zless_negative]; 
+
+
+Goal "(w <= z) = (EX n. z = w + $# n)";
+by (auto_tac (claset(),
+	      simpset() addsimps [zless_iff_Suc_zadd, integ_le_less]));
+by (ALLGOALS (full_simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac)));
+by (ALLGOALS (full_simp_tac (simpset() addsimps [iszero_def])));
+by (blast_tac (claset() addIs [Suc_pred RS sym]) 1);
+qed "zle_iff_zadd";
+
+
+Goalw [zdiff_def,zless_def] "neg x = (x < $# 0)";
+by Auto_tac; 
+qed "neg_eq_less_nat0"; 
+
+Goalw [zle_def] "(~neg x) = ($# 0 <= x)";
+by (simp_tac (simpset() addsimps [neg_eq_less_nat0]) 1); 
+qed "not_neg_eq_ge_nat0"; 
+
+
+(**** nat: magnitide of an integer, as a natural number ****)
+
+Goalw [nat_def] "nat($# n) = n";
+by Auto_tac;
+qed "nat_nat";
+
+Goalw [nat_def] "nat(- $# n) = 0";
+by (auto_tac (claset(),
+	      simpset() addsimps [neg_eq_less_nat0, zminus_zless])); 
+qed "nat_zminus_nat";
+
+Addsimps [nat_nat, nat_zminus_nat];
+
+Goal "~ neg z ==> $# (nat z) = z"; 
+by (dtac (not_neg_eq_ge_nat0 RS iffD1) 1); 
+by (dtac zle_imp_zless_or_eq 1); 
+by (auto_tac (claset(), simpset() addsimps [zless_iff_Suc_zadd])); 
+qed "not_neg_nat"; 
+
+Goal "neg x ==> ? n. x = - $# Suc n"; 
+by (auto_tac (claset(), 
+	      simpset() addsimps [neg_eq_less_nat0, zless_iff_Suc_zadd,
+				  zdiff_eq_eq RS sym, zdiff_def])); 
+qed "negD"; 
+
+Goalw [nat_def] "neg z ==> nat z = 0"; 
+by Auto_tac; 
+qed "neg_nat"; 
+
+(* a case theorem distinguishing positive and negative int *)  
+
+val prems = Goal "[|!! n. P ($# n); !! n. P (- $# Suc n) |] ==> P z"; 
+by (case_tac "neg z" 1); 
+by (blast_tac (claset() addSDs [negD] addSIs prems) 1); 
+by (etac (not_neg_nat RS subst) 1);
+by (resolve_tac prems 1);
+qed "int_cases"; 
+
+fun int_case_tac x = res_inst_tac [("z",x)] int_cases; 
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Integ/Int.thy	Fri Sep 25 13:57:01 1998 +0200
@@ -0,0 +1,18 @@
+(*  Title:      Integ/Int.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+Type "int" is a linear order
+*)
+
+Int = IntDef +
+
+instance int :: order (zle_refl,zle_trans,zle_anti_sym,int_less_le)
+instance int :: linorder (zle_linear)
+
+constdefs
+  nat  :: int => nat
+  "nat(Z) == if neg Z then 0 else (@ m. Z = $# m)"
+
+end

--- a/src/HOL/Integ/IntDef.ML	Fri Sep 25 13:18:07 1998 +0200
+++ b/src/HOL/Integ/IntDef.ML	Fri Sep 25 13:57:01 1998 +0200
@@ -81,11 +81,11 @@
 qed "inj_Rep_Integ";
 
 
-(** nat: the injection from nat to Integ **)
+(** int: the injection from "nat" to "int" **)
 
-Goal "inj(nat)";
+Goal "inj int";
 by (rtac injI 1);
-by (rewtac nat_def);
+by (rewtac int_def);
 by (dtac (inj_on_Abs_Integ RS inj_onD) 1);
 by (REPEAT (rtac intrel_in_integ 1));
 by (dtac eq_equiv_class 1);
@@ -137,7 +137,7 @@
 by (Asm_full_simp_tac 1);
 qed "inj_zminus";
 
-Goalw [nat_def] "- ($# 0) = $# 0";
+Goalw [int_def] "- ($# 0) = $# 0";
 by (simp_tac (simpset() addsimps [zminus]) 1);
 qed "zminus_nat0";
 
@@ -147,12 +147,12 @@
 (**** neg: the test for negative integers ****)
 
 
-Goalw [neg_def, nat_def] "~ neg($# n)";
+Goalw [neg_def, int_def] "~ neg($# n)";
 by (Simp_tac 1);
 by Safe_tac;
 qed "not_neg_nat";
 
-Goalw [neg_def, nat_def] "neg(- $# Suc(n))";
+Goalw [neg_def, int_def] "neg(- $# Suc(n))";
 by (simp_tac (simpset() addsimps [zminus]) 1);
 qed "neg_zminus_nat";
 
@@ -214,15 +214,15 @@
 (*Integer addition is an AC operator*)
 val zadd_ac = [zadd_assoc,zadd_commute,zadd_left_commute];
 
-Goalw [nat_def] "($#m) + ($#n) = $# (m + n)";
+Goalw [int_def] "($#m) + ($#n) = $# (m + n)";
 by (simp_tac (simpset() addsimps [zadd]) 1);
 qed "add_nat";
 
 Goal "$# (Suc m) = $# 1 + ($# m)";
 by (simp_tac (simpset() addsimps [add_nat]) 1);
-qed "nat_Suc";
+qed "int_Suc";
 
-Goalw [nat_def] "$# 0 + z = z";
+Goalw [int_def] "$# 0 + z = z";
 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
 by (asm_simp_tac (simpset() addsimps [zadd]) 1);
 qed "zadd_nat0";
@@ -232,7 +232,7 @@
 by (rtac zadd_nat0 1);
 qed "zadd_nat0_right";
 
-Goalw [nat_def] "z + (- z) = $# 0";
+Goalw [int_def] "z + (- z) = $# 0";
 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
 by (asm_simp_tac (simpset() addsimps [zminus, zadd, add_commute]) 1);
 qed "zadd_zminus_inverse_nat";
@@ -362,12 +362,12 @@
 by (simp_tac (simpset() addsimps [zmult_commute',zadd_zmult_distrib]) 1);
 qed "zadd_zmult_distrib2";
 
-Goalw [nat_def] "$# 0 * z = $# 0";
+Goalw [int_def] "$# 0 * z = $# 0";
 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
 by (asm_simp_tac (simpset() addsimps [zmult]) 1);
 qed "zmult_nat0";
 
-Goalw [nat_def] "$# 1 * z = z";
+Goalw [int_def] "$# 1 * z = z";
 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
 by (asm_simp_tac (simpset() addsimps [zmult]) 1);
 qed "zmult_nat1";
@@ -393,7 +393,7 @@
 (* Theorems about less and less_equal *)
 
 (*This lemma allows direct proofs of other <-properties*)
-Goalw [zless_def, neg_def, zdiff_def, nat_def] 
+Goalw [zless_def, neg_def, zdiff_def, int_def] 
     "(w < z) = (EX n. z = w + $#(Suc n))";
 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
 by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
@@ -420,7 +420,7 @@
 by (safe_tac (claset() addSDs [zless_iff_Suc_zadd RS iffD1]));
 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
 by Safe_tac;
-by (asm_full_simp_tac (simpset() addsimps [nat_def, zadd]) 1);
+by (asm_full_simp_tac (simpset() addsimps [int_def, zadd]) 1);
 qed "zless_not_sym";
 
 (* [| n<m;  ~P ==> m<n |] ==> P *)
@@ -465,8 +465,8 @@
 
 Goal "($# m = $# n) = (m = n)"; 
 by (fast_tac (claset() addSEs [inj_nat RS injD]) 1); 
-qed "nat_nat_eq"; 
-AddIffs [nat_nat_eq]; 
+qed "int_int_eq"; 
+AddIffs [int_int_eq]; 
 
 Goal "($#m < $#n) = (m<n)";
 by (simp_tac (simpset() addsimps [less_iff_Suc_add, zless_iff_Suc_zadd, 
@@ -637,7 +637,7 @@
 by (auto_tac (claset(),
 	      simpset() addsimps [zless_iff_Suc_zadd, zadd_assoc, 
 				  add_nat]));
-by (cut_inst_tac [("m","n")] nat_Suc 1);
+by (cut_inst_tac [("m","n")] int_Suc 1);
 by (exhaust_tac "n" 1);
 by Auto_tac;
 by (full_simp_tac (simpset() addsimps zadd_ac) 1);

--- a/src/HOL/Integ/IntDef.thy	Fri Sep 25 13:18:07 1998 +0200
+++ b/src/HOL/Integ/IntDef.thy	Fri Sep 25 13:57:01 1998 +0200
@@ -23,7 +23,7 @@
 
 constdefs
 
-  nat        :: nat => int                                  ("$# _" [80] 80)
+  int :: nat => int                                  ("$# _" [80] 80)
   "$# m == Abs_Integ(intrel ^^ {(m,0)})"
 
   neg   :: int => bool

--- a/src/HOL/Integ/Integ.ML	Fri Sep 25 13:18:07 1998 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,200 +0,0 @@
-(*  Title:      Integ.thy
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1998  University of Cambridge
-
-Type "int" is a linear order
-*)
-
-Goal "(w<z) = neg(w-z)";
-by (simp_tac (simpset() addsimps [zless_def]) 1);
-qed "zless_eq_neg";
-
-Goal "(w=z) = iszero(w-z)";
-by (simp_tac (simpset() addsimps [iszero_def, zdiff_eq_eq]) 1);
-qed "eq_eq_iszero";
-
-Goal "(w<=z) = (~ neg(z-w))";
-by (simp_tac (simpset() addsimps [zle_def, zless_def]) 1);
-qed "zle_eq_not_neg";
-
-(*This list of rewrites simplifies (in)equalities by subtracting the RHS
-  from the LHS, then using the cancellation simproc.  Use with zadd_ac.*)
-val zcompare_0_rls = 
-    [zdiff_def, zless_eq_neg, eq_eq_iszero, zle_eq_not_neg];
-
-
-(*** Monotonicity results ***)
-
-Goal "(v+z < w+z) = (v < (w::int))";
-by (full_simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1);
-qed "zadd_right_cancel_zless";
-
-Goal "(z+v < z+w) = (v < (w::int))";
-by (full_simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1);
-qed "zadd_left_cancel_zless";
-
-Addsimps [zadd_right_cancel_zless, zadd_left_cancel_zless];
-
-Goal "(v+z <= w+z) = (v <= (w::int))";
-by (full_simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1);
-qed "zadd_right_cancel_zle";
-
-Goal "(z+v <= z+w) = (v <= (w::int))";
-by (full_simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1);
-qed "zadd_left_cancel_zle";
-
-Addsimps [zadd_right_cancel_zle, zadd_left_cancel_zle];
-
-(*"v<=w ==> v+z <= w+z"*)
-bind_thm ("zadd_zless_mono1", zadd_right_cancel_zless RS iffD2);
-
-(*"v<=w ==> v+z <= w+z"*)
-bind_thm ("zadd_zle_mono1", zadd_right_cancel_zle RS iffD2);
-
-Goal "!!z z'::int. [| w'<=w; z'<=z |] ==> w' + z' <= w + z";
-by (etac (zadd_zle_mono1 RS zle_trans) 1);
-by (Simp_tac 1);
-qed "zadd_zle_mono";
-
-Goal "!!z z'::int. [| w'<w; z'<=z |] ==> w' + z' < w + z";
-by (etac (zadd_zless_mono1 RS zless_zle_trans) 1);
-by (Simp_tac 1);
-qed "zadd_zless_mono";
-
-
-(*** Comparison laws ***)
-
-Goal "(- x < - y) = (y < (x::int))";
-by (simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1);
-qed "zminus_zless_zminus"; 
-Addsimps [zminus_zless_zminus];
-
-Goal "(- x <= - y) = (y <= (x::int))";
-by (simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1);
-qed "zminus_zle_zminus"; 
-Addsimps [zminus_zle_zminus];
-
-(** The next several equations can make the simplifier loop! **)
-
-Goal "(x < - y) = (y < - (x::int))";
-by (simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1);
-qed "zless_zminus"; 
-
-Goal "(- x < y) = (- y < (x::int))";
-by (simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1);
-qed "zminus_zless"; 
-
-Goal "(x <= - y) = (y <= - (x::int))";
-by (simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1);
-qed "zle_zminus"; 
-
-Goal "(- x <= y) = (- y <= (x::int))";
-by (simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1);
-qed "zminus_zle"; 
-
-Goal "- $# Suc n < $# 0";
-by (simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1);
-qed "negative_zless_0"; 
-
-Goal "- $# Suc n < $# m";
-by (rtac (negative_zless_0 RS zless_zle_trans) 1);
-by (Simp_tac 1); 
-qed "negative_zless"; 
-AddIffs [negative_zless]; 
-
-Goal "- $# n <= $#0";
-by (simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1);
-qed "negative_zle_0"; 
-
-Goal "- $# n <= $# m";
-by (simp_tac (simpset() addsimps add_nat :: zcompare_0_rls @ zadd_ac) 1);
-qed "negative_zle"; 
-AddIffs [negative_zle]; 
-
-Goal "~($# 0 <= - $# Suc n)";
-by (stac zle_zminus 1);
-by (Simp_tac 1);
-qed "not_zle_0_negative"; 
-Addsimps [not_zle_0_negative]; 
-
-Goal "($# n <= - $# m) = (n = 0 & m = 0)"; 
-by Safe_tac; 
-by (Simp_tac 3); 
-by (dtac (zle_zminus RS iffD1) 2); 
-by (ALLGOALS (dtac (negative_zle_0 RSN(2,zle_trans)))); 
-by (ALLGOALS Asm_full_simp_tac); 
-qed "nat_zle_neg"; 
-
-Goal "~($# n < - $# m)";
-by (simp_tac (simpset() addsimps [symmetric zle_def]) 1); 
-qed "not_nat_zless_negative"; 
-
-Goal "(- $# n = $# m) = (n = 0 & m = 0)"; 
-by (rtac iffI 1);
-by (rtac (nat_zle_neg RS iffD1) 1); 
-by (dtac sym 1); 
-by (ALLGOALS Asm_simp_tac); 
-qed "negative_eq_positive"; 
-
-Addsimps [negative_eq_positive, not_nat_zless_negative]; 
-
-
-Goal "(w <= z) = (EX n. z = w + $# n)";
-by (auto_tac (claset(),
-	      simpset() addsimps [zless_iff_Suc_zadd, integ_le_less]));
-by (ALLGOALS (full_simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac)));
-by (ALLGOALS (full_simp_tac (simpset() addsimps [iszero_def])));
-by (blast_tac (claset() addIs [Suc_pred RS sym]) 1);
-qed "zle_iff_zadd";
-
-
-Goalw [zdiff_def,zless_def] "neg x = (x < $# 0)";
-by Auto_tac; 
-qed "neg_eq_less_nat0"; 
-
-Goalw [zle_def] "(~neg x) = ($# 0 <= x)";
-by (simp_tac (simpset() addsimps [neg_eq_less_nat0]) 1); 
-qed "not_neg_eq_ge_nat0"; 
-
-
-(**** nat_of: magnitide of an integer, as a natural number ****)
-
-Goalw [nat_of_def] "nat_of($# n) = n";
-by Auto_tac;
-qed "nat_of_nat";
-
-Goalw [nat_of_def] "nat_of(- $# n) = 0";
-by (auto_tac (claset(),
-	      simpset() addsimps [neg_eq_less_nat0, zminus_zless])); 
-qed "nat_of_zminus_nat";
-
-Addsimps [nat_of_nat, nat_of_zminus_nat];
-
-Goal "~ neg z ==> $# (nat_of z) = z"; 
-by (dtac (not_neg_eq_ge_nat0 RS iffD1) 1); 
-by (dtac zle_imp_zless_or_eq 1); 
-by (auto_tac (claset(), simpset() addsimps [zless_iff_Suc_zadd])); 
-qed "not_neg_nat_of"; 
-
-Goal "neg x ==> ? n. x = - $# Suc n"; 
-by (auto_tac (claset(), 
-	      simpset() addsimps [neg_eq_less_nat0, zless_iff_Suc_zadd,
-				  zdiff_eq_eq RS sym, zdiff_def])); 
-qed "negD"; 
-
-Goalw [nat_of_def] "neg z ==> nat_of z = 0"; 
-by Auto_tac; 
-qed "neg_nat_of"; 
-
-(* a case theorem distinguishing positive and negative int *)  
-
-val prems = Goal "[|!! n. P ($# n); !! n. P (- $# Suc n) |] ==> P z"; 
-by (case_tac "neg z" 1); 
-by (blast_tac (claset() addSDs [negD] addSIs prems) 1); 
-by (etac (not_neg_nat_of RS subst) 1);
-by (resolve_tac prems 1);
-qed "int_cases"; 
-
-fun int_case_tac x = res_inst_tac [("z",x)] int_cases; 
-

--- a/src/HOL/Integ/Integ.thy	Fri Sep 25 13:18:07 1998 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,18 +0,0 @@
-(*  Title:      Integ.thy
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1998  University of Cambridge
-
-Type "int" is a linear order
-*)
-
-Integ = IntDef +
-
-instance int :: order (zle_refl,zle_trans,zle_anti_sym,int_less_le)
-instance int :: linorder (zle_linear)
-
-constdefs
-  nat_of  :: int => nat
-  "nat_of(Z) == if neg Z then 0 else (@ m. Z = $# m)"
-
-end