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