src/ZF/func.ML
author clasohm
Tue, 30 Jan 1996 13:42:57 +0100
changeset 1461 6bcb44e4d6e5
parent 857 f5314a7c93f2
child 2033 639de962ded4
permissions -rw-r--r--
expanded tabs
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 857
diff changeset
     1
(*  Title:      ZF/func
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 857
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
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
691
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
    11
goalw ZF.thy [Pi_def]
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
    12
    "f: Pi(A,B) <-> function(f) & f<=Sigma(A,B) & A<=domain(f)";
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
    13
by (fast_tac ZF_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
    14
qed "Pi_iff";
691
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
    15
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
    16
(*For upward compatibility with the former definition*)
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
    17
goalw ZF.thy [Pi_def, function_def]
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
    18
    "f: Pi(A,B) <-> f<=Sigma(A,B) & (ALL x:A. EX! y. <x,y>: f)";
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
    19
by (safe_tac ZF_cs);
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
    20
by (best_tac ZF_cs 1);
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
    21
by (best_tac ZF_cs 1);
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
    22
by (set_mp_tac 1);
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
    23
by (deepen_tac ZF_cs 3 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
    24
qed "Pi_iff_old";
691
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
    25
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
    26
goal ZF.thy "!!f. f: Pi(A,B) ==> function(f)";
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
    27
by (asm_full_simp_tac (FOL_ss addsimps [Pi_iff]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
    28
qed "fun_is_function";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
(**Two "destruct" rules for Pi **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
val [major] = goalw ZF.thy [Pi_def] "f: Pi(A,B) ==> f <= Sigma(A,B)";  
691
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
    33
by (rtac (major RS CollectD1 RS PowD) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
    34
qed "fun_is_rel";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
691
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
    36
goal ZF.thy "!!f. [| f: Pi(A,B);  a:A |] ==> EX! y. <a,y>: f";  
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
    37
by (fast_tac (ZF_cs addSDs [Pi_iff_old RS iffD1]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
    38
qed "fun_unique_Pair";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
val prems = goalw ZF.thy [Pi_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
    "[| 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
    42
by (simp_tac (FOL_ss addsimps prems addcongs [Sigma_cong]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
    43
qed "Pi_cong";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 437
diff changeset
    45
(*Weakening one function type to another; see also Pi_type*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
goalw ZF.thy [Pi_def] "!!f. [| f: A->B;  B<=D |] ==> f: A->D";
691
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
    47
by (best_tac ZF_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
    48
qed "fun_weaken_type";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
(*Empty function spaces*)
691
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
    51
goalw ZF.thy [Pi_def, function_def] "Pi(0,A) = {0}";
519
98b88551e102 ZF/func/empty_fun: renamed from fun_empty
lcp
parents: 517
diff changeset
    52
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
    53
qed "Pi_empty1";
0
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";
519
98b88551e102 ZF/func/empty_fun: renamed from fun_empty
lcp
parents: 517
diff changeset
    56
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
    57
qed "Pi_empty2";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
519
98b88551e102 ZF/func/empty_fun: renamed from fun_empty
lcp
parents: 517
diff changeset
    59
(*The empty function*)
824
120fc7e857ba empty_fun: generalized from -> to Pi
lcp
parents: 760
diff changeset
    60
goalw ZF.thy [Pi_def, function_def] "0: Pi(0,B)";
691
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
    61
by (fast_tac ZF_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
    62
qed "empty_fun";
519
98b88551e102 ZF/func/empty_fun: renamed from fun_empty
lcp
parents: 517
diff changeset
    63
98b88551e102 ZF/func/empty_fun: renamed from fun_empty
lcp
parents: 517
diff changeset
    64
(*The singleton function*)
691
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
    65
goalw ZF.thy [Pi_def, function_def] "{<a,b>} : {a} -> {b}";
519
98b88551e102 ZF/func/empty_fun: renamed from fun_empty
lcp
parents: 517
diff changeset
    66
by (fast_tac eq_cs 1);
857
f5314a7c93f2 Renamed single_fun to singleton_fun.
lcp
parents: 824
diff changeset
    67
qed "singleton_fun";
519
98b88551e102 ZF/func/empty_fun: renamed from fun_empty
lcp
parents: 517
diff changeset
    68
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
(*** Function Application ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
691
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
    71
goalw ZF.thy [Pi_def, function_def]
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
    72
     "!!a b f. [| <a,b>: f;  <a,c>: f;  f: Pi(A,B) |] ==> b=c";
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
    73
by (deepen_tac ZF_cs 3 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
    74
qed "apply_equality2";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
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
    77
by (rtac the_equality 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
by (rtac apply_equality2 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
by (REPEAT (assume_tac 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
    80
qed "apply_equality";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
517
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 485
diff changeset
    82
(*Applying a function outside its domain yields 0*)
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 485
diff changeset
    83
goalw ZF.thy [apply_def]
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 485
diff changeset
    84
    "!!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
    85
by (rtac the_0 1);
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 485
diff changeset
    86
by (fast_tac ZF_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
    87
qed "apply_0";
517
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 485
diff changeset
    88
691
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
    89
goal ZF.thy "!!f. [| f: Pi(A,B);  c: f |] ==> EX x:A.  c = <x,f`x>";
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
    90
by (forward_tac [fun_is_rel] 1);
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
    91
by (fast_tac (ZF_cs addDs [apply_equality]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
    92
qed "Pi_memberD";
691
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
    93
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
    94
goal ZF.thy "!!f. [| f: Pi(A,B);  a:A |] ==> <a,f`a>: f";
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
    95
by (rtac (fun_unique_Pair RS ex1E) 1);
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
    96
by (resolve_tac [apply_equality RS ssubst] 3);
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
    97
by (REPEAT (assume_tac 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
    98
qed "apply_Pair";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   100
(*Conclusion is flexible -- use res_inst_tac or else apply_funtype below!*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
goal ZF.thy "!!f. [| f: Pi(A,B);  a:A |] ==> f`a : B(a)"; 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
by (rtac (fun_is_rel RS subsetD RS SigmaE2) 1);
691
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
   103
by (REPEAT (ares_tac [apply_Pair] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
   104
qed "apply_type";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   106
(*This version is acceptable to the simplifier*)
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   107
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
   108
by (REPEAT (ares_tac [apply_type] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
   109
qed "apply_funtype";
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   110
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
val [major] = goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
    "f: Pi(A,B) ==> <a,b>: f <-> a:A & f`a = b";
691
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
   113
by (cut_facts_tac [major RS fun_is_rel] 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
by (fast_tac (ZF_cs addSIs [major RS apply_Pair, 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 857
diff changeset
   115
                            major RSN (2,apply_equality)]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
   116
qed "apply_iff";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
(*Refining one Pi type to another*)
691
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
   119
val pi_prem::prems = goal ZF.thy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
    "[| f: Pi(A,C);  !!x. x:A ==> f`x : B(x) |] ==> f : Pi(A,B)";
691
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
   121
by (cut_facts_tac [pi_prem] 1);
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
   122
by (asm_full_simp_tac (FOL_ss addsimps [Pi_iff]) 1);
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
   123
by (fast_tac (ZF_cs addIs prems addSDs [pi_prem RS Pi_memberD]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
   124
qed "Pi_type";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
(** Elimination of membership in a function **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
goal ZF.thy "!!a A. [| <a,b> : f;  f: Pi(A,B) |] ==> a : A";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
by (REPEAT (ares_tac [fun_is_rel RS subsetD RS SigmaD1] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
   131
qed "domain_type";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
goal ZF.thy "!!b B a. [| <a,b> : f;  f: Pi(A,B) |] ==> b : B(a)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
by (etac (fun_is_rel RS subsetD RS SigmaD2) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   135
by (assume_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
   136
qed "range_type";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   137
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   138
val prems = goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   139
    "[| <a,b>: f;  f: Pi(A,B);       \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   140
\       [| a:A;  b:B(a);  f`a = b |] ==> P  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   141
\    |] ==> P";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   142
by (cut_facts_tac prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   143
by (resolve_tac prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   144
by (REPEAT (eresolve_tac [asm_rl,domain_type,range_type,apply_equality] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
   145
qed "Pair_mem_PiE";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   146
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   147
(*** Lambda Abstraction ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   148
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   149
goalw ZF.thy [lam_def] "!!A b. a:A ==> <a,b(a)> : (lam x:A. b(x))";  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   150
by (etac RepFunI 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
   151
qed "lamI";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   153
val major::prems = goalw ZF.thy [lam_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   154
    "[| p: (lam x:A. b(x));  !!x.[| x:A; p=<x,b(x)> |] ==> P  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   155
\    |] ==>  P";  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   156
by (rtac (major RS RepFunE) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   157
by (REPEAT (ares_tac prems 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
   158
qed "lamE";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   159
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   160
goal ZF.thy "!!a b c. [| <a,c>: (lam x:A. b(x)) |] ==> c = b(a)";  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   161
by (REPEAT (eresolve_tac [asm_rl,lamE,Pair_inject,ssubst] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
   162
qed "lamD";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   163
691
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
   164
val prems = goalw ZF.thy [lam_def, Pi_def, function_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   165
    "[| !!x. x:A ==> b(x): B(x) |] ==> (lam x:A.b(x)) : Pi(A,B)";  
691
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
   166
by (fast_tac (ZF_cs addIs prems) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
   167
qed "lam_type";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   168
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   169
goal ZF.thy "(lam x:A.b(x)) : A -> {b(x). x:A}";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   170
by (REPEAT (ares_tac [refl,lam_type,RepFunI] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
   171
qed "lam_funtype";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   172
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   173
goal ZF.thy "!!a A. a : A ==> (lam x:A.b(x)) ` a = b(a)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   174
by (REPEAT (ares_tac [apply_equality,lam_funtype,lamI] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
   175
qed "beta";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   176
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   177
(*congruence rule for lambda abstraction*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   178
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
   179
    "[| 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
   180
by (simp_tac (FOL_ss addsimps prems addcongs [RepFun_cong]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
   181
qed "lam_cong";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   182
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   183
val [major] = goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   184
    "(!!x. x:A ==> EX! y. Q(x,y)) ==> EX f. ALL x:A. Q(x, f`x)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   185
by (res_inst_tac [("x", "lam x: A. THE y. Q(x,y)")] exI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   186
by (rtac ballI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   187
by (rtac (beta RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   188
by (assume_tac 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   189
by (etac (major RS theI) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
   190
qed "lam_theI";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   191
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   192
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   193
(** Extensionality **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   194
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   195
(*Semi-extensionality!*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   196
val prems = goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   197
    "[| f : Pi(A,B);  g: Pi(C,D);  A<=C; \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   198
\       !!x. x:A ==> f`x = g`x       |] ==> f<=g";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   199
by (rtac subsetI 1);
691
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
   200
by (eresolve_tac (prems RL [Pi_memberD RS bexE]) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   201
by (etac ssubst 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   202
by (resolve_tac (prems RL [ssubst]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   203
by (REPEAT (ares_tac (prems@[apply_Pair,subsetD]) 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
   204
qed "fun_subset";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   205
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   206
val prems = goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   207
    "[| f : Pi(A,B);  g: Pi(A,D);  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   208
\       !!x. x:A ==> f`x = g`x       |] ==> f=g";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   209
by (REPEAT (ares_tac (prems @ (prems RL [sym]) @
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 857
diff changeset
   210
                      [subset_refl,equalityI,fun_subset]) 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
   211
qed "fun_extension";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   212
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   213
goal ZF.thy "!!f A B. f : Pi(A,B) ==> (lam x:A. f`x) = f";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   214
by (rtac fun_extension 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   215
by (REPEAT (ares_tac [lam_type,apply_type,beta] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
   216
qed "eta";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   217
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   218
(*Every element of Pi(A,B) may be expressed as a lambda abstraction!*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   219
val prems = goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   220
    "[| f: Pi(A,B);        \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   221
\       !!b. [| ALL x:A. b(x):B(x);  f = (lam x:A.b(x)) |] ==> P   \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   222
\    |] ==> P";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   223
by (resolve_tac prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   224
by (rtac (eta RS sym) 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   225
by (REPEAT (ares_tac (prems@[ballI,apply_type]) 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
   226
qed "Pi_lamE";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   227
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   228
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 129
diff changeset
   229
(** Images of functions **)
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
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
   232
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
   233
qed "image_lam";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 129
diff changeset
   234
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 129
diff changeset
   235
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
   236
by (etac (eta RS subst) 1);
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 129
diff changeset
   237
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
   238
                              addcongs [RepFun_cong]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
   239
qed "image_fun";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 129
diff changeset
   240
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 129
diff changeset
   241
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   242
(*** properties of "restrict" ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   243
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   244
goalw ZF.thy [restrict_def,lam_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   245
    "!!f A. [| f: Pi(C,B);  A<=C |] ==> restrict(f,A) <= f";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   246
by (fast_tac (ZF_cs addIs [apply_Pair]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
   247
qed "restrict_subset";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   248
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   249
val prems = goalw ZF.thy [restrict_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   250
    "[| !!x. x:A ==> f`x: B(x) |] ==> restrict(f,A) : Pi(A,B)";  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   251
by (rtac lam_type 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   252
by (eresolve_tac prems 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
   253
qed "restrict_type";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   254
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   255
val [pi,subs] = goal ZF.thy 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   256
    "[| f: Pi(C,B);  A<=C |] ==> restrict(f,A) : Pi(A,B)";  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   257
by (rtac (pi RS apply_type RS restrict_type) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   258
by (etac (subs RS subsetD) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
   259
qed "restrict_type2";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   260
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   261
goalw ZF.thy [restrict_def] "!!a A. a : A ==> restrict(f,A) ` a = f`a";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   262
by (etac beta 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
   263
qed "restrict";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   264
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   265
(*NOT SAFE as a congruence rule for the simplifier!  Can cause it to fail!*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   266
val prems = goalw ZF.thy [restrict_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   267
    "[| A=B;  !!x. x:B ==> f`x=g`x |] ==> restrict(f,A) = restrict(g,B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   268
by (REPEAT (ares_tac (prems@[lam_cong]) 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
   269
qed "restrict_eqI";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   270
691
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
   271
goalw ZF.thy [restrict_def, lam_def] "domain(restrict(f,C)) = C";
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
   272
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
   273
qed "domain_restrict";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   274
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   275
val [prem] = goalw ZF.thy [restrict_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   276
    "A<=C ==> restrict(lam x:C. b(x), A) = (lam x:A. b(x))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   277
by (rtac (refl RS lam_cong) 1);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 857
diff changeset
   278
by (etac (prem RS subsetD RS beta) 1);  (*easier than calling simp_tac*)
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
   279
qed "restrict_lam_eq";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   280
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   281
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   282
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   283
(*** Unions of functions ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   284
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   285
(** The Union of a set of COMPATIBLE functions is a function **)
691
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
   286
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
   287
goalw ZF.thy [function_def]
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
   288
    "!!S. [| ALL x:S. function(x); \
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
   289
\            ALL x:S. ALL y:S. x<=y | y<=x  |] ==>  \
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
   290
\         function(Union(S))";
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
   291
by (fast_tac (ZF_cs addSDs [bspec RS bspec]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
   292
qed "function_Union";
691
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
   293
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
   294
goalw ZF.thy [Pi_def]
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
   295
    "!!S. [| ALL f:S. EX C D. f:C->D; \
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
   296
\            ALL f:S. ALL y:S. f<=y | y<=f  |] ==>  \
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
   297
\         Union(S) : domain(Union(S)) -> range(Union(S))";
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
   298
by (fast_tac (subset_cs addSIs [rel_Union, function_Union]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
   299
qed "fun_Union";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   300
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   301
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   302
(** The Union of 2 disjoint functions is a function **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   303
691
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
   304
val Un_rls = [Un_subset_iff, domain_Un_eq, SUM_Un_distrib1, prod_Un_distrib2, 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 857
diff changeset
   305
              Un_upper1 RSN (2, subset_trans), 
6bcb44e4d6e5 expanded tabs
clasohm
parents: 857
diff changeset
   306
              Un_upper2 RSN (2, subset_trans)];
691
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
   307
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
   308
goal ZF.thy
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
   309
    "!!f. [| f: A->B;  g: C->D;  A Int C = 0  |] ==>  \
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
   310
\         (f Un g) : (A Un C) -> (B Un D)";
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
   311
(*Solve the product and domain subgoals using distributive laws*)
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
   312
by (asm_full_simp_tac (FOL_ss addsimps [Pi_iff,extension]@Un_rls) 1);
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
   313
by (asm_simp_tac (FOL_ss addsimps [function_def]) 1);
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
   314
by (safe_tac ZF_cs);
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
   315
(*Solve the two cases that contradict A Int C = 0*)
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
   316
by (deepen_tac ZF_cs 2 2);
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
   317
by (deepen_tac ZF_cs 2 2);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 857
diff changeset
   318
by (rewtac function_def);
691
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
   319
by (REPEAT_FIRST (dtac (spec RS spec)));
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
   320
by (deepen_tac ZF_cs 1 1);
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
   321
by (deepen_tac ZF_cs 1 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
   322
qed "fun_disjoint_Un";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   323
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   324
goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   325
    "!!f g a. [| a:A;  f: A->B;  g: C->D;  A Int C = 0 |] ==>  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   326
\             (f Un g)`a = f`a";
691
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
   327
by (rtac (apply_Pair RS UnI1 RS apply_equality) 1);
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
   328
by (REPEAT (ares_tac [fun_disjoint_Un] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
   329
qed "fun_disjoint_apply1";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   330
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   331
goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   332
    "!!f g c. [| c:C;  f: A->B;  g: C->D;  A Int C = 0 |] ==>  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   333
\             (f Un g)`c = g`c";
691
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
   334
by (rtac (apply_Pair RS UnI2 RS apply_equality) 1);
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
   335
by (REPEAT (ares_tac [fun_disjoint_Un] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
   336
qed "fun_disjoint_apply2";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   337
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   338
(** Domain and range of a function/relation **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   339
691
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
   340
goalw ZF.thy [Pi_def] "!!f. f : Pi(A,B) ==> domain(f)=A";
b9fc536792bb ZF/func: tidied many proofs, using new definition of Pi(A,B)
lcp
parents: 538
diff changeset
   341
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
   342
qed "domain_of_fun";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   343
517
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 485
diff changeset
   344
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
   345
by (etac (apply_Pair RS rangeI) 1);
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 485
diff changeset
   346
by (assume_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
   347
qed "apply_rangeI";
517
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 485
diff changeset
   348
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   349
val [major] = goal ZF.thy "f : Pi(A,B) ==> f : A->range(f)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   350
by (rtac (major RS Pi_type) 1);
517
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 485
diff changeset
   351
by (etac (major RS apply_rangeI) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
   352
qed "range_of_fun";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   353
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   354
(*** Extensions of functions ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   355
519
98b88551e102 ZF/func/empty_fun: renamed from fun_empty
lcp
parents: 517
diff changeset
   356
goal ZF.thy
37
cebe01deba80 added ~: for "not in"
lcp
parents: 14
diff changeset
   357
    "!!f A B. [| f: A->B;  c~:A |] ==> cons(<c,b>,f) : cons(c,A) -> cons(b,B)";
857
f5314a7c93f2 Renamed single_fun to singleton_fun.
lcp
parents: 824
diff changeset
   358
by (forward_tac [singleton_fun RS fun_disjoint_Un] 1);
519
98b88551e102 ZF/func/empty_fun: renamed from fun_empty
lcp
parents: 517
diff changeset
   359
by (asm_full_simp_tac (FOL_ss addsimps [cons_eq]) 2);
98b88551e102 ZF/func/empty_fun: renamed from fun_empty
lcp
parents: 517
diff changeset
   360
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
   361
qed "fun_extend";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   362
538
b4fe3da03449 ZF/func/fun_extend3: new
lcp
parents: 519
diff changeset
   363
goal ZF.thy
b4fe3da03449 ZF/func/fun_extend3: new
lcp
parents: 519
diff changeset
   364
    "!!f A B. [| f: A->B;  c~:A;  b: B |] ==> cons(<c,b>,f) : cons(c,A) -> B";
b4fe3da03449 ZF/func/fun_extend3: new
lcp
parents: 519
diff changeset
   365
by (fast_tac (ZF_cs addEs [fun_extend RS fun_weaken_type]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
   366
qed "fun_extend3";
538
b4fe3da03449 ZF/func/fun_extend3: new
lcp
parents: 519
diff changeset
   367
37
cebe01deba80 added ~: for "not in"
lcp
parents: 14
diff changeset
   368
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
   369
by (rtac (apply_Pair RS consI2 RS apply_equality) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   370
by (rtac fun_extend 3);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   371
by (REPEAT (assume_tac 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
   372
qed "fun_extend_apply1";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   373
37
cebe01deba80 added ~: for "not in"
lcp
parents: 14
diff changeset
   374
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
   375
by (rtac (consI1 RS apply_equality) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   376
by (rtac fun_extend 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   377
by (REPEAT (assume_tac 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
   378
qed "fun_extend_apply2";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   379
538
b4fe3da03449 ZF/func/fun_extend3: new
lcp
parents: 519
diff changeset
   380
(*For Finite.ML.  Inclusion of right into left is easy*)
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 437
diff changeset
   381
goal ZF.thy
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 437
diff changeset
   382
    "!!c. c ~: A ==> cons(c,A) -> B = (UN f: A->B. UN b:B. {cons(<c,b>, f)})";
737
436019ca97d7 cons_fun_eq: modified strange uses of classical reasoner
lcp
parents: 691
diff changeset
   383
by (rtac equalityI 1);
436019ca97d7 cons_fun_eq: modified strange uses of classical reasoner
lcp
parents: 691
diff changeset
   384
by (safe_tac (ZF_cs addSEs [fun_extend3]));
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 437
diff changeset
   385
(*Inclusion of left into right*)
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 437
diff changeset
   386
by (subgoal_tac "restrict(x, A) : A -> B" 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 437
diff changeset
   387
by (fast_tac (ZF_cs addEs [restrict_type2]) 2);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 437
diff changeset
   388
by (rtac UN_I 1 THEN assume_tac 1);
737
436019ca97d7 cons_fun_eq: modified strange uses of classical reasoner
lcp
parents: 691
diff changeset
   389
by (rtac (apply_funtype RS UN_I) 1 THEN REPEAT (ares_tac [consI1] 1));
538
b4fe3da03449 ZF/func/fun_extend3: new
lcp
parents: 519
diff changeset
   390
by (simp_tac (FOL_ss addsimps cons_iff::mem_simps) 1);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 857
diff changeset
   391
by (rtac fun_extension 1 THEN REPEAT (ares_tac [fun_extend] 1));
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 437
diff changeset
   392
by (etac consE 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 437
diff changeset
   393
by (ALLGOALS 
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 437
diff changeset
   394
    (asm_simp_tac (FOL_ss addsimps [restrict, fun_extend_apply1, 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 857
diff changeset
   395
                                    fun_extend_apply2])));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 737
diff changeset
   396
qed "cons_fun_eq";
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 437
diff changeset
   397