src/HOL/Isar_examples/Puzzle.thy
 changeset 10007 64bf7da1994a parent 9941 fe05af7ec816 child 10436 98c421dd5972
     1.1 --- a/src/HOL/Isar_examples/Puzzle.thy	Sun Sep 17 22:15:08 2000 +0200
1.2 +++ b/src/HOL/Isar_examples/Puzzle.thy	Sun Sep 17 22:19:02 2000 +0200
1.3 @@ -1,128 +1,128 @@
1.4
1.5 -header {* An old chestnut *};
1.6 +header {* An old chestnut *}
1.7
1.8 -theory Puzzle = Main:;
1.9 +theory Puzzle = Main:
1.10
1.11  text_raw {*
1.12   \footnote{A question from Bundeswettbewerb Mathematik''.
1.13   Original pen-and-paper proof due to Herbert Ehler; Isabelle tactic
1.14   script by Tobias Nipkow.}
1.15 -*};
1.16 +*}
1.17
1.18
1.19 -subsection {* Generalized mathematical induction *};
1.20 +subsection {* Generalized mathematical induction *}
1.21
1.22  text {*
1.23   The following derived rule admits induction over some expression
1.24   $f(x)$ wrt.\ the ${<}$ relation on natural numbers.
1.25 -*};
1.26 +*}
1.27
1.28  lemma gen_less_induct:
1.29    "(!!x. ALL y. f y < f x --> P y (f y) ==> P x (f x))
1.30      ==> P x (f x :: nat)"
1.31 -  (is "(!!x. ?H x ==> ?C x) ==> _");
1.32 -proof -;
1.33 -  assume asm: "!!x. ?H x ==> ?C x";
1.34 -  {;
1.35 -    fix k;
1.36 -    have "ALL x. k = f x --> ?C x" (is "?Q k");
1.37 -    proof (rule nat_less_induct);
1.38 -      fix k; assume hyp: "ALL m<k. ?Q m";
1.39 -      show "?Q k";
1.40 -      proof;
1.41 -	fix x; show "k = f x --> ?C x";
1.42 -	proof;
1.43 -	  assume "k = f x";
1.44 -	  with hyp; have "?H x"; by blast;
1.45 -	  thus "?C x"; by (rule asm);
1.46 -	qed;
1.47 -      qed;
1.48 -    qed;
1.49 -  };
1.50 -  thus "?C x"; by simp;
1.51 -qed;
1.52 +  (is "(!!x. ?H x ==> ?C x) ==> _")
1.53 +proof -
1.54 +  assume asm: "!!x. ?H x ==> ?C x"
1.55 +  {
1.56 +    fix k
1.57 +    have "ALL x. k = f x --> ?C x" (is "?Q k")
1.58 +    proof (rule nat_less_induct)
1.59 +      fix k assume hyp: "ALL m<k. ?Q m"
1.60 +      show "?Q k"
1.61 +      proof
1.62 +	fix x show "k = f x --> ?C x"
1.63 +	proof
1.64 +	  assume "k = f x"
1.65 +	  with hyp have "?H x" by blast
1.66 +	  thus "?C x" by (rule asm)
1.67 +	qed
1.68 +      qed
1.69 +    qed
1.70 +  }
1.71 +  thus "?C x" by simp
1.72 +qed
1.73
1.74
1.75 -subsection {* The problem *};
1.76 +subsection {* The problem *}
1.77
1.78  text {*
1.79   Given some function $f\colon \Nat \to \Nat$ such that $f \ap (f \ap 1.80 n) < f \ap (\idt{Suc} \ap n)$ for all $n$.  Demonstrate that $f$ is
1.81   the identity.
1.82 -*};
1.83 +*}
1.84
1.85 -consts f :: "nat => nat";
1.86 -axioms f_ax: "f (f n) < f (Suc n)";
1.87 +consts f :: "nat => nat"
1.88 +axioms f_ax: "f (f n) < f (Suc n)"
1.89
1.90 -theorem "f n = n";
1.91 -proof (rule order_antisym);
1.92 +theorem "f n = n"
1.93 +proof (rule order_antisym)
1.94    txt {*
1.95      Note that the generalized form of $n \le f \ap n$ is required
1.96      later for monotonicity as well.
1.97 -  *};
1.98 -  show ge: "!!n. n <= f n";
1.99 -  proof -;
1.100 -    fix n;
1.101 -    show "?thesis n" (is "?P n (f n)");
1.102 -    proof (rule gen_less_induct [of f ?P]);
1.103 -      fix n; assume hyp: "ALL m. f m < f n --> ?P m (f m)";
1.104 -      show "?P n (f n)";
1.105 -      proof (rule nat.exhaust);
1.106 -	assume "n = 0"; thus ?thesis; by simp;
1.107 -      next;
1.108 -	fix m; assume n_Suc: "n = Suc m";
1.109 -	from f_ax; have "f (f m) < f (Suc m)"; .;
1.110 -	with hyp n_Suc; have "f m <= f (f m)"; by blast;
1.111 -	also; from f_ax; have "... < f (Suc m)"; .;
1.112 -	finally; have lt: "f m < f (Suc m)"; .;
1.113 -	with hyp n_Suc; have "m <= f m"; by blast;
1.114 -	also; note lt;
1.115 -	finally; have "m < f (Suc m)"; .;
1.116 -	thus "n <= f n"; by (simp only: n_Suc);
1.117 -      qed;
1.118 -    qed;
1.119 -  qed;
1.120 +  *}
1.121 +  show ge: "!!n. n <= f n"
1.122 +  proof -
1.123 +    fix n
1.124 +    show "?thesis n" (is "?P n (f n)")
1.125 +    proof (rule gen_less_induct [of f ?P])
1.126 +      fix n assume hyp: "ALL m. f m < f n --> ?P m (f m)"
1.127 +      show "?P n (f n)"
1.128 +      proof (rule nat.exhaust)
1.129 +	assume "n = 0" thus ?thesis by simp
1.130 +      next
1.131 +	fix m assume n_Suc: "n = Suc m"
1.132 +	from f_ax have "f (f m) < f (Suc m)" .
1.133 +	with hyp n_Suc have "f m <= f (f m)" by blast
1.134 +	also from f_ax have "... < f (Suc m)" .
1.135 +	finally have lt: "f m < f (Suc m)" .
1.136 +	with hyp n_Suc have "m <= f m" by blast
1.137 +	also note lt
1.138 +	finally have "m < f (Suc m)" .
1.139 +	thus "n <= f n" by (simp only: n_Suc)
1.140 +      qed
1.141 +    qed
1.142 +  qed
1.143
1.144    txt {*
1.145      In order to show the other direction, we first establish
1.146      monotonicity of $f$.
1.147 -  *};
1.148 -  have mono: "!!m n. m <= n --> f m <= f n";
1.149 -  proof -;
1.150 -    fix m n;
1.151 -    show "?thesis m n" (is "?P n");
1.152 -    proof (induct n);
1.153 -      show "?P 0"; by simp;
1.154 -      fix n; assume hyp: "?P n";
1.155 -      show "?P (Suc n)";
1.156 -      proof;
1.157 -	assume "m <= Suc n";
1.158 -	thus "f m <= f (Suc n)";
1.159 -	proof (rule le_SucE);
1.160 -	  assume "m <= n";
1.161 -	  with hyp; have "f m <= f n"; ..;
1.162 -	  also; from ge f_ax; have "... < f (Suc n)";
1.163 -	    by (rule le_less_trans);
1.164 -	  finally; show ?thesis; by simp;
1.165 -	next;
1.166 -	  assume "m = Suc n";
1.167 -	  thus ?thesis; by simp;
1.168 -	qed;
1.169 -      qed;
1.170 -    qed;
1.171 -  qed;
1.172 +  *}
1.173 +  have mono: "!!m n. m <= n --> f m <= f n"
1.174 +  proof -
1.175 +    fix m n
1.176 +    show "?thesis m n" (is "?P n")
1.177 +    proof (induct n)
1.178 +      show "?P 0" by simp
1.179 +      fix n assume hyp: "?P n"
1.180 +      show "?P (Suc n)"
1.181 +      proof
1.182 +	assume "m <= Suc n"
1.183 +	thus "f m <= f (Suc n)"
1.184 +	proof (rule le_SucE)
1.185 +	  assume "m <= n"
1.186 +	  with hyp have "f m <= f n" ..
1.187 +	  also from ge f_ax have "... < f (Suc n)"
1.188 +	    by (rule le_less_trans)
1.189 +	  finally show ?thesis by simp
1.190 +	next
1.191 +	  assume "m = Suc n"
1.192 +	  thus ?thesis by simp
1.193 +	qed
1.194 +      qed
1.195 +    qed
1.196 +  qed
1.197
1.198 -  show "f n <= n";
1.199 -  proof (rule leI);
1.200 -    show "~ n < f n";
1.201 -    proof;
1.202 -      assume "n < f n";
1.203 -      hence "Suc n <= f n"; by (rule Suc_leI);
1.204 -      hence "f (Suc n) <= f (f n)"; by (rule mono [rule_format]);
1.205 -      also; have "... < f (Suc n)"; by (rule f_ax);
1.206 -      finally; have "... < ..."; .; thus False; ..;
1.207 -    qed;
1.208 -  qed;
1.209 -qed;
1.210 +  show "f n <= n"
1.211 +  proof (rule leI)
1.212 +    show "~ n < f n"
1.213 +    proof
1.214 +      assume "n < f n"
1.215 +      hence "Suc n <= f n" by (rule Suc_leI)
1.216 +      hence "f (Suc n) <= f (f n)" by (rule mono [rule_format])
1.217 +      also have "... < f (Suc n)" by (rule f_ax)
1.218 +      finally have "... < ..." . thus False ..
1.219 +    qed
1.220 +  qed
1.221 +qed
1.222
1.223 -end;
1.224 +end