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