src/HOL/Power.ML
author berghofe
Tue, 30 May 2000 18:02:49 +0200
changeset 9001 93af64f54bf2
parent 8935 548901d05a0e
child 9424 234ef8652cae
permissions -rw-r--r--
the is now defined using primrec, avoiding explicit use of arbitrary.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3390
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
     1
(*  Title:      HOL/Power.ML
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
     2
    ID:         $Id$
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
     4
    Copyright   1997  University of Cambridge
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
     5
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
     6
The (overloaded) exponentiation operator, ^ :: [nat,nat]=>nat
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
     7
Also binomial coefficents
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
     8
*)
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
     9
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    10
(*** Simple laws about Power ***)
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    11
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4089
diff changeset
    12
Goal "!!i::nat. i ^ (j+k) = (i^j) * (i^k)";
3390
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    13
by (induct_tac "k" 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3457
diff changeset
    14
by (ALLGOALS (asm_simp_tac (simpset() addsimps mult_ac)));
3390
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    15
qed "power_add";
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    16
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4089
diff changeset
    17
Goal "!!i::nat. i ^ (j*k) = (i^j) ^ k";
3390
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    18
by (induct_tac "k" 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3457
diff changeset
    19
by (ALLGOALS (asm_simp_tac (simpset() addsimps [power_add])));
3390
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    20
qed "power_mult";
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    21
8935
548901d05a0e added type constraint ::nat because 0 is now overloaded
paulson
parents: 8861
diff changeset
    22
Goal "!!i::nat. 0 < i ==> 0 < i^n";
3390
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    23
by (induct_tac "n" 1);
8935
548901d05a0e added type constraint ::nat because 0 is now overloaded
paulson
parents: 8861
diff changeset
    24
by (ALLGOALS Asm_simp_tac);
3390
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    25
qed "zero_less_power";
8861
8341f24e09b5 new theorem one_le_power
paulson
parents: 8442
diff changeset
    26
Addsimps [zero_less_power];
8341f24e09b5 new theorem one_le_power
paulson
parents: 8442
diff changeset
    27
8341f24e09b5 new theorem one_le_power
paulson
parents: 8442
diff changeset
    28
Goal "!!i::nat. 1 <= i ==> 1 <= i^n";
8341f24e09b5 new theorem one_le_power
paulson
parents: 8442
diff changeset
    29
by (induct_tac "n" 1);
8341f24e09b5 new theorem one_le_power
paulson
parents: 8442
diff changeset
    30
by Auto_tac;
8341f24e09b5 new theorem one_le_power
paulson
parents: 8442
diff changeset
    31
qed "one_le_power";
8341f24e09b5 new theorem one_le_power
paulson
parents: 8442
diff changeset
    32
Addsimps [one_le_power];
3390
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    33
8935
548901d05a0e added type constraint ::nat because 0 is now overloaded
paulson
parents: 8861
diff changeset
    34
Goalw [dvd_def] "!!i::nat. m<=n ==> i^m dvd i^n";
3457
a8ab7c64817c Ran expandshort
paulson
parents: 3396
diff changeset
    35
by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3457
diff changeset
    36
by (asm_simp_tac (simpset() addsimps [power_add]) 1);
3390
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    37
by (Blast_tac 1);
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    38
qed "le_imp_power_dvd";
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    39
8935
548901d05a0e added type constraint ::nat because 0 is now overloaded
paulson
parents: 8861
diff changeset
    40
Goal "!!i::nat. [| 0 < i; i^m < i^n |] ==> m < n";
3457
a8ab7c64817c Ran expandshort
paulson
parents: 3396
diff changeset
    41
by (rtac ccontr 1);
a8ab7c64817c Ran expandshort
paulson
parents: 3396
diff changeset
    42
by (dtac (leI RS le_imp_power_dvd RS dvd_imp_le RS leD) 1);
a8ab7c64817c Ran expandshort
paulson
parents: 3396
diff changeset
    43
by (etac zero_less_power 1);
3390
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    44
by (contr_tac 1);
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    45
qed "power_less_imp_less";
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    46
6865
5577ffe4c2f1 now div and mod are overloaded; dvd is polymorphic
paulson
parents: 5143
diff changeset
    47
Goal "k^j dvd n --> i<j --> k^i dvd (n::nat)";
3390
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    48
by (induct_tac "j" 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3457
diff changeset
    49
by (ALLGOALS (simp_tac (simpset() addsimps [less_Suc_eq])));
3390
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    50
by (stac mult_commute 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3457
diff changeset
    51
by (blast_tac (claset() addSDs [dvd_mult_left]) 1);
3390
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    52
qed_spec_mp "power_less_dvd";
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    53
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    54
3396
aa74c71c3982 eliminated non-ASCII;
wenzelm
parents: 3390
diff changeset
    55
(*** Binomial Coefficients, following Andy Gordon and Florian Kammueller ***)
3390
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    56
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4089
diff changeset
    57
Goal "(n choose 0) = 1";
8442
96023903c2df case_tac now subsumes both boolean and datatype cases;
wenzelm
parents: 8423
diff changeset
    58
by (case_tac "n" 1);
3390
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    59
by (ALLGOALS Asm_simp_tac);
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    60
qed "binomial_n_0";
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    61
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4089
diff changeset
    62
Goal "(0 choose Suc k) = 0";
3390
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    63
by (Simp_tac 1);
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    64
qed "binomial_0_Suc";
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    65
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4089
diff changeset
    66
Goal "(Suc n choose Suc k) = (n choose k) + (n choose Suc k)";
3390
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    67
by (Simp_tac 1);
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    68
qed "binomial_Suc_Suc";
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    69
7084
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
    70
Goal "ALL k. n < k --> (n choose k) = 0";
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
    71
by (induct_tac "n" 1);
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
    72
by Auto_tac;
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
    73
by (etac allE 1);
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
    74
by (etac mp 1);
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
    75
by (arith_tac 1);
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
    76
qed_spec_mp "binomial_eq_0";
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
    77
3390
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    78
Addsimps [binomial_n_0, binomial_0_Suc, binomial_Suc_Suc];
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    79
Delsimps [binomial_0, binomial_Suc];
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    80
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4089
diff changeset
    81
Goal "(n choose n) = 1";
3390
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    82
by (induct_tac "n" 1);
7844
6462cb4dfdc2 deleted the redundant less_imp_binomial_eq_0
paulson
parents: 7084
diff changeset
    83
by (ALLGOALS (asm_simp_tac (simpset() addsimps [binomial_eq_0])));
3390
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    84
qed "binomial_n_n";
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    85
Addsimps [binomial_n_n];
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    86
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4089
diff changeset
    87
Goal "(Suc n choose n) = Suc n";
3390
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    88
by (induct_tac "n" 1);
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    89
by (ALLGOALS Asm_simp_tac);
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    90
qed "binomial_Suc_n";
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    91
Addsimps [binomial_Suc_n];
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    92
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4089
diff changeset
    93
Goal "(n choose 1) = n";
3390
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    94
by (induct_tac "n" 1);
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    95
by (ALLGOALS Asm_simp_tac);
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    96
qed "binomial_1";
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    97
Addsimps [binomial_1];
7084
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
    98
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
    99
Goal "k <= n --> 0 < (n choose k)";
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
   100
by (res_inst_tac [("m","n"),("n","k")] diff_induct 1);
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
   101
by (ALLGOALS Asm_simp_tac);
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
   102
qed_spec_mp "zero_less_binomial";
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
   103
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
   104
(*Might be more useful if re-oriented*)
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
   105
Goal "ALL k. k <= n --> Suc n * (n choose k) = (Suc n choose Suc k) * Suc k";
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
   106
by (induct_tac "n" 1);
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
   107
by (simp_tac (simpset() addsimps [binomial_0]) 1);
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
   108
by (Clarify_tac 1);
8442
96023903c2df case_tac now subsumes both boolean and datatype cases;
wenzelm
parents: 8423
diff changeset
   109
by (case_tac "k" 1);
7084
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
   110
by (auto_tac (claset(),
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
   111
	      simpset() addsimps [add_mult_distrib, add_mult_distrib2,
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
   112
				  le_Suc_eq, binomial_eq_0]));
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
   113
qed_spec_mp "Suc_times_binomial_eq";
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
   114
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
   115
Goal "k <= n ==> (Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k";
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
   116
by (asm_simp_tac
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
   117
    (simpset_of Nat.thy addsimps [Suc_times_binomial_eq, 
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
   118
				  div_mult_self_is_m]) 1);
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
   119
qed "binomial_Suc_Suc_eq_times";
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
   120