clasohm@0: (*  Title: 	ZF/univ
clasohm@0:     ID:         $Id$
clasohm@0:     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0:     Copyright   1992  University of Cambridge
clasohm@0: 
clasohm@0: The cumulative hierarchy and a small universe for recursive types
clasohm@0: *)
clasohm@0: 
clasohm@0: open Univ;
clasohm@0: 
clasohm@0: (*NOT SUITABLE FOR REWRITING -- RECURSIVE!*)
clasohm@0: goal Univ.thy "Vfrom(A,i) = A Un (UN j:i. Pow(Vfrom(A,j)))";
clasohm@0: by (rtac (Vfrom_def RS def_transrec RS ssubst) 1);
clasohm@0: by (SIMP_TAC ZF_ss 1);
clasohm@0: val Vfrom = result();
clasohm@0: 
clasohm@0: (** Monotonicity **)
clasohm@0: 
clasohm@0: goal Univ.thy "!!A B. A<=B ==> ALL j. i<=j --> Vfrom(A,i) <= Vfrom(B,j)";
clasohm@0: by (eps_ind_tac "i" 1);
clasohm@0: by (rtac (impI RS allI) 1);
clasohm@0: by (rtac (Vfrom RS ssubst) 1);
clasohm@0: by (rtac (Vfrom RS ssubst) 1);
clasohm@0: by (etac Un_mono 1);
clasohm@0: by (rtac UN_mono 1);
clasohm@0: by (assume_tac 1);
clasohm@0: by (rtac Pow_mono 1);
clasohm@0: by (etac (bspec RS spec RS mp) 1);
clasohm@0: by (assume_tac 1);
clasohm@0: by (rtac subset_refl 1);
clasohm@0: val Vfrom_mono_lemma = result();
clasohm@0: 
clasohm@0: (*  [| A<=B; i<=x |] ==> Vfrom(A,i) <= Vfrom(B,x)  *)
clasohm@0: val Vfrom_mono = standard (Vfrom_mono_lemma RS spec RS mp);
clasohm@0: 
clasohm@0: 
clasohm@0: (** A fundamental equality: Vfrom does not require ordinals! **)
clasohm@0: 
clasohm@0: goal Univ.thy "Vfrom(A,x) <= Vfrom(A,rank(x))";
clasohm@0: by (eps_ind_tac "x" 1);
clasohm@0: by (rtac (Vfrom RS ssubst) 1);
clasohm@0: by (rtac (Vfrom RS ssubst) 1);
clasohm@0: by (fast_tac (ZF_cs addSIs [rank_lt]) 1);
clasohm@0: val Vfrom_rank_subset1 = result();
clasohm@0: 
clasohm@0: goal Univ.thy "Vfrom(A,rank(x)) <= Vfrom(A,x)";
clasohm@0: by (eps_ind_tac "x" 1);
clasohm@0: by (rtac (Vfrom RS ssubst) 1);
clasohm@0: by (rtac (Vfrom RS ssubst) 1);
clasohm@0: br (subset_refl RS Un_mono) 1;
clasohm@0: br UN_least 1;
clasohm@0: by (etac (rank_implies_mem RS bexE) 1);
clasohm@0: br subset_trans 1;
clasohm@0: be UN_upper 2;
clasohm@0: by (etac (subset_refl RS Vfrom_mono RS subset_trans RS Pow_mono) 1);
clasohm@0: by (etac bspec 1);
clasohm@0: by (assume_tac 1);
clasohm@0: val Vfrom_rank_subset2 = result();
clasohm@0: 
clasohm@0: goal Univ.thy "Vfrom(A,rank(x)) = Vfrom(A,x)";
clasohm@0: by (rtac equalityI 1);
clasohm@0: by (rtac Vfrom_rank_subset2 1);
clasohm@0: by (rtac Vfrom_rank_subset1 1);
clasohm@0: val Vfrom_rank_eq = result();
clasohm@0: 
clasohm@0: 
clasohm@0: (*** Basic closure properties ***)
clasohm@0: 
clasohm@0: goal Univ.thy "!!x y. y:x ==> 0 : Vfrom(A,x)";
clasohm@0: by (rtac (Vfrom RS ssubst) 1);
clasohm@0: by (fast_tac ZF_cs 1);
clasohm@0: val zero_in_Vfrom = result();
clasohm@0: 
clasohm@0: goal Univ.thy "i <= Vfrom(A,i)";
clasohm@0: by (eps_ind_tac "i" 1);
clasohm@0: by (rtac (Vfrom RS ssubst) 1);
clasohm@0: by (fast_tac ZF_cs 1);
clasohm@0: val i_subset_Vfrom = result();
clasohm@0: 
clasohm@0: goal Univ.thy "A <= Vfrom(A,i)";
clasohm@0: by (rtac (Vfrom RS ssubst) 1);
clasohm@0: by (rtac Un_upper1 1);
clasohm@0: val A_subset_Vfrom = result();
clasohm@0: 
clasohm@0: goal Univ.thy "!!A a i. a <= Vfrom(A,i) ==> a: Vfrom(A,succ(i))";
clasohm@0: by (rtac (Vfrom RS ssubst) 1);
clasohm@0: by (fast_tac ZF_cs 1);
clasohm@0: val subset_mem_Vfrom = result();
clasohm@0: 
clasohm@0: (** Finite sets and ordered pairs **)
clasohm@0: 
clasohm@0: goal Univ.thy "!!a. a: Vfrom(A,i) ==> {a} : Vfrom(A,succ(i))";
clasohm@0: by (rtac subset_mem_Vfrom 1);
clasohm@0: by (safe_tac ZF_cs);
clasohm@0: val singleton_in_Vfrom = result();
clasohm@0: 
clasohm@0: goal Univ.thy
clasohm@0:     "!!A. [| a: Vfrom(A,i);  b: Vfrom(A,i) |] ==> {a,b} : Vfrom(A,succ(i))";
clasohm@0: by (rtac subset_mem_Vfrom 1);
clasohm@0: by (safe_tac ZF_cs);
clasohm@0: val doubleton_in_Vfrom = result();
clasohm@0: 
clasohm@0: goalw Univ.thy [Pair_def]
clasohm@0:     "!!A. [| a: Vfrom(A,i);  b: Vfrom(A,i) |] ==> \
clasohm@0: \         <a,b> : Vfrom(A,succ(succ(i)))";
clasohm@0: by (REPEAT (ares_tac [doubleton_in_Vfrom] 1));
clasohm@0: val Pair_in_Vfrom = result();
clasohm@0: 
clasohm@0: val [prem] = goal Univ.thy
clasohm@0:     "a<=Vfrom(A,i) ==> succ(a) : Vfrom(A,succ(succ(i)))";
clasohm@0: by (REPEAT (resolve_tac [subset_mem_Vfrom, succ_subsetI] 1));
clasohm@0: by (rtac (Vfrom_mono RSN (2,subset_trans)) 2);
clasohm@0: by (REPEAT (resolve_tac [prem, subset_refl, subset_succI] 1));
clasohm@0: val succ_in_Vfrom = result();
clasohm@0: 
clasohm@0: (*** 0, successor and limit equations fof Vfrom ***)
clasohm@0: 
clasohm@0: goal Univ.thy "Vfrom(A,0) = A";
clasohm@0: by (rtac (Vfrom RS ssubst) 1);
clasohm@0: by (fast_tac eq_cs 1);
clasohm@0: val Vfrom_0 = result();
clasohm@0: 
clasohm@0: goal Univ.thy "!!i. Ord(i) ==> Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))";
clasohm@0: by (rtac (Vfrom RS trans) 1);
clasohm@0: brs ([refl] RL ZF_congs) 1;
clasohm@0: by (rtac equalityI 1);
clasohm@0: by (rtac (succI1 RS RepFunI RS Union_upper) 2);
clasohm@0: by (rtac UN_least 1);
clasohm@0: by (rtac (subset_refl RS Vfrom_mono RS Pow_mono) 1);
clasohm@0: by (etac member_succD 1);
clasohm@0: by (assume_tac 1);
clasohm@0: val Vfrom_succ_lemma = result();
clasohm@0: 
clasohm@0: goal Univ.thy "Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))";
clasohm@0: by (res_inst_tac [("x1", "succ(i)")] (Vfrom_rank_eq RS subst) 1);
clasohm@0: by (res_inst_tac [("x1", "i")] (Vfrom_rank_eq RS subst) 1);
clasohm@0: by (rtac (rank_succ RS ssubst) 1);
clasohm@0: by (rtac (Ord_rank RS Vfrom_succ_lemma) 1);
clasohm@0: val Vfrom_succ = result();
clasohm@0: 
clasohm@0: (*The premise distinguishes this from Vfrom(A,0);  allowing X=0 forces
clasohm@0:   the conclusion to be Vfrom(A,Union(X)) = A Un (UN y:X. Vfrom(A,y)) *)
clasohm@0: val [prem] = goal Univ.thy "y:X ==> Vfrom(A,Union(X)) = (UN y:X. Vfrom(A,y))";
clasohm@0: by (rtac (Vfrom RS ssubst) 1);
clasohm@0: by (rtac equalityI 1);
clasohm@0: (*first inclusion*)
clasohm@0: by (rtac Un_least 1);
clasohm@0: br (A_subset_Vfrom RS subset_trans) 1;
clasohm@0: br (prem RS UN_upper) 1;
clasohm@0: br UN_least 1;
clasohm@0: be UnionE 1;
clasohm@0: br subset_trans 1;
clasohm@0: be UN_upper 2;
clasohm@0: by (rtac (Vfrom RS ssubst) 1);
clasohm@0: be ([UN_upper, Un_upper2] MRS subset_trans) 1;
clasohm@0: (*opposite inclusion*)
clasohm@0: br UN_least 1;
clasohm@0: by (rtac (Vfrom RS ssubst) 1);
clasohm@0: by (fast_tac ZF_cs 1);
clasohm@0: val Vfrom_Union = result();
clasohm@0: 
clasohm@0: (*** Limit ordinals -- general properties ***)
clasohm@0: 
clasohm@0: goalw Univ.thy [Limit_def] "!!i. Limit(i) ==> Union(i) = i";
clasohm@0: by (fast_tac (eq_cs addEs [Ord_trans]) 1);
clasohm@0: val Limit_Union_eq = result();
clasohm@0: 
clasohm@0: goalw Univ.thy [Limit_def] "!!i. Limit(i) ==> Ord(i)";
clasohm@0: by (etac conjunct1 1);
clasohm@0: val Limit_is_Ord = result();
clasohm@0: 
clasohm@0: goalw Univ.thy [Limit_def] "!!i. Limit(i) ==> 0 : i";
clasohm@0: by (fast_tac ZF_cs 1);
clasohm@0: val Limit_has_0 = result();
clasohm@0: 
clasohm@0: goalw Univ.thy [Limit_def] "!!i. [| Limit(i);  j:i |] ==> succ(j) : i";
clasohm@0: by (fast_tac ZF_cs 1);
clasohm@0: val Limit_has_succ = result();
clasohm@0: 
clasohm@0: goalw Univ.thy [Limit_def] "Limit(nat)";
clasohm@0: by (REPEAT (ares_tac [conjI, ballI, nat_0I, nat_succI, Ord_nat] 1));
clasohm@0: val Limit_nat = result();
clasohm@0: 
clasohm@0: goalw Univ.thy [Limit_def]
clasohm@0:     "!!i. [| Ord(i);  0:i;  ALL y. ~ succ(y)=i |] ==> Limit(i)";
clasohm@0: by (safe_tac subset_cs);
clasohm@0: br Ord_member 1;
clasohm@0: by (REPEAT_FIRST (eresolve_tac [asm_rl, Ord_in_Ord RS Ord_succ]
clasohm@0:           ORELSE' dresolve_tac [Ord_succ_subsetI]));
clasohm@0: by (fast_tac (subset_cs addSIs [equalityI]) 1);
clasohm@0: val non_succ_LimitI = result();
clasohm@0: 
clasohm@0: goal Univ.thy "!!i. Ord(i) ==> i=0 | (EX j. i=succ(j)) | Limit(i)";
clasohm@0: by (fast_tac (ZF_cs addSIs [non_succ_LimitI, Ord_0_member_iff RS iffD2]) 1);
clasohm@0: val Ord_cases_lemma = result();
clasohm@0: 
clasohm@0: val major::prems = goal Univ.thy
clasohm@0:     "[| Ord(i);			\
clasohm@0: \       i=0            ==> P;	\
clasohm@0: \       !!j. i=succ(j) ==> P;	\
clasohm@0: \       Limit(i)       ==> P	\
clasohm@0: \    |] ==> P";
clasohm@0: by (cut_facts_tac [major RS Ord_cases_lemma] 1);
clasohm@0: by (REPEAT (eresolve_tac (prems@[disjE, exE]) 1));
clasohm@0: val Ord_cases = result();
clasohm@0: 
clasohm@0: 
clasohm@0: (*** Vfrom applied to Limit ordinals ***)
clasohm@0: 
clasohm@0: (*NB. limit ordinals are non-empty;
clasohm@0:                         Vfrom(A,0) = A = A Un (UN y:0. Vfrom(A,y)) *)
clasohm@0: val [limiti] = goal Univ.thy
clasohm@0:     "Limit(i) ==> Vfrom(A,i) = (UN y:i. Vfrom(A,y))";
clasohm@0: by (rtac (limiti RS Limit_has_0 RS Vfrom_Union RS subst) 1);
clasohm@0: by (rtac (limiti RS Limit_Union_eq RS ssubst) 1);
clasohm@0: by (rtac refl 1);
clasohm@0: val Limit_Vfrom_eq = result();
clasohm@0: 
clasohm@0: val Limit_VfromE = standard (Limit_Vfrom_eq RS equalityD1 RS subsetD RS UN_E);
clasohm@0: 
clasohm@0: val [major,limiti] = goal Univ.thy
clasohm@0:     "[| a: Vfrom(A,i);  Limit(i) |] ==> {a} : Vfrom(A,i)";
clasohm@0: by (rtac (limiti RS Limit_VfromE) 1);
clasohm@0: by (rtac major 1);
clasohm@0: by (rtac (limiti RS Limit_Vfrom_eq RS ssubst) 1);
clasohm@0: by (rtac UN_I 1);
clasohm@0: by (etac singleton_in_Vfrom 2);
clasohm@0: by (etac (limiti RS Limit_has_succ) 1);
clasohm@0: val singleton_in_Vfrom_limit = result();
clasohm@0: 
clasohm@0: val Vfrom_UnI1 = Un_upper1 RS (subset_refl RS Vfrom_mono RS subsetD)
clasohm@0: and Vfrom_UnI2 = Un_upper2 RS (subset_refl RS Vfrom_mono RS subsetD);
clasohm@0: 
clasohm@0: (*Hard work is finding a single j:i such that {a,b}<=Vfrom(A,j)*)
clasohm@0: val [aprem,bprem,limiti] = goal Univ.thy
clasohm@0:     "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i) |] ==> \
clasohm@0: \    {a,b} : Vfrom(A,i)";
clasohm@0: by (rtac (aprem RS (limiti RS Limit_VfromE)) 1);
clasohm@0: by (rtac (bprem RS (limiti RS Limit_VfromE)) 1);
clasohm@0: by (rtac (limiti RS Limit_Vfrom_eq RS ssubst) 1);
clasohm@0: by (rtac UN_I 1);
clasohm@0: by (rtac doubleton_in_Vfrom 2);
clasohm@0: by (etac Vfrom_UnI1 2);
clasohm@0: by (etac Vfrom_UnI2 2);
clasohm@0: by (REPEAT (ares_tac[limiti, Limit_has_succ, Ord_member_UnI, Limit_is_Ord] 1));
clasohm@0: val doubleton_in_Vfrom_limit = result();
clasohm@0: 
clasohm@0: val [aprem,bprem,limiti] = goal Univ.thy
clasohm@0:     "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i) |] ==> \
clasohm@0: \    <a,b> : Vfrom(A,i)";
clasohm@0: (*Infer that a, b occur at ordinals x,xa < i.*)
clasohm@0: by (rtac (aprem RS (limiti RS Limit_VfromE)) 1);
clasohm@0: by (rtac (bprem RS (limiti RS Limit_VfromE)) 1);
clasohm@0: by (rtac (limiti RS Limit_Vfrom_eq RS ssubst) 1);
clasohm@0: by (rtac UN_I 1);
clasohm@0: by (rtac Pair_in_Vfrom 2);
clasohm@0: (*Infer that succ(succ(x Un xa)) < i *)
clasohm@0: by (etac Vfrom_UnI1 2);
clasohm@0: by (etac Vfrom_UnI2 2);
clasohm@0: by (REPEAT (ares_tac[limiti, Limit_has_succ, Ord_member_UnI, Limit_is_Ord] 1));
clasohm@0: val Pair_in_Vfrom_limit = result();
clasohm@0: 
clasohm@0: 
clasohm@0: (*** Properties assuming Transset(A) ***)
clasohm@0: 
clasohm@0: goal Univ.thy "!!i A. Transset(A) ==> Transset(Vfrom(A,i))";
clasohm@0: by (eps_ind_tac "i" 1);
clasohm@0: by (rtac (Vfrom RS ssubst) 1);
clasohm@0: by (fast_tac (ZF_cs addSIs [Transset_Union_family, Transset_Un,
clasohm@0: 			    Transset_Pow]) 1);
clasohm@0: val Transset_Vfrom = result();
clasohm@0: 
clasohm@0: goal Univ.thy "!!A i. Transset(A) ==> Vfrom(A, succ(i)) = Pow(Vfrom(A,i))";
clasohm@0: by (rtac (Vfrom_succ RS trans) 1);
clasohm@0: br (Un_upper2 RSN (2,equalityI)) 1;;
clasohm@0: br (subset_refl RSN (2,Un_least)) 1;;
clasohm@0: br (A_subset_Vfrom RS subset_trans) 1;
clasohm@0: be (Transset_Vfrom RS (Transset_iff_Pow RS iffD1)) 1;
clasohm@0: val Transset_Vfrom_succ = result();
clasohm@0: 
clasohm@0: goalw Ord.thy [Pair_def,Transset_def]
clasohm@0:     "!!C. [| <a,b> <= C; Transset(C) |] ==> a: C & b: C";
clasohm@0: by (fast_tac ZF_cs 1);
clasohm@0: val Transset_Pair_subset = result();
clasohm@0: 
clasohm@0: goal Univ.thy
clasohm@0:     "!!a b.[| <a,b> <= Vfrom(A,i);  Transset(A);  Limit(i) |] ==> \
clasohm@0: \          <a,b> : Vfrom(A,i)";
clasohm@0: be (Transset_Pair_subset RS conjE) 1;
clasohm@0: be Transset_Vfrom 1;
clasohm@0: by (REPEAT (ares_tac [Pair_in_Vfrom_limit] 1));
clasohm@0: val Transset_Pair_subset_Vfrom_limit = result();
clasohm@0: 
clasohm@0: 
clasohm@0: (*** Closure under product/sum applied to elements -- thus Vfrom(A,i) 
clasohm@0:      is a model of simple type theory provided A is a transitive set
clasohm@0:      and i is a limit ordinal
clasohm@0: ***)
clasohm@0: 
clasohm@0: (*There are three nearly identical proofs below -- needs a general theorem
clasohm@0:   for proving  ...a...b : Vfrom(A,i) where i is a limit ordinal*)
clasohm@0: 
clasohm@0: (** products **)
clasohm@0: 
clasohm@0: goal Univ.thy
clasohm@0:     "!!A. [| a: Vfrom(A,i);  b: Vfrom(A,i);  Transset(A) |] ==> \
clasohm@0: \         a*b : Vfrom(A, succ(succ(succ(i))))";
clasohm@0: by (dtac Transset_Vfrom 1);
clasohm@0: by (rtac subset_mem_Vfrom 1);
clasohm@0: by (rewtac Transset_def);
clasohm@0: by (fast_tac (ZF_cs addIs [Pair_in_Vfrom]) 1);
clasohm@0: val prod_in_Vfrom = result();
clasohm@0: 
clasohm@0: val [aprem,bprem,limiti,transset] = goal Univ.thy
clasohm@0:   "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> \
clasohm@0: \  a*b : Vfrom(A,i)";
clasohm@0: (*Infer that a, b occur at ordinals x,xa < i.*)
clasohm@0: by (rtac (aprem RS (limiti RS Limit_VfromE)) 1);
clasohm@0: by (rtac (bprem RS (limiti RS Limit_VfromE)) 1);
clasohm@0: by (rtac (limiti RS Limit_Vfrom_eq RS ssubst) 1);
clasohm@0: by (rtac UN_I 1);
clasohm@0: by (rtac prod_in_Vfrom 2);
clasohm@0: (*Infer that succ(succ(succ(x Un xa))) < i *)
clasohm@0: by (etac (Vfrom_UnI1 RS Vfrom_UnI2) 2);
clasohm@0: by (etac (Vfrom_UnI2 RS Vfrom_UnI2) 2);
clasohm@0: by (REPEAT (ares_tac [limiti RS Limit_has_succ,
clasohm@0: 		      Ord_member_UnI, limiti RS Limit_is_Ord, transset] 1));
clasohm@0: val prod_in_Vfrom_limit = result();
clasohm@0: 
clasohm@0: (** Disjoint sums, aka Quine ordered pairs **)
clasohm@0: 
clasohm@0: goalw Univ.thy [sum_def]
clasohm@0:     "!!A. [| a: Vfrom(A,i);  b: Vfrom(A,i);  Transset(A);  1:i |] ==> \
clasohm@0: \         a+b : Vfrom(A, succ(succ(succ(i))))";
clasohm@0: by (dtac Transset_Vfrom 1);
clasohm@0: by (rtac subset_mem_Vfrom 1);
clasohm@0: by (rewtac Transset_def);
clasohm@0: by (fast_tac (ZF_cs addIs [zero_in_Vfrom, Pair_in_Vfrom, 
clasohm@0: 			   i_subset_Vfrom RS subsetD]) 1);
clasohm@0: val sum_in_Vfrom = result();
clasohm@0: 
clasohm@0: val [aprem,bprem,limiti,transset] = goal Univ.thy
clasohm@0:   "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> \
clasohm@0: \  a+b : Vfrom(A,i)";
clasohm@0: (*Infer that a, b occur at ordinals x,xa < i.*)
clasohm@0: by (rtac (aprem RS (limiti RS Limit_VfromE)) 1);
clasohm@0: by (rtac (bprem RS (limiti RS Limit_VfromE)) 1);
clasohm@0: by (rtac (limiti RS Limit_Vfrom_eq RS ssubst) 1);
clasohm@0: by (rtac UN_I 1);
clasohm@0: by (rtac (rewrite_rule [one_def] sum_in_Vfrom) 2);
clasohm@0: by (rtac (succI1 RS UnI1) 5);
clasohm@0: (*Infer that succ(succ(succ(x Un xa))) < i *)
clasohm@0: by (etac (Vfrom_UnI1 RS Vfrom_UnI2) 2);
clasohm@0: by (etac (Vfrom_UnI2 RS Vfrom_UnI2) 2);
clasohm@0: by (REPEAT (ares_tac [limiti RS Limit_has_0, 
clasohm@0: 		      limiti RS Limit_has_succ,
clasohm@0: 		      Ord_member_UnI, limiti RS Limit_is_Ord, transset] 1));
clasohm@0: val sum_in_Vfrom_limit = result();
clasohm@0: 
clasohm@0: (** function space! **)
clasohm@0: 
clasohm@0: goalw Univ.thy [Pi_def]
clasohm@0:     "!!A. [| a: Vfrom(A,i);  b: Vfrom(A,i);  Transset(A) |] ==> \
clasohm@0: \         a->b : Vfrom(A, succ(succ(succ(succ(i)))))";
clasohm@0: by (dtac Transset_Vfrom 1);
clasohm@0: by (rtac subset_mem_Vfrom 1);
clasohm@0: by (rtac (Collect_subset RS subset_trans) 1);
clasohm@0: by (rtac (Vfrom RS ssubst) 1);
clasohm@0: by (rtac (subset_trans RS subset_trans) 1);
clasohm@0: by (rtac Un_upper2 3);
clasohm@0: by (rtac (succI1 RS UN_upper) 2);
clasohm@0: by (rtac Pow_mono 1);
clasohm@0: by (rewtac Transset_def);
clasohm@0: by (fast_tac (ZF_cs addIs [Pair_in_Vfrom]) 1);
clasohm@0: val fun_in_Vfrom = result();
clasohm@0: 
clasohm@0: val [aprem,bprem,limiti,transset] = goal Univ.thy
clasohm@0:   "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> \
clasohm@0: \  a->b : Vfrom(A,i)";
clasohm@0: (*Infer that a, b occur at ordinals x,xa < i.*)
clasohm@0: by (rtac (aprem RS (limiti RS Limit_VfromE)) 1);
clasohm@0: by (rtac (bprem RS (limiti RS Limit_VfromE)) 1);
clasohm@0: by (rtac (limiti RS Limit_Vfrom_eq RS ssubst) 1);
clasohm@0: by (rtac UN_I 1);
clasohm@0: by (rtac fun_in_Vfrom 2);
clasohm@0: (*Infer that succ(succ(succ(x Un xa))) < i *)
clasohm@0: by (etac (Vfrom_UnI1 RS Vfrom_UnI2) 2);
clasohm@0: by (etac (Vfrom_UnI2 RS Vfrom_UnI2) 2);
clasohm@0: by (REPEAT (ares_tac [limiti RS Limit_has_succ,
clasohm@0: 		      Ord_member_UnI, limiti RS Limit_is_Ord, transset] 1));
clasohm@0: val fun_in_Vfrom_limit = result();
clasohm@0: 
clasohm@0: 
clasohm@0: (*** The set Vset(i) ***)
clasohm@0: 
clasohm@0: goal Univ.thy "Vset(i) = (UN j:i. Pow(Vset(j)))";
clasohm@0: by (rtac (Vfrom RS ssubst) 1);
clasohm@0: by (fast_tac eq_cs 1);
clasohm@0: val Vset = result();
clasohm@0: 
clasohm@0: val Vset_succ = Transset_0 RS Transset_Vfrom_succ;
clasohm@0: 
clasohm@0: val Transset_Vset = Transset_0 RS Transset_Vfrom;
clasohm@0: 
clasohm@0: (** Characterisation of the elements of Vset(i) **)
clasohm@0: 
clasohm@0: val [ordi] = goal Univ.thy "Ord(i) ==> ALL b. b : Vset(i) --> rank(b) : i";
clasohm@0: by (rtac (ordi RS trans_induct) 1);
clasohm@0: by (rtac (Vset RS ssubst) 1);
clasohm@0: by (safe_tac ZF_cs);
clasohm@0: by (rtac (rank RS ssubst) 1);
clasohm@0: by (rtac sup_least2 1);
clasohm@0: by (assume_tac 1);
clasohm@0: by (assume_tac 1);
clasohm@0: by (fast_tac ZF_cs 1);
clasohm@0: val Vset_rank_imp1 = result();
clasohm@0: 
clasohm@0: (*  [| Ord(i); x : Vset(i) |] ==> rank(x) : i  *)
clasohm@0: val Vset_D = standard (Vset_rank_imp1 RS spec RS mp);
clasohm@0: 
clasohm@0: val [ordi] = goal Univ.thy "Ord(i) ==> ALL b. rank(b) : i --> b : Vset(i)";
clasohm@0: by (rtac (ordi RS trans_induct) 1);
clasohm@0: by (rtac allI 1);
clasohm@0: by (rtac (Vset RS ssubst) 1);
clasohm@0: by (fast_tac (ZF_cs addSIs [rank_lt]) 1);
clasohm@0: val Vset_rank_imp2 = result();
clasohm@0: 
clasohm@0: (*  [| Ord(i); rank(x) : i |] ==> x : Vset(i)  *)
clasohm@0: val VsetI = standard (Vset_rank_imp2 RS spec RS mp);
clasohm@0: 
clasohm@0: val [ordi] = goal Univ.thy "Ord(i) ==> b : Vset(i) <-> rank(b) : i";
clasohm@0: by (rtac iffI 1);
clasohm@0: by (etac (ordi RS Vset_D) 1);
clasohm@0: by (etac (ordi RS VsetI) 1);
clasohm@0: val Vset_Ord_rank_iff = result();
clasohm@0: 
clasohm@0: goal Univ.thy "b : Vset(a) <-> rank(b) : rank(a)";
clasohm@0: by (rtac (Vfrom_rank_eq RS subst) 1);
clasohm@0: by (rtac (Ord_rank RS Vset_Ord_rank_iff) 1);
clasohm@0: val Vset_rank_iff = result();
clasohm@0: 
clasohm@0: goal Univ.thy "!!i. Ord(i) ==> rank(Vset(i)) = i";
clasohm@0: by (rtac (rank RS ssubst) 1);
clasohm@0: by (rtac equalityI 1);
clasohm@0: by (safe_tac ZF_cs);
clasohm@0: by (EVERY' [wtac UN_I, 
clasohm@0: 	    etac (i_subset_Vfrom RS subsetD),
clasohm@0: 	    etac (Ord_in_Ord RS rank_of_Ord RS ssubst),
clasohm@0: 	    assume_tac,
clasohm@0: 	    rtac succI1] 3);
clasohm@0: by (REPEAT (eresolve_tac [asm_rl,Vset_D,Ord_trans] 1));
clasohm@0: val rank_Vset = result();
clasohm@0: 
clasohm@0: (** Lemmas for reasoning about sets in terms of their elements' ranks **)
clasohm@0: 
clasohm@0: (*  rank(x) : rank(a) ==> x : Vset(rank(a))  *)
clasohm@0: val Vset_rankI = Ord_rank RS VsetI;
clasohm@0: 
clasohm@0: goal Univ.thy "a <= Vset(rank(a))";
clasohm@0: br subsetI 1;
clasohm@0: be (rank_lt RS Vset_rankI) 1;
clasohm@0: val arg_subset_Vset_rank = result();
clasohm@0: 
clasohm@0: val [iprem] = goal Univ.thy
clasohm@0:     "[| !!i. Ord(i) ==> a Int Vset(i) <= b |] ==> a <= b";
clasohm@0: br ([subset_refl, arg_subset_Vset_rank] MRS Int_greatest RS subset_trans) 1;
clasohm@0: br (Ord_rank RS iprem) 1;
clasohm@0: val Int_Vset_subset = result();
clasohm@0: 
clasohm@0: (** Set up an environment for simplification **)
clasohm@0: 
clasohm@0: val rank_rls = [rank_Inl, rank_Inr, rank_pair1, rank_pair2];
clasohm@0: val rank_trans_rls = rank_rls @ (rank_rls RLN (2, [rank_trans]));
clasohm@0: 
clasohm@0: val rank_ss = ZF_ss 
clasohm@0:     addrews [split, case_Inl, case_Inr, Vset_rankI]
clasohm@0:     addrews rank_trans_rls;
clasohm@0: 
clasohm@0: (** Recursion over Vset levels! **)
clasohm@0: 
clasohm@0: (*NOT SUITABLE FOR REWRITING: recursive!*)
clasohm@0: goalw Univ.thy [Vrec_def] "Vrec(a,H) = H(a, lam x:Vset(rank(a)). Vrec(x,H))";
clasohm@0: by (rtac (transrec RS ssubst) 1);
clasohm@0: by (SIMP_TAC (wf_ss addrews [Ord_rank, Ord_succ, Vset_D RS beta, 
clasohm@0: 			     VsetI RS beta]) 1);
clasohm@0: val Vrec = result();
clasohm@0: 
clasohm@0: (*This form avoids giant explosions in proofs.  NOTE USE OF == *)
clasohm@0: val rew::prems = goal Univ.thy
clasohm@0:     "[| !!x. h(x)==Vrec(x,H) |] ==> \
clasohm@0: \    h(a) = H(a, lam x: Vset(rank(a)). h(x))";
clasohm@0: by (rewtac rew);
clasohm@0: by (rtac Vrec 1);
clasohm@0: val def_Vrec = result();
clasohm@0: 
clasohm@0: val prems = goalw Univ.thy [Vrec_def]
clasohm@0:     "[| a=a';  !!x u. H(x,u)=H'(x,u) |]  ==> Vrec(a,H)=Vrec(a',H')";
clasohm@0: val Vrec_ss = ZF_ss addcongs ([transrec_cong] @ mk_congs Univ.thy ["rank"])
clasohm@0: 		      addrews (prems RL [sym]);
clasohm@0: by (SIMP_TAC Vrec_ss 1);
clasohm@0: val Vrec_cong = result();
clasohm@0: 
clasohm@0: 
clasohm@0: (*** univ(A) ***)
clasohm@0: 
clasohm@0: goalw Univ.thy [univ_def] "!!A B. A<=B ==> univ(A) <= univ(B)";
clasohm@0: by (etac Vfrom_mono 1);
clasohm@0: by (rtac subset_refl 1);
clasohm@0: val univ_mono = result();
clasohm@0: 
clasohm@0: goalw Univ.thy [univ_def] "!!A. Transset(A) ==> Transset(univ(A))";
clasohm@0: by (etac Transset_Vfrom 1);
clasohm@0: val Transset_univ = result();
clasohm@0: 
clasohm@0: (** univ(A) as a limit **)
clasohm@0: 
clasohm@0: goalw Univ.thy [univ_def] "univ(A) = (UN i:nat. Vfrom(A,i))";
clasohm@0: br (Limit_nat RS Limit_Vfrom_eq) 1;
clasohm@0: val univ_eq_UN = result();
clasohm@0: 
clasohm@0: goal Univ.thy "!!c. c <= univ(A) ==> c = (UN i:nat. c Int Vfrom(A,i))";
clasohm@0: br (subset_UN_iff_eq RS iffD1) 1;
clasohm@0: be (univ_eq_UN RS subst) 1;
clasohm@0: val subset_univ_eq_Int = result();
clasohm@0: 
clasohm@0: val [aprem, iprem] = goal Univ.thy
clasohm@0:     "[| a <= univ(X);			 	\
clasohm@0: \       !!i. i:nat ==> a Int Vfrom(X,i) <= b 	\
clasohm@0: \    |] ==> a <= b";
clasohm@0: br (aprem RS subset_univ_eq_Int RS ssubst) 1;
clasohm@0: br UN_least 1;
clasohm@0: be iprem 1;
clasohm@0: val univ_Int_Vfrom_subset = result();
clasohm@0: 
clasohm@0: val prems = goal Univ.thy
clasohm@0:     "[| a <= univ(X);   b <= univ(X);   \
clasohm@0: \       !!i. i:nat ==> a Int Vfrom(X,i) = b Int Vfrom(X,i) \
clasohm@0: \    |] ==> a = b";
clasohm@0: br equalityI 1;
clasohm@0: by (ALLGOALS
clasohm@0:     (resolve_tac (prems RL [univ_Int_Vfrom_subset]) THEN'
clasohm@0:      eresolve_tac (prems RL [equalityD1,equalityD2] RL [subset_trans]) THEN'
clasohm@0:      rtac Int_lower1));
clasohm@0: val univ_Int_Vfrom_eq = result();
clasohm@0: 
clasohm@0: (** Closure properties **)
clasohm@0: 
clasohm@0: goalw Univ.thy [univ_def] "0 : univ(A)";
clasohm@0: by (rtac (nat_0I RS zero_in_Vfrom) 1);
clasohm@0: val zero_in_univ = result();
clasohm@0: 
clasohm@0: goalw Univ.thy [univ_def] "A <= univ(A)";
clasohm@0: by (rtac A_subset_Vfrom 1);
clasohm@0: val A_subset_univ = result();
clasohm@0: 
clasohm@0: val A_into_univ = A_subset_univ RS subsetD;
clasohm@0: 
clasohm@0: (** Closure under unordered and ordered pairs **)
clasohm@0: 
clasohm@0: goalw Univ.thy [univ_def] "!!A a. a: univ(A) ==> {a} : univ(A)";
clasohm@0: by (rtac singleton_in_Vfrom_limit 1);
clasohm@0: by (REPEAT (ares_tac [Ord_nat,Limit_nat] 1));
clasohm@0: val singleton_in_univ = result();
clasohm@0: 
clasohm@0: goalw Univ.thy [univ_def] 
clasohm@0:     "!!A a. [| a: univ(A);  b: univ(A) |] ==> {a,b} : univ(A)";
clasohm@0: by (rtac doubleton_in_Vfrom_limit 1);
clasohm@0: by (REPEAT (ares_tac [Ord_nat,Limit_nat] 1));
clasohm@0: val doubleton_in_univ = result();
clasohm@0: 
clasohm@0: goalw Univ.thy [univ_def]
clasohm@0:     "!!A a. [| a: univ(A);  b: univ(A) |] ==> <a,b> : univ(A)";
clasohm@0: by (rtac Pair_in_Vfrom_limit 1);
clasohm@0: by (REPEAT (ares_tac [Ord_nat,Limit_nat] 1));
clasohm@0: val Pair_in_univ = result();
clasohm@0: 
clasohm@0: goal Univ.thy "univ(A)*univ(A) <= univ(A)";
clasohm@0: by (REPEAT (ares_tac [subsetI,Pair_in_univ] 1
clasohm@0:      ORELSE eresolve_tac [SigmaE, ssubst] 1));
clasohm@0: val product_univ = result();
clasohm@0: 
clasohm@0: val Sigma_subset_univ = standard
clasohm@0:     (Sigma_mono RS (product_univ RSN (2,subset_trans)));
clasohm@0: 
clasohm@0: goalw Univ.thy [univ_def]
clasohm@0:     "!!a b.[| <a,b> <= univ(A);  Transset(A) |] ==> <a,b> : univ(A)";
clasohm@0: be Transset_Pair_subset_Vfrom_limit 1;
clasohm@0: by (REPEAT (ares_tac [Ord_nat,Limit_nat] 1));
clasohm@0: val Transset_Pair_subset_univ = result();
clasohm@0: 
clasohm@0: 
clasohm@0: (** The natural numbers **)
clasohm@0: 
clasohm@0: goalw Univ.thy [univ_def] "nat <= univ(A)";
clasohm@0: by (rtac i_subset_Vfrom 1);
clasohm@0: val nat_subset_univ = result();
clasohm@0: 
clasohm@0: (* n:nat ==> n:univ(A) *)
clasohm@0: val nat_into_univ = standard (nat_subset_univ RS subsetD);
clasohm@0: 
clasohm@0: (** instances for 1 and 2 **)
clasohm@0: 
clasohm@0: goalw Univ.thy [one_def] "1 : univ(A)";
clasohm@0: by (REPEAT (ares_tac [nat_into_univ, nat_0I, nat_succI] 1));
clasohm@0: val one_in_univ = result();
clasohm@0: 
clasohm@0: (*unused!*)
clasohm@0: goal Univ.thy "succ(succ(0)) : univ(A)";
clasohm@0: by (REPEAT (ares_tac [nat_into_univ, nat_0I, nat_succI] 1));
clasohm@0: val two_in_univ = result();
clasohm@0: 
clasohm@0: goalw Univ.thy [bool_def] "bool <= univ(A)";
clasohm@0: by (fast_tac (ZF_cs addSIs [zero_in_univ,one_in_univ]) 1);
clasohm@0: val bool_subset_univ = result();
clasohm@0: 
clasohm@0: val bool_into_univ = standard (bool_subset_univ RS subsetD);
clasohm@0: 
clasohm@0: 
clasohm@0: (** Closure under disjoint union **)
clasohm@0: 
clasohm@0: goalw Univ.thy [Inl_def] "!!A a. a: univ(A) ==> Inl(a) : univ(A)";
clasohm@0: by (REPEAT (ares_tac [zero_in_univ,Pair_in_univ] 1));
clasohm@0: val Inl_in_univ = result();
clasohm@0: 
clasohm@0: goalw Univ.thy [Inr_def] "!!A b. b: univ(A) ==> Inr(b) : univ(A)";
clasohm@0: by (REPEAT (ares_tac [one_in_univ, Pair_in_univ] 1));
clasohm@0: val Inr_in_univ = result();
clasohm@0: 
clasohm@0: goal Univ.thy "univ(C)+univ(C) <= univ(C)";
clasohm@0: by (REPEAT (ares_tac [subsetI,Inl_in_univ,Inr_in_univ] 1
clasohm@0:      ORELSE eresolve_tac [sumE, ssubst] 1));
clasohm@0: val sum_univ = result();
clasohm@0: 
clasohm@0: val sum_subset_univ = standard
clasohm@0:     (sum_mono RS (sum_univ RSN (2,subset_trans)));
clasohm@0: 
clasohm@0: 
clasohm@0: (** Closure under binary union -- use Un_least **)
clasohm@0: (** Closure under Collect -- use  (Collect_subset RS subset_trans)  **)
clasohm@0: (** Closure under RepFun -- use   RepFun_subset  **)
clasohm@0: 
clasohm@0: