1 (* Title: HOL/Hoare/Arith2.ML |
|
2 ID: $Id$ |
|
3 Author: Norbert Galm |
|
4 Copyright 1995 TUM |
|
5 |
|
6 More arithmetic lemmas. |
|
7 *) |
|
8 |
|
9 (*** cd ***) |
|
10 |
|
11 Goalw [cd_def] "0<n ==> cd n n n"; |
|
12 by (Asm_simp_tac 1); |
|
13 qed "cd_nnn"; |
|
14 |
|
15 Goalw [cd_def] "[| cd x m n; 0<m; 0<n |] ==> x<=m & x<=n"; |
|
16 by (blast_tac (claset() addIs [dvd_imp_le]) 1); |
|
17 qed "cd_le"; |
|
18 |
|
19 Goalw [cd_def] "cd x m n = cd x n m"; |
|
20 by (Fast_tac 1); |
|
21 qed "cd_swap"; |
|
22 |
|
23 Goalw [cd_def] "n<=m ==> cd x m n = cd x (m-n) n"; |
|
24 by (blast_tac (claset() addIs [dvd_diff] addDs [dvd_diffD]) 1); |
|
25 qed "cd_diff_l"; |
|
26 |
|
27 Goalw [cd_def] "m<=n ==> cd x m n = cd x m (n-m)"; |
|
28 by (blast_tac (claset() addIs [dvd_diff] addDs [dvd_diffD]) 1); |
|
29 qed "cd_diff_r"; |
|
30 |
|
31 |
|
32 (*** gcd ***) |
|
33 |
|
34 Goalw [gcd_def] "0<n ==> n = gcd n n"; |
|
35 by (ftac cd_nnn 1); |
|
36 by (rtac (some_equality RS sym) 1); |
|
37 by (blast_tac (claset() addDs [cd_le]) 1); |
|
38 by (blast_tac (claset() addIs [le_anti_sym] addDs [cd_le]) 1); |
|
39 qed "gcd_nnn"; |
|
40 |
|
41 val prems = goalw (the_context ()) [gcd_def] "gcd m n = gcd n m"; |
|
42 by (simp_tac (simpset() addsimps [cd_swap]) 1); |
|
43 qed "gcd_swap"; |
|
44 |
|
45 Goalw [gcd_def] "n<=m ==> gcd m n = gcd (m-n) n"; |
|
46 by (subgoal_tac "n<=m ==> !x. cd x m n = cd x (m-n) n" 1); |
|
47 by (Asm_simp_tac 1); |
|
48 by (rtac allI 1); |
|
49 by (etac cd_diff_l 1); |
|
50 qed "gcd_diff_l"; |
|
51 |
|
52 Goalw [gcd_def] "m<=n ==> gcd m n = gcd m (n-m)"; |
|
53 by (subgoal_tac "m<=n ==> !x. cd x m n = cd x m (n-m)" 1); |
|
54 by (Asm_simp_tac 1); |
|
55 by (rtac allI 1); |
|
56 by (etac cd_diff_r 1); |
|
57 qed "gcd_diff_r"; |
|
58 |
|
59 |
|
60 (*** pow ***) |
|
61 |
|
62 Goal "m mod 2 = 0 ==> ((n::nat)*n)^(m div 2) = n^m"; |
|
63 by (asm_simp_tac (simpset() addsimps [power2_eq_square RS sym, |
|
64 power_mult RS sym, mult_div_cancel]) 1); |
|
65 qed "sq_pow_div2"; |
|
66 Addsimps [sq_pow_div2]; |
|