author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 9969  4753185f1dd2 
child 11701  3d51fbf81c17 
permissions  rwrr 
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 
(*** cd ***) 

13 

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] "0<n ==> cd n n n"; 
1335  16 
by (Asm_simp_tac 1); 
17 
qed "cd_nnn"; 

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; 0<m; 0<n ] ==> x<=m & x<=n"; 
4089  20 
by (blast_tac (claset() addIs [dvd_imp_le]) 1); 
1335  21 
qed "cd_le"; 
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] "cd x m n = cd x n m"; 
1875  24 
by (Fast_tac 1); 
1335  25 
qed "cd_swap"; 
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] "n<=m ==> cd x m n = cd x (mn) n"; 
4089  28 
by (blast_tac (claset() addIs [dvd_diff] addDs [dvd_diffD]) 1); 
1335  29 
qed "cd_diff_l"; 
30 

7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
5118
diff
changeset

31 
Goalw [cd_def] "m<=n ==> cd x m n = cd x m (nm)"; 
4089  32 
by (blast_tac (claset() addIs [dvd_diff] addDs [dvd_diffD]) 1); 
1335  33 
qed "cd_diff_r"; 
34 

35 

36 
(*** gcd ***) 

37 

5118  38 
Goalw [gcd_def] "0<n ==> n = gcd n n"; 
7499  39 
by (ftac cd_nnn 1); 
9969  40 
by (rtac (some_equality RS sym) 1); 
4089  41 
by (blast_tac (claset() addDs [cd_le]) 1); 
42 
by (blast_tac (claset() addIs [le_anti_sym] addDs [cd_le]) 1); 

1335  43 
qed "gcd_nnn"; 
44 

45 
val prems = goalw thy [gcd_def] "gcd m n = gcd n m"; 

4089  46 
by (simp_tac (simpset() addsimps [cd_swap]) 1); 
1335  47 
qed "gcd_swap"; 
48 

7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
5118
diff
changeset

49 
Goalw [gcd_def] "n<=m ==> gcd m n = gcd (mn) n"; 
3842  50 
by (subgoal_tac "n<=m ==> !x. cd x m n = cd x (mn) n" 1); 
1335  51 
by (Asm_simp_tac 1); 
2031  52 
by (rtac allI 1); 
53 
by (etac cd_diff_l 1); 

1335  54 
qed "gcd_diff_l"; 
55 

7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
5118
diff
changeset

56 
Goalw [gcd_def] "m<=n ==> gcd m n = gcd m (nm)"; 
3842  57 
by (subgoal_tac "m<=n ==> !x. cd x m n = cd x m (nm)" 1); 
1335  58 
by (Asm_simp_tac 1); 
2031  59 
by (rtac allI 1); 
60 
by (etac cd_diff_r 1); 

1335  61 
qed "gcd_diff_r"; 
62 

63 

64 
(*** pow ***) 

65 

8791  66 
Goal "m mod #2 = 0 ==> ((n::nat)*n)^(m div #2) = n^m"; 
67 
by (asm_simp_tac (simpset() addsimps [power_two RS sym, power_mult RS sym, 

68 
mult_div_cancel]) 1); 

4359  69 
qed "sq_pow_div2"; 
70 
Addsimps [sq_pow_div2]; 