equal
deleted
inserted
replaced
5 |
5 |
6 The "divides" relation, the greatest common divisor and Euclid's algorithm |
6 The "divides" relation, the greatest common divisor and Euclid's algorithm |
7 *) |
7 *) |
8 |
8 |
9 eta_contract:=false; |
9 eta_contract:=false; |
10 |
|
11 open Primes; |
|
12 |
10 |
13 (************************************************) |
11 (************************************************) |
14 (** Divides Relation **) |
12 (** Divides Relation **) |
15 (************************************************) |
13 (************************************************) |
16 |
14 |
123 |
121 |
124 |
122 |
125 (* if f divides a and b then f divides egcd(a,b) *) |
123 (* if f divides a and b then f divides egcd(a,b) *) |
126 |
124 |
127 Goalw [dvd_def] "[| f dvd a; f dvd b; 0<b |] ==> f dvd (a mod b)"; |
125 Goalw [dvd_def] "[| f dvd a; f dvd b; 0<b |] ==> f dvd (a mod b)"; |
128 by (safe_tac (claset() addSIs [mult_type, mod_type])); |
126 by (safe_tac (claset() addSIs [mod_type])); |
129 ren "m n" 1; |
127 ren "m n" 1; |
130 by (rtac (zero_lt_mult_iff RS iffD1 RS conjE) 1); |
128 by (Asm_full_simp_tac 1); |
131 by (REPEAT_SOME assume_tac); |
|
132 by (res_inst_tac |
129 by (res_inst_tac |
133 [("x", "(((m div n)#*n #+ m mod n) #- ((f#*m) div (f#*n)) #* n)")] |
130 [("x", "(((m div n)#*n #+ m mod n) #- ((f#*m) div (f#*n)) #* n)")] |
134 bexI 1); |
131 bexI 1); |
135 by (asm_simp_tac (simpset() addsimps [diff_mult_distrib2, div_cancel, |
132 by (asm_simp_tac (simpset() addsimps [diff_mult_distrib2, div_cancel, |
136 mult_mod_distrib, add_mult_distrib_left, |
133 mult_mod_distrib, add_mult_distrib_left, |