src/LCF/pair.ML
author berghofe
Fri, 11 Jul 2003 14:55:17 +0200
changeset 14102 8af7334af4b3
parent 1461 6bcb44e4d6e5
child 17248 81bf91654e73
permissions -rw-r--r--
- Installed specific code generator for equality enforcing that arguments do not have function types, which would result in an error message during compilation. - Added test case generators for basic types.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 660
diff changeset
     1
(*  Title:      LCF/pair
660
7fe6ec24d842 added header files; deleted commented-out code
lcp
parents: 442
diff changeset
     2
    ID:         $Id$
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 660
diff changeset
     3
    Author:     Tobias Nipkow
660
7fe6ec24d842 added header files; deleted commented-out code
lcp
parents: 442
diff changeset
     4
    Copyright   1992  University of Cambridge
7fe6ec24d842 added header files; deleted commented-out code
lcp
parents: 442
diff changeset
     5
7fe6ec24d842 added header files; deleted commented-out code
lcp
parents: 442
diff changeset
     6
Theory of ordered pairs and products
7fe6ec24d842 added header files; deleted commented-out code
lcp
parents: 442
diff changeset
     7
*)
7fe6ec24d842 added header files; deleted commented-out code
lcp
parents: 442
diff changeset
     8
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
val expand_all_PROD = prove_goal LCF.thy
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 660
diff changeset
    10
        "(ALL p. P(p)) <-> (ALL x y. P(<x,y>))"
6bcb44e4d6e5 expanded tabs
clasohm
parents: 660
diff changeset
    11
        (fn _ => [rtac iffI 1, fast_tac FOL_cs 1, rtac allI 1,
6bcb44e4d6e5 expanded tabs
clasohm
parents: 660
diff changeset
    12
                  rtac (surj_pairing RS subst) 1, fast_tac FOL_cs 1]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
local
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
val ppair = read_instantiate [("z","p::'a*'b")] surj_pairing;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
val qpair = read_instantiate [("z","q::'a*'b")] surj_pairing;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
in
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
val PROD_less = prove_goal LCF.thy
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 660
diff changeset
    19
        "(p::'a*'b) << q <-> FST(p) << FST(q) & SND(p) << SND(q)"
6bcb44e4d6e5 expanded tabs
clasohm
parents: 660
diff changeset
    20
        (fn _ => [EVERY1[rtac iffI,
6bcb44e4d6e5 expanded tabs
clasohm
parents: 660
diff changeset
    21
                  rtac conjI, etac less_ap_term, etac less_ap_term,
6bcb44e4d6e5 expanded tabs
clasohm
parents: 660
diff changeset
    22
                  rtac (ppair RS subst), rtac (qpair RS subst),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 660
diff changeset
    23
                  etac conjE, rtac mono, etac less_ap_term, atac]]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
val PROD_eq = prove_goal LCF.thy "p=q <-> FST(p)=FST(q) & SND(p)=SND(q)"
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 660
diff changeset
    27
        (fn _ => [rtac iffI 1, asm_simp_tac LCF_ss 1,
6bcb44e4d6e5 expanded tabs
clasohm
parents: 660
diff changeset
    28
                  rewtac eq_def,
6bcb44e4d6e5 expanded tabs
clasohm
parents: 660
diff changeset
    29
                  asm_simp_tac (LCF_ss addsimps [PROD_less]) 1]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
val PAIR_less = prove_goal LCF.thy "<a,b> << <c,d> <-> a<<c & b<<d"
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 660
diff changeset
    32
        (fn _ => [simp_tac (LCF_ss addsimps [PROD_less])1]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
val PAIR_eq = prove_goal LCF.thy "<a,b> = <c,d> <-> a=c & b=d"
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 660
diff changeset
    35
        (fn _ => [simp_tac (LCF_ss addsimps [PROD_eq])1]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
val UU_is_UU_UU = prove_goal LCF.thy "<UU,UU> << UU"
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 660
diff changeset
    38
                (fn _ => [simp_tac (LCF_ss addsimps [PROD_less]) 1])
6bcb44e4d6e5 expanded tabs
clasohm
parents: 660
diff changeset
    39
        RS less_UU RS sym;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
val LCF_ss = LCF_ss addsimps [PAIR_less,PAIR_eq,UU_is_UU_UU];