src/ZF/pair.ML
author paulson
Fri, 16 Feb 1996 18:00:47 +0100
changeset 1512 ce37c64244c0
parent 1461 6bcb44e4d6e5
child 2469 b50b8c0eec01
permissions -rw-r--r--
Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
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
822
8d5748202c53 Added Krzysztof's theorems singleton_eq_iff, fst_type, snd_type
lcp
parents: 782
diff changeset
    11
qed_goal "singleton_eq_iff" ZF.thy
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),
8d5748202c53 Added Krzysztof's theorems singleton_eq_iff, fst_type, snd_type
lcp
parents: 782
diff changeset
    14
           (fast_tac upair_cs 1) ]);
8d5748202c53 Added Krzysztof's theorems singleton_eq_iff, fst_type, snd_type
lcp
parents: 782
diff changeset
    15
8d5748202c53 Added Krzysztof's theorems singleton_eq_iff, fst_type, snd_type
lcp
parents: 782
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),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
           (fast_tac upair_cs 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 533
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"
822
8d5748202c53 Added Krzysztof's theorems singleton_eq_iff, fst_type, snd_type
lcp
parents: 782
diff changeset
    23
 (fn _=> [ (simp_tac (FOL_ss addsimps [doubleton_eq_iff]) 1),
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
           (fast_tac FOL_cs 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
782
200a16083201 added bind_thm for theorems defined by "standard ..."
clasohm
parents: 760
diff changeset
    26
bind_thm ("Pair_inject", (Pair_iff RS iffD1 RS conjE));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 533
diff changeset
    28
qed_goal "Pair_inject1" ZF.thy "<a,b> = <c,d> ==> a=c"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
 (fn [major]=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
  [ (rtac (major RS Pair_inject) 1), (assume_tac 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 533
diff changeset
    32
qed_goal "Pair_inject2" ZF.thy "<a,b> = <c,d> ==> b=d"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
 (fn [major]=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
  [ (rtac (major RS Pair_inject) 1), (assume_tac 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 533
diff changeset
    36
qed_goalw "Pair_neq_0" ZF.thy [Pair_def] "<a,b>=0 ==> P"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
 (fn [major]=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
  [ (rtac (major RS equalityD1 RS subsetD RS emptyE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
    (rtac consI1 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 533
diff changeset
    41
qed_goalw "Pair_neq_fst" ZF.thy [Pair_def] "<a,b>=a ==> P"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
 (fn [major]=>
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
    43
  [ (rtac (consI1 RS mem_asym RS FalseE) 1),
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
    (rtac (major RS subst) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
    (rtac consI1 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 533
diff changeset
    47
qed_goalw "Pair_neq_snd" ZF.thy [Pair_def] "<a,b>=b ==> P"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
 (fn [major]=>
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
    49
  [ (rtac (consI1 RS consI2 RS mem_asym RS FalseE) 1),
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
    (rtac (major RS subst) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
    (rtac (consI1 RS consI2) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
(*** Sigma: Disjoint union of a family of sets
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
     Generalizes Cartesian product ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 533
diff changeset
    57
qed_goalw "SigmaI" ZF.thy [Sigma_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
    "[| a:A;  b:B(a) |] ==> <a,b> : Sigma(A,B)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
 (fn prems=> [ (REPEAT (resolve_tac (prems@[singletonI,UN_I]) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
(*The general elimination rule*)
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 533
diff changeset
    62
qed_goalw "SigmaE" ZF.thy [Sigma_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
    "[| c: Sigma(A,B);  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
\       !!x y.[| x:A;  y:B(x);  c=<x,y> |] ==> P \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
\    |] ==> P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
 (fn major::prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
  [ (cut_facts_tac [major] 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
    (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
(** Elimination of <a,b>:A*B -- introduces no eigenvariables **)
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 533
diff changeset
    71
qed_goal "SigmaD1" ZF.thy "<a,b> : Sigma(A,B) ==> a : A"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
 (fn [major]=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
  [ (rtac (major RS SigmaE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
    (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 533
diff changeset
    76
qed_goal "SigmaD2" ZF.thy "<a,b> : Sigma(A,B) ==> b : B(a)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
 (fn [major]=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
  [ (rtac (major RS SigmaE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
    (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
(*Also provable via 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
  rule_by_tactic (REPEAT_FIRST (etac Pair_inject ORELSE' bound_hyp_subst_tac)
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1105
diff changeset
    83
                  THEN prune_params_tac)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
      (read_instantiate [("c","<a,b>")] SigmaE);  *)
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 533
diff changeset
    85
qed_goal "SigmaE2" ZF.thy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
    "[| <a,b> : Sigma(A,B);    \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
\       [| a:A;  b:B(a) |] ==> P   \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
\    |] ==> P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
 (fn [major,minor]=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
  [ (rtac minor 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
    (rtac (major RS SigmaD1) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
    (rtac (major RS SigmaD2) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 533
diff changeset
    94
qed_goalw "Sigma_cong" ZF.thy [Sigma_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
    "[| A=A';  !!x. x:A' ==> B(x)=B'(x) |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
\    Sigma(A,B) = Sigma(A',B')"
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    97
 (fn prems=> [ (simp_tac (FOL_ss addsimps prems addcongs [RepFun_cong]) 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 533
diff changeset
    99
qed_goal "Sigma_empty1" ZF.thy "Sigma(0,B) = 0"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
 (fn _ => [ (fast_tac (lemmas_cs addIs [equalityI] addSEs [SigmaE]) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 533
diff changeset
   102
qed_goal "Sigma_empty2" ZF.thy "A*0 = 0"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
 (fn _ => [ (fast_tac (lemmas_cs addIs [equalityI] addSEs [SigmaE]) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
1105
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   105
val pair_cs = upair_cs 
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   106
    addSIs [SigmaI]
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   107
    addSEs [SigmaE2, SigmaE, Pair_inject, make_elim succ_inject,
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1105
diff changeset
   108
            Pair_neq_0, sym RS Pair_neq_0, succ_neq_0, sym RS succ_neq_0];
1105
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   109
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   110
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   111
(*** Projections: fst, snd ***)
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   112
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   113
qed_goalw "fst_conv" ZF.thy [fst_def] "fst(<a,b>) = a"
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   114
 (fn _=> 
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   115
  [ (fast_tac (pair_cs addIs [the_equality]) 1) ]);
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   116
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   117
qed_goalw "snd_conv" ZF.thy [snd_def] "snd(<a,b>) = b"
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   118
 (fn _=> 
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   119
  [ (fast_tac (pair_cs addIs [the_equality]) 1) ]);
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   120
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   121
val pair_ss = FOL_ss addsimps [fst_conv,snd_conv];
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   122
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   123
qed_goal "fst_type" ZF.thy
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   124
    "!!p. p:Sigma(A,B) ==> fst(p) : A"
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   125
 (fn _=> [ (fast_tac (pair_cs addss pair_ss) 1) ]);
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   126
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   127
qed_goal "snd_type" ZF.thy
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   128
    "!!p. p:Sigma(A,B) ==> snd(p) : B(fst(p))"
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   129
 (fn _=> [ (fast_tac (pair_cs addss pair_ss) 1) ]);
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   130
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   131
goal ZF.thy "!!a A B. a: Sigma(A,B) ==> <fst(a),snd(a)> = a";
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   132
by (etac SigmaE 1);
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   133
by (asm_simp_tac pair_ss 1);
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   134
qed "Pair_fst_snd_eq";
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   135
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   137
(*** Eliminator - split ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   138
1105
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   139
(*A META-equality, so that it applies to higher types as well...*)
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 533
diff changeset
   140
qed_goalw "split" ZF.thy [split_def]
1105
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   141
    "split(%x y.c(x,y), <a,b>) == c(a,b)"
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   142
 (fn _ => [ (simp_tac pair_ss 1),
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   143
            (rtac reflexive_thm 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   144
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 533
diff changeset
   145
qed_goal "split_type" ZF.thy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   146
    "[|  p:Sigma(A,B);   \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   147
\        !!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x,y>) \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   148
\    |] ==> split(%x y.c(x,y), p) : C(p)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   149
 (fn major::prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   150
  [ (rtac (major RS SigmaE) 1),
1105
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   151
    (asm_simp_tac (pair_ss addsimps (split::prems)) 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
1105
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   153
goalw ZF.thy [split_def]
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   154
  "!!u. u: A*B ==>   \
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   155
\       R(split(c,u)) <-> (ALL x:A. ALL y:B. u = <x,y> --> R(c(x,y)))";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   156
by (etac SigmaE 1);
1105
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   157
by (asm_simp_tac pair_ss 1);
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   158
by (fast_tac pair_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 533
diff changeset
   159
qed "expand_split";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   160
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   161
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   162
(*** split for predicates: result type o ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   163
1105
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   164
goalw ZF.thy [split_def] "!!R a b. R(a,b) ==> split(R, <a,b>)";
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   165
by (asm_simp_tac pair_ss 1);
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   166
qed "splitI";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   167
1105
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   168
val major::sigma::prems = goalw ZF.thy [split_def]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1105
diff changeset
   169
    "[| split(R,z);  z:Sigma(A,B);                      \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1105
diff changeset
   170
\       !!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
   171
\    |] ==> P";
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   172
by (rtac (sigma RS SigmaE) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   173
by (cut_facts_tac [major] 1);
1105
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   174
by (asm_full_simp_tac (pair_ss addsimps prems) 1);
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   175
qed "splitE";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   176
1105
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   177
goalw ZF.thy [split_def] "!!R a b. split(R,<a,b>) ==> R(a,b)";
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   178
by (asm_full_simp_tac pair_ss 1);
136b05aa77ed Modified proofs for (q)split, fst, snd for new
lcp
parents: 860
diff changeset
   179
qed "splitD";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   180
533
7357160bc56a ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents: 437
diff changeset
   181
7357160bc56a ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents: 437
diff changeset
   182
(*** Basic simplification for ZF; see simpdata.ML for full version ***)
7357160bc56a ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents: 437
diff changeset
   183
7357160bc56a ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents: 437
diff changeset
   184
fun prove_fun s = 
7357160bc56a ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents: 437
diff changeset
   185
    (writeln s;  prove_goal ZF.thy s
860
c8e93e8b3f55 prove_fun now includes equalityI. Added the rewrite rules
lcp
parents: 822
diff changeset
   186
       (fn prems => [ (cut_facts_tac prems 1), 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1105
diff changeset
   187
                      (fast_tac (pair_cs addSIs [equalityI]) 1) ]));
533
7357160bc56a ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents: 437
diff changeset
   188
7357160bc56a ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents: 437
diff changeset
   189
(*INCLUDED IN ZF_ss*)
7357160bc56a ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents: 437
diff changeset
   190
val mem_simps = map prove_fun
7357160bc56a ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents: 437
diff changeset
   191
 [ "a : 0             <-> False",
7357160bc56a ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents: 437
diff changeset
   192
   "a : A Un B        <-> a:A | a:B",
7357160bc56a ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents: 437
diff changeset
   193
   "a : A Int B       <-> a:A & a:B",
7357160bc56a ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents: 437
diff changeset
   194
   "a : A-B           <-> a:A & ~a:B",
7357160bc56a ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents: 437
diff changeset
   195
   "<a,b>: Sigma(A,B) <-> a:A & b:B(a)",
7357160bc56a ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents: 437
diff changeset
   196
   "a : Collect(A,P)  <-> a:A & P(a)" ];
7357160bc56a ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents: 437
diff changeset
   197
7357160bc56a ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents: 437
diff changeset
   198
goal ZF.thy "{x.x:A} = A";
7357160bc56a ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents: 437
diff changeset
   199
by (fast_tac (pair_cs addSIs [equalityI]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 533
diff changeset
   200
qed "triv_RepFun";
533
7357160bc56a ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents: 437
diff changeset
   201
860
c8e93e8b3f55 prove_fun now includes equalityI. Added the rewrite rules
lcp
parents: 822
diff changeset
   202
(*INCLUDED: should be?  And what about cons(a,b)?*)
533
7357160bc56a ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents: 437
diff changeset
   203
val bquant_simps = map prove_fun
7357160bc56a ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents: 437
diff changeset
   204
 [ "(ALL x:0.P(x)) <-> True",
7357160bc56a ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents: 437
diff changeset
   205
   "(EX  x:0.P(x)) <-> False",
7357160bc56a ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents: 437
diff changeset
   206
   "(ALL x:succ(i).P(x)) <-> P(i) & (ALL x:i.P(x))",
860
c8e93e8b3f55 prove_fun now includes equalityI. Added the rewrite rules
lcp
parents: 822
diff changeset
   207
   "(EX  x:succ(i).P(x)) <-> P(i) | (EX  x:i.P(x))",
c8e93e8b3f55 prove_fun now includes equalityI. Added the rewrite rules
lcp
parents: 822
diff changeset
   208
   "(ALL x:cons(a,B).P(x)) <-> P(a) & (ALL x:B.P(x))",
c8e93e8b3f55 prove_fun now includes equalityI. Added the rewrite rules
lcp
parents: 822
diff changeset
   209
   "(EX  x:cons(a,B).P(x)) <-> P(a) | (EX  x:B.P(x))" ];
533
7357160bc56a ZF/pair.ML: moved some definitions here from simpdata.ML
lcp
parents: 437
diff changeset
   210
860
c8e93e8b3f55 prove_fun now includes equalityI. Added the rewrite rules
lcp
parents: 822
diff changeset
   211
val Collect_simps = map prove_fun
c8e93e8b3f55 prove_fun now includes equalityI. Added the rewrite rules
lcp
parents: 822
diff changeset
   212
 [ "{x:0. P(x)} = 0",
c8e93e8b3f55 prove_fun now includes equalityI. Added the rewrite rules
lcp
parents: 822
diff changeset
   213
   "{x:A. False} = 0",
c8e93e8b3f55 prove_fun now includes equalityI. Added the rewrite rules
lcp
parents: 822
diff changeset
   214
   "{x:A. True} = A",
c8e93e8b3f55 prove_fun now includes equalityI. Added the rewrite rules
lcp
parents: 822
diff changeset
   215
   "RepFun(0,f) = 0",
c8e93e8b3f55 prove_fun now includes equalityI. Added the rewrite rules
lcp
parents: 822
diff changeset
   216
   "RepFun(succ(i),f) = cons(f(i), RepFun(i,f))",
c8e93e8b3f55 prove_fun now includes equalityI. Added the rewrite rules
lcp
parents: 822
diff changeset
   217
   "RepFun(cons(a,B),f) = cons(f(a), RepFun(B,f))" ];
c8e93e8b3f55 prove_fun now includes equalityI. Added the rewrite rules
lcp
parents: 822
diff changeset
   218
c8e93e8b3f55 prove_fun now includes equalityI. Added the rewrite rules
lcp
parents: 822
diff changeset
   219
val UnInt_simps = map prove_fun
c8e93e8b3f55 prove_fun now includes equalityI. Added the rewrite rules
lcp
parents: 822
diff changeset
   220
 [ "0 Un A = A",  "A Un 0 = A",
c8e93e8b3f55 prove_fun now includes equalityI. Added the rewrite rules
lcp
parents: 822
diff changeset
   221
   "0 Int A = 0", "A Int 0 = 0",
c8e93e8b3f55 prove_fun now includes equalityI. Added the rewrite rules
lcp
parents: 822
diff changeset
   222
   "0-A = 0",     "A-0 = A",
c8e93e8b3f55 prove_fun now includes equalityI. Added the rewrite rules
lcp
parents: 822
diff changeset
   223
   "Union(0) = 0",
c8e93e8b3f55 prove_fun now includes equalityI. Added the rewrite rules
lcp
parents: 822
diff changeset
   224
   "Union(cons(b,A)) = b Un Union(A)",
c8e93e8b3f55 prove_fun now includes equalityI. Added the rewrite rules
lcp
parents: 822
diff changeset
   225
   "Inter({b}) = b"];
c8e93e8b3f55 prove_fun now includes equalityI. Added the rewrite rules
lcp
parents: 822
diff changeset
   226