Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
changed filenames to lower case name of theory the file contains
authorclasohm
Wed, 06 Oct 1993 14:45:04 +0100
changeset 34 747f1aad03cf
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 file | annotate | diff | comparison | revisions
src/ZF/ex/LList_Eq.ML file | annotate | diff | comparison | revisions
src/ZF/ex/ROOT.ML file | annotate | diff | comparison | revisions
src/ZF/ex/llist.ML file | annotate | diff | comparison | revisions
src/ZF/ex/llist_eq.ML file | annotate | diff | comparison | revisions 
--- a/src/ZF/ex/LList.ML	Wed Oct 06 14:21:36 1993 +0100
+++ b/src/ZF/ex/LList.ML	Wed Oct 06 14:45:04 1993 +0100
@@ -75,76 +75,5 @@
 val llist_subset_quniv = standard
     (llist_mono RS (llist_quniv RSN (2,subset_trans)));
 
-(*** Equality for llist(A) as a greatest fixed point ***)
-
-structure LList_Eq = Co_Inductive_Fun
- (val thy = LList.thy addconsts [(["lleq"],"i=>i")];
-  val rec_doms = [("lleq","llist(A) <*> llist(A)")];
-  val sintrs = 
-      ["<LNil; LNil> : lleq(A)",
-       "[| a:A;  <l; l'>: lleq(A) |] ==> <LCons(a,l); LCons(a,l')> : lleq(A)"];
-  val monos = [];
-  val con_defs = [];
-  val type_intrs = LList.intrs@[QSigmaI];
-  val type_elims = [QSigmaE2]);
-
-(** Alternatives for above:
-  val con_defs = LList.con_defs
-  val type_intrs = co_data_typechecks
-  val type_elims = [quniv_QPair_E]
-**)
-
-val lleq_cs = subset_cs
-	addSIs [succI1, Int_Vset_0_subset,
-		QPair_Int_Vset_succ_subset_trans,
-		QPair_Int_Vset_subset_trans];
-
-(*Keep unfolding the lazy list until the induction hypothesis applies*)
-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 (etac LList_Eq.elim 1);
-by (safe_tac (subset_cs addSEs [QPair_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);
-val lleq_Int_Vset_subset_lemma = result();
-
-val lleq_Int_Vset_subset = standard
-	(lleq_Int_Vset_subset_lemma RS spec RS spec RS mp);
-
-
-(*lleq(A) is a symmetric relation because qconverse(lleq(A)) is a fixedpoint*)
-val [prem] = goal LList_Eq.thy "<l;l'> : lleq(A) ==> <l';l> : lleq(A)";
-by (rtac (prem RS qconverseI RS LList_Eq.co_induct) 1);
-by (rtac (LList_Eq.dom_subset RS qconverse_type) 1);
-by (safe_tac qconverse_cs);
-by (etac LList_Eq.elim 1);
-by (ALLGOALS (fast_tac qconverse_cs));
-val lleq_symmetric = result();
-
-goal LList_Eq.thy "!!l l'. <l;l'> : lleq(A) ==> l=l'";
-by (rtac equalityI 1);
-by (REPEAT (ares_tac [lleq_Int_Vset_subset RS Int_Vset_subset] 1
-     ORELSE etac lleq_symmetric 1));
-val lleq_implies_equal = result();
-
-val [eqprem,lprem] = goal LList_Eq.thy
-    "[| l=l';  l: llist(A) |] ==> <l;l'> : lleq(A)";
-by (res_inst_tac [("X", "{<l;l>. l: llist(A)}")] LList_Eq.co_induct 1);
-by (rtac (lprem RS RepFunI RS (eqprem RS subst)) 1);
-by (safe_tac qpair_cs);
-by (etac LList.elim 1);
-by (ALLGOALS (fast_tac qpair_cs));
-val equal_llist_implies_leq = result();
-
-
+(* Definition and use of LList_Eq has been moved to llist_eq.ML to allow
+   automatic association between theory name and filename. *)
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/LList_Eq.ML	Wed Oct 06 14:45:04 1993 +0100
@@ -0,0 +1,81 @@
+(*  Title: 	ZF/ex/llist_eq.ML
+    ID:         $Id$
+    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1993  University of Cambridge
+
+Former part of llist.ML, contains definition and use of LList_Eq
+*)
+
+(*** Equality for llist(A) as a greatest fixed point ***)
+
+structure LList_Eq = Co_Inductive_Fun
+ (val thy = LList.thy addconsts [(["lleq"],"i=>i")];
+  val rec_doms = [("lleq","llist(A) <*> llist(A)")];
+  val sintrs = 
+      ["<LNil; LNil> : lleq(A)",
+       "[| a:A;  <l; l'>: lleq(A) |] ==> <LCons(a,l); LCons(a,l')> : lleq(A)"];
+  val monos = [];
+  val con_defs = [];
+  val type_intrs = LList.intrs@[QSigmaI];
+  val type_elims = [QSigmaE2]);
+
+(** Alternatives for above:
+  val con_defs = LList.con_defs
+  val type_intrs = co_data_typechecks
+  val type_elims = [quniv_QPair_E]
+**)
+
+val lleq_cs = subset_cs
+	addSIs [succI1, Int_Vset_0_subset,
+		QPair_Int_Vset_succ_subset_trans,
+		QPair_Int_Vset_subset_trans];
+
+(*Keep unfolding the lazy list until the induction hypothesis applies*)
+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 (etac LList_Eq.elim 1);
+by (safe_tac (subset_cs addSEs [QPair_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);
+val lleq_Int_Vset_subset_lemma = result();
+
+val lleq_Int_Vset_subset = standard
+	(lleq_Int_Vset_subset_lemma RS spec RS spec RS mp);
+
+
+(*lleq(A) is a symmetric relation because qconverse(lleq(A)) is a fixedpoint*)
+val [prem] = goal LList_Eq.thy "<l;l'> : lleq(A) ==> <l';l> : lleq(A)";
+by (rtac (prem RS qconverseI RS LList_Eq.co_induct) 1);
+by (rtac (LList_Eq.dom_subset RS qconverse_type) 1);
+by (safe_tac qconverse_cs);
+by (etac LList_Eq.elim 1);
+by (ALLGOALS (fast_tac qconverse_cs));
+val lleq_symmetric = result();
+
+goal LList_Eq.thy "!!l l'. <l;l'> : lleq(A) ==> l=l'";
+by (rtac equalityI 1);
+by (REPEAT (ares_tac [lleq_Int_Vset_subset RS Int_Vset_subset] 1
+     ORELSE etac lleq_symmetric 1));
+val lleq_implies_equal = result();
+
+val [eqprem,lprem] = goal LList_Eq.thy
+    "[| l=l';  l: llist(A) |] ==> <l;l'> : lleq(A)";
+by (res_inst_tac [("X", "{<l;l>. l: llist(A)}")] LList_Eq.co_induct 1);
+by (rtac (lprem RS RepFunI RS (eqprem RS subst)) 1);
+by (safe_tac qpair_cs);
+by (etac LList.elim 1);
+by (ALLGOALS (fast_tac qpair_cs));
+val equal_llist_implies_leq = result();
+
+
--- a/src/ZF/ex/ROOT.ML	Wed Oct 06 14:21:36 1993 +0100
+++ b/src/ZF/ex/ROOT.ML	Wed Oct 06 14:45:04 1993 +0100
@@ -20,18 +20,18 @@
 (*Binary integer arithmetic*)
 use          "ex/twos-compl.ML";
 time_use     "ex/bin.ML";
-time_use_thy "ex/bin-fn";
+time_use_thy "ex/binfn";
 
 (** Datatypes **)
 (*binary trees*)
 time_use     "ex/bt.ML";
-time_use_thy "ex/bt-fn";
+time_use_thy "ex/bt_fn";
 (*terms: recursion over the list functor*)
 time_use     "ex/term.ML";
-time_use_thy "ex/term-fn";
+time_use_thy "ex/termfn";
 (*trees/forests: mutual recursion*)
 time_use     "ex/tf.ML";
-time_use_thy "ex/tf-fn";
+time_use_thy "ex/tf_fn";
 (*Enormous enumeration type -- could be even bigger?*)
 time_use     "ex/enum.ML";
 
@@ -40,7 +40,7 @@
 time_use     "ex/rmap.ML";
 (*completeness of propositional logic*)
 time_use     "ex/prop.ML";
-time_use_thy "ex/prop-log";
+time_use_thy "ex/propthms";
 (*two Coq examples by Ch. Paulin-Mohring*)
 time_use     "ex/listn.ML";
 time_use     "ex/acc.ML";
@@ -52,7 +52,8 @@
 
 (** Co-Datatypes **)
 time_use     "ex/llist.ML";
-time_use_thy "ex/llist-fn";
+time_use     "ex/llist_eq.ML";
+time_use_thy "ex/llistfn";
 
 
 maketest"END: Root file for ZF Set Theory examples";
--- a/src/ZF/ex/llist.ML	Wed Oct 06 14:21:36 1993 +0100
+++ b/src/ZF/ex/llist.ML	Wed Oct 06 14:45:04 1993 +0100
@@ -75,76 +75,5 @@
 val llist_subset_quniv = standard
     (llist_mono RS (llist_quniv RSN (2,subset_trans)));
 
-(*** Equality for llist(A) as a greatest fixed point ***)
-
-structure LList_Eq = Co_Inductive_Fun
- (val thy = LList.thy addconsts [(["lleq"],"i=>i")];
-  val rec_doms = [("lleq","llist(A) <*> llist(A)")];
-  val sintrs = 
-      ["<LNil; LNil> : lleq(A)",
-       "[| a:A;  <l; l'>: lleq(A) |] ==> <LCons(a,l); LCons(a,l')> : lleq(A)"];
-  val monos = [];
-  val con_defs = [];
-  val type_intrs = LList.intrs@[QSigmaI];
-  val type_elims = [QSigmaE2]);
-
-(** Alternatives for above:
-  val con_defs = LList.con_defs
-  val type_intrs = co_data_typechecks
-  val type_elims = [quniv_QPair_E]
-**)
-
-val lleq_cs = subset_cs
-	addSIs [succI1, Int_Vset_0_subset,
-		QPair_Int_Vset_succ_subset_trans,
-		QPair_Int_Vset_subset_trans];
-
-(*Keep unfolding the lazy list until the induction hypothesis applies*)
-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 (etac LList_Eq.elim 1);
-by (safe_tac (subset_cs addSEs [QPair_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);
-val lleq_Int_Vset_subset_lemma = result();
-
-val lleq_Int_Vset_subset = standard
-	(lleq_Int_Vset_subset_lemma RS spec RS spec RS mp);
-
-
-(*lleq(A) is a symmetric relation because qconverse(lleq(A)) is a fixedpoint*)
-val [prem] = goal LList_Eq.thy "<l;l'> : lleq(A) ==> <l';l> : lleq(A)";
-by (rtac (prem RS qconverseI RS LList_Eq.co_induct) 1);
-by (rtac (LList_Eq.dom_subset RS qconverse_type) 1);
-by (safe_tac qconverse_cs);
-by (etac LList_Eq.elim 1);
-by (ALLGOALS (fast_tac qconverse_cs));
-val lleq_symmetric = result();
-
-goal LList_Eq.thy "!!l l'. <l;l'> : lleq(A) ==> l=l'";
-by (rtac equalityI 1);
-by (REPEAT (ares_tac [lleq_Int_Vset_subset RS Int_Vset_subset] 1
-     ORELSE etac lleq_symmetric 1));
-val lleq_implies_equal = result();
-
-val [eqprem,lprem] = goal LList_Eq.thy
-    "[| l=l';  l: llist(A) |] ==> <l;l'> : lleq(A)";
-by (res_inst_tac [("X", "{<l;l>. l: llist(A)}")] LList_Eq.co_induct 1);
-by (rtac (lprem RS RepFunI RS (eqprem RS subst)) 1);
-by (safe_tac qpair_cs);
-by (etac LList.elim 1);
-by (ALLGOALS (fast_tac qpair_cs));
-val equal_llist_implies_leq = result();
-
-
+(* Definition and use of LList_Eq has been moved to llist_eq.ML to allow
+   automatic association between theory name and filename. *)
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/llist_eq.ML	Wed Oct 06 14:45:04 1993 +0100
@@ -0,0 +1,81 @@
+(*  Title: 	ZF/ex/llist_eq.ML
+    ID:         $Id$
+    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1993  University of Cambridge
+
+Former part of llist.ML, contains definition and use of LList_Eq
+*)
+
+(*** Equality for llist(A) as a greatest fixed point ***)
+
+structure LList_Eq = Co_Inductive_Fun
+ (val thy = LList.thy addconsts [(["lleq"],"i=>i")];
+  val rec_doms = [("lleq","llist(A) <*> llist(A)")];
+  val sintrs = 
+      ["<LNil; LNil> : lleq(A)",
+       "[| a:A;  <l; l'>: lleq(A) |] ==> <LCons(a,l); LCons(a,l')> : lleq(A)"];
+  val monos = [];
+  val con_defs = [];
+  val type_intrs = LList.intrs@[QSigmaI];
+  val type_elims = [QSigmaE2]);
+
+(** Alternatives for above:
+  val con_defs = LList.con_defs
+  val type_intrs = co_data_typechecks
+  val type_elims = [quniv_QPair_E]
+**)
+
+val lleq_cs = subset_cs
+	addSIs [succI1, Int_Vset_0_subset,
+		QPair_Int_Vset_succ_subset_trans,
+		QPair_Int_Vset_subset_trans];
+
+(*Keep unfolding the lazy list until the induction hypothesis applies*)
+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 (etac LList_Eq.elim 1);
+by (safe_tac (subset_cs addSEs [QPair_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);
+val lleq_Int_Vset_subset_lemma = result();
+
+val lleq_Int_Vset_subset = standard
+	(lleq_Int_Vset_subset_lemma RS spec RS spec RS mp);
+
+
+(*lleq(A) is a symmetric relation because qconverse(lleq(A)) is a fixedpoint*)
+val [prem] = goal LList_Eq.thy "<l;l'> : lleq(A) ==> <l';l> : lleq(A)";
+by (rtac (prem RS qconverseI RS LList_Eq.co_induct) 1);
+by (rtac (LList_Eq.dom_subset RS qconverse_type) 1);
+by (safe_tac qconverse_cs);
+by (etac LList_Eq.elim 1);
+by (ALLGOALS (fast_tac qconverse_cs));
+val lleq_symmetric = result();
+
+goal LList_Eq.thy "!!l l'. <l;l'> : lleq(A) ==> l=l'";
+by (rtac equalityI 1);
+by (REPEAT (ares_tac [lleq_Int_Vset_subset RS Int_Vset_subset] 1
+     ORELSE etac lleq_symmetric 1));
+val lleq_implies_equal = result();
+
+val [eqprem,lprem] = goal LList_Eq.thy
+    "[| l=l';  l: llist(A) |] ==> <l;l'> : lleq(A)";
+by (res_inst_tac [("X", "{<l;l>. l: llist(A)}")] LList_Eq.co_induct 1);
+by (rtac (lprem RS RepFunI RS (eqprem RS subst)) 1);
+by (safe_tac qpair_cs);
+by (etac LList.elim 1);
+by (ALLGOALS (fast_tac qpair_cs));
+val equal_llist_implies_leq = result();
+
+
isabelle