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