# HG changeset patch
# User haftmann
# Date 1270997467 -7200
# Node ID 7fa17a225852db0672ddf20474dc12bc38588fae
# Parent  5844017e31f883e9b5c08ba047d8e55c5af00516
user interface for abstract datatypes is an attribute, not a command

diff -r 5844017e31f8 -r 7fa17a225852 src/HOL/Library/Dlist.thy
--- a/src/HOL/Library/Dlist.thy	Sun Apr 11 16:51:06 2010 +0200
+++ b/src/HOL/Library/Dlist.thy	Sun Apr 11 16:51:07 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)
diff -r 5844017e31f8 -r 7fa17a225852 src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Sun Apr 11 16:51:06 2010 +0200
+++ b/src/HOL/Rat.thy	Sun Apr 11 16:51:07 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"
diff -r 5844017e31f8 -r 7fa17a225852 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Sun Apr 11 16:51:06 2010 +0200
+++ b/src/Pure/Isar/code.ML	Sun Apr 11 16:51:07 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))
diff -r 5844017e31f8 -r 7fa17a225852 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sun Apr 11 16:51:06 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Sun Apr 11 16:51:07 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 **)