src/ZF/Tools/induct_tacs.ML
author wenzelm
Sat Oct 06 16:50:04 2007 +0200 (2007-10-06)
changeset 24867 e5b55d7be9bb
parent 24826 78e6a3cea367
child 26336 a0e2b706ce73
permissions -rw-r--r--
simplified interfaces for outer syntax;
paulson@6070
     1
(*  Title:      ZF/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
wenzelm@12204
     6
Induction and exhaustion tactics for Isabelle/ZF.  The theory
wenzelm@12204
     7
information needed to support them (and to support primrec).  Also a
wenzelm@12204
     8
function to install other sets as if they were datatypes.
paulson@6065
     9
*)
paulson@6065
    10
paulson@6065
    11
signature DATATYPE_TACTICS =
paulson@6065
    12
sig
wenzelm@12204
    13
  val induct_tac: string -> int -> tactic
wenzelm@12204
    14
  val exhaust_tac: string -> int -> tactic
wenzelm@12204
    15
  val rep_datatype_i: thm -> thm -> thm list -> thm list -> theory -> theory
wenzelm@15703
    16
  val rep_datatype: thmref * Attrib.src list -> thmref * Attrib.src list ->
wenzelm@15703
    17
    (thmref * Attrib.src list) list -> (thmref * Attrib.src list) list -> theory -> theory
wenzelm@18708
    18
  val setup: theory -> theory
paulson@6065
    19
end;
paulson@6065
    20
paulson@6065
    21
paulson@6070
    22
(** Datatype information, e.g. associated theorems **)
paulson@6070
    23
paulson@6070
    24
type datatype_info =
wenzelm@12175
    25
  {inductive: bool,             (*true if inductive, not coinductive*)
paulson@6070
    26
   constructors : term list,    (*the constructors, as Consts*)
paulson@6070
    27
   rec_rewrites : thm list,     (*recursor equations*)
paulson@6070
    28
   case_rewrites : thm list,    (*case equations*)
paulson@6070
    29
   induct : thm,
paulson@6070
    30
   mutual_induct : thm,
paulson@6070
    31
   exhaustion : thm};
paulson@6070
    32
wenzelm@16458
    33
structure DatatypesData = TheoryDataFun
wenzelm@22846
    34
(
paulson@6070
    35
  type T = datatype_info Symtab.table;
paulson@6070
    36
  val empty = Symtab.empty;
wenzelm@6556
    37
  val copy = I;
wenzelm@16458
    38
  val extend = I;
wenzelm@16458
    39
  fun merge _ tabs : T = Symtab.merge (K true) tabs;
wenzelm@22846
    40
);
paulson@6070
    41
paulson@6070
    42
paulson@6070
    43
paulson@6070
    44
(** Constructor information: needed to map constructors to datatypes **)
paulson@6070
    45
paulson@6070
    46
type constructor_info =
paulson@6070
    47
  {big_rec_name : string,     (*name of the mutually recursive set*)
paulson@6070
    48
   constructors : term list,  (*the constructors, as Consts*)
paulson@6141
    49
   free_iffs    : thm list,   (*freeness simprules*)
paulson@6070
    50
   rec_rewrites : thm list};  (*recursor equations*)
paulson@6070
    51
paulson@6070
    52
wenzelm@16458
    53
structure ConstructorsData = TheoryDataFun
wenzelm@22846
    54
(
paulson@6070
    55
  type T = constructor_info Symtab.table
paulson@6070
    56
  val empty = Symtab.empty
wenzelm@6556
    57
  val copy = I;
wenzelm@16458
    58
  val extend = I
wenzelm@16458
    59
  fun merge _ tabs: T = Symtab.merge (K true) tabs;
wenzelm@22846
    60
);
paulson@6070
    61
paulson@6065
    62
structure DatatypeTactics : DATATYPE_TACTICS =
paulson@6065
    63
struct
paulson@6065
    64
wenzelm@16458
    65
fun datatype_info thy name =
wenzelm@17412
    66
  (case Symtab.lookup (DatatypesData.get thy) name of
skalberg@15531
    67
    SOME info => info
skalberg@15531
    68
  | NONE => error ("Unknown datatype " ^ quote name));
paulson@6065
    69
paulson@6065
    70
paulson@6065
    71
(*Given a variable, find the inductive set associated it in the assumptions*)
paulson@14153
    72
exception Find_tname of string
paulson@14153
    73
paulson@6065
    74
fun find_tname var Bi =
wenzelm@24826
    75
  let fun mk_pair (Const(@{const_name mem},_) $ Free (v,_) $ A) =
paulson@6065
    76
             (v, #1 (dest_Const (head_of A)))
wenzelm@12175
    77
        | mk_pair _ = raise Match
skalberg@15570
    78
      val pairs = List.mapPartial (try (mk_pair o FOLogic.dest_Trueprop))
wenzelm@12175
    79
          (#2 (strip_context Bi))
haftmann@17314
    80
  in case AList.lookup (op =) pairs var of
skalberg@15531
    81
       NONE => raise Find_tname ("Cannot determine datatype of " ^ quote var)
skalberg@15531
    82
     | SOME t => t
paulson@6065
    83
  end;
paulson@6065
    84
wenzelm@12175
    85
(** generic exhaustion and induction tactic for datatypes
wenzelm@12175
    86
    Differences from HOL:
paulson@6065
    87
      (1) no checking if the induction var occurs in premises, since it always
paulson@6065
    88
          appears in one of them, and it's hard to check for other occurrences
paulson@6065
    89
      (2) exhaustion works for VARIABLES in the premises, not general terms
paulson@6065
    90
**)
paulson@6065
    91
paulson@6065
    92
fun exhaust_induct_tac exh var i state =
paulson@6065
    93
  let
paulson@6065
    94
    val (_, _, Bi, _) = dest_state (state, i)
wenzelm@16458
    95
    val thy = Thm.theory_of_thm state
paulson@6065
    96
    val tn = find_tname var Bi
wenzelm@12175
    97
    val rule =
wenzelm@16458
    98
        if exh then #exhaustion (datatype_info thy tn)
wenzelm@16458
    99
               else #induct  (datatype_info thy tn)
wenzelm@24826
   100
    val (Const(@{const_name mem},_) $ Var(ixn,_) $ _) =
paulson@6112
   101
        (case prems_of rule of
wenzelm@12175
   102
             [] => error "induction is not available for this datatype"
wenzelm@12175
   103
           | major::_ => FOLogic.dest_Trueprop major)
paulson@6065
   104
  in
berghofe@15462
   105
    Tactic.eres_inst_tac' [(ixn, var)] rule i state
paulson@14153
   106
  end
paulson@14153
   107
  handle Find_tname msg =>
paulson@14153
   108
            if exh then (*try boolean case analysis instead*)
wenzelm@16458
   109
                case_tac var i state
paulson@14153
   110
            else error msg;
paulson@6065
   111
paulson@6065
   112
val exhaust_tac = exhaust_induct_tac true;
paulson@6065
   113
val induct_tac = exhaust_induct_tac false;
paulson@6065
   114
paulson@6070
   115
paulson@6070
   116
(**** declare non-datatype as datatype ****)
paulson@6070
   117
paulson@6070
   118
fun rep_datatype_i elim induct case_eqns recursor_eqns thy =
paulson@6070
   119
  let
paulson@6070
   120
    (*analyze the LHS of a case equation to get a constructor*)
paulson@6070
   121
    fun const_of (Const("op =", _) $ (_ $ c) $ _) = c
paulson@6070
   122
      | const_of eqn = error ("Ill-formed case equation: " ^
wenzelm@16458
   123
                              Sign.string_of_term thy eqn);
paulson@6070
   124
paulson@6070
   125
    val constructors =
wenzelm@12175
   126
        map (head_of o const_of o FOLogic.dest_Trueprop o
wenzelm@12175
   127
             #prop o rep_thm) case_eqns;
paulson@6070
   128
wenzelm@24826
   129
    val Const (@{const_name mem}, _) $ _ $ data =
wenzelm@12175
   130
        FOLogic.dest_Trueprop (hd (prems_of elim));
wenzelm@12175
   131
paulson@6112
   132
    val Const(big_rec_name, _) = head_of data;
paulson@6112
   133
paulson@6070
   134
    val simps = case_eqns @ recursor_eqns;
paulson@6070
   135
paulson@6070
   136
    val dt_info =
wenzelm@12175
   137
          {inductive = true,
wenzelm@12175
   138
           constructors = constructors,
wenzelm@12175
   139
           rec_rewrites = recursor_eqns,
wenzelm@12175
   140
           case_rewrites = case_eqns,
wenzelm@12175
   141
           induct = induct,
wenzelm@12175
   142
           mutual_induct = TrueI,  (*No need for mutual induction*)
wenzelm@12175
   143
           exhaustion = elim};
paulson@6070
   144
paulson@6070
   145
    val con_info =
wenzelm@12175
   146
          {big_rec_name = big_rec_name,
wenzelm@12175
   147
           constructors = constructors,
wenzelm@12175
   148
              (*let primrec handle definition by cases*)
wenzelm@12175
   149
           free_iffs = [],  (*thus we expect the necessary freeness rewrites
wenzelm@12175
   150
                              to be in the simpset already, as is the case for
wenzelm@12175
   151
                              Nat and disjoint sum*)
wenzelm@12175
   152
           rec_rewrites = (case recursor_eqns of
wenzelm@12175
   153
                               [] => case_eqns | _ => recursor_eqns)};
paulson@6070
   154
paulson@6070
   155
    (*associate with each constructor the datatype name and rewrites*)
paulson@6070
   156
    val con_pairs = map (fn c => (#1 (dest_Const c), con_info)) constructors
paulson@6070
   157
paulson@6070
   158
  in
wenzelm@17223
   159
    thy
wenzelm@24712
   160
    |> Sign.add_path (Sign.base_name big_rec_name)
wenzelm@18728
   161
    |> PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add])] |> snd
wenzelm@17412
   162
    |> DatatypesData.put (Symtab.update (big_rec_name, dt_info) (DatatypesData.get thy))
wenzelm@17412
   163
    |> ConstructorsData.put (fold_rev Symtab.update con_pairs (ConstructorsData.get thy))
wenzelm@24712
   164
    |> Sign.parent_path
wenzelm@12204
   165
  end;
paulson@6065
   166
wenzelm@12204
   167
fun rep_datatype raw_elim raw_induct raw_case_eqns raw_recursor_eqns thy =
wenzelm@24725
   168
  let
wenzelm@24725
   169
    val ctxt = ProofContext.init thy;
wenzelm@24725
   170
    val elim = PureThy.single_thm "elimination" (Attrib.eval_thms ctxt [raw_elim]);
wenzelm@24725
   171
    val induct = PureThy.single_thm "induction" (Attrib.eval_thms ctxt [raw_induct]);
wenzelm@24725
   172
    val case_eqns = Attrib.eval_thms ctxt raw_case_eqns;
wenzelm@24725
   173
    val recursor_eqns = Attrib.eval_thms ctxt raw_recursor_eqns;
wenzelm@24725
   174
  in rep_datatype_i elim induct case_eqns recursor_eqns thy end;
wenzelm@12175
   175
wenzelm@12204
   176
wenzelm@12204
   177
(* theory setup *)
wenzelm@12204
   178
wenzelm@12204
   179
val setup =
wenzelm@12175
   180
  Method.add_methods
wenzelm@12175
   181
    [("induct_tac", Method.goal_args Args.name induct_tac,
wenzelm@12175
   182
      "induct_tac emulation (dynamic instantiation!)"),
paulson@14153
   183
     ("case_tac", Method.goal_args Args.name exhaust_tac,
wenzelm@22846
   184
      "datatype case_tac emulation (dynamic instantiation!)")];
wenzelm@12204
   185
wenzelm@12204
   186
wenzelm@12204
   187
(* outer syntax *)
wenzelm@12204
   188
wenzelm@17057
   189
local structure P = OuterParse and K = OuterKeyword in
wenzelm@12204
   190
wenzelm@24867
   191
val _ = OuterSyntax.keywords ["elimination", "induction", "case_eqns", "recursor_eqns"];
wenzelm@24867
   192
wenzelm@12204
   193
val rep_datatype_decl =
wenzelm@22101
   194
  (P.$$$ "elimination" |-- P.!!! SpecParse.xthm) --
wenzelm@22101
   195
  (P.$$$ "induction" |-- P.!!! SpecParse.xthm) --
wenzelm@22101
   196
  (P.$$$ "case_eqns" |-- P.!!! SpecParse.xthms1) --
wenzelm@22101
   197
  Scan.optional (P.$$$ "recursor_eqns" |-- P.!!! SpecParse.xthms1) []
wenzelm@12204
   198
  >> (fn (((x, y), z), w) => rep_datatype x y z w);
wenzelm@12204
   199
wenzelm@24867
   200
val _ =
wenzelm@12204
   201
  OuterSyntax.command "rep_datatype" "represent existing set inductively" K.thy_decl
wenzelm@12204
   202
    (rep_datatype_decl >> Toplevel.theory);
wenzelm@12204
   203
wenzelm@12204
   204
end;
wenzelm@12204
   205
wenzelm@12204
   206
end;
wenzelm@12204
   207
wenzelm@12204
   208
wenzelm@12204
   209
val exhaust_tac = DatatypeTactics.exhaust_tac;
wenzelm@12204
   210
val induct_tac  = DatatypeTactics.induct_tac;