src/HOL/Tools/Quotient/quotient_type.ML

--- a/src/HOL/Tools/Quotient/quotient_type.ML	Wed May 16 19:15:45 2012 +0200
+++ b/src/HOL/Tools/Quotient/quotient_type.ML	Wed May 16 19:17:20 2012 +0200
@@ -9,12 +9,12 @@
   val can_generate_code_cert: thm -> bool
   
   val add_quotient_type: ((string list * binding * mixfix) * (typ * term * bool) * 
-    ((binding * binding) option)) * thm -> local_theory -> Quotient_Info.quotients * local_theory
+    ((binding * binding) option * bool)) * thm -> local_theory -> Quotient_Info.quotients * local_theory
 
   val quotient_type: ((string list * binding * mixfix) * (typ * term * bool) * 
-    ((binding * binding) option)) list -> Proof.context -> Proof.state
+    ((binding * binding) option * bool)) list -> Proof.context -> Proof.state
 
-  val quotient_type_cmd: (((((string list * binding) * mixfix) * string) * (bool * string)) *
+  val quotient_type_cmd: ((((((bool * string list) * binding) * mixfix) * string) * (bool * string)) *
     (binding * binding) option) list -> Proof.context -> Proof.state
 end;
 
@@ -132,7 +132,7 @@
     (def_thm, lthy'')
   end;
 
-fun setup_lifting_package quot3_thm equiv_thm lthy =
+fun setup_lifting_package gen_code quot3_thm equiv_thm lthy =
   let
     val (_ $ _ $ abs_fun $ _) = (HOLogic.dest_Trueprop o prop_of) quot3_thm
     val (T_def, lthy') = define_cr_rel equiv_thm abs_fun lthy
@@ -150,11 +150,11 @@
       )
   in
     lthy'
-      |> Lifting_Setup.setup_by_quotient false quot_thm reflp_thm
+      |> Lifting_Setup.setup_by_quotient gen_code quot_thm reflp_thm
       |> (snd oo Local_Theory.note) ((quotient_thm_name, []), [quot_thm])
   end
 
-fun init_quotient_infr quot_thm equiv_thm lthy =
+fun init_quotient_infr gen_code quot_thm equiv_thm lthy =
   let
     val (_ $ rel $ abs $ rep) = (HOLogic.dest_Trueprop o prop_of) quot_thm
     val (qtyp, rtyp) = (dest_funT o fastype_of) rep
@@ -170,11 +170,11 @@
         (fn phi => Quotient_Info.update_quotients qty_full_name (quot_info phi)
           #> Quotient_Info.update_abs_rep qty_full_name (abs_rep_info phi))
       |> define_abs_type quot_thm
-      |> setup_lifting_package quot_thm equiv_thm
+      |> setup_lifting_package gen_code quot_thm equiv_thm
   end
 
 (* main function for constructing a quotient type *)
-fun add_quotient_type (((vs, qty_name, mx), (rty, rel, partial), opt_morphs), equiv_thm) lthy =
+fun add_quotient_type (((vs, qty_name, mx), (rty, rel, partial), (opt_morphs, gen_code)), equiv_thm) lthy =
   let
     val part_equiv =
       if partial
@@ -226,7 +226,7 @@
       quot_thm = quotient_thm}
 
     val lthy4 = lthy3
-      |> init_quotient_infr quotient_thm equiv_thm
+      |> init_quotient_infr gen_code quotient_thm equiv_thm
       |> (snd oo Local_Theory.note)
         ((equiv_thm_name,
           if partial then [] else [Attrib.internal (K Quotient_Info.equiv_rules_add)]),
@@ -307,6 +307,7 @@
  - the partial flag (a boolean)
  - the relation according to which the type is quotient
  - optional names of morphisms (rep/abs)
+ - flag if code should be generated by Lifting package
 
  it opens a proof-state in which one has to show that the
  relations are equivalence relations
@@ -336,7 +337,7 @@
 
 fun quotient_type_cmd specs lthy =
   let
-    fun parse_spec (((((vs, qty_name), mx), rty_str), (partial, rel_str)), opt_morphs) lthy =
+    fun parse_spec ((((((gen_code, vs), qty_name), mx), rty_str), (partial, rel_str)), opt_morphs) lthy =
       let
         val rty = Syntax.read_typ lthy rty_str
         val tmp_lthy1 = Variable.declare_typ rty lthy
@@ -346,7 +347,7 @@
           |> Syntax.check_term tmp_lthy1
         val tmp_lthy2 = Variable.declare_term rel tmp_lthy1
       in
-        (((vs, qty_name, mx), (rty, rel, partial), opt_morphs), tmp_lthy2)
+        (((vs, qty_name, mx), (rty, rel, partial), (opt_morphs, gen_code)), tmp_lthy2)
       end
 
     val (spec', _) = fold_map parse_spec specs lthy
@@ -354,11 +355,14 @@
     quotient_type spec' lthy
   end
 
+val opt_gen_code =
+  Scan.optional (@{keyword "("} |-- (Parse.reserved "no_code" >> K false) --| Parse.!!! @{keyword ")"}) true
+
 val partial = Scan.optional (Parse.reserved "partial" -- @{keyword ":"} >> K true) false
 
 val quotspec_parser =
   Parse.and_list1
-    ((Parse.type_args -- Parse.binding) --
+    ((opt_gen_code -- Parse.type_args -- Parse.binding) --
       (* FIXME Parse.type_args_constrained and standard treatment of sort constraints *)
       Parse.opt_mixfix -- (@{keyword "="} |-- Parse.typ) --
         (@{keyword "/"} |-- (partial -- Parse.term))  --