src/ZF/Tools/induct_tacs.ML
author wenzelm
Tue Jan 12 13:54:51 1999 +0100 (1999-01-12)
changeset 6092 d9db67970c73
parent 6070 032babd0120b
child 6112 5e4871c5136b
permissions -rw-r--r--
eliminated tthm type and Attribute structure;
     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
     7 
     8 The theory information needed to support them (and to support primrec)
     9 
    10 Also, a function to install other sets as if they were datatypes
    11 *)
    12 
    13 
    14 signature DATATYPE_TACTICS =
    15 sig
    16   val induct_tac : string -> int -> tactic
    17   val exhaust_tac : string -> int -> tactic
    18   val rep_datatype_i : thm -> thm -> thm list -> thm list -> theory -> theory
    19 end;
    20 
    21 
    22 
    23 (** Datatype information, e.g. associated theorems **)
    24 
    25 type datatype_info =
    26   {inductive: bool,		(*true if inductive, not coinductive*)
    27    constructors : term list,    (*the constructors, as Consts*)
    28    rec_rewrites : thm list,     (*recursor equations*)
    29    case_rewrites : thm list,    (*case equations*)
    30    induct : thm,
    31    mutual_induct : thm,
    32    exhaustion : thm};
    33 
    34 structure DatatypesArgs =
    35   struct
    36   val name = "ZF/datatypes";
    37   type T = datatype_info Symtab.table;
    38 
    39   val empty = Symtab.empty;
    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 (Sign.cond_extern sg Sign.typeK o fst) (Symtab.dest 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    rec_rewrites : thm list};  (*recursor equations*)
    57 
    58 
    59 structure ConstructorsArgs =
    60 struct
    61   val name = "ZF/constructors"
    62   type T = constructor_info Symtab.table
    63 
    64   val empty = Symtab.empty
    65   val prep_ext = I
    66   val merge: T * T -> T = Symtab.merge (K true)
    67 
    68   fun print sg tab = ()   (*nothing extra to print*)
    69 end;
    70 
    71 structure ConstructorsData = TheoryDataFun(ConstructorsArgs);
    72 
    73 val setup_datatypes = [DatatypesData.init, ConstructorsData.init];
    74 
    75 
    76 
    77 structure DatatypeTactics : DATATYPE_TACTICS =
    78 struct
    79 
    80 fun datatype_info_sg sign name =
    81   (case Symtab.lookup (DatatypesData.get_sg sign, name) of
    82     Some info => info
    83   | None => error ("Unknown datatype " ^ quote name));
    84 
    85 
    86 (*Given a variable, find the inductive set associated it in the assumptions*)
    87 fun find_tname var Bi =
    88   let fun mk_pair (Const("op :",_) $ Free (v,_) $ A) = 
    89              (v, #1 (dest_Const (head_of A)))
    90 	| mk_pair _ = raise Match
    91       val pairs = mapfilter (try (mk_pair o FOLogic.dest_Trueprop))
    92 	  (#2 (strip_context Bi))
    93   in case assoc (pairs, var) of
    94        None => error ("Cannot determine datatype of " ^ quote var)
    95      | Some t => t
    96   end;
    97 
    98 (** generic exhaustion and induction tactic for datatypes 
    99     Differences from HOL: 
   100       (1) no checking if the induction var occurs in premises, since it always
   101           appears in one of them, and it's hard to check for other occurrences
   102       (2) exhaustion works for VARIABLES in the premises, not general terms
   103 **)
   104 
   105 fun exhaust_induct_tac exh var i state =
   106   let
   107     val (_, _, Bi, _) = dest_state (state, i)
   108     val {sign, ...} = rep_thm state
   109     val tn = find_tname var Bi
   110     val rule = 
   111 	if exh then #exhaustion (datatype_info_sg sign tn)
   112 	       else #induct  (datatype_info_sg sign tn)
   113     val (Const("op :",_) $ Var(ixn,_) $ _) = 
   114 	FOLogic.dest_Trueprop (hd (prems_of rule))
   115     val ind_vname = Syntax.string_of_vname ixn
   116     val vname' = (*delete leading question mark*)
   117 	String.substring (ind_vname, 1, size ind_vname-1)
   118   in
   119     eres_inst_tac [(vname',var)] rule i state
   120   end;
   121 
   122 val exhaust_tac = exhaust_induct_tac true;
   123 val induct_tac = exhaust_induct_tac false;
   124 
   125 
   126 
   127 (**** declare non-datatype as datatype ****)
   128 
   129 fun rep_datatype_i elim induct case_eqns recursor_eqns thy =
   130   let
   131     val sign = sign_of thy;
   132 
   133     (*analyze the LHS of a case equation to get a constructor*)
   134     fun const_of (Const("op =", _) $ (_ $ c) $ _) = c
   135       | const_of eqn = error ("Ill-formed case equation: " ^
   136 			      Sign.string_of_term sign eqn);
   137 
   138     val constructors =
   139 	map (head_of o const_of o FOLogic.dest_Trueprop o
   140 	     #prop o rep_thm) case_eqns;
   141 
   142     val Const ("op :", _) $ _ $ Const(big_rec_name, _) =
   143 	FOLogic.dest_Trueprop (hd (prems_of elim));	
   144     
   145     val simps = case_eqns @ recursor_eqns;
   146 
   147     val dt_info =
   148 	  {inductive = true,
   149 	   constructors = constructors,
   150 	   rec_rewrites = recursor_eqns,
   151 	   case_rewrites = case_eqns,
   152 	   induct = induct,
   153 	   mutual_induct = TrueI,  (*No need for mutual induction*)
   154 	   exhaustion = elim};
   155 
   156     val con_info =
   157 	  {big_rec_name = big_rec_name,
   158 	   constructors = constructors,
   159 	      (*let primrec handle definition by cases*)
   160 	   rec_rewrites = (case recursor_eqns of
   161 			       [] => case_eqns | _ => recursor_eqns)};
   162 
   163     (*associate with each constructor the datatype name and rewrites*)
   164     val con_pairs = map (fn c => (#1 (dest_Const c), con_info)) constructors
   165 
   166   in
   167       thy |> Theory.add_path (Sign.base_name big_rec_name)
   168 	  |> PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])]
   169 	  |> DatatypesData.put 
   170 	      (Symtab.update
   171 	       ((big_rec_name, dt_info), DatatypesData.get thy)) 
   172 	  |> ConstructorsData.put
   173 	       (foldr Symtab.update (con_pairs, ConstructorsData.get thy))
   174 	  |> Theory.parent_path
   175   end
   176   handle _ => error "Failure in rep_datatype";
   177 
   178 end;
   179 
   180 
   181 val exhaust_tac = DatatypeTactics.exhaust_tac;
   182 val induct_tac  = DatatypeTactics.induct_tac;