--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/func.ML Thu Sep 16 12:20:38 1993 +0200
@@ -0,0 +1,367 @@
+(* Title: ZF/func
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1991 University of Cambridge
+
+Functions in Zermelo-Fraenkel Set Theory
+*)
+
+(*** The Pi operator -- dependent function space ***)
+
+val prems = goalw ZF.thy [Pi_def]
+ "[| f <= Sigma(A,B); !!x. x:A ==> EX! y. <x,y>: f |] ==> \
+\ f: Pi(A,B)";
+by (REPEAT (ares_tac (prems @ [CollectI,PowI,ballI,impI]) 1));
+val PiI = result();
+
+(**Two "destruct" rules for Pi **)
+
+val [major] = goalw ZF.thy [Pi_def] "f: Pi(A,B) ==> f <= Sigma(A,B)";
+by (rtac (major RS CollectE) 1);
+by (etac PowD 1);
+val fun_is_rel = result();
+
+val major::prems = goalw ZF.thy [Pi_def]
+ "[| f: Pi(A,B); a:A |] ==> EX! y. <a,y>: f";
+by (rtac (major RS CollectE) 1);
+by (etac bspec 1);
+by (resolve_tac prems 1);
+val fun_unique_Pair = result();
+
+val prems = goal ZF.thy
+ "[| f: Pi(A,B); \
+\ [| f <= Sigma(A,B); ALL x:A. EX! y. <x,y>: f |] ==> P \
+\ |] ==> P";
+by (REPEAT (ares_tac (prems@[ballI,fun_is_rel,fun_unique_Pair]) 1));
+val PiE = result();
+
+val prems = goalw ZF.thy [Pi_def]
+ "[| A=A'; !!x. x:A' ==> B(x)=B'(x) |] ==> Pi(A,B) = Pi(A',B')";
+by (prove_cong_tac (prems@[Collect_cong,Sigma_cong,ball_cong]) 1);
+val Pi_cong = result();
+
+(*Weaking one function type to another*)
+goalw ZF.thy [Pi_def] "!!f. [| f: A->B; B<=D |] ==> f: A->D";
+by (safe_tac ZF_cs);
+by (set_mp_tac 1);
+by (fast_tac ZF_cs 1);
+val fun_weaken_type = result();
+
+(*Empty function spaces*)
+goalw ZF.thy [Pi_def] "Pi(0,A) = {0}";
+by (fast_tac (ZF_cs addIs [equalityI]) 1);
+val Pi_empty1 = result();
+
+goalw ZF.thy [Pi_def] "!!A a. a:A ==> A->0 = 0";
+by (fast_tac (ZF_cs addIs [equalityI]) 1);
+val Pi_empty2 = result();
+
+
+(*** Function Application ***)
+
+goal ZF.thy "!!a b f. [| <a,b>: f; <a,c>: f; f: Pi(A,B) |] ==> b=c";
+by (etac PiE 1);
+by (etac (bspec RS ex1_equalsE) 1);
+by (etac (subsetD RS SigmaD1) 1);
+by (REPEAT (assume_tac 1));
+val apply_equality2 = result();
+
+goalw ZF.thy [apply_def] "!!a b f. [| <a,b>: f; f: Pi(A,B) |] ==> f`a = b";
+by (rtac the_equality 1);
+by (rtac apply_equality2 2);
+by (REPEAT (assume_tac 1));
+val apply_equality = result();
+
+val prems = goal ZF.thy
+ "[| f: Pi(A,B); c: f; !!x. [| x:A; c = <x,f`x> |] ==> P \
+\ |] ==> P";
+by (cut_facts_tac prems 1);
+by (etac (fun_is_rel RS subsetD RS SigmaE) 1);
+by (REPEAT (ares_tac prems 1));
+by (hyp_subst_tac 1);
+by (etac (apply_equality RS ssubst) 1);
+by (resolve_tac prems 1);
+by (rtac refl 1);
+val memberPiE = result();
+
+(*Conclusion is flexible -- use res_inst_tac or else RS with a theorem
+ of the form f:A->B *)
+goal ZF.thy "!!f. [| f: Pi(A,B); a:A |] ==> f`a : B(a)";
+by (rtac (fun_unique_Pair RS ex1E) 1);
+by (REPEAT (assume_tac 1));
+by (rtac (fun_is_rel RS subsetD RS SigmaE2) 1);
+by (etac (apply_equality RS ssubst) 3);
+by (REPEAT (assume_tac 1));
+val apply_type = result();
+
+goal ZF.thy "!!f. [| f: Pi(A,B); a:A |] ==> <a,f`a>: f";
+by (rtac (fun_unique_Pair RS ex1E) 1);
+by (resolve_tac [apply_equality RS ssubst] 3);
+by (REPEAT (assume_tac 1));
+val apply_Pair = result();
+
+val [major] = goal ZF.thy
+ "f: Pi(A,B) ==> <a,b>: f <-> a:A & f`a = b";
+by (rtac (major RS PiE) 1);
+by (fast_tac (ZF_cs addSIs [major RS apply_Pair,
+ major RSN (2,apply_equality)]) 1);
+val apply_iff = result();
+
+(*Refining one Pi type to another*)
+val prems = goal ZF.thy
+ "[| f: Pi(A,C); !!x. x:A ==> f`x : B(x) |] ==> f : Pi(A,B)";
+by (rtac (subsetI RS PiI) 1);
+by (eresolve_tac (prems RL [memberPiE]) 1);
+by (etac ssubst 1);
+by (REPEAT (ares_tac (prems@[SigmaI,fun_unique_Pair]) 1));
+val Pi_type = result();
+
+
+(** Elimination of membership in a function **)
+
+goal ZF.thy "!!a A. [| <a,b> : f; f: Pi(A,B) |] ==> a : A";
+by (REPEAT (ares_tac [fun_is_rel RS subsetD RS SigmaD1] 1));
+val domain_type = result();
+
+goal ZF.thy "!!b B a. [| <a,b> : f; f: Pi(A,B) |] ==> b : B(a)";
+by (etac (fun_is_rel RS subsetD RS SigmaD2) 1);
+by (assume_tac 1);
+val range_type = result();
+
+val prems = goal ZF.thy
+ "[| <a,b>: f; f: Pi(A,B); \
+\ [| a:A; b:B(a); f`a = b |] ==> P \
+\ |] ==> P";
+by (cut_facts_tac prems 1);
+by (resolve_tac prems 1);
+by (REPEAT (eresolve_tac [asm_rl,domain_type,range_type,apply_equality] 1));
+val Pair_mem_PiE = result();
+
+(*** Lambda Abstraction ***)
+
+goalw ZF.thy [lam_def] "!!A b. a:A ==> <a,b(a)> : (lam x:A. b(x))";
+by (etac RepFunI 1);
+val lamI = result();
+
+val major::prems = goalw ZF.thy [lam_def]
+ "[| p: (lam x:A. b(x)); !!x.[| x:A; p=<x,b(x)> |] ==> P \
+\ |] ==> P";
+by (rtac (major RS RepFunE) 1);
+by (REPEAT (ares_tac prems 1));
+val lamE = result();
+
+goal ZF.thy "!!a b c. [| <a,c>: (lam x:A. b(x)) |] ==> c = b(a)";
+by (REPEAT (eresolve_tac [asm_rl,lamE,Pair_inject,ssubst] 1));
+val lamD = result();
+
+val prems = goalw ZF.thy [lam_def]
+ "[| !!x. x:A ==> b(x): B(x) |] ==> (lam x:A.b(x)) : Pi(A,B)";
+by (fast_tac (ZF_cs addIs (PiI::prems)) 1);
+val lam_type = result();
+
+goal ZF.thy "(lam x:A.b(x)) : A -> {b(x). x:A}";
+by (REPEAT (ares_tac [refl,lam_type,RepFunI] 1));
+val lam_funtype = result();
+
+goal ZF.thy "!!a A. a : A ==> (lam x:A.b(x)) ` a = b(a)";
+by (REPEAT (ares_tac [apply_equality,lam_funtype,lamI] 1));
+val beta = result();
+
+(*congruence rule for lambda abstraction*)
+val prems = goalw ZF.thy [lam_def]
+ "[| A=A'; !!x. x:A' ==> b(x)=b'(x) |] ==> \
+\ (lam x:A.b(x)) = (lam x:A'.b'(x))";
+by (rtac RepFun_cong 1);
+by (res_inst_tac [("t","Pair")] subst_context2 2);
+by (REPEAT (ares_tac (prems@[refl]) 1));
+val lam_cong = result();
+
+val [major] = goal ZF.thy
+ "(!!x. x:A ==> EX! y. Q(x,y)) ==> EX f. ALL x:A. Q(x, f`x)";
+by (res_inst_tac [("x", "lam x: A. THE y. Q(x,y)")] exI 1);
+by (rtac ballI 1);
+by (rtac (beta RS ssubst) 1);
+by (assume_tac 1);
+by (etac (major RS theI) 1);
+val lam_theI = result();
+
+
+(** Extensionality **)
+
+(*Semi-extensionality!*)
+val prems = goal ZF.thy
+ "[| f : Pi(A,B); g: Pi(C,D); A<=C; \
+\ !!x. x:A ==> f`x = g`x |] ==> f<=g";
+by (rtac subsetI 1);
+by (eresolve_tac (prems RL [memberPiE]) 1);
+by (etac ssubst 1);
+by (resolve_tac (prems RL [ssubst]) 1);
+by (REPEAT (ares_tac (prems@[apply_Pair,subsetD]) 1));
+val fun_subset = result();
+
+val prems = goal ZF.thy
+ "[| f : Pi(A,B); g: Pi(A,D); \
+\ !!x. x:A ==> f`x = g`x |] ==> f=g";
+by (REPEAT (ares_tac (prems @ (prems RL [sym]) @
+ [subset_refl,equalityI,fun_subset]) 1));
+val fun_extension = result();
+
+goal ZF.thy "!!f A B. f : Pi(A,B) ==> (lam x:A. f`x) = f";
+by (rtac fun_extension 1);
+by (REPEAT (ares_tac [lam_type,apply_type,beta] 1));
+val eta = result();
+
+(*Every element of Pi(A,B) may be expressed as a lambda abstraction!*)
+val prems = goal ZF.thy
+ "[| f: Pi(A,B); \
+\ !!b. [| ALL x:A. b(x):B(x); f = (lam x:A.b(x)) |] ==> P \
+\ |] ==> P";
+by (resolve_tac prems 1);
+by (rtac (eta RS sym) 2);
+by (REPEAT (ares_tac (prems@[ballI,apply_type]) 1));
+val Pi_lamE = result();
+
+
+(*** properties of "restrict" ***)
+
+goalw ZF.thy [restrict_def,lam_def]
+ "!!f A. [| f: Pi(C,B); A<=C |] ==> restrict(f,A) <= f";
+by (fast_tac (ZF_cs addIs [apply_Pair]) 1);
+val restrict_subset = result();
+
+val prems = goalw ZF.thy [restrict_def]
+ "[| !!x. x:A ==> f`x: B(x) |] ==> restrict(f,A) : Pi(A,B)";
+by (rtac lam_type 1);
+by (eresolve_tac prems 1);
+val restrict_type = result();
+
+val [pi,subs] = goal ZF.thy
+ "[| f: Pi(C,B); A<=C |] ==> restrict(f,A) : Pi(A,B)";
+by (rtac (pi RS apply_type RS restrict_type) 1);
+by (etac (subs RS subsetD) 1);
+val restrict_type2 = result();
+
+goalw ZF.thy [restrict_def] "!!a A. a : A ==> restrict(f,A) ` a = f`a";
+by (etac beta 1);
+val restrict = result();
+
+(*NOT SAFE as a congruence rule for the simplifier! Can cause it to fail!*)
+val prems = goalw ZF.thy [restrict_def]
+ "[| A=B; !!x. x:B ==> f`x=g`x |] ==> restrict(f,A) = restrict(g,B)";
+by (REPEAT (ares_tac (prems@[lam_cong]) 1));
+val restrict_eqI = result();
+
+goalw ZF.thy [restrict_def] "domain(restrict(f,C)) = C";
+by (REPEAT (ares_tac [equalityI,subsetI,domainI,lamI] 1
+ ORELSE eresolve_tac [domainE,lamE,Pair_inject,ssubst] 1));
+val domain_restrict = result();
+
+val [prem] = goalw ZF.thy [restrict_def]
+ "A<=C ==> restrict(lam x:C. b(x), A) = (lam x:A. b(x))";
+by (rtac (refl RS lam_cong) 1);
+be (prem RS subsetD RS beta) 1; (*easier than calling SIMP_TAC*)
+val restrict_lam_eq = result();
+
+
+
+(*** Unions of functions ***)
+
+(** The Union of a set of COMPATIBLE functions is a function **)
+val [ex_prem,disj_prem] = goal ZF.thy
+ "[| ALL x:S. EX C D. x:C->D; \
+\ !!x y. [| x:S; y:S |] ==> x<=y | y<=x |] ==> \
+\ Union(S) : domain(Union(S)) -> range(Union(S))";
+val premE = ex_prem RS bspec RS exE;
+by (REPEAT (eresolve_tac [exE,PiE,premE] 1
+ ORELSE ares_tac [PiI, ballI RS rel_Union, exI] 1));
+by (REPEAT (eresolve_tac [asm_rl,domainE,UnionE,exE] 1
+ ORELSE ares_tac [allI,impI,ex1I,UnionI] 1));
+by (res_inst_tac [ ("x1","B") ] premE 1);
+by (res_inst_tac [ ("x1","Ba") ] premE 2);
+by (REPEAT (eresolve_tac [asm_rl,exE] 1));
+by (eresolve_tac [disj_prem RS disjE] 1);
+by (DEPTH_SOLVE (set_mp_tac 1
+ ORELSE eresolve_tac [asm_rl, apply_equality2] 1));
+val fun_Union = result();
+
+
+(** The Union of 2 disjoint functions is a function **)
+
+val prems = goal ZF.thy
+ "[| f: A->B; g: C->D; A Int C = 0 |] ==> \
+\ (f Un g) : (A Un C) -> (B Un D)";
+ (*Contradiction if A Int C = 0, a:A, a:B*)
+val [disjoint] = prems RL ([IntI] RLN (2, [equals0D]));
+by (cut_facts_tac prems 1);
+by (rtac PiI 1);
+(*solve subgoal 2 first!!*)
+by (DEPTH_SOLVE_1 (eresolve_tac [UnE, Pair_mem_PiE, sym, disjoint] 2
+ INTLEAVE ares_tac [ex1I, apply_Pair RS UnI1, apply_Pair RS UnI2] 2));
+by (REPEAT (eresolve_tac [asm_rl,UnE,rel_Un,PiE] 1));
+val fun_disjoint_Un = result();
+
+goal ZF.thy
+ "!!f g a. [| a:A; f: A->B; g: C->D; A Int C = 0 |] ==> \
+\ (f Un g)`a = f`a";
+by (REPEAT (ares_tac [apply_equality,UnI1,apply_Pair,
+ fun_disjoint_Un] 1));
+val fun_disjoint_apply1 = result();
+
+goal ZF.thy
+ "!!f g c. [| c:C; f: A->B; g: C->D; A Int C = 0 |] ==> \
+\ (f Un g)`c = g`c";
+by (REPEAT (ares_tac [apply_equality,UnI2,apply_Pair,
+ fun_disjoint_Un] 1));
+val fun_disjoint_apply2 = result();
+
+(** Domain and range of a function/relation **)
+
+val [major] = goal ZF.thy "f : Pi(A,B) ==> domain(f)=A";
+by (rtac equalityI 1);
+by (fast_tac (ZF_cs addIs [major RS apply_Pair]) 2);
+by (rtac (major RS PiE) 1);
+by (fast_tac ZF_cs 1);
+val domain_of_fun = result();
+
+val [major] = goal ZF.thy "f : Pi(A,B) ==> f : A->range(f)";
+by (rtac (major RS Pi_type) 1);
+by (etac (major RS apply_Pair RS rangeI) 1);
+val range_of_fun = result();
+
+(*** Extensions of functions ***)
+
+(*Singleton function -- in the underlying form of singletons*)
+goal ZF.thy "Upair(<a,b>,<a,b>) : Upair(a,a) -> Upair(b,b)";
+by (fast_tac (ZF_cs addIs [PiI]) 1);
+val fun_single_lemma = result();
+
+goalw ZF.thy [cons_def]
+ "!!f A B. [| f: A->B; ~c:A |] ==> cons(<c,b>,f) : cons(c,A) -> cons(b,B)";
+by (rtac (fun_single_lemma RS fun_disjoint_Un) 1);
+by (assume_tac 1);
+by (rtac equals0I 1);
+by (fast_tac ZF_cs 1);
+val fun_extend = result();
+
+goal ZF.thy "!!f A B. [| f: A->B; a:A; ~ c:A |] ==> cons(<c,b>,f)`a = f`a";
+by (rtac (apply_Pair RS consI2 RS apply_equality) 1);
+by (rtac fun_extend 3);
+by (REPEAT (assume_tac 1));
+val fun_extend_apply1 = result();
+
+goal ZF.thy "!!f A B. [| f: A->B; ~ c:A |] ==> cons(<c,b>,f)`c = b";
+by (rtac (consI1 RS apply_equality) 1);
+by (rtac fun_extend 1);
+by (REPEAT (assume_tac 1));
+val fun_extend_apply2 = result();
+
+(*The empty function*)
+goal ZF.thy "0: 0->A";
+by (fast_tac (ZF_cs addIs [PiI]) 1);
+val fun_empty = result();
+
+(*The singleton function*)
+goal ZF.thy "{<a,b>} : {a} -> cons(b,C)";
+by (REPEAT (ares_tac [fun_extend,fun_empty,notI] 1 ORELSE etac emptyE 1));
+val fun_single = result();
+