Minor changes; addition of counit.ML
authorlcp
Mon Nov 08 17:52:24 1993 +0100 (1993-11-08)
changeset 952246a80b1cb5
parent 94 40f292719398
child 96 91e8875e9c45
Minor changes; addition of counit.ML
src/ZF/ex/Acc.ML
src/ZF/ex/LList_Eq.ML
src/ZF/ex/ROOT.ML
src/ZF/ex/acc.ML
src/ZF/ex/counit.ML
src/ZF/ex/llist_eq.ML
     1.1 --- a/src/ZF/ex/Acc.ML	Fri Nov 05 18:49:22 1993 +0100
     1.2 +++ b/src/ZF/ex/Acc.ML	Mon Nov 08 17:52:24 1993 +0100
     1.3 @@ -13,7 +13,7 @@
     1.4   (val thy = WF.thy addconsts [(["acc"],"i=>i")];
     1.5    val rec_doms = [("acc", "field(r)")];
     1.6    val sintrs = 
     1.7 -      ["[| r-``{b} : Pow(acc(r));  b : field(r) |] ==> b : acc(r)"];
     1.8 +      ["[| r-``{a} : Pow(acc(r));  a : field(r) |] ==> a : acc(r)"];
     1.9    val monos = [Pow_mono];
    1.10    val con_defs = [];
    1.11    val type_intrs = [];
     2.1 --- a/src/ZF/ex/LList_Eq.ML	Fri Nov 05 18:49:22 1993 +0100
     2.2 +++ b/src/ZF/ex/LList_Eq.ML	Mon Nov 08 17:52:24 1993 +0100
     2.3 @@ -30,6 +30,8 @@
     2.4  		QPair_Int_Vset_succ_subset_trans,
     2.5  		QPair_Int_Vset_subset_trans];
     2.6  
     2.7 +(** Some key feature of this proof needs to be made a general theorem! **)
     2.8 +
     2.9  (*Keep unfolding the lazy list until the induction hypothesis applies*)
    2.10  goal LList_Eq.thy
    2.11     "!!i. Ord(i) ==> ALL l l'. <l;l'> : lleq(A) --> l Int Vset(i) <= l'";
     3.1 --- a/src/ZF/ex/ROOT.ML	Fri Nov 05 18:49:22 1993 +0100
     3.2 +++ b/src/ZF/ex/ROOT.ML	Mon Nov 08 17:52:24 1993 +0100
     3.3 @@ -55,6 +55,6 @@
     3.4  time_use_thy "ex/LList";
     3.5  time_use     "ex/llist_eq.ML";
     3.6  time_use_thy "ex/llistfn";
     3.7 -
     3.8 +time_use     "ex/counit.ML";
     3.9  
    3.10  maketest"END: Root file for ZF Set Theory examples";
     4.1 --- a/src/ZF/ex/acc.ML	Fri Nov 05 18:49:22 1993 +0100
     4.2 +++ b/src/ZF/ex/acc.ML	Mon Nov 08 17:52:24 1993 +0100
     4.3 @@ -13,7 +13,7 @@
     4.4   (val thy = WF.thy addconsts [(["acc"],"i=>i")];
     4.5    val rec_doms = [("acc", "field(r)")];
     4.6    val sintrs = 
     4.7 -      ["[| r-``{b} : Pow(acc(r));  b : field(r) |] ==> b : acc(r)"];
     4.8 +      ["[| r-``{a} : Pow(acc(r));  a : field(r) |] ==> a : acc(r)"];
     4.9    val monos = [Pow_mono];
    4.10    val con_defs = [];
    4.11    val type_intrs = [];
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/ZF/ex/counit.ML	Mon Nov 08 17:52:24 1993 +0100
     5.3 @@ -0,0 +1,122 @@
     5.4 +(*  Title: 	ZF/ex/counit.ML
     5.5 +    ID:         $Id$
     5.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     5.7 +    Copyright   1993  University of Cambridge
     5.8 +
     5.9 +Trivial co-datatype definitions, one of which goes wrong!
    5.10 +
    5.11 +Need to find sufficient conditions for co-datatypes to work correctly!
    5.12 +*)
    5.13 +
    5.14 +(*This degenerate definition does not work well because the one constructor's
    5.15 +  definition is trivial!
    5.16 +*)
    5.17 +structure CoUnit = Co_Datatype_Fun
    5.18 + (val thy = QUniv.thy;
    5.19 +  val rec_specs = 
    5.20 +      [("counit", "quniv(0)",
    5.21 +	  [(["Con"],	"i=>i")])];
    5.22 +  val rec_styp = "i";
    5.23 +  val ext = None
    5.24 +  val sintrs = ["x: counit ==> Con(x) : counit"];
    5.25 +  val monos = [];
    5.26 +  val type_intrs = co_datatype_intrs
    5.27 +  val type_elims = co_datatype_elims);
    5.28 +  
    5.29 +val [ConI] = CoUnit.intrs;
    5.30 +
    5.31 +(*USELESS because folding on Con(?xa) == ?xa fails*)
    5.32 +val ConE = CoUnit.mk_cases CoUnit.con_defs "Con(x) : counit";
    5.33 +
    5.34 +(*Proving freeness results*)
    5.35 +val Con_iff = CoUnit.mk_free "Con(x)=Con(y) <-> x=y";
    5.36 +
    5.37 +(*Should be a singleton, not everything!*)
    5.38 +goal CoUnit.thy "counit = quniv(0)";
    5.39 +by (rtac (CoUnit.dom_subset RS equalityI) 1);
    5.40 +by (rtac subsetI 1);
    5.41 +by (etac CoUnit.co_induct 1);
    5.42 +by (rtac subset_refl 1);
    5.43 +by (rewrite_goals_tac CoUnit.con_defs);
    5.44 +by (fast_tac ZF_cs 1);
    5.45 +val counit_eq_univ = result();
    5.46 +
    5.47 +
    5.48 +(*****************************************************************)
    5.49 +
    5.50 +(*A similar example, but the constructor is non-degenerate and it works!
    5.51 +  The resulting set is a singleton.
    5.52 +*)
    5.53 +
    5.54 +structure CoUnit2 = Co_Datatype_Fun
    5.55 + (val thy = QUniv.thy;
    5.56 +  val rec_specs = 
    5.57 +      [("counit2", "quniv(0)",
    5.58 +	  [(["Con2"],	"[i,i]=>i")])];
    5.59 +  val rec_styp = "i";
    5.60 +  val ext = None
    5.61 +  val sintrs = ["[| x: counit2;  y: counit2 |] ==> Con2(x,y) : counit2"];
    5.62 +  val monos = [];
    5.63 +  val type_intrs = co_datatype_intrs
    5.64 +  val type_elims = co_datatype_elims);
    5.65 +
    5.66 +val [Con2I] = CoUnit2.intrs;
    5.67 +
    5.68 +val Con2E = CoUnit2.mk_cases CoUnit2.con_defs "Con2(x,y) : counit2";
    5.69 +
    5.70 +(*Proving freeness results*)
    5.71 +val Con2_iff = CoUnit2.mk_free "Con2(x,y)=Con2(x',y') <-> x=x' & y=y'";
    5.72 +
    5.73 +goalw CoUnit2.thy CoUnit2.con_defs "bnd_mono(univ(0), %x. Con2(x,x))";
    5.74 +by (rtac bnd_monoI 1);
    5.75 +by (REPEAT (ares_tac [subset_refl, QPair_subset_univ, QPair_mono] 1));
    5.76 +val Con2_bnd_mono = result();
    5.77 +
    5.78 +goal CoUnit2.thy "lfp(univ(0), %x. Con2(x,x)) : counit2";
    5.79 +by (rtac (singletonI RS CoUnit2.co_induct) 1);
    5.80 +by (rtac (qunivI RS singleton_subsetI) 1);
    5.81 +by (rtac ([lfp_subset, empty_subsetI RS univ_mono] MRS subset_trans) 1);
    5.82 +by (fast_tac (ZF_cs addSIs [Con2_bnd_mono RS lfp_Tarski]) 1);
    5.83 +val lfp_Con2_in_counit2 = result();
    5.84 +
    5.85 +(*borrowed from ex/llist_eq.ML! the proofs are almost identical!*)
    5.86 +val lleq_cs = subset_cs
    5.87 +	addSIs [succI1, Int_Vset_0_subset,
    5.88 +		QPair_Int_Vset_succ_subset_trans,
    5.89 +		QPair_Int_Vset_subset_trans];
    5.90 +
    5.91 +goal CoUnit2.thy
    5.92 +    "!!i. Ord(i) ==> ALL x y. x: counit2 & y: counit2 --> x Int Vset(i) <= y";
    5.93 +by (etac trans_induct 1);
    5.94 +by (safe_tac subset_cs);
    5.95 +by (etac CoUnit2.elim 1);
    5.96 +by (etac CoUnit2.elim 1);
    5.97 +by (safe_tac subset_cs);
    5.98 +by (rewrite_goals_tac CoUnit2.con_defs);
    5.99 +by (etac Ord_cases 1 THEN REPEAT_FIRST hyp_subst_tac);
   5.100 +(*0 case*)
   5.101 +by (fast_tac lleq_cs 1);
   5.102 +(*succ(j) case*)
   5.103 +by (fast_tac lleq_cs 1);
   5.104 +(*Limit(i) case*)
   5.105 +by (etac (Limit_Vfrom_eq RS ssubst) 1);
   5.106 +by (rtac (Int_UN_distrib RS ssubst) 1);
   5.107 +by (fast_tac lleq_cs 1);
   5.108 +val counit2_Int_Vset_subset_lemma = result();
   5.109 +
   5.110 +val counit2_Int_Vset_subset = standard
   5.111 +	(counit2_Int_Vset_subset_lemma RS spec RS spec RS mp);
   5.112 +
   5.113 +goal CoUnit2.thy "!!x y. [| x: counit2;  y: counit2 |] ==> x=y";
   5.114 +by (rtac equalityI 1);
   5.115 +by (REPEAT (ares_tac [conjI, counit2_Int_Vset_subset RS Int_Vset_subset] 1));
   5.116 +val counit2_implies_equal = result();
   5.117 +
   5.118 +goal CoUnit2.thy "counit2 = {lfp(univ(0), %x. Con2(x,x))}";
   5.119 +by (rtac equalityI 1);
   5.120 +by (rtac (lfp_Con2_in_counit2 RS singleton_subsetI) 2);
   5.121 +by (rtac subsetI 1);
   5.122 +by (dtac (lfp_Con2_in_counit2 RS counit2_implies_equal) 1);
   5.123 +by (etac subst 1);
   5.124 +by (rtac singletonI 1);
   5.125 +val counit2_eq_univ = result();
     6.1 --- a/src/ZF/ex/llist_eq.ML	Fri Nov 05 18:49:22 1993 +0100
     6.2 +++ b/src/ZF/ex/llist_eq.ML	Mon Nov 08 17:52:24 1993 +0100
     6.3 @@ -30,6 +30,8 @@
     6.4  		QPair_Int_Vset_succ_subset_trans,
     6.5  		QPair_Int_Vset_subset_trans];
     6.6  
     6.7 +(** Some key feature of this proof needs to be made a general theorem! **)
     6.8 +
     6.9  (*Keep unfolding the lazy list until the induction hypothesis applies*)
    6.10  goal LList_Eq.thy
    6.11     "!!i. Ord(i) ==> ALL l l'. <l;l'> : lleq(A) --> l Int Vset(i) <= l'";