# HG changeset patch
# User kuncar
# Date 1379338217 -7200
# Node ID ee90c67502c9a341665256e68d60521e0e34a367
# Parent  71a0a8687d6cbe36cb313204c3bc7b74bf2513b7
restoring Transfer/Lifting context

diff -r 71a0a8687d6c -r ee90c67502c9 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Mon Sep 16 11:54:57 2013 +0200
+++ b/etc/isar-keywords.el	Mon Sep 16 15:30:17 2013 +0200
@@ -135,6 +135,8 @@
     "lemmas"
     "let"
     "lift_definition"
+    "lifting_forget"
+    "lifting_update"
     "linear_undo"
     "local_setup"
     "locale"
@@ -539,6 +541,8 @@
     "instantiation"
     "judgment"
     "lemmas"
+    "lifting_forget"
+    "lifting_update"
     "local_setup"
     "locale"
     "method_setup"
diff -r 71a0a8687d6c -r ee90c67502c9 src/HOL/Lifting.thy
--- a/src/HOL/Lifting.thy	Mon Sep 16 11:54:57 2013 +0200
+++ b/src/HOL/Lifting.thy	Mon Sep 16 15:30:17 2013 +0200
@@ -11,7 +11,7 @@
   "parametric" and
   "print_quot_maps" "print_quotients" :: diag and
   "lift_definition" :: thy_goal and
-  "setup_lifting" :: thy_decl
+  "setup_lifting" "lifting_forget" "lifting_update" :: thy_decl
 begin
 
 subsection {* Function map *}
diff -r 71a0a8687d6c -r ee90c67502c9 src/HOL/Tools/Lifting/lifting_def.ML
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Mon Sep 16 11:54:57 2013 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Mon Sep 16 15:30:17 2013 +0200
@@ -16,7 +16,7 @@
     (binding * string option * mixfix) * string * (Facts.ref * Args.src list) option -> local_theory -> Proof.state
 
   val can_generate_code_cert: thm -> bool
-end;
+end
 
 structure Lifting_Def: LIFTING_DEF =
 struct
@@ -583,4 +583,4 @@
       (liftdef_parser >> lift_def_cmd_with_err_handling)
 
 
-end; (* structure *)
+end (* structure *)
diff -r 71a0a8687d6c -r ee90c67502c9 src/HOL/Tools/Lifting/lifting_info.ML
--- a/src/HOL/Tools/Lifting/lifting_info.ML	Mon Sep 16 11:54:57 2013 +0200
+++ b/src/HOL/Tools/Lifting/lifting_info.ML	Mon Sep 16 15:30:17 2013 +0200
@@ -12,12 +12,19 @@
   
   type pcr = {pcrel_def: thm, pcr_cr_eq: thm}
   type quotient = {quot_thm: thm, pcr_info: pcr option}
+  val pcr_eq: pcr * pcr -> bool
+  val quotient_eq: quotient * quotient -> bool
   val transform_quotient: morphism -> quotient -> quotient
   val lookup_quotients: Proof.context -> string -> quotient option
   val update_quotients: string -> quotient -> Context.generic -> Context.generic
   val delete_quotients: thm -> Context.generic -> Context.generic
   val print_quotients: Proof.context -> unit
 
+  type restore_data = {quotient : quotient, transfer_rules: thm Item_Net.T}
+  val lookup_restore_data: Proof.context -> string -> restore_data option
+  val init_restore_data: string -> quotient -> Context.generic -> Context.generic
+  val add_transfer_rules_in_restore_data: string -> thm Item_Net.T -> Context.generic -> Context.generic  
+
   val get_invariant_commute_rules: Proof.context -> thm list
   
   val get_reflexivity_rules: Proof.context -> thm list
@@ -31,9 +38,10 @@
   val get_quot_maps           : Proof.context -> quot_map Symtab.table
   val get_quotients           : Proof.context -> quotient Symtab.table
   val get_relator_distr_data  : Proof.context -> relator_distr_data Symtab.table
+  val get_restore_data        : Proof.context -> restore_data Symtab.table
 
   val setup: theory -> theory
-end;
+end
 
 structure Lifting_Info: LIFTING_INFO =
 struct
@@ -47,6 +55,7 @@
 type quotient = {quot_thm: thm, pcr_info: pcr option}
 type relator_distr_data = {pos_mono_rule: thm, neg_mono_rule: thm, 
   pos_distr_rules: thm list, neg_distr_rules: thm list}
+type restore_data = {quotient : quotient, transfer_rules: thm Item_Net.T}
 
 structure Data = Generic_Data
 (
@@ -54,44 +63,53 @@
     { quot_maps : quot_map Symtab.table,
       quotients : quotient Symtab.table,
       reflexivity_rules : thm Item_Net.T,
-      relator_distr_data : relator_distr_data Symtab.table
+      relator_distr_data : relator_distr_data Symtab.table,
+      restore_data : restore_data Symtab.table
     }
   val empty =
     { quot_maps = Symtab.empty,
       quotients = Symtab.empty,
       reflexivity_rules = Thm.full_rules,
-      relator_distr_data = Symtab.empty
+      relator_distr_data = Symtab.empty,
+      restore_data = Symtab.empty
     }
   val extend = I
   fun merge
-    ( { quot_maps = qm1, quotients = q1, reflexivity_rules = rr1, relator_distr_data = rdd1 },
-      { quot_maps = qm2, quotients = q2, reflexivity_rules = rr2, relator_distr_data = rdd2 } ) =
+    ( { quot_maps = qm1, quotients = q1, reflexivity_rules = rr1, relator_distr_data = rdd1, 
+        restore_data = rd1 },
+      { quot_maps = qm2, quotients = q2, reflexivity_rules = rr2, relator_distr_data = rdd2,
+        restore_data = rd2 } ) =
     { quot_maps = Symtab.merge (K true) (qm1, qm2),
       quotients = Symtab.merge (K true) (q1, q2),
       reflexivity_rules = Item_Net.merge (rr1, rr2),
-      relator_distr_data = Symtab.merge (K true) (rdd1, rdd2) }
+      relator_distr_data = Symtab.merge (K true) (rdd1, rdd2),
+      restore_data = Symtab.merge (K true) (rd1, rd2) }
 )
 
-fun map_data f1 f2 f3 f4
-  { quot_maps, quotients, reflexivity_rules, relator_distr_data} =
+fun map_data f1 f2 f3 f4 f5
+  { quot_maps, quotients, reflexivity_rules, relator_distr_data, restore_data } =
   { quot_maps = f1 quot_maps,
     quotients = f2 quotients,
     reflexivity_rules = f3 reflexivity_rules,
-    relator_distr_data = f4 relator_distr_data }
+    relator_distr_data = f4 relator_distr_data,
+    restore_data = f5 restore_data }
 
-fun map_quot_maps           f = map_data f I I I
-fun map_quotients           f = map_data I f I I
-fun map_reflexivity_rules   f = map_data I I f I
-fun map_relator_distr_data  f = map_data I I I f
+fun map_quot_maps           f = map_data f I I I I
+fun map_quotients           f = map_data I f I I I
+fun map_reflexivity_rules   f = map_data I I f I I
+fun map_relator_distr_data  f = map_data I I I f I
+fun map_restore_data        f = map_data I I I I f
   
 val get_quot_maps'           = #quot_maps o Data.get
 val get_quotients'           = #quotients o Data.get
 val get_reflexivity_rules'   = #reflexivity_rules o Data.get
 val get_relator_distr_data'  = #relator_distr_data o Data.get
+val get_restore_data'        = #restore_data o Data.get
 
 fun get_quot_maps          ctxt = get_quot_maps' (Context.Proof ctxt)
 fun get_quotients          ctxt = get_quotients' (Context.Proof ctxt)
 fun get_relator_distr_data ctxt = get_relator_distr_data' (Context.Proof ctxt)
+fun get_restore_data       ctxt = get_restore_data' (Context.Proof ctxt)
 
 (* info about Quotient map theorems *)
 
@@ -164,6 +182,20 @@
   end
 
 (* info about quotient types *)
+
+fun pcr_eq ({pcrel_def = pcrel_def1, pcr_cr_eq = pcr_cr_eq1},
+           {pcrel_def = pcrel_def2, pcr_cr_eq = pcr_cr_eq2}) = 
+           Thm.eq_thm (pcrel_def1, pcrel_def2) andalso Thm.eq_thm (pcr_cr_eq1, pcr_cr_eq2)
+
+fun option_eq _ (NONE,NONE) = true
+  | option_eq _ (NONE,_) = false
+  | option_eq _ (_,NONE) = false
+  | option_eq cmp (SOME x, SOME y) = cmp (x,y);
+
+fun quotient_eq ({quot_thm = quot_thm1, pcr_info = pcr_info1},
+                {quot_thm = quot_thm2, pcr_info = pcr_info2}) =
+                Thm.eq_thm (quot_thm1, quot_thm2) andalso option_eq pcr_eq (pcr_info1, pcr_info2)
+
 fun transform_pcr_info phi {pcrel_def, pcr_cr_eq} =
   {pcrel_def = Morphism.thm phi pcrel_def, pcr_cr_eq = Morphism.thm phi pcr_cr_eq}
 
@@ -209,6 +241,22 @@
   Attrib.setup @{binding quot_del} (Scan.succeed (Thm.declaration_attribute delete_quotients))
     "deletes the Quotient theorem"
 
+(* data for restoring Transfer/Lifting context *)
+
+fun lookup_restore_data ctxt bundle_name = Symtab.lookup (get_restore_data ctxt) bundle_name
+
+fun update_restore_data bundle_name restore_data ctxt = 
+  Data.map (map_restore_data (Symtab.update (bundle_name, restore_data))) ctxt
+
+fun init_restore_data bundle_name qinfo ctxt = 
+  update_restore_data bundle_name { quotient = qinfo, transfer_rules = Thm.full_rules } ctxt
+
+fun add_transfer_rules_in_restore_data bundle_name transfer_rules ctxt =
+  case Symtab.lookup (get_restore_data' ctxt) bundle_name of
+    SOME restore_data => update_restore_data bundle_name { quotient = #quotient restore_data, 
+      transfer_rules = Item_Net.merge ((#transfer_rules restore_data), transfer_rules) } ctxt
+    | NONE => error ("The restore data " ^ quote bundle_name ^ " is not defined.")
+
 (* theorems that a relator of an invariant is an invariant of the corresponding predicate *)
 
 structure Invariant_Commute = Named_Thms
@@ -469,4 +517,4 @@
   Outer_Syntax.improper_command @{command_spec "print_quotients"} "print quotients"
     (Scan.succeed (Toplevel.keep (print_quotients o Toplevel.context_of)))
 
-end;
+end
diff -r 71a0a8687d6c -r ee90c67502c9 src/HOL/Tools/Lifting/lifting_setup.ML
--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Mon Sep 16 11:54:57 2013 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Mon Sep 16 15:30:17 2013 +0200
@@ -11,7 +11,9 @@
   val setup_by_quotient: bool -> thm -> thm option -> thm option -> local_theory -> local_theory
 
   val setup_by_typedef_thm: bool -> thm -> local_theory -> local_theory
-end;
+
+  val lifting_restore: Lifting_Info.quotient -> Context.generic -> Context.generic
+end
 
 structure Lifting_Setup: LIFTING_SETUP =
 struct
@@ -164,8 +166,24 @@
   else
     lthy
 
+local
+  exception QUOT_ERROR of Pretty.T list
+in
 fun quot_thm_sanity_check ctxt quot_thm =
   let
+    val _ = 
+      if (nprems_of quot_thm > 0) then   
+          raise QUOT_ERROR [Pretty.block
+            [Pretty.str "The Quotient theorem has extra assumptions:",
+             Pretty.brk 1,
+             Display.pretty_thm ctxt quot_thm]]
+      else ()
+    val _ = quot_thm |> concl_of |> HOLogic.dest_Trueprop |> dest_Quotient
+    handle TERM _ => raise QUOT_ERROR
+          [Pretty.block
+            [Pretty.str "The Quotient theorem is not of the right form:",
+             Pretty.brk 1,
+             Display.pretty_thm ctxt quot_thm]]
     val ((_, [quot_thm_fixed]), ctxt') = Variable.importT [quot_thm] ctxt 
     val (rty, qty) = quot_thm_rty_qty quot_thm_fixed
     val rty_tfreesT = Term.add_tfree_namesT rty []
@@ -186,8 +204,31 @@
                                 Pretty.str "is not a type constructor."]]
     val errs = extra_rty_tfrees @ not_type_constr
   in
-    if null errs then () else error (cat_lines (["Sanity check of the quotient theorem failed:",""] 
-                                                @ (map Pretty.string_of errs)))
+    if null errs then () else raise QUOT_ERROR errs
+  end
+  handle QUOT_ERROR errs => error (cat_lines (["Sanity check of the quotient theorem failed:"] 
+                                            @ (map (Pretty.string_of o Pretty.item o single) errs)))
+end
+
+fun lifting_bundle qty_full_name qinfo lthy = 
+  let
+    fun qualify suffix defname = Binding.qualified true suffix defname
+    val binding =  qty_full_name |> Long_Name.base_name |> Binding.name |> qualify "lifting"
+    val morphed_binding = Morphism.binding (Local_Theory.target_morphism lthy) binding
+    val bundle_name = Name_Space.full_name (Name_Space.naming_of 
+      (Context.Theory (Proof_Context.theory_of lthy))) morphed_binding
+    fun phi_qinfo phi = Lifting_Info.transform_quotient phi qinfo
+
+    val thy = Proof_Context.theory_of lthy
+    val dummy_thm = Thm.transfer thy Drule.dummy_thm
+    val pointer = Outer_Syntax.scan Position.none bundle_name
+    val restore_lifting_att = 
+      ([dummy_thm], [Args.src (("Lifting.lifting_restore_internal", pointer), Position.none)])
+  in
+    lthy 
+      |> Local_Theory.declaration {syntax = false, pervasive = true}
+           (fn phi => Lifting_Info.init_restore_data bundle_name (phi_qinfo phi))
+      |> Bundle.bundle ((binding, [restore_lifting_att])) []
   end
 
 fun setup_lifting_infr gen_code quot_thm opt_reflp_thm lthy =
@@ -221,23 +262,24 @@
     lthy
       |> Local_Theory.declaration {syntax = false, pervasive = true}
         (fn phi => Lifting_Info.update_quotients qty_full_name (quot_info phi))
+      |> lifting_bundle qty_full_name quotients
   end
 
 local
   fun importT_inst_exclude exclude ts ctxt =
     let
-      val tvars = rev (subtract op= exclude (fold Term.add_tvars ts []));
-      val (tfrees, ctxt') = Variable.invent_types (map #2 tvars) ctxt;
+      val tvars = rev (subtract op= exclude (fold Term.add_tvars ts []))
+      val (tfrees, ctxt') = Variable.invent_types (map #2 tvars) ctxt
     in (tvars ~~ map TFree tfrees, ctxt') end
   
   fun import_inst_exclude exclude ts ctxt =
     let
       val excludeT = fold (Term.add_tvarsT o snd) exclude []
-      val (instT, ctxt') = importT_inst_exclude excludeT ts ctxt;
+      val (instT, ctxt') = importT_inst_exclude excludeT ts ctxt
       val vars = map (apsnd (Term_Subst.instantiateT instT)) 
-        (rev (subtract op= exclude (fold Term.add_vars ts [])));
-      val (xs, ctxt'') = Variable.variant_fixes (map (#1 o #1) vars) ctxt';
-      val inst = vars ~~ map Free (xs ~~ map #2 vars);
+        (rev (subtract op= exclude (fold Term.add_vars ts [])))
+      val (xs, ctxt'') = Variable.variant_fixes (map (#1 o #1) vars) ctxt'
+      val inst = vars ~~ map Free (xs ~~ map #2 vars)
     in ((instT, inst), ctxt'') end
   
   fun import_terms_exclude exclude ts ctxt =
@@ -328,16 +370,16 @@
       val orig_lthy = lthy
       (* it doesn't raise an exception because it would have already raised it in define_pcrel *)
       val (quot_thm, _, lthy) = Lifting_Term.prove_param_quot_thm lthy rty
-      val parametrized_relator = singleton (Variable.export_terms lthy orig_lthy) (quot_thm_crel quot_thm);
+      val parametrized_relator = singleton (Variable.export_terms lthy orig_lthy) (quot_thm_crel quot_thm)
       val lthy = orig_lthy
       val id_transfer = 
          @{thm id_transfer}
         |> Thm.incr_indexes (Term.maxidx_of_term parametrized_relator + 1)
         |> Conv.fconv_rule(HOLogic.Trueprop_conv (Conv.arg_conv id_unfold then_conv Conv.arg1_conv id_unfold))
-      val var = Var (hd (Term.add_vars (prop_of id_transfer) []));
-      val thy = Proof_Context.theory_of lthy;
+      val var = Var (hd (Term.add_vars (prop_of id_transfer) []))
+      val thy = Proof_Context.theory_of lthy
       val inst = [(cterm_of thy var, cterm_of thy parametrized_relator)]
-      val id_par_thm = Drule.cterm_instantiate inst id_transfer;
+      val id_par_thm = Drule.cterm_instantiate inst id_transfer
     in
       Lifting_Def.generate_parametric_transfer_rule lthy id_transfer_rule id_par_thm
     end
@@ -362,7 +404,7 @@
       val ct = thm |> cprop_of |> Drule.strip_imp_concl |> Thm.dest_arg |> Thm.dest_arg1 |> Thm.dest_arg
       val pcrel_def = Thm.incr_indexes (#maxidx (Thm.rep_cterm ct) + 1) pcrel_def
       val thm = Thm.instantiate (Thm.match (ct, Thm.rhs_of pcrel_def)) thm
-        handle Pattern.MATCH => raise CTERM ("fold_Domainp_pcrel", [ct, Thm.rhs_of pcrel_def]);
+        handle Pattern.MATCH => raise CTERM ("fold_Domainp_pcrel", [ct, Thm.rhs_of pcrel_def])
     in
       rewrite_first_Domainp_arg (Thm.symmetric pcrel_def) thm
     end
@@ -734,4 +776,243 @@
       -- Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse_Spec.xthm) >> 
         (fn (((gen_code, xthm), opt_reflp_xthm), opt_par_xthm) => 
           setup_lifting_cmd gen_code xthm opt_reflp_xthm opt_par_xthm))
-end;
+
+(* restoring lifting infrastructure *)
+
+local
+  exception PCR_ERROR of Pretty.T list
+in
+
+fun lifting_restore_sanity_check ctxt (qinfo:Lifting_Info.quotient) =
+  let
+    val quot_thm = (#quot_thm qinfo)
+    val _ = quot_thm_sanity_check ctxt quot_thm
+    val pcr_info_err =
+      (case #pcr_info qinfo of
+        SOME pcr => 
+          let
+            val pcrel_def = #pcrel_def pcr
+            val pcr_cr_eq = #pcr_cr_eq pcr
+            val (def_lhs, _) = Logic.dest_equals (prop_of pcrel_def)
+              handle TERM _ => raise PCR_ERROR [Pretty.block 
+                    [Pretty.str "The pcr definiton theorem is not a plain meta equation:",
+                    Pretty.brk 1,
+                    Display.pretty_thm ctxt pcrel_def]]
+            val pcr_const_def = head_of def_lhs
+            val (eq_lhs, eq_rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of pcr_cr_eq))
+              handle TERM _ => raise PCR_ERROR [Pretty.block 
+                    [Pretty.str "The pcr_cr equation theorem is not a plain equation:",
+                    Pretty.brk 1,
+                    Display.pretty_thm ctxt pcr_cr_eq]]
+            val (pcr_const_eq, eqs) = strip_comb eq_lhs
+            fun is_eq (Const ("HOL.eq", _)) = true
+              | is_eq _ = false
+            fun eq_Const (Const (name1, _)) (Const (name2, _)) = (name1 = name2)
+              | eq_Const _ _ = false
+            val all_eqs = if not (forall is_eq eqs) then 
+              [Pretty.block
+                    [Pretty.str "Arguments of the lhs of the pcr_cr equation theorem are not only equalities:",
+                    Pretty.brk 1,
+                    Display.pretty_thm ctxt pcr_cr_eq]]
+              else []
+            val pcr_consts_not_equal = if not (eq_Const pcr_const_def pcr_const_eq) then
+              [Pretty.block
+                    [Pretty.str "Parametrized correspondence relation constants in pcr_def and pcr_cr_eq are not equal:",
+                    Pretty.brk 1,
+                    Syntax.pretty_term ctxt pcr_const_def,
+                    Pretty.brk 1,
+                    Pretty.str "vs.",
+                    Pretty.brk 1,
+                    Syntax.pretty_term ctxt pcr_const_eq]]
+              else []
+            val crel = quot_thm_crel quot_thm
+            val cr_consts_not_equal = if not (eq_Const crel eq_rhs) then
+              [Pretty.block
+                    [Pretty.str "Correspondence relation constants in the Quotient theorem and pcr_cr_eq are not equal:",
+                    Pretty.brk 1,
+                    Syntax.pretty_term ctxt crel,
+                    Pretty.brk 1,
+                    Pretty.str "vs.",
+                    Pretty.brk 1,
+                    Syntax.pretty_term ctxt eq_rhs]]
+              else []
+          in
+            all_eqs @ pcr_consts_not_equal @ cr_consts_not_equal
+          end
+        | NONE => [])
+    val errs = pcr_info_err
+  in
+    if null errs then () else raise PCR_ERROR errs
+  end
+  handle PCR_ERROR errs => error (cat_lines (["Sanity check failed:"] 
+                                            @ (map (Pretty.string_of o Pretty.item o single) errs)))
+end
+
+fun lifting_restore qinfo ctxt =
+  let
+    val _ = lifting_restore_sanity_check (Context.proof_of ctxt) qinfo
+    val (_, qty) = quot_thm_rty_qty (#quot_thm qinfo)
+    val qty_full_name = (fst o dest_Type) qty
+    val stored_qinfo = Lifting_Info.lookup_quotients (Context.proof_of ctxt) qty_full_name
+  in
+    if is_some (stored_qinfo) andalso not (Lifting_Info.quotient_eq (qinfo, (the stored_qinfo)))
+      then error (Pretty.string_of 
+        (Pretty.block
+          [Pretty.str "Lifting is already setup for the type",
+           Pretty.brk 1,
+           Pretty.quote (Syntax.pretty_typ (Context.proof_of ctxt) qty)]))
+      else Lifting_Info.update_quotients qty_full_name qinfo ctxt
+  end
+
+val parse_opt_pcr =
+  Scan.optional (Attrib.thm -- Attrib.thm >> 
+    (fn (pcrel_def, pcr_cr_eq) => SOME {pcrel_def = pcrel_def, pcr_cr_eq = pcr_cr_eq})) NONE
+
+val lifting_restore_attribute_setup =
+  Attrib.setup @{binding lifting_restore}
+    ((Attrib.thm -- parse_opt_pcr) >>
+      (fn (quot_thm, opt_pcr) =>
+        let val qinfo = { quot_thm = quot_thm, pcr_info = opt_pcr}
+        in Thm.declaration_attribute (K (lifting_restore qinfo)) end))
+    "restoring lifting infrastructure"
+
+val _ = Theory.setup lifting_restore_attribute_setup 
+
+fun lifting_restore_internal bundle_name ctxt = 
+  let 
+    val restore_info = Lifting_Info.lookup_restore_data (Context.proof_of ctxt) bundle_name
+  in
+    case restore_info of
+      SOME restore_info =>
+        ctxt 
+        |> lifting_restore (#quotient restore_info)
+        |> fold_rev Transfer.transfer_raw_add (Item_Net.content (#transfer_rules restore_info))
+      | NONE => ctxt
+  end
+
+val lifting_restore_internal_attribute_setup =
+  Attrib.setup @{binding lifting_restore_internal}
+     (Scan.lift Args.name >> (fn name => Thm.declaration_attribute (K (lifting_restore_internal name))))
+    "restoring lifting infrastructure; internal attribute; not meant to be used directly by regular users"
+
+val _ = Theory.setup lifting_restore_internal_attribute_setup 
+
+(* lifting_forget *)
+
+val monotonicity_names = [@{const_name right_unique}, @{const_name left_unique}, @{const_name right_total},
+  @{const_name left_total}, @{const_name bi_unique}, @{const_name bi_total}]
+
+fun fold_transfer_rel f (Const (@{const_name "Transfer.Rel"}, _) $ rel $ _ $ _) = f rel
+  | fold_transfer_rel f (Const (@{const_name "HOL.eq"}, _) $ 
+    (Const (@{const_name Domainp}, _) $ rel) $ _) = f rel
+  | fold_transfer_rel f (Const (name, _) $ rel) = 
+    if member op= monotonicity_names name then f rel else f @{term undefined}
+  | fold_transfer_rel f _ = f @{term undefined}
+
+fun filter_transfer_rules_by_rel transfer_rel transfer_rules =
+  let
+    val transfer_rel_name = transfer_rel |> dest_Const |> fst;
+    fun has_transfer_rel thm = 
+      let
+        val concl = thm |> concl_of |> HOLogic.dest_Trueprop
+      in
+        member op= (fold_transfer_rel (fn tm => Term.add_const_names tm []) concl) transfer_rel_name
+      end
+      handle TERM _ => false
+  in
+    filter has_transfer_rel transfer_rules
+  end
+
+type restore_data = {quotient : Lifting_Info.quotient, transfer_rules: thm Item_Net.T}
+
+fun get_transfer_rel qinfo =
+  let
+    fun get_pcrel pcr_def = pcr_def |> concl_of |> Logic.dest_equals |> fst |> head_of
+  in
+    if is_some (#pcr_info qinfo) 
+      then get_pcrel (#pcrel_def (the (#pcr_info qinfo)))
+      else quot_thm_crel (#quot_thm qinfo)
+  end
+
+fun pointer_of_bundle_name bundle_name ctxt =
+  let
+    val bundle_name = Bundle.check ctxt bundle_name
+    val bundle = Bundle.the_bundle ctxt bundle_name
+  in
+    case bundle of
+      [(_, [arg_src])] => 
+        (let
+          val ((_, tokens), _) = Args.dest_src arg_src
+        in
+          (fst (Args.name tokens))
+          handle _ => error "The provided bundle is not a lifting bundle."
+        end)
+      | _ => error "The provided bundle is not a lifting bundle."
+  end
+
+fun lifting_forget pointer lthy =
+  let
+    fun get_transfer_rules_to_delete qinfo ctxt =
+      let
+        fun get_pcrel pcr_def = pcr_def |> concl_of |> Logic.dest_equals |> fst |> head_of
+        val transfer_rel = if is_some (#pcr_info qinfo) 
+          then get_pcrel (#pcrel_def (the (#pcr_info qinfo)))
+          else quot_thm_crel (#quot_thm qinfo)
+      in
+         filter_transfer_rules_by_rel transfer_rel (Transfer.get_transfer_raw ctxt)
+      end
+  in
+    case Lifting_Info.lookup_restore_data lthy pointer of
+      SOME restore_info =>
+        let
+          val qinfo = #quotient restore_info
+          val quot_thm = #quot_thm qinfo
+          val transfer_rules = get_transfer_rules_to_delete qinfo lthy
+        in
+          Local_Theory.declaration {syntax = false, pervasive = true}
+            (K (fold (Transfer.transfer_raw_del) transfer_rules #> Lifting_Info.delete_quotients quot_thm))
+            lthy
+        end
+      | NONE => error "The lifting bundle refers to non-existent restore data."
+    end
+    
+
+fun lifting_forget_cmd bundle_name lthy = 
+  lifting_forget (pointer_of_bundle_name bundle_name lthy) lthy
+
+
+val _ =
+  Outer_Syntax.local_theory @{command_spec "lifting_forget"} 
+    "unsetup Lifting and Transfer for the given lifting bundle"
+    (Parse.position Parse.xname >> (lifting_forget_cmd))
+
+(* lifting_update *)
+
+fun update_transfer_rules pointer lthy =
+  let
+    fun new_transfer_rules { quotient = qinfo, ... } lthy =
+      let
+        val transfer_rel = get_transfer_rel qinfo
+        val transfer_rules = filter_transfer_rules_by_rel transfer_rel (Transfer.get_transfer_raw lthy)
+      in
+        fn phi => fold_rev 
+          (Item_Net.update o Morphism.thm phi) transfer_rules Thm.full_rules
+      end
+  in
+    case Lifting_Info.lookup_restore_data lthy pointer of
+      SOME refresh_data => 
+        Local_Theory.declaration {syntax = false, pervasive = true}
+          (fn phi => Lifting_Info.add_transfer_rules_in_restore_data pointer 
+            (new_transfer_rules refresh_data lthy phi)) lthy
+      | NONE => error "The lifting bundle refers to non-existent restore data."
+  end
+
+fun lifting_update_cmd bundle_name lthy = 
+  update_transfer_rules (pointer_of_bundle_name bundle_name lthy) lthy
+
+val _ =
+  Outer_Syntax.local_theory @{command_spec "lifting_update"}
+    "add newly introduced transfer rules to a bundle storing the state of Lifting and Transfer"
+    (Parse.position Parse.xname >> lifting_update_cmd)
+
+end
diff -r 71a0a8687d6c -r ee90c67502c9 src/HOL/Tools/Lifting/lifting_term.ML
--- a/src/HOL/Tools/Lifting/lifting_term.ML	Mon Sep 16 11:54:57 2013 +0200
+++ b/src/HOL/Tools/Lifting/lifting_term.ML	Mon Sep 16 15:30:17 2013 +0200
@@ -523,4 +523,4 @@
       Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.fun2_conv parametrize_relation_conv)) thm
     end
 
-end;
+end
diff -r 71a0a8687d6c -r ee90c67502c9 src/HOL/Tools/Lifting/lifting_util.ML
--- a/src/HOL/Tools/Lifting/lifting_util.ML	Mon Sep 16 11:54:57 2013 +0200
+++ b/src/HOL/Tools/Lifting/lifting_util.ML	Mon Sep 16 15:30:17 2013 +0200
@@ -28,7 +28,7 @@
   val relation_types: typ -> typ * typ
   val mk_HOL_eq: thm -> thm
   val safe_HOL_meta_eq: thm -> thm
-end;
+end
 
 
 structure Lifting_Util: LIFTING_UTIL =
@@ -110,4 +110,4 @@
 
 fun safe_HOL_meta_eq r = mk_HOL_eq r handle Thm.THM _ => r
 
-end;
+end