src/ZF/domrange.ML
author clasohm
Tue, 30 Jan 1996 13:42:57 +0100
changeset 1461 6bcb44e4d6e5
parent 795 d689e796d186
child 2033 639de962ded4
permissions -rw-r--r--
expanded tabs
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 795
diff changeset
     1
(*  Title:      ZF/domrange
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 795
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
0
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
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 687
diff changeset
    11
qed_goalw "converse_iff" ZF.thy [converse_def]
687
91bc4b9eee1d ZF/domrange/converse_iff: new
lcp
parents: 674
diff changeset
    12
    "<a,b>: converse(r) <-> <b,a>:r"
91bc4b9eee1d ZF/domrange/converse_iff: new
lcp
parents: 674
diff changeset
    13
 (fn _ => [ (fast_tac pair_cs 1) ]);
91bc4b9eee1d ZF/domrange/converse_iff: new
lcp
parents: 674
diff changeset
    14
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 687
diff changeset
    15
qed_goalw "converseI" ZF.thy [converse_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
    "!!a b r. <a,b>:r ==> <b,a>:converse(r)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
 (fn _ => [ (fast_tac pair_cs 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 687
diff changeset
    19
qed_goalw "converseD" ZF.thy [converse_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
    "!!a b r. <a,b> : converse(r) ==> <b,a> : r"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
 (fn _ => [ (fast_tac pair_cs 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 687
diff changeset
    23
qed_goalw "converseE" ZF.thy [converse_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
    "[| yx : converse(r);  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
\       !!x y. [| yx=<y,x>;  <x,y>:r |] ==> P \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
\    |] ==> P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
 (fn [major,minor]=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
  [ (rtac (major RS ReplaceE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
    (REPEAT (eresolve_tac [exE, conjE, minor] 1)),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
    (hyp_subst_tac 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
    (assume_tac 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
val converse_cs = pair_cs addSIs [converseI] 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 795
diff changeset
    34
                          addSEs [converseD,converseE];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
795
d689e796d186 converse_converse, converse_prod: renamed from
lcp
parents: 760
diff changeset
    36
qed_goal "converse_converse" ZF.thy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
    "!!A B r. r<=Sigma(A,B) ==> converse(converse(r)) = r"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
 (fn _ => [ (fast_tac (converse_cs addSIs [equalityI]) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 687
diff changeset
    40
qed_goal "converse_type" ZF.thy "!!A B r. r<=A*B ==> converse(r)<=B*A"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
 (fn _ => [ (fast_tac converse_cs 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
795
d689e796d186 converse_converse, converse_prod: renamed from
lcp
parents: 760
diff changeset
    43
qed_goal "converse_prod" ZF.thy "converse(A*B) = B*A"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
 (fn _ => [ (fast_tac (converse_cs addSIs [equalityI]) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 687
diff changeset
    46
qed_goal "converse_empty" ZF.thy "converse(0) = 0"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
 (fn _ => [ (fast_tac (converse_cs addSIs [equalityI]) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
(*** domain ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 687
diff changeset
    51
qed_goalw "domain_iff" ZF.thy [domain_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
    "a: domain(r) <-> (EX y. <a,y>: r)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
 (fn _=> [ (fast_tac pair_cs 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 687
diff changeset
    55
qed_goal "domainI" ZF.thy "!!a b r. <a,b>: r ==> a: domain(r)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
 (fn _ => [ (etac (exI RS (domain_iff RS iffD2)) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 687
diff changeset
    58
qed_goal "domainE" ZF.thy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
    "[| a : domain(r);  !!y. <a,y>: r ==> P |] ==> P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
  [ (rtac (domain_iff RS iffD1 RS exE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
    (REPEAT (ares_tac prems 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 687
diff changeset
    64
qed_goal "domain_subset" ZF.thy "domain(Sigma(A,B)) <= A"
536
5fbfa997f1b0 ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents: 14
diff changeset
    65
 (fn _ => [ (rtac subsetI 1), (etac domainE 1), (etac SigmaD1 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
(*** range ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 687
diff changeset
    70
qed_goalw "rangeI" ZF.thy [range_def] "!!a b r.<a,b>: r ==> b : range(r)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
 (fn _ => [ (etac (converseI RS domainI) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 687
diff changeset
    73
qed_goalw "rangeE" ZF.thy [range_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
    "[| b : range(r);  !!x. <x,b>: r ==> P |] ==> P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
 (fn major::prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
  [ (rtac (major RS domainE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
    (resolve_tac prems 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
    (etac converseD 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 687
diff changeset
    80
qed_goalw "range_subset" ZF.thy [range_def] "range(A*B) <= B"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
 (fn _ =>
795
d689e796d186 converse_converse, converse_prod: renamed from
lcp
parents: 760
diff changeset
    82
  [ (rtac (converse_prod RS ssubst) 1),
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
    (rtac domain_subset 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
(*** field ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 687
diff changeset
    88
qed_goalw "fieldI1" ZF.thy [field_def] "<a,b>: r ==> a : field(r)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
 (fn [prem]=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
  [ (rtac (prem RS domainI RS UnI1) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 687
diff changeset
    92
qed_goalw "fieldI2" ZF.thy [field_def] "<a,b>: r ==> b : field(r)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
 (fn [prem]=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
  [ (rtac (prem RS rangeI RS UnI2) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 687
diff changeset
    96
qed_goalw "fieldCI" ZF.thy [field_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
    "(~ <c,a>:r ==> <a,b>: r) ==> a : field(r)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
 (fn [prem]=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
  [ (rtac (prem RS domainI RS UnCI) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
    (swap_res_tac [rangeI] 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
    (etac notnotD 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 687
diff changeset
   103
qed_goalw "fieldE" ZF.thy [field_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
     "[| a : field(r);  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
\        !!x. <a,x>: r ==> P;  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
\        !!x. <x,a>: r ==> P        |] ==> P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
 (fn major::prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
  [ (rtac (major RS UnE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
    (REPEAT (eresolve_tac (prems@[domainE,rangeE]) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 687
diff changeset
   111
qed_goal "field_subset" ZF.thy "field(A*B) <= A Un B"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
 (fn _ => [ (fast_tac (pair_cs addIs  [fieldCI] addSEs [fieldE]) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 687
diff changeset
   114
qed_goalw "domain_subset_field" ZF.thy [field_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
    "domain(r) <= field(r)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
 (fn _ => [ (rtac Un_upper1 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 687
diff changeset
   118
qed_goalw "range_subset_field" ZF.thy [field_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
    "range(r) <= field(r)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
 (fn _ => [ (rtac Un_upper2 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 687
diff changeset
   122
qed_goal "domain_times_range" ZF.thy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
    "!!A B r. r <= Sigma(A,B) ==> r <= domain(r)*range(r)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
 (fn _ => [ (fast_tac (pair_cs addIs [domainI,rangeI]) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 687
diff changeset
   126
qed_goal "field_times_field" ZF.thy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
    "!!A B r. r <= Sigma(A,B) ==> r <= field(r)*field(r)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
 (fn _ => [ (fast_tac (pair_cs addIs [fieldI1,fieldI2]) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
(*** Image of a set under a function/relation ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 687
diff changeset
   133
qed_goalw "image_iff" ZF.thy [image_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
    "b : r``A <-> (EX x:A. <x,b>:r)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   135
 (fn _ => [ fast_tac (pair_cs addIs [rangeI]) 1 ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 687
diff changeset
   137
qed_goal "image_singleton_iff" ZF.thy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   138
    "b : r``{a} <-> <a,b>:r"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   139
 (fn _ => [ rtac (image_iff RS iff_trans) 1,
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 795
diff changeset
   140
            fast_tac pair_cs 1 ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   141
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 687
diff changeset
   142
qed_goalw "imageI" ZF.thy [image_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   143
    "!!a b r. [| <a,b>: r;  a:A |] ==> b : r``A"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   144
 (fn _ => [ (REPEAT (ares_tac [CollectI,rangeI,bexI] 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   145
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 687
diff changeset
   146
qed_goalw "imageE" ZF.thy [image_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   147
    "[| b: r``A;  !!x.[| <x,b>: r;  x:A |] ==> P |] ==> P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   148
 (fn major::prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   149
  [ (rtac (major RS CollectE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   150
    (REPEAT (etac bexE 1 ORELSE ares_tac prems 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   151
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 687
diff changeset
   152
qed_goal "image_subset" ZF.thy
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 0
diff changeset
   153
    "!!A B r. r <= A*B ==> r``C <= B"
674
41b59e4c78c4 ZF/domrange/image_subset: tidied
lcp
parents: 536
diff changeset
   154
 (fn _ => [ (fast_tac (pair_cs addSEs [imageE]) 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   155
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   156
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   157
(*** Inverse image of a set under a function/relation ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   158
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 687
diff changeset
   159
qed_goalw "vimage_iff" ZF.thy [vimage_def,image_def,converse_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   160
    "a : r-``B <-> (EX y:B. <a,y>:r)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   161
 (fn _ => [ fast_tac (pair_cs addIs [rangeI]) 1 ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   162
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 687
diff changeset
   163
qed_goal "vimage_singleton_iff" ZF.thy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   164
    "a : r-``{b} <-> <a,b>:r"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   165
 (fn _ => [ rtac (vimage_iff RS iff_trans) 1,
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 795
diff changeset
   166
            fast_tac pair_cs 1 ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   167
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 687
diff changeset
   168
qed_goalw "vimageI" ZF.thy [vimage_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   169
    "!!A B r. [| <a,b>: r;  b:B |] ==> a : r-``B"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   170
 (fn _ => [ (REPEAT (ares_tac [converseI RS imageI] 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   171
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 687
diff changeset
   172
qed_goalw "vimageE" ZF.thy [vimage_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   173
    "[| a: r-``B;  !!x.[| <a,x>: r;  x:B |] ==> P |] ==> P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   174
 (fn major::prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   175
  [ (rtac (major RS imageE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   176
    (REPEAT (etac converseD 1 ORELSE ares_tac prems 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   177
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 687
diff changeset
   178
qed_goalw "vimage_subset" ZF.thy [vimage_def]
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 0
diff changeset
   179
    "!!A B r. r <= A*B ==> r-``C <= A"
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 0
diff changeset
   180
 (fn _ => [ (etac (converse_type RS image_subset) 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   181
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   182
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   183
(** Theorem-proving for ZF set theory **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   184
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   185
val ZF_cs = pair_cs 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   186
    addSIs [converseI]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   187
    addIs  [imageI, vimageI, domainI, rangeI, fieldCI]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   188
    addSEs [imageE, vimageE, domainE, rangeE, fieldE, converseD, converseE];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   189
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   190
val eq_cs = ZF_cs addSIs [equalityI];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   191
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   192
(** The Union of a set of relations is a relation -- Lemma for fun_Union **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   193
goal ZF.thy "!!S. (ALL x:S. EX A B. x <= A*B) ==>  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   194
\                 Union(S) <= domain(Union(S)) * range(Union(S))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   195
by (fast_tac ZF_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 687
diff changeset
   196
qed "rel_Union";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   197
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   198
(** The Union of 2 relations is a relation (Lemma for fun_Un)  **)
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 687
diff changeset
   199
qed_goal "rel_Un" ZF.thy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   200
    "!!r s. [| r <= A*B;  s <= C*D |] ==> (r Un s) <= (A Un C) * (B Un D)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   201
 (fn _ => [ (fast_tac ZF_cs 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   202
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   203