# HG changeset patch # User huffman # Date 1268519438 28800 # Node ID cae4f840d15d5b3d1a7cc91d44f59f0c942d49f9 # Parent ea0ac5538c53664840a7cd9450aac64698b2d7c8 more consistent use of qualified bindings diff -r ea0ac5538c53 -r cae4f840d15d src/HOLCF/Tools/Domain/domain_axioms.ML --- a/src/HOLCF/Tools/Domain/domain_axioms.ML Sat Mar 13 14:26:26 2010 -0800 +++ b/src/HOLCF/Tools/Domain/domain_axioms.ML Sat Mar 13 14:30:38 2010 -0800 @@ -35,8 +35,6 @@ (thy : theory) : Domain_Take_Proofs.iso_info * theory = let - 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; @@ -53,17 +51,16 @@ 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_bind = Binding.qualified true "abs_iso" dbind; + val rep_iso_bind = Binding.qualified true "rep_iso" dbind; val (abs_iso_thm, thy) = yield_singleton PureThy.add_axioms - ((Binding.name "abs_iso", abs_iso_eqn), []) thy; + ((abs_iso_bind, 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; + ((rep_iso_bind, rep_iso_eqn), []) thy; val result = { @@ -83,21 +80,17 @@ (thy : theory) : thm * theory = let - val dname = Long_Name.base_name (Binding.name_of dbind); - val i = Free ("i", natT); val T = (fst o dest_cfunT o range_type o fastype_of) take_const; val lub_take_eqn = mk_trp (mk_eq (mk_lub (lambda i (take_const $ i)), mk_ID T)); - val thy = Sign.add_path dname thy; + val lub_take_bind = Binding.qualified true "lub_take" dbind; val (lub_take_thm, thy) = yield_singleton PureThy.add_axioms - ((Binding.name "lub_take", lub_take_eqn), []) thy; - - val thy = Sign.parent_path thy; + ((lub_take_bind, lub_take_eqn), []) thy; in (lub_take_thm, thy) end; diff -r ea0ac5538c53 -r cae4f840d15d src/HOLCF/Tools/Domain/domain_isomorphism.ML --- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Sat Mar 13 14:26:26 2010 -0800 +++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Sat Mar 13 14:30:38 2010 -0800 @@ -236,12 +236,9 @@ ((const, def_thm), thy) end; -fun add_qualified_thm name (path, thm) thy = - thy - |> Sign.add_path path - |> yield_singleton PureThy.add_thms - (Thm.no_attributes (Binding.name name, thm)) - ||> Sign.parent_path; +fun add_qualified_thm name (dbind, thm) = + yield_singleton PureThy.add_thms + ((Binding.qualified true name dbind, thm), []); (******************************************************************************) (******************************* main function ********************************) @@ -306,7 +303,7 @@ | dups => error ("Duplicate parameter(s) for domain " ^ quote (Binding.str_of tname) ^ " : " ^ commas dups)) end) doms; - val dom_binds = map (fn (_, tbind, _, _, _) => tbind) doms; + val dbinds = map (fn (_, dbind, _, _, _) => dbind) doms; val morphs = map (fn (_, _, _, _, morphs) => morphs) doms; (* declare deflation combinator constants *) @@ -331,7 +328,7 @@ val defl_specs = map mk_defl_spec dom_eqns; (* register recursive definition of deflation combinators *) - val defl_binds = map (Binding.suffix_name "_defl") dom_binds; + val defl_binds = map (Binding.suffix_name "_defl") dbinds; val ((defl_apply_thms, defl_unfold_thms), thy) = add_fixdefs (defl_binds ~~ defl_specs) thy; @@ -363,7 +360,7 @@ val REP_eq_thms = map mk_REP_eq_thm dom_eqns; (* register REP equations *) - val REP_eq_binds = map (Binding.prefix_name "REP_eq_") dom_binds; + val REP_eq_binds = map (Binding.prefix_name "REP_eq_") dbinds; val (_, thy) = thy |> (PureThy.add_thms o map Thm.no_attributes) (REP_eq_binds ~~ REP_eq_thms); @@ -381,32 +378,27 @@ (((rep_const, abs_const), (rep_def, abs_def)), thy) end; val ((rep_abs_consts, rep_abs_defs), thy) = thy - |> fold_map mk_rep_abs (dom_binds ~~ morphs ~~ dom_eqns) + |> fold_map mk_rep_abs (dbinds ~~ morphs ~~ dom_eqns) |>> ListPair.unzip; (* prove isomorphism and isodefl rules *) fun mk_iso_thms ((tbind, REP_eq), (rep_def, abs_def)) thy = let - fun make thm = Drule.export_without_context (thm OF [REP_eq, abs_def, rep_def]); + fun make thm = + Drule.export_without_context (thm OF [REP_eq, abs_def, rep_def]); val rep_iso_thm = make @{thm domain_rep_iso}; val abs_iso_thm = make @{thm domain_abs_iso}; val isodefl_thm = make @{thm isodefl_abs_rep}; - val rep_iso_bind = Binding.name "rep_iso"; - val abs_iso_bind = Binding.name "abs_iso"; - val isodefl_bind = Binding.name "isodefl_abs_rep"; - val (_, thy) = thy - |> Sign.add_path (Binding.name_of tbind) - |> (PureThy.add_thms o map Thm.no_attributes) - [(rep_iso_bind, rep_iso_thm), - (abs_iso_bind, abs_iso_thm), - (isodefl_bind, isodefl_thm)] - ||> Sign.parent_path; + val thy = thy + |> snd o add_qualified_thm "rep_iso" (tbind, rep_iso_thm) + |> snd o add_qualified_thm "abs_iso" (tbind, abs_iso_thm) + |> snd o add_qualified_thm "isodefl_abs_rep" (tbind, isodefl_thm); in (((rep_iso_thm, abs_iso_thm), isodefl_thm), thy) end; val ((iso_thms, isodefl_abs_rep_thms), thy) = thy - |> fold_map mk_iso_thms (dom_binds ~~ REP_eq_thms ~~ rep_abs_defs) + |> fold_map mk_iso_thms (dbinds ~~ REP_eq_thms ~~ rep_abs_defs) |>> ListPair.unzip; (* collect info about rep/abs *) @@ -434,7 +426,7 @@ Sign.declare_const ((map_bind, map_type), NoSyn) thy end; val (map_consts, thy) = thy |> - fold_map declare_map_const (dom_binds ~~ dom_eqns); + fold_map declare_map_const (dbinds ~~ dom_eqns); (* defining equations for map functions *) local @@ -457,7 +449,7 @@ end; (* register recursive definition of map functions *) - val map_binds = map (Binding.suffix_name "_map") dom_binds; + val map_binds = map (Binding.suffix_name "_map") dbinds; val ((map_apply_thms, map_unfold_thms), thy) = add_fixdefs (map_binds ~~ map_specs) thy; @@ -503,7 +495,7 @@ REPEAT (etac @{thm conjE} 1), REPEAT (resolve_tac (isodefl_rules @ prems) 1 ORELSE atac 1)]) end; - val isodefl_binds = map (Binding.prefix_name "isodefl_") dom_binds; + val isodefl_binds = map (Binding.prefix_name "isodefl_") dbinds; fun conjuncts [] thm = [] | conjuncts (n::[]) thm = [(n, thm)] | conjuncts (n::ns) thm = let @@ -530,7 +522,7 @@ in Goal.prove_global thy [] [] goal (K tac) end; - val map_ID_binds = map (Binding.suffix_name "_map_ID") dom_binds; + val map_ID_binds = map (Binding.suffix_name "_map_ID") dbinds; val map_ID_thms = map prove_map_ID_thm (map_consts ~~ dom_eqns ~~ REP_thms ~~ isodefl_thms); @@ -577,7 +569,7 @@ REPEAT (etac @{thm conjE} 1), REPEAT (resolve_tac (deflation_rules @ prems) 1 ORELSE atac 1)]) end; - val deflation_map_binds = dom_binds |> + val deflation_map_binds = dbinds |> map (Binding.prefix_name "deflation_" o Binding.suffix_name "_map"); val (deflation_map_thms, thy) = thy |> (PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.export_without_context)) @@ -597,7 +589,7 @@ (* definitions and proofs related to take functions *) val (take_info, thy) = Domain_Take_Proofs.define_take_functions - (dom_binds ~~ iso_infos) thy; + (dbinds ~~ iso_infos) thy; val { take_consts, take_defs, chain_take_thms, take_0_thms, take_Suc_thms, deflation_take_thms, finite_consts, finite_defs } = take_info; @@ -632,7 +624,7 @@ end; (* prove lub of take equals ID *) - fun prove_lub_take (((bind, take_const), map_ID_thm), (lhsT, rhsT)) thy = + fun prove_lub_take (((dbind, take_const), map_ID_thm), (lhsT, rhsT)) thy = let val n = Free ("n", natT); val goal = mk_eqs (mk_lub (lambda n (take_const $ n)), mk_ID lhsT); @@ -643,16 +635,16 @@ REPEAT (etac @{thm Pair_inject} 1), atac 1]; val lub_take_thm = Goal.prove_global thy [] [] goal (K tac); in - add_qualified_thm "lub_take" (Binding.name_of bind, lub_take_thm) thy + add_qualified_thm "lub_take" (dbind, lub_take_thm) thy end; val (lub_take_thms, thy) = fold_map prove_lub_take - (dom_binds ~~ take_consts ~~ map_ID_thms ~~ dom_eqns) thy; + (dbinds ~~ take_consts ~~ map_ID_thms ~~ dom_eqns) thy; (* prove additional take theorems *) val (take_info2, thy) = Domain_Take_Proofs.add_lub_take_theorems - (dom_binds ~~ iso_infos) take_info lub_take_thms thy; + (dbinds ~~ iso_infos) take_info lub_take_thms thy; in ((iso_infos, take_info2), thy) end; diff -r ea0ac5538c53 -r cae4f840d15d src/HOLCF/Tools/Domain/domain_take_proofs.ML --- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML Sat Mar 13 14:26:26 2010 -0800 +++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML Sat Mar 13 14:30:38 2010 -0800 @@ -203,40 +203,17 @@ (********************* declaring definitions and theorems *********************) (******************************************************************************) -fun define_const - (bind : binding, rhs : term) - (thy : theory) - : (term * thm) * theory = - let - val typ = Term.fastype_of rhs; - val (const, thy) = Sign.declare_const ((bind, typ), NoSyn) thy; - val eqn = Logic.mk_equals (const, rhs); - val def = Thm.no_attributes (Binding.suffix_name "_def" bind, eqn); - val (def_thm, thy) = yield_singleton (PureThy.add_defs false) def thy; - in - ((const, def_thm), thy) - end; +fun add_qualified_def name (dbind, eqn) = + yield_singleton (PureThy.add_defs false) + ((Binding.qualified true name dbind, eqn), []); -fun add_qualified_def name (path, eqn) thy = - thy - |> Sign.add_path path - |> yield_singleton (PureThy.add_defs false) - (Thm.no_attributes (Binding.name name, eqn)) - ||> Sign.parent_path; +fun add_qualified_thm name (dbind, thm) = + yield_singleton PureThy.add_thms + ((Binding.qualified true name dbind, thm), []); -fun add_qualified_thm name (path, thm) thy = - thy - |> Sign.add_path path - |> yield_singleton PureThy.add_thms - (Thm.no_attributes (Binding.name name, thm)) - ||> Sign.parent_path; - -fun add_qualified_simp_thm name (path, thm) thy = - thy - |> Sign.add_path path - |> yield_singleton PureThy.add_thms - ((Binding.name name, thm), [Simplifier.simp_add]) - ||> Sign.parent_path; +fun add_qualified_simp_thm name (dbind, thm) = + yield_singleton PureThy.add_thms + ((Binding.qualified true name dbind, thm), [Simplifier.simp_add]); (******************************************************************************) (************************** defining take functions ***************************) @@ -248,11 +225,10 @@ let (* retrieve components of spec *) - val dom_binds = map fst spec; + val dbinds = map fst spec; val iso_infos = map snd spec; 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; - val dnames = map Binding.name_of dom_binds; (* get table of map functions *) val map_tab = MapData.get thy; @@ -268,7 +244,7 @@ val newTs : typ list = map fst dom_eqns; val copy_arg_type = mk_tupleT (map (fn T => T ->> T) newTs); val copy_arg = Free ("f", copy_arg_type); - val copy_args = map snd (mk_projs dom_binds copy_arg); + val copy_args = map snd (mk_projs dbinds copy_arg); fun one_copy_rhs (rep_abs, (lhsT, rhsT)) = let val body = map_of_typ thy (newTs ~~ copy_args) rhsT; @@ -283,40 +259,39 @@ val n = Free ("n", HOLogic.natT); val rhs = mk_iterate (n, take_functional); in - map (lambda n o snd) (mk_projs dom_binds rhs) + map (lambda n o snd) (mk_projs dbinds rhs) end; (* define take constants *) - fun define_take_const ((tbind, take_rhs), (lhsT, rhsT)) thy = + fun define_take_const ((dbind, take_rhs), (lhsT, rhsT)) thy = let val take_type = HOLogic.natT --> lhsT ->> lhsT; - val take_bind = Binding.suffix_name "_take" tbind; + val take_bind = Binding.suffix_name "_take" dbind; val (take_const, thy) = Sign.declare_const ((take_bind, take_type), NoSyn) thy; val take_eqn = Logic.mk_equals (take_const, take_rhs); val (take_def_thm, thy) = - add_qualified_def "take_def" - (Binding.name_of tbind, take_eqn) thy; + add_qualified_def "take_def" (dbind, take_eqn) thy; in ((take_const, take_def_thm), thy) end; val ((take_consts, take_defs), thy) = thy - |> fold_map define_take_const (dom_binds ~~ take_rhss ~~ dom_eqns) + |> fold_map define_take_const (dbinds ~~ take_rhss ~~ dom_eqns) |>> ListPair.unzip; (* prove chain_take lemmas *) - fun prove_chain_take (take_const, dname) thy = + fun prove_chain_take (take_const, dbind) thy = let val goal = mk_trp (mk_chain take_const); val rules = take_defs @ @{thms chain_iterate ch2ch_fst ch2ch_snd}; val tac = simp_tac (HOL_basic_ss addsimps rules) 1; val thm = Goal.prove_global thy [] [] goal (K tac); in - add_qualified_simp_thm "chain_take" (dname, thm) thy + add_qualified_simp_thm "chain_take" (dbind, thm) thy end; val (chain_take_thms, thy) = - fold_map prove_chain_take (take_consts ~~ dnames) thy; + fold_map prove_chain_take (take_consts ~~ dbinds) thy; (* prove take_0 lemmas *) - fun prove_take_0 ((take_const, dname), (lhsT, rhsT)) thy = + fun prove_take_0 ((take_const, dbind), (lhsT, rhsT)) thy = let val lhs = take_const $ @{term "0::nat"}; val goal = mk_eqs (lhs, mk_bottom (lhsT ->> lhsT)); @@ -324,16 +299,16 @@ val tac = simp_tac (HOL_basic_ss addsimps rules) 1; val take_0_thm = Goal.prove_global thy [] [] goal (K tac); in - add_qualified_thm "take_0" (dname, take_0_thm) thy + add_qualified_thm "take_0" (dbind, take_0_thm) thy end; val (take_0_thms, thy) = - fold_map prove_take_0 (take_consts ~~ dnames ~~ dom_eqns) thy; + fold_map prove_take_0 (take_consts ~~ dbinds ~~ dom_eqns) thy; (* prove take_Suc lemmas *) val n = Free ("n", natT); val take_is = map (fn t => t $ n) take_consts; fun prove_take_Suc - (((take_const, rep_abs), dname), (lhsT, rhsT)) thy = + (((take_const, rep_abs), dbind), (lhsT, rhsT)) thy = let val lhs = take_const $ (@{term Suc} $ n); val body = map_of_typ thy (newTs ~~ take_is) rhsT; @@ -344,11 +319,11 @@ val tac = simp_tac (beta_ss addsimps rules) 1; val take_Suc_thm = Goal.prove_global thy [] [] goal (K tac); in - add_qualified_thm "take_Suc" (dname, take_Suc_thm) thy + add_qualified_thm "take_Suc" (dbind, take_Suc_thm) thy end; val (take_Suc_thms, thy) = fold_map prove_take_Suc - (take_consts ~~ rep_abs_consts ~~ dnames ~~ dom_eqns) thy; + (take_consts ~~ rep_abs_consts ~~ dbinds ~~ dom_eqns) thy; (* prove deflation theorems for take functions *) val deflation_abs_rep_thms = map deflation_abs_rep iso_infos; @@ -385,52 +360,52 @@ val (deflation_take_thms, thy) = fold_map (add_qualified_thm "deflation_take") (map (apsnd Drule.export_without_context) - (conjuncts dnames deflation_take_thm)) thy; + (conjuncts dbinds deflation_take_thm)) thy; (* prove strictness of take functions *) - fun prove_take_strict (deflation_take, dname) thy = + fun prove_take_strict (deflation_take, dbind) thy = let val take_strict_thm = Drule.export_without_context (@{thm deflation_strict} OF [deflation_take]); in - add_qualified_thm "take_strict" (dname, take_strict_thm) thy + add_qualified_thm "take_strict" (dbind, take_strict_thm) thy end; val (take_strict_thms, thy) = fold_map prove_take_strict - (deflation_take_thms ~~ dnames) thy; + (deflation_take_thms ~~ dbinds) thy; (* prove take/take rules *) - fun prove_take_take ((chain_take, deflation_take), dname) thy = + fun prove_take_take ((chain_take, deflation_take), dbind) thy = let val take_take_thm = Drule.export_without_context (@{thm deflation_chain_min} OF [chain_take, deflation_take]); in - add_qualified_thm "take_take" (dname, take_take_thm) thy + add_qualified_thm "take_take" (dbind, take_take_thm) thy end; val (take_take_thms, thy) = fold_map prove_take_take - (chain_take_thms ~~ deflation_take_thms ~~ dnames) thy; + (chain_take_thms ~~ deflation_take_thms ~~ dbinds) thy; (* prove take_below rules *) - fun prove_take_below (deflation_take, dname) thy = + fun prove_take_below (deflation_take, dbind) thy = let val take_below_thm = Drule.export_without_context (@{thm deflation.below} OF [deflation_take]); in - add_qualified_thm "take_below" (dname, take_below_thm) thy + add_qualified_thm "take_below" (dbind, take_below_thm) thy end; val (take_below_thms, thy) = fold_map prove_take_below - (deflation_take_thms ~~ dnames) thy; + (deflation_take_thms ~~ dbinds) thy; (* define finiteness predicates *) - fun define_finite_const ((tbind, take_const), (lhsT, rhsT)) thy = + fun define_finite_const ((dbind, take_const), (lhsT, rhsT)) thy = let val finite_type = lhsT --> boolT; - val finite_bind = Binding.suffix_name "_finite" tbind; + val finite_bind = Binding.suffix_name "_finite" dbind; val (finite_const, thy) = Sign.declare_const ((finite_bind, finite_type), NoSyn) thy; val x = Free ("x", lhsT); @@ -440,11 +415,10 @@ (lambda n (mk_eq (mk_capply (take_const $ n, x), x)))); val finite_eqn = Logic.mk_equals (finite_const, finite_rhs); val (finite_def_thm, thy) = - add_qualified_def "finite_def" - (Binding.name_of tbind, finite_eqn) thy; + add_qualified_def "finite_def" (dbind, finite_eqn) thy; 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) + |> fold_map define_finite_const (dbinds ~~ take_consts ~~ dom_eqns) |>> ListPair.unzip; val result = @@ -469,10 +443,9 @@ (lub_take_thms : thm list) (thy : theory) = let - val dom_binds = map fst spec; + val dbinds = map fst spec; val iso_infos = map snd spec; val absTs = map #absT iso_infos; - val dnames = map Binding.name_of dom_binds; val {take_consts, ...} = take_info; val {chain_take_thms, take_0_thms, take_Suc_thms, ...} = take_info; val {finite_consts, finite_defs, ...} = take_info; @@ -530,9 +503,9 @@ val thy = thy |> fold (snd oo add_qualified_thm "finite") - (dnames ~~ finite_thms) + (dbinds ~~ finite_thms) |> fold (snd oo add_qualified_thm "take_induct") - (dnames ~~ take_induct_thms); + (dbinds ~~ take_induct_thms); in ((finite_thms, take_induct_thms), thy) end; @@ -545,39 +518,38 @@ let (* retrieve components of spec *) - val dom_binds = map fst spec; + val dbinds = map fst spec; val iso_infos = map snd spec; val absTs = map #absT iso_infos; val repTs = map #repT iso_infos; - val dnames = map Binding.name_of dom_binds; val {take_consts, take_0_thms, take_Suc_thms, ...} = take_info; val {chain_take_thms, deflation_take_thms, ...} = take_info; (* prove take lemmas *) - fun prove_take_lemma ((chain_take, lub_take), dname) thy = + fun prove_take_lemma ((chain_take, lub_take), dbind) thy = let val take_lemma = Drule.export_without_context (@{thm lub_ID_take_lemma} OF [chain_take, lub_take]); in - add_qualified_thm "take_lemma" (dname, take_lemma) thy + add_qualified_thm "take_lemma" (dbind, take_lemma) thy end; val (take_lemma_thms, thy) = fold_map prove_take_lemma - (chain_take_thms ~~ lub_take_thms ~~ dnames) thy; + (chain_take_thms ~~ lub_take_thms ~~ dbinds) thy; (* prove reach lemmas *) - fun prove_reach_lemma ((chain_take, lub_take), dname) thy = + fun prove_reach_lemma ((chain_take, lub_take), dbind) thy = let val thm = Drule.export_without_context (@{thm lub_ID_reach} OF [chain_take, lub_take]); in - add_qualified_thm "reach" (dname, thm) thy + add_qualified_thm "reach" (dbind, thm) thy end; val (reach_thms, thy) = fold_map prove_reach_lemma - (chain_take_thms ~~ lub_take_thms ~~ dnames) thy; + (chain_take_thms ~~ lub_take_thms ~~ dbinds) thy; (* test for finiteness of domain definitions *) local @@ -608,7 +580,7 @@ val take_inducts = map prove_take_induct (chain_take_thms ~~ lub_take_thms); val thy = fold (snd oo add_qualified_thm "take_induct") - (dnames ~~ take_inducts) thy; + (dbinds ~~ take_inducts) thy; in ((NONE, take_inducts), thy) end;