1 (* Title: HOL/ex/Puzzle.thy |
1 (* Title: HOL/ex/Puzzle.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tobias Nipkow |
3 Author: Tobias Nipkow |
4 Copyright 1993 TU Muenchen |
|
5 |
|
6 A question from "Bundeswettbewerb Mathematik" |
|
7 |
|
8 Proof due to Herbert Ehler |
|
9 *) |
4 *) |
10 |
5 |
11 header {* A question from ``Bundeswettbewerb Mathematik'' *} |
6 header {* Fun with Functions *} |
12 |
7 |
13 theory Puzzle imports Main begin |
8 theory Puzzle imports Main begin |
14 |
9 |
15 consts f :: "nat => nat" |
10 text{* From \emph{Solving Mathematical Problems} by Terence Tao. He quotes |
16 |
11 Greitzer's \emph{Interational Mathematical Olympiads 1959--1977} as the |
17 specification (f) |
12 original source. Was first brought to our attention by Herbert Ehler who |
18 f_ax [intro!]: "f(f(n)) < f(Suc(n))" |
13 provided a similar proof. *} |
19 by (rule exI [of _ id], simp) |
|
20 |
14 |
21 |
15 |
22 lemma lemma0 [rule_format]: "\<forall>n. k=f(n) --> n <= f(n)" |
16 theorem identity1: fixes f :: "nat \<Rightarrow> nat" |
23 apply (induct_tac "k" rule: nat_less_induct) |
17 assumes fff: "!!n. f(f(n)) < f(Suc(n))" |
24 apply (rule allI) |
18 shows "f(n) = n" |
25 apply (rename_tac "i") |
19 proof - |
26 apply (case_tac "i") |
20 { fix m n have key: "n \<le> m \<Longrightarrow> n \<le> f(m)" |
27 apply simp |
21 proof(induct n arbitrary: m) |
28 apply (blast intro!: Suc_leI intro: le_less_trans) |
22 case 0 show ?case by simp |
29 done |
23 next |
|
24 case (Suc n) |
|
25 hence "m \<noteq> 0" by simp |
|
26 then obtain k where [simp]: "m = Suc k" by (metis not0_implies_Suc) |
|
27 have "n \<le> f(k)" using Suc by simp |
|
28 hence "n \<le> f(f(k))" using Suc by simp |
|
29 also have "\<dots> < f(m)" using fff by simp |
|
30 finally show ?case by simp |
|
31 qed } |
|
32 hence "!!n. n \<le> f(n)" by simp |
|
33 hence "!!n. f(n) < f(Suc n)" by(metis fff order_le_less_trans) |
|
34 hence "f(n) < n+1" by (metis fff lift_Suc_mono_less_iff[of f] Suc_plus1) |
|
35 with `n \<le> f(n)` show "f n = n" by arith |
|
36 qed |
30 |
37 |
31 lemma lemma1: "n <= f(n)" |
|
32 by (blast intro: lemma0) |
|
33 |
38 |
34 lemma f_mono [rule_format (no_asm)]: "m <= n --> f(m) <= f(n)" |
39 text{* From \emph{Solving Mathematical Problems} by Terence Tao. He quotes |
35 apply (induct_tac "n") |
40 the \emph{Australian Mathematics Competition} 1984 as the original source. |
36 apply simp |
41 Possible extension: |
37 apply (metis f_ax le_SucE le_trans lemma0 nat_le_linear nat_less_le) |
42 Should also hold if the range of @{text f} is the reals! |
38 done |
43 *} |
39 |
44 |
40 lemma f_id: "f(n) = n" |
45 lemma identity2: fixes f :: "nat \<Rightarrow> nat" |
41 apply (rule order_antisym) |
46 assumes "f(k) = k" and "k \<ge> 2" |
42 apply (rule_tac [2] lemma1) |
47 and f_times: "\<And>m n. f(m*n) = f(m)*f(n)" |
43 apply (blast intro: leI dest: leD f_mono Suc_leI) |
48 and f_mono: "\<And>m n. m<n \<Longrightarrow> f m < f n" |
44 done |
49 shows "f(n) = n" |
|
50 proof - |
|
51 have 0: "f(0) = 0" |
|
52 by (metis f_mono f_times mult_1_right mult_is_0 nat_less_le nat_mult_eq_cancel_disj not_less_eq) |
|
53 have 1: "f(1) = 1" |
|
54 by (metis f_mono f_times gr_implies_not0 mult_eq_self_implies_10 nat_mult_1_right zero_less_one) |
|
55 have 2: "f 2 = 2" |
|
56 proof - |
|
57 have "2 + (k - 2) = k" using `k \<ge> 2` by arith |
|
58 hence "f(2) \<le> 2" |
|
59 using mono_nat_linear_lb[of f 2 "k - 2",OF f_mono] `f k = k` |
|
60 by simp arith |
|
61 thus "f 2 = 2" using 1 f_mono[of 1 2] by arith |
|
62 qed |
|
63 show ?thesis |
|
64 proof(induct rule:less_induct) |
|
65 case (less i) |
|
66 show ?case |
|
67 proof cases |
|
68 assume "i\<le>1" thus ?case using 0 1 by (auto simp add:le_Suc_eq) |
|
69 next |
|
70 assume "~i\<le>1" |
|
71 show ?case |
|
72 proof cases |
|
73 assume "i mod 2 = 0" |
|
74 hence "EX k. i=2*k" by arith |
|
75 then obtain k where "i = 2*k" .. |
|
76 hence "0 < k" and "k<i" using `~i\<le>1` by arith+ |
|
77 hence "f(k) = k" using less(1) by blast |
|
78 thus "f(i) = i" using `i = 2*k` by(simp add:f_times 2) |
|
79 next |
|
80 assume "i mod 2 \<noteq> 0" |
|
81 hence "EX k. i=2*k+1" by arith |
|
82 then obtain k where "i = 2*k+1" .. |
|
83 hence "0<k" and "k+1<i" using `~i\<le>1` by arith+ |
|
84 have "2*k < f(2*k+1)" |
|
85 proof - |
|
86 have "2*k = 2*f(k)" using less(1) `i=2*k+1` by simp |
|
87 also have "\<dots> = f(2*k)" by(simp add:f_times 2) |
|
88 also have "\<dots> < f(2*k+1)" using f_mono[of "2*k" "2*k+1"] by simp |
|
89 finally show ?thesis . |
|
90 qed |
|
91 moreover |
|
92 have "f(2*k+1) < 2*(k+1)" |
|
93 proof - |
|
94 have "f(2*k+1) < f(2*k+2)" using f_mono[of "2*k+1" "2*k+2"] by simp |
|
95 also have "\<dots> = f(2*(k+1))" by simp |
|
96 also have "\<dots> = 2*f(k+1)" by(simp only:f_times 2) |
|
97 also have "f(k+1) = k+1" using less(1) `i=2*k+1` `~i\<le>1` by simp |
|
98 finally show ?thesis . |
|
99 qed |
|
100 ultimately show "f(i) = i" using `i = 2*k+1` by arith |
|
101 qed |
|
102 qed |
|
103 qed |
|
104 qed |
|
105 |
|
106 |
|
107 text{* The only total model of a naive recursion equation of factorial on |
|
108 integers is 0 for all negative arguments: *} |
|
109 |
|
110 theorem ifac_neg0: fixes ifac :: "int \<Rightarrow> int" |
|
111 assumes ifac_rec: "!!i. ifac i = (if i=0 then 1 else i*ifac(i - 1))" |
|
112 shows "i<0 \<Longrightarrow> ifac i = 0" |
|
113 proof(rule ccontr) |
|
114 assume 0: "i<0" "ifac i \<noteq> 0" |
|
115 { fix j assume "j \<le> i" |
|
116 have "ifac j \<noteq> 0" |
|
117 apply(rule int_le_induct[OF `j\<le>i`]) |
|
118 apply(rule `ifac i \<noteq> 0`) |
|
119 apply (metis `i<0` ifac_rec linorder_not_le mult_eq_0_iff) |
|
120 done |
|
121 } note below0 = this |
|
122 { fix j assume "j<i" |
|
123 have "1 < -j" using `j<i` `i<0` by arith |
|
124 have "ifac(j - 1) \<noteq> 0" using `j<i` by(simp add: below0) |
|
125 then have "\<bar>ifac (j - 1)\<bar> < (-j) * \<bar>ifac (j - 1)\<bar>" using `j<i` |
|
126 mult_le_less_imp_less[OF order_refl[of "abs(ifac(j - 1))"] `1 < -j`] |
|
127 by(simp add:mult_commute) |
|
128 hence "abs(ifac(j - 1)) < abs(ifac j)" |
|
129 using `1 < -j` by(simp add: ifac_rec[of "j"] abs_mult) |
|
130 } note not_wf = this |
|
131 let ?f = "%j. nat(abs(ifac(i - int(j+1))))" |
|
132 obtain k where "\<not> ?f (Suc k) < ?f k" |
|
133 using wf_no_infinite_down_chainE[OF wf_less, of "?f"] by blast |
|
134 moreover have "i - int (k + 1) - 1 = i - int (Suc k + 1)" by arith |
|
135 ultimately show False using not_wf[of "i - int(k+1)"] |
|
136 by (simp only:) arith |
|
137 qed |
45 |
138 |
46 end |
139 end |
47 |
|