equal
deleted
inserted
replaced
1364 Simproc patterns: |
1364 Simproc patterns: |
1365 \<dots>"} |
1365 \<dots>"} |
1366 |
1366 |
1367 |
1367 |
1368 The simplifier is often used to unfold definitions in a proof. For this the |
1368 The simplifier is often used to unfold definitions in a proof. For this the |
1369 simplifier implements the tactic @{ML_ind rewrite_goals_tac}.\footnote{FIXME: |
1369 simplifier implements the tactic @{ML_ind rewrite_goal_tac}.\footnote{\bf FIXME: |
1370 see LocalDefs infrastructure.} Suppose for example the |
1370 see LocalDefs infrastructure.} Suppose for example the |
1371 definition |
1371 definition |
1372 *} |
1372 *} |
1373 |
1373 |
1374 definition "MyTrue \<equiv> True" |
1374 definition "MyTrue \<equiv> True" |
1375 |
1375 |
1376 text {* |
1376 text {* |
1377 then in the following proof we can unfold this constant |
1377 then we can use this tactic to unfold the definition of the constant. |
1378 *} |
1378 *} |
1379 |
1379 |
1380 lemma shows "MyTrue \<Longrightarrow> True \<and> True" |
1380 lemma shows "MyTrue \<Longrightarrow> True" |
1381 apply(rule conjI) |
1381 apply(tactic {* rewrite_goal_tac @{thms MyTrue_def} 1 *}) |
1382 apply(tactic {* rewrite_goals_tac @{thms MyTrue_def} *}) |
|
1383 txt{* producing the goal state |
1382 txt{* producing the goal state |
1384 |
1383 |
1385 \begin{minipage}{\textwidth} |
1384 \begin{minipage}{\textwidth} |
1386 @{subgoals [display]} |
1385 @{subgoals [display]} |
1387 \end{minipage} *} |
1386 \end{minipage} *} |
1388 (*<*)oops(*>*) |
1387 (*<*)oops(*>*) |
1389 |
1388 |
1390 text {* |
1389 text {* |
1391 As you can see, the tactic unfolds the definitions in all subgoals. |
1390 If you want to unfold definitions in all subgoals, then use the |
|
1391 the tactic @{ML_ind rewrite_goals_tac}. |
1392 *} |
1392 *} |
1393 |
1393 |
1394 |
1394 |
1395 text_raw {* |
1395 text_raw {* |
1396 \begin{figure}[p] |
1396 \begin{figure}[p] |