src/ZF/func.ML
author lcp
Thu, 30 Sep 1993 10:10:21 +0100
changeset 14 1c0926788772
parent 6 8ce8c4d13d4d
child 37 cebe01deba80
permissions -rw-r--r--
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext domrange/image_subset,vimage_subset: deleted needless premise! misc: This slightly simplifies two proofs in Schroeder-Bernstein Theorem ind-syntax/rule_concl: recoded to avoid exceptions intr-elim: now checks conclusions of introduction rules func/fun_disjoint_Un: now uses ex_ex1I list-fn/hd,tl,drop: new simpdata/bquant_simps: new list/list_case_type: restored! bool.thy: changed 1 from a "def" to a translation Removed occurreces of one_def in bool.ML, nat.ML, univ.ML, ex/integ.ML nat/succ_less_induct: new induction principle arith/add_mono: new results about monotonicity simpdata/mem_simps: removed the ones for succ and cons; added succI1, consI2 to ZF_ss upair/succ_iff: new, for use with simp_tac (cons_iff already existed) ordinal/Ord_0_in_succ: renamed from Ord_0_mem_succ nat/nat_0_in_succ: new ex/prop-log/hyps_thms_if: split up the fast_tac call for more speed
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]));
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   296
val Pair_UnE = read_instantiate [("c","<?a,?b>")] UnE;  (* ignores x: A Un C *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   297
by (cut_facts_tac prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   298
by (rtac PiI 1);
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   299
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
   300
by (rtac ex_ex1I 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   301
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
   302
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
   303
	     ORELSE' eresolve_tac [Pair_mem_PiE,disjoint] THEN' atac));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   304
val fun_disjoint_Un = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   305
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   306
goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   307
    "!!f g a. [| a:A;  f: A->B;  g: C->D;  A Int C = 0 |] ==>  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   308
\             (f Un g)`a = f`a";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   309
by (REPEAT (ares_tac [apply_equality,UnI1,apply_Pair,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   310
		      fun_disjoint_Un] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   311
val fun_disjoint_apply1 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   312
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   313
goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   314
    "!!f g c. [| c:C;  f: A->B;  g: C->D;  A Int C = 0 |] ==>  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   315
\             (f Un g)`c = g`c";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   316
by (REPEAT (ares_tac [apply_equality,UnI2,apply_Pair,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   317
		      fun_disjoint_Un] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   318
val fun_disjoint_apply2 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   319
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   320
(** Domain and range of a function/relation **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   321
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   322
val [major] = goal ZF.thy "f : Pi(A,B) ==> domain(f)=A";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   323
by (rtac equalityI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   324
by (fast_tac (ZF_cs addIs [major RS apply_Pair]) 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   325
by (rtac (major RS PiE) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   326
by (fast_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   327
val domain_of_fun = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   328
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   329
val [major] = goal ZF.thy "f : Pi(A,B) ==> f : A->range(f)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   330
by (rtac (major RS Pi_type) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   331
by (etac (major RS apply_Pair RS rangeI) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   332
val range_of_fun = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   333
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   334
(*** Extensions of functions ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   335
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   336
(*Singleton function -- in the underlying form of singletons*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   337
goal ZF.thy "Upair(<a,b>,<a,b>) : Upair(a,a) -> Upair(b,b)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   338
by (fast_tac (ZF_cs addIs [PiI]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   339
val fun_single_lemma = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   340
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   341
goalw ZF.thy [cons_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   342
    "!!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
   343
by (rtac (fun_single_lemma RS fun_disjoint_Un) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   344
by (assume_tac 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   345
by (rtac equals0I 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   346
by (fast_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   347
val fun_extend = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   348
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   349
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
   350
by (rtac (apply_Pair RS consI2 RS apply_equality) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   351
by (rtac fun_extend 3);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   352
by (REPEAT (assume_tac 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   353
val fun_extend_apply1 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   354
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   355
goal ZF.thy "!!f A B. [| f: A->B;  ~ c:A |] ==> cons(<c,b>,f)`c = b";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   356
by (rtac (consI1 RS apply_equality) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   357
by (rtac fun_extend 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   358
by (REPEAT (assume_tac 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   359
val fun_extend_apply2 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   360
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   361
(*The empty function*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   362
goal ZF.thy "0: 0->A";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   363
by (fast_tac (ZF_cs addIs [PiI]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   364
val fun_empty = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   365
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   366
(*The singleton function*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   367
goal ZF.thy "{<a,b>} : {a} -> cons(b,C)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   368
by (REPEAT (ares_tac [fun_extend,fun_empty,notI] 1 ORELSE etac emptyE 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   369
val fun_single = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   370