# HG changeset patch
# User paulson
# Date 906539137 -7200
# Node ID 0f16c3b66ab4d479cf4edad7ab1096675f054616
# Parent  25e743eef48a39f91a9276e7b95821f3d46f2dab
much renaming and reorganization

diff -r 25e743eef48a -r 0f16c3b66ab4 src/HOL/Integ/Bin.ML
--- a/src/HOL/Integ/Bin.ML	Wed Sep 23 10:17:11 1998 +0200
+++ b/src/HOL/Integ/Bin.ML	Wed Sep 23 10:25:37 1998 +0200
@@ -25,10 +25,6 @@
     "NCons Min True = Min"
  (fn _ => [(Simp_tac 1)]);
 
-qed_goal "NCons_BIT" Bin.thy
-    "NCons (w BIT x) b = (w BIT x) BIT b"
- (fn _ => [(Simp_tac 1)]);
-
 qed_goal "bin_succ_1" Bin.thy
     "bin_succ(w BIT True) = (bin_succ w) BIT False"
  (fn _ => [(Simp_tac 1)]);
@@ -136,7 +132,7 @@
 by (simp_tac (simpset() addsimps bin_add_simps) 1);
 by (rtac allI 1);
 by (induct_tac "w" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps (bin_add_simps @ zadd_ac))));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps bin_add_simps @ zadd_ac)));
 qed_spec_mp "integ_of_add";
 
 val bin_mult_simps = [zmult_zminus, integ_of_minus, integ_of_add];
@@ -147,8 +143,7 @@
 by (simp_tac (simpset() addsimps bin_mult_simps) 1);
 by (simp_tac (simpset() addsimps bin_mult_simps) 1);
 by (asm_simp_tac
-    (simpset() addsimps (bin_mult_simps @ [zadd_zmult_distrib] @ 
-                                  zadd_ac)) 1);
+    (simpset() addsimps bin_mult_simps @ [zadd_zmult_distrib] @ zadd_ac) 1);
 qed "integ_of_mult";
 
 
@@ -218,13 +213,13 @@
 qed "add1_zle_eq";
 Addsimps [add1_zle_eq];
 
-Goal "znegative x = (x < #0)";
-by (simp_tac (simpset() addsimps [znegative_eq_less_nat0]) 1); 
-qed "znegative_eq_less_0"; 
+Goal "neg x = (x < #0)";
+by (simp_tac (simpset() addsimps [neg_eq_less_nat0]) 1); 
+qed "neg_eq_less_0"; 
 
-Goal "(~znegative x) = ($# 0 <= x)";
-by (simp_tac (simpset() addsimps [not_znegative_eq_ge_nat0]) 1); 
-qed "not_znegative_eq_ge_0"; 
+Goal "(~neg x) = ($# 0 <= x)";
+by (simp_tac (simpset() addsimps [not_neg_eq_ge_nat0]) 1); 
+qed "not_neg_eq_ge_0"; 
 
 
 
@@ -252,9 +247,9 @@
 by (Simp_tac 1);
 by (int_case_tac "integ_of w" 1); 
 by (ALLGOALS (asm_simp_tac 
-	      (simpset() addsimps (zcompare_rls @ 
-				   [zminus_zadd_distrib RS sym, 
-				    add_znat])))); 
+	      (simpset() addsimps zcompare_rls @ 
+				  [zminus_zadd_distrib RS sym, 
+				   add_nat]))); 
 qed "iszero_integ_of_BIT"; 
 
 
@@ -262,25 +257,24 @@
 
 Goalw [zless_def,zdiff_def] 
     "integ_of x < integ_of y \
-\    = znegative (integ_of (bin_add x (bin_minus y)))";
+\    = neg (integ_of (bin_add x (bin_minus y)))";
 by (simp_tac (simpset() addsimps bin_mult_simps) 1);
-qed "less_integ_of_eq_zneg"; 
+qed "less_integ_of_eq_neg"; 
 
-Goal "~ znegative (integ_of Pls)"; 
+Goal "~ neg (integ_of Pls)"; 
 by (Simp_tac 1); 
 qed "not_neg_integ_of_Pls"; 
 
-Goal "znegative (integ_of Min)"; 
+Goal "neg (integ_of Min)"; 
 by (Simp_tac 1);
 qed "neg_integ_of_Min"; 
 
-Goal "znegative (integ_of (w BIT x)) = znegative (integ_of w)"; 
+Goal "neg (integ_of (w BIT x)) = neg (integ_of w)"; 
 by (Asm_simp_tac 1); 
 by (int_case_tac "integ_of w" 1); 
 by (ALLGOALS (asm_simp_tac 
-	      (simpset() addsimps ([add_znat, znegative_eq_less_nat0, 
-				    symmetric zdiff_def] @ 
-				   zcompare_rls)))); 
+	      (simpset() addsimps [add_nat, neg_eq_less_nat0, 
+				   symmetric zdiff_def] @ zcompare_rls))); 
 qed "neg_integ_of_BIT"; 
 
 
@@ -290,11 +284,12 @@
 by (simp_tac (simpset() addsimps [zle_def]) 1);
 qed "le_integ_of_eq_not_less"; 
 
+(*Delete the original rewrites, with their clumsy conditional expressions*)
+Delsimps [succ_BIT, pred_BIT, minus_BIT, 
+          NCons_Pls, NCons_Min, add_BIT, mult_BIT];
 
 (*Hide the binary representation of integer constants*)
-Delsimps [succ_BIT, pred_BIT, minus_BIT, add_BIT, mult_BIT, 
-          integ_of_Pls, integ_of_Min, integ_of_BIT, 
-          norm_Pls, norm_Min, NCons];
+Delsimps [integ_of_Pls, integ_of_Min, integ_of_BIT];
 
 (*Add simplification of arithmetic operations on integer constants*)
 Addsimps [integ_of_add RS sym,
@@ -313,7 +308,7 @@
 (*... and simplification of relational operations*)
 Addsimps [eq_integ_of_eq, iszero_integ_of_Pls, nonzero_integ_of_Min,
 	  iszero_integ_of_BIT,
-	  less_integ_of_eq_zneg,
+	  less_integ_of_eq_neg,
 	  not_neg_integ_of_Pls, neg_integ_of_Min, neg_integ_of_BIT,
 	  le_integ_of_eq_not_less];
 
@@ -329,7 +324,7 @@
 (** Simplification of inequalities involving numerical constants **)
 
 Goal "(w <= z + #1) = (w<=z | w = z + #1)";
-by (simp_tac (simpset() addsimps [zle_eq_zless_or_eq, zless_add1_eq]) 1);
+by (simp_tac (simpset() addsimps [integ_le_less, zless_add1_eq]) 1);
 qed "zle_add1_eq";
 
 Goal "(w <= z - #1) = (w<z)";
@@ -360,7 +355,7 @@
 qed "zless_imp_zless_zadd1";
 
 Goal "(w < z + #1) = (w<=z)";
-by (simp_tac (simpset() addsimps [zless_add1_eq, zle_eq_zless_or_eq]) 1);
+by (simp_tac (simpset() addsimps [zless_add1_eq, integ_le_less]) 1);
 qed "zle_add1_eq_le";
 Addsimps [zle_add1_eq_le];
 
@@ -378,10 +373,10 @@
 by (full_simp_tac (simpset() addsimps zadd_ac) 1);
 qed "zless_zadd_imp_zless";
 
-(*LOOPS as a simprule!*)
+(*LOOPS as a simprule!  Analogous to Suc_lessD*)
 Goal "w + #1 < z ==> w < z";
-bd zless_zadd_imp_zless 1;
-ba 2;
+by (dtac zless_zadd_imp_zless 1);
+by (assume_tac 2);
 by (Simp_tac 1);
 qed "zless_zadd1_imp_zless";
 
diff -r 25e743eef48a -r 0f16c3b66ab4 src/HOL/Integ/Bin.thy
--- a/src/HOL/Integ/Bin.thy	Wed Sep 23 10:17:11 1998 +0200
+++ b/src/HOL/Integ/Bin.thy	Wed Sep 23 10:25:37 1998 +0200
@@ -43,9 +43,9 @@
 
 (*NCons inserts a bit, suppressing leading 0s and 1s*)
 primrec
-  norm_Pls "NCons Pls b = (if b then (Pls BIT b) else Pls)"
-  norm_Min "NCons Min b = (if b then Min else (Min BIT b))"
-  NCons    "NCons (w' BIT x') b = (w' BIT x') BIT b"
+  NCons_Pls "NCons Pls b = (if b then (Pls BIT b) else Pls)"
+  NCons_Min "NCons Min b = (if b then Min else (Min BIT b))"
+  NCons_BIT "NCons (w BIT x) b = (w BIT x) BIT b"
  
 primrec
   integ_of_Pls  "integ_of Pls = $# 0"
@@ -89,7 +89,7 @@
 primrec
   mult_Pls  "bin_mult Pls w = Pls"
   mult_Min  "bin_mult Min w = bin_minus w"
-  mult_BIT "bin_mult (v BIT x) w =
+  mult_BIT  "bin_mult (v BIT x) w =
 	        (if x then (bin_add (NCons (bin_mult v w) False) w)
 	              else (NCons (bin_mult v w) False))"
 
@@ -141,9 +141,13 @@
 
   fun dest_bin tm =
     let
-      fun bin_of (Const ("Pls", _)) = []
-        | bin_of (Const ("Min", _)) = [~1]
-        | bin_of (Const ("op BIT", _) $ bs $ b) = dest_bit b :: bin_of bs
+      (*We consider both "spellings", since Min might be declared elsewhere*)
+      fun bin_of (Const ("Pls", _))     = []
+        | bin_of (Const ("bin.Pls", _)) = []
+        | bin_of (Const ("Min", _))     = [~1]
+        | bin_of (Const ("bin.Min", _)) = [~1]
+        | bin_of (Const ("op BIT", _) $ bs $ b)     = dest_bit b :: bin_of bs
+        | bin_of (Const ("bin.op BIT", _) $ bs $ b) = dest_bit b :: bin_of bs
         | bin_of _ = raise Match;
 
       fun int_of [] = 0
diff -r 25e743eef48a -r 0f16c3b66ab4 src/HOL/Integ/IntDef.ML
--- a/src/HOL/Integ/IntDef.ML	Wed Sep 23 10:17:11 1998 +0200
+++ b/src/HOL/Integ/IntDef.ML	Wed Sep 23 10:25:37 1998 +0200
@@ -81,11 +81,11 @@
 qed "inj_Rep_Integ";
 
 
-(** znat: the injection from nat to Integ **)
+(** nat: the injection from nat to Integ **)
 
-Goal "inj(znat)";
+Goal "inj(nat)";
 by (rtac injI 1);
-by (rewtac znat_def);
+by (rewtac nat_def);
 by (dtac (inj_on_Abs_Integ RS inj_onD) 1);
 by (REPEAT (rtac intrel_in_integ 1));
 by (dtac eq_equiv_class 1);
@@ -93,7 +93,7 @@
 by (Fast_tac 1);
 by Safe_tac;
 by (Asm_full_simp_tac 1);
-qed "inj_znat";
+qed "inj_nat";
 
 
 (**** zminus: unary negation on Integ ****)
@@ -137,26 +137,26 @@
 by (Asm_full_simp_tac 1);
 qed "inj_zminus";
 
-Goalw [znat_def] "- ($# 0) = $# 0";
+Goalw [nat_def] "- ($# 0) = $# 0";
 by (simp_tac (simpset() addsimps [zminus]) 1);
 qed "zminus_nat0";
 
 Addsimps [zminus_nat0];
 
 
-(**** znegative: the test for negative integers ****)
+(**** neg: the test for negative integers ****)
 
 
-Goalw [znegative_def, znat_def] "~ znegative($# n)";
+Goalw [neg_def, nat_def] "~ neg($# n)";
 by (Simp_tac 1);
 by Safe_tac;
-qed "not_znegative_znat";
+qed "not_neg_nat";
 
-Goalw [znegative_def, znat_def] "znegative(- $# Suc(n))";
+Goalw [neg_def, nat_def] "neg(- $# Suc(n))";
 by (simp_tac (simpset() addsimps [zminus]) 1);
-qed "znegative_zminus_znat";
+qed "neg_zminus_nat";
 
-Addsimps [znegative_zminus_znat, not_znegative_znat]; 
+Addsimps [neg_zminus_nat, not_neg_nat]; 
 
 
 (**** zadd: addition on Integ ****)
@@ -194,7 +194,7 @@
 Goal "(z::int) + w = w + z";
 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
 by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
-by (asm_simp_tac (simpset() addsimps (add_ac @ [zadd])) 1);
+by (asm_simp_tac (simpset() addsimps add_ac @ [zadd]) 1);
 qed "zadd_commute";
 
 Goal "((z1::int) + z2) + z3 = z1 + (z2 + z3)";
@@ -214,15 +214,15 @@
 (*Integer addition is an AC operator*)
 val zadd_ac = [zadd_assoc,zadd_commute,zadd_left_commute];
 
-Goalw [znat_def] "($#m) + ($#n) = $# (m + n)";
+Goalw [nat_def] "($#m) + ($#n) = $# (m + n)";
 by (simp_tac (simpset() addsimps [zadd]) 1);
-qed "add_znat";
+qed "add_nat";
 
 Goal "$# (Suc m) = $# 1 + ($# m)";
-by (simp_tac (simpset() addsimps [add_znat]) 1);
-qed "znat_Suc";
+by (simp_tac (simpset() addsimps [add_nat]) 1);
+qed "nat_Suc";
 
-Goalw [znat_def] "$# 0 + z = z";
+Goalw [nat_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 [znat_def] "z + (- z) = $# 0";
+Goalw [nat_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";
@@ -309,28 +309,28 @@
 Goal "(- z) * w = - (z * (w::int))";
 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
 by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
-by (asm_simp_tac (simpset() addsimps ([zminus, zmult] @ add_ac)) 1);
+by (asm_simp_tac (simpset() addsimps [zminus, zmult] @ add_ac) 1);
 qed "zmult_zminus";
 
 
 Goal "(- z) * (- w) = (z * (w::int))";
 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
 by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
-by (asm_simp_tac (simpset() addsimps ([zminus, zmult] @ add_ac)) 1);
+by (asm_simp_tac (simpset() addsimps [zminus, zmult] @ add_ac) 1);
 qed "zmult_zminus_zminus";
 
 Goal "(z::int) * w = w * z";
 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
 by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
-by (asm_simp_tac (simpset() addsimps ([zmult] @ add_ac @ mult_ac)) 1);
+by (asm_simp_tac (simpset() addsimps [zmult] @ add_ac @ mult_ac) 1);
 qed "zmult_commute";
 
 Goal "((z1::int) * z2) * z3 = z1 * (z2 * z3)";
 by (res_inst_tac [("z","z1")] eq_Abs_Integ 1);
 by (res_inst_tac [("z","z2")] eq_Abs_Integ 1);
 by (res_inst_tac [("z","z3")] eq_Abs_Integ 1);
-by (asm_simp_tac (simpset() addsimps ([add_mult_distrib2,zmult] @ 
-                                     add_ac @ mult_ac)) 1);
+by (asm_simp_tac (simpset() addsimps [add_mult_distrib2,zmult] @ 
+                                     add_ac @ mult_ac) 1);
 qed "zmult_assoc";
 
 (*For AC rewriting*)
@@ -348,8 +348,8 @@
 by (res_inst_tac [("z","z2")] eq_Abs_Integ 1);
 by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
 by (asm_simp_tac 
-    (simpset() addsimps ([add_mult_distrib2, zadd, zmult] @ 
-			 add_ac @ mult_ac)) 1);
+    (simpset() addsimps [add_mult_distrib2, zadd, zmult] @ 
+                        add_ac @ mult_ac) 1);
 qed "zadd_zmult_distrib";
 
 val zmult_commute'= read_instantiate [("z","w")] zmult_commute;
@@ -362,12 +362,12 @@
 by (simp_tac (simpset() addsimps [zmult_commute',zadd_zmult_distrib]) 1);
 qed "zadd_zmult_distrib2";
 
-Goalw [znat_def] "$# 0 * z = $# 0";
+Goalw [nat_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 [znat_def] "$# 1 * z = z";
+Goalw [nat_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, znegative_def, zdiff_def, znat_def] 
+Goalw [zless_def, neg_def, zdiff_def, nat_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);
@@ -407,24 +407,24 @@
 Goal "z < z + $# (Suc n)";
 by (auto_tac (claset(),
 	      simpset() addsimps [zless_iff_Suc_zadd, zadd_assoc, 
-				  add_znat]));
+				  add_nat]));
 qed "zless_zadd_Suc";
 
 Goal "[| z1<z2; z2<z3 |] ==> z1 < (z3::int)";
 by (auto_tac (claset(),
 	      simpset() addsimps [zless_iff_Suc_zadd, zadd_assoc, 
-				  add_znat]));
+				  add_nat]));
 qed "zless_trans";
 
 Goal "!!w::int. z<w ==> ~w<z";
 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 ([znat_def, zadd])) 1);
+by (asm_full_simp_tac (simpset() addsimps [nat_def, zadd]) 1);
 qed "zless_not_sym";
 
 (* [| n<m;  ~P ==> m<n |] ==> P *)
-bind_thm ("zless_asym", (zless_not_sym RS swap));
+bind_thm ("zless_asym", zless_not_sym RS swap);
 
 Goal "!!z::int. ~ z<z";
 by (resolve_tac [zless_asym RS notI] 1);
@@ -444,7 +444,7 @@
 
 
 (*"Less than" is a linear ordering*)
-Goalw [zless_def, znegative_def, zdiff_def] 
+Goalw [zless_def, neg_def, zdiff_def] 
     "z<w | z=w | w<(z::int)";
 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
 by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
@@ -464,13 +464,13 @@
 bind_thm("int_neqE", int_neq_iff RS iffD1 RS disjE);
 
 Goal "($# m = $# n) = (m = n)"; 
-by (fast_tac (claset() addSEs [inj_znat RS injD]) 1); 
-qed "znat_znat_eq"; 
-AddIffs [znat_znat_eq]; 
+by (fast_tac (claset() addSEs [inj_nat RS injD]) 1); 
+qed "nat_nat_eq"; 
+AddIffs [nat_nat_eq]; 
 
 Goal "($#m < $#n) = (m<n)";
 by (simp_tac (simpset() addsimps [less_iff_Suc_add, zless_iff_Suc_zadd, 
-				  add_znat]) 1);
+				  add_nat]) 1);
 qed "zless_eq_less";
 Addsimps [zless_eq_less];
 
@@ -513,10 +513,10 @@
 
 Goal "(x <= (y::int)) = (x < y | x=y)";
 by (REPEAT(ares_tac [iffI, zless_or_eq_imp_zle, zle_imp_zless_or_eq] 1));
-qed "zle_eq_zless_or_eq";
+qed "integ_le_less";
 
 Goal "w <= (w::int)";
-by (simp_tac (simpset() addsimps [zle_eq_zless_or_eq]) 1);
+by (simp_tac (simpset() addsimps [integ_le_less]) 1);
 qed "zle_refl";
 
 Goalw [zle_def] "z < w ==> z <= (w::int)";
@@ -527,7 +527,7 @@
 
 (* Axiom 'linorder_linear' of class 'linorder': *)
 Goal "(z::int) <= w | w <= z";
-by (simp_tac (simpset() addsimps [zle_eq_zless_or_eq]) 1);
+by (simp_tac (simpset() addsimps [integ_le_less]) 1);
 by (cut_facts_tac [zless_linear] 1);
 by (Blast_tac 1);
 qed "zle_linear";
@@ -567,19 +567,19 @@
 (*** Subtraction laws ***)
 
 Goal "x + (y - z) = (x + y) - (z::int)";
-by (simp_tac (simpset() addsimps (zdiff_def::zadd_ac)) 1);
+by (simp_tac (simpset() addsimps zdiff_def::zadd_ac) 1);
 qed "zadd_zdiff_eq";
 
 Goal "(x - y) + z = (x + z) - (y::int)";
-by (simp_tac (simpset() addsimps (zdiff_def::zadd_ac)) 1);
+by (simp_tac (simpset() addsimps zdiff_def::zadd_ac) 1);
 qed "zdiff_zadd_eq";
 
 Goal "(x - y) - z = x - (y + (z::int))";
-by (simp_tac (simpset() addsimps (zdiff_def::zadd_ac)) 1);
+by (simp_tac (simpset() addsimps zdiff_def::zadd_ac) 1);
 qed "zdiff_zdiff_eq";
 
 Goal "x - (y - z) = (x + z) - (y::int)";
-by (simp_tac (simpset() addsimps (zdiff_def::zadd_ac)) 1);
+by (simp_tac (simpset() addsimps zdiff_def::zadd_ac) 1);
 qed "zdiff_zdiff_eq2";
 
 Goalw [zless_def, zdiff_def] "(x-y < z) = (x < z + (y::int))";
@@ -636,10 +636,10 @@
 Goal "(w < z + $# 1) = (w<z | w=z)";
 by (auto_tac (claset(),
 	      simpset() addsimps [zless_iff_Suc_zadd, zadd_assoc, 
-				  add_znat]));
-by (cut_inst_tac [("m","n")] znat_Suc 1);
+				  add_nat]));
+by (cut_inst_tac [("m","n")] nat_Suc 1);
 by (exhaust_tac "n" 1);
-auto();
+by Auto_tac;
 by (full_simp_tac (simpset() addsimps zadd_ac) 1);
 by (asm_full_simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
 qed "zless_add_nat1_eq";
diff -r 25e743eef48a -r 0f16c3b66ab4 src/HOL/Integ/IntDef.thy
--- a/src/HOL/Integ/IntDef.thy	Wed Sep 23 10:17:11 1998 +0200
+++ b/src/HOL/Integ/IntDef.thy	Wed Sep 23 10:25:37 1998 +0200
@@ -23,11 +23,11 @@
 
 constdefs
 
-  znat        :: nat => int                                  ("$# _" [80] 80)
+  nat        :: nat => int                                  ("$# _" [80] 80)
   "$# m == Abs_Integ(intrel ^^ {(m,0)})"
 
-  znegative   :: int => bool
-  "znegative(Z) == EX x y. x<y & (x,y::nat):Rep_Integ(Z)"
+  neg   :: int => bool
+  "neg(Z) == EX x y. x<y & (x,y::nat):Rep_Integ(Z)"
 
   (*For simplifying equalities*)
   iszero :: int => bool
@@ -41,7 +41,7 @@
 
   zdiff_def "Z1 - Z2 == Z1 + -(Z2::int)"
 
-  zless_def "Z1<Z2 == znegative(Z1 - Z2)"
+  zless_def "Z1<Z2 == neg(Z1 - Z2)"
 
   zle_def   "Z1 <= (Z2::int) == ~(Z2 < Z1)"
 
diff -r 25e743eef48a -r 0f16c3b66ab4 src/HOL/Integ/Integ.ML
--- a/src/HOL/Integ/Integ.ML	Wed Sep 23 10:17:11 1998 +0200
+++ b/src/HOL/Integ/Integ.ML	Wed Sep 23 10:25:37 1998 +0200
@@ -6,43 +6,42 @@
 Type "int" is a linear order
 *)
 
-Goal "(w<z) = znegative(w-z)";
+Goal "(w<z) = neg(w-z)";
 by (simp_tac (simpset() addsimps [zless_def]) 1);
-qed "zless_eq_znegative";
+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) = (~ znegative(z-w))";
+Goal "(w<=z) = (~ neg(z-w))";
 by (simp_tac (simpset() addsimps [zle_def, zless_def]) 1);
-qed "zle_eq_not_znegative";
+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_znegative, eq_eq_iszero, zle_eq_not_znegative];
-
+    [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);
+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);
+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);
+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);
+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];
@@ -67,39 +66,35 @@
 (*** Comparison laws ***)
 
 Goal "(- x < - y) = (y < (x::int))";
-by (simp_tac (simpset() addsimps (zcompare_0_rls @ zadd_ac)) 1);
+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);
+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);
+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);
+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);
+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);
+by (simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1);
 qed "zminus_zle"; 
 
-Goal "$#0 < $# Suc n"; 
-by (Simp_tac 1);
-qed "zero_zless_Suc"; 
-
 Goal "- $# Suc n < $# 0";
-by (simp_tac (simpset() addsimps (zcompare_0_rls @ zadd_ac)) 1);
+by (simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1);
 qed "negative_zless_0"; 
 
 Goal "- $# Suc n < $# m";
@@ -109,11 +104,11 @@
 AddIffs [negative_zless]; 
 
 Goal "- $# n <= $#0";
-by (simp_tac (simpset() addsimps (zcompare_0_rls @ zadd_ac)) 1);
+by (simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1);
 qed "negative_zle_0"; 
 
 Goal "- $# n <= $# m";
-by (simp_tac (simpset() addsimps (add_znat::(zcompare_0_rls @ zadd_ac))) 1);
+by (simp_tac (simpset() addsimps add_nat :: zcompare_0_rls @ zadd_ac) 1);
 qed "negative_zle"; 
 AddIffs [negative_zle]; 
 
@@ -129,67 +124,76 @@
 by (dtac (zle_zminus RS iffD1) 2); 
 by (ALLGOALS (dtac (negative_zle_0 RSN(2,zle_trans)))); 
 by (ALLGOALS Asm_full_simp_tac); 
-qed "znat_zle_znegative"; 
+qed "nat_zle_neg"; 
 
 Goal "~($# n < - $# m)";
 by (simp_tac (simpset() addsimps [symmetric zle_def]) 1); 
-qed "not_znat_zless_negative"; 
+qed "not_nat_zless_negative"; 
 
 Goal "(- $# n = $# m) = (n = 0 & m = 0)"; 
 by (rtac iffI 1);
-by (rtac (znat_zle_znegative RS iffD1) 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_znat_zless_negative]; 
+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"; 
 
 
-Goalw [zdiff_def,zless_def] "znegative x = (x < $# 0)";
-by Auto_tac; 
-qed "znegative_eq_less_nat0"; 
+(**** nat_of: magnitide of an integer, as a natural number ****)
 
-Goalw [zle_def] "(~znegative x) = ($# 0 <= x)";
-by (simp_tac (simpset() addsimps [znegative_eq_less_nat0]) 1); 
-qed "not_znegative_eq_ge_nat0"; 
-
-(**** zmagnitude: magnitide of an integer, as a natural number ****)
+Goalw [nat_of_def] "nat_of($# n) = n";
+by Auto_tac;
+qed "nat_of_nat";
 
-Goalw [zmagnitude_def] "zmagnitude($# n) = n";
-by Auto_tac;
-qed "zmagnitude_znat";
-
-Goalw [zmagnitude_def] "zmagnitude(- $# n) = n";
+Goalw [nat_of_def] "nat_of(- $# n) = n";
 by Auto_tac;
-qed "zmagnitude_zminus_znat";
+qed "nat_of_zminus_nat";
 
-Addsimps [zmagnitude_znat, zmagnitude_zminus_znat];
+Addsimps [nat_of_nat, nat_of_zminus_nat];
 
-Goal "~ znegative z ==> $# (zmagnitude z) = z"; 
-by (dtac (not_znegative_eq_ge_nat0 RS iffD1) 1); 
+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_zneg_mag"; 
+qed "not_neg_nat_of"; 
 
-Goal "znegative x ==> ? n. x = - $# Suc n"; 
+Goal "neg x ==> ? n. x = - $# Suc n"; 
 by (auto_tac (claset(), 
-	      simpset() addsimps [znegative_eq_less_nat0, zless_iff_Suc_zadd,
+	      simpset() addsimps [neg_eq_less_nat0, zless_iff_Suc_zadd,
 				  zdiff_eq_eq RS sym, zdiff_def])); 
-qed "znegativeD"; 
+qed "negD"; 
 
-Goal "znegative z ==> $# (zmagnitude z) = -z"; 
-bd znegativeD 1;
+Goal "neg z ==> $# (nat_of z) = -z"; 
+by (dtac negD 1);
 by Auto_tac; 
-qed "zneg_mag"; 
+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 "znegative z" 1); 
-by (blast_tac (claset() addSDs [znegativeD] addSIs prems) 1); 
-be (not_zneg_mag RS subst) 1;
-brs prems 1;
+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; 
diff -r 25e743eef48a -r 0f16c3b66ab4 src/HOL/Integ/Integ.thy
--- a/src/HOL/Integ/Integ.thy	Wed Sep 23 10:17:11 1998 +0200
+++ b/src/HOL/Integ/Integ.thy	Wed Sep 23 10:25:37 1998 +0200
@@ -12,7 +12,7 @@
 instance int :: linorder (zle_linear)
 
 constdefs
-  zmagnitude  :: int => nat
-  "zmagnitude(Z) == @m. Z = $# m | -Z = $# m"
+  nat_of  :: int => nat
+  "nat_of(Z) == @m. Z = $# m | -Z = $# m"
 
 end