src/ZF/Arith.ML
changeset 14 1c0926788772
parent 6 8ce8c4d13d4d
child 25 3ac1c0c0016e
     1.1 --- a/src/ZF/Arith.ML	Fri Sep 24 11:27:15 1993 +0200
     1.2 +++ b/src/ZF/Arith.ML	Thu Sep 30 10:10:21 1993 +0100
     1.3 @@ -28,10 +28,8 @@
     1.4  val rec_0 = result();
     1.5  
     1.6  goal Arith.thy "rec(succ(m),a,b) = b(m, rec(m,a,b))";
     1.7 -val rec_ss = ZF_ss 
     1.8 -      addsimps [nat_case_succ, nat_succI];
     1.9  by (rtac rec_trans 1);
    1.10 -by (simp_tac rec_ss 1);
    1.11 +by (simp_tac (ZF_ss addsimps [nat_case_succ, nat_succI]) 1);
    1.12  val rec_succ = result();
    1.13  
    1.14  val major::prems = goal Arith.thy
    1.15 @@ -103,6 +101,7 @@
    1.16      (nat_ind_tac "n" prems 1),
    1.17      (ALLGOALS (asm_simp_tac (nat_ss addsimps prems))) ]);
    1.18  
    1.19 +(*The conclusion is equivalent to m#-n <= m *)
    1.20  val prems = goal Arith.thy 
    1.21      "[| m:nat;  n:nat |] ==> m #- n : succ(m)";
    1.22  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    1.23 @@ -111,8 +110,9 @@
    1.24  by (etac succE 3);
    1.25  by (ALLGOALS
    1.26      (asm_simp_tac
    1.27 -     (nat_ss addsimps (prems@[diff_0,diff_0_eq_0,diff_succ_succ]))));
    1.28 -val diff_leq = result();
    1.29 +     (nat_ss addsimps (prems @ [succ_iff, diff_0, diff_0_eq_0, 
    1.30 +				diff_succ_succ]))));
    1.31 +val diff_less_succ = result();
    1.32  
    1.33  (*** Simplification over add, mult, diff ***)
    1.34  
    1.35 @@ -193,10 +193,10 @@
    1.36  
    1.37  (*addition distributes over multiplication*)
    1.38  val add_mult_distrib = prove_goal Arith.thy 
    1.39 -    "[| m:nat;  k:nat |] ==> (m #+ n) #* k = (m #* k) #+ (n #* k)"
    1.40 - (fn prems=>
    1.41 -  [ (nat_ind_tac "m" prems 1),
    1.42 -    (ALLGOALS (asm_simp_tac (arith_ss addsimps ([add_assoc RS sym]@prems)))) ]);
    1.43 +    "!!m n. [| m:nat;  k:nat |] ==> (m #+ n) #* k = (m #* k) #+ (n #* k)"
    1.44 + (fn _=>
    1.45 +  [ (etac nat_induct 1),
    1.46 +    (ALLGOALS (asm_simp_tac (arith_ss addsimps [add_assoc RS sym]))) ]);
    1.47  
    1.48  (*Distributive law on the left; requires an extra typing premise*)
    1.49  val add_mult_distrib_left = prove_goal Arith.thy 
    1.50 @@ -209,10 +209,10 @@
    1.51  
    1.52  (*Associative law for multiplication*)
    1.53  val mult_assoc = prove_goal Arith.thy 
    1.54 -    "[| m:nat;  n:nat;  k:nat |] ==> (m #* n) #* k = m #* (n #* k)"
    1.55 - (fn prems=>
    1.56 -  [ (nat_ind_tac "m" prems 1),
    1.57 -    (ALLGOALS (asm_simp_tac (arith_ss addsimps (prems@[add_mult_distrib])))) ]);
    1.58 +    "!!m n k. [| m:nat;  n:nat;  k:nat |] ==> (m #* n) #* k = m #* (n #* k)"
    1.59 + (fn _=>
    1.60 +  [ (etac nat_induct 1),
    1.61 +    (ALLGOALS (asm_simp_tac (arith_ss addsimps [add_mult_distrib]))) ]);
    1.62  
    1.63  
    1.64  (*** Difference ***)
    1.65 @@ -231,8 +231,8 @@
    1.66  by (resolve_tac prems 1);
    1.67  by (resolve_tac prems 1);
    1.68  by (ALLGOALS (asm_simp_tac
    1.69 -	      (arith_ss addsimps (prems@[succ_mem_succ_iff, Ord_0_mem_succ, 
    1.70 -				  naturals_are_ordinals]))));
    1.71 +	      (arith_ss addsimps (prems@[succ_mem_succ_iff, nat_0_in_succ,
    1.72 +					 naturals_are_ordinals]))));
    1.73  val add_diff_inverse = result();
    1.74  
    1.75  
    1.76 @@ -257,7 +257,7 @@
    1.77  by (etac rev_mp 1);
    1.78  by (etac rev_mp 1);
    1.79  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    1.80 -by (ALLGOALS (asm_simp_tac (nat_ss addsimps [diff_leq,diff_succ_succ])));
    1.81 +by (ALLGOALS (asm_simp_tac (nat_ss addsimps [diff_less_succ,diff_succ_succ])));
    1.82  val div_termination = result();
    1.83  
    1.84  val div_rls =
    1.85 @@ -335,6 +335,65 @@
    1.86  (*May not simplify even with ZF_ss because it would expand m:succ(...) *)
    1.87  by (rtac (add_0 RS ssubst) 1);
    1.88  by (rtac (add_succ RS ssubst) 2);
    1.89 -by (REPEAT (ares_tac [nnat, Ord_0_mem_succ, succ_mem_succI, 
    1.90 +by (REPEAT (ares_tac [nnat, nat_0_in_succ, succ_mem_succI, 
    1.91  		      naturals_are_ordinals, nat_succI, add_type] 1));
    1.92  val add_less_succ_self = result();
    1.93 +
    1.94 +goal Arith.thy "!!m n. [| m:nat;  n:nat |] ==> m <= m #+ n";
    1.95 +by (rtac (add_less_succ_self RS member_succD) 1);
    1.96 +by (REPEAT (ares_tac [naturals_are_ordinals, add_type] 1));
    1.97 +val add_leq_self = result();
    1.98 +
    1.99 +goal Arith.thy "!!m n. [| m:nat;  n:nat |] ==> m <= n #+ m";
   1.100 +by (rtac (add_commute RS ssubst) 1);
   1.101 +by (REPEAT (ares_tac [add_leq_self] 1));
   1.102 +val add_leq_self2 = result();
   1.103 +
   1.104 +(** Monotonicity of addition **)
   1.105 +
   1.106 +(*strict, in 1st argument*)
   1.107 +goal Arith.thy "!!i j k. [| i:j; j:nat |] ==> i#+k : j#+k";
   1.108 +by (etac succ_less_induct 1);
   1.109 +by (ALLGOALS (asm_simp_tac (arith_ss addsimps [succ_iff])));
   1.110 +val add_less_mono1 = result();
   1.111 +
   1.112 +(*strict, in both arguments*)
   1.113 +goal Arith.thy "!!i j k l. [| i:j; k:l; j:nat; l:nat |] ==> i#+k : j#+l";
   1.114 +by (rtac (add_less_mono1 RS Ord_trans) 1);
   1.115 +by (REPEAT_FIRST (ares_tac [add_type, naturals_are_ordinals]));
   1.116 +by (EVERY [rtac (add_commute RS ssubst) 1,
   1.117 +	   rtac (add_commute RS ssubst) 3,
   1.118 +	   rtac add_less_mono1 5]);
   1.119 +by (REPEAT (ares_tac [Ord_nat RSN (3,Ord_trans)] 1));
   1.120 +val add_less_mono = result();
   1.121 +
   1.122 +(*A [clumsy] way of lifting < monotonictity to <= monotonicity *)
   1.123 +val less_mono::ford::prems = goal Ord.thy
   1.124 +     "[| !!i j. [| i:j; j:k |] ==> f(i) : f(j);	\
   1.125 +\        !!i. i:k ==> f(i):k;			\
   1.126 +\        i<=j;  i:k;  j:k;  Ord(k)		\
   1.127 +\     |] ==> f(i) <= f(j)";
   1.128 +by (cut_facts_tac prems 1);
   1.129 +by (rtac member_succD 1);
   1.130 +by (dtac member_succI 1);
   1.131 +by (fast_tac (ZF_cs addSIs [less_mono]) 3);
   1.132 +by (REPEAT (ares_tac [ford,Ord_in_Ord] 1));
   1.133 +val Ord_less_mono_imp_mono = result();
   1.134 +
   1.135 +(*<=, in 1st argument*)
   1.136 +goal Arith.thy
   1.137 +    "!!i j k. [| i<=j; i:nat; j:nat; k:nat |] ==> i#+k <= j#+k";
   1.138 +by (res_inst_tac [("f", "%j.j#+k")] Ord_less_mono_imp_mono 1);
   1.139 +by (REPEAT (ares_tac [add_less_mono1, add_type, Ord_nat] 1));
   1.140 +val add_mono1 = result();
   1.141 +
   1.142 +(*<=, in both arguments*)
   1.143 +goal Arith.thy
   1.144 +    "!!i j k. [| i<=j; k<=l; i:nat; j:nat; k:nat; l:nat |] ==> i#+k <= j#+l";
   1.145 +by (rtac (add_mono1 RS subset_trans) 1);
   1.146 +by (REPEAT (assume_tac 1));
   1.147 +by (EVERY [rtac (add_commute RS ssubst) 1,
   1.148 +	   rtac (add_commute RS ssubst) 3,
   1.149 +	   rtac add_mono1 5]);
   1.150 +by (REPEAT (assume_tac 1));
   1.151 +val add_mono = result();