# HG changeset patch # User huffman # Date 1267569214 28800 # Node ID d631dc53ede0e4149796faae45390ad8c388c487 # Parent a2cfa413eaab3f82150d3b27a13f531bb047d194 move definition of finiteness predicate into domain_take_proofs.ML diff -r a2cfa413eaab -r d631dc53ede0 src/HOLCF/Tools/Domain/domain_axioms.ML --- 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 = diff -r a2cfa413eaab -r d631dc53ede0 src/HOLCF/Tools/Domain/domain_isomorphism.ML --- 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 = diff -r a2cfa413eaab -r d631dc53ede0 src/HOLCF/Tools/Domain/domain_syntax.ML --- 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 ------------------------------ *) diff -r a2cfa413eaab -r d631dc53ede0 src/HOLCF/Tools/Domain/domain_take_proofs.ML --- 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