isabelle: src/HOL/ex/Puzzle.ML@44e57a6d947d (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)
3842 b55686a7b22c fixed dots; wenzelm parents: 3336 diff changeset	12	val prems = goal Nat.thy "[\| P(0); !!n. P(Suc(n)) \|] ==> !n. P(n)";
969 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);
4089 96fba19bcbe2 isatool fixclasimp; wenzelm parents: 3842 diff changeset	24	by (fast_tac (claset() addIs [Puzzle.f_ax]) 2);
3336 29ddef80bd49 Renamed lessD to Suc_leI paulson parents: 2609 diff changeset	25	by (rtac Suc_leI 1);
4089 96fba19bcbe2 isatool fixclasimp; wenzelm parents: 3842 diff changeset	26	by (fast_tac (claset() delrules [order_refl]
2017 dd3e2a91aeca Proofs made more robust to work in presence of le_refl paulson parents: 1820 diff changeset	27	addIs [Puzzle.f_ax, le_less_trans]) 1);
1266 3ae9fe3c0f68 added local simpsets clasohm parents: 969 diff changeset	28	val lemma = result() RS spec RS mp;
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	29
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	30	goal Puzzle.thy "n <= f(n)";
4089 96fba19bcbe2 isatool fixclasimp; wenzelm parents: 3842 diff changeset	31	by (fast_tac (claset() addIs [lemma]) 1);
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	32	qed "lemma1";
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	33
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	34	goal Puzzle.thy "f(n) < f(Suc(n))";
4089 96fba19bcbe2 isatool fixclasimp; wenzelm parents: 3842 diff changeset	35	by (deepen_tac (claset() addIs [Puzzle.f_ax, le_less_trans, lemma1]) 0 1);
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	36	qed "lemma2";
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	37
3842 b55686a7b22c fixed dots; wenzelm parents: 3336 diff changeset	38	val prems = goal Puzzle.thy "(!!n. f(n) <= f(Suc(n))) ==> m<n --> f(m) <= f(n)";
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	39	by (res_inst_tac[("n","n")]nat_induct 1);
1266 3ae9fe3c0f68 added local simpsets clasohm parents: 969 diff changeset	40	by (Simp_tac 1);
4089 96fba19bcbe2 isatool fixclasimp; wenzelm parents: 3842 diff changeset	41	by (simp_tac (simpset() addsimps [less_Suc_eq]) 1);
96fba19bcbe2 isatool fixclasimp; wenzelm parents: 3842 diff changeset	42	by (best_tac (claset() addIs (le_trans::prems)) 1);
2017 dd3e2a91aeca Proofs made more robust to work in presence of le_refl paulson parents: 1820 diff changeset	43	qed_spec_mp "mono_lemma1";
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	44
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	45	val [p1,p2] = goal Puzzle.thy
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	46	"[\| !! n. f(n)<=f(Suc(n)); m<=n \|] ==> f(m) <= f(n)";
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	47	by (rtac (p2 RS le_imp_less_or_eq RS disjE) 1);
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	48	by (etac (p1 RS mono_lemma1) 1);
2017 dd3e2a91aeca Proofs made more robust to work in presence of le_refl paulson parents: 1820 diff changeset	49	by (Fast_tac 1);
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	50	qed "mono_lemma";
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	51
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	52	val prems = goal Puzzle.thy "m <= n ==> f(m) <= f(n)";
4089 96fba19bcbe2 isatool fixclasimp; wenzelm parents: 3842 diff changeset	53	by (fast_tac (claset() addIs ([mono_lemma,less_imp_le,lemma2]@prems)) 1);
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	54	qed "f_mono";
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	55
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	56	goal Puzzle.thy "f(n) = n";
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	57	by (rtac le_anti_sym 1);
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	58	by (rtac lemma1 2);
4089 96fba19bcbe2 isatool fixclasimp; wenzelm parents: 3842 diff changeset	59	by (fast_tac (claset() addIs [Puzzle.f_ax,leI] addDs [leD,f_mono,Suc_leI]) 1);
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	60	result();

author	wenzelm
	Fri, 19 Dec 1997 12:09:58 +0100
changeset 4456	44e57a6d947d
parent 4089	96fba19bcbe2
child 5069	3ea049f7979d
permissions	-rw-r--r--