src/ZF/subset.ML
author paulson
Fri, 16 Feb 1996 18:00:47 +0100
changeset 1512 ce37c64244c0
parent 1461 6bcb44e4d6e5
child 1745 6040ec66e1e4
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: 782
diff changeset
     1
(*  Title:      ZF/subset
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 782
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
Derived rules involving subsets
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
Union and Intersection as lattice operations
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
(*** cons ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 689
diff changeset
    12
qed_goal "cons_subsetI" ZF.thy "[| a:C; B<=C |] ==> cons(a,B) <= C"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
  [ (cut_facts_tac prems 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
    (REPEAT (ares_tac [subsetI] 1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
     ORELSE eresolve_tac  [consE,ssubst,subsetD] 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 689
diff changeset
    18
qed_goal "subset_consI" ZF.thy "B <= cons(a,B)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
 (fn _=> [ (rtac subsetI 1), (etac consI2 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
(*Useful for rewriting!*)
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 689
diff changeset
    22
qed_goal "cons_subset_iff" ZF.thy "cons(a,B)<=C <-> a:C & B<=C"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
 (fn _=> [ (fast_tac upair_cs 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
(*A safe special case of subset elimination, adding no new variables 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
  [| cons(a,B) <= C; [| a : C; B <= C |] ==> R |] ==> R *)
782
200a16083201 added bind_thm for theorems defined by "standard ..."
clasohm
parents: 760
diff changeset
    27
bind_thm ("cons_subsetE", (cons_subset_iff RS iffD1 RS conjE));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 689
diff changeset
    29
qed_goal "subset_empty_iff" ZF.thy "A<=0 <-> A=0"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
 (fn _=> [ (fast_tac (upair_cs addIs [equalityI]) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 689
diff changeset
    32
qed_goal "subset_cons_iff" ZF.thy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
    "C<=cons(a,B) <-> C<=B | (a:C & C-{a} <= B)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
 (fn _=> [ (fast_tac upair_cs 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
(*** succ ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 689
diff changeset
    38
qed_goal "subset_succI" ZF.thy "i <= succ(i)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
 (fn _=> [ (rtac subsetI 1), (etac succI2 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
(*But if j is an ordinal or is transitive, then i:j implies i<=j! 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
  See ordinal/Ord_succ_subsetI*)
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 689
diff changeset
    43
qed_goalw "succ_subsetI" ZF.thy [succ_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
    "[| i:j;  i<=j |] ==> succ(i)<=j"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
  [ (REPEAT (ares_tac (prems@[cons_subsetI]) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 689
diff changeset
    48
qed_goalw "succ_subsetE" ZF.thy [succ_def] 
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
    "[| succ(i) <= j;  [| i:j;  i<=j |] ==> P \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
\    |] ==> P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
 (fn major::prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
  [ (rtac (major RS cons_subsetE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
    (REPEAT (ares_tac prems 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
(*** singletons ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 689
diff changeset
    57
qed_goal "singleton_subsetI" ZF.thy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
    "a:C ==> {a} <= C"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
  [ (REPEAT (resolve_tac (prems@[cons_subsetI,empty_subsetI]) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 689
diff changeset
    62
qed_goal "singleton_subsetD" ZF.thy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
    "{a} <= C  ==>  a:C"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
 (fn prems=> [ (REPEAT (ares_tac (prems@[cons_subsetE]) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
(*** Big Union -- least upper bound of a set  ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 689
diff changeset
    68
qed_goal "Union_subset_iff" ZF.thy "Union(A) <= C <-> (ALL x:A. x <= C)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
 (fn _ => [ fast_tac upair_cs 1 ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 689
diff changeset
    71
qed_goal "Union_upper" ZF.thy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
    "B:A ==> B <= Union(A)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
 (fn prems=> [ (REPEAT (ares_tac (prems@[subsetI,UnionI]) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 689
diff changeset
    75
qed_goal "Union_least" ZF.thy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
    "[| !!x. x:A ==> x<=C |] ==> Union(A) <= C"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
 (fn [prem]=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
  [ (rtac (ballI RS (Union_subset_iff RS iffD2)) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
    (etac prem 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
(*** Union of a family of sets  ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
goal ZF.thy "A <= (UN i:I. B(i)) <-> A = (UN i:I. A Int B(i))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
by (fast_tac (upair_cs addSIs [equalityI] addSEs [equalityE]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 689
diff changeset
    85
qed "subset_UN_iff_eq";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 689
diff changeset
    87
qed_goal "UN_subset_iff" ZF.thy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
     "(UN x:A.B(x)) <= C <-> (ALL x:A. B(x) <= C)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
 (fn _ => [ fast_tac upair_cs 1 ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 689
diff changeset
    91
qed_goal "UN_upper" ZF.thy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
    "!!x A. x:A ==> B(x) <= (UN x:A.B(x))"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
 (fn _ => [ etac (RepFunI RS Union_upper) 1 ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 689
diff changeset
    95
qed_goal "UN_least" ZF.thy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
    "[| !!x. x:A ==> B(x)<=C |] ==> (UN x:A.B(x)) <= C"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
 (fn [prem]=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
  [ (rtac (ballI RS (UN_subset_iff RS iffD2)) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
    (etac prem 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
(*** Big Intersection -- greatest lower bound of a nonempty set ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 689
diff changeset
   104
qed_goal "Inter_subset_iff" ZF.thy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
     "!!a A. a: A  ==>  C <= Inter(A) <-> (ALL x:A. C <= x)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
 (fn _ => [ fast_tac upair_cs 1 ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 689
diff changeset
   108
qed_goal "Inter_lower" ZF.thy "B:A ==> Inter(A) <= B"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
  [ (REPEAT (resolve_tac (prems@[subsetI]) 1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
     ORELSE etac InterD 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 689
diff changeset
   113
qed_goal "Inter_greatest" ZF.thy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
    "[| a:A;  !!x. x:A ==> C<=x |] ==> C <= Inter(A)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
 (fn [prem1,prem2]=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
  [ (rtac ([prem1, ballI] MRS (Inter_subset_iff RS iffD2)) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
    (etac prem2 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
(*** Intersection of a family of sets  ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 689
diff changeset
   121
qed_goal "INT_lower" ZF.thy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
    "x:A ==> (INT x:A.B(x)) <= B(x)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
 (fn [prem] =>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
  [ rtac (prem RS RepFunI RS Inter_lower) 1 ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 689
diff changeset
   126
qed_goal "INT_greatest" ZF.thy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
    "[| a:A;  !!x. x:A ==> C<=B(x) |] ==> C <= (INT x:A.B(x))"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
 (fn [nonempty,prem] =>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
  [ rtac (nonempty RS RepFunI RS Inter_greatest) 1,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
    REPEAT (eresolve_tac [RepFunE, prem, ssubst] 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
(*** Finite Union -- the least upper bound of 2 sets ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 689
diff changeset
   135
qed_goal "Un_subset_iff" ZF.thy "A Un B <= C <-> A <= C & B <= C"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
 (fn _ => [ fast_tac upair_cs 1 ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   137
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 689
diff changeset
   138
qed_goal "Un_upper1" ZF.thy "A <= A Un B"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   139
 (fn _ => [ (REPEAT (ares_tac [subsetI,UnI1] 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   140
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 689
diff changeset
   141
qed_goal "Un_upper2" ZF.thy "B <= A Un B"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   142
 (fn _ => [ (REPEAT (ares_tac [subsetI,UnI2] 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   143
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 689
diff changeset
   144
qed_goal "Un_least" ZF.thy "!!A B C. [| A<=C;  B<=C |] ==> A Un B <= C"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   145
 (fn _ =>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   146
  [ (rtac (Un_subset_iff RS iffD2) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   147
    (REPEAT (ares_tac [conjI] 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   148
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   149
(*** Finite Intersection -- the greatest lower bound of 2 sets *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   150
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 689
diff changeset
   151
qed_goal "Int_subset_iff" ZF.thy "C <= A Int B <-> C <= A & C <= B"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
 (fn _ => [ fast_tac upair_cs 1 ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   153
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 689
diff changeset
   154
qed_goal "Int_lower1" ZF.thy "A Int B <= A"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   155
 (fn _ => [ (REPEAT (ares_tac [subsetI] 1 ORELSE etac IntE 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   156
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 689
diff changeset
   157
qed_goal "Int_lower2" ZF.thy "A Int B <= B"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   158
 (fn _ => [ (REPEAT (ares_tac [subsetI] 1 ORELSE etac IntE 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   159
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 689
diff changeset
   160
qed_goal "Int_greatest" ZF.thy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   161
                             "!!A B C. [| C<=A;  C<=B |] ==> C <= A Int B"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   162
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   163
  [ (rtac (Int_subset_iff RS iffD2) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   164
    (REPEAT (ares_tac [conjI] 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   165
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   166
(*** Set difference *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   167
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 689
diff changeset
   168
qed_goal "Diff_subset" ZF.thy "A-B <= A"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   169
 (fn _ => [ (REPEAT (ares_tac [subsetI] 1 ORELSE etac DiffE 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   170
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 689
diff changeset
   171
qed_goal "Diff_contains" ZF.thy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   172
    "[| C<=A;  C Int B = 0 |] ==> C <= A-B"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   173
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   174
  [ (cut_facts_tac prems 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   175
    (rtac subsetI 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   176
    (REPEAT (ares_tac [DiffI,IntI,notI] 1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   177
     ORELSE eresolve_tac [subsetD,equals0D] 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   178
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   179
(** Collect **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   180
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 689
diff changeset
   181
qed_goal "Collect_subset" ZF.thy "Collect(A,P) <= A"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   182
 (fn _ => [ (REPEAT (ares_tac [subsetI] 1 ORELSE etac CollectD1 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   183
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   184
(** RepFun **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   185
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   186
val prems = goal ZF.thy "[| !!x. x:A ==> f(x): B |] ==> {f(x). x:A} <= B";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   187
by (rtac subsetI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   188
by (etac RepFunE 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   189
by (etac ssubst 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   190
by (eresolve_tac prems 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 689
diff changeset
   191
qed "RepFun_subset";
689
bf95dada47ac ZF/Fixedpt/subset_cs: moved to ZF/subset.ML
lcp
parents: 0
diff changeset
   192
bf95dada47ac ZF/Fixedpt/subset_cs: moved to ZF/subset.ML
lcp
parents: 0
diff changeset
   193
(*A more powerful claset for subset reasoning*)
bf95dada47ac ZF/Fixedpt/subset_cs: moved to ZF/subset.ML
lcp
parents: 0
diff changeset
   194
val subset_cs = subset0_cs 
bf95dada47ac ZF/Fixedpt/subset_cs: moved to ZF/subset.ML
lcp
parents: 0
diff changeset
   195
  addSIs [subset_refl,cons_subsetI,subset_consI,Union_least,UN_least,Un_least,
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 782
diff changeset
   196
          Inter_greatest,Int_greatest,RepFun_subset]
689
bf95dada47ac ZF/Fixedpt/subset_cs: moved to ZF/subset.ML
lcp
parents: 0
diff changeset
   197
  addSIs [Un_upper1,Un_upper2,Int_lower1,Int_lower2]
bf95dada47ac ZF/Fixedpt/subset_cs: moved to ZF/subset.ML
lcp
parents: 0
diff changeset
   198
  addIs  [Union_upper,Inter_lower]
bf95dada47ac ZF/Fixedpt/subset_cs: moved to ZF/subset.ML
lcp
parents: 0
diff changeset
   199
  addSEs [cons_subsetE];
bf95dada47ac ZF/Fixedpt/subset_cs: moved to ZF/subset.ML
lcp
parents: 0
diff changeset
   200