author | wenzelm |
Tue, 06 Sep 2005 16:59:53 +0200 | |
changeset 17278 | f27456a2a975 |
parent 14353 | 79f9fbef9106 |
permissions | -rw-r--r-- |
1465 | 1 |
(* Title: HOL/Hoare/Arith2.ML |
1335 | 2 |
ID: $Id$ |
1465 | 3 |
Author: Norbert Galm |
1335 | 4 |
Copyright 1995 TUM |
5 |
||
6 |
More arithmetic lemmas. |
|
7 |
*) |
|
8 |
||
9 |
(*** cd ***) |
|
10 |
||
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
5118
diff
changeset
|
11 |
Goalw [cd_def] "0<n ==> cd n n n"; |
1335 | 12 |
by (Asm_simp_tac 1); |
13 |
qed "cd_nnn"; |
|
14 |
||
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
5118
diff
changeset
|
15 |
Goalw [cd_def] "[| cd x m n; 0<m; 0<n |] ==> x<=m & x<=n"; |
4089 | 16 |
by (blast_tac (claset() addIs [dvd_imp_le]) 1); |
1335 | 17 |
qed "cd_le"; |
18 |
||
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
5118
diff
changeset
|
19 |
Goalw [cd_def] "cd x m n = cd x n m"; |
1875 | 20 |
by (Fast_tac 1); |
1335 | 21 |
qed "cd_swap"; |
22 |
||
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
5118
diff
changeset
|
23 |
Goalw [cd_def] "n<=m ==> cd x m n = cd x (m-n) n"; |
4089 | 24 |
by (blast_tac (claset() addIs [dvd_diff] addDs [dvd_diffD]) 1); |
1335 | 25 |
qed "cd_diff_l"; |
26 |
||
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
5118
diff
changeset
|
27 |
Goalw [cd_def] "m<=n ==> cd x m n = cd x m (n-m)"; |
4089 | 28 |
by (blast_tac (claset() addIs [dvd_diff] addDs [dvd_diffD]) 1); |
1335 | 29 |
qed "cd_diff_r"; |
30 |
||
31 |
||
32 |
(*** gcd ***) |
|
33 |
||
5118 | 34 |
Goalw [gcd_def] "0<n ==> n = gcd n n"; |
7499 | 35 |
by (ftac cd_nnn 1); |
9969 | 36 |
by (rtac (some_equality RS sym) 1); |
4089 | 37 |
by (blast_tac (claset() addDs [cd_le]) 1); |
38 |
by (blast_tac (claset() addIs [le_anti_sym] addDs [cd_le]) 1); |
|
1335 | 39 |
qed "gcd_nnn"; |
40 |
||
17278 | 41 |
val prems = goalw (the_context ()) [gcd_def] "gcd m n = gcd n m"; |
4089 | 42 |
by (simp_tac (simpset() addsimps [cd_swap]) 1); |
1335 | 43 |
qed "gcd_swap"; |
44 |
||
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
5118
diff
changeset
|
45 |
Goalw [gcd_def] "n<=m ==> gcd m n = gcd (m-n) n"; |
3842 | 46 |
by (subgoal_tac "n<=m ==> !x. cd x m n = cd x (m-n) n" 1); |
1335 | 47 |
by (Asm_simp_tac 1); |
2031 | 48 |
by (rtac allI 1); |
49 |
by (etac cd_diff_l 1); |
|
1335 | 50 |
qed "gcd_diff_l"; |
51 |
||
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
5118
diff
changeset
|
52 |
Goalw [gcd_def] "m<=n ==> gcd m n = gcd m (n-m)"; |
3842 | 53 |
by (subgoal_tac "m<=n ==> !x. cd x m n = cd x m (n-m)" 1); |
1335 | 54 |
by (Asm_simp_tac 1); |
2031 | 55 |
by (rtac allI 1); |
56 |
by (etac cd_diff_r 1); |
|
1335 | 57 |
qed "gcd_diff_r"; |
58 |
||
59 |
||
60 |
(*** pow ***) |
|
61 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
62 |
Goal "m mod 2 = 0 ==> ((n::nat)*n)^(m div 2) = n^m"; |
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
11704
diff
changeset
|
63 |
by (asm_simp_tac (simpset() addsimps [power2_eq_square RS sym, |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
11704
diff
changeset
|
64 |
power_mult RS sym, mult_div_cancel]) 1); |
4359 | 65 |
qed "sq_pow_div2"; |
66 |
Addsimps [sq_pow_div2]; |