doc-src/Pure/theory-extensions

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