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

1465 5d7a7e439cec expanded tabs clasohm parents: 972 diff changeset	1	(* Title: HOL/ex/lex-prod.ML
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	2	ID: $Id$
1465 5d7a7e439cec expanded tabs clasohm parents: 972 diff changeset	3	Author: Tobias Nipkow, TU Munich
969 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);
2031 03a843f0f447 Ran expandshort paulson parents: 1820 diff changeset	13	by (stac surjective_pairing 1);
1820 e381e1c51689 Classical tactics now use default claset. berghofe parents: 1465 diff changeset	14	by (Fast_tac 1);
969 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);
1820 e381e1c51689 Classical tactics now use default claset. berghofe parents: 1465 diff changeset	23	by (fast_tac (!claset addSEs [Pair_inject]) 1);
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	24	qed "wf_lex_prod";

author	paulson
	Wed, 13 Nov 1996 10:47:08 +0100
changeset 2183	8d42a7bccf0b
parent 2031	03a843f0f447
permissions	-rw-r--r--