--- 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) *)
--- 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;
--- 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 *)
--- 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 -------------------------------- *)