# HG changeset patch # User wenzelm # Date 1135207751 -3600 # Node ID 82707239f377b79ab58988ab44fe831b80dad7d1 # Parent 29a5070b517c76c77e66ee5293190fe88104fbc7 updated auxiliary facts for induct method; removed dead code; diff -r 29a5070b517c -r 82707239f377 TFL/casesplit.ML --- 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