src/ZF/func.ML
author lcp
Fri, 17 Sep 1993 16:16:38 +0200
changeset 6 8ce8c4d13d4d
parent 0 a5a9c433f639
child 14 1c0926788772
permissions -rw-r--r--
Installation of new simplifier for ZF. Deleted all congruence rules not involving local assumptions. NB the congruence rules for Sigma and Pi (dependent type constructions) cause difficulties and are not used by default.
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
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
(*Weaking one function type to another*)
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
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
(*** Function Application ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
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
    63
by (etac PiE 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
by (etac (bspec RS ex1_equalsE) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
by (etac (subsetD RS SigmaD1) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
by (REPEAT (assume_tac 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
val apply_equality2 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
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
    70
by (rtac the_equality 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
by (rtac apply_equality2 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
by (REPEAT (assume_tac 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
val apply_equality = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
val prems = goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
    "[| f: Pi(A,B);   c: f;   !!x. [| x:A;  c = <x,f`x> |] ==> P  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
\    |] ==> P";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
by (cut_facts_tac prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
by (etac (fun_is_rel RS subsetD RS SigmaE) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
by (REPEAT (ares_tac prems 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
by (hyp_subst_tac 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
by (etac (apply_equality RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
by (resolve_tac prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
by (rtac refl 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
val memberPiE = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    87
(*Conclusion is flexible -- use res_inst_tac or else apply_funtype below!*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
goal ZF.thy "!!f. [| f: Pi(A,B);  a:A |] ==> f`a : B(a)"; 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
by (rtac (fun_unique_Pair RS ex1E) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
by (REPEAT (assume_tac 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
by (rtac (fun_is_rel RS subsetD RS SigmaE2) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
by (etac (apply_equality RS ssubst) 3);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
by (REPEAT (assume_tac 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
val apply_type = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    96
(*This version is acceptable to the simplifier*)
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    97
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
    98
by (REPEAT (ares_tac [apply_type] 1));
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    99
val apply_funtype = result();
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   100
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
goal ZF.thy "!!f. [| f: Pi(A,B);  a:A |] ==> <a,f`a>: f";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
by (rtac (fun_unique_Pair RS ex1E) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
by (resolve_tac [apply_equality RS ssubst] 3);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
by (REPEAT (assume_tac 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
val apply_Pair = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
val [major] = goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
    "f: Pi(A,B) ==> <a,b>: f <-> a:A & f`a = b";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
by (rtac (major RS PiE) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
by (fast_tac (ZF_cs addSIs [major RS apply_Pair, 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
			    major RSN (2,apply_equality)]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
val apply_iff = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
(*Refining one Pi type to another*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
val prems = goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
    "[| f: Pi(A,C);  !!x. x:A ==> f`x : B(x) |] ==> f : Pi(A,B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
by (rtac (subsetI RS PiI) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
by (eresolve_tac (prems RL [memberPiE]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
by (etac ssubst 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
by (REPEAT (ares_tac (prems@[SigmaI,fun_unique_Pair]) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
val Pi_type = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
(** Elimination of membership in a function **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
goal ZF.thy "!!a A. [| <a,b> : f;  f: Pi(A,B) |] ==> a : A";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
by (REPEAT (ares_tac [fun_is_rel RS subsetD RS SigmaD1] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
val domain_type = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
goal ZF.thy "!!b B a. [| <a,b> : f;  f: Pi(A,B) |] ==> b : B(a)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
by (etac (fun_is_rel RS subsetD RS SigmaD2) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
by (assume_tac 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
val range_type = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   135
val prems = goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
    "[| <a,b>: f;  f: Pi(A,B);       \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   137
\       [| a:A;  b:B(a);  f`a = b |] ==> P  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   138
\    |] ==> P";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   139
by (cut_facts_tac prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   140
by (resolve_tac prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   141
by (REPEAT (eresolve_tac [asm_rl,domain_type,range_type,apply_equality] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   142
val Pair_mem_PiE = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   143
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   144
(*** Lambda Abstraction ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   145
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   146
goalw ZF.thy [lam_def] "!!A b. a:A ==> <a,b(a)> : (lam x:A. b(x))";  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   147
by (etac RepFunI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   148
val lamI = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   149
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   150
val major::prems = goalw ZF.thy [lam_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   151
    "[| p: (lam x:A. b(x));  !!x.[| x:A; p=<x,b(x)> |] ==> P  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
\    |] ==>  P";  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   153
by (rtac (major RS RepFunE) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   154
by (REPEAT (ares_tac prems 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   155
val lamE = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   156
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   157
goal ZF.thy "!!a b c. [| <a,c>: (lam x:A. b(x)) |] ==> c = b(a)";  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   158
by (REPEAT (eresolve_tac [asm_rl,lamE,Pair_inject,ssubst] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   159
val lamD = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   160
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   161
val prems = goalw ZF.thy [lam_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   162
    "[| !!x. x:A ==> b(x): B(x) |] ==> (lam x:A.b(x)) : Pi(A,B)";  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   163
by (fast_tac (ZF_cs addIs (PiI::prems)) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   164
val lam_type = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   165
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   166
goal ZF.thy "(lam x:A.b(x)) : A -> {b(x). x:A}";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   167
by (REPEAT (ares_tac [refl,lam_type,RepFunI] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   168
val lam_funtype = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   169
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   170
goal ZF.thy "!!a A. a : A ==> (lam x:A.b(x)) ` a = b(a)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   171
by (REPEAT (ares_tac [apply_equality,lam_funtype,lamI] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   172
val beta = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   173
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   174
(*congruence rule for lambda abstraction*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   175
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
   176
    "[| 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
   177
by (simp_tac (FOL_ss addsimps prems addcongs [RepFun_cong]) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   178
val lam_cong = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   179
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   180
val [major] = goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   181
    "(!!x. x:A ==> EX! y. Q(x,y)) ==> EX f. ALL x:A. Q(x, f`x)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   182
by (res_inst_tac [("x", "lam x: A. THE y. Q(x,y)")] exI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   183
by (rtac ballI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   184
by (rtac (beta RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   185
by (assume_tac 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   186
by (etac (major RS theI) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   187
val lam_theI = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   188
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   189
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   190
(** Extensionality **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   191
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   192
(*Semi-extensionality!*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   193
val prems = goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   194
    "[| f : Pi(A,B);  g: Pi(C,D);  A<=C; \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   195
\       !!x. x:A ==> f`x = g`x       |] ==> f<=g";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   196
by (rtac subsetI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   197
by (eresolve_tac (prems RL [memberPiE]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   198
by (etac ssubst 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   199
by (resolve_tac (prems RL [ssubst]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   200
by (REPEAT (ares_tac (prems@[apply_Pair,subsetD]) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   201
val fun_subset = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   202
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   203
val prems = goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   204
    "[| f : Pi(A,B);  g: Pi(A,D);  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   205
\       !!x. x:A ==> f`x = g`x       |] ==> f=g";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   206
by (REPEAT (ares_tac (prems @ (prems RL [sym]) @
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   207
		      [subset_refl,equalityI,fun_subset]) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   208
val fun_extension = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   209
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   210
goal ZF.thy "!!f A B. f : Pi(A,B) ==> (lam x:A. f`x) = f";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   211
by (rtac fun_extension 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   212
by (REPEAT (ares_tac [lam_type,apply_type,beta] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   213
val eta = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   214
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   215
(*Every element of Pi(A,B) may be expressed as a lambda abstraction!*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   216
val prems = goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   217
    "[| f: Pi(A,B);        \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   218
\       !!b. [| ALL x:A. b(x):B(x);  f = (lam x:A.b(x)) |] ==> P   \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   219
\    |] ==> P";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   220
by (resolve_tac prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   221
by (rtac (eta RS sym) 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   222
by (REPEAT (ares_tac (prems@[ballI,apply_type]) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   223
val Pi_lamE = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   224
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   225
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   226
(*** properties of "restrict" ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   227
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   228
goalw ZF.thy [restrict_def,lam_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   229
    "!!f A. [| f: Pi(C,B);  A<=C |] ==> restrict(f,A) <= f";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   230
by (fast_tac (ZF_cs addIs [apply_Pair]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   231
val restrict_subset = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   232
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   233
val prems = goalw ZF.thy [restrict_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   234
    "[| !!x. x:A ==> f`x: B(x) |] ==> restrict(f,A) : Pi(A,B)";  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   235
by (rtac lam_type 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   236
by (eresolve_tac prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   237
val restrict_type = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   238
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   239
val [pi,subs] = goal ZF.thy 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   240
    "[| f: Pi(C,B);  A<=C |] ==> restrict(f,A) : Pi(A,B)";  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   241
by (rtac (pi RS apply_type RS restrict_type) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   242
by (etac (subs RS subsetD) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   243
val restrict_type2 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   244
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   245
goalw ZF.thy [restrict_def] "!!a A. a : A ==> restrict(f,A) ` a = f`a";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   246
by (etac beta 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   247
val restrict = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   248
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   249
(*NOT SAFE as a congruence rule for the simplifier!  Can cause it to fail!*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   250
val prems = goalw ZF.thy [restrict_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   251
    "[| A=B;  !!x. x:B ==> f`x=g`x |] ==> restrict(f,A) = restrict(g,B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   252
by (REPEAT (ares_tac (prems@[lam_cong]) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   253
val restrict_eqI = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   254
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   255
goalw ZF.thy [restrict_def] "domain(restrict(f,C)) = C";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   256
by (REPEAT (ares_tac [equalityI,subsetI,domainI,lamI] 1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   257
     ORELSE eresolve_tac [domainE,lamE,Pair_inject,ssubst] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   258
val domain_restrict = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   259
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   260
val [prem] = goalw ZF.thy [restrict_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   261
    "A<=C ==> restrict(lam x:C. b(x), A) = (lam x:A. b(x))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   262
by (rtac (refl RS lam_cong) 1);
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   263
be (prem RS subsetD RS beta) 1;	(*easier than calling simp_tac*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   264
val restrict_lam_eq = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   265
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   266
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   267
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   268
(*** Unions of functions ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   269
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   270
(** The Union of a set of COMPATIBLE functions is a function **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   271
val [ex_prem,disj_prem] = goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   272
    "[| ALL x:S. EX C D. x:C->D; \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   273
\       !!x y. [| x:S;  y:S |] ==> x<=y | y<=x  |] ==>  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   274
\    Union(S) : domain(Union(S)) -> range(Union(S))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   275
val premE = ex_prem RS bspec RS exE;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   276
by (REPEAT (eresolve_tac [exE,PiE,premE] 1 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   277
     ORELSE ares_tac [PiI, ballI RS rel_Union, exI] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   278
by (REPEAT (eresolve_tac [asm_rl,domainE,UnionE,exE] 1 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   279
     ORELSE ares_tac [allI,impI,ex1I,UnionI] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   280
by (res_inst_tac [ ("x1","B") ] premE 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   281
by (res_inst_tac [ ("x1","Ba") ] premE 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   282
by (REPEAT (eresolve_tac [asm_rl,exE] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   283
by (eresolve_tac [disj_prem RS disjE] 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   284
by (DEPTH_SOLVE (set_mp_tac 1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   285
		 ORELSE eresolve_tac [asm_rl, apply_equality2] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   286
val fun_Union = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   287
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   288
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   289
(** The Union of 2 disjoint functions is a function **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   290
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   291
val prems = goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   292
    "[| f: A->B;  g: C->D;  A Int C = 0  |] ==>  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   293
\    (f Un g) : (A Un C) -> (B Un D)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   294
     (*Contradiction if A Int C = 0, a:A, a:B*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   295
val [disjoint] = prems RL ([IntI] RLN (2, [equals0D]));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   296
by (cut_facts_tac prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   297
by (rtac PiI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   298
(*solve subgoal 2 first!!*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   299
by (DEPTH_SOLVE_1 (eresolve_tac [UnE, Pair_mem_PiE, sym, disjoint] 2
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   300
       INTLEAVE ares_tac [ex1I, apply_Pair RS UnI1, apply_Pair RS UnI2] 2));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   301
by (REPEAT (eresolve_tac [asm_rl,UnE,rel_Un,PiE] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   302
val fun_disjoint_Un = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   303
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   304
goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   305
    "!!f g a. [| a:A;  f: A->B;  g: C->D;  A Int C = 0 |] ==>  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   306
\             (f Un g)`a = f`a";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   307
by (REPEAT (ares_tac [apply_equality,UnI1,apply_Pair,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   308
		      fun_disjoint_Un] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   309
val fun_disjoint_apply1 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   310
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   311
goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   312
    "!!f g c. [| c:C;  f: A->B;  g: C->D;  A Int C = 0 |] ==>  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   313
\             (f Un g)`c = g`c";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   314
by (REPEAT (ares_tac [apply_equality,UnI2,apply_Pair,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   315
		      fun_disjoint_Un] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   316
val fun_disjoint_apply2 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   317
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   318
(** Domain and range of a function/relation **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   319
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   320
val [major] = goal ZF.thy "f : Pi(A,B) ==> domain(f)=A";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   321
by (rtac equalityI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   322
by (fast_tac (ZF_cs addIs [major RS apply_Pair]) 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   323
by (rtac (major RS PiE) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   324
by (fast_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   325
val domain_of_fun = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   326
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   327
val [major] = goal ZF.thy "f : Pi(A,B) ==> f : A->range(f)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   328
by (rtac (major RS Pi_type) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   329
by (etac (major RS apply_Pair RS rangeI) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   330
val range_of_fun = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   331
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   332
(*** Extensions of functions ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   333
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   334
(*Singleton function -- in the underlying form of singletons*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   335
goal ZF.thy "Upair(<a,b>,<a,b>) : Upair(a,a) -> Upair(b,b)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   336
by (fast_tac (ZF_cs addIs [PiI]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   337
val fun_single_lemma = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   338
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   339
goalw ZF.thy [cons_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   340
    "!!f A B. [| f: A->B;  ~c:A |] ==> cons(<c,b>,f) : cons(c,A) -> cons(b,B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   341
by (rtac (fun_single_lemma RS fun_disjoint_Un) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   342
by (assume_tac 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   343
by (rtac equals0I 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   344
by (fast_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   345
val fun_extend = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   346
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   347
goal ZF.thy "!!f A B. [| f: A->B;  a:A;  ~ c:A |] ==> cons(<c,b>,f)`a = f`a";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   348
by (rtac (apply_Pair RS consI2 RS apply_equality) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   349
by (rtac fun_extend 3);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   350
by (REPEAT (assume_tac 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   351
val fun_extend_apply1 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   352
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   353
goal ZF.thy "!!f A B. [| f: A->B;  ~ c:A |] ==> cons(<c,b>,f)`c = b";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   354
by (rtac (consI1 RS apply_equality) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   355
by (rtac fun_extend 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   356
by (REPEAT (assume_tac 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   357
val fun_extend_apply2 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   358
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   359
(*The empty function*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   360
goal ZF.thy "0: 0->A";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   361
by (fast_tac (ZF_cs addIs [PiI]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   362
val fun_empty = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   363
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   364
(*The singleton function*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   365
goal ZF.thy "{<a,b>} : {a} -> cons(b,C)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   366
by (REPEAT (ares_tac [fun_extend,fun_empty,notI] 1 ORELSE etac emptyE 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   367
val fun_single = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   368