src/HOL/Hoare/Arith2.ML
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 9969 4753185f1dd2
child 11701 3d51fbf81c17
permissions -rw-r--r--
hide many names from Datatype_Universe.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
     1
(*  Title:      HOL/Hoare/Arith2.ML
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     2
    ID:         $Id$
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
     3
    Author:     Norbert Galm
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     4
    Copyright   1995 TUM
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     5
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     6
More arithmetic lemmas.
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     7
*)
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     8
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     9
open Arith2;
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    10
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    11
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    12
(*** cd ***)
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    13
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    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
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    16
by (Asm_simp_tac 1);
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    17
qed "cd_nnn";
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    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
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3842
diff changeset
    20
by (blast_tac (claset() addIs [dvd_imp_le]) 1);
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    21
qed "cd_le";
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    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
54c0462f8fb2 Classical tactics now use default claset.
berghofe
parents: 1714
diff changeset
    24
by (Fast_tac 1);
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    25
qed "cd_swap";
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    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 (m-n) n";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3842
diff changeset
    28
by (blast_tac (claset() addIs [dvd_diff] addDs [dvd_diffD]) 1);
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    29
qed "cd_diff_l";
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    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 (n-m)";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3842
diff changeset
    32
by (blast_tac (claset() addIs [dvd_diff] addDs [dvd_diffD]) 1);
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    33
qed "cd_diff_r";
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    34
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    35
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    36
(*** gcd ***)
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    37
5118
6b995dad8a9d Removed leading !! in goals.
nipkow
parents: 5069
diff changeset
    38
Goalw [gcd_def] "0<n ==> n = gcd n n";
7499
23e090051cb8 isatool expandshort;
wenzelm
parents: 7127
diff changeset
    39
by (ftac cd_nnn 1);
9969
4753185f1dd2 renamed (most of...) the select rules
paulson
parents: 8791
diff changeset
    40
by (rtac (some_equality RS sym) 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3842
diff changeset
    41
by (blast_tac (claset() addDs [cd_le]) 1);
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3842
diff changeset
    42
by (blast_tac (claset() addIs [le_anti_sym] addDs [cd_le]) 1);
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    43
qed "gcd_nnn";
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    44
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    45
val prems = goalw thy [gcd_def] "gcd m n = gcd n m";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3842
diff changeset
    46
by (simp_tac (simpset() addsimps [cd_swap]) 1);
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    47
qed "gcd_swap";
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    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 (m-n) n";
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3372
diff changeset
    50
by (subgoal_tac "n<=m ==> !x. cd x m n = cd x (m-n) n" 1);
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    51
by (Asm_simp_tac 1);
2031
03a843f0f447 Ran expandshort
paulson
parents: 1875
diff changeset
    52
by (rtac allI 1);
03a843f0f447 Ran expandshort
paulson
parents: 1875
diff changeset
    53
by (etac cd_diff_l 1);
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    54
qed "gcd_diff_l";
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    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 (n-m)";
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3372
diff changeset
    57
by (subgoal_tac "m<=n ==> !x. cd x m n = cd x m (n-m)" 1);
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    58
by (Asm_simp_tac 1);
2031
03a843f0f447 Ran expandshort
paulson
parents: 1875
diff changeset
    59
by (rtac allI 1);
03a843f0f447 Ran expandshort
paulson
parents: 1875
diff changeset
    60
by (etac cd_diff_r 1);
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    61
qed "gcd_diff_r";
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    62
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    63
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    64
(*** pow ***)
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    65
8791
50b650d19641 changed 2 to #2
paulson
parents: 7499
diff changeset
    66
Goal "m mod #2 = 0 ==> ((n::nat)*n)^(m div #2) = n^m";
50b650d19641 changed 2 to #2
paulson
parents: 7499
diff changeset
    67
by (asm_simp_tac (simpset() addsimps [power_two RS sym, power_mult RS sym,
50b650d19641 changed 2 to #2
paulson
parents: 7499
diff changeset
    68
				      mult_div_cancel]) 1);
4359
6f2986464280 Simplified proofs.
nipkow
parents: 4089
diff changeset
    69
qed "sq_pow_div2";
6f2986464280 Simplified proofs.
nipkow
parents: 4089
diff changeset
    70
Addsimps [sq_pow_div2];