src/HOL/add_ind_def.ML
author nipkow
Tue Apr 08 10:48:42 1997 +0200 (1997-04-08)
changeset 2919 953a47dc0519
parent 2859 7d640451ae7d
child 2995 84df3b150b67
permissions -rw-r--r--
Dep. on Provers/nat_transitive
clasohm@1465
     1
(*  Title:      HOL/add_ind_def.ML
clasohm@923
     2
    ID:         $Id$
clasohm@1465
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@923
     4
    Copyright   1994  University of Cambridge
clasohm@923
     5
clasohm@923
     6
Fixedpoint definition module -- for Inductive/Coinductive Definitions
clasohm@923
     7
clasohm@923
     8
Features:
clasohm@923
     9
* least or greatest fixedpoints
clasohm@923
    10
* user-specified product and sum constructions
clasohm@923
    11
* mutually recursive definitions
clasohm@923
    12
* definitions involving arbitrary monotone operators
clasohm@923
    13
* automatically proves introduction and elimination rules
clasohm@923
    14
clasohm@923
    15
The recursive sets must *already* be declared as constants in parent theory!
clasohm@923
    16
clasohm@923
    17
  Introduction rules have the form
clasohm@923
    18
  [| ti:M(Sj), ..., P(x), ... |] ==> t: Sk |]
clasohm@923
    19
  where M is some monotone operator (usually the identity)
clasohm@923
    20
  P(x) is any (non-conjunctive) side condition on the free variables
clasohm@923
    21
  ti, t are any terms
clasohm@923
    22
  Sj, Sk are two of the sets being defined in mutual recursion
clasohm@923
    23
clasohm@923
    24
Sums are used only for mutual recursion;
clasohm@923
    25
Products are used only to derive "streamlined" induction rules for relations
clasohm@923
    26
clasohm@923
    27
Nestings of disjoint sum types:
clasohm@923
    28
   (a+(b+c)) for 3,  ((a+b)+(c+d)) for 4,  ((a+b)+(c+(d+e))) for 5,
clasohm@923
    29
   ((a+(b+c))+(d+(e+f))) for 6
clasohm@923
    30
*)
clasohm@923
    31
clasohm@1465
    32
signature FP =          (** Description of a fixed point operator **)
clasohm@923
    33
  sig
paulson@2859
    34
  val checkThy  : theory -> unit   (*signals error if Lfp/Gfp is missing*)
clasohm@1465
    35
  val oper      : string * typ * term -> term   (*fixed point operator*)
paulson@2859
    36
  val Tarski    : thm              (*Tarski's fixed point theorem*)
paulson@2859
    37
  val induct    : thm              (*induction/coinduction rule*)
clasohm@923
    38
  end;
clasohm@923
    39
clasohm@923
    40
clasohm@923
    41
signature ADD_INDUCTIVE_DEF =
clasohm@923
    42
  sig 
clasohm@923
    43
  val add_fp_def_i : term list * term list -> theory -> theory
clasohm@923
    44
  end;
clasohm@923
    45
clasohm@923
    46
clasohm@923
    47
clasohm@923
    48
(*Declares functions to add fixedpoint/constructor defs to a theory*)
clasohm@923
    49
functor Add_inductive_def_Fun (Fp: FP) : ADD_INDUCTIVE_DEF =
clasohm@923
    50
struct
paulson@1397
    51
open Ind_Syntax;
clasohm@923
    52
clasohm@923
    53
(*internal version*)
clasohm@923
    54
fun add_fp_def_i (rec_tms, intr_tms) thy = 
clasohm@923
    55
  let
paulson@2859
    56
    val dummy = Fp.checkThy thy		(*has essential ancestors?*)
paulson@2859
    57
    
clasohm@923
    58
    val sign = sign_of thy;
clasohm@923
    59
lcp@1189
    60
    (*rec_params should agree for all mutually recursive components*)
clasohm@923
    61
    val rec_hds = map head_of rec_tms;
clasohm@923
    62
clasohm@923
    63
    val _ = assert_all is_Const rec_hds
clasohm@1465
    64
            (fn t => "Recursive set not previously declared as constant: " ^ 
clasohm@1465
    65
                     Sign.string_of_term sign t);
clasohm@923
    66
clasohm@923
    67
    (*Now we know they are all Consts, so get their names, type and params*)
clasohm@923
    68
    val rec_names = map (#1 o dest_Const) rec_hds
clasohm@923
    69
    and (Const(_,recT),rec_params) = strip_comb (hd rec_tms);
clasohm@923
    70
clasohm@923
    71
    val _ = assert_all Syntax.is_identifier rec_names
clasohm@923
    72
       (fn a => "Name of recursive set not an identifier: " ^ a);
clasohm@923
    73
clasohm@923
    74
    local (*Checking the introduction rules*)
clasohm@923
    75
      val intr_sets = map (#2 o rule_concl_msg sign) intr_tms;
clasohm@923
    76
      fun intr_ok set =
clasohm@1465
    77
          case head_of set of Const(a,_) => a mem rec_names | _ => false;
clasohm@923
    78
    in
clasohm@923
    79
      val _ =  assert_all intr_ok intr_sets
clasohm@1465
    80
         (fn t => "Conclusion of rule does not name a recursive set: " ^ 
clasohm@1465
    81
                  Sign.string_of_term sign t);
clasohm@923
    82
    end;
clasohm@923
    83
clasohm@923
    84
    val _ = assert_all is_Free rec_params
clasohm@1465
    85
        (fn t => "Param in recursion term not a free variable: " ^
clasohm@1465
    86
                 Sign.string_of_term sign t);
clasohm@923
    87
clasohm@923
    88
    (*** Construct the lfp definition ***)
clasohm@923
    89
    val mk_variant = variant (foldr add_term_names (intr_tms,[]));
clasohm@923
    90
clasohm@923
    91
    val z = mk_variant"z" and X = mk_variant"X" and w = mk_variant"w";
clasohm@923
    92
lcp@1189
    93
    (*Mutual recursion ?? *)
lcp@1189
    94
    val domTs = summands (dest_setT (body_type recT));
clasohm@1465
    95
                (*alternative defn: map (dest_setT o fastype_of) rec_tms *)
clasohm@923
    96
    val dom_sumT = fold_bal mk_sum domTs;
paulson@1397
    97
    val dom_set  = mk_setT dom_sumT;
clasohm@923
    98
clasohm@923
    99
    val freez   = Free(z, dom_sumT)
clasohm@923
   100
    and freeX   = Free(X, dom_set);
clasohm@923
   101
    (*type of w may be any of the domTs*)
clasohm@923
   102
clasohm@923
   103
    fun dest_tprop (Const("Trueprop",_) $ P) = P
clasohm@923
   104
      | dest_tprop Q = error ("Ill-formed premise of introduction rule: " ^ 
clasohm@1465
   105
                              Sign.string_of_term sign Q);
clasohm@923
   106
clasohm@923
   107
    (*Makes a disjunct from an introduction rule*)
clasohm@923
   108
    fun lfp_part intr = (*quantify over rule's free vars except parameters*)
paulson@1397
   109
      let val prems = map dest_tprop (Logic.strip_imp_prems intr)
clasohm@1465
   110
          val _ = seq (fn rec_hd => seq (chk_prem rec_hd) prems) rec_hds
clasohm@1465
   111
          val exfrees = term_frees intr \\ rec_params
clasohm@1465
   112
          val zeq = eq_const dom_sumT $ freez $ (#1 (rule_concl intr))
clasohm@923
   113
      in foldr mk_exists (exfrees, fold_bal (app conj) (zeq::prems)) end;
clasohm@923
   114
clasohm@923
   115
    (*The Part(A,h) terms -- compose injections to make h*)
clasohm@1465
   116
    fun mk_Part (Bound 0, _) = freeX    (*no mutual rec, no Part needed*)
clasohm@923
   117
      | mk_Part (h, domT)    = 
clasohm@1465
   118
          let val goodh = mend_sum_types (h, dom_sumT)
clasohm@923
   119
              and Part_const = 
clasohm@1465
   120
                  Const("Part", [dom_set, domT-->dom_sumT]---> dom_set)
clasohm@923
   121
          in  Part_const $ freeX $ Abs(w,domT,goodh)  end;
clasohm@923
   122
clasohm@923
   123
    (*Access to balanced disjoint sums via injections*)
paulson@2270
   124
    val parts = ListPair.map mk_Part
paulson@2270
   125
                (accesses_bal (ap Inl, ap Inr, Bound 0) (length domTs),
clasohm@1465
   126
                 domTs);
clasohm@923
   127
clasohm@923
   128
    (*replace each set by the corresponding Part(A,h)*)
clasohm@923
   129
    val part_intrs = map (subst_free (rec_tms ~~ parts) o lfp_part) intr_tms;
clasohm@923
   130
clasohm@923
   131
    val lfp_rhs = Fp.oper(X, dom_sumT, 
clasohm@1465
   132
                          mk_Collect(z, dom_sumT, 
clasohm@1465
   133
                                     fold_bal (app disj) part_intrs))
clasohm@923
   134
clasohm@923
   135
clasohm@923
   136
    (*** Make the new theory ***)
clasohm@923
   137
clasohm@923
   138
    (*A key definition:
clasohm@923
   139
      If no mutual recursion then it equals the one recursive set.
clasohm@923
   140
      If mutual recursion then it differs from all the recursive sets. *)
clasohm@923
   141
    val big_rec_name = space_implode "_" rec_names;
clasohm@923
   142
clasohm@923
   143
    (*Big_rec... is the union of the mutually recursive sets*)
clasohm@923
   144
    val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params);
clasohm@923
   145
clasohm@923
   146
    (*The individual sets must already be declared*)
clasohm@923
   147
    val axpairs = map mk_defpair 
clasohm@1465
   148
          ((big_rec_tm, lfp_rhs) ::
clasohm@1465
   149
           (case parts of 
clasohm@1465
   150
               [_] => []                        (*no mutual recursion*)
clasohm@1465
   151
             | _ => rec_tms ~~          (*define the sets as Parts*)
clasohm@1465
   152
                    map (subst_atomic [(freeX, big_rec_tm)]) parts));
clasohm@923
   153
clasohm@923
   154
    val _ = seq (writeln o Sign.string_of_term sign o #2) axpairs
clasohm@923
   155
  
paulson@1397
   156
    (*Detect occurrences of operator, even with other types!*)
paulson@1397
   157
    val _ = (case rec_names inter (add_term_names (lfp_rhs,[])) of
clasohm@1465
   158
               [] => ()
clasohm@1465
   159
             | x::_ => error ("Illegal occurrence of recursion op: " ^ x ^
paulson@1397
   160
                               "\n\t*Consider adding type constraints*"))
paulson@1397
   161
clasohm@923
   162
  in  thy |> add_defs_i axpairs  end
clasohm@923
   163
clasohm@923
   164
clasohm@923
   165
(****************************************************************OMITTED
clasohm@923
   166
clasohm@923
   167
(*Expects the recursive sets to have been defined already.
clasohm@923
   168
  con_ty_lists specifies the constructors in the form (name,prems,mixfix) *)
clasohm@923
   169
fun add_constructs_def (rec_names, con_ty_lists) thy = 
clasohm@923
   170
* let
clasohm@923
   171
*   val _ = writeln"  Defining the constructor functions...";
clasohm@1465
   172
*   val case_name = "f";                (*name for case variables*)
clasohm@923
   173
clasohm@923
   174
*   (** Define the constructors **)
clasohm@923
   175
clasohm@923
   176
*   (*The empty tuple is 0*)
clasohm@923
   177
*   fun mk_tuple [] = Const("0",iT)
clasohm@923
   178
*     | mk_tuple args = foldr1 mk_Pair args;
clasohm@923
   179
clasohm@923
   180
*   fun mk_inject n k u = access_bal(ap Inl, ap Inr, u) n k;
clasohm@923
   181
clasohm@1465
   182
*   val npart = length rec_names;       (*total # of mutually recursive parts*)
clasohm@923
   183
clasohm@923
   184
*   (*Make constructor definition; kpart is # of this mutually recursive part*)
clasohm@923
   185
*   fun mk_con_defs (kpart, con_ty_list) = 
clasohm@1465
   186
*     let val ncon = length con_ty_list    (*number of constructors*)
clasohm@1465
   187
          fun mk_def (((id,T,syn), name, args, prems), kcon) =
clasohm@1465
   188
                (*kcon is index of constructor*)
clasohm@1465
   189
              mk_defpair (list_comb (Const(name,T), args),
clasohm@1465
   190
                          mk_inject npart kpart
clasohm@1465
   191
                          (mk_inject ncon kcon (mk_tuple args)))
paulson@2270
   192
*     in  ListPair.map mk_def (con_ty_list, (1 upto ncon))  end;
clasohm@923
   193
clasohm@923
   194
*   (** Define the case operator **)
clasohm@923
   195
clasohm@923
   196
*   (*Combine split terms using case; yields the case operator for one part*)
clasohm@923
   197
*   fun call_case case_list = 
clasohm@923
   198
*     let fun call_f (free,args) = 
clasohm@1465
   199
              ap_split T free (map (#2 o dest_Free) args)
clasohm@923
   200
*     in  fold_bal (app sum_case) (map call_f case_list)  end;
clasohm@923
   201
clasohm@923
   202
*   (** Generating function variables for the case definition
clasohm@1465
   203
        Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **)
clasohm@923
   204
clasohm@923
   205
*   (*Treatment of a single constructor*)
clasohm@923
   206
*   fun add_case (((id,T,syn), name, args, prems), (opno,cases)) =
clasohm@1465
   207
        if Syntax.is_identifier id
clasohm@1465
   208
        then (opno,   
clasohm@1465
   209
              (Free(case_name ^ "_" ^ id, T), args) :: cases)
clasohm@1465
   210
        else (opno+1, 
clasohm@1465
   211
              (Free(case_name ^ "_op_" ^ string_of_int opno, T), args) :: 
clasohm@1465
   212
              cases)
clasohm@923
   213
clasohm@923
   214
*   (*Treatment of a list of constructors, for one part*)
clasohm@923
   215
*   fun add_case_list (con_ty_list, (opno,case_lists)) =
clasohm@1465
   216
        let val (opno',case_list) = foldr add_case (con_ty_list, (opno,[]))
clasohm@1465
   217
        in (opno', case_list :: case_lists) end;
clasohm@923
   218
clasohm@923
   219
*   (*Treatment of all parts*)
clasohm@923
   220
*   val (_, case_lists) = foldr add_case_list (con_ty_lists, (1,[]));
clasohm@923
   221
clasohm@923
   222
*   val big_case_typ = flat (map (map (#2 o #1)) con_ty_lists) ---> (iT-->iT);
clasohm@923
   223
clasohm@923
   224
*   val big_rec_name = space_implode "_" rec_names;
clasohm@923
   225
clasohm@923
   226
*   val big_case_name = big_rec_name ^ "_case";
clasohm@923
   227
clasohm@923
   228
*   (*The list of all the function variables*)
clasohm@923
   229
*   val big_case_args = flat (map (map #1) case_lists);
clasohm@923
   230
clasohm@923
   231
*   val big_case_tm = 
clasohm@1465
   232
        list_comb (Const(big_case_name, big_case_typ), big_case_args); 
clasohm@923
   233
clasohm@923
   234
*   val big_case_def = mk_defpair  
clasohm@1465
   235
        (big_case_tm, fold_bal (app sum_case) (map call_case case_lists)); 
clasohm@923
   236
clasohm@923
   237
*   (** Build the new theory **)
clasohm@923
   238
clasohm@923
   239
*   val const_decs =
clasohm@1465
   240
        (big_case_name, big_case_typ, NoSyn) :: map #1 (flat con_ty_lists);
clasohm@923
   241
clasohm@923
   242
*   val axpairs =
paulson@2270
   243
        big_case_def :: flat (ListPair.map mk_con_defs ((1 upto npart), con_ty_lists))
clasohm@923
   244
clasohm@923
   245
*   in  thy |> add_consts_i const_decs |> add_defs_i axpairs  end;
clasohm@923
   246
****************************************************************)
clasohm@923
   247
end;
clasohm@923
   248
clasohm@923
   249
clasohm@923
   250
clasohm@923
   251