merged

--- a/src/HOL/Library/AssocList.thy	Sun Apr 11 15:42:05 2010 +0200
+++ b/src/HOL/Library/AssocList.thy	Sun Apr 11 16:51:36 2010 +0200
@@ -659,49 +659,49 @@
 
 subsection {* Implementation of mappings *}
 
-definition AList :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) mapping" where
-  "AList xs = Mapping (map_of xs)"
+definition Mapping :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) mapping" where
+  "Mapping xs = Mapping.Mapping (map_of xs)"
 
-code_datatype AList
+code_datatype Mapping
 
-lemma lookup_AList [simp, code]:
-  "Mapping.lookup (AList xs) = map_of xs"
-  by (simp add: AList_def)
+lemma lookup_Mapping [simp, code]:
+  "Mapping.lookup (Mapping xs) = map_of xs"
+  by (simp add: Mapping_def)
 
-lemma empty_AList [code]:
-  "Mapping.empty = AList []"
+lemma empty_Mapping [code]:
+  "Mapping.empty = Mapping []"
   by (rule mapping_eqI) simp
 
-lemma is_empty_AList [code]:
-  "Mapping.is_empty (AList xs) \<longleftrightarrow> null xs"
+lemma is_empty_Mapping [code]:
+  "Mapping.is_empty (Mapping xs) \<longleftrightarrow> null xs"
   by (cases xs) (simp_all add: is_empty_def)
 
-lemma update_AList [code]:
-  "Mapping.update k v (AList xs) = AList (update k v xs)"
+lemma update_Mapping [code]:
+  "Mapping.update k v (Mapping xs) = Mapping (update k v xs)"
   by (rule mapping_eqI) (simp add: update_conv')
 
-lemma delete_AList [code]:
-  "Mapping.delete k (AList xs) = AList (delete k xs)"
+lemma delete_Mapping [code]:
+  "Mapping.delete k (Mapping xs) = Mapping (delete k xs)"
   by (rule mapping_eqI) (simp add: delete_conv')
 
-lemma keys_AList [code]:
-  "Mapping.keys (AList xs) = set (map fst xs)"
+lemma keys_Mapping [code]:
+  "Mapping.keys (Mapping xs) = set (map fst xs)"
   by (simp add: keys_def dom_map_of_conv_image_fst)
 
-lemma ordered_keys_AList [code]:
-  "Mapping.ordered_keys (AList xs) = sort (remdups (map fst xs))"
-  by (simp only: ordered_keys_def keys_AList sorted_list_of_set_sort_remdups)
+lemma ordered_keys_Mapping [code]:
+  "Mapping.ordered_keys (Mapping xs) = sort (remdups (map fst xs))"
+  by (simp only: ordered_keys_def keys_Mapping sorted_list_of_set_sort_remdups)
 
-lemma size_AList [code]:
-  "Mapping.size (AList xs) = length (remdups (map fst xs))"
+lemma size_Mapping [code]:
+  "Mapping.size (Mapping xs) = length (remdups (map fst xs))"
   by (simp add: size_def length_remdups_card_conv dom_map_of_conv_image_fst)
 
-lemma tabulate_AList [code]:
-  "Mapping.tabulate ks f = AList (map (\<lambda>k. (k, f k)) ks)"
+lemma tabulate_Mapping [code]:
+  "Mapping.tabulate ks f = Mapping (map (\<lambda>k. (k, f k)) ks)"
   by (rule mapping_eqI) (simp add: map_of_map_restrict)
 
-lemma bulkload_AList [code]:
-  "Mapping.bulkload vs = AList (map (\<lambda>n. (n, vs ! n)) [0..<length vs])"
+lemma bulkload_Mapping [code]:
+  "Mapping.bulkload vs = Mapping (map (\<lambda>n. (n, vs ! n)) [0..<length vs])"
   by (rule mapping_eqI) (simp add: map_of_map_restrict expand_fun_eq)
 
 end

--- a/src/HOL/Library/Dlist.thy	Sun Apr 11 15:42:05 2010 +0200
+++ b/src/HOL/Library/Dlist.thy	Sun Apr 11 16:51:36 2010 +0200
@@ -47,6 +47,7 @@
   show "[] \<in> ?dlist" by simp
 qed
 
+
 text {* Formal, totalized constructor for @{typ "'a dlist"}: *}
 
 definition Dlist :: "'a list \<Rightarrow> 'a dlist" where
@@ -60,7 +61,7 @@
   "list_of_dlist (Dlist xs) = remdups xs"
   by (simp add: Dlist_def Abs_dlist_inverse)
 
-lemma Dlist_list_of_dlist [simp]:
+lemma Dlist_list_of_dlist [simp, code abstype]:
   "Dlist (list_of_dlist dxs) = dxs"
   by (simp add: Dlist_def list_of_dlist_inverse distinct_remdups_id)
 
@@ -100,9 +101,6 @@
 
 section {* Executable version obeying invariant *}
 
-code_abstype Dlist list_of_dlist
-  by simp
-
 lemma list_of_dlist_empty [simp, code abstract]:
   "list_of_dlist empty = []"
   by (simp add: empty_def)

--- a/src/HOL/Library/Mapping.thy	Sun Apr 11 15:42:05 2010 +0200
+++ b/src/HOL/Library/Mapping.thy	Sun Apr 11 16:51:36 2010 +0200
@@ -122,6 +122,10 @@
   "bulkload xs = tabulate [0..<length xs] (nth xs)"
   by (rule mapping_eqI) (simp add: expand_fun_eq)
 
+lemma is_empty_empty:
+  "is_empty m \<longleftrightarrow> m = Mapping Map.empty"
+  by (cases m) (simp add: is_empty_def)
+
 
 subsection {* Some technical code lemmas *}
 

--- a/src/HOL/Library/Table.thy	Sun Apr 11 15:42:05 2010 +0200
+++ b/src/HOL/Library/Table.thy	Sun Apr 11 16:51:36 2010 +0200
@@ -3,7 +3,7 @@
 header {* Tables: finite mappings implemented by red-black trees *}
 
 theory Table
-imports Main RBT
+imports Main RBT Mapping
 begin
 
 subsection {* Type definition *}
@@ -23,7 +23,8 @@
   "t1 = t2 \<longleftrightarrow> tree_of t1 = tree_of t2"
   by (simp add: tree_of_inject)
 
-code_abstype Table tree_of
+lemma [code abstype]:
+  "Table (tree_of t) = t"
   by (simp add: tree_of_inverse)
 
 
@@ -56,6 +57,9 @@
 definition entries :: "('a\<Colon>linorder, 'b) table \<Rightarrow> ('a \<times> 'b) list" where
   [code]: "entries t = RBT.entries (tree_of t)"
 
+definition keys :: "('a\<Colon>linorder, 'b) table \<Rightarrow> 'a list" where
+  [code]: "keys t = RBT.keys (tree_of t)"
+
 definition bulkload :: "('a\<Colon>linorder \<times> 'b) list \<Rightarrow> ('a, 'b) table" where
   "bulkload xs = Table (RBT.bulkload xs)"
 
@@ -101,6 +105,10 @@
   "RBT.entries (tree_of t) = entries t"
   by (simp add: entries_def)
 
+lemma keys_tree_of:
+  "RBT.keys (tree_of t) = keys t"
+  by (simp add: keys_def)
+
 lemma lookup_empty [simp]:
   "lookup empty = Map.empty"
   by (simp add: empty_def lookup_Table expand_fun_eq)
@@ -111,15 +119,19 @@
 
 lemma lookup_delete [simp]:
   "lookup (delete k t) = (lookup t)(k := None)"
-  by (simp add: delete_def lookup_Table lookup_delete lookup_tree_of restrict_complement_singleton_eq)
+  by (simp add: delete_def lookup_Table RBT.lookup_delete lookup_tree_of restrict_complement_singleton_eq)
 
 lemma map_of_entries [simp]:
   "map_of (entries t) = lookup t"
   by (simp add: entries_def map_of_entries lookup_tree_of)
 
+lemma entries_lookup:
+  "entries t1 = entries t2 \<longleftrightarrow> lookup t1 = lookup t2"
+  by (simp add: entries_def lookup_def entries_lookup)
+
 lemma lookup_bulkload [simp]:
   "lookup (bulkload xs) = map_of xs"
-  by (simp add: bulkload_def lookup_Table lookup_bulkload)
+  by (simp add: bulkload_def lookup_Table RBT.lookup_bulkload)
 
 lemma lookup_map_entry [simp]:
   "lookup (map_entry k f t) = (lookup t)(k := Option.map f (lookup t k))"
@@ -133,7 +145,85 @@
   "fold f t = (\<lambda>s. foldl (\<lambda>s (k, v). f k v s) s (entries t))"
   by (simp add: fold_def expand_fun_eq RBT.fold_def entries_tree_of)
 
+lemma is_empty_empty [simp]:
+  "is_empty t \<longleftrightarrow> t = empty"
+  by (simp add: table_eq is_empty_def tree_of_empty split: rbt.split)
+
+lemma RBT_lookup_empty [simp]: (*FIXME*)
+  "RBT.lookup t = Map.empty \<longleftrightarrow> t = RBT.Empty"
+  by (cases t) (auto simp add: expand_fun_eq)
+
+lemma lookup_empty_empty [simp]:
+  "lookup t = Map.empty \<longleftrightarrow> t = empty"
+  by (cases t) (simp add: empty_def lookup_def Table_inject Table_inverse)
+
+lemma sorted_keys [iff]:
+  "sorted (keys t)"
+  by (simp add: keys_def RBT.keys_def sorted_entries)
+
+lemma distinct_keys [iff]:
+  "distinct (keys t)"
+  by (simp add: keys_def RBT.keys_def distinct_entries)
+
+
+subsection {* Implementation of mappings *}
+
+definition Mapping :: "('a\<Colon>linorder, 'b) table \<Rightarrow> ('a, 'b) mapping" where
+  "Mapping t = Mapping.Mapping (lookup t)"
+
+code_datatype Mapping
+
+lemma lookup_Mapping [simp, code]:
+  "Mapping.lookup (Mapping t) = lookup t"
+  by (simp add: Mapping_def)
+
+lemma empty_Mapping [code]:
+  "Mapping.empty = Mapping empty"
+  by (rule mapping_eqI) simp
+
+lemma is_empty_Mapping [code]:
+  "Mapping.is_empty (Mapping t) \<longleftrightarrow> is_empty t"
+  by (simp add: table_eq Mapping.is_empty_empty Mapping_def)
+
+lemma update_Mapping [code]:
+  "Mapping.update k v (Mapping t) = Mapping (update k v t)"
+  by (rule mapping_eqI) simp
+
+lemma delete_Mapping [code]:
+  "Mapping.delete k (Mapping xs) = Mapping (delete k xs)"
+  by (rule mapping_eqI) simp
+
+lemma keys_Mapping [code]:
+  "Mapping.keys (Mapping t) = set (keys t)"
+  by (simp add: keys_def Mapping_def Mapping.keys_def lookup_def lookup_keys)
+
+lemma ordered_keys_Mapping [code]:
+  "Mapping.ordered_keys (Mapping t) = keys t"
+  by (rule sorted_distinct_set_unique) (simp_all add: ordered_keys_def keys_Mapping)
+
+lemma Mapping_size_card_keys: (*FIXME*)
+  "Mapping.size m = card (Mapping.keys m)"
+  by (simp add: Mapping.size_def Mapping.keys_def)
+
+lemma size_Mapping [code]:
+  "Mapping.size (Mapping t) = length (keys t)"
+  by (simp add: Mapping_size_card_keys keys_Mapping distinct_card)
+
+lemma tabulate_Mapping [code]:
+  "Mapping.tabulate ks f = Mapping (bulkload (List.map (\<lambda>k. (k, f k)) ks))"
+  by (rule mapping_eqI) (simp add: map_of_map_restrict)
+
+lemma bulkload_Mapping [code]:
+  "Mapping.bulkload vs = Mapping (bulkload (List.map (\<lambda>n. (n, vs ! n)) [0..<length vs]))"
+  by (rule mapping_eqI) (simp add: map_of_map_restrict expand_fun_eq)
+
+lemma [code, code del]: "HOL.eq (x :: (_, _) mapping) y \<longleftrightarrow> x = y" by (fact eq_equals) (*FIXME*)
+
+lemma eq_Mapping [code]:
+  "HOL.eq (Mapping t1) (Mapping t2) \<longleftrightarrow> entries t1 = entries t2"
+  by (simp add: eq Mapping_def entries_lookup)
+
 hide (open) const tree_of lookup empty update delete
-  entries bulkload map_entry map fold
+  entries keys bulkload map_entry map fold
 
 end

--- a/src/HOL/Rat.thy	Sun Apr 11 15:42:05 2010 +0200
+++ b/src/HOL/Rat.thy	Sun Apr 11 16:51:36 2010 +0200
@@ -1019,11 +1019,9 @@
 definition Frct :: "int \<times> int \<Rightarrow> rat" where
   [simp]: "Frct p = Fract (fst p) (snd p)"
 
-code_abstype Frct quotient_of
-proof (rule eq_reflection)
-  fix r :: rat
-  show "Frct (quotient_of r) = r" by (cases r) (auto intro: quotient_of_eq)
-qed
+lemma [code abstype]:
+  "Frct (quotient_of q) = q"
+  by (cases q) (auto intro: quotient_of_eq)
 
 lemma Frct_code_post [code_post]:
   "Frct (0, k) = 0"

--- a/src/HOL/ex/Execute_Choice.thy	Sun Apr 11 15:42:05 2010 +0200
+++ b/src/HOL/ex/Execute_Choice.thy	Sun Apr 11 16:51:36 2010 +0200
@@ -58,15 +58,15 @@
 
 text {*
   Given @{text valuesum_rec} as initial description, we stepwise refine it to something executable;
-  first, we formally insert the constructor @{term AList} and split the one equation into two,
+  first, we formally insert the constructor @{term Mapping} and split the one equation into two,
   where the second one provides the necessary context:
 *}
 
-lemma valuesum_rec_AList:
-  shows [code]: "valuesum (AList []) = 0"
-  and "valuesum (AList (x # xs)) = (let l = (SOME l. l \<in> Mapping.keys (AList (x # xs))) in
-    the (Mapping.lookup (AList (x # xs)) l) + valuesum (Mapping.delete l (AList (x # xs))))"
-  by (simp_all add: valuesum_rec finite_dom_map_of is_empty_AList)
+lemma valuesum_rec_Mapping:
+  shows [code]: "valuesum (Mapping []) = 0"
+  and "valuesum (Mapping (x # xs)) = (let l = (SOME l. l \<in> Mapping.keys (Mapping (x # xs))) in
+    the (Mapping.lookup (Mapping (x # xs)) l) + valuesum (Mapping.delete l (Mapping (x # xs))))"
+  by (simp_all add: valuesum_rec finite_dom_map_of is_empty_Mapping)
 
 text {*
   As a side effect the precondition disappears (but note this has nothing to do with choice!).
@@ -76,27 +76,27 @@
 *}
 
 lemma valuesum_rec_exec [code]:
-  "valuesum (AList (x # xs)) = (let l = fst (hd (x # xs)) in
-    the (Mapping.lookup (AList (x # xs)) l) + valuesum (Mapping.delete l (AList (x # xs))))"
+  "valuesum (Mapping (x # xs)) = (let l = fst (hd (x # xs)) in
+    the (Mapping.lookup (Mapping (x # xs)) l) + valuesum (Mapping.delete l (Mapping (x # xs))))"
 proof -
-  let ?M = "AList (x # xs)"
+  let ?M = "Mapping (x # xs)"
   let ?l1 = "(SOME l. l \<in> Mapping.keys ?M)"
   let ?l2 = "fst (hd (x # xs))"
-  have "finite (Mapping.keys ?M)" by (simp add: keys_AList)
+  have "finite (Mapping.keys ?M)" by (simp add: keys_Mapping)
   moreover have "?l1 \<in> Mapping.keys ?M"
-    by (rule someI) (auto simp add: keys_AList)
+    by (rule someI) (auto simp add: keys_Mapping)
   moreover have "?l2 \<in> Mapping.keys ?M"
-    by (simp add: keys_AList)
+    by (simp add: keys_Mapping)
   ultimately have "the (Mapping.lookup ?M ?l1) + valuesum (Mapping.delete ?l1 ?M) =
     the (Mapping.lookup ?M ?l2) + valuesum (Mapping.delete ?l2 ?M)"
     by (rule valuesum_choice)
-  then show ?thesis by (simp add: valuesum_rec_AList)
+  then show ?thesis by (simp add: valuesum_rec_Mapping)
 qed
   
 text {*
   See how it works:
 *}
 
-value "valuesum (AList [(''abc'', (42::int)), (''def'', 1705)])"
+value "valuesum (Mapping [(''abc'', (42::int)), (''def'', 1705)])"
 
 end

--- a/src/Pure/Isar/code.ML	Sun Apr 11 15:42:05 2010 +0200
+++ b/src/Pure/Isar/code.ML	Sun Apr 11 16:51:36 2010 +0200
@@ -22,8 +22,6 @@
   (*constructor sets*)
   val constrset_of_consts: theory -> (string * typ) list
     -> string * ((string * sort) list * (string * typ list) list)
-  val abstype_cert: theory -> string * typ -> string
-    -> string * ((string * sort) list * ((string * typ) * (string * term)))
 
   (*code equations and certificates*)
   val mk_eqn: theory -> thm * bool -> thm * bool
@@ -52,8 +50,7 @@
   val datatype_interpretation:
     (string * ((string * sort) list * (string * typ list) list)
       -> theory -> theory) -> theory -> theory
-  val add_abstype: string * typ -> string * typ -> theory -> Proof.state
-  val add_abstype_cmd: string -> string -> theory -> Proof.state
+  val add_abstype: thm -> theory -> theory
   val abstype_interpretation:
     (string * ((string * sort) list * ((string * typ) * (string * thm)))
       -> theory -> theory) -> theory -> theory
@@ -380,6 +377,7 @@
         val tfrees = Term.add_tfreesT ty [];
         val (tyco, vs) = ((apsnd o map) (dest_TFree) o dest_Type o snd o strip_type) ty
           handle TYPE _ => no_constr thy "bad type" c_ty
+        val _ = if tyco = "fun" then no_constr thy "bad type" c_ty else ();
         val _ = if has_duplicates (eq_fst (op =)) vs
           then no_constr thy "duplicate type variables in datatype" c_ty else ();
         val _ = if length tfrees <> length vs
@@ -411,22 +409,6 @@
     val cs''' = map (inst vs) cs'';
   in (tyco, (vs, rev cs''')) end;
 
-fun abstype_cert thy abs_ty rep =
-  let
-    val _ = pairself (fn c => if (is_some o AxClass.class_of_param thy) c
-      then error ("Is a class parameter: " ^ string_of_const thy c) else ()) (fst abs_ty, rep);
-    val ((tyco, sorts), (abs, (vs, ty'))) = ty_sorts thy abs_ty;
-    val (ty, ty_abs) = case ty'
-     of Type ("fun", [ty, ty_abs]) => (ty, ty_abs)
-      | _ => error ("Not a datatype abstractor:\n" ^ string_of_const thy abs
-          ^ " :: " ^ string_of_typ thy ty');
-    val _ = Thm.cterm_of thy (Const (rep, ty_abs --> ty)) handle TYPE _ =>
-      error ("Not a projection:\n" ^ string_of_const thy rep);
-    val param = Free ("x", ty_abs);
-    val cert = Logic.all param (Logic.mk_equals
-      (Const (abs, ty --> ty_abs) $ (Const (rep, ty_abs --> ty) $ param), param));
-  in (tyco, (vs ~~ sorts, ((fst abs_ty, ty), (rep, cert)))) end;    
-
 fun get_type_entry thy tyco = case these (Symtab.lookup ((the_types o the_exec) thy) tyco)
  of (_, entry) :: _ => SOME entry
   | _ => NONE;
@@ -657,6 +639,29 @@
 fun canonize_thms thy = desymbolize_tvars thy #> same_arity thy #> map (desymbolize_vars thy);
 
 
+(* abstype certificates *)
+
+fun check_abstype_cert thy proto_thm =
+  let
+    val thm = meta_rewrite thy proto_thm;
+    fun bad s = bad_thm (s ^ ":\n" ^ Display.string_of_thm_global thy thm);
+    val (lhs, rhs) = Logic.dest_equals (Thm.plain_prop_of thm)
+      handle TERM _ => bad "Not an equation"
+           | THM _ => bad "Not a proper equation";
+    val ((abs, raw_ty), ((rep, _), param)) = (apsnd (apfst dest_Const o dest_comb)
+        o apfst dest_Const o dest_comb) lhs
+      handle TERM _ => bad "Not an abstype certificate";
+    val var = (fst o dest_Var) param
+      handle TERM _ => bad "Not an abstype certificate";
+    val _ = if param = rhs then () else bad "Not an abstype certificate";
+    val _ = pairself (fn c => if (is_some o AxClass.class_of_param thy) c
+      then error ("Is a class parameter: " ^ string_of_const thy c) else ()) (abs, rep);
+    val ((tyco, sorts), (abs, (vs, ty'))) = ty_sorts thy (abs, Logic.unvarifyT_global raw_ty);
+    val ty = domain_type ty';
+    val ty_abs = range_type ty';
+  in (tyco, (vs ~~ sorts, ((abs, ty), (rep, thm)))) end;
+
+
 (* code equation certificates *)
 
 fun build_head thy (c, ty) =
@@ -1152,25 +1157,19 @@
 fun abstype_interpretation f = Abstype_Interpretation.interpretation
   (fn (tyco, _) => fn thy => f (tyco, get_abstype_spec thy tyco) thy);
 
-fun add_abstype proto_abs proto_rep thy =
+fun add_abstype proto_thm thy =
   let
-    val (abs, rep) = pairself (unoverload_const_typ thy) (proto_abs, proto_rep);
-    val (tyco, (vs, (abs_ty as (abs, ty), (rep, cert_prop)))) = abstype_cert thy abs (fst rep);
-    fun after_qed [[cert]] = ProofContext.theory
-      (del_eqns abs
-      #> register_type (tyco, (vs, Abstractor (abs_ty, (rep, cert))))
-      #> change_fun_spec false rep ((K o Proj)
-        (map_types Logic.varifyT_global (mk_proj tyco vs ty abs rep), tyco))
-      #> Abstype_Interpretation.data (tyco, serial ()));
+    val (tyco, (vs, (abs_ty as (abs, ty), (rep, cert)))) =
+      check_abstype_cert thy proto_thm;
   in
     thy
-    |> ProofContext.init
-    |> Proof.theorem_i NONE after_qed [[(cert_prop, [])]]
+    |> del_eqns abs
+    |> register_type (tyco, (vs, Abstractor (abs_ty, (rep, cert))))
+    |> change_fun_spec false rep ((K o Proj)
+        (map_types Logic.varifyT_global (mk_proj tyco vs ty abs rep), tyco))
+    |> Abstype_Interpretation.data (tyco, serial ())
   end;
 
-fun add_abstype_cmd raw_abs raw_rep thy =
-  add_abstype (read_bare_const thy raw_abs) (read_bare_const thy raw_rep) thy;
-
 
 (** infrastructure **)
 
@@ -1200,6 +1199,7 @@
     val code_attribute_parser =
       Args.del |-- Scan.succeed (mk_attribute del_eqn)
       || Args.$$$ "nbe" |-- Scan.succeed (mk_attribute add_nbe_eqn)
+      || Args.$$$ "abstype" |-- Scan.succeed (mk_attribute add_abstype)
       || Args.$$$ "abstract" |-- Scan.succeed (mk_attribute add_abs_eqn)
       || (Args.$$$ "target" |-- Args.colon |-- Args.name >>
            (mk_attribute o code_target_attr))

--- a/src/Pure/Isar/isar_syn.ML	Sun Apr 11 15:42:05 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Sun Apr 11 16:51:36 2010 +0200
@@ -480,11 +480,6 @@
   OuterSyntax.command "code_datatype" "define set of code datatype constructors" K.thy_decl
     (Scan.repeat1 P.term >> (Toplevel.theory o Code.add_datatype_cmd));
 
-val _ =
-  OuterSyntax.command "code_abstype" "define abstract code type" K.thy_goal
-    (P.term -- P.term >> (fn (abs, rep) => Toplevel.print
-      o Toplevel.theory_to_proof (Code.add_abstype_cmd abs rep)));
-
 
 
 (** proof commands **)