# HG changeset patch # User huffman # Date 1289258025 28800 # Node ID 1320a07479740f1d58fb37d22433ca9bb3388cbc # Parent 0f2ae76c2e1dcc9aeb5aedee5e8945768592f388 implement defl_of_typ using Pattern.rewrite_term instead of DeflData theory data diff -r 0f2ae76c2e1d -r 1320a0747974 src/HOLCF/Library/Strict_Fun.thy --- a/src/HOLCF/Library/Strict_Fun.thy Mon Nov 08 14:36:17 2010 -0800 +++ b/src/HOLCF/Library/Strict_Fun.thy Mon Nov 08 15:13:45 2010 -0800 @@ -212,8 +212,8 @@ done setup {* - Domain_Isomorphism.add_type_constructor - (@{type_name "sfun"}, @{const_name sfun_defl}, @{const_name sfun_map}, [true, true]) + Domain_Take_Proofs.add_map_function + (@{type_name "sfun"}, @{const_name sfun_map}, [true, true]) *} end diff -r 0f2ae76c2e1d -r 1320a0747974 src/HOLCF/Powerdomains.thy --- a/src/HOLCF/Powerdomains.thy Mon Nov 08 14:36:17 2010 -0800 +++ b/src/HOLCF/Powerdomains.thy Mon Nov 08 15:13:45 2010 -0800 @@ -42,10 +42,10 @@ deflation_upper_map deflation_lower_map deflation_convex_map setup {* - fold Domain_Isomorphism.add_type_constructor - [(@{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])] + fold Domain_Take_Proofs.add_map_function + [(@{type_name "upper_pd"}, @{const_name upper_map}, [true]), + (@{type_name "lower_pd"}, @{const_name lower_map}, [true]), + (@{type_name "convex_pd"}, @{const_name convex_map}, [true])] *} end diff -r 0f2ae76c2e1d -r 1320a0747974 src/HOLCF/Representable.thy --- a/src/HOLCF/Representable.thy Mon Nov 08 14:36:17 2010 -0800 +++ b/src/HOLCF/Representable.thy Mon Nov 08 15:13:45 2010 -0800 @@ -283,12 +283,12 @@ deflation_cprod_map deflation_u_map setup {* - fold Domain_Isomorphism.add_type_constructor - [(@{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])] + fold Domain_Take_Proofs.add_map_function + [(@{type_name cfun}, @{const_name cfun_map}, [true, true]), + (@{type_name ssum}, @{const_name ssum_map}, [true, true]), + (@{type_name sprod}, @{const_name sprod_map}, [true, true]), + (@{type_name prod}, @{const_name cprod_map}, [true, true]), + (@{type_name "u"}, @{const_name u_map}, [true])] *} end diff -r 0f2ae76c2e1d -r 1320a0747974 src/HOLCF/Tools/Domain/domain_isomorphism.ML --- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Mon Nov 08 14:36:17 2010 -0800 +++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Mon Nov 08 15:13:45 2010 -0800 @@ -28,9 +28,6 @@ (string list * binding * mixfix * string * (binding * binding) option) list -> theory -> theory - val add_type_constructor : - (string * string * string * bool list) -> theory -> theory - val setup : theory -> theory end; @@ -52,17 +49,6 @@ (******************************** theory data *********************************) (******************************************************************************) -structure DeflData = Theory_Data -( - (* 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; -); - structure RepData = Named_Thms ( val name = "domain_defl_simps" @@ -81,13 +67,8 @@ val description = "theorems like isodefl d t ==> isodefl (foo_map$d) (foo_defl$t)" ); -fun add_type_constructor - (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 + RepData.setup #> MapIdData.setup #> IsodeflData.setup (******************************************************************************) @@ -105,6 +86,9 @@ fun mk_DEFL T = Const (@{const_name defl}, Term.itselfT T --> deflT) $ Logic.mk_type T; +fun dest_DEFL (Const (@{const_name defl}, _) $ t) = Logic.dest_type t + | dest_DEFL t = raise TERM ("dest_DEFL", [t]); + fun emb_const T = Const (@{const_name emb}, T ->> udomT); fun prj_const T = Const (@{const_name prj}, udomT ->> T); fun coerce_const (T, U) = mk_cfcomp (prj_const U, emb_const T); @@ -214,29 +198,19 @@ fun defl_of_typ (thy : theory) - (tab : (string * bool list) Symtab.table) + (tab : (typ * term) list) (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 (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); - in defl_of T end; - + val defl_simps = RepData.get (ProofContext.init_global thy); + val rules = map (Thm.concl_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq) defl_simps; + val rules' = map (apfst mk_DEFL) tab; + fun defl_proc t = + (case dest_DEFL t of + TFree (a, _) => SOME (Free (Library.unprefix "'" a, deflT)) + | _ => NONE) handle TERM _ => NONE; + in + Pattern.rewrite_term thy (rules @ rules') [defl_proc] (mk_DEFL T) + end; (******************************************************************************) (********************* declaring definitions and theorems *********************) @@ -440,6 +414,15 @@ (* lookup function for sorts of type variables *) fun the_sort v = the (AList.lookup (op =) sorts v); + (* temporary arities for rewriting *) + val tmp_thy = + let + fun arity (vs, tbind, mx, _, _) = + (Sign.full_name thy tbind, map the_sort vs, @{sort bifinite}); + in + fold AxClass.axiomatize_arity (map arity doms) tmp_thy + end; + (* domain equations *) fun mk_dom_eqn (vs, tbind, mx, rhs, morphs) = let fun arg v = TFree (v, the_sort v); @@ -482,14 +465,19 @@ 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 (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_tab (defl_const, (flags, lhsT)) = + let + val Ts = snd (dest_Type lhsT); + val type_args = map (Logic.mk_type o snd) (filter_out fst (flags ~~ Ts)); + val defl_args = map (mk_DEFL o snd) (filter fst (flags ~~ Ts)); + in + (lhsT, list_ccomb (list_comb (defl_const, type_args), defl_args)) + end; + val defl_tab = + map mk_defl_tab (defl_consts ~~ (defl_flagss ~~ map fst dom_eqns)); fun mk_defl_spec (lhsT, rhsT) = - mk_eqs (defl_of_typ thy defl_tab' lhsT, - defl_of_typ thy defl_tab' rhsT); + mk_eqs (defl_of_typ tmp_thy defl_tab lhsT, + defl_of_typ tmp_thy defl_tab rhsT); val defl_specs = map mk_defl_spec dom_eqns; (* register recursive definition of deflation combinators *)