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