--- a/src/HOLCF/Tools/Domain/domain_constructors.ML Thu Oct 14 14:42:05 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML Thu Oct 14 19:16:52 2010 -0700
@@ -10,7 +10,7 @@
type constr_info =
{
iso_info : Domain_Take_Proofs.iso_info,
- con_consts : term list,
+ con_specs : (term * (bool * typ) list) list,
con_betas : thm list,
nchotomy : thm,
exhaust : thm,
@@ -46,7 +46,7 @@
type constr_info =
{
iso_info : Domain_Take_Proofs.iso_info,
- con_consts : term list,
+ con_specs : (term * (bool * typ) list) list,
con_betas : thm list,
nchotomy : thm,
exhaust : thm,
@@ -858,6 +858,8 @@
val dname = Binding.name_of dbind;
val _ = writeln ("Proving isomorphism properties of domain "^dname^" ...");
+ val bindings = map #1 spec;
+
(* retrieve facts about rep/abs *)
val lhsT = #absT iso_info;
val {rep_const, abs_const, ...} = iso_info;
@@ -885,16 +887,19 @@
val {con_consts, con_betas, nchotomy, exhaust, compacts, con_rews,
inverts, injects, dist_les, dist_eqs} = con_result;
- (* define case combinator *)
- val ((case_const : typ -> term, cases : thm list), thy) =
+ (* prepare constructor spec *)
+ val con_specs : (term * (bool * typ) list) list =
let
fun prep_arg (lazy, sel, T) = (lazy, T);
fun prep_con c (b, args, mx) = (c, map prep_arg args);
- val case_spec = map2 prep_con con_consts spec;
in
- add_case_combinator case_spec lhsT dbind
+ map2 prep_con con_consts spec
+ end;
+
+ (* define case combinator *)
+ val ((case_const : typ -> term, cases : thm list), thy) =
+ add_case_combinator con_specs lhsT dbind
con_betas exhaust iso_locale rep_const thy
- end;
(* define and prove theorems for selector functions *)
val (sel_thms : thm list, thy : theory) =
@@ -908,27 +913,13 @@
(* 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 lhsT
- exhaust case_const cases thy
- end
+ add_discriminators bindings con_specs lhsT
+ exhaust case_const cases thy;
(* define and prove theorems for match combinators *)
val (match_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 mat_spec = map2 prep_con con_consts spec;
- in
- add_match_combinators bindings mat_spec lhsT
- exhaust case_const cases thy
- end
+ add_match_combinators bindings con_specs lhsT
+ exhaust case_const cases thy;
(* restore original signature path *)
val thy = Sign.parent_path thy;
@@ -962,7 +953,7 @@
val result =
{
iso_info = iso_info,
- con_consts = con_consts,
+ con_specs = con_specs,
con_betas = con_betas,
nchotomy = nchotomy,
exhaust = exhaust,
--- a/src/HOLCF/Tools/Domain/domain_extender.ML Thu Oct 14 14:42:05 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML Thu Oct 14 19:16:52 2010 -0700
@@ -198,7 +198,7 @@
val (take_rews, theorems_thy) =
thy
|> Domain_Theorems.comp_theorems (comp_dbind, eqs)
- (dbinds ~~ map snd eqs') take_info constr_infos;
+ dbinds take_info constr_infos;
in
theorems_thy
end;
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML Thu Oct 14 14:42:05 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Thu Oct 14 19:16:52 2010 -0700
@@ -11,7 +11,7 @@
sig
val comp_theorems :
binding * Domain_Library.eq list ->
- (binding * (binding * (bool * binding option * typ) list * mixfix) list) list ->
+ binding list ->
Domain_Take_Proofs.take_induct_info ->
Domain_Constructors.constr_info list ->
theory -> thm list * theory
@@ -97,7 +97,7 @@
(******************************************************************************)
fun take_theorems
- (specs : (binding * (binding * (bool * binding option * typ) list * mixfix) list) list)
+ (dbinds : binding list)
(take_info : Domain_Take_Proofs.take_induct_info)
(constr_infos : Domain_Constructors.constr_info list)
(thy : theory) : thm list list * theory =
@@ -122,13 +122,13 @@
end
fun prove_take_apps
- (((dbind, spec), take_const), constr_info) thy =
+ ((dbind, take_const), constr_info) thy =
let
- val {iso_info, con_consts, con_betas, ...} = constr_info;
+ val {iso_info, con_specs, con_betas, ...} = constr_info;
val {abs_inverse, ...} = iso_info;
- fun prove_take_app (con_const : term) (bind, args, mx) =
+ fun prove_take_app (con_const, args) =
let
- val Ts = map (fn (_, _, T) => T) args;
+ val Ts = map snd args;
val ns = Name.variant_list ["n"] (Datatype_Prop.make_tnames Ts);
val vs = map Free (ns ~~ Ts);
val lhs = mk_capply (take_const $ n', list_ccomb (con_const, vs));
@@ -141,7 +141,7 @@
in
Goal.prove_global thy [] [] goal (K tac)
end;
- val take_apps = map2 prove_take_app con_consts spec;
+ val take_apps = map prove_take_app con_specs;
in
yield_singleton Global_Theory.add_thmss
((Binding.qualified true "take_rews" dbind, take_apps),
@@ -149,7 +149,7 @@
end;
in
fold_map prove_take_apps
- (specs ~~ take_consts ~~ constr_infos) thy
+ (dbinds ~~ take_consts ~~ constr_infos) thy
end;
(* ----- general proofs ----------------------------------------------------- *)
@@ -508,7 +508,7 @@
fun comp_theorems
(comp_dbind : binding, eqs : eq list)
- (specs : (binding * (binding * (bool * binding option * typ) list * mixfix) list) list)
+ (dbinds : binding list)
(take_info : Domain_Take_Proofs.take_induct_info)
(constr_infos : Domain_Constructors.constr_info list)
(thy : theory) =
@@ -537,7 +537,7 @@
(* theorems about take *)
val (take_rewss, thy) =
- take_theorems specs take_info constr_infos thy;
+ take_theorems dbinds take_info constr_infos thy;
val {take_lemma_thms, take_0_thms, take_strict_thms, ...} = take_info;