src/ZF/Tools/induct_tacs.ML
author wenzelm
Fri Jan 19 22:08:08 2007 +0100 (2007-01-19)
changeset 22101 6d13239d5f52
parent 21350 6e58289b6685
child 22846 fb79144af9a3
permissions -rw-r--r--
moved parts of OuterParse to SpecParse;
     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 (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.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 AList.lookup (op =) 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     |> PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add])] |> snd
   169     |> DatatypesData.put (Symtab.update (big_rec_name, dt_info) (DatatypesData.get thy))
   170     |> ConstructorsData.put (fold_rev Symtab.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   thy
   176   |> IsarCmd.apply_theorems [raw_elim]
   177   ||>> IsarCmd.apply_theorems [raw_induct]
   178   ||>> IsarCmd.apply_theorems raw_case_eqns
   179   ||>> IsarCmd.apply_theorems raw_recursor_eqns
   180   |-> (fn (((elims, inducts), case_eqns), recursor_eqns) =>
   181           rep_datatype_i (PureThy.single_thm "elimination" elims)
   182             (PureThy.single_thm "induction" inducts) case_eqns recursor_eqns);
   183 
   184 
   185 (* theory setup *)
   186 
   187 val setup =
   188  (DatatypesData.init #>
   189   ConstructorsData.init #>
   190   Method.add_methods
   191     [("induct_tac", Method.goal_args Args.name induct_tac,
   192       "induct_tac emulation (dynamic instantiation!)"),
   193      ("case_tac", Method.goal_args Args.name exhaust_tac,
   194       "datatype case_tac emulation (dynamic instantiation!)")]);
   195 
   196 
   197 (* outer syntax *)
   198 
   199 local structure P = OuterParse and K = OuterKeyword in
   200 
   201 val rep_datatype_decl =
   202   (P.$$$ "elimination" |-- P.!!! SpecParse.xthm) --
   203   (P.$$$ "induction" |-- P.!!! SpecParse.xthm) --
   204   (P.$$$ "case_eqns" |-- P.!!! SpecParse.xthms1) --
   205   Scan.optional (P.$$$ "recursor_eqns" |-- P.!!! SpecParse.xthms1) []
   206   >> (fn (((x, y), z), w) => rep_datatype x y z w);
   207 
   208 val rep_datatypeP =
   209   OuterSyntax.command "rep_datatype" "represent existing set inductively" K.thy_decl
   210     (rep_datatype_decl >> Toplevel.theory);
   211 
   212 val _ = OuterSyntax.add_keywords ["elimination", "induction", "case_eqns", "recursor_eqns"];
   213 val _ = OuterSyntax.add_parsers [rep_datatypeP];
   214 
   215 end;
   216 
   217 end;
   218 
   219 
   220 val exhaust_tac = DatatypeTactics.exhaust_tac;
   221 val induct_tac  = DatatypeTactics.induct_tac;