462

1 
The new Internal Interface for Theory Extension


2 
===============================================


3 


4 
MMW 06Jun1994


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 nondestructive):


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 realworld example simply reset delete_tmpfiles, use_thy your favourite


102 
theory definition file and inspect the generated .XXX.thy.ML file.


103 


104 
=============================================================================
