src/ZF/domrange.ML
author wenzelm
Sat, 15 Apr 2000 15:00:57 +0200
changeset 8717 20c42415c07d
parent 5325 f7a5e06adea1
child 9180 3bda56c0d70d
permissions -rw-r--r--
plain ASCII;
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
5325
f7a5e06adea1 Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents: 5202
diff changeset
    11
qed_goalw "converse_iff" thy [converse_def]
687
91bc4b9eee1d ZF/domrange/converse_iff: new
lcp
parents: 674
diff changeset
    12
    "<a,b>: converse(r) <-> <b,a>:r"
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
    13
 (fn _ => [ (Blast_tac 1) ]);
687
91bc4b9eee1d ZF/domrange/converse_iff: new
lcp
parents: 674
diff changeset
    14
5325
f7a5e06adea1 Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents: 5202
diff changeset
    15
qed_goalw "converseI" thy [converse_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
    "!!a b r. <a,b>:r ==> <b,a>:converse(r)"
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
    17
 (fn _ => [ (Blast_tac 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
5325
f7a5e06adea1 Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents: 5202
diff changeset
    19
qed_goalw "converseD" thy [converse_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
    "!!a b r. <a,b> : converse(r) ==> <b,a> : r"
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
    21
 (fn _ => [ (Blast_tac 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
5325
f7a5e06adea1 Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents: 5202
diff changeset
    23
qed_goalw "converseE" 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
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2033
diff changeset
    33
Addsimps [converse_iff];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2033
diff changeset
    34
AddSIs [converseI];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2033
diff changeset
    35
AddSEs [converseD,converseE];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
5325
f7a5e06adea1 Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents: 5202
diff changeset
    37
qed_goal "converse_converse" thy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
    "!!A B r. r<=Sigma(A,B) ==> converse(converse(r)) = r"
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
    39
 (fn _ => [ (Blast_tac 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
5325
f7a5e06adea1 Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents: 5202
diff changeset
    41
qed_goal "converse_type" thy "!!A B r. r<=A*B ==> converse(r)<=B*A"
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
    42
 (fn _ => [ (Blast_tac 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
5325
f7a5e06adea1 Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents: 5202
diff changeset
    44
qed_goal "converse_prod" thy "converse(A*B) = B*A"
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
    45
 (fn _ => [ (Blast_tac 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
5325
f7a5e06adea1 Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents: 5202
diff changeset
    47
qed_goal "converse_empty" thy "converse(0) = 0"
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
    48
 (fn _ => [ (Blast_tac 1) ]);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2033
diff changeset
    49
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2033
diff changeset
    50
Addsimps [converse_prod, converse_empty];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
5325
f7a5e06adea1 Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents: 5202
diff changeset
    52
val converse_subset_iff = prove_goal thy
5202
084ceb3844f5 A few new lemmas by Mark Staples
paulson
parents: 4091
diff changeset
    53
  "!!z. A <= Sigma(X,Y) ==> converse(A) <= converse(B) <-> A <= B"
084ceb3844f5 A few new lemmas by Mark Staples
paulson
parents: 4091
diff changeset
    54
 (fn _=> [ (Blast_tac 1) ]);
084ceb3844f5 A few new lemmas by Mark Staples
paulson
parents: 4091
diff changeset
    55
084ceb3844f5 A few new lemmas by Mark Staples
paulson
parents: 4091
diff changeset
    56
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
(*** domain ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
5325
f7a5e06adea1 Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents: 5202
diff changeset
    59
qed_goalw "domain_iff" thy [domain_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
    "a: domain(r) <-> (EX y. <a,y>: r)"
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
    61
 (fn _=> [ (Blast_tac 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
5325
f7a5e06adea1 Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents: 5202
diff changeset
    63
qed_goal "domainI" thy "!!a b r. <a,b>: r ==> a: domain(r)"
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2033
diff changeset
    64
 (fn _=> [ (etac (exI RS (domain_iff RS iffD2)) 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
5325
f7a5e06adea1 Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents: 5202
diff changeset
    66
qed_goal "domainE" thy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
    "[| a : domain(r);  !!y. <a,y>: r ==> P |] ==> P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
  [ (rtac (domain_iff RS iffD1 RS exE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
    (REPEAT (ares_tac prems 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2033
diff changeset
    72
AddIs  [domainI];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2033
diff changeset
    73
AddSEs [domainE];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
5325
f7a5e06adea1 Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents: 5202
diff changeset
    75
qed_goal "domain_subset" thy "domain(Sigma(A,B)) <= A"
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
    76
 (fn _=> [ (Blast_tac 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
(*** range ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
5325
f7a5e06adea1 Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents: 5202
diff changeset
    80
qed_goalw "rangeI" thy [range_def] "!!a b r.<a,b>: r ==> b : range(r)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
 (fn _ => [ (etac (converseI RS domainI) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
5325
f7a5e06adea1 Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents: 5202
diff changeset
    83
qed_goalw "rangeE" thy [range_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
    "[| b : range(r);  !!x. <x,b>: r ==> P |] ==> P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
 (fn major::prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
  [ (rtac (major RS domainE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
    (resolve_tac prems 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
    (etac converseD 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2033
diff changeset
    90
AddIs  [rangeI];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2033
diff changeset
    91
AddSEs [rangeE];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2033
diff changeset
    92
5325
f7a5e06adea1 Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents: 5202
diff changeset
    93
qed_goalw "range_subset" thy [range_def] "range(A*B) <= B"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
 (fn _ =>
2033
639de962ded4 Ran expandshort; used stac instead of ssubst
paulson
parents: 1461
diff changeset
    95
  [ (stac converse_prod 1),
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
    (rtac domain_subset 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
(*** field ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
5325
f7a5e06adea1 Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents: 5202
diff changeset
   101
qed_goalw "fieldI1" thy [field_def] "!!r. <a,b>: r ==> a : field(r)"
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   102
 (fn _ => [ (Blast_tac 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
5325
f7a5e06adea1 Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents: 5202
diff changeset
   104
qed_goalw "fieldI2" thy [field_def] "!!r. <a,b>: r ==> b : field(r)"
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   105
 (fn _ => [ (Blast_tac 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
5325
f7a5e06adea1 Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents: 5202
diff changeset
   107
qed_goalw "fieldCI" thy [field_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
    "(~ <c,a>:r ==> <a,b>: r) ==> a : field(r)"
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 2877
diff changeset
   109
 (fn [prem]=> [ (blast_tac (claset() addIs [prem]) 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
5325
f7a5e06adea1 Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents: 5202
diff changeset
   111
qed_goalw "fieldE" thy [field_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
     "[| a : field(r);  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
\        !!x. <a,x>: r ==> P;  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
\        !!x. <x,a>: r ==> P        |] ==> P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
 (fn major::prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
  [ (rtac (major RS UnE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
    (REPEAT (eresolve_tac (prems@[domainE,rangeE]) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2033
diff changeset
   119
AddIs  [fieldCI];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2033
diff changeset
   120
AddSEs [fieldE];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
5325
f7a5e06adea1 Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents: 5202
diff changeset
   122
qed_goal "field_subset" thy "field(A*B) <= A Un B"
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   123
 (fn _ => [ (Blast_tac 1) ]);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2033
diff changeset
   124
5325
f7a5e06adea1 Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents: 5202
diff changeset
   125
qed_goalw "domain_subset_field" thy [field_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
    "domain(r) <= field(r)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
 (fn _ => [ (rtac Un_upper1 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
5325
f7a5e06adea1 Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents: 5202
diff changeset
   129
qed_goalw "range_subset_field" thy [field_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
    "range(r) <= field(r)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
 (fn _ => [ (rtac Un_upper2 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
5325
f7a5e06adea1 Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents: 5202
diff changeset
   133
qed_goal "domain_times_range" thy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
    "!!A B r. r <= Sigma(A,B) ==> r <= domain(r)*range(r)"
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   135
 (fn _ => [ (Blast_tac 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
5325
f7a5e06adea1 Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents: 5202
diff changeset
   137
qed_goal "field_times_field" thy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   138
    "!!A B r. r <= Sigma(A,B) ==> r <= field(r)*field(r)"
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   139
 (fn _ => [ (Blast_tac 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   140
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   141
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   142
(*** Image of a set under a function/relation ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   143
5325
f7a5e06adea1 Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents: 5202
diff changeset
   144
qed_goalw "image_iff" thy [image_def] "b : r``A <-> (EX x:A. <x,b>:r)"
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   145
 (fn _ => [ (Blast_tac 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   146
5325
f7a5e06adea1 Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents: 5202
diff changeset
   147
qed_goal "image_singleton_iff" thy    "b : r``{a} <-> <a,b>:r"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   148
 (fn _ => [ rtac (image_iff RS iff_trans) 1,
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   149
            Blast_tac 1 ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   150
5325
f7a5e06adea1 Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents: 5202
diff changeset
   151
qed_goalw "imageI" thy [image_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
    "!!a b r. [| <a,b>: r;  a:A |] ==> b : r``A"
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   153
 (fn _ => [ (Blast_tac 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   154
5325
f7a5e06adea1 Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents: 5202
diff changeset
   155
qed_goalw "imageE" thy [image_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   156
    "[| b: r``A;  !!x.[| <x,b>: r;  x:A |] ==> P |] ==> P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   157
 (fn major::prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   158
  [ (rtac (major RS CollectE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   159
    (REPEAT (etac bexE 1 ORELSE ares_tac prems 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   160
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2033
diff changeset
   161
AddIs  [imageI];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2033
diff changeset
   162
AddSEs [imageE];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2033
diff changeset
   163
5325
f7a5e06adea1 Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents: 5202
diff changeset
   164
qed_goal "image_subset" thy "!!A B r. r <= A*B ==> r``C <= B"
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   165
 (fn _ => [ (Blast_tac 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   166
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   167
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   168
(*** Inverse image of a set under a function/relation ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   169
5325
f7a5e06adea1 Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents: 5202
diff changeset
   170
qed_goalw "vimage_iff" thy [vimage_def,image_def,converse_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   171
    "a : r-``B <-> (EX y:B. <a,y>:r)"
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   172
 (fn _ => [ (Blast_tac 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   173
5325
f7a5e06adea1 Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents: 5202
diff changeset
   174
qed_goal "vimage_singleton_iff" thy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   175
    "a : r-``{b} <-> <a,b>:r"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   176
 (fn _ => [ rtac (vimage_iff RS iff_trans) 1,
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   177
            Blast_tac 1 ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   178
5325
f7a5e06adea1 Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents: 5202
diff changeset
   179
qed_goalw "vimageI" thy [vimage_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   180
    "!!A B r. [| <a,b>: r;  b:B |] ==> a : r-``B"
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   181
 (fn _ => [ (Blast_tac 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   182
5325
f7a5e06adea1 Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents: 5202
diff changeset
   183
qed_goalw "vimageE" thy [vimage_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   184
    "[| a: r-``B;  !!x.[| <a,x>: r;  x:B |] ==> P |] ==> P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   185
 (fn major::prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   186
  [ (rtac (major RS imageE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   187
    (REPEAT (etac converseD 1 ORELSE ares_tac prems 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   188
5325
f7a5e06adea1 Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents: 5202
diff changeset
   189
qed_goalw "vimage_subset" thy [vimage_def]
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 0
diff changeset
   190
    "!!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
   191
 (fn _ => [ (etac (converse_type RS image_subset) 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   192
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   193
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   194
(** Theorem-proving for ZF set theory **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   195
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2033
diff changeset
   196
AddIs  [vimageI];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2033
diff changeset
   197
AddSEs [vimageE];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2033
diff changeset
   198
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 2877
diff changeset
   199
val ZF_cs = claset() delrules [equalityI];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   200
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   201
(** The Union of a set of relations is a relation -- Lemma for fun_Union **)
5325
f7a5e06adea1 Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents: 5202
diff changeset
   202
Goal "(ALL x:S. EX A B. x <= A*B) ==>  \
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   203
\                 Union(S) <= domain(Union(S)) * range(Union(S))";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   204
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 687
diff changeset
   205
qed "rel_Union";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   206
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   207
(** The Union of 2 relations is a relation (Lemma for fun_Un)  **)
5325
f7a5e06adea1 Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents: 5202
diff changeset
   208
qed_goal "rel_Un" thy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   209
    "!!r s. [| r <= A*B;  s <= C*D |] ==> (r Un s) <= (A Un C) * (B Un D)"
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   210
 (fn _ => [ (Blast_tac 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   211
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   212
5325
f7a5e06adea1 Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents: 5202
diff changeset
   213
Goal "[| <a,c> : r; c~=b |] ==> domain(r-{<a,b>}) = domain(r)";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   214
by (Blast_tac 1);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2033
diff changeset
   215
qed "domain_Diff_eq";
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2033
diff changeset
   216
5325
f7a5e06adea1 Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents: 5202
diff changeset
   217
Goal "[| <c,b> : r; c~=a |] ==> range(r-{<a,b>}) = range(r)";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2493
diff changeset
   218
by (Blast_tac 1);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2033
diff changeset
   219
qed "range_Diff_eq";
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2033
diff changeset
   220