src/ZF/Arith.ML

 \       a: C(0);  \
 \       !!m z. [| m: nat;  z: C(m) |] ==> b(m,z): C(succ(m))  \
 \    |] ==> rec(n,a,b) : C(n)";
 by (rtac (major RS nat_induct) 1);
 by (ALLGOALS
-    (asm_simp_tac (!simpset addsimps prems)));
+    (asm_simp_tac (simpset() addsimps prems)));
 qed "rec_type";
 
 Addsimps [rec_type, nat_0_le, nat_le_refl];
 val nat_typechecks = [rec_type, nat_0I, nat_1I, nat_succI, Ord_nat];
 

 (*Must simplify BEFORE the induction!!  (Else we get a critical pair)
   succ(m) #- succ(n)   rewrites to   pred(succ(m) #- n)  *)
 qed_goalw "diff_succ_succ" Arith.thy [diff_def]
     "[| m:nat;  n:nat |] ==> succ(m) #- succ(n) = m #- n"
  (fn prems=>
-  [ (asm_simp_tac (!simpset addsimps prems) 1),
+  [ (asm_simp_tac (simpset() addsimps prems) 1),
     (nat_ind_tac "n" prems 1),
-    (ALLGOALS (asm_simp_tac (!simpset addsimps prems))) ]);
+    (ALLGOALS (asm_simp_tac (simpset() addsimps prems))) ]);
 
 Addsimps [diff_0, diff_0_eq_0, diff_succ_succ];
 
 val prems = goal Arith.thy 
     "[| m:nat;  n:nat |] ==> m #- n le m";
 by (rtac (prems MRS diff_induct) 1);
 by (etac leE 3);
 by (ALLGOALS
-    (asm_simp_tac (!simpset addsimps (prems @ [le_iff, nat_into_Ord]))));
+    (asm_simp_tac (simpset() addsimps (prems @ [le_iff, nat_into_Ord]))));
 qed "diff_le_self";
 
 (*** Simplification over add, mult, diff ***)
 
 val arith_typechecks = [add_type, mult_type, diff_type];

 (*Associative law for addition*)
 qed_goal "add_assoc" Arith.thy 
     "m:nat ==> (m #+ n) #+ k = m #+ (n #+ k)"
  (fn prems=>
   [ (nat_ind_tac "m" prems 1),
-    (ALLGOALS (asm_simp_tac (!simpset addsimps prems))) ]);
+    (ALLGOALS (asm_simp_tac (simpset() addsimps prems))) ]);
 
 (*The following two lemmas are used for add_commute and sometimes
   elsewhere, since they are safe for rewriting.*)
 qed_goal "add_0_right" Arith.thy
     "m:nat ==> m #+ 0 = m"
  (fn prems=>
   [ (nat_ind_tac "m" prems 1),
-    (ALLGOALS (asm_simp_tac (!simpset addsimps prems))) ]); 
+    (ALLGOALS (asm_simp_tac (simpset() addsimps prems))) ]); 
 
 qed_goal "add_succ_right" Arith.thy
     "m:nat ==> m #+ succ(n) = succ(m #+ n)"
  (fn prems=>
   [ (nat_ind_tac "m" prems 1),
-    (ALLGOALS (asm_simp_tac (!simpset addsimps prems))) ]); 
+    (ALLGOALS (asm_simp_tac (simpset() addsimps prems))) ]); 
 
 Addsimps [add_0_right, add_succ_right];
 
 (*Commutative law for addition*)  
 qed_goal "add_commute" Arith.thy 

     (ALLGOALS Asm_simp_tac) ]);
 
 (*for a/c rewriting*)
 qed_goal "add_left_commute" Arith.thy
     "!!m n k. [| m:nat;  n:nat |] ==> m#+(n#+k)=n#+(m#+k)"
- (fn _ => [asm_simp_tac(!simpset addsimps [add_assoc RS sym, add_commute]) 1]);
+ (fn _ => [asm_simp_tac(simpset() addsimps [add_assoc RS sym, add_commute]) 1]);
 
 (*Addition is an AC-operator*)
 val add_ac = [add_assoc, add_commute, add_left_commute];
 
 (*Cancellation law on the left*)

 (*right successor law for multiplication*)
 qed_goal "mult_succ_right" Arith.thy 
     "!!m n. [| m:nat;  n:nat |] ==> m #* succ(n) = m #+ (m #* n)"
  (fn _ =>
   [ (nat_ind_tac "m" [] 1),
-    (ALLGOALS (asm_simp_tac (!simpset addsimps add_ac))) ]);
+    (ALLGOALS (asm_simp_tac (simpset() addsimps add_ac))) ]);
 
 Addsimps [mult_0_right, mult_succ_right];
 
 goal Arith.thy "!!n. n:nat ==> 1 #* n = n";
 by (Asm_simp_tac 1);

 (*addition distributes over multiplication*)
 qed_goal "add_mult_distrib" Arith.thy 
     "!!m n. [| m:nat;  k:nat |] ==> (m #+ n) #* k = (m #* k) #+ (n #* k)"
  (fn _=>
   [ (etac nat_induct 1),
-    (ALLGOALS (asm_simp_tac (!simpset addsimps [add_assoc RS sym]))) ]);
+    (ALLGOALS (asm_simp_tac (simpset() addsimps [add_assoc RS sym]))) ]);
 
 (*Distributive law on the left; requires an extra typing premise*)
 qed_goal "add_mult_distrib_left" Arith.thy 
     "!!m. [| m:nat;  n:nat;  k:nat |] ==> k #* (m #+ n) = (k #* m) #+ (k #* n)"
  (fn prems=>
   [ (nat_ind_tac "m" [] 1),
     (Asm_simp_tac 1),
-    (asm_simp_tac (!simpset addsimps add_ac) 1) ]);
+    (asm_simp_tac (simpset() addsimps add_ac) 1) ]);
 
 (*Associative law for multiplication*)
 qed_goal "mult_assoc" Arith.thy 
     "!!m n k. [| m:nat;  n:nat;  k:nat |] ==> (m #* n) #* k = m #* (n #* k)"
  (fn _=>
   [ (etac nat_induct 1),
-    (ALLGOALS (asm_simp_tac (!simpset addsimps [add_mult_distrib]))) ]);
+    (ALLGOALS (asm_simp_tac (simpset() addsimps [add_mult_distrib]))) ]);
 
 (*for a/c rewriting*)
 qed_goal "mult_left_commute" Arith.thy 
     "!!m n k. [| m:nat;  n:nat;  k:nat |] ==> m #* (n #* k) = n #* (m #* k)"
  (fn _ => [rtac (mult_commute RS trans) 1, 

 
 qed_goal "diff_self_eq_0" Arith.thy 
     "m:nat ==> m #- m = 0"
  (fn prems=>
   [ (nat_ind_tac "m" prems 1),
-    (ALLGOALS (asm_simp_tac (!simpset addsimps prems))) ]);
+    (ALLGOALS (asm_simp_tac (simpset() addsimps prems))) ]);
 
 (*Addition is the inverse of subtraction*)
 goal Arith.thy "!!m n. [| n le m;  m:nat |] ==> n #+ (m#-n) = m";
 by (forward_tac [lt_nat_in_nat] 1);
 by (etac nat_succI 1);

 (** Subtraction is the inverse of addition. **)
 
 val [mnat,nnat] = goal Arith.thy
     "[| m:nat;  n:nat |] ==> (n#+m) #- n = m";
 by (rtac (nnat RS nat_induct) 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [mnat])));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [mnat])));
 qed "diff_add_inverse";
 
 goal Arith.thy
     "!!m n. [| m:nat;  n:nat |] ==> (m#+n) #- n = m";
 by (res_inst_tac [("m1","m")] (add_commute RS ssubst) 1);

 qed "diff_cancel";
 
 goal Arith.thy
     "!!n. [| k:nat; m: nat; n: nat |] ==> (m#+k) #- (n#+k) = m #- n";
 val add_commute_k = read_instantiate [("n","k")] add_commute;
-by (asm_simp_tac (!simpset addsimps [add_commute_k, diff_cancel]) 1);
+by (asm_simp_tac (simpset() addsimps [add_commute_k, diff_cancel]) 1);
 qed "diff_cancel2";
 
 val [mnat,nnat] = goal Arith.thy
     "[| m:nat;  n:nat |] ==> n #- (n#+m) = 0";
 by (rtac (nnat RS nat_induct) 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [mnat])));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [mnat])));
 qed "diff_add_0";
 
 (** Difference distributes over multiplication **)
 
 goal Arith.thy 
   "!!m n. [| m:nat; n: nat; k:nat |] ==> (m #- n) #* k = (m #* k) #- (n #* k)";
 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [diff_cancel])));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_cancel])));
 qed "diff_mult_distrib" ;
 
 goal Arith.thy 
   "!!m. [| m:nat; n: nat; k:nat |] ==> k #* (m #- n) = (k #* m) #- (k #* n)";
 val mult_commute_k = read_instantiate [("m","k")] mult_commute;
-by (asm_simp_tac (!simpset addsimps 
+by (asm_simp_tac (simpset() addsimps 
                   [mult_commute_k, diff_mult_distrib]) 1);
 qed "diff_mult_distrib2" ;
 
 (*** Remainder ***)
 
 goal Arith.thy "!!m n. [| 0<n;  n le m;  m:nat |] ==> m #- n < m";
 by (forward_tac [lt_nat_in_nat] 1 THEN etac nat_succI 1);
 by (etac rev_mp 1);
 by (etac rev_mp 1);
 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [diff_le_self,diff_succ_succ])));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_le_self,diff_succ_succ])));
 qed "div_termination";
 
 val div_rls =   (*for mod and div*)
     nat_typechecks @
     [Ord_transrec_type, apply_type, div_termination RS ltD, if_type,
      nat_into_Ord, not_lt_iff_le RS iffD1];
 
-val div_ss = (!simpset) addsimps [nat_into_Ord, div_termination RS ltD,
+val div_ss = (simpset()) addsimps [nat_into_Ord, div_termination RS ltD,
                                   not_lt_iff_le RS iffD2];
 
 (*Type checking depends upon termination!*)
 goalw Arith.thy [mod_def] "!!m n. [| 0<n;  m:nat;  n:nat |] ==> m mod n : nat";
 by (REPEAT (ares_tac div_rls 1 ORELSE etac lt_trans 1));

 by (excluded_middle_tac "x<n" 1);
 (*case x<n*)
 by (Asm_simp_tac 2);
 (*case n le x*)
 by (asm_full_simp_tac
-     (!simpset addsimps [not_lt_iff_le, nat_into_Ord, add_assoc,
+     (simpset() addsimps [not_lt_iff_le, nat_into_Ord, add_assoc,
                          div_termination RS ltD, add_diff_inverse]) 1);
 qed "mod_div_equality";
 
 (*** Further facts about mod (mainly for mutilated checkerboard ***)
 

     "!!m n. [| 0<n;  m:nat;  n:nat |] ==> \
 \           succ(m) mod n = if(succ(m mod n) = n, 0, succ(m mod n))";
 by (etac complete_induct 1);
 by (excluded_middle_tac "succ(x)<n" 1);
 (* case succ(x) < n *)
-by (asm_simp_tac (!simpset addsimps [mod_less, nat_le_refl RS lt_trans,
+by (asm_simp_tac (simpset() addsimps [mod_less, nat_le_refl RS lt_trans,
                                      succ_neq_self]) 2);
-by (asm_simp_tac (!simpset addsimps [ltD RS mem_imp_not_eq]) 2);
+by (asm_simp_tac (simpset() addsimps [ltD RS mem_imp_not_eq]) 2);
 (* case n le succ(x) *)
 by (asm_full_simp_tac
-     (!simpset addsimps [not_lt_iff_le, nat_into_Ord, mod_geq]) 1);
+     (simpset() addsimps [not_lt_iff_le, nat_into_Ord, mod_geq]) 1);
 by (etac leE 1);
-by (asm_simp_tac (!simpset addsimps [div_termination RS ltD, diff_succ, 
+by (asm_simp_tac (simpset() addsimps [div_termination RS ltD, diff_succ, 
                                      mod_geq]) 1);
-by (asm_simp_tac (!simpset addsimps [mod_less, diff_self_eq_0]) 1);
+by (asm_simp_tac (simpset() addsimps [mod_less, diff_self_eq_0]) 1);
 qed "mod_succ";
 
 goal Arith.thy "!!m n. [| 0<n;  m:nat;  n:nat |] ==> m mod n < n";
 by (etac complete_induct 1);
 by (excluded_middle_tac "x<n" 1);
 (*case x<n*)
-by (asm_simp_tac (!simpset addsimps [mod_less]) 2);
+by (asm_simp_tac (simpset() addsimps [mod_less]) 2);
 (*case n le x*)
 by (asm_full_simp_tac
-     (!simpset addsimps [not_lt_iff_le, nat_into_Ord,
+     (simpset() addsimps [not_lt_iff_le, nat_into_Ord,
                          mod_geq, div_termination RS ltD]) 1);
 qed "mod_less_divisor";
 
 
 goal Arith.thy
     "!!k b. [| k: nat; b<2 |] ==> k mod 2 = b | k mod 2 = if(b=1,0,1)";
 by (subgoal_tac "k mod 2: 2" 1);
-by (asm_simp_tac (!simpset addsimps [mod_less_divisor RS ltD]) 2);
+by (asm_simp_tac (simpset() addsimps [mod_less_divisor RS ltD]) 2);
 by (dtac ltD 1);
-by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
+by (asm_simp_tac (simpset() setloop split_tac [expand_if]) 1);
 by (Blast_tac 1);
 qed "mod2_cases";
 
 goal Arith.thy "!!m. m:nat ==> succ(succ(m)) mod 2 = m mod 2";
 by (subgoal_tac "m mod 2: 2" 1);
-by (asm_simp_tac (!simpset addsimps [mod_less_divisor RS ltD]) 2);
-by (asm_simp_tac (!simpset addsimps [mod_succ] setloop Step_tac) 1);
+by (asm_simp_tac (simpset() addsimps [mod_less_divisor RS ltD]) 2);
+by (asm_simp_tac (simpset() addsimps [mod_succ] setloop Step_tac) 1);
 qed "mod2_succ_succ";
 
 goal Arith.thy "!!m. m:nat ==> (m#+m) mod 2 = 0";
 by (etac nat_induct 1);
-by (simp_tac (!simpset addsimps [mod_less]) 1);
-by (asm_simp_tac (!simpset addsimps [mod2_succ_succ, add_succ_right]) 1);
+by (simp_tac (simpset() addsimps [mod_less]) 1);
+by (asm_simp_tac (simpset() addsimps [mod2_succ_succ, add_succ_right]) 1);
 qed "mod2_add_self";
 
 
 (**** Additional theorems about "le" ****)
 

 (*strict, in 1st argument; proof is by rule induction on 'less than'*)
 goal Arith.thy "!!i j k. [| i<j; j:nat; k:nat |] ==> i#+k < j#+k";
 by (forward_tac [lt_nat_in_nat] 1);
 by (assume_tac 1);
 by (etac succ_lt_induct 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [leI])));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [leI])));
 qed "add_lt_mono1";
 
 (*strict, in both arguments*)
 goal Arith.thy "!!i j k l. [| i<j; k<l; j:nat; l:nat |] ==> i#+k < j#+l";
 by (rtac (add_lt_mono1 RS lt_trans) 1);

 (*** Monotonicity of Multiplication ***)
 
 goal Arith.thy "!!i j k. [| i le j; j:nat; k:nat |] ==> i#*k le j#*k";
 by (forward_tac [lt_nat_in_nat] 1);
 by (nat_ind_tac "k" [] 2);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [add_le_mono])));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_le_mono])));
 qed "mult_le_mono1";
 
 (* le monotonicity, BOTH arguments*)
 goal Arith.thy
     "!!i j k. [| i le j; k le l; j:nat; l:nat |] ==> i#*k le j#*l";

 goal Arith.thy "!!i j k. [| i<j; 0<k; j:nat; k:nat |] ==> k#*i < k#*j";
 by (etac zero_lt_natE 1);
 by (forward_tac [lt_nat_in_nat] 2);
 by (ALLGOALS Asm_simp_tac);
 by (nat_ind_tac "x" [] 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [add_lt_mono])));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_lt_mono])));
 qed "mult_lt_mono2";
 
 goal Arith.thy "!!k. [| m: nat; n: nat |] ==> 0 < m#*n <-> 0<m & 0<n";
-by (best_tac (!claset addEs [natE] addss (!simpset)) 1);
+by (best_tac (claset() addEs [natE] addss (simpset())) 1);
 qed "zero_lt_mult_iff";
 
 goal Arith.thy "!!k. [| m: nat; n: nat |] ==> m#*n = 1 <-> m=1 & n=1";
-by (best_tac (!claset addEs [natE] addss (!simpset)) 1);
+by (best_tac (claset() addEs [natE] addss (simpset())) 1);
 qed "mult_eq_1_iff";
 
 (*Cancellation law for division*)
 goal Arith.thy
    "!!k. [| 0<n; 0<k; k:nat; m:nat; n:nat |] ==> (k#*m) div (k#*n) = m div n";
 by (eres_inst_tac [("i","m")] complete_induct 1);
 by (excluded_middle_tac "x<n" 1);
-by (asm_simp_tac (!simpset addsimps [div_less, zero_lt_mult_iff, 
+by (asm_simp_tac (simpset() addsimps [div_less, zero_lt_mult_iff, 
                                      mult_lt_mono2]) 2);
 by (asm_full_simp_tac
-     (!simpset addsimps [not_lt_iff_le, nat_into_Ord,
+     (simpset() addsimps [not_lt_iff_le, nat_into_Ord,
                          zero_lt_mult_iff, le_refl RS mult_le_mono, div_geq,
                          diff_mult_distrib2 RS sym,
                          div_termination RS ltD]) 1);
 qed "div_cancel";
 
 goal Arith.thy
    "!!k. [| 0<n; 0<k; k:nat; m:nat; n:nat |] ==> \
 \        (k#*m) mod (k#*n) = k #* (m mod n)";
 by (eres_inst_tac [("i","m")] complete_induct 1);
 by (excluded_middle_tac "x<n" 1);
-by (asm_simp_tac (!simpset addsimps [mod_less, zero_lt_mult_iff, 
+by (asm_simp_tac (simpset() addsimps [mod_less, zero_lt_mult_iff, 
                                      mult_lt_mono2]) 2);
 by (asm_full_simp_tac
-     (!simpset addsimps [not_lt_iff_le, nat_into_Ord,
+     (simpset() addsimps [not_lt_iff_le, nat_into_Ord,
                          zero_lt_mult_iff, le_refl RS mult_le_mono, mod_geq,
                          diff_mult_distrib2 RS sym,
                          div_termination RS ltD]) 1);
 qed "mult_mod_distrib";
 

 
 goal Arith.thy "!!m n. [| m = m#*n; m: nat; n: nat |] ==> n=1 | m=0";
 by (rtac disjCI 1);
 by (dtac sym 1);
 by (rtac Ord_linear_lt 1 THEN REPEAT_SOME (ares_tac [nat_into_Ord,nat_1I]));
-by (fast_tac (!claset addss (!simpset)) 1);
+by (fast_tac (claset() addss (simpset())) 1);
 by (fast_tac (le_cs addDs [mono_lemma] 
-                    addss (!simpset addsimps [mult_1_right])) 1);
+                    addss (simpset() addsimps [mult_1_right])) 1);
 qed "mult_eq_self_implies_10";
 
 
 (*Thanks to Sten Agerholm*)
 goal Arith.thy  (* add_le_elim1 *)
     "!!m n k. [|m#+n le m#+k; m:nat; n:nat; k:nat|] ==> n le k";
 by (etac rev_mp 1);
 by (eres_inst_tac [("n","n")] nat_induct 1);
 by (Asm_simp_tac 1);
 by Safe_tac;
-by (asm_full_simp_tac (!simpset addsimps [not_le_iff_lt,nat_into_Ord]) 1);
+by (asm_full_simp_tac (simpset() addsimps [not_le_iff_lt,nat_into_Ord]) 1);
 by (etac lt_asym 1);
 by (assume_tac 1);
 by (Asm_full_simp_tac 1);
-by (asm_full_simp_tac (!simpset addsimps [le_iff, nat_into_Ord]) 1);
+by (asm_full_simp_tac (simpset() addsimps [le_iff, nat_into_Ord]) 1);
 by (Blast_tac 1);
 qed "add_le_elim1";