224 |
224 |
225 @{ML [display] "print_depth 50"} |
225 @{ML [display] "print_depth 50"} |
226 |
226 |
227 The antiquotation @{text "@{prop \<dots>}"} constructs terms of propositional type, |
227 The antiquotation @{text "@{prop \<dots>}"} constructs terms of propositional type, |
228 inserting the invisible @{text "Trueprop"}-coercions whenever necessary. |
228 inserting the invisible @{text "Trueprop"}-coercions whenever necessary. |
229 Consider for example |
229 Consider for example the pairs |
230 |
230 |
231 @{ML_response [display] "(@{term \"P x\"}, @{prop \"P x\"})" "(Free (\"P\", \<dots>) $ Free (\"x\", \<dots>), |
231 @{ML_response [display] "(@{term \"P x\"}, @{prop \"P x\"})" "(Free (\"P\", \<dots>) $ Free (\"x\", \<dots>), |
232 Const (\"Trueprop\", \<dots>) $ (Free (\"P\", \<dots>) $ Free (\"x\", \<dots>)))"} |
232 Const (\"Trueprop\", \<dots>) $ (Free (\"P\", \<dots>) $ Free (\"x\", \<dots>)))"} |
233 |
233 |
234 which inserts the coercion in the second component and |
234 where an coercion is inserted in the second component and |
235 |
235 |
236 @{ML_response [display] "(@{term \"P x \<Longrightarrow> Q x\"}, @{prop \"P x \<Longrightarrow> Q x\"})" |
236 @{ML_response [display] "(@{term \"P x \<Longrightarrow> Q x\"}, @{prop \"P x \<Longrightarrow> Q x\"})" |
237 "(Const (\"==>\", \<dots>) $ \<dots> $ \<dots>, Const (\"==>\", \<dots>) $ \<dots> $ \<dots>)"} |
237 "(Const (\"==>\", \<dots>) $ \<dots> $ \<dots>, Const (\"==>\", \<dots>) $ \<dots> $ \<dots>)"} |
238 |
238 |
239 which does not (since it is already constructed using the meta-implication). |
239 where it is not (since it is already constructed using the meta-implication). |
240 |
240 |
241 Types can be constructed using the antiquotation @{text "@{typ \<dots>}"}. For example |
241 Types can be constructed using the antiquotation @{text "@{typ \<dots>}"}. For example |
242 |
242 |
243 @{ML_response_fake [display] "@{typ \"bool \<Rightarrow> nat\"}" "bool \<Rightarrow> nat"} |
243 @{ML_response_fake [display] "@{typ \"bool \<Rightarrow> nat\"}" "bool \<Rightarrow> nat"} |
244 |
244 |
279 fun make_wrong_imp P Q tau = @{prop "\<And>x. P x \<Longrightarrow> Q x"} |
279 fun make_wrong_imp P Q tau = @{prop "\<And>x. P x \<Longrightarrow> Q x"} |
280 *} |
280 *} |
281 |
281 |
282 text {* |
282 text {* |
283 To see this apply @{text "@{term S}"}, @{text "@{term T}"} and @{text "@{typ nat}"} |
283 To see this apply @{text "@{term S}"}, @{text "@{term T}"} and @{text "@{typ nat}"} |
284 to both functions: |
284 to both functions. With @{ML make_imp} we obtain the correct term involving |
|
285 @{term "S"}, @{text "T"} and @{text "@{typ nat}"} |
285 |
286 |
286 @{ML_response [display] "make_imp @{term S} @{term T} @{typ nat}" |
287 @{ML_response [display] "make_imp @{term S} @{term T} @{typ nat}" |
287 "Const \<dots> $ |
288 "Const \<dots> $ |
288 Abs (\"x\", Type (\"nat\",[]), |
289 Abs (\"x\", Type (\"nat\",[]), |
289 Const \<dots> $ (Free (\"S\",\<dots>) $ \<dots>) $ |
290 Const \<dots> $ (Free (\"S\",\<dots>) $ \<dots>) $ |
290 (Free (\"T\",\<dots>) $ \<dots>))"} |
291 (Free (\"T\",\<dots>) $ \<dots>))"} |
|
292 |
|
293 With @{ML make_wrong_imp} we obtain an incorrect term involving the @{term "P"} |
|
294 and @{text "Q"} from the antiquotation. |
|
295 |
291 @{ML_response [display] "make_wrong_imp @{term S} @{term T} @{typ nat}" |
296 @{ML_response [display] "make_wrong_imp @{term S} @{term T} @{typ nat}" |
292 "Const \<dots> $ |
297 "Const \<dots> $ |
293 Abs (\"x\", \<dots>, |
298 Abs (\"x\", \<dots>, |
294 Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $ |
299 Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $ |
295 (Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"} |
300 (Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"} |
296 |
301 |
297 As can be seen, in the first case the arguments are correctly used, while the |
302 One tricky point in constructing terms by hand is to obtain the fully |
298 second generates a term involving the @{term "P"} and @{text "Q"} from the |
303 qualified name for constants. For example the names for @{text "zero"} and |
299 antiquotation. |
304 @{text "+"} are more complex than one first expects, namely |
300 |
305 |
301 One tricky point in constructing terms by hand is to obtain the |
|
302 fully qualified name for constants. For example the names for @{text "zero"} and |
|
303 @{text "+"} are more complex than one first expects, namely |
|
304 |
306 |
305 \begin{center} |
307 \begin{center} |
306 @{text "HOL.zero_class.zero"} and @{text "HOL.plus_class.plus"}. |
308 @{text "HOL.zero_class.zero"} and @{text "HOL.plus_class.plus"}. |
307 \end{center} |
309 \end{center} |
308 |
310 |
309 The extra prefixes @{text zero_class} and @{text plus_class} are present because |
311 The extra prefixes @{text zero_class} and @{text plus_class} are present |
310 these constants are defined within type classes; the prefix @{text "HOL"} indicates in |
312 because these constants are defined within type classes; the prefix @{text |
311 which theory they are defined. Guessing such internal names can sometimes be quite hard. |
313 "HOL"} indicates in which theory they are defined. Guessing such internal |
312 Therefore Isabelle provides the antiquotation @{text "@{const_name \<dots>}"} which does the |
314 names can sometimes be quite hard. Therefore Isabelle provides the |
313 expansion automatically, for example: |
315 antiquotation @{text "@{const_name \<dots>}"} which does the expansion |
|
316 automatically, for example: |
314 |
317 |
315 @{ML_response_fake [display] "@{const_name \"Nil\"}" "List.list.Nil"} |
318 @{ML_response_fake [display] "@{const_name \"Nil\"}" "List.list.Nil"} |
316 |
319 |
317 (FIXME: Is it useful to explain @{text "@{const_syntax}"}?) |
320 (FIXME: Is it useful to explain @{text "@{const_syntax}"}?) |
318 |
321 |