src/ZF/add_ind_def.ML
author paulson
Fri Apr 10 13:15:28 1998 +0200 (1998-04-10 ago)
changeset 4804 02b7c759159b
parent 4352 7ac9f3e8a97d
child 4860 3692eb8a6cdb
permissions -rw-r--r--
Fixed bug in inductive sections to allow disjunctive premises;
added tracing flag trace_induct
clasohm@1461
     1
(*  Title:      ZF/add_ind_def.ML
lcp@516
     2
    ID:         $Id$
clasohm@1461
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
lcp@516
     4
    Copyright   1994  University of Cambridge
lcp@516
     5
lcp@516
     6
Fixedpoint definition module -- for Inductive/Coinductive Definitions
lcp@516
     7
lcp@516
     8
Features:
lcp@516
     9
* least or greatest fixedpoints
lcp@516
    10
* user-specified product and sum constructions
lcp@516
    11
* mutually recursive definitions
lcp@516
    12
* definitions involving arbitrary monotone operators
lcp@516
    13
* automatically proves introduction and elimination rules
lcp@516
    14
lcp@516
    15
The recursive sets must *already* be declared as constants in parent theory!
lcp@516
    16
lcp@516
    17
  Introduction rules have the form
lcp@516
    18
  [| ti:M(Sj), ..., P(x), ... |] ==> t: Sk |]
lcp@516
    19
  where M is some monotone operator (usually the identity)
lcp@516
    20
  P(x) is any (non-conjunctive) side condition on the free variables
lcp@516
    21
  ti, t are any terms
lcp@516
    22
  Sj, Sk are two of the sets being defined in mutual recursion
lcp@516
    23
lcp@516
    24
Sums are used only for mutual recursion;
lcp@516
    25
Products are used only to derive "streamlined" induction rules for relations
lcp@516
    26
*)
lcp@516
    27
clasohm@1461
    28
signature FP =          (** Description of a fixed point operator **)
lcp@516
    29
  sig
clasohm@1461
    30
  val oper      : term                  (*fixed point operator*)
clasohm@1461
    31
  val bnd_mono  : term                  (*monotonicity predicate*)
clasohm@1461
    32
  val bnd_monoI : thm                   (*intro rule for bnd_mono*)
clasohm@1461
    33
  val subs      : thm                   (*subset theorem for fp*)
clasohm@1461
    34
  val Tarski    : thm                   (*Tarski's fixed point theorem*)
clasohm@1461
    35
  val induct    : thm                   (*induction/coinduction rule*)
lcp@516
    36
  end;
lcp@516
    37
clasohm@1461
    38
signature SU =                  (** Description of a disjoint sum **)
lcp@516
    39
  sig
clasohm@1461
    40
  val sum       : term                  (*disjoint sum operator*)
clasohm@1461
    41
  val inl       : term                  (*left injection*)
clasohm@1461
    42
  val inr       : term                  (*right injection*)
clasohm@1461
    43
  val elim      : term                  (*case operator*)
clasohm@1461
    44
  val case_inl  : thm                   (*inl equality rule for case*)
clasohm@1461
    45
  val case_inr  : thm                   (*inr equality rule for case*)
clasohm@1461
    46
  val inl_iff   : thm                   (*injectivity of inl, using <->*)
clasohm@1461
    47
  val inr_iff   : thm                   (*injectivity of inr, using <->*)
clasohm@1461
    48
  val distinct  : thm                   (*distinctness of inl, inr using <->*)
clasohm@1461
    49
  val distinct' : thm                   (*distinctness of inr, inl using <->*)
clasohm@1461
    50
  val free_SEs  : thm list              (*elim rules for SU, and pair_iff!*)
lcp@516
    51
  end;
lcp@516
    52
lcp@516
    53
signature ADD_INDUCTIVE_DEF =
lcp@516
    54
  sig 
lcp@727
    55
  val add_fp_def_i : term list * term * term list -> theory -> theory
lcp@516
    56
  val add_constructs_def :
lcp@516
    57
        string list * ((string*typ*mixfix) * 
lcp@516
    58
                       string * term list * term list) list list ->
lcp@516
    59
        theory -> theory
lcp@516
    60
  end;
lcp@516
    61
lcp@516
    62
lcp@516
    63
lcp@516
    64
(*Declares functions to add fixedpoint/constructor defs to a theory*)
lcp@516
    65
functor Add_inductive_def_Fun 
paulson@1735
    66
    (structure Fp: FP and Pr : PR and CP: CARTPROD and Su : SU)
paulson@1735
    67
    : ADD_INDUCTIVE_DEF =
lcp@516
    68
struct
lcp@516
    69
open Logic Ind_Syntax;
lcp@516
    70
lcp@516
    71
(*internal version*)
lcp@727
    72
fun add_fp_def_i (rec_tms, dom_sum, intr_tms) thy = 
lcp@516
    73
  let
paulson@2871
    74
    val dummy = (*has essential ancestors?*)
paulson@2871
    75
	require_thy thy "Inductive" "(co)inductive definitions" 
paulson@2871
    76
lcp@516
    77
    val sign = sign_of thy;
lcp@516
    78
lcp@516
    79
    (*recT and rec_params should agree for all mutually recursive components*)
lcp@750
    80
    val rec_hds = map head_of rec_tms;
lcp@516
    81
paulson@2871
    82
    val dummy = assert_all is_Const rec_hds
clasohm@1461
    83
            (fn t => "Recursive set not previously declared as constant: " ^ 
clasohm@1461
    84
                     Sign.string_of_term sign t);
lcp@750
    85
lcp@750
    86
    (*Now we know they are all Consts, so get their names, type and params*)
lcp@750
    87
    val rec_names = map (#1 o dest_Const) rec_hds
lcp@750
    88
    and (Const(_,recT),rec_params) = strip_comb (hd rec_tms);
lcp@516
    89
wenzelm@3939
    90
    val rec_base_names = map Sign.base_name rec_names;
wenzelm@3925
    91
    val dummy = assert_all Syntax.is_identifier rec_base_names
wenzelm@3925
    92
      (fn a => "Base name of recursive set not an identifier: " ^ a);
lcp@516
    93
lcp@516
    94
    local (*Checking the introduction rules*)
lcp@516
    95
      val intr_sets = map (#2 o rule_concl_msg sign) intr_tms;
lcp@516
    96
      fun intr_ok set =
clasohm@1461
    97
          case head_of set of Const(a,recT) => a mem rec_names | _ => false;
lcp@516
    98
    in
paulson@2871
    99
      val dummy =  assert_all intr_ok intr_sets
clasohm@1461
   100
         (fn t => "Conclusion of rule does not name a recursive set: " ^ 
clasohm@1461
   101
                  Sign.string_of_term sign t);
lcp@516
   102
    end;
lcp@516
   103
paulson@2871
   104
    val dummy = assert_all is_Free rec_params
clasohm@1461
   105
        (fn t => "Param in recursion term not a free variable: " ^
clasohm@1461
   106
                 Sign.string_of_term sign t);
lcp@516
   107
lcp@516
   108
    (*** Construct the lfp definition ***)
lcp@516
   109
    val mk_variant = variant (foldr add_term_names (intr_tms,[]));
lcp@516
   110
lcp@516
   111
    val z' = mk_variant"z" and X' = mk_variant"X" and w' = mk_variant"w";
lcp@516
   112
lcp@516
   113
    fun dest_tprop (Const("Trueprop",_) $ P) = P
lcp@516
   114
      | dest_tprop Q = error ("Ill-formed premise of introduction rule: " ^ 
clasohm@1461
   115
                              Sign.string_of_term sign Q);
lcp@516
   116
lcp@516
   117
    (*Makes a disjunct from an introduction rule*)
lcp@516
   118
    fun lfp_part intr = (*quantify over rule's free vars except parameters*)
lcp@516
   119
      let val prems = map dest_tprop (strip_imp_prems intr)
paulson@2871
   120
          val dummy = seq (fn rec_hd => seq (chk_prem rec_hd) prems) rec_hds
clasohm@1461
   121
          val exfrees = term_frees intr \\ rec_params
paulson@4352
   122
          val zeq = FOLogic.mk_eq (Free(z',iT), #1 (rule_concl intr))
paulson@4352
   123
      in foldr FOLogic.mk_exists
paulson@4352
   124
	       (exfrees, fold_bal (app FOLogic.conj) (zeq::prems)) 
paulson@4352
   125
      end;
lcp@516
   126
lcp@516
   127
    (*The Part(A,h) terms -- compose injections to make h*)
clasohm@1461
   128
    fun mk_Part (Bound 0) = Free(X',iT) (*no mutual rec, no Part needed*)
lcp@516
   129
      | mk_Part h         = Part_const $ Free(X',iT) $ Abs(w',iT,h);
lcp@516
   130
lcp@516
   131
    (*Access to balanced disjoint sums via injections*)
lcp@516
   132
    val parts = 
clasohm@1461
   133
        map mk_Part (accesses_bal (ap Su.inl, ap Su.inr, Bound 0) 
clasohm@1461
   134
                                  (length rec_tms));
lcp@516
   135
lcp@516
   136
    (*replace each set by the corresponding Part(A,h)*)
lcp@516
   137
    val part_intrs = map (subst_free (rec_tms ~~ parts) o lfp_part) intr_tms;
lcp@516
   138
lcp@516
   139
    val lfp_abs = absfree(X', iT, 
paulson@4352
   140
                     mk_Collect(z', dom_sum, 
paulson@4352
   141
				fold_bal (app FOLogic.disj) part_intrs));
lcp@516
   142
lcp@516
   143
    val lfp_rhs = Fp.oper $ dom_sum $ lfp_abs
lcp@516
   144
paulson@2871
   145
    val dummy = seq (fn rec_hd => deny (rec_hd occs lfp_rhs) 
clasohm@1461
   146
                               "Illegal occurrence of recursion operator")
clasohm@1461
   147
             rec_hds;
lcp@516
   148
lcp@516
   149
    (*** Make the new theory ***)
lcp@516
   150
lcp@516
   151
    (*A key definition:
lcp@516
   152
      If no mutual recursion then it equals the one recursive set.
lcp@516
   153
      If mutual recursion then it differs from all the recursive sets. *)
wenzelm@3925
   154
    val big_rec_base_name = space_implode "_" rec_base_names;
wenzelm@4235
   155
    val big_rec_name = Sign.intern_const sign big_rec_base_name;
lcp@516
   156
lcp@516
   157
    (*Big_rec... is the union of the mutually recursive sets*)
lcp@516
   158
    val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params);
lcp@516
   159
lcp@516
   160
    (*The individual sets must already be declared*)
lcp@516
   161
    val axpairs = map mk_defpair 
clasohm@1461
   162
          ((big_rec_tm, lfp_rhs) ::
clasohm@1461
   163
           (case parts of 
clasohm@1461
   164
               [_] => []                        (*no mutual recursion*)
clasohm@1461
   165
             | _ => rec_tms ~~          (*define the sets as Parts*)
clasohm@1461
   166
                    map (subst_atomic [(Free(X',iT),big_rec_tm)]) parts));
lcp@516
   167
paulson@4804
   168
    (*tracing: print the fixedpoint definition*)
paulson@4804
   169
    val _ = if !Ind_Syntax.trace then
paulson@4804
   170
		seq (writeln o Sign.string_of_term sign o #2) axpairs
paulson@4804
   171
            else ()
paulson@4804
   172
wenzelm@4027
   173
  in  thy |> PureThy.add_store_defs_i axpairs  end
lcp@516
   174
lcp@516
   175
lcp@516
   176
(*Expects the recursive sets to have been defined already.
lcp@516
   177
  con_ty_lists specifies the constructors in the form (name,prems,mixfix) *)
wenzelm@3925
   178
fun add_constructs_def (rec_base_names, con_ty_lists) thy = 
lcp@516
   179
  let
paulson@2871
   180
    val dummy = (*has essential ancestors?*)
wenzelm@3925
   181
      require_thy thy "Datatype" "(co)datatype definitions";
wenzelm@3925
   182
wenzelm@3925
   183
    val sign = sign_of thy;
wenzelm@3925
   184
    val full_name = Sign.full_name sign;
paulson@2871
   185
paulson@2871
   186
    val dummy = writeln"  Defining the constructor functions...";
clasohm@1461
   187
    val case_name = "f";                (*name for case variables*)
lcp@516
   188
wenzelm@3925
   189
lcp@516
   190
    (** Define the constructors **)
lcp@516
   191
lcp@516
   192
    (*The empty tuple is 0*)
lcp@516
   193
    fun mk_tuple [] = Const("0",iT)
lcp@516
   194
      | mk_tuple args = foldr1 (app Pr.pair) args;
lcp@516
   195
wenzelm@3925
   196
    fun mk_inject n k u = access_bal (ap Su.inl, ap Su.inr, u) n k;
lcp@516
   197
wenzelm@3925
   198
    val npart = length rec_base_names;       (*total # of mutually recursive parts*)
lcp@516
   199
lcp@516
   200
    (*Make constructor definition; kpart is # of this mutually recursive part*)
lcp@516
   201
    fun mk_con_defs (kpart, con_ty_list) = 
clasohm@1461
   202
      let val ncon = length con_ty_list    (*number of constructors*)
clasohm@1461
   203
          fun mk_def (((id,T,syn), name, args, prems), kcon) =
clasohm@1461
   204
                (*kcon is index of constructor*)
wenzelm@3925
   205
              mk_defpair (list_comb (Const (full_name name, T), args),
clasohm@1461
   206
                          mk_inject npart kpart
clasohm@1461
   207
                          (mk_inject ncon kcon (mk_tuple args)))
paulson@2266
   208
      in  ListPair.map mk_def (con_ty_list, 1 upto ncon)  end;
lcp@516
   209
lcp@516
   210
    (** Define the case operator **)
lcp@516
   211
lcp@516
   212
    (*Combine split terms using case; yields the case operator for one part*)
lcp@516
   213
    fun call_case case_list = 
paulson@1735
   214
      let fun call_f (free,[]) = Abs("null", iT, free)
paulson@2033
   215
            | call_f (free,args) =
paulson@1735
   216
                  CP.ap_split (foldr1 CP.mk_prod (map (#2 o dest_Free) args))
paulson@2033
   217
                              Ind_Syntax.iT 
paulson@2033
   218
                              free 
lcp@516
   219
      in  fold_bal (app Su.elim) (map call_f case_list)  end;
lcp@516
   220
lcp@516
   221
    (** Generating function variables for the case definition
clasohm@1461
   222
        Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **)
lcp@516
   223
lcp@516
   224
    (*Treatment of a single constructor*)
wenzelm@3925
   225
    fun add_case (((_, T, _), name, args, prems), (opno, cases)) =
wenzelm@3925
   226
      if Syntax.is_identifier name then
wenzelm@3925
   227
        (opno, (Free (case_name ^ "_" ^ name, T), args) :: cases)
wenzelm@3925
   228
      else
wenzelm@3925
   229
        (opno + 1, (Free (case_name ^ "_op_" ^ string_of_int opno, T), args) :: cases);
lcp@516
   230
lcp@516
   231
    (*Treatment of a list of constructors, for one part*)
wenzelm@3925
   232
    fun add_case_list (con_ty_list, (opno, case_lists)) =
wenzelm@3925
   233
      let val (opno', case_list) = foldr add_case (con_ty_list, (opno, []))
wenzelm@3925
   234
      in (opno', case_list :: case_lists) end;
lcp@516
   235
lcp@516
   236
    (*Treatment of all parts*)
lcp@516
   237
    val (_, case_lists) = foldr add_case_list (con_ty_lists, (1,[]));
lcp@516
   238
lcp@516
   239
    val big_case_typ = flat (map (map (#2 o #1)) con_ty_lists) ---> (iT-->iT);
lcp@516
   240
wenzelm@3925
   241
    val big_rec_base_name = space_implode "_" rec_base_names;
wenzelm@3925
   242
    val big_case_base_name = big_rec_base_name ^ "_case";
wenzelm@3925
   243
    val big_case_name = full_name big_case_base_name;
lcp@516
   244
lcp@516
   245
    (*The list of all the function variables*)
lcp@516
   246
    val big_case_args = flat (map (map #1) case_lists);
lcp@516
   247
wenzelm@3925
   248
    val big_case_tm =
wenzelm@3925
   249
      list_comb (Const (big_case_name, big_case_typ), big_case_args); 
lcp@516
   250
wenzelm@3925
   251
    val big_case_def = mk_defpair
wenzelm@3925
   252
      (big_case_tm, fold_bal (app Su.elim) (map call_case case_lists));
lcp@516
   253
wenzelm@3925
   254
wenzelm@3925
   255
    (* Build the new theory *)
lcp@516
   256
lcp@516
   257
    val const_decs =
wenzelm@3925
   258
      (big_case_base_name, big_case_typ, NoSyn) :: map #1 (flat con_ty_lists);
lcp@516
   259
lcp@516
   260
    val axpairs =
wenzelm@3925
   261
      big_case_def :: flat (ListPair.map mk_con_defs (1 upto npart, con_ty_lists));
lcp@516
   262
wenzelm@3925
   263
  in
wenzelm@3925
   264
    thy
wenzelm@3925
   265
    |> Theory.add_consts_i const_decs
wenzelm@4027
   266
    |> PureThy.add_store_defs_i axpairs
wenzelm@3925
   267
  end;
wenzelm@3925
   268
wenzelm@3925
   269
lcp@516
   270
end;