author | haftmann |
Mon, 01 Mar 2010 13:40:23 +0100 | |
changeset 35416 | d8d7d1b785af |
parent 33657 | a4179bf442d1 |
child 38353 | d98baa2cf589 |
permissions | -rw-r--r-- |
1476 | 1 |
(* Title: HOL/Hoare/Arith2.thy |
2 |
Author: Norbert Galm |
|
1335 | 3 |
Copyright 1995 TUM |
4 |
||
3372
6e472c8f0011
Replacement of "divides" by "dvd" from Divides.thy, and updating of proofs
paulson
parents:
1824
diff
changeset
|
5 |
More arithmetic. Much of this duplicates ex/Primes. |
1335 | 6 |
*) |
7 |
||
17278 | 8 |
theory Arith2 |
9 |
imports Main |
|
10 |
begin |
|
1335 | 11 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
33657
diff
changeset
|
12 |
definition "cd" :: "[nat, nat, nat] => bool" where |
3372
6e472c8f0011
Replacement of "divides" by "dvd" from Divides.thy, and updating of proofs
paulson
parents:
1824
diff
changeset
|
13 |
"cd x m n == x dvd m & x dvd n" |
1335 | 14 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
33657
diff
changeset
|
15 |
definition gcd :: "[nat, nat] => nat" where |
1558 | 16 |
"gcd m n == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)" |
1335 | 17 |
|
17278 | 18 |
consts fac :: "nat => nat" |
5183 | 19 |
|
20 |
primrec |
|
21 |
"fac 0 = Suc 0" |
|
22 |
"fac(Suc n) = (Suc n)*fac(n)" |
|
1335 | 23 |
|
19802 | 24 |
|
25 |
subsubsection {* cd *} |
|
26 |
||
27 |
lemma cd_nnn: "0<n ==> cd n n n" |
|
28 |
apply (simp add: cd_def) |
|
29 |
done |
|
30 |
||
31 |
lemma cd_le: "[| cd x m n; 0<m; 0<n |] ==> x<=m & x<=n" |
|
32 |
apply (unfold cd_def) |
|
33 |
apply (blast intro: dvd_imp_le) |
|
34 |
done |
|
35 |
||
36 |
lemma cd_swap: "cd x m n = cd x n m" |
|
37 |
apply (unfold cd_def) |
|
38 |
apply blast |
|
39 |
done |
|
40 |
||
41 |
lemma cd_diff_l: "n<=m ==> cd x m n = cd x (m-n) n" |
|
42 |
apply (unfold cd_def) |
|
30042 | 43 |
apply (fastsimp dest: dvd_diffD) |
19802 | 44 |
done |
45 |
||
46 |
lemma cd_diff_r: "m<=n ==> cd x m n = cd x m (n-m)" |
|
47 |
apply (unfold cd_def) |
|
30042 | 48 |
apply (fastsimp dest: dvd_diffD) |
19802 | 49 |
done |
50 |
||
51 |
||
52 |
subsubsection {* gcd *} |
|
53 |
||
54 |
lemma gcd_nnn: "0<n ==> n = gcd n n" |
|
55 |
apply (unfold gcd_def) |
|
56 |
apply (frule cd_nnn) |
|
57 |
apply (rule some_equality [symmetric]) |
|
58 |
apply (blast dest: cd_le) |
|
33657 | 59 |
apply (blast intro: le_antisym dest: cd_le) |
19802 | 60 |
done |
61 |
||
62 |
lemma gcd_swap: "gcd m n = gcd n m" |
|
63 |
apply (simp add: gcd_def cd_swap) |
|
64 |
done |
|
65 |
||
66 |
lemma gcd_diff_l: "n<=m ==> gcd m n = gcd (m-n) n" |
|
67 |
apply (unfold gcd_def) |
|
68 |
apply (subgoal_tac "n<=m ==> !x. cd x m n = cd x (m-n) n") |
|
69 |
apply simp |
|
70 |
apply (rule allI) |
|
71 |
apply (erule cd_diff_l) |
|
72 |
done |
|
73 |
||
74 |
lemma gcd_diff_r: "m<=n ==> gcd m n = gcd m (n-m)" |
|
75 |
apply (unfold gcd_def) |
|
76 |
apply (subgoal_tac "m<=n ==> !x. cd x m n = cd x m (n-m) ") |
|
77 |
apply simp |
|
78 |
apply (rule allI) |
|
79 |
apply (erule cd_diff_r) |
|
80 |
done |
|
81 |
||
82 |
||
83 |
subsubsection {* pow *} |
|
84 |
||
85 |
lemma sq_pow_div2 [simp]: |
|
86 |
"m mod 2 = 0 ==> ((n::nat)*n)^(m div 2) = n^m" |
|
87 |
apply (simp add: power2_eq_square [symmetric] power_mult [symmetric] mult_div_cancel) |
|
88 |
done |
|
17278 | 89 |
|
1335 | 90 |
end |