--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/add_ind_def.ML Thu Aug 25 11:01:45 1994 +0200
@@ -0,0 +1,242 @@
+(* Title: HOL/add_ind_def.ML
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1994 University of Cambridge
+
+Fixedpoint definition module -- for Inductive/Coinductive Definitions
+
+Features:
+* least or greatest fixedpoints
+* user-specified product and sum constructions
+* mutually recursive definitions
+* definitions involving arbitrary monotone operators
+* automatically proves introduction and elimination rules
+
+The recursive sets must *already* be declared as constants in parent theory!
+
+ Introduction rules have the form
+ [| ti:M(Sj), ..., P(x), ... |] ==> t: Sk |]
+ where M is some monotone operator (usually the identity)
+ P(x) is any (non-conjunctive) side condition on the free variables
+ ti, t are any terms
+ Sj, Sk are two of the sets being defined in mutual recursion
+
+Sums are used only for mutual recursion;
+Products are used only to derive "streamlined" induction rules for relations
+
+Nestings of disjoint sum types:
+ (a+(b+c)) for 3, ((a+b)+(c+d)) for 4, ((a+b)+(c+(d+e))) for 5,
+ ((a+(b+c))+(d+(e+f))) for 6
+*)
+
+signature FP = (** Description of a fixed point operator **)
+ sig
+ val oper : string * typ * term -> term (*fixed point operator*)
+ val Tarski : thm (*Tarski's fixed point theorem*)
+ val induct : thm (*induction/coinduction rule*)
+ end;
+
+
+signature ADD_INDUCTIVE_DEF =
+ sig
+ val add_fp_def_i : term list * term list -> theory -> theory
+ end;
+
+
+
+(*Declares functions to add fixedpoint/constructor defs to a theory*)
+functor Add_inductive_def_Fun (Fp: FP) : ADD_INDUCTIVE_DEF =
+struct
+open Logic Ind_Syntax;
+
+(*internal version*)
+fun add_fp_def_i (rec_tms, intr_tms) thy =
+ let
+ val sign = sign_of thy;
+
+ (*recT and rec_params should agree for all mutually recursive components*)
+ val (Const(_,recT),rec_params) = strip_comb (hd rec_tms)
+ and rec_hds = map head_of rec_tms;
+
+ val domTs = summands(dest_set (body_type recT));
+
+ val rec_names = map (#1 o dest_Const) rec_hds;
+
+ val _ = assert_all Syntax.is_identifier rec_names
+ (fn a => "Name of recursive set not an identifier: " ^ a);
+
+ val _ = assert_all (is_some o lookup_const sign) rec_names
+ (fn a => "Recursive set not previously declared as constant: " ^ a);
+
+ local (*Checking the introduction rules*)
+ val intr_sets = map (#2 o rule_concl_msg sign) intr_tms;
+ fun intr_ok set =
+ case head_of set of Const(a,_) => a mem rec_names | _ => false;
+ in
+ val _ = assert_all intr_ok intr_sets
+ (fn t => "Conclusion of rule does not name a recursive set: " ^
+ Sign.string_of_term sign t);
+ end;
+
+ val _ = assert_all is_Free rec_params
+ (fn t => "Param in recursion term not a free variable: " ^
+ Sign.string_of_term sign t);
+
+ (*** Construct the lfp definition ***)
+ val mk_variant = variant (foldr add_term_names (intr_tms,[]));
+
+ val z = mk_variant"z" and X = mk_variant"X" and w = mk_variant"w";
+
+ val dom_sumT = fold_bal mk_sum domTs;
+ val dom_set = mk_set dom_sumT;
+
+ val freez = Free(z, dom_sumT)
+ and freeX = Free(X, dom_set);
+ (*type of w may be any of the domTs*)
+
+ fun dest_tprop (Const("Trueprop",_) $ P) = P
+ | dest_tprop Q = error ("Ill-formed premise of introduction rule: " ^
+ Sign.string_of_term sign Q);
+
+ (*Makes a disjunct from an introduction rule*)
+ fun lfp_part intr = (*quantify over rule's free vars except parameters*)
+ let val prems = map dest_tprop (strip_imp_prems intr)
+ val _ = seq (fn rec_hd => seq (chk_prem rec_hd) prems) rec_hds
+ val exfrees = term_frees intr \\ rec_params
+ val zeq = eq_const dom_sumT $ freez $ (#1 (rule_concl intr))
+ in foldr mk_exists (exfrees, fold_bal (app conj) (zeq::prems)) end;
+
+ (*The Part(A,h) terms -- compose injections to make h*)
+ fun mk_Part (Bound 0, _) = freeX (*no mutual rec, no Part needed*)
+ | mk_Part (h, domT) =
+ let val goodh = mend_sum_types (h, dom_sumT)
+ and Part_const =
+ Const("Part", [dom_set, domT-->dom_sumT]---> dom_set)
+ in Part_const $ freeX $ Abs(w,domT,goodh) end;
+
+ (*Access to balanced disjoint sums via injections*)
+ val parts = map mk_Part
+ (accesses_bal (ap Inl, ap Inr, Bound 0) (length domTs) ~~
+ domTs);
+
+ (*replace each set by the corresponding Part(A,h)*)
+ val part_intrs = map (subst_free (rec_tms ~~ parts) o lfp_part) intr_tms;
+
+ val lfp_rhs = Fp.oper(X, dom_sumT,
+ mk_Collect(z, dom_sumT,
+ fold_bal (app disj) part_intrs))
+
+ val _ = seq (fn rec_hd => deny (rec_hd occs lfp_rhs)
+ "Illegal occurrence of recursion operator")
+ rec_hds;
+
+ (*** Make the new theory ***)
+
+ (*A key definition:
+ If no mutual recursion then it equals the one recursive set.
+ If mutual recursion then it differs from all the recursive sets. *)
+ val big_rec_name = space_implode "_" rec_names;
+
+ (*Big_rec... is the union of the mutually recursive sets*)
+ val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params);
+
+ (*The individual sets must already be declared*)
+ val axpairs = map mk_defpair
+ ((big_rec_tm, lfp_rhs) ::
+ (case parts of
+ [_] => [] (*no mutual recursion*)
+ | _ => rec_tms ~~ (*define the sets as Parts*)
+ map (subst_atomic [(freeX, big_rec_tm)]) parts));
+
+ val _ = seq (writeln o Sign.string_of_term sign o #2) axpairs
+
+ in thy |> add_defs_i axpairs end
+
+
+(****************************************************************OMITTED
+
+(*Expects the recursive sets to have been defined already.
+ con_ty_lists specifies the constructors in the form (name,prems,mixfix) *)
+fun add_constructs_def (rec_names, con_ty_lists) thy =
+* let
+* val _ = writeln" Defining the constructor functions...";
+* val case_name = "f"; (*name for case variables*)
+
+* (** Define the constructors **)
+
+* (*The empty tuple is 0*)
+* fun mk_tuple [] = Const("0",iT)
+* | mk_tuple args = foldr1 mk_Pair args;
+
+* fun mk_inject n k u = access_bal(ap Inl, ap Inr, u) n k;
+
+* val npart = length rec_names; (*total # of mutually recursive parts*)
+
+* (*Make constructor definition; kpart is # of this mutually recursive part*)
+* fun mk_con_defs (kpart, con_ty_list) =
+* let val ncon = length con_ty_list (*number of constructors*)
+ fun mk_def (((id,T,syn), name, args, prems), kcon) =
+ (*kcon is index of constructor*)
+ mk_defpair (list_comb (Const(name,T), args),
+ mk_inject npart kpart
+ (mk_inject ncon kcon (mk_tuple args)))
+* in map mk_def (con_ty_list ~~ (1 upto ncon)) end;
+
+* (** Define the case operator **)
+
+* (*Combine split terms using case; yields the case operator for one part*)
+* fun call_case case_list =
+* let fun call_f (free,args) =
+ ap_split T free (map (#2 o dest_Free) args)
+* in fold_bal (app sum_case) (map call_f case_list) end;
+
+* (** Generating function variables for the case definition
+ Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **)
+
+* (*Treatment of a single constructor*)
+* fun add_case (((id,T,syn), name, args, prems), (opno,cases)) =
+ if Syntax.is_identifier id
+ then (opno,
+ (Free(case_name ^ "_" ^ id, T), args) :: cases)
+ else (opno+1,
+ (Free(case_name ^ "_op_" ^ string_of_int opno, T), args) ::
+ cases)
+
+* (*Treatment of a list of constructors, for one part*)
+* fun add_case_list (con_ty_list, (opno,case_lists)) =
+ let val (opno',case_list) = foldr add_case (con_ty_list, (opno,[]))
+ in (opno', case_list :: case_lists) end;
+
+* (*Treatment of all parts*)
+* val (_, case_lists) = foldr add_case_list (con_ty_lists, (1,[]));
+
+* val big_case_typ = flat (map (map (#2 o #1)) con_ty_lists) ---> (iT-->iT);
+
+* val big_rec_name = space_implode "_" rec_names;
+
+* val big_case_name = big_rec_name ^ "_case";
+
+* (*The list of all the function variables*)
+* val big_case_args = flat (map (map #1) case_lists);
+
+* val big_case_tm =
+ list_comb (Const(big_case_name, big_case_typ), big_case_args);
+
+* val big_case_def = mk_defpair
+ (big_case_tm, fold_bal (app sum_case) (map call_case case_lists));
+
+* (** Build the new theory **)
+
+* val const_decs =
+ (big_case_name, big_case_typ, NoSyn) :: map #1 (flat con_ty_lists);
+
+* val axpairs =
+ big_case_def :: flat (map mk_con_defs ((1 upto npart) ~~ con_ty_lists))
+
+* in thy |> add_consts_i const_decs |> add_defs_i axpairs end;
+****************************************************************)
+end;
+
+
+
+