src/ZF/Tools/induct_tacs.ML
author wenzelm
Sat May 15 21:50:05 2010 +0200 (2010-05-15)
changeset 36945 9bec62c10714
parent 36610 bafd82950e24
child 36954 ef698bd61057
permissions -rw-r--r--
less pervasive names from structure Thm;
     1 (*  Title:      ZF/Tools/induct_tacs.ML
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   1994  University of Cambridge
     4 
     5 Induction and exhaustion tactics for Isabelle/ZF.  The theory
     6 information needed to support them (and to support primrec).  Also a
     7 function to install other sets as if they were datatypes.
     8 *)
     9 
    10 signature DATATYPE_TACTICS =
    11 sig
    12   val induct_tac: Proof.context -> string -> int -> tactic
    13   val exhaust_tac: Proof.context -> string -> int -> tactic
    14   val rep_datatype_i: thm -> thm -> thm list -> thm list -> theory -> theory
    15   val rep_datatype: Facts.ref * Attrib.src list -> Facts.ref * Attrib.src list ->
    16     (Facts.ref * Attrib.src list) list -> (Facts.ref * Attrib.src list) list -> theory -> theory
    17   val setup: theory -> theory
    18 end;
    19 
    20 
    21 (** Datatype information, e.g. associated theorems **)
    22 
    23 type datatype_info =
    24   {inductive: bool,             (*true if inductive, not coinductive*)
    25    constructors : term list,    (*the constructors, as Consts*)
    26    rec_rewrites : thm list,     (*recursor equations*)
    27    case_rewrites : thm list,    (*case equations*)
    28    induct : thm,
    29    mutual_induct : thm,
    30    exhaustion : thm};
    31 
    32 structure DatatypesData = Theory_Data
    33 (
    34   type T = datatype_info Symtab.table;
    35   val empty = Symtab.empty;
    36   val extend = I;
    37   fun merge data : T = Symtab.merge (K true) data;
    38 );
    39 
    40 
    41 
    42 (** Constructor information: needed to map constructors to datatypes **)
    43 
    44 type constructor_info =
    45   {big_rec_name : string,     (*name of the mutually recursive set*)
    46    constructors : term list,  (*the constructors, as Consts*)
    47    free_iffs    : thm list,   (*freeness simprules*)
    48    rec_rewrites : thm list};  (*recursor equations*)
    49 
    50 
    51 structure ConstructorsData = Theory_Data
    52 (
    53   type T = constructor_info Symtab.table
    54   val empty = Symtab.empty
    55   val extend = I
    56   fun merge data = Symtab.merge (K true) data;
    57 );
    58 
    59 structure DatatypeTactics : DATATYPE_TACTICS =
    60 struct
    61 
    62 fun datatype_info thy name =
    63   (case Symtab.lookup (DatatypesData.get thy) name of
    64     SOME info => info
    65   | NONE => error ("Unknown datatype " ^ quote name));
    66 
    67 
    68 (*Given a variable, find the inductive set associated it in the assumptions*)
    69 exception Find_tname of string
    70 
    71 fun find_tname var Bi =
    72   let fun mk_pair (Const(@{const_name mem},_) $ Free (v,_) $ A) =
    73              (v, #1 (dest_Const (head_of A)))
    74         | mk_pair _ = raise Match
    75       val pairs = map_filter (try (mk_pair o FOLogic.dest_Trueprop))
    76           (#2 (OldGoals.strip_context Bi))
    77   in case AList.lookup (op =) pairs var of
    78        NONE => raise Find_tname ("Cannot determine datatype of " ^ quote var)
    79      | SOME t => t
    80   end;
    81 
    82 (** generic exhaustion and induction tactic for datatypes
    83     Differences from HOL:
    84       (1) no checking if the induction var occurs in premises, since it always
    85           appears in one of them, and it's hard to check for other occurrences
    86       (2) exhaustion works for VARIABLES in the premises, not general terms
    87 **)
    88 
    89 fun exhaust_induct_tac exh ctxt var i state =
    90   let
    91     val thy = ProofContext.theory_of ctxt
    92     val (_, _, Bi, _) = Thm.dest_state (state, i)
    93     val tn = find_tname var Bi
    94     val rule =
    95         if exh then #exhaustion (datatype_info thy tn)
    96                else #induct  (datatype_info thy tn)
    97     val (Const(@{const_name mem},_) $ Var(ixn,_) $ _) =
    98         (case prems_of rule of
    99              [] => error "induction is not available for this datatype"
   100            | major::_ => FOLogic.dest_Trueprop major)
   101   in
   102     eres_inst_tac ctxt [(ixn, var)] rule i state
   103   end
   104   handle Find_tname msg =>
   105             if exh then (*try boolean case analysis instead*)
   106                 case_tac ctxt var i state
   107             else error msg;
   108 
   109 val exhaust_tac = exhaust_induct_tac true;
   110 val induct_tac = exhaust_induct_tac false;
   111 
   112 
   113 (**** declare non-datatype as datatype ****)
   114 
   115 fun rep_datatype_i elim induct case_eqns recursor_eqns thy =
   116   let
   117     (*analyze the LHS of a case equation to get a constructor*)
   118     fun const_of (Const("op =", _) $ (_ $ c) $ _) = c
   119       | const_of eqn = error ("Ill-formed case equation: " ^
   120                               Syntax.string_of_term_global thy eqn);
   121 
   122     val constructors =
   123         map (head_of o const_of o FOLogic.dest_Trueprop o
   124              #prop o rep_thm) case_eqns;
   125 
   126     val Const (@{const_name mem}, _) $ _ $ data =
   127         FOLogic.dest_Trueprop (hd (prems_of elim));
   128 
   129     val Const(big_rec_name, _) = head_of data;
   130 
   131     val simps = case_eqns @ recursor_eqns;
   132 
   133     val dt_info =
   134           {inductive = true,
   135            constructors = constructors,
   136            rec_rewrites = recursor_eqns,
   137            case_rewrites = case_eqns,
   138            induct = induct,
   139            mutual_induct = @{thm TrueI},  (*No need for mutual induction*)
   140            exhaustion = elim};
   141 
   142     val con_info =
   143           {big_rec_name = big_rec_name,
   144            constructors = constructors,
   145               (*let primrec handle definition by cases*)
   146            free_iffs = [],  (*thus we expect the necessary freeness rewrites
   147                               to be in the simpset already, as is the case for
   148                               Nat and disjoint sum*)
   149            rec_rewrites = (case recursor_eqns of
   150                                [] => case_eqns | _ => recursor_eqns)};
   151 
   152     (*associate with each constructor the datatype name and rewrites*)
   153     val con_pairs = map (fn c => (#1 (dest_Const c), con_info)) constructors
   154 
   155   in
   156     thy
   157     |> Sign.add_path (Long_Name.base_name big_rec_name)
   158     |> PureThy.add_thmss [((Binding.name "simps", simps), [Simplifier.simp_add])] |> snd
   159     |> DatatypesData.put (Symtab.update (big_rec_name, dt_info) (DatatypesData.get thy))
   160     |> ConstructorsData.put (fold_rev Symtab.update con_pairs (ConstructorsData.get thy))
   161     |> Sign.parent_path
   162   end;
   163 
   164 fun rep_datatype raw_elim raw_induct raw_case_eqns raw_recursor_eqns thy =
   165   let
   166     val ctxt = ProofContext.init_global thy;
   167     val elim = Facts.the_single "elimination" (Attrib.eval_thms ctxt [raw_elim]);
   168     val induct = Facts.the_single "induction" (Attrib.eval_thms ctxt [raw_induct]);
   169     val case_eqns = Attrib.eval_thms ctxt raw_case_eqns;
   170     val recursor_eqns = Attrib.eval_thms ctxt raw_recursor_eqns;
   171   in rep_datatype_i elim induct case_eqns recursor_eqns thy end;
   172 
   173 
   174 (* theory setup *)
   175 
   176 val setup =
   177   Method.setup @{binding induct_tac}
   178     (Args.goal_spec -- Scan.lift Args.name >>
   179       (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (induct_tac ctxt s)))
   180     "induct_tac emulation (dynamic instantiation!)" #>
   181   Method.setup @{binding case_tac}
   182    (Args.goal_spec -- Scan.lift Args.name >>
   183       (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (exhaust_tac ctxt s)))
   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;