180 *} |
180 *} |
181 |
181 |
182 section {* Terms and Types *} |
182 section {* Terms and Types *} |
183 |
183 |
184 text {* |
184 text {* |
185 One way to construct terms of Isabelle on the ML-level is by using the antiquotation |
185 One way to construct terms of Isabelle on the ML level is by using the antiquotation |
186 @{text "@{term \<dots>}"}: |
186 \mbox{@{text "@{term \<dots>}"}}: |
187 *} |
187 *} |
188 |
188 |
189 ML {* @{term "(a::nat) + b = c"} *} |
189 ML {* @{term "(a::nat) + b = c"} *} |
190 |
190 |
191 text {* |
191 text {* |
192 This will show the term @{term "(a::nat) + b = c"}, but printed out using the internal |
192 This will show the term @{term "(a::nat) + b = c"}, but printed out using the internal |
193 representation of this term. This internal representation corresponds to the |
193 representation of this term. This internal representation corresponds to the |
194 datatype @{ML_text "term"}. |
194 datatype @{ML_text "term"}. |
195 |
195 |
196 The internal representation of terms uses the usual de-Bruijn index mechanism where bound |
196 The internal representation of terms uses the usual de Bruijn index mechanism where bound |
197 variables are represented by the constructor @{ML Bound}. The index in @{ML Bound} refers to |
197 variables are represented by the constructor @{ML Bound}. The index in @{ML Bound} refers to |
198 the number of Abstractions (@{ML Abs}) we have to skip until we hit the @{ML Abs} that |
198 the number of Abstractions (@{ML Abs}) we have to skip until we hit the @{ML Abs} that |
199 binds the corresponding variable. However, in Isabelle the names of bound variables are |
199 binds the corresponding variable. However, in Isabelle the names of bound variables are |
200 kept at abstractions for printing purposes, and so should be treated only as comments. |
200 kept at abstractions for printing purposes, and so should be treated only as comments. |
201 |
201 |
499 constructs sequences explicitly, but uses the predefined tactic |
499 constructs sequences explicitly, but uses the predefined tactic |
500 combinators (tacticals) instead (see @{ML_file "Pure/tctical.ML"}). |
500 combinators (tacticals) instead (see @{ML_file "Pure/tctical.ML"}). |
501 (FIXME: Pointer to the old reference manual) |
501 (FIXME: Pointer to the old reference manual) |
502 \end{readmore} |
502 \end{readmore} |
503 |
503 |
504 While tatics can operate on the subgoals (the @{text "A\<^isub>i"} above), they |
504 While tactics can operate on the subgoals (the @{text "A\<^isub>i"} above), they |
505 are expected to leave the conclusion @{term C} intact, with the |
505 are expected to leave the conclusion @{term C} intact, with the |
506 exception of possibly instantiating schematic variables. |
506 exception of possibly instantiating schematic variables. |
507 |
507 |
508 To see how tactics work, let us transcribe a simple @{text apply}-style |
508 To see how tactics work, let us transcribe a simple @{text apply}-style |
509 proof from the tutorial \cite{isa-tutorial} into ML: |
509 proof from the tutorial \cite{isa-tutorial} into ML: |