# HG changeset patch # User huffman # Date 1288203036 25200 # Node ID f7d4d023a899744c689a29a2e8760dbf249c355d # Parent 656bb85f01ab1e9409fc371fa9bb3e26a749c6f1 make domain package work with non-cpo argument types diff -r 656bb85f01ab -r f7d4d023a899 src/HOLCF/Library/Strict_Fun.thy --- a/src/HOLCF/Library/Strict_Fun.thy Wed Oct 27 11:06:53 2010 -0700 +++ b/src/HOLCF/Library/Strict_Fun.thy Wed Oct 27 11:10:36 2010 -0700 @@ -213,7 +213,7 @@ setup {* Domain_Isomorphism.add_type_constructor - (@{type_name "sfun"}, @{term sfun_defl}, @{const_name sfun_map}) + (@{type_name "sfun"}, @{const_name sfun_defl}, @{const_name sfun_map}, [true, true]) *} end diff -r 656bb85f01ab -r f7d4d023a899 src/HOLCF/Powerdomains.thy --- a/src/HOLCF/Powerdomains.thy Wed Oct 27 11:06:53 2010 -0700 +++ b/src/HOLCF/Powerdomains.thy Wed Oct 27 11:10:36 2010 -0700 @@ -43,9 +43,9 @@ setup {* fold Domain_Isomorphism.add_type_constructor - [(@{type_name "upper_pd"}, @{term upper_defl}, @{const_name upper_map}), - (@{type_name "lower_pd"}, @{term lower_defl}, @{const_name lower_map}), - (@{type_name "convex_pd"}, @{term convex_defl}, @{const_name convex_map})] + [(@{type_name "upper_pd"}, @{const_name upper_defl}, @{const_name upper_map}, [true]), + (@{type_name "lower_pd"}, @{const_name lower_defl}, @{const_name lower_map}, [true]), + (@{type_name "convex_pd"}, @{const_name convex_defl}, @{const_name convex_map}, [true])] *} end diff -r 656bb85f01ab -r f7d4d023a899 src/HOLCF/Representable.thy --- a/src/HOLCF/Representable.thy Wed Oct 27 11:06:53 2010 -0700 +++ b/src/HOLCF/Representable.thy Wed Oct 27 11:10:36 2010 -0700 @@ -284,11 +284,11 @@ setup {* fold Domain_Isomorphism.add_type_constructor - [(@{type_name cfun}, @{term cfun_defl}, @{const_name cfun_map}), - (@{type_name ssum}, @{term ssum_defl}, @{const_name ssum_map}), - (@{type_name sprod}, @{term sprod_defl}, @{const_name sprod_map}), - (@{type_name prod}, @{term cprod_defl}, @{const_name cprod_map}), - (@{type_name "u"}, @{term u_defl}, @{const_name u_map})] + [(@{type_name cfun}, @{const_name cfun_defl}, @{const_name cfun_map}, [true, true]), + (@{type_name ssum}, @{const_name ssum_defl}, @{const_name ssum_map}, [true, true]), + (@{type_name sprod}, @{const_name sprod_defl}, @{const_name sprod_map}, [true, true]), + (@{type_name prod}, @{const_name prod_defl}, @{const_name cprod_map}, [true, true]), + (@{type_name "u"}, @{const_name u_defl}, @{const_name u_map}, [true])] *} end diff -r 656bb85f01ab -r f7d4d023a899 src/HOLCF/Tools/Domain/domain_isomorphism.ML --- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Wed Oct 27 11:06:53 2010 -0700 +++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Wed Oct 27 11:10:36 2010 -0700 @@ -27,8 +27,9 @@ val domain_isomorphism_cmd : (string list * binding * mixfix * string * (binding * binding) option) list -> theory -> theory + val add_type_constructor : - (string * term * string) -> theory -> theory + (string * string * string * bool list) -> theory -> theory val setup : theory -> theory end; @@ -44,14 +45,19 @@ val beta_tac = simp_tac beta_ss; +fun is_cpo thy T = Sign.of_sort thy (T, @{sort cpo}); +fun is_bifinite thy T = Sign.of_sort thy (T, @{sort bifinite}); + (******************************************************************************) (******************************** theory data *********************************) (******************************************************************************) structure DeflData = Theory_Data ( - (* terms like "foo_defl" *) - type T = term Symtab.table; + (* constant names like "foo_defl" *) + (* list indicates which type arguments correspond to deflation parameters *) + (* alternatively, which type arguments allow indirect recursion *) + type T = (string * bool list) Symtab.table; val empty = Symtab.empty; val extend = I; fun merge data = Symtab.merge (K true) data; @@ -76,9 +82,9 @@ ); fun add_type_constructor - (tname, defl_const, map_name) = - DeflData.map (Symtab.insert (K true) (tname, defl_const)) - #> Domain_Take_Proofs.add_map_function (tname, map_name) + (tname, defl_name, map_name, flags) = + DeflData.map (Symtab.insert (K true) (tname, (defl_name, flags))) + #> Domain_Take_Proofs.add_map_function (tname, map_name, flags) val setup = RepData.setup #> MapIdData.setup #> IsodeflData.setup @@ -91,15 +97,11 @@ open HOLCF_Library; infixr 6 ->>; -infix -->>; +infixr -->>; val udomT = @{typ udom}; val deflT = @{typ "defl"}; -fun mapT (T as Type (_, Ts)) = - (map (fn T => T ->> T) Ts) -->> (T ->> T) - | mapT T = T ->> T; - fun mk_DEFL T = Const (@{const_name defl}, Term.itselfT T --> deflT) $ Logic.mk_type T; @@ -155,6 +157,8 @@ case lhs of Const (@{const_name Rep_CFun}, _) $ f $ (x as Free _) => mk_eqn (f, big_lambda x rhs) + | f $ Const (@{const_name TYPE}, T) => + mk_eqn (f, Abs ("t", T, rhs)) | Const _ => Logic.mk_equals (lhs, rhs) | _ => raise TERM ("lhs not of correct form", [lhs, rhs]); val eqns = map mk_eqn projs; @@ -204,17 +208,30 @@ (****************** deflation combinators and map functions *******************) (******************************************************************************) +fun mk_defl_type (flags : bool list) (Ts : typ list) = + map (Term.itselfT o snd) (filter_out fst (flags ~~ Ts)) ---> + map (K deflT) (filter I flags) -->> deflT; + fun defl_of_typ - (tab : term Symtab.table) + (thy : theory) + (tab : (string * bool list) Symtab.table) (T : typ) : term = let fun is_closed_typ (Type (_, Ts)) = forall is_closed_typ Ts + | is_closed_typ (TFree (n, s)) = not (Sign.subsort thy (s, @{sort bifinite})) | is_closed_typ _ = false; fun defl_of (TFree (a, _)) = Free (Library.unprefix "'" a, deflT) | defl_of (TVar _) = error ("defl_of_typ: TVar") | defl_of (T as Type (c, Ts)) = case Symtab.lookup tab c of - SOME t => list_ccomb (t, map defl_of Ts) + SOME (s, flags) => + let + val defl_const = Const (s, mk_defl_type flags Ts); + val type_args = map (Logic.mk_type o snd) (filter_out fst (flags ~~ Ts)); + val defl_args = map (defl_of o snd) (filter fst (flags ~~ Ts)); + in + list_ccomb (list_comb (defl_const, type_args), defl_args) + end | NONE => if is_closed_typ T then mk_DEFL T else error ("defl_of_typ: type variable under unsupported type constructor " ^ c); @@ -258,6 +275,10 @@ val dom_eqns = map (fn x => (#absT x, #repT x)) iso_infos; val rep_abs_consts = map (fn x => (#rep_const x, #abs_const x)) iso_infos; + fun mapT (T as Type (_, Ts)) = + (map (fn T => T ->> T) (filter (is_cpo thy) Ts)) -->> (T ->> T) + | mapT T = T ->> T; + (* declare map functions *) fun declare_map_const (tbind, (lhsT, rhsT)) thy = let @@ -274,7 +295,7 @@ fun unprime a = Library.unprefix "'" a; fun mapvar T = Free (unprime (fst (dest_TFree T)), T ->> T); fun map_lhs (map_const, lhsT) = - (lhsT, list_ccomb (map_const, map mapvar (snd (dest_Type lhsT)))); + (lhsT, list_ccomb (map_const, map mapvar (filter (is_cpo thy) (snd (dest_Type lhsT))))); val tab1 = map map_lhs (map_consts ~~ map fst dom_eqns); val Ts = (snd o dest_Type o fst o hd) dom_eqns; val tab = (Ts ~~ map mapvar Ts) @ tab1; @@ -304,9 +325,9 @@ fun mk_goal (map_const, (lhsT, rhsT)) = let val (_, Ts) = dest_Type lhsT; - val map_term = list_ccomb (map_const, map mk_f Ts); + val map_term = list_ccomb (map_const, map mk_f (filter (is_cpo thy) Ts)); in mk_deflation map_term end; - val assms = (map mk_assm o snd o dest_Type o fst o hd) dom_eqns; + val assms = (map mk_assm o filter (is_cpo thy) o snd o dest_Type o fst o hd) dom_eqns; val goals = map mk_goal (map_consts ~~ dom_eqns); val goal = mk_trp (foldr1 HOLogic.mk_conj goals); val start_thms = @@ -346,11 +367,15 @@ (* register map functions in theory data *) local + fun register_map ((dname, map_name), args) = + Domain_Take_Proofs.add_map_function (dname, map_name, args); val dnames = map (fst o dest_Type o fst) dom_eqns; val map_names = map (fst o dest_Const) map_consts; + fun args (T, _) = case T of Type (_, Ts) => map (is_cpo thy) Ts | _ => []; + val argss = map args dom_eqns; in val thy = - fold Domain_Take_Proofs.add_map_function (dnames ~~ map_names) thy; + fold register_map (dnames ~~ map_names ~~ argss) thy; end; (* register deflation theorems *) @@ -433,25 +458,35 @@ val dbinds = map (fn (_, dbind, _, _, _) => dbind) doms; val morphs = map (fn (_, _, _, _, morphs) => morphs) doms; + (* determine deflation combinator arguments *) + fun defl_flags (vs, tbind, mx, rhs, morphs) = + let fun argT v = TFree (v, the (AList.lookup (op =) sorts v)); + in map (is_bifinite thy o argT) vs end; + val defl_flagss = map defl_flags doms; + (* declare deflation combinator constants *) fun declare_defl_const (vs, tbind, mx, rhs, morphs) thy = let - val defl_type = map (K deflT) vs -->> deflT; + fun argT v = TFree (v, the (AList.lookup (op =) sorts v)); + val Ts = map argT vs; + val flags = map (is_bifinite thy) Ts; + val defl_type = mk_defl_type flags Ts; val defl_bind = Binding.suffix_name "_defl" tbind; in Sign.declare_const ((defl_bind, defl_type), NoSyn) thy end; val (defl_consts, thy) = fold_map declare_defl_const doms thy; + val defl_names = map (fst o dest_Const) defl_consts; (* defining equations for type combinators *) + val dnames = map (fst o dest_Type o fst) dom_eqns; val defl_tab1 = DeflData.get thy; - val defl_tab2 = - Symtab.make (map (fst o dest_Type o fst) dom_eqns ~~ defl_consts); + val defl_tab2 = Symtab.make (dnames ~~ (defl_names ~~ defl_flagss)); val defl_tab' = Symtab.merge (K true) (defl_tab1, defl_tab2); val thy = DeflData.put defl_tab' thy; fun mk_defl_spec (lhsT, rhsT) = - mk_eqs (defl_of_typ defl_tab' lhsT, - defl_of_typ defl_tab' rhsT); + mk_eqs (defl_of_typ thy defl_tab' lhsT, + defl_of_typ thy defl_tab' rhsT); val defl_specs = map mk_defl_spec dom_eqns; (* register recursive definition of deflation combinators *) @@ -462,9 +497,11 @@ (* define types using deflation combinators *) fun make_repdef ((vs, tbind, mx, _, _), defl_const) thy = let - fun tfree a = TFree (a, the (AList.lookup (op =) sorts a)) - val reps = map (mk_DEFL o tfree) vs; - val defl = list_ccomb (defl_const, reps); + fun tfree a = TFree (a, the (AList.lookup (op =) sorts a)); + val Ts = map tfree vs; + val type_args = map Logic.mk_type (filter_out (is_bifinite thy) Ts); + val defl_args = map mk_DEFL (filter (is_bifinite thy) Ts); + val defl = list_ccomb (list_comb (defl_const, type_args), defl_args); val ((_, _, _, {DEFL, ...}), thy) = Repdef.add_repdef false NONE (tbind, map (rpair dummyS) vs, mx) defl NONE thy; in @@ -560,10 +597,12 @@ fun mk_goal ((map_const, defl_const), (T, rhsT)) = let val (_, Ts) = dest_Type T; - val map_term = list_ccomb (map_const, map mk_f Ts); - val defl_term = list_ccomb (defl_const, map mk_d Ts); + val map_term = list_ccomb (map_const, map mk_f (filter (is_cpo thy) Ts)); + val type_args = map Logic.mk_type (filter_out (is_bifinite thy) Ts); + val defl_args = map mk_d (filter (is_bifinite thy) Ts); + val defl_term = list_ccomb (list_comb (defl_const, type_args), defl_args); in isodefl_const T $ map_term $ defl_term end; - val assms = (map mk_assm o snd o dest_Type o fst o hd) dom_eqns; + val assms = (map mk_assm o filter (is_cpo thy) o snd o dest_Type o fst o hd) dom_eqns; val goals = map mk_goal (map_consts ~~ defl_consts ~~ dom_eqns); val goal = mk_trp (foldr1 HOLogic.mk_conj goals); val start_thms = @@ -610,7 +649,8 @@ (((map_const, (lhsT, _)), DEFL_thm), isodefl_thm) = let val Ts = snd (dest_Type lhsT); - val lhs = list_ccomb (map_const, map mk_ID Ts); + fun is_cpo T = Sign.of_sort thy (T, @{sort cpo}); + val lhs = list_ccomb (map_const, map mk_ID (filter is_cpo Ts)); val goal = mk_eqs (lhs, mk_ID lhsT); val tac = EVERY [rtac @{thm isodefl_DEFL_imp_ID} 1, @@ -640,8 +680,9 @@ val lub_take_lemma = let val lhs = mk_tuple (map mk_lub take_consts); + fun is_cpo T = Sign.of_sort thy (T, @{sort cpo}); fun mk_map_ID (map_const, (lhsT, rhsT)) = - list_ccomb (map_const, map mk_ID (snd (dest_Type lhsT))); + list_ccomb (map_const, map mk_ID (filter is_cpo (snd (dest_Type lhsT)))); val rhs = mk_tuple (map mk_map_ID (map_consts ~~ dom_eqns)); val goal = mk_trp (mk_eq (lhs, rhs)); val map_ID_thms = MapIdData.get (ProofContext.init_global thy); diff -r 656bb85f01ab -r f7d4d023a899 src/HOLCF/Tools/Domain/domain_take_proofs.ML --- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML Wed Oct 27 11:06:53 2010 -0700 +++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML Wed Oct 27 11:10:36 2010 -0700 @@ -55,8 +55,8 @@ val map_of_typ : theory -> (typ * term) list -> typ -> term - val add_map_function : (string * string) -> theory -> theory - val get_map_tab : theory -> string Symtab.table + val add_map_function : (string * string * bool list) -> theory -> theory + val get_map_tab : theory -> (string * bool list) Symtab.table val add_deflation_thm : thm -> theory -> theory val get_deflation_thms : theory -> thm list val setup : theory -> theory @@ -120,7 +120,9 @@ structure MapData = Theory_Data ( (* constant names like "foo_map" *) - type T = string Symtab.table; + (* list indicates which type arguments correspond to map arguments *) + (* alternatively, which type arguments allow indirect recursion *) + type T = (string * bool list) Symtab.table; val empty = Symtab.empty; val extend = I; fun merge data = Symtab.merge (K true) data; @@ -132,8 +134,8 @@ val description = "theorems like deflation a ==> deflation (foo_map$a)" ); -fun add_map_function (tname, map_name) = - MapData.map (Symtab.insert (K true) (tname, map_name)); +fun add_map_function (tname, map_name, bs) = + MapData.map (Symtab.insert (K true) (tname, (map_name, bs))); fun add_deflation_thm thm = Context.theory_map (DeflMapData.add_thm thm); @@ -188,10 +190,11 @@ SOME m => (m, true) | NONE => map_of' T and map_of' (T as (Type (c, Ts))) = (case Symtab.lookup map_tab c of - SOME map_name => + SOME (map_name, ds) => let - val map_type = map auto Ts -->> auto T; - val (ms, bs) = map_split map_of Ts; + val Ts' = map snd (filter fst (ds ~~ Ts)); + val map_type = map auto Ts' -->> auto T; + val (ms, bs) = map_split map_of Ts'; in if exists I bs then (list_ccomb (Const (map_name, map_type), ms), true) @@ -235,9 +238,6 @@ val dom_eqns = map (fn x => (#absT x, #repT x)) iso_infos; val rep_abs_consts = map (fn x => (#rep_const x, #abs_const x)) iso_infos; - (* get table of map functions *) - val map_tab = MapData.get thy; - fun mk_projs [] t = [] | mk_projs (x::[]) t = [(x, t)] | mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t);