src/HOL/Tools/TFL/casesplit.ML
author wenzelm
Sat, 16 Apr 2011 18:11:20 +0200
changeset 42364 8c674b3b8e44
parent 41840 f69045fdc836
child 42365 bfd28ba57859
permissions -rw-r--r--
eliminated old List.nth; tuned;
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
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    10
  (* try to recursively split conjectured thm to given list of thms *)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    11
  val splitto : thm list -> thm -> thm
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    12
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    13
end;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    14
41840
f69045fdc836 removed dead code/unused exports/speculative generality
krauss
parents: 41228
diff changeset
    15
structure CaseSplit: CASE_SPLIT =
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    16
struct
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    17
41840
f69045fdc836 removed dead code/unused exports/speculative generality
krauss
parents: 41228
diff changeset
    18
val rulify_goals = Raw_Simplifier.rewrite_goals_rule @{thms induct_rulify};
f69045fdc836 removed dead code/unused exports/speculative generality
krauss
parents: 41228
diff changeset
    19
val atomize_goals = Raw_Simplifier.rewrite_goals_rule @{thms induct_atomize};
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    20
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    21
(* beta-eta contract the theorem *)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    22
fun beta_eta_contract thm =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    23
    let
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 32952
diff changeset
    24
      val thm2 = Thm.equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 32952
diff changeset
    25
      val thm3 = Thm.equal_elim (Thm.eta_conversion (Thm.cprop_of thm2)) thm2
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    26
    in thm3 end;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    27
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    28
(* make a casethm from an induction thm *)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    29
val cases_thm_of_induct_thm =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    30
     Seq.hd o (ALLGOALS (fn i => REPEAT (etac Drule.thin_rl i)));
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    31
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    32
(* get the case_thm (my version) from a type *)
31784
bd3486c57ba3 tuned interfaces of datatype module
haftmann
parents: 31723
diff changeset
    33
fun case_thm_of_ty thy ty  =
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    34
    let
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    35
      val ty_str = case ty of
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    36
                     Type(ty_str, _) => ty_str
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    37
                   | TFree(s,_)  => error ("Free type: " ^ s)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    38
                   | TVar((s,i),_) => error ("Free variable: " ^ s)
31784
bd3486c57ba3 tuned interfaces of datatype module
haftmann
parents: 31723
diff changeset
    39
      val dt = Datatype.the_info thy ty_str
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    40
    in
32727
9072201cd69d avoid compound fields in datatype info record
haftmann
parents: 32712
diff changeset
    41
      cases_thm_of_induct_thm (#induct dt)
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    42
    end;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    43
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    44
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    45
(* for use when there are no prems to the subgoal *)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    46
(* does a case split on the given variable *)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    47
fun mk_casesplit_goal_thm sgn (vstr,ty) gt =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    48
    let
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    49
      val x = Free(vstr,ty)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    50
      val abst = Abs(vstr, ty, Term.abstract_over (x, gt));
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    51
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    52
      val ctermify = Thm.cterm_of sgn;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    53
      val ctypify = Thm.ctyp_of sgn;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    54
      val case_thm = case_thm_of_ty sgn ty;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    55
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    56
      val abs_ct = ctermify abst;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    57
      val free_ct = ctermify x;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    58
29265
5b4247055bd7 moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents: 23150
diff changeset
    59
      val casethm_vars = rev (OldTerm.term_vars (Thm.concl_of case_thm));
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    60
29270
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29265
diff changeset
    61
      val casethm_tvars = OldTerm.term_tvars (Thm.concl_of case_thm);
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    62
      val (Pv, Dv, type_insts) =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    63
          case (Thm.concl_of case_thm) of
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    64
            (_ $ ((Pv as Var(P,Pty)) $ (Dv as Var(D, Dty)))) =>
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    65
            (Pv, Dv,
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    66
             Sign.typ_match sgn (Dty, ty) Vartab.empty)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    67
          | _ => error "not a valid case thm";
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    68
      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
    69
        (Vartab.dest type_insts);
32035
8e77b6a250d5 tuned/modernized Envir.subst_XXX;
wenzelm
parents: 31784
diff changeset
    70
      val cPv = ctermify (Envir.subst_term_types type_insts Pv);
8e77b6a250d5 tuned/modernized Envir.subst_XXX;
wenzelm
parents: 31784
diff changeset
    71
      val cDv = ctermify (Envir.subst_term_types type_insts Dv);
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    72
    in
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    73
      (beta_eta_contract
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    74
         (case_thm
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    75
            |> Thm.instantiate (type_cinsts, [])
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    76
            |> Thm.instantiate ([], [(cPv, abs_ct), (cDv, free_ct)])))
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    77
    end;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    78
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    79
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    80
(* the find_XXX_split functions are simply doing a lightwieght (I
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    81
think) term matching equivalent to find where to do the next split *)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    82
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    83
(* assuming two twems are identical except for a free in one at a
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    84
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
    85
another, then gives back the free variable that has been split. *)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    86
exception find_split_exp of string
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    87
fun find_term_split (Free v, _ $ _) = SOME v
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    88
  | find_term_split (Free v, Const _) = SOME v
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    89
  | 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
    90
  | find_term_split (Free v, Var _) = NONE (* keep searching *)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    91
  | find_term_split (a $ b, a2 $ b2) =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    92
    (case find_term_split (a, a2) of
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    93
       NONE => find_term_split (b,b2)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    94
     | vopt => vopt)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    95
  | find_term_split (Abs(_,ty,t1), Abs(_,ty2,t2)) =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    96
    find_term_split (t1, t2)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    97
  | find_term_split (Const (x,ty), Const(x2,ty2)) =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    98
    if x = x2 then NONE else (* keep searching *)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    99
    raise find_split_exp (* stop now *)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   100
            "Terms are not identical upto a free varaible! (Consts)"
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   101
  | find_term_split (Bound i, Bound j) =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   102
    if i = j then NONE else (* keep searching *)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   103
    raise find_split_exp (* stop now *)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   104
            "Terms are not identical upto a free varaible! (Bound)"
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   105
  | find_term_split (a, b) =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   106
    raise find_split_exp (* stop now *)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   107
            "Terms are not identical upto a free varaible! (Other)";
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   108
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   109
(* assume that "splitth" is a case split form of subgoal i of "genth",
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   110
then look for a free variable to split, breaking the subgoal closer to
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   111
splitth. *)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   112
fun find_thm_split splitth i genth =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   113
    find_term_split (Logic.get_goal (Thm.prop_of genth) i,
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   114
                     Thm.concl_of splitth) handle find_split_exp _ => NONE;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   115
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   116
(* as above but searches "splitths" for a theorem that suggest a case split *)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   117
fun find_thms_split splitths i genth =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   118
    Library.get_first (fn sth => find_thm_split sth i genth) splitths;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   119
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   120
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   121
(* split the subgoal i of "genth" until we get to a member of
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   122
splitths. Assumes that genth will be a general form of splitths, that
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   123
can be case-split, as needed. Otherwise fails. Note: We assume that
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   124
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
   125
matter which one we choose to look for the next split. Simply add
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   126
search on splitthms and split variable, to change this.  *)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   127
(* Note: possible efficiency measure: when a case theorem is no longer
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   128
useful, drop it? *)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   129
(* Note: This should not be a separate tactic but integrated into the
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   130
case split done during recdef's case analysis, this would avoid us
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   131
having to (re)search for variables to split. *)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   132
fun splitto splitths genth =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   133
    let
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   134
      val _ = not (null splitths) orelse error "splitto: no given splitths";
42364
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 41840
diff changeset
   135
      val thy = Thm.theory_of_thm genth;
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   136
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   137
      (* check if we are a member of splitths - FIXME: quicker and
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   138
      more flexible with discrim net. *)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   139
      fun solve_by_splitth th split =
42364
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 41840
diff changeset
   140
        Thm.biresolution false [(false,split)] 1 th;
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   141
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   142
      fun split th =
42364
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 41840
diff changeset
   143
        (case find_thms_split splitths 1 th of
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 41840
diff changeset
   144
          NONE =>
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 41840
diff changeset
   145
           (writeln (cat_lines
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 41840
diff changeset
   146
            (["th:", Display.string_of_thm_without_context th, "split ths:"] @
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 41840
diff changeset
   147
              map Display.string_of_thm_without_context splitths @ ["\n--"]));
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 41840
diff changeset
   148
            error "splitto: cannot find variable to split on")
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 41840
diff changeset
   149
        | SOME v =>
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 41840
diff changeset
   150
            let
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 41840
diff changeset
   151
              val gt = HOLogic.dest_Trueprop (nth (Thm.prems_of th) 0);
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 41840
diff changeset
   152
              val split_thm = mk_casesplit_goal_thm thy v gt;
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 41840
diff changeset
   153
              val (subthms, expf) = IsaND.fixed_subgoal_thms split_thm;
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 41840
diff changeset
   154
            in
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 41840
diff changeset
   155
              expf (map recsplitf subthms)
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 41840
diff changeset
   156
            end)
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   157
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   158
      and recsplitf th =
42364
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 41840
diff changeset
   159
        (* note: multiple unifiers! we only take the first element,
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 41840
diff changeset
   160
           probably fine -- there is probably only one anyway. *)
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 41840
diff changeset
   161
        (case get_first (Seq.pull o solve_by_splitth th) splitths of
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 41840
diff changeset
   162
          NONE => split th
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 41840
diff changeset
   163
        | SOME (solved_th, more) => solved_th);
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   164
    in
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   165
      recsplitf genth
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   166
    end;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   167
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
   168
end;