equal
deleted
inserted
replaced
342 function @{ML variant_frees in Variable} generates for each @{text "z"} a |
342 function @{ML variant_frees in Variable} generates for each @{text "z"} a |
343 unique name avoiding the given @{text f}; the list of name-type pairs is turned |
343 unique name avoiding the given @{text f}; the list of name-type pairs is turned |
344 into a list of variable terms in Line 6, which in the last line is applied |
344 into a list of variable terms in Line 6, which in the last line is applied |
345 by the function @{ML list_comb} to the function. In this last step we have to |
345 by the function @{ML list_comb} to the function. In this last step we have to |
346 use the function @{ML curry}, because @{ML list_comb} expects the function and the |
346 use the function @{ML curry}, because @{ML list_comb} expects the function and the |
347 variables list as a pair. |
347 variables list as a pair. This kind of functions is often needed when |
|
348 constructing terms and the infrastructure helps tremendously to avoid |
|
349 any name clashes. Consider for example: |
|
350 |
|
351 @{ML_response_fake [display,gray] |
|
352 "apply_fresh_args @{term \"za::'a \<Rightarrow> 'b \<Rightarrow> 'c\"} @{context} |
|
353 |> Syntax.string_of_term @{context} |
|
354 |> writeln" |
|
355 "za z zb"} |
348 |
356 |
349 The combinator @{ML "#>"} is the reverse function composition. It can be |
357 The combinator @{ML "#>"} is the reverse function composition. It can be |
350 used to define the following function |
358 used to define the following function |
351 *} |
359 *} |
352 |
360 |
995 A handy function for manipulating terms is @{ML map_types}: it takes a |
1003 A handy function for manipulating terms is @{ML map_types}: it takes a |
996 function and applies it to every type in a term. You can, for example, |
1004 function and applies it to every type in a term. You can, for example, |
997 change every @{typ nat} in a term into an @{typ int} using the function: |
1005 change every @{typ nat} in a term into an @{typ int} using the function: |
998 *} |
1006 *} |
999 |
1007 |
1000 ML{*fun nat_to_int t = |
1008 ML{*fun nat_to_int ty = |
1001 (case t of |
1009 (case ty of |
1002 @{typ nat} => @{typ int} |
1010 @{typ nat} => @{typ int} |
1003 | Type (s, ts) => Type (s, map nat_to_int ts) |
1011 | Type (s, tys) => Type (s, map nat_to_int tys) |
1004 | _ => t)*} |
1012 | _ => ty)*} |
1005 |
1013 |
1006 text {* |
1014 text {* |
1007 Here is an example: |
1015 Here is an example: |
1008 |
1016 |
1009 @{ML_response_fake [display,gray] |
1017 @{ML_response_fake [display,gray] |
1319 text {* |
1327 text {* |
1320 where the function @{ML "Thm.rule_attribute"} expects a function taking a |
1328 where the function @{ML "Thm.rule_attribute"} expects a function taking a |
1321 context (which we ignore in the code above) and a theorem (@{text thm}), and |
1329 context (which we ignore in the code above) and a theorem (@{text thm}), and |
1322 returns another theorem (namely @{text thm} resolved with the theorem |
1330 returns another theorem (namely @{text thm} resolved with the theorem |
1323 @{thm [source] sym}: @{thm sym[no_vars]}).\footnote{The function @{ML RS} is explained |
1331 @{thm [source] sym}: @{thm sym[no_vars]}).\footnote{The function @{ML RS} is explained |
1324 later on in Section~\ref{sec:simpletacs}.} The function |
1332 in Section~\ref{sec:simpletacs}.} The function |
1325 @{ML "Thm.rule_attribute"} then returns |
1333 @{ML "Thm.rule_attribute"} then returns |
1326 an attribute. |
1334 an attribute. |
1327 |
1335 |
1328 Before we can use the attribute, we need to set it up. This can be done |
1336 Before we can use the attribute, we need to set it up. This can be done |
1329 using the Isabelle command \isacommand{attribute\_setup} as follows: |
1337 using the Isabelle command \isacommand{attribute\_setup} as follows: |