src/ZF/Arith.ML
changeset 6 8ce8c4d13d4d
parent 0 a5a9c433f639
child 14 1c0926788772
     1.1 --- a/src/ZF/Arith.ML	Fri Sep 17 12:53:53 1993 +0200
     1.2 +++ b/src/ZF/Arith.ML	Fri Sep 17 16:16:38 1993 +0200
     1.3 @@ -29,10 +29,9 @@
     1.4  
     1.5  goal Arith.thy "rec(succ(m),a,b) = b(m, rec(m,a,b))";
     1.6  val rec_ss = ZF_ss 
     1.7 -      addcongs (mk_typed_congs Arith.thy [("b", "[i,i]=>i")])
     1.8 -      addrews [nat_case_succ, nat_succI];
     1.9 +      addsimps [nat_case_succ, nat_succI];
    1.10  by (rtac rec_trans 1);
    1.11 -by (SIMP_TAC rec_ss 1);
    1.12 +by (simp_tac rec_ss 1);
    1.13  val rec_succ = result();
    1.14  
    1.15  val major::prems = goal Arith.thy
    1.16 @@ -42,20 +41,12 @@
    1.17  \    |] ==> rec(n,a,b) : C(n)";
    1.18  by (rtac (major RS nat_induct) 1);
    1.19  by (ALLGOALS
    1.20 -    (ASM_SIMP_TAC (ZF_ss addrews (prems@[rec_0,rec_succ]))));
    1.21 +    (asm_simp_tac (ZF_ss addsimps (prems@[rec_0,rec_succ]))));
    1.22  val rec_type = result();
    1.23  
    1.24 -val prems = goalw Arith.thy [rec_def]
    1.25 -    "[| n=n';  a=a';  !!m z. b(m,z)=b'(m,z)  \
    1.26 -\    |] ==> rec(n,a,b)=rec(n',a',b')";
    1.27 -by (SIMP_TAC (ZF_ss addcongs [transrec_cong,nat_case_cong] 
    1.28 -		    addrews (prems RL [sym])) 1);
    1.29 -val rec_cong = result();
    1.30 -
    1.31  val nat_typechecks = [rec_type,nat_0I,nat_1I,nat_succI,Ord_nat];
    1.32  
    1.33 -val nat_ss = ZF_ss addcongs [nat_case_cong,rec_cong]
    1.34 -	       	   addrews ([rec_0,rec_succ] @ nat_typechecks);
    1.35 +val nat_ss = ZF_ss addsimps ([rec_0,rec_succ] @ nat_typechecks);
    1.36  
    1.37  
    1.38  (** Addition **)
    1.39 @@ -101,16 +92,16 @@
    1.40      "n:nat ==> 0 #- n = 0"
    1.41   (fn [prem]=>
    1.42    [ (rtac (prem RS nat_induct) 1),
    1.43 -    (ALLGOALS (ASM_SIMP_TAC nat_ss)) ]);
    1.44 +    (ALLGOALS (asm_simp_tac nat_ss)) ]);
    1.45  
    1.46  (*Must simplify BEFORE the induction!!  (Else we get a critical pair)
    1.47    succ(m) #- succ(n)   rewrites to   pred(succ(m) #- n)  *)
    1.48  val diff_succ_succ = prove_goalw Arith.thy [diff_def]
    1.49      "[| m:nat;  n:nat |] ==> succ(m) #- succ(n) = m #- n"
    1.50   (fn prems=>
    1.51 -  [ (ASM_SIMP_TAC (nat_ss addrews prems) 1),
    1.52 +  [ (asm_simp_tac (nat_ss addsimps prems) 1),
    1.53      (nat_ind_tac "n" prems 1),
    1.54 -    (ALLGOALS (ASM_SIMP_TAC (nat_ss addrews prems))) ]);
    1.55 +    (ALLGOALS (asm_simp_tac (nat_ss addsimps prems))) ]);
    1.56  
    1.57  val prems = goal Arith.thy 
    1.58      "[| m:nat;  n:nat |] ==> m #- n : succ(m)";
    1.59 @@ -119,8 +110,8 @@
    1.60  by (resolve_tac prems 1);
    1.61  by (etac succE 3);
    1.62  by (ALLGOALS
    1.63 -    (ASM_SIMP_TAC
    1.64 -     (nat_ss addrews (prems@[diff_0,diff_0_eq_0,diff_succ_succ]))));
    1.65 +    (asm_simp_tac
    1.66 +     (nat_ss addsimps (prems@[diff_0,diff_0_eq_0,diff_succ_succ]))));
    1.67  val diff_leq = result();
    1.68  
    1.69  (*** Simplification over add, mult, diff ***)
    1.70 @@ -130,10 +121,7 @@
    1.71  		  mult_0, mult_succ,
    1.72  		  diff_0, diff_0_eq_0, diff_succ_succ];
    1.73  
    1.74 -val arith_congs = mk_congs Arith.thy ["op #+", "op #-", "op #*"];
    1.75 -
    1.76 -val arith_ss = nat_ss addcongs arith_congs
    1.77 -                      addrews  (arith_rews@arith_typechecks);
    1.78 +val arith_ss = nat_ss addsimps (arith_rews@arith_typechecks);
    1.79  
    1.80  (*** Addition ***)
    1.81  
    1.82 @@ -142,7 +130,7 @@
    1.83      "m:nat ==> (m #+ n) #+ k = m #+ (n #+ k)"
    1.84   (fn prems=>
    1.85    [ (nat_ind_tac "m" prems 1),
    1.86 -    (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]);
    1.87 +    (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]);
    1.88  
    1.89  (*The following two lemmas are used for add_commute and sometimes
    1.90    elsewhere, since they are safe for rewriting.*)
    1.91 @@ -150,13 +138,13 @@
    1.92      "m:nat ==> m #+ 0 = m"
    1.93   (fn prems=>
    1.94    [ (nat_ind_tac "m" prems 1),
    1.95 -    (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]); 
    1.96 +    (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]); 
    1.97  
    1.98  val add_succ_right = prove_goal Arith.thy
    1.99      "m:nat ==> m #+ succ(n) = succ(m #+ n)"
   1.100   (fn prems=>
   1.101    [ (nat_ind_tac "m" prems 1),
   1.102 -    (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]); 
   1.103 +    (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]); 
   1.104  
   1.105  (*Commutative law for addition*)  
   1.106  val add_commute = prove_goal Arith.thy 
   1.107 @@ -164,15 +152,15 @@
   1.108   (fn prems=>
   1.109    [ (nat_ind_tac "n" prems 1),
   1.110      (ALLGOALS
   1.111 -     (ASM_SIMP_TAC
   1.112 -      (arith_ss addrews (prems@[add_0_right, add_succ_right])))) ]);
   1.113 +     (asm_simp_tac
   1.114 +      (arith_ss addsimps (prems@[add_0_right, add_succ_right])))) ]);
   1.115  
   1.116  (*Cancellation law on the left*)
   1.117  val [knat,eqn] = goal Arith.thy 
   1.118      "[| k:nat;  k #+ m = k #+ n |] ==> m=n";
   1.119  by (rtac (eqn RS rev_mp) 1);
   1.120  by (nat_ind_tac "k" [knat] 1);
   1.121 -by (ALLGOALS (SIMP_TAC arith_ss));
   1.122 +by (ALLGOALS (simp_tac arith_ss));
   1.123  by (fast_tac ZF_cs 1);
   1.124  val add_left_cancel = result();
   1.125  
   1.126 @@ -183,39 +171,40 @@
   1.127      "m:nat ==> m #* 0 = 0"
   1.128   (fn prems=>
   1.129    [ (nat_ind_tac "m" prems 1),
   1.130 -    (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems)))  ]);
   1.131 +    (ALLGOALS (asm_simp_tac (arith_ss addsimps prems)))  ]);
   1.132  
   1.133  (*right successor law for multiplication*)
   1.134  val mult_succ_right = prove_goal Arith.thy 
   1.135 -    "[| m:nat;  n:nat |] ==> m #* succ(n) = m #+ (m #* n)"
   1.136 - (fn prems=>
   1.137 -  [ (nat_ind_tac "m" prems 1),
   1.138 -    (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews ([add_assoc RS sym]@prems)))),
   1.139 +    "!!m n. [| m:nat;  n:nat |] ==> m #* succ(n) = m #+ (m #* n)"
   1.140 + (fn _=>
   1.141 +  [ (nat_ind_tac "m" [] 1),
   1.142 +    (ALLGOALS (asm_simp_tac (arith_ss addsimps [add_assoc RS sym]))),
   1.143         (*The final goal requires the commutative law for addition*)
   1.144 -    (REPEAT (ares_tac (prems@[refl,add_commute]@ZF_congs@arith_congs) 1))  ]);
   1.145 +    (rtac (add_commute RS subst_context) 1),
   1.146 +    (REPEAT (assume_tac 1))  ]);
   1.147  
   1.148  (*Commutative law for multiplication*)
   1.149  val mult_commute = prove_goal Arith.thy 
   1.150      "[| m:nat;  n:nat |] ==> m #* n = n #* m"
   1.151   (fn prems=>
   1.152    [ (nat_ind_tac "m" prems 1),
   1.153 -    (ALLGOALS (ASM_SIMP_TAC
   1.154 -	       (arith_ss addrews (prems@[mult_0_right, mult_succ_right])))) ]);
   1.155 +    (ALLGOALS (asm_simp_tac
   1.156 +	     (arith_ss addsimps (prems@[mult_0_right, mult_succ_right])))) ]);
   1.157  
   1.158  (*addition distributes over multiplication*)
   1.159  val add_mult_distrib = prove_goal Arith.thy 
   1.160      "[| m:nat;  k:nat |] ==> (m #+ n) #* k = (m #* k) #+ (n #* k)"
   1.161   (fn prems=>
   1.162    [ (nat_ind_tac "m" prems 1),
   1.163 -    (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews ([add_assoc RS sym]@prems)))) ]);
   1.164 +    (ALLGOALS (asm_simp_tac (arith_ss addsimps ([add_assoc RS sym]@prems)))) ]);
   1.165  
   1.166  (*Distributive law on the left; requires an extra typing premise*)
   1.167  val add_mult_distrib_left = prove_goal Arith.thy 
   1.168      "[| m:nat;  n:nat;  k:nat |] ==> k #* (m #+ n) = (k #* m) #+ (k #* n)"
   1.169   (fn prems=>
   1.170        let val mult_commute' = read_instantiate [("m","k")] mult_commute
   1.171 -          val ss = arith_ss addrews ([mult_commute',add_mult_distrib]@prems)
   1.172 -      in [ (SIMP_TAC ss 1) ]
   1.173 +          val ss = arith_ss addsimps ([mult_commute',add_mult_distrib]@prems)
   1.174 +      in [ (simp_tac ss 1) ]
   1.175        end);
   1.176  
   1.177  (*Associative law for multiplication*)
   1.178 @@ -223,7 +212,7 @@
   1.179      "[| m:nat;  n:nat;  k:nat |] ==> (m #* n) #* k = m #* (n #* k)"
   1.180   (fn prems=>
   1.181    [ (nat_ind_tac "m" prems 1),
   1.182 -    (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews (prems@[add_mult_distrib])))) ]);
   1.183 +    (ALLGOALS (asm_simp_tac (arith_ss addsimps (prems@[add_mult_distrib])))) ]);
   1.184  
   1.185  
   1.186  (*** Difference ***)
   1.187 @@ -232,7 +221,7 @@
   1.188      "m:nat ==> m #- m = 0"
   1.189   (fn prems=>
   1.190    [ (nat_ind_tac "m" prems 1),
   1.191 -    (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]);
   1.192 +    (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]);
   1.193  
   1.194  (*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *)
   1.195  val notless::prems = goal Arith.thy
   1.196 @@ -241,8 +230,8 @@
   1.197  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   1.198  by (resolve_tac prems 1);
   1.199  by (resolve_tac prems 1);
   1.200 -by (ALLGOALS (ASM_SIMP_TAC
   1.201 -	      (arith_ss addrews (prems@[succ_mem_succ_iff, Ord_0_mem_succ, 
   1.202 +by (ALLGOALS (asm_simp_tac
   1.203 +	      (arith_ss addsimps (prems@[succ_mem_succ_iff, Ord_0_mem_succ, 
   1.204  				  naturals_are_ordinals]))));
   1.205  val add_diff_inverse = result();
   1.206  
   1.207 @@ -251,29 +240,24 @@
   1.208  val [mnat,nnat] = goal Arith.thy
   1.209      "[| m:nat;  n:nat |] ==> (n#+m) #-n = m";
   1.210  by (rtac (nnat RS nat_induct) 1);
   1.211 -by (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews [mnat])));
   1.212 +by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mnat])));
   1.213  val diff_add_inverse = result();
   1.214  
   1.215  val [mnat,nnat] = goal Arith.thy
   1.216      "[| m:nat;  n:nat |] ==> n #- (n#+m) = 0";
   1.217  by (rtac (nnat RS nat_induct) 1);
   1.218 -by (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews [mnat])));
   1.219 +by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mnat])));
   1.220  val diff_add_0 = result();
   1.221  
   1.222  
   1.223  (*** Remainder ***)
   1.224  
   1.225  (*In ordinary notation: if 0<n and n<=m then m-n < m *)
   1.226 -val prems = goal Arith.thy
   1.227 -    "[| 0:n; ~ m:n;  m:nat;  n:nat |] ==> m #- n : m";
   1.228 -by (cut_facts_tac prems 1);
   1.229 +goal Arith.thy "!!m n. [| 0:n; ~ m:n;  m:nat;  n:nat |] ==> m #- n : m";
   1.230  by (etac rev_mp 1);
   1.231  by (etac rev_mp 1);
   1.232  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   1.233 -by (resolve_tac prems 1);
   1.234 -by (resolve_tac prems 1);
   1.235 -by (ALLGOALS (ASM_SIMP_TAC
   1.236 -	      (nat_ss addrews (prems@[diff_leq,diff_succ_succ]))));
   1.237 +by (ALLGOALS (asm_simp_tac (nat_ss addsimps [diff_leq,diff_succ_succ])));
   1.238  val div_termination = result();
   1.239  
   1.240  val div_rls =
   1.241 @@ -286,17 +270,17 @@
   1.242  by (REPEAT (ares_tac (prems @ div_rls) 1 ORELSE etac Ord_trans 1));
   1.243  val mod_type = result();
   1.244  
   1.245 -val div_ss = ZF_ss addrews [naturals_are_ordinals,div_termination];
   1.246 +val div_ss = ZF_ss addsimps [naturals_are_ordinals,div_termination];
   1.247  
   1.248  val prems = goal Arith.thy "[| 0:n;  m:n;  m:nat;  n:nat |] ==> m mod n = m";
   1.249  by (rtac (mod_def RS def_transrec RS trans) 1);
   1.250 -by (SIMP_TAC (div_ss addrews prems) 1);
   1.251 +by (simp_tac (div_ss addsimps prems) 1);
   1.252  val mod_less = result();
   1.253  
   1.254  val prems = goal Arith.thy
   1.255      "[| 0:n;  ~m:n;  m:nat;  n:nat |] ==> m mod n = (m#-n) mod n";
   1.256  by (rtac (mod_def RS def_transrec RS trans) 1);
   1.257 -by (SIMP_TAC (div_ss addrews prems) 1);
   1.258 +by (simp_tac (div_ss addsimps prems) 1);
   1.259  val mod_geq = result();
   1.260  
   1.261  (*** Quotient ***)
   1.262 @@ -310,13 +294,13 @@
   1.263  val prems = goal Arith.thy
   1.264      "[| 0:n;  m:n;  m:nat;  n:nat |] ==> m div n = 0";
   1.265  by (rtac (div_def RS def_transrec RS trans) 1);
   1.266 -by (SIMP_TAC (div_ss addrews prems) 1);
   1.267 +by (simp_tac (div_ss addsimps prems) 1);
   1.268  val div_less = result();
   1.269  
   1.270  val prems = goal Arith.thy
   1.271      "[| 0:n;  ~m:n;  m:nat;  n:nat |] ==> m div n = succ((m#-n) div n)";
   1.272  by (rtac (div_def RS def_transrec RS trans) 1);
   1.273 -by (SIMP_TAC (div_ss addrews prems) 1);
   1.274 +by (simp_tac (div_ss addsimps prems) 1);
   1.275  val div_geq = result();
   1.276  
   1.277  (*Main Result.*)
   1.278 @@ -326,8 +310,8 @@
   1.279  by (resolve_tac prems 1);
   1.280  by (res_inst_tac [("Q","x:n")] (excluded_middle RS disjE) 1);
   1.281  by (ALLGOALS 
   1.282 -    (ASM_SIMP_TAC
   1.283 -     (arith_ss addrews ([mod_type,div_type] @ prems @
   1.284 +    (asm_simp_tac
   1.285 +     (arith_ss addsimps ([mod_type,div_type] @ prems @
   1.286          [mod_less,mod_geq, div_less, div_geq,
   1.287  	 add_assoc, add_diff_inverse, div_termination]))));
   1.288  val mod_div_equality = result();
   1.289 @@ -338,7 +322,7 @@
   1.290  val [mnat,nnat] = goal Arith.thy
   1.291      "[| m:nat;  n:nat |] ==> ~ (m #+ n) : n";
   1.292  by (rtac (mnat RS nat_induct) 1);
   1.293 -by (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews [mem_not_refl])));
   1.294 +by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mem_not_refl])));
   1.295  by (rtac notI 1);
   1.296  by (etac notE 1);
   1.297  by (etac (succI1 RS Ord_trans) 1);