isabelle: src/HOL/ex/Puzzle.thy@3ff5a2e05810 (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 lemma2: "f(n) < f(Suc(n))"
baabb0fd2ccf converted to Isar paulson parents: 8018 diff changeset	35	by (blast intro: le_less_trans lemma1)
baabb0fd2ccf converted to Isar paulson parents: 8018 diff changeset	36
baabb0fd2ccf converted to Isar paulson parents: 8018 diff changeset	37	lemma f_mono [rule_format (no_asm)]: "m <= n --> f(m) <= f(n)"
baabb0fd2ccf converted to Isar paulson parents: 8018 diff changeset	38	apply (induct_tac "n")
baabb0fd2ccf converted to Isar paulson parents: 8018 diff changeset	39	apply simp
baabb0fd2ccf converted to Isar paulson parents: 8018 diff changeset	40	apply (rule impI)
baabb0fd2ccf converted to Isar paulson parents: 8018 diff changeset	41	apply (erule le_SucE)
baabb0fd2ccf converted to Isar paulson parents: 8018 diff changeset	42	apply (cut_tac n = n in lemma2, auto)
baabb0fd2ccf converted to Isar paulson parents: 8018 diff changeset	43	done
baabb0fd2ccf converted to Isar paulson parents: 8018 diff changeset	44
baabb0fd2ccf converted to Isar paulson parents: 8018 diff changeset	45	lemma f_id: "f(n) = n"
baabb0fd2ccf converted to Isar paulson parents: 8018 diff changeset	46	apply (rule order_antisym)
baabb0fd2ccf converted to Isar paulson parents: 8018 diff changeset	47	apply (rule_tac [2] lemma1)
baabb0fd2ccf converted to Isar paulson parents: 8018 diff changeset	48	apply (blast intro: leI dest: leD f_mono Suc_leI)
baabb0fd2ccf converted to Isar paulson parents: 8018 diff changeset	49	done
baabb0fd2ccf converted to Isar paulson parents: 8018 diff changeset	50
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	51	end
13116 baabb0fd2ccf converted to Isar paulson parents: 8018 diff changeset	52

author	haftmann
	Wed, 04 Oct 2006 14:14:33 +0200
changeset 20853	3ff5a2e05810
parent 17388	495c799df31d
child 23813	5440f9f5522c
permissions	-rw-r--r--