--- a/src/HOLCF/Tools/Domain/domain_axioms.ML Wed Mar 03 07:36:31 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML Wed Mar 03 07:55:52 2010 -0800
@@ -18,8 +18,8 @@
string Symtab.table -> (int -> term) -> Datatype.dtyp -> term
val add_axioms :
- (binding * (typ * typ)) list ->
- theory -> theory
+ (binding * (typ * typ)) list -> theory ->
+ Domain_Take_Proofs.iso_info list * theory
end;
@@ -146,7 +146,7 @@
(map fst dom_eqns ~~ #take_consts take_info) thy;
in
- thy (* TODO: also return iso_infos, take_info, lub_take_thms *)
+ (iso_infos, thy) (* TODO: also return take_info, lub_take_thms *)
end;
end; (* struct *)
--- a/src/HOLCF/Tools/Domain/domain_extender.ML Wed Mar 03 07:36:31 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML Wed Mar 03 07:55:52 2010 -0800
@@ -184,13 +184,14 @@
fun mk_eq_typ (_, cons) = foldr1 mk_ssumT (map mk_con_typ cons);
val repTs : typ list = map mk_eq_typ eqs';
val dom_eqns : (binding * (typ * typ)) list = dbinds ~~ (dts ~~ repTs);
- val thy = Domain_Axioms.add_axioms dom_eqns thy;
+ val (iso_infos, thy) =
+ Domain_Axioms.add_axioms dom_eqns thy;
val ((rewss, take_rews), theorems_thy) =
thy
- |> fold_map (fn (eq, (x,cs)) =>
- Domain_Theorems.theorems (eq, eqs) (Type x, cs))
- (eqs ~~ eqs')
+ |> fold_map (fn ((eq, (x,cs)), info) =>
+ Domain_Theorems.theorems (eq, eqs) (Type x, cs) info)
+ (eqs ~~ eqs' ~~ iso_infos)
||>> Domain_Theorems.comp_theorems (comp_dnam, eqs);
in
theorems_thy
@@ -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)) =>
- Domain_Theorems.theorems (eq, eqs) (Type x, cs))
- (eqs ~~ eqs')
+ |> fold_map (fn ((eq, (x,cs)), info) =>
+ Domain_Theorems.theorems (eq, eqs) (Type x, cs) info)
+ (eqs ~~ eqs' ~~ iso_infos)
||>> Domain_Theorems.comp_theorems (comp_dnam, eqs);
in
theorems_thy
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML Wed Mar 03 07:36:31 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Wed Mar 03 07:55:52 2010 -0800
@@ -12,6 +12,7 @@
val theorems:
Domain_Library.eq * Domain_Library.eq list
-> typ * (binding * (bool * binding option * typ) list * mixfix) list
+ -> Domain_Take_Proofs.iso_info
-> theory -> thm list * theory;
val comp_theorems: bstring * Domain_Library.eq list -> theory -> thm list * theory;
@@ -102,6 +103,7 @@
fun theorems
(((dname, _), cons) : eq, eqs : eq list)
(dom_eqn : typ * (binding * (bool * binding option * typ) list * mixfix) list)
+ (iso_info : Domain_Take_Proofs.iso_info)
(thy : theory) =
let
@@ -111,11 +113,15 @@
(* ----- getting the axioms and definitions --------------------------------- *)
+val ax_abs_iso = #abs_inverse iso_info;
+val ax_rep_iso = #rep_inverse iso_info;
+
+val abs_const = #abs_const iso_info;
+val rep_const = #rep_const iso_info;
+
local
fun ga s dn = PureThy.get_thm thy (dn ^ "." ^ s);
in
- val ax_abs_iso = ga "abs_iso" dname;
- val ax_rep_iso = ga "rep_iso" dname;
val ax_take_0 = ga "take_0" dname;
val ax_take_Suc = ga "take_Suc" dname;
val ax_take_strict = ga "take_strict" dname;
@@ -123,32 +129,6 @@
(* ----- define constructors ------------------------------------------------ *)
-val lhsT = fst dom_eqn;
-
-val rhsT =
- let
- fun mk_arg_typ (lazy, sel, T) = if lazy then mk_uT T else T;
- fun mk_con_typ (bind, args, mx) =
- if null args then oneT else foldr1 mk_sprodT (map mk_arg_typ args);
- fun mk_eq_typ (_, cons) = foldr1 mk_ssumT (map mk_con_typ cons);
- in
- mk_eq_typ dom_eqn
- end;
-
-val rep_const = Const(dname^"_rep", lhsT ->> rhsT);
-
-val abs_const = Const(dname^"_abs", rhsT ->> lhsT);
-
-val iso_info : Domain_Take_Proofs.iso_info =
- {
- absT = lhsT,
- repT = rhsT,
- abs_const = abs_const,
- rep_const = rep_const,
- abs_inverse = ax_abs_iso,
- rep_inverse = ax_rep_iso
- };
-
val (result, thy) =
Domain_Constructors.add_domain_constructors
(Long_Name.base_name dname) (snd dom_eqn) iso_info thy;