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