author  paulson 
Mon, 23 Sep 1996 18:26:51 +0200  
changeset 2017  dd3e2a91aeca 
parent 1820  e381e1c51689 
child 2031  03a843f0f447 
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 

6 
For puzzle.thy. A question from "Bundeswettbewerb Mathematik" 

7 

8 
Proof due to Herbert Ehler 

9 
*) 

10 

11 
(*specialized form of induction needed below*) 

12 
val prems = goal Nat.thy "[ P(0); !!n. P(Suc(n)) ] ==> !n.P(n)"; 

13 
by (EVERY1 [rtac (nat_induct RS allI), resolve_tac prems, resolve_tac prems]); 

14 
qed "nat_exh"; 

15 

16 
goal Puzzle.thy "! n. k=f(n) > n <= f(n)"; 

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

18 
by (rtac nat_exh 1); 

1266  19 
by (Simp_tac 1); 
969  20 
by (rtac impI 1); 
21 
by (rtac classical 1); 

22 
by (dtac not_leE 1); 

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

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

24 
by (fast_tac (!claset addIs [Puzzle.f_ax]) 2); 
dd3e2a91aeca
Proofs made more robust to work in presence of le_refl
paulson
parents:
1820
diff
changeset

25 
br lessD 1; 
dd3e2a91aeca
Proofs made more robust to work in presence of le_refl
paulson
parents:
1820
diff
changeset

26 
by (best_tac (!claset delrules [le_refl] 
dd3e2a91aeca
Proofs made more robust to work in presence of le_refl
paulson
parents:
1820
diff
changeset

27 
addIs [Puzzle.f_ax, le_less_trans]) 1); 
1266  28 
val lemma = result() RS spec RS mp; 
969  29 

30 
goal Puzzle.thy "n <= f(n)"; 

1820  31 
by (fast_tac (!claset addIs [lemma]) 1); 
969  32 
qed "lemma1"; 
33 

34 
goal Puzzle.thy "f(n) < f(Suc(n))"; 

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

35 
by (deepen_tac (!claset addIs [Puzzle.f_ax, le_less_trans, lemma1]) 0 1); 
969  36 
qed "lemma2"; 
37 

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

39 
by (res_inst_tac[("n","n")]nat_induct 1); 

1266  40 
by (Simp_tac 1); 
1673
d22110ddd0af
repaired critical proofs depending on the order inside nonconfluent SimpSets
oheimb
parents:
1465
diff
changeset

41 
by (simp_tac (!simpset addsimps [less_Suc_eq]) 1); 
2017
dd3e2a91aeca
Proofs made more robust to work in presence of le_refl
paulson
parents:
1820
diff
changeset

42 
by (best_tac (!claset addIs (le_trans::prems)) 1); 
dd3e2a91aeca
Proofs made more robust to work in presence of le_refl
paulson
parents:
1820
diff
changeset

43 
qed_spec_mp "mono_lemma1"; 
969  44 

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

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

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

48 
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

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

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

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

56 
goal Puzzle.thy "f(n) = n"; 

57 
by (rtac le_anti_sym 1); 

58 
by (rtac lemma1 2); 

1820  59 
by (fast_tac (!claset addIs [Puzzle.f_ax,leI] addDs [leD,f_mono,lessD]) 1); 
969  60 
result(); 