summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Isar_examples/Puzzle.thy

changeset 18191 | ef29685acef0 |

parent 16417 | 9bc16273c2d4 |

child 18193 | 54419506df9e |

1.1 --- a/src/HOL/Isar_examples/Puzzle.thy Wed Nov 16 17:45:36 2005 +0100 1.2 +++ b/src/HOL/Isar_examples/Puzzle.thy Wed Nov 16 17:49:16 2005 +0100 1.3 @@ -13,76 +13,70 @@ 1.4 $n$. Demonstrate that $f$ is the identity. 1.5 *} 1.6 1.7 -theorem "(!!n::nat. f (f n) < f (Suc n)) ==> f n = n" 1.8 +theorem 1.9 + fixes n :: nat 1.10 + assumes f_ax: "\<And>n. f (f n) < f (Suc n)" 1.11 + shows "f n = n" 1.12 proof (rule order_antisym) 1.13 - assume f_ax: "!!n. f (f n) < f (Suc n)" 1.14 - 1.15 - txt {* 1.16 - Note that the generalized form of $n \le f \ap n$ is required 1.17 - later for monotonicity as well. 1.18 - *} 1.19 - show ge: "!!n. n <= f n" 1.20 - proof - 1.21 - fix k show "!!n. k == f n ==> n <= k" (is "PROP ?P k") 1.22 - proof (induct k rule: less_induct) 1.23 - fix k assume hyp: "!!m. m < k ==> PROP ?P m" 1.24 - fix n assume k_def: "k == f n" 1.25 - show "n <= k" 1.26 + { 1.27 + fix n show "n \<le> f n" 1.28 + proof (induct k \<equiv> "f n" rule: less_induct fixing: n) 1.29 + case (less k n) 1.30 + then have hyp: "\<And>m. f m < f n \<Longrightarrow> m \<le> f m" by (simp only:) 1.31 + show "n \<le> f n" 1.32 proof (cases n) 1.33 - assume "n = 0" thus ?thesis by simp 1.34 + case (Suc m) 1.35 + from f_ax have "f (f m) < f n" by (simp only: Suc) 1.36 + with hyp have "f m \<le> f (f m)" . 1.37 + also from f_ax have "\<dots> < f n" by (simp only: Suc) 1.38 + finally have "f m < f n" . 1.39 + with hyp have "m \<le> f m" . 1.40 + also note `\<dots> < f n` 1.41 + finally have "m < f n" . 1.42 + then have "n \<le> f n" by (simp only: Suc) 1.43 + then show ?thesis . 1.44 next 1.45 - fix m assume Suc: "n = Suc m" 1.46 - from f_ax have "f (f m) < f (Suc m)" . 1.47 - with hyp k_def Suc have "f m <= f (f m)" by simp 1.48 - also from f_ax have "... < f (Suc m)" . 1.49 - finally have less: "f m < f (Suc m)" . 1.50 - with hyp k_def Suc have "m <= f m" by simp 1.51 - also note less 1.52 - finally have "m < f (Suc m)" . 1.53 - hence "n <= f n" by (simp only: Suc) 1.54 - thus ?thesis by (simp only: k_def) 1.55 + case 0 1.56 + then show ?thesis by simp 1.57 qed 1.58 qed 1.59 - qed 1.60 + } note ge = this 1.61 1.62 - txt {* 1.63 - In order to show the other direction, we first establish 1.64 - monotonicity of $f$. 1.65 - *} 1.66 { 1.67 - fix m n 1.68 - have "m <= n \<Longrightarrow> f m <= f n" (is "PROP ?P n") 1.69 + fix m n :: nat 1.70 + assume "m \<le> n" 1.71 + then have "f m \<le> f n" 1.72 proof (induct n) 1.73 - assume "m <= 0" hence "m = 0" by simp 1.74 - thus "f m <= f 0" by simp 1.75 + case 0 1.76 + then have "m = 0" by simp 1.77 + then show ?case by simp 1.78 next 1.79 - fix n assume hyp: "PROP ?P n" 1.80 - assume "m <= Suc n" 1.81 - thus "f m <= f (Suc n)" 1.82 + case (Suc n) 1.83 + from Suc.prems show "f m \<le> f (Suc n)" 1.84 proof (rule le_SucE) 1.85 - assume "m <= n" 1.86 - with hyp have "f m <= f n" . 1.87 - also from ge f_ax have "... < f (Suc n)" 1.88 + assume "m \<le> n" 1.89 + with Suc.hyps have "f m \<le> f n" . 1.90 + also from ge f_ax have "\<dots> < f (Suc n)" 1.91 by (rule le_less_trans) 1.92 finally show ?thesis by simp 1.93 next 1.94 assume "m = Suc n" 1.95 - thus ?thesis by simp 1.96 + then show ?thesis by simp 1.97 qed 1.98 qed 1.99 } note mono = this 1.100 1.101 - show "f n <= n" 1.102 + show "f n \<le> n" 1.103 proof - 1.104 - have "~ n < f n" 1.105 + have "\<not> n < f n" 1.106 proof 1.107 assume "n < f n" 1.108 - hence "Suc n <= f n" by simp 1.109 - hence "f (Suc n) <= f (f n)" by (rule mono) 1.110 - also have "... < f (Suc n)" by (rule f_ax) 1.111 - finally have "... < ..." . thus False .. 1.112 + then have "Suc n \<le> f n" by simp 1.113 + then have "f (Suc n) \<le> f (f n)" by (rule mono) 1.114 + also have "\<dots> < f (Suc n)" by (rule f_ax) 1.115 + finally have "\<dots> < \<dots>" . then show False .. 1.116 qed 1.117 - thus ?thesis by simp 1.118 + then show ?thesis by simp 1.119 qed 1.120 qed 1.121