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