src/HOL/Divides.ML
changeset 5537 c2bd39a2c0ee
parent 5498 7b81cae2774f
child 5983 79e301a6a51b
equal deleted inserted replaced
5536:130f3d891fb2 5537:c2bd39a2c0ee
    59 by (asm_simp_tac (simpset() addsimps [add_commute, mod_add_self2]) 1);
    59 by (asm_simp_tac (simpset() addsimps [add_commute, mod_add_self2]) 1);
    60 qed "mod_add_self1";
    60 qed "mod_add_self1";
    61 
    61 
    62 Goal "!!n. 0<n ==> (m + k*n) mod n = m mod n";
    62 Goal "!!n. 0<n ==> (m + k*n) mod n = m mod n";
    63 by (induct_tac "k" 1);
    63 by (induct_tac "k" 1);
    64 by (ALLGOALS (asm_simp_tac (simpset() addsimps (add_ac @ [mod_add_self1]))));
    64 by (ALLGOALS (asm_simp_tac (simpset() addsimps add_ac @ [mod_add_self1])));
    65 qed "mod_mult_self1";
    65 qed "mod_mult_self1";
    66 
    66 
    67 Goal "0<n ==> (m + n*k) mod n = m mod n";
    67 Goal "0<n ==> (m + n*k) mod n = m mod n";
    68 by (asm_simp_tac (simpset() addsimps [mult_commute, mod_mult_self1]) 1);
    68 by (asm_simp_tac (simpset() addsimps [mult_commute, mod_mult_self1]) 1);
    69 qed "mod_mult_self2";
    69 qed "mod_mult_self2";
   124 (*Main Result about quotient and remainder.*)
   124 (*Main Result about quotient and remainder.*)
   125 Goal "0<n ==> (m div n)*n + m mod n = m";
   125 Goal "0<n ==> (m div n)*n + m mod n = m";
   126 by (res_inst_tac [("n","m")] less_induct 1);
   126 by (res_inst_tac [("n","m")] less_induct 1);
   127 by (stac mod_if 1);
   127 by (stac mod_if 1);
   128 by (ALLGOALS (asm_simp_tac 
   128 by (ALLGOALS (asm_simp_tac 
   129 	      (simpset() addsimps ([add_assoc] @
   129 	      (simpset() addsimps [add_assoc, div_less, div_geq,
   130 				   [div_less, div_geq,
   130 				   add_diff_inverse, diff_less])));
   131 				    add_diff_inverse, diff_less]))));
       
   132 qed "mod_div_equality";
   131 qed "mod_div_equality";
   133 
   132 
   134 (* a simple rearrangement of mod_div_equality: *)
   133 (* a simple rearrangement of mod_div_equality: *)
   135 Goal "0<k ==> k*(m div k) = m - (m mod k)";
   134 Goal "0<k ==> k*(m div k) = m - (m mod k)";
   136 by (dres_inst_tac [("m","m")] mod_div_equality 1);
   135 by (dres_inst_tac [("m","m")] mod_div_equality 1);
   159 by (asm_simp_tac (simpset() addsimps [add_commute, div_add_self2]) 1);
   158 by (asm_simp_tac (simpset() addsimps [add_commute, div_add_self2]) 1);
   160 qed "div_add_self1";
   159 qed "div_add_self1";
   161 
   160 
   162 Goal "!!n. 0<n ==> (m + k*n) div n = k + m div n";
   161 Goal "!!n. 0<n ==> (m + k*n) div n = k + m div n";
   163 by (induct_tac "k" 1);
   162 by (induct_tac "k" 1);
   164 by (ALLGOALS (asm_simp_tac (simpset() addsimps (add_ac @ [div_add_self1]))));
   163 by (ALLGOALS (asm_simp_tac (simpset() addsimps add_ac @ [div_add_self1])));
   165 qed "div_mult_self1";
   164 qed "div_mult_self1";
   166 
   165 
   167 Goal "0<n ==> (m + n*k) div n = k + m div n";
   166 Goal "0<n ==> (m + n*k) div n = k + m div n";
   168 by (asm_simp_tac (simpset() addsimps [mult_commute, div_mult_self1]) 1);
   167 by (asm_simp_tac (simpset() addsimps [mult_commute, div_mult_self1]) 1);
   169 qed "div_mult_self2";
   168 qed "div_mult_self2";