# HG changeset patch # User haftmann # Date 1277064082 -7200 # Node ID de4a8298c6f327ae3535cbf20687f243e4b7a3c8 # Parent 13328f8853c7f8d9fdc7c57165379d3d729c305a# Parent 907e130726750f24a1fedda4f3625b75845c0bad merged diff -r 13328f8853c7 -r de4a8298c6f3 src/HOL/Library/Fset.thy --- a/src/HOL/Library/Fset.thy Fri Jun 18 22:41:16 2010 +0200 +++ b/src/HOL/Library/Fset.thy Sun Jun 20 22:01:22 2010 +0200 @@ -7,22 +7,26 @@ imports More_Set More_List begin -declare mem_def [simp] - subsection {* Lifting *} -datatype 'a fset = Fset "'a set" +typedef (open) 'a fset = "UNIV :: 'a set set" + morphisms member Fset by rule+ -primrec member :: "'a fset \ 'a set" where +lemma member_Fset [simp]: "member (Fset A) = A" - -lemma member_inject [simp]: - "member A = member B \ A = B" - by (cases A, cases B) simp + by (rule Fset_inverse) rule lemma Fset_member [simp]: "Fset (member A) = A" - by (cases A) simp + by (rule member_inverse) + +declare member_inject [simp] + +lemma Fset_inject [simp]: + "Fset A = Fset B \ A = B" + by (simp add: Fset_inject) + +declare mem_def [simp] definition Set :: "'a list \ 'a fset" where "Set xs = Fset (set xs)" @@ -56,6 +60,27 @@ then show ?thesis by (simp add: image_def) qed +definition (in term_syntax) + setify :: "'a\typerep list \ (unit \ Code_Evaluation.term) + \ 'a fset \ (unit \ Code_Evaluation.term)" where + [code_unfold]: "setify xs = Code_Evaluation.valtermify Set {\} xs" + +notation fcomp (infixl "o>" 60) +notation scomp (infixl "o\" 60) + +instantiation fset :: (random) random +begin + +definition + "Quickcheck.random i = Quickcheck.random i o\ (\xs. Pair (setify xs))" + +instance .. + +end + +no_notation fcomp (infixl "o>" 60) +no_notation scomp (infixl "o\" 60) + subsection {* Lattice instantiation *} @@ -117,11 +142,11 @@ lemma empty_Set [code]: "bot = Set []" - by simp + by (simp add: Set_def) lemma UNIV_Set [code]: "top = Coset []" - by simp + by (simp add: Coset_def) definition insert :: "'a \ 'a fset \ 'a fset" where [simp]: "insert x A = Fset (Set.insert x (member A))" @@ -198,9 +223,16 @@ "A < B \ A \ B \ \ B \ (A :: 'a fset)" by (fact less_le_not_le) -lemma eq_fset_subfset_eq [code]: - "eq_class.eq A B \ A \ B \ B \ (A :: 'a fset)" - by (cases A, cases B) (simp add: eq set_eq) +instantiation fset :: (type) eq +begin + +definition + "eq_fset A B \ A \ B \ B \ (A :: 'a fset)" + +instance proof +qed (simp add: eq_fset_def set_eq [symmetric]) + +end subsection {* Functorial operations *} @@ -276,22 +308,6 @@ end -subsection {* Misc operations *} - -lemma size_fset [code]: - "fset_size f A = 0" - "size A = 0" - by (cases A, simp) (cases A, simp) - -lemma fset_case_code [code]: - "fset_case f A = f (member A)" - by (cases A) simp - -lemma fset_rec_code [code]: - "fset_rec f A = f (member A)" - by (cases A) simp - - subsection {* Simplified simprules *} lemma is_empty_simp [simp]: @@ -312,7 +328,7 @@ declare mem_def [simp del] -hide_const (open) is_empty insert remove map filter forall exists card +hide_const (open) setify is_empty insert remove map filter forall exists card Inter Union end diff -r 13328f8853c7 -r de4a8298c6f3 src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Fri Jun 18 22:41:16 2010 +0200 +++ b/src/HOL/Tools/record.ML Sun Jun 20 22:01:22 2010 +0200 @@ -64,7 +64,7 @@ signature ISO_TUPLE_SUPPORT = sig - val add_iso_tuple_type: bstring * (string * sort) list -> + val add_iso_tuple_type: binding * (string * sort) list -> typ * typ -> theory -> (term * term) * theory val mk_cons_tuple: term * term -> term val dest_cons_tuple: term -> term * term @@ -80,7 +80,7 @@ val iso_tuple_intro = @{thm isomorphic_tuple_intro}; val iso_tuple_intros = Tactic.build_net @{thms isomorphic_tuple.intros}; -val tuple_iso_tuple = (@{const_name tuple_iso_tuple}, @{thm tuple_iso_tuple}); +val tuple_iso_tuple = (@{const_name Record.tuple_iso_tuple}, @{thm tuple_iso_tuple}); fun named_cterm_instantiate values thm = let @@ -101,21 +101,21 @@ fun merge data = Symtab.merge Thm.eq_thm_prop data; (* FIXME handle Symtab.DUP ?? *) ); -fun do_typedef name repT alphas thy = +fun do_typedef b repT alphas thy = let - fun get_thms thy name = + val (b_constr, b_proj) = (Binding.prefix_name "make_" b, Binding.prefix_name "dest_" b); + fun get_thms thy tyco = let - val [({Abs_name, abs_type = absT, ...}, {Rep_inject, Abs_inverse, ...})] = - Typedef.get_info_global thy name; - val rewrite_rule = - MetaSimplifier.rewrite_rule [@{thm iso_tuple_UNIV_I}, @{thm iso_tuple_True_simp}]; + val SOME { vs, constr, typ = repT, proj_inject, proj_constr, ... } = + Typecopy.get_info thy tyco; + val absT = Type (tyco, map TFree vs); in - (map rewrite_rule [Rep_inject, Abs_inverse], Const (Abs_name, repT --> absT), absT) + ((proj_inject, proj_constr), Const (constr, repT --> absT), absT) end; in thy - |> Typecopy.typecopy (Binding.name name, alphas) repT NONE - |-> (fn (name, _) => `(fn thy => get_thms thy name)) + |> Typecopy.typecopy (b, alphas) repT b_constr b_proj + |-> (fn (tyco, _) => `(fn thy => get_thms thy tyco)) end; fun mk_cons_tuple (left, right) = @@ -124,21 +124,21 @@ val prodT = HOLogic.mk_prodT (leftT, rightT); val isomT = Type (@{type_name tuple_isomorphism}, [prodT, leftT, rightT]); in - Const (@{const_name iso_tuple_cons}, isomT --> leftT --> rightT --> prodT) $ + Const (@{const_name Record.iso_tuple_cons}, isomT --> leftT --> rightT --> prodT) $ Const (fst tuple_iso_tuple, isomT) $ left $ right end; -fun dest_cons_tuple (Const (@{const_name iso_tuple_cons}, _) $ Const _ $ t $ u) = (t, u) +fun dest_cons_tuple (Const (@{const_name Record.iso_tuple_cons}, _) $ Const _ $ t $ u) = (t, u) | dest_cons_tuple t = raise TERM ("dest_cons_tuple", [t]); -fun add_iso_tuple_type (name, alphas) (leftT, rightT) thy = +fun add_iso_tuple_type (b, alphas) (leftT, rightT) thy = let val repT = HOLogic.mk_prodT (leftT, rightT); - val (([rep_inject, abs_inverse], absC, absT), typ_thy) = + val (((rep_inject, abs_inverse), absC, absT), typ_thy) = thy - |> do_typedef name repT alphas - ||> Sign.add_path name; + |> do_typedef b repT alphas + ||> Sign.add_path (Binding.name_of b); (*FIXME proper prefixing instead*) (*construct a type and body for the isomorphism constant by instantiating the theorem to which the definition will be applied*) @@ -146,7 +146,7 @@ rep_inject RS named_cterm_instantiate [("abst", cterm_of typ_thy absC)] iso_tuple_intro; val (_, body) = Logic.dest_equals (List.last (prems_of intro_inst)); val isomT = fastype_of body; - val isom_binding = Binding.name (name ^ isoN); + val isom_binding = Binding.suffix_name isoN b; val isom_name = Sign.full_name typ_thy isom_binding; val isom = Const (isom_name, isomT); @@ -157,7 +157,7 @@ [((Binding.conceal (Thm.def_binding isom_binding), Logic.mk_equals (isom, body)), [])]; val iso_tuple = isom_def RS (abs_inverse RS (rep_inject RS iso_tuple_intro)); - val cons = Const (@{const_name iso_tuple_cons}, isomT --> leftT --> rightT --> absT); + val cons = Const (@{const_name Record.iso_tuple_cons}, isomT --> leftT --> rightT --> absT); val thm_thy = cdef_thy @@ -1654,7 +1654,7 @@ val suff = if i = 0 then ext_typeN else inner_typeN ^ string_of_int i; val ((_, cons), thy') = thy |> Iso_Tuple_Support.add_iso_tuple_type - (suffix suff base_name, alphas_zeta) (fastype_of left, fastype_of right); + (Binding.suffix_name suff (Binding.name base_name), alphas_zeta) (fastype_of left, fastype_of right); in (cons $ left $ right, (thy', i + 1)) end; @@ -1846,8 +1846,9 @@ fun record_definition (alphas, binding) parent (parents: parent_info list) raw_fields thy = let + val prefix = Binding.name_of binding; val name = Sign.full_name thy binding; - val full = Sign.full_name_path thy (Binding.name_of binding); (* FIXME Binding.qualified (!?) *) + val full = Sign.full_name_path thy prefix; val bfields = map (fn (x, T, _) => (x, T)) raw_fields; val field_syntax = map #3 raw_fields; @@ -1859,7 +1860,7 @@ val parent_fields_len = length parent_fields; val parent_variants = Name.variant_list [moreN, rN, rN ^ "'", wN] (map Long_Name.base_name parent_names); - val parent_vars = ListPair.map Free (parent_variants, parent_types); + val parent_vars = map2 (curry Free) parent_variants parent_types; val parent_len = length parents; val fields = map (apfst full) bfields; @@ -1871,7 +1872,7 @@ val variants = Name.variant_list (moreN :: rN :: (rN ^ "'") :: wN :: parent_variants) (map (Binding.name_of o fst) bfields); - val vars = ListPair.map Free (variants, types); + val vars = map2 (curry Free) variants types; val named_vars = names ~~ vars; val idxms = 0 upto len; @@ -2090,13 +2091,13 @@ map (fn (c, x as Free (_, T)) => mk_sel r_rec0 (c, T) === x) named_vars_more; (*updates*) - fun mk_upd_prop (i, (c, T)) = + fun mk_upd_prop i (c, T) = let val x' = Free (Name.variant all_variants (Long_Name.base_name c ^ "'"), T --> T); val n = parent_fields_len + i; val args' = nth_map n (K (x' $ nth all_vars_more n)) all_vars_more; in mk_upd updateN c x' r_rec0 === mk_rec args' 0 end; - val upd_conv_props = ListPair.map mk_upd_prop (idxms, fields_more); + val upd_conv_props = map2 mk_upd_prop idxms fields_more; (*induct*) val induct_scheme_prop = diff -r 13328f8853c7 -r de4a8298c6f3 src/HOL/Tools/typecopy.ML --- a/src/HOL/Tools/typecopy.ML Fri Jun 18 22:41:16 2010 +0200 +++ b/src/HOL/Tools/typecopy.ML Sun Jun 20 22:01:22 2010 +0200 @@ -6,9 +6,9 @@ signature TYPECOPY = sig - type info = { vs: (string * sort) list, constr: string, typ: typ, - inject: thm, proj: string * typ, proj_def: thm } - val typecopy: binding * (string * sort) list -> typ -> (binding * binding) option + type info = { vs: (string * sort) list, typ: typ, constr: string, proj: string, + constr_inject: thm, proj_inject: thm, constr_proj: thm, proj_constr: thm } + val typecopy: binding * (string * sort) list -> typ -> binding -> binding -> theory -> (string * info) * theory val get_info: theory -> string -> info option val interpretation: (string -> theory -> theory) -> theory -> theory @@ -23,14 +23,16 @@ type info = { vs: (string * sort) list, + typ: typ, constr: string, - typ: typ, - inject: thm, - proj: string * typ, - proj_def: thm + proj: string, + constr_inject: thm, + proj_inject: thm, + constr_proj: thm, + proj_constr: thm }; -structure TypecopyData = Theory_Data +structure Typecopy_Data = Theory_Data ( type T = info Symtab.table; val empty = Symtab.empty; @@ -38,7 +40,7 @@ fun merge data = Symtab.merge (K true) data; ); -val get_info = Symtab.lookup o TypecopyData.get; +val get_info = Symtab.lookup o Typecopy_Data.get; (* interpretation of type copies *) @@ -49,40 +51,42 @@ (* introducing typecopies *) -fun typecopy (raw_tyco, raw_vs) raw_ty constr_proj thy = +fun add_info tyco vs (({ rep_type, Abs_name, Rep_name, ...}, + { Abs_inject, Rep_inject, Abs_inverse, Rep_inverse, ... }) : Typedef.info) thy = + let + val exists_thm = + UNIV_I + |> Drule.instantiate' [SOME (ctyp_of thy (Logic.varifyT_global rep_type))] []; + val constr_inject = Abs_inject OF [exists_thm, exists_thm]; + val proj_constr = Abs_inverse OF [exists_thm]; + val info = { + vs = vs, + typ = rep_type, + constr = Abs_name, + proj = Rep_name, + constr_inject = constr_inject, + proj_inject = Rep_inject, + constr_proj = Rep_inverse, + proj_constr = proj_constr + }; + in + thy + |> (Typecopy_Data.map o Symtab.update_new) (tyco, info) + |> Typecopy_Interpretation.data tyco + |> pair (tyco, info) + end + +fun typecopy (raw_tyco, raw_vs) raw_ty constr proj thy = let val ty = Sign.certify_typ thy raw_ty; val ctxt = ProofContext.init_global thy |> Variable.declare_typ ty; val vs = map (ProofContext.check_tfree ctxt) raw_vs; val tac = Tactic.rtac UNIV_witness 1; - fun add_info tyco (({ abs_type = ty_abs, rep_type = ty_rep, Abs_name = c_abs, - Rep_name = c_rep, ...}, { Abs_inject = inject, Abs_inverse = inverse, ... }) - : Typedef.info) thy = - let - val exists_thm = - UNIV_I - |> Drule.instantiate' [SOME (ctyp_of thy (Logic.varifyT_global ty_rep))] []; - val inject' = inject OF [exists_thm, exists_thm]; - val proj_def = inverse OF [exists_thm]; - val info = { - vs = vs, - constr = c_abs, - typ = ty_rep, - inject = inject', - proj = (c_rep, ty_abs --> ty_rep), - proj_def = proj_def - }; - in - thy - |> (TypecopyData.map o Symtab.update_new) (tyco, info) - |> Typecopy_Interpretation.data tyco - |> pair (tyco, info) - end in thy |> Typedef.add_typedef_global false (SOME raw_tyco) (raw_tyco, vs, NoSyn) - (HOLogic.mk_UNIV ty) (Option.map swap constr_proj) tac - |-> (fn (tyco, info) => add_info tyco info) + (HOLogic.mk_UNIV ty) (SOME (proj, constr)) tac + |-> (fn (tyco, info) => add_info tyco vs info) end; @@ -90,10 +94,8 @@ fun add_default_code tyco thy = let - val SOME { constr = c, proj = (proj, _), proj_def = proj_eq, vs = vs, - typ = ty_rep, ... } = get_info thy tyco; - (* FIXME handle multiple typedef interpretations (!??) *) - val [(_, { Rep_inject = proj_inject, ... })] = Typedef.get_info_global thy tyco; + val SOME { vs, typ = ty_rep, constr = c, proj, proj_constr, proj_inject, ... } = + get_info thy tyco; val constr = (c, Logic.unvarifyT_global (Sign.the_const_type thy c)); val ty = Type (tyco, map TFree vs); val proj = Const (proj, ty --> ty_rep); @@ -113,7 +115,7 @@ in thy |> Code.add_datatype [constr] - |> Code.add_eqn proj_eq + |> Code.add_eqn proj_constr |> Theory_Target.instantiation ([tyco], vs, [HOLogic.class_eq]) |> `(fn lthy => Syntax.check_term lthy eq) |-> (fn eq => Specification.definition diff -r 13328f8853c7 -r de4a8298c6f3 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Fri Jun 18 22:41:16 2010 +0200 +++ b/src/Pure/Isar/locale.ML Sun Jun 20 22:01:22 2010 +0200 @@ -73,6 +73,7 @@ val add_dependency: string -> string * morphism -> morphism -> theory -> theory (* Diagnostic *) + val all_locales: theory -> string list val print_locales: theory -> unit val print_locale: theory -> bool -> xstring -> unit val print_registrations: theory -> string -> unit @@ -149,10 +150,6 @@ fun change_locale name = Locales.map o apsnd o Symtab.map_entry name o map_locale o apsnd; -fun print_locales thy = - Pretty.strs ("locales:" :: map #1 (Name_Space.extern_table (Locales.get thy))) - |> Pretty.writeln; - (*** Primitive operations ***) @@ -343,20 +340,6 @@ activate_all name thy Element.init (Element.transfer_morphism o Context.theory_of) ([], Context.Proof (ProofContext.init_global thy)) |-> put_idents |> Context.proof_of; -fun print_locale thy show_facts raw_name = - let - val name = intern thy raw_name; - val ctxt = init name thy; - fun cons_elem (elem as Notes _) = show_facts ? cons elem - | cons_elem elem = cons elem; - val elems = - activate_all name thy cons_elem (K (Element.transfer_morphism thy)) ([], []) - |> snd |> rev; - in - Pretty.big_list "locale elements:" (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems) - |> Pretty.writeln - end; - (*** Registrations: interpretations in theories ***) @@ -458,15 +441,6 @@ in roundup thy activate export dep (get_idents context, context) |-> put_idents end; -(* Diagnostic *) - -fun print_registrations thy raw_name = - (case these_registrations thy (intern thy raw_name) of - [] => Pretty.str ("no interpretations") - | regs => Pretty.big_list "interpretations:" (map (pretty_reg thy) (rev regs))) - |> Pretty.writeln; - - (* Add and extend registrations *) fun amend_registration (name, morph) mixin export thy = @@ -595,4 +569,33 @@ Method.setup (Binding.name "unfold_locales") (Scan.succeed (METHOD o try_intro_locales_tac true)) "back-chain all introduction rules of locales")); + +(*** diagnostic commands and interfaces ***) + +fun all_locales thy = map #1 (Name_Space.extern_table (Locales.get thy)); + +fun print_locales thy = + Pretty.strs ("locales:" :: all_locales thy) + |> Pretty.writeln; + +fun print_locale thy show_facts raw_name = + let + val name = intern thy raw_name; + val ctxt = init name thy; + fun cons_elem (elem as Notes _) = show_facts ? cons elem + | cons_elem elem = cons elem; + val elems = + activate_all name thy cons_elem (K (Element.transfer_morphism thy)) ([], []) + |> snd |> rev; + in + Pretty.big_list "locale elements:" (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems) + |> Pretty.writeln + end; + +fun print_registrations thy raw_name = + (case these_registrations thy (intern thy raw_name) of + [] => Pretty.str ("no interpretations") + | regs => Pretty.big_list "interpretations:" (map (pretty_reg thy) (rev regs))) + |> Pretty.writeln; + end;