isabelle: src/HOL/ex/Puzzle.ML@5d7a7e439cec (annotated)

1465 5d7a7e439cec expanded tabs clasohm parents: 1266 diff changeset	1	(* Title: HOL/ex/puzzle.ML
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	2	ID: $Id$
1465 5d7a7e439cec expanded tabs clasohm parents: 1266 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
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	6	For puzzle.thy. A question from "Bundeswettbewerb Mathematik"
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	7
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	8	Proof due to Herbert Ehler
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	9	*)
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	10
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	11	(specialized form of induction needed below)
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	12	val prems = goal Nat.thy "[\| P(0); !!n. P(Suc(n)) \|] ==> !n.P(n)";
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	13	by (EVERY1 [rtac (nat_induct RS allI), resolve_tac prems, resolve_tac prems]);
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	14	qed "nat_exh";
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	15
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	16	goal Puzzle.thy "! n. k=f(n) --> n <= f(n)";
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	17	by (res_inst_tac [("n","k")] less_induct 1);
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	18	by (rtac nat_exh 1);
1266 3ae9fe3c0f68 added local simpsets clasohm parents: 969 diff changeset	19	by (Simp_tac 1);
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	20	by (rtac impI 1);
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	21	by (rtac classical 1);
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	22	by (dtac not_leE 1);
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	23	by (subgoal_tac "f(na) <= f(f(na))" 1);
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	24	by (best_tac (HOL_cs addIs [lessD,Puzzle.f_ax,le_less_trans,le_trans]) 1);
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	25	by (fast_tac (HOL_cs addIs [Puzzle.f_ax]) 1);
1266 3ae9fe3c0f68 added local simpsets clasohm parents: 969 diff changeset	26	val lemma = result() RS spec RS mp;
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	27
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	28	goal Puzzle.thy "n <= f(n)";
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	29	by (fast_tac (HOL_cs addIs [lemma]) 1);
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	30	qed "lemma1";
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	31
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	32	goal Puzzle.thy "f(n) < f(Suc(n))";
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	33	by (fast_tac (HOL_cs addIs [Puzzle.f_ax,le_less_trans,lemma1]) 1);
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	34	qed "lemma2";
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	35
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	36	val prems = goal Puzzle.thy "(!!n.f(n) <= f(Suc(n))) ==> m<n --> f(m) <= f(n)";
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	37	by (res_inst_tac[("n","n")]nat_induct 1);
1266 3ae9fe3c0f68 added local simpsets clasohm parents: 969 diff changeset	38	by (Simp_tac 1);
3ae9fe3c0f68 added local simpsets clasohm parents: 969 diff changeset	39	by (Simp_tac 1);
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	40	by (fast_tac (HOL_cs addIs (le_trans::prems)) 1);
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	41	bind_thm("mono_lemma1", result() RS mp);
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	42
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	43	val [p1,p2] = goal Puzzle.thy
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	44	"[\| !! n. f(n)<=f(Suc(n)); m<=n \|] ==> f(m) <= f(n)";
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	45	by (rtac (p2 RS le_imp_less_or_eq RS disjE) 1);
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	46	by (etac (p1 RS mono_lemma1) 1);
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	47	by (fast_tac (HOL_cs addIs [le_refl]) 1);
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	48	qed "mono_lemma";
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	49
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	50	val prems = goal Puzzle.thy "m <= n ==> f(m) <= f(n)";
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	51	by (fast_tac (HOL_cs addIs ([mono_lemma,less_imp_le,lemma2]@prems)) 1);
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	52	qed "f_mono";
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	53
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	54	goal Puzzle.thy "f(n) = n";
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	55	by (rtac le_anti_sym 1);
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	56	by (rtac lemma1 2);
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	57	by (fast_tac (HOL_cs addIs [Puzzle.f_ax,leI] addDs [leD,f_mono,lessD]) 1);
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	58	result();

author	clasohm
	Tue, 30 Jan 1996 15:24:36 +0100
changeset 1465	5d7a7e439cec
parent 1266	3ae9fe3c0f68
child 1673	d22110ddd0af
permissions	-rw-r--r--