summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Thu, 22 Dec 2005 00:29:11 +0100 | |

changeset 18479 | 82707239f377 |

parent 18478 | 29a5070b517c |

child 18480 | 8ac97f71369d |

updated auxiliary facts for induct method;
removed dead code;

TFL/casesplit.ML | file | annotate | diff | comparison | revisions |

--- a/TFL/casesplit.ML Thu Dec 22 00:29:10 2005 +0100 +++ b/TFL/casesplit.ML Thu Dec 22 00:29:11 2005 +0100 @@ -30,26 +30,18 @@ sig val dest_Trueprop : term -> term val mk_Trueprop : term -> term - - val localize : thm list - val local_impI : thm val atomize : thm list - val rulify1 : thm list - val rulify2 : thm list - + val rulify : thm list end; -(* for HOL *) structure CaseSplitData_HOL : CASE_SPLIT_DATA = struct val dest_Trueprop = HOLogic.dest_Trueprop; val mk_Trueprop = HOLogic.mk_Trueprop; -val localize = [Thm.symmetric (thm "induct_implies_def")]; -val local_impI = thm "induct_impliesI"; val atomize = thms "induct_atomize"; -val rulify1 = thms "induct_rulify1"; -val rulify2 = thms "induct_rulify2"; +val rulify = thms "induct_rulify"; +val rulify_fallback = thms "induct_rulify_fallback"; end; @@ -88,23 +80,9 @@ functor CaseSplitFUN(Data : CASE_SPLIT_DATA) = struct -val rulify_goals = Tactic.rewrite_goals_rule Data.rulify1; +val rulify_goals = Tactic.rewrite_goals_rule Data.rulify; val atomize_goals = Tactic.rewrite_goals_rule Data.atomize; -(* -val localize = Tactic.norm_hhf_rule o Tactic.simplify false Data.localize; -fun atomize_term sg = - ObjectLogic.drop_judgment sg o MetaSimplifier.rewrite_term sg Data.atomize []; -val rulify_tac = Tactic.rewrite_goal_tac Data.rulify1; -val atomize_tac = Tactic.rewrite_goal_tac Data.atomize; -Tactic.simplify_goal -val rulify_tac = - Tactic.rewrite_goal_tac Data.rulify1 THEN' - Tactic.rewrite_goal_tac Data.rulify2 THEN' - Tactic.norm_hhf_tac; -val atomize = Tactic.norm_hhf_rule o Tactic.simplify true Data.atomize; -*) - (* beta-eta contract the theorem *) fun beta_eta_contract thm = let