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;
     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 ctxt var As =
    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)) As
    76       val x =
    77         (case try (dest_Free o Syntax.read_term ctxt) var of
    78           SOME (x, _) => x
    79         | _ => raise Find_tname ("Bad variable " ^ quote var))
    80   in case AList.lookup (op =) pairs x 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 = Proof_Context.theory_of ctxt
    95     val ({context = ctxt', asms, ...}, _) = Subgoal.focus ctxt i state
    96     val tn = find_tname ctxt' var (map term_of asms)
    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(@{const_name IFOL.eq}, _) $ (_ $ 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 Thm.prop_of) case_eqns;
   127 
   128     val Const (@{const_name mem}, _) $ _ $ data =
   129         FOLogic.dest_Trueprop (hd (prems_of elim));
   130 
   131     val Const(big_rec_name, _) = head_of data;
   132 
   133     val simps = case_eqns @ recursor_eqns;
   134 
   135     val dt_info =
   136           {inductive = true,
   137            constructors = constructors,
   138            rec_rewrites = recursor_eqns,
   139            case_rewrites = case_eqns,
   140            induct = induct,
   141            mutual_induct = @{thm TrueI},  (*No need for mutual induction*)
   142            exhaustion = elim};
   143 
   144     val con_info =
   145           {big_rec_name = big_rec_name,
   146            constructors = constructors,
   147               (*let primrec handle definition by cases*)
   148            free_iffs = [],  (*thus we expect the necessary freeness rewrites
   149                               to be in the simpset already, as is the case for
   150                               Nat and disjoint sum*)
   151            rec_rewrites = (case recursor_eqns of
   152                                [] => case_eqns | _ => recursor_eqns)};
   153 
   154     (*associate with each constructor the datatype name and rewrites*)
   155     val con_pairs = map (fn c => (#1 (dest_Const c), con_info)) constructors
   156 
   157   in
   158     thy
   159     |> Sign.add_path (Long_Name.base_name big_rec_name)
   160     |> Global_Theory.add_thmss [((Binding.name "simps", simps), [Simplifier.simp_add])] |> snd
   161     |> DatatypesData.put (Symtab.update (big_rec_name, dt_info) (DatatypesData.get thy))
   162     |> ConstructorsData.put (fold_rev Symtab.update con_pairs (ConstructorsData.get thy))
   163     |> Sign.parent_path
   164   end;
   165 
   166 fun rep_datatype raw_elim raw_induct raw_case_eqns raw_recursor_eqns thy =
   167   let
   168     val ctxt = Proof_Context.init_global thy;
   169     val elim = Facts.the_single ("elimination", Position.none) (Attrib.eval_thms ctxt [raw_elim]);
   170     val induct = Facts.the_single ("induction", Position.none) (Attrib.eval_thms ctxt [raw_induct]);
   171     val case_eqns = Attrib.eval_thms ctxt raw_case_eqns;
   172     val recursor_eqns = Attrib.eval_thms ctxt raw_recursor_eqns;
   173   in rep_datatype_i elim induct case_eqns recursor_eqns thy end;
   174 
   175 
   176 (* theory setup *)
   177 
   178 val setup =
   179   Method.setup @{binding induct_tac}
   180     (Args.goal_spec -- Scan.lift Args.name >>
   181       (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (induct_tac ctxt s)))
   182     "induct_tac emulation (dynamic instantiation!)" #>
   183   Method.setup @{binding case_tac}
   184    (Args.goal_spec -- Scan.lift Args.name >>
   185       (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (exhaust_tac ctxt s)))
   186     "datatype case_tac emulation (dynamic instantiation!)";
   187 
   188 
   189 (* outer syntax *)
   190 
   191 val _ =
   192   Outer_Syntax.command @{command_spec "rep_datatype"} "represent existing set inductively"
   193     ((@{keyword "elimination"} |-- Parse.!!! Parse_Spec.xthm) --
   194      (@{keyword "induction"} |-- Parse.!!! Parse_Spec.xthm) --
   195      (@{keyword "case_eqns"} |-- Parse.!!! Parse_Spec.xthms1) --
   196      Scan.optional (@{keyword "recursor_eqns"} |-- Parse.!!! Parse_Spec.xthms1) []
   197      >> (fn (((x, y), z), w) => Toplevel.theory (rep_datatype x y z w)));
   198 
   199 end;
   200 
   201 val exhaust_tac = DatatypeTactics.exhaust_tac;
   202 val induct_tac  = DatatypeTactics.induct_tac;