src/LCF/pair.ML
 author oheimb Fri Jun 02 20:38:28 2000 +0200 (2000-06-02) changeset 9028 8a1ec8f05f14 parent 1461 6bcb44e4d6e5 child 17248 81bf91654e73 permissions -rw-r--r--
```     1 (*  Title:      LCF/pair
```
```     2     ID:         \$Id\$
```
```     3     Author:     Tobias Nipkow
```
```     4     Copyright   1992  University of Cambridge
```
```     5
```
```     6 Theory of ordered pairs and products
```
```     7 *)
```
```     8
```
```     9 val expand_all_PROD = prove_goal LCF.thy
```
```    10         "(ALL p. P(p)) <-> (ALL x y. P(<x,y>))"
```
```    11         (fn _ => [rtac iffI 1, fast_tac FOL_cs 1, rtac allI 1,
```
```    12                   rtac (surj_pairing RS subst) 1, fast_tac FOL_cs 1]);
```
```    13
```
```    14 local
```
```    15 val ppair = read_instantiate [("z","p::'a*'b")] surj_pairing;
```
```    16 val qpair = read_instantiate [("z","q::'a*'b")] surj_pairing;
```
```    17 in
```
```    18 val PROD_less = prove_goal LCF.thy
```
```    19         "(p::'a*'b) << q <-> FST(p) << FST(q) & SND(p) << SND(q)"
```
```    20         (fn _ => [EVERY1[rtac iffI,
```
```    21                   rtac conjI, etac less_ap_term, etac less_ap_term,
```
```    22                   rtac (ppair RS subst), rtac (qpair RS subst),
```
```    23                   etac conjE, rtac mono, etac less_ap_term, atac]]);
```
```    24 end;
```
```    25
```
```    26 val PROD_eq = prove_goal LCF.thy "p=q <-> FST(p)=FST(q) & SND(p)=SND(q)"
```
```    27         (fn _ => [rtac iffI 1, asm_simp_tac LCF_ss 1,
```
```    28                   rewtac eq_def,
```
```    29                   asm_simp_tac (LCF_ss addsimps [PROD_less]) 1]);
```
```    30
```
```    31 val PAIR_less = prove_goal LCF.thy "<a,b> << <c,d> <-> a<<c & b<<d"
```
```    32         (fn _ => [simp_tac (LCF_ss addsimps [PROD_less])1]);
```
```    33
```
```    34 val PAIR_eq = prove_goal LCF.thy "<a,b> = <c,d> <-> a=c & b=d"
```
```    35         (fn _ => [simp_tac (LCF_ss addsimps [PROD_eq])1]);
```
```    36
```
```    37 val UU_is_UU_UU = prove_goal LCF.thy "<UU,UU> << UU"
```
```    38                 (fn _ => [simp_tac (LCF_ss addsimps [PROD_less]) 1])
```
```    39         RS less_UU RS sym;
```
```    40
```
```    41 val LCF_ss = LCF_ss addsimps [PAIR_less,PAIR_eq,UU_is_UU_UU];
```