src/ZF/Tools/induct_tacs.ML
author paulson
Wed Jan 06 13:24:33 1999 +0100 (1999-01-06)
changeset 6065 3b4a29166f26
child 6070 032babd0120b
permissions -rw-r--r--
induct_tac and exhaust_tac
paulson@6065
     1
(*  Title:      HOL/Tools/induct_tacs.ML
paulson@6065
     2
    ID:         $Id$
paulson@6065
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@6065
     4
    Copyright   1994  University of Cambridge
paulson@6065
     5
paulson@6065
     6
Induction and exhaustion tactics for Isabelle/ZF
paulson@6065
     7
*)
paulson@6065
     8
paulson@6065
     9
paulson@6065
    10
signature DATATYPE_TACTICS =
paulson@6065
    11
sig
paulson@6065
    12
  val induct_tac : string -> int -> tactic
paulson@6065
    13
  val exhaust_tac : string -> int -> tactic
paulson@6065
    14
end;
paulson@6065
    15
paulson@6065
    16
paulson@6065
    17
structure DatatypeTactics : DATATYPE_TACTICS =
paulson@6065
    18
struct
paulson@6065
    19
paulson@6065
    20
fun datatype_info_sg sign name =
paulson@6065
    21
  (case Symtab.lookup (DatatypesData.get_sg sign, name) of
paulson@6065
    22
    Some info => info
paulson@6065
    23
  | None => error ("Unknown datatype " ^ quote name));
paulson@6065
    24
paulson@6065
    25
paulson@6065
    26
(*Given a variable, find the inductive set associated it in the assumptions*)
paulson@6065
    27
fun find_tname var Bi =
paulson@6065
    28
  let fun mk_pair (Const("op :",_) $ Free (v,_) $ A) = 
paulson@6065
    29
             (v, #1 (dest_Const (head_of A)))
paulson@6065
    30
	| mk_pair _ = raise Match
paulson@6065
    31
      val pairs = mapfilter (try (mk_pair o FOLogic.dest_Trueprop))
paulson@6065
    32
	  (#2 (strip_context Bi))
paulson@6065
    33
  in case assoc (pairs, var) of
paulson@6065
    34
       None => error ("Cannot determine datatype of " ^ quote var)
paulson@6065
    35
     | Some t => t
paulson@6065
    36
  end;
paulson@6065
    37
paulson@6065
    38
(** generic exhaustion and induction tactic for datatypes 
paulson@6065
    39
    Differences from HOL: 
paulson@6065
    40
      (1) no checking if the induction var occurs in premises, since it always
paulson@6065
    41
          appears in one of them, and it's hard to check for other occurrences
paulson@6065
    42
      (2) exhaustion works for VARIABLES in the premises, not general terms
paulson@6065
    43
**)
paulson@6065
    44
paulson@6065
    45
fun exhaust_induct_tac exh var i state =
paulson@6065
    46
  let
paulson@6065
    47
    val (_, _, Bi, _) = dest_state (state, i)
paulson@6065
    48
    val {sign, ...} = rep_thm state
paulson@6065
    49
    val tn = find_tname var Bi
paulson@6065
    50
    val rule = 
paulson@6065
    51
	if exh then #exhaustion (datatype_info_sg sign tn)
paulson@6065
    52
	       else #induct  (datatype_info_sg sign tn)
paulson@6065
    53
    val (Const("op :",_) $ Var(ixn,_) $ _) = 
paulson@6065
    54
	FOLogic.dest_Trueprop (hd (prems_of rule))
paulson@6065
    55
    val ind_vname = Syntax.string_of_vname ixn
paulson@6065
    56
    val vname' = (*delete leading question mark*)
paulson@6065
    57
	String.substring (ind_vname, 1, size ind_vname-1)
paulson@6065
    58
  in
paulson@6065
    59
    eres_inst_tac [(vname',var)] rule i state
paulson@6065
    60
  end;
paulson@6065
    61
paulson@6065
    62
val exhaust_tac = exhaust_induct_tac true;
paulson@6065
    63
val induct_tac = exhaust_induct_tac false;
paulson@6065
    64
paulson@6065
    65
end;
paulson@6065
    66
paulson@6065
    67
paulson@6065
    68
open DatatypeTactics;