src/HOL/ex/Puzzle.ML
author paulson
Fri, 21 May 1999 10:56:46 +0200
changeset 6676 62d1e642da30
parent 5618 721671c68324
child 8018 bedd0beabbae
permissions -rw-r--r--
preferring generic rules to specific ones...
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
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    13
(*specialized form of induction needed below*)
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3336
diff changeset
    14
val prems = goal Nat.thy "[| P(0); !!n. P(Suc(n)) |] ==> !n. P(n)";
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    15
by (EVERY1 [rtac (nat_induct RS allI), resolve_tac prems, resolve_tac prems]);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    16
qed "nat_exh";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    17
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4089
diff changeset
    18
Goal "! n. k=f(n) --> n <= f(n)";
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    19
by (res_inst_tac [("n","k")] less_induct 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    20
by (rtac nat_exh 1);
1266
3ae9fe3c0f68 added local simpsets
clasohm
parents: 969
diff changeset
    21
by (Simp_tac 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    22
by (rtac impI 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    23
by (rtac classical 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    24
by (dtac not_leE 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    25
by (subgoal_tac "f(na) <= f(f(na))" 1);
5456
paulson
parents: 5069
diff changeset
    26
by (Blast_tac 2);
3336
29ddef80bd49 Renamed lessD to Suc_leI
paulson
parents: 2609
diff changeset
    27
by (rtac Suc_leI 1);
5456
paulson
parents: 5069
diff changeset
    28
by (blast_tac (claset() addSDs [spec] addIs [le_less_trans]) 1);
1266
3ae9fe3c0f68 added local simpsets
clasohm
parents: 969
diff changeset
    29
val lemma = result() RS spec RS mp;
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    30
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4089
diff changeset
    31
Goal "n <= f(n)";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3842
diff changeset
    32
by (fast_tac (claset() addIs [lemma]) 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    33
qed "lemma1";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    34
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4089
diff changeset
    35
Goal "f(n) < f(Suc(n))";
5456
paulson
parents: 5069
diff changeset
    36
by (blast_tac (claset() addIs [le_less_trans, lemma1]) 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    37
qed "lemma2";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    38
5456
paulson
parents: 5069
diff changeset
    39
val prems = Goal "(!!n. f(n) <= f(Suc(n))) ==> m<n --> f(m) <= f(n)";
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    40
by (res_inst_tac[("n","n")]nat_induct 1);
1266
3ae9fe3c0f68 added local simpsets
clasohm
parents: 969
diff changeset
    41
by (Simp_tac 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3842
diff changeset
    42
by (simp_tac (simpset() addsimps [less_Suc_eq]) 1);
5479
5a5dfb0f0d7d fixed PROOF FAILED
paulson
parents: 5456
diff changeset
    43
by (blast_tac (claset() addIs (le_trans::prems)) 1);
2017
dd3e2a91aeca Proofs made more robust to work in presence of le_refl
paulson
parents: 1820
diff changeset
    44
qed_spec_mp "mono_lemma1";
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    45
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    46
val [p1,p2] = goal Puzzle.thy
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    47
    "[| !! n. f(n)<=f(Suc(n));  m<=n |] ==> f(m) <= f(n)";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    48
by (rtac (p2 RS le_imp_less_or_eq RS disjE) 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    49
by (etac (p1 RS mono_lemma1) 1);
2017
dd3e2a91aeca Proofs made more robust to work in presence of le_refl
paulson
parents: 1820
diff changeset
    50
by (Fast_tac 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    51
qed "mono_lemma";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    52
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    53
val prems = goal Puzzle.thy "m <= n ==> f(m) <= f(n)";
5618
paulson
parents: 5479
diff changeset
    54
by (fast_tac (claset() addIs [mono_lemma,less_imp_le,lemma2]@prems) 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    55
qed "f_mono";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    56
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4089
diff changeset
    57
Goal "f(n) = n";
6676
62d1e642da30 preferring generic rules to specific ones...
paulson
parents: 5618
diff changeset
    58
by (rtac order_antisym 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    59
by (rtac lemma1 2);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3842
diff changeset
    60
by (fast_tac (claset() addIs [Puzzle.f_ax,leI] addDs [leD,f_mono,Suc_leI]) 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    61
result();