# HG changeset patch # User huffman # Date 1288127999 25200 # Node ID 366309dfaf60a511750b820a6af53be546692347 # Parent d8fd7ae0254fa758bf79ee3cbe57610556b201c7 use Named_Thms instead of Theory_Data for some domain package theorems diff -r d8fd7ae0254f -r 366309dfaf60 src/HOLCF/Domain_Aux.thy --- a/src/HOLCF/Domain_Aux.thy Tue Oct 26 09:00:07 2010 -0700 +++ b/src/HOLCF/Domain_Aux.thy Tue Oct 26 14:19:59 2010 -0700 @@ -260,4 +260,6 @@ use "Tools/Domain/domain_take_proofs.ML" +setup Domain_Take_Proofs.setup + end diff -r d8fd7ae0254f -r 366309dfaf60 src/HOLCF/Library/Strict_Fun.thy --- a/src/HOLCF/Library/Strict_Fun.thy Tue Oct 26 09:00:07 2010 -0700 +++ b/src/HOLCF/Library/Strict_Fun.thy Tue Oct 26 14:19:59 2010 -0700 @@ -69,7 +69,7 @@ where "sfun_map = (\ a b. sfun_abs oo cfun_map\a\b oo sfun_rep)" -lemma sfun_map_ID: "sfun_map\ID\ID = ID" +lemma sfun_map_ID [domain_map_ID]: "sfun_map\ID\ID = ID" unfolding sfun_map_def by (simp add: cfun_map_ID cfun_eq_iff) @@ -103,7 +103,7 @@ done qed -lemma deflation_sfun_map: +lemma deflation_sfun_map [domain_deflation]: assumes 1: "deflation d1" assumes 2: "deflation d2" shows "deflation (sfun_map\d1\d2)" @@ -198,11 +198,11 @@ end -lemma DEFL_sfun: +lemma DEFL_sfun [domain_defl_simps]: "DEFL('a::bifinite \! 'b::bifinite) = sfun_defl\DEFL('a)\DEFL('b)" by (rule defl_sfun_def) -lemma isodefl_sfun: +lemma isodefl_sfun [domain_isodefl]: "isodefl d1 t1 \ isodefl d2 t2 \ isodefl (sfun_map\d1\d2) (sfun_defl\t1\t2)" apply (rule isodeflI) @@ -213,8 +213,7 @@ setup {* Domain_Isomorphism.add_type_constructor - (@{type_name "sfun"}, @{term sfun_defl}, @{const_name sfun_map}, @{thm DEFL_sfun}, - @{thm isodefl_sfun}, @{thm sfun_map_ID}, @{thm deflation_sfun_map}) + (@{type_name "sfun"}, @{term sfun_defl}, @{const_name sfun_map}) *} end diff -r d8fd7ae0254f -r 366309dfaf60 src/HOLCF/Powerdomains.thy --- a/src/HOLCF/Powerdomains.thy Tue Oct 26 09:00:07 2010 -0700 +++ b/src/HOLCF/Powerdomains.thy Tue Oct 26 14:19:59 2010 -0700 @@ -34,19 +34,18 @@ subsection {* Domain package setup for powerdomains *} +lemmas [domain_defl_simps] = DEFL_upper DEFL_lower DEFL_convex +lemmas [domain_map_ID] = upper_map_ID lower_map_ID convex_map_ID +lemmas [domain_isodefl] = isodefl_upper isodefl_lower isodefl_convex + +lemmas [domain_deflation] = + deflation_upper_map deflation_lower_map deflation_convex_map + setup {* fold Domain_Isomorphism.add_type_constructor - [(@{type_name "upper_pd"}, @{term upper_defl}, @{const_name upper_map}, - @{thm DEFL_upper}, @{thm isodefl_upper}, @{thm upper_map_ID}, - @{thm deflation_upper_map}), - - (@{type_name "lower_pd"}, @{term lower_defl}, @{const_name lower_map}, - @{thm DEFL_lower}, @{thm isodefl_lower}, @{thm lower_map_ID}, - @{thm deflation_lower_map}), - - (@{type_name "convex_pd"}, @{term convex_defl}, @{const_name convex_map}, - @{thm DEFL_convex}, @{thm isodefl_convex}, @{thm convex_map_ID}, - @{thm deflation_convex_map})] + [(@{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})] *} end diff -r d8fd7ae0254f -r 366309dfaf60 src/HOLCF/Representable.thy --- a/src/HOLCF/Representable.thy Tue Oct 26 09:00:07 2010 -0700 +++ b/src/HOLCF/Representable.thy Tue Oct 26 14:19:59 2010 -0700 @@ -267,22 +267,28 @@ use "Tools/Domain/domain_isomorphism.ML" +setup Domain_Isomorphism.setup + +lemmas [domain_defl_simps] = + DEFL_cfun DEFL_ssum DEFL_sprod DEFL_prod DEFL_u + +lemmas [domain_map_ID] = + cfun_map_ID ssum_map_ID sprod_map_ID cprod_map_ID u_map_ID + +lemmas [domain_isodefl] = + isodefl_cfun isodefl_ssum isodefl_sprod isodefl_cprod isodefl_u + +lemmas [domain_deflation] = + deflation_cfun_map deflation_ssum_map deflation_sprod_map + deflation_cprod_map deflation_u_map + setup {* fold Domain_Isomorphism.add_type_constructor - [(@{type_name cfun}, @{term cfun_defl}, @{const_name cfun_map}, @{thm DEFL_cfun}, - @{thm isodefl_cfun}, @{thm cfun_map_ID}, @{thm deflation_cfun_map}), - - (@{type_name ssum}, @{term ssum_defl}, @{const_name ssum_map}, @{thm DEFL_ssum}, - @{thm isodefl_ssum}, @{thm ssum_map_ID}, @{thm deflation_ssum_map}), - - (@{type_name sprod}, @{term sprod_defl}, @{const_name sprod_map}, @{thm DEFL_sprod}, - @{thm isodefl_sprod}, @{thm sprod_map_ID}, @{thm deflation_sprod_map}), - - (@{type_name prod}, @{term cprod_defl}, @{const_name cprod_map}, @{thm DEFL_prod}, - @{thm isodefl_cprod}, @{thm cprod_map_ID}, @{thm deflation_cprod_map}), - - (@{type_name "u"}, @{term u_defl}, @{const_name u_map}, @{thm DEFL_u}, - @{thm isodefl_u}, @{thm u_map_ID}, @{thm deflation_u_map})] + [(@{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})] *} end diff -r d8fd7ae0254f -r 366309dfaf60 src/HOLCF/Tools/Domain/domain_isomorphism.ML --- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Tue Oct 26 09:00:07 2010 -0700 +++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Tue Oct 26 14:19:59 2010 -0700 @@ -28,7 +28,9 @@ (string list * binding * mixfix * string * (binding * binding) option) list -> theory -> theory val add_type_constructor : - (string * term * string * thm * thm * thm * thm) -> theory -> theory + (string * term * string) -> theory -> theory + + val setup : theory -> theory end; structure Domain_Isomorphism : DOMAIN_ISOMORPHISM = @@ -55,44 +57,31 @@ fun merge data = Symtab.merge (K true) data; ); -structure RepData = Theory_Data +structure RepData = Named_Thms ( - (* theorems like "DEFL('a foo) = foo_defl$DEFL('a)" *) - type T = thm list; - val empty = []; - val extend = I; - val merge = Thm.merge_thms; + val name = "domain_defl_simps" + val description = "theorems like DEFL('a t) = t_defl$DEFL('a)" +) + +structure MapIdData = Named_Thms +( + val name = "domain_map_ID" + val description = "theorems like foo_map$ID = ID" ); -structure MapIdData = Theory_Data +structure IsodeflData = Named_Thms ( - (* theorems like "foo_map$ID = ID" *) - type T = thm list; - val empty = []; - val extend = I; - val merge = Thm.merge_thms; -); - -structure IsodeflData = Theory_Data -( - (* theorems like "isodefl d t ==> isodefl (foo_map$d) (foo_defl$t)" *) - type T = thm list; - val empty = []; - val extend = I; - val merge = Thm.merge_thms; + val name = "domain_isodefl" + val description = "theorems like isodefl d t ==> isodefl (foo_map$d) (foo_defl$t)" ); fun add_type_constructor - (tname, defl_const, map_name, DEFL_thm, - isodefl_thm, map_ID_thm, defl_map_thm) = + (tname, defl_const, map_name) = DeflData.map (Symtab.insert (K true) (tname, defl_const)) - #> Domain_Take_Proofs.add_map_function (tname, map_name, defl_map_thm) - #> RepData.map (Thm.add_thm DEFL_thm) - #> IsodeflData.map (Thm.add_thm isodefl_thm) - #> MapIdData.map (Thm.add_thm map_ID_thm); + #> Domain_Take_Proofs.add_map_function (tname, map_name) - -(* val get_map_tab = MapData.get; *) +val setup = + RepData.setup #> MapIdData.setup #> IsodeflData.setup (******************************************************************************) @@ -357,15 +346,16 @@ (* register map functions in theory data *) local - fun register_map ((dname, map_name), defl_thm) = - Domain_Take_Proofs.add_map_function (dname, map_name, defl_thm); val dnames = map (fst o dest_Type o fst) dom_eqns; val map_names = map (fst o dest_Const) map_consts; in val thy = - fold register_map (dnames ~~ map_names ~~ deflation_map_thms) thy; + fold Domain_Take_Proofs.add_map_function (dnames ~~ map_names) thy; end; + (* register deflation theorems *) + val thy = fold Domain_Take_Proofs.add_deflation_thm deflation_map_thms thy; + val result = { map_consts = map_consts, @@ -481,13 +471,13 @@ (DEFL, thy) end; val (DEFL_thms, thy) = fold_map make_repdef (doms ~~ defl_consts) thy; - val thy = RepData.map (fold Thm.add_thm DEFL_thms) thy; + val thy = fold (Context.theory_map o RepData.add_thm) DEFL_thms thy; (* prove DEFL equations *) fun mk_DEFL_eq_thm (lhsT, rhsT) = let val goal = mk_eqs (mk_DEFL lhsT, mk_DEFL rhsT); - val DEFL_simps = RepData.get thy; + val DEFL_simps = RepData.get (ProofContext.init_global thy); val tac = rewrite_goals_tac (map mk_meta_eq DEFL_simps) THEN resolve_tac defl_unfold_thms 1; @@ -582,11 +572,12 @@ @{thms adm_conj adm_isodefl cont2cont_fst cont2cont_snd cont_id}; val bottom_rules = @{thms fst_strict snd_strict isodefl_bottom simp_thms}; - val DEFL_simps = map (fn th => th RS sym) (RepData.get thy); + val lthy = ProofContext.init_global thy; + val DEFL_simps = map (fn th => th RS sym) (RepData.get lthy); val isodefl_rules = @{thms conjI isodefl_ID_DEFL} @ isodefl_abs_rep_thms - @ IsodeflData.get thy; + @ IsodeflData.get (ProofContext.init_global thy); in Goal.prove_global thy [] assms goal (fn {prems, ...} => EVERY @@ -612,7 +603,7 @@ val (isodefl_thms, thy) = thy |> (Global_Theory.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes)) (conjuncts isodefl_binds isodefl_thm); - val thy = IsodeflData.map (fold Thm.add_thm isodefl_thms) thy; + val thy = fold (Context.theory_map o IsodeflData.add_thm) isodefl_thms thy; (* prove map_ID theorems *) fun prove_map_ID_thm @@ -636,7 +627,7 @@ val (_, thy) = thy |> (Global_Theory.add_thms o map Thm.no_attributes) (map_ID_binds ~~ map_ID_thms); - val thy = MapIdData.map (fold Thm.add_thm map_ID_thms) thy; + val thy = fold (Context.theory_map o MapIdData.add_thm) map_ID_thms thy; (* definitions and proofs related to take functions *) val (take_info, thy) = @@ -653,10 +644,11 @@ list_ccomb (map_const, map mk_ID (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); val start_rules = @{thms thelub_Pair [symmetric] ch2ch_Pair} @ chain_take_thms @ @{thms pair_collapse split_def} - @ map_apply_thms @ MapIdData.get thy; + @ map_apply_thms @ map_ID_thms; val rules0 = @{thms iterate_0 Pair_strict} @ take_0_thms; val rules1 = diff -r d8fd7ae0254f -r 366309dfaf60 src/HOLCF/Tools/Domain/domain_take_proofs.ML --- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML Tue Oct 26 09:00:07 2010 -0700 +++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML Tue Oct 26 14:19:59 2010 -0700 @@ -55,11 +55,11 @@ val map_of_typ : theory -> (typ * term) list -> typ -> term - val add_map_function : - (string * string * thm) -> theory -> theory - + val add_map_function : (string * string) -> theory -> theory val get_map_tab : theory -> string Symtab.table + val add_deflation_thm : thm -> theory -> theory val get_deflation_thms : theory -> thm list + val setup : theory -> theory end; structure Domain_Take_Proofs : DOMAIN_TAKE_PROOFS = @@ -126,21 +126,22 @@ fun merge data = Symtab.merge (K true) data; ); -structure DeflMapData = Theory_Data +structure DeflMapData = Named_Thms ( - (* theorems like "deflation a ==> deflation (foo_map$a)" *) - type T = thm list; - val empty = []; - val extend = I; - val merge = Thm.merge_thms; + val name = "domain_deflation" + val description = "theorems like deflation a ==> deflation (foo_map$a)" ); -fun add_map_function (tname, map_name, deflation_map_thm) = - MapData.map (Symtab.insert (K true) (tname, map_name)) - #> DeflMapData.map (Thm.add_thm deflation_map_thm); +fun add_map_function (tname, map_name) = + MapData.map (Symtab.insert (K true) (tname, map_name)); + +fun add_deflation_thm thm = + Context.theory_map (DeflMapData.add_thm thm); val get_map_tab = MapData.get; -val get_deflation_thms = DeflMapData.get; +fun get_deflation_thms thy = DeflMapData.get (ProofContext.init_global thy); + +val setup = DeflMapData.setup; (******************************************************************************) (************************** building types and terms **************************) @@ -344,7 +345,7 @@ val deflation_rules = @{thms conjI deflation_ID} @ deflation_abs_rep_thms - @ DeflMapData.get thy; + @ get_deflation_thms thy; in Goal.prove_global thy [] [] goal (fn _ => EVERY