--- a/src/ZF/List.ML Thu Mar 17 11:24:31 1994 +0100
+++ b/src/ZF/List.ML Thu Mar 17 12:36:58 1994 +0100
@@ -7,17 +7,15 @@
*)
structure List = Datatype_Fun
- (val thy = Univ.thy;
- val rec_specs =
- [("list", "univ(A)",
- [(["Nil"], "i"),
- (["Cons"], "[i,i]=>i")])];
- val rec_styp = "i=>i";
- val ext = None
- val sintrs =
- ["Nil : list(A)",
- "[| a: A; l: list(A) |] ==> Cons(a,l) : list(A)"];
- val monos = [];
+ (val thy = Univ.thy
+ val rec_specs = [("list", "univ(A)",
+ [(["Nil"], "i"),
+ (["Cons"], "[i,i]=>i")])]
+ val rec_styp = "i=>i"
+ val ext = None
+ val sintrs = ["Nil : list(A)",
+ "[| a: A; l: list(A) |] ==> Cons(a,l) : list(A)"]
+ val monos = []
val type_intrs = datatype_intrs
val type_elims = datatype_elims);
--- a/src/ZF/ex/Acc.ML Thu Mar 17 11:24:31 1994 +0100
+++ b/src/ZF/ex/Acc.ML Thu Mar 17 12:36:58 1994 +0100
@@ -10,13 +10,12 @@
*)
structure Acc = Inductive_Fun
- (val thy = WF.thy addconsts [(["acc"],"i=>i")];
- val rec_doms = [("acc", "field(r)")];
- val sintrs =
- ["[| r-``{a} : Pow(acc(r)); a : field(r) |] ==> a : acc(r)"];
- val monos = [Pow_mono];
- val con_defs = [];
- val type_intrs = [];
+ (val thy = WF.thy addconsts [(["acc"],"i=>i")]
+ val rec_doms = [("acc", "field(r)")]
+ val sintrs = ["[| r-``{a}: Pow(acc(r)); a: field(r) |] ==> a: acc(r)"]
+ val monos = [Pow_mono]
+ val con_defs = []
+ val type_intrs = []
val type_elims = []);
goal Acc.thy "!!a b r. [| b: acc(r); <a,b>: r |] ==> a: acc(r)";
--- a/src/ZF/ex/Data.ML Thu Mar 17 11:24:31 1994 +0100
+++ b/src/ZF/ex/Data.ML Thu Mar 17 12:36:58 1994 +0100
@@ -8,21 +8,20 @@
*)
structure Data = Datatype_Fun
- (val thy = Univ.thy;
- val rec_specs =
- [("data", "univ(A Un B)",
- [(["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 =
- ["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 thy = Univ.thy
+ val rec_specs = [("data", "univ(A Un B)",
+ [(["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 =
+ ["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 Mar 17 11:24:31 1994 +0100
+++ b/src/ZF/ex/LList.ML Thu Mar 17 12:36:58 1994 +0100
@@ -7,20 +7,18 @@
*)
structure LList = CoDatatype_Fun
- (val thy = QUniv.thy;
- val rec_specs =
- [("llist", "quniv(A)",
- [(["LNil"], "i"),
- (["LCons"], "[i,i]=>i")])];
- val rec_styp = "i=>i";
- val ext = None
- val sintrs =
- ["LNil : llist(A)",
- "[| a: A; l: llist(A) |] ==> LCons(a,l) : llist(A)"];
- val monos = [];
+ (val thy = QUniv.thy
+ val rec_specs = [("llist", "quniv(A)",
+ [(["LNil"], "i"),
+ (["LCons"], "[i,i]=>i")])]
+ val rec_styp = "i=>i"
+ val ext = None
+ val sintrs = ["LNil : llist(A)",
+ "[| a: A; l: llist(A) |] ==> LCons(a,l) : llist(A)"]
+ val monos = []
val type_intrs = codatatype_intrs
val type_elims = codatatype_elims);
-
+
val [LNilI, LConsI] = LList.intrs;
(*An elimination rule, for type-checking*)
--- a/src/ZF/ex/LList_Eq.ML Thu Mar 17 11:24:31 1994 +0100
+++ b/src/ZF/ex/LList_Eq.ML Thu Mar 17 12:36:58 1994 +0100
@@ -11,14 +11,14 @@
a q/Q to the Sigma, Pair and converse rules.*)
structure LList_Eq = CoInductive_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@[SigmaI];
+ (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 @ [SigmaI]
val type_elims = [SigmaE2]);
(** Alternatives for above:
--- a/src/ZF/ex/ListN.ML Thu Mar 17 11:24:31 1994 +0100
+++ b/src/ZF/ex/ListN.ML Thu Mar 17 12:36:58 1994 +0100
@@ -10,14 +10,14 @@
*)
structure ListN = Inductive_Fun
- (val thy = ListFn.thy addconsts [(["listn"],"i=>i")];
- val rec_doms = [("listn", "nat*list(A)")];
- val sintrs =
- ["<0,Nil> : listn(A)",
- "[| a: A; <n,l> : listn(A) |] ==> <succ(n), Cons(a,l)> : listn(A)"];
- val monos = [];
- val con_defs = [];
- val type_intrs = nat_typechecks@List.intrs@[SigmaI]
+ (val thy = ListFn.thy addconsts [(["listn"],"i=>i")]
+ val rec_doms = [("listn", "nat*list(A)")]
+ val sintrs =
+ ["<0,Nil> : listn(A)",
+ "[| a: A; <n,l> : listn(A) |] ==> <succ(n), Cons(a,l)> : listn(A)"]
+ val monos = []
+ val con_defs = []
+ val type_intrs = nat_typechecks @ List.intrs @ [SigmaI]
val type_elims = [SigmaE2]);
val listn_induct = standard
--- a/src/ZF/ex/Primrec0.ML Thu Mar 17 11:24:31 1994 +0100
+++ b/src/ZF/ex/Primrec0.ML Thu Mar 17 12:36:58 1994 +0100
@@ -64,20 +64,20 @@
(*** Inductive definition of the PR functions ***)
structure Primrec = Inductive_Fun
- (val thy = Primrec0.thy;
- val rec_doms = [("primrec", "list(nat)->nat")];
- val ext = None
- val sintrs =
+ (val thy = Primrec0.thy
+ val rec_doms = [("primrec", "list(nat)->nat")]
+ val sintrs =
["SC : primrec",
"k: nat ==> CONST(k) : primrec",
"i: nat ==> PROJ(i) : primrec",
- "[| g: primrec; fs: list(primrec) |] ==> COMP(g,fs): primrec",
- "[| f: primrec; g: primrec |] ==> PREC(f,g): primrec"];
- val monos = [list_mono];
- val con_defs = [SC_def,CONST_def,PROJ_def,COMP_def,PREC_def];
+ "[| g: primrec; fs: list(primrec) |] ==> COMP(g,fs): primrec",
+ "[| f: primrec; g: primrec |] ==> PREC(f,g): primrec"]
+ val monos = [list_mono]
+ val con_defs = [SC_def,CONST_def,PROJ_def,COMP_def,PREC_def]
val type_intrs = pr0_typechecks
val type_elims = []);
+
(* c: primrec ==> c: list(nat) -> nat *)
val primrec_into_fun = Primrec.dom_subset RS subsetD;
--- a/src/ZF/ex/TF.ML Thu Mar 17 11:24:31 1994 +0100
+++ b/src/ZF/ex/TF.ML Thu Mar 17 12:36:58 1994 +0100
@@ -7,20 +7,19 @@
*)
structure TF = Datatype_Fun
- (val thy = Univ.thy;
- val rec_specs =
- [("tree", "univ(A)",
- [(["Tcons"], "[i,i]=>i")]),
- ("forest", "univ(A)",
- [(["Fnil"], "i"),
- (["Fcons"], "[i,i]=>i")])];
- val rec_styp = "i=>i";
- val ext = None
- val sintrs =
- ["[| a:A; f: forest(A) |] ==> Tcons(a,f) : tree(A)",
- "Fnil : forest(A)",
- "[| t: tree(A); f: forest(A) |] ==> Fcons(t,f) : forest(A)"];
- val monos = [];
+ (val thy = Univ.thy
+ val rec_specs = [("tree", "univ(A)",
+ [(["Tcons"], "[i,i]=>i")]),
+ ("forest", "univ(A)",
+ [(["Fnil"], "i"),
+ (["Fcons"], "[i,i]=>i")])]
+ val rec_styp = "i=>i"
+ val ext = None
+ val sintrs =
+ ["[| a:A; f: forest(A) |] ==> Tcons(a,f) : tree(A)",
+ "Fnil : forest(A)",
+ "[| t: tree(A); f: forest(A) |] ==> Fcons(t,f) : forest(A)"]
+ val monos = []
val type_intrs = datatype_intrs
val type_elims = datatype_elims);
--- a/src/ZF/ex/acc.ML Thu Mar 17 11:24:31 1994 +0100
+++ b/src/ZF/ex/acc.ML Thu Mar 17 12:36:58 1994 +0100
@@ -10,13 +10,12 @@
*)
structure Acc = Inductive_Fun
- (val thy = WF.thy addconsts [(["acc"],"i=>i")];
- val rec_doms = [("acc", "field(r)")];
- val sintrs =
- ["[| r-``{a} : Pow(acc(r)); a : field(r) |] ==> a : acc(r)"];
- val monos = [Pow_mono];
- val con_defs = [];
- val type_intrs = [];
+ (val thy = WF.thy addconsts [(["acc"],"i=>i")]
+ val rec_doms = [("acc", "field(r)")]
+ val sintrs = ["[| r-``{a}: Pow(acc(r)); a: field(r) |] ==> a: acc(r)"]
+ val monos = [Pow_mono]
+ val con_defs = []
+ val type_intrs = []
val type_elims = []);
goal Acc.thy "!!a b r. [| b: acc(r); <a,b>: r |] ==> a: acc(r)";
--- a/src/ZF/ex/data.ML Thu Mar 17 11:24:31 1994 +0100
+++ b/src/ZF/ex/data.ML Thu Mar 17 12:36:58 1994 +0100
@@ -8,21 +8,20 @@
*)
structure Data = Datatype_Fun
- (val thy = Univ.thy;
- val rec_specs =
- [("data", "univ(A Un B)",
- [(["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 =
- ["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 thy = Univ.thy
+ val rec_specs = [("data", "univ(A Un B)",
+ [(["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 =
+ ["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 Mar 17 11:24:31 1994 +0100
+++ b/src/ZF/ex/listn.ML Thu Mar 17 12:36:58 1994 +0100
@@ -10,14 +10,14 @@
*)
structure ListN = Inductive_Fun
- (val thy = ListFn.thy addconsts [(["listn"],"i=>i")];
- val rec_doms = [("listn", "nat*list(A)")];
- val sintrs =
- ["<0,Nil> : listn(A)",
- "[| a: A; <n,l> : listn(A) |] ==> <succ(n), Cons(a,l)> : listn(A)"];
- val monos = [];
- val con_defs = [];
- val type_intrs = nat_typechecks@List.intrs@[SigmaI]
+ (val thy = ListFn.thy addconsts [(["listn"],"i=>i")]
+ val rec_doms = [("listn", "nat*list(A)")]
+ val sintrs =
+ ["<0,Nil> : listn(A)",
+ "[| a: A; <n,l> : listn(A) |] ==> <succ(n), Cons(a,l)> : listn(A)"]
+ val monos = []
+ val con_defs = []
+ val type_intrs = nat_typechecks @ List.intrs @ [SigmaI]
val type_elims = [SigmaE2]);
val listn_induct = standard
--- a/src/ZF/ex/llist.ML Thu Mar 17 11:24:31 1994 +0100
+++ b/src/ZF/ex/llist.ML Thu Mar 17 12:36:58 1994 +0100
@@ -7,20 +7,18 @@
*)
structure LList = CoDatatype_Fun
- (val thy = QUniv.thy;
- val rec_specs =
- [("llist", "quniv(A)",
- [(["LNil"], "i"),
- (["LCons"], "[i,i]=>i")])];
- val rec_styp = "i=>i";
- val ext = None
- val sintrs =
- ["LNil : llist(A)",
- "[| a: A; l: llist(A) |] ==> LCons(a,l) : llist(A)"];
- val monos = [];
+ (val thy = QUniv.thy
+ val rec_specs = [("llist", "quniv(A)",
+ [(["LNil"], "i"),
+ (["LCons"], "[i,i]=>i")])]
+ val rec_styp = "i=>i"
+ val ext = None
+ val sintrs = ["LNil : llist(A)",
+ "[| a: A; l: llist(A) |] ==> LCons(a,l) : llist(A)"]
+ val monos = []
val type_intrs = codatatype_intrs
val type_elims = codatatype_elims);
-
+
val [LNilI, LConsI] = LList.intrs;
(*An elimination rule, for type-checking*)
--- a/src/ZF/ex/llist_eq.ML Thu Mar 17 11:24:31 1994 +0100
+++ b/src/ZF/ex/llist_eq.ML Thu Mar 17 12:36:58 1994 +0100
@@ -11,14 +11,14 @@
a q/Q to the Sigma, Pair and converse rules.*)
structure LList_Eq = CoInductive_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@[SigmaI];
+ (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 @ [SigmaI]
val type_elims = [SigmaE2]);
(** Alternatives for above:
--- a/src/ZF/ex/primrec0.ML Thu Mar 17 11:24:31 1994 +0100
+++ b/src/ZF/ex/primrec0.ML Thu Mar 17 12:36:58 1994 +0100
@@ -64,20 +64,20 @@
(*** Inductive definition of the PR functions ***)
structure Primrec = Inductive_Fun
- (val thy = Primrec0.thy;
- val rec_doms = [("primrec", "list(nat)->nat")];
- val ext = None
- val sintrs =
+ (val thy = Primrec0.thy
+ val rec_doms = [("primrec", "list(nat)->nat")]
+ val sintrs =
["SC : primrec",
"k: nat ==> CONST(k) : primrec",
"i: nat ==> PROJ(i) : primrec",
- "[| g: primrec; fs: list(primrec) |] ==> COMP(g,fs): primrec",
- "[| f: primrec; g: primrec |] ==> PREC(f,g): primrec"];
- val monos = [list_mono];
- val con_defs = [SC_def,CONST_def,PROJ_def,COMP_def,PREC_def];
+ "[| g: primrec; fs: list(primrec) |] ==> COMP(g,fs): primrec",
+ "[| f: primrec; g: primrec |] ==> PREC(f,g): primrec"]
+ val monos = [list_mono]
+ val con_defs = [SC_def,CONST_def,PROJ_def,COMP_def,PREC_def]
val type_intrs = pr0_typechecks
val type_elims = []);
+
(* c: primrec ==> c: list(nat) -> nat *)
val primrec_into_fun = Primrec.dom_subset RS subsetD;
--- a/src/ZF/ex/tf.ML Thu Mar 17 11:24:31 1994 +0100
+++ b/src/ZF/ex/tf.ML Thu Mar 17 12:36:58 1994 +0100
@@ -7,20 +7,19 @@
*)
structure TF = Datatype_Fun
- (val thy = Univ.thy;
- val rec_specs =
- [("tree", "univ(A)",
- [(["Tcons"], "[i,i]=>i")]),
- ("forest", "univ(A)",
- [(["Fnil"], "i"),
- (["Fcons"], "[i,i]=>i")])];
- val rec_styp = "i=>i";
- val ext = None
- val sintrs =
- ["[| a:A; f: forest(A) |] ==> Tcons(a,f) : tree(A)",
- "Fnil : forest(A)",
- "[| t: tree(A); f: forest(A) |] ==> Fcons(t,f) : forest(A)"];
- val monos = [];
+ (val thy = Univ.thy
+ val rec_specs = [("tree", "univ(A)",
+ [(["Tcons"], "[i,i]=>i")]),
+ ("forest", "univ(A)",
+ [(["Fnil"], "i"),
+ (["Fcons"], "[i,i]=>i")])]
+ val rec_styp = "i=>i"
+ val ext = None
+ val sintrs =
+ ["[| a:A; f: forest(A) |] ==> Tcons(a,f) : tree(A)",
+ "Fnil : forest(A)",
+ "[| t: tree(A); f: forest(A) |] ==> Fcons(t,f) : forest(A)"]
+ val monos = []
val type_intrs = datatype_intrs
val type_elims = datatype_elims);
--- a/src/ZF/fin.ML Thu Mar 17 11:24:31 1994 +0100
+++ b/src/ZF/fin.ML Thu Mar 17 12:36:58 1994 +0100
@@ -18,13 +18,12 @@
*)
structure Fin = Inductive_Fun
- (val thy = Arith.thy addconsts [(["Fin"],"i=>i")];
- val rec_doms = [("Fin","Pow(A)")];
- val sintrs =
- ["0 : Fin(A)",
- "[| a: A; b: Fin(A) |] ==> cons(a,b) : Fin(A)"];
- val monos = [];
- val con_defs = [];
+ (val thy = Arith.thy addconsts [(["Fin"],"i=>i")]
+ val rec_doms = [("Fin","Pow(A)")]
+ val sintrs = ["0 : Fin(A)",
+ "[| a: A; b: Fin(A) |] ==> cons(a,b) : Fin(A)"]
+ val monos = []
+ val con_defs = []
val type_intrs = [empty_subsetI, cons_subsetI, PowI]
val type_elims = [make_elim PowD]);
--- a/src/ZF/list.ML Thu Mar 17 11:24:31 1994 +0100
+++ b/src/ZF/list.ML Thu Mar 17 12:36:58 1994 +0100
@@ -7,17 +7,15 @@
*)
structure List = Datatype_Fun
- (val thy = Univ.thy;
- val rec_specs =
- [("list", "univ(A)",
- [(["Nil"], "i"),
- (["Cons"], "[i,i]=>i")])];
- val rec_styp = "i=>i";
- val ext = None
- val sintrs =
- ["Nil : list(A)",
- "[| a: A; l: list(A) |] ==> Cons(a,l) : list(A)"];
- val monos = [];
+ (val thy = Univ.thy
+ val rec_specs = [("list", "univ(A)",
+ [(["Nil"], "i"),
+ (["Cons"], "[i,i]=>i")])]
+ val rec_styp = "i=>i"
+ val ext = None
+ val sintrs = ["Nil : list(A)",
+ "[| a: A; l: list(A) |] ==> Cons(a,l) : list(A)"]
+ val monos = []
val type_intrs = datatype_intrs
val type_elims = datatype_elims);
--- a/src/ZF/simpdata.ML Thu Mar 17 11:24:31 1994 +0100
+++ b/src/ZF/simpdata.ML Thu Mar 17 12:36:58 1994 +0100
@@ -86,9 +86,6 @@
| _ $ A => tryrules atomize_pairs A
end;
-fun ZF_mk_rew_rules th = map mk_meta_eq (atomize th);
-
-
val ZF_simps = [empty_subsetI, consI1, succI1, ball_simp, if_true, if_false,
beta, eta, restrict, fst_conv, snd_conv, split];
@@ -99,6 +96,6 @@
[ball_cong, bex_cong, Replace_cong, RepFun_cong, Collect_cong, lam_cong];
val ZF_ss = FOL_ss
- setmksimps ZF_mk_rew_rules
+ setmksimps (map mk_meta_eq o atomize o gen_all)
addsimps (ZF_simps @ mem_simps @ bquant_simps)
addcongs ZF_congs;