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);

8423

17 
by (cases_tac "i" 1);

8021

18 
by (Asm_simp_tac 1);

8022

19 
by (blast_tac (claset() addSIs [Suc_leI] addIs [le_less_trans]) 1);

1266

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

969

21 

5069

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

4089

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

969

24 
qed "lemma1";


25 

5069

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

5456

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

969

28 
qed "lemma2";


29 

8018

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


31 
by (induct_tac "n" 1);


32 
by (Simp_tac 1);


33 
by (rtac impI 1);


34 
by (etac le_SucE 1);


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


36 
by(arith_tac 1);


37 
by(Asm_simp_tac 1);


38 
qed_spec_mp "f_mono";

969

39 

5069

40 
Goal "f(n) = n";

6676

41 
by (rtac order_antisym 1);

969

42 
by (rtac lemma1 2);

8018

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


44 
qed "f_id";
