src/HOL/Tools/TFL/casesplit.ML
author blanchet
Mon, 01 Sep 2014 16:17:46 +0200
changeset 58111 82db9ad610b9
parent 55236 8d61b0aa7a0d
child 58112 8081087096ad
permissions -rw-r--r--
tuned structure inclusion
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
     1
(*  Title:      HOL/Tools/TFL/casesplit.ML
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
     2
    Author:     Lucas Dixon, University of Edinburgh
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
     3
41840
f69045fdc836 removed dead code/unused exports/speculative generality
krauss
parents: 41228
diff changeset
     4
Extra case splitting for TFL.
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
     5
*)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
     6
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
     7
signature CASE_SPLIT =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
     8
sig
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
     9
  (* try to recursively split conjectured thm to given list of thms *)
49340
25fc6e0da459 observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents: 46489
diff changeset
    10
  val splitto : Proof.context -> thm list -> thm -> thm
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    11
end;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    12
41840
f69045fdc836 removed dead code/unused exports/speculative generality
krauss
parents: 41228
diff changeset
    13
structure CaseSplit: CASE_SPLIT =
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    14
struct
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    15
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    16
(* make a casethm from an induction thm *)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    17
val cases_thm_of_induct_thm =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    18
     Seq.hd o (ALLGOALS (fn i => REPEAT (etac Drule.thin_rl i)));
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    19
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    20
(* get the case_thm (my version) from a type *)
31784
bd3486c57ba3 tuned interfaces of datatype module
haftmann
parents: 31723
diff changeset
    21
fun case_thm_of_ty thy ty  =
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    22
    let
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    23
      val ty_str = case ty of
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    24
                     Type(ty_str, _) => ty_str
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    25
                   | TFree(s,_)  => error ("Free type: " ^ s)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    26
                   | TVar((s,i),_) => error ("Free variable: " ^ s)
58111
82db9ad610b9 tuned structure inclusion
blanchet
parents: 55236
diff changeset
    27
      val {induct, ...} = Datatype_Data.the_info thy ty_str
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    28
    in
45701
615da8b8d758 discontinued obsolete datatype "alt_names";
wenzelm
parents: 44121
diff changeset
    29
      cases_thm_of_induct_thm induct
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    30
    end;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    31
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    32
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    33
(* for use when there are no prems to the subgoal *)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    34
(* does a case split on the given variable *)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    35
fun mk_casesplit_goal_thm sgn (vstr,ty) gt =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    36
    let
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    37
      val x = Free(vstr,ty)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    38
      val abst = Abs(vstr, ty, Term.abstract_over (x, gt));
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    39
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    40
      val ctermify = Thm.cterm_of sgn;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    41
      val ctypify = Thm.ctyp_of sgn;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    42
      val case_thm = case_thm_of_ty sgn ty;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    43
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    44
      val abs_ct = ctermify abst;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    45
      val free_ct = ctermify x;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    46
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    47
      val (Pv, Dv, type_insts) =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    48
          case (Thm.concl_of case_thm) of
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    49
            (_ $ ((Pv as Var(P,Pty)) $ (Dv as Var(D, Dty)))) =>
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    50
            (Pv, Dv,
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    51
             Sign.typ_match sgn (Dty, ty) Vartab.empty)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    52
          | _ => error "not a valid case thm";
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    53
      val type_cinsts = map (fn (ixn, (S, T)) => (ctypify (TVar (ixn, S)), ctypify T))
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    54
        (Vartab.dest type_insts);
32035
8e77b6a250d5 tuned/modernized Envir.subst_XXX;
wenzelm
parents: 31784
diff changeset
    55
      val cPv = ctermify (Envir.subst_term_types type_insts Pv);
8e77b6a250d5 tuned/modernized Envir.subst_XXX;
wenzelm
parents: 31784
diff changeset
    56
      val cDv = ctermify (Envir.subst_term_types type_insts Dv);
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    57
    in
52243
92bafa4235fa prefer existing beta_eta_conversion;
wenzelm
parents: 49340
diff changeset
    58
      Conv.fconv_rule Drule.beta_eta_conversion
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    59
         (case_thm
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    60
            |> Thm.instantiate (type_cinsts, [])
52243
92bafa4235fa prefer existing beta_eta_conversion;
wenzelm
parents: 49340
diff changeset
    61
            |> Thm.instantiate ([], [(cPv, abs_ct), (cDv, free_ct)]))
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    62
    end;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    63
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    64
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    65
(* the find_XXX_split functions are simply doing a lightwieght (I
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    66
think) term matching equivalent to find where to do the next split *)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    67
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    68
(* assuming two twems are identical except for a free in one at a
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    69
subterm, or constant in another, ie assume that one term is a plit of
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    70
another, then gives back the free variable that has been split. *)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    71
exception find_split_exp of string
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    72
fun find_term_split (Free v, _ $ _) = SOME v
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    73
  | find_term_split (Free v, Const _) = SOME v
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    74
  | find_term_split (Free v, Abs _) = SOME v (* do we really want this case? *)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    75
  | find_term_split (Free v, Var _) = NONE (* keep searching *)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    76
  | find_term_split (a $ b, a2 $ b2) =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    77
    (case find_term_split (a, a2) of
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    78
       NONE => find_term_split (b,b2)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    79
     | vopt => vopt)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    80
  | find_term_split (Abs(_,ty,t1), Abs(_,ty2,t2)) =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    81
    find_term_split (t1, t2)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    82
  | find_term_split (Const (x,ty), Const(x2,ty2)) =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    83
    if x = x2 then NONE else (* keep searching *)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    84
    raise find_split_exp (* stop now *)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    85
            "Terms are not identical upto a free varaible! (Consts)"
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    86
  | find_term_split (Bound i, Bound j) =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    87
    if i = j then NONE else (* keep searching *)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    88
    raise find_split_exp (* stop now *)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    89
            "Terms are not identical upto a free varaible! (Bound)"
46489
2accd201e5bc removed dead code;
wenzelm
parents: 45701
diff changeset
    90
  | find_term_split _ =
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    91
    raise find_split_exp (* stop now *)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    92
            "Terms are not identical upto a free varaible! (Other)";
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    93
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    94
(* assume that "splitth" is a case split form of subgoal i of "genth",
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    95
then look for a free variable to split, breaking the subgoal closer to
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    96
splitth. *)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    97
fun find_thm_split splitth i genth =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    98
    find_term_split (Logic.get_goal (Thm.prop_of genth) i,
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    99
                     Thm.concl_of splitth) handle find_split_exp _ => NONE;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   100
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   101
(* as above but searches "splitths" for a theorem that suggest a case split *)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   102
fun find_thms_split splitths i genth =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   103
    Library.get_first (fn sth => find_thm_split sth i genth) splitths;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   104
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   105
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   106
(* split the subgoal i of "genth" until we get to a member of
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   107
splitths. Assumes that genth will be a general form of splitths, that
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   108
can be case-split, as needed. Otherwise fails. Note: We assume that
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   109
all of "splitths" are split to the same level, and thus it doesn't
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   110
matter which one we choose to look for the next split. Simply add
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   111
search on splitthms and split variable, to change this.  *)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   112
(* Note: possible efficiency measure: when a case theorem is no longer
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   113
useful, drop it? *)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   114
(* Note: This should not be a separate tactic but integrated into the
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   115
case split done during recdef's case analysis, this would avoid us
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   116
having to (re)search for variables to split. *)
49340
25fc6e0da459 observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents: 46489
diff changeset
   117
fun splitto ctxt splitths genth =
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   118
    let
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   119
      val _ = not (null splitths) orelse error "splitto: no given splitths";
42364
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 41840
diff changeset
   120
      val thy = Thm.theory_of_thm genth;
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   121
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   122
      (* check if we are a member of splitths - FIXME: quicker and
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   123
      more flexible with discrim net. *)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   124
      fun solve_by_splitth th split =
42364
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 41840
diff changeset
   125
        Thm.biresolution false [(false,split)] 1 th;
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   126
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   127
      fun split th =
42364
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 41840
diff changeset
   128
        (case find_thms_split splitths 1 th of
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 41840
diff changeset
   129
          NONE =>
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 41840
diff changeset
   130
           (writeln (cat_lines
55236
8d61b0aa7a0d proper context for printing;
wenzelm
parents: 52243
diff changeset
   131
            (["th:", Display.string_of_thm ctxt th, "split ths:"] @
8d61b0aa7a0d proper context for printing;
wenzelm
parents: 52243
diff changeset
   132
              map (Display.string_of_thm ctxt) splitths @ ["\n--"]));
42364
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 41840
diff changeset
   133
            error "splitto: cannot find variable to split on")
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 41840
diff changeset
   134
        | SOME v =>
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 41840
diff changeset
   135
            let
42365
bfd28ba57859 more direct Logic.dest_implies (with exception TERM instead of Subscript);
wenzelm
parents: 42364
diff changeset
   136
              val gt = HOLogic.dest_Trueprop (#1 (Logic.dest_implies (Thm.prop_of th)));
42364
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 41840
diff changeset
   137
              val split_thm = mk_casesplit_goal_thm thy v gt;
49340
25fc6e0da459 observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents: 46489
diff changeset
   138
              val (subthms, expf) = IsaND.fixed_subgoal_thms ctxt split_thm;
42364
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 41840
diff changeset
   139
            in
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 41840
diff changeset
   140
              expf (map recsplitf subthms)
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 41840
diff changeset
   141
            end)
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   142
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   143
      and recsplitf th =
42364
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 41840
diff changeset
   144
        (* note: multiple unifiers! we only take the first element,
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 41840
diff changeset
   145
           probably fine -- there is probably only one anyway. *)
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 41840
diff changeset
   146
        (case get_first (Seq.pull o solve_by_splitth th) splitths of
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 41840
diff changeset
   147
          NONE => split th
46489
2accd201e5bc removed dead code;
wenzelm
parents: 45701
diff changeset
   148
        | SOME (solved_th, _) => solved_th);
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   149
    in
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   150
      recsplitf genth
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   151
    end;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   152
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   153
end;