equal
deleted
inserted
replaced
276 *} |
276 *} |
277 |
277 |
278 ML %linenosgray{*fun ind_tac defs prem insts = |
278 ML %linenosgray{*fun ind_tac defs prem insts = |
279 EVERY1 [ObjectLogic.full_atomize_tac, |
279 EVERY1 [ObjectLogic.full_atomize_tac, |
280 cut_facts_tac prem, |
280 cut_facts_tac prem, |
281 K (rewrite_goals_tac defs), |
281 rewrite_goal_tac defs, |
282 inst_spec_tac insts, |
282 inst_spec_tac insts, |
283 assume_tac]*} |
283 assume_tac]*} |
284 |
284 |
285 text {* |
285 text {* |
286 We have to give it as arguments the definitions, the premise (a list of |
286 We have to give it as arguments the definitions, the premise (a list of |
561 will use the tactic |
561 will use the tactic |
562 *} |
562 *} |
563 |
563 |
564 ML %linenosgray{*fun expand_tac defs = |
564 ML %linenosgray{*fun expand_tac defs = |
565 ObjectLogic.rulify_tac 1 |
565 ObjectLogic.rulify_tac 1 |
566 THEN rewrite_goals_tac defs |
566 THEN rewrite_goal_tac defs 1 |
567 THEN (REPEAT (resolve_tac [@{thm allI}, @{thm impI}] 1)) *} |
567 THEN (REPEAT (resolve_tac [@{thm allI}, @{thm impI}] 1)) *} |
568 |
568 |
569 text {* |
569 text {* |
570 The function in Line 2 ``rulifies'' the lemma.\footnote{FIXME: explain this better} |
570 The function in Line 2 ``rulifies'' the lemma.\footnote{FIXME: explain this better} |
571 This will turn out to |
571 This will turn out to |
903 function is the tactic that performs the proofs. |
903 function is the tactic that performs the proofs. |
904 *} |
904 *} |
905 |
905 |
906 ML %linenosgray{*fun intro_tac defs rules preds i ctxt = |
906 ML %linenosgray{*fun intro_tac defs rules preds i ctxt = |
907 EVERY1 [ObjectLogic.rulify_tac, |
907 EVERY1 [ObjectLogic.rulify_tac, |
908 K (rewrite_goals_tac defs), |
908 rewrite_goal_tac defs, |
909 REPEAT o (resolve_tac [@{thm allI}, @{thm impI}]), |
909 REPEAT o (resolve_tac [@{thm allI}, @{thm impI}]), |
910 prove_intro_tac i preds rules ctxt]*} |
910 prove_intro_tac i preds rules ctxt]*} |
911 |
911 |
912 text {* |
912 text {* |
913 Lines 2 to 4 in this tactic correspond to the function @{ML expand_tac}. |
913 Lines 2 to 4 in this tactic correspond to the function @{ML expand_tac}. |