--- a/src/HOLCF/Tools/Domain/domain_extender.ML Sat Mar 13 14:30:38 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML Sat Mar 13 15:18:25 2010 -0800
@@ -7,25 +7,25 @@
signature DOMAIN_EXTENDER =
sig
val add_domain_cmd:
- string ->
+ binding ->
((string * string option) list * binding * mixfix *
(binding * (bool * binding option * string) list * mixfix) list) list
-> theory -> theory
val add_domain:
- string ->
+ binding ->
((string * string option) list * binding * mixfix *
(binding * (bool * binding option * typ) list * mixfix) list) list
-> theory -> theory
val add_new_domain_cmd:
- string ->
+ binding ->
((string * string option) list * binding * mixfix *
(binding * (bool * binding option * string) list * mixfix) list) list
-> theory -> theory
val add_new_domain:
- string ->
+ binding ->
((string * string option) list * binding * mixfix *
(binding * (bool * binding option * typ) list * mixfix) list) list
-> theory -> theory
@@ -126,7 +126,7 @@
fun gen_add_domain
(prep_typ : theory -> 'a -> typ)
- (comp_dnam : string)
+ (comp_dbind : binding)
(eqs''' : ((string * string option) list * binding * mixfix *
(binding * (bool * binding option * 'a) list * mixfix) list) list)
(thy : theory) =
@@ -192,19 +192,18 @@
|> 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) take_info;
+ ||>> Domain_Theorems.comp_theorems (comp_dbind, eqs) take_info;
in
theorems_thy
- |> Sign.add_path (Long_Name.base_name comp_dnam)
|> PureThy.add_thmss
- [((Binding.name "rews", flat rewss @ take_rews), [])]
+ [((Binding.qualified true "rews" comp_dbind,
+ flat rewss @ take_rews), [])]
|> snd
- |> Sign.parent_path
end;
fun gen_add_new_domain
(prep_typ : theory -> 'a -> typ)
- (comp_dnam : string)
+ (comp_dbind : binding)
(eqs''' : ((string * string option) list * binding * mixfix *
(binding * (bool * binding option * 'a) list * mixfix) list) list)
(thy : theory) =
@@ -268,14 +267,13 @@
|> 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) take_info;
+ ||>> Domain_Theorems.comp_theorems (comp_dbind, eqs) take_info;
in
theorems_thy
- |> Sign.add_path (Long_Name.base_name comp_dnam)
|> PureThy.add_thmss
- [((Binding.name "rews", flat rewss @ take_rews), [])]
+ [((Binding.qualified true "rews" comp_dbind,
+ flat rewss @ take_rews), [])]
|> snd
- |> Sign.parent_path
end;
val add_domain = gen_add_domain Sign.certify_typ;
@@ -314,12 +312,12 @@
(P.$$$ "=" |-- P.enum1 "|" cons_decl);
val domains_decl =
- Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") --
+ Scan.option (P.$$$ "(" |-- P.binding --| P.$$$ ")") --
P.and_list1 domain_decl;
fun mk_domain
(definitional : bool)
- (opt_name : string option,
+ (opt_name : binding option,
doms : ((((string * string option) list * binding) * mixfix) *
((binding * (bool * binding option * string) list) * mixfix) list) list ) =
let
@@ -328,12 +326,13 @@
(binding * (bool * binding option * string) list * mixfix) list) list =
map (fn (((vs, t), mx), cons) =>
(vs, t, mx, map (fn ((c, ds), mx) => (c, ds, mx)) cons)) doms;
- val comp_dnam =
- case opt_name of NONE => space_implode "_" names | SOME s => s;
+ val comp_dbind =
+ case opt_name of NONE => Binding.name (space_implode "_" names)
+ | SOME s => s;
in
if definitional
- then add_new_domain_cmd comp_dnam specs
- else add_domain_cmd comp_dnam specs
+ then add_new_domain_cmd comp_dbind specs
+ else add_domain_cmd comp_dbind specs
end;
val _ =
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML Sat Mar 13 14:30:38 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Sat Mar 13 15:18:25 2010 -0800
@@ -16,7 +16,7 @@
-> theory -> thm list * theory;
val comp_theorems :
- bstring * Domain_Library.eq list ->
+ binding * Domain_Library.eq list ->
Domain_Take_Proofs.take_induct_info ->
theory -> thm list * theory
@@ -207,11 +207,12 @@
(******************************************************************************)
fun prove_induction
- (comp_dnam, eqs : eq list)
+ (comp_dbind : binding, eqs : eq list)
(take_rews : thm list)
(take_info : Domain_Take_Proofs.take_induct_info)
(thy : theory) =
let
+ val comp_dname = Sign.full_name thy comp_dbind;
val dnames = map (fst o fst) eqs;
val conss = map snd eqs;
fun dc_take dn = %%:(dn^"_take");
@@ -286,7 +287,7 @@
val is_emptys = map warn n__eqs;
val is_finite = #is_finite take_info;
val _ = if is_finite
- then message ("Proving finiteness rule for domain "^comp_dnam^" ...")
+ then message ("Proving finiteness rule for domain "^comp_dname^" ...")
else ();
end;
val _ = trace " Proving finite_ind...";
@@ -400,12 +401,12 @@
((Binding.empty, [rule]),
[Rule_Cases.case_names case_ns, Induct.induct_type dname]);
-in thy |> Sign.add_path comp_dnam
- |> snd o PureThy.add_thmss [
- ((Binding.name "finite_ind" , [finite_ind]), []),
- ((Binding.name "ind" , [ind] ), [])]
- |> (snd o PureThy.add_thmss (map ind_rule (dnames ~~ inducts)))
- |> Sign.parent_path
+in
+ thy
+ |> snd o PureThy.add_thmss [
+ ((Binding.qualified true "finite_ind" comp_dbind, [finite_ind]), []),
+ ((Binding.qualified true "ind" comp_dbind, [ind] ), [])]
+ |> (snd o PureThy.add_thmss (map ind_rule (dnames ~~ inducts)))
end; (* prove_induction *)
(******************************************************************************)
@@ -413,13 +414,13 @@
(******************************************************************************)
fun prove_coinduction
- (comp_dnam, eqs : eq list)
+ (comp_dbind : binding, eqs : eq list)
(take_lemmas : thm list)
(thy : theory) : theory =
let
val dnames = map (fst o fst) eqs;
-val comp_dname = Sign.full_bname thy comp_dnam;
+val comp_dname = Sign.full_name thy comp_dbind;
fun dc_take dn = %%:(dn^"_take");
val x_name = idx_name dnames "x";
val n_eqs = length eqs;
@@ -433,7 +434,7 @@
open HOLCF_Library
val dtypes = map (Type o fst) eqs;
val relprod = mk_tupleT (map (fn tp => tp --> tp --> boolT) dtypes);
- val bisim_bind = Binding.name (comp_dnam ^ "_bisim");
+ val bisim_bind = Binding.suffix_name "_bisim" comp_dbind;
val bisim_type = relprod --> boolT;
in
val (bisim_const, thy) =
@@ -449,10 +450,6 @@
fun add_defs_i x = PureThy.add_defs false (map Thm.no_attributes x);
fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy;
- val comp_dname = Sign.full_bname thy comp_dnam;
- val dnames = map (fst o fst) eqs;
- val x_name = idx_name dnames "x";
-
fun one_con (con, args) =
let
val nonrec_args = filter_out is_rec args;
@@ -494,11 +491,9 @@
mk_lam("R", foldr1 mk_conj (mapn one_comp 0 eqs));
in
- val ([ax_bisim_def], thy) =
- thy
- |> Sign.add_path comp_dnam
- |> add_defs_infer [(Binding.name "bisim_def", bisim_eqn)]
- ||> Sign.parent_path;
+ val (ax_bisim_def, thy) =
+ yield_singleton add_defs_infer
+ (Binding.qualified true "bisim_def" comp_dbind, bisim_eqn) thy;
end; (* local *)
(* ----- theorem concerning coinduction ------------------------------------- *)
@@ -555,20 +550,19 @@
in pg [] goal (K tacs) end;
end; (* local *)
-in thy |> Sign.add_path comp_dnam
- |> snd o PureThy.add_thmss [((Binding.name "coind", [coind]), [])]
- |> Sign.parent_path
+in thy |> snd o PureThy.add_thmss
+ [((Binding.qualified true "coind" comp_dbind, [coind]), [])]
end; (* let *)
fun comp_theorems
- (comp_dnam : string, eqs : eq list)
+ (comp_dbind : binding, eqs : eq list)
(take_info : Domain_Take_Proofs.take_induct_info)
(thy : theory) =
let
val map_tab = Domain_Take_Proofs.get_map_tab thy;
val dnames = map (fst o fst) eqs;
-val comp_dname = Sign.full_bname thy comp_dnam;
+val comp_dname = Sign.full_name thy comp_dbind;
(* ----- getting the composite axiom and definitions ------------------------ *)
@@ -596,11 +590,11 @@
(* prove induction rules, unless definition is indirect recursive *)
val thy =
if is_indirect then thy else
- prove_induction (comp_dnam, eqs) take_rews take_info thy;
+ prove_induction (comp_dbind, eqs) take_rews take_info thy;
val thy =
if is_indirect then thy else
- prove_coinduction (comp_dnam, eqs) take_lemmas thy;
+ prove_coinduction (comp_dbind, eqs) take_lemmas thy;
in
(take_rews, thy)