--- a/src/HOLCF/Tools/Domain/domain_extender.ML Sat Mar 13 15:51:12 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML Sat Mar 13 16:48:57 2010 -0800
@@ -166,7 +166,6 @@
val eqs' : ((string * typ list) *
(binding * (bool * binding option * typ) list * mixfix) list) list =
check_and_sort_domain false dtnvs' cons'' thy;
-(* val thy = Domain_Syntax.add_syntax eqs' thy; *)
val dts : typ list = map (Type o fst) eqs';
val new_dts : (string * string list) list =
map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
@@ -189,9 +188,9 @@
val ((rewss, take_rews), theorems_thy) =
thy
- |> fold_map (fn ((eq, (x,cs)), info) =>
- Domain_Theorems.theorems (eq, eqs) (Type x, cs) info take_info)
- (eqs ~~ eqs' ~~ iso_infos)
+ |> fold_map (fn (((dbind, eq), (_,cs)), info) =>
+ Domain_Theorems.theorems (eq, eqs) dbind cs info take_info)
+ (dbinds ~~ eqs ~~ eqs' ~~ iso_infos)
||>> Domain_Theorems.comp_theorems (comp_dbind, eqs) take_info;
in
theorems_thy
@@ -228,6 +227,8 @@
|> Sign.add_types (map thy_type dtnvs)
|> fold (AxClass.axiomatize_arity o thy_arity) dtnvs;
+ val dbinds : binding list =
+ map (fn (_,dbind,_,_) => dbind) eqs''';
val cons''' :
(binding * (bool * binding option * 'a) list * mixfix) list list =
map (fn (_,_,_,cons) => cons) eqs''';
@@ -264,9 +265,9 @@
map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs';
val ((rewss, take_rews), theorems_thy) =
thy
- |> fold_map (fn ((eq, (x,cs)), info) =>
- Domain_Theorems.theorems (eq, eqs) (Type x, cs) info take_info)
- (eqs ~~ eqs' ~~ iso_infos)
+ |> fold_map (fn (((dbind, eq), (x,cs)), info) =>
+ Domain_Theorems.theorems (eq, eqs) dbind cs info take_info)
+ (dbinds ~~ eqs ~~ eqs' ~~ iso_infos)
||>> Domain_Theorems.comp_theorems (comp_dbind, eqs) take_info;
in
theorems_thy
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML Sat Mar 13 15:51:12 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Sat Mar 13 16:48:57 2010 -0800
@@ -10,11 +10,12 @@
signature DOMAIN_THEOREMS =
sig
val theorems:
- Domain_Library.eq * Domain_Library.eq list ->
- typ * (binding * (bool * binding option * typ) list * mixfix) list ->
- Domain_Take_Proofs.iso_info ->
- Domain_Take_Proofs.take_induct_info ->
- theory -> thm list * theory;
+ Domain_Library.eq * Domain_Library.eq list ->
+ binding ->
+ (binding * (bool * binding option * typ) list * mixfix) list ->
+ Domain_Take_Proofs.iso_info ->
+ Domain_Take_Proofs.take_induct_info ->
+ theory -> thm list * theory;
val comp_theorems :
binding * Domain_Library.eq list ->
@@ -83,7 +84,8 @@
fun theorems
(((dname, _), cons) : eq, eqs : eq list)
- (dom_eqn : typ * (binding * (bool * binding option * typ) list * mixfix) list)
+ (dbind : binding)
+ (spec : (binding * (bool * binding option * typ) list * mixfix) list)
(iso_info : Domain_Take_Proofs.iso_info)
(take_info : Domain_Take_Proofs.take_induct_info)
(thy : theory) =
@@ -114,7 +116,7 @@
val (result, thy) =
Domain_Constructors.add_domain_constructors
- (Long_Name.base_name dname) (snd dom_eqn) iso_info thy;
+ (Long_Name.base_name dname) spec iso_info thy;
val con_appls = #con_betas result;
val {exhaust, casedist, ...} = result;
@@ -174,33 +176,34 @@
end;
val case_ns =
- "bottom" :: map (fn (b,_,_) => Binding.name_of b) (snd dom_eqn);
+ "bottom" :: map (fn (b,_,_) => Binding.name_of b) spec;
+
+fun qualified name = Binding.qualified true name dbind;
+val simp = Simplifier.simp_add;
+val fixrec_simp = Fixrec.fixrec_simp_add;
in
thy
- |> Sign.add_path (Long_Name.base_name dname)
- |> snd o PureThy.add_thmss [
- ((Binding.name "iso_rews" , iso_rews ), [Simplifier.simp_add]),
- ((Binding.name "exhaust" , [exhaust] ), []),
- ((Binding.name "casedist" , [casedist] ),
- [Rule_Cases.case_names case_ns, Induct.cases_type dname]),
- ((Binding.name "when_rews" , when_rews ), [Simplifier.simp_add]),
- ((Binding.name "compacts" , con_compacts), [Simplifier.simp_add]),
- ((Binding.name "con_rews" , con_rews ),
- [Simplifier.simp_add, Fixrec.fixrec_simp_add]),
- ((Binding.name "sel_rews" , sel_rews ), [Simplifier.simp_add]),
- ((Binding.name "dis_rews" , dis_rews ), [Simplifier.simp_add]),
- ((Binding.name "pat_rews" , pat_rews ), [Simplifier.simp_add]),
- ((Binding.name "dist_les" , dist_les ), [Simplifier.simp_add]),
- ((Binding.name "dist_eqs" , dist_eqs ), [Simplifier.simp_add]),
- ((Binding.name "inverts" , inverts ), [Simplifier.simp_add]),
- ((Binding.name "injects" , injects ), [Simplifier.simp_add]),
- ((Binding.name "take_rews" , take_rews ), [Simplifier.simp_add]),
- ((Binding.name "match_rews", mat_rews ),
- [Simplifier.simp_add, Fixrec.fixrec_simp_add])]
- |> Sign.parent_path
- |> pair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @
- pat_rews @ dist_les @ dist_eqs)
+ |> PureThy.add_thmss [
+ ((qualified "iso_rews" , iso_rews ), [simp]),
+ ((qualified "exhaust" , [exhaust] ), []),
+ ((qualified "casedist" , [casedist] ),
+ [Rule_Cases.case_names case_ns, Induct.cases_type dname]),
+ ((qualified "when_rews" , when_rews ), [simp]),
+ ((qualified "compacts" , con_compacts), [simp]),
+ ((qualified "con_rews" , con_rews ), [simp, fixrec_simp]),
+ ((qualified "sel_rews" , sel_rews ), [simp]),
+ ((qualified "dis_rews" , dis_rews ), [simp]),
+ ((qualified "pat_rews" , pat_rews ), [simp]),
+ ((qualified "dist_les" , dist_les ), [simp]),
+ ((qualified "dist_eqs" , dist_eqs ), [simp]),
+ ((qualified "inverts" , inverts ), [simp]),
+ ((qualified "injects" , injects ), [simp]),
+ ((qualified "take_rews" , take_rews ), [simp]),
+ ((qualified "match_rews", mat_rews ), [simp, fixrec_simp])]
+ |> snd
+ |> pair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @
+ pat_rews @ dist_les @ dist_eqs)
end; (* let *)
(******************************************************************************)