src/ZF/domrange.ML
author clasohm
Thu, 16 Sep 1993 12:20:38 +0200
changeset 0 a5a9c433f639
child 14 1c0926788772
permissions -rw-r--r--
Initial revision
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	ZF/domrange
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1991  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
Converse, domain, range of a relation or function
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
(*** converse ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
val converseI = prove_goalw ZF.thy [converse_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
    "!!a b r. <a,b>:r ==> <b,a>:converse(r)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
 (fn _ => [ (fast_tac pair_cs 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
val converseD = prove_goalw ZF.thy [converse_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
    "!!a b r. <a,b> : converse(r) ==> <b,a> : r"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
 (fn _ => [ (fast_tac pair_cs 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
val converseE = prove_goalw ZF.thy [converse_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
    "[| yx : converse(r);  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
\       !!x y. [| yx=<y,x>;  <x,y>:r |] ==> P \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
\    |] ==> P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
 (fn [major,minor]=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
  [ (rtac (major RS ReplaceE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
    (REPEAT (eresolve_tac [exE, conjE, minor] 1)),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
    (hyp_subst_tac 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
    (assume_tac 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
val converse_cs = pair_cs addSIs [converseI] 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
			  addSEs [converseD,converseE];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
val converse_of_converse = prove_goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
    "!!A B r. r<=Sigma(A,B) ==> converse(converse(r)) = r"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
 (fn _ => [ (fast_tac (converse_cs addSIs [equalityI]) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
val converse_type = prove_goal ZF.thy "!!A B r. r<=A*B ==> converse(r)<=B*A"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
 (fn _ => [ (fast_tac converse_cs 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
val converse_of_prod = prove_goal ZF.thy "converse(A*B) = B*A"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
 (fn _ => [ (fast_tac (converse_cs addSIs [equalityI]) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
val converse_empty = prove_goal ZF.thy "converse(0) = 0"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
 (fn _ => [ (fast_tac (converse_cs addSIs [equalityI]) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
(*** domain ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
val domain_iff = prove_goalw ZF.thy [domain_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
    "a: domain(r) <-> (EX y. <a,y>: r)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
 (fn _=> [ (fast_tac pair_cs 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
val domainI = prove_goal ZF.thy "!!a b r. <a,b>: r ==> a: domain(r)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
 (fn _ => [ (etac (exI RS (domain_iff RS iffD2)) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
val domainE = prove_goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
    "[| a : domain(r);  !!y. <a,y>: r ==> P |] ==> P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
  [ (rtac (domain_iff RS iffD1 RS exE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
    (REPEAT (ares_tac prems 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
val domain_of_prod = prove_goal ZF.thy "!!A B. b:B ==> domain(A*B) = A"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
 (fn _ =>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
  [ (REPEAT (eresolve_tac [domainE,SigmaE2] 1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
     ORELSE ares_tac [domainI,equalityI,subsetI,SigmaI] 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
val domain_empty = prove_goal ZF.thy "domain(0) = 0"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
 (fn _ =>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
  [ (REPEAT (eresolve_tac [domainE,emptyE] 1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
     ORELSE ares_tac [equalityI,subsetI] 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
val domain_subset = prove_goal ZF.thy "domain(Sigma(A,B)) <= A"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
 (fn _ =>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
  [ (rtac subsetI 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
    (etac domainE 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
    (etac SigmaD1 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
(*** range ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
val rangeI = prove_goalw ZF.thy [range_def] "!!a b r.<a,b>: r ==> b : range(r)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
 (fn _ => [ (etac (converseI RS domainI) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
val rangeE = prove_goalw ZF.thy [range_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
    "[| b : range(r);  !!x. <x,b>: r ==> P |] ==> P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
 (fn major::prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
  [ (rtac (major RS domainE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
    (resolve_tac prems 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
    (etac converseD 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
val range_of_prod = prove_goalw ZF.thy [range_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
    "!!a A B. a:A ==> range(A*B) = B"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
 (fn _ =>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
  [ (rtac (converse_of_prod RS ssubst) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
    (etac domain_of_prod 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
val range_empty = prove_goalw ZF.thy [range_def] "range(0) = 0"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
 (fn _ =>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
  [ (rtac (converse_empty RS ssubst) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
    (rtac domain_empty 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
val range_subset = prove_goalw ZF.thy [range_def] "range(A*B) <= B"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
 (fn _ =>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
  [ (rtac (converse_of_prod RS ssubst) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
    (rtac domain_subset 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
(*** field ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
val fieldI1 = prove_goalw ZF.thy [field_def] "<a,b>: r ==> a : field(r)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
 (fn [prem]=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
  [ (rtac (prem RS domainI RS UnI1) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
val fieldI2 = prove_goalw ZF.thy [field_def] "<a,b>: r ==> b : field(r)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
 (fn [prem]=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
  [ (rtac (prem RS rangeI RS UnI2) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
val fieldCI = prove_goalw ZF.thy [field_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
    "(~ <c,a>:r ==> <a,b>: r) ==> a : field(r)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
 (fn [prem]=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
  [ (rtac (prem RS domainI RS UnCI) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
    (swap_res_tac [rangeI] 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
    (etac notnotD 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
val fieldE = prove_goalw ZF.thy [field_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
     "[| a : field(r);  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
\        !!x. <a,x>: r ==> P;  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
\        !!x. <x,a>: r ==> P        |] ==> P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
 (fn major::prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
  [ (rtac (major RS UnE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
    (REPEAT (eresolve_tac (prems@[domainE,rangeE]) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
val field_of_prod = prove_goal ZF.thy "field(A*A) = A"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
 (fn _ =>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
  [ (fast_tac (pair_cs addIs  [fieldCI,equalityI] addSEs [fieldE]) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   135
val field_subset = prove_goal ZF.thy "field(A*B) <= A Un B"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
 (fn _ => [ (fast_tac (pair_cs addIs  [fieldCI] addSEs [fieldE]) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   137
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   138
val domain_subset_field = prove_goalw ZF.thy [field_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   139
    "domain(r) <= field(r)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   140
 (fn _ => [ (rtac Un_upper1 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   141
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   142
val range_subset_field = prove_goalw ZF.thy [field_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   143
    "range(r) <= field(r)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   144
 (fn _ => [ (rtac Un_upper2 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   145
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   146
val domain_times_range = prove_goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   147
    "!!A B r. r <= Sigma(A,B) ==> r <= domain(r)*range(r)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   148
 (fn _ => [ (fast_tac (pair_cs addIs [domainI,rangeI]) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   149
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   150
val field_times_field = prove_goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   151
    "!!A B r. r <= Sigma(A,B) ==> r <= field(r)*field(r)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
 (fn _ => [ (fast_tac (pair_cs addIs [fieldI1,fieldI2]) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   153
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   154
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   155
(*** Image of a set under a function/relation ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   156
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   157
val image_iff = prove_goalw ZF.thy [image_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   158
    "b : r``A <-> (EX x:A. <x,b>:r)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   159
 (fn _ => [ fast_tac (pair_cs addIs [rangeI]) 1 ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   160
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   161
val image_singleton_iff = prove_goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   162
    "b : r``{a} <-> <a,b>:r"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   163
 (fn _ => [ rtac (image_iff RS iff_trans) 1,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   164
	    fast_tac pair_cs 1 ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   165
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   166
val imageI = prove_goalw ZF.thy [image_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   167
    "!!a b r. [| <a,b>: r;  a:A |] ==> b : r``A"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   168
 (fn _ => [ (REPEAT (ares_tac [CollectI,rangeI,bexI] 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   169
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   170
val imageE = prove_goalw ZF.thy [image_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   171
    "[| b: r``A;  !!x.[| <x,b>: r;  x:A |] ==> P |] ==> P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   172
 (fn major::prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   173
  [ (rtac (major RS CollectE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   174
    (REPEAT (etac bexE 1 ORELSE ares_tac prems 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   175
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   176
val image_subset = prove_goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   177
    "!!A B r. [| r <= A*B;  C<=A |] ==> r``C <= B"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   178
 (fn _ =>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   179
  [ (rtac subsetI 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   180
    (REPEAT (eresolve_tac [asm_rl, imageE, subsetD RS SigmaD2] 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   181
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   182
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   183
(*** Inverse image of a set under a function/relation ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   184
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   185
val vimage_iff = prove_goalw ZF.thy [vimage_def,image_def,converse_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   186
    "a : r-``B <-> (EX y:B. <a,y>:r)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   187
 (fn _ => [ fast_tac (pair_cs addIs [rangeI]) 1 ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   188
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   189
val vimage_singleton_iff = prove_goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   190
    "a : r-``{b} <-> <a,b>:r"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   191
 (fn _ => [ rtac (vimage_iff RS iff_trans) 1,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   192
	    fast_tac pair_cs 1 ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   193
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   194
val vimageI = prove_goalw ZF.thy [vimage_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   195
    "!!A B r. [| <a,b>: r;  b:B |] ==> a : r-``B"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   196
 (fn _ => [ (REPEAT (ares_tac [converseI RS imageI] 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   197
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   198
val vimageE = prove_goalw ZF.thy [vimage_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   199
    "[| a: r-``B;  !!x.[| <a,x>: r;  x:B |] ==> P |] ==> P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   200
 (fn major::prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   201
  [ (rtac (major RS imageE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   202
    (REPEAT (etac converseD 1 ORELSE ares_tac prems 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   203
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   204
val vimage_subset = prove_goalw ZF.thy [vimage_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   205
    "!!A B r. [| r <= A*B;  C<=B |] ==> r-``C <= A"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   206
 (fn _ => [ (REPEAT (ares_tac [converse_type RS image_subset] 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   207
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   208
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   209
(** Theorem-proving for ZF set theory **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   210
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   211
val ZF_cs = pair_cs 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   212
    addSIs [converseI]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   213
    addIs  [imageI, vimageI, domainI, rangeI, fieldCI]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   214
    addSEs [imageE, vimageE, domainE, rangeE, fieldE, converseD, converseE];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   215
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   216
val eq_cs = ZF_cs addSIs [equalityI];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   217
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   218
(** The Union of a set of relations is a relation -- Lemma for fun_Union **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   219
goal ZF.thy "!!S. (ALL x:S. EX A B. x <= A*B) ==>  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   220
\                 Union(S) <= domain(Union(S)) * range(Union(S))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   221
by (fast_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   222
val rel_Union = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   223
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   224
(** The Union of 2 relations is a relation (Lemma for fun_Un)  **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   225
val rel_Un = prove_goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   226
    "!!r s. [| r <= A*B;  s <= C*D |] ==> (r Un s) <= (A Un C) * (B Un D)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   227
 (fn _ => [ (fast_tac ZF_cs 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   228
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   229