src/ZF/Tools/induct_tacs.ML
author wenzelm
Mon Jun 28 21:48:36 1999 +0200 (1999-06-28)
changeset 6851 526c0b90bcef
parent 6556 daa00919502b
child 6970 ac37a8fcaad1
permissions -rw-r--r--
cond_extern_table;
     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 copy = I;
    41   val prep_ext = I;
    42   val merge: T * T -> T = Symtab.merge (K true);
    43 
    44   fun print sg tab =
    45     Pretty.writeln (Pretty.strs ("datatypes:" ::
    46       map #1 (Sign.cond_extern_table sg Sign.typeK tab)));
    47   end;
    48 
    49 structure DatatypesData = TheoryDataFun(DatatypesArgs);
    50 
    51 
    52 (** Constructor information: needed to map constructors to datatypes **)
    53 
    54 type constructor_info =
    55   {big_rec_name : string,     (*name of the mutually recursive set*)
    56    constructors : term list,  (*the constructors, as Consts*)
    57    free_iffs    : thm list,   (*freeness simprules*)
    58    rec_rewrites : thm list};  (*recursor equations*)
    59 
    60 
    61 structure ConstructorsArgs =
    62 struct
    63   val name = "ZF/constructors"
    64   type T = constructor_info Symtab.table
    65 
    66   val empty = Symtab.empty
    67   val copy = I;
    68   val prep_ext = I
    69   val merge: T * T -> T = Symtab.merge (K true)
    70 
    71   fun print sg tab = ()   (*nothing extra to print*)
    72 end;
    73 
    74 structure ConstructorsData = TheoryDataFun(ConstructorsArgs);
    75 
    76 val setup_datatypes = [DatatypesData.init, ConstructorsData.init];
    77 
    78 
    79 
    80 structure DatatypeTactics : DATATYPE_TACTICS =
    81 struct
    82 
    83 fun datatype_info_sg sign name =
    84   (case Symtab.lookup (DatatypesData.get_sg sign, name) of
    85     Some info => info
    86   | None => error ("Unknown datatype " ^ quote name));
    87 
    88 
    89 (*Given a variable, find the inductive set associated it in the assumptions*)
    90 fun find_tname var Bi =
    91   let fun mk_pair (Const("op :",_) $ Free (v,_) $ A) = 
    92              (v, #1 (dest_Const (head_of A)))
    93 	| mk_pair _ = raise Match
    94       val pairs = mapfilter (try (mk_pair o FOLogic.dest_Trueprop))
    95 	  (#2 (strip_context Bi))
    96   in case assoc (pairs, var) of
    97        None => error ("Cannot determine datatype of " ^ quote var)
    98      | Some t => t
    99   end;
   100 
   101 (** generic exhaustion and induction tactic for datatypes 
   102     Differences from HOL: 
   103       (1) no checking if the induction var occurs in premises, since it always
   104           appears in one of them, and it's hard to check for other occurrences
   105       (2) exhaustion works for VARIABLES in the premises, not general terms
   106 **)
   107 
   108 fun exhaust_induct_tac exh var i state =
   109   let
   110     val (_, _, Bi, _) = dest_state (state, i)
   111     val {sign, ...} = rep_thm state
   112     val tn = find_tname var Bi
   113     val rule = 
   114 	if exh then #exhaustion (datatype_info_sg sign tn)
   115 	       else #induct  (datatype_info_sg sign tn)
   116     val (Const("op :",_) $ Var(ixn,_) $ _) = 
   117         (case prems_of rule of
   118 	     [] => error "induction is not available for this datatype"
   119 	   | major::_ => FOLogic.dest_Trueprop major)
   120     val ind_vname = Syntax.string_of_vname ixn
   121     val vname' = (*delete leading question mark*)
   122 	String.substring (ind_vname, 1, size ind_vname-1)
   123   in
   124     eres_inst_tac [(vname',var)] rule i state
   125   end;
   126 
   127 val exhaust_tac = exhaust_induct_tac true;
   128 val induct_tac = exhaust_induct_tac false;
   129 
   130 
   131 
   132 (**** declare non-datatype as datatype ****)
   133 
   134 fun rep_datatype_i elim induct case_eqns recursor_eqns thy =
   135   let
   136     val sign = sign_of thy;
   137 
   138     (*analyze the LHS of a case equation to get a constructor*)
   139     fun const_of (Const("op =", _) $ (_ $ c) $ _) = c
   140       | const_of eqn = error ("Ill-formed case equation: " ^
   141 			      Sign.string_of_term sign eqn);
   142 
   143     val constructors =
   144 	map (head_of o const_of o FOLogic.dest_Trueprop o
   145 	     #prop o rep_thm) case_eqns;
   146 
   147     val Const ("op :", _) $ _ $ data =
   148 	FOLogic.dest_Trueprop (hd (prems_of elim));	
   149     
   150     val Const(big_rec_name, _) = head_of data;
   151 
   152     val simps = case_eqns @ recursor_eqns;
   153 
   154     val dt_info =
   155 	  {inductive = true,
   156 	   constructors = constructors,
   157 	   rec_rewrites = recursor_eqns,
   158 	   case_rewrites = case_eqns,
   159 	   induct = induct,
   160 	   mutual_induct = TrueI,  (*No need for mutual induction*)
   161 	   exhaustion = elim};
   162 
   163     val con_info =
   164 	  {big_rec_name = big_rec_name,
   165 	   constructors = constructors,
   166 	      (*let primrec handle definition by cases*)
   167 	   free_iffs = [],  (*thus we expect the necessary freeness rewrites
   168 			      to be in the simpset already, as is the case for
   169 			      Nat and disjoint sum*)
   170 	   rec_rewrites = (case recursor_eqns of
   171 			       [] => case_eqns | _ => recursor_eqns)};
   172 
   173     (*associate with each constructor the datatype name and rewrites*)
   174     val con_pairs = map (fn c => (#1 (dest_Const c), con_info)) constructors
   175 
   176   in
   177       thy |> Theory.add_path (Sign.base_name big_rec_name)
   178 	  |> PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])]
   179 	  |> DatatypesData.put 
   180 	      (Symtab.update
   181 	       ((big_rec_name, dt_info), DatatypesData.get thy)) 
   182 	  |> ConstructorsData.put
   183 	       (foldr Symtab.update (con_pairs, ConstructorsData.get thy))
   184 	  |> Theory.parent_path
   185   end
   186   handle _ => error "Failure in rep_datatype";
   187 
   188 end;
   189 
   190 
   191 val exhaust_tac = DatatypeTactics.exhaust_tac;
   192 val induct_tac  = DatatypeTactics.induct_tac;