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