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