# HG changeset patch # User huffman # Date 1267589057 28800 # Node ID 089e438b925b57a0f88b0a420944b2cdc33b8bdf # Parent 297e801b54658de20e8e597cc32ffade10bab7b6 simplify add_axioms function; remove obsolete domain_syntax.ML diff -r 297e801b5465 -r 089e438b925b src/HOLCF/Domain.thy --- a/src/HOLCF/Domain.thy Tue Mar 02 19:45:37 2010 -0800 +++ b/src/HOLCF/Domain.thy Tue Mar 02 20:04:17 2010 -0800 @@ -274,7 +274,6 @@ use "Tools/cont_consts.ML" use "Tools/cont_proc.ML" use "Tools/Domain/domain_library.ML" -use "Tools/Domain/domain_syntax.ML" use "Tools/Domain/domain_axioms.ML" use "Tools/Domain/domain_constructors.ML" use "Tools/Domain/domain_theorems.ML" diff -r 297e801b5465 -r 089e438b925b src/HOLCF/Tools/Domain/domain_axioms.ML --- a/src/HOLCF/Tools/Domain/domain_axioms.ML Tue Mar 02 19:45:37 2010 -0800 +++ b/src/HOLCF/Tools/Domain/domain_axioms.ML Tue Mar 02 20:04:17 2010 -0800 @@ -1,22 +1,22 @@ (* Title: HOLCF/Tools/Domain/domain_axioms.ML Author: David von Oheimb + Author: Brian Huffman Syntax generator for domain command. *) signature DOMAIN_AXIOMS = sig + val axiomatize_isomorphism : + binding * (typ * typ) -> + theory -> Domain_Take_Proofs.iso_info * theory + val copy_of_dtyp : string Symtab.table -> (int -> term) -> Datatype.dtyp -> term - val calc_axioms : - Domain_Library.eq list -> int -> Domain_Library.eq -> - string * (string * term) list - val add_axioms : - ((string * typ list) * - (binding * (bool * binding option * typ) list * mixfix) list) list -> - Domain_Library.eq list -> theory -> theory + (binding * (typ * typ)) list -> + theory -> theory end; @@ -46,24 +46,57 @@ SOME f => list_ccomb (%%:f, map (copy_of_dtyp tab r) ds) | NONE => (warning ("copy_of_dtyp: unknown type constructor " ^ c); ID); -fun calc_axioms - (eqs : eq list) - (n : int) - (eqn as ((dname,_),cons) : eq) - : string * (string * term) list = +local open HOLCF_Library in + +fun axiomatize_isomorphism + (dbind : binding, (lhsT, rhsT)) + (thy : theory) + : Domain_Take_Proofs.iso_info * theory = let - val dc_abs = %%:(dname^"_abs"); - val dc_rep = %%:(dname^"_rep"); - val x_name'= "x"; - val x_name = idx_name eqs x_name' (n+1); - val dnam = Long_Name.base_name dname; + val dname = Long_Name.base_name (Binding.name_of dbind); + + val abs_bind = Binding.suffix_name "_abs" dbind; + val rep_bind = Binding.suffix_name "_rep" dbind; + + val (abs_const, thy) = + Sign.declare_const ((abs_bind, rhsT ->> lhsT), NoSyn) thy; + val (rep_const, thy) = + Sign.declare_const ((rep_bind, lhsT ->> rhsT), NoSyn) thy; + + val x = Free ("x", lhsT); + val y = Free ("y", rhsT); + + val abs_iso_eqn = + Logic.all y (mk_trp (mk_eq (rep_const ` (abs_const ` y), y))); + val rep_iso_eqn = + Logic.all x (mk_trp (mk_eq (abs_const ` (rep_const ` x), x))); + + val thy = Sign.add_path dname thy; - 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')); + val (abs_iso_thm, thy) = + yield_singleton PureThy.add_axioms + ((Binding.name "abs_iso", abs_iso_eqn), []) thy; + + val (rep_iso_thm, thy) = + yield_singleton PureThy.add_axioms + ((Binding.name "rep_iso", rep_iso_eqn), []) thy; + + val thy = Sign.parent_path thy; + + val result = + { + absT = lhsT, + repT = rhsT, + abs_const = abs_const, + rep_const = rep_const, + abs_inverse = abs_iso_thm, + rep_inverse = rep_iso_thm + }; in - (dnam, [abs_iso_ax, rep_iso_ax]) + (result, thy) end; +end; (* legacy type inference *) @@ -78,52 +111,30 @@ 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_axioms eqs' (eqs : eq list) thy' = +fun add_axioms + (dom_eqns : (binding * (typ * typ)) list) + (thy : theory) = let - val dnames = map (fst o fst) eqs; - val x_name = idx_name dnames "x"; + + (* declare and axiomatize abs/rep *) + val (iso_infos, thy) = + fold_map axiomatize_isomorphism dom_eqns thy; fun add_one (dnam, axs) = Sign.add_path dnam #> add_axioms_infer axs #> Sign.parent_path; - val axs = mapn (calc_axioms eqs) 0 eqs; - val thy = thy' |> fold add_one axs; - - fun get_iso_info ((dname, tyvars), cons') = - let - fun opt_lazy (lazy,_,t) = if lazy then mk_uT t else t - fun prod (_,args,_) = - case args of [] => oneT - | _ => foldr1 mk_sprodT (map opt_lazy args); - val ax_abs_iso = PureThy.get_thm thy (dname ^ ".abs_iso"); - val ax_rep_iso = PureThy.get_thm thy (dname ^ ".rep_iso"); - val lhsT = Type(dname,tyvars); - val rhsT = foldr1 mk_ssumT (map prod cons'); - val rep_const = Const(dname^"_rep", lhsT ->> rhsT); - val abs_const = Const(dname^"_abs", rhsT ->> lhsT); - in - { - absT = lhsT, - repT = rhsT, - abs_const = abs_const, - rep_const = rep_const, - abs_inverse = ax_abs_iso, - rep_inverse = ax_rep_iso - } - end; - val dom_binds = map (Binding.name o Long_Name.base_name) dnames; + (* define take function *) val (take_info, thy) = Domain_Take_Proofs.define_take_functions - (dom_binds ~~ map get_iso_info eqs') thy; + (map fst dom_eqns ~~ iso_infos) thy; (* declare lub_take axioms *) local - fun ax_lub_take dname = + fun ax_lub_take (dbind, take_const) = let - val dnam : string = Long_Name.base_name dname; - val take_const = %%:(dname^"_take"); + val dnam = Long_Name.base_name (Binding.name_of dbind); val lub = %%: @{const_name lub}; val image = %%: @{const_name image}; val UNIV = @{term "UNIV :: nat set"}; @@ -132,11 +143,14 @@ in add_one (dnam, [("lub_take", ax)]) end + val dbinds = map fst dom_eqns; + val take_consts = #take_consts take_info; in - val thy = fold ax_lub_take dnames thy + val thy = fold ax_lub_take (dbinds ~~ take_consts) thy end; + in - thy - end; (* let (add_axioms) *) + thy (* TODO: also return iso_infos, take_info, lub_take_thms *) + end; end; (* struct *) diff -r 297e801b5465 -r 089e438b925b src/HOLCF/Tools/Domain/domain_extender.ML --- a/src/HOLCF/Tools/Domain/domain_extender.ML Tue Mar 02 19:45:37 2010 -0800 +++ b/src/HOLCF/Tools/Domain/domain_extender.ML Tue Mar 02 20:04:17 2010 -0800 @@ -153,6 +153,8 @@ |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs end; + val dbinds : binding list = + map (fn (_,dbind,_,_) => dbind) eqs'''; val cons''' : (binding * (bool * binding option * 'a) list * mixfix) list list = map (fn (_,_,_,cons) => cons) eqs'''; @@ -164,7 +166,7 @@ val eqs' : ((string * typ list) * (binding * (bool * binding option * typ) list * mixfix) list) list = check_and_sort_domain false dtnvs' cons'' thy; - val thy = Domain_Syntax.add_syntax eqs' thy; +(* val thy = Domain_Syntax.add_syntax eqs' thy; *) val dts : typ list = map (Type o fst) eqs'; val new_dts : (string * string list) list = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs'; @@ -175,7 +177,15 @@ (args, Datatype_Prop.make_tnames (map third args))); val eqs : eq list = map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs'; - val thy = Domain_Axioms.add_axioms eqs' eqs thy; + + fun mk_arg_typ (lazy, dest_opt, 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); + 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 ((rewss, take_rews), theorems_thy) = thy |> fold_map (fn (eq, (x,cs)) => diff -r 297e801b5465 -r 089e438b925b src/HOLCF/Tools/Domain/domain_syntax.ML --- a/src/HOLCF/Tools/Domain/domain_syntax.ML Tue Mar 02 19:45:37 2010 -0800 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,62 +0,0 @@ -(* Title: HOLCF/Tools/Domain/domain_syntax.ML - Author: David von Oheimb - -Syntax generator for domain command. -*) - -signature DOMAIN_SYNTAX = -sig - val calc_syntax: - theory -> - (string * typ list) * - (binding * (bool * binding option * typ) list * mixfix) list -> - (binding * typ * mixfix) list - - val add_syntax: - ((string * typ list) * - (binding * (bool * binding option * typ) list * mixfix) list) list -> - theory -> theory -end; - - -structure Domain_Syntax :> DOMAIN_SYNTAX = -struct - -open Domain_Library; -infixr 5 -->; infixr 6 ->>; - -fun calc_syntax thy - ((dname : string, typevars : typ list), - (cons': (binding * (bool * binding option * typ) list * mixfix) list)) - : (binding * typ * mixfix) list = - let -(* ----- constants concerning the isomorphism ------------------------------- *) - local - fun opt_lazy (lazy,_,t) = if lazy then mk_uT t else t - fun prod (_,args,_) = case args of [] => oneT - | _ => foldr1 mk_sprodT (map opt_lazy args); - in - val dtype = Type(dname,typevars); - val dtype2 = foldr1 mk_ssumT (map prod cons'); - val dnam = Long_Name.base_name dname; - fun dbind s = Binding.name (dnam ^ s); - val const_rep = (dbind "_rep" , dtype ->> dtype2, NoSyn); - val const_abs = (dbind "_abs" , dtype2 ->> dtype , NoSyn); - end; - - in [const_rep, const_abs] end; - -(* ----- putting all the syntax stuff together ------------------------------ *) - -fun add_syntax - (eqs' : ((string * typ list) * - (binding * (bool * binding option * typ) list * mixfix) list) list) - (thy : theory) = - let - val ctt : (binding * typ * mixfix) list list = - map (calc_syntax thy) eqs'; - in - Cont_Consts.add_consts (flat ctt) thy - end; - -end; (* struct *)