Mercurial Mercurial > hg > isabelle-cookbook / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
used rewrite_goal_tac (instead of rewrite_goals_tac)
authorChristian Urban <urbanc@in.tum.de>
Mon, 05 Oct 2009 11:45:49 +0200
changeset 331 46100dc4a808
parent 330 7718da58d9c0
child 332 6fba3a3e80a3
used rewrite_goal_tac (instead of rewrite_goals_tac)
ProgTutorial/Package/Ind_Code.thy file | annotate | diff | comparison | revisions
ProgTutorial/Package/simple_inductive_package.ML file | annotate | diff | comparison | revisions
ProgTutorial/Tactical.thy file | annotate | diff | comparison | revisions
progtutorial.pdf file | annotate | diff | comparison | revisions 
--- a/ProgTutorial/Package/Ind_Code.thy	Sun Oct 04 21:56:53 2009 +0200
+++ b/ProgTutorial/Package/Ind_Code.thy	Mon Oct 05 11:45:49 2009 +0200
@@ -278,7 +278,7 @@
 ML %linenosgray{*fun ind_tac defs prem insts =
   EVERY1 [ObjectLogic.full_atomize_tac,
           cut_facts_tac prem,
-          K (rewrite_goals_tac defs),
+          rewrite_goal_tac defs,
           inst_spec_tac insts,
           assume_tac]*}
 
@@ -563,7 +563,7 @@
 
 ML %linenosgray{*fun expand_tac defs =
   ObjectLogic.rulify_tac 1
-  THEN rewrite_goals_tac defs
+  THEN rewrite_goal_tac defs 1
   THEN (REPEAT (resolve_tac [@{thm allI}, @{thm impI}] 1)) *}
 
 text {*
@@ -905,7 +905,7 @@
 
 ML %linenosgray{*fun intro_tac defs rules preds i ctxt =
   EVERY1 [ObjectLogic.rulify_tac,
-          K (rewrite_goals_tac defs),
+          rewrite_goal_tac defs,
           REPEAT o (resolve_tac [@{thm allI}, @{thm impI}]),
           prove_intro_tac i preds rules ctxt]*}
 
--- a/ProgTutorial/Package/simple_inductive_package.ML	Sun Oct 04 21:56:53 2009 +0200
+++ b/ProgTutorial/Package/simple_inductive_package.ML	Mon Oct 05 11:45:49 2009 +0200
@@ -65,7 +65,7 @@
 fun induction_tac defs prems insts =
   EVERY1 [ObjectLogic.full_atomize_tac,
           cut_facts_tac prems,
-          K (rewrite_goals_tac defs),
+          rewrite_goal_tac defs,
           EVERY' (map (dtac o inst_spec) insts),
           assume_tac]
 (* @end *)
@@ -139,7 +139,7 @@
 
 fun introductions_tac defs rules preds i ctxt =
   EVERY1 [ObjectLogic.rulify_tac,
-          K (rewrite_goals_tac defs),
+          rewrite_goal_tac defs,
           REPEAT o (resolve_tac [@{thm allI},@{thm impI}]),
           subproof1 rules preds i ctxt]
 
--- a/ProgTutorial/Tactical.thy	Sun Oct 04 21:56:53 2009 +0200
+++ b/ProgTutorial/Tactical.thy	Mon Oct 05 11:45:49 2009 +0200
@@ -1366,7 +1366,7 @@
 
   
   The simplifier is often used to unfold definitions in a proof. For this the
-  simplifier implements the tactic @{ML_ind  rewrite_goals_tac}.\footnote{FIXME: 
+  simplifier implements the tactic @{ML_ind  rewrite_goal_tac}.\footnote{\bf FIXME: 
   see LocalDefs infrastructure.} Suppose for example the
   definition
 *}
@@ -1374,12 +1374,11 @@
 definition "MyTrue \<equiv> True"
 
 text {*
-  then in the following proof we can unfold this constant
+  then we can use this tactic to unfold the definition of the constant.
 *}
 
-lemma shows "MyTrue \<Longrightarrow> True \<and> True"
-apply(rule conjI)
-apply(tactic {* rewrite_goals_tac @{thms MyTrue_def} *})
+lemma shows "MyTrue \<Longrightarrow> True"
+apply(tactic {* rewrite_goal_tac @{thms MyTrue_def} 1 *})
 txt{* producing the goal state
 
       \begin{minipage}{\textwidth}
@@ -1388,7 +1387,8 @@
 (*<*)oops(*>*)
 
 text {*
-  As you can see, the tactic unfolds the definitions in all subgoals.
+  If you want to unfold definitions in all subgoals, then use the 
+  the tactic @{ML_ind rewrite_goals_tac}.
 *}
 
 
Binary file progtutorial.pdf has changed
isabelle-cookbook