src/HOL/ex/Puzzle.ML
author nipkow
Mon, 15 Nov 1999 09:41:06 +0100
changeset 8018 bedd0beabbae
parent 6676 62d1e642da30
child 8019 fead0dbf5b0a
permissions -rw-r--r--
Streamlined it a bit.
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)";
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    14
by (res_inst_tac [("n","k")] less_induct 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);
bedd0beabbae Streamlined it a bit.
nipkow
parents: 6676
diff changeset
    17
by (exhaust_tac "i" 1);
bedd0beabbae Streamlined it a bit.
nipkow
parents: 6676
diff changeset
    18
 by (Asm_simp_tac 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    19
by (rtac impI 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    20
by (rtac classical 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    21
by (dtac not_leE 1);
8018
bedd0beabbae Streamlined it a bit.
nipkow
parents: 6676
diff changeset
    22
by (subgoal_tac "f(nat) <= f(f(nat))" 1);
bedd0beabbae Streamlined it a bit.
nipkow
parents: 6676
diff changeset
    23
 by (Blast_tac 2);
bedd0beabbae Streamlined it a bit.
nipkow
parents: 6676
diff changeset
    24
by (blast_tac (claset() addSDs [spec] addIs [Suc_leI,le_less_trans]) 1);
1266
3ae9fe3c0f68 added local simpsets
clasohm
parents: 969
diff changeset
    25
val lemma = result() RS spec RS mp;
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    26
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4089
diff changeset
    27
Goal "n <= f(n)";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3842
diff changeset
    28
by (fast_tac (claset() addIs [lemma]) 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    29
qed "lemma1";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    30
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4089
diff changeset
    31
Goal "f(n) < f(Suc(n))";
5456
paulson
parents: 5069
diff changeset
    32
by (blast_tac (claset() addIs [le_less_trans, lemma1]) 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    33
qed "lemma2";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    34
8018
bedd0beabbae Streamlined it a bit.
nipkow
parents: 6676
diff changeset
    35
Goal "m <= n --> f(m) <= f(n)";
bedd0beabbae Streamlined it a bit.
nipkow
parents: 6676
diff changeset
    36
by (induct_tac "n" 1);
bedd0beabbae Streamlined it a bit.
nipkow
parents: 6676
diff changeset
    37
 by (Simp_tac 1);
bedd0beabbae Streamlined it a bit.
nipkow
parents: 6676
diff changeset
    38
by (rtac impI 1);
bedd0beabbae Streamlined it a bit.
nipkow
parents: 6676
diff changeset
    39
by (etac le_SucE 1);
bedd0beabbae Streamlined it a bit.
nipkow
parents: 6676
diff changeset
    40
 by(cut_inst_tac [("n","n")]lemma2 1);
bedd0beabbae Streamlined it a bit.
nipkow
parents: 6676
diff changeset
    41
 by(arith_tac 1);
bedd0beabbae Streamlined it a bit.
nipkow
parents: 6676
diff changeset
    42
by(Asm_simp_tac 1);
bedd0beabbae Streamlined it a bit.
nipkow
parents: 6676
diff changeset
    43
qed_spec_mp "f_mono";
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    44
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4089
diff changeset
    45
Goal "f(n) = n";
6676
62d1e642da30 preferring generic rules to specific ones...
paulson
parents: 5618
diff changeset
    46
by (rtac order_antisym 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    47
by (rtac lemma1 2);
8018
bedd0beabbae Streamlined it a bit.
nipkow
parents: 6676
diff changeset
    48
by (fast_tac (claset() addIs [leI] addDs [leD,f_mono,Suc_leI]) 1);
bedd0beabbae Streamlined it a bit.
nipkow
parents: 6676
diff changeset
    49
qed "f_id";