src/HOL/Tools/TFL/casesplit.ML
author wenzelm
Fri Jul 17 23:11:40 2009 +0200 (2009-07-17)
changeset 32035 8e77b6a250d5
parent 31784 bd3486c57ba3
child 32091 30e2ffbba718
permissions -rw-r--r--
tuned/modernized Envir.subst_XXX;
     1 (*  Title:      HOL/Tools/TFL/casesplit.ML
     2     Author:     Lucas Dixon, University of Edinburgh
     3 
     4 A structure that defines a tactic to program case splits.
     5 
     6     casesplit_free :
     7       string * typ -> int -> thm -> thm Seq.seq
     8 
     9     casesplit_name :
    10       string -> int -> thm -> thm Seq.seq
    11 
    12 These use the induction theorem associated with the recursive data
    13 type to be split.
    14 
    15 The structure includes a function to try and recursively split a
    16 conjecture into a list sub-theorems:
    17 
    18     splitto : thm list -> thm -> thm
    19 *)
    20 
    21 (* logic-specific *)
    22 signature CASE_SPLIT_DATA =
    23 sig
    24   val dest_Trueprop : term -> term
    25   val mk_Trueprop : term -> term
    26   val atomize : thm list
    27   val rulify : thm list
    28 end;
    29 
    30 structure CaseSplitData_HOL : CASE_SPLIT_DATA =
    31 struct
    32 val dest_Trueprop = HOLogic.dest_Trueprop;
    33 val mk_Trueprop = HOLogic.mk_Trueprop;
    34 
    35 val atomize = thms "induct_atomize";
    36 val rulify = thms "induct_rulify";
    37 val rulify_fallback = thms "induct_rulify_fallback";
    38 
    39 end;
    40 
    41 
    42 signature CASE_SPLIT =
    43 sig
    44   (* failure to find a free to split on *)
    45   exception find_split_exp of string
    46 
    47   (* getting a case split thm from the induction thm *)
    48   val case_thm_of_ty : theory -> typ -> thm
    49   val cases_thm_of_induct_thm : thm -> thm
    50 
    51   (* case split tactics *)
    52   val casesplit_free :
    53       string * typ -> int -> thm -> thm Seq.seq
    54   val casesplit_name : string -> int -> thm -> thm Seq.seq
    55 
    56   (* finding a free var to split *)
    57   val find_term_split :
    58       term * term -> (string * typ) option
    59   val find_thm_split :
    60       thm -> int -> thm -> (string * typ) option
    61   val find_thms_split :
    62       thm list -> int -> thm -> (string * typ) option
    63 
    64   (* try to recursively split conjectured thm to given list of thms *)
    65   val splitto : thm list -> thm -> thm
    66 
    67   (* for use with the recdef package *)
    68   val derive_init_eqs :
    69       theory ->
    70       (thm * int) list -> term list -> (thm * int) list
    71 end;
    72 
    73 functor CaseSplitFUN(Data : CASE_SPLIT_DATA) =
    74 struct
    75 
    76 val rulify_goals = MetaSimplifier.rewrite_goals_rule Data.rulify;
    77 val atomize_goals = MetaSimplifier.rewrite_goals_rule Data.atomize;
    78 
    79 (* beta-eta contract the theorem *)
    80 fun beta_eta_contract thm =
    81     let
    82       val thm2 = equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm
    83       val thm3 = equal_elim (Thm.eta_conversion (Thm.cprop_of thm2)) thm2
    84     in thm3 end;
    85 
    86 (* make a casethm from an induction thm *)
    87 val cases_thm_of_induct_thm =
    88      Seq.hd o (ALLGOALS (fn i => REPEAT (etac Drule.thin_rl i)));
    89 
    90 (* get the case_thm (my version) from a type *)
    91 fun case_thm_of_ty thy ty  =
    92     let
    93       val ty_str = case ty of
    94                      Type(ty_str, _) => ty_str
    95                    | TFree(s,_)  => error ("Free type: " ^ s)
    96                    | TVar((s,i),_) => error ("Free variable: " ^ s)
    97       val dt = Datatype.the_info thy ty_str
    98     in
    99       cases_thm_of_induct_thm (#induction dt)
   100     end;
   101 
   102 (*
   103  val ty = (snd o hd o map Term.dest_Free o OldTerm.term_frees) t;
   104 *)
   105 
   106 
   107 (* for use when there are no prems to the subgoal *)
   108 (* does a case split on the given variable *)
   109 fun mk_casesplit_goal_thm sgn (vstr,ty) gt =
   110     let
   111       val x = Free(vstr,ty)
   112       val abst = Abs(vstr, ty, Term.abstract_over (x, gt));
   113 
   114       val ctermify = Thm.cterm_of sgn;
   115       val ctypify = Thm.ctyp_of sgn;
   116       val case_thm = case_thm_of_ty sgn ty;
   117 
   118       val abs_ct = ctermify abst;
   119       val free_ct = ctermify x;
   120 
   121       val casethm_vars = rev (OldTerm.term_vars (Thm.concl_of case_thm));
   122 
   123       val casethm_tvars = OldTerm.term_tvars (Thm.concl_of case_thm);
   124       val (Pv, Dv, type_insts) =
   125           case (Thm.concl_of case_thm) of
   126             (_ $ ((Pv as Var(P,Pty)) $ (Dv as Var(D, Dty)))) =>
   127             (Pv, Dv,
   128              Sign.typ_match sgn (Dty, ty) Vartab.empty)
   129           | _ => error "not a valid case thm";
   130       val type_cinsts = map (fn (ixn, (S, T)) => (ctypify (TVar (ixn, S)), ctypify T))
   131         (Vartab.dest type_insts);
   132       val cPv = ctermify (Envir.subst_term_types type_insts Pv);
   133       val cDv = ctermify (Envir.subst_term_types type_insts Dv);
   134     in
   135       (beta_eta_contract
   136          (case_thm
   137             |> Thm.instantiate (type_cinsts, [])
   138             |> Thm.instantiate ([], [(cPv, abs_ct), (cDv, free_ct)])))
   139     end;
   140 
   141 
   142 (* for use when there are no prems to the subgoal *)
   143 (* does a case split on the given variable (Free fv) *)
   144 fun casesplit_free fv i th =
   145     let
   146       val (subgoalth, exp) = IsaND.fix_alls i th;
   147       val subgoalth' = atomize_goals subgoalth;
   148       val gt = Data.dest_Trueprop (Logic.get_goal (Thm.prop_of subgoalth') 1);
   149       val sgn = Thm.theory_of_thm th;
   150 
   151       val splitter_thm = mk_casesplit_goal_thm sgn fv gt;
   152       val nsplits = Thm.nprems_of splitter_thm;
   153 
   154       val split_goal_th = splitter_thm RS subgoalth';
   155       val rulified_split_goal_th = rulify_goals split_goal_th;
   156     in
   157       IsaND.export_back exp rulified_split_goal_th
   158     end;
   159 
   160 
   161 (* for use when there are no prems to the subgoal *)
   162 (* does a case split on the given variable *)
   163 fun casesplit_name vstr i th =
   164     let
   165       val (subgoalth, exp) = IsaND.fix_alls i th;
   166       val subgoalth' = atomize_goals subgoalth;
   167       val gt = Data.dest_Trueprop (Logic.get_goal (Thm.prop_of subgoalth') 1);
   168 
   169       val freets = OldTerm.term_frees gt;
   170       fun getter x =
   171           let val (n,ty) = Term.dest_Free x in
   172             (if vstr = n orelse vstr = Name.dest_skolem n
   173              then SOME (n,ty) else NONE )
   174             handle Fail _ => NONE (* dest_skolem *)
   175           end;
   176       val (n,ty) = case Library.get_first getter freets
   177                 of SOME (n, ty) => (n, ty)
   178                  | _ => error ("no such variable " ^ vstr);
   179       val sgn = Thm.theory_of_thm th;
   180 
   181       val splitter_thm = mk_casesplit_goal_thm sgn (n,ty) gt;
   182       val nsplits = Thm.nprems_of splitter_thm;
   183 
   184       val split_goal_th = splitter_thm RS subgoalth';
   185 
   186       val rulified_split_goal_th = rulify_goals split_goal_th;
   187     in
   188       IsaND.export_back exp rulified_split_goal_th
   189     end;
   190 
   191 
   192 (* small example:
   193 Goal "P (x :: nat) & (C y --> Q (y :: nat))";
   194 by (rtac (thm "conjI") 1);
   195 val th = topthm();
   196 val i = 2;
   197 val vstr = "y";
   198 
   199 by (casesplit_name "y" 2);
   200 
   201 val th = topthm();
   202 val i = 1;
   203 val th' = casesplit_name "x" i th;
   204 *)
   205 
   206 
   207 (* the find_XXX_split functions are simply doing a lightwieght (I
   208 think) term matching equivalent to find where to do the next split *)
   209 
   210 (* assuming two twems are identical except for a free in one at a
   211 subterm, or constant in another, ie assume that one term is a plit of
   212 another, then gives back the free variable that has been split. *)
   213 exception find_split_exp of string
   214 fun find_term_split (Free v, _ $ _) = SOME v
   215   | find_term_split (Free v, Const _) = SOME v
   216   | find_term_split (Free v, Abs _) = SOME v (* do we really want this case? *)
   217   | find_term_split (Free v, Var _) = NONE (* keep searching *)
   218   | find_term_split (a $ b, a2 $ b2) =
   219     (case find_term_split (a, a2) of
   220        NONE => find_term_split (b,b2)
   221      | vopt => vopt)
   222   | find_term_split (Abs(_,ty,t1), Abs(_,ty2,t2)) =
   223     find_term_split (t1, t2)
   224   | find_term_split (Const (x,ty), Const(x2,ty2)) =
   225     if x = x2 then NONE else (* keep searching *)
   226     raise find_split_exp (* stop now *)
   227             "Terms are not identical upto a free varaible! (Consts)"
   228   | find_term_split (Bound i, Bound j) =
   229     if i = j then NONE else (* keep searching *)
   230     raise find_split_exp (* stop now *)
   231             "Terms are not identical upto a free varaible! (Bound)"
   232   | find_term_split (a, b) =
   233     raise find_split_exp (* stop now *)
   234             "Terms are not identical upto a free varaible! (Other)";
   235 
   236 (* assume that "splitth" is a case split form of subgoal i of "genth",
   237 then look for a free variable to split, breaking the subgoal closer to
   238 splitth. *)
   239 fun find_thm_split splitth i genth =
   240     find_term_split (Logic.get_goal (Thm.prop_of genth) i,
   241                      Thm.concl_of splitth) handle find_split_exp _ => NONE;
   242 
   243 (* as above but searches "splitths" for a theorem that suggest a case split *)
   244 fun find_thms_split splitths i genth =
   245     Library.get_first (fn sth => find_thm_split sth i genth) splitths;
   246 
   247 
   248 (* split the subgoal i of "genth" until we get to a member of
   249 splitths. Assumes that genth will be a general form of splitths, that
   250 can be case-split, as needed. Otherwise fails. Note: We assume that
   251 all of "splitths" are split to the same level, and thus it doesn't
   252 matter which one we choose to look for the next split. Simply add
   253 search on splitthms and split variable, to change this.  *)
   254 (* Note: possible efficiency measure: when a case theorem is no longer
   255 useful, drop it? *)
   256 (* Note: This should not be a separate tactic but integrated into the
   257 case split done during recdef's case analysis, this would avoid us
   258 having to (re)search for variables to split. *)
   259 fun splitto splitths genth =
   260     let
   261       val _ = not (null splitths) orelse error "splitto: no given splitths";
   262       val sgn = Thm.theory_of_thm genth;
   263 
   264       (* check if we are a member of splitths - FIXME: quicker and
   265       more flexible with discrim net. *)
   266       fun solve_by_splitth th split =
   267           Thm.biresolution false [(false,split)] 1 th;
   268 
   269       fun split th =
   270           (case find_thms_split splitths 1 th of
   271              NONE =>
   272              (writeln "th:";
   273               Display.print_thm th; writeln "split ths:";
   274               Display.print_thms splitths; writeln "\n--";
   275               error "splitto: cannot find variable to split on")
   276             | SOME v =>
   277              let
   278                val gt = Data.dest_Trueprop (List.nth(Thm.prems_of th, 0));
   279                val split_thm = mk_casesplit_goal_thm sgn v gt;
   280                val (subthms, expf) = IsaND.fixed_subgoal_thms split_thm;
   281              in
   282                expf (map recsplitf subthms)
   283              end)
   284 
   285       and recsplitf th =
   286           (* note: multiple unifiers! we only take the first element,
   287              probably fine -- there is probably only one anyway. *)
   288           (case Library.get_first (Seq.pull o solve_by_splitth th) splitths of
   289              NONE => split th
   290            | SOME (solved_th, more) => solved_th)
   291     in
   292       recsplitf genth
   293     end;
   294 
   295 
   296 (* Note: We dont do this if wf conditions fail to be solved, as each
   297 case may have a different wf condition - we could group the conditions
   298 togeather and say that they must be true to solve the general case,
   299 but that would hide from the user which sub-case they were related
   300 to. Probably this is not important, and it would work fine, but I
   301 prefer leaving more fine grain control to the user. *)
   302 
   303 (* derive eqs, assuming strict, ie the rules have no assumptions = all
   304    the well-foundness conditions have been solved. *)
   305 fun derive_init_eqs sgn rules eqs =
   306   let
   307     fun get_related_thms i =
   308       List.mapPartial ((fn (r, x) => if x = i then SOME r else NONE));
   309     fun add_eq (i, e) xs =
   310       (e, (get_related_thms i rules), i) :: xs
   311     fun solve_eq (th, [], i) =
   312           error "derive_init_eqs: missing rules"
   313       | solve_eq (th, [a], i) = (a, i)
   314       | solve_eq (th, splitths as (_ :: _), i) = (splitto splitths th, i);
   315     val eqths =
   316       map (Thm.trivial o Thm.cterm_of sgn o Data.mk_Trueprop) eqs;
   317   in
   318     []
   319     |> fold_index add_eq eqths
   320     |> map solve_eq
   321     |> rev
   322   end;
   323 
   324 end;
   325 
   326 
   327 structure CaseSplit = CaseSplitFUN(CaseSplitData_HOL);