71 *} |
71 *} |
72 |
72 |
73 section {* Setups (TBD) *} |
73 section {* Setups (TBD) *} |
74 |
74 |
75 text {* |
75 text {* |
76 In the previous section we used \isacommand{setup}, for example, in |
76 In the previous section we used \isacommand{setup} in order, for example, |
77 order to make a theorem attribute known to Isabelle. What happens |
77 to make a theorem attribute known to Isabelle or register a theorem under |
78 behind the scenes is that \isacommand{setup} expects a function of |
78 a name. What happens behind the scenes is that \isacommand{setup} expects a |
79 type @{ML_type "theory -> theory"}: the input theory is the current |
79 function of type @{ML_type "theory -> theory"}: the input theory is the current |
80 theory and the output the theory where the theory attribute has been |
80 theory and the output the theory where the theory attribute or theorem has been |
81 stored. |
81 stored. |
82 |
82 |
83 This is a fundamental principle in Isabelle. A similar situation arises |
83 This is a fundamental principle in Isabelle. A similar situation arises |
84 with declaring constants. The function that declares a |
84 with declaring constants. The function that declares a |
85 constant on the ML-level is @{ML_ind declare_const in Sign}. |
85 constant on the ML-level is @{ML_ind declare_const in Sign}. |
86 However, if you simply write\footnote{Recall that ML-code needs to be |
86 However, note that if you simply write\footnote{Recall that ML-code needs to be |
87 enclosed in \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}.} |
87 enclosed in \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}.} |
88 *} |
88 *} |
89 |
89 |
90 ML{*Sign.declare_const @{context} |
90 ML{*let |
91 ((@{binding "BAR"}, @{typ "nat"}), NoSyn) @{theory} *} |
91 val thy = @{theory} |
|
92 val bar_const = ((@{binding "BAR"}, @{typ "nat"}), NoSyn) |
|
93 in |
|
94 Sign.declare_const @{context} bar_const thy |
|
95 end*} |
92 |
96 |
93 text {* |
97 text {* |
94 with the intention of declaring the constant @{text "BAR"} with type @{typ nat} |
98 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 |
99 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} |
100 query the constant on the Isabelle level using the command \isacommand{term} |
97 |
101 |
98 \begin{isabelle} |
102 \begin{isabelle} |
99 \isacommand{term}~@{text [quotes] "BAR"}\\ |
103 \isacommand{term}~@{text BAR}\\ |
100 @{text "> \"BAR\" :: \"'a\""} |
104 @{text "> \"BAR\" :: \"'a\""} |
101 \end{isabelle} |
105 \end{isabelle} |
102 |
106 |
103 you can see that you do not obtain a constant of type @{typ nat}, but a free |
107 you can see that you do \emph{not} obtain a constant of type @{typ nat}, but a free |
104 variable (printed in blue) of polymorphic type. The problem is that the |
108 variable (printed in blue) of polymorphic type. The problem is that the |
105 ML-expression above did not ``register'' the declaration with the current theory. |
109 ML-expression above did not ``register'' the declaration with the current theory. |
106 This is what the command \isacommand{setup} is for. The constant is properly |
110 This is what the command \isacommand{setup} is for. The constant is properly |
107 declared with |
111 declared with |
108 *} |
112 *} |
109 |
113 |
110 setup %gray {* Sign.declare_const @{context} |
114 setup %gray {* let |
111 ((@{binding "BAR"}, @{typ "nat"}), NoSyn) #> snd *} |
115 val bar_const = ((@{binding "BAR"}, @{typ "nat"}), NoSyn) |
|
116 in |
|
117 Sign.declare_const @{context} bar_const #> snd |
|
118 end *} |
112 |
119 |
113 text {* |
120 text {* |
114 Now |
121 where the declaration is actually applied to the theory and |
115 |
122 |
116 \begin{isabelle} |
123 \begin{isabelle} |
117 \isacommand{term}~@{text [quotes] "BAR"}\\ |
124 \isacommand{term}~@{text [quotes] "BAR"}\\ |
118 @{text "> \"BAR\" :: \"nat\""} |
125 @{text "> \"BAR\" :: \"nat\""} |
119 \end{isabelle} |
126 \end{isabelle} |
120 |
127 |
121 returns a (black) constant with the type @{typ nat}, as expected. |
128 returns a (black) constant with the type @{typ nat}, as expected. |
|
129 |
|
130 In a sense, \isacommand{setup} can be seen as a transaction that takes the |
|
131 current theory, applies an operation, and produces a new current theory. This |
|
132 means that we have to be careful to apply operations always to the current |
|
133 theory, not to a \emph{stale} one. The code below produces |
|
134 |
122 |
135 |
123 A similar command is \isacommand{local\_setup}, which expects a function |
136 A similar command is \isacommand{local\_setup}, which expects a function |
124 of type @{ML_type "local_theory -> local_theory"}. Later on we will also |
137 of type @{ML_type "local_theory -> local_theory"}. Later on we will also |
125 use the commands \isacommand{method\_setup} for installing methods in the |
138 use the commands \isacommand{method\_setup} for installing methods in the |
126 current theory and \isacommand{simproc\_setup} for adding new simprocs to |
139 current theory and \isacommand{simproc\_setup} for adding new simprocs to |