ex/LexProd.ML
author clasohm
Wed, 02 Mar 1994 12:26:55 +0100
changeset 48 21291189b51e
parent 0 7949f97df77a
child 171 16c4ea954511
permissions -rw-r--r--
changed "." to "$" and Cons to infix "#" to eliminate ambiguity
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	HOL/ex/lex-prod.ML
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     3
    Author: 	Tobias Nipkow, TU Munich
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1993  TU Munich
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     5
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     6
For lex-prod.thy.
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     7
The lexicographic product of two wellfounded relations is again wellfounded.
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     8
*)
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     9
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    10
val prems = goal Prod.thy "!a b. P(<a,b>) ==> !p.P(p)";
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    11
by (cut_facts_tac prems 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    12
by (rtac allI 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    13
by (rtac (surjective_pairing RS ssubst) 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    14
by (fast_tac HOL_cs 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    15
val split_all_pair = result();
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    16
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    17
val [wfa,wfb] = goalw LexProd.thy [wf_def,LexProd.lex_prod_def]
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    18
 "[| wf(ra); wf(rb) |] ==> wf(ra**rb)";
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    19
by (EVERY1 [rtac allI,rtac impI, rtac split_all_pair]);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    20
by (rtac (wfa RS spec RS mp) 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    21
by (EVERY1 [rtac allI,rtac impI]);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    22
by (rtac (wfb RS spec RS mp) 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    23
by (fast_tac (set_cs addSEs [Pair_inject]) 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    24
val wf_lex_prod = result();