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