src/ZF/Tools/induct_tacs.ML
author wenzelm
Tue Aug 16 13:42:26 2005 +0200 (2005-08-16)
changeset 17057 0934ac31985f
parent 16458 4c6fd0c01d28
child 17223 430edc6b7826
permissions -rw-r--r--
OuterKeyword;
     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) list
    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 assoc (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 |> Theory.add_path (Sign.base_name big_rec_name)
   167           |> (#1 o PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])])
   168           |> DatatypesData.put
   169               (Symtab.update
   170                ((big_rec_name, dt_info), DatatypesData.get thy))
   171           |> ConstructorsData.put
   172                (foldr Symtab.update (ConstructorsData.get thy) con_pairs)
   173           |> Theory.parent_path
   174   end;
   175 
   176 fun rep_datatype raw_elim raw_induct raw_case_eqns raw_recursor_eqns thy =
   177   let
   178     val (thy', (((elims, inducts), case_eqns), recursor_eqns)) = thy
   179       |> IsarThy.apply_theorems [raw_elim]
   180       |>>> IsarThy.apply_theorems [raw_induct]
   181       |>>> IsarThy.apply_theorems raw_case_eqns
   182       |>>> IsarThy.apply_theorems raw_recursor_eqns;
   183   in
   184     thy' |> rep_datatype_i (PureThy.single_thm "elimination" elims)
   185       (PureThy.single_thm "induction" inducts) case_eqns recursor_eqns
   186   end;
   187 
   188 
   189 (* theory setup *)
   190 
   191 val setup =
   192  [DatatypesData.init,
   193   ConstructorsData.init,
   194   Method.add_methods
   195     [("induct_tac", Method.goal_args Args.name induct_tac,
   196       "induct_tac emulation (dynamic instantiation!)"),
   197      ("case_tac", Method.goal_args Args.name exhaust_tac,
   198       "datatype case_tac emulation (dynamic instantiation!)")]];
   199 
   200 
   201 (* outer syntax *)
   202 
   203 local structure P = OuterParse and K = OuterKeyword in
   204 
   205 val rep_datatype_decl =
   206   (P.$$$ "elimination" |-- P.!!! P.xthm) --
   207   (P.$$$ "induction" |-- P.!!! P.xthm) --
   208   (P.$$$ "case_eqns" |-- P.!!! P.xthms1) --
   209   Scan.optional (P.$$$ "recursor_eqns" |-- P.!!! P.xthms1) []
   210   >> (fn (((x, y), z), w) => rep_datatype x y z w);
   211 
   212 val rep_datatypeP =
   213   OuterSyntax.command "rep_datatype" "represent existing set inductively" K.thy_decl
   214     (rep_datatype_decl >> Toplevel.theory);
   215 
   216 val _ = OuterSyntax.add_keywords ["elimination", "induction", "case_eqns", "recursor_eqns"];
   217 val _ = OuterSyntax.add_parsers [rep_datatypeP];
   218 
   219 end;
   220 
   221 end;
   222 
   223 
   224 val exhaust_tac = DatatypeTactics.exhaust_tac;
   225 val induct_tac  = DatatypeTactics.induct_tac;