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


18 
by (Asm_simp_tac 1);

969

19 
by (rtac impI 1);


20 
by (rtac classical 1);


21 
by (dtac not_leE 1);

8018

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


23 
by (Blast_tac 2);


24 
by (blast_tac (claset() addSDs [spec] addIs [Suc_leI,le_less_trans]) 1);

1266

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

969

26 

5069

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

4089

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

969

29 
qed "lemma1";


30 

5069

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

5456

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

969

33 
qed "lemma2";


34 

8018

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


36 
by (induct_tac "n" 1);


37 
by (Simp_tac 1);


38 
by (rtac impI 1);


39 
by (etac le_SucE 1);


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


41 
by(arith_tac 1);


42 
by(Asm_simp_tac 1);


43 
qed_spec_mp "f_mono";

969

44 

5069

45 
Goal "f(n) = n";

6676

46 
by (rtac order_antisym 1);

969

47 
by (rtac lemma1 2);

8018

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


49 
qed "f_id";
