src/ZF/Tools/induct_tacs.ML
author wenzelm
Tue Feb 25 11:36:04 2014 +0100 (2014-02-25)
changeset 55740 11dd48f84441
parent 46961 5c6955f487e5
child 56231 b98813774a63
permissions -rw-r--r--
more positions;
tuned messages;
paulson@6070
     1
(*  Title:      ZF/Tools/induct_tacs.ML
paulson@6065
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@6065
     3
    Copyright   1994  University of Cambridge
paulson@6065
     4
wenzelm@12204
     5
Induction and exhaustion tactics for Isabelle/ZF.  The theory
wenzelm@12204
     6
information needed to support them (and to support primrec).  Also a
wenzelm@12204
     7
function to install other sets as if they were datatypes.
paulson@6065
     8
*)
paulson@6065
     9
paulson@6065
    10
signature DATATYPE_TACTICS =
paulson@6065
    11
sig
wenzelm@27208
    12
  val induct_tac: Proof.context -> string -> int -> tactic
wenzelm@27208
    13
  val exhaust_tac: Proof.context -> string -> int -> tactic
wenzelm@12204
    14
  val rep_datatype_i: thm -> thm -> thm list -> thm list -> theory -> theory
wenzelm@26336
    15
  val rep_datatype: Facts.ref * Attrib.src list -> Facts.ref * Attrib.src list ->
wenzelm@26336
    16
    (Facts.ref * Attrib.src list) list -> (Facts.ref * Attrib.src list) list -> theory -> theory
wenzelm@18708
    17
  val setup: theory -> theory
paulson@6065
    18
end;
paulson@6065
    19
paulson@6065
    20
paulson@6070
    21
(** Datatype information, e.g. associated theorems **)
paulson@6070
    22
paulson@6070
    23
type datatype_info =
wenzelm@12175
    24
  {inductive: bool,             (*true if inductive, not coinductive*)
paulson@6070
    25
   constructors : term list,    (*the constructors, as Consts*)
paulson@6070
    26
   rec_rewrites : thm list,     (*recursor equations*)
paulson@6070
    27
   case_rewrites : thm list,    (*case equations*)
paulson@6070
    28
   induct : thm,
paulson@6070
    29
   mutual_induct : thm,
paulson@6070
    30
   exhaustion : thm};
paulson@6070
    31
wenzelm@33522
    32
structure DatatypesData = Theory_Data
wenzelm@22846
    33
(
paulson@6070
    34
  type T = datatype_info Symtab.table;
paulson@6070
    35
  val empty = Symtab.empty;
wenzelm@16458
    36
  val extend = I;
wenzelm@33522
    37
  fun merge data : T = Symtab.merge (K true) data;
wenzelm@22846
    38
);
paulson@6070
    39
paulson@6070
    40
paulson@6070
    41
paulson@6070
    42
(** Constructor information: needed to map constructors to datatypes **)
paulson@6070
    43
paulson@6070
    44
type constructor_info =
paulson@6070
    45
  {big_rec_name : string,     (*name of the mutually recursive set*)
paulson@6070
    46
   constructors : term list,  (*the constructors, as Consts*)
paulson@6141
    47
   free_iffs    : thm list,   (*freeness simprules*)
paulson@6070
    48
   rec_rewrites : thm list};  (*recursor equations*)
paulson@6070
    49
paulson@6070
    50
wenzelm@33522
    51
structure ConstructorsData = Theory_Data
wenzelm@22846
    52
(
paulson@6070
    53
  type T = constructor_info Symtab.table
paulson@6070
    54
  val empty = Symtab.empty
wenzelm@16458
    55
  val extend = I
wenzelm@33522
    56
  fun merge data = Symtab.merge (K true) data;
wenzelm@22846
    57
);
paulson@6070
    58
paulson@6065
    59
structure DatatypeTactics : DATATYPE_TACTICS =
paulson@6065
    60
struct
paulson@6065
    61
wenzelm@16458
    62
fun datatype_info thy name =
wenzelm@17412
    63
  (case Symtab.lookup (DatatypesData.get thy) name of
skalberg@15531
    64
    SOME info => info
skalberg@15531
    65
  | NONE => error ("Unknown datatype " ^ quote name));
paulson@6065
    66
paulson@6065
    67
paulson@6065
    68
(*Given a variable, find the inductive set associated it in the assumptions*)
paulson@14153
    69
exception Find_tname of string
paulson@14153
    70
wenzelm@37780
    71
fun find_tname ctxt var As =
wenzelm@24826
    72
  let fun mk_pair (Const(@{const_name mem},_) $ Free (v,_) $ A) =
paulson@6065
    73
             (v, #1 (dest_Const (head_of A)))
wenzelm@12175
    74
        | mk_pair _ = raise Match
wenzelm@37780
    75
      val pairs = map_filter (try (mk_pair o FOLogic.dest_Trueprop)) As
wenzelm@37780
    76
      val x =
wenzelm@37780
    77
        (case try (dest_Free o Syntax.read_term ctxt) var of
wenzelm@37780
    78
          SOME (x, _) => x
wenzelm@37780
    79
        | _ => raise Find_tname ("Bad variable " ^ quote var))
wenzelm@37780
    80
  in case AList.lookup (op =) pairs x 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
wenzelm@27208
    92
fun exhaust_induct_tac exh ctxt var i state =
paulson@6065
    93
  let
wenzelm@42361
    94
    val thy = Proof_Context.theory_of ctxt
wenzelm@37780
    95
    val ({context = ctxt', asms, ...}, _) = Subgoal.focus ctxt i state
wenzelm@37780
    96
    val tn = find_tname ctxt' var (map term_of asms)
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
wenzelm@27239
   105
    eres_inst_tac ctxt [(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@27208
   109
                case_tac ctxt 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*)
wenzelm@41310
   121
    fun const_of (Const(@{const_name IFOL.eq}, _) $ (_ $ c) $ _) = c
paulson@6070
   122
      | const_of eqn = error ("Ill-formed case equation: " ^
wenzelm@26939
   123
                              Syntax.string_of_term_global thy eqn);
paulson@6070
   124
paulson@6070
   125
    val constructors =
wenzelm@44058
   126
        map (head_of o const_of o FOLogic.dest_Trueprop o Thm.prop_of) case_eqns;
paulson@6070
   127
wenzelm@24826
   128
    val Const (@{const_name mem}, _) $ _ $ data =
wenzelm@12175
   129
        FOLogic.dest_Trueprop (hd (prems_of elim));
wenzelm@12175
   130
paulson@6112
   131
    val Const(big_rec_name, _) = head_of data;
paulson@6112
   132
paulson@6070
   133
    val simps = case_eqns @ recursor_eqns;
paulson@6070
   134
paulson@6070
   135
    val dt_info =
wenzelm@12175
   136
          {inductive = true,
wenzelm@12175
   137
           constructors = constructors,
wenzelm@12175
   138
           rec_rewrites = recursor_eqns,
wenzelm@12175
   139
           case_rewrites = case_eqns,
wenzelm@12175
   140
           induct = induct,
wenzelm@35409
   141
           mutual_induct = @{thm TrueI},  (*No need for mutual induction*)
wenzelm@12175
   142
           exhaustion = elim};
paulson@6070
   143
paulson@6070
   144
    val con_info =
wenzelm@12175
   145
          {big_rec_name = big_rec_name,
wenzelm@12175
   146
           constructors = constructors,
wenzelm@12175
   147
              (*let primrec handle definition by cases*)
wenzelm@12175
   148
           free_iffs = [],  (*thus we expect the necessary freeness rewrites
wenzelm@12175
   149
                              to be in the simpset already, as is the case for
wenzelm@12175
   150
                              Nat and disjoint sum*)
wenzelm@12175
   151
           rec_rewrites = (case recursor_eqns of
wenzelm@12175
   152
                               [] => case_eqns | _ => recursor_eqns)};
paulson@6070
   153
paulson@6070
   154
    (*associate with each constructor the datatype name and rewrites*)
paulson@6070
   155
    val con_pairs = map (fn c => (#1 (dest_Const c), con_info)) constructors
paulson@6070
   156
paulson@6070
   157
  in
wenzelm@17223
   158
    thy
wenzelm@30364
   159
    |> Sign.add_path (Long_Name.base_name big_rec_name)
wenzelm@39557
   160
    |> Global_Theory.add_thmss [((Binding.name "simps", simps), [Simplifier.simp_add])] |> snd
wenzelm@17412
   161
    |> DatatypesData.put (Symtab.update (big_rec_name, dt_info) (DatatypesData.get thy))
wenzelm@17412
   162
    |> ConstructorsData.put (fold_rev Symtab.update con_pairs (ConstructorsData.get thy))
wenzelm@24712
   163
    |> Sign.parent_path
wenzelm@12204
   164
  end;
paulson@6065
   165
wenzelm@12204
   166
fun rep_datatype raw_elim raw_induct raw_case_eqns raw_recursor_eqns thy =
wenzelm@24725
   167
  let
wenzelm@42361
   168
    val ctxt = Proof_Context.init_global thy;
wenzelm@55740
   169
    val elim = Facts.the_single ("elimination", Position.none) (Attrib.eval_thms ctxt [raw_elim]);
wenzelm@55740
   170
    val induct = Facts.the_single ("induction", Position.none) (Attrib.eval_thms ctxt [raw_induct]);
wenzelm@24725
   171
    val case_eqns = Attrib.eval_thms ctxt raw_case_eqns;
wenzelm@24725
   172
    val recursor_eqns = Attrib.eval_thms ctxt raw_recursor_eqns;
wenzelm@24725
   173
  in rep_datatype_i elim induct case_eqns recursor_eqns thy end;
wenzelm@12175
   174
wenzelm@12204
   175
wenzelm@12204
   176
(* theory setup *)
wenzelm@12204
   177
wenzelm@12204
   178
val setup =
wenzelm@30541
   179
  Method.setup @{binding induct_tac}
wenzelm@30541
   180
    (Args.goal_spec -- Scan.lift Args.name >>
wenzelm@30541
   181
      (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (induct_tac ctxt s)))
wenzelm@30541
   182
    "induct_tac emulation (dynamic instantiation!)" #>
wenzelm@30541
   183
  Method.setup @{binding case_tac}
wenzelm@30541
   184
   (Args.goal_spec -- Scan.lift Args.name >>
wenzelm@30541
   185
      (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (exhaust_tac ctxt s)))
wenzelm@30541
   186
    "datatype case_tac emulation (dynamic instantiation!)";
wenzelm@12204
   187
wenzelm@12204
   188
wenzelm@12204
   189
(* outer syntax *)
wenzelm@12204
   190
wenzelm@24867
   191
val _ =
wenzelm@46961
   192
  Outer_Syntax.command @{command_spec "rep_datatype"} "represent existing set inductively"
wenzelm@46961
   193
    ((@{keyword "elimination"} |-- Parse.!!! Parse_Spec.xthm) --
wenzelm@46961
   194
     (@{keyword "induction"} |-- Parse.!!! Parse_Spec.xthm) --
wenzelm@46961
   195
     (@{keyword "case_eqns"} |-- Parse.!!! Parse_Spec.xthms1) --
wenzelm@46961
   196
     Scan.optional (@{keyword "recursor_eqns"} |-- Parse.!!! Parse_Spec.xthms1) []
wenzelm@46961
   197
     >> (fn (((x, y), z), w) => Toplevel.theory (rep_datatype x y z w)));
wenzelm@12204
   198
wenzelm@12204
   199
end;
wenzelm@12204
   200
wenzelm@12204
   201
val exhaust_tac = DatatypeTactics.exhaust_tac;
wenzelm@12204
   202
val induct_tac  = DatatypeTactics.induct_tac;