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