author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 9870  2374ba026fc6 
child 12486  0ed8bdd883e0 
permissions  rwrr 
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)"; 
9870  14 
by (induct_thm_tac nat_less_induct "k" 1); 
8018  15 
by (rtac allI 1); 
16 
by (rename_tac "i" 1); 

8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset

17 
by (case_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"; 