src/HOL/Divides.ML
changeset 3496 32e7edc609fd
parent 3484 1e93eb09ebb9
child 3718 d78cf498a88c
equal deleted inserted replaced
3495:04739732b13e 3496:32e7edc609fd
   124 by (strip_tac 1);
   124 by (strip_tac 1);
   125 by (case_tac "na<k" 1);
   125 by (case_tac "na<k" 1);
   126 (* 1  case n<k *)
   126 (* 1  case n<k *)
   127 by (subgoal_tac "m<k" 1);
   127 by (subgoal_tac "m<k" 1);
   128 by (asm_simp_tac (!simpset addsimps [div_less]) 1);
   128 by (asm_simp_tac (!simpset addsimps [div_less]) 1);
   129 by (etac le_less_trans 1);
   129 by (trans_tac 1);
   130 by (atac 1);
       
   131 (* 2  case n >= k *)
   130 (* 2  case n >= k *)
   132 by (case_tac "m<k" 1);
   131 by (case_tac "m<k" 1);
   133 (* 2.1  case m<k *)
   132 (* 2.1  case m<k *)
   134 by (asm_simp_tac (!simpset addsimps [div_less]) 1);
   133 by (asm_simp_tac (!simpset addsimps [div_less]) 1);
   135 (* 2.2  case m>=k *)
   134 (* 2.2  case m>=k *)
   136 by (asm_simp_tac (!simpset addsimps [div_geq]) 1);
   135 by (asm_simp_tac (!simpset addsimps [div_geq, diff_less, diff_le_mono]) 1);
   137 by (REPEAT (eresolve_tac [allE,impE] 1));
       
   138 by (REPEAT (eresolve_tac [allE,impE] 2));
       
   139 by (atac 3);
       
   140 by (asm_simp_tac (!simpset addsimps [diff_less]) 1);
       
   141 by (etac diff_le_mono 1);
       
   142 qed_spec_mp "div_le_mono";
   136 qed_spec_mp "div_le_mono";
   143 
   137 
   144 
   138 
   145 (* Antimonotonicity of div in second argument *)
   139 (* Antimonotonicity of div in second argument *)
   146 goal thy "!!k m n. [| 0<m; m<=n |] ==> (k div n) <= (k div m)";
   140 goal thy "!!k m n. [| 0<m; m<=n |] ==> (k div n) <= (k div m)";
   147 by (subgoal_tac "0<n" 1);
   141 by (subgoal_tac "0<n" 1);
   148  by(trans_tac 2);
   142  by (trans_tac 2);
   149 by (res_inst_tac [("n","k")] less_induct 1);
   143 by (res_inst_tac [("n","k")] less_induct 1);
   150 by(Simp_tac 1);
   144 by (Simp_tac 1);
   151 by(rename_tac "k" 1);
   145 by (rename_tac "k" 1);
   152 by (case_tac "k<n" 1);
   146 by (case_tac "k<n" 1);
   153  by (asm_simp_tac (!simpset addsimps [div_less]) 1);
   147  by (asm_simp_tac (!simpset addsimps [div_less]) 1);
   154 by (subgoal_tac "~(k<m)" 1);
   148 by (subgoal_tac "~(k<m)" 1);
   155  by(trans_tac 2);
   149  by (trans_tac 2);
   156 by (asm_simp_tac (!simpset addsimps [div_geq]) 1);
   150 by (asm_simp_tac (!simpset addsimps [div_geq]) 1);
   157 by (subgoal_tac "(k-n) div n <= (k-m) div n" 1);
   151 by (subgoal_tac "(k-n) div n <= (k-m) div n" 1);
   158  by (etac le_trans 1);
   152  by (best_tac (!claset addIs [le_trans] 
   159  by (REPEAT (eresolve_tac [allE,impE] 1));
   153                        addss (!simpset addsimps [diff_less])) 1);
   160   by (atac 2);
       
   161  by (asm_simp_tac (!simpset addsimps [diff_less]) 1);
       
   162 by (REPEAT (eresolve_tac [div_le_mono,diff_le_mono2] 1));
   154 by (REPEAT (eresolve_tac [div_le_mono,diff_le_mono2] 1));
   163 qed "div_le_mono2";
   155 qed "div_le_mono2";
   164 
   156 
   165 goal thy "!!m n. 0<n ==> m div n <= m";
   157 goal thy "!!m n. 0<n ==> m div n <= m";
   166 by (subgoal_tac "m div n <= m div 1" 1);
   158 by (subgoal_tac "m div n <= m div 1" 1);
   171 Addsimps [div_le_dividend];
   163 Addsimps [div_le_dividend];
   172 
   164 
   173 (* Similar for "less than" *)
   165 (* Similar for "less than" *)
   174 goal thy "!!m n. 1<n ==> (0 < m) --> (m div n < m)";
   166 goal thy "!!m n. 1<n ==> (0 < m) --> (m div n < m)";
   175 by (res_inst_tac [("n","m")] less_induct 1);
   167 by (res_inst_tac [("n","m")] less_induct 1);
   176 by(Simp_tac 1);
   168 by (Simp_tac 1);
   177 by(rename_tac "m" 1);
   169 by (rename_tac "m" 1);
   178 by (case_tac "m<n" 1);
   170 by (case_tac "m<n" 1);
   179  by (asm_full_simp_tac (!simpset addsimps [div_less]) 1);
   171  by (asm_full_simp_tac (!simpset addsimps [div_less]) 1);
   180 by (subgoal_tac "0<n" 1);
   172 by (subgoal_tac "0<n" 1);
   181  by(trans_tac 2);
   173  by (trans_tac 2);
   182 by (asm_full_simp_tac (!simpset addsimps [div_geq]) 1);
   174 by (asm_full_simp_tac (!simpset addsimps [div_geq]) 1);
   183 by (case_tac "n<m" 1);
   175 by (case_tac "n<m" 1);
   184  by (subgoal_tac "(m-n) div n < (m-n)" 1);
   176  by (subgoal_tac "(m-n) div n < (m-n)" 1);
   185   by (REPEAT (ares_tac [impI,less_trans_Suc] 1));
   177   by (REPEAT (ares_tac [impI,less_trans_Suc] 1));
   186   by (asm_full_simp_tac (!simpset addsimps [diff_less]) 1);
   178   by (asm_full_simp_tac (!simpset addsimps [diff_less]) 1);
   187  by (dres_inst_tac [("m","n")] less_imp_diff_positive 1);
   179  by (dres_inst_tac [("m","n")] less_imp_diff_positive 1);
   188  by (asm_full_simp_tac (!simpset addsimps [diff_less]) 1);
   180  by (asm_full_simp_tac (!simpset addsimps [diff_less]) 1);
   189 (* case n=m *)
   181 (* case n=m *)
   190 by (subgoal_tac "m=n" 1);
   182 by (subgoal_tac "m=n" 1);
   191  by(trans_tac 2);
   183  by (trans_tac 2);
   192 by (asm_simp_tac (!simpset addsimps [div_less]) 1);
   184 by (asm_simp_tac (!simpset addsimps [div_less]) 1);
   193 qed_spec_mp "div_less_dividend";
   185 qed_spec_mp "div_less_dividend";
   194 Addsimps [div_less_dividend];
   186 Addsimps [div_less_dividend];
   195 
   187 
   196 (*** Further facts about mod (mainly for the mutilated chess board ***)
   188 (*** Further facts about mod (mainly for the mutilated chess board ***)