--- 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 \<Rightarrow> 'a set" where
+lemma member_Fset [simp]:
"member (Fset A) = A"
-
-lemma member_inject [simp]:
- "member A = member B \<Longrightarrow> 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 \<longleftrightarrow> A = B"
+ by (simp add: Fset_inject)
+
+declare mem_def [simp]
definition Set :: "'a list \<Rightarrow> '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\<Colon>typerep list \<times> (unit \<Rightarrow> Code_Evaluation.term)
+ \<Rightarrow> 'a fset \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
+ [code_unfold]: "setify xs = Code_Evaluation.valtermify Set {\<cdot>} xs"
+
+notation fcomp (infixl "o>" 60)
+notation scomp (infixl "o\<rightarrow>" 60)
+
+instantiation fset :: (random) random
+begin
+
+definition
+ "Quickcheck.random i = Quickcheck.random i o\<rightarrow> (\<lambda>xs. Pair (setify xs))"
+
+instance ..
+
+end
+
+no_notation fcomp (infixl "o>" 60)
+no_notation scomp (infixl "o\<rightarrow>" 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 \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
[simp]: "insert x A = Fset (Set.insert x (member A))"
@@ -198,9 +223,16 @@
"A < B \<longleftrightarrow> A \<le> B \<and> \<not> B \<le> (A :: 'a fset)"
by (fact less_le_not_le)
-lemma eq_fset_subfset_eq [code]:
- "eq_class.eq A B \<longleftrightarrow> A \<le> B \<and> B \<le> (A :: 'a fset)"
- by (cases A, cases B) (simp add: eq set_eq)
+instantiation fset :: (type) eq
+begin
+
+definition
+ "eq_fset A B \<longleftrightarrow> A \<le> B \<and> B \<le> (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
--- 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 =
--- 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
--- 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;