ZF/ex/llist_eq/lleq_Int_Vset_subset_lemma,
authorlcp
Tue Nov 30 11:08:18 1993 +0100 (1993-11-30)
changeset 17385071e6ad295
parent 172 3224c46737ef
child 174 319ff2d6760b
ZF/ex/llist_eq/lleq_Int_Vset_subset_lemma,
ZF/ex/counit/counit2_Int_Vset_subset_lemma: now uses QPair_Int_Vset_subset_UN

ZF/ex/llistfn/flip_llist_quniv_lemma: now uses transfinite induction and
QPair_Int_Vset_subset_UN

ZF/ex/llist/llist_quniv_lemma: now uses transfinite induction and
QPair_Int_Vset_subset_UN
src/ZF/ex/LList.ML
src/ZF/ex/LListFn.ML
src/ZF/ex/LList_Eq.ML
src/ZF/ex/counit.ML
src/ZF/ex/llist.ML
src/ZF/ex/llist_eq.ML
src/ZF/ex/llistfn.ML
     1.1 --- a/src/ZF/ex/LList.ML	Tue Nov 30 11:07:57 1993 +0100
     1.2 +++ b/src/ZF/ex/LList.ML	Tue Nov 30 11:08:18 1993 +0100
     1.3 @@ -3,7 +3,7 @@
     1.4      Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.5      Copyright   1993  University of Cambridge
     1.6  
     1.7 -CoDatatype definition of Lazy Lists
     1.8 +Codatatype definition of Lazy Lists
     1.9  *)
    1.10  
    1.11  structure LList = CoDatatype_Fun
    1.12 @@ -40,32 +40,29 @@
    1.13  
    1.14  (** Closure of quniv(A) under llist -- why so complex?  Its a gfp... **)
    1.15  
    1.16 -val in_quniv_rls =
    1.17 - [Transset_quniv, QPair_Int_quniv_in_quniv, Int_Vfrom_0_in_quniv, 
    1.18 -  zero_Int_in_quniv, one_Int_in_quniv,
    1.19 -  QPair_Int_Vfrom_succ_in_quniv, QPair_Int_Vfrom_in_quniv];
    1.20 +val quniv_cs = subset_cs addSIs [QPair_Int_Vset_subset_UN RS subset_trans, 
    1.21 +				 QPair_subset_univ,
    1.22 +				 empty_subsetI, one_in_quniv RS qunivD]
    1.23 +                 addIs  [Int_lower1 RS subset_trans]
    1.24 +		 addSDs [qunivD]
    1.25 +                 addSEs [Ord_in_Ord];
    1.26  
    1.27 -val quniv_cs = ZF_cs addSIs in_quniv_rls 
    1.28 -                     addIs (Int_quniv_in_quniv::codatatype_intrs);
    1.29 -
    1.30 -(*Keep unfolding the lazy list until the induction hypothesis applies*)
    1.31  goal LList.thy
    1.32 -   "!!i. i : nat ==> 	\
    1.33 -\        ALL l: llist(quniv(A)). l Int Vfrom(quniv(A), i) : quniv(A)";
    1.34 -by (etac complete_induct 1);
    1.35 +   "!!i. Ord(i) ==> ALL l: llist(quniv(A)). l Int Vset(i) <= univ(eclose(A))";
    1.36 +by (etac trans_induct 1);
    1.37  by (rtac ballI 1);
    1.38  by (etac LList.elim 1);
    1.39  by (rewrite_goals_tac ([QInl_def,QInr_def]@LList.con_defs));
    1.40 +(*LNil case*)
    1.41  by (fast_tac quniv_cs 1);
    1.42 -by (etac natE 1 THEN REPEAT_FIRST hyp_subst_tac);
    1.43 -by (fast_tac quniv_cs 1);
    1.44 -by (fast_tac quniv_cs 1);
    1.45 +(*LCons case*)
    1.46 +by (safe_tac quniv_cs);
    1.47 +by (ALLGOALS (fast_tac (quniv_cs addSEs [Ord_trans, make_elim bspec])));
    1.48  val llist_quniv_lemma = result();
    1.49  
    1.50  goal LList.thy "llist(quniv(A)) <= quniv(A)";
    1.51 -by (rtac subsetI 1);
    1.52 -by (rtac quniv_Int_Vfrom 1);
    1.53 -by (etac (LList.dom_subset RS subsetD) 1);
    1.54 +by (rtac (qunivI RS subsetI) 1);
    1.55 +by (rtac Int_Vset_subset 1);
    1.56  by (REPEAT (ares_tac [llist_quniv_lemma RS bspec] 1));
    1.57  val llist_quniv = result();
    1.58  
     2.1 --- a/src/ZF/ex/LListFn.ML	Tue Nov 30 11:07:57 1993 +0100
     2.2 +++ b/src/ZF/ex/LListFn.ML	Tue Nov 30 11:08:18 1993 +0100
     2.3 @@ -42,51 +42,33 @@
     2.4  
     2.5  val flip_ss = ZF_ss addsimps [flip_LNil, flip_LCons, not_type];
     2.6  
     2.7 -goal QUniv.thy "!!b. b:bool ==> b Int X : quniv(A)";
     2.8 -by (etac boolE 1);
     2.9 -by (REPEAT (resolve_tac [one_Int_in_quniv, zero_Int_in_quniv] 1
    2.10 -     ORELSE etac ssubst 1));
    2.11 -val bool_Int_into_quniv = result();
    2.12 -
    2.13 -(* (!!x. x : A ==> B(x) : quniv(C)) ==> (UN x:A. B(x)) : quniv(C) *)
    2.14 -val UN_in_quniv = standard (qunivD RS UN_least RS qunivI);
    2.15 +goal QUniv.thy "!!b. b:bool ==> b Int X <= univ(eclose(A))";
    2.16 +by (fast_tac (quniv_cs addSEs [boolE]) 1);
    2.17 +val bool_Int_subset_univ = result();
    2.18  
    2.19 -val Int_Vset_in_quniv = qunivD RS Int_Vset_subset RS qunivI;
    2.20 -
    2.21 -val flip_cs = 
    2.22 -  ZF_cs addSIs [not_type,
    2.23 -		QPair_in_quniv, QInl_in_quniv, QInr_in_quniv, 
    2.24 -		zero_in_quniv, Int_Vset_0_subset RS qunivI,
    2.25 -		Transset_0,
    2.26 -		zero_Int_in_quniv, one_Int_in_quniv,
    2.27 -		QPair_Int_Vfrom_succ_in_quniv, QPair_Int_Vfrom_in_quniv]
    2.28 -        addIs  [bool_Int_into_quniv, Int_quniv_in_quniv];
    2.29 +val flip_cs = quniv_cs addSIs [not_type]
    2.30 +                       addIs  [bool_Int_subset_univ];
    2.31  
    2.32  (*Reasoning borrowed from llist_eq.ML; a similar proof works for all
    2.33    "productive" functions -- cf Coquand's "Infinite Objects in Type Theory".*)
    2.34  goal LListFn.thy
    2.35 -   "!!i. Ord(i) ==> ALL l: llist(bool). flip(l) Int Vset(i) : quniv(bool)";
    2.36 +   "!!i. Ord(i) ==> ALL l: llist(bool). flip(l) Int Vset(i) <= \
    2.37 +\                   univ(eclose(bool))";
    2.38  by (etac trans_induct 1);
    2.39 -by (safe_tac ZF_cs);
    2.40 +by (rtac ballI 1);
    2.41  by (etac LList.elim 1);
    2.42  by (asm_simp_tac flip_ss 1);
    2.43  by (asm_simp_tac flip_ss 2);
    2.44  by (rewrite_goals_tac ([QInl_def,QInr_def]@LList.con_defs));
    2.45 -by (fast_tac flip_cs 1);
    2.46 -by (etac Ord_cases 1 THEN REPEAT_FIRST hyp_subst_tac);
    2.47 -(*0 case*)
    2.48 -by (fast_tac flip_cs 1);
    2.49 -(*succ(j) case*)
    2.50 +(*LNil case*)
    2.51  by (fast_tac flip_cs 1);
    2.52 -(*Limit(i) case*)
    2.53 -by (etac (Limit_Vfrom_eq RS ssubst) 1);
    2.54 -by (rtac (Int_UN_distrib RS ssubst) 1);
    2.55 -by (rtac UN_in_quniv 1);
    2.56 -by (fast_tac flip_cs 1);
    2.57 +(*LCons case*)
    2.58 +by (safe_tac flip_cs);
    2.59 +by (ALLGOALS (fast_tac (flip_cs addSEs [Ord_trans, make_elim bspec])));
    2.60  val flip_llist_quniv_lemma = result();
    2.61  
    2.62  goal LListFn.thy "!!l. l: llist(bool) ==> flip(l) : quniv(bool)";
    2.63 -by (rtac (flip_llist_quniv_lemma RS bspec RS Int_Vset_in_quniv) 1);
    2.64 +by (rtac (flip_llist_quniv_lemma RS bspec RS Int_Vset_subset RS qunivI) 1);
    2.65  by (REPEAT (assume_tac 1));
    2.66  val flip_in_quniv = result();
    2.67  
     3.1 --- a/src/ZF/ex/LList_Eq.ML	Tue Nov 30 11:07:57 1993 +0100
     3.2 +++ b/src/ZF/ex/LList_Eq.ML	Tue Nov 30 11:08:18 1993 +0100
     3.3 @@ -28,30 +28,18 @@
     3.4  **)
     3.5  
     3.6  val lleq_cs = subset_cs
     3.7 -	addSIs [succI1, Int_Vset_0_subset,
     3.8 -		QPair_Int_Vset_succ_subset_trans,
     3.9 -		QPair_Int_Vset_subset_trans];
    3.10 +	addSIs [QPair_Int_Vset_subset_UN RS subset_trans, QPair_mono]
    3.11 +        addSEs [Ord_in_Ord, Pair_inject];
    3.12  
    3.13 -(** Some key feature of this proof needs to be made a general theorem! **)
    3.14 -
    3.15 -(*Keep unfolding the lazy list until the induction hypothesis applies*)
    3.16 +(*Lemma for proving finality.  Unfold the lazy list; use induction hypothesis*)
    3.17  goal LList_Eq.thy
    3.18     "!!i. Ord(i) ==> ALL l l'. <l,l'> : lleq(A) --> l Int Vset(i) <= l'";
    3.19  by (etac trans_induct 1);
    3.20 -by (safe_tac subset_cs);
    3.21 +by (REPEAT (resolve_tac [allI, impI] 1));
    3.22  by (etac LList_Eq.elim 1);
    3.23 -by (safe_tac (subset_cs addSEs [Pair_inject]));
    3.24 -by (rewrite_goals_tac LList.con_defs);
    3.25 -by (etac Ord_cases 1 THEN REPEAT_FIRST hyp_subst_tac);
    3.26 -(*0 case*)
    3.27 -by (fast_tac lleq_cs 1);
    3.28 -(*succ(j) case*)
    3.29 -by (rewtac QInr_def);
    3.30 -by (fast_tac lleq_cs 1);
    3.31 -(*Limit(i) case*)
    3.32 -by (etac (Limit_Vfrom_eq RS ssubst) 1);
    3.33 -by (rtac (Int_UN_distrib RS ssubst) 1);
    3.34 -by (fast_tac lleq_cs 1);
    3.35 +by (rewrite_goals_tac (QInr_def::LList.con_defs));
    3.36 +by (safe_tac lleq_cs);
    3.37 +by (fast_tac (subset_cs addSEs [Ord_trans, make_elim bspec]) 1);
    3.38  val lleq_Int_Vset_subset_lemma = result();
    3.39  
    3.40  val lleq_Int_Vset_subset = standard
     4.1 --- a/src/ZF/ex/counit.ML	Tue Nov 30 11:07:57 1993 +0100
     4.2 +++ b/src/ZF/ex/counit.ML	Tue Nov 30 11:08:18 1993 +0100
     4.3 @@ -9,7 +9,8 @@
     4.4  *)
     4.5  
     4.6  (*This degenerate definition does not work well because the one constructor's
     4.7 -  definition is trivial!
     4.8 +  definition is trivial!  The same thing occurs with Aczel's Special Final
     4.9 +  Coalgebra Theorem
    4.10  *)
    4.11  structure CoUnit = CoDatatype_Fun
    4.12   (val thy = QUniv.thy;
    4.13 @@ -79,28 +80,14 @@
    4.14  by (fast_tac (ZF_cs addSIs [Con2_bnd_mono RS lfp_Tarski]) 1);
    4.15  val lfp_Con2_in_counit2 = result();
    4.16  
    4.17 -(*borrowed from ex/llist_eq.ML! the proofs are almost identical!*)
    4.18 -val lleq_cs = subset_cs
    4.19 -	addSIs [succI1, Int_Vset_0_subset,
    4.20 -		QPair_Int_Vset_succ_subset_trans,
    4.21 -		QPair_Int_Vset_subset_trans];
    4.22 -
    4.23 +(*Lemma for proving finality.  Borrowed from ex/llist_eq.ML!*)
    4.24  goal CoUnit2.thy
    4.25      "!!i. Ord(i) ==> ALL x y. x: counit2 & y: counit2 --> x Int Vset(i) <= y";
    4.26  by (etac trans_induct 1);
    4.27  by (safe_tac subset_cs);
    4.28  by (etac CoUnit2.elim 1);
    4.29  by (etac CoUnit2.elim 1);
    4.30 -by (safe_tac subset_cs);
    4.31  by (rewrite_goals_tac CoUnit2.con_defs);
    4.32 -by (etac Ord_cases 1 THEN REPEAT_FIRST hyp_subst_tac);
    4.33 -(*0 case*)
    4.34 -by (fast_tac lleq_cs 1);
    4.35 -(*succ(j) case*)
    4.36 -by (fast_tac lleq_cs 1);
    4.37 -(*Limit(i) case*)
    4.38 -by (etac (Limit_Vfrom_eq RS ssubst) 1);
    4.39 -by (rtac (Int_UN_distrib RS ssubst) 1);
    4.40  by (fast_tac lleq_cs 1);
    4.41  val counit2_Int_Vset_subset_lemma = result();
    4.42  
     5.1 --- a/src/ZF/ex/llist.ML	Tue Nov 30 11:07:57 1993 +0100
     5.2 +++ b/src/ZF/ex/llist.ML	Tue Nov 30 11:08:18 1993 +0100
     5.3 @@ -3,7 +3,7 @@
     5.4      Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     5.5      Copyright   1993  University of Cambridge
     5.6  
     5.7 -CoDatatype definition of Lazy Lists
     5.8 +Codatatype definition of Lazy Lists
     5.9  *)
    5.10  
    5.11  structure LList = CoDatatype_Fun
    5.12 @@ -40,32 +40,29 @@
    5.13  
    5.14  (** Closure of quniv(A) under llist -- why so complex?  Its a gfp... **)
    5.15  
    5.16 -val in_quniv_rls =
    5.17 - [Transset_quniv, QPair_Int_quniv_in_quniv, Int_Vfrom_0_in_quniv, 
    5.18 -  zero_Int_in_quniv, one_Int_in_quniv,
    5.19 -  QPair_Int_Vfrom_succ_in_quniv, QPair_Int_Vfrom_in_quniv];
    5.20 +val quniv_cs = subset_cs addSIs [QPair_Int_Vset_subset_UN RS subset_trans, 
    5.21 +				 QPair_subset_univ,
    5.22 +				 empty_subsetI, one_in_quniv RS qunivD]
    5.23 +                 addIs  [Int_lower1 RS subset_trans]
    5.24 +		 addSDs [qunivD]
    5.25 +                 addSEs [Ord_in_Ord];
    5.26  
    5.27 -val quniv_cs = ZF_cs addSIs in_quniv_rls 
    5.28 -                     addIs (Int_quniv_in_quniv::codatatype_intrs);
    5.29 -
    5.30 -(*Keep unfolding the lazy list until the induction hypothesis applies*)
    5.31  goal LList.thy
    5.32 -   "!!i. i : nat ==> 	\
    5.33 -\        ALL l: llist(quniv(A)). l Int Vfrom(quniv(A), i) : quniv(A)";
    5.34 -by (etac complete_induct 1);
    5.35 +   "!!i. Ord(i) ==> ALL l: llist(quniv(A)). l Int Vset(i) <= univ(eclose(A))";
    5.36 +by (etac trans_induct 1);
    5.37  by (rtac ballI 1);
    5.38  by (etac LList.elim 1);
    5.39  by (rewrite_goals_tac ([QInl_def,QInr_def]@LList.con_defs));
    5.40 +(*LNil case*)
    5.41  by (fast_tac quniv_cs 1);
    5.42 -by (etac natE 1 THEN REPEAT_FIRST hyp_subst_tac);
    5.43 -by (fast_tac quniv_cs 1);
    5.44 -by (fast_tac quniv_cs 1);
    5.45 +(*LCons case*)
    5.46 +by (safe_tac quniv_cs);
    5.47 +by (ALLGOALS (fast_tac (quniv_cs addSEs [Ord_trans, make_elim bspec])));
    5.48  val llist_quniv_lemma = result();
    5.49  
    5.50  goal LList.thy "llist(quniv(A)) <= quniv(A)";
    5.51 -by (rtac subsetI 1);
    5.52 -by (rtac quniv_Int_Vfrom 1);
    5.53 -by (etac (LList.dom_subset RS subsetD) 1);
    5.54 +by (rtac (qunivI RS subsetI) 1);
    5.55 +by (rtac Int_Vset_subset 1);
    5.56  by (REPEAT (ares_tac [llist_quniv_lemma RS bspec] 1));
    5.57  val llist_quniv = result();
    5.58  
     6.1 --- a/src/ZF/ex/llist_eq.ML	Tue Nov 30 11:07:57 1993 +0100
     6.2 +++ b/src/ZF/ex/llist_eq.ML	Tue Nov 30 11:08:18 1993 +0100
     6.3 @@ -28,30 +28,18 @@
     6.4  **)
     6.5  
     6.6  val lleq_cs = subset_cs
     6.7 -	addSIs [succI1, Int_Vset_0_subset,
     6.8 -		QPair_Int_Vset_succ_subset_trans,
     6.9 -		QPair_Int_Vset_subset_trans];
    6.10 +	addSIs [QPair_Int_Vset_subset_UN RS subset_trans, QPair_mono]
    6.11 +        addSEs [Ord_in_Ord, Pair_inject];
    6.12  
    6.13 -(** Some key feature of this proof needs to be made a general theorem! **)
    6.14 -
    6.15 -(*Keep unfolding the lazy list until the induction hypothesis applies*)
    6.16 +(*Lemma for proving finality.  Unfold the lazy list; use induction hypothesis*)
    6.17  goal LList_Eq.thy
    6.18     "!!i. Ord(i) ==> ALL l l'. <l,l'> : lleq(A) --> l Int Vset(i) <= l'";
    6.19  by (etac trans_induct 1);
    6.20 -by (safe_tac subset_cs);
    6.21 +by (REPEAT (resolve_tac [allI, impI] 1));
    6.22  by (etac LList_Eq.elim 1);
    6.23 -by (safe_tac (subset_cs addSEs [Pair_inject]));
    6.24 -by (rewrite_goals_tac LList.con_defs);
    6.25 -by (etac Ord_cases 1 THEN REPEAT_FIRST hyp_subst_tac);
    6.26 -(*0 case*)
    6.27 -by (fast_tac lleq_cs 1);
    6.28 -(*succ(j) case*)
    6.29 -by (rewtac QInr_def);
    6.30 -by (fast_tac lleq_cs 1);
    6.31 -(*Limit(i) case*)
    6.32 -by (etac (Limit_Vfrom_eq RS ssubst) 1);
    6.33 -by (rtac (Int_UN_distrib RS ssubst) 1);
    6.34 -by (fast_tac lleq_cs 1);
    6.35 +by (rewrite_goals_tac (QInr_def::LList.con_defs));
    6.36 +by (safe_tac lleq_cs);
    6.37 +by (fast_tac (subset_cs addSEs [Ord_trans, make_elim bspec]) 1);
    6.38  val lleq_Int_Vset_subset_lemma = result();
    6.39  
    6.40  val lleq_Int_Vset_subset = standard
     7.1 --- a/src/ZF/ex/llistfn.ML	Tue Nov 30 11:07:57 1993 +0100
     7.2 +++ b/src/ZF/ex/llistfn.ML	Tue Nov 30 11:08:18 1993 +0100
     7.3 @@ -42,51 +42,33 @@
     7.4  
     7.5  val flip_ss = ZF_ss addsimps [flip_LNil, flip_LCons, not_type];
     7.6  
     7.7 -goal QUniv.thy "!!b. b:bool ==> b Int X : quniv(A)";
     7.8 -by (etac boolE 1);
     7.9 -by (REPEAT (resolve_tac [one_Int_in_quniv, zero_Int_in_quniv] 1
    7.10 -     ORELSE etac ssubst 1));
    7.11 -val bool_Int_into_quniv = result();
    7.12 -
    7.13 -(* (!!x. x : A ==> B(x) : quniv(C)) ==> (UN x:A. B(x)) : quniv(C) *)
    7.14 -val UN_in_quniv = standard (qunivD RS UN_least RS qunivI);
    7.15 +goal QUniv.thy "!!b. b:bool ==> b Int X <= univ(eclose(A))";
    7.16 +by (fast_tac (quniv_cs addSEs [boolE]) 1);
    7.17 +val bool_Int_subset_univ = result();
    7.18  
    7.19 -val Int_Vset_in_quniv = qunivD RS Int_Vset_subset RS qunivI;
    7.20 -
    7.21 -val flip_cs = 
    7.22 -  ZF_cs addSIs [not_type,
    7.23 -		QPair_in_quniv, QInl_in_quniv, QInr_in_quniv, 
    7.24 -		zero_in_quniv, Int_Vset_0_subset RS qunivI,
    7.25 -		Transset_0,
    7.26 -		zero_Int_in_quniv, one_Int_in_quniv,
    7.27 -		QPair_Int_Vfrom_succ_in_quniv, QPair_Int_Vfrom_in_quniv]
    7.28 -        addIs  [bool_Int_into_quniv, Int_quniv_in_quniv];
    7.29 +val flip_cs = quniv_cs addSIs [not_type]
    7.30 +                       addIs  [bool_Int_subset_univ];
    7.31  
    7.32  (*Reasoning borrowed from llist_eq.ML; a similar proof works for all
    7.33    "productive" functions -- cf Coquand's "Infinite Objects in Type Theory".*)
    7.34  goal LListFn.thy
    7.35 -   "!!i. Ord(i) ==> ALL l: llist(bool). flip(l) Int Vset(i) : quniv(bool)";
    7.36 +   "!!i. Ord(i) ==> ALL l: llist(bool). flip(l) Int Vset(i) <= \
    7.37 +\                   univ(eclose(bool))";
    7.38  by (etac trans_induct 1);
    7.39 -by (safe_tac ZF_cs);
    7.40 +by (rtac ballI 1);
    7.41  by (etac LList.elim 1);
    7.42  by (asm_simp_tac flip_ss 1);
    7.43  by (asm_simp_tac flip_ss 2);
    7.44  by (rewrite_goals_tac ([QInl_def,QInr_def]@LList.con_defs));
    7.45 -by (fast_tac flip_cs 1);
    7.46 -by (etac Ord_cases 1 THEN REPEAT_FIRST hyp_subst_tac);
    7.47 -(*0 case*)
    7.48 -by (fast_tac flip_cs 1);
    7.49 -(*succ(j) case*)
    7.50 +(*LNil case*)
    7.51  by (fast_tac flip_cs 1);
    7.52 -(*Limit(i) case*)
    7.53 -by (etac (Limit_Vfrom_eq RS ssubst) 1);
    7.54 -by (rtac (Int_UN_distrib RS ssubst) 1);
    7.55 -by (rtac UN_in_quniv 1);
    7.56 -by (fast_tac flip_cs 1);
    7.57 +(*LCons case*)
    7.58 +by (safe_tac flip_cs);
    7.59 +by (ALLGOALS (fast_tac (flip_cs addSEs [Ord_trans, make_elim bspec])));
    7.60  val flip_llist_quniv_lemma = result();
    7.61  
    7.62  goal LListFn.thy "!!l. l: llist(bool) ==> flip(l) : quniv(bool)";
    7.63 -by (rtac (flip_llist_quniv_lemma RS bspec RS Int_Vset_in_quniv) 1);
    7.64 +by (rtac (flip_llist_quniv_lemma RS bspec RS Int_Vset_subset RS qunivI) 1);
    7.65  by (REPEAT (assume_tac 1));
    7.66  val flip_in_quniv = result();
    7.67