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