ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
the keyword "inductive" making the theory file fail
ZF/Makefile: now has Inductive.thy,.ML
ZF/Datatype,Finite,Zorn: depend upon Inductive
ZF/intr_elim: now checks that the inductive name does not clash with
existing theory names
ZF/ind_section: deleted things replicated in Pure/section_utils.ML
ZF/ROOT: now loads Pure/section_utils
--- a/src/ZF/Datatype.thy Thu Aug 25 10:41:17 1994 +0200
+++ b/src/ZF/Datatype.thy Thu Aug 25 12:09:21 1994 +0200
@@ -1,5 +1,5 @@
(*Dummy theory to document dependencies *)
-Datatype = "constructor" + "inductive" + Univ + QUniv
+Datatype = "constructor" + "Inductive" + Univ + QUniv
(*Datatype must be capital to avoid conflicts with ML's "datatype" *)
\ No newline at end of file
--- a/src/ZF/Finite.thy Thu Aug 25 10:41:17 1994 +0200
+++ b/src/ZF/Finite.thy Thu Aug 25 12:09:21 1994 +0200
@@ -6,7 +6,7 @@
Finite powerset operator
*)
-Finite = Arith +
+Finite = Arith + "Inductive" +
consts
Fin :: "i=>i"
FiniteFun :: "[i,i]=>i" ("(_ -||>/ _)" [61, 60] 60)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Inductive.ML Thu Aug 25 12:09:21 1994 +0200
@@ -0,0 +1,228 @@
+(* Title: ZF/Inductive.ML
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1993 University of Cambridge
+
+(Co)Inductive Definitions for Zermelo-Fraenkel Set Theory
+
+Inductive definitions use least fixedpoints with standard products and sums
+Coinductive definitions use greatest fixedpoints with Quine products and sums
+
+Sums are used only for mutual recursion;
+Products are used only to derive "streamlined" induction rules for relations
+*)
+
+local open Ind_Syntax
+in
+structure Lfp =
+ struct
+ val oper = Const("lfp", [iT,iT-->iT]--->iT)
+ val bnd_mono = Const("bnd_mono", [iT,iT-->iT]--->oT)
+ val bnd_monoI = bnd_monoI
+ val subs = def_lfp_subset
+ val Tarski = def_lfp_Tarski
+ val induct = def_induct
+ end;
+
+structure Standard_Prod =
+ struct
+ val sigma = Const("Sigma", [iT, iT-->iT]--->iT)
+ val pair = Const("Pair", [iT,iT]--->iT)
+ val split_const = Const("split", [[iT,iT]--->iT, iT]--->iT)
+ val fsplit_const = Const("fsplit", [[iT,iT]--->oT, iT]--->oT)
+ val pair_iff = Pair_iff
+ val split_eq = split
+ val fsplitI = fsplitI
+ val fsplitD = fsplitD
+ val fsplitE = fsplitE
+ end;
+
+structure Standard_Sum =
+ struct
+ val sum = Const("op +", [iT,iT]--->iT)
+ val inl = Const("Inl", iT-->iT)
+ val inr = Const("Inr", iT-->iT)
+ val elim = Const("case", [iT-->iT, iT-->iT, iT]--->iT)
+ val case_inl = case_Inl
+ val case_inr = case_Inr
+ val inl_iff = Inl_iff
+ val inr_iff = Inr_iff
+ val distinct = Inl_Inr_iff
+ val distinct' = Inr_Inl_iff
+ end;
+end;
+
+functor Ind_section_Fun (Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end)
+ : sig include INTR_ELIM INDRULE end =
+struct
+structure Intr_elim =
+ Intr_elim_Fun(structure Inductive=Inductive and Fp=Lfp and
+ Pr=Standard_Prod and Su=Standard_Sum);
+
+structure Indrule = Indrule_Fun (structure Inductive=Inductive and
+ Pr=Standard_Prod and Intr_elim=Intr_elim);
+
+open Intr_elim Indrule
+end;
+
+
+structure Ind = Add_inductive_def_Fun
+ (structure Fp=Lfp and Pr=Standard_Prod and Su=Standard_Sum);
+
+
+signature INDUCTIVE_STRING =
+ sig
+ val thy_name : string (*name of the new theory*)
+ val rec_doms : (string*string) list (*recursion terms and their domains*)
+ val sintrs : string list (*desired introduction rules*)
+ end;
+
+
+(*For upwards compatibility: can be called directly from ML*)
+functor Inductive_Fun
+ (Inductive: sig include INDUCTIVE_STRING INDUCTIVE_ARG end)
+ : sig include INTR_ELIM INDRULE end =
+Ind_section_Fun
+ (open Inductive Ind_Syntax
+ val sign = sign_of thy;
+ val rec_tms = map (readtm sign iT o #1) rec_doms
+ and domts = map (readtm sign iT o #2) rec_doms
+ and intr_tms = map (readtm sign propT) sintrs;
+ val thy = thy |> Ind.add_fp_def_i(rec_tms, domts, intr_tms)
+ |> add_thyname thy_name);
+
+
+
+local open Ind_Syntax
+in
+structure Gfp =
+ struct
+ val oper = Const("gfp", [iT,iT-->iT]--->iT)
+ val bnd_mono = Const("bnd_mono", [iT,iT-->iT]--->oT)
+ val bnd_monoI = bnd_monoI
+ val subs = def_gfp_subset
+ val Tarski = def_gfp_Tarski
+ val induct = def_Collect_coinduct
+ end;
+
+structure Quine_Prod =
+ struct
+ val sigma = Const("QSigma", [iT, iT-->iT]--->iT)
+ val pair = Const("QPair", [iT,iT]--->iT)
+ val split_const = Const("qsplit", [[iT,iT]--->iT, iT]--->iT)
+ val fsplit_const = Const("qfsplit", [[iT,iT]--->oT, iT]--->oT)
+ val pair_iff = QPair_iff
+ val split_eq = qsplit
+ val fsplitI = qfsplitI
+ val fsplitD = qfsplitD
+ val fsplitE = qfsplitE
+ end;
+
+structure Quine_Sum =
+ struct
+ val sum = Const("op <+>", [iT,iT]--->iT)
+ val inl = Const("QInl", iT-->iT)
+ val inr = Const("QInr", iT-->iT)
+ val elim = Const("qcase", [iT-->iT, iT-->iT, iT]--->iT)
+ val case_inl = qcase_QInl
+ val case_inr = qcase_QInr
+ val inl_iff = QInl_iff
+ val inr_iff = QInr_iff
+ val distinct = QInl_QInr_iff
+ val distinct' = QInr_QInl_iff
+ end;
+end;
+
+
+signature COINDRULE =
+ sig
+ val coinduct : thm
+ end;
+
+
+functor CoInd_section_Fun
+ (Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end)
+ : sig include INTR_ELIM COINDRULE end =
+struct
+structure Intr_elim =
+ Intr_elim_Fun(structure Inductive=Inductive and Fp=Gfp and
+ Pr=Quine_Prod and Su=Quine_Sum);
+
+open Intr_elim
+val coinduct = raw_induct
+end;
+
+
+structure CoInd =
+ Add_inductive_def_Fun(structure Fp=Gfp and Pr=Quine_Prod and Su=Quine_Sum);
+
+
+(*For upwards compatibility: can be called directly from ML*)
+functor CoInductive_Fun
+ (Inductive: sig include INDUCTIVE_STRING INDUCTIVE_ARG end)
+ : sig include INTR_ELIM COINDRULE end =
+CoInd_section_Fun
+ (open Inductive Ind_Syntax
+ val sign = sign_of thy;
+ val rec_tms = map (readtm sign iT o #1) rec_doms
+ and domts = map (readtm sign iT o #2) rec_doms
+ and intr_tms = map (readtm sign propT) sintrs;
+ val thy = thy |> CoInd.add_fp_def_i(rec_tms, domts, intr_tms)
+ |> add_thyname thy_name);
+
+
+
+(*For installing the theory section. co is either "" or "Co"*)
+fun inductive_decl co =
+ let open ThyParse Ind_Syntax
+ fun mk_intr_name (s,_) = (*the "op" cancels any infix status*)
+ if Syntax.is_identifier s then "op " ^ s else "_"
+ fun mk_params (((((domains: (string*string) list, ipairs),
+ monos), con_defs), type_intrs), type_elims) =
+ let val big_rec_name = space_implode "_"
+ (map (scan_to_id o trim o #1) domains)
+ and srec_tms = mk_list (map #1 domains)
+ and sdoms = mk_list (map #2 domains)
+ and sintrs = mk_big_list (map snd ipairs)
+ val stri_name = big_rec_name ^ "_Intrnl"
+ in
+ (";\n\n\
+ \structure " ^ stri_name ^ " =\n\
+ \ let open Ind_Syntax in\n\
+ \ struct\n\
+ \ val _ = writeln \"" ^ co ^
+ "Inductive definition " ^ big_rec_name ^ "\"\n\
+ \ val rec_tms\t= map (readtm (sign_of thy) iT) "
+ ^ srec_tms ^ "\n\
+ \ and domts\t= map (readtm (sign_of thy) iT) "
+ ^ sdoms ^ "\n\
+ \ and intr_tms\t= map (readtm (sign_of thy) propT)\n"
+ ^ sintrs ^ "\n\
+ \ end\n\
+ \ end;\n\n\
+ \val thy = thy |> " ^ co ^ "Ind.add_fp_def_i \n (" ^
+ stri_name ^ ".rec_tms, " ^
+ stri_name ^ ".domts, " ^
+ stri_name ^ ".intr_tms)"
+ ,
+ "structure " ^ big_rec_name ^ " =\n\
+ \ struct\n\
+ \ structure Result = " ^ co ^ "Ind_section_Fun\n\
+ \ (open " ^ stri_name ^ "\n\
+ \ val thy\t\t= thy\n\
+ \ val monos\t\t= " ^ monos ^ "\n\
+ \ val con_defs\t\t= " ^ con_defs ^ "\n\
+ \ val type_intrs\t= " ^ type_intrs ^ "\n\
+ \ val type_elims\t= " ^ type_elims ^ ");\n\n\
+ \ val " ^ mk_list (map mk_intr_name ipairs) ^ " = Result.intrs;\n\
+ \ open Result\n\
+ \ end\n"
+ )
+ end
+ val domains = "domains" $$-- repeat1 (string --$$ "<=" -- !! string)
+ val ipairs = "intrs" $$-- repeat1 (ident -- !! string)
+ fun optstring s = optional (s $$-- string) "\"[]\"" >> trim
+ in domains -- ipairs -- optstring "monos" -- optstring "con_defs"
+ -- optstring "type_intrs" -- optstring "type_elims"
+ >> mk_params
+ end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Inductive.thy Thu Aug 25 12:09:21 1994 +0200
@@ -0,0 +1,3 @@
+(*Dummy theory to document dependencies *)
+
+Inductive = "indrule"
--- a/src/ZF/Makefile Thu Aug 25 10:41:17 1994 +0200
+++ b/src/ZF/Makefile Thu Aug 25 12:09:21 1994 +0200
@@ -23,9 +23,10 @@
func.thy func.ML AC.thy AC.ML simpdata.thy simpdata.ML\
equalities.thy equalities.ML Bool.thy Bool.ML \
Sum.thy Sum.ML QPair.thy QPair.ML mono.ML Fixedpt.thy Fixedpt.ML \
- ind_syntax.thy ind_syntax.ML add_ind_def.thy add_ind_def.ML \
+ ../Pure/section_utils.ML ind_syntax.thy ind_syntax.ML \
+ add_ind_def.thy add_ind_def.ML \
intr_elim.thy intr_elim.ML indrule.thy indrule.ML \
- inductive.thy inductive.ML \
+ Inductive.thy Inductive.ML \
Perm.thy Perm.ML Rel.thy Rel.ML EquivClass.ML EquivClass.thy \
Trancl.thy Trancl.ML \
WF.thy WF.ML Order.thy Order.ML Ordinal.thy Ordinal.ML \
--- a/src/ZF/Order.thy Thu Aug 25 10:41:17 1994 +0200
+++ b/src/ZF/Order.thy Thu Aug 25 12:09:21 1994 +0200
@@ -14,7 +14,7 @@
ord_iso :: "[i,i,i,i]=>i" (*Order isomorphisms*)
pred :: "[i,i,i]=>i" (*Set of predecessors*)
-rules
+defs
part_ord_def "part_ord(A,r) == irrefl(A,r) & trans[A](r)"
linear_def "linear(A,r) == (ALL x:A. ALL y:A. <x,y>:r | x=y | <y,x>:r)"
--- a/src/ZF/ROOT.ML Thu Aug 25 10:41:17 1994 +0200
+++ b/src/ZF/ROOT.ML Thu Aug 25 12:09:21 1994 +0200
@@ -29,6 +29,7 @@
print_depth 1;
(*Add user sections for inductive/datatype definitions*)
+use "../Pure/section_utils.ML";
use_thy "Datatype";
structure ThySyn = ThySynFun
(val user_keywords = ["inductive", "coinductive", "datatype", "codatatype",
--- a/src/ZF/Zorn.thy Thu Aug 25 10:41:17 1994 +0200
+++ b/src/ZF/Zorn.thy Thu Aug 25 12:09:21 1994 +0200
@@ -11,7 +11,7 @@
Union_in_Pow is proved in ZF.ML
*)
-Zorn = OrderArith + AC + "inductive" +
+Zorn = OrderArith + AC + "Inductive" +
consts
Subset_rel :: "i=>i"
--- a/src/ZF/ex/Acc.thy Thu Aug 25 10:41:17 1994 +0200
+++ b/src/ZF/ex/Acc.thy Thu Aug 25 12:09:21 1994 +0200
@@ -9,10 +9,10 @@
Research Report 92-49, LIP, ENS Lyon. Dec 1992.
*)
-Acc = WF + "inductive" +
+Acc = WF + "Inductive" +
consts
- "acc" :: "i=>i"
+ acc :: "i=>i"
inductive
domains "acc(r)" <= "field(r)"
--- a/src/ZF/ind_syntax.ML Thu Aug 25 10:41:17 1994 +0200
+++ b/src/ZF/ind_syntax.ML Thu Aug 25 12:09:21 1994 +0200
@@ -11,23 +11,12 @@
*)
structure Ind_Syntax =
struct
-(*Make a definition lhs==rhs, checking that vars on lhs contain those of rhs*)
-fun mk_defpair (lhs, rhs) =
- let val Const(name, _) = head_of lhs
- in (name ^ "_def", Logic.mk_equals (lhs, rhs)) end;
-
-fun get_def thy s = get_axiom thy (s^"_def");
-
-fun lookup_const sign a = Symtab.lookup(#const_tab (Sign.rep_sg sign), a);
(** Abstract syntax definitions for FOL and ZF **)
val iT = Type("i",[])
and oT = Type("o",[]);
-fun ap t u = t$u;
-fun app t (u1,u2) = t $ u1 $ u2;
-
(*Given u expecting arguments of types [T1,...,Tn], create term of
type T1*...*Tn => i using split*)
fun ap_split split u [ ] = Abs("null", iT, u)
@@ -62,38 +51,6 @@
val Trueprop = Const("Trueprop",oT-->propT);
fun mk_tprop P = Trueprop $ P;
-(*Read an assumption in the given theory*)
-fun assume_read thy a = assume (read_cterm (sign_of thy) (a,propT));
-
-fun readtm sign T a =
- read_cterm sign (a,T) |> term_of
- handle ERROR => error ("The error above occurred for " ^ a);
-
-(*Skipping initial blanks, find the first identifier*)
-fun scan_to_id s =
- s |> explode |> take_prefix is_blank |> #2 |> Scanner.scan_id |> #1
- handle LEXICAL_ERROR => error ("Expected to find an identifier in " ^ s);
-
-fun is_backslash c = c = "\\";
-
-(*Apply string escapes to a quoted string; see Def of Standard ML, page 3
- Does not handle the \ddd form; no error checking*)
-fun escape [] = []
- | escape cs = (case take_prefix (not o is_backslash) cs of
- (front, []) => front
- | (front, _::"n"::rest) => front @ ("\n" :: escape rest)
- | (front, _::"t"::rest) => front @ ("\t" :: escape rest)
- | (front, _::"^"::c::rest) => front @ (chr(ord(c)-64) :: escape rest)
- | (front, _::"\""::rest) => front @ ("\"" :: escape rest)
- | (front, _::"\\"::rest) => front @ ("\\" :: escape rest)
- | (front, b::c::rest) =>
- if is_blank c (*remove any further blanks and the following \ *)
- then front @ escape (tl (snd (take_prefix is_blank rest)))
- else error ("Unrecognized string escape: " ^ implode(b::c::rest)));
-
-(*Remove the first and last charaters -- presumed to be quotes*)
-val trim = implode o escape o rev o tl o rev o tl o explode;
-
(*simple error-checking in the premises of an inductive definition*)
fun chk_prem rec_hd (Const("op &",_) $ _ $ _) =
error"Premises may not be conjuctive"
@@ -102,10 +59,6 @@
| chk_prem rec_hd t =
deny (Logic.occs(rec_hd,t)) "Recursion term in side formula";
-(*Make distinct individual variables a1, a2, a3, ..., an. *)
-fun mk_frees a [] = []
- | mk_frees a (T::Ts) = Free(a,T) :: mk_frees (bump_string a) Ts;
-
(*Return the conclusion of a rule, of the form t:X*)
fun rule_concl rl =
let val Const("Trueprop",_) $ (Const("op :",_) $ t $ X) =
@@ -124,13 +77,6 @@
(make_elim (equalityD1 RS subsetD RS CollectD2));
-(*From HOL/ex/meson.ML: raises exception if no rules apply -- unlike RL*)
-fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls))
- | tryres (th, []) = raise THM("tryres", 0, [th]);
-
-fun gen_make_elim elim_rls rl =
- standard (tryres (rl, elim_rls @ [revcut_rl]));
-
(** For datatype definitions **)
fun dest_mem (Const("op :",_) $ x $ A) = (x,A)
--- a/src/ZF/intr_elim.ML Thu Aug 25 10:41:17 1994 +0200
+++ b/src/ZF/intr_elim.ML Thu Aug 25 12:09:21 1994 +0200
@@ -1,4 +1,4 @@
-(* Title: ZF/intr-elim.ML
+(* Title: ZF/intr_elim.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
@@ -48,6 +48,10 @@
val rec_names = map (#1 o dest_Const o head_of) rec_tms;
val big_rec_name = space_implode "_" rec_names;
+val _ = deny (big_rec_name mem map ! (stamps_of_thy thy))
+ ("Definition " ^ big_rec_name ^
+ " would clash with the theory of the same name!");
+
(*fetch fp definitions from the theory*)
val big_rec_def::part_rec_defs =
map (get_def thy)
@@ -89,9 +93,10 @@
(*Now 2-3 subgoals: typechecking, the disjunction, perhaps equality.*)
rtac disjIn 2,
REPEAT (ares_tac [refl,exI,conjI] 2),
+ (*Now solve the equations like Tcons(a,f) = Inl(?b4)*)
rewrite_goals_tac con_defs,
- (*Now can solve the trivial equation*)
REPEAT (rtac refl 2),
+ (*Typechecking; this can fail*)
REPEAT (FIRSTGOAL ( dresolve_tac rec_typechecks
ORELSE' eresolve_tac (asm_rl::PartE::SigmaE2::type_elims)
ORELSE' hyp_subst_tac)),