author | oheimb |
Wed, 12 Nov 1997 12:34:43 +0100 | |
changeset 4206 | 688050e83d89 |
parent 4089 | 96fba19bcbe2 |
child 4359 | 6f2986464280 |
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 |
open Arith2; |
|
10 |
||
11 |
||
12 |
(*** HOL lemmas ***) |
|
13 |
||
14 |
||
15 |
val [prem1,prem2]=goal HOL.thy "[|~P ==> ~Q; Q|] ==> P"; |
|
16 |
by (cut_facts_tac [prem1 COMP impI,prem2] 1); |
|
1875 | 17 |
by (Fast_tac 1); |
1335 | 18 |
val not_imp_swap=result(); |
19 |
||
20 |
||
21 |
||
22 |
(*** cd ***) |
|
23 |
||
24 |
||
25 |
val prems=goalw thy [cd_def] "0<n ==> cd n n n"; |
|
26 |
by (cut_facts_tac prems 1); |
|
27 |
by (Asm_simp_tac 1); |
|
28 |
qed "cd_nnn"; |
|
29 |
||
3372
6e472c8f0011
Replacement of "divides" by "dvd" from Divides.thy, and updating of proofs
paulson
parents:
3343
diff
changeset
|
30 |
val prems=goalw thy [cd_def] "[| cd x m n; 0<m; 0<n |] ==> x<=m & x<=n"; |
1335 | 31 |
by (cut_facts_tac prems 1); |
4089 | 32 |
by (blast_tac (claset() addIs [dvd_imp_le]) 1); |
1335 | 33 |
qed "cd_le"; |
34 |
||
35 |
val prems=goalw thy [cd_def] "cd x m n = cd x n m"; |
|
1875 | 36 |
by (Fast_tac 1); |
1335 | 37 |
qed "cd_swap"; |
38 |
||
3372
6e472c8f0011
Replacement of "divides" by "dvd" from Divides.thy, and updating of proofs
paulson
parents:
3343
diff
changeset
|
39 |
val prems=goalw thy [cd_def] "n<=m ==> cd x m n = cd x (m-n) n"; |
1335 | 40 |
by (cut_facts_tac prems 1); |
4089 | 41 |
by (blast_tac (claset() addIs [dvd_diff] addDs [dvd_diffD]) 1); |
1335 | 42 |
qed "cd_diff_l"; |
43 |
||
3372
6e472c8f0011
Replacement of "divides" by "dvd" from Divides.thy, and updating of proofs
paulson
parents:
3343
diff
changeset
|
44 |
val prems=goalw thy [cd_def] "m<=n ==> cd x m n = cd x m (n-m)"; |
1335 | 45 |
by (cut_facts_tac prems 1); |
4089 | 46 |
by (blast_tac (claset() addIs [dvd_diff] addDs [dvd_diffD]) 1); |
1335 | 47 |
qed "cd_diff_r"; |
48 |
||
49 |
||
50 |
(*** gcd ***) |
|
51 |
||
3372
6e472c8f0011
Replacement of "divides" by "dvd" from Divides.thy, and updating of proofs
paulson
parents:
3343
diff
changeset
|
52 |
goalw thy [gcd_def] "!!n. 0<n ==> n = gcd n n"; |
6e472c8f0011
Replacement of "divides" by "dvd" from Divides.thy, and updating of proofs
paulson
parents:
3343
diff
changeset
|
53 |
by (forward_tac [cd_nnn] 1); |
2031 | 54 |
by (rtac (select_equality RS sym) 1); |
4089 | 55 |
by (blast_tac (claset() addDs [cd_le]) 1); |
56 |
by (blast_tac (claset() addIs [le_anti_sym] addDs [cd_le]) 1); |
|
1335 | 57 |
qed "gcd_nnn"; |
58 |
||
59 |
val prems = goalw thy [gcd_def] "gcd m n = gcd n m"; |
|
4089 | 60 |
by (simp_tac (simpset() addsimps [cd_swap]) 1); |
1335 | 61 |
qed "gcd_swap"; |
62 |
||
3372
6e472c8f0011
Replacement of "divides" by "dvd" from Divides.thy, and updating of proofs
paulson
parents:
3343
diff
changeset
|
63 |
val prems=goalw thy [gcd_def] "n<=m ==> gcd m n = gcd (m-n) n"; |
1335 | 64 |
by (cut_facts_tac prems 1); |
3842 | 65 |
by (subgoal_tac "n<=m ==> !x. cd x m n = cd x (m-n) n" 1); |
1335 | 66 |
by (Asm_simp_tac 1); |
2031 | 67 |
by (rtac allI 1); |
68 |
by (etac cd_diff_l 1); |
|
1335 | 69 |
qed "gcd_diff_l"; |
70 |
||
3372
6e472c8f0011
Replacement of "divides" by "dvd" from Divides.thy, and updating of proofs
paulson
parents:
3343
diff
changeset
|
71 |
val prems=goalw thy [gcd_def] "m<=n ==> gcd m n = gcd m (n-m)"; |
1335 | 72 |
by (cut_facts_tac prems 1); |
3842 | 73 |
by (subgoal_tac "m<=n ==> !x. cd x m n = cd x m (n-m)" 1); |
1335 | 74 |
by (Asm_simp_tac 1); |
2031 | 75 |
by (rtac allI 1); |
76 |
by (etac cd_diff_r 1); |
|
1335 | 77 |
qed "gcd_diff_r"; |
78 |
||
79 |
||
80 |
(*** pow ***) |
|
81 |
||
82 |
val [pow_0,pow_Suc] = nat_recs pow_def; |
|
83 |
store_thm("pow_0",pow_0); |
|
84 |
store_thm("pow_Suc",pow_Suc); |
|
85 |
||
86 |
goalw thy [pow_def] "m pow (n+k) = m pow n * m pow k"; |
|
87 |
by (nat_ind_tac "k" 1); |
|
4089 | 88 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [mult_left_commute]))); |
1335 | 89 |
qed "pow_add_reduce"; |
90 |
||
91 |
goalw thy [pow_def] "m pow n pow k = m pow (n*k)"; |
|
92 |
by (nat_ind_tac "k" 1); |
|
93 |
by (ALLGOALS Asm_simp_tac); |
|
94 |
by (fold_goals_tac [pow_def]); |
|
2031 | 95 |
by (rtac (pow_add_reduce RS sym) 1); |
1335 | 96 |
qed "pow_pow_reduce"; |
97 |
||
98 |
(*** fac ***) |
|
99 |
||
100 |
Addsimps(nat_recs fac_def); |