--- a/src/HOLCF/Tools/Domain/domain_axioms.ML Tue Mar 02 13:50:23 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML Tue Mar 02 14:33:34 2010 -0800
@@ -12,7 +12,7 @@
val calc_axioms :
bool ->
Domain_Library.eq list -> int -> Domain_Library.eq ->
- string * (string * term) list * (string * term) list
+ string * (string * term) list
val add_axioms :
bool ->
@@ -53,7 +53,7 @@
(eqs : eq list)
(n : int)
(eqn as ((dname,_),cons) : eq)
- : string * (string * term) list * (string * term) list =
+ : string * (string * term) list =
let
(* ----- axioms and definitions concerning the isomorphism ------------------ *)
@@ -67,17 +67,8 @@
val abs_iso_ax = ("abs_iso", mk_trp(dc_rep`(dc_abs`%x_name') === %:x_name'));
val rep_iso_ax = ("rep_iso", mk_trp(dc_abs`(dc_rep`%x_name') === %:x_name'));
-(* ----- axiom and definitions concerning induction ------------------------- *)
-
- val finite_def =
- ("finite_def",
- %%:(dname^"_finite") ==
- mk_lam(x_name,
- mk_ex("n",(%%:(dname^"_take") $ Bound 0)`Bound 1 === Bound 1)));
-
- in (dnam,
- (if definitional then [] else [abs_iso_ax, rep_iso_ax]),
- [finite_def])
+ in
+ (dnam, if definitional then [] else [abs_iso_ax, rep_iso_ax])
end; (* let (calc_axioms) *)
@@ -94,15 +85,12 @@
fun add_axioms_i x = snd o PureThy.add_axioms (map (Thm.no_attributes o apfst Binding.name) x);
fun add_axioms_infer axms thy = add_axioms_i (infer_props thy axms) thy;
-fun add_defs_i x = snd o (PureThy.add_defs false) (map (Thm.no_attributes o apfst Binding.name) x);
-fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy;
-
fun add_axioms definitional eqs' (eqs : eq list) thy' =
let
val dnames = map (fst o fst) eqs;
val x_name = idx_name dnames "x";
- fun add_one (dnam, axs, dfs) =
+ fun add_one (dnam, axs) =
Sign.add_path dnam
#> add_axioms_infer axs
#> Sign.parent_path;
@@ -138,12 +126,6 @@
else snd (Domain_Take_Proofs.define_take_functions
(dom_binds ~~ map get_iso_info eqs') thy);
- fun add_one' (dnam, axs, dfs) =
- Sign.add_path dnam
- #> add_defs_infer dfs
- #> Sign.parent_path;
- val thy = fold add_one' axs thy;
-
(* declare lub_take axioms *)
local
fun ax_lub_take dname =
@@ -156,7 +138,7 @@
val lhs = lub $ (image $ take_const $ UNIV);
val ax = mk_trp (lhs === ID);
in
- add_one (dnam, [("lub_take", ax)], [])
+ add_one (dnam, [("lub_take", ax)])
end
in
val thy =
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Tue Mar 02 13:50:23 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Tue Mar 02 14:33:34 2010 -0800
@@ -602,8 +602,9 @@
val (take_info, thy) =
Domain_Take_Proofs.define_take_functions
(dom_binds ~~ iso_infos) thy;
- val {take_consts, take_defs, chain_take_thms, take_0_thms,
- take_Suc_thms, deflation_take_thms} = take_info;
+ val { take_consts, take_defs, chain_take_thms, take_0_thms,
+ take_Suc_thms, deflation_take_thms,
+ finite_consts, finite_defs } = take_info;
(* least-upper-bound lemma for take functions *)
val lub_take_lemma =
--- a/src/HOLCF/Tools/Domain/domain_syntax.ML Tue Mar 02 13:50:23 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_syntax.ML Tue Mar 02 14:33:34 2010 -0800
@@ -47,12 +47,10 @@
val const_abs = (dbind "_abs" , dtype2 ->> dtype , NoSyn);
end;
- val const_finite = (dbind "_finite", dtype-->HOLogic.boolT , NoSyn);
-
val optional_consts =
if definitional then [] else [const_rep, const_abs];
- in (optional_consts @ [const_finite])
+ in optional_consts
end; (* let *)
(* ----- putting all the syntax stuff together ------------------------------ *)
--- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML Tue Mar 02 13:50:23 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML Tue Mar 02 14:33:34 2010 -0800
@@ -24,7 +24,9 @@
chain_take_thms : thm list,
take_0_thms : thm list,
take_Suc_thms : thm list,
- deflation_take_thms : thm list
+ deflation_take_thms : thm list,
+ finite_consts : term list,
+ finite_defs : thm list
} * theory
val map_of_typ :
@@ -95,6 +97,7 @@
infixr 6 ->>;
infix -->>;
+infix 9 `;
val deflT = @{typ "udom alg_defl"};
@@ -374,6 +377,31 @@
fold_map prove_take_take
(chain_take_thms ~~ deflation_take_thms ~~ dnames) thy;
+ (* define finiteness predicates *)
+ fun define_finite_const ((tbind, take_const), (lhsT, rhsT)) thy =
+ let
+ val finite_type = lhsT --> boolT;
+ val finite_bind = Binding.suffix_name "_finite" tbind;
+ val (finite_const, thy) =
+ Sign.declare_const ((finite_bind, finite_type), NoSyn) thy;
+ val x = Free ("x", lhsT);
+ val i = Free ("i", natT);
+ val finite_rhs =
+ lambda x (HOLogic.exists_const natT $
+ (lambda i (mk_eq (mk_capply (take_const $ i, x), x))));
+ val finite_eqn = Logic.mk_equals (finite_const, finite_rhs);
+ val (finite_def_thm, thy) =
+ thy
+ |> Sign.add_path (Binding.name_of tbind)
+ |> yield_singleton
+ (PureThy.add_defs false o map Thm.no_attributes)
+ (Binding.name "finite_def", finite_eqn)
+ ||> Sign.parent_path;
+ in ((finite_const, finite_def_thm), thy) end;
+ val ((finite_consts, finite_defs), thy) = thy
+ |> fold_map define_finite_const (dom_binds ~~ take_consts ~~ dom_eqns)
+ |>> ListPair.unzip;
+
val result =
{
take_consts = take_consts,
@@ -381,7 +409,9 @@
chain_take_thms = chain_take_thms,
take_0_thms = take_0_thms,
take_Suc_thms = take_Suc_thms,
- deflation_take_thms = deflation_take_thms
+ deflation_take_thms = deflation_take_thms,
+ finite_consts = finite_consts,
+ finite_defs = finite_defs
};
in