# HG changeset patch # User huffman # Date 1267313562 28800 # Node ID 8cb42aa19358fe1a84a5d39dce22d4c52c56b311 # Parent 3d8acfae6fb89162d7969dbef50c56ac116aff53 move definition of discriminators to domain_constructors.ML diff -r 3d8acfae6fb8 -r 8cb42aa19358 src/HOLCF/Tools/Domain/domain_axioms.ML --- a/src/HOLCF/Tools/Domain/domain_axioms.ML Sat Feb 27 14:04:46 2010 -0800 +++ b/src/HOLCF/Tools/Domain/domain_axioms.ML Sat Feb 27 15:32:42 2010 -0800 @@ -78,15 +78,6 @@ (dc_abs oo (copy_of_dtyp map_tab r (dtyp_of_eq eqn)) oo dc_rep)) end; -(* -- definitions concerning the discriminators - *) - - val dis_defs = let - fun ddef (con,_,_) = (dis_name con ^"_def",%%:(dis_name con) == - list_ccomb(%%:(dname^"_when"),map - (fn (con',_,args) => (List.foldr /\# - (if con'=con then TT else FF) args)) cons)) - in map ddef cons end; - val mat_defs = let fun mdef (con, _, _) = @@ -134,7 +125,7 @@ in (dnam, (if definitional then [] else [abs_iso_ax, rep_iso_ax, reach_ax]), (if definitional then [when_def] else [when_def, copy_def]) @ - dis_defs @ mat_defs @ pat_defs @ + mat_defs @ pat_defs @ [take_def, finite_def]) end; (* let (calc_axioms) *) diff -r 3d8acfae6fb8 -r 8cb42aa19358 src/HOLCF/Tools/Domain/domain_constructors.ML --- a/src/HOLCF/Tools/Domain/domain_constructors.ML Sat Feb 27 14:04:46 2010 -0800 +++ b/src/HOLCF/Tools/Domain/domain_constructors.ML Sat Feb 27 15:32:42 2010 -0800 @@ -25,7 +25,8 @@ dist_les : thm list, dist_eqs : thm list, cases : thm list, - sel_rews : thm list + sel_rews : thm list, + dis_rews : thm list } * theory; end; @@ -590,7 +591,8 @@ (con_betas : thm list) (casedist : thm) (iso_locale : thm) - (thy : theory) = + (thy : theory) + : ((typ -> term) * thm list) * theory = let (* prove rep/abs rules *) @@ -598,16 +600,17 @@ val abs_inverse = iso_locale RS @{thm iso.abs_iso}; (* calculate function arguments of case combinator *) - val resultT = TVar (("'a",0), @{sort pcpo}); - val fTs = map (fn (_, args) => map snd args -->> resultT) spec; + val resultT = TVar (("'t",0), @{sort pcpo}); + fun fTs T = map (fn (_, args) => map snd args -->> T) spec; val fns = Datatype_Prop.indexify_names (map (K "f") spec); - val fs = map Free (fns ~~ fTs); - val caseT = fTs -->> (lhsT ->> resultT); + val fs = map Free (fns ~~ fTs resultT); + fun caseT T = fTs T -->> (lhsT ->> T); (* TODO: move definition of case combinator here *) val case_bind = Binding.name (dname ^ "_when"); - val case_const = Const (Sign.full_name thy case_bind, caseT); - val case_app = list_ccomb (case_const, fs); + val case_name = Sign.full_name thy case_bind; + fun case_const T = Const (case_name, caseT T); + val case_app = list_ccomb (case_const resultT, fs); (* prove beta reduction rule for case combinator *) val case_beta = beta_of_def thy case_def; @@ -645,7 +648,7 @@ end in - (case_strict :: case_apps, thy) + ((case_const, case_strict :: case_apps), thy) end (******************************************************************************) @@ -791,6 +794,52 @@ end (******************************************************************************) +(************ definitions and theorems for discriminator functions ************) +(******************************************************************************) + +fun add_discriminators + (bindings : binding list) + (spec : (term * (bool * typ) list) list) + (case_const : typ -> term) + (thy : theory) = + let + + fun vars_of args = + let + val Ts = map snd args; + val ns = Datatype_Prop.make_tnames Ts; + in + map Free (ns ~~ Ts) + end; + + (* define discriminator functions *) + local + fun dis_fun i (j, (con, args)) = + let + val Ts = map snd args; + val ns = Datatype_Prop.make_tnames Ts; + val vs = map Free (ns ~~ Ts); + val tr = if i = j then @{term TT} else @{term FF}; + in + big_lambdas vs tr + end; + fun dis_eqn (i, bind) : binding * term * mixfix = + let + val dis_bind = Binding.prefix_name "is_" bind; + val rhs = list_ccomb (case_const trT, map_index (dis_fun i) spec); + in + (dis_bind, rhs, NoSyn) + end; + in + val ((dis_consts, dis_defs), thy) = + define_consts (map_index dis_eqn bindings) thy + end; + + in + (dis_defs, thy) + end; + +(******************************************************************************) (******************************* main function ********************************) (******************************************************************************) @@ -823,7 +872,7 @@ val {con_consts, con_betas, casedist, ...} = con_result; (* define case combinator *) - val (cases : thm list, thy) = + val ((case_const : typ -> term, cases : thm list), thy) = let fun prep_arg (lazy, sel, T) = (lazy, T); fun prep_con c (b, args, mx) = (c, map prep_arg args); @@ -836,14 +885,26 @@ (* TODO: enable this earlier *) val thy = Sign.add_path dname thy; - (* replace bindings with terms in constructor spec *) - val sel_spec : (term * (bool * binding option * typ) list) list = - map2 (fn con => fn (b, args, mx) => (con, args)) con_consts spec; - (* define and prove theorems for selector functions *) val (sel_thms : thm list, thy : theory) = - add_selectors sel_spec rep_const - abs_iso_thm rep_strict rep_defined_iff con_betas thy; + let + val sel_spec : (term * (bool * binding option * typ) list) list = + map2 (fn con => fn (b, args, mx) => (con, args)) con_consts spec; + in + add_selectors sel_spec rep_const + abs_iso_thm rep_strict rep_defined_iff con_betas thy + end; + + (* define and prove theorems for discriminator functions *) + val (dis_thms : thm list, thy : theory) = + let + val bindings = map #1 spec; + fun prep_arg (lazy, sel, T) = (lazy, T); + fun prep_con c (b, args, mx) = (c, map prep_arg args); + val dis_spec = map2 prep_con con_consts spec; + in + add_discriminators bindings dis_spec case_const thy + end (* restore original signature path *) val thy = Sign.parent_path thy; @@ -860,7 +921,8 @@ dist_les = #dist_les con_result, dist_eqs = #dist_eqs con_result, cases = cases, - sel_rews = sel_thms }; + sel_rews = sel_thms, + dis_rews = dis_thms }; in (result, thy) end; diff -r 3d8acfae6fb8 -r 8cb42aa19358 src/HOLCF/Tools/Domain/domain_syntax.ML --- a/src/HOLCF/Tools/Domain/domain_syntax.ML Sat Feb 27 14:04:46 2010 -0800 +++ b/src/HOLCF/Tools/Domain/domain_syntax.ML Sat Feb 27 15:32:42 2010 -0800 @@ -64,15 +64,10 @@ | esc [] = [] in implode o esc o Symbol.explode end; - fun dis_name_ con = - Binding.name ("is_" ^ strip_esc (Binding.name_of con)); fun mat_name_ con = Binding.name ("match_" ^ strip_esc (Binding.name_of con)); fun pat_name_ con = Binding.name (strip_esc (Binding.name_of con) ^ "_pat"); - fun dis (con,args,mx) = - (dis_name_ con, dtype->>trT, - Mixfix(escape ("is_" ^ Binding.name_of con), [], Syntax.max_pri)); (* strictly speaking, these constants have one argument, but the mixfix (without arguments) is introduced only to generate parse rules for non-alphanumeric names*) @@ -95,7 +90,6 @@ mk_patT (dtype, mk_ctupleT (map (freetvar "t") (1 upto length args))), Mixfix(escape (Binding.name_of con ^ "_pat"), [], Syntax.max_pri)); in - val consts_dis = map dis cons'; val consts_mat = map mat cons'; val consts_pat = map pat cons'; end; @@ -165,7 +159,7 @@ if definitional then [] else [const_rep, const_abs, const_copy]; in (optional_consts @ [const_when] @ - consts_dis @ consts_mat @ consts_pat @ + consts_mat @ consts_pat @ [const_take, const_finite], (case_trans false :: case_trans true :: (abscon_trans false @ abscon_trans true @ Case_trans))) end; (* let *) diff -r 3d8acfae6fb8 -r 8cb42aa19358 src/HOLCF/Tools/Domain/domain_theorems.ML --- a/src/HOLCF/Tools/Domain/domain_theorems.ML Sat Feb 27 14:04:46 2010 -0800 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Sat Feb 27 15:32:42 2010 -0800 @@ -156,7 +156,6 @@ val ax_rep_iso = ga "rep_iso" dname; val ax_when_def = ga "when_def" dname; fun get_def mk_name (con, _, _) = ga (mk_name con^"_def") dname; - val axs_dis_def = map (get_def dis_name) cons; val axs_mat_def = map (get_def mat_name) cons; val axs_pat_def = map (get_def pat_name) cons; val ax_copy_def = ga "copy_def" dname; @@ -191,6 +190,7 @@ val {sel_rews, ...} = result; val when_rews = #cases result; val when_strict = hd when_rews; +val axs_dis_def = #dis_rews result; (* ----- theorems concerning the isomorphism -------------------------------- *)