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