--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/constructor.ML Thu Sep 16 12:20:38 1993 +0200
@@ -0,0 +1,200 @@
+(* Title: ZF/constructor.ML
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1993 University of Cambridge
+
+Constructor function module -- for Datatype Definitions
+
+Defines constructors and a case-style eliminator (no primitive recursion)
+
+Features:
+* least or greatest fixedpoints
+* user-specified product and sum constructions
+* mutually recursive datatypes
+* recursion over arbitrary monotone operators
+* flexible: can derive any reasonable set of introduction rules
+* automatically constructs a case analysis operator (but no recursion op)
+* efficient treatment of large declarations (e.g. 60 constructors)
+*)
+
+(** STILL NEEDS: some treatment of recursion **)
+
+signature CONSTRUCTOR =
+ sig
+ val thy : theory (*parent theory*)
+ val rec_specs : (string * string * (string list * string)list) list
+ (*recursion ops, types, domains, constructors*)
+ val rec_styp : string (*common type of all recursion ops*)
+ val ext : Syntax.sext option (*syntax extension for new theory*)
+ val sintrs : string list (*desired introduction rules*)
+ val monos : thm list (*monotonicity of each M operator*)
+ val type_intrs : thm list (*type-checking intro rules*)
+ val type_elims : thm list (*type-checking elim rules*)
+ end;
+
+signature CONSTRUCTOR_RESULT =
+ sig
+ val con_thy : theory (*theory defining the constructors*)
+ val con_defs : thm list (*definitions made in con_thy*)
+ val case_eqns : thm list (*equations for case operator*)
+ val free_iffs : thm list (*freeness rewrite rules*)
+ val free_SEs : thm list (*freeness destruct rules*)
+ val mk_free : string -> thm (*makes freeness theorems*)
+ val congs : thm list (*congruence rules for simplifier*)
+ end;
+
+
+functor Constructor_Fun (structure Const: CONSTRUCTOR and
+ Pr : PR and Su : SU) : CONSTRUCTOR_RESULT =
+struct
+open Logic Const;
+
+val dummy = writeln"Defining the constructor functions...";
+
+val case_name = "f"; (*name for case variables*)
+
+(** Extract basic information from arguments **)
+
+val sign = sign_of thy;
+val rdty = Sign.typ_of o Sign.read_ctyp sign;
+
+val rec_names = map #1 rec_specs;
+
+val dummy = assert_all Syntax.is_identifier rec_names
+ (fn a => "Name of recursive set not an identifier: " ^ a);
+
+(*Expands multiple constant declarations*)
+fun pairtypes (cs,st) = map (rpair st) cs;
+
+(*Constructors with types and arguments*)
+fun mk_con_ty_list cons_pairs =
+ let fun mk_con_ty (a,st) =
+ let val T = rdty st
+ val args = mk_frees "xa" (binder_types T)
+ in (a,T,args) end
+ in map mk_con_ty (flat (map pairtypes cons_pairs)) end;
+
+val con_ty_lists = map (mk_con_ty_list o #3) rec_specs;
+
+(** Define the constructors **)
+
+(*We identify 0 (the empty set) with the empty tuple*)
+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_names; (*number of mutually recursive parts*)
+
+(*Make constructor definition*)
+fun mk_con_defs (kpart, con_ty_list) =
+ let val ncon = length con_ty_list (*number of constructors*)
+ fun mk_def ((a,T,args), kcon) = (*kcon = index of this constructor*)
+ mk_defpair sign
+ (list_comb (Const(a,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 Pr.split_const free (map (#2 o dest_Free) args)
+ 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 ((a,T,args), (opno,cases)) =
+ if Syntax.is_identifier a
+ then (opno,
+ (Free(case_name ^ "_" ^ a, 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) 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 sign
+ (big_case_tm, fold_bal (app Su.elim) (map call_case case_lists));
+
+(** Build the new theory **)
+
+val axpairs =
+ big_case_def :: flat (map mk_con_defs ((1 upto npart) ~~ con_ty_lists));
+
+val const_decs = remove_mixfixes ext
+ (([big_case_name], flatten_typ sign big_case_typ) ::
+ (big_rec_name ins rec_names, rec_styp) ::
+ flat (map #3 rec_specs));
+
+val con_thy = extend_theory thy (big_rec_name ^ "_Constructors")
+ ([], [], [], [], const_decs, ext) axpairs;
+
+(*1st element is the case definition; others are the constructors*)
+val con_defs = map (get_axiom con_thy o #1) axpairs;
+
+(** Prove the case theorem **)
+
+(*Each equation has the form
+ rec_case(f_con1,...,f_conn)(coni(args)) = f_coni(args) *)
+fun mk_case_equation ((a,T,args), case_free) =
+ mk_tprop
+ (eq_const $ (big_case_tm $ (list_comb (Const(a,T), args)))
+ $ (list_comb (case_free, args)));
+
+val case_trans = hd con_defs RS def_trans;
+
+(*proves a single case equation*)
+fun case_tacsf con_def _ =
+ [rewtac con_def,
+ rtac case_trans 1,
+ REPEAT (resolve_tac [refl, Pr.split_eq RS trans,
+ Su.case_inl RS trans,
+ Su.case_inr RS trans] 1)];
+
+fun prove_case_equation (arg,con_def) =
+ prove_term (sign_of con_thy) []
+ (mk_case_equation arg, case_tacsf con_def);
+
+val free_iffs =
+ map standard (con_defs RL [def_swap_iff]) @
+ [Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff, Pr.pair_iff];
+
+val free_SEs = map (gen_make_elim [conjE,FalseE]) (free_iffs RL [iffD1]);
+
+val free_cs = ZF_cs addSEs free_SEs;
+
+(*Typical theorems have the form ~con1=con2, con1=con2==>False,
+ con1(x)=con1(y) ==> x=y, con1(x)=con1(y) <-> x=y, etc. *)
+fun mk_free s =
+ prove_goalw con_thy con_defs s
+ (fn prems => [cut_facts_tac prems 1, fast_tac free_cs 1]);
+
+val case_eqns = map prove_case_equation
+ (flat con_ty_lists ~~ big_case_args ~~ tl con_defs);
+
+val congs = mk_congs con_thy (flat (map #1 (const_decs @ ext_constants ext)));
+end;
+
+