# HG changeset patch # User lcp # Date 777809361 -7200 # Node ID efc648d29dd0a720d61c9a508fcf60017914a48d # Parent 776b5ba748d8a97e28e6773a694008f5b45757c6 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 diff -r 776b5ba748d8 -r efc648d29dd0 src/ZF/Datatype.thy --- 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 diff -r 776b5ba748d8 -r efc648d29dd0 src/ZF/Finite.thy --- 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) diff -r 776b5ba748d8 -r efc648d29dd0 src/ZF/Inductive.ML --- /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; diff -r 776b5ba748d8 -r efc648d29dd0 src/ZF/Inductive.thy --- /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" diff -r 776b5ba748d8 -r efc648d29dd0 src/ZF/Makefile --- 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 \ diff -r 776b5ba748d8 -r efc648d29dd0 src/ZF/Order.thy --- 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. :r | x=y | :r)" diff -r 776b5ba748d8 -r efc648d29dd0 src/ZF/ROOT.ML --- 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", diff -r 776b5ba748d8 -r efc648d29dd0 src/ZF/Zorn.thy --- 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" diff -r 776b5ba748d8 -r efc648d29dd0 src/ZF/ex/Acc.thy --- 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)" diff -r 776b5ba748d8 -r efc648d29dd0 src/ZF/ind_syntax.ML --- 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) diff -r 776b5ba748d8 -r efc648d29dd0 src/ZF/intr_elim.ML --- 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)),