src/HOL/Arith.ML
changeset 4360 40e5c97e988d
parent 4356 0dfd34f0d33d
child 4378 e52f864c5b88
     1.1 --- a/src/HOL/Arith.ML	Thu Dec 04 09:05:59 1997 +0100
     1.2 +++ b/src/HOL/Arith.ML	Thu Dec 04 12:44:37 1997 +0100
     1.3 @@ -9,56 +9,38 @@
     1.4  
     1.5  (*** Basic rewrite rules for the arithmetic operators ***)
     1.6  
     1.7 -goalw Arith.thy [pred_def] "pred 0 = 0";
     1.8 -by (Simp_tac 1);
     1.9 -qed "pred_0";
    1.10 -
    1.11 -goalw Arith.thy [pred_def] "pred(Suc n) = n";
    1.12 -by (Simp_tac 1);
    1.13 -qed "pred_Suc";
    1.14 -
    1.15 -Addsimps [pred_0,pred_Suc];
    1.16 -
    1.17 -(** pred **)
    1.18 -
    1.19 -val prems = goal Arith.thy "n ~= 0 ==> Suc(pred n) = n";
    1.20 -by (res_inst_tac [("n","n")] natE 1);
    1.21 -by (cut_facts_tac prems 1);
    1.22 -by (ALLGOALS Asm_full_simp_tac);
    1.23 -qed "Suc_pred";
    1.24 -Addsimps [Suc_pred];
    1.25 -
    1.26 -goal Arith.thy "pred(n) <= (n::nat)";
    1.27 -by (res_inst_tac [("n","n")] natE 1);
    1.28 -by (ALLGOALS Asm_simp_tac);
    1.29 -qed "pred_le";
    1.30 -AddIffs [pred_le];
    1.31 -
    1.32 -goalw Arith.thy [pred_def] "m<=n --> pred(m) <= pred(n)";
    1.33 -by (simp_tac (simpset() addsplits [expand_nat_case]) 1);
    1.34 -qed_spec_mp "pred_le_mono";
    1.35 -
    1.36 -goal Arith.thy "!!n. n ~= 0 ==> pred n < n";
    1.37 -by (exhaust_tac "n" 1);
    1.38 -by (ALLGOALS Asm_full_simp_tac);
    1.39 -qed "pred_less";
    1.40 -Addsimps [pred_less];
    1.41  
    1.42  (** Difference **)
    1.43  
    1.44 -qed_goalw "diff_0_eq_0" Arith.thy [pred_def]
    1.45 +qed_goal "diff_0_eq_0" Arith.thy
    1.46      "0 - n = 0"
    1.47   (fn _ => [induct_tac "n" 1,  ALLGOALS Asm_simp_tac]);
    1.48  
    1.49  (*Must simplify BEFORE the induction!!  (Else we get a critical pair)
    1.50    Suc(m) - Suc(n)   rewrites to   pred(Suc(m) - n)  *)
    1.51 -qed_goalw "diff_Suc_Suc" Arith.thy [pred_def]
    1.52 +qed_goal "diff_Suc_Suc" Arith.thy
    1.53      "Suc(m) - Suc(n) = m - n"
    1.54   (fn _ =>
    1.55    [Simp_tac 1, induct_tac "n" 1, ALLGOALS Asm_simp_tac]);
    1.56  
    1.57  Addsimps [diff_0_eq_0, diff_Suc_Suc];
    1.58  
    1.59 +(* Could be (and is, below) generalized in various ways;
    1.60 +   However, none of the generalizations are currently in the simpset,
    1.61 +   and I dread to think what happens if I put them in *)
    1.62 +goal Arith.thy "!!n. 0 < n ==> Suc(n-1) = n";
    1.63 +by(asm_simp_tac (simpset() addsplits [expand_nat_case]) 1);
    1.64 +qed "Suc_pred";
    1.65 +Addsimps [Suc_pred];
    1.66 +
    1.67 +(* Generalize? *)
    1.68 +goal Arith.thy "!!n. 0<n ==> n-1 < n";
    1.69 +by(asm_simp_tac (simpset() addsplits [expand_nat_case]) 1);
    1.70 +qed "pred_less";
    1.71 +Addsimps [pred_less];
    1.72 +
    1.73 +Delsimps [diff_Suc];
    1.74 +
    1.75  
    1.76  (**** Inductive properties of the operators ****)
    1.77  
    1.78 @@ -120,17 +102,25 @@
    1.79  by (induct_tac "m" 1);
    1.80  by (ALLGOALS Asm_simp_tac);
    1.81  qed "add_is_0";
    1.82 -Addsimps [add_is_0];
    1.83 +AddIffs [add_is_0];
    1.84  
    1.85 -goal Arith.thy "(pred (m+n) = 0) = (m=0 & pred n = 0 | pred m = 0 & n=0)";
    1.86 -by (induct_tac "m" 1);
    1.87 +goal Arith.thy "(0<m+n) = (0<m | 0<n)";
    1.88 +by(simp_tac (simpset() delsimps [neq0_conv] addsimps [neq0_conv RS sym]) 1);
    1.89 +qed "add_gr_0";
    1.90 +AddIffs [add_gr_0];
    1.91 +
    1.92 +(* FIXME: really needed?? *)
    1.93 +goal Arith.thy "((m+n)-1 = 0) = (m=0 & n-1 = 0 | m-1 = 0 & n=0)";
    1.94 +by (exhaust_tac "m" 1);
    1.95  by (ALLGOALS (fast_tac (claset() addss (simpset()))));
    1.96  qed "pred_add_is_0";
    1.97  Addsimps [pred_add_is_0];
    1.98  
    1.99 +(* Could be generalized, eg to "!!n. k<n ==> m+(n-(Suc k)) = (m+n)-(Suc k)" *)
   1.100  goal Arith.thy "!!n. n ~= 0 ==> m + pred n = pred(m+n)";
   1.101 -by (induct_tac "m" 1);
   1.102 -by (ALLGOALS Asm_simp_tac);
   1.103 +by (exhaust_tac "m" 1);
   1.104 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_Suc]
   1.105 +                                      addsplits [expand_nat_case])));
   1.106  qed "add_pred";
   1.107  Addsimps [add_pred];
   1.108  
   1.109 @@ -336,9 +326,6 @@
   1.110  
   1.111  (*** Difference ***)
   1.112  
   1.113 -qed_goal "pred_Suc_diff" Arith.thy "pred(Suc m - n) = m - n"
   1.114 - (fn _ => [induct_tac "n" 1, ALLGOALS Asm_simp_tac]);
   1.115 -Addsimps [pred_Suc_diff];
   1.116  
   1.117  qed_goal "diff_self_eq_0" Arith.thy "m - m = 0"
   1.118   (fn _ => [induct_tac "m" 1, ALLGOALS Asm_simp_tac]);
   1.119 @@ -359,7 +346,6 @@
   1.120  qed "le_add_diff_inverse2";
   1.121  
   1.122  Addsimps  [le_add_diff_inverse, le_add_diff_inverse2];
   1.123 -Delsimps  [diff_Suc];
   1.124  
   1.125  
   1.126  (*** More results about difference ***)
   1.127 @@ -387,6 +373,14 @@
   1.128  by (ALLGOALS Asm_simp_tac);
   1.129  qed "diff_diff_left";
   1.130  
   1.131 +(* This is a trivial consequence of diff_diff_left;
   1.132 +   could be got rid of if diff_diff_left were in the simpset...
   1.133 +*)
   1.134 +goal Arith.thy "(Suc m - n)-1 = m - n";
   1.135 +by(simp_tac (simpset() addsimps [diff_diff_left]) 1);
   1.136 +qed "pred_Suc_diff";
   1.137 +Addsimps [pred_Suc_diff];
   1.138 +
   1.139  (*This and the next few suggested by Florian Kammueller*)
   1.140  goal Arith.thy "!!i::nat. i-j-k = i-k-j";
   1.141  by (simp_tac (simpset() addsimps [diff_diff_left, add_commute]) 1);
   1.142 @@ -654,7 +648,7 @@
   1.143  by (atac 1);
   1.144  by (etac le_trans 1);
   1.145  by (res_inst_tac [("m1","n")] (pred_Suc_diff RS subst) 1);
   1.146 -by (rtac pred_le 1);
   1.147 +by (simp_tac (simpset() addsimps [diff_Suc] addsplits [expand_nat_case]) 1);
   1.148  qed_spec_mp "diff_le_mono";
   1.149  
   1.150  goal Arith.thy "!!n::nat. m<=n ==> (l-n) <= (l-m)";