src/ZF/func.ML
author lcp
Tue, 26 Jul 1994 13:44:42 +0200
changeset 485 5e00a676a211
parent 437 435875e4b21d
child 517 a9f93400f307
permissions -rw-r--r--
Axiom of choice, cardinality results, etc.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	ZF/func
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
Functions 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
(*** The Pi operator -- dependent function space ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
val prems = goalw ZF.thy [Pi_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
    "[| f <= Sigma(A,B);  !!x. x:A ==> EX! y. <x,y>: f |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
\     f: Pi(A,B)";  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
by (REPEAT (ares_tac (prems @ [CollectI,PowI,ballI,impI]) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
val PiI = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
(**Two "destruct" rules for Pi **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
val [major] = goalw ZF.thy [Pi_def] "f: Pi(A,B) ==> f <= Sigma(A,B)";  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
by (rtac (major RS CollectE) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
by (etac PowD 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
val fun_is_rel = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
val major::prems = goalw ZF.thy [Pi_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
    "[| f: Pi(A,B);  a:A |] ==> EX! y. <a,y>: f";  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
by (rtac (major RS CollectE) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
by (etac bspec 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
by (resolve_tac prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
val fun_unique_Pair = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
val prems = goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
    "[| f: Pi(A,B); \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
\       [| f <= Sigma(A,B);  ALL x:A. EX! y. <x,y>: f |] ==> P \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
\    |] ==> P";  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
by (REPEAT (ares_tac (prems@[ballI,fun_is_rel,fun_unique_Pair]) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
val PiE = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
val prems = goalw ZF.thy [Pi_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
    "[| A=A';  !!x. x:A' ==> B(x)=B'(x) |] ==> Pi(A,B) = Pi(A',B')";
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    40
by (simp_tac (FOL_ss addsimps prems addcongs [Sigma_cong]) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
val Pi_cong = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 437
diff changeset
    43
(*Weakening one function type to another; see also Pi_type*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
goalw ZF.thy [Pi_def] "!!f. [| f: A->B;  B<=D |] ==> f: A->D";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
by (safe_tac ZF_cs);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
by (set_mp_tac 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
by (fast_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
val fun_weaken_type = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
(*Empty function spaces*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
goalw ZF.thy [Pi_def] "Pi(0,A) = {0}";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
by (fast_tac (ZF_cs addIs [equalityI]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
val Pi_empty1 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
goalw ZF.thy [Pi_def] "!!A a. a:A ==> A->0 = 0";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
by (fast_tac (ZF_cs addIs [equalityI]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
val Pi_empty2 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
(*** Function Application ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
goal ZF.thy "!!a b f. [| <a,b>: f;  <a,c>: f;  f: Pi(A,B) |] ==> b=c";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
by (etac PiE 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
by (etac (bspec RS ex1_equalsE) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
by (etac (subsetD RS SigmaD1) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
by (REPEAT (assume_tac 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
val apply_equality2 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
goalw ZF.thy [apply_def] "!!a b f. [| <a,b>: f;  f: Pi(A,B) |] ==> f`a = b";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
by (rtac the_equality 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
by (rtac apply_equality2 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
by (REPEAT (assume_tac 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
val apply_equality = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
val prems = goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
    "[| f: Pi(A,B);   c: f;   !!x. [| x:A;  c = <x,f`x> |] ==> P  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
\    |] ==> P";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
by (cut_facts_tac prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
by (etac (fun_is_rel RS subsetD RS SigmaE) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
by (REPEAT (ares_tac prems 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
by (hyp_subst_tac 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
by (etac (apply_equality RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
by (resolve_tac prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
by (rtac refl 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
val memberPiE = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    86
(*Conclusion is flexible -- use res_inst_tac or else apply_funtype below!*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
goal ZF.thy "!!f. [| f: Pi(A,B);  a:A |] ==> f`a : B(a)"; 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
by (rtac (fun_unique_Pair RS ex1E) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
by (REPEAT (assume_tac 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
by (rtac (fun_is_rel RS subsetD RS SigmaE2) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
by (etac (apply_equality RS ssubst) 3);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
by (REPEAT (assume_tac 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
val apply_type = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    95
(*This version is acceptable to the simplifier*)
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    96
goal ZF.thy "!!f. [| f: A->B;  a:A |] ==> f`a : B"; 
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    97
by (REPEAT (ares_tac [apply_type] 1));
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    98
val apply_funtype = result();
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    99
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
goal ZF.thy "!!f. [| f: Pi(A,B);  a:A |] ==> <a,f`a>: f";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
by (rtac (fun_unique_Pair RS ex1E) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
by (resolve_tac [apply_equality RS ssubst] 3);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
by (REPEAT (assume_tac 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
val apply_Pair = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
val [major] = goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
    "f: Pi(A,B) ==> <a,b>: f <-> a:A & f`a = b";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
by (rtac (major RS PiE) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
by (fast_tac (ZF_cs addSIs [major RS apply_Pair, 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
			    major RSN (2,apply_equality)]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
val apply_iff = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
(*Refining one Pi type to another*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
val prems = goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
    "[| f: Pi(A,C);  !!x. x:A ==> f`x : B(x) |] ==> f : Pi(A,B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
by (rtac (subsetI RS PiI) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
by (eresolve_tac (prems RL [memberPiE]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
by (etac ssubst 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
by (REPEAT (ares_tac (prems@[SigmaI,fun_unique_Pair]) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
val Pi_type = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
(** Elimination of membership in a function **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
goal ZF.thy "!!a A. [| <a,b> : f;  f: Pi(A,B) |] ==> a : A";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
by (REPEAT (ares_tac [fun_is_rel RS subsetD RS SigmaD1] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
val domain_type = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
goal ZF.thy "!!b B a. [| <a,b> : f;  f: Pi(A,B) |] ==> b : B(a)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
by (etac (fun_is_rel RS subsetD RS SigmaD2) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
by (assume_tac 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
val range_type = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
val prems = goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   135
    "[| <a,b>: f;  f: Pi(A,B);       \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
\       [| a:A;  b:B(a);  f`a = b |] ==> P  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   137
\    |] ==> P";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   138
by (cut_facts_tac prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   139
by (resolve_tac prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   140
by (REPEAT (eresolve_tac [asm_rl,domain_type,range_type,apply_equality] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   141
val Pair_mem_PiE = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   142
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   143
(*** Lambda Abstraction ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   144
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   145
goalw ZF.thy [lam_def] "!!A b. a:A ==> <a,b(a)> : (lam x:A. b(x))";  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   146
by (etac RepFunI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   147
val lamI = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   148
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   149
val major::prems = goalw ZF.thy [lam_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   150
    "[| p: (lam x:A. b(x));  !!x.[| x:A; p=<x,b(x)> |] ==> P  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   151
\    |] ==>  P";  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
by (rtac (major RS RepFunE) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   153
by (REPEAT (ares_tac prems 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   154
val lamE = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   155
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   156
goal ZF.thy "!!a b c. [| <a,c>: (lam x:A. b(x)) |] ==> c = b(a)";  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   157
by (REPEAT (eresolve_tac [asm_rl,lamE,Pair_inject,ssubst] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   158
val lamD = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   159
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   160
val prems = goalw ZF.thy [lam_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   161
    "[| !!x. x:A ==> b(x): B(x) |] ==> (lam x:A.b(x)) : Pi(A,B)";  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   162
by (fast_tac (ZF_cs addIs (PiI::prems)) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   163
val lam_type = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   164
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   165
goal ZF.thy "(lam x:A.b(x)) : A -> {b(x). x:A}";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   166
by (REPEAT (ares_tac [refl,lam_type,RepFunI] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   167
val lam_funtype = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   168
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   169
goal ZF.thy "!!a A. a : A ==> (lam x:A.b(x)) ` a = b(a)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   170
by (REPEAT (ares_tac [apply_equality,lam_funtype,lamI] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   171
val beta = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   172
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   173
(*congruence rule for lambda abstraction*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   174
val prems = goalw ZF.thy [lam_def] 
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   175
    "[| A=A';  !!x. x:A' ==> b(x)=b'(x) |] ==> Lambda(A,b) = Lambda(A',b')";
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   176
by (simp_tac (FOL_ss addsimps prems addcongs [RepFun_cong]) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   177
val lam_cong = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   178
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   179
val [major] = goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   180
    "(!!x. x:A ==> EX! y. Q(x,y)) ==> EX f. ALL x:A. Q(x, f`x)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   181
by (res_inst_tac [("x", "lam x: A. THE y. Q(x,y)")] exI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   182
by (rtac ballI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   183
by (rtac (beta RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   184
by (assume_tac 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   185
by (etac (major RS theI) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   186
val lam_theI = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   187
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   188
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   189
(** Extensionality **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   190
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   191
(*Semi-extensionality!*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   192
val prems = goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   193
    "[| f : Pi(A,B);  g: Pi(C,D);  A<=C; \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   194
\       !!x. x:A ==> f`x = g`x       |] ==> f<=g";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   195
by (rtac subsetI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   196
by (eresolve_tac (prems RL [memberPiE]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   197
by (etac ssubst 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   198
by (resolve_tac (prems RL [ssubst]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   199
by (REPEAT (ares_tac (prems@[apply_Pair,subsetD]) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   200
val fun_subset = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   201
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   202
val prems = goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   203
    "[| f : Pi(A,B);  g: Pi(A,D);  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   204
\       !!x. x:A ==> f`x = g`x       |] ==> f=g";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   205
by (REPEAT (ares_tac (prems @ (prems RL [sym]) @
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   206
		      [subset_refl,equalityI,fun_subset]) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   207
val fun_extension = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   208
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   209
goal ZF.thy "!!f A B. f : Pi(A,B) ==> (lam x:A. f`x) = f";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   210
by (rtac fun_extension 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   211
by (REPEAT (ares_tac [lam_type,apply_type,beta] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   212
val eta = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   213
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   214
(*Every element of Pi(A,B) may be expressed as a lambda abstraction!*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   215
val prems = goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   216
    "[| f: Pi(A,B);        \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   217
\       !!b. [| ALL x:A. b(x):B(x);  f = (lam x:A.b(x)) |] ==> P   \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   218
\    |] ==> P";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   219
by (resolve_tac prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   220
by (rtac (eta RS sym) 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   221
by (REPEAT (ares_tac (prems@[ballI,apply_type]) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   222
val Pi_lamE = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   223
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   224
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 129
diff changeset
   225
(** Images of functions **)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 129
diff changeset
   226
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 129
diff changeset
   227
goalw ZF.thy [lam_def] "!!C A. C <= A ==> (lam x:A.b(x)) `` C = {b(x). x:C}";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 129
diff changeset
   228
by (fast_tac eq_cs 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 129
diff changeset
   229
val image_lam = result();
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 129
diff changeset
   230
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 129
diff changeset
   231
goal ZF.thy "!!C A. [| f : Pi(A,B);  C <= A |] ==> f``C = {f`x. x:C}";
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   232
by (etac (eta RS subst) 1);
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 129
diff changeset
   233
by (asm_full_simp_tac (FOL_ss addsimps [beta, image_lam, subset_iff]
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 129
diff changeset
   234
                              addcongs [RepFun_cong]) 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 129
diff changeset
   235
val image_fun = result();
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 129
diff changeset
   236
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 129
diff changeset
   237
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   238
(*** properties of "restrict" ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   239
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   240
goalw ZF.thy [restrict_def,lam_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   241
    "!!f A. [| f: Pi(C,B);  A<=C |] ==> restrict(f,A) <= f";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   242
by (fast_tac (ZF_cs addIs [apply_Pair]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   243
val restrict_subset = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   244
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   245
val prems = goalw ZF.thy [restrict_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   246
    "[| !!x. x:A ==> f`x: B(x) |] ==> restrict(f,A) : Pi(A,B)";  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   247
by (rtac lam_type 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   248
by (eresolve_tac prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   249
val restrict_type = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   250
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   251
val [pi,subs] = goal ZF.thy 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   252
    "[| f: Pi(C,B);  A<=C |] ==> restrict(f,A) : Pi(A,B)";  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   253
by (rtac (pi RS apply_type RS restrict_type) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   254
by (etac (subs RS subsetD) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   255
val restrict_type2 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   256
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   257
goalw ZF.thy [restrict_def] "!!a A. a : A ==> restrict(f,A) ` a = f`a";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   258
by (etac beta 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   259
val restrict = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   260
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   261
(*NOT SAFE as a congruence rule for the simplifier!  Can cause it to fail!*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   262
val prems = goalw ZF.thy [restrict_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   263
    "[| A=B;  !!x. x:B ==> f`x=g`x |] ==> restrict(f,A) = restrict(g,B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   264
by (REPEAT (ares_tac (prems@[lam_cong]) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   265
val restrict_eqI = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   266
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   267
goalw ZF.thy [restrict_def] "domain(restrict(f,C)) = C";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   268
by (REPEAT (ares_tac [equalityI,subsetI,domainI,lamI] 1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   269
     ORELSE eresolve_tac [domainE,lamE,Pair_inject,ssubst] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   270
val domain_restrict = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   271
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   272
val [prem] = goalw ZF.thy [restrict_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   273
    "A<=C ==> restrict(lam x:C. b(x), A) = (lam x:A. b(x))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   274
by (rtac (refl RS lam_cong) 1);
129
dc50a4b96d7b expandshort and other trivial changes
lcp
parents: 37
diff changeset
   275
by (etac (prem RS subsetD RS beta) 1);	(*easier than calling simp_tac*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   276
val restrict_lam_eq = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   277
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   278
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   279
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   280
(*** Unions of functions ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   281
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   282
(** The Union of a set of COMPATIBLE functions is a function **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   283
val [ex_prem,disj_prem] = goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   284
    "[| ALL x:S. EX C D. x:C->D; \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   285
\       !!x y. [| x:S;  y:S |] ==> x<=y | y<=x  |] ==>  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   286
\    Union(S) : domain(Union(S)) -> range(Union(S))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   287
val premE = ex_prem RS bspec RS exE;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   288
by (REPEAT (eresolve_tac [exE,PiE,premE] 1 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   289
     ORELSE ares_tac [PiI, ballI RS rel_Union, exI] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   290
by (REPEAT (eresolve_tac [asm_rl,domainE,UnionE,exE] 1 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   291
     ORELSE ares_tac [allI,impI,ex1I,UnionI] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   292
by (res_inst_tac [ ("x1","B") ] premE 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   293
by (res_inst_tac [ ("x1","Ba") ] premE 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   294
by (REPEAT (eresolve_tac [asm_rl,exE] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   295
by (eresolve_tac [disj_prem RS disjE] 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   296
by (DEPTH_SOLVE (set_mp_tac 1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   297
		 ORELSE eresolve_tac [asm_rl, apply_equality2] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   298
val fun_Union = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   299
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   300
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   301
(** The Union of 2 disjoint functions is a function **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   302
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   303
val prems = goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   304
    "[| f: A->B;  g: C->D;  A Int C = 0  |] ==>  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   305
\    (f Un g) : (A Un C) -> (B Un D)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   306
     (*Contradiction if A Int C = 0, a:A, a:B*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   307
val [disjoint] = prems RL ([IntI] RLN (2, [equals0D]));
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   308
val Pair_UnE = read_instantiate [("c","<?a,?b>")] UnE;  (* ignores x: A Un C *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   309
by (cut_facts_tac prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   310
by (rtac PiI 1);
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   311
by (REPEAT (ares_tac [rel_Un, fun_is_rel] 1));
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   312
by (rtac ex_ex1I 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   313
by (fast_tac (ZF_cs addDs [apply_Pair]) 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   314
by (REPEAT_FIRST (eresolve_tac [asm_rl, Pair_UnE, sym RS trans]
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   315
	     ORELSE' eresolve_tac [Pair_mem_PiE,disjoint] THEN' atac));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   316
val fun_disjoint_Un = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   317
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   318
goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   319
    "!!f g a. [| a:A;  f: A->B;  g: C->D;  A Int C = 0 |] ==>  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   320
\             (f Un g)`a = f`a";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   321
by (REPEAT (ares_tac [apply_equality,UnI1,apply_Pair,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   322
		      fun_disjoint_Un] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   323
val fun_disjoint_apply1 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   324
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   325
goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   326
    "!!f g c. [| c:C;  f: A->B;  g: C->D;  A Int C = 0 |] ==>  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   327
\             (f Un g)`c = g`c";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   328
by (REPEAT (ares_tac [apply_equality,UnI2,apply_Pair,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   329
		      fun_disjoint_Un] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   330
val fun_disjoint_apply2 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   331
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   332
(** Domain and range of a function/relation **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   333
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   334
val [major] = goal ZF.thy "f : Pi(A,B) ==> domain(f)=A";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   335
by (rtac equalityI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   336
by (fast_tac (ZF_cs addIs [major RS apply_Pair]) 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   337
by (rtac (major RS PiE) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   338
by (fast_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   339
val domain_of_fun = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   340
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   341
val [major] = goal ZF.thy "f : Pi(A,B) ==> f : A->range(f)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   342
by (rtac (major RS Pi_type) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   343
by (etac (major RS apply_Pair RS rangeI) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   344
val range_of_fun = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   345
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   346
(*** Extensions of functions ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   347
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   348
(*Singleton function -- in the underlying form of singletons*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   349
goal ZF.thy "Upair(<a,b>,<a,b>) : Upair(a,a) -> Upair(b,b)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   350
by (fast_tac (ZF_cs addIs [PiI]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   351
val fun_single_lemma = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   352
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   353
goalw ZF.thy [cons_def]
37
cebe01deba80 added ~: for "not in"
lcp
parents: 14
diff changeset
   354
    "!!f A B. [| f: A->B;  c~:A |] ==> cons(<c,b>,f) : cons(c,A) -> cons(b,B)";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   355
by (rtac (fun_single_lemma RS fun_disjoint_Un) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   356
by (assume_tac 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   357
by (rtac equals0I 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   358
by (fast_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   359
val fun_extend = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   360
37
cebe01deba80 added ~: for "not in"
lcp
parents: 14
diff changeset
   361
goal ZF.thy "!!f A B. [| f: A->B;  a:A;  c~:A |] ==> cons(<c,b>,f)`a = f`a";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   362
by (rtac (apply_Pair RS consI2 RS apply_equality) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   363
by (rtac fun_extend 3);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   364
by (REPEAT (assume_tac 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   365
val fun_extend_apply1 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   366
37
cebe01deba80 added ~: for "not in"
lcp
parents: 14
diff changeset
   367
goal ZF.thy "!!f A B. [| f: A->B;  c~:A |] ==> cons(<c,b>,f)`c = b";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   368
by (rtac (consI1 RS apply_equality) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   369
by (rtac fun_extend 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   370
by (REPEAT (assume_tac 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   371
val fun_extend_apply2 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   372
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   373
(*The empty function*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   374
goal ZF.thy "0: 0->A";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   375
by (fast_tac (ZF_cs addIs [PiI]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   376
val fun_empty = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   377
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   378
(*The singleton function*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   379
goal ZF.thy "{<a,b>} : {a} -> cons(b,C)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   380
by (REPEAT (ares_tac [fun_extend,fun_empty,notI] 1 ORELSE etac emptyE 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   381
val fun_single = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   382
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 437
diff changeset
   383
goal ZF.thy
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 437
diff changeset
   384
    "!!c. c ~: A ==> cons(c,A) -> B = (UN f: A->B. UN b:B. {cons(<c,b>, f)})";
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 437
diff changeset
   385
by (safe_tac eq_cs);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 437
diff changeset
   386
(*Inclusion of right into left is easy*)
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 437
diff changeset
   387
by (fast_tac (ZF_cs addEs [fun_extend RS fun_weaken_type]) 2);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 437
diff changeset
   388
(*Inclusion of left into right*)
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 437
diff changeset
   389
by (subgoal_tac "restrict(x, A) : A -> B" 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 437
diff changeset
   390
by (fast_tac (ZF_cs addEs [restrict_type2]) 2);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 437
diff changeset
   391
by (rtac UN_I 1 THEN assume_tac 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 437
diff changeset
   392
by (rtac UN_I 1 THEN fast_tac (ZF_cs addEs [apply_type]) 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 437
diff changeset
   393
by (subgoal_tac "x = cons(<c, x ` c>, restrict(x, A))" 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 437
diff changeset
   394
by (fast_tac ZF_cs 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 437
diff changeset
   395
(*Proving the lemma*)
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 437
diff changeset
   396
by (resolve_tac [fun_extension] 1 THEN REPEAT (ares_tac [fun_extend] 1));
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 437
diff changeset
   397
by (etac consE 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 437
diff changeset
   398
by (ALLGOALS 
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 437
diff changeset
   399
    (asm_simp_tac (FOL_ss addsimps [restrict, fun_extend_apply1, 
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 437
diff changeset
   400
				   fun_extend_apply2])));
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 437
diff changeset
   401
val cons_fun_eq = result();
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 437
diff changeset
   402