merged
authorhaftmann
Sun, 20 Jun 2010 22:01:22 +0200
changeset 37472 de4a8298c6f3
parent 37467 13328f8853c7 (current diff)
parent 37471 907e13072675 (diff)
child 37473 013f78aed840
merged
--- 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;