src/ZF/pair.ML
author paulson
Thu, 06 Aug 1998 10:37:39 +0200
changeset 5264 7538fce1fe37
parent 4477 b3e5857d8d99
child 5325 f7a5e06adea1
permissions -rw-r--r--
New result from AC directory
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1105
diff changeset
     1
(*  Title:      ZF/pair
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1105
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1992  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
Ordered pairs in Zermelo-Fraenkel Set Theory 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
(** Lemmas for showing that <a,b> uniquely determines a and b **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
    11
qed_goal "singleton_eq_iff" ZF.thy
822
8d5748202c53 Added Krzysztof's theorems singleton_eq_iff, fst_type, snd_type
lcp
parents: 782
diff changeset
    12
    "{a} = {b} <-> a=b"
8d5748202c53 Added Krzysztof's theorems singleton_eq_iff, fst_type, snd_type
lcp
parents: 782
diff changeset
    13
 (fn _=> [ (resolve_tac [extension RS iff_trans] 1),
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
    14
           (Blast_tac 1) ]);
822
8d5748202c53 Added Krzysztof's theorems singleton_eq_iff, fst_type, snd_type
lcp
parents: 782
diff changeset
    15
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
    16
qed_goal "doubleton_eq_iff" ZF.thy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
    "{a,b} = {c,d} <-> (a=c & b=d) | (a=d & b=c)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
 (fn _=> [ (resolve_tac [extension RS iff_trans] 1),
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
    19
           (Blast_tac 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
    21
qed_goalw "Pair_iff" ZF.thy [Pair_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
    "<a,b> = <c,d> <-> a=c & b=d"
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
    23
 (fn _=> [ (simp_tac (simpset() addsimps [doubleton_eq_iff]) 1),
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
    24
           (Blast_tac 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
    26
Addsimps [Pair_iff];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
    27
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
    28
bind_thm ("Pair_inject", Pair_iff RS iffD1 RS conjE);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
    30
AddSEs [Pair_inject];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
    31
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
    32
bind_thm ("Pair_inject1", Pair_iff RS iffD1 RS conjunct1);
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
    33
bind_thm ("Pair_inject2", Pair_iff RS iffD1 RS conjunct2);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
    35
qed_goalw "Pair_not_0" ZF.thy [Pair_def] "<a,b> ~= 0"
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
    36
 (fn _ => [ (blast_tac (claset() addEs [equalityE]) 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
    38
bind_thm ("Pair_neq_0", Pair_not_0 RS notE);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
    40
AddSEs [Pair_neq_0, sym RS Pair_neq_0];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
    41
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
    42
qed_goalw "Pair_neq_fst" ZF.thy [Pair_def] "<a,b>=a ==> P"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
 (fn [major]=>
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
    44
  [ (rtac (consI1 RS mem_asym RS FalseE) 1),
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
    (rtac (major RS subst) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
    (rtac consI1 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
    48
qed_goalw "Pair_neq_snd" ZF.thy [Pair_def] "<a,b>=b ==> P"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
 (fn [major]=>
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
    50
  [ (rtac (consI1 RS consI2 RS mem_asym RS FalseE) 1),
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
    (rtac (major RS subst) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
    (rtac (consI1 RS consI2) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
(*** Sigma: Disjoint union of a family of sets
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
     Generalizes Cartesian product ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
    58
qed_goalw "Sigma_iff" ZF.thy [Sigma_def] "<a,b>: Sigma(A,B) <-> a:A & b:B(a)"
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
    59
 (fn _ => [ Blast_tac 1 ]);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
    60
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
    61
Addsimps [Sigma_iff];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
    62
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
    63
qed_goal "SigmaI" ZF.thy
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
    64
    "!!a b. [| a:A;  b:B(a) |] ==> <a,b> : Sigma(A,B)"
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
    65
 (fn _ => [ Asm_simp_tac 1 ]);
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
    66
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
    67
bind_thm ("SigmaD1", Sigma_iff RS iffD1 RS conjunct1);
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
    68
bind_thm ("SigmaD2", Sigma_iff RS iffD1 RS conjunct2);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
(*The general elimination rule*)
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
    71
qed_goalw "SigmaE" ZF.thy [Sigma_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
    "[| c: Sigma(A,B);  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
\       !!x y.[| x:A;  y:B(x);  c=<x,y> |] ==> P \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
\    |] ==> P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
 (fn major::prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
  [ (cut_facts_tac [major] 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
    (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
    79
qed_goal "SigmaE2" ZF.thy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
    "[| <a,b> : Sigma(A,B);    \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
\       [| a:A;  b:B(a) |] ==> P   \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
\    |] ==> P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
 (fn [major,minor]=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
  [ (rtac minor 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
    (rtac (major RS SigmaD1) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
    (rtac (major RS SigmaD2) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
    88
qed_goalw "Sigma_cong" ZF.thy [Sigma_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
    "[| A=A';  !!x. x:A' ==> B(x)=B'(x) |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
\    Sigma(A,B) = Sigma(A',B')"
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
    91
 (fn prems=> [ (simp_tac (simpset() addsimps prems) 1) ]);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
    92
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
    94
(*Sigma_cong, Pi_cong NOT given to Addcongs: they cause
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
    95
  flex-flex pairs and the "Check your prover" error.  Most
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
    96
  Sigmas and Pis are abbreviated as * or -> *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
    98
AddSIs [SigmaI];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
    99
AddSEs [SigmaE2, SigmaE];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   101
qed_goal "Sigma_empty1" ZF.thy "Sigma(0,B) = 0"
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   102
 (fn _ => [ (Blast_tac 1) ]);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
   103
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   104
qed_goal "Sigma_empty2" ZF.thy "A*0 = 0"
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   105
 (fn _ => [ (Blast_tac 1) ]);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
   106
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
   107
Addsimps [Sigma_empty1, Sigma_empty2];
1105
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   108
5264
7538fce1fe37 New result from AC directory
paulson
parents: 4477
diff changeset
   109
Goal "A*B=0 <-> A=0 | B=0";
7538fce1fe37 New result from AC directory
paulson
parents: 4477
diff changeset
   110
by (Blast_tac 1);
7538fce1fe37 New result from AC directory
paulson
parents: 4477
diff changeset
   111
qed "Sigma_empty_iff";
7538fce1fe37 New result from AC directory
paulson
parents: 4477
diff changeset
   112
1105
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   113
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   114
(*** Projections: fst, snd ***)
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   115
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   116
qed_goalw "fst_conv" ZF.thy [fst_def] "fst(<a,b>) = a"
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
   117
 (fn _=> [ (blast_tac (claset() addIs [the_equality]) 1) ]);
1105
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   118
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   119
qed_goalw "snd_conv" ZF.thy [snd_def] "snd(<a,b>) = b"
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
   120
 (fn _=> [ (blast_tac (claset() addIs [the_equality]) 1) ]);
1105
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   121
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
   122
Addsimps [fst_conv,snd_conv];
1105
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   123
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   124
qed_goal "fst_type" ZF.thy "!!p. p:Sigma(A,B) ==> fst(p) : A"
4477
b3e5857d8d99 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents: 4091
diff changeset
   125
 (fn _=> [ Auto_tac ]);
1105
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   126
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   127
qed_goal "snd_type" ZF.thy "!!p. p:Sigma(A,B) ==> snd(p) : B(fst(p))"
4477
b3e5857d8d99 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents: 4091
diff changeset
   128
 (fn _=> [ Auto_tac ]);
1105
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   129
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   130
qed_goal "Pair_fst_snd_eq" ZF.thy
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
   131
    "!!a A B. a: Sigma(A,B) ==> <fst(a),snd(a)> = a"
4477
b3e5857d8d99 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents: 4091
diff changeset
   132
 (fn _=> [ Auto_tac ]);
1105
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   133
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   135
(*** Eliminator - split ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
1105
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   137
(*A META-equality, so that it applies to higher types as well...*)
3840
e0baea4d485a fixed dots;
wenzelm
parents: 2877
diff changeset
   138
qed_goalw "split" ZF.thy [split_def] "split(%x y. c(x,y), <a,b>) == c(a,b)"
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
   139
 (fn _ => [ (Simp_tac 1),
1105
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   140
            (rtac reflexive_thm 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   141
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
   142
Addsimps [split];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
   143
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   144
qed_goal "split_type" ZF.thy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   145
    "[|  p:Sigma(A,B);   \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   146
\        !!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x,y>) \
3840
e0baea4d485a fixed dots;
wenzelm
parents: 2877
diff changeset
   147
\    |] ==> split(%x y. c(x,y), p) : C(p)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   148
 (fn major::prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   149
  [ (rtac (major RS SigmaE) 1),
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
   150
    (asm_simp_tac (simpset() addsimps prems) 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   151
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   152
goalw ZF.thy [split_def]
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   153
  "!!u. u: A*B ==>   \
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   154
\       R(split(c,u)) <-> (ALL x:A. ALL y:B. u = <x,y> --> R(c(x,y)))";
4477
b3e5857d8d99 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents: 4091
diff changeset
   155
by Auto_tac;
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 533
diff changeset
   156
qed "expand_split";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   157
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   158
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   159
(*** split for predicates: result type o ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   160
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   161
goalw ZF.thy [split_def] "!!R a b. R(a,b) ==> split(R, <a,b>)";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
   162
by (Asm_simp_tac 1);
1105
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   163
qed "splitI";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   164
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   165
val major::sigma::prems = goalw ZF.thy [split_def]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1105
diff changeset
   166
    "[| split(R,z);  z:Sigma(A,B);                      \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1105
diff changeset
   167
\       !!x y. [| z = <x,y>;  R(x,y) |] ==> P           \
1105
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   168
\    |] ==> P";
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   169
by (rtac (sigma RS SigmaE) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   170
by (cut_facts_tac [major] 1);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
   171
by (REPEAT (ares_tac prems 1));
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
   172
by (Asm_full_simp_tac 1);
1105
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   173
qed "splitE";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   174
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   175
goalw ZF.thy [split_def] "!!R a b. split(R,<a,b>) ==> R(a,b)";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
   176
by (Full_simp_tac 1);
1105
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   177
qed "splitD";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   178
533
7357160bc56a ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents: 437
diff changeset
   179
7357160bc56a ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents: 437
diff changeset
   180