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