# HG changeset patch
# User kuncar
# Date 1337611008 -7200
# Node ID 8c8a03765de79223a84db4f8e16cb59d92d9759d
# Parent  9cb132898ac84a4646ad0e317710fe38c0cba80b
quot_del attribute, it allows us to deregister quotient types

diff -r 9cb132898ac8 -r 8c8a03765de7 src/HOL/Tools/Lifting/lifting_def.ML
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Mon May 21 11:31:52 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Mon May 21 16:36:48 2012 +0200
@@ -118,7 +118,7 @@
 *)
 
 fun can_generate_code_cert quot_thm  =
-  case Lifting_Term.quot_thm_rel quot_thm of
+  case quot_thm_rel quot_thm of
     Const (@{const_name HOL.eq}, _) => true
     | Const (@{const_name invariant}, _) $ _  => true
     | _ => false
@@ -136,7 +136,7 @@
         | _ => raise CODE_CERT_GEN "relation is neither equality nor invariant"
     val unfolded_def = Conv.fconv_rule (Conv.arg_conv unfold_fun_maps_beta) def_thm
     val unabs_def = unabs_all_def ctxt unfolded_def
-    val rep = (cterm_of thy o Lifting_Term.quot_thm_rep) quot_thm
+    val rep = (cterm_of thy o quot_thm_rep) quot_thm
     val rep_refl = Thm.reflexive rep RS @{thm meta_eq_to_obj_eq}
     val repped_eq = [rep_refl, unabs_def RS @{thm meta_eq_to_obj_eq}] MRSL @{thm cong}
     val code_cert = [repped_eq, abs_rep_eq] MRSL @{thm trans}
@@ -195,8 +195,8 @@
 
     val abs_eq_with_assms =
       let
-        val (rty, qty) = Lifting_Term.quot_thm_rty_qty quot_thm
-        val rel = Lifting_Term.quot_thm_rel quot_thm
+        val (rty, qty) = quot_thm_rty_qty quot_thm
+        val rel = quot_thm_rel quot_thm
         val ty_args = get_binder_types_by_rel rel (rty, qty)
         val body_type = get_body_type_by_rel rel (rty, qty)
         val quot_ret_thm = Lifting_Term.prove_quot_thm ctxt body_type
@@ -248,7 +248,7 @@
 fun has_constr ctxt quot_thm =
   let
     val thy = Proof_Context.theory_of ctxt
-    val abs_fun = Lifting_Term.quot_thm_abs quot_thm
+    val abs_fun = quot_thm_abs quot_thm
   in
     if is_Const abs_fun then
       Code.is_constr thy ((fst o dest_Const) abs_fun)
@@ -259,7 +259,7 @@
 fun has_abstr ctxt quot_thm =
   let
     val thy = Proof_Context.theory_of ctxt
-    val abs_fun = Lifting_Term.quot_thm_abs quot_thm
+    val abs_fun = quot_thm_abs quot_thm
   in
     if is_Const abs_fun then
       Code.is_abstr thy ((fst o dest_Const) abs_fun)
@@ -304,7 +304,7 @@
   let
     val rty = fastype_of rhs
     val quot_thm = Lifting_Term.prove_quot_thm lthy (rty, qty)
-    val absrep_trm =  Lifting_Term.quot_thm_abs quot_thm
+    val absrep_trm =  quot_thm_abs quot_thm
     val rty_forced = (domain_type o fastype_of) absrep_trm
     val forced_rhs = force_rty_type lthy rty_forced rhs
     val lhs = Free (Binding.print (#1 var), qty)
diff -r 9cb132898ac8 -r 8c8a03765de7 src/HOL/Tools/Lifting/lifting_info.ML
--- a/src/HOL/Tools/Lifting/lifting_info.ML	Mon May 21 11:31:52 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_info.ML	Mon May 21 16:36:48 2012 +0200
@@ -99,7 +99,7 @@
     Quotmaps.map (Symtab.update (relatorT_name, minfo)) ctxt
   end    
 
-val quotmaps_attribute_setup =
+val quot_map_attribute_setup =
   Attrib.setup @{binding quot_map} (Scan.succeed (Thm.declaration_attribute add_quot_map))
     "declaration of the Quotient map theorem"
 
@@ -136,6 +136,22 @@
 
 fun update_quotients str qinfo = Quotients.map (Symtab.update (str, qinfo))
 
+fun delete_quotients quot_thm ctxt =
+  let
+    val (_, qtyp) = quot_thm_rty_qty quot_thm
+    val qty_full_name = (fst o dest_Type) qtyp
+    val symtab = Quotients.get ctxt
+    val maybe_stored_quot_thm = Symtab.lookup symtab qty_full_name
+  in
+    case maybe_stored_quot_thm of
+      SOME {quot_thm = stored_quot_thm} => 
+        if Thm.eq_thm_prop (stored_quot_thm, quot_thm) then
+          Quotients.map (Symtab.delete qty_full_name) ctxt
+        else
+          ctxt
+      | NONE => ctxt
+  end
+
 fun dest_quotients ctxt =  (* FIXME slightly expensive way to retrieve data *)
   map snd (Symtab.dest (Quotients.get (Context.Proof ctxt)))
 
@@ -153,6 +169,10 @@
     |> Pretty.writeln
   end
 
+val quot_del_attribute_setup =
+  Attrib.setup @{binding quot_del} (Scan.succeed (Thm.declaration_attribute delete_quotients))
+    "deletes the Quotient theorem"
+
 structure Invariant_Commute = Named_Thms
 (
   val name = @{binding invariant_commute}
@@ -174,7 +194,8 @@
 (* theory setup *)
 
 val setup =
-  quotmaps_attribute_setup
+  quot_map_attribute_setup
+  #> quot_del_attribute_setup
   #> Invariant_Commute.setup
   #> Reflp_Preserve.setup
 
diff -r 9cb132898ac8 -r 8c8a03765de7 src/HOL/Tools/Lifting/lifting_setup.ML
--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Mon May 21 11:31:52 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Mon May 21 16:36:48 2012 +0200
@@ -38,7 +38,7 @@
 
 fun define_code_constr gen_code quot_thm lthy =
   let
-    val abs = Lifting_Term.quot_thm_abs quot_thm
+    val abs = quot_thm_abs quot_thm
     val abs_background = Morphism.term (Local_Theory.target_morphism lthy) abs
   in
     if gen_code andalso is_Const abs_background then
@@ -71,7 +71,7 @@
 fun quot_thm_sanity_check ctxt quot_thm =
   let
     val ((_, [quot_thm_fixed]), ctxt') = Variable.importT [quot_thm] ctxt 
-    val (rty, qty) = Lifting_Term.quot_thm_rty_qty quot_thm_fixed
+    val (rty, qty) = quot_thm_rty_qty quot_thm_fixed
     val rty_tfreesT = Term.add_tfree_namesT rty []
     val qty_tfreesT = Term.add_tfree_namesT qty []
     val extra_rty_tfrees =
@@ -97,7 +97,7 @@
 fun setup_lifting_infr gen_code quot_thm maybe_reflp_thm lthy =
   let
     val _ = quot_thm_sanity_check lthy quot_thm
-    val (_, qtyp) = Lifting_Term.quot_thm_rty_qty quot_thm
+    val (_, qtyp) = quot_thm_rty_qty quot_thm
     val qty_full_name = (fst o dest_Type) qtyp
     val quotients = { quot_thm = quot_thm }
     fun quot_info phi = Lifting_Info.transform_quotients phi quotients
@@ -127,7 +127,7 @@
 fun setup_by_quotient gen_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
+    val (_, qty) = quot_thm_rty_qty quot_thm
     val induct_attr = Attrib.internal (K (Induct.induct_type (fst (dest_Type qty))))
     val qty_name = (Binding.name o Long_Name.base_name o fst o dest_Type) qty
     fun qualify suffix = Binding.qualified true suffix qty_name
@@ -183,7 +183,7 @@
       | _ => 
         [typedef_thm, T_def] MRSL @{thm typedef_to_Quotient}
 
-    val (_, qty) = Lifting_Term.quot_thm_rty_qty quot_thm
+    val (_, qty) = quot_thm_rty_qty quot_thm
     val qty_name = (Binding.name o Long_Name.base_name o fst o dest_Type) qty
     fun qualify suffix = Binding.qualified true suffix qty_name
     val simplify = Raw_Simplifier.rewrite_rule [mk_meta_eq @{thm mem_Collect_eq}]
diff -r 9cb132898ac8 -r 8c8a03765de7 src/HOL/Tools/Lifting/lifting_term.ML
--- a/src/HOL/Tools/Lifting/lifting_term.ML	Mon May 21 11:31:52 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_term.ML	Mon May 21 16:36:48 2012 +0200
@@ -14,11 +14,6 @@
   val abs_fun: Proof.context -> typ * typ -> term
 
   val equiv_relation: Proof.context -> typ * typ -> term
-
-  val quot_thm_rel: thm -> term
-  val quot_thm_abs: thm -> term
-  val quot_thm_rep: thm -> term
-  val quot_thm_rty_qty: thm -> typ * typ
 end
 
 structure Lifting_Term: LIFTING_TERM =
@@ -79,31 +74,6 @@
 
 fun is_id_quot thm = (prop_of thm = prop_of @{thm identity_quotient})
 
-(*
-  quot_thm_rel, quot_thm_abs, quot_thm_rep and quot_thm_rty_qty - simple functions
-    for destructing quotient theorems (Quotient R Abs Rep T).
-*)
-
-fun quot_thm_rel quot_thm =
-  case (dest_Quotient o HOLogic.dest_Trueprop o prop_of) quot_thm of
-    (rel, _, _, _) => rel
-
-fun quot_thm_abs quot_thm =
-  case (dest_Quotient o HOLogic.dest_Trueprop o prop_of) quot_thm of
-    (_, abs, _, _) => abs
-
-fun quot_thm_rep quot_thm =
-  case (dest_Quotient o HOLogic.dest_Trueprop o prop_of) quot_thm of
-    (_, _, rep, _) => rep
-
-fun quot_thm_rty_qty quot_thm =
-  let
-    val abs = quot_thm_abs quot_thm
-    val abs_type = fastype_of abs  
-  in
-    (domain_type abs_type, range_type abs_type)
-  end
-
 fun check_raw_types (provided_rty_name, rty_of_qty_name) qty_name =
   if provided_rty_name <> rty_of_qty_name then
     raise QUOT_THM_INTERNAL (Pretty.block 
diff -r 9cb132898ac8 -r 8c8a03765de7 src/HOL/Tools/Lifting/lifting_util.ML
--- a/src/HOL/Tools/Lifting/lifting_util.ML	Mon May 21 11:31:52 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_util.ML	Mon May 21 16:36:48 2012 +0200
@@ -9,6 +9,11 @@
   val MRSL: thm list * thm -> thm
   val Trueprop_conv: conv -> conv
   val dest_Quotient: term -> term * term * term * term
+
+  val quot_thm_rel: thm -> term
+  val quot_thm_abs: thm -> term
+  val quot_thm_rep: thm -> term
+  val quot_thm_rty_qty: thm -> typ * typ
 end;
 
 
@@ -28,4 +33,29 @@
       = (rel, abs, rep, cr)
   | dest_Quotient t = raise TERM ("dest_Quotient", [t])
 
+(*
+  quot_thm_rel, quot_thm_abs, quot_thm_rep and quot_thm_rty_qty - simple functions
+    for destructing quotient theorems (Quotient R Abs Rep T).
+*)
+
+fun quot_thm_rel quot_thm =
+  case (dest_Quotient o HOLogic.dest_Trueprop o prop_of) quot_thm of
+    (rel, _, _, _) => rel
+
+fun quot_thm_abs quot_thm =
+  case (dest_Quotient o HOLogic.dest_Trueprop o prop_of) quot_thm of
+    (_, abs, _, _) => abs
+
+fun quot_thm_rep quot_thm =
+  case (dest_Quotient o HOLogic.dest_Trueprop o prop_of) quot_thm of
+    (_, _, rep, _) => rep
+
+fun quot_thm_rty_qty quot_thm =
+  let
+    val abs = quot_thm_abs quot_thm
+    val abs_type = fastype_of abs  
+  in
+    (domain_type abs_type, range_type abs_type)
+  end
+
 end;