src/ZF/ex/LList_Eq.ML
changeset 173 85071e6ad295
parent 120 09287f26bfb8
child 279 7738aed3f84d
     1.1 --- a/src/ZF/ex/LList_Eq.ML	Tue Nov 30 11:07:57 1993 +0100
     1.2 +++ b/src/ZF/ex/LList_Eq.ML	Tue Nov 30 11:08:18 1993 +0100
     1.3 @@ -28,30 +28,18 @@
     1.4  **)
     1.5  
     1.6  val lleq_cs = subset_cs
     1.7 -	addSIs [succI1, Int_Vset_0_subset,
     1.8 -		QPair_Int_Vset_succ_subset_trans,
     1.9 -		QPair_Int_Vset_subset_trans];
    1.10 +	addSIs [QPair_Int_Vset_subset_UN RS subset_trans, QPair_mono]
    1.11 +        addSEs [Ord_in_Ord, Pair_inject];
    1.12  
    1.13 -(** Some key feature of this proof needs to be made a general theorem! **)
    1.14 -
    1.15 -(*Keep unfolding the lazy list until the induction hypothesis applies*)
    1.16 +(*Lemma for proving finality.  Unfold the lazy list; use induction hypothesis*)
    1.17  goal LList_Eq.thy
    1.18     "!!i. Ord(i) ==> ALL l l'. <l,l'> : lleq(A) --> l Int Vset(i) <= l'";
    1.19  by (etac trans_induct 1);
    1.20 -by (safe_tac subset_cs);
    1.21 +by (REPEAT (resolve_tac [allI, impI] 1));
    1.22  by (etac LList_Eq.elim 1);
    1.23 -by (safe_tac (subset_cs addSEs [Pair_inject]));
    1.24 -by (rewrite_goals_tac LList.con_defs);
    1.25 -by (etac Ord_cases 1 THEN REPEAT_FIRST hyp_subst_tac);
    1.26 -(*0 case*)
    1.27 -by (fast_tac lleq_cs 1);
    1.28 -(*succ(j) case*)
    1.29 -by (rewtac QInr_def);
    1.30 -by (fast_tac lleq_cs 1);
    1.31 -(*Limit(i) case*)
    1.32 -by (etac (Limit_Vfrom_eq RS ssubst) 1);
    1.33 -by (rtac (Int_UN_distrib RS ssubst) 1);
    1.34 -by (fast_tac lleq_cs 1);
    1.35 +by (rewrite_goals_tac (QInr_def::LList.con_defs));
    1.36 +by (safe_tac lleq_cs);
    1.37 +by (fast_tac (subset_cs addSEs [Ord_trans, make_elim bspec]) 1);
    1.38  val lleq_Int_Vset_subset_lemma = result();
    1.39  
    1.40  val lleq_Int_Vset_subset = standard