diff -r 170de0c52a9b -r f4e9e7aacda7 doc-src/Pure/theory-extensions --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Pure/theory-extensions Mon Jul 11 20:03:40 1994 +0200 @@ -0,0 +1,104 @@ +The new Internal Interface for Theory Extension +=============================================== + +MMW 06-Jun-1994 + + +In former versions of Isabelle, the interface for theory extension was +provided by extend_theory. This had many deficiencies and has been removed in +Isabelle94/2. + +Instead of one monolithic function, there is now a host of small functions of +the form: + + add_XXX: ... -> theory -> theory + +These provide an extension mechanism which is: + + - incremental (but non-destructive): + + An extend operation may now involve many functions of the add_XXX kind. + These act in a purely functional manner. + + - nameless: + + One no longer needs to invent new theory names for intermediate theories. + There's now a notion of _draft_theories_ that behave like ordinary ones + in many cases (main exceptions: extensions of drafts are not related (wrt + subthy); merges of drafts with unrelated theories are impossible). A + draft is "closed" by add_thyname. + + - extendable: + + Package writers simply have to provide add_XXX like functions, which are + built using a basic set provided by Pure Isabelle. + + +Here follows a sample interactive session using the new functions: + + > add_consts + # [("nand", "[o, o] => o", NoSyn), ("#", "[o, o] => o", Infixl 30)] + # FOL.thy; + Building new grammar... + val it = {Pure, IFOL, FOL, #} : theory + > add_axioms + # [("nand_def", "nand(P, Q) == ~(P & Q)"), ("xor_def", "P # Q == P & ~Q | ~P & Q")] + # it; + val it = {Pure, IFOL, FOL, #} : theory + > add_thyname "Gate" it; + val it = {Pure, IFOL, FOL, Gate} : theory + +Note that theories and theorems with a "#" draft stamp are not supposed to +persist. Typically, there is a final add_thyname somewhere with the "real" +theory name as supplied by the user. + + +Appendix A: Basic theory extension functions +-------------------------------------------- + + val add_classes: (class list * class * class list) list -> theory -> theory + val add_defsort: sort -> theory -> theory + val add_types: (string * int * mixfix) list -> theory -> theory + val add_tyabbrs: (string * string list * string * mixfix) list + -> theory -> theory + val add_tyabbrs_i: (string * string list * typ * mixfix) list + -> theory -> theory + val add_arities: (string * sort list * sort) list -> theory -> theory + val add_consts: (string * string * mixfix) list -> theory -> theory + val add_consts_i: (string * typ * mixfix) list -> theory -> theory + val add_syntax: (string * string * mixfix) list -> theory -> theory + val add_syntax_i: (string * typ * mixfix) list -> theory -> theory + val add_trfuns: + (string * (ast list -> ast)) list * + (string * (term list -> term)) list * + (string * (term list -> term)) list * + (string * (ast list -> ast)) list -> theory -> theory + val add_trrules: xrule list -> theory -> theory + val add_axioms: (string * string) list -> theory -> theory + val add_axioms_i: (string * term) list -> theory -> theory + val add_thyname: string -> theory -> theory + + +Appendix B: The |> operator +--------------------------- + +Isabelle now provides an ML infix operator for reverse function application: + + infix |>; + fun (x |> f) = f x; + +Using this, theory extension really becomes a plasure, e.g.: + + FOL.thy + |> add_consts + [("nand", "[o, o] => o", NoSyn), + ("#", "[o, o] => o", Infixl 30)] + |> add_axioms + [("nand_def", "nand(P, Q) == ~(P & Q)"), + ("xor_def", "P # Q == P & ~Q | ~P & Q")] + |> add_thyname "Gate"; + +For a real-world example simply reset delete_tmpfiles, use_thy your favourite +theory definition file and inspect the generated .XXX.thy.ML file. + +=============================================================================