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
--- a/src/ZF/ex/LList.ML Tue Nov 30 11:07:57 1993 +0100
+++ b/src/ZF/ex/LList.ML Tue Nov 30 11:08:18 1993 +0100
@@ -3,7 +3,7 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
-CoDatatype definition of Lazy Lists
+Codatatype definition of Lazy Lists
*)
structure LList = CoDatatype_Fun
@@ -40,32 +40,29 @@
(** Closure of quniv(A) under llist -- why so complex? Its a gfp... **)
-val in_quniv_rls =
- [Transset_quniv, QPair_Int_quniv_in_quniv, Int_Vfrom_0_in_quniv,
- zero_Int_in_quniv, one_Int_in_quniv,
- QPair_Int_Vfrom_succ_in_quniv, QPair_Int_Vfrom_in_quniv];
+val quniv_cs = subset_cs addSIs [QPair_Int_Vset_subset_UN RS subset_trans,
+ QPair_subset_univ,
+ empty_subsetI, one_in_quniv RS qunivD]
+ addIs [Int_lower1 RS subset_trans]
+ addSDs [qunivD]
+ addSEs [Ord_in_Ord];
-val quniv_cs = ZF_cs addSIs in_quniv_rls
- addIs (Int_quniv_in_quniv::codatatype_intrs);
-
-(*Keep unfolding the lazy list until the induction hypothesis applies*)
goal LList.thy
- "!!i. i : nat ==> \
-\ ALL l: llist(quniv(A)). l Int Vfrom(quniv(A), i) : quniv(A)";
-by (etac complete_induct 1);
+ "!!i. Ord(i) ==> ALL l: llist(quniv(A)). l Int Vset(i) <= univ(eclose(A))";
+by (etac trans_induct 1);
by (rtac ballI 1);
by (etac LList.elim 1);
by (rewrite_goals_tac ([QInl_def,QInr_def]@LList.con_defs));
+(*LNil case*)
by (fast_tac quniv_cs 1);
-by (etac natE 1 THEN REPEAT_FIRST hyp_subst_tac);
-by (fast_tac quniv_cs 1);
-by (fast_tac quniv_cs 1);
+(*LCons case*)
+by (safe_tac quniv_cs);
+by (ALLGOALS (fast_tac (quniv_cs addSEs [Ord_trans, make_elim bspec])));
val llist_quniv_lemma = result();
goal LList.thy "llist(quniv(A)) <= quniv(A)";
-by (rtac subsetI 1);
-by (rtac quniv_Int_Vfrom 1);
-by (etac (LList.dom_subset RS subsetD) 1);
+by (rtac (qunivI RS subsetI) 1);
+by (rtac Int_Vset_subset 1);
by (REPEAT (ares_tac [llist_quniv_lemma RS bspec] 1));
val llist_quniv = result();
--- a/src/ZF/ex/LListFn.ML Tue Nov 30 11:07:57 1993 +0100
+++ b/src/ZF/ex/LListFn.ML Tue Nov 30 11:08:18 1993 +0100
@@ -42,51 +42,33 @@
val flip_ss = ZF_ss addsimps [flip_LNil, flip_LCons, not_type];
-goal QUniv.thy "!!b. b:bool ==> b Int X : quniv(A)";
-by (etac boolE 1);
-by (REPEAT (resolve_tac [one_Int_in_quniv, zero_Int_in_quniv] 1
- ORELSE etac ssubst 1));
-val bool_Int_into_quniv = result();
-
-(* (!!x. x : A ==> B(x) : quniv(C)) ==> (UN x:A. B(x)) : quniv(C) *)
-val UN_in_quniv = standard (qunivD RS UN_least RS qunivI);
+goal QUniv.thy "!!b. b:bool ==> b Int X <= univ(eclose(A))";
+by (fast_tac (quniv_cs addSEs [boolE]) 1);
+val bool_Int_subset_univ = result();
-val Int_Vset_in_quniv = qunivD RS Int_Vset_subset RS qunivI;
-
-val flip_cs =
- ZF_cs addSIs [not_type,
- QPair_in_quniv, QInl_in_quniv, QInr_in_quniv,
- zero_in_quniv, Int_Vset_0_subset RS qunivI,
- Transset_0,
- zero_Int_in_quniv, one_Int_in_quniv,
- QPair_Int_Vfrom_succ_in_quniv, QPair_Int_Vfrom_in_quniv]
- addIs [bool_Int_into_quniv, Int_quniv_in_quniv];
+val flip_cs = quniv_cs addSIs [not_type]
+ addIs [bool_Int_subset_univ];
(*Reasoning borrowed from llist_eq.ML; a similar proof works for all
"productive" functions -- cf Coquand's "Infinite Objects in Type Theory".*)
goal LListFn.thy
- "!!i. Ord(i) ==> ALL l: llist(bool). flip(l) Int Vset(i) : quniv(bool)";
+ "!!i. Ord(i) ==> ALL l: llist(bool). flip(l) Int Vset(i) <= \
+\ univ(eclose(bool))";
by (etac trans_induct 1);
-by (safe_tac ZF_cs);
+by (rtac ballI 1);
by (etac LList.elim 1);
by (asm_simp_tac flip_ss 1);
by (asm_simp_tac flip_ss 2);
by (rewrite_goals_tac ([QInl_def,QInr_def]@LList.con_defs));
-by (fast_tac flip_cs 1);
-by (etac Ord_cases 1 THEN REPEAT_FIRST hyp_subst_tac);
-(*0 case*)
-by (fast_tac flip_cs 1);
-(*succ(j) case*)
+(*LNil case*)
by (fast_tac flip_cs 1);
-(*Limit(i) case*)
-by (etac (Limit_Vfrom_eq RS ssubst) 1);
-by (rtac (Int_UN_distrib RS ssubst) 1);
-by (rtac UN_in_quniv 1);
-by (fast_tac flip_cs 1);
+(*LCons case*)
+by (safe_tac flip_cs);
+by (ALLGOALS (fast_tac (flip_cs addSEs [Ord_trans, make_elim bspec])));
val flip_llist_quniv_lemma = result();
goal LListFn.thy "!!l. l: llist(bool) ==> flip(l) : quniv(bool)";
-by (rtac (flip_llist_quniv_lemma RS bspec RS Int_Vset_in_quniv) 1);
+by (rtac (flip_llist_quniv_lemma RS bspec RS Int_Vset_subset RS qunivI) 1);
by (REPEAT (assume_tac 1));
val flip_in_quniv = result();
--- a/src/ZF/ex/LList_Eq.ML Tue Nov 30 11:07:57 1993 +0100
+++ b/src/ZF/ex/LList_Eq.ML Tue Nov 30 11:08:18 1993 +0100
@@ -28,30 +28,18 @@
**)
val lleq_cs = subset_cs
- addSIs [succI1, Int_Vset_0_subset,
- QPair_Int_Vset_succ_subset_trans,
- QPair_Int_Vset_subset_trans];
+ addSIs [QPair_Int_Vset_subset_UN RS subset_trans, QPair_mono]
+ addSEs [Ord_in_Ord, Pair_inject];
-(** Some key feature of this proof needs to be made a general theorem! **)
-
-(*Keep unfolding the lazy list until the induction hypothesis applies*)
+(*Lemma for proving finality. Unfold the lazy list; use induction hypothesis*)
goal LList_Eq.thy
"!!i. Ord(i) ==> ALL l l'. <l,l'> : lleq(A) --> l Int Vset(i) <= l'";
by (etac trans_induct 1);
-by (safe_tac subset_cs);
+by (REPEAT (resolve_tac [allI, impI] 1));
by (etac LList_Eq.elim 1);
-by (safe_tac (subset_cs addSEs [Pair_inject]));
-by (rewrite_goals_tac LList.con_defs);
-by (etac Ord_cases 1 THEN REPEAT_FIRST hyp_subst_tac);
-(*0 case*)
-by (fast_tac lleq_cs 1);
-(*succ(j) case*)
-by (rewtac QInr_def);
-by (fast_tac lleq_cs 1);
-(*Limit(i) case*)
-by (etac (Limit_Vfrom_eq RS ssubst) 1);
-by (rtac (Int_UN_distrib RS ssubst) 1);
-by (fast_tac lleq_cs 1);
+by (rewrite_goals_tac (QInr_def::LList.con_defs));
+by (safe_tac lleq_cs);
+by (fast_tac (subset_cs addSEs [Ord_trans, make_elim bspec]) 1);
val lleq_Int_Vset_subset_lemma = result();
val lleq_Int_Vset_subset = standard
--- a/src/ZF/ex/counit.ML Tue Nov 30 11:07:57 1993 +0100
+++ b/src/ZF/ex/counit.ML Tue Nov 30 11:08:18 1993 +0100
@@ -9,7 +9,8 @@
*)
(*This degenerate definition does not work well because the one constructor's
- definition is trivial!
+ definition is trivial! The same thing occurs with Aczel's Special Final
+ Coalgebra Theorem
*)
structure CoUnit = CoDatatype_Fun
(val thy = QUniv.thy;
@@ -79,28 +80,14 @@
by (fast_tac (ZF_cs addSIs [Con2_bnd_mono RS lfp_Tarski]) 1);
val lfp_Con2_in_counit2 = result();
-(*borrowed from ex/llist_eq.ML! the proofs are almost identical!*)
-val lleq_cs = subset_cs
- addSIs [succI1, Int_Vset_0_subset,
- QPair_Int_Vset_succ_subset_trans,
- QPair_Int_Vset_subset_trans];
-
+(*Lemma for proving finality. Borrowed from ex/llist_eq.ML!*)
goal CoUnit2.thy
"!!i. Ord(i) ==> ALL x y. x: counit2 & y: counit2 --> x Int Vset(i) <= y";
by (etac trans_induct 1);
by (safe_tac subset_cs);
by (etac CoUnit2.elim 1);
by (etac CoUnit2.elim 1);
-by (safe_tac subset_cs);
by (rewrite_goals_tac CoUnit2.con_defs);
-by (etac Ord_cases 1 THEN REPEAT_FIRST hyp_subst_tac);
-(*0 case*)
-by (fast_tac lleq_cs 1);
-(*succ(j) case*)
-by (fast_tac lleq_cs 1);
-(*Limit(i) case*)
-by (etac (Limit_Vfrom_eq RS ssubst) 1);
-by (rtac (Int_UN_distrib RS ssubst) 1);
by (fast_tac lleq_cs 1);
val counit2_Int_Vset_subset_lemma = result();
--- a/src/ZF/ex/llist.ML Tue Nov 30 11:07:57 1993 +0100
+++ b/src/ZF/ex/llist.ML Tue Nov 30 11:08:18 1993 +0100
@@ -3,7 +3,7 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
-CoDatatype definition of Lazy Lists
+Codatatype definition of Lazy Lists
*)
structure LList = CoDatatype_Fun
@@ -40,32 +40,29 @@
(** Closure of quniv(A) under llist -- why so complex? Its a gfp... **)
-val in_quniv_rls =
- [Transset_quniv, QPair_Int_quniv_in_quniv, Int_Vfrom_0_in_quniv,
- zero_Int_in_quniv, one_Int_in_quniv,
- QPair_Int_Vfrom_succ_in_quniv, QPair_Int_Vfrom_in_quniv];
+val quniv_cs = subset_cs addSIs [QPair_Int_Vset_subset_UN RS subset_trans,
+ QPair_subset_univ,
+ empty_subsetI, one_in_quniv RS qunivD]
+ addIs [Int_lower1 RS subset_trans]
+ addSDs [qunivD]
+ addSEs [Ord_in_Ord];
-val quniv_cs = ZF_cs addSIs in_quniv_rls
- addIs (Int_quniv_in_quniv::codatatype_intrs);
-
-(*Keep unfolding the lazy list until the induction hypothesis applies*)
goal LList.thy
- "!!i. i : nat ==> \
-\ ALL l: llist(quniv(A)). l Int Vfrom(quniv(A), i) : quniv(A)";
-by (etac complete_induct 1);
+ "!!i. Ord(i) ==> ALL l: llist(quniv(A)). l Int Vset(i) <= univ(eclose(A))";
+by (etac trans_induct 1);
by (rtac ballI 1);
by (etac LList.elim 1);
by (rewrite_goals_tac ([QInl_def,QInr_def]@LList.con_defs));
+(*LNil case*)
by (fast_tac quniv_cs 1);
-by (etac natE 1 THEN REPEAT_FIRST hyp_subst_tac);
-by (fast_tac quniv_cs 1);
-by (fast_tac quniv_cs 1);
+(*LCons case*)
+by (safe_tac quniv_cs);
+by (ALLGOALS (fast_tac (quniv_cs addSEs [Ord_trans, make_elim bspec])));
val llist_quniv_lemma = result();
goal LList.thy "llist(quniv(A)) <= quniv(A)";
-by (rtac subsetI 1);
-by (rtac quniv_Int_Vfrom 1);
-by (etac (LList.dom_subset RS subsetD) 1);
+by (rtac (qunivI RS subsetI) 1);
+by (rtac Int_Vset_subset 1);
by (REPEAT (ares_tac [llist_quniv_lemma RS bspec] 1));
val llist_quniv = result();
--- a/src/ZF/ex/llist_eq.ML Tue Nov 30 11:07:57 1993 +0100
+++ b/src/ZF/ex/llist_eq.ML Tue Nov 30 11:08:18 1993 +0100
@@ -28,30 +28,18 @@
**)
val lleq_cs = subset_cs
- addSIs [succI1, Int_Vset_0_subset,
- QPair_Int_Vset_succ_subset_trans,
- QPair_Int_Vset_subset_trans];
+ addSIs [QPair_Int_Vset_subset_UN RS subset_trans, QPair_mono]
+ addSEs [Ord_in_Ord, Pair_inject];
-(** Some key feature of this proof needs to be made a general theorem! **)
-
-(*Keep unfolding the lazy list until the induction hypothesis applies*)
+(*Lemma for proving finality. Unfold the lazy list; use induction hypothesis*)
goal LList_Eq.thy
"!!i. Ord(i) ==> ALL l l'. <l,l'> : lleq(A) --> l Int Vset(i) <= l'";
by (etac trans_induct 1);
-by (safe_tac subset_cs);
+by (REPEAT (resolve_tac [allI, impI] 1));
by (etac LList_Eq.elim 1);
-by (safe_tac (subset_cs addSEs [Pair_inject]));
-by (rewrite_goals_tac LList.con_defs);
-by (etac Ord_cases 1 THEN REPEAT_FIRST hyp_subst_tac);
-(*0 case*)
-by (fast_tac lleq_cs 1);
-(*succ(j) case*)
-by (rewtac QInr_def);
-by (fast_tac lleq_cs 1);
-(*Limit(i) case*)
-by (etac (Limit_Vfrom_eq RS ssubst) 1);
-by (rtac (Int_UN_distrib RS ssubst) 1);
-by (fast_tac lleq_cs 1);
+by (rewrite_goals_tac (QInr_def::LList.con_defs));
+by (safe_tac lleq_cs);
+by (fast_tac (subset_cs addSEs [Ord_trans, make_elim bspec]) 1);
val lleq_Int_Vset_subset_lemma = result();
val lleq_Int_Vset_subset = standard
--- a/src/ZF/ex/llistfn.ML Tue Nov 30 11:07:57 1993 +0100
+++ b/src/ZF/ex/llistfn.ML Tue Nov 30 11:08:18 1993 +0100
@@ -42,51 +42,33 @@
val flip_ss = ZF_ss addsimps [flip_LNil, flip_LCons, not_type];
-goal QUniv.thy "!!b. b:bool ==> b Int X : quniv(A)";
-by (etac boolE 1);
-by (REPEAT (resolve_tac [one_Int_in_quniv, zero_Int_in_quniv] 1
- ORELSE etac ssubst 1));
-val bool_Int_into_quniv = result();
-
-(* (!!x. x : A ==> B(x) : quniv(C)) ==> (UN x:A. B(x)) : quniv(C) *)
-val UN_in_quniv = standard (qunivD RS UN_least RS qunivI);
+goal QUniv.thy "!!b. b:bool ==> b Int X <= univ(eclose(A))";
+by (fast_tac (quniv_cs addSEs [boolE]) 1);
+val bool_Int_subset_univ = result();
-val Int_Vset_in_quniv = qunivD RS Int_Vset_subset RS qunivI;
-
-val flip_cs =
- ZF_cs addSIs [not_type,
- QPair_in_quniv, QInl_in_quniv, QInr_in_quniv,
- zero_in_quniv, Int_Vset_0_subset RS qunivI,
- Transset_0,
- zero_Int_in_quniv, one_Int_in_quniv,
- QPair_Int_Vfrom_succ_in_quniv, QPair_Int_Vfrom_in_quniv]
- addIs [bool_Int_into_quniv, Int_quniv_in_quniv];
+val flip_cs = quniv_cs addSIs [not_type]
+ addIs [bool_Int_subset_univ];
(*Reasoning borrowed from llist_eq.ML; a similar proof works for all
"productive" functions -- cf Coquand's "Infinite Objects in Type Theory".*)
goal LListFn.thy
- "!!i. Ord(i) ==> ALL l: llist(bool). flip(l) Int Vset(i) : quniv(bool)";
+ "!!i. Ord(i) ==> ALL l: llist(bool). flip(l) Int Vset(i) <= \
+\ univ(eclose(bool))";
by (etac trans_induct 1);
-by (safe_tac ZF_cs);
+by (rtac ballI 1);
by (etac LList.elim 1);
by (asm_simp_tac flip_ss 1);
by (asm_simp_tac flip_ss 2);
by (rewrite_goals_tac ([QInl_def,QInr_def]@LList.con_defs));
-by (fast_tac flip_cs 1);
-by (etac Ord_cases 1 THEN REPEAT_FIRST hyp_subst_tac);
-(*0 case*)
-by (fast_tac flip_cs 1);
-(*succ(j) case*)
+(*LNil case*)
by (fast_tac flip_cs 1);
-(*Limit(i) case*)
-by (etac (Limit_Vfrom_eq RS ssubst) 1);
-by (rtac (Int_UN_distrib RS ssubst) 1);
-by (rtac UN_in_quniv 1);
-by (fast_tac flip_cs 1);
+(*LCons case*)
+by (safe_tac flip_cs);
+by (ALLGOALS (fast_tac (flip_cs addSEs [Ord_trans, make_elim bspec])));
val flip_llist_quniv_lemma = result();
goal LListFn.thy "!!l. l: llist(bool) ==> flip(l) : quniv(bool)";
-by (rtac (flip_llist_quniv_lemma RS bspec RS Int_Vset_in_quniv) 1);
+by (rtac (flip_llist_quniv_lemma RS bspec RS Int_Vset_subset RS qunivI) 1);
by (REPEAT (assume_tac 1));
val flip_in_quniv = result();