src/ZF/Tools/induct_tacs.ML
author wenzelm
Wed Nov 28 00:46:26 2001 +0100 (2001-11-28)
changeset 12311 ce5f9e61c037
parent 12204 98115606ee42
child 14153 76a6ba67bd15
permissions -rw-r--r--
theory data: removed obsolete finish method;
     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: xstring * Args.src list -> xstring * Args.src list ->
    17     (xstring * Args.src list) list -> (xstring * Args.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 DatatypesArgs =
    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 prep_ext = I;
    41   val merge: T * T -> T = Symtab.merge (K true);
    42 
    43   fun print sg tab =
    44     Pretty.writeln (Pretty.strs ("datatypes:" ::
    45       map #1 (Sign.cond_extern_table sg Sign.typeK tab)));
    46   end;
    47 
    48 structure DatatypesData = TheoryDataFun(DatatypesArgs);
    49 
    50 
    51 (** Constructor information: needed to map constructors to datatypes **)
    52 
    53 type constructor_info =
    54   {big_rec_name : string,     (*name of the mutually recursive set*)
    55    constructors : term list,  (*the constructors, as Consts*)
    56    free_iffs    : thm list,   (*freeness simprules*)
    57    rec_rewrites : thm list};  (*recursor equations*)
    58 
    59 
    60 structure ConstructorsArgs =
    61 struct
    62   val name = "ZF/constructors"
    63   type T = constructor_info Symtab.table
    64 
    65   val empty = Symtab.empty
    66   val copy = I;
    67   val prep_ext = I
    68   val merge: T * T -> T = Symtab.merge (K true)
    69 
    70   fun print sg tab = ()   (*nothing extra to print*)
    71 end;
    72 
    73 structure ConstructorsData = TheoryDataFun(ConstructorsArgs);
    74 
    75 
    76 structure DatatypeTactics : DATATYPE_TACTICS =
    77 struct
    78 
    79 fun datatype_info_sg sign name =
    80   (case Symtab.lookup (DatatypesData.get_sg sign, name) of
    81     Some info => info
    82   | None => error ("Unknown datatype " ^ quote name));
    83 
    84 
    85 (*Given a variable, find the inductive set associated it in the assumptions*)
    86 fun find_tname var Bi =
    87   let fun mk_pair (Const("op :",_) $ Free (v,_) $ A) =
    88              (v, #1 (dest_Const (head_of A)))
    89         | mk_pair _ = raise Match
    90       val pairs = mapfilter (try (mk_pair o FOLogic.dest_Trueprop))
    91           (#2 (strip_context Bi))
    92   in case assoc (pairs, var) of
    93        None => error ("Cannot determine datatype of " ^ quote var)
    94      | Some t => t
    95   end;
    96 
    97 (** generic exhaustion and induction tactic for datatypes
    98     Differences from HOL:
    99       (1) no checking if the induction var occurs in premises, since it always
   100           appears in one of them, and it's hard to check for other occurrences
   101       (2) exhaustion works for VARIABLES in the premises, not general terms
   102 **)
   103 
   104 fun exhaust_induct_tac exh var i state =
   105   let
   106     val (_, _, Bi, _) = dest_state (state, i)
   107     val {sign, ...} = rep_thm state
   108     val tn = find_tname var Bi
   109     val rule =
   110         if exh then #exhaustion (datatype_info_sg sign tn)
   111                else #induct  (datatype_info_sg sign tn)
   112     val (Const("op :",_) $ Var(ixn,_) $ _) =
   113         (case prems_of rule of
   114              [] => error "induction is not available for this datatype"
   115            | major::_ => FOLogic.dest_Trueprop major)
   116     val ind_vname = Syntax.string_of_vname ixn
   117     val vname' = (*delete leading question mark*)
   118         String.substring (ind_vname, 1, size ind_vname-1)
   119   in
   120     eres_inst_tac [(vname',var)] rule i state
   121   end;
   122 
   123 val exhaust_tac = exhaust_induct_tac true;
   124 val induct_tac = exhaust_induct_tac false;
   125 
   126 
   127 
   128 (**** declare non-datatype as datatype ****)
   129 
   130 fun rep_datatype_i elim induct case_eqns recursor_eqns thy =
   131   let
   132     val sign = sign_of thy;
   133 
   134     (*analyze the LHS of a case equation to get a constructor*)
   135     fun const_of (Const("op =", _) $ (_ $ c) $ _) = c
   136       | const_of eqn = error ("Ill-formed case equation: " ^
   137                               Sign.string_of_term sign eqn);
   138 
   139     val constructors =
   140         map (head_of o const_of o FOLogic.dest_Trueprop o
   141              #prop o rep_thm) case_eqns;
   142 
   143     val Const ("op :", _) $ _ $ data =
   144         FOLogic.dest_Trueprop (hd (prems_of elim));
   145 
   146     val Const(big_rec_name, _) = head_of data;
   147 
   148     val simps = case_eqns @ recursor_eqns;
   149 
   150     val dt_info =
   151           {inductive = true,
   152            constructors = constructors,
   153            rec_rewrites = recursor_eqns,
   154            case_rewrites = case_eqns,
   155            induct = induct,
   156            mutual_induct = TrueI,  (*No need for mutual induction*)
   157            exhaustion = elim};
   158 
   159     val con_info =
   160           {big_rec_name = big_rec_name,
   161            constructors = constructors,
   162               (*let primrec handle definition by cases*)
   163            free_iffs = [],  (*thus we expect the necessary freeness rewrites
   164                               to be in the simpset already, as is the case for
   165                               Nat and disjoint sum*)
   166            rec_rewrites = (case recursor_eqns of
   167                                [] => case_eqns | _ => recursor_eqns)};
   168 
   169     (*associate with each constructor the datatype name and rewrites*)
   170     val con_pairs = map (fn c => (#1 (dest_Const c), con_info)) constructors
   171 
   172   in
   173       thy |> Theory.add_path (Sign.base_name big_rec_name)
   174           |> (#1 o PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])])
   175           |> DatatypesData.put
   176               (Symtab.update
   177                ((big_rec_name, dt_info), DatatypesData.get thy))
   178           |> ConstructorsData.put
   179                (foldr Symtab.update (con_pairs, ConstructorsData.get thy))
   180           |> Theory.parent_path
   181   end;
   182 
   183 fun rep_datatype raw_elim raw_induct raw_case_eqns raw_recursor_eqns thy =
   184   let
   185     val (thy', (((elims, inducts), case_eqns), recursor_eqns)) = thy
   186       |> IsarThy.apply_theorems [raw_elim]
   187       |>>> IsarThy.apply_theorems [raw_induct]
   188       |>>> IsarThy.apply_theorems raw_case_eqns
   189       |>>> IsarThy.apply_theorems raw_recursor_eqns;
   190   in
   191     thy' |> rep_datatype_i (PureThy.single_thm "elimination" elims)
   192       (PureThy.single_thm "induction" inducts) case_eqns recursor_eqns
   193   end;
   194 
   195 
   196 (* theory setup *)
   197 
   198 val setup =
   199  [DatatypesData.init,
   200   ConstructorsData.init,
   201   Method.add_methods
   202     [("induct_tac", Method.goal_args Args.name induct_tac,
   203       "induct_tac emulation (dynamic instantiation!)"),
   204      ("case_tac", Method.goal_args Args.name case_tac,
   205       "case_tac emulation (dynamic instantiation!)")]];
   206 
   207 
   208 (* outer syntax *)
   209 
   210 local structure P = OuterParse and K = OuterSyntax.Keyword in
   211 
   212 val rep_datatype_decl =
   213   (P.$$$ "elimination" |-- P.!!! P.xthm) --
   214   (P.$$$ "induction" |-- P.!!! P.xthm) --
   215   (P.$$$ "case_eqns" |-- P.!!! P.xthms1) --
   216   Scan.optional (P.$$$ "recursor_eqns" |-- P.!!! P.xthms1) []
   217   >> (fn (((x, y), z), w) => rep_datatype x y z w);
   218 
   219 val rep_datatypeP =
   220   OuterSyntax.command "rep_datatype" "represent existing set inductively" K.thy_decl
   221     (rep_datatype_decl >> Toplevel.theory);
   222 
   223 val _ = OuterSyntax.add_keywords ["elimination", "induction", "case_eqns", "recursor_eqns"];
   224 val _ = OuterSyntax.add_parsers [rep_datatypeP];
   225 
   226 end;
   227 
   228 end;
   229 
   230 
   231 val exhaust_tac = DatatypeTactics.exhaust_tac;
   232 val induct_tac  = DatatypeTactics.induct_tac;