doc-src/Pure/theory-extensions

author | nipkow |

Mon, 11 Jul 1994 20:03:40 +0200 | |

changeset 462 | f4e9e7aacda7 |

child 509 | 8a2bcbd8479d |

permissions | -rw-r--r-- |

Initial revision

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. =============================================================================