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

TFL/casesplit.ML

author | wenzelm |

Fri, 17 Jun 2005 18:33:08 +0200 | |

changeset 16425 | 2427be27cc60 |

parent 15798 | 016f3be5a5ec |

child 16935 | 4d7f19d340e8 |

permissions | -rw-r--r-- |

accomodate identification of type Sign.sg and theory;

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) (* Title: TFL/casesplit.ML Author: Lucas Dixon, University of Edinburgh lucas.dixon@ed.ac.uk Date: 17 Aug 2004 *) (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) (* DESCRIPTION: A structure that defines a tactic to program case splits. casesplit_free : string * Term.type -> int -> Thm.thm -> Thm.thm Seq.seq casesplit_name : string -> int -> Thm.thm -> 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.thm list -> Thm.thm -> Thm.thm *) (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) (* logic-specific *) signature CASE_SPLIT_DATA = sig 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 *) structure CaseSplitData_HOL : CASE_SPLIT_DATA = struct 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; 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 : Sign.sg -> Term.typ -> Thm.thm val cases_thm_of_induct_thm : Thm.thm -> Thm.thm (* case split tactics *) val casesplit_free : string * Term.typ -> int -> Thm.thm -> Thm.thm Seq.seq val casesplit_name : string -> int -> Thm.thm -> Thm.thm Seq.seq (* finding a free var to split *) val find_term_split : Term.term * Term.term -> (string * Term.typ) option val find_thm_split : Thm.thm -> int -> Thm.thm -> (string * Term.typ) option val find_thms_split : Thm.thm list -> int -> Thm.thm -> (string * Term.typ) option (* try to recursively split conjectured thm to given list of thms *) val splitto : Thm.thm list -> Thm.thm -> Thm.thm (* for use with the recdef package *) val derive_init_eqs : Sign.sg -> (Thm.thm * int) list -> Term.term list -> (Thm.thm * int) list end; 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 val thm2 = equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm val thm3 = equal_elim (Thm.eta_conversion (Thm.cprop_of thm2)) thm2 in thm3 end; (* make a casethm from an induction thm *) val cases_thm_of_induct_thm = Seq.hd o (ALLGOALS (fn i => REPEAT (etac Drule.thin_rl i))); (* get the case_thm (my version) from a type *) fun case_thm_of_ty sgn ty = let val dtypestab = DatatypePackage.get_datatypes sgn; val ty_str = case ty of Type(ty_str, _) => ty_str | TFree(s,_) => raise ERROR_MESSAGE ("Free type: " ^ s) | TVar((s,i),_) => raise ERROR_MESSAGE ("Free variable: " ^ s) val dt = case (Symtab.lookup (dtypestab,ty_str)) of SOME dt => dt | NONE => raise ERROR_MESSAGE ("Not a Datatype: " ^ ty_str) in cases_thm_of_induct_thm (#induction dt) end; (* val ty = (snd o hd o map Term.dest_Free o Term.term_frees) t; *) (* for use when there are no prems to the subgoal *) (* does a case split on the given variable *) fun mk_casesplit_goal_thm sgn (vstr,ty) gt = let val x = Free(vstr,ty) val abst = Abs(vstr, ty, Term.abstract_over (x, gt)); val ctermify = Thm.cterm_of sgn; val ctypify = Thm.ctyp_of sgn; val case_thm = case_thm_of_ty sgn ty; val abs_ct = ctermify abst; val free_ct = ctermify x; val casethm_vars = rev (Term.term_vars (Thm.concl_of case_thm)); val tsig = Sign.tsig_of sgn; val casethm_tvars = Term.term_tvars (Thm.concl_of case_thm); val (Pv, Dv, type_insts) = case (Thm.concl_of case_thm) of (_ $ ((Pv as Var(P,Pty)) $ (Dv as Var(D, Dty)))) => (Pv, Dv, Type.typ_match tsig (Vartab.empty, (Dty, ty))) | _ => raise ERROR_MESSAGE ("not a valid case thm"); val type_cinsts = map (fn (ixn, (S, T)) => (ctypify (TVar (ixn, S)), ctypify T)) (Vartab.dest type_insts); val cPv = ctermify (Envir.subst_TVars type_insts Pv); val cDv = ctermify (Envir.subst_TVars type_insts Dv); in (beta_eta_contract (case_thm |> Thm.instantiate (type_cinsts, []) |> Thm.instantiate ([], [(cPv, abs_ct), (cDv, free_ct)]))) 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.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 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 = Term.term_frees gt; 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 Fail _ => NONE (* dest_skolem *) 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 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 *) (* assuming two twems are identical except for a free in one at a subterm, or constant in another, ie assume that one term is a plit of another, then gives back the free variable that has been split. *) exception find_split_exp of string 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) | vopt => vopt) | find_term_split (Abs(_,ty,t1), Abs(_,ty2,t2)) = find_term_split (t1, t2) | find_term_split (Const (x,ty), Const(x2,ty2)) = if x = x2 then NONE else (* keep searching *) raise find_split_exp (* stop now *) "Terms are not identical upto a free varaible! (Consts)" | find_term_split (Bound i, Bound j) = if i = j then NONE else (* keep searching *) raise find_split_exp (* stop now *) "Terms are not identical upto a free varaible! (Bound)" | find_term_split (a, b) = raise find_split_exp (* stop now *) "Terms are not identical upto a free varaible! (Other)"; (* assume that "splitth" is a case split form of subgoal i of "genth", then look for a free variable to split, breaking the subgoal closer to splitth. *) fun find_thm_split splitth i genth = find_term_split (Logic.get_goal (Thm.prop_of genth) i, Thm.concl_of splitth) handle find_split_exp _ => NONE; (* as above but searches "splitths" for a theorem that suggest a case split *) fun find_thms_split splitths i genth = Library.get_first (fn sth => find_thm_split sth i genth) splitths; (* 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 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 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 case split done during recdef's case analysis, this would avoid us having to (re)search for variables to split. *) fun splitto splitths genth = let val _ = assert (not (null splitths)) "splitto: no given splitths"; val sgn = Thm.sign_of_thm genth; (* check if we are a member of splitths - FIXME: quicker and more flexible with discrim net. *) 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 => (writeln "th:"; Display.print_thm th; writeln "split ths:"; Display.print_thms splitths; writeln "\n--"; raise ERROR_MESSAGE "splitto: cannot find variable to split on") | SOME v => let val gt = Data.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 expf (map recsplitf subthms) end) and recsplitf th = (* note: multiple unifiers! we only take the first element, probably fine -- there is probably only one anyway. *) (case Library.get_first (Seq.pull o solve_by_splitth th) splitths of NONE => split th | SOME (solved_th, more) => solved_th) in 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. *) local fun get_related_thms i = List.mapPartial ((fn (r,x) => if x = i then SOME r else NONE)); fun solve_eq (th, [], i) = raise ERROR_MESSAGE "derive_init_eqs: missing rules" | solve_eq (th, [a], i) = (a, i) | solve_eq (th, splitths as (_ :: _), i) = (splitto splitths th,i); in fun derive_init_eqs sgn rules eqs = let val eqths = map (Thm.trivial o (Thm.cterm_of sgn) o Data.mk_Trueprop) eqs in (rev o map solve_eq) (Library.foldln (fn (e,i) => (curry (op ::)) (e, (get_related_thms (i - 1) rules), i - 1)) eqths []) end; end; (* val (rs_hwfc, unhidefs) = Library.split_list (map hide_prems rules) (map2 (op |>) (ths, expfs)) *) end; structure CaseSplit = CaseSplitFUN(CaseSplitData_HOL);