1465

1 
(* Title: HOL/ex/puzzle.ML

969

2 
ID: $Id$

1465

3 
Author: Tobias Nipkow

969

4 
Copyright 1993 TU Muenchen


5 

5456

6 
A question from "Bundeswettbewerb Mathematik"

969

7 


8 
Proof due to Herbert Ehler


9 
*)


10 

5456

11 
AddSIs [Puzzle.f_ax];


12 

5069

13 
Goal "! n. k=f(n) > n <= f(n)";

969

14 
by (res_inst_tac [("n","k")] less_induct 1);

8018

15 
by (rtac allI 1);


16 
by (rename_tac "i" 1);


17 
by (exhaust_tac "i" 1);

8019

18 
by Auto_tac;

8018

19 
by (subgoal_tac "f(nat) <= f(f(nat))" 1);


20 
by (Blast_tac 2);

8019

21 
by (blast_tac (claset() addIs [Suc_leI,le_less_trans]) 1);

1266

22 
val lemma = result() RS spec RS mp;

969

23 

5069

24 
Goal "n <= f(n)";

4089

25 
by (fast_tac (claset() addIs [lemma]) 1);

969

26 
qed "lemma1";


27 

5069

28 
Goal "f(n) < f(Suc(n))";

5456

29 
by (blast_tac (claset() addIs [le_less_trans, lemma1]) 1);

969

30 
qed "lemma2";


31 

8018

32 
Goal "m <= n > f(m) <= f(n)";


33 
by (induct_tac "n" 1);


34 
by (Simp_tac 1);


35 
by (rtac impI 1);


36 
by (etac le_SucE 1);


37 
by(cut_inst_tac [("n","n")]lemma2 1);


38 
by(arith_tac 1);


39 
by(Asm_simp_tac 1);


40 
qed_spec_mp "f_mono";

969

41 

5069

42 
Goal "f(n) = n";

6676

43 
by (rtac order_antisym 1);

969

44 
by (rtac lemma1 2);

8018

45 
by (fast_tac (claset() addIs [leI] addDs [leD,f_mono,Suc_leI]) 1);


46 
qed "f_id";
