made pseudo theories for all ML files;
documented dependencies between all thy and ML files
--- a/src/ZF/Arith.thy Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/Arith.thy Tue Nov 16 14:24:21 1993 +0100
@@ -6,7 +6,7 @@
Arithmetic operators and their definitions
*)
-Arith = Epsilon +
+Arith = Epsilon + "simpdata" +
consts
rec :: "[i, i, [i,i]=>i]=>i"
"#*" :: "[i,i]=>i" (infixl 70)
--- a/src/ZF/Bool.thy Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/Bool.thy Tue Nov 16 14:24:21 1993 +0100
@@ -6,7 +6,7 @@
Booleans in Zermelo-Fraenkel Set Theory
*)
-Bool = ZF +
+Bool = ZF + "simpdata" +
consts
"1" :: "i" ("1")
bool :: "i"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Datatype.thy Tue Nov 16 14:24:21 1993 +0100
@@ -0,0 +1,4 @@
+(*Dummy theory to document dependencies *)
+
+Datatype = "constructor" + "inductive" + "coinductive" + Univ + QUniv
+ (*this must be capital to avoid conflicts with ML's "datatype" *)
\ No newline at end of file
--- a/src/ZF/Epsilon.thy Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/Epsilon.thy Tue Nov 16 14:24:21 1993 +0100
@@ -6,7 +6,7 @@
Epsilon induction and recursion
*)
-Epsilon = Nat +
+Epsilon = Nat + "mono" +
consts
eclose,rank :: "i=>i"
transrec :: "[i, [i,i]=>i] =>i"
--- a/src/ZF/Fixedpt.thy Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/Fixedpt.thy Tue Nov 16 14:24:21 1993 +0100
@@ -6,7 +6,7 @@
Least and greatest fixed points
*)
-Fixedpt = ZF +
+Fixedpt = ZF + "domrange" +
consts
bnd_mono :: "[i,i=>i]=>o"
lfp, gfp :: "[i,i=>i]=>i"
--- a/src/ZF/List.ML Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/List.ML Tue Nov 16 14:24:21 1993 +0100
@@ -21,6 +21,8 @@
val type_intrs = datatype_intrs
val type_elims = datatype_elims);
+store_theory "List" List.thy;
+
val [NilI, ConsI] = List.intrs;
(*An elimination rule, for type-checking*)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/List.thy Tue Nov 16 14:24:21 1993 +0100
@@ -0,0 +1,3 @@
+(*Dummy theory to document dependencies *)
+
+list = Univ + "Datatype" + "intr_elim"
--- a/src/ZF/ListFn.thy Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/ListFn.thy Tue Nov 16 14:24:21 1993 +0100
@@ -10,7 +10,7 @@
although complicating its derivation.
*)
-ListFn = List +
+ListFn = List + "constructor" +
consts
"@" :: "[i,i]=>i" (infixr 60)
list_rec :: "[i, i, [i,i,i]=>i] => i"
--- a/src/ZF/Nat.thy Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/Nat.thy Tue Nov 16 14:24:21 1993 +0100
@@ -6,7 +6,7 @@
Natural numbers in Zermelo-Fraenkel Set Theory
*)
-Nat = Ord + Bool +
+Nat = Ord + Bool + "mono" +
consts
nat :: "i"
nat_case :: "[i, i=>i, i]=>i"
--- a/src/ZF/Ord.thy Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/Ord.thy Tue Nov 16 14:24:21 1993 +0100
@@ -6,7 +6,7 @@
Ordinals in Zermelo-Fraenkel Set Theory
*)
-Ord = WF +
+Ord = WF + "simpdata" + "equalities" +
consts
Memrel :: "i=>i"
Transset,Ord :: "i=>o"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Pair.thy Tue Nov 16 14:24:21 1993 +0100
@@ -0,0 +1,3 @@
+(*Dummy theory to document dependencies *)
+
+pair = "upair"
--- a/src/ZF/Perm.thy Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/Perm.thy Tue Nov 16 14:24:21 1993 +0100
@@ -9,7 +9,7 @@
-- Lemmas for the Schroeder-Bernstein Theorem
*)
-Perm = ZF +
+Perm = ZF + "mono" +
consts
O :: "[i,i]=>i" (infixr 60)
id :: "i=>i"
--- a/src/ZF/QPair.thy Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/QPair.thy Tue Nov 16 14:24:21 1993 +0100
@@ -11,7 +11,7 @@
1966.
*)
-QPair = Sum +
+QPair = Sum + "simpdata" +
consts
QPair :: "[i, i] => i" ("<(_;/ _)>")
qsplit :: "[[i,i] => i, i] => i"
--- a/src/ZF/QUniv.thy Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/QUniv.thy Tue Nov 16 14:24:21 1993 +0100
@@ -6,7 +6,7 @@
A small universe for lazy recursive types
*)
-QUniv = Univ + QPair +
+QUniv = Univ + QPair + "mono" + "equalities" +
consts
quniv :: "i=>i"
--- a/src/ZF/ROOT.ML Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/ROOT.ML Tue Nov 16 14:24:21 1993 +0100
@@ -11,8 +11,6 @@
val banner = "ZF Set Theory (in FOL)";
writeln banner;
-set_loadpath [".", "ex", "../FOL"];
-
(*For Pure/tactic?? A crude way of adding structure to rules*)
fun CHECK_SOLVED (Tactic tf) =
Tactic (fn state =>
@@ -29,47 +27,9 @@
fun DO_GOAL tfs = SELECT_GOAL (CHECK_SOLVED (EVERY1 tfs));
print_depth 1;
-use_thy "zf";
-use "upair.ML";
-use "subset.ML";
-use "pair.ML";
-use "domrange.ML";
-use "func.ML";
-use "equalities.ML";
-use "simpdata.ML";
-
-(*further development*)
-use_thy "bool";
-use_thy "sum";
-use_thy "qpair";
-use "mono.ML";
-use_thy "fixedpt";
-
-(*Inductive/coinductive definitions*)
-use "ind_syntax.ML";
-use "intr_elim.ML";
-use "indrule.ML";
-use "inductive.ML";
-use "coinductive.ML";
-
-use_thy "perm";
-use_thy "trancl";
-use_thy "wf";
-use_thy "ord";
-use_thy "nat";
-use_thy "epsilon";
-use_thy "arith";
-
-(*Datatype/codatatype definitions*)
-use_thy "univ";
-use_thy "quniv";
-use "constructor.ML";
-use "datatype.ML";
-
-use "fin.ML";
-use_thy "List";
-use_thy "listfn";
+use_thy "fin";
+use_thy "ListFn";
(*printing functions are inherited from FOL*)
print_depth 8;
--- a/src/ZF/Sum.thy Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/Sum.thy Tue Nov 16 14:24:21 1993 +0100
@@ -7,7 +7,7 @@
"Part" primitive for simultaneous recursive type definitions
*)
-Sum = Bool +
+Sum = Bool + "simpdata" +
consts
"+" :: "[i,i]=>i" (infixr 65)
Inl,Inr :: "i=>i"
--- a/src/ZF/Trancl.thy Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/Trancl.thy Tue Nov 16 14:24:21 1993 +0100
@@ -6,7 +6,7 @@
Transitive closure of a relation
*)
-Trancl = Fixedpt + Perm +
+Trancl = Fixedpt + Perm + "mono" +
consts
"rtrancl" :: "i=>i" ("(_^*)" [100] 100) (*refl/transitive closure*)
"trancl" :: "i=>i" ("(_^+)" [100] 100) (*transitive closure*)
--- a/src/ZF/Univ.thy Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/Univ.thy Tue Nov 16 14:24:21 1993 +0100
@@ -8,7 +8,7 @@
Standard notation for Vset(i) is V(i), but users might want V for a variable
*)
-Univ = Arith + Sum +
+Univ = Arith + Sum + "mono" +
consts
Limit :: "i=>o"
Vfrom :: "[i,i]=>i"
--- a/src/ZF/WF.thy Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/WF.thy Tue Nov 16 14:24:21 1993 +0100
@@ -6,7 +6,7 @@
Well-founded Recursion
*)
-WF = Trancl +
+WF = Trancl + "mono" +
consts
wf :: "i=>o"
wftrec,wfrec :: "[i, i, [i,i]=>i] =>i"
--- a/src/ZF/arith.thy Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/arith.thy Tue Nov 16 14:24:21 1993 +0100
@@ -6,7 +6,7 @@
Arithmetic operators and their definitions
*)
-Arith = Epsilon +
+Arith = Epsilon + "simpdata" +
consts
rec :: "[i, i, [i,i]=>i]=>i"
"#*" :: "[i,i]=>i" (infixl 70)
--- a/src/ZF/bool.thy Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/bool.thy Tue Nov 16 14:24:21 1993 +0100
@@ -6,7 +6,7 @@
Booleans in Zermelo-Fraenkel Set Theory
*)
-Bool = ZF +
+Bool = ZF + "simpdata" +
consts
"1" :: "i" ("1")
bool :: "i"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/coinductive.thy Tue Nov 16 14:24:21 1993 +0100
@@ -0,0 +1,3 @@
+(*Dummy theory to document dependencies *)
+
+coinductive = "ind_syntax" + "intr_elim"
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/constructor.thy Tue Nov 16 14:24:21 1993 +0100
@@ -0,0 +1,3 @@
+(*Dummy theory to document dependencies *)
+
+constructor = "ind_syntax"
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/datatype.thy Tue Nov 16 14:24:21 1993 +0100
@@ -0,0 +1,4 @@
+(*Dummy theory to document dependencies *)
+
+Datatype = "constructor" + "inductive" + "coinductive" + Univ + QUniv
+ (*this must be capital to avoid conflicts with ML's "datatype" *)
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/domrange.thy Tue Nov 16 14:24:21 1993 +0100
@@ -0,0 +1,3 @@
+(*Dummy theory to document dependencies *)
+
+domrange = "pair" + "subset"
--- a/src/ZF/epsilon.thy Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/epsilon.thy Tue Nov 16 14:24:21 1993 +0100
@@ -6,7 +6,7 @@
Epsilon induction and recursion
*)
-Epsilon = Nat +
+Epsilon = Nat + "mono" +
consts
eclose,rank :: "i=>i"
transrec :: "[i, [i,i]=>i] =>i"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/equalities.thy Tue Nov 16 14:24:21 1993 +0100
@@ -0,0 +1,3 @@
+(*Dummy theory to document dependencies *)
+
+equalities = "domrange"
\ No newline at end of file
--- a/src/ZF/fin.ML Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/fin.ML Tue Nov 16 14:24:21 1993 +0100
@@ -28,6 +28,8 @@
val type_intrs = [empty_subsetI, cons_subsetI, PowI]
val type_elims = [make_elim PowD]);
+store_theory "Fin" Fin.thy;
+
val [Fin_0I, Fin_consI] = Fin.intrs;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/fin.thy Tue Nov 16 14:24:21 1993 +0100
@@ -0,0 +1,3 @@
+(*Dummy theory to document dependencies *)
+
+fin = Arith + "inductive" + "constructor" + "intr_elim" + "equalities"
--- a/src/ZF/fixedpt.thy Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/fixedpt.thy Tue Nov 16 14:24:21 1993 +0100
@@ -6,7 +6,7 @@
Least and greatest fixed points
*)
-Fixedpt = ZF +
+Fixedpt = ZF + "domrange" +
consts
bnd_mono :: "[i,i=>i]=>o"
lfp, gfp :: "[i,i=>i]=>i"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/func.thy Tue Nov 16 14:24:21 1993 +0100
@@ -0,0 +1,3 @@
+(*Dummy theory to document dependencies *)
+
+func = "domrange"
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ind_syntax.thy Tue Nov 16 14:24:21 1993 +0100
@@ -0,0 +1,3 @@
+(*Dummy theory to document dependencies *)
+
+ind_syntax = "mono"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/indrule.thy Tue Nov 16 14:24:21 1993 +0100
@@ -0,0 +1,3 @@
+(*Dummy theory to document dependencies *)
+
+indrule = "ind_syntax" + "intr_elim"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/inductive.thy Tue Nov 16 14:24:21 1993 +0100
@@ -0,0 +1,3 @@
+(*Dummy theory to document dependencies *)
+
+inductive = "indrule"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/intr_elim.thy Tue Nov 16 14:24:21 1993 +0100
@@ -0,0 +1,3 @@
+(*Dummy theory to document dependencies *)
+
+intr_elim = Fixedpt + "ind_syntax"
--- a/src/ZF/list.ML Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/list.ML Tue Nov 16 14:24:21 1993 +0100
@@ -21,6 +21,8 @@
val type_intrs = datatype_intrs
val type_elims = datatype_elims);
+store_theory "List" List.thy;
+
val [NilI, ConsI] = List.intrs;
(*An elimination rule, for type-checking*)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/list.thy Tue Nov 16 14:24:21 1993 +0100
@@ -0,0 +1,3 @@
+(*Dummy theory to document dependencies *)
+
+list = Univ + "Datatype" + "intr_elim"
--- a/src/ZF/listfn.thy Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/listfn.thy Tue Nov 16 14:24:21 1993 +0100
@@ -10,7 +10,7 @@
although complicating its derivation.
*)
-ListFn = List +
+ListFn = List + "constructor" +
consts
"@" :: "[i,i]=>i" (infixr 60)
list_rec :: "[i, i, [i,i,i]=>i] => i"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/mono.thy Tue Nov 16 14:24:21 1993 +0100
@@ -0,0 +1,3 @@
+(*Dummy theory to document dependencies *)
+
+mono = QPair + Sum
--- a/src/ZF/nat.thy Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/nat.thy Tue Nov 16 14:24:21 1993 +0100
@@ -6,7 +6,7 @@
Natural numbers in Zermelo-Fraenkel Set Theory
*)
-Nat = Ord + Bool +
+Nat = Ord + Bool + "mono" +
consts
nat :: "i"
nat_case :: "[i, i=>i, i]=>i"
--- a/src/ZF/ord.thy Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/ord.thy Tue Nov 16 14:24:21 1993 +0100
@@ -6,7 +6,7 @@
Ordinals in Zermelo-Fraenkel Set Theory
*)
-Ord = WF +
+Ord = WF + "simpdata" + "equalities" +
consts
Memrel :: "i=>i"
Transset,Ord :: "i=>o"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/pair.thy Tue Nov 16 14:24:21 1993 +0100
@@ -0,0 +1,3 @@
+(*Dummy theory to document dependencies *)
+
+pair = "upair"
--- a/src/ZF/perm.thy Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/perm.thy Tue Nov 16 14:24:21 1993 +0100
@@ -9,7 +9,7 @@
-- Lemmas for the Schroeder-Bernstein Theorem
*)
-Perm = ZF +
+Perm = ZF + "mono" +
consts
O :: "[i,i]=>i" (infixr 60)
id :: "i=>i"
--- a/src/ZF/qpair.thy Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/qpair.thy Tue Nov 16 14:24:21 1993 +0100
@@ -11,7 +11,7 @@
1966.
*)
-QPair = Sum +
+QPair = Sum + "simpdata" +
consts
QPair :: "[i, i] => i" ("<(_;/ _)>")
qsplit :: "[[i,i] => i, i] => i"
--- a/src/ZF/quniv.thy Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/quniv.thy Tue Nov 16 14:24:21 1993 +0100
@@ -6,7 +6,7 @@
A small universe for lazy recursive types
*)
-QUniv = Univ + QPair +
+QUniv = Univ + QPair + "mono" + "equalities" +
consts
quniv :: "i=>i"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/simpdata.thy Tue Nov 16 14:24:21 1993 +0100
@@ -0,0 +1,3 @@
+(*Dummy theory to document dependencies *)
+
+simpdata = "func"
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/subset.thy Tue Nov 16 14:24:21 1993 +0100
@@ -0,0 +1,3 @@
+(*Dummy theory to document dependencies *)
+
+subset = "upair"
--- a/src/ZF/sum.thy Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/sum.thy Tue Nov 16 14:24:21 1993 +0100
@@ -7,7 +7,7 @@
"Part" primitive for simultaneous recursive type definitions
*)
-Sum = Bool +
+Sum = Bool + "simpdata" +
consts
"+" :: "[i,i]=>i" (infixr 65)
Inl,Inr :: "i=>i"
--- a/src/ZF/trancl.thy Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/trancl.thy Tue Nov 16 14:24:21 1993 +0100
@@ -6,7 +6,7 @@
Transitive closure of a relation
*)
-Trancl = Fixedpt + Perm +
+Trancl = Fixedpt + Perm + "mono" +
consts
"rtrancl" :: "i=>i" ("(_^*)" [100] 100) (*refl/transitive closure*)
"trancl" :: "i=>i" ("(_^+)" [100] 100) (*transitive closure*)
--- a/src/ZF/univ.thy Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/univ.thy Tue Nov 16 14:24:21 1993 +0100
@@ -8,7 +8,7 @@
Standard notation for Vset(i) is V(i), but users might want V for a variable
*)
-Univ = Arith + Sum +
+Univ = Arith + Sum + "mono" +
consts
Limit :: "i=>o"
Vfrom :: "[i,i]=>i"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/upair.thy Tue Nov 16 14:24:21 1993 +0100
@@ -0,0 +1,3 @@
+(*Dummy theory to document dependencies *)
+
+upair = ZF
--- a/src/ZF/wf.thy Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/wf.thy Tue Nov 16 14:24:21 1993 +0100
@@ -6,7 +6,7 @@
Well-founded Recursion
*)
-WF = Trancl +
+WF = Trancl + "mono" +
consts
wf :: "i=>o"
wftrec,wfrec :: "[i, i, [i,i]=>i] =>i"