changed filenames to lower case name of theory the file contains
authorclasohm
Wed Oct 06 14:45:04 1993 +0100 (1993-10-06)
changeset 34747f1aad03cf
parent 33 ab5ed678130d
child 35 d71f96f1780e
changed filenames to lower case name of theory the file contains
(only one theory per file, therefore llist.ML has been split)
src/ZF/ex/LList.ML
src/ZF/ex/LList_Eq.ML
src/ZF/ex/ROOT.ML
src/ZF/ex/llist.ML
src/ZF/ex/llist_eq.ML
     1.1 --- a/src/ZF/ex/LList.ML	Wed Oct 06 14:21:36 1993 +0100
     1.2 +++ b/src/ZF/ex/LList.ML	Wed Oct 06 14:45:04 1993 +0100
     1.3 @@ -75,76 +75,5 @@
     1.4  val llist_subset_quniv = standard
     1.5      (llist_mono RS (llist_quniv RSN (2,subset_trans)));
     1.6  
     1.7 -(*** Equality for llist(A) as a greatest fixed point ***)
     1.8 -
     1.9 -structure LList_Eq = Co_Inductive_Fun
    1.10 - (val thy = LList.thy addconsts [(["lleq"],"i=>i")];
    1.11 -  val rec_doms = [("lleq","llist(A) <*> llist(A)")];
    1.12 -  val sintrs = 
    1.13 -      ["<LNil; LNil> : lleq(A)",
    1.14 -       "[| a:A;  <l; l'>: lleq(A) |] ==> <LCons(a,l); LCons(a,l')> : lleq(A)"];
    1.15 -  val monos = [];
    1.16 -  val con_defs = [];
    1.17 -  val type_intrs = LList.intrs@[QSigmaI];
    1.18 -  val type_elims = [QSigmaE2]);
    1.19 -
    1.20 -(** Alternatives for above:
    1.21 -  val con_defs = LList.con_defs
    1.22 -  val type_intrs = co_data_typechecks
    1.23 -  val type_elims = [quniv_QPair_E]
    1.24 -**)
    1.25 -
    1.26 -val lleq_cs = subset_cs
    1.27 -	addSIs [succI1, Int_Vset_0_subset,
    1.28 -		QPair_Int_Vset_succ_subset_trans,
    1.29 -		QPair_Int_Vset_subset_trans];
    1.30 -
    1.31 -(*Keep unfolding the lazy list until the induction hypothesis applies*)
    1.32 -goal LList_Eq.thy
    1.33 -   "!!i. Ord(i) ==> ALL l l'. <l;l'> : lleq(A) --> l Int Vset(i) <= l'";
    1.34 -by (etac trans_induct 1);
    1.35 -by (safe_tac subset_cs);
    1.36 -by (etac LList_Eq.elim 1);
    1.37 -by (safe_tac (subset_cs addSEs [QPair_inject]));
    1.38 -by (rewrite_goals_tac LList.con_defs);
    1.39 -by (etac Ord_cases 1 THEN REPEAT_FIRST hyp_subst_tac);
    1.40 -(*0 case*)
    1.41 -by (fast_tac lleq_cs 1);
    1.42 -(*succ(j) case*)
    1.43 -by (rewtac QInr_def);
    1.44 -by (fast_tac lleq_cs 1);
    1.45 -(*Limit(i) case*)
    1.46 -by (etac (Limit_Vfrom_eq RS ssubst) 1);
    1.47 -by (rtac (Int_UN_distrib RS ssubst) 1);
    1.48 -by (fast_tac lleq_cs 1);
    1.49 -val lleq_Int_Vset_subset_lemma = result();
    1.50 -
    1.51 -val lleq_Int_Vset_subset = standard
    1.52 -	(lleq_Int_Vset_subset_lemma RS spec RS spec RS mp);
    1.53 -
    1.54 -
    1.55 -(*lleq(A) is a symmetric relation because qconverse(lleq(A)) is a fixedpoint*)
    1.56 -val [prem] = goal LList_Eq.thy "<l;l'> : lleq(A) ==> <l';l> : lleq(A)";
    1.57 -by (rtac (prem RS qconverseI RS LList_Eq.co_induct) 1);
    1.58 -by (rtac (LList_Eq.dom_subset RS qconverse_type) 1);
    1.59 -by (safe_tac qconverse_cs);
    1.60 -by (etac LList_Eq.elim 1);
    1.61 -by (ALLGOALS (fast_tac qconverse_cs));
    1.62 -val lleq_symmetric = result();
    1.63 -
    1.64 -goal LList_Eq.thy "!!l l'. <l;l'> : lleq(A) ==> l=l'";
    1.65 -by (rtac equalityI 1);
    1.66 -by (REPEAT (ares_tac [lleq_Int_Vset_subset RS Int_Vset_subset] 1
    1.67 -     ORELSE etac lleq_symmetric 1));
    1.68 -val lleq_implies_equal = result();
    1.69 -
    1.70 -val [eqprem,lprem] = goal LList_Eq.thy
    1.71 -    "[| l=l';  l: llist(A) |] ==> <l;l'> : lleq(A)";
    1.72 -by (res_inst_tac [("X", "{<l;l>. l: llist(A)}")] LList_Eq.co_induct 1);
    1.73 -by (rtac (lprem RS RepFunI RS (eqprem RS subst)) 1);
    1.74 -by (safe_tac qpair_cs);
    1.75 -by (etac LList.elim 1);
    1.76 -by (ALLGOALS (fast_tac qpair_cs));
    1.77 -val equal_llist_implies_leq = result();
    1.78 -
    1.79 -
    1.80 +(* Definition and use of LList_Eq has been moved to llist_eq.ML to allow
    1.81 +   automatic association between theory name and filename. *)
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/ZF/ex/LList_Eq.ML	Wed Oct 06 14:45:04 1993 +0100
     2.3 @@ -0,0 +1,81 @@
     2.4 +(*  Title: 	ZF/ex/llist_eq.ML
     2.5 +    ID:         $Id$
     2.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 +    Copyright   1993  University of Cambridge
     2.8 +
     2.9 +Former part of llist.ML, contains definition and use of LList_Eq
    2.10 +*)
    2.11 +
    2.12 +(*** Equality for llist(A) as a greatest fixed point ***)
    2.13 +
    2.14 +structure LList_Eq = Co_Inductive_Fun
    2.15 + (val thy = LList.thy addconsts [(["lleq"],"i=>i")];
    2.16 +  val rec_doms = [("lleq","llist(A) <*> llist(A)")];
    2.17 +  val sintrs = 
    2.18 +      ["<LNil; LNil> : lleq(A)",
    2.19 +       "[| a:A;  <l; l'>: lleq(A) |] ==> <LCons(a,l); LCons(a,l')> : lleq(A)"];
    2.20 +  val monos = [];
    2.21 +  val con_defs = [];
    2.22 +  val type_intrs = LList.intrs@[QSigmaI];
    2.23 +  val type_elims = [QSigmaE2]);
    2.24 +
    2.25 +(** Alternatives for above:
    2.26 +  val con_defs = LList.con_defs
    2.27 +  val type_intrs = co_data_typechecks
    2.28 +  val type_elims = [quniv_QPair_E]
    2.29 +**)
    2.30 +
    2.31 +val lleq_cs = subset_cs
    2.32 +	addSIs [succI1, Int_Vset_0_subset,
    2.33 +		QPair_Int_Vset_succ_subset_trans,
    2.34 +		QPair_Int_Vset_subset_trans];
    2.35 +
    2.36 +(*Keep unfolding the lazy list until the induction hypothesis applies*)
    2.37 +goal LList_Eq.thy
    2.38 +   "!!i. Ord(i) ==> ALL l l'. <l;l'> : lleq(A) --> l Int Vset(i) <= l'";
    2.39 +by (etac trans_induct 1);
    2.40 +by (safe_tac subset_cs);
    2.41 +by (etac LList_Eq.elim 1);
    2.42 +by (safe_tac (subset_cs addSEs [QPair_inject]));
    2.43 +by (rewrite_goals_tac LList.con_defs);
    2.44 +by (etac Ord_cases 1 THEN REPEAT_FIRST hyp_subst_tac);
    2.45 +(*0 case*)
    2.46 +by (fast_tac lleq_cs 1);
    2.47 +(*succ(j) case*)
    2.48 +by (rewtac QInr_def);
    2.49 +by (fast_tac lleq_cs 1);
    2.50 +(*Limit(i) case*)
    2.51 +by (etac (Limit_Vfrom_eq RS ssubst) 1);
    2.52 +by (rtac (Int_UN_distrib RS ssubst) 1);
    2.53 +by (fast_tac lleq_cs 1);
    2.54 +val lleq_Int_Vset_subset_lemma = result();
    2.55 +
    2.56 +val lleq_Int_Vset_subset = standard
    2.57 +	(lleq_Int_Vset_subset_lemma RS spec RS spec RS mp);
    2.58 +
    2.59 +
    2.60 +(*lleq(A) is a symmetric relation because qconverse(lleq(A)) is a fixedpoint*)
    2.61 +val [prem] = goal LList_Eq.thy "<l;l'> : lleq(A) ==> <l';l> : lleq(A)";
    2.62 +by (rtac (prem RS qconverseI RS LList_Eq.co_induct) 1);
    2.63 +by (rtac (LList_Eq.dom_subset RS qconverse_type) 1);
    2.64 +by (safe_tac qconverse_cs);
    2.65 +by (etac LList_Eq.elim 1);
    2.66 +by (ALLGOALS (fast_tac qconverse_cs));
    2.67 +val lleq_symmetric = result();
    2.68 +
    2.69 +goal LList_Eq.thy "!!l l'. <l;l'> : lleq(A) ==> l=l'";
    2.70 +by (rtac equalityI 1);
    2.71 +by (REPEAT (ares_tac [lleq_Int_Vset_subset RS Int_Vset_subset] 1
    2.72 +     ORELSE etac lleq_symmetric 1));
    2.73 +val lleq_implies_equal = result();
    2.74 +
    2.75 +val [eqprem,lprem] = goal LList_Eq.thy
    2.76 +    "[| l=l';  l: llist(A) |] ==> <l;l'> : lleq(A)";
    2.77 +by (res_inst_tac [("X", "{<l;l>. l: llist(A)}")] LList_Eq.co_induct 1);
    2.78 +by (rtac (lprem RS RepFunI RS (eqprem RS subst)) 1);
    2.79 +by (safe_tac qpair_cs);
    2.80 +by (etac LList.elim 1);
    2.81 +by (ALLGOALS (fast_tac qpair_cs));
    2.82 +val equal_llist_implies_leq = result();
    2.83 +
    2.84 +
     3.1 --- a/src/ZF/ex/ROOT.ML	Wed Oct 06 14:21:36 1993 +0100
     3.2 +++ b/src/ZF/ex/ROOT.ML	Wed Oct 06 14:45:04 1993 +0100
     3.3 @@ -20,18 +20,18 @@
     3.4  (*Binary integer arithmetic*)
     3.5  use          "ex/twos-compl.ML";
     3.6  time_use     "ex/bin.ML";
     3.7 -time_use_thy "ex/bin-fn";
     3.8 +time_use_thy "ex/binfn";
     3.9  
    3.10  (** Datatypes **)
    3.11  (*binary trees*)
    3.12  time_use     "ex/bt.ML";
    3.13 -time_use_thy "ex/bt-fn";
    3.14 +time_use_thy "ex/bt_fn";
    3.15  (*terms: recursion over the list functor*)
    3.16  time_use     "ex/term.ML";
    3.17 -time_use_thy "ex/term-fn";
    3.18 +time_use_thy "ex/termfn";
    3.19  (*trees/forests: mutual recursion*)
    3.20  time_use     "ex/tf.ML";
    3.21 -time_use_thy "ex/tf-fn";
    3.22 +time_use_thy "ex/tf_fn";
    3.23  (*Enormous enumeration type -- could be even bigger?*)
    3.24  time_use     "ex/enum.ML";
    3.25  
    3.26 @@ -40,7 +40,7 @@
    3.27  time_use     "ex/rmap.ML";
    3.28  (*completeness of propositional logic*)
    3.29  time_use     "ex/prop.ML";
    3.30 -time_use_thy "ex/prop-log";
    3.31 +time_use_thy "ex/propthms";
    3.32  (*two Coq examples by Ch. Paulin-Mohring*)
    3.33  time_use     "ex/listn.ML";
    3.34  time_use     "ex/acc.ML";
    3.35 @@ -52,7 +52,8 @@
    3.36  
    3.37  (** Co-Datatypes **)
    3.38  time_use     "ex/llist.ML";
    3.39 -time_use_thy "ex/llist-fn";
    3.40 +time_use     "ex/llist_eq.ML";
    3.41 +time_use_thy "ex/llistfn";
    3.42  
    3.43  
    3.44  maketest"END: Root file for ZF Set Theory examples";
     4.1 --- a/src/ZF/ex/llist.ML	Wed Oct 06 14:21:36 1993 +0100
     4.2 +++ b/src/ZF/ex/llist.ML	Wed Oct 06 14:45:04 1993 +0100
     4.3 @@ -75,76 +75,5 @@
     4.4  val llist_subset_quniv = standard
     4.5      (llist_mono RS (llist_quniv RSN (2,subset_trans)));
     4.6  
     4.7 -(*** Equality for llist(A) as a greatest fixed point ***)
     4.8 -
     4.9 -structure LList_Eq = Co_Inductive_Fun
    4.10 - (val thy = LList.thy addconsts [(["lleq"],"i=>i")];
    4.11 -  val rec_doms = [("lleq","llist(A) <*> llist(A)")];
    4.12 -  val sintrs = 
    4.13 -      ["<LNil; LNil> : lleq(A)",
    4.14 -       "[| a:A;  <l; l'>: lleq(A) |] ==> <LCons(a,l); LCons(a,l')> : lleq(A)"];
    4.15 -  val monos = [];
    4.16 -  val con_defs = [];
    4.17 -  val type_intrs = LList.intrs@[QSigmaI];
    4.18 -  val type_elims = [QSigmaE2]);
    4.19 -
    4.20 -(** Alternatives for above:
    4.21 -  val con_defs = LList.con_defs
    4.22 -  val type_intrs = co_data_typechecks
    4.23 -  val type_elims = [quniv_QPair_E]
    4.24 -**)
    4.25 -
    4.26 -val lleq_cs = subset_cs
    4.27 -	addSIs [succI1, Int_Vset_0_subset,
    4.28 -		QPair_Int_Vset_succ_subset_trans,
    4.29 -		QPair_Int_Vset_subset_trans];
    4.30 -
    4.31 -(*Keep unfolding the lazy list until the induction hypothesis applies*)
    4.32 -goal LList_Eq.thy
    4.33 -   "!!i. Ord(i) ==> ALL l l'. <l;l'> : lleq(A) --> l Int Vset(i) <= l'";
    4.34 -by (etac trans_induct 1);
    4.35 -by (safe_tac subset_cs);
    4.36 -by (etac LList_Eq.elim 1);
    4.37 -by (safe_tac (subset_cs addSEs [QPair_inject]));
    4.38 -by (rewrite_goals_tac LList.con_defs);
    4.39 -by (etac Ord_cases 1 THEN REPEAT_FIRST hyp_subst_tac);
    4.40 -(*0 case*)
    4.41 -by (fast_tac lleq_cs 1);
    4.42 -(*succ(j) case*)
    4.43 -by (rewtac QInr_def);
    4.44 -by (fast_tac lleq_cs 1);
    4.45 -(*Limit(i) case*)
    4.46 -by (etac (Limit_Vfrom_eq RS ssubst) 1);
    4.47 -by (rtac (Int_UN_distrib RS ssubst) 1);
    4.48 -by (fast_tac lleq_cs 1);
    4.49 -val lleq_Int_Vset_subset_lemma = result();
    4.50 -
    4.51 -val lleq_Int_Vset_subset = standard
    4.52 -	(lleq_Int_Vset_subset_lemma RS spec RS spec RS mp);
    4.53 -
    4.54 -
    4.55 -(*lleq(A) is a symmetric relation because qconverse(lleq(A)) is a fixedpoint*)
    4.56 -val [prem] = goal LList_Eq.thy "<l;l'> : lleq(A) ==> <l';l> : lleq(A)";
    4.57 -by (rtac (prem RS qconverseI RS LList_Eq.co_induct) 1);
    4.58 -by (rtac (LList_Eq.dom_subset RS qconverse_type) 1);
    4.59 -by (safe_tac qconverse_cs);
    4.60 -by (etac LList_Eq.elim 1);
    4.61 -by (ALLGOALS (fast_tac qconverse_cs));
    4.62 -val lleq_symmetric = result();
    4.63 -
    4.64 -goal LList_Eq.thy "!!l l'. <l;l'> : lleq(A) ==> l=l'";
    4.65 -by (rtac equalityI 1);
    4.66 -by (REPEAT (ares_tac [lleq_Int_Vset_subset RS Int_Vset_subset] 1
    4.67 -     ORELSE etac lleq_symmetric 1));
    4.68 -val lleq_implies_equal = result();
    4.69 -
    4.70 -val [eqprem,lprem] = goal LList_Eq.thy
    4.71 -    "[| l=l';  l: llist(A) |] ==> <l;l'> : lleq(A)";
    4.72 -by (res_inst_tac [("X", "{<l;l>. l: llist(A)}")] LList_Eq.co_induct 1);
    4.73 -by (rtac (lprem RS RepFunI RS (eqprem RS subst)) 1);
    4.74 -by (safe_tac qpair_cs);
    4.75 -by (etac LList.elim 1);
    4.76 -by (ALLGOALS (fast_tac qpair_cs));
    4.77 -val equal_llist_implies_leq = result();
    4.78 -
    4.79 -
    4.80 +(* Definition and use of LList_Eq has been moved to llist_eq.ML to allow
    4.81 +   automatic association between theory name and filename. *)
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/ZF/ex/llist_eq.ML	Wed Oct 06 14:45:04 1993 +0100
     5.3 @@ -0,0 +1,81 @@
     5.4 +(*  Title: 	ZF/ex/llist_eq.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 +Former part of llist.ML, contains definition and use of LList_Eq
    5.10 +*)
    5.11 +
    5.12 +(*** Equality for llist(A) as a greatest fixed point ***)
    5.13 +
    5.14 +structure LList_Eq = Co_Inductive_Fun
    5.15 + (val thy = LList.thy addconsts [(["lleq"],"i=>i")];
    5.16 +  val rec_doms = [("lleq","llist(A) <*> llist(A)")];
    5.17 +  val sintrs = 
    5.18 +      ["<LNil; LNil> : lleq(A)",
    5.19 +       "[| a:A;  <l; l'>: lleq(A) |] ==> <LCons(a,l); LCons(a,l')> : lleq(A)"];
    5.20 +  val monos = [];
    5.21 +  val con_defs = [];
    5.22 +  val type_intrs = LList.intrs@[QSigmaI];
    5.23 +  val type_elims = [QSigmaE2]);
    5.24 +
    5.25 +(** Alternatives for above:
    5.26 +  val con_defs = LList.con_defs
    5.27 +  val type_intrs = co_data_typechecks
    5.28 +  val type_elims = [quniv_QPair_E]
    5.29 +**)
    5.30 +
    5.31 +val lleq_cs = subset_cs
    5.32 +	addSIs [succI1, Int_Vset_0_subset,
    5.33 +		QPair_Int_Vset_succ_subset_trans,
    5.34 +		QPair_Int_Vset_subset_trans];
    5.35 +
    5.36 +(*Keep unfolding the lazy list until the induction hypothesis applies*)
    5.37 +goal LList_Eq.thy
    5.38 +   "!!i. Ord(i) ==> ALL l l'. <l;l'> : lleq(A) --> l Int Vset(i) <= l'";
    5.39 +by (etac trans_induct 1);
    5.40 +by (safe_tac subset_cs);
    5.41 +by (etac LList_Eq.elim 1);
    5.42 +by (safe_tac (subset_cs addSEs [QPair_inject]));
    5.43 +by (rewrite_goals_tac LList.con_defs);
    5.44 +by (etac Ord_cases 1 THEN REPEAT_FIRST hyp_subst_tac);
    5.45 +(*0 case*)
    5.46 +by (fast_tac lleq_cs 1);
    5.47 +(*succ(j) case*)
    5.48 +by (rewtac QInr_def);
    5.49 +by (fast_tac lleq_cs 1);
    5.50 +(*Limit(i) case*)
    5.51 +by (etac (Limit_Vfrom_eq RS ssubst) 1);
    5.52 +by (rtac (Int_UN_distrib RS ssubst) 1);
    5.53 +by (fast_tac lleq_cs 1);
    5.54 +val lleq_Int_Vset_subset_lemma = result();
    5.55 +
    5.56 +val lleq_Int_Vset_subset = standard
    5.57 +	(lleq_Int_Vset_subset_lemma RS spec RS spec RS mp);
    5.58 +
    5.59 +
    5.60 +(*lleq(A) is a symmetric relation because qconverse(lleq(A)) is a fixedpoint*)
    5.61 +val [prem] = goal LList_Eq.thy "<l;l'> : lleq(A) ==> <l';l> : lleq(A)";
    5.62 +by (rtac (prem RS qconverseI RS LList_Eq.co_induct) 1);
    5.63 +by (rtac (LList_Eq.dom_subset RS qconverse_type) 1);
    5.64 +by (safe_tac qconverse_cs);
    5.65 +by (etac LList_Eq.elim 1);
    5.66 +by (ALLGOALS (fast_tac qconverse_cs));
    5.67 +val lleq_symmetric = result();
    5.68 +
    5.69 +goal LList_Eq.thy "!!l l'. <l;l'> : lleq(A) ==> l=l'";
    5.70 +by (rtac equalityI 1);
    5.71 +by (REPEAT (ares_tac [lleq_Int_Vset_subset RS Int_Vset_subset] 1
    5.72 +     ORELSE etac lleq_symmetric 1));
    5.73 +val lleq_implies_equal = result();
    5.74 +
    5.75 +val [eqprem,lprem] = goal LList_Eq.thy
    5.76 +    "[| l=l';  l: llist(A) |] ==> <l;l'> : lleq(A)";
    5.77 +by (res_inst_tac [("X", "{<l;l>. l: llist(A)}")] LList_Eq.co_induct 1);
    5.78 +by (rtac (lprem RS RepFunI RS (eqprem RS subst)) 1);
    5.79 +by (safe_tac qpair_cs);
    5.80 +by (etac LList.elim 1);
    5.81 +by (ALLGOALS (fast_tac qpair_cs));
    5.82 +val equal_llist_implies_leq = result();
    5.83 +
    5.84 +