# HG changeset patch
# User paulson
# Date 1067527310 -3600
# Node ID b91f632a1d370aec06ce49b288dd90b0325aeb9f
# Parent  d09e92e7c2bf699d1fc6df304c54aeb3101bfca5
Got rid of the structure "Int", which was obsolete and which obscured the
eponymous Basis Library structure

diff -r d09e92e7c2bf -r b91f632a1d37 src/HOL/Integ/Int_lemmas.ML
--- a/src/HOL/Integ/Int_lemmas.ML	Wed Oct 29 19:18:15 2003 +0100
+++ b/src/HOL/Integ/Int_lemmas.ML	Thu Oct 30 16:21:50 2003 +0100
@@ -8,16 +8,10 @@
 And many further lemmas
 *)
 
-(* legacy ML bindings *)
-
-structure Int =
-struct
-  val thy = the_context ();
-  val zabs_def = thm "zabs_def";
-  val nat_def  = thm "nat_def";
-end;
-
-open Int;
+(*Legacy ML bindings, but no longer the structure Int.*)
+val Int_thy = the_context ();
+val zabs_def = thm "zabs_def";
+val nat_def  = thm "nat_def";
 
 Goal "int 0 = (0::int)";
 by (simp_tac (simpset() addsimps [Zero_int_def]) 1);
@@ -319,7 +313,7 @@
 qed "zle_iff_zadd";
 
 Goal "abs (int m) = int m";
-by (simp_tac (simpset() addsimps [Int.zabs_def]) 1); 
+by (simp_tac (simpset() addsimps [zabs_def]) 1); 
 qed "abs_int_eq";
 Addsimps [abs_int_eq];
 
diff -r d09e92e7c2bf -r b91f632a1d37 src/HOL/Integ/NatSimprocs.ML
--- a/src/HOL/Integ/NatSimprocs.ML	Wed Oct 29 19:18:15 2003 +0100
+++ b/src/HOL/Integ/NatSimprocs.ML	Thu Oct 30 16:21:50 2003 +0100
@@ -27,9 +27,8 @@
 by (stac Suc_diff_eq_diff_pred 1);
 by (Simp_tac 1);
 by (Simp_tac 1);
-by (asm_full_simp_tac
-    (simpset_of Int.thy addsimps [diff_nat_number_of, less_0_number_of RS sym,
-                                  neg_number_of_bin_pred_iff_0]) 1);
+by (asm_full_simp_tac (ss_Int addsimps [diff_nat_number_of, 
+                    less_0_number_of RS sym, neg_number_of_bin_pred_iff_0]) 1);
 qed "Suc_diff_number_of";
 
 (* now redundant because of the inverse_fold simproc
diff -r d09e92e7c2bf -r b91f632a1d37 src/HOL/Integ/nat_bin.ML
--- a/src/HOL/Integ/nat_bin.ML	Wed Oct 29 19:18:15 2003 +0100
+++ b/src/HOL/Integ/nat_bin.ML	Thu Oct 30 16:21:50 2003 +0100
@@ -8,6 +8,7 @@
 
 val nat_number_of_def = thm "nat_number_of_def";
 
+val ss_Int = simpset_of Int_thy;
 
 (** nat (coercion from int to nat) **)
 
@@ -83,8 +84,7 @@
 \        (if neg (number_of v) then 0 \
 \         else (number_of v :: int))";
 by (simp_tac
-    (simpset_of Int.thy addsimps [neg_nat, nat_number_of_def, 
-				  not_neg_nat, int_0]) 1);
+    (ss_Int addsimps [neg_nat, nat_number_of_def, not_neg_nat, int_0]) 1);
 qed "int_nat_number_of";
 Addsimps [int_nat_number_of];
 
@@ -98,10 +98,9 @@
 
 Goal "Suc (number_of v + n) = \
 \       (if neg (number_of v) then 1+n else number_of (bin_succ v) + n)";
-by (simp_tac
-    (simpset_of Int.thy addsimps [neg_nat, nat_1, not_neg_eq_ge_0, 
-				  nat_number_of_def, int_Suc, 
-				  Suc_nat_eq_nat_zadd1, number_of_succ]) 1);
+by (simp_tac (ss_Int addsimps [neg_nat, nat_1, not_neg_eq_ge_0, 
+		               nat_number_of_def, int_Suc, 
+		               Suc_nat_eq_nat_zadd1, number_of_succ]) 1);
 qed "Suc_nat_number_of_add";
 
 Goal "Suc (number_of v) = \
@@ -128,9 +127,8 @@
 \        (if neg (number_of v) then number_of v' \
 \         else if neg (number_of v') then number_of v \
 \         else number_of (bin_add v v'))";
-by (simp_tac
-    (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, 
-				  nat_add_distrib RS sym, number_of_add]) 1);
+by (simp_tac (ss_Int addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, 
+		  	       nat_add_distrib RS sym, number_of_add]) 1);
 qed "add_nat_number_of";
 
 Addsimps [add_nat_number_of];
@@ -152,10 +150,9 @@
 \       (if neg (number_of v') then number_of v \
 \        else let d = number_of (bin_add v (bin_minus v')) in    \
 \             if neg d then 0 else nat d)";
-by (simp_tac
-    (simpset_of Int.thy delcongs [if_weak_cong]
-			addsimps [not_neg_eq_ge_0, nat_0,
-				  diff_nat_eq_if, diff_number_of_eq]) 1);
+by (simp_tac (ss_Int delcongs [if_weak_cong]
+		     addsimps [not_neg_eq_ge_0, nat_0,
+			       diff_nat_eq_if, diff_number_of_eq]) 1);
 qed "diff_nat_number_of";
 
 Addsimps [diff_nat_number_of];
@@ -165,10 +162,9 @@
 
 Goal "(number_of v :: nat) * number_of v' = \
 \      (if neg (number_of v) then 0 else number_of (bin_mult v v'))";
-by (simp_tac
-    (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, 
-				  nat_mult_distrib RS sym, number_of_mult, 
-				  nat_0]) 1);
+by (simp_tac (ss_Int addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, 
+		               nat_mult_distrib RS sym, number_of_mult, 
+			       nat_0]) 1);
 qed "mult_nat_number_of";
 
 Addsimps [mult_nat_number_of];
@@ -179,9 +175,8 @@
 Goal "(number_of v :: nat)  div  number_of v' = \
 \         (if neg (number_of v) then 0 \
 \          else nat (number_of v div number_of v'))";
-by (simp_tac
-    (simpset_of Int.thy addsimps [not_neg_eq_ge_0, nat_number_of_def, neg_nat, 
-				  nat_div_distrib RS sym, nat_0]) 1);
+by (simp_tac (ss_Int addsimps [not_neg_eq_ge_0, nat_number_of_def, neg_nat, 
+			       nat_div_distrib RS sym, nat_0]) 1);
 qed "div_nat_number_of";
 
 Addsimps [div_nat_number_of];
@@ -193,10 +188,9 @@
 \       (if neg (number_of v) then 0 \
 \        else if neg (number_of v') then number_of v \
 \        else nat (number_of v mod number_of v'))";
-by (simp_tac
-    (simpset_of Int.thy addsimps [not_neg_eq_ge_0, nat_number_of_def, 
-				  neg_nat, nat_0, DIVISION_BY_ZERO_MOD,
-				  nat_mod_distrib RS sym]) 1);
+by (simp_tac (ss_Int addsimps [not_neg_eq_ge_0, nat_number_of_def, 
+                               neg_nat, nat_0, DIVISION_BY_ZERO_MOD,
+                               nat_mod_distrib RS sym]) 1);
 qed "mod_nat_number_of";
 
 Addsimps [mod_nat_number_of];
@@ -235,11 +229,9 @@
 \     (if neg (number_of v) then (iszero (number_of v') | neg (number_of v')) \
 \      else if neg (number_of v') then iszero (number_of v) \
 \      else iszero (number_of (bin_add v (bin_minus v'))))";
-by (simp_tac
-    (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, 
-				  eq_nat_nat_iff, eq_number_of_eq, nat_0]) 1);
-by (simp_tac (simpset_of Int.thy addsimps [nat_eq_iff, nat_eq_iff2, 
-					   iszero_def]) 1);
+by (simp_tac (ss_Int addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, 
+                               eq_nat_nat_iff, eq_number_of_eq, nat_0]) 1);
+by (simp_tac (ss_Int addsimps [nat_eq_iff, nat_eq_iff2, iszero_def]) 1);
 by (simp_tac (simpset () addsimps [not_neg_eq_ge_0 RS sym]) 1);
 qed "eq_nat_number_of";
 
@@ -251,11 +243,9 @@
 Goal "((number_of v :: nat) < number_of v') = \
 \        (if neg (number_of v) then neg (number_of (bin_minus v')) \
 \         else neg (number_of (bin_add v (bin_minus v'))))";
-by (simp_tac
-    (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, 
-				  nat_less_eq_zless, less_number_of_eq_neg,
-				  nat_0]) 1);
-by (simp_tac (simpset_of Int.thy addsimps [neg_eq_less_0, zminus_zless, 
+by (simp_tac (ss_Int addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, 
+                          nat_less_eq_zless, less_number_of_eq_neg, nat_0]) 1);
+by (simp_tac (ss_Int addsimps [neg_eq_less_0, zminus_zless, 
 				number_of_minus, zless_nat_eq_int_zless]) 1);
 qed "less_nat_number_of";
 
@@ -352,10 +342,9 @@
 Goal "(number_of v = Suc n) = \
 \       (let pv = number_of (bin_pred v) in \
 \        if neg pv then False else nat pv = n)";
-by (simp_tac
-    (simpset_of Int.thy addsimps
-      [Let_def, neg_eq_less_0, linorder_not_less, number_of_pred,
-       nat_number_of_def, zadd_0] @ zadd_ac) 1);
+by (simp_tac (ss_Int addsimps
+	      [Let_def, neg_eq_less_0, linorder_not_less, number_of_pred,
+	       nat_number_of_def, zadd_0] @ zadd_ac) 1);
 by (res_inst_tac [("x", "number_of v")] spec 1);
 by (auto_tac (claset(), simpset() addsimps [nat_eq_iff]));
 qed "eq_number_of_Suc";
@@ -369,10 +358,9 @@
 Goal "(number_of v < Suc n) = \
 \       (let pv = number_of (bin_pred v) in \
 \        if neg pv then True else nat pv < n)";
-by (simp_tac
-    (simpset_of Int.thy addsimps
-      [Let_def, neg_eq_less_0, linorder_not_less, number_of_pred,
-       nat_number_of_def, zadd_0] @ zadd_ac) 1);
+by (simp_tac (ss_Int addsimps
+	      [Let_def, neg_eq_less_0, linorder_not_less, number_of_pred,
+	       nat_number_of_def, zadd_0] @ zadd_ac) 1);
 by (res_inst_tac [("x", "number_of v")] spec 1);
 by (auto_tac (claset(), simpset() addsimps [nat_less_iff]));
 qed "less_number_of_Suc";
@@ -380,10 +368,9 @@
 Goal "(Suc n < number_of v) = \
 \       (let pv = number_of (bin_pred v) in \
 \        if neg pv then False else n < nat pv)";
-by (simp_tac
-    (simpset_of Int.thy addsimps
-      [Let_def, neg_eq_less_0, linorder_not_less, number_of_pred,
-       nat_number_of_def, zadd_0] @ zadd_ac) 1);
+by (simp_tac (ss_Int addsimps
+	      [Let_def, neg_eq_less_0, linorder_not_less, number_of_pred,
+	       nat_number_of_def, zadd_0] @ zadd_ac) 1);
 by (res_inst_tac [("x", "number_of v")] spec 1);
 by (auto_tac (claset(), simpset() addsimps [zless_nat_eq_int_zless]));
 qed "less_Suc_number_of";
@@ -423,14 +410,12 @@
 
 Goal "((number_of (v BIT x) ::int) = number_of (w BIT y)) = \
 \     (x=y & (((number_of v) ::int) = number_of w))"; 
-by (simp_tac (simpset_of Int.thy addsimps
-	       [number_of_BIT, lemma1, lemma2, eq_commute]) 1); 
+by (simp_tac (ss_Int addsimps [number_of_BIT, lemma1, lemma2, eq_commute]) 1); 
 qed "eq_number_of_BIT_BIT"; 
 
 Goal "((number_of (v BIT x) ::int) = number_of bin.Pls) = \
 \     (x=False & (((number_of v) ::int) = number_of bin.Pls))"; 
-by (simp_tac (simpset_of Int.thy addsimps
-	       [number_of_BIT, number_of_Pls, eq_commute]) 1); 
+by (simp_tac (ss_Int addsimps [number_of_BIT, number_of_Pls, eq_commute]) 1); 
 by (res_inst_tac [("x", "number_of v")] spec 1);
 by Safe_tac;
 by (ALLGOALS Full_simp_tac);
@@ -440,8 +425,7 @@
 
 Goal "((number_of (v BIT x) ::int) = number_of bin.Min) = \
 \     (x=True & (((number_of v) ::int) = number_of bin.Min))"; 
-by (simp_tac (simpset_of Int.thy addsimps
-	       [number_of_BIT, number_of_Min, eq_commute]) 1); 
+by (simp_tac (ss_Int addsimps [number_of_BIT, number_of_Min, eq_commute]) 1); 
 by (res_inst_tac [("x", "number_of v")] spec 1);
 by Auto_tac;
 by (dres_inst_tac [("f", "%x. x mod 2")] arg_cong 1);
@@ -468,8 +452,7 @@
 
 Goal "(number_of v :: nat) ^ n = \
 \      (if neg (number_of v) then 0^n else nat ((number_of v :: int) ^ n))";
-by (simp_tac
-    (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, 
+by (simp_tac (ss_Int addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, 
 				  nat_power_eq]) 1);
 qed "power_nat_number_of";
 
@@ -493,8 +476,7 @@
 
 Goal "(z::int) ^ number_of (w BIT False) = \
 \     (let w = z ^ (number_of w) in  w*w)";
-by (simp_tac (simpset_of Int.thy addsimps [nat_number_of_def,
-        number_of_BIT, Let_def]) 1);
+by (simp_tac (ss_Int addsimps [nat_number_of_def, number_of_BIT, Let_def]) 1);
 by (res_inst_tac [("x","number_of w")] spec 1 THEN Clarify_tac 1); 
 by (case_tac "(0::int) <= x" 1);
 by (auto_tac (claset(), 
@@ -505,8 +487,7 @@
 \         (if (0::int) <= number_of w                   \
 \          then (let w = z ^ (number_of w) in  z*w*w)   \
 \          else 1)";
-by (simp_tac (simpset_of Int.thy addsimps [nat_number_of_def,
-        number_of_BIT, Let_def]) 1);
+by (simp_tac (ss_Int addsimps [nat_number_of_def, number_of_BIT, Let_def]) 1);
 by (res_inst_tac [("x","number_of w")] spec 1 THEN Clarify_tac 1); 
 by (case_tac "(0::int) <= x" 1);
 by (auto_tac (claset(),