src/HOL/Tools/Lifting/lifting_setup.ML
author wenzelm
Sun May 03 14:35:48 2015 +0200 (2015-05-03)
changeset 60239 755e11e2e15d
parent 60231 0daab758e087
child 60784 4f590c08fd5d
permissions -rw-r--r--
make SML/NJ more happy;
kuncar@47308
     1
(*  Title:      HOL/Tools/Lifting/lifting_setup.ML
kuncar@47308
     2
    Author:     Ondrej Kuncar
kuncar@47308
     3
huffman@47352
     4
Setting up the lifting infrastructure.
kuncar@47308
     5
*)
kuncar@47308
     6
kuncar@47308
     7
signature LIFTING_SETUP =
kuncar@47308
     8
sig
kuncar@47308
     9
  exception SETUP_LIFTING_INFR of string
kuncar@47308
    10
kuncar@60225
    11
  type config = { notes: bool };
kuncar@60225
    12
  val default_config: config;
kuncar@47308
    13
kuncar@60225
    14
  val setup_by_quotient: config -> thm -> thm option -> thm option -> local_theory -> 
kuncar@60225
    15
    binding * local_theory
kuncar@60225
    16
kuncar@60225
    17
  val setup_by_typedef_thm: config -> thm -> local_theory -> binding * local_theory
kuncar@53651
    18
kuncar@53651
    19
  val lifting_restore: Lifting_Info.quotient -> Context.generic -> Context.generic
kuncar@60226
    20
kuncar@60226
    21
  val lifting_forget: string -> local_theory -> local_theory
kuncar@60226
    22
  val update_transfer_rules: string -> local_theory -> local_theory
kuncar@60226
    23
  val pointer_of_bundle_binding: Proof.context -> binding -> string
kuncar@53651
    24
end
kuncar@47308
    25
huffman@47334
    26
structure Lifting_Setup: LIFTING_SETUP =
kuncar@47308
    27
struct
kuncar@47308
    28
kuncar@47698
    29
open Lifting_Util
kuncar@47308
    30
kuncar@47698
    31
infix 0 MRSL
kuncar@47308
    32
kuncar@47308
    33
exception SETUP_LIFTING_INFR of string
kuncar@47308
    34
kuncar@60225
    35
(* Config *)
kuncar@60225
    36
kuncar@60225
    37
type config = { notes: bool };
kuncar@60225
    38
val default_config = { notes = true };
kuncar@60225
    39
wenzelm@60239
    40
fun define_crel (config: config) rep_fun lthy =
kuncar@47308
    41
  let
kuncar@47361
    42
    val (qty, rty) = (dest_funT o fastype_of) rep_fun
kuncar@47361
    43
    val rep_fun_graph = (HOLogic.eq_const rty) $ Bound 1 $ (rep_fun $ Bound 0)
kuncar@51374
    44
    val def_term = Abs ("x", rty, Abs ("y", qty, rep_fun_graph))
kuncar@50175
    45
    val qty_name = (Binding.name o Long_Name.base_name o fst o dest_Type) qty
kuncar@50227
    46
    val crel_name = Binding.prefix_name "cr_" qty_name
kuncar@60225
    47
    val (fixed_def_term, lthy) = yield_singleton (Variable.importT_terms) def_term lthy
kuncar@60225
    48
    val ((_, (_ , def_thm)), lthy) = if #notes config then
kuncar@60225
    49
        Local_Theory.define ((crel_name, NoSyn), ((Thm.def_binding crel_name, []), fixed_def_term)) lthy
kuncar@60225
    50
      else 
kuncar@60225
    51
        Local_Theory.define ((Binding.concealed crel_name, NoSyn), ((Binding.empty, []), fixed_def_term)) lthy
kuncar@60225
    52
  in  
kuncar@60225
    53
    (def_thm, lthy)
kuncar@47308
    54
  end
kuncar@47308
    55
kuncar@50227
    56
fun print_define_pcrel_warning msg = 
kuncar@50227
    57
  let
kuncar@50227
    58
    val warning_msg = cat_lines 
kuncar@50227
    59
      ["Generation of a parametrized correspondence relation failed.",
kuncar@50227
    60
      (Pretty.string_of (Pretty.block
kuncar@50227
    61
         [Pretty.str "Reason:", Pretty.brk 2, msg]))]
kuncar@50227
    62
  in
kuncar@50227
    63
    warning warning_msg
kuncar@50227
    64
  end
kuncar@50227
    65
wenzelm@60239
    66
fun define_pcrel (config: config) crel lthy =
kuncar@50227
    67
  let
kuncar@50288
    68
    val (fixed_crel, lthy) = yield_singleton Variable.importT_terms crel lthy
kuncar@50288
    69
    val [rty', qty] = (binder_types o fastype_of) fixed_crel
kuncar@50288
    70
    val (param_rel, args) = Lifting_Term.generate_parametrized_relator lthy rty'
kuncar@50288
    71
    val rty_raw = (domain_type o range_type o fastype_of) param_rel
kuncar@50227
    72
    val thy = Proof_Context.theory_of lthy
kuncar@50227
    73
    val tyenv_match = Sign.typ_match thy (rty_raw, rty') Vartab.empty
kuncar@50288
    74
    val param_rel_subst = Envir.subst_term (tyenv_match,Vartab.empty) param_rel
kuncar@50288
    75
    val args_subst = map (Envir.subst_term (tyenv_match,Vartab.empty)) args
kuncar@50288
    76
    val lthy = Variable.declare_names fixed_crel lthy
kuncar@50288
    77
    val (instT, lthy) = Variable.importT_inst (param_rel_subst :: args_subst) lthy
kuncar@50288
    78
    val args_fixed = (map (Term_Subst.instantiate (instT, []))) args_subst
kuncar@50288
    79
    val param_rel_fixed = Term_Subst.instantiate (instT, []) param_rel_subst
kuncar@50288
    80
    val rty = (domain_type o fastype_of) param_rel_fixed
kuncar@50227
    81
    val relcomp_op = Const (@{const_name "relcompp"}, 
kuncar@50227
    82
          (rty --> rty' --> HOLogic.boolT) --> 
kuncar@50227
    83
          (rty' --> qty --> HOLogic.boolT) --> 
kuncar@50227
    84
          rty --> qty --> HOLogic.boolT)
kuncar@50227
    85
    val qty_name = (fst o dest_Type) qty
kuncar@50227
    86
    val pcrel_name = Binding.prefix_name "pcr_" ((Binding.name o Long_Name.base_name) qty_name)
kuncar@60225
    87
    val relator_type = foldr1 (op -->) ((map type_of args_fixed) @ [rty, qty, HOLogic.boolT])
kuncar@50288
    88
    val lhs = Library.foldl (op $) ((Free (Binding.name_of pcrel_name, relator_type)), args_fixed)
kuncar@51374
    89
    val rhs = relcomp_op $ param_rel_fixed $ fixed_crel
kuncar@50227
    90
    val definition_term = Logic.mk_equals (lhs, rhs)
kuncar@60225
    91
    fun note_def lthy =
kuncar@60225
    92
      Specification.definition ((SOME (pcrel_name, SOME relator_type, NoSyn)), 
kuncar@60225
    93
        ((Binding.empty, []), definition_term)) lthy |>> (snd #> snd);
kuncar@60225
    94
    fun raw_def lthy =
kuncar@60225
    95
      let
kuncar@60225
    96
        val ((_, rhs), prove) = Local_Defs.derived_def lthy true definition_term;
kuncar@60225
    97
        val ((_, (_, raw_th)), lthy) = lthy
kuncar@60225
    98
          |> Local_Theory.define ((Binding.concealed pcrel_name, NoSyn), ((Binding.empty, []), rhs));
kuncar@60225
    99
        val th = prove lthy raw_th;
kuncar@60225
   100
      in
kuncar@60225
   101
        (th, lthy)
kuncar@60225
   102
      end
kuncar@60225
   103
    val (def_thm, lthy) = if #notes config then note_def lthy else raw_def lthy
kuncar@50227
   104
  in
kuncar@50227
   105
    (SOME def_thm, lthy)
kuncar@50227
   106
  end
kuncar@50227
   107
  handle Lifting_Term.PARAM_QUOT_THM (_, msg) => (print_define_pcrel_warning msg; (NONE, lthy))
kuncar@50227
   108
kuncar@51374
   109
kuncar@51374
   110
local
kuncar@51374
   111
  val eq_OO_meta = mk_meta_eq @{thm eq_OO} 
kuncar@51374
   112
kuncar@51374
   113
  fun print_generate_pcr_cr_eq_error ctxt term = 
wenzelm@56257
   114
    let
wenzelm@56257
   115
      val goal = Const (@{const_name HOL.eq}, dummyT) $ term $ Const (@{const_name HOL.eq}, dummyT)
wenzelm@56257
   116
      val error_msg = cat_lines 
wenzelm@56257
   117
        ["Generation of a pcr_cr_eq failed.",
wenzelm@56257
   118
        (Pretty.string_of (Pretty.block
wenzelm@56257
   119
           [Pretty.str "Reason: Cannot prove this: ", Pretty.brk 2, Syntax.pretty_term ctxt goal])),
wenzelm@56257
   120
         "Most probably a relator_eq rule for one of the involved types is missing."]
wenzelm@56257
   121
    in
wenzelm@56257
   122
      error error_msg
wenzelm@56257
   123
    end
kuncar@51374
   124
in
wenzelm@60239
   125
  fun define_pcr_cr_eq (config: config) lthy pcr_rel_def =
kuncar@51374
   126
    let
wenzelm@59582
   127
      val lhs = (Thm.term_of o Thm.lhs_of) pcr_rel_def
wenzelm@60239
   128
      val qty_name =
wenzelm@60239
   129
        (Binding.name o Long_Name.base_name o fst o dest_Type o
wenzelm@60239
   130
          List.last o binder_types o fastype_of) lhs
kuncar@51374
   131
      val args = (snd o strip_comb) lhs
kuncar@51374
   132
      
kuncar@51374
   133
      fun make_inst var ctxt = 
kuncar@51374
   134
        let 
kuncar@51374
   135
          val typ = (snd o relation_types o snd o dest_Var) var
kuncar@51374
   136
          val sort = Type.sort_of_atyp typ
wenzelm@59630
   137
          val (fresh_var, ctxt') = yield_singleton Variable.invent_types sort ctxt
kuncar@51374
   138
        in
wenzelm@59630
   139
          (apply2 (Thm.cterm_of ctxt') (var, HOLogic.eq_const (TFree fresh_var)), ctxt')
kuncar@51374
   140
        end
kuncar@51374
   141
      
kuncar@51374
   142
      val orig_lthy = lthy
kuncar@51374
   143
      val (args_inst, lthy) = fold_map make_inst args lthy
kuncar@51374
   144
      val pcr_cr_eq = 
kuncar@51374
   145
        pcr_rel_def
kuncar@51374
   146
        |> Drule.cterm_instantiate args_inst    
kuncar@52883
   147
        |> Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv 
kuncar@52883
   148
          (Transfer.bottom_rewr_conv (Transfer.get_relator_eq lthy))))
kuncar@51374
   149
  in
wenzelm@59582
   150
    case (Thm.term_of o Thm.rhs_of) pcr_cr_eq of
wenzelm@56257
   151
      Const (@{const_name "relcompp"}, _) $ Const (@{const_name HOL.eq}, _) $ _ =>
kuncar@51374
   152
        let
kuncar@51374
   153
          val thm = 
kuncar@51374
   154
            pcr_cr_eq
kuncar@51374
   155
            |> Conv.fconv_rule (Conv.arg_conv (Conv.rewr_conv eq_OO_meta))
kuncar@51374
   156
            |> mk_HOL_eq
kuncar@51374
   157
            |> singleton (Variable.export lthy orig_lthy)
kuncar@60225
   158
          val lthy = (#notes config ? (Local_Theory.note 
kuncar@60225
   159
              ((Binding.qualified true "pcr_cr_eq" qty_name, []), [thm]) #> snd)) lthy
kuncar@51374
   160
        in
kuncar@51374
   161
          (thm, lthy)
kuncar@51374
   162
        end
kuncar@51374
   163
      | Const (@{const_name "relcompp"}, _) $ t $ _ => print_generate_pcr_cr_eq_error lthy t
kuncar@51374
   164
      | _ => error "generate_pcr_cr_eq: implementation error"
kuncar@51374
   165
  end
kuncar@51374
   166
end
kuncar@51374
   167
haftmann@59487
   168
fun define_code_constr quot_thm lthy =
kuncar@47937
   169
  let
kuncar@47951
   170
    val abs = quot_thm_abs quot_thm
kuncar@47937
   171
  in
haftmann@59487
   172
    if is_Const abs then
kuncar@47937
   173
      let
haftmann@59487
   174
        val (fixed_abs, lthy') = yield_singleton Variable.importT_terms abs lthy
kuncar@47937
   175
      in  
haftmann@59487
   176
         Local_Theory.background_theory (Code.add_datatype [dest_Const fixed_abs]) lthy'
kuncar@47937
   177
      end
kuncar@47937
   178
    else
kuncar@47937
   179
      lthy
kuncar@47937
   180
  end
kuncar@47937
   181
haftmann@59487
   182
fun define_abs_type quot_thm lthy =
haftmann@59487
   183
  if Lifting_Def.can_generate_code_cert quot_thm then
kuncar@47308
   184
    let
kuncar@47308
   185
      val abs_type_thm = quot_thm RS @{thm Quotient_abs_rep}
kuncar@47308
   186
      val add_abstype_attribute = 
haftmann@59458
   187
          Thm.declaration_attribute (fn thm => Context.mapping (Code.add_abstype_default thm) I)
kuncar@51374
   188
        val add_abstype_attrib = Attrib.internal (K add_abstype_attribute)
kuncar@47308
   189
    in
kuncar@47308
   190
      lthy
kuncar@47308
   191
        |> (snd oo Local_Theory.note) ((Binding.empty, [add_abstype_attrib]), [abs_type_thm])
kuncar@47308
   192
    end
kuncar@47308
   193
  else
kuncar@47308
   194
    lthy
kuncar@47308
   195
kuncar@53651
   196
local
kuncar@53651
   197
  exception QUOT_ERROR of Pretty.T list
kuncar@53651
   198
in
kuncar@47379
   199
fun quot_thm_sanity_check ctxt quot_thm =
kuncar@47379
   200
  let
kuncar@53651
   201
    val _ = 
wenzelm@59582
   202
      if (Thm.nprems_of quot_thm > 0) then   
kuncar@53651
   203
          raise QUOT_ERROR [Pretty.block
kuncar@53651
   204
            [Pretty.str "The Quotient theorem has extra assumptions:",
kuncar@53651
   205
             Pretty.brk 1,
kuncar@53651
   206
             Display.pretty_thm ctxt quot_thm]]
kuncar@53651
   207
      else ()
wenzelm@59582
   208
    val _ = quot_thm |> Thm.concl_of |> HOLogic.dest_Trueprop |> dest_Quotient
kuncar@53651
   209
    handle TERM _ => raise QUOT_ERROR
kuncar@53651
   210
          [Pretty.block
kuncar@53651
   211
            [Pretty.str "The Quotient theorem is not of the right form:",
kuncar@53651
   212
             Pretty.brk 1,
kuncar@53651
   213
             Display.pretty_thm ctxt quot_thm]]
kuncar@47379
   214
    val ((_, [quot_thm_fixed]), ctxt') = Variable.importT [quot_thm] ctxt 
kuncar@47951
   215
    val (rty, qty) = quot_thm_rty_qty quot_thm_fixed
kuncar@47379
   216
    val rty_tfreesT = Term.add_tfree_namesT rty []
kuncar@47379
   217
    val qty_tfreesT = Term.add_tfree_namesT qty []
kuncar@47379
   218
    val extra_rty_tfrees =
kuncar@47545
   219
      case subtract (op =) qty_tfreesT rty_tfreesT of
kuncar@47379
   220
        [] => []
kuncar@47379
   221
      | extras => [Pretty.block ([Pretty.str "Extra variables in the raw type:",
kuncar@47379
   222
                                 Pretty.brk 1] @ 
kuncar@47379
   223
                                 ((Pretty.commas o map (Pretty.str o quote)) extras) @
kuncar@47545
   224
                                 [Pretty.str "."])]
kuncar@47379
   225
    val not_type_constr = 
kuncar@47545
   226
      case qty of
kuncar@47379
   227
         Type _ => []
kuncar@47379
   228
         | _ => [Pretty.block [Pretty.str "The quotient type ",
kuncar@47379
   229
                                Pretty.quote (Syntax.pretty_typ ctxt' qty),
kuncar@47379
   230
                                Pretty.brk 1,
kuncar@47545
   231
                                Pretty.str "is not a type constructor."]]
kuncar@47379
   232
    val errs = extra_rty_tfrees @ not_type_constr
kuncar@47379
   233
  in
kuncar@53651
   234
    if null errs then () else raise QUOT_ERROR errs
kuncar@53651
   235
  end
kuncar@53651
   236
  handle QUOT_ERROR errs => error (cat_lines (["Sanity check of the quotient theorem failed:"] 
kuncar@53651
   237
                                            @ (map (Pretty.string_of o Pretty.item o single) errs)))
kuncar@53651
   238
end
kuncar@53651
   239
kuncar@53651
   240
fun lifting_bundle qty_full_name qinfo lthy = 
kuncar@53651
   241
  let
kuncar@53651
   242
    fun qualify suffix defname = Binding.qualified true suffix defname
kuncar@53651
   243
    val binding =  qty_full_name |> Long_Name.base_name |> Binding.name |> qualify "lifting"
kuncar@53651
   244
    val morphed_binding = Morphism.binding (Local_Theory.target_morphism lthy) binding
kuncar@53651
   245
    val bundle_name = Name_Space.full_name (Name_Space.naming_of 
kuncar@53651
   246
      (Context.Theory (Proof_Context.theory_of lthy))) morphed_binding
kuncar@53651
   247
    fun phi_qinfo phi = Lifting_Info.transform_quotient phi qinfo
kuncar@53651
   248
kuncar@53651
   249
    val thy = Proof_Context.theory_of lthy
kuncar@53651
   250
    val dummy_thm = Thm.transfer thy Drule.dummy_thm
wenzelm@59084
   251
    val pointer =
wenzelm@59084
   252
      Token.explode (Thy_Header.get_keywords thy) Position.none (cartouche bundle_name)
kuncar@53651
   253
    val restore_lifting_att = 
wenzelm@58011
   254
      ([dummy_thm], [Token.src ("Lifting.lifting_restore_internal", Position.none) pointer])
kuncar@53651
   255
  in
kuncar@53651
   256
    lthy 
kuncar@53651
   257
      |> Local_Theory.declaration {syntax = false, pervasive = true}
kuncar@53651
   258
           (fn phi => Lifting_Info.init_restore_data bundle_name (phi_qinfo phi))
kuncar@53651
   259
      |> Bundle.bundle ((binding, [restore_lifting_att])) []
kuncar@60225
   260
      |> pair binding
kuncar@47379
   261
  end
kuncar@47379
   262
kuncar@60225
   263
fun setup_lifting_infr config quot_thm opt_reflp_thm lthy =
kuncar@47308
   264
  let
kuncar@47379
   265
    val _ = quot_thm_sanity_check lthy quot_thm
kuncar@57663
   266
    val (_, qty) = quot_thm_rty_qty quot_thm
kuncar@60225
   267
    val (pcrel_def, lthy) = define_pcrel config (quot_thm_crel quot_thm) lthy
kuncar@51374
   268
    (**)
kuncar@51374
   269
    val pcrel_def = Option.map (Morphism.thm (Local_Theory.target_morphism lthy)) pcrel_def
kuncar@51374
   270
    (**)
kuncar@51374
   271
    val (pcr_cr_eq, lthy) = case pcrel_def of
kuncar@60225
   272
      SOME pcrel_def => apfst SOME (define_pcr_cr_eq config lthy pcrel_def)
kuncar@51374
   273
      | NONE => (NONE, lthy)
kuncar@53219
   274
    val pcr_info = case pcrel_def of
kuncar@51374
   275
      SOME pcrel_def => SOME { pcrel_def = pcrel_def, pcr_cr_eq = the pcr_cr_eq }
kuncar@51374
   276
      | NONE => NONE
kuncar@53219
   277
    val quotients = { quot_thm = quot_thm, pcr_info = pcr_info }
kuncar@57663
   278
    val qty_full_name = (fst o dest_Type) qty
kuncar@53219
   279
    fun quot_info phi = Lifting_Info.transform_quotient phi quotients
kuncar@51994
   280
    val reflexivity_rule_attr = Attrib.internal (K Lifting_Info.add_reflexivity_rule_attribute)
kuncar@51374
   281
    val lthy = case opt_reflp_thm of
kuncar@47937
   282
      SOME reflp_thm => lthy
kuncar@51994
   283
        |> (snd oo Local_Theory.note) ((Binding.empty, [reflexivity_rule_attr]),
kuncar@55563
   284
              [reflp_thm RS @{thm reflp_ge_eq}])
haftmann@59487
   285
        |> define_code_constr quot_thm
kuncar@47937
   286
      | NONE => lthy
haftmann@59487
   287
        |> define_abs_type quot_thm
kuncar@47308
   288
  in
kuncar@50227
   289
    lthy
kuncar@47308
   290
      |> Local_Theory.declaration {syntax = false, pervasive = true}
kuncar@47308
   291
        (fn phi => Lifting_Info.update_quotients qty_full_name (quot_info phi))
kuncar@53651
   292
      |> lifting_bundle qty_full_name quotients
kuncar@47308
   293
  end
kuncar@47308
   294
kuncar@51956
   295
local
kuncar@51956
   296
  fun importT_inst_exclude exclude ts ctxt =
kuncar@51956
   297
    let
kuncar@53651
   298
      val tvars = rev (subtract op= exclude (fold Term.add_tvars ts []))
kuncar@53651
   299
      val (tfrees, ctxt') = Variable.invent_types (map #2 tvars) ctxt
kuncar@51956
   300
    in (tvars ~~ map TFree tfrees, ctxt') end
kuncar@51956
   301
  
kuncar@51956
   302
  fun import_inst_exclude exclude ts ctxt =
kuncar@51956
   303
    let
kuncar@51956
   304
      val excludeT = fold (Term.add_tvarsT o snd) exclude []
kuncar@53651
   305
      val (instT, ctxt') = importT_inst_exclude excludeT ts ctxt
kuncar@51956
   306
      val vars = map (apsnd (Term_Subst.instantiateT instT)) 
kuncar@53651
   307
        (rev (subtract op= exclude (fold Term.add_vars ts [])))
kuncar@53651
   308
      val (xs, ctxt'') = Variable.variant_fixes (map (#1 o #1) vars) ctxt'
kuncar@53651
   309
      val inst = vars ~~ map Free (xs ~~ map #2 vars)
kuncar@51956
   310
    in ((instT, inst), ctxt'') end
kuncar@51956
   311
  
kuncar@51956
   312
  fun import_terms_exclude exclude ts ctxt =
kuncar@51956
   313
    let val (inst, ctxt') = import_inst_exclude exclude ts ctxt
kuncar@51956
   314
    in (map (Term_Subst.instantiate inst) ts, ctxt') end
kuncar@51956
   315
in
kuncar@51956
   316
  fun reduce_goal not_fix goal tac ctxt =
kuncar@51956
   317
    let
wenzelm@59630
   318
      val (fixed_goal, ctxt') = yield_singleton (import_terms_exclude not_fix) goal ctxt
wenzelm@59630
   319
      val init_goal = Goal.init (Thm.cterm_of ctxt' fixed_goal)
kuncar@51956
   320
    in
wenzelm@59630
   321
      (singleton (Variable.export ctxt' ctxt) o Goal.conclude) (the (SINGLE tac init_goal))
kuncar@51956
   322
    end
kuncar@51956
   323
end
kuncar@51956
   324
kuncar@51374
   325
local 
kuncar@56518
   326
  val OO_rules = @{thms left_total_OO left_unique_OO right_total_OO right_unique_OO bi_total_OO
kuncar@56518
   327
    bi_unique_OO}
kuncar@51374
   328
in
kuncar@51374
   329
  fun parametrize_class_constraint ctxt pcr_def constraint =
kuncar@51374
   330
    let
kuncar@51374
   331
      fun generate_transfer_rule pcr_def constraint goal ctxt =
kuncar@51374
   332
        let
wenzelm@59630
   333
          val (fixed_goal, ctxt') = yield_singleton (Variable.import_terms true) goal ctxt
wenzelm@59630
   334
          val init_goal = Goal.init (Thm.cterm_of ctxt' fixed_goal)
wenzelm@59630
   335
          val rules = Transfer.get_transfer_raw ctxt'
kuncar@51374
   336
          val rules = constraint :: OO_rules @ rules
wenzelm@59498
   337
          val tac =
wenzelm@59630
   338
            K (Local_Defs.unfold_tac ctxt' [pcr_def]) THEN' REPEAT_ALL_NEW (resolve_tac ctxt' rules)
kuncar@51374
   339
        in
wenzelm@59630
   340
          (singleton (Variable.export ctxt' ctxt) o Goal.conclude) (the (SINGLE (tac 1) init_goal))
kuncar@51374
   341
        end
kuncar@51374
   342
      
kuncar@51374
   343
      fun make_goal pcr_def constr =
kuncar@51374
   344
        let 
wenzelm@59582
   345
          val pred_name =
wenzelm@59582
   346
            (fst o dest_Const o strip_args 1 o HOLogic.dest_Trueprop o Thm.prop_of) constr
wenzelm@59582
   347
          val arg = (fst o Logic.dest_equals o Thm.prop_of) pcr_def
kuncar@51374
   348
        in
kuncar@51374
   349
          HOLogic.mk_Trueprop ((Const (pred_name, (fastype_of arg) --> HOLogic.boolT)) $ arg)
kuncar@51374
   350
        end
kuncar@51374
   351
      
kuncar@51374
   352
      val check_assms =
kuncar@51374
   353
        let 
kuncar@56518
   354
          val right_names = ["right_total", "right_unique", "left_total", "left_unique", "bi_total",
kuncar@56518
   355
            "bi_unique"]
kuncar@51374
   356
      
kuncar@51374
   357
          fun is_right_name name = member op= right_names (Long_Name.base_name name)
kuncar@51374
   358
      
kuncar@51374
   359
          fun is_trivial_assm (Const (name, _) $ Var (_, _)) = is_right_name name
kuncar@51374
   360
            | is_trivial_assm (Const (name, _) $ Free (_, _)) = is_right_name name
kuncar@51374
   361
            | is_trivial_assm _ = false
kuncar@51374
   362
        in
kuncar@51374
   363
          fn thm => 
kuncar@51374
   364
            let
wenzelm@59582
   365
              val prems = map HOLogic.dest_Trueprop (Thm.prems_of thm)
wenzelm@59582
   366
              val thm_name =
wenzelm@59582
   367
                (Long_Name.base_name o fst o dest_Const o strip_args 1 o HOLogic.dest_Trueprop o Thm.concl_of) thm
kuncar@51374
   368
              val non_trivial_assms = filter_out is_trivial_assm prems
kuncar@51374
   369
            in
kuncar@51374
   370
              if null non_trivial_assms then ()
kuncar@51374
   371
              else
kuncar@51374
   372
                let
kuncar@51374
   373
                  val pretty_msg = Pretty.block ([Pretty.str "Non-trivial assumptions in ",
kuncar@51374
   374
                    Pretty.str thm_name,
kuncar@51374
   375
                    Pretty.str " transfer rule found:",
kuncar@51374
   376
                    Pretty.brk 1] @ 
kuncar@51374
   377
                    ((Pretty.commas o map (Syntax.pretty_term ctxt)) non_trivial_assms) @
kuncar@51374
   378
                                       [Pretty.str "."])
kuncar@51374
   379
                in
kuncar@51374
   380
                  warning (Pretty.str_of pretty_msg)
kuncar@51374
   381
                end
kuncar@51374
   382
            end
kuncar@51374
   383
        end
kuncar@51374
   384
  
kuncar@51374
   385
      val goal = make_goal pcr_def constraint
kuncar@51374
   386
      val thm = generate_transfer_rule pcr_def constraint goal ctxt
kuncar@51374
   387
      val _ = check_assms thm
kuncar@51374
   388
    in
kuncar@51374
   389
      thm
kuncar@51374
   390
    end
kuncar@51374
   391
end
kuncar@51374
   392
kuncar@51374
   393
local
kuncar@51374
   394
  val id_unfold = (Conv.rewr_conv (mk_meta_eq @{thm id_def}))
kuncar@51374
   395
in
kuncar@51374
   396
  fun generate_parametric_id lthy rty id_transfer_rule =
kuncar@51374
   397
    let
kuncar@51374
   398
      (* it doesn't raise an exception because it would have already raised it in define_pcrel *)
wenzelm@59630
   399
      val (quot_thm, _, ctxt') = Lifting_Term.prove_param_quot_thm lthy rty
wenzelm@59630
   400
      val parametrized_relator =
wenzelm@59630
   401
        singleton (Variable.export_terms ctxt' lthy) (quot_thm_crel quot_thm)
kuncar@51374
   402
      val id_transfer = 
kuncar@51374
   403
         @{thm id_transfer}
kuncar@51374
   404
        |> Thm.incr_indexes (Term.maxidx_of_term parametrized_relator + 1)
kuncar@51374
   405
        |> Conv.fconv_rule(HOLogic.Trueprop_conv (Conv.arg_conv id_unfold then_conv Conv.arg1_conv id_unfold))
wenzelm@59582
   406
      val var = Var (hd (Term.add_vars (Thm.prop_of id_transfer) []))
wenzelm@59630
   407
      val inst = [(Thm.cterm_of lthy var, Thm.cterm_of lthy parametrized_relator)]
kuncar@53651
   408
      val id_par_thm = Drule.cterm_instantiate inst id_transfer
kuncar@51374
   409
    in
kuncar@51374
   410
      Lifting_Def.generate_parametric_transfer_rule lthy id_transfer_rule id_par_thm
kuncar@51374
   411
    end
kuncar@51374
   412
    handle Lifting_Term.MERGE_TRANSFER_REL msg => 
kuncar@51374
   413
      let
kuncar@51374
   414
        val error_msg = cat_lines 
kuncar@51374
   415
          ["Generation of a parametric transfer rule for the abs. or the rep. function failed.",
kuncar@51374
   416
          "A non-parametric version will be used.",
kuncar@51374
   417
          (Pretty.string_of (Pretty.block
kuncar@51374
   418
             [Pretty.str "Reason:", Pretty.brk 2, msg]))]
kuncar@51374
   419
      in
kuncar@51374
   420
        (warning error_msg; id_transfer_rule)
kuncar@51374
   421
      end
kuncar@51374
   422
end
kuncar@51374
   423
kuncar@51956
   424
local
kuncar@51956
   425
  fun rewrite_first_Domainp_arg rewr_thm thm = Conv.fconv_rule (Conv.concl_conv ~1 (HOLogic.Trueprop_conv 
kuncar@51956
   426
      (Conv.arg1_conv (Conv.arg_conv (Conv.rewr_conv rewr_thm))))) thm
kuncar@51956
   427
  
kuncar@51956
   428
  fun fold_Domainp_pcrel pcrel_def thm =
kuncar@51956
   429
    let
wenzelm@59582
   430
      val ct =
wenzelm@59582
   431
        thm |> Thm.cprop_of |> Drule.strip_imp_concl
wenzelm@59582
   432
        |> Thm.dest_arg |> Thm.dest_arg1 |> Thm.dest_arg
wenzelm@59586
   433
      val pcrel_def = Thm.incr_indexes (Thm.maxidx_of_cterm ct + 1) pcrel_def
kuncar@51956
   434
      val thm = Thm.instantiate (Thm.match (ct, Thm.rhs_of pcrel_def)) thm
kuncar@53651
   435
        handle Pattern.MATCH => raise CTERM ("fold_Domainp_pcrel", [ct, Thm.rhs_of pcrel_def])
kuncar@51956
   436
    in
kuncar@51956
   437
      rewrite_first_Domainp_arg (Thm.symmetric pcrel_def) thm
kuncar@51956
   438
    end
kuncar@51956
   439
kuncar@51956
   440
  fun reduce_Domainp ctxt rules thm =
kuncar@51956
   441
    let
wenzelm@59582
   442
      val goal = thm |> Thm.prems_of |> hd
kuncar@51956
   443
      val var = goal |> HOLogic.dest_Trueprop |> dest_comb |> snd |> dest_Var 
wenzelm@59498
   444
      val reduced_assm =
wenzelm@59498
   445
        reduce_goal [var] goal (TRY (REPEAT_ALL_NEW (resolve_tac ctxt rules) 1)) ctxt
kuncar@51956
   446
    in
kuncar@51956
   447
      reduced_assm RS thm
kuncar@51956
   448
    end
kuncar@51956
   449
in
kuncar@53219
   450
  fun parametrize_domain dom_thm (pcr_info : Lifting_Info.pcr) ctxt =
kuncar@51956
   451
    let
kuncar@51956
   452
      fun reduce_first_assm ctxt rules thm =
kuncar@51956
   453
        let
wenzelm@59582
   454
          val goal = thm |> Thm.prems_of |> hd
wenzelm@59498
   455
          val reduced_assm =
wenzelm@59498
   456
            reduce_goal [] goal (TRY (REPEAT_ALL_NEW (resolve_tac ctxt rules) 1)) ctxt
kuncar@51956
   457
        in
kuncar@51956
   458
          reduced_assm RS thm
kuncar@51956
   459
        end
kuncar@51956
   460
kuncar@53219
   461
      val pcr_cr_met_eq = #pcr_cr_eq pcr_info RS @{thm eq_reflection}
kuncar@51956
   462
      val pcr_Domainp_eq = rewrite_first_Domainp_arg (Thm.symmetric pcr_cr_met_eq) dom_thm
kuncar@53219
   463
      val pcrel_def = #pcrel_def pcr_info
kuncar@51956
   464
      val pcr_Domainp_par_left_total = 
kuncar@51956
   465
        (dom_thm RS @{thm pcr_Domainp_par_left_total})
kuncar@51956
   466
          |> fold_Domainp_pcrel pcrel_def
kuncar@51956
   467
          |> reduce_first_assm ctxt (Lifting_Info.get_reflexivity_rules ctxt)
kuncar@51956
   468
      val pcr_Domainp_par = 
kuncar@51956
   469
        (dom_thm RS @{thm pcr_Domainp_par})      
kuncar@51956
   470
          |> fold_Domainp_pcrel pcrel_def
kuncar@51956
   471
          |> reduce_Domainp ctxt (Transfer.get_relator_domain ctxt)
kuncar@51956
   472
      val pcr_Domainp = 
kuncar@51956
   473
        (dom_thm RS @{thm pcr_Domainp})
kuncar@51956
   474
          |> fold_Domainp_pcrel pcrel_def
kuncar@51956
   475
      val thms =
kuncar@60225
   476
        [("domain",                 [pcr_Domainp], @{attributes [transfer_domain_rule]}),
kuncar@60225
   477
         ("domain_par",             [pcr_Domainp_par], @{attributes [transfer_domain_rule]}),
kuncar@60225
   478
         ("domain_par_left_total",  [pcr_Domainp_par_left_total], @{attributes [transfer_domain_rule]}),
kuncar@60225
   479
         ("domain_eq",              [pcr_Domainp_eq], @{attributes [transfer_domain_rule]})]
kuncar@51956
   480
    in
kuncar@51956
   481
      thms
kuncar@51956
   482
    end
kuncar@51956
   483
kuncar@56518
   484
  fun parametrize_total_domain left_total pcrel_def ctxt =
kuncar@51956
   485
    let
kuncar@51956
   486
      val thm =
kuncar@56518
   487
        (left_total RS @{thm pcr_Domainp_total})
kuncar@51956
   488
          |> fold_Domainp_pcrel pcrel_def 
kuncar@51956
   489
          |> reduce_Domainp ctxt (Transfer.get_relator_domain ctxt)
kuncar@51956
   490
    in
kuncar@60225
   491
      [("domain", [thm], @{attributes [transfer_domain_rule]})]
kuncar@51956
   492
    end
kuncar@51956
   493
kuncar@51956
   494
end
kuncar@51374
   495
kuncar@51374
   496
fun get_pcrel_info ctxt qty_full_name =  
kuncar@53219
   497
  #pcr_info (the (Lifting_Info.lookup_quotients ctxt qty_full_name))
kuncar@51374
   498
kuncar@51956
   499
fun get_Domainp_thm quot_thm =
kuncar@56519
   500
   the (get_first (try(curry op RS quot_thm)) [@{thm eq_onp_to_Domainp}, @{thm Quotient_to_Domainp}])
kuncar@51956
   501
kuncar@60225
   502
fun notes names thms = 
kuncar@60225
   503
  let
kuncar@60225
   504
    val notes =
kuncar@60225
   505
        if names then map (fn (name, thms, attrs) => ((name, []), [(thms, attrs)])) thms
kuncar@60225
   506
        else map_filter (fn (_, thms, attrs) => if null attrs then NONE 
kuncar@60225
   507
          else SOME ((Binding.empty, []), [(thms, attrs)])) thms
kuncar@60225
   508
  in
kuncar@60225
   509
    Local_Theory.notes notes #> snd
kuncar@60225
   510
  end
kuncar@60225
   511
kuncar@60225
   512
fun map_thms map_name map_thm thms = 
kuncar@60225
   513
  map (fn (name, thms, attr) => (map_name name, map map_thm thms, attr)) thms
kuncar@60225
   514
kuncar@47852
   515
(*
kuncar@47852
   516
  Sets up the Lifting package by a quotient theorem.
kuncar@47852
   517
kuncar@47852
   518
  quot_thm - a quotient theorem (Quotient R Abs Rep T)
kuncar@51374
   519
  opt_reflp_thm - a theorem saying that a relation from quot_thm is reflexive
kuncar@47852
   520
    (in the form "reflp R")
kuncar@54335
   521
  opt_par_thm - a parametricity theorem for R
kuncar@47852
   522
*)
kuncar@47852
   523
wenzelm@60239
   524
fun setup_by_quotient (config: config) quot_thm opt_reflp_thm opt_par_thm lthy =
kuncar@47521
   525
  let
kuncar@51374
   526
    (**)
kuncar@51374
   527
    val quot_thm = Morphism.thm (Local_Theory.target_morphism lthy) quot_thm
kuncar@51374
   528
    (**)
kuncar@51374
   529
    val (rty, qty) = quot_thm_rty_qty quot_thm
huffman@47575
   530
    val induct_attr = Attrib.internal (K (Induct.induct_type (fst (dest_Type qty))))
kuncar@51374
   531
    val qty_full_name = (fst o dest_Type) qty
kuncar@51374
   532
    val qty_name = (Binding.name o Long_Name.base_name) qty_full_name
kuncar@47545
   533
    fun qualify suffix = Binding.qualified true suffix qty_name
kuncar@60225
   534
    val notes1 = case opt_reflp_thm of
kuncar@51374
   535
      SOME reflp_thm =>
kuncar@51374
   536
        let 
kuncar@51374
   537
          val thms =
kuncar@60225
   538
            [("abs_induct",     @{thms Quotient_total_abs_induct}, [induct_attr]),
kuncar@60225
   539
             ("abs_eq_iff",     @{thms Quotient_total_abs_eq_iff}, []           )]
kuncar@51374
   540
        in
kuncar@60225
   541
          map_thms qualify (fn thm => [quot_thm, reflp_thm] MRSL thm) thms
kuncar@51374
   542
        end
kuncar@51374
   543
      | NONE =>
kuncar@51374
   544
        let
kuncar@51374
   545
          val thms = 
kuncar@60225
   546
            [("abs_induct",     @{thms Quotient_abs_induct},       [induct_attr])]
kuncar@51374
   547
        in
kuncar@60225
   548
          map_thms qualify (fn thm => quot_thm RS thm) thms
kuncar@51374
   549
        end
kuncar@51956
   550
    val dom_thm = get_Domainp_thm quot_thm
kuncar@51374
   551
kuncar@60225
   552
    fun setup_transfer_rules_nonpar notes =
kuncar@51374
   553
      let
kuncar@60225
   554
        val notes1 =
kuncar@51374
   555
          case opt_reflp_thm of
kuncar@51374
   556
            SOME reflp_thm =>
kuncar@51374
   557
              let 
kuncar@51374
   558
                val thms =
kuncar@60225
   559
                  [("id_abs_transfer",@{thms Quotient_id_abs_transfer}, @{attributes [transfer_rule]}),
kuncar@60225
   560
                   ("left_total",     @{thms Quotient_left_total},      @{attributes [transfer_rule]}),
kuncar@60225
   561
                   ("bi_total",       @{thms Quotient_bi_total},        @{attributes [transfer_rule]})]
kuncar@51374
   562
              in
kuncar@60225
   563
                map_thms qualify (fn thm => [quot_thm, reflp_thm] MRSL thm) thms
kuncar@51374
   564
              end
kuncar@60225
   565
            | NONE => map_thms qualify I [("domain", [dom_thm], @{attributes [transfer_domain_rule]})]
kuncar@51956
   566
kuncar@60225
   567
        val notes2 = map_thms qualify (fn thm => quot_thm RS thm)
kuncar@60225
   568
          [("rel_eq_transfer", @{thms Quotient_rel_eq_transfer}, @{attributes [transfer_rule]}),
kuncar@60225
   569
           ("right_unique",    @{thms Quotient_right_unique},    @{attributes [transfer_rule]}), 
kuncar@60225
   570
           ("right_total",     @{thms Quotient_right_total},     @{attributes [transfer_rule]})]
kuncar@51374
   571
      in
kuncar@60225
   572
         notes2 @ notes1 @ notes
kuncar@51374
   573
      end
kuncar@51374
   574
kuncar@51374
   575
    fun generate_parametric_rel_eq lthy transfer_rule opt_param_thm =
kuncar@51374
   576
      option_fold transfer_rule (Lifting_Def.generate_parametric_transfer_rule lthy transfer_rule) opt_param_thm
kuncar@51374
   577
      handle Lifting_Term.MERGE_TRANSFER_REL msg => 
kuncar@51374
   578
        let
kuncar@51374
   579
          val error_msg = cat_lines 
kuncar@51374
   580
            ["Generation of a parametric transfer rule for the quotient relation failed.",
kuncar@51374
   581
            (Pretty.string_of (Pretty.block
kuncar@51374
   582
               [Pretty.str "Reason:", Pretty.brk 2, msg]))]
kuncar@51374
   583
        in
kuncar@51374
   584
          error error_msg
kuncar@51374
   585
        end
kuncar@51374
   586
kuncar@60225
   587
    fun setup_transfer_rules_par lthy notes =
kuncar@51374
   588
      let
kuncar@51956
   589
        val pcrel_info = (the (get_pcrel_info lthy qty_full_name))
kuncar@51956
   590
        val pcrel_def = #pcrel_def pcrel_info
kuncar@60225
   591
        val notes1 =
kuncar@51374
   592
          case opt_reflp_thm of
kuncar@51374
   593
            SOME reflp_thm =>
kuncar@51374
   594
              let
kuncar@56518
   595
                val left_total = ([quot_thm, reflp_thm] MRSL @{thm Quotient_left_total})
kuncar@51956
   596
                val bi_total = ([quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total})
kuncar@56518
   597
                val domain_thms = parametrize_total_domain left_total pcrel_def lthy
kuncar@51374
   598
                val id_abs_transfer = generate_parametric_id lthy rty
kuncar@51374
   599
                  (Lifting_Term.parametrize_transfer_rule lthy
kuncar@51374
   600
                    ([quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer}))
kuncar@56518
   601
                val left_total = parametrize_class_constraint lthy pcrel_def left_total
kuncar@51956
   602
                val bi_total = parametrize_class_constraint lthy pcrel_def bi_total
kuncar@51374
   603
                val thms = 
kuncar@60225
   604
                  [("id_abs_transfer", [id_abs_transfer], @{attributes [transfer_rule]}),
kuncar@60225
   605
                   ("left_total",      [left_total],      @{attributes [transfer_rule]}),  
kuncar@60225
   606
                   ("bi_total",        [bi_total],        @{attributes [transfer_rule]})]
kuncar@51374
   607
              in
kuncar@60225
   608
                map_thms qualify I thms @ map_thms qualify I domain_thms
kuncar@51374
   609
              end
kuncar@51374
   610
            | NONE =>
kuncar@51374
   611
              let
kuncar@51956
   612
                val thms = parametrize_domain dom_thm pcrel_info lthy
kuncar@51374
   613
              in
kuncar@60225
   614
                map_thms qualify I thms
kuncar@51374
   615
              end
kuncar@51956
   616
kuncar@51374
   617
        val rel_eq_transfer = generate_parametric_rel_eq lthy 
kuncar@51374
   618
          (Lifting_Term.parametrize_transfer_rule lthy (quot_thm RS @{thm Quotient_rel_eq_transfer}))
kuncar@51374
   619
            opt_par_thm
kuncar@51374
   620
        val right_unique = parametrize_class_constraint lthy pcrel_def 
kuncar@51374
   621
            (quot_thm RS @{thm Quotient_right_unique})
kuncar@51374
   622
        val right_total = parametrize_class_constraint lthy pcrel_def 
kuncar@51374
   623
            (quot_thm RS @{thm Quotient_right_total})
kuncar@60225
   624
        val notes2 = map_thms qualify I
kuncar@60225
   625
          [("rel_eq_transfer", [rel_eq_transfer], @{attributes [transfer_rule]}),
kuncar@60225
   626
           ("right_unique",    [right_unique],    @{attributes [transfer_rule]}), 
kuncar@60225
   627
           ("right_total",     [right_total],     @{attributes [transfer_rule]})]      
kuncar@51374
   628
      in
kuncar@60225
   629
        notes2 @ notes1 @ notes
kuncar@51374
   630
      end
kuncar@51374
   631
kuncar@60225
   632
    fun setup_rules lthy = 
kuncar@60225
   633
      let
kuncar@60225
   634
        val thms =  if is_some (get_pcrel_info lthy qty_full_name) 
kuncar@60225
   635
          then setup_transfer_rules_par lthy notes1 else setup_transfer_rules_nonpar notes1
kuncar@60225
   636
      in
kuncar@60225
   637
        notes (#notes config) thms lthy
kuncar@60225
   638
      end
kuncar@47521
   639
  in
kuncar@50227
   640
    lthy
kuncar@60225
   641
      |> setup_lifting_infr config quot_thm opt_reflp_thm
kuncar@60225
   642
      ||> setup_rules
kuncar@47521
   643
  end
kuncar@47521
   644
kuncar@47852
   645
(*
kuncar@47852
   646
  Sets up the Lifting package by a typedef theorem.
kuncar@47852
   647
kuncar@47937
   648
  gen_code - flag if an abstract type given by typedef_thm should be registred 
kuncar@47852
   649
    as an abstract type in the code generator
kuncar@47852
   650
  typedef_thm - a typedef theorem (type_definition Rep Abs S)
kuncar@47852
   651
*)
kuncar@47852
   652
kuncar@60225
   653
fun setup_by_typedef_thm config typedef_thm lthy =
kuncar@47308
   654
  let
wenzelm@59582
   655
    val (_ $ rep_fun $ _ $ typedef_set) = (HOLogic.dest_Trueprop o Thm.prop_of) typedef_thm
kuncar@60225
   656
    val (T_def, lthy) = define_crel config rep_fun lthy
kuncar@51374
   657
    (**)
kuncar@51374
   658
    val T_def = Morphism.thm (Local_Theory.target_morphism lthy) T_def
kuncar@51374
   659
    (**)    
kuncar@47545
   660
    val quot_thm = case typedef_set of
wenzelm@56257
   661
      Const (@{const_name top}, _) => 
kuncar@47521
   662
        [typedef_thm, T_def] MRSL @{thm UNIV_typedef_to_Quotient}
kuncar@47521
   663
      | Const (@{const_name "Collect"}, _) $ Abs (_, _, _) => 
kuncar@47521
   664
        [typedef_thm, T_def] MRSL @{thm open_typedef_to_Quotient}
kuncar@47521
   665
      | _ => 
kuncar@47545
   666
        [typedef_thm, T_def] MRSL @{thm typedef_to_Quotient}
kuncar@51374
   667
    val (rty, qty) = quot_thm_rty_qty quot_thm
kuncar@51374
   668
    val qty_full_name = (fst o dest_Type) qty
kuncar@51374
   669
    val qty_name = (Binding.name o Long_Name.base_name) qty_full_name
kuncar@47545
   670
    fun qualify suffix = Binding.qualified true suffix qty_name
kuncar@51374
   671
    val opt_reflp_thm = 
kuncar@51374
   672
      case typedef_set of
wenzelm@56257
   673
        Const (@{const_name top}, _) => 
kuncar@51374
   674
          SOME ((typedef_thm RS @{thm UNIV_typedef_to_equivp}) RS @{thm equivp_reflp2})
kuncar@51374
   675
        | _ =>  NONE
kuncar@51956
   676
    val dom_thm = get_Domainp_thm quot_thm
kuncar@47308
   677
kuncar@60225
   678
    fun setup_transfer_rules_nonpar notes =
kuncar@51374
   679
      let
kuncar@60225
   680
        val notes1 =
kuncar@51374
   681
          case opt_reflp_thm of
kuncar@51374
   682
            SOME reflp_thm =>
kuncar@51374
   683
              let 
kuncar@51374
   684
                val thms =
kuncar@60225
   685
                  [("id_abs_transfer",@{thms Quotient_id_abs_transfer}, @{attributes [transfer_rule]}),
kuncar@60225
   686
                   ("left_total",     @{thms Quotient_left_total},      @{attributes [transfer_rule]}),
kuncar@60225
   687
                   ("bi_total",       @{thms Quotient_bi_total},        @{attributes [transfer_rule]})]
kuncar@51374
   688
              in
kuncar@60225
   689
                map_thms qualify (fn thm => [quot_thm, reflp_thm] MRSL thm) thms
kuncar@51374
   690
              end
kuncar@51374
   691
            | NONE =>
kuncar@60225
   692
              map_thms qualify I [("domain", [dom_thm], @{attributes [transfer_domain_rule]})]
kuncar@51374
   693
        val thms = 
kuncar@60225
   694
          [("rep_transfer", @{thms typedef_rep_transfer}, @{attributes [transfer_rule]}),
kuncar@60225
   695
           ("left_unique",  @{thms typedef_left_unique},  @{attributes [transfer_rule]}),
kuncar@60225
   696
           ("right_unique", @{thms typedef_right_unique}, @{attributes [transfer_rule]}), 
kuncar@60225
   697
           ("right_total",  @{thms typedef_right_total},  @{attributes [transfer_rule]}),
kuncar@60225
   698
           ("bi_unique",    @{thms typedef_bi_unique},    @{attributes [transfer_rule]})]
kuncar@60225
   699
      in                                               
kuncar@60225
   700
        map_thms qualify (fn thm => [typedef_thm, T_def] MRSL thm) thms @ notes1 @ notes
kuncar@51374
   701
      end
kuncar@51374
   702
kuncar@60225
   703
    fun setup_transfer_rules_par lthy notes =
kuncar@51374
   704
      let
kuncar@51956
   705
        val pcrel_info = (the (get_pcrel_info lthy qty_full_name))
kuncar@51956
   706
        val pcrel_def = #pcrel_def pcrel_info
kuncar@51956
   707
kuncar@60225
   708
        val notes1 =
kuncar@51374
   709
          case opt_reflp_thm of
kuncar@51374
   710
            SOME reflp_thm =>
kuncar@51374
   711
              let
kuncar@56518
   712
                val left_total = ([quot_thm, reflp_thm] MRSL @{thm Quotient_left_total})
kuncar@51956
   713
                val bi_total = ([quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total})
kuncar@56518
   714
                val domain_thms = parametrize_total_domain left_total pcrel_def lthy
kuncar@56518
   715
                val left_total = parametrize_class_constraint lthy pcrel_def left_total
kuncar@51956
   716
                val bi_total = parametrize_class_constraint lthy pcrel_def bi_total
kuncar@51374
   717
                val id_abs_transfer = generate_parametric_id lthy rty
kuncar@51374
   718
                  (Lifting_Term.parametrize_transfer_rule lthy
kuncar@51374
   719
                    ([quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer}))
kuncar@51374
   720
                val thms = 
kuncar@60225
   721
                  [("left_total",     [left_total],      @{attributes [transfer_rule]}),
kuncar@60225
   722
                   ("bi_total",       [bi_total],        @{attributes [transfer_rule]}),
kuncar@60225
   723
                   ("id_abs_transfer",[id_abs_transfer], @{attributes [transfer_rule]})]              
kuncar@51374
   724
              in
kuncar@60225
   725
                map_thms qualify I thms @ map_thms qualify I domain_thms
kuncar@51374
   726
              end
kuncar@51374
   727
            | NONE =>
kuncar@51374
   728
              let
kuncar@51956
   729
                val thms = parametrize_domain dom_thm pcrel_info lthy
kuncar@51374
   730
              in
kuncar@60225
   731
                map_thms qualify I thms
kuncar@51374
   732
              end
kuncar@51956
   733
              
kuncar@60225
   734
        val notes2 = map_thms qualify (fn thm => generate_parametric_id lthy rty 
kuncar@60225
   735
            (Lifting_Term.parametrize_transfer_rule lthy ([typedef_thm, T_def] MRSL thm)))
kuncar@60225
   736
          [("rep_transfer", @{thms typedef_rep_transfer}, @{attributes [transfer_rule]})];
kuncar@60225
   737
        val notes3 =
kuncar@60225
   738
          map_thms qualify
kuncar@60225
   739
          (fn thm => parametrize_class_constraint lthy pcrel_def ([typedef_thm, T_def] MRSL thm))
kuncar@60225
   740
          [("left_unique",  @{thms typedef_left_unique}, @{attributes [transfer_rule]}),
kuncar@60225
   741
           ("right_unique", @{thms typedef_right_unique},@{attributes [transfer_rule]}),
kuncar@60225
   742
           ("bi_unique",    @{thms typedef_bi_unique},   @{attributes [transfer_rule]}),
kuncar@60225
   743
           ("right_total",  @{thms typedef_right_total}, @{attributes [transfer_rule]})]
kuncar@51374
   744
      in
kuncar@60225
   745
        notes3 @ notes2 @ notes1 @ notes
kuncar@51374
   746
      end
kuncar@51374
   747
kuncar@60225
   748
    val notes1 = [(Binding.prefix_name "Quotient_" qty_name, [quot_thm], [])]
kuncar@51374
   749
kuncar@60225
   750
    fun setup_rules lthy = 
kuncar@60225
   751
      let
kuncar@60225
   752
        val thms =  if is_some (get_pcrel_info lthy qty_full_name) 
kuncar@60225
   753
          then setup_transfer_rules_par lthy notes1 else setup_transfer_rules_nonpar notes1
kuncar@60225
   754
      in
kuncar@60225
   755
        notes (#notes config) thms lthy
kuncar@60225
   756
      end
kuncar@47308
   757
  in
kuncar@51374
   758
    lthy
kuncar@60225
   759
      |> setup_lifting_infr config quot_thm opt_reflp_thm
kuncar@60225
   760
      ||> setup_rules
kuncar@47308
   761
  end
kuncar@47308
   762
haftmann@59487
   763
fun setup_lifting_cmd xthm opt_reflp_xthm opt_par_xthm lthy =
kuncar@47521
   764
  let 
kuncar@47521
   765
    val input_thm = singleton (Attrib.eval_thms lthy) xthm
wenzelm@59582
   766
    val input_term = (HOLogic.dest_Trueprop o Thm.prop_of) input_thm
kuncar@47566
   767
      handle TERM _ => error "Unsupported type of a theorem. Only Quotient or type_definition are supported."
kuncar@47566
   768
kuncar@47566
   769
    fun sanity_check_reflp_thm reflp_thm = 
kuncar@47566
   770
      let
wenzelm@59582
   771
        val reflp_tm = (HOLogic.dest_Trueprop o Thm.prop_of) reflp_thm
kuncar@47566
   772
          handle TERM _ => error "Invalid form of the reflexivity theorem. Use \"reflp R\"."
kuncar@47566
   773
      in
kuncar@47566
   774
        case reflp_tm of
kuncar@47566
   775
          Const (@{const_name reflp}, _) $ _ => ()
kuncar@47566
   776
          | _ => error "Invalid form of the reflexivity theorem. Use \"reflp R\"."
kuncar@47566
   777
      end
kuncar@55487
   778
      
kuncar@55487
   779
    fun check_qty qty = if not (is_Type qty) 
kuncar@55487
   780
          then error "The abstract type must be a type constructor."
kuncar@55487
   781
          else ()
kuncar@60225
   782
   
kuncar@47566
   783
    fun setup_quotient () = 
kuncar@51374
   784
      let
kuncar@51374
   785
        val opt_reflp_thm = Option.map (singleton (Attrib.eval_thms lthy)) opt_reflp_xthm
kuncar@51374
   786
        val _ = if is_some opt_reflp_thm then sanity_check_reflp_thm (the opt_reflp_thm) else ()
kuncar@51374
   787
        val opt_par_thm = Option.map (singleton (Attrib.eval_thms lthy)) opt_par_xthm
kuncar@55487
   788
        val _ = check_qty (snd (quot_thm_rty_qty input_thm))
kuncar@51374
   789
      in
kuncar@60231
   790
        setup_by_quotient default_config input_thm opt_reflp_thm opt_par_thm lthy |> snd
kuncar@51374
   791
      end
kuncar@47566
   792
kuncar@47566
   793
    fun setup_typedef () = 
kuncar@55487
   794
      let
kuncar@55487
   795
        val qty = (range_type o fastype_of o hd o get_args 2) input_term
kuncar@55487
   796
        val _ = check_qty qty
kuncar@55487
   797
      in
kuncar@55487
   798
        case opt_reflp_xthm of
kuncar@55487
   799
          SOME _ => error "The reflexivity theorem cannot be specified if the type_definition theorem is used."
kuncar@55487
   800
          | NONE => (
kuncar@55487
   801
            case opt_par_xthm of
kuncar@55487
   802
              SOME _ => error "The parametricity theorem cannot be specified if the type_definition theorem is used."
kuncar@60231
   803
              | NONE => setup_by_typedef_thm default_config input_thm lthy |> snd
kuncar@55487
   804
          )
kuncar@55487
   805
      end
kuncar@47521
   806
  in
kuncar@47521
   807
    case input_term of
kuncar@47566
   808
      (Const (@{const_name Quotient}, _) $ _ $ _ $ _ $ _) => setup_quotient ()
kuncar@47566
   809
      | (Const (@{const_name type_definition}, _) $ _ $ _ $ _) => setup_typedef ()
kuncar@47521
   810
      | _ => error "Unsupported type of a theorem. Only Quotient or type_definition are supported."
kuncar@47521
   811
  end
kuncar@47308
   812
kuncar@47308
   813
val _ = 
wenzelm@59936
   814
  Outer_Syntax.local_theory @{command_keyword setup_lifting}
wenzelm@50214
   815
    "setup lifting infrastructure" 
haftmann@59487
   816
      (Parse.xthm -- Scan.option Parse.xthm 
wenzelm@58028
   817
      -- Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse.xthm) >> 
haftmann@59487
   818
        (fn ((xthm, opt_reflp_xthm), opt_par_xthm) => 
haftmann@59487
   819
          setup_lifting_cmd xthm opt_reflp_xthm opt_par_xthm))
kuncar@53651
   820
kuncar@53651
   821
(* restoring lifting infrastructure *)
kuncar@53651
   822
kuncar@53651
   823
local
kuncar@53651
   824
  exception PCR_ERROR of Pretty.T list
kuncar@53651
   825
in
kuncar@53651
   826
kuncar@53651
   827
fun lifting_restore_sanity_check ctxt (qinfo:Lifting_Info.quotient) =
kuncar@53651
   828
  let
kuncar@53651
   829
    val quot_thm = (#quot_thm qinfo)
kuncar@53651
   830
    val _ = quot_thm_sanity_check ctxt quot_thm
kuncar@53651
   831
    val pcr_info_err =
kuncar@53651
   832
      (case #pcr_info qinfo of
kuncar@53651
   833
        SOME pcr => 
kuncar@53651
   834
          let
kuncar@53651
   835
            val pcrel_def = #pcrel_def pcr
kuncar@53651
   836
            val pcr_cr_eq = #pcr_cr_eq pcr
wenzelm@59582
   837
            val (def_lhs, _) = Logic.dest_equals (Thm.prop_of pcrel_def)
kuncar@53651
   838
              handle TERM _ => raise PCR_ERROR [Pretty.block 
kuncar@53651
   839
                    [Pretty.str "The pcr definiton theorem is not a plain meta equation:",
kuncar@53651
   840
                    Pretty.brk 1,
kuncar@53651
   841
                    Display.pretty_thm ctxt pcrel_def]]
kuncar@53651
   842
            val pcr_const_def = head_of def_lhs
wenzelm@59582
   843
            val (eq_lhs, eq_rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of pcr_cr_eq))
kuncar@53651
   844
              handle TERM _ => raise PCR_ERROR [Pretty.block 
kuncar@53651
   845
                    [Pretty.str "The pcr_cr equation theorem is not a plain equation:",
kuncar@53651
   846
                    Pretty.brk 1,
kuncar@53651
   847
                    Display.pretty_thm ctxt pcr_cr_eq]]
kuncar@53651
   848
            val (pcr_const_eq, eqs) = strip_comb eq_lhs
wenzelm@56257
   849
            fun is_eq (Const (@{const_name HOL.eq}, _)) = true
kuncar@53651
   850
              | is_eq _ = false
kuncar@53651
   851
            fun eq_Const (Const (name1, _)) (Const (name2, _)) = (name1 = name2)
kuncar@53651
   852
              | eq_Const _ _ = false
kuncar@53651
   853
            val all_eqs = if not (forall is_eq eqs) then 
kuncar@53651
   854
              [Pretty.block
kuncar@53651
   855
                    [Pretty.str "Arguments of the lhs of the pcr_cr equation theorem are not only equalities:",
kuncar@53651
   856
                    Pretty.brk 1,
kuncar@53651
   857
                    Display.pretty_thm ctxt pcr_cr_eq]]
kuncar@53651
   858
              else []
kuncar@53651
   859
            val pcr_consts_not_equal = if not (eq_Const pcr_const_def pcr_const_eq) then
kuncar@53651
   860
              [Pretty.block
kuncar@53651
   861
                    [Pretty.str "Parametrized correspondence relation constants in pcr_def and pcr_cr_eq are not equal:",
kuncar@53651
   862
                    Pretty.brk 1,
kuncar@53651
   863
                    Syntax.pretty_term ctxt pcr_const_def,
kuncar@53651
   864
                    Pretty.brk 1,
kuncar@53651
   865
                    Pretty.str "vs.",
kuncar@53651
   866
                    Pretty.brk 1,
kuncar@53651
   867
                    Syntax.pretty_term ctxt pcr_const_eq]]
kuncar@53651
   868
              else []
kuncar@53651
   869
            val crel = quot_thm_crel quot_thm
kuncar@53651
   870
            val cr_consts_not_equal = if not (eq_Const crel eq_rhs) then
kuncar@53651
   871
              [Pretty.block
kuncar@53651
   872
                    [Pretty.str "Correspondence relation constants in the Quotient theorem and pcr_cr_eq are not equal:",
kuncar@53651
   873
                    Pretty.brk 1,
kuncar@53651
   874
                    Syntax.pretty_term ctxt crel,
kuncar@53651
   875
                    Pretty.brk 1,
kuncar@53651
   876
                    Pretty.str "vs.",
kuncar@53651
   877
                    Pretty.brk 1,
kuncar@53651
   878
                    Syntax.pretty_term ctxt eq_rhs]]
kuncar@53651
   879
              else []
kuncar@53651
   880
          in
kuncar@53651
   881
            all_eqs @ pcr_consts_not_equal @ cr_consts_not_equal
kuncar@53651
   882
          end
kuncar@53651
   883
        | NONE => [])
kuncar@53651
   884
    val errs = pcr_info_err
kuncar@53651
   885
  in
kuncar@53651
   886
    if null errs then () else raise PCR_ERROR errs
kuncar@53651
   887
  end
kuncar@53651
   888
  handle PCR_ERROR errs => error (cat_lines (["Sanity check failed:"] 
kuncar@53651
   889
                                            @ (map (Pretty.string_of o Pretty.item o single) errs)))
kuncar@53651
   890
end
kuncar@53651
   891
kuncar@54335
   892
(*
kuncar@54335
   893
  Registers the data in qinfo in the Lifting infrastructure.
kuncar@54335
   894
*)
kuncar@54335
   895
kuncar@53651
   896
fun lifting_restore qinfo ctxt =
kuncar@53651
   897
  let
kuncar@53651
   898
    val _ = lifting_restore_sanity_check (Context.proof_of ctxt) qinfo
kuncar@53651
   899
    val (_, qty) = quot_thm_rty_qty (#quot_thm qinfo)
kuncar@53651
   900
    val qty_full_name = (fst o dest_Type) qty
kuncar@53651
   901
    val stored_qinfo = Lifting_Info.lookup_quotients (Context.proof_of ctxt) qty_full_name
kuncar@53651
   902
  in
kuncar@53651
   903
    if is_some (stored_qinfo) andalso not (Lifting_Info.quotient_eq (qinfo, (the stored_qinfo)))
kuncar@53651
   904
      then error (Pretty.string_of 
kuncar@53651
   905
        (Pretty.block
kuncar@53651
   906
          [Pretty.str "Lifting is already setup for the type",
kuncar@53651
   907
           Pretty.brk 1,
kuncar@53651
   908
           Pretty.quote (Syntax.pretty_typ (Context.proof_of ctxt) qty)]))
kuncar@53651
   909
      else Lifting_Info.update_quotients qty_full_name qinfo ctxt
kuncar@53651
   910
  end
kuncar@53651
   911
kuncar@53651
   912
val parse_opt_pcr =
kuncar@53651
   913
  Scan.optional (Attrib.thm -- Attrib.thm >> 
kuncar@53651
   914
    (fn (pcrel_def, pcr_cr_eq) => SOME {pcrel_def = pcrel_def, pcr_cr_eq = pcr_cr_eq})) NONE
kuncar@53651
   915
kuncar@53651
   916
val lifting_restore_attribute_setup =
kuncar@53651
   917
  Attrib.setup @{binding lifting_restore}
kuncar@53651
   918
    ((Attrib.thm -- parse_opt_pcr) >>
kuncar@53651
   919
      (fn (quot_thm, opt_pcr) =>
kuncar@53651
   920
        let val qinfo = { quot_thm = quot_thm, pcr_info = opt_pcr}
kuncar@53651
   921
        in Thm.declaration_attribute (K (lifting_restore qinfo)) end))
kuncar@53651
   922
    "restoring lifting infrastructure"
kuncar@53651
   923
kuncar@53651
   924
val _ = Theory.setup lifting_restore_attribute_setup 
kuncar@53651
   925
kuncar@53651
   926
fun lifting_restore_internal bundle_name ctxt = 
kuncar@53651
   927
  let 
kuncar@53651
   928
    val restore_info = Lifting_Info.lookup_restore_data (Context.proof_of ctxt) bundle_name
kuncar@53651
   929
  in
kuncar@53651
   930
    case restore_info of
kuncar@53651
   931
      SOME restore_info =>
kuncar@53651
   932
        ctxt 
kuncar@53651
   933
        |> lifting_restore (#quotient restore_info)
kuncar@53651
   934
        |> fold_rev Transfer.transfer_raw_add (Item_Net.content (#transfer_rules restore_info))
kuncar@53651
   935
      | NONE => ctxt
kuncar@53651
   936
  end
kuncar@53651
   937
kuncar@53651
   938
val lifting_restore_internal_attribute_setup =
kuncar@53651
   939
  Attrib.setup @{binding lifting_restore_internal}
wenzelm@59084
   940
    (Scan.lift Parse.cartouche >>
wenzelm@59084
   941
      (fn name => Thm.declaration_attribute (K (lifting_restore_internal name))))
kuncar@53651
   942
    "restoring lifting infrastructure; internal attribute; not meant to be used directly by regular users"
kuncar@53651
   943
kuncar@53651
   944
val _ = Theory.setup lifting_restore_internal_attribute_setup 
kuncar@53651
   945
kuncar@53651
   946
(* lifting_forget *)
kuncar@53651
   947
kuncar@53651
   948
val monotonicity_names = [@{const_name right_unique}, @{const_name left_unique}, @{const_name right_total},
kuncar@53651
   949
  @{const_name left_total}, @{const_name bi_unique}, @{const_name bi_total}]
kuncar@53651
   950
kuncar@53651
   951
fun fold_transfer_rel f (Const (@{const_name "Transfer.Rel"}, _) $ rel $ _ $ _) = f rel
kuncar@53651
   952
  | fold_transfer_rel f (Const (@{const_name "HOL.eq"}, _) $ 
kuncar@53651
   953
    (Const (@{const_name Domainp}, _) $ rel) $ _) = f rel
kuncar@53651
   954
  | fold_transfer_rel f (Const (name, _) $ rel) = 
kuncar@53651
   955
    if member op= monotonicity_names name then f rel else f @{term undefined}
kuncar@53651
   956
  | fold_transfer_rel f _ = f @{term undefined}
kuncar@53651
   957
kuncar@53651
   958
fun filter_transfer_rules_by_rel transfer_rel transfer_rules =
kuncar@53651
   959
  let
kuncar@53651
   960
    val transfer_rel_name = transfer_rel |> dest_Const |> fst;
kuncar@53651
   961
    fun has_transfer_rel thm = 
kuncar@53651
   962
      let
wenzelm@59582
   963
        val concl = thm |> Thm.concl_of |> HOLogic.dest_Trueprop
kuncar@53651
   964
      in
kuncar@53651
   965
        member op= (fold_transfer_rel (fn tm => Term.add_const_names tm []) concl) transfer_rel_name
kuncar@53651
   966
      end
kuncar@53651
   967
      handle TERM _ => false
kuncar@53651
   968
  in
kuncar@53651
   969
    filter has_transfer_rel transfer_rules
kuncar@53651
   970
  end
kuncar@53651
   971
kuncar@53651
   972
type restore_data = {quotient : Lifting_Info.quotient, transfer_rules: thm Item_Net.T}
kuncar@53651
   973
kuncar@53754
   974
fun get_transfer_rel (qinfo : Lifting_Info.quotient) =
kuncar@53651
   975
  let
wenzelm@59582
   976
    fun get_pcrel pcr_def = pcr_def |> Thm.concl_of |> Logic.dest_equals |> fst |> head_of
kuncar@53651
   977
  in
kuncar@53651
   978
    if is_some (#pcr_info qinfo) 
kuncar@53651
   979
      then get_pcrel (#pcrel_def (the (#pcr_info qinfo)))
kuncar@53651
   980
      else quot_thm_crel (#quot_thm qinfo)
kuncar@53651
   981
  end
kuncar@53651
   982
kuncar@53651
   983
fun pointer_of_bundle_name bundle_name ctxt =
kuncar@53651
   984
  let
wenzelm@56026
   985
    val bundle = Bundle.get_bundle_cmd ctxt bundle_name
kuncar@53651
   986
  in
kuncar@53651
   987
    case bundle of
kuncar@53651
   988
      [(_, [arg_src])] => 
wenzelm@56035
   989
        let
wenzelm@59084
   990
          val (name, _) = Token.syntax (Scan.lift Parse.cartouche) arg_src ctxt
wenzelm@56035
   991
            handle ERROR _ => error "The provided bundle is not a lifting bundle."
wenzelm@56035
   992
        in name end
kuncar@53651
   993
      | _ => error "The provided bundle is not a lifting bundle."
kuncar@53651
   994
  end
kuncar@53651
   995
kuncar@60226
   996
fun pointer_of_bundle_binding ctxt binding = Name_Space.full_name (Name_Space.naming_of 
kuncar@60226
   997
      (Context.Theory (Proof_Context.theory_of ctxt))) binding
kuncar@60226
   998
kuncar@53651
   999
fun lifting_forget pointer lthy =
kuncar@53651
  1000
  let
kuncar@53651
  1001
    fun get_transfer_rules_to_delete qinfo ctxt =
kuncar@53651
  1002
      let
kuncar@53754
  1003
        val transfer_rel = get_transfer_rel qinfo
kuncar@53651
  1004
      in
kuncar@53651
  1005
         filter_transfer_rules_by_rel transfer_rel (Transfer.get_transfer_raw ctxt)
kuncar@53651
  1006
      end
kuncar@53651
  1007
  in
kuncar@53651
  1008
    case Lifting_Info.lookup_restore_data lthy pointer of
kuncar@53651
  1009
      SOME restore_info =>
kuncar@53651
  1010
        let
kuncar@53651
  1011
          val qinfo = #quotient restore_info
kuncar@53651
  1012
          val quot_thm = #quot_thm qinfo
kuncar@53651
  1013
          val transfer_rules = get_transfer_rules_to_delete qinfo lthy
kuncar@53651
  1014
        in
kuncar@53651
  1015
          Local_Theory.declaration {syntax = false, pervasive = true}
kuncar@53651
  1016
            (K (fold (Transfer.transfer_raw_del) transfer_rules #> Lifting_Info.delete_quotients quot_thm))
kuncar@53651
  1017
            lthy
kuncar@53651
  1018
        end
kuncar@53651
  1019
      | NONE => error "The lifting bundle refers to non-existent restore data."
kuncar@53651
  1020
    end
kuncar@53651
  1021
    
kuncar@53651
  1022
kuncar@53651
  1023
fun lifting_forget_cmd bundle_name lthy = 
kuncar@53651
  1024
  lifting_forget (pointer_of_bundle_name bundle_name lthy) lthy
kuncar@53651
  1025
kuncar@53651
  1026
kuncar@53651
  1027
val _ =
wenzelm@59936
  1028
  Outer_Syntax.local_theory @{command_keyword lifting_forget} 
kuncar@53651
  1029
    "unsetup Lifting and Transfer for the given lifting bundle"
kuncar@53651
  1030
    (Parse.position Parse.xname >> (lifting_forget_cmd))
kuncar@53651
  1031
kuncar@53651
  1032
(* lifting_update *)
kuncar@53651
  1033
kuncar@53651
  1034
fun update_transfer_rules pointer lthy =
kuncar@53651
  1035
  let
kuncar@53754
  1036
    fun new_transfer_rules ({ quotient = qinfo, ... }:Lifting_Info.restore_data) lthy =
kuncar@53651
  1037
      let
kuncar@53651
  1038
        val transfer_rel = get_transfer_rel qinfo
kuncar@53651
  1039
        val transfer_rules = filter_transfer_rules_by_rel transfer_rel (Transfer.get_transfer_raw lthy)
kuncar@53651
  1040
      in
kuncar@53651
  1041
        fn phi => fold_rev 
kuncar@53651
  1042
          (Item_Net.update o Morphism.thm phi) transfer_rules Thm.full_rules
kuncar@53651
  1043
      end
kuncar@53651
  1044
  in
kuncar@53651
  1045
    case Lifting_Info.lookup_restore_data lthy pointer of
kuncar@53651
  1046
      SOME refresh_data => 
kuncar@53651
  1047
        Local_Theory.declaration {syntax = false, pervasive = true}
kuncar@53651
  1048
          (fn phi => Lifting_Info.add_transfer_rules_in_restore_data pointer 
kuncar@53651
  1049
            (new_transfer_rules refresh_data lthy phi)) lthy
kuncar@53651
  1050
      | NONE => error "The lifting bundle refers to non-existent restore data."
kuncar@53651
  1051
  end
kuncar@53651
  1052
kuncar@53651
  1053
fun lifting_update_cmd bundle_name lthy = 
kuncar@53651
  1054
  update_transfer_rules (pointer_of_bundle_name bundle_name lthy) lthy
kuncar@53651
  1055
kuncar@53651
  1056
val _ =
wenzelm@59936
  1057
  Outer_Syntax.local_theory @{command_keyword lifting_update}
kuncar@53651
  1058
    "add newly introduced transfer rules to a bundle storing the state of Lifting and Transfer"
kuncar@53651
  1059
    (Parse.position Parse.xname >> lifting_update_cmd)
kuncar@53651
  1060
kuncar@53651
  1061
end