# HG changeset patch
# User haftmann
# Date 1422430148 -3600
# Node ID 9de8ac92cafa3e02cf6d9b5046fdb0b7f3e858b1
# Parent  c4f044389c283402ef7486ef641385cdbe3162b6
abstract code equation may also be default

diff -r c4f044389c28 -r 9de8ac92cafa src/HOL/Tools/Lifting/lifting_def.ML
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Wed Jan 28 08:29:08 2015 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Wed Jan 28 08:29:08 2015 +0100
@@ -369,7 +369,7 @@
         else
           if is_some opt_rep_eq_thm andalso is_valid_abs_eq (the opt_rep_eq_thm)
           then
-            Code.add_abs_eqn (the opt_rep_eq_thm) thy
+            Code.add_abs_default_eqn (the opt_rep_eq_thm) thy
           else
             thy
       end
diff -r c4f044389c28 -r 9de8ac92cafa src/HOL/Tools/Lifting/lifting_setup.ML
--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Wed Jan 28 08:29:08 2015 +0100
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Wed Jan 28 08:29:08 2015 +0100
@@ -157,7 +157,7 @@
     let
       val abs_type_thm = quot_thm RS @{thm Quotient_abs_rep}
       val add_abstype_attribute = 
-          Thm.declaration_attribute (fn thm => Context.mapping (Code.add_abstype thm) I)
+          Thm.declaration_attribute (fn thm => Context.mapping (Code.add_abstype_default thm) I)
         val add_abstype_attrib = Attrib.internal (K add_abstype_attribute)
     in
       lthy
diff -r c4f044389c28 -r 9de8ac92cafa src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Wed Jan 28 08:29:08 2015 +0100
+++ b/src/Pure/Isar/code.ML	Wed Jan 28 08:29:08 2015 +0100
@@ -42,6 +42,7 @@
     (string * ((string * sort) list * (string * ((string * sort) list * typ list)) list)
       -> theory -> theory) -> theory -> theory
   val add_abstype: thm -> theory -> theory
+  val add_abstype_default: thm -> theory -> theory
   val abstype_interpretation:
     (string * ((string * sort) list * ((string * ((string * sort) list * typ)) * (string * thm)))
       -> theory -> theory) -> theory -> theory
@@ -56,6 +57,9 @@
   val add_nbe_default_eqn: thm -> theory -> theory
   val add_nbe_default_eqn_attribute: attribute
   val add_nbe_default_eqn_attrib: Token.src
+  val add_abs_default_eqn: thm -> theory -> theory
+  val add_abs_default_eqn_attribute: attribute
+  val add_abs_default_eqn_attrib: Token.src
   val del_eqn: thm -> theory -> theory
   val del_eqns: string -> theory -> theory
   val del_exception: string -> theory -> theory
@@ -175,20 +179,22 @@
 
 (* functions *)
 
-datatype fun_spec = Default of (thm * bool) list * (thm * bool) list lazy
+datatype fun_spec = Eqns_Default of (thm * bool) list * (thm * bool) list lazy
       (* (cache for default equations, lazy computation of default equations)
          -- helps to restore natural order of default equations *)
   | Eqns of (thm * bool) list
   | None
-  | Proj of term * string
-  | Abstr of thm * string;
+  | Proj of (term * string) * bool
+  | Abstr of (thm * string) * bool;
 
-val initial_fun_spec = Default ([], Lazy.value []);
+val initial_fun_spec = Eqns_Default ([], Lazy.value []);
 
-fun is_default (Default _) = true
+fun is_default (Eqns_Default _) = true
+  | is_default (Proj (_, default)) = default
+  | is_default (Abstr (_, default)) = default
   | is_default _ = false;
 
-fun associated_abstype (Abstr (_, tyco)) = SOME tyco
+fun associated_abstype (Abstr ((_, tyco), _)) = SOME tyco
   | associated_abstype _ = NONE;
 
 
@@ -935,13 +941,13 @@
     val thy = Proof_Context.theory_of ctxt;
   in
     case retrieve_raw thy c of
-      Default (_, eqns_lazy) => Lazy.force eqns_lazy
+      Eqns_Default (_, eqns_lazy) => Lazy.force eqns_lazy
         |> cert_of_eqns_preprocess ctxt functrans c
     | Eqns eqns => eqns
         |> cert_of_eqns_preprocess ctxt functrans c
     | None => nothing_cert ctxt c
-    | Proj (_, tyco) => cert_of_proj thy c tyco
-    | Abstr (abs_thm, tyco) => abs_thm
+    | Proj ((_, tyco), _) => cert_of_proj thy c tyco
+    | Abstr ((abs_thm, tyco), _) => abs_thm
        |> preprocess Conv.arg_conv ctxt
        |> cert_of_abs thy tyco c
   end;
@@ -1004,13 +1010,13 @@
     fun pretty_equations const thms =
       (Pretty.block o Pretty.fbreaks)
         (Pretty.str (string_of_const thy const) :: map (Display.pretty_thm_item ctxt) thms);
-    fun pretty_function (const, Default (_, eqns_lazy)) =
+    fun pretty_function (const, Eqns_Default (_, eqns_lazy)) =
           pretty_equations const (map fst (Lazy.force eqns_lazy))
       | pretty_function (const, Eqns eqns) = pretty_equations const (map fst eqns)
       | pretty_function (const, None) = pretty_equations const []
-      | pretty_function (const, Proj (proj, _)) = Pretty.block
+      | pretty_function (const, Proj ((proj, _), _)) = Pretty.block
           [Pretty.str (string_of_const thy const), Pretty.fbrk, Syntax.pretty_term ctxt proj]
-      | pretty_function (const, Abstr (thm, _)) = pretty_equations const [thm];
+      | pretty_function (const, Abstr ((thm, _), _)) = pretty_equations const [thm];
     fun pretty_typ (tyco, vs) = Pretty.str
       (string_of_typ thy (Type (tyco, map TFree vs)));
     fun pretty_typspec (typ, (cos, abstract)) = if null cos
@@ -1094,19 +1100,19 @@
       in (thm, proper) :: filter_out drop eqns end;
     fun natural_order eqns =
       (eqns, Lazy.lazy (fn () => fold (update_subsume false) eqns []))
-    fun add_eqn' true (Default (eqns, _)) = Default (natural_order ((thm, proper) :: eqns))
+    fun add_eqn' true (Eqns_Default (eqns, _)) = Eqns_Default (natural_order ((thm, proper) :: eqns))
           (*this restores the natural order and drops syntactic redundancies*)
-      | add_eqn' true None = Default (natural_order [(thm, proper)])
+      | add_eqn' true None = Eqns_Default (natural_order [(thm, proper)])
       | add_eqn' true fun_spec = fun_spec
       | add_eqn' false (Eqns eqns) = Eqns (update_subsume true (thm, proper) eqns)
       | add_eqn' false _ = Eqns [(thm, proper)];
   in change_fun_spec c (add_eqn' default) thy end;
 
-fun gen_add_abs_eqn raw_thm thy =
+fun gen_add_abs_eqn default raw_thm thy =
   let
     val (abs_thm, tyco) = apfst Thm.close_derivation raw_thm;
     val c = const_abs_eqn thy abs_thm;
-  in change_fun_spec c (K (Abstr (abs_thm, tyco))) thy end;
+  in change_fun_spec c (K (Abstr ((abs_thm, tyco), default))) thy end;
 
 fun add_eqn thm thy =
   gen_add_eqn false (mk_eqn thy (thm, true)) thy;
@@ -1130,22 +1136,27 @@
   (fn thm => Context.mapping (add_nbe_default_eqn thm) I);
 val add_nbe_default_eqn_attrib = Attrib.internal (K add_nbe_default_eqn_attribute);
 
-fun add_abs_eqn raw_thm thy = gen_add_abs_eqn (mk_abs_eqn thy raw_thm) thy;
+fun add_abs_eqn raw_thm thy = gen_add_abs_eqn false (mk_abs_eqn thy raw_thm) thy;
+fun add_abs_default_eqn raw_thm thy = gen_add_abs_eqn true (mk_abs_eqn thy raw_thm) thy;
 
 val add_abs_eqn_attribute = Thm.declaration_attribute
   (fn thm => Context.mapping (add_abs_eqn thm) I);
+val add_abs_default_eqn_attribute = Thm.declaration_attribute
+  (fn thm => Context.mapping (add_abs_default_eqn thm) I);
+
 val add_abs_eqn_attrib = Attrib.internal (K add_abs_eqn_attribute);
+val add_abs_default_eqn_attrib = Attrib.internal (K add_abs_default_eqn_attribute);
 
 fun add_eqn_maybe_abs thm thy =
   case mk_eqn_maybe_abs thy thm
    of SOME (eqn, NONE) => gen_add_eqn false eqn thy
-    | SOME ((thm, _), SOME tyco) => gen_add_abs_eqn (thm, tyco) thy
+    | SOME ((thm, _), SOME tyco) => gen_add_abs_eqn false (thm, tyco) thy
     | NONE => thy;
 
 fun del_eqn thm thy = case mk_eqn_liberal thy thm
  of SOME (thm, _) =>
       let
-        fun del_eqn' (Default _) = initial_fun_spec
+        fun del_eqn' (Eqns_Default _) = initial_fun_spec
           | del_eqn' (Eqns eqns) =
               let
                 val eqns' = filter_out (fn (thm', _) => Thm.eq_thm_prop (thm, thm')) eqns
@@ -1272,7 +1283,7 @@
     (fn tyco =>
       Local_Theory.background_theory (fn thy => f (tyco, get_abstype_spec thy tyco) thy));
 
-fun add_abstype proto_thm thy =
+fun gen_add_abstype default proto_thm thy =
   let
     val (tyco, (vs, (abs_ty as (abs, (_, ty)), (rep, cert)))) =
       error_abs_thm (check_abstype_cert thy) thy proto_thm;
@@ -1280,10 +1291,13 @@
     thy
     |> register_type (tyco, (vs, Abstractor (abs_ty, (rep, cert))))
     |> change_fun_spec rep
-      (K (Proj (Logic.varify_types_global (mk_proj tyco vs ty abs rep), tyco)))
+      (K (Proj ((Logic.varify_types_global (mk_proj tyco vs ty abs rep), tyco), default)))
     |> Named_Target.theory_map (Abstype_Plugin.data_default tyco)
   end;
 
+val add_abstype = gen_add_abstype false;
+val add_abstype_default = gen_add_abstype true;
+
 
 (* setup *)