added Isar_examples/Puzzle.thy;
authorwenzelm
Wed Nov 17 15:03:23 1999 +0100 (1999-11-17)
changeset 80202823ce1753a5
parent 8019 fead0dbf5b0a
child 8021 9a400ba634b8
added Isar_examples/Puzzle.thy;
src/HOL/IsaMakefile
src/HOL/Isar_examples/Puzzle.thy
src/HOL/Isar_examples/ROOT.ML
src/HOL/Isar_examples/document/style.tex
     1.1 --- a/src/HOL/IsaMakefile	Wed Nov 17 11:16:26 1999 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Wed Nov 17 15:03:23 1999 +0100
     1.3 @@ -421,10 +421,10 @@
     1.4    Isar_examples/ExprCompiler.thy Isar_examples/Group.thy \
     1.5    Isar_examples/KnasterTarski.thy Isar_examples/MultisetOrder.thy \
     1.6    Isar_examples/MutilatedCheckerboard.thy Isar_examples/Peirce.thy \
     1.7 -  Isar_examples/Summation.thy Isar_examples/ROOT.ML \
     1.8 -  Isar_examples/W_correct.thy Isar_examples/document/proof.sty \
     1.9 -  Isar_examples/document/root.bib Isar_examples/document/root.tex \
    1.10 -  Isar_examples/document/style.tex
    1.11 +  Isar_examples/Puzzle.thy Isar_examples/Summation.thy \
    1.12 +  Isar_examples/ROOT.ML Isar_examples/W_correct.thy \
    1.13 +  Isar_examples/document/proof.sty Isar_examples/document/root.bib \
    1.14 +  Isar_examples/document/root.tex Isar_examples/document/style.tex
    1.15  	@$(ISATOOL) usedir $(OUT)/HOL Isar_examples
    1.16  
    1.17  
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Isar_examples/Puzzle.thy	Wed Nov 17 15:03:23 1999 +0100
     2.3 @@ -0,0 +1,128 @@
     2.4 +
     2.5 +header {* An old chestnut *};
     2.6 +
     2.7 +theory Puzzle = Main:;
     2.8 +
     2.9 +text_raw {*
    2.10 + \footnote{A question from ``Bundeswettbewerb Mathematik''.
    2.11 + Original pen-and-paper proof due to Herbert Ehler; Isabelle tactic
    2.12 + script by Tobias Nipkow.}
    2.13 +*};
    2.14 +
    2.15 +
    2.16 +subsection {* Generalized mathematical induction *};
    2.17 +
    2.18 +text {*
    2.19 + The following derived rule admits induction over some expression
    2.20 + $f(x)$ wrt.\ the ${<}$ relation on natural numbers.
    2.21 +*};
    2.22 +
    2.23 +lemma gen_less_induct:
    2.24 +  "(!!x. ALL y. f y < f x --> P y (f y) ==> P x (f x))
    2.25 +    ==> P x (f x :: nat)"
    2.26 +  (is "(!!x. ?H x ==> ?C x) ==> _");
    2.27 +proof -;
    2.28 +  assume asm: "!!x. ?H x ==> ?C x";
    2.29 +  {{;
    2.30 +    fix k;
    2.31 +    have "ALL x. k = f x --> ?C x" (is "?Q k");
    2.32 +    proof (rule less_induct);
    2.33 +      fix k; assume hyp: "ALL m<k. ?Q m";
    2.34 +      show "?Q k";
    2.35 +      proof;
    2.36 +	fix x; show "k = f x --> ?C x";
    2.37 +	proof;
    2.38 +	  assume "k = f x";
    2.39 +	  with hyp; have "?H x"; by blast;
    2.40 +	  thus "?C x"; by (rule asm);
    2.41 +	qed;
    2.42 +      qed;
    2.43 +    qed;
    2.44 +  }};
    2.45 +  thus "?C x"; by simp;
    2.46 +qed;
    2.47 +
    2.48 +
    2.49 +subsection {* The problem *};
    2.50 +
    2.51 +text {*
    2.52 + Given some function $f\colon \Nat \to \Nat$ such that $f \ap (f \ap
    2.53 + n) < f \ap (\idt{Suc} \ap n)$ for all $n$.  Demonstrate that $f$ is
    2.54 + the identity.
    2.55 +*};
    2.56 +
    2.57 +consts f :: "nat => nat";
    2.58 +axioms f_ax: "f (f n) < f (Suc n)";
    2.59 +
    2.60 +theorem "f n = n";
    2.61 +proof (rule order_antisym);
    2.62 +  txt {*
    2.63 +    Note that the generalized form of $n \le f \ap n$ is required
    2.64 +    later for monotonicity as well.
    2.65 +  *};
    2.66 +  show ge: "!!n. n <= f n";
    2.67 +  proof -;
    2.68 +    fix n;
    2.69 +    show "?thesis n" (is "?P n (f n)");
    2.70 +    proof (rule gen_less_induct [of f ?P]);
    2.71 +      fix n; assume hyp: "ALL m. f m < f n --> ?P m (f m)";
    2.72 +      show "?P n (f n)";
    2.73 +      proof (rule nat.exhaust);
    2.74 +	assume "n = 0"; thus ?thesis; by simp;
    2.75 +      next;
    2.76 +	fix m; assume n_Suc: "n = Suc m";
    2.77 +	from f_ax; have "f (f m) < f (Suc m)"; .;
    2.78 +	with hyp n_Suc; have "f m <= f (f m)"; by blast;
    2.79 +	also; from f_ax; have "... < f (Suc m)"; .;
    2.80 +	finally; have lt: "f m < f (Suc m)"; .;
    2.81 +	with hyp n_Suc; have "m <= f m"; by blast;
    2.82 +	also; note lt;
    2.83 +	finally; have "m < f (Suc m)"; .;
    2.84 +	thus "n <= f n"; by (simp only: n_Suc);
    2.85 +      qed;
    2.86 +    qed;
    2.87 +  qed;
    2.88 +
    2.89 +  txt {*
    2.90 +    In order to show the other direction, we first establish
    2.91 +    monotonicity of $f$.
    2.92 +  *};
    2.93 +  have mono: "!!m n. m <= n --> f m <= f n";
    2.94 +  proof -;
    2.95 +    fix m n;
    2.96 +    show "?thesis m n" (is "?P n");
    2.97 +    proof (induct n);
    2.98 +      show "?P 0"; by simp;
    2.99 +      fix n; assume hyp: "?P n";
   2.100 +      show "?P (Suc n)";
   2.101 +      proof;
   2.102 +	assume "m <= Suc n";
   2.103 +	thus "f m <= f (Suc n)";
   2.104 +	proof (rule le_SucE);
   2.105 +	  assume "m <= n";
   2.106 +	  with hyp; have "f m <= f n"; ..;
   2.107 +	  also; from ge f_ax; have "... < f (Suc n)";
   2.108 +	    by (rule le_less_trans);
   2.109 +	  finally; show ?thesis; by simp;
   2.110 +	next;
   2.111 +	  assume "m = Suc n";
   2.112 +	  thus ?thesis; by simp;
   2.113 +	qed;
   2.114 +      qed;
   2.115 +    qed;
   2.116 +  qed;
   2.117 +
   2.118 +  show "f n <= n";
   2.119 +  proof (rule leI);
   2.120 +    show "~ n < f n";
   2.121 +    proof;
   2.122 +      assume "n < f n";
   2.123 +      hence "Suc n <= f n"; by (rule Suc_leI);
   2.124 +      hence "f (Suc n) <= f (f n)"; by (rule mono [rulify]);
   2.125 +      also; have "... < f (Suc n)"; by (rule f_ax);
   2.126 +      finally; have "... < ..."; .; thus False; ..;
   2.127 +    qed;
   2.128 +  qed;
   2.129 +qed;
   2.130 +
   2.131 +end;
     3.1 --- a/src/HOL/Isar_examples/ROOT.ML	Wed Nov 17 11:16:26 1999 +0100
     3.2 +++ b/src/HOL/Isar_examples/ROOT.ML	Wed Nov 17 15:03:23 1999 +0100
     3.3 @@ -15,3 +15,4 @@
     3.4  time_use_thy "MutilatedCheckerboard";
     3.5  with_path "../Induct" time_use_thy "MultisetOrder";
     3.6  with_path "../W0" time_use_thy "W_correct";
     3.7 +time_use_thy "Puzzle";
     4.1 --- a/src/HOL/Isar_examples/document/style.tex	Wed Nov 17 11:16:26 1999 +0100
     4.2 +++ b/src/HOL/Isar_examples/document/style.tex	Wed Nov 17 15:03:23 1999 +0100
     4.3 @@ -24,6 +24,9 @@
     4.4  \newcommand{\disj}{\lor}
     4.5  \newcommand{\Impl}{\Longrightarrow}
     4.6  
     4.7 +\newcommand{\Nat}{\mathord{\mathrm{I}\mkern-3.8mu\mathrm{N}}}
     4.8 +
     4.9 +
    4.10  %%% Local Variables: 
    4.11  %%% mode: latex
    4.12  %%% TeX-master: "root"