src/HOL/ex/Puzzle.ML
author paulson
Wed Nov 05 13:23:46 1997 +0100 (1997-11-05)
changeset 4153 e534c4c32d54
parent 4089 96fba19bcbe2
child 5069 3ea049f7979d
permissions -rw-r--r--
Ran expandshort, especially to introduce Safe_tac
clasohm@1465
     1
(*  Title:      HOL/ex/puzzle.ML
clasohm@969
     2
    ID:         $Id$
clasohm@1465
     3
    Author:     Tobias Nipkow
clasohm@969
     4
    Copyright   1993 TU Muenchen
clasohm@969
     5
clasohm@969
     6
For puzzle.thy.  A question from "Bundeswettbewerb Mathematik"
clasohm@969
     7
clasohm@969
     8
Proof due to Herbert Ehler
clasohm@969
     9
*)
clasohm@969
    10
clasohm@969
    11
(*specialized form of induction needed below*)
wenzelm@3842
    12
val prems = goal Nat.thy "[| P(0); !!n. P(Suc(n)) |] ==> !n. P(n)";
clasohm@969
    13
by (EVERY1 [rtac (nat_induct RS allI), resolve_tac prems, resolve_tac prems]);
clasohm@969
    14
qed "nat_exh";
clasohm@969
    15
clasohm@969
    16
goal Puzzle.thy "! n. k=f(n) --> n <= f(n)";
clasohm@969
    17
by (res_inst_tac [("n","k")] less_induct 1);
clasohm@969
    18
by (rtac nat_exh 1);
clasohm@1266
    19
by (Simp_tac 1);
clasohm@969
    20
by (rtac impI 1);
clasohm@969
    21
by (rtac classical 1);
clasohm@969
    22
by (dtac not_leE 1);
clasohm@969
    23
by (subgoal_tac "f(na) <= f(f(na))" 1);
wenzelm@4089
    24
by (fast_tac (claset() addIs [Puzzle.f_ax]) 2);
paulson@3336
    25
by (rtac Suc_leI 1);
wenzelm@4089
    26
by (fast_tac (claset() delrules [order_refl] 
paulson@2017
    27
                      addIs [Puzzle.f_ax, le_less_trans]) 1);
clasohm@1266
    28
val lemma = result() RS spec RS mp;
clasohm@969
    29
clasohm@969
    30
goal Puzzle.thy "n <= f(n)";
wenzelm@4089
    31
by (fast_tac (claset() addIs [lemma]) 1);
clasohm@969
    32
qed "lemma1";
clasohm@969
    33
clasohm@969
    34
goal Puzzle.thy "f(n) < f(Suc(n))";
wenzelm@4089
    35
by (deepen_tac (claset() addIs [Puzzle.f_ax, le_less_trans, lemma1]) 0 1);
clasohm@969
    36
qed "lemma2";
clasohm@969
    37
wenzelm@3842
    38
val prems = goal Puzzle.thy "(!!n. f(n) <= f(Suc(n))) ==> m<n --> f(m) <= f(n)";
clasohm@969
    39
by (res_inst_tac[("n","n")]nat_induct 1);
clasohm@1266
    40
by (Simp_tac 1);
wenzelm@4089
    41
by (simp_tac (simpset() addsimps [less_Suc_eq]) 1);
wenzelm@4089
    42
by (best_tac (claset() addIs (le_trans::prems)) 1);
paulson@2017
    43
qed_spec_mp "mono_lemma1";
clasohm@969
    44
clasohm@969
    45
val [p1,p2] = goal Puzzle.thy
clasohm@969
    46
    "[| !! n. f(n)<=f(Suc(n));  m<=n |] ==> f(m) <= f(n)";
clasohm@969
    47
by (rtac (p2 RS le_imp_less_or_eq RS disjE) 1);
clasohm@969
    48
by (etac (p1 RS mono_lemma1) 1);
paulson@2017
    49
by (Fast_tac 1);
clasohm@969
    50
qed "mono_lemma";
clasohm@969
    51
clasohm@969
    52
val prems = goal Puzzle.thy "m <= n ==> f(m) <= f(n)";
wenzelm@4089
    53
by (fast_tac (claset() addIs ([mono_lemma,less_imp_le,lemma2]@prems)) 1);
clasohm@969
    54
qed "f_mono";
clasohm@969
    55
clasohm@969
    56
goal Puzzle.thy "f(n) = n";
clasohm@969
    57
by (rtac le_anti_sym 1);
clasohm@969
    58
by (rtac lemma1 2);
wenzelm@4089
    59
by (fast_tac (claset() addIs [Puzzle.f_ax,leI] addDs [leD,f_mono,Suc_leI]) 1);
clasohm@969
    60
result();