summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

TFL/casesplit.ML

changeset 15250 | 217bececa2bd |

parent 15150 | c7af682b9ee5 |

child 15252 | d4f1b11c336b |

--- a/TFL/casesplit.ML Mon Oct 18 11:43:40 2004 +0200 +++ b/TFL/casesplit.ML Mon Oct 18 13:40:45 2004 +0200 @@ -31,6 +31,13 @@ val dest_Trueprop : Term.term -> Term.term val mk_Trueprop : Term.term -> Term.term val read_cterm : Sign.sg -> string -> Thm.cterm + + val localize : Thm.thm list + val local_impI : Thm.thm + val atomize : Thm.thm list + val rulify1 : Thm.thm list + val rulify2 : Thm.thm list + end; (* for HOL *) @@ -39,6 +46,13 @@ val dest_Trueprop = HOLogic.dest_Trueprop; val mk_Trueprop = HOLogic.mk_Trueprop; val read_cterm = HOLogic.read_cterm; + +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"; + end; @@ -76,6 +90,23 @@ functor CaseSplitFUN(Data : CASE_SPLIT_DATA) = struct +val rulify_goals = Tactic.rewrite_goals_rule Data.rulify1; +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 @@ -148,26 +179,49 @@ (* does a case split on the given variable (Free fv) *) fun casesplit_free fv i th = let - val gt = Data.dest_Trueprop (nth_elem( i - 1, Thm.prems_of th)); + 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.sign_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 - Tactic.rtac (mk_casesplit_goal_thm sgn fv gt) i th + 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 gt = Data.dest_Trueprop (nth_elem( i - 1, Thm.prems_of th)); + 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 = Term.term_frees gt; - fun getter x = let val (n,ty) = Term.dest_Free x in - if vstr = n then Some (n,ty) else None end; + fun getter x = + let val (n,ty) = Term.dest_Free x in + (if vstr = n orelse vstr = Syntax.dest_skolem n + then Some (n,ty) else None ) + handle LIST _ => None + end; val (n,ty) = case Library.get_first getter freets of Some (n, ty) => (n, ty) | _ => raise ERROR_MESSAGE ("no such variable " ^ vstr); val sgn = Thm.sign_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 - Tactic.rtac (mk_casesplit_goal_thm sgn (n,ty) gt) i th + IsaND.export_back exp rulified_split_goal_th end; @@ -196,6 +250,7 @@ fun find_term_split (Free v, _ $ _) = Some v | find_term_split (Free v, Const _) = Some v | find_term_split (Free v, Abs _) = Some v (* do we really want this case? *) + | find_term_split (Free v, Var _) = None (* keep searching *) | find_term_split (a $ b, a2 $ b2) = (case find_term_split (a, a2) of None => find_term_split (b,b2) @@ -229,9 +284,9 @@ (* split the subgoal i of "genth" until we get to a member of splitths. Assumes that genth will be a general form of splitths, that can be case-split, as needed. Otherwise fails. Note: We assume that -all of "splitths" are aplit to the same level, and thus it doesn't +all of "splitths" are split to the same level, and thus it doesn't matter which one we choose to look for the next split. Simply add -search on splitthms and plit variable, to change this. *) +search on splitthms and split variable, to change this. *) (* Note: possible efficiency measure: when a case theorem is no longer useful, drop it? *) (* Note: This should not be a separate tactic but integrated into the @@ -244,11 +299,16 @@ (* check if we are a member of splitths - FIXME: quicker and more flexible with discrim net. *) - fun solve_by_splitth th split = biresolution false [(false,split)] 1 th; + fun solve_by_splitth th split = + Thm.biresolution false [(false,split)] 1 th; fun split th = (case find_thms_split splitths 1 th of - None => raise ERROR_MESSAGE "splitto: cannot find variable to split on" + None => + (writeln "th:"; + print th; writeln "split ths:"; + print splitths; writeln "\n--"; + raise ERROR_MESSAGE "splitto: cannot find variable to split on") | Some v => let val gt = Data.dest_Trueprop (nth_elem(0, Thm.prems_of th));