src/ZF/Tools/induct_tacs.ML
author skalberg
Thu Mar 03 12:43:01 2005 +0100 (2005-03-03)
changeset 15570 8d8c70b41bab
parent 15531 08c8dad8e399
child 15574 b1d1b5bfc464
permissions -rw-r--r--
Move towards standard functions.
     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 * Args.src list -> thmref * Args.src list ->
    17     (thmref * Args.src list) list -> (thmref * 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 exception Find_tname of string
    87 
    88 fun find_tname var Bi =
    89   let fun mk_pair (Const("op :",_) $ Free (v,_) $ A) =
    90              (v, #1 (dest_Const (head_of A)))
    91         | mk_pair _ = raise Match
    92       val pairs = List.mapPartial (try (mk_pair o FOLogic.dest_Trueprop))
    93           (#2 (strip_context Bi))
    94   in case assoc (pairs, var) of
    95        NONE => raise Find_tname ("Cannot determine datatype of " ^ quote var)
    96      | SOME t => t
    97   end;
    98 
    99 (** generic exhaustion and induction tactic for datatypes
   100     Differences from HOL:
   101       (1) no checking if the induction var occurs in premises, since it always
   102           appears in one of them, and it's hard to check for other occurrences
   103       (2) exhaustion works for VARIABLES in the premises, not general terms
   104 **)
   105 
   106 fun exhaust_induct_tac exh var i state =
   107   let
   108     val (_, _, Bi, _) = dest_state (state, i)
   109     val {sign, ...} = rep_thm state
   110     val tn = find_tname var Bi
   111     val rule =
   112         if exh then #exhaustion (datatype_info_sg sign tn)
   113                else #induct  (datatype_info_sg sign tn)
   114     val (Const("op :",_) $ Var(ixn,_) $ _) =
   115         (case prems_of rule of
   116              [] => error "induction is not available for this datatype"
   117            | major::_ => FOLogic.dest_Trueprop major)
   118   in
   119     Tactic.eres_inst_tac' [(ixn, var)] rule i state
   120   end
   121   handle Find_tname msg =>
   122             if exh then (*try boolean case analysis instead*)
   123 		case_tac var i state
   124             else error msg;
   125 
   126 val exhaust_tac = exhaust_induct_tac true;
   127 val induct_tac = exhaust_induct_tac false;
   128 
   129 
   130 (**** declare non-datatype as datatype ****)
   131 
   132 fun rep_datatype_i elim induct case_eqns recursor_eqns thy =
   133   let
   134     val sign = sign_of thy;
   135 
   136     (*analyze the LHS of a case equation to get a constructor*)
   137     fun const_of (Const("op =", _) $ (_ $ c) $ _) = c
   138       | const_of eqn = error ("Ill-formed case equation: " ^
   139                               Sign.string_of_term sign eqn);
   140 
   141     val constructors =
   142         map (head_of o const_of o FOLogic.dest_Trueprop o
   143              #prop o rep_thm) case_eqns;
   144 
   145     val Const ("op :", _) $ _ $ data =
   146         FOLogic.dest_Trueprop (hd (prems_of elim));
   147 
   148     val Const(big_rec_name, _) = head_of data;
   149 
   150     val simps = case_eqns @ recursor_eqns;
   151 
   152     val dt_info =
   153           {inductive = true,
   154            constructors = constructors,
   155            rec_rewrites = recursor_eqns,
   156            case_rewrites = case_eqns,
   157            induct = induct,
   158            mutual_induct = TrueI,  (*No need for mutual induction*)
   159            exhaustion = elim};
   160 
   161     val con_info =
   162           {big_rec_name = big_rec_name,
   163            constructors = constructors,
   164               (*let primrec handle definition by cases*)
   165            free_iffs = [],  (*thus we expect the necessary freeness rewrites
   166                               to be in the simpset already, as is the case for
   167                               Nat and disjoint sum*)
   168            rec_rewrites = (case recursor_eqns of
   169                                [] => case_eqns | _ => recursor_eqns)};
   170 
   171     (*associate with each constructor the datatype name and rewrites*)
   172     val con_pairs = map (fn c => (#1 (dest_Const c), con_info)) constructors
   173 
   174   in
   175       thy |> Theory.add_path (Sign.base_name big_rec_name)
   176           |> (#1 o PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])])
   177           |> DatatypesData.put
   178               (Symtab.update
   179                ((big_rec_name, dt_info), DatatypesData.get thy))
   180           |> ConstructorsData.put
   181                (Library.foldr Symtab.update (con_pairs, ConstructorsData.get thy))
   182           |> Theory.parent_path
   183   end;
   184 
   185 fun rep_datatype raw_elim raw_induct raw_case_eqns raw_recursor_eqns thy =
   186   let
   187     val (thy', (((elims, inducts), case_eqns), recursor_eqns)) = thy
   188       |> IsarThy.apply_theorems [raw_elim]
   189       |>>> IsarThy.apply_theorems [raw_induct]
   190       |>>> IsarThy.apply_theorems raw_case_eqns
   191       |>>> IsarThy.apply_theorems raw_recursor_eqns;
   192   in
   193     thy' |> rep_datatype_i (PureThy.single_thm "elimination" elims)
   194       (PureThy.single_thm "induction" inducts) case_eqns recursor_eqns
   195   end;
   196 
   197 
   198 (* theory setup *)
   199 
   200 val setup =
   201  [DatatypesData.init,
   202   ConstructorsData.init,
   203   Method.add_methods
   204     [("induct_tac", Method.goal_args Args.name induct_tac,
   205       "induct_tac emulation (dynamic instantiation!)"),
   206      ("case_tac", Method.goal_args Args.name exhaust_tac,
   207       "datatype case_tac emulation (dynamic instantiation!)")]];
   208 
   209 
   210 (* outer syntax *)
   211 
   212 local structure P = OuterParse and K = OuterSyntax.Keyword in
   213 
   214 val rep_datatype_decl =
   215   (P.$$$ "elimination" |-- P.!!! P.xthm) --
   216   (P.$$$ "induction" |-- P.!!! P.xthm) --
   217   (P.$$$ "case_eqns" |-- P.!!! P.xthms1) --
   218   Scan.optional (P.$$$ "recursor_eqns" |-- P.!!! P.xthms1) []
   219   >> (fn (((x, y), z), w) => rep_datatype x y z w);
   220 
   221 val rep_datatypeP =
   222   OuterSyntax.command "rep_datatype" "represent existing set inductively" K.thy_decl
   223     (rep_datatype_decl >> Toplevel.theory);
   224 
   225 val _ = OuterSyntax.add_keywords ["elimination", "induction", "case_eqns", "recursor_eqns"];
   226 val _ = OuterSyntax.add_parsers [rep_datatypeP];
   227 
   228 end;
   229 
   230 end;
   231 
   232 
   233 val exhaust_tac = DatatypeTactics.exhaust_tac;
   234 val induct_tac  = DatatypeTactics.induct_tac;