isabelle: src/HOL/ex/LexProd.ML@c820b3cc3df0 (annotated)

969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	1	(* Title: HOL/ex/lex-prod.ML
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	2	ID: $Id$
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	3	Author: Tobias Nipkow, TU Munich
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	4	Copyright 1993 TU Munich
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 lex-prod.thy.
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	7	The lexicographic product of two wellfounded relations is again wellfounded.
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	8	*)
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	9
972 e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...) clasohm parents: 969 diff changeset	10	val prems = goal Prod.thy "!a b. P((a,b)) ==> !p.P(p)";
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	11	by (cut_facts_tac prems 1);
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	12	by (rtac allI 1);
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	13	by (rtac (surjective_pairing RS ssubst) 1);
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	14	by (fast_tac HOL_cs 1);
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	15	qed "split_all_pair";
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	16
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	17	val [wfa,wfb] = goalw LexProd.thy [wf_def,LexProd.lex_prod_def]
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	18	"[\| wf(ra); wf(rb) \|] ==> wf(ra**rb)";
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	19	by (EVERY1 [rtac allI,rtac impI, rtac split_all_pair]);
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	20	by (rtac (wfa RS spec RS mp) 1);
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	21	by (EVERY1 [rtac allI,rtac impI]);
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	22	by (rtac (wfb RS spec RS mp) 1);
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	23	by (fast_tac (set_cs addSEs [Pair_inject]) 1);
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	24	qed "wf_lex_prod";

author	clasohm
	Wed, 21 Jun 1995 15:47:10 +0200
changeset 1151	c820b3cc3df0
parent 972	e61b058d58d2
child 1465	5d7a7e439cec
permissions	-rw-r--r--