# HG changeset patch # User nipkow # Date 925211152 -7200 # Node ID bb2c4ddd8e5e1182d13585edb13460e2d35d9044 # Parent 13410ecfce0b18d914d7727298f481a564c2757e Old stuff. diff -r 13410ecfce0b -r bb2c4ddd8e5e doc-src/Pure/theory-extensions --- a/doc-src/Pure/theory-extensions Tue Apr 27 10:52:25 1999 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,104 +0,0 @@ -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 pleasure, 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. - -=============================================================================