# HG changeset patch # User krauss # Date 1298620012 -3600 # Node ID f69045fdc836fd2119553b43d31d8d65fb7a3dd0 # Parent 421a795cee0537d2870067ae0c48436b8ebef8f5 removed dead code/unused exports/speculative generality diff -r 421a795cee05 -r f69045fdc836 src/HOL/Tools/TFL/casesplit.ML --- a/src/HOL/Tools/TFL/casesplit.ML Thu Feb 24 21:54:28 2011 +0100 +++ b/src/HOL/Tools/TFL/casesplit.ML Fri Feb 25 08:46:52 2011 +0100 @@ -1,80 +1,22 @@ (* Title: HOL/Tools/TFL/casesplit.ML Author: Lucas Dixon, University of Edinburgh -A structure that defines a tactic to program case splits. - - casesplit_free : - string * typ -> int -> thm -> thm Seq.seq - - casesplit_name : - string -> int -> thm -> thm Seq.seq - -These use the induction theorem associated with the recursive data -type to be split. - -The structure includes a function to try and recursively split a -conjecture into a list sub-theorems: - - splitto : thm list -> thm -> thm +Extra case splitting for TFL. *) -(* logic-specific *) -signature CASE_SPLIT_DATA = -sig - val dest_Trueprop : term -> term - val mk_Trueprop : term -> term - val atomize : thm list - val rulify : thm list -end; - -structure CaseSplitData_HOL : CASE_SPLIT_DATA = -struct -val dest_Trueprop = HOLogic.dest_Trueprop; -val mk_Trueprop = HOLogic.mk_Trueprop; - -val atomize = @{thms induct_atomize}; -val rulify = @{thms induct_rulify}; -val rulify_fallback = @{thms induct_rulify_fallback}; - -end; - - signature CASE_SPLIT = sig - (* failure to find a free to split on *) - exception find_split_exp of string - - (* getting a case split thm from the induction thm *) - val case_thm_of_ty : theory -> typ -> thm - val cases_thm_of_induct_thm : thm -> thm - - (* case split tactics *) - val casesplit_free : - string * typ -> int -> thm -> thm Seq.seq - val casesplit_name : string -> int -> thm -> thm Seq.seq - - (* finding a free var to split *) - val find_term_split : - term * term -> (string * typ) option - val find_thm_split : - thm -> int -> thm -> (string * typ) option - val find_thms_split : - thm list -> int -> thm -> (string * typ) option (* try to recursively split conjectured thm to given list of thms *) val splitto : thm list -> thm -> thm - (* for use with the recdef package *) - val derive_init_eqs : - theory -> - (thm * int) list -> term list -> (thm * int) list end; -functor CaseSplitFUN(Data : CASE_SPLIT_DATA) = +structure CaseSplit: CASE_SPLIT = struct -val rulify_goals = Raw_Simplifier.rewrite_goals_rule Data.rulify; -val atomize_goals = Raw_Simplifier.rewrite_goals_rule Data.atomize; +val rulify_goals = Raw_Simplifier.rewrite_goals_rule @{thms induct_rulify}; +val atomize_goals = Raw_Simplifier.rewrite_goals_rule @{thms induct_atomize}; (* beta-eta contract the theorem *) fun beta_eta_contract thm = @@ -99,10 +41,6 @@ cases_thm_of_induct_thm (#induct dt) end; -(* - val ty = (snd o hd o map Term.dest_Free o OldTerm.term_frees) t; -*) - (* for use when there are no prems to the subgoal *) (* does a case split on the given variable *) @@ -139,71 +77,6 @@ end; -(* for use when there are no prems to the subgoal *) -(* does a case split on the given variable (Free fv) *) -fun casesplit_free fv i th = - let - val (subgoalth, exp) = IsaND.fix_alls i th; - val subgoalth' = atomize_goals subgoalth; - val gt = Data.dest_Trueprop (Logic.get_goal (Thm.prop_of subgoalth') 1); - val sgn = Thm.theory_of_thm th; - - val splitter_thm = mk_casesplit_goal_thm sgn fv gt; - val nsplits = Thm.nprems_of splitter_thm; - - val split_goal_th = splitter_thm RS subgoalth'; - val rulified_split_goal_th = rulify_goals split_goal_th; - in - IsaND.export_back exp rulified_split_goal_th - end; - - -(* for use when there are no prems to the subgoal *) -(* does a case split on the given variable *) -fun casesplit_name vstr i th = - let - val (subgoalth, exp) = IsaND.fix_alls i th; - val subgoalth' = atomize_goals subgoalth; - val gt = Data.dest_Trueprop (Logic.get_goal (Thm.prop_of subgoalth') 1); - - val freets = OldTerm.term_frees gt; - fun getter x = - let val (n,ty) = Term.dest_Free x in - (if vstr = n orelse vstr = Name.dest_skolem n - then SOME (n,ty) else NONE ) - handle Fail _ => NONE (* dest_skolem *) - end; - val (n,ty) = case Library.get_first getter freets - of SOME (n, ty) => (n, ty) - | _ => error ("no such variable " ^ vstr); - val sgn = Thm.theory_of_thm th; - - val splitter_thm = mk_casesplit_goal_thm sgn (n,ty) gt; - val nsplits = Thm.nprems_of splitter_thm; - - val split_goal_th = splitter_thm RS subgoalth'; - - val rulified_split_goal_th = rulify_goals split_goal_th; - in - IsaND.export_back exp rulified_split_goal_th - end; - - -(* small example: -Goal "P (x :: nat) & (C y --> Q (y :: nat))"; -by (rtac (thm "conjI") 1); -val th = topthm(); -val i = 2; -val vstr = "y"; - -by (casesplit_name "y" 2); - -val th = topthm(); -val i = 1; -val th' = casesplit_name "x" i th; -*) - - (* the find_XXX_split functions are simply doing a lightwieght (I think) term matching equivalent to find where to do the next split *) @@ -275,7 +148,7 @@ error "splitto: cannot find variable to split on") | SOME v => let - val gt = Data.dest_Trueprop (List.nth(Thm.prems_of th, 0)); + val gt = HOLogic.dest_Trueprop (List.nth(Thm.prems_of th, 0)); val split_thm = mk_casesplit_goal_thm sgn v gt; val (subthms, expf) = IsaND.fixed_subgoal_thms split_thm; in @@ -292,36 +165,4 @@ recsplitf genth end; - -(* Note: We dont do this if wf conditions fail to be solved, as each -case may have a different wf condition - we could group the conditions -togeather and say that they must be true to solve the general case, -but that would hide from the user which sub-case they were related -to. Probably this is not important, and it would work fine, but I -prefer leaving more fine grain control to the user. *) - -(* derive eqs, assuming strict, ie the rules have no assumptions = all - the well-foundness conditions have been solved. *) -fun derive_init_eqs sgn rules eqs = - let - fun get_related_thms i = - map_filter ((fn (r, x) => if x = i then SOME r else NONE)); - fun add_eq (i, e) xs = - (e, (get_related_thms i rules), i) :: xs - fun solve_eq (th, [], i) = - error "derive_init_eqs: missing rules" - | solve_eq (th, [a], i) = (a, i) - | solve_eq (th, splitths as (_ :: _), i) = (splitto splitths th, i); - val eqths = - map (Thm.trivial o Thm.cterm_of sgn o Data.mk_Trueprop) eqs; - in - [] - |> fold_index add_eq eqths - |> map solve_eq - |> rev - end; - end; - - -structure CaseSplit = CaseSplitFUN(CaseSplitData_HOL);