--- a/src/HOLCF/Tools/Domain/domain_axioms.ML Mon Mar 08 12:21:07 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML Mon Mar 08 12:36:26 2010 -0800
@@ -17,7 +17,6 @@
val add_axioms :
(binding * (typ * typ)) list -> theory ->
(Domain_Take_Proofs.iso_info list
- * Domain_Take_Proofs.take_info
* Domain_Take_Proofs.take_induct_info) * theory
end;
@@ -128,7 +127,7 @@
(map fst dom_eqns ~~ iso_infos) take_info lub_take_thms thy;
in
- ((iso_infos, take_info, take_info2), thy)
+ ((iso_infos, take_info2), thy)
end;
end; (* struct *)
--- a/src/HOLCF/Tools/Domain/domain_extender.ML Mon Mar 08 12:21:07 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML Mon Mar 08 12:36:26 2010 -0800
@@ -184,7 +184,7 @@
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 ((iso_infos, take_info, take_info2), thy) =
+ val ((iso_infos, take_info), thy) =
Domain_Axioms.add_axioms dom_eqns thy;
val ((rewss, take_rews), theorems_thy) =
@@ -192,7 +192,7 @@
|> 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 take_info2;
+ ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs) take_info;
in
theorems_thy
|> Sign.add_path (Long_Name.base_name comp_dnam)
@@ -246,7 +246,7 @@
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);
- val ((iso_infos, take_info, take_info2), thy) = thy |>
+ val ((iso_infos, take_info), thy) = thy |>
Domain_Isomorphism.domain_isomorphism
(map (fn ((vs, dname, mx, _), eq) =>
(map fst vs, dname, mx, mk_eq_typ eq, NONE))
@@ -268,7 +268,7 @@
|> 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 take_info2;
+ ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs) take_info;
in
theorems_thy
|> Sign.add_path (Long_Name.base_name comp_dnam)
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Mon Mar 08 12:21:07 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Mon Mar 08 12:36:26 2010 -0800
@@ -11,7 +11,6 @@
* (binding * binding) option) list ->
theory ->
(Domain_Take_Proofs.iso_info list
- * Domain_Take_Proofs.take_info
* Domain_Take_Proofs.take_induct_info) * theory
val domain_isomorphism_cmd :
@@ -271,7 +270,6 @@
(doms_raw: (string list * binding * mixfix * 'a * (binding * binding) option) list)
(thy: theory)
: (Domain_Take_Proofs.iso_info list
- * Domain_Take_Proofs.take_info
* Domain_Take_Proofs.take_induct_info) * theory =
let
val _ = Theory.requires thy "Representable" "domain isomorphisms";
@@ -656,7 +654,7 @@
Domain_Take_Proofs.add_lub_take_theorems
(dom_binds ~~ iso_infos) take_info lub_take_thms thy;
in
- ((iso_infos, take_info, take_info2), thy)
+ ((iso_infos, take_info2), thy)
end;
val domain_isomorphism = gen_domain_isomorphism cert_typ;
--- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML Mon Mar 08 12:21:07 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML Mon Mar 08 12:36:26 2010 -0800
@@ -17,7 +17,8 @@
rep_inverse : thm
}
type take_info =
- { take_consts : term list,
+ {
+ take_consts : term list,
take_defs : thm list,
chain_take_thms : thm list,
take_0_thms : thm list,
@@ -28,10 +29,19 @@
}
type take_induct_info =
{
- reach_thms : thm list,
- take_lemma_thms : thm list,
- is_finite : bool,
- take_induct_thms : thm list
+ take_consts : term list,
+ take_defs : thm list,
+ chain_take_thms : thm list,
+ take_0_thms : thm list,
+ take_Suc_thms : thm list,
+ deflation_take_thms : thm list,
+ finite_consts : term list,
+ finite_defs : thm list,
+ lub_take_thms : thm list,
+ reach_thms : thm list,
+ take_lemma_thms : thm list,
+ is_finite : bool,
+ take_induct_thms : thm list
}
val define_take_functions :
(binding * iso_info) list -> theory -> take_info * theory
@@ -76,10 +86,19 @@
type take_induct_info =
{
- reach_thms : thm list,
- take_lemma_thms : thm list,
- is_finite : bool,
- take_induct_thms : thm list
+ take_consts : term list,
+ take_defs : thm list,
+ chain_take_thms : thm list,
+ take_0_thms : thm list,
+ take_Suc_thms : thm list,
+ deflation_take_thms : thm list,
+ finite_consts : term list,
+ finite_defs : thm list,
+ lub_take_thms : thm list,
+ reach_thms : thm list,
+ take_lemma_thms : thm list,
+ is_finite : bool,
+ take_induct_thms : thm list
};
val beta_ss =
@@ -596,10 +615,19 @@
val result =
{
- reach_thms = reach_thms,
- take_lemma_thms = take_lemma_thms,
- is_finite = is_finite,
- take_induct_thms = take_induct_thms
+ take_consts = #take_consts take_info,
+ take_defs = #take_defs take_info,
+ chain_take_thms = #chain_take_thms take_info,
+ take_0_thms = #take_0_thms take_info,
+ take_Suc_thms = #take_Suc_thms take_info,
+ deflation_take_thms = #deflation_take_thms take_info,
+ finite_consts = #finite_consts take_info,
+ finite_defs = #finite_defs take_info,
+ lub_take_thms = lub_take_thms,
+ reach_thms = reach_thms,
+ take_lemma_thms = take_lemma_thms,
+ is_finite = is_finite,
+ take_induct_thms = take_induct_thms
};
in
(result, thy)
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML Mon Mar 08 12:21:07 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Mon Mar 08 12:36:26 2010 -0800
@@ -17,7 +17,6 @@
val comp_theorems :
bstring * Domain_Library.eq list ->
- Domain_Take_Proofs.take_info ->
Domain_Take_Proofs.take_induct_info ->
theory -> thm list * theory
@@ -212,7 +211,7 @@
(take_lemmas : thm list)
(axs_reach : thm list)
(take_rews : thm list)
- (take_info : Domain_Take_Proofs.take_info)
+ (take_info : Domain_Take_Proofs.take_induct_info)
(thy : theory) =
let
val dnames = map (fst o fst) eqs;
@@ -228,14 +227,12 @@
in
val axs_rep_iso = map (ga "rep_iso") dnames;
val axs_abs_iso = map (ga "abs_iso") dnames;
- val axs_chain_take = map (ga "chain_take") dnames;
- val lub_take_thms = map (ga "lub_take") dnames;
- val axs_finite_def = map (ga "finite_def") dnames;
val cases = map (ga "casedist" ) dnames;
val con_rews = maps (gts "con_rews" ) dnames;
end;
- val {take_0_thms, take_Suc_thms, ...} = take_info;
+ val {take_0_thms, take_Suc_thms, chain_take_thms, ...} = take_info;
+ val {lub_take_thms, finite_defs, ...} = take_info;
fun one_con p (con, args) =
let
@@ -364,10 +361,10 @@
val goal = mk_trp (%%:(dn^"_finite") $ %:"x");
val tacs = [
rtac @{thm lub_ID_finite} 1,
- resolve_tac axs_chain_take 1,
+ resolve_tac chain_take_thms 1,
resolve_tac lub_take_thms 1,
rtac decisive_thm 1];
- in pg axs_finite_def goal (K tacs) end;
+ in pg finite_defs goal (K tacs) end;
val _ = trace " Proving finites";
val finites = map one_finite (dnames ~~ atomize global_ctxt decisive_lemma);
@@ -378,7 +375,7 @@
fun tacf {prems, context} =
let
fun finite_tacs (finite, fin_ind) = [
- rtac(rewrite_rule axs_finite_def finite RS exE)1,
+ rtac(rewrite_rule finite_defs finite RS exE)1,
etac subst 1,
rtac fin_ind 1,
ind_prems_tac prems];
@@ -417,7 +414,7 @@
cut_facts_tac (subthm :: take (length dnames) prems) 1,
REPEAT (rtac @{thm conjI} 1 ORELSE
EVERY [etac @{thm admD [OF _ ch2ch_Rep_CFunL]} 1,
- resolve_tac axs_chain_take 1,
+ resolve_tac chain_take_thms 1,
asm_simp_tac HOL_basic_ss 1])
]
end;
@@ -612,8 +609,7 @@
fun comp_theorems
(comp_dnam : string, eqs : eq list)
- (take_info : Domain_Take_Proofs.take_info)
- (take_induct_info : Domain_Take_Proofs.take_induct_info)
+ (take_info : Domain_Take_Proofs.take_induct_info)
(thy : theory) =
let
val map_tab = Domain_Take_Proofs.get_map_tab thy;
@@ -639,8 +635,8 @@
(* theorems about take *)
-val take_lemmas = #take_lemma_thms take_induct_info;
-val axs_reach = #reach_thms take_induct_info;
+val take_lemmas = #take_lemma_thms take_info;
+val axs_reach = #reach_thms take_info;
val take_rews =
maps (fn dn => PureThy.get_thms thy (dn ^ ".take_rews")) dnames;