equal
deleted
inserted
replaced
2400 |
2400 |
2401 Finally, conversions can also be turned into tactics and then applied to |
2401 Finally, conversions can also be turned into tactics and then applied to |
2402 goal states. This can be done with the help of the function |
2402 goal states. This can be done with the help of the function |
2403 @{ML_ind CONVERSION in Tactical}, |
2403 @{ML_ind CONVERSION in Tactical}, |
2404 and also some predefined conversion combinators that traverse a goal |
2404 and also some predefined conversion combinators that traverse a goal |
2405 state. The combinators for the goal state are: |
2405 state and can selectively apply the conversion. The combinators for |
|
2406 the goal state are: |
2406 |
2407 |
2407 \begin{itemize} |
2408 \begin{itemize} |
2408 \item @{ML_ind params_conv in Conv} for converting under parameters |
2409 \item @{ML_ind params_conv in Conv} for converting under parameters |
2409 (i.e.~where goals are of the form @{text "\<And>x. P x \<Longrightarrow> Q x"}) |
2410 (i.e.~where goals are of the form @{text "\<And>x. P x \<Longrightarrow> Q x"}) |
2410 |
2411 |
2446 \end{isabelle}*} |
2447 \end{isabelle}*} |
2447 (*<*)oops(*>*) |
2448 (*<*)oops(*>*) |
2448 |
2449 |
2449 text {* |
2450 text {* |
2450 As you can see, the premises are rewritten according to @{ML if_true1_conv}, while |
2451 As you can see, the premises are rewritten according to @{ML if_true1_conv}, while |
2451 the conclusion according to @{ML true_conj1_conv}. |
2452 the conclusion according to @{ML true_conj1_conv}. If we only have one |
|
2453 conversion that should be uniformly applied to the whole goal state, we |
|
2454 can also use @{ML_ind top_conv in More_Conv}. |
2452 |
2455 |
2453 Conversions can also be helpful for constructing meta-equality theorems. |
2456 Conversions can also be helpful for constructing meta-equality theorems. |
2454 Such theorems are often definitions. As an example consider the following |
2457 Such theorems are often definitions. As an example consider the following |
2455 two ways of defining the identity function in Isabelle. |
2458 two ways of defining the identity function in Isabelle. |
2456 *} |
2459 *} |