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