src/ZF/Tools/induct_tacs.ML
author wenzelm
Sun Mar 08 17:26:14 2009 +0100 (2009-03-08)
changeset 30364 577edc39b501
parent 30280 eb98b49ef835
child 30541 9f168bdc468a
permissions -rw-r--r--
moved basic algebra of long names from structure NameSpace to Long_Name;
     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: Proof.context -> string -> int -> tactic
    14   val exhaust_tac: Proof.context -> string -> int -> tactic
    15   val rep_datatype_i: thm -> thm -> thm list -> thm list -> theory -> theory
    16   val rep_datatype: Facts.ref * Attrib.src list -> Facts.ref * Attrib.src list ->
    17     (Facts.ref * Attrib.src list) list -> (Facts.ref * 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(@{const_name mem},_) $ 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 ctxt var i state =
    93   let
    94     val thy = ProofContext.theory_of ctxt
    95     val (_, _, Bi, _) = dest_state (state, i)
    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(@{const_name mem},_) $ 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     eres_inst_tac ctxt [(ixn, var)] rule i state
   106   end
   107   handle Find_tname msg =>
   108             if exh then (*try boolean case analysis instead*)
   109                 case_tac ctxt 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                               Syntax.string_of_term_global 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 (@{const_name mem}, _) $ _ $ 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 (Long_Name.base_name big_rec_name)
   161     |> PureThy.add_thmss [((Binding.name "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   let
   169     val ctxt = ProofContext.init thy;
   170     val elim = Facts.the_single "elimination" (Attrib.eval_thms ctxt [raw_elim]);
   171     val induct = Facts.the_single "induction" (Attrib.eval_thms ctxt [raw_induct]);
   172     val case_eqns = Attrib.eval_thms ctxt raw_case_eqns;
   173     val recursor_eqns = Attrib.eval_thms ctxt raw_recursor_eqns;
   174   in rep_datatype_i elim induct case_eqns recursor_eqns thy end;
   175 
   176 
   177 (* theory setup *)
   178 
   179 val setup =
   180   Method.add_methods
   181     [("induct_tac", Method.goal_args_ctxt Args.name induct_tac,
   182       "induct_tac emulation (dynamic instantiation!)"),
   183      ("case_tac", Method.goal_args_ctxt Args.name exhaust_tac,
   184       "datatype case_tac emulation (dynamic instantiation!)")];
   185 
   186 
   187 (* outer syntax *)
   188 
   189 local structure P = OuterParse and K = OuterKeyword in
   190 
   191 val _ = List.app OuterKeyword.keyword ["elimination", "induction", "case_eqns", "recursor_eqns"];
   192 
   193 val rep_datatype_decl =
   194   (P.$$$ "elimination" |-- P.!!! SpecParse.xthm) --
   195   (P.$$$ "induction" |-- P.!!! SpecParse.xthm) --
   196   (P.$$$ "case_eqns" |-- P.!!! SpecParse.xthms1) --
   197   Scan.optional (P.$$$ "recursor_eqns" |-- P.!!! SpecParse.xthms1) []
   198   >> (fn (((x, y), z), w) => rep_datatype x y z w);
   199 
   200 val _ =
   201   OuterSyntax.command "rep_datatype" "represent existing set inductively" K.thy_decl
   202     (rep_datatype_decl >> Toplevel.theory);
   203 
   204 end;
   205 
   206 end;
   207 
   208 
   209 val exhaust_tac = DatatypeTactics.exhaust_tac;
   210 val induct_tac  = DatatypeTactics.induct_tac;