doc-src/Pure/theory-extensions
changeset 462 f4e9e7aacda7
child 509 8a2bcbd8479d
equal deleted inserted replaced
461:170de0c52a9b 462:f4e9e7aacda7
       
     1 The new Internal Interface for Theory Extension
       
     2 ===============================================
       
     3 
       
     4 MMW 06-Jun-1994
       
     5 
       
     6 
       
     7 In former versions of Isabelle, the interface for theory extension was
       
     8 provided by extend_theory. This had many deficiencies and has been removed in
       
     9 Isabelle94/2.
       
    10 
       
    11 Instead of one monolithic function, there is now a host of small functions of
       
    12 the form:
       
    13 
       
    14   add_XXX: ... -> theory -> theory
       
    15 
       
    16 These provide an extension mechanism which is:
       
    17 
       
    18   - incremental (but non-destructive):
       
    19 
       
    20     An extend operation may now involve many functions of the add_XXX kind.
       
    21     These act in a purely functional manner.
       
    22 
       
    23   - nameless:
       
    24 
       
    25     One no longer needs to invent new theory names for intermediate theories.
       
    26     There's now a notion of _draft_theories_ that behave like ordinary ones
       
    27     in many cases (main exceptions: extensions of drafts are not related (wrt
       
    28     subthy); merges of drafts with unrelated theories are impossible). A
       
    29     draft is "closed" by add_thyname.
       
    30 
       
    31   - extendable:
       
    32 
       
    33     Package writers simply have to provide add_XXX like functions, which are
       
    34     built using a basic set provided by Pure Isabelle.
       
    35 
       
    36 
       
    37 Here follows a sample interactive session using the new functions:
       
    38 
       
    39   > add_consts
       
    40   # [("nand", "[o, o] => o", NoSyn), ("#", "[o, o] => o", Infixl 30)]
       
    41   # FOL.thy;
       
    42   Building new grammar...
       
    43   val it = {Pure, IFOL, FOL, #} : theory   
       
    44   > add_axioms
       
    45   # [("nand_def", "nand(P, Q) == ~(P & Q)"), ("xor_def", "P # Q == P & ~Q | ~P & Q")]
       
    46   # it;
       
    47   val it = {Pure, IFOL, FOL, #} : theory   
       
    48   > add_thyname "Gate" it;
       
    49   val it = {Pure, IFOL, FOL, Gate} : theory   
       
    50 
       
    51 Note that theories and theorems with a "#" draft stamp are not supposed to
       
    52 persist. Typically, there is a final add_thyname somewhere with the "real"
       
    53 theory name as supplied by the user.
       
    54 
       
    55 
       
    56 Appendix A: Basic theory extension functions
       
    57 --------------------------------------------
       
    58 
       
    59    val add_classes: (class list * class * class list) list -> theory -> theory
       
    60    val add_defsort: sort -> theory -> theory
       
    61    val add_types: (string * int * mixfix) list -> theory -> theory
       
    62    val add_tyabbrs: (string * string list * string * mixfix) list
       
    63      -> theory -> theory
       
    64    val add_tyabbrs_i: (string * string list * typ * mixfix) list
       
    65      -> theory -> theory
       
    66    val add_arities: (string * sort list * sort) list -> theory -> theory
       
    67    val add_consts: (string * string * mixfix) list -> theory -> theory
       
    68    val add_consts_i: (string * typ * mixfix) list -> theory -> theory
       
    69    val add_syntax: (string * string * mixfix) list -> theory -> theory
       
    70    val add_syntax_i: (string * typ * mixfix) list -> theory -> theory
       
    71    val add_trfuns:
       
    72      (string * (ast list -> ast)) list *
       
    73      (string * (term list -> term)) list *
       
    74      (string * (term list -> term)) list *
       
    75      (string * (ast list -> ast)) list -> theory -> theory
       
    76    val add_trrules: xrule list -> theory -> theory
       
    77    val add_axioms: (string * string) list -> theory -> theory
       
    78    val add_axioms_i: (string * term) list -> theory -> theory
       
    79    val add_thyname: string -> theory -> theory
       
    80 
       
    81 
       
    82 Appendix B: The |> operator
       
    83 ---------------------------
       
    84 
       
    85 Isabelle now provides an ML infix operator for reverse function application:
       
    86 
       
    87   infix |>;
       
    88   fun (x |> f) = f x;
       
    89 
       
    90 Using this, theory extension really becomes a plasure, e.g.:
       
    91 
       
    92   FOL.thy 
       
    93   |> add_consts
       
    94       [("nand", "[o, o] => o", NoSyn),
       
    95        ("#", "[o, o] => o", Infixl 30)]
       
    96   |> add_axioms
       
    97       [("nand_def", "nand(P, Q) == ~(P & Q)"),
       
    98        ("xor_def", "P # Q == P & ~Q | ~P & Q")]
       
    99   |> add_thyname "Gate";
       
   100 
       
   101 For a real-world example simply reset delete_tmpfiles, use_thy your favourite
       
   102 theory definition file and inspect the generated .XXX.thy.ML file.
       
   103 
       
   104 =============================================================================