# HG changeset patch
# User kuncar
# Date 1334786264 -7200
# Node ID c201a1fe0a81efdb368a861009cf1f82c56fc1db
# Parent  762eb0dacaa6ceab2ceb38a74563c2a4ab606f0d
setup_lifting: no_code switch and supoport for quotient theorems

diff -r 762eb0dacaa6 -r c201a1fe0a81 src/HOL/Tools/Lifting/lifting_def.ML
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Wed Apr 18 23:13:11 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Wed Apr 18 23:57:44 2012 +0200
@@ -127,9 +127,19 @@
     simplify_code_eq ctxt code_cert
   end
 
+fun is_abstype ctxt typ =
+  let
+    val thy = Proof_Context.theory_of ctxt
+    val type_name = (fst o dest_Type) typ
+  in
+    (snd oo Code.get_type) thy type_name
+  end
+  
+
 fun define_code_cert code_eqn_thm_name def_thm rsp_thm (rty, qty) lthy = 
   let
-    val quot_thm = Lifting_Term.prove_quot_thm lthy (get_body_types (rty, qty))
+    val (rty_body, qty_body) = get_body_types (rty, qty)
+    val quot_thm = Lifting_Term.prove_quot_thm lthy (rty_body, qty_body)
   in
     if can_generate_code_cert quot_thm then
       let
@@ -137,9 +147,13 @@
         val add_abs_eqn_attribute = 
           Thm.declaration_attribute (fn thm => Context.mapping (Code.add_abs_eqn thm) I)
         val add_abs_eqn_attrib = Attrib.internal (K add_abs_eqn_attribute);
+        val lthy' = 
+          (snd oo Local_Theory.note) ((code_eqn_thm_name, []), [code_cert]) lthy
       in
-        lthy
-          |> (snd oo Local_Theory.note) ((code_eqn_thm_name, [add_abs_eqn_attrib]), [code_cert])
+        if is_abstype lthy qty_body then
+          (snd oo Local_Theory.note) ((Binding.empty, [add_abs_eqn_attrib]), [code_cert]) lthy'
+        else
+          lthy'
       end
     else
       lthy
diff -r 762eb0dacaa6 -r c201a1fe0a81 src/HOL/Tools/Lifting/lifting_setup.ML
--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Wed Apr 18 23:13:11 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Wed Apr 18 23:57:44 2012 +0200
@@ -8,11 +8,11 @@
 sig
   exception SETUP_LIFTING_INFR of string
 
-  val setup_lifting_infr: thm -> local_theory -> local_theory
+  val setup_lifting_infr: bool -> thm -> local_theory -> local_theory
 
-  val setup_by_quotient: thm -> thm option -> local_theory -> local_theory
+  val setup_by_quotient: bool -> thm -> thm option -> local_theory -> local_theory
 
-  val setup_by_typedef_thm: thm -> local_theory -> local_theory
+  val setup_by_typedef_thm: bool -> thm -> local_theory -> local_theory
 end;
 
 structure Lifting_Setup: LIFTING_SETUP =
@@ -38,8 +38,8 @@
     (def_thm, lthy'')
   end
 
-fun define_abs_type quot_thm lthy =
-  if Lifting_Def.can_generate_code_cert quot_thm then
+fun define_abs_type no_code quot_thm lthy =
+  if not no_code andalso Lifting_Def.can_generate_code_cert quot_thm then
     let
       val abs_type_thm = quot_thm RS @{thm Quotient_abs_rep}
       val add_abstype_attribute = 
@@ -78,7 +78,7 @@
                                                 @ (map Pretty.string_of errs)))
   end
 
-fun setup_lifting_infr quot_thm lthy =
+fun setup_lifting_infr no_code quot_thm lthy =
   let
     val _ = quot_thm_sanity_check lthy quot_thm
     val (_, qtyp) = Lifting_Term.quot_thm_rty_qty quot_thm
@@ -89,10 +89,10 @@
     lthy
       |> Local_Theory.declaration {syntax = false, pervasive = true}
         (fn phi => Lifting_Info.update_quotients qty_full_name (quot_info phi))
-      |> define_abs_type quot_thm
+      |> define_abs_type no_code quot_thm
   end
 
-fun setup_by_quotient quot_thm maybe_reflp_thm lthy =
+fun setup_by_quotient no_code quot_thm maybe_reflp_thm lthy =
   let
     val transfer_attr = Attrib.internal (K Transfer.transfer_add)
     val (_, qty) = Lifting_Term.quot_thm_rty_qty quot_thm
@@ -119,10 +119,10 @@
         [quot_thm RS @{thm Quotient_right_total}])
       |> (snd oo Local_Theory.note) ((qualify "rel_eq_transfer", [transfer_attr]), 
         [quot_thm RS @{thm Quotient_rel_eq_transfer}])
-      |> setup_lifting_infr quot_thm
+      |> setup_lifting_infr no_code quot_thm
   end
 
-fun setup_by_typedef_thm typedef_thm lthy =
+fun setup_by_typedef_thm no_code typedef_thm lthy =
   let
     val transfer_attr = Attrib.internal (K Transfer.transfer_add)
     val (_ $ rep_fun $ _ $ typedef_set) = (HOLogic.dest_Trueprop o prop_of) typedef_thm
@@ -169,22 +169,53 @@
         [[quot_thm] MRSL @{thm Quotient_right_unique}])
       |> (snd oo Local_Theory.note) ((qualify "right_total", [transfer_attr]), 
         [[quot_thm] MRSL @{thm Quotient_right_total}])
-      |> setup_lifting_infr quot_thm
+      |> setup_lifting_infr no_code quot_thm
   end
 
-fun setup_lifting_cmd xthm lthy =
+fun setup_lifting_cmd no_code xthm opt_reflp_xthm lthy =
   let 
     val input_thm = singleton (Attrib.eval_thms lthy) xthm
     val input_term = (HOLogic.dest_Trueprop o prop_of) input_thm
+      handle TERM _ => error "Unsupported type of a theorem. Only Quotient or type_definition are supported."
+
+    fun sanity_check_reflp_thm reflp_thm = 
+      let
+        val reflp_tm = (HOLogic.dest_Trueprop o prop_of) reflp_thm
+          handle TERM _ => error "Invalid form of the reflexivity theorem. Use \"reflp R\"."
+      in
+        case reflp_tm of
+          Const (@{const_name reflp}, _) $ _ => ()
+          | _ => error "Invalid form of the reflexivity theorem. Use \"reflp R\"."
+      end
+
+    fun setup_quotient () = 
+      case opt_reflp_xthm of
+        SOME reflp_xthm => 
+          let
+            val reflp_thm = singleton (Attrib.eval_thms lthy) reflp_xthm
+            val _ = sanity_check_reflp_thm reflp_thm
+          in
+            setup_by_quotient no_code input_thm (SOME reflp_thm) lthy
+          end
+        | NONE => setup_by_quotient no_code input_thm NONE lthy
+
+    fun setup_typedef () = 
+      case opt_reflp_xthm of
+        SOME _ => error "The reflexivity theorem cannot be specified if the type_definition theorem is used."
+        | NONE => setup_by_typedef_thm no_code input_thm lthy
   in
     case input_term of
-      (Const (@{const_name Quotient}, _) $ _ $ _ $ _ $ _) => setup_lifting_infr input_thm lthy
-      | (Const (@{const_name type_definition}, _) $ _ $ _ $ _) => setup_by_typedef_thm input_thm lthy
+      (Const (@{const_name Quotient}, _) $ _ $ _ $ _ $ _) => setup_quotient ()
+      | (Const (@{const_name type_definition}, _) $ _ $ _ $ _) => setup_typedef ()
       | _ => error "Unsupported type of a theorem. Only Quotient or type_definition are supported."
   end
 
+val opt_no_code =
+  Scan.optional (@{keyword "("} |-- Parse.!!! ((Parse.reserved "no_code" >> K true) --| @{keyword ")"})) false
+
 val _ = 
   Outer_Syntax.local_theory @{command_spec "setup_lifting"}
     "Setup lifting infrastructure" 
-      (Parse_Spec.xthm >> (fn xthm => setup_lifting_cmd xthm))
+      (opt_no_code -- Parse_Spec.xthm -- Scan.option Parse_Spec.xthm >> 
+        (fn ((no_code, xthm), opt_reflp_xthm) => setup_lifting_cmd no_code xthm opt_reflp_xthm))
 end;
diff -r 762eb0dacaa6 -r c201a1fe0a81 src/HOL/Tools/Quotient/quotient_type.ML
--- a/src/HOL/Tools/Quotient/quotient_type.ML	Wed Apr 18 23:13:11 2012 +0200
+++ b/src/HOL/Tools/Quotient/quotient_type.ML	Wed Apr 18 23:57:44 2012 +0200
@@ -150,7 +150,7 @@
       )
   in
     lthy'
-      |> Lifting_Setup.setup_by_quotient quot_thm reflp_thm
+      |> Lifting_Setup.setup_by_quotient false quot_thm reflp_thm
       |> (snd oo Local_Theory.note) ((quotient_thm_name, []), [quot_thm])
   end
 
diff -r 762eb0dacaa6 -r c201a1fe0a81 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Wed Apr 18 23:13:11 2012 +0200
+++ b/src/HOL/Word/Word.thy	Wed Apr 18 23:57:44 2012 +0200
@@ -243,9 +243,7 @@
   "reflp (\<lambda>x y. bintrunc (len_of TYPE('a::len0)) x = bintrunc (len_of TYPE('a)) y)"
   by (simp add: reflp_def)
 
-local_setup {*
-  Lifting_Setup.setup_by_quotient @{thm Quotient_word} (SOME @{thm reflp_word})
-*}
+setup_lifting Quotient_word reflp_word
 
 text {* TODO: The next lemma could be generated automatically. *}