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