store explicitly quotient types with no_code => more precise registration of code equations

--- a/src/HOL/Tools/Lifting/lifting_def.ML	Thu Jul 24 19:01:06 2014 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Thu Jul 24 20:21:34 2014 +0200
@@ -401,6 +401,22 @@
   val register_code_eq_attribute = Thm.declaration_attribute
     (fn thm => Context.mapping (register_encoded_code_eq thm) I)
   val register_code_eq_attrib = Attrib.internal (K register_code_eq_attribute)
+
+  fun no_no_code ctxt (rty, qty) =
+    if same_type_constrs (rty, qty) then
+      forall (no_no_code ctxt) (Targs rty ~~ Targs qty)
+    else
+      if is_Type qty then
+        if Lifting_Info.is_no_code_type ctxt (Tname qty) then false
+        else 
+          let 
+            val (rty', rtyq) = Lifting_Term.instantiate_rtys ctxt (rty, qty)
+            val (rty's, rtyqs) = (Targs rty', Targs rtyq)
+          in
+            forall (no_no_code ctxt) (rty's ~~ rtyqs)
+          end
+      else
+        true
 in
 
 fun register_code_eq abs_eq_thm opt_rep_eq_thm (rty, qty) lthy =
@@ -408,8 +424,10 @@
     val thy = Proof_Context.theory_of lthy
     val encoded_code_eq = encode_code_eq thy abs_eq_thm opt_rep_eq_thm (rty, qty)
   in
-    (snd oo Local_Theory.note) ((Binding.empty, [register_code_eq_attrib]), 
-      [encoded_code_eq]) lthy
+    if no_no_code lthy (rty, qty) then 
+      (snd oo Local_Theory.note) ((Binding.empty, [register_code_eq_attrib]), [encoded_code_eq]) lthy
+    else
+      lthy
   end
 end
             

--- a/src/HOL/Tools/Lifting/lifting_info.ML	Thu Jul 24 19:01:06 2014 +0200
+++ b/src/HOL/Tools/Lifting/lifting_info.ML	Thu Jul 24 20:21:34 2014 +0200
@@ -34,10 +34,14 @@
     pos_distr_rules: thm list, neg_distr_rules: thm list}
   val lookup_relator_distr_data: Proof.context -> string -> relator_distr_data option
 
+  val add_no_code_type: string -> Context.generic -> Context.generic
+  val is_no_code_type: Proof.context -> string -> bool
+
   val get_quot_maps           : Proof.context -> quot_map Symtab.table
   val get_quotients           : Proof.context -> quotient Symtab.table
   val get_relator_distr_data  : Proof.context -> relator_distr_data Symtab.table
   val get_restore_data        : Proof.context -> restore_data Symtab.table
+  val get_no_code_types       : Proof.context -> unit Symtab.table
 
   val setup: theory -> theory
 end
@@ -82,52 +86,61 @@
       quotients : quotient Symtab.table,
       reflexivity_rules : thm Item_Net.T,
       relator_distr_data : relator_distr_data Symtab.table,
-      restore_data : restore_data Symtab.table
+      restore_data : restore_data Symtab.table,
+      no_code_types : unit Symtab.table
     }
   val empty =
     { quot_maps = Symtab.empty,
       quotients = Symtab.empty,
       reflexivity_rules = Thm.full_rules,
       relator_distr_data = Symtab.empty,
-      restore_data = Symtab.empty
+      restore_data = Symtab.empty,
+      no_code_types = Symtab.empty
     }
   val extend = I
   fun merge
     ( { quot_maps = qm1, quotients = q1, reflexivity_rules = rr1, relator_distr_data = rdd1, 
-        restore_data = rd1 },
+        restore_data = rd1, no_code_types = nct1 },
       { quot_maps = qm2, quotients = q2, reflexivity_rules = rr2, relator_distr_data = rdd2,
-        restore_data = rd2 } ) =
+        restore_data = rd2, no_code_types = nct2 } ) =
     { quot_maps = Symtab.merge (K true) (qm1, qm2),
       quotients = Symtab.merge (K true) (q1, q2),
       reflexivity_rules = Item_Net.merge (rr1, rr2),
       relator_distr_data = Symtab.merge (K true) (rdd1, rdd2),
-      restore_data = Symtab.join join_restore_data (rd1, rd2) }
+      restore_data = Symtab.join join_restore_data (rd1, rd2),
+      no_code_types = Symtab.merge (K true) (nct1, nct2)
+    }
 )
 
-fun map_data f1 f2 f3 f4 f5
-  { quot_maps, quotients, reflexivity_rules, relator_distr_data, restore_data } =
+fun map_data f1 f2 f3 f4 f5 f6
+  { quot_maps, quotients, reflexivity_rules, relator_distr_data, restore_data, no_code_types } =
   { quot_maps = f1 quot_maps,
     quotients = f2 quotients,
     reflexivity_rules = f3 reflexivity_rules,
     relator_distr_data = f4 relator_distr_data,
-    restore_data = f5 restore_data }
+    restore_data = f5 restore_data,
+    no_code_types = f6 no_code_types
+  }
 
-fun map_quot_maps           f = map_data f I I I I
-fun map_quotients           f = map_data I f I I I
-fun map_reflexivity_rules   f = map_data I I f I I
-fun map_relator_distr_data  f = map_data I I I f I
-fun map_restore_data        f = map_data I I I I f
+fun map_quot_maps           f = map_data f I I I I I
+fun map_quotients           f = map_data I f I I I I
+fun map_reflexivity_rules   f = map_data I I f I I I
+fun map_relator_distr_data  f = map_data I I I f I I
+fun map_restore_data        f = map_data I I I I f I
+fun map_no_code_types       f = map_data I I I I I f
   
 val get_quot_maps'           = #quot_maps o Data.get
 val get_quotients'           = #quotients o Data.get
 val get_reflexivity_rules'   = #reflexivity_rules o Data.get
 val get_relator_distr_data'  = #relator_distr_data o Data.get
 val get_restore_data'        = #restore_data o Data.get
+val get_no_code_types'       = #no_code_types o Data.get
 
 fun get_quot_maps          ctxt = get_quot_maps' (Context.Proof ctxt)
 fun get_quotients          ctxt = get_quotients' (Context.Proof ctxt)
 fun get_relator_distr_data ctxt = get_relator_distr_data' (Context.Proof ctxt)
 fun get_restore_data       ctxt = get_restore_data' (Context.Proof ctxt)
+fun get_no_code_types      ctxt = get_no_code_types' (Context.Proof ctxt)
 
 (* info about Quotient map theorems *)
 
@@ -500,6 +513,13 @@
   #> Global_Theory.add_thms_dynamic
      (@{binding relator_mono_raw}, get_mono_rules_raw)
 
+(* no_code types *)
+
+fun add_no_code_type type_name ctxt = 
+  Data.map (map_no_code_types (Symtab.update (type_name, ()))) ctxt;
+
+fun is_no_code_type ctxt type_name = (Symtab.defined o get_no_code_types) ctxt type_name
+
 (* theory setup *)
 
 val setup =

--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Thu Jul 24 19:01:06 2014 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Thu Jul 24 20:21:34 2014 +0200
@@ -234,7 +234,7 @@
 fun setup_lifting_infr gen_code quot_thm opt_reflp_thm lthy =
   let
     val _ = quot_thm_sanity_check lthy quot_thm
-    val (_, qtyp) = quot_thm_rty_qty quot_thm
+    val (_, qty) = quot_thm_rty_qty quot_thm
     val (pcrel_def, lthy) = define_pcrel (quot_thm_crel quot_thm) lthy
     (**)
     val pcrel_def = Option.map (Morphism.thm (Local_Theory.target_morphism lthy)) pcrel_def
@@ -246,7 +246,7 @@
       SOME pcrel_def => SOME { pcrel_def = pcrel_def, pcr_cr_eq = the pcr_cr_eq }
       | NONE => NONE
     val quotients = { quot_thm = quot_thm, pcr_info = pcr_info }
-    val qty_full_name = (fst o dest_Type) qtyp  
+    val qty_full_name = (fst o dest_Type) qty
     fun quot_info phi = Lifting_Info.transform_quotient phi quotients
     val reflexivity_rule_attr = Attrib.internal (K Lifting_Info.add_reflexivity_rule_attribute)
     val lthy = case opt_reflp_thm of
@@ -256,11 +256,14 @@
         |> define_code_constr gen_code quot_thm
       | NONE => lthy
         |> define_abs_type gen_code quot_thm
+    fun declare_no_code qty =  Local_Theory.declaration {syntax = false, pervasive = true}
+        (fn phi => Lifting_Info.add_no_code_type (Morphism.typ phi qty |> Tname))
   in
     lthy
       |> Local_Theory.declaration {syntax = false, pervasive = true}
         (fn phi => Lifting_Info.update_quotients qty_full_name (quot_info phi))
       |> lifting_bundle qty_full_name quotients
+      |> (if not gen_code then declare_no_code qty else I)
   end
 
 local

--- a/src/HOL/Tools/Lifting/lifting_term.ML	Thu Jul 24 19:01:06 2014 +0200
+++ b/src/HOL/Tools/Lifting/lifting_term.ML	Thu Jul 24 20:21:34 2014 +0200
@@ -11,6 +11,8 @@
   exception MERGE_TRANSFER_REL of Pretty.T
   exception CHECK_RTY of typ * typ
 
+  val instantiate_rtys: Proof.context -> typ * typ -> typ * typ
+
   val prove_quot_thm: Proof.context -> typ * typ -> thm
 
   val abs_fun: Proof.context -> typ * typ -> term