restoring Transfer/Lifting context
authorkuncar
Mon Sep 16 15:30:17 2013 +0200 (2013-09-16)
changeset 53651ee90c67502c9
parent 53650 71a0a8687d6c
child 53652 18fbca265e2e
restoring Transfer/Lifting context
etc/isar-keywords.el
src/HOL/Lifting.thy
src/HOL/Tools/Lifting/lifting_def.ML
src/HOL/Tools/Lifting/lifting_info.ML
src/HOL/Tools/Lifting/lifting_setup.ML
src/HOL/Tools/Lifting/lifting_term.ML
src/HOL/Tools/Lifting/lifting_util.ML
     1.1 --- a/etc/isar-keywords.el	Mon Sep 16 11:54:57 2013 +0200
     1.2 +++ b/etc/isar-keywords.el	Mon Sep 16 15:30:17 2013 +0200
     1.3 @@ -135,6 +135,8 @@
     1.4      "lemmas"
     1.5      "let"
     1.6      "lift_definition"
     1.7 +    "lifting_forget"
     1.8 +    "lifting_update"
     1.9      "linear_undo"
    1.10      "local_setup"
    1.11      "locale"
    1.12 @@ -539,6 +541,8 @@
    1.13      "instantiation"
    1.14      "judgment"
    1.15      "lemmas"
    1.16 +    "lifting_forget"
    1.17 +    "lifting_update"
    1.18      "local_setup"
    1.19      "locale"
    1.20      "method_setup"
     2.1 --- a/src/HOL/Lifting.thy	Mon Sep 16 11:54:57 2013 +0200
     2.2 +++ b/src/HOL/Lifting.thy	Mon Sep 16 15:30:17 2013 +0200
     2.3 @@ -11,7 +11,7 @@
     2.4    "parametric" and
     2.5    "print_quot_maps" "print_quotients" :: diag and
     2.6    "lift_definition" :: thy_goal and
     2.7 -  "setup_lifting" :: thy_decl
     2.8 +  "setup_lifting" "lifting_forget" "lifting_update" :: thy_decl
     2.9  begin
    2.10  
    2.11  subsection {* Function map *}
     3.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Mon Sep 16 11:54:57 2013 +0200
     3.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Mon Sep 16 15:30:17 2013 +0200
     3.3 @@ -16,7 +16,7 @@
     3.4      (binding * string option * mixfix) * string * (Facts.ref * Args.src list) option -> local_theory -> Proof.state
     3.5  
     3.6    val can_generate_code_cert: thm -> bool
     3.7 -end;
     3.8 +end
     3.9  
    3.10  structure Lifting_Def: LIFTING_DEF =
    3.11  struct
    3.12 @@ -583,4 +583,4 @@
    3.13        (liftdef_parser >> lift_def_cmd_with_err_handling)
    3.14  
    3.15  
    3.16 -end; (* structure *)
    3.17 +end (* structure *)
     4.1 --- a/src/HOL/Tools/Lifting/lifting_info.ML	Mon Sep 16 11:54:57 2013 +0200
     4.2 +++ b/src/HOL/Tools/Lifting/lifting_info.ML	Mon Sep 16 15:30:17 2013 +0200
     4.3 @@ -12,12 +12,19 @@
     4.4    
     4.5    type pcr = {pcrel_def: thm, pcr_cr_eq: thm}
     4.6    type quotient = {quot_thm: thm, pcr_info: pcr option}
     4.7 +  val pcr_eq: pcr * pcr -> bool
     4.8 +  val quotient_eq: quotient * quotient -> bool
     4.9    val transform_quotient: morphism -> quotient -> quotient
    4.10    val lookup_quotients: Proof.context -> string -> quotient option
    4.11    val update_quotients: string -> quotient -> Context.generic -> Context.generic
    4.12    val delete_quotients: thm -> Context.generic -> Context.generic
    4.13    val print_quotients: Proof.context -> unit
    4.14  
    4.15 +  type restore_data = {quotient : quotient, transfer_rules: thm Item_Net.T}
    4.16 +  val lookup_restore_data: Proof.context -> string -> restore_data option
    4.17 +  val init_restore_data: string -> quotient -> Context.generic -> Context.generic
    4.18 +  val add_transfer_rules_in_restore_data: string -> thm Item_Net.T -> Context.generic -> Context.generic  
    4.19 +
    4.20    val get_invariant_commute_rules: Proof.context -> thm list
    4.21    
    4.22    val get_reflexivity_rules: Proof.context -> thm list
    4.23 @@ -31,9 +38,10 @@
    4.24    val get_quot_maps           : Proof.context -> quot_map Symtab.table
    4.25    val get_quotients           : Proof.context -> quotient Symtab.table
    4.26    val get_relator_distr_data  : Proof.context -> relator_distr_data Symtab.table
    4.27 +  val get_restore_data        : Proof.context -> restore_data Symtab.table
    4.28  
    4.29    val setup: theory -> theory
    4.30 -end;
    4.31 +end
    4.32  
    4.33  structure Lifting_Info: LIFTING_INFO =
    4.34  struct
    4.35 @@ -47,6 +55,7 @@
    4.36  type quotient = {quot_thm: thm, pcr_info: pcr option}
    4.37  type relator_distr_data = {pos_mono_rule: thm, neg_mono_rule: thm, 
    4.38    pos_distr_rules: thm list, neg_distr_rules: thm list}
    4.39 +type restore_data = {quotient : quotient, transfer_rules: thm Item_Net.T}
    4.40  
    4.41  structure Data = Generic_Data
    4.42  (
    4.43 @@ -54,44 +63,53 @@
    4.44      { quot_maps : quot_map Symtab.table,
    4.45        quotients : quotient Symtab.table,
    4.46        reflexivity_rules : thm Item_Net.T,
    4.47 -      relator_distr_data : relator_distr_data Symtab.table
    4.48 +      relator_distr_data : relator_distr_data Symtab.table,
    4.49 +      restore_data : restore_data Symtab.table
    4.50      }
    4.51    val empty =
    4.52      { quot_maps = Symtab.empty,
    4.53        quotients = Symtab.empty,
    4.54        reflexivity_rules = Thm.full_rules,
    4.55 -      relator_distr_data = Symtab.empty
    4.56 +      relator_distr_data = Symtab.empty,
    4.57 +      restore_data = Symtab.empty
    4.58      }
    4.59    val extend = I
    4.60    fun merge
    4.61 -    ( { quot_maps = qm1, quotients = q1, reflexivity_rules = rr1, relator_distr_data = rdd1 },
    4.62 -      { quot_maps = qm2, quotients = q2, reflexivity_rules = rr2, relator_distr_data = rdd2 } ) =
    4.63 +    ( { quot_maps = qm1, quotients = q1, reflexivity_rules = rr1, relator_distr_data = rdd1, 
    4.64 +        restore_data = rd1 },
    4.65 +      { quot_maps = qm2, quotients = q2, reflexivity_rules = rr2, relator_distr_data = rdd2,
    4.66 +        restore_data = rd2 } ) =
    4.67      { quot_maps = Symtab.merge (K true) (qm1, qm2),
    4.68        quotients = Symtab.merge (K true) (q1, q2),
    4.69        reflexivity_rules = Item_Net.merge (rr1, rr2),
    4.70 -      relator_distr_data = Symtab.merge (K true) (rdd1, rdd2) }
    4.71 +      relator_distr_data = Symtab.merge (K true) (rdd1, rdd2),
    4.72 +      restore_data = Symtab.merge (K true) (rd1, rd2) }
    4.73  )
    4.74  
    4.75 -fun map_data f1 f2 f3 f4
    4.76 -  { quot_maps, quotients, reflexivity_rules, relator_distr_data} =
    4.77 +fun map_data f1 f2 f3 f4 f5
    4.78 +  { quot_maps, quotients, reflexivity_rules, relator_distr_data, restore_data } =
    4.79    { quot_maps = f1 quot_maps,
    4.80      quotients = f2 quotients,
    4.81      reflexivity_rules = f3 reflexivity_rules,
    4.82 -    relator_distr_data = f4 relator_distr_data }
    4.83 +    relator_distr_data = f4 relator_distr_data,
    4.84 +    restore_data = f5 restore_data }
    4.85  
    4.86 -fun map_quot_maps           f = map_data f I I I
    4.87 -fun map_quotients           f = map_data I f I I
    4.88 -fun map_reflexivity_rules   f = map_data I I f I
    4.89 -fun map_relator_distr_data  f = map_data I I I f
    4.90 +fun map_quot_maps           f = map_data f I I I I
    4.91 +fun map_quotients           f = map_data I f I I I
    4.92 +fun map_reflexivity_rules   f = map_data I I f I I
    4.93 +fun map_relator_distr_data  f = map_data I I I f I
    4.94 +fun map_restore_data        f = map_data I I I I f
    4.95    
    4.96  val get_quot_maps'           = #quot_maps o Data.get
    4.97  val get_quotients'           = #quotients o Data.get
    4.98  val get_reflexivity_rules'   = #reflexivity_rules o Data.get
    4.99  val get_relator_distr_data'  = #relator_distr_data o Data.get
   4.100 +val get_restore_data'        = #restore_data o Data.get
   4.101  
   4.102  fun get_quot_maps          ctxt = get_quot_maps' (Context.Proof ctxt)
   4.103  fun get_quotients          ctxt = get_quotients' (Context.Proof ctxt)
   4.104  fun get_relator_distr_data ctxt = get_relator_distr_data' (Context.Proof ctxt)
   4.105 +fun get_restore_data       ctxt = get_restore_data' (Context.Proof ctxt)
   4.106  
   4.107  (* info about Quotient map theorems *)
   4.108  
   4.109 @@ -164,6 +182,20 @@
   4.110    end
   4.111  
   4.112  (* info about quotient types *)
   4.113 +
   4.114 +fun pcr_eq ({pcrel_def = pcrel_def1, pcr_cr_eq = pcr_cr_eq1},
   4.115 +           {pcrel_def = pcrel_def2, pcr_cr_eq = pcr_cr_eq2}) = 
   4.116 +           Thm.eq_thm (pcrel_def1, pcrel_def2) andalso Thm.eq_thm (pcr_cr_eq1, pcr_cr_eq2)
   4.117 +
   4.118 +fun option_eq _ (NONE,NONE) = true
   4.119 +  | option_eq _ (NONE,_) = false
   4.120 +  | option_eq _ (_,NONE) = false
   4.121 +  | option_eq cmp (SOME x, SOME y) = cmp (x,y);
   4.122 +
   4.123 +fun quotient_eq ({quot_thm = quot_thm1, pcr_info = pcr_info1},
   4.124 +                {quot_thm = quot_thm2, pcr_info = pcr_info2}) =
   4.125 +                Thm.eq_thm (quot_thm1, quot_thm2) andalso option_eq pcr_eq (pcr_info1, pcr_info2)
   4.126 +
   4.127  fun transform_pcr_info phi {pcrel_def, pcr_cr_eq} =
   4.128    {pcrel_def = Morphism.thm phi pcrel_def, pcr_cr_eq = Morphism.thm phi pcr_cr_eq}
   4.129  
   4.130 @@ -209,6 +241,22 @@
   4.131    Attrib.setup @{binding quot_del} (Scan.succeed (Thm.declaration_attribute delete_quotients))
   4.132      "deletes the Quotient theorem"
   4.133  
   4.134 +(* data for restoring Transfer/Lifting context *)
   4.135 +
   4.136 +fun lookup_restore_data ctxt bundle_name = Symtab.lookup (get_restore_data ctxt) bundle_name
   4.137 +
   4.138 +fun update_restore_data bundle_name restore_data ctxt = 
   4.139 +  Data.map (map_restore_data (Symtab.update (bundle_name, restore_data))) ctxt
   4.140 +
   4.141 +fun init_restore_data bundle_name qinfo ctxt = 
   4.142 +  update_restore_data bundle_name { quotient = qinfo, transfer_rules = Thm.full_rules } ctxt
   4.143 +
   4.144 +fun add_transfer_rules_in_restore_data bundle_name transfer_rules ctxt =
   4.145 +  case Symtab.lookup (get_restore_data' ctxt) bundle_name of
   4.146 +    SOME restore_data => update_restore_data bundle_name { quotient = #quotient restore_data, 
   4.147 +      transfer_rules = Item_Net.merge ((#transfer_rules restore_data), transfer_rules) } ctxt
   4.148 +    | NONE => error ("The restore data " ^ quote bundle_name ^ " is not defined.")
   4.149 +
   4.150  (* theorems that a relator of an invariant is an invariant of the corresponding predicate *)
   4.151  
   4.152  structure Invariant_Commute = Named_Thms
   4.153 @@ -469,4 +517,4 @@
   4.154    Outer_Syntax.improper_command @{command_spec "print_quotients"} "print quotients"
   4.155      (Scan.succeed (Toplevel.keep (print_quotients o Toplevel.context_of)))
   4.156  
   4.157 -end;
   4.158 +end
     5.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML	Mon Sep 16 11:54:57 2013 +0200
     5.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Mon Sep 16 15:30:17 2013 +0200
     5.3 @@ -11,7 +11,9 @@
     5.4    val setup_by_quotient: bool -> thm -> thm option -> thm option -> local_theory -> local_theory
     5.5  
     5.6    val setup_by_typedef_thm: bool -> thm -> local_theory -> local_theory
     5.7 -end;
     5.8 +
     5.9 +  val lifting_restore: Lifting_Info.quotient -> Context.generic -> Context.generic
    5.10 +end
    5.11  
    5.12  structure Lifting_Setup: LIFTING_SETUP =
    5.13  struct
    5.14 @@ -164,8 +166,24 @@
    5.15    else
    5.16      lthy
    5.17  
    5.18 +local
    5.19 +  exception QUOT_ERROR of Pretty.T list
    5.20 +in
    5.21  fun quot_thm_sanity_check ctxt quot_thm =
    5.22    let
    5.23 +    val _ = 
    5.24 +      if (nprems_of quot_thm > 0) then   
    5.25 +          raise QUOT_ERROR [Pretty.block
    5.26 +            [Pretty.str "The Quotient theorem has extra assumptions:",
    5.27 +             Pretty.brk 1,
    5.28 +             Display.pretty_thm ctxt quot_thm]]
    5.29 +      else ()
    5.30 +    val _ = quot_thm |> concl_of |> HOLogic.dest_Trueprop |> dest_Quotient
    5.31 +    handle TERM _ => raise QUOT_ERROR
    5.32 +          [Pretty.block
    5.33 +            [Pretty.str "The Quotient theorem is not of the right form:",
    5.34 +             Pretty.brk 1,
    5.35 +             Display.pretty_thm ctxt quot_thm]]
    5.36      val ((_, [quot_thm_fixed]), ctxt') = Variable.importT [quot_thm] ctxt 
    5.37      val (rty, qty) = quot_thm_rty_qty quot_thm_fixed
    5.38      val rty_tfreesT = Term.add_tfree_namesT rty []
    5.39 @@ -186,8 +204,31 @@
    5.40                                  Pretty.str "is not a type constructor."]]
    5.41      val errs = extra_rty_tfrees @ not_type_constr
    5.42    in
    5.43 -    if null errs then () else error (cat_lines (["Sanity check of the quotient theorem failed:",""] 
    5.44 -                                                @ (map Pretty.string_of errs)))
    5.45 +    if null errs then () else raise QUOT_ERROR errs
    5.46 +  end
    5.47 +  handle QUOT_ERROR errs => error (cat_lines (["Sanity check of the quotient theorem failed:"] 
    5.48 +                                            @ (map (Pretty.string_of o Pretty.item o single) errs)))
    5.49 +end
    5.50 +
    5.51 +fun lifting_bundle qty_full_name qinfo lthy = 
    5.52 +  let
    5.53 +    fun qualify suffix defname = Binding.qualified true suffix defname
    5.54 +    val binding =  qty_full_name |> Long_Name.base_name |> Binding.name |> qualify "lifting"
    5.55 +    val morphed_binding = Morphism.binding (Local_Theory.target_morphism lthy) binding
    5.56 +    val bundle_name = Name_Space.full_name (Name_Space.naming_of 
    5.57 +      (Context.Theory (Proof_Context.theory_of lthy))) morphed_binding
    5.58 +    fun phi_qinfo phi = Lifting_Info.transform_quotient phi qinfo
    5.59 +
    5.60 +    val thy = Proof_Context.theory_of lthy
    5.61 +    val dummy_thm = Thm.transfer thy Drule.dummy_thm
    5.62 +    val pointer = Outer_Syntax.scan Position.none bundle_name
    5.63 +    val restore_lifting_att = 
    5.64 +      ([dummy_thm], [Args.src (("Lifting.lifting_restore_internal", pointer), Position.none)])
    5.65 +  in
    5.66 +    lthy 
    5.67 +      |> Local_Theory.declaration {syntax = false, pervasive = true}
    5.68 +           (fn phi => Lifting_Info.init_restore_data bundle_name (phi_qinfo phi))
    5.69 +      |> Bundle.bundle ((binding, [restore_lifting_att])) []
    5.70    end
    5.71  
    5.72  fun setup_lifting_infr gen_code quot_thm opt_reflp_thm lthy =
    5.73 @@ -221,23 +262,24 @@
    5.74      lthy
    5.75        |> Local_Theory.declaration {syntax = false, pervasive = true}
    5.76          (fn phi => Lifting_Info.update_quotients qty_full_name (quot_info phi))
    5.77 +      |> lifting_bundle qty_full_name quotients
    5.78    end
    5.79  
    5.80  local
    5.81    fun importT_inst_exclude exclude ts ctxt =
    5.82      let
    5.83 -      val tvars = rev (subtract op= exclude (fold Term.add_tvars ts []));
    5.84 -      val (tfrees, ctxt') = Variable.invent_types (map #2 tvars) ctxt;
    5.85 +      val tvars = rev (subtract op= exclude (fold Term.add_tvars ts []))
    5.86 +      val (tfrees, ctxt') = Variable.invent_types (map #2 tvars) ctxt
    5.87      in (tvars ~~ map TFree tfrees, ctxt') end
    5.88    
    5.89    fun import_inst_exclude exclude ts ctxt =
    5.90      let
    5.91        val excludeT = fold (Term.add_tvarsT o snd) exclude []
    5.92 -      val (instT, ctxt') = importT_inst_exclude excludeT ts ctxt;
    5.93 +      val (instT, ctxt') = importT_inst_exclude excludeT ts ctxt
    5.94        val vars = map (apsnd (Term_Subst.instantiateT instT)) 
    5.95 -        (rev (subtract op= exclude (fold Term.add_vars ts [])));
    5.96 -      val (xs, ctxt'') = Variable.variant_fixes (map (#1 o #1) vars) ctxt';
    5.97 -      val inst = vars ~~ map Free (xs ~~ map #2 vars);
    5.98 +        (rev (subtract op= exclude (fold Term.add_vars ts [])))
    5.99 +      val (xs, ctxt'') = Variable.variant_fixes (map (#1 o #1) vars) ctxt'
   5.100 +      val inst = vars ~~ map Free (xs ~~ map #2 vars)
   5.101      in ((instT, inst), ctxt'') end
   5.102    
   5.103    fun import_terms_exclude exclude ts ctxt =
   5.104 @@ -328,16 +370,16 @@
   5.105        val orig_lthy = lthy
   5.106        (* it doesn't raise an exception because it would have already raised it in define_pcrel *)
   5.107        val (quot_thm, _, lthy) = Lifting_Term.prove_param_quot_thm lthy rty
   5.108 -      val parametrized_relator = singleton (Variable.export_terms lthy orig_lthy) (quot_thm_crel quot_thm);
   5.109 +      val parametrized_relator = singleton (Variable.export_terms lthy orig_lthy) (quot_thm_crel quot_thm)
   5.110        val lthy = orig_lthy
   5.111        val id_transfer = 
   5.112           @{thm id_transfer}
   5.113          |> Thm.incr_indexes (Term.maxidx_of_term parametrized_relator + 1)
   5.114          |> Conv.fconv_rule(HOLogic.Trueprop_conv (Conv.arg_conv id_unfold then_conv Conv.arg1_conv id_unfold))
   5.115 -      val var = Var (hd (Term.add_vars (prop_of id_transfer) []));
   5.116 -      val thy = Proof_Context.theory_of lthy;
   5.117 +      val var = Var (hd (Term.add_vars (prop_of id_transfer) []))
   5.118 +      val thy = Proof_Context.theory_of lthy
   5.119        val inst = [(cterm_of thy var, cterm_of thy parametrized_relator)]
   5.120 -      val id_par_thm = Drule.cterm_instantiate inst id_transfer;
   5.121 +      val id_par_thm = Drule.cterm_instantiate inst id_transfer
   5.122      in
   5.123        Lifting_Def.generate_parametric_transfer_rule lthy id_transfer_rule id_par_thm
   5.124      end
   5.125 @@ -362,7 +404,7 @@
   5.126        val ct = thm |> cprop_of |> Drule.strip_imp_concl |> Thm.dest_arg |> Thm.dest_arg1 |> Thm.dest_arg
   5.127        val pcrel_def = Thm.incr_indexes (#maxidx (Thm.rep_cterm ct) + 1) pcrel_def
   5.128        val thm = Thm.instantiate (Thm.match (ct, Thm.rhs_of pcrel_def)) thm
   5.129 -        handle Pattern.MATCH => raise CTERM ("fold_Domainp_pcrel", [ct, Thm.rhs_of pcrel_def]);
   5.130 +        handle Pattern.MATCH => raise CTERM ("fold_Domainp_pcrel", [ct, Thm.rhs_of pcrel_def])
   5.131      in
   5.132        rewrite_first_Domainp_arg (Thm.symmetric pcrel_def) thm
   5.133      end
   5.134 @@ -734,4 +776,243 @@
   5.135        -- Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse_Spec.xthm) >> 
   5.136          (fn (((gen_code, xthm), opt_reflp_xthm), opt_par_xthm) => 
   5.137            setup_lifting_cmd gen_code xthm opt_reflp_xthm opt_par_xthm))
   5.138 -end;
   5.139 +
   5.140 +(* restoring lifting infrastructure *)
   5.141 +
   5.142 +local
   5.143 +  exception PCR_ERROR of Pretty.T list
   5.144 +in
   5.145 +
   5.146 +fun lifting_restore_sanity_check ctxt (qinfo:Lifting_Info.quotient) =
   5.147 +  let
   5.148 +    val quot_thm = (#quot_thm qinfo)
   5.149 +    val _ = quot_thm_sanity_check ctxt quot_thm
   5.150 +    val pcr_info_err =
   5.151 +      (case #pcr_info qinfo of
   5.152 +        SOME pcr => 
   5.153 +          let
   5.154 +            val pcrel_def = #pcrel_def pcr
   5.155 +            val pcr_cr_eq = #pcr_cr_eq pcr
   5.156 +            val (def_lhs, _) = Logic.dest_equals (prop_of pcrel_def)
   5.157 +              handle TERM _ => raise PCR_ERROR [Pretty.block 
   5.158 +                    [Pretty.str "The pcr definiton theorem is not a plain meta equation:",
   5.159 +                    Pretty.brk 1,
   5.160 +                    Display.pretty_thm ctxt pcrel_def]]
   5.161 +            val pcr_const_def = head_of def_lhs
   5.162 +            val (eq_lhs, eq_rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of pcr_cr_eq))
   5.163 +              handle TERM _ => raise PCR_ERROR [Pretty.block 
   5.164 +                    [Pretty.str "The pcr_cr equation theorem is not a plain equation:",
   5.165 +                    Pretty.brk 1,
   5.166 +                    Display.pretty_thm ctxt pcr_cr_eq]]
   5.167 +            val (pcr_const_eq, eqs) = strip_comb eq_lhs
   5.168 +            fun is_eq (Const ("HOL.eq", _)) = true
   5.169 +              | is_eq _ = false
   5.170 +            fun eq_Const (Const (name1, _)) (Const (name2, _)) = (name1 = name2)
   5.171 +              | eq_Const _ _ = false
   5.172 +            val all_eqs = if not (forall is_eq eqs) then 
   5.173 +              [Pretty.block
   5.174 +                    [Pretty.str "Arguments of the lhs of the pcr_cr equation theorem are not only equalities:",
   5.175 +                    Pretty.brk 1,
   5.176 +                    Display.pretty_thm ctxt pcr_cr_eq]]
   5.177 +              else []
   5.178 +            val pcr_consts_not_equal = if not (eq_Const pcr_const_def pcr_const_eq) then
   5.179 +              [Pretty.block
   5.180 +                    [Pretty.str "Parametrized correspondence relation constants in pcr_def and pcr_cr_eq are not equal:",
   5.181 +                    Pretty.brk 1,
   5.182 +                    Syntax.pretty_term ctxt pcr_const_def,
   5.183 +                    Pretty.brk 1,
   5.184 +                    Pretty.str "vs.",
   5.185 +                    Pretty.brk 1,
   5.186 +                    Syntax.pretty_term ctxt pcr_const_eq]]
   5.187 +              else []
   5.188 +            val crel = quot_thm_crel quot_thm
   5.189 +            val cr_consts_not_equal = if not (eq_Const crel eq_rhs) then
   5.190 +              [Pretty.block
   5.191 +                    [Pretty.str "Correspondence relation constants in the Quotient theorem and pcr_cr_eq are not equal:",
   5.192 +                    Pretty.brk 1,
   5.193 +                    Syntax.pretty_term ctxt crel,
   5.194 +                    Pretty.brk 1,
   5.195 +                    Pretty.str "vs.",
   5.196 +                    Pretty.brk 1,
   5.197 +                    Syntax.pretty_term ctxt eq_rhs]]
   5.198 +              else []
   5.199 +          in
   5.200 +            all_eqs @ pcr_consts_not_equal @ cr_consts_not_equal
   5.201 +          end
   5.202 +        | NONE => [])
   5.203 +    val errs = pcr_info_err
   5.204 +  in
   5.205 +    if null errs then () else raise PCR_ERROR errs
   5.206 +  end
   5.207 +  handle PCR_ERROR errs => error (cat_lines (["Sanity check failed:"] 
   5.208 +                                            @ (map (Pretty.string_of o Pretty.item o single) errs)))
   5.209 +end
   5.210 +
   5.211 +fun lifting_restore qinfo ctxt =
   5.212 +  let
   5.213 +    val _ = lifting_restore_sanity_check (Context.proof_of ctxt) qinfo
   5.214 +    val (_, qty) = quot_thm_rty_qty (#quot_thm qinfo)
   5.215 +    val qty_full_name = (fst o dest_Type) qty
   5.216 +    val stored_qinfo = Lifting_Info.lookup_quotients (Context.proof_of ctxt) qty_full_name
   5.217 +  in
   5.218 +    if is_some (stored_qinfo) andalso not (Lifting_Info.quotient_eq (qinfo, (the stored_qinfo)))
   5.219 +      then error (Pretty.string_of 
   5.220 +        (Pretty.block
   5.221 +          [Pretty.str "Lifting is already setup for the type",
   5.222 +           Pretty.brk 1,
   5.223 +           Pretty.quote (Syntax.pretty_typ (Context.proof_of ctxt) qty)]))
   5.224 +      else Lifting_Info.update_quotients qty_full_name qinfo ctxt
   5.225 +  end
   5.226 +
   5.227 +val parse_opt_pcr =
   5.228 +  Scan.optional (Attrib.thm -- Attrib.thm >> 
   5.229 +    (fn (pcrel_def, pcr_cr_eq) => SOME {pcrel_def = pcrel_def, pcr_cr_eq = pcr_cr_eq})) NONE
   5.230 +
   5.231 +val lifting_restore_attribute_setup =
   5.232 +  Attrib.setup @{binding lifting_restore}
   5.233 +    ((Attrib.thm -- parse_opt_pcr) >>
   5.234 +      (fn (quot_thm, opt_pcr) =>
   5.235 +        let val qinfo = { quot_thm = quot_thm, pcr_info = opt_pcr}
   5.236 +        in Thm.declaration_attribute (K (lifting_restore qinfo)) end))
   5.237 +    "restoring lifting infrastructure"
   5.238 +
   5.239 +val _ = Theory.setup lifting_restore_attribute_setup 
   5.240 +
   5.241 +fun lifting_restore_internal bundle_name ctxt = 
   5.242 +  let 
   5.243 +    val restore_info = Lifting_Info.lookup_restore_data (Context.proof_of ctxt) bundle_name
   5.244 +  in
   5.245 +    case restore_info of
   5.246 +      SOME restore_info =>
   5.247 +        ctxt 
   5.248 +        |> lifting_restore (#quotient restore_info)
   5.249 +        |> fold_rev Transfer.transfer_raw_add (Item_Net.content (#transfer_rules restore_info))
   5.250 +      | NONE => ctxt
   5.251 +  end
   5.252 +
   5.253 +val lifting_restore_internal_attribute_setup =
   5.254 +  Attrib.setup @{binding lifting_restore_internal}
   5.255 +     (Scan.lift Args.name >> (fn name => Thm.declaration_attribute (K (lifting_restore_internal name))))
   5.256 +    "restoring lifting infrastructure; internal attribute; not meant to be used directly by regular users"
   5.257 +
   5.258 +val _ = Theory.setup lifting_restore_internal_attribute_setup 
   5.259 +
   5.260 +(* lifting_forget *)
   5.261 +
   5.262 +val monotonicity_names = [@{const_name right_unique}, @{const_name left_unique}, @{const_name right_total},
   5.263 +  @{const_name left_total}, @{const_name bi_unique}, @{const_name bi_total}]
   5.264 +
   5.265 +fun fold_transfer_rel f (Const (@{const_name "Transfer.Rel"}, _) $ rel $ _ $ _) = f rel
   5.266 +  | fold_transfer_rel f (Const (@{const_name "HOL.eq"}, _) $ 
   5.267 +    (Const (@{const_name Domainp}, _) $ rel) $ _) = f rel
   5.268 +  | fold_transfer_rel f (Const (name, _) $ rel) = 
   5.269 +    if member op= monotonicity_names name then f rel else f @{term undefined}
   5.270 +  | fold_transfer_rel f _ = f @{term undefined}
   5.271 +
   5.272 +fun filter_transfer_rules_by_rel transfer_rel transfer_rules =
   5.273 +  let
   5.274 +    val transfer_rel_name = transfer_rel |> dest_Const |> fst;
   5.275 +    fun has_transfer_rel thm = 
   5.276 +      let
   5.277 +        val concl = thm |> concl_of |> HOLogic.dest_Trueprop
   5.278 +      in
   5.279 +        member op= (fold_transfer_rel (fn tm => Term.add_const_names tm []) concl) transfer_rel_name
   5.280 +      end
   5.281 +      handle TERM _ => false
   5.282 +  in
   5.283 +    filter has_transfer_rel transfer_rules
   5.284 +  end
   5.285 +
   5.286 +type restore_data = {quotient : Lifting_Info.quotient, transfer_rules: thm Item_Net.T}
   5.287 +
   5.288 +fun get_transfer_rel qinfo =
   5.289 +  let
   5.290 +    fun get_pcrel pcr_def = pcr_def |> concl_of |> Logic.dest_equals |> fst |> head_of
   5.291 +  in
   5.292 +    if is_some (#pcr_info qinfo) 
   5.293 +      then get_pcrel (#pcrel_def (the (#pcr_info qinfo)))
   5.294 +      else quot_thm_crel (#quot_thm qinfo)
   5.295 +  end
   5.296 +
   5.297 +fun pointer_of_bundle_name bundle_name ctxt =
   5.298 +  let
   5.299 +    val bundle_name = Bundle.check ctxt bundle_name
   5.300 +    val bundle = Bundle.the_bundle ctxt bundle_name
   5.301 +  in
   5.302 +    case bundle of
   5.303 +      [(_, [arg_src])] => 
   5.304 +        (let
   5.305 +          val ((_, tokens), _) = Args.dest_src arg_src
   5.306 +        in
   5.307 +          (fst (Args.name tokens))
   5.308 +          handle _ => error "The provided bundle is not a lifting bundle."
   5.309 +        end)
   5.310 +      | _ => error "The provided bundle is not a lifting bundle."
   5.311 +  end
   5.312 +
   5.313 +fun lifting_forget pointer lthy =
   5.314 +  let
   5.315 +    fun get_transfer_rules_to_delete qinfo ctxt =
   5.316 +      let
   5.317 +        fun get_pcrel pcr_def = pcr_def |> concl_of |> Logic.dest_equals |> fst |> head_of
   5.318 +        val transfer_rel = if is_some (#pcr_info qinfo) 
   5.319 +          then get_pcrel (#pcrel_def (the (#pcr_info qinfo)))
   5.320 +          else quot_thm_crel (#quot_thm qinfo)
   5.321 +      in
   5.322 +         filter_transfer_rules_by_rel transfer_rel (Transfer.get_transfer_raw ctxt)
   5.323 +      end
   5.324 +  in
   5.325 +    case Lifting_Info.lookup_restore_data lthy pointer of
   5.326 +      SOME restore_info =>
   5.327 +        let
   5.328 +          val qinfo = #quotient restore_info
   5.329 +          val quot_thm = #quot_thm qinfo
   5.330 +          val transfer_rules = get_transfer_rules_to_delete qinfo lthy
   5.331 +        in
   5.332 +          Local_Theory.declaration {syntax = false, pervasive = true}
   5.333 +            (K (fold (Transfer.transfer_raw_del) transfer_rules #> Lifting_Info.delete_quotients quot_thm))
   5.334 +            lthy
   5.335 +        end
   5.336 +      | NONE => error "The lifting bundle refers to non-existent restore data."
   5.337 +    end
   5.338 +    
   5.339 +
   5.340 +fun lifting_forget_cmd bundle_name lthy = 
   5.341 +  lifting_forget (pointer_of_bundle_name bundle_name lthy) lthy
   5.342 +
   5.343 +
   5.344 +val _ =
   5.345 +  Outer_Syntax.local_theory @{command_spec "lifting_forget"} 
   5.346 +    "unsetup Lifting and Transfer for the given lifting bundle"
   5.347 +    (Parse.position Parse.xname >> (lifting_forget_cmd))
   5.348 +
   5.349 +(* lifting_update *)
   5.350 +
   5.351 +fun update_transfer_rules pointer lthy =
   5.352 +  let
   5.353 +    fun new_transfer_rules { quotient = qinfo, ... } lthy =
   5.354 +      let
   5.355 +        val transfer_rel = get_transfer_rel qinfo
   5.356 +        val transfer_rules = filter_transfer_rules_by_rel transfer_rel (Transfer.get_transfer_raw lthy)
   5.357 +      in
   5.358 +        fn phi => fold_rev 
   5.359 +          (Item_Net.update o Morphism.thm phi) transfer_rules Thm.full_rules
   5.360 +      end
   5.361 +  in
   5.362 +    case Lifting_Info.lookup_restore_data lthy pointer of
   5.363 +      SOME refresh_data => 
   5.364 +        Local_Theory.declaration {syntax = false, pervasive = true}
   5.365 +          (fn phi => Lifting_Info.add_transfer_rules_in_restore_data pointer 
   5.366 +            (new_transfer_rules refresh_data lthy phi)) lthy
   5.367 +      | NONE => error "The lifting bundle refers to non-existent restore data."
   5.368 +  end
   5.369 +
   5.370 +fun lifting_update_cmd bundle_name lthy = 
   5.371 +  update_transfer_rules (pointer_of_bundle_name bundle_name lthy) lthy
   5.372 +
   5.373 +val _ =
   5.374 +  Outer_Syntax.local_theory @{command_spec "lifting_update"}
   5.375 +    "add newly introduced transfer rules to a bundle storing the state of Lifting and Transfer"
   5.376 +    (Parse.position Parse.xname >> lifting_update_cmd)
   5.377 +
   5.378 +end
     6.1 --- a/src/HOL/Tools/Lifting/lifting_term.ML	Mon Sep 16 11:54:57 2013 +0200
     6.2 +++ b/src/HOL/Tools/Lifting/lifting_term.ML	Mon Sep 16 15:30:17 2013 +0200
     6.3 @@ -523,4 +523,4 @@
     6.4        Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.fun2_conv parametrize_relation_conv)) thm
     6.5      end
     6.6  
     6.7 -end;
     6.8 +end
     7.1 --- a/src/HOL/Tools/Lifting/lifting_util.ML	Mon Sep 16 11:54:57 2013 +0200
     7.2 +++ b/src/HOL/Tools/Lifting/lifting_util.ML	Mon Sep 16 15:30:17 2013 +0200
     7.3 @@ -28,7 +28,7 @@
     7.4    val relation_types: typ -> typ * typ
     7.5    val mk_HOL_eq: thm -> thm
     7.6    val safe_HOL_meta_eq: thm -> thm
     7.7 -end;
     7.8 +end
     7.9  
    7.10  
    7.11  structure Lifting_Util: LIFTING_UTIL =
    7.12 @@ -110,4 +110,4 @@
    7.13  
    7.14  fun safe_HOL_meta_eq r = mk_HOL_eq r handle Thm.THM _ => r
    7.15  
    7.16 -end;
    7.17 +end