src/HOL/ex/Puzzle.thy
 author obua Mon Apr 10 16:00:34 2006 +0200 (2006-04-10) changeset 19404 9bf2cdc9e8e8 parent 17388 495c799df31d child 23813 5440f9f5522c permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
```     1 (*  Title:      HOL/ex/Puzzle.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Tobias Nipkow
```
```     4     Copyright   1993 TU Muenchen
```
```     5
```
```     6 A question from "Bundeswettbewerb Mathematik"
```
```     7
```
```     8 Proof due to Herbert Ehler
```
```     9 *)
```
```    10
```
```    11 header {* A question from ``Bundeswettbewerb Mathematik'' *}
```
```    12
```
```    13 theory Puzzle imports Main begin
```
```    14
```
```    15 consts f :: "nat => nat"
```
```    16
```
```    17 specification (f)
```
```    18   f_ax [intro!]: "f(f(n)) < f(Suc(n))"
```
```    19     by (rule exI [of _ id], simp)
```
```    20
```
```    21
```
```    22 lemma lemma0 [rule_format]: "\<forall>n. k=f(n) --> n <= f(n)"
```
```    23 apply (induct_tac "k" rule: nat_less_induct)
```
```    24 apply (rule allI)
```
```    25 apply (rename_tac "i")
```
```    26 apply (case_tac "i")
```
```    27  apply simp
```
```    28 apply (blast intro!: Suc_leI intro: le_less_trans)
```
```    29 done
```
```    30
```
```    31 lemma lemma1: "n <= f(n)"
```
```    32 by (blast intro: lemma0)
```
```    33
```
```    34 lemma lemma2: "f(n) < f(Suc(n))"
```
```    35 by (blast intro: le_less_trans lemma1)
```
```    36
```
```    37 lemma f_mono [rule_format (no_asm)]: "m <= n --> f(m) <= f(n)"
```
```    38 apply (induct_tac "n")
```
```    39  apply simp
```
```    40 apply (rule impI)
```
```    41 apply (erule le_SucE)
```
```    42  apply (cut_tac n = n in lemma2, auto)
```
```    43 done
```
```    44
```
```    45 lemma f_id: "f(n) = n"
```
```    46 apply (rule order_antisym)
```
```    47 apply (rule_tac [2] lemma1)
```
```    48 apply (blast intro: leI dest: leD f_mono Suc_leI)
```
```    49 done
```
```    50
```
```    51 end
```
```    52
```