src/HOL/ex/Puzzle.ML
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 9870 2374ba026fc6
child 12486 0ed8bdd883e0
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: 1266
diff changeset
     1
(*  Title:      HOL/ex/puzzle.ML
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1266
diff changeset
     3
    Author:     Tobias Nipkow
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     4
    Copyright   1993 TU Muenchen
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     5
5456
paulson
parents: 5069
diff changeset
     6
A question from "Bundeswettbewerb Mathematik"
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     7
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     8
Proof due to Herbert Ehler
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     9
*)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    10
5456
paulson
parents: 5069
diff changeset
    11
AddSIs [Puzzle.f_ax];
paulson
parents: 5069
diff changeset
    12
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4089
diff changeset
    13
Goal "! n. k=f(n) --> n <= f(n)";
9870
2374ba026fc6 less_induct -> nat_less_induct
nipkow
parents: 9747
diff changeset
    14
by (induct_thm_tac nat_less_induct "k" 1);
8018
bedd0beabbae Streamlined it a bit.
nipkow
parents: 6676
diff changeset
    15
by (rtac allI 1);
bedd0beabbae Streamlined it a bit.
nipkow
parents: 6676
diff changeset
    16
by (rename_tac "i" 1);
8442
96023903c2df case_tac now subsumes both boolean and datatype cases;
wenzelm
parents: 8423
diff changeset
    17
by (case_tac "i" 1);
8021
9a400ba634b8 A small mod.
nipkow
parents: 8019
diff changeset
    18
 by (Asm_simp_tac 1);
8022
2855e262129c Streamlined it a bit more.
nipkow
parents: 8021
diff changeset
    19
by (blast_tac (claset() addSIs [Suc_leI] addIs [le_less_trans]) 1);
1266
3ae9fe3c0f68 added local simpsets
clasohm
parents: 969
diff changeset
    20
val lemma = result() RS spec RS mp;
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    21
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4089
diff changeset
    22
Goal "n <= f(n)";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3842
diff changeset
    23
by (fast_tac (claset() addIs [lemma]) 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    24
qed "lemma1";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    25
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4089
diff changeset
    26
Goal "f(n) < f(Suc(n))";
5456
paulson
parents: 5069
diff changeset
    27
by (blast_tac (claset() addIs [le_less_trans, lemma1]) 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    28
qed "lemma2";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    29
8018
bedd0beabbae Streamlined it a bit.
nipkow
parents: 6676
diff changeset
    30
Goal "m <= n --> f(m) <= f(n)";
bedd0beabbae Streamlined it a bit.
nipkow
parents: 6676
diff changeset
    31
by (induct_tac "n" 1);
bedd0beabbae Streamlined it a bit.
nipkow
parents: 6676
diff changeset
    32
 by (Simp_tac 1);
bedd0beabbae Streamlined it a bit.
nipkow
parents: 6676
diff changeset
    33
by (rtac impI 1);
bedd0beabbae Streamlined it a bit.
nipkow
parents: 6676
diff changeset
    34
by (etac le_SucE 1);
bedd0beabbae Streamlined it a bit.
nipkow
parents: 6676
diff changeset
    35
 by(cut_inst_tac [("n","n")]lemma2 1);
bedd0beabbae Streamlined it a bit.
nipkow
parents: 6676
diff changeset
    36
 by(arith_tac 1);
bedd0beabbae Streamlined it a bit.
nipkow
parents: 6676
diff changeset
    37
by(Asm_simp_tac 1);
bedd0beabbae Streamlined it a bit.
nipkow
parents: 6676
diff changeset
    38
qed_spec_mp "f_mono";
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    39
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4089
diff changeset
    40
Goal "f(n) = n";
6676
62d1e642da30 preferring generic rules to specific ones...
paulson
parents: 5618
diff changeset
    41
by (rtac order_antisym 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    42
by (rtac lemma1 2);
8018
bedd0beabbae Streamlined it a bit.
nipkow
parents: 6676
diff changeset
    43
by (fast_tac (claset() addIs [leI] addDs [leD,f_mono,Suc_leI]) 1);
bedd0beabbae Streamlined it a bit.
nipkow
parents: 6676
diff changeset
    44
qed "f_id";