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