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.
minor changes e.g. datatype_elims
authorlcp
Thu, 28 Oct 1993 11:32:37 +0100
changeset 85 914270f33f2d
parent 84 01d6c0ddaae3
child 86 3406bd994306
minor changes e.g. datatype_elims
src/ZF/ex/Data.ML file | annotate | diff | comparison | revisions
src/ZF/ex/LList.ML file | annotate | diff | comparison | revisions
src/ZF/ex/ListN.ML file | annotate | diff | comparison | revisions
src/ZF/ex/data.ML file | annotate | diff | comparison | revisions
src/ZF/ex/listn.ML file | annotate | diff | comparison | revisions
src/ZF/ex/llist.ML file | annotate | diff | comparison | revisions 
--- a/src/ZF/ex/Data.ML	Thu Oct 28 11:30:35 1993 +0100
+++ b/src/ZF/ex/Data.ML	Thu Oct 28 11:32:37 1993 +0100
@@ -11,17 +11,17 @@
  (val thy = Univ.thy;
   val rec_specs = 
       [("data", "univ(A Un B)",
-	  [(["Zero"],	"i"),
-	   (["One"],	"i=>i"),
-	   (["Two"],	"[i,i]=>i"),
-	   (["Three"],	"[i,i,i]=>i")])];
+	  [(["Con0"],	"i"),
+	   (["Con1"],	"i=>i"),
+	   (["Con2"],	"[i,i]=>i"),
+	   (["Con3"],	"[i,i,i]=>i")])];
   val rec_styp = "[i,i]=>i";
   val ext = None
   val sintrs = 
-	  ["Zero : data(A,B)",
-	   "[| a: A |] ==> One(a) : data(A,B)",
-	   "[| a: A; b: B |] ==> Two(a,b) : data(A,B)",
-	   "[| a: A; b: B;  d: data(A,B) |] ==> Three(a,b,d) : data(A,B)"];
+	  ["Con0 : data(A,B)",
+	   "[| a: A |] ==> Con1(a) : data(A,B)",
+	   "[| a: A; b: B |] ==> Con2(a,b) : data(A,B)",
+	   "[| a: A; b: B;  d: data(A,B) |] ==> Con3(a,b,d) : data(A,B)"];
   val monos = [];
   val type_intrs = datatype_intrs
   val type_elims = datatype_elims);
--- a/src/ZF/ex/LList.ML	Thu Oct 28 11:30:35 1993 +0100
+++ b/src/ZF/ex/LList.ML	Thu Oct 28 11:32:37 1993 +0100
@@ -4,9 +4,6 @@
     Copyright   1993  University of Cambridge
 
 Co-Datatype definition of Lazy Lists
-
-Needs a "take-lemma" to prove llist_subset_quniv and to justify co-induction
-for proving equality
 *)
 
 structure LList = Co_Datatype_Fun
@@ -22,7 +19,7 @@
        "[| a: A;  l: llist(A) |] ==> LCons(a,l) : llist(A)"];
   val monos = [];
   val type_intrs = co_datatype_intrs
-  val type_elims = []);
+  val type_elims = co_datatype_elims);
   
 val [LNilI, LConsI] = LList.intrs;
 
--- a/src/ZF/ex/ListN.ML	Thu Oct 28 11:30:35 1993 +0100
+++ b/src/ZF/ex/ListN.ML	Thu Oct 28 11:32:37 1993 +0100
@@ -55,4 +55,7 @@
 val listn_append = result();
 
 val Nil_listn_case = ListN.mk_cases List.con_defs "<i,Nil> : listn(A)"
-and Cons_listn_case = ListN.mk_cases List.con_defs "<i,Cons(x,xs)> : listn(A)";
+and Cons_listn_case = ListN.mk_cases List.con_defs "<i,Cons(x,l)> : listn(A)";
+
+val zero_listn_case = ListN.mk_cases List.con_defs "<0,l> : listn(A)"
+and succ_listn_case = ListN.mk_cases List.con_defs "<succ(i),l> : listn(A)";
--- a/src/ZF/ex/data.ML	Thu Oct 28 11:30:35 1993 +0100
+++ b/src/ZF/ex/data.ML	Thu Oct 28 11:32:37 1993 +0100
@@ -11,17 +11,17 @@
  (val thy = Univ.thy;
   val rec_specs = 
       [("data", "univ(A Un B)",
-	  [(["Zero"],	"i"),
-	   (["One"],	"i=>i"),
-	   (["Two"],	"[i,i]=>i"),
-	   (["Three"],	"[i,i,i]=>i")])];
+	  [(["Con0"],	"i"),
+	   (["Con1"],	"i=>i"),
+	   (["Con2"],	"[i,i]=>i"),
+	   (["Con3"],	"[i,i,i]=>i")])];
   val rec_styp = "[i,i]=>i";
   val ext = None
   val sintrs = 
-	  ["Zero : data(A,B)",
-	   "[| a: A |] ==> One(a) : data(A,B)",
-	   "[| a: A; b: B |] ==> Two(a,b) : data(A,B)",
-	   "[| a: A; b: B;  d: data(A,B) |] ==> Three(a,b,d) : data(A,B)"];
+	  ["Con0 : data(A,B)",
+	   "[| a: A |] ==> Con1(a) : data(A,B)",
+	   "[| a: A; b: B |] ==> Con2(a,b) : data(A,B)",
+	   "[| a: A; b: B;  d: data(A,B) |] ==> Con3(a,b,d) : data(A,B)"];
   val monos = [];
   val type_intrs = datatype_intrs
   val type_elims = datatype_elims);
--- a/src/ZF/ex/listn.ML	Thu Oct 28 11:30:35 1993 +0100
+++ b/src/ZF/ex/listn.ML	Thu Oct 28 11:32:37 1993 +0100
@@ -55,4 +55,7 @@
 val listn_append = result();
 
 val Nil_listn_case = ListN.mk_cases List.con_defs "<i,Nil> : listn(A)"
-and Cons_listn_case = ListN.mk_cases List.con_defs "<i,Cons(x,xs)> : listn(A)";
+and Cons_listn_case = ListN.mk_cases List.con_defs "<i,Cons(x,l)> : listn(A)";
+
+val zero_listn_case = ListN.mk_cases List.con_defs "<0,l> : listn(A)"
+and succ_listn_case = ListN.mk_cases List.con_defs "<succ(i),l> : listn(A)";
--- a/src/ZF/ex/llist.ML	Thu Oct 28 11:30:35 1993 +0100
+++ b/src/ZF/ex/llist.ML	Thu Oct 28 11:32:37 1993 +0100
@@ -4,9 +4,6 @@
     Copyright   1993  University of Cambridge
 
 Co-Datatype definition of Lazy Lists
-
-Needs a "take-lemma" to prove llist_subset_quniv and to justify co-induction
-for proving equality
 *)
 
 structure LList = Co_Datatype_Fun
@@ -22,7 +19,7 @@
        "[| a: A;  l: llist(A) |] ==> LCons(a,l) : llist(A)"];
   val monos = [];
   val type_intrs = co_datatype_intrs
-  val type_elims = []);
+  val type_elims = co_datatype_elims);
   
 val [LNilI, LConsI] = LList.intrs;
isabelle