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