src/HOL/Integ/nat_bin.ML

 Binary arithmetic for the natural numbers
 *)
 
 val nat_number_of_def = thm "nat_number_of_def";
 
+val ss_Int = simpset_of Int_thy;
 
 (** nat (coercion from int to nat) **)
 
 Goal "nat (number_of w) = number_of w";
 by (simp_tac (simpset() addsimps [nat_number_of_def]) 1);

 (*"neg" is used in rewrite rules for binary comparisons*)
 Goal "int (number_of v :: nat) = \
 \        (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];
 
 
 (** Successor **)

 by (asm_simp_tac (simpset() addsimps [nat_eq_iff, int_Suc]) 1);
 qed "Suc_nat_eq_nat_zadd1";
 
 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) = \
 \       (if neg (number_of v) then 1 else number_of (bin_succ v))";
 by (cut_inst_tac [("n","0")] Suc_nat_number_of_add 1);

 (*"neg" is used in rewrite rules for binary comparisons*)
 Goal "(number_of v :: nat) + number_of v' = \
 \        (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];
 
 

 Goalw [nat_number_of_def]
      "(number_of v :: nat) - number_of v' = \
 \       (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];
 
 
 (** Multiplication **)
 
 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];
 
 
 (** Quotient **)
 
 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];
 
 

 
 Goal "(number_of v :: nat)  mod  number_of v' = \
 \       (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];
 
 structure NatAbstractNumeralsData =

 (*"neg" is used in rewrite rules for binary comparisons*)
 Goal "((number_of v :: nat) = number_of v') = \
 \     (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";
 
 Addsimps [eq_nat_number_of];
 

 
 (*"neg" is used in rewrite rules for binary comparisons*)
 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";
 
 Addsimps [less_nat_number_of];
 

 (*** Comparisons involving Suc ***)
 
 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";
 
 Goal "(Suc n = number_of v) = \

 qed "Suc_eq_number_of";
 
 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";
 
 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";
 
 Goal "(number_of v <= Suc n) = \

 by (full_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1); 
 val lemma2 = result();
 
 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);
 by (dres_inst_tac [("f", "%x. x mod 2")] arg_cong 1);
 by (full_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1); 
 qed "eq_number_of_BIT_Pls"; 
 
 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);
 by Auto_tac;
 qed "eq_number_of_BIT_Min"; 

 by (ALLGOALS (asm_simp_tac (simpset() addsimps [nat_mult_distrib])));
 qed "nat_power_eq";
 
 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";
 
 Addsimps [inst "n" "number_of ?w" power_nat_number_of];
 

 by (simp_tac (simpset() addsimps [zpower_even, zpower_zadd_distrib]) 1); 
 qed "zpower_odd";
 
 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(), 
      simpset() addsimps [nat_mult_distrib, zpower_even, zpower_two])); 
 qed "zpower_number_of_even";
 
 Goal "(z::int) ^ number_of (w BIT True) = \
 \         (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(), 
               simpset() addsimps [nat_add_distrib, nat_mult_distrib, 
                                   zpower_even, zpower_two]));