author wenzelm Wed Nov 16 17:49:16 2005 +0100 (2005-11-16) changeset 18191 ef29685acef0 parent 18190 b7748c77562f child 18192 6e2fd2d276d3
improved induction proof: local defs/fixes;
```     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
```