259 |> Variable.variant_frees ctxt [pred] |
259 |> Variable.variant_frees ctxt [pred] |
260 |> map Free |
260 |> map Free |
261 |> (curry list_comb) pred *} |
261 |> (curry list_comb) pred *} |
262 |
262 |
263 text {* |
263 text {* |
264 This code extracts the argument types of the given |
264 This code extracts the argument types of a given |
265 predicate and then generate for each type a distinct variable; finally it |
265 predicate and then generates for each argument type a distinct variable; finally it |
266 applies the generated variables to the predicate. For example |
266 applies the generated variables to the predicate. For example |
267 |
267 |
268 @{ML_response_fake [display,gray] |
268 @{ML_response_fake [display,gray] |
269 "apply_fresh_args @{term \"P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool\"} @{context} |
269 "apply_fresh_args @{term \"P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool\"} @{context} |
270 |> Syntax.string_of_term @{context} |
270 |> Syntax.string_of_term @{context} |
271 |> warning" |
271 |> warning" |
272 "P z za zb"} |
272 "P z za zb"} |
273 |
273 |
274 You can read this off this behaviour from how @{ML apply_fresh_args} is |
274 You can read off this behaviour from how @{ML apply_fresh_args} is |
275 coded: in Line 2, the function @{ML fastype_of} calculates the type of the |
275 coded: in Line 2, the function @{ML fastype_of} calculates the type of the |
276 predicate; in Line 3, @{ML binder_types} produces the list of argument |
276 predicate; @{ML binder_types} in the next line produces the list of argument |
277 types (in the case above the list @{text "[nat, int, unit]"}); Line 4 pairs up each |
277 types (in the case above the list @{text "[nat, int, unit]"}); Line 4 |
278 type with the string @{text "z"}; the |
278 pairs up each type with the string @{text "z"}; the |
279 function @{ML variant_frees in Variable} generates for each @{text "z"} a |
279 function @{ML variant_frees in Variable} generates for each @{text "z"} a |
280 unique name avoiding @{text pred}; the list of name-type pairs is turned |
280 unique name avoiding the given @{text pred}; the list of name-type pairs is turned |
281 into a list of variable terms in Line 6, which in the last line are applied |
281 into a list of variable terms in Line 6, which in the last line is applied |
282 by the function @{ML list_comb} to the predicate. We have to use the |
282 by the function @{ML list_comb} to the predicate. We have to use the |
283 function @{ML curry}, because @{ML list_comb} expects the predicate and the |
283 function @{ML curry}, because @{ML list_comb} expects the predicate and the |
284 argument list as a pair. |
284 variables list as a pair. |
285 |
285 |
286 The combinator @{ML "#>"} is the reverse function composition. It can be |
286 The combinator @{ML "#>"} is the reverse function composition. It can be |
287 used to define the following function |
287 used to define the following function |
288 *} |
288 *} |
289 |
289 |
441 map #1 simps |
441 map #1 simps |
442 end*} |
442 end*} |
443 |
443 |
444 text {* |
444 text {* |
445 The function @{ML dest_ss in MetaSimplifier} returns a record containing all |
445 The function @{ML dest_ss in MetaSimplifier} returns a record containing all |
446 information stored in the simpset. We are only interested in the You can now use @{ML get_thm_names_from_ss} to obtain all names of theorems stored |
446 information stored in the simpset. We are only interested in the names of the |
447 in the current simpset. This simpset can be referred to using the antiquotation |
447 simp-rules. So now you can feed in the current simpset into this function. |
448 @{text "@{simpset}"}. |
448 The simpset can be referred to using the antiquotation @{text "@{simpset}"}. |
449 |
449 |
450 @{ML_response_fake [display,gray] |
450 @{ML_response_fake [display,gray] |
451 "get_thm_names_from_ss @{simpset}" |
451 "get_thm_names_from_ss @{simpset}" |
452 "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"} |
452 "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"} |
453 |
453 |
594 "Const \<dots> $ |
594 "Const \<dots> $ |
595 Abs (\"x\", \<dots>, |
595 Abs (\"x\", \<dots>, |
596 Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $ |
596 Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $ |
597 (Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"} |
597 (Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"} |
598 |
598 |
599 (FIXME: handy functions for constructing terms @{ML list_comb}, @{ML lambda}) |
599 (FIXME: handy functions for constructing terms: @{ML list_comb}, @{ML lambda}) |
600 |
600 |
601 |
601 |
602 Although types of terms can often be inferred, there are many |
602 Although types of terms can often be inferred, there are many |
603 situations where you need to construct types manually, especially |
603 situations where you need to construct types manually, especially |
604 when defining constants. For example the function returning a function |
604 when defining constants. For example the function returning a function |