src/HOL/Power.ML
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 9637 47d39a31eb2f
child 11311 5a659c406465
permissions -rw-r--r--
hide many names from Datatype_Universe.
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
qed "le_imp_power_dvd";
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    38
8935
548901d05a0e added type constraint ::nat because 0 is now overloaded
paulson
parents: 8861
diff changeset
    39
Goal "!!i::nat. [| 0 < i; i^m < i^n |] ==> m < n";
3457
a8ab7c64817c Ran expandshort
paulson
parents: 3396
diff changeset
    40
by (rtac ccontr 1);
a8ab7c64817c Ran expandshort
paulson
parents: 3396
diff changeset
    41
by (dtac (leI RS le_imp_power_dvd RS dvd_imp_le RS leD) 1);
a8ab7c64817c Ran expandshort
paulson
parents: 3396
diff changeset
    42
by (etac zero_less_power 1);
3390
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    43
by (contr_tac 1);
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    44
qed "power_less_imp_less";
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    45
6865
5577ffe4c2f1 now div and mod are overloaded; dvd is polymorphic
paulson
parents: 5143
diff changeset
    46
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
    47
by (induct_tac "j" 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3457
diff changeset
    48
by (ALLGOALS (simp_tac (simpset() addsimps [less_Suc_eq])));
3390
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    49
by (stac mult_commute 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3457
diff changeset
    50
by (blast_tac (claset() addSDs [dvd_mult_left]) 1);
3390
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    51
qed_spec_mp "power_less_dvd";
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    52
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    53
3396
aa74c71c3982 eliminated non-ASCII;
wenzelm
parents: 3390
diff changeset
    54
(*** Binomial Coefficients, following Andy Gordon and Florian Kammueller ***)
3390
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    55
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4089
diff changeset
    56
Goal "(n choose 0) = 1";
8442
96023903c2df case_tac now subsumes both boolean and datatype cases;
wenzelm
parents: 8423
diff changeset
    57
by (case_tac "n" 1);
3390
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    58
by (ALLGOALS Asm_simp_tac);
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    59
qed "binomial_n_0";
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    60
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4089
diff changeset
    61
Goal "(0 choose Suc k) = 0";
3390
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    62
by (Simp_tac 1);
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    63
qed "binomial_0_Suc";
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    64
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4089
diff changeset
    65
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
    66
by (Simp_tac 1);
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    67
qed "binomial_Suc_Suc";
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    68
7084
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
    69
Goal "ALL k. n < k --> (n choose k) = 0";
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
    70
by (induct_tac "n" 1);
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
    71
by Auto_tac;
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
    72
by (etac allE 1);
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
    73
by (etac mp 1);
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
    74
by (arith_tac 1);
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
    75
qed_spec_mp "binomial_eq_0";
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
    76
3390
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    77
Addsimps [binomial_n_0, binomial_0_Suc, binomial_Suc_Suc];
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    78
Delsimps [binomial_0, binomial_Suc];
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    79
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4089
diff changeset
    80
Goal "(n choose n) = 1";
3390
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    81
by (induct_tac "n" 1);
7844
6462cb4dfdc2 deleted the redundant less_imp_binomial_eq_0
paulson
parents: 7084
diff changeset
    82
by (ALLGOALS (asm_simp_tac (simpset() addsimps [binomial_eq_0])));
3390
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    83
qed "binomial_n_n";
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    84
Addsimps [binomial_n_n];
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    85
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4089
diff changeset
    86
Goal "(Suc n choose n) = Suc n";
3390
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    87
by (induct_tac "n" 1);
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    88
by (ALLGOALS Asm_simp_tac);
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    89
qed "binomial_Suc_n";
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    90
Addsimps [binomial_Suc_n];
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    91
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4089
diff changeset
    92
Goal "(n choose 1) = n";
3390
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    93
by (induct_tac "n" 1);
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    94
by (ALLGOALS Asm_simp_tac);
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    95
qed "binomial_1";
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    96
Addsimps [binomial_1];
7084
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
    97
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
    98
Goal "k <= n --> 0 < (n choose k)";
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
    99
by (res_inst_tac [("m","n"),("n","k")] diff_induct 1);
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
   100
by (ALLGOALS Asm_simp_tac);
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
   101
qed_spec_mp "zero_less_binomial";
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
   102
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
   103
(*Might be more useful if re-oriented*)
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
   104
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
   105
by (induct_tac "n" 1);
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
   106
by (simp_tac (simpset() addsimps [binomial_0]) 1);
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
   107
by (Clarify_tac 1);
8442
96023903c2df case_tac now subsumes both boolean and datatype cases;
wenzelm
parents: 8423
diff changeset
   108
by (case_tac "k" 1);
7084
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
   109
by (auto_tac (claset(),
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
   110
	      simpset() addsimps [add_mult_distrib, add_mult_distrib2,
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
   111
				  le_Suc_eq, binomial_eq_0]));
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
   112
qed_spec_mp "Suc_times_binomial_eq";
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
   113
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
   114
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
   115
by (asm_simp_tac
9424
234ef8652cae simpset_of NatDef.thy (why anyway?);
wenzelm
parents: 8935
diff changeset
   116
    (simpset_of NatDef.thy addsimps [Suc_times_binomial_eq, 
7084
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
   117
				  div_mult_self_is_m]) 1);
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
   118
qed "binomial_Suc_Suc_eq_times";
4af4f4d8035c new facts about binomials
paulson
parents: 6865
diff changeset
   119