71 *} |
71 *} |
72 |
72 |
73 section {* Setups (TBD) *} |
73 section {* Setups (TBD) *} |
74 |
74 |
75 text {* |
75 text {* |
76 @{ML Sign.declare_const} |
76 In the previous section we used \isacommand{setup}, for example, in |
77 |
77 order to make a theorem attribute known to Isabelle. What happens |
78 In the previous section we used \isacommand{setup} in order to make |
78 behind the scenes is that \isacommand{setup} expects a function of |
79 a theorem attribute known to Isabelle. What happens behind the scenes |
79 type @{ML_type "theory -> theory"}: the input theory is the current |
80 is that \isacommand{setup} expects a function of type |
80 theory and the output the theory where the theory attribute has been |
81 @{ML_type "theory -> theory"}: the input theory is the current theory and the |
81 stored. |
82 output the theory where the theory attribute has been stored. |
82 |
83 |
83 This is a fundamental principle in Isabelle. A similar situation arises |
84 This is a fundamental principle in Isabelle. A similar situation occurs |
84 with declaring constants. The function that declares a |
85 for example with declaring constants. The function that declares a |
85 constant on the ML-level is @{ML_ind declare_const in Sign}. |
86 constant on the ML-level is @{ML_ind add_consts_i in Sign}. |
86 However, if you simply write\footnote{Recall that ML-code needs to be |
87 If you write\footnote{Recall that ML-code needs to be |
|
88 enclosed in \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}.} |
87 enclosed in \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}.} |
89 *} |
88 *} |
90 |
89 |
91 ML{*Sign.add_consts_i [(@{binding "BAR"}, @{typ "nat"}, NoSyn)] @{theory} *} |
90 ML{*Sign.declare_const @{context} |
92 |
91 ((@{binding "BAR"}, @{typ "nat"}), NoSyn) @{theory} *} |
93 text {* |
92 |
94 for declaring the constant @{text "BAR"} with type @{typ nat} and |
93 text {* |
95 run the code, then you indeed obtain a theory as result. But if you |
94 with the intention of declaring the constant @{text "BAR"} with type @{typ nat} |
|
95 and run the code, then indeed you obtain a theory as result. But if you |
96 query the constant on the Isabelle level using the command \isacommand{term} |
96 query the constant on the Isabelle level using the command \isacommand{term} |
97 |
97 |
98 \begin{isabelle} |
98 \begin{isabelle} |
99 \isacommand{term}~@{text [quotes] "BAR"}\\ |
99 \isacommand{term}~@{text [quotes] "BAR"}\\ |
100 @{text "> \"BAR\" :: \"'a\""} |
100 @{text "> \"BAR\" :: \"'a\""} |
101 \end{isabelle} |
101 \end{isabelle} |
102 |
102 |
103 you do not obtain a constant of type @{typ nat}, but a free variable (printed in |
103 you can see that you do not obtain a constant of type @{typ nat}, but a free |
104 blue) of polymorphic type. The problem is that the ML-expression above did |
104 variable (printed in blue) of polymorphic type. The problem is that the |
105 not register the declaration with the current theory. This is what the command |
105 ML-expression above did not ``register'' the declaration with the current theory. |
106 \isacommand{setup} is for. The constant is properly declared with |
106 This is what the command \isacommand{setup} is for. The constant is properly |
107 *} |
107 declared with |
108 |
108 *} |
109 setup %gray {* Sign.add_consts_i [(@{binding "BAR"}, @{typ "nat"}, NoSyn)] *} |
109 |
|
110 setup %gray {* Sign.declare_const @{context} |
|
111 ((@{binding "BAR"}, @{typ "nat"}), NoSyn) #> snd *} |
110 |
112 |
111 text {* |
113 text {* |
112 Now |
114 Now |
113 |
115 |
114 \begin{isabelle} |
116 \begin{isabelle} |
115 \isacommand{term}~@{text [quotes] "BAR"}\\ |
117 \isacommand{term}~@{text [quotes] "BAR"}\\ |
116 @{text "> \"BAR\" :: \"nat\""} |
118 @{text "> \"BAR\" :: \"nat\""} |
117 \end{isabelle} |
119 \end{isabelle} |
118 |
120 |
119 returns a (black) constant with the type @{typ nat}. |
121 returns a (black) constant with the type @{typ nat}, as expected. |
120 |
122 |
121 A similar command is \isacommand{local\_setup}, which expects a function |
123 A similar command is \isacommand{local\_setup}, which expects a function |
122 of type @{ML_type "local_theory -> local_theory"}. Later on we will also |
124 of type @{ML_type "local_theory -> local_theory"}. Later on we will also |
123 use the commands \isacommand{method\_setup} for installing methods in the |
125 use the commands \isacommand{method\_setup} for installing methods in the |
124 current theory and \isacommand{simproc\_setup} for adding new simprocs to |
126 current theory and \isacommand{simproc\_setup} for adding new simprocs to |