1.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Thu Jul 24 19:01:06 2014 +0200
     1.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Thu Jul 24 20:21:34 2014 +0200
     1.3 @@ -401,6 +401,22 @@
     1.4    val register_code_eq_attribute = Thm.declaration_attribute
     1.5      (fn thm => Context.mapping (register_encoded_code_eq thm) I)
     1.6    val register_code_eq_attrib = Attrib.internal (K register_code_eq_attribute)
     1.7 +
     1.8 +  fun no_no_code ctxt (rty, qty) =
     1.9 +    if same_type_constrs (rty, qty) then
    1.10 +      forall (no_no_code ctxt) (Targs rty ~~ Targs qty)
    1.11 +    else
    1.12 +      if is_Type qty then
    1.13 +        if Lifting_Info.is_no_code_type ctxt (Tname qty) then false
    1.14 +        else 
    1.15 +          let 
    1.16 +            val (rty', rtyq) = Lifting_Term.instantiate_rtys ctxt (rty, qty)
    1.17 +            val (rty's, rtyqs) = (Targs rty', Targs rtyq)
    1.18 +          in
    1.19 +            forall (no_no_code ctxt) (rty's ~~ rtyqs)
    1.20 +          end
    1.21 +      else
    1.22 +        true
    1.23  in
    1.24  
    1.25  fun register_code_eq abs_eq_thm opt_rep_eq_thm (rty, qty) lthy =
    1.26 @@ -408,8 +424,10 @@
    1.27      val thy = Proof_Context.theory_of lthy
    1.28      val encoded_code_eq = encode_code_eq thy abs_eq_thm opt_rep_eq_thm (rty, qty)
    1.29    in
    1.30 -    (snd oo Local_Theory.note) ((Binding.empty, [register_code_eq_attrib]), 
    1.31 -      [encoded_code_eq]) lthy
    1.32 +    if no_no_code lthy (rty, qty) then 
    1.33 +      (snd oo Local_Theory.note) ((Binding.empty, [register_code_eq_attrib]), [encoded_code_eq]) lthy
    1.34 +    else
    1.35 +      lthy
    1.36    end
    1.37  end
    1.38              

     2.1 --- a/src/HOL/Tools/Lifting/lifting_info.ML	Thu Jul 24 19:01:06 2014 +0200
     2.2 +++ b/src/HOL/Tools/Lifting/lifting_info.ML	Thu Jul 24 20:21:34 2014 +0200
     2.3 @@ -34,10 +34,14 @@
     2.4      pos_distr_rules: thm list, neg_distr_rules: thm list}
     2.5    val lookup_relator_distr_data: Proof.context -> string -> relator_distr_data option
     2.6  
     2.7 +  val add_no_code_type: string -> Context.generic -> Context.generic
     2.8 +  val is_no_code_type: Proof.context -> string -> bool
     2.9 +
    2.10    val get_quot_maps           : Proof.context -> quot_map Symtab.table
    2.11    val get_quotients           : Proof.context -> quotient Symtab.table
    2.12    val get_relator_distr_data  : Proof.context -> relator_distr_data Symtab.table
    2.13    val get_restore_data        : Proof.context -> restore_data Symtab.table
    2.14 +  val get_no_code_types       : Proof.context -> unit Symtab.table
    2.15  
    2.16    val setup: theory -> theory
    2.17  end
    2.18 @@ -82,52 +86,61 @@
    2.19        quotients : quotient Symtab.table,
    2.20        reflexivity_rules : thm Item_Net.T,
    2.21        relator_distr_data : relator_distr_data Symtab.table,
    2.22 -      restore_data : restore_data Symtab.table
    2.23 +      restore_data : restore_data Symtab.table,
    2.24 +      no_code_types : unit Symtab.table
    2.25      }
    2.26    val empty =
    2.27      { quot_maps = Symtab.empty,
    2.28        quotients = Symtab.empty,
    2.29        reflexivity_rules = Thm.full_rules,
    2.30        relator_distr_data = Symtab.empty,
    2.31 -      restore_data = Symtab.empty
    2.32 +      restore_data = Symtab.empty,
    2.33 +      no_code_types = Symtab.empty
    2.34      }
    2.35    val extend = I
    2.36    fun merge
    2.37      ( { quot_maps = qm1, quotients = q1, reflexivity_rules = rr1, relator_distr_data = rdd1, 
    2.38 -        restore_data = rd1 },
    2.39 +        restore_data = rd1, no_code_types = nct1 },
    2.40        { quot_maps = qm2, quotients = q2, reflexivity_rules = rr2, relator_distr_data = rdd2,
    2.41 -        restore_data = rd2 } ) =
    2.42 +        restore_data = rd2, no_code_types = nct2 } ) =
    2.43      { quot_maps = Symtab.merge (K true) (qm1, qm2),
    2.44        quotients = Symtab.merge (K true) (q1, q2),
    2.45        reflexivity_rules = Item_Net.merge (rr1, rr2),
    2.46        relator_distr_data = Symtab.merge (K true) (rdd1, rdd2),
    2.47 -      restore_data = Symtab.join join_restore_data (rd1, rd2) }
    2.48 +      restore_data = Symtab.join join_restore_data (rd1, rd2),
    2.49 +      no_code_types = Symtab.merge (K true) (nct1, nct2)
    2.50 +    }
    2.51  )
    2.52  
    2.53 -fun map_data f1 f2 f3 f4 f5
    2.54 -  { quot_maps, quotients, reflexivity_rules, relator_distr_data, restore_data } =
    2.55 +fun map_data f1 f2 f3 f4 f5 f6
    2.56 +  { quot_maps, quotients, reflexivity_rules, relator_distr_data, restore_data, no_code_types } =
    2.57    { quot_maps = f1 quot_maps,
    2.58      quotients = f2 quotients,
    2.59      reflexivity_rules = f3 reflexivity_rules,
    2.60      relator_distr_data = f4 relator_distr_data,
    2.61 -    restore_data = f5 restore_data }
    2.62 +    restore_data = f5 restore_data,
    2.63 +    no_code_types = f6 no_code_types
    2.64 +  }
    2.65  
    2.66 -fun map_quot_maps           f = map_data f I I I I
    2.67 -fun map_quotients           f = map_data I f I I I
    2.68 -fun map_reflexivity_rules   f = map_data I I f I I
    2.69 -fun map_relator_distr_data  f = map_data I I I f I
    2.70 -fun map_restore_data        f = map_data I I I I f
    2.71 +fun map_quot_maps           f = map_data f I I I I I
    2.72 +fun map_quotients           f = map_data I f I I I I
    2.73 +fun map_reflexivity_rules   f = map_data I I f I I I
    2.74 +fun map_relator_distr_data  f = map_data I I I f I I
    2.75 +fun map_restore_data        f = map_data I I I I f I
    2.76 +fun map_no_code_types       f = map_data I I I I I f
    2.77    
    2.78  val get_quot_maps'           = #quot_maps o Data.get
    2.79  val get_quotients'           = #quotients o Data.get
    2.80  val get_reflexivity_rules'   = #reflexivity_rules o Data.get
    2.81  val get_relator_distr_data'  = #relator_distr_data o Data.get
    2.82  val get_restore_data'        = #restore_data o Data.get
    2.83 +val get_no_code_types'       = #no_code_types o Data.get
    2.84  
    2.85  fun get_quot_maps          ctxt = get_quot_maps' (Context.Proof ctxt)
    2.86  fun get_quotients          ctxt = get_quotients' (Context.Proof ctxt)
    2.87  fun get_relator_distr_data ctxt = get_relator_distr_data' (Context.Proof ctxt)
    2.88  fun get_restore_data       ctxt = get_restore_data' (Context.Proof ctxt)
    2.89 +fun get_no_code_types      ctxt = get_no_code_types' (Context.Proof ctxt)
    2.90  
    2.91  (* info about Quotient map theorems *)
    2.92  
    2.93 @@ -500,6 +513,13 @@
    2.94    #> Global_Theory.add_thms_dynamic
    2.95       (@{binding relator_mono_raw}, get_mono_rules_raw)
    2.96  
    2.97 +(* no_code types *)
    2.98 +
    2.99 +fun add_no_code_type type_name ctxt = 
   2.100 +  Data.map (map_no_code_types (Symtab.update (type_name, ()))) ctxt;
   2.101 +
   2.102 +fun is_no_code_type ctxt type_name = (Symtab.defined o get_no_code_types) ctxt type_name
   2.103 +
   2.104  (* theory setup *)
   2.105  
   2.106  val setup =

     3.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML	Thu Jul 24 19:01:06 2014 +0200
     3.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Thu Jul 24 20:21:34 2014 +0200
     3.3 @@ -234,7 +234,7 @@
     3.4  fun setup_lifting_infr gen_code quot_thm opt_reflp_thm lthy =
     3.5    let
     3.6      val _ = quot_thm_sanity_check lthy quot_thm
     3.7 -    val (_, qtyp) = quot_thm_rty_qty quot_thm
     3.8 +    val (_, qty) = quot_thm_rty_qty quot_thm
     3.9      val (pcrel_def, lthy) = define_pcrel (quot_thm_crel quot_thm) lthy
    3.10      (**)
    3.11      val pcrel_def = Option.map (Morphism.thm (Local_Theory.target_morphism lthy)) pcrel_def
    3.12 @@ -246,7 +246,7 @@
    3.13        SOME pcrel_def => SOME { pcrel_def = pcrel_def, pcr_cr_eq = the pcr_cr_eq }
    3.14        | NONE => NONE
    3.15      val quotients = { quot_thm = quot_thm, pcr_info = pcr_info }
    3.16 -    val qty_full_name = (fst o dest_Type) qtyp  
    3.17 +    val qty_full_name = (fst o dest_Type) qty
    3.18      fun quot_info phi = Lifting_Info.transform_quotient phi quotients
    3.19      val reflexivity_rule_attr = Attrib.internal (K Lifting_Info.add_reflexivity_rule_attribute)
    3.20      val lthy = case opt_reflp_thm of
    3.21 @@ -256,11 +256,14 @@
    3.22          |> define_code_constr gen_code quot_thm
    3.23        | NONE => lthy
    3.24          |> define_abs_type gen_code quot_thm
    3.25 +    fun declare_no_code qty =  Local_Theory.declaration {syntax = false, pervasive = true}
    3.26 +        (fn phi => Lifting_Info.add_no_code_type (Morphism.typ phi qty |> Tname))
    3.27    in
    3.28      lthy
    3.29        |> Local_Theory.declaration {syntax = false, pervasive = true}
    3.30          (fn phi => Lifting_Info.update_quotients qty_full_name (quot_info phi))
    3.31        |> lifting_bundle qty_full_name quotients
    3.32 +      |> (if not gen_code then declare_no_code qty else I)
    3.33    end
    3.34  
    3.35  local

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