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