--- a/src/ZF/add_ind_def.ML Mon Dec 28 16:58:11 1998 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,270 +0,0 @@
-(* Title: ZF/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
-*)
-
-signature FP = (** Description of a fixed point operator **)
- sig
- val oper : term (*fixed point operator*)
- val bnd_mono : term (*monotonicity predicate*)
- val bnd_monoI : thm (*intro rule for bnd_mono*)
- val subs : thm (*subset theorem for fp*)
- val Tarski : thm (*Tarski's fixed point theorem*)
- val induct : thm (*induction/coinduction rule*)
- end;
-
-signature SU = (** Description of a disjoint sum **)
- sig
- val sum : term (*disjoint sum operator*)
- val inl : term (*left injection*)
- val inr : term (*right injection*)
- val elim : term (*case operator*)
- val case_inl : thm (*inl equality rule for case*)
- val case_inr : thm (*inr equality rule for case*)
- val inl_iff : thm (*injectivity of inl, using <->*)
- val inr_iff : thm (*injectivity of inr, using <->*)
- val distinct : thm (*distinctness of inl, inr using <->*)
- val distinct' : thm (*distinctness of inr, inl using <->*)
- val free_SEs : thm list (*elim rules for SU, and pair_iff!*)
- end;
-
-signature ADD_INDUCTIVE_DEF =
- sig
- val add_fp_def_i : term list * term * term list -> theory -> theory
- val add_constructs_def :
- string list * ((string*typ*mixfix) *
- string * term list * term list) list list ->
- theory -> theory
- end;
-
-
-
-(*Declares functions to add fixedpoint/constructor defs to a theory*)
-functor Add_inductive_def_Fun
- (structure Fp: FP and Pr : PR and CP: CARTPROD and Su : SU)
- : ADD_INDUCTIVE_DEF =
-struct
-open Logic Ind_Syntax;
-
-(*internal version*)
-fun add_fp_def_i (rec_tms, dom_sum, intr_tms) thy =
- let
- val dummy = (*has essential ancestors?*)
- Theory.requires thy "Inductive" "(co)inductive definitions"
-
- val sign = sign_of thy;
-
- (*recT and rec_params should agree for all mutually recursive components*)
- val rec_hds = map head_of rec_tms;
-
- val dummy = assert_all is_Const rec_hds
- (fn t => "Recursive set not previously declared as constant: " ^
- Sign.string_of_term sign t);
-
- (*Now we know they are all Consts, so get their names, type and params*)
- val rec_names = map (#1 o dest_Const) rec_hds
- and (Const(_,recT),rec_params) = strip_comb (hd rec_tms);
-
- val rec_base_names = map Sign.base_name rec_names;
- val dummy = assert_all Syntax.is_identifier rec_base_names
- (fn a => "Base name of recursive set not an identifier: " ^ 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,recT) => a mem rec_names | _ => false;
- in
- val dummy = 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 dummy = 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";
-
- 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 dummy = seq (fn rec_hd => seq (chk_prem rec_hd) prems) rec_hds
- val exfrees = term_frees intr \\ rec_params
- val zeq = FOLogic.mk_eq (Free(z',iT), #1 (rule_concl intr))
- in foldr FOLogic.mk_exists
- (exfrees, fold_bal (app FOLogic.conj) (zeq::prems))
- end;
-
- (*The Part(A,h) terms -- compose injections to make h*)
- fun mk_Part (Bound 0) = Free(X',iT) (*no mutual rec, no Part needed*)
- | mk_Part h = Part_const $ Free(X',iT) $ Abs(w',iT,h);
-
- (*Access to balanced disjoint sums via injections*)
- val parts =
- map mk_Part (accesses_bal (ap Su.inl, ap Su.inr, Bound 0)
- (length rec_tms));
-
- (*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_abs = absfree(X', iT,
- mk_Collect(z', dom_sum,
- fold_bal (app FOLogic.disj) part_intrs));
-
- val lfp_rhs = Fp.oper $ dom_sum $ lfp_abs
-
- val dummy = 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_base_name = space_implode "_" rec_base_names;
- val big_rec_name = Sign.intern_const sign big_rec_base_name;
-
- (*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 Logic.mk_defpair
- ((big_rec_tm, lfp_rhs) ::
- (case parts of
- [_] => [] (*no mutual recursion*)
- | _ => rec_tms ~~ (*define the sets as Parts*)
- map (subst_atomic [(Free(X',iT),big_rec_tm)]) parts));
-
- (*tracing: print the fixedpoint definition*)
- val _ = if !Ind_Syntax.trace then
- seq (writeln o Sign.string_of_term sign o #2) axpairs
- else ()
-
- in thy |> PureThy.add_defs_i (map Attribute.none axpairs) end
-
-
-(*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_base_names, con_ty_lists) thy =
- let
- val dummy = (*has essential ancestors?*)
- Theory.requires thy "Datatype" "(co)datatype definitions";
-
- val sign = sign_of thy;
- val full_name = Sign.full_name sign;
-
- val dummy = 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 (app Pr.pair) args;
-
- fun mk_inject n k u = access_bal (ap Su.inl, ap Su.inr, u) n k;
-
- val npart = length rec_base_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 (full_name name, T), args),
- mk_inject npart kpart
- (mk_inject ncon kcon (mk_tuple args)))
- in ListPair.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,[]) = Abs("null", iT, free)
- | call_f (free,args) =
- CP.ap_split (foldr1 CP.mk_prod (map (#2 o dest_Free) args))
- Ind_Syntax.iT
- free
- in fold_bal (app Su.elim) (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 (((_, T, _), name, args, prems), (opno, cases)) =
- if Syntax.is_identifier name then
- (opno, (Free (case_name ^ "_" ^ name, 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_base_name = space_implode "_" rec_base_names;
- val big_case_base_name = big_rec_base_name ^ "_case";
- val big_case_name = full_name big_case_base_name;
-
- (*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 Su.elim) (map call_case case_lists));
-
-
- (* Build the new theory *)
-
- val const_decs =
- (big_case_base_name, big_case_typ, NoSyn) :: map #1 (flat con_ty_lists);
-
- val axpairs =
- big_case_def :: flat (ListPair.map mk_con_defs (1 upto npart, con_ty_lists));
-
- in
- thy
- |> Theory.add_consts_i const_decs
- |> PureThy.add_defs_i (map Attribute.none axpairs)
- end;
-
-
-end;