ex/LexProd.ML

+(*  Title: 	HOL/ex/lex-prod.ML
+    ID:         $Id$
+    Author: 	Tobias Nipkow, TU Munich
+    Copyright   1993  TU Munich
+
+For lex-prod.thy.
+The lexicographic product of two wellfounded relations is again wellfounded.
+*)
+
+val prems = goal Prod.thy "!a b. P(<a,b>) ==> !p.P(p)";
+by (cut_facts_tac prems 1);
+by (rtac allI 1);
+by (rtac (surjective_pairing RS ssubst) 1);
+by (fast_tac HOL_cs 1);
+val split_all_pair = result();
+
+val [wfa,wfb] = goalw LexProd.thy [wf_def,LexProd.lex_prod_def]
+ "[| wf(ra); wf(rb) |] ==> wf(ra**rb)";
+by (EVERY1 [rtac allI,rtac impI, rtac split_all_pair]);
+by (rtac (wfa RS spec RS mp) 1);
+by (EVERY1 [rtac allI,rtac impI]);
+by (rtac (wfb RS spec RS mp) 1);
+by (fast_tac (set_cs addSEs [Pair_inject]) 1);
+val wf_lex_prod = result();