isabelle: src/HOL/ex/Puzzle.thy@039ae566a4a2 (annotated)

2222 a3fb552f10e3 Added Lagrang. Modified comment. nipkow parents: 1476 diff changeset	1	(* Title: HOL/ex/Puzzle.thy
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	2	ID: $Id$
1476 608483c2122a expanded tabs; incorporated Konrad's changes clasohm parents: 1376 diff changeset	3	Author: Tobias Nipkow
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	4	Copyright 1993 TU Muenchen
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	5
2222 a3fb552f10e3 Added Lagrang. Modified comment. nipkow parents: 1476 diff changeset	6	A question from "Bundeswettbewerb Mathematik"
13116 baabb0fd2ccf converted to Isar paulson parents: 8018 diff changeset	7
baabb0fd2ccf converted to Isar paulson parents: 8018 diff changeset	8	Proof due to Herbert Ehler
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	9	*)
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	10
17388 495c799df31d tuned headers etc.; wenzelm parents: 16417 diff changeset	11	header {* A question from ``Bundeswettbewerb Mathematik'' *}
495c799df31d tuned headers etc.; wenzelm parents: 16417 diff changeset	12
16417 9bc16273c2d4 migrated theory headers to new format haftmann parents: 14126 diff changeset	13	theory Puzzle imports Main begin
13116 baabb0fd2ccf converted to Isar paulson parents: 8018 diff changeset	14
baabb0fd2ccf converted to Isar paulson parents: 8018 diff changeset	15	consts f :: "nat => nat"
baabb0fd2ccf converted to Isar paulson parents: 8018 diff changeset	16
14126 28824746d046 Tidying and replacement of some axioms by specifications paulson parents: 13116 diff changeset	17	specification (f)
28824746d046 Tidying and replacement of some axioms by specifications paulson parents: 13116 diff changeset	18	f_ax [intro!]: "f(f(n)) < f(Suc(n))"
28824746d046 Tidying and replacement of some axioms by specifications paulson parents: 13116 diff changeset	19	by (rule exI [of _ id], simp)
13116 baabb0fd2ccf converted to Isar paulson parents: 8018 diff changeset	20
baabb0fd2ccf converted to Isar paulson parents: 8018 diff changeset	21
baabb0fd2ccf converted to Isar paulson parents: 8018 diff changeset	22	lemma lemma0 [rule_format]: "\<forall>n. k=f(n) --> n <= f(n)"
baabb0fd2ccf converted to Isar paulson parents: 8018 diff changeset	23	apply (induct_tac "k" rule: nat_less_induct)
baabb0fd2ccf converted to Isar paulson parents: 8018 diff changeset	24	apply (rule allI)
baabb0fd2ccf converted to Isar paulson parents: 8018 diff changeset	25	apply (rename_tac "i")
baabb0fd2ccf converted to Isar paulson parents: 8018 diff changeset	26	apply (case_tac "i")
baabb0fd2ccf converted to Isar paulson parents: 8018 diff changeset	27	apply simp
baabb0fd2ccf converted to Isar paulson parents: 8018 diff changeset	28	apply (blast intro!: Suc_leI intro: le_less_trans)
baabb0fd2ccf converted to Isar paulson parents: 8018 diff changeset	29	done
baabb0fd2ccf converted to Isar paulson parents: 8018 diff changeset	30
baabb0fd2ccf converted to Isar paulson parents: 8018 diff changeset	31	lemma lemma1: "n <= f(n)"
baabb0fd2ccf converted to Isar paulson parents: 8018 diff changeset	32	by (blast intro: lemma0)
baabb0fd2ccf converted to Isar paulson parents: 8018 diff changeset	33
baabb0fd2ccf converted to Isar paulson parents: 8018 diff changeset	34	lemma f_mono [rule_format (no_asm)]: "m <= n --> f(m) <= f(n)"
baabb0fd2ccf converted to Isar paulson parents: 8018 diff changeset	35	apply (induct_tac "n")
23813 5440f9f5522c tidied using sledgehammer paulson parents: 17388 diff changeset	36	apply simp
5440f9f5522c tidied using sledgehammer paulson parents: 17388 diff changeset	37	apply (metis f_ax le_SucE le_trans lemma0 nat_le_linear nat_less_le)
13116 baabb0fd2ccf converted to Isar paulson parents: 8018 diff changeset	38	done
baabb0fd2ccf converted to Isar paulson parents: 8018 diff changeset	39
baabb0fd2ccf converted to Isar paulson parents: 8018 diff changeset	40	lemma f_id: "f(n) = n"
baabb0fd2ccf converted to Isar paulson parents: 8018 diff changeset	41	apply (rule order_antisym)
baabb0fd2ccf converted to Isar paulson parents: 8018 diff changeset	42	apply (rule_tac [2] lemma1)
baabb0fd2ccf converted to Isar paulson parents: 8018 diff changeset	43	apply (blast intro: leI dest: leD f_mono Suc_leI)
baabb0fd2ccf converted to Isar paulson parents: 8018 diff changeset	44	done
baabb0fd2ccf converted to Isar paulson parents: 8018 diff changeset	45
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	46	end
13116 baabb0fd2ccf converted to Isar paulson parents: 8018 diff changeset	47

author	wenzelm
	Sun, 22 Jul 2007 21:20:56 +0200
changeset 23912	039ae566a4a2
parent 23813	5440f9f5522c
child 27789	1bf827e3258d
permissions	-rw-r--r--