author  paulson 
Fri, 21 May 1999 10:56:46 +0200  
changeset 6676  62d1e642da30 
parent 5618  721671c68324 
child 8018  bedd0beabbae 
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 

969  13 
(*specialized form of induction needed below*) 
3842  14 
val prems = goal Nat.thy "[ P(0); !!n. P(Suc(n)) ] ==> !n. P(n)"; 
969  15 
by (EVERY1 [rtac (nat_induct RS allI), resolve_tac prems, resolve_tac prems]); 
16 
qed "nat_exh"; 

17 

5069  18 
Goal "! n. k=f(n) > n <= f(n)"; 
969  19 
by (res_inst_tac [("n","k")] less_induct 1); 
20 
by (rtac nat_exh 1); 

1266  21 
by (Simp_tac 1); 
969  22 
by (rtac impI 1); 
23 
by (rtac classical 1); 

24 
by (dtac not_leE 1); 

25 
by (subgoal_tac "f(na) <= f(f(na))" 1); 

5456  26 
by (Blast_tac 2); 
3336  27 
by (rtac Suc_leI 1); 
5456  28 
by (blast_tac (claset() addSDs [spec] addIs [le_less_trans]) 1); 
1266  29 
val lemma = result() RS spec RS mp; 
969  30 

5069  31 
Goal "n <= f(n)"; 
4089  32 
by (fast_tac (claset() addIs [lemma]) 1); 
969  33 
qed "lemma1"; 
34 

5069  35 
Goal "f(n) < f(Suc(n))"; 
5456  36 
by (blast_tac (claset() addIs [le_less_trans, lemma1]) 1); 
969  37 
qed "lemma2"; 
38 

5456  39 
val prems = Goal "(!!n. f(n) <= f(Suc(n))) ==> m<n > f(m) <= f(n)"; 
969  40 
by (res_inst_tac[("n","n")]nat_induct 1); 
1266  41 
by (Simp_tac 1); 
4089  42 
by (simp_tac (simpset() addsimps [less_Suc_eq]) 1); 
5479  43 
by (blast_tac (claset() addIs (le_trans::prems)) 1); 
2017
dd3e2a91aeca
Proofs made more robust to work in presence of le_refl
paulson
parents:
1820
diff
changeset

44 
qed_spec_mp "mono_lemma1"; 
969  45 

46 
val [p1,p2] = goal Puzzle.thy 

47 
"[ !! n. f(n)<=f(Suc(n)); m<=n ] ==> f(m) <= f(n)"; 

48 
by (rtac (p2 RS le_imp_less_or_eq RS disjE) 1); 

49 
by (etac (p1 RS mono_lemma1) 1); 

2017
dd3e2a91aeca
Proofs made more robust to work in presence of le_refl
paulson
parents:
1820
diff
changeset

50 
by (Fast_tac 1); 
969  51 
qed "mono_lemma"; 
52 

53 
val prems = goal Puzzle.thy "m <= n ==> f(m) <= f(n)"; 

5618  54 
by (fast_tac (claset() addIs [mono_lemma,less_imp_le,lemma2]@prems) 1); 
969  55 
qed "f_mono"; 
56 

5069  57 
Goal "f(n) = n"; 
6676  58 
by (rtac order_antisym 1); 
969  59 
by (rtac lemma1 2); 
4089  60 
by (fast_tac (claset() addIs [Puzzle.f_ax,leI] addDs [leD,f_mono,Suc_leI]) 1); 
969  61 
result(); 