src/ZF/ex/llistfn.ML
changeset 173 85071e6ad295
parent 128 b0ec0c1bddb7
     1.1 --- a/src/ZF/ex/llistfn.ML	Tue Nov 30 11:07:57 1993 +0100
     1.2 +++ b/src/ZF/ex/llistfn.ML	Tue Nov 30 11:08:18 1993 +0100
     1.3 @@ -42,51 +42,33 @@
     1.4  
     1.5  val flip_ss = ZF_ss addsimps [flip_LNil, flip_LCons, not_type];
     1.6  
     1.7 -goal QUniv.thy "!!b. b:bool ==> b Int X : quniv(A)";
     1.8 -by (etac boolE 1);
     1.9 -by (REPEAT (resolve_tac [one_Int_in_quniv, zero_Int_in_quniv] 1
    1.10 -     ORELSE etac ssubst 1));
    1.11 -val bool_Int_into_quniv = result();
    1.12 -
    1.13 -(* (!!x. x : A ==> B(x) : quniv(C)) ==> (UN x:A. B(x)) : quniv(C) *)
    1.14 -val UN_in_quniv = standard (qunivD RS UN_least RS qunivI);
    1.15 +goal QUniv.thy "!!b. b:bool ==> b Int X <= univ(eclose(A))";
    1.16 +by (fast_tac (quniv_cs addSEs [boolE]) 1);
    1.17 +val bool_Int_subset_univ = result();
    1.18  
    1.19 -val Int_Vset_in_quniv = qunivD RS Int_Vset_subset RS qunivI;
    1.20 -
    1.21 -val flip_cs = 
    1.22 -  ZF_cs addSIs [not_type,
    1.23 -		QPair_in_quniv, QInl_in_quniv, QInr_in_quniv, 
    1.24 -		zero_in_quniv, Int_Vset_0_subset RS qunivI,
    1.25 -		Transset_0,
    1.26 -		zero_Int_in_quniv, one_Int_in_quniv,
    1.27 -		QPair_Int_Vfrom_succ_in_quniv, QPair_Int_Vfrom_in_quniv]
    1.28 -        addIs  [bool_Int_into_quniv, Int_quniv_in_quniv];
    1.29 +val flip_cs = quniv_cs addSIs [not_type]
    1.30 +                       addIs  [bool_Int_subset_univ];
    1.31  
    1.32  (*Reasoning borrowed from llist_eq.ML; a similar proof works for all
    1.33    "productive" functions -- cf Coquand's "Infinite Objects in Type Theory".*)
    1.34  goal LListFn.thy
    1.35 -   "!!i. Ord(i) ==> ALL l: llist(bool). flip(l) Int Vset(i) : quniv(bool)";
    1.36 +   "!!i. Ord(i) ==> ALL l: llist(bool). flip(l) Int Vset(i) <= \
    1.37 +\                   univ(eclose(bool))";
    1.38  by (etac trans_induct 1);
    1.39 -by (safe_tac ZF_cs);
    1.40 +by (rtac ballI 1);
    1.41  by (etac LList.elim 1);
    1.42  by (asm_simp_tac flip_ss 1);
    1.43  by (asm_simp_tac flip_ss 2);
    1.44  by (rewrite_goals_tac ([QInl_def,QInr_def]@LList.con_defs));
    1.45 -by (fast_tac flip_cs 1);
    1.46 -by (etac Ord_cases 1 THEN REPEAT_FIRST hyp_subst_tac);
    1.47 -(*0 case*)
    1.48 -by (fast_tac flip_cs 1);
    1.49 -(*succ(j) case*)
    1.50 +(*LNil case*)
    1.51  by (fast_tac flip_cs 1);
    1.52 -(*Limit(i) case*)
    1.53 -by (etac (Limit_Vfrom_eq RS ssubst) 1);
    1.54 -by (rtac (Int_UN_distrib RS ssubst) 1);
    1.55 -by (rtac UN_in_quniv 1);
    1.56 -by (fast_tac flip_cs 1);
    1.57 +(*LCons case*)
    1.58 +by (safe_tac flip_cs);
    1.59 +by (ALLGOALS (fast_tac (flip_cs addSEs [Ord_trans, make_elim bspec])));
    1.60  val flip_llist_quniv_lemma = result();
    1.61  
    1.62  goal LListFn.thy "!!l. l: llist(bool) ==> flip(l) : quniv(bool)";
    1.63 -by (rtac (flip_llist_quniv_lemma RS bspec RS Int_Vset_in_quniv) 1);
    1.64 +by (rtac (flip_llist_quniv_lemma RS bspec RS Int_Vset_subset RS qunivI) 1);
    1.65  by (REPEAT (assume_tac 1));
    1.66  val flip_in_quniv = result();
    1.67