1.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Wed Apr 18 23:13:11 2012 +0200
     1.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Wed Apr 18 23:57:44 2012 +0200
     1.3 @@ -127,9 +127,19 @@
     1.4      simplify_code_eq ctxt code_cert
     1.5    end
     1.6  
     1.7 +fun is_abstype ctxt typ =
     1.8 +  let
     1.9 +    val thy = Proof_Context.theory_of ctxt
    1.10 +    val type_name = (fst o dest_Type) typ
    1.11 +  in
    1.12 +    (snd oo Code.get_type) thy type_name
    1.13 +  end
    1.14 +  
    1.15 +
    1.16  fun define_code_cert code_eqn_thm_name def_thm rsp_thm (rty, qty) lthy = 
    1.17    let
    1.18 -    val quot_thm = Lifting_Term.prove_quot_thm lthy (get_body_types (rty, qty))
    1.19 +    val (rty_body, qty_body) = get_body_types (rty, qty)
    1.20 +    val quot_thm = Lifting_Term.prove_quot_thm lthy (rty_body, qty_body)
    1.21    in
    1.22      if can_generate_code_cert quot_thm then
    1.23        let
    1.24 @@ -137,9 +147,13 @@
    1.25          val add_abs_eqn_attribute = 
    1.26            Thm.declaration_attribute (fn thm => Context.mapping (Code.add_abs_eqn thm) I)
    1.27          val add_abs_eqn_attrib = Attrib.internal (K add_abs_eqn_attribute);
    1.28 +        val lthy' = 
    1.29 +          (snd oo Local_Theory.note) ((code_eqn_thm_name, []), [code_cert]) lthy
    1.30        in
    1.31 -        lthy
    1.32 -          |> (snd oo Local_Theory.note) ((code_eqn_thm_name, [add_abs_eqn_attrib]), [code_cert])
    1.33 +        if is_abstype lthy qty_body then
    1.34 +          (snd oo Local_Theory.note) ((Binding.empty, [add_abs_eqn_attrib]), [code_cert]) lthy'
    1.35 +        else
    1.36 +          lthy'
    1.37        end
    1.38      else
    1.39        lthy

     2.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML	Wed Apr 18 23:13:11 2012 +0200
     2.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Wed Apr 18 23:57:44 2012 +0200
     2.3 @@ -8,11 +8,11 @@
     2.4  sig
     2.5    exception SETUP_LIFTING_INFR of string
     2.6  
     2.7 -  val setup_lifting_infr: thm -> local_theory -> local_theory
     2.8 +  val setup_lifting_infr: bool -> thm -> local_theory -> local_theory
     2.9  
    2.10 -  val setup_by_quotient: thm -> thm option -> local_theory -> local_theory
    2.11 +  val setup_by_quotient: bool -> thm -> thm option -> local_theory -> local_theory
    2.12  
    2.13 -  val setup_by_typedef_thm: thm -> local_theory -> local_theory
    2.14 +  val setup_by_typedef_thm: bool -> thm -> local_theory -> local_theory
    2.15  end;
    2.16  
    2.17  structure Lifting_Setup: LIFTING_SETUP =
    2.18 @@ -38,8 +38,8 @@
    2.19      (def_thm, lthy'')
    2.20    end
    2.21  
    2.22 -fun define_abs_type quot_thm lthy =
    2.23 -  if Lifting_Def.can_generate_code_cert quot_thm then
    2.24 +fun define_abs_type no_code quot_thm lthy =
    2.25 +  if not no_code andalso Lifting_Def.can_generate_code_cert quot_thm then
    2.26      let
    2.27        val abs_type_thm = quot_thm RS @{thm Quotient_abs_rep}
    2.28        val add_abstype_attribute = 
    2.29 @@ -78,7 +78,7 @@
    2.30                                                  @ (map Pretty.string_of errs)))
    2.31    end
    2.32  
    2.33 -fun setup_lifting_infr quot_thm lthy =
    2.34 +fun setup_lifting_infr no_code quot_thm lthy =
    2.35    let
    2.36      val _ = quot_thm_sanity_check lthy quot_thm
    2.37      val (_, qtyp) = Lifting_Term.quot_thm_rty_qty quot_thm
    2.38 @@ -89,10 +89,10 @@
    2.39      lthy
    2.40        |> Local_Theory.declaration {syntax = false, pervasive = true}
    2.41          (fn phi => Lifting_Info.update_quotients qty_full_name (quot_info phi))
    2.42 -      |> define_abs_type quot_thm
    2.43 +      |> define_abs_type no_code quot_thm
    2.44    end
    2.45  
    2.46 -fun setup_by_quotient quot_thm maybe_reflp_thm lthy =
    2.47 +fun setup_by_quotient no_code quot_thm maybe_reflp_thm lthy =
    2.48    let
    2.49      val transfer_attr = Attrib.internal (K Transfer.transfer_add)
    2.50      val (_, qty) = Lifting_Term.quot_thm_rty_qty quot_thm
    2.51 @@ -119,10 +119,10 @@
    2.52          [quot_thm RS @{thm Quotient_right_total}])
    2.53        |> (snd oo Local_Theory.note) ((qualify "rel_eq_transfer", [transfer_attr]), 
    2.54          [quot_thm RS @{thm Quotient_rel_eq_transfer}])
    2.55 -      |> setup_lifting_infr quot_thm
    2.56 +      |> setup_lifting_infr no_code quot_thm
    2.57    end
    2.58  
    2.59 -fun setup_by_typedef_thm typedef_thm lthy =
    2.60 +fun setup_by_typedef_thm no_code typedef_thm lthy =
    2.61    let
    2.62      val transfer_attr = Attrib.internal (K Transfer.transfer_add)
    2.63      val (_ $ rep_fun $ _ $ typedef_set) = (HOLogic.dest_Trueprop o prop_of) typedef_thm
    2.64 @@ -169,22 +169,53 @@
    2.65          [[quot_thm] MRSL @{thm Quotient_right_unique}])
    2.66        |> (snd oo Local_Theory.note) ((qualify "right_total", [transfer_attr]), 
    2.67          [[quot_thm] MRSL @{thm Quotient_right_total}])
    2.68 -      |> setup_lifting_infr quot_thm
    2.69 +      |> setup_lifting_infr no_code quot_thm
    2.70    end
    2.71  
    2.72 -fun setup_lifting_cmd xthm lthy =
    2.73 +fun setup_lifting_cmd no_code xthm opt_reflp_xthm lthy =
    2.74    let 
    2.75      val input_thm = singleton (Attrib.eval_thms lthy) xthm
    2.76      val input_term = (HOLogic.dest_Trueprop o prop_of) input_thm
    2.77 +      handle TERM _ => error "Unsupported type of a theorem. Only Quotient or type_definition are supported."
    2.78 +
    2.79 +    fun sanity_check_reflp_thm reflp_thm = 
    2.80 +      let
    2.81 +        val reflp_tm = (HOLogic.dest_Trueprop o prop_of) reflp_thm
    2.82 +          handle TERM _ => error "Invalid form of the reflexivity theorem. Use \"reflp R\"."
    2.83 +      in
    2.84 +        case reflp_tm of
    2.85 +          Const (@{const_name reflp}, _) $ _ => ()
    2.86 +          | _ => error "Invalid form of the reflexivity theorem. Use \"reflp R\"."
    2.87 +      end
    2.88 +
    2.89 +    fun setup_quotient () = 
    2.90 +      case opt_reflp_xthm of
    2.91 +        SOME reflp_xthm => 
    2.92 +          let
    2.93 +            val reflp_thm = singleton (Attrib.eval_thms lthy) reflp_xthm
    2.94 +            val _ = sanity_check_reflp_thm reflp_thm
    2.95 +          in
    2.96 +            setup_by_quotient no_code input_thm (SOME reflp_thm) lthy
    2.97 +          end
    2.98 +        | NONE => setup_by_quotient no_code input_thm NONE lthy
    2.99 +
   2.100 +    fun setup_typedef () = 
   2.101 +      case opt_reflp_xthm of
   2.102 +        SOME _ => error "The reflexivity theorem cannot be specified if the type_definition theorem is used."
   2.103 +        | NONE => setup_by_typedef_thm no_code input_thm lthy
   2.104    in
   2.105      case input_term of
   2.106 -      (Const (@{const_name Quotient}, _) $ _ $ _ $ _ $ _) => setup_lifting_infr input_thm lthy
   2.107 -      | (Const (@{const_name type_definition}, _) $ _ $ _ $ _) => setup_by_typedef_thm input_thm lthy
   2.108 +      (Const (@{const_name Quotient}, _) $ _ $ _ $ _ $ _) => setup_quotient ()
   2.109 +      | (Const (@{const_name type_definition}, _) $ _ $ _ $ _) => setup_typedef ()
   2.110        | _ => error "Unsupported type of a theorem. Only Quotient or type_definition are supported."
   2.111    end
   2.112  
   2.113 +val opt_no_code =
   2.114 +  Scan.optional (@{keyword "("} |-- Parse.!!! ((Parse.reserved "no_code" >> K true) --| @{keyword ")"})) false
   2.115 +
   2.116  val _ = 
   2.117    Outer_Syntax.local_theory @{command_spec "setup_lifting"}
   2.118      "Setup lifting infrastructure" 
   2.119 -      (Parse_Spec.xthm >> (fn xthm => setup_lifting_cmd xthm))
   2.120 +      (opt_no_code -- Parse_Spec.xthm -- Scan.option Parse_Spec.xthm >> 
   2.121 +        (fn ((no_code, xthm), opt_reflp_xthm) => setup_lifting_cmd no_code xthm opt_reflp_xthm))
   2.122  end;

     3.1 --- a/src/HOL/Tools/Quotient/quotient_type.ML	Wed Apr 18 23:13:11 2012 +0200
     3.2 +++ b/src/HOL/Tools/Quotient/quotient_type.ML	Wed Apr 18 23:57:44 2012 +0200
     3.3 @@ -150,7 +150,7 @@
     3.4        )
     3.5    in
     3.6      lthy'
     3.7 -      |> Lifting_Setup.setup_by_quotient quot_thm reflp_thm
     3.8 +      |> Lifting_Setup.setup_by_quotient false quot_thm reflp_thm
     3.9        |> (snd oo Local_Theory.note) ((quotient_thm_name, []), [quot_thm])
    3.10    end
    3.11  

     4.1 --- a/src/HOL/Word/Word.thy	Wed Apr 18 23:13:11 2012 +0200
     4.2 +++ b/src/HOL/Word/Word.thy	Wed Apr 18 23:57:44 2012 +0200
     4.3 @@ -243,9 +243,7 @@
     4.4    "reflp (\<lambda>x y. bintrunc (len_of TYPE('a::len0)) x = bintrunc (len_of TYPE('a)) y)"
     4.5    by (simp add: reflp_def)
     4.6  
     4.7 -local_setup {*
     4.8 -  Lifting_Setup.setup_by_quotient @{thm Quotient_word} (SOME @{thm reflp_word})
     4.9 -*}
    4.10 +setup_lifting Quotient_word reflp_word
    4.11  
    4.12  text {* TODO: The next lemma could be generated automatically. *}
    4.13