src/HOL/Tools/Lifting/lifting_def_code_dt.ML
author wenzelm
Sun May 03 14:35:48 2015 +0200 (2015-05-03)
changeset 60239 755e11e2e15d
parent 60236 865741686926
child 60379 51d9dcd71ad7
permissions -rw-r--r--
make SML/NJ more happy;
kuncar@60229
     1
(*  Title:      HOL/Tools/Lifting/lifting_def_code_dt.ML
kuncar@60229
     2
    Author:     Ondrej Kuncar
kuncar@60229
     3
kuncar@60229
     4
Workaround that allows us to execute lifted constants that have
kuncar@60229
     5
as a return type a datatype containing a subtype; lift_definition command
kuncar@60229
     6
*)
kuncar@60229
     7
kuncar@60229
     8
signature LIFTING_DEF_CODE_DT =
kuncar@60229
     9
sig
kuncar@60229
    10
  type rep_isom_data
kuncar@60229
    11
  val isom_of_rep_isom_data: rep_isom_data -> term
kuncar@60229
    12
  val transfer_of_rep_isom_data: rep_isom_data -> thm
kuncar@60229
    13
  val bundle_name_of_rep_isom_data: rep_isom_data -> string
kuncar@60229
    14
  val pointer_of_rep_isom_data: rep_isom_data -> string
kuncar@60229
    15
kuncar@60229
    16
  type code_dt
kuncar@60229
    17
  val rty_of_code_dt: code_dt -> typ
kuncar@60229
    18
  val qty_of_code_dt: code_dt -> typ
kuncar@60229
    19
  val wit_of_code_dt: code_dt -> term
kuncar@60229
    20
  val wit_thm_of_code_dt: code_dt -> thm
kuncar@60229
    21
  val rep_isom_data_of_code_dt: code_dt -> rep_isom_data option
kuncar@60229
    22
  val morph_code_dt: morphism -> code_dt -> code_dt
kuncar@60229
    23
  val mk_witness_of_code_dt: typ -> code_dt -> term
kuncar@60229
    24
  val mk_rep_isom_of_code_dt: typ -> code_dt -> term option
kuncar@60229
    25
kuncar@60229
    26
  val code_dt_of: Proof.context -> typ * typ -> code_dt option
kuncar@60229
    27
  val code_dt_of_global: theory -> typ * typ -> code_dt option
kuncar@60229
    28
  val all_code_dt_of: Proof.context -> code_dt list
kuncar@60229
    29
  val all_code_dt_of_global: theory -> code_dt list
kuncar@60229
    30
kuncar@60229
    31
  type config_code_dt = { code_dt: bool, lift_config: Lifting_Def.config }
kuncar@60229
    32
  val default_config_code_dt: config_code_dt
kuncar@60229
    33
kuncar@60229
    34
  val add_lift_def_code_dt:
kuncar@60229
    35
    config_code_dt -> binding * mixfix -> typ -> term -> thm -> thm list -> local_theory ->
kuncar@60229
    36
      Lifting_Def.lift_def * local_theory
kuncar@60229
    37
kuncar@60229
    38
  val lift_def_code_dt:
kuncar@60229
    39
    config_code_dt -> binding * mixfix -> typ -> term -> (Proof.context -> tactic) -> thm list ->
kuncar@60229
    40
    local_theory -> Lifting_Def.lift_def * local_theory
kuncar@60229
    41
kuncar@60229
    42
  val lift_def_cmd:
kuncar@60229
    43
    string list * (binding * string option * mixfix) * string * (Facts.ref * Token.src list) list ->
kuncar@60229
    44
    local_theory -> Proof.state
kuncar@60229
    45
end
kuncar@60229
    46
kuncar@60229
    47
structure Lifting_Def_Code_Dt: LIFTING_DEF_CODE_DT =
kuncar@60229
    48
struct
kuncar@60231
    49
                                                                       
kuncar@60231
    50
open Ctr_Sugar_Util BNF_Util BNF_FP_Util BNF_FP_Def_Sugar Lifting_Def Lifting_Util
kuncar@60229
    51
kuncar@60231
    52
infix 0 MRSL
kuncar@60229
    53
kuncar@60229
    54
(** data structures **)
kuncar@60229
    55
kuncar@60229
    56
(* all type variables in qty are in rty *)
kuncar@60229
    57
datatype rep_isom_data = REP_ISOM of { isom: term, transfer: thm, bundle_name: string, pointer: string }
kuncar@60229
    58
fun isom_of_rep_isom_data (REP_ISOM rep_isom) = #isom rep_isom;
kuncar@60229
    59
fun transfer_of_rep_isom_data (REP_ISOM rep_isom) = #transfer rep_isom;
kuncar@60229
    60
fun bundle_name_of_rep_isom_data (REP_ISOM rep_isom) = #bundle_name rep_isom;
kuncar@60229
    61
fun pointer_of_rep_isom_data (REP_ISOM rep_isom) = #pointer rep_isom;
kuncar@60229
    62
kuncar@60229
    63
datatype code_dt = CODE_DT of { rty: typ, qty: typ, wit: term, wit_thm: thm,
kuncar@60229
    64
  rep_isom_data: rep_isom_data option };
kuncar@60229
    65
fun rty_of_code_dt (CODE_DT code_dt) = #rty code_dt;
kuncar@60229
    66
fun qty_of_code_dt (CODE_DT code_dt) = #qty code_dt;
kuncar@60229
    67
fun wit_of_code_dt (CODE_DT code_dt) = #wit code_dt;
kuncar@60229
    68
fun wit_thm_of_code_dt (CODE_DT code_dt) = #wit_thm code_dt;
kuncar@60229
    69
fun rep_isom_data_of_code_dt (CODE_DT code_dt) = #rep_isom_data code_dt;
kuncar@60232
    70
fun ty_alpha_equiv (T, U) = Type.raw_instance (T, U) andalso Type.raw_instance (U, T);
kuncar@60232
    71
fun code_dt_eq c = (ty_alpha_equiv o apply2 rty_of_code_dt) c 
kuncar@60232
    72
  andalso (ty_alpha_equiv o apply2 qty_of_code_dt) c;
kuncar@60229
    73
fun term_of_code_dt code_dt = code_dt |> `rty_of_code_dt ||> qty_of_code_dt |> HOLogic.mk_prodT
kuncar@60229
    74
  |> Net.encode_type |> single;
kuncar@60229
    75
kuncar@60229
    76
(* modulo renaming, typ must contain TVars *)
kuncar@60229
    77
fun is_code_dt_of_type (rty, qty) code_dt = code_dt |> `rty_of_code_dt ||> qty_of_code_dt
kuncar@60232
    78
  |> HOLogic.mk_prodT |> curry ty_alpha_equiv (HOLogic.mk_prodT (rty, qty));
kuncar@60229
    79
kuncar@60229
    80
fun mk_rep_isom_data isom transfer bundle_name pointer =
kuncar@60229
    81
  REP_ISOM { isom = isom, transfer = transfer, bundle_name = bundle_name, pointer = pointer}
kuncar@60229
    82
kuncar@60229
    83
fun mk_code_dt rty qty wit wit_thm rep_isom_data =
kuncar@60229
    84
  CODE_DT { rty = rty, qty = qty, wit = wit, wit_thm = wit_thm, rep_isom_data = rep_isom_data };
kuncar@60229
    85
kuncar@60229
    86
fun map_rep_isom_data f1 f2 f3 f4
kuncar@60229
    87
  (REP_ISOM { isom = isom, transfer = transfer, bundle_name = bundle_name, pointer = pointer }) =
kuncar@60229
    88
  REP_ISOM { isom = f1 isom, transfer = f2 transfer, bundle_name = f3 bundle_name, pointer = f4 pointer };
kuncar@60229
    89
kuncar@60229
    90
fun map_code_dt f1 f2 f3 f4 f5 f6 f7 f8
kuncar@60229
    91
  (CODE_DT {rty = rty, qty = qty, wit = wit, wit_thm = wit_thm, rep_isom_data = rep_isom_data}) =
kuncar@60229
    92
  CODE_DT {rty = f1 rty, qty = f2 qty, wit = f3 wit, wit_thm = f4 wit_thm,
kuncar@60229
    93
    rep_isom_data = Option.map (map_rep_isom_data f5 f6 f7 f8) rep_isom_data};
kuncar@60229
    94
kuncar@60229
    95
fun update_rep_isom isom transfer binding pointer i = mk_code_dt (rty_of_code_dt i) (qty_of_code_dt i)
kuncar@60229
    96
  (wit_of_code_dt i) (wit_thm_of_code_dt i) (SOME (mk_rep_isom_data isom transfer binding pointer))
kuncar@60229
    97
kuncar@60229
    98
fun morph_code_dt phi =
kuncar@60229
    99
  let
kuncar@60229
   100
    val mty = Morphism.typ phi
kuncar@60229
   101
    val mterm = Morphism.term phi
kuncar@60229
   102
    val mthm = Morphism.thm phi
kuncar@60229
   103
  in
kuncar@60229
   104
    map_code_dt mty mty mterm mthm mterm mthm I I
kuncar@60229
   105
  end
kuncar@60229
   106
kuncar@60229
   107
val transfer_code_dt = morph_code_dt o Morphism.transfer_morphism;
kuncar@60229
   108
kuncar@60229
   109
structure Data = Generic_Data
kuncar@60229
   110
(
kuncar@60229
   111
  type T = code_dt Item_Net.T
kuncar@60229
   112
  val empty = Item_Net.init code_dt_eq term_of_code_dt
kuncar@60229
   113
  val extend = I
kuncar@60229
   114
  val merge = Item_Net.merge
kuncar@60229
   115
);
kuncar@60229
   116
kuncar@60229
   117
fun code_dt_of_generic context (rty, qty) =
kuncar@60229
   118
  let
kuncar@60229
   119
    val typ = HOLogic.mk_prodT (rty, qty)
kuncar@60229
   120
    val prefiltred = Item_Net.retrieve_matching (Data.get context) (Net.encode_type typ)
kuncar@60229
   121
  in
kuncar@60229
   122
    prefiltred |> filter (is_code_dt_of_type (rty, qty))
kuncar@60229
   123
    |> map (transfer_code_dt (Context.theory_of context)) |> find_first (fn _ => true)
kuncar@60229
   124
  end;
kuncar@60229
   125
kuncar@60229
   126
fun code_dt_of ctxt (rty, qty) =
kuncar@60229
   127
  let
kuncar@60229
   128
    val sch_rty = Logic.type_map (singleton (Variable.polymorphic ctxt)) rty
kuncar@60229
   129
    val sch_qty = Logic.type_map (singleton (Variable.polymorphic ctxt)) qty
kuncar@60229
   130
  in
kuncar@60229
   131
    code_dt_of_generic (Context.Proof ctxt) (sch_rty, sch_qty)
kuncar@60229
   132
  end;
kuncar@60229
   133
kuncar@60229
   134
fun code_dt_of_global thy (rty, qty) =
kuncar@60229
   135
  let
kuncar@60229
   136
    val sch_rty = Logic.varifyT_global rty
kuncar@60229
   137
    val sch_qty = Logic.varifyT_global qty
kuncar@60229
   138
  in
kuncar@60229
   139
    code_dt_of_generic (Context.Theory thy) (sch_rty, sch_qty)
kuncar@60229
   140
  end;
kuncar@60229
   141
kuncar@60229
   142
fun all_code_dt_of_generic context =
kuncar@60229
   143
    Item_Net.content (Data.get context) |> map (transfer_code_dt (Context.theory_of context));
kuncar@60229
   144
kuncar@60229
   145
val all_code_dt_of = all_code_dt_of_generic o Context.Proof;
kuncar@60229
   146
val all_code_dt_of_global = all_code_dt_of_generic o Context.Theory;
kuncar@60229
   147
kuncar@60229
   148
fun update_code_dt code_dt =
kuncar@60229
   149
  Local_Theory.declaration {syntax = false, pervasive = true}
kuncar@60229
   150
    (fn phi => Data.map (Item_Net.update (morph_code_dt phi code_dt)));
kuncar@60229
   151
kuncar@60229
   152
fun mk_match_of_code_dt qty code_dt = Vartab.empty |> Type.raw_match (qty_of_code_dt code_dt, qty)
kuncar@60229
   153
  |> Vartab.dest |> map (fn (x, (S, T)) => (TVar (x, S), T));
kuncar@60229
   154
kuncar@60229
   155
fun mk_witness_of_code_dt qty code_dt =
kuncar@60229
   156
  Term.subst_atomic_types (mk_match_of_code_dt qty code_dt) (wit_of_code_dt code_dt)
kuncar@60229
   157
kuncar@60229
   158
fun mk_rep_isom_of_code_dt qty code_dt = Option.map
kuncar@60229
   159
  (isom_of_rep_isom_data #> Term.subst_atomic_types (mk_match_of_code_dt qty code_dt))
kuncar@60229
   160
    (rep_isom_data_of_code_dt code_dt)
kuncar@60229
   161
kuncar@60229
   162
kuncar@60229
   163
(** unique name for a type **)
kuncar@60229
   164
kuncar@60229
   165
fun var_name name sort = if sort = @{sort "{type}"} orelse sort = [] then ["x" ^ name]
kuncar@60229
   166
  else "x" ^ name :: "x_" :: sort @ ["x_"];
kuncar@60229
   167
kuncar@60229
   168
fun concat_Tnames (Type (name, ts)) = name :: maps concat_Tnames ts
kuncar@60229
   169
  | concat_Tnames (TFree (name, sort)) = var_name name sort
kuncar@60229
   170
  | concat_Tnames (TVar ((name, _), sort)) = var_name name sort;
kuncar@60229
   171
kuncar@60229
   172
fun unique_Tname (rty, qty) =
kuncar@60229
   173
  let
kuncar@60229
   174
    val Tnames = map Long_Name.base_name (concat_Tnames rty @ ["x_x"] @ concat_Tnames qty);
kuncar@60229
   175
  in
kuncar@60229
   176
    fold (Binding.qualify false) (tl Tnames) (Binding.name (hd Tnames))
kuncar@60229
   177
  end;
kuncar@60229
   178
kuncar@60229
   179
(** witnesses **)
kuncar@60229
   180
kuncar@60229
   181
fun mk_undefined T = Const (@{const_name undefined}, T);
kuncar@60229
   182
kuncar@60229
   183
fun mk_witness quot_thm =
kuncar@60229
   184
  let
kuncar@60229
   185
    val wit_thm = quot_thm RS @{thm type_definition_Quotient_not_empty_witness}
kuncar@60229
   186
    val wit = quot_thm_rep quot_thm $ mk_undefined (quot_thm_rty_qty quot_thm |> snd)
kuncar@60229
   187
  in
kuncar@60229
   188
    (wit, wit_thm)
kuncar@60229
   189
  end
kuncar@60229
   190
kuncar@60229
   191
(** config **)
kuncar@60229
   192
kuncar@60229
   193
type config_code_dt = { code_dt: bool, lift_config: config }
kuncar@60229
   194
val default_config_code_dt = { code_dt = false, lift_config = default_config }
kuncar@60229
   195
kuncar@60229
   196
kuncar@60229
   197
(** Main code **)
kuncar@60229
   198
kuncar@60229
   199
val ld_no_notes = { notes = false }
kuncar@60229
   200
kuncar@60229
   201
fun comp_lift_error _ _ = error "Composition of abstract types has not been implemented yet."
kuncar@60229
   202
kuncar@60229
   203
fun lift qty (quot_thm, (lthy, rel_eq_onps)) =
kuncar@60229
   204
  let
kuncar@60229
   205
    val quot_thm = Lifting_Term.force_qty_type lthy qty quot_thm
kuncar@60229
   206
    val (rty, qty) = quot_thm_rty_qty quot_thm;
kuncar@60229
   207
  in
kuncar@60229
   208
    if is_none (code_dt_of lthy (rty, qty)) then
kuncar@60229
   209
      let
kuncar@60229
   210
        val (wit, wit_thm) = (mk_witness quot_thm
kuncar@60229
   211
          handle THM _ => error ("code_dt: " ^ quote (Tname qty) ^ " was not defined as a subtype."))
kuncar@60229
   212
        val code_dt = mk_code_dt rty qty wit wit_thm NONE
kuncar@60229
   213
      in
kuncar@60229
   214
        (quot_thm, (update_code_dt code_dt lthy |> Local_Theory.restore, rel_eq_onps))
kuncar@60229
   215
      end
kuncar@60229
   216
    else
kuncar@60229
   217
      (quot_thm, (lthy, rel_eq_onps))
kuncar@60229
   218
  end;
kuncar@60229
   219
kuncar@60229
   220
fun case_tac rule ctxt i st =
kuncar@60229
   221
  (Subgoal.FOCUS_PARAMS (fn {params, ...} => HEADGOAL(rtac
kuncar@60229
   222
    (Ctr_Sugar_Util.cterm_instantiate_pos [SOME (params |> hd |> snd)] rule))) ctxt i st);
kuncar@60229
   223
kuncar@60229
   224
fun bundle_name_of_bundle_binding binding phi context  =
kuncar@60229
   225
  Name_Space.full_name (Name_Space.naming_of context) (Morphism.binding phi binding);
kuncar@60229
   226
kuncar@60229
   227
fun prove_schematic_quot_thm actions ctxt = Lifting_Term.prove_schematic_quot_thm actions
kuncar@60229
   228
 (Lifting_Info.get_quotients ctxt) ctxt
kuncar@60229
   229
kuncar@60229
   230
fun prove_code_dt (rty, qty) lthy =
kuncar@60229
   231
  let
kuncar@60229
   232
    val (fold_quot_thm: (local_theory * thm list) Lifting_Term.fold_quot_thm) =
kuncar@60229
   233
      { constr = constr, lift = lift, comp_lift = comp_lift_error };
kuncar@60229
   234
  in prove_schematic_quot_thm fold_quot_thm lthy (rty, qty) (lthy, []) |> snd end
kuncar@60229
   235
and add_lift_def_code_dt config var qty rhs rsp_thm par_thms lthy =
kuncar@60229
   236
  let
kuncar@60229
   237
    fun binop_conv2 cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
kuncar@60229
   238
    fun ret_rel_conv conv ctm =
kuncar@60229
   239
      case (Thm.term_of ctm) of
kuncar@60229
   240
        Const (@{const_name "rel_fun"}, _) $ _ $ _ =>
kuncar@60229
   241
          binop_conv2 Conv.all_conv conv ctm
kuncar@60229
   242
        | _ => conv ctm
kuncar@60229
   243
    fun R_conv rel_eq_onps = Transfer.top_sweep_rewr_conv @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]}
kuncar@60229
   244
      then_conv Transfer.bottom_rewr_conv rel_eq_onps
kuncar@60229
   245
kuncar@60229
   246
    val (ret_lift_def, lthy) = add_lift_def (#lift_config config) var qty rhs rsp_thm par_thms lthy
kuncar@60229
   247
  in
kuncar@60230
   248
    if (not (#code_dt config) orelse (code_eq_of_lift_def ret_lift_def <> NONE_EQ)
kuncar@60230
   249
      andalso (code_eq_of_lift_def ret_lift_def <> UNKNOWN_EQ))
kuncar@60230
   250
      (* Let us try even in case of UNKNOWN_EQ. If this leads to problems, the user can always
kuncar@60230
   251
        say that they do not want this workaround. *)
kuncar@60229
   252
    then  (ret_lift_def, lthy)
kuncar@60229
   253
    else
kuncar@60229
   254
      let
kuncar@60229
   255
        val lift_def = inst_of_lift_def lthy qty ret_lift_def
kuncar@60229
   256
        val rty = rty_of_lift_def lift_def
kuncar@60229
   257
        val rty_ret = body_type rty
kuncar@60229
   258
        val qty_ret = body_type qty
kuncar@60229
   259
kuncar@60229
   260
        val (lthy, rel_eq_onps) = prove_code_dt (rty_ret, qty_ret) lthy
kuncar@60229
   261
        val code_dt = code_dt_of lthy (rty_ret, qty_ret)
kuncar@60229
   262
      in
kuncar@60229
   263
        if is_none code_dt orelse is_none (rep_isom_data_of_code_dt (the code_dt)) then (ret_lift_def, lthy)
kuncar@60229
   264
        else
kuncar@60229
   265
          let
kuncar@60229
   266
            val code_dt = the code_dt
kuncar@60229
   267
            val rhs = dest_comb (rhs_of_lift_def lift_def) |> snd
kuncar@60229
   268
            val rep_isom_data = code_dt |> rep_isom_data_of_code_dt |> the
kuncar@60235
   269
            val pointer = pointer_of_rep_isom_data rep_isom_data
kuncar@60235
   270
            val quot_active = 
kuncar@60235
   271
              Lifting_Info.lookup_restore_data lthy pointer |> the |> #quotient |> #quot_thm
kuncar@60235
   272
              |> Lifting_Info.lookup_quot_thm_quotients lthy |> is_some
kuncar@60229
   273
            val qty_code_dt_bundle_name = bundle_name_of_rep_isom_data rep_isom_data
kuncar@60229
   274
            val rep_isom = mk_rep_isom_of_code_dt qty_ret code_dt |> the
kuncar@60235
   275
            val lthy = if quot_active then lthy else Bundle.includes [qty_code_dt_bundle_name] lthy
kuncar@60229
   276
            fun qty_isom_of_rep_isom rep = rep |> dest_Const |> snd |> domain_type
kuncar@60229
   277
            val qty_isom = qty_isom_of_rep_isom rep_isom
kuncar@60229
   278
            val f'_var = (Binding.suffix_name "_aux" (fst var), NoSyn);
kuncar@60229
   279
            val f'_qty = strip_type qty |> fst |> rpair qty_isom |> op --->
kuncar@60229
   280
            val f'_rsp_rel = Lifting_Term.equiv_relation lthy (rty, f'_qty);
kuncar@60229
   281
            val rsp = rsp_thm_of_lift_def lift_def
kuncar@60231
   282
            val rel_eq_onps_conv = HOLogic.Trueprop_conv (Conv.fun2_conv (ret_rel_conv (R_conv rel_eq_onps)))
kuncar@60229
   283
            val rsp_norm = Conv.fconv_rule rel_eq_onps_conv rsp
kuncar@60229
   284
            val f'_rsp_goal = HOLogic.mk_Trueprop (f'_rsp_rel $ rhs $ rhs);
kuncar@60229
   285
            val f'_rsp = Goal.prove_sorry lthy [] [] f'_rsp_goal
kuncar@60229
   286
              (K (HEADGOAL (CONVERSION (rel_eq_onps_conv) THEN' rtac rsp_norm)))
kuncar@60229
   287
              |> Thm.close_derivation
kuncar@60229
   288
            val (f'_lift_def, lthy) = add_lift_def ld_no_notes f'_var f'_qty rhs f'_rsp [] lthy
kuncar@60229
   289
            val f'_lift_def = inst_of_lift_def lthy f'_qty f'_lift_def
kuncar@60229
   290
            val f'_lift_const = mk_lift_const_of_lift_def f'_qty f'_lift_def
kuncar@60229
   291
            val args_lthy = lthy
kuncar@60229
   292
            val (args, lthy) = mk_Frees "x" (binder_types qty) lthy
kuncar@60229
   293
            val f_alt_def_goal_lhs = list_comb (lift_const_of_lift_def lift_def, args);
kuncar@60229
   294
            val f_alt_def_goal_rhs = rep_isom $ list_comb (f'_lift_const, args);
kuncar@60229
   295
            val f_alt_def_goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (f_alt_def_goal_lhs, f_alt_def_goal_rhs));
kuncar@60229
   296
            fun f_alt_def_tac ctxt i =
kuncar@60229
   297
              EVERY' [Transfer.gen_frees_tac [] ctxt, DETERM o Transfer.transfer_tac true ctxt,
kuncar@60229
   298
                SELECT_GOAL (Local_Defs.unfold_tac ctxt [id_apply]), rtac refl] i;
kuncar@60229
   299
            val rep_isom_transfer = transfer_of_rep_isom_data rep_isom_data
kuncar@60229
   300
            val (_, transfer_lthy) = Proof_Context.note_thmss "" [((Binding.empty, []),
kuncar@60229
   301
              [([rep_isom_transfer], [Transfer.transfer_add])])] lthy
kuncar@60229
   302
            val f_alt_def = Goal.prove_sorry transfer_lthy [] [] f_alt_def_goal
kuncar@60229
   303
              (fn {context = ctxt, prems = _} => HEADGOAL (f_alt_def_tac ctxt))
kuncar@60229
   304
              |> Thm.close_derivation
kuncar@60229
   305
              |> singleton (Variable.export lthy args_lthy)
kuncar@60229
   306
            val lthy = args_lthy
kuncar@60229
   307
            val lthy =  lthy
kuncar@60229
   308
              |> Local_Theory.note ((Binding.empty, @{attributes [code]}), [f_alt_def])
kuncar@60229
   309
              |> snd
kuncar@60235
   310
              (* if processing a mutual datatype (there is a cycle!) the corresponding quotient 
kuncar@60235
   311
                 will be needed later and will be forgotten later *)
kuncar@60235
   312
              |> (if quot_active then I else Lifting_Setup.lifting_forget pointer)
kuncar@60229
   313
          in
kuncar@60229
   314
            (ret_lift_def, lthy)
kuncar@60229
   315
          end
kuncar@60229
   316
       end
kuncar@60229
   317
    end
kuncar@60229
   318
and mk_rep_isom qty_isom_bundle (rty, qty, qty_isom) lthy =
kuncar@60229
   319
  let
kuncar@60235
   320
    (* logical definition of qty qty_isom isomorphism *) 
kuncar@60235
   321
    val uTname = unique_Tname (rty, qty)
kuncar@60235
   322
    fun eq_onp_to_top_tac ctxt = SELECT_GOAL (Local_Defs.unfold_tac ctxt 
kuncar@60235
   323
      (@{thm eq_onp_top_eq_eq[symmetric]} :: Lifting_Info.get_relator_eq_onp_rules ctxt))
kuncar@60235
   324
    fun lift_isom_tac ctxt = HEADGOAL (eq_onp_to_top_tac ctxt
kuncar@60235
   325
      THEN' (rtac @{thm id_transfer}));
kuncar@60235
   326
kuncar@60235
   327
    val (rep_isom_lift_def, lthy) = lift_def ld_no_notes (Binding.qualified true "Rep_isom" uTname, NoSyn)
kuncar@60235
   328
      (qty_isom --> qty) (HOLogic.id_const rty) lift_isom_tac [] lthy
kuncar@60235
   329
      |> apfst (inst_of_lift_def lthy (qty_isom --> qty));
kuncar@60235
   330
    val (abs_isom, lthy) = lift_def ld_no_notes (Binding.qualified true "Abs_isom" uTname, NoSyn)
kuncar@60235
   331
      (qty --> qty_isom) (HOLogic.id_const rty) lift_isom_tac [] lthy
kuncar@60235
   332
      |> apfst (mk_lift_const_of_lift_def (qty --> qty_isom));
kuncar@60235
   333
    val rep_isom = lift_const_of_lift_def rep_isom_lift_def
kuncar@60235
   334
kuncar@60235
   335
    val pointer = Lifting_Setup.pointer_of_bundle_binding lthy qty_isom_bundle
kuncar@60235
   336
    fun code_dt phi context = code_dt_of lthy (rty, qty) |> the |>
kuncar@60235
   337
      update_rep_isom rep_isom (transfer_rules_of_lift_def rep_isom_lift_def |> hd)
kuncar@60235
   338
       (bundle_name_of_bundle_binding qty_isom_bundle phi context) pointer;
kuncar@60235
   339
    val lthy = lthy  
kuncar@60235
   340
      |> Local_Theory.declaration {syntax = false, pervasive = true}
kuncar@60235
   341
        (fn phi => fn context => Data.map (Item_Net.update (morph_code_dt phi (code_dt phi context))) context)
kuncar@60235
   342
      |> Local_Theory.restore
kuncar@60235
   343
kuncar@60235
   344
    (* in order to make the qty qty_isom isomorphism executable we have to define discriminators 
kuncar@60235
   345
      and selectors for qty_isom *)
kuncar@60229
   346
    val (rty_name, typs) = dest_Type rty
kuncar@60229
   347
    val (_, qty_typs) = dest_Type qty
kuncar@60229
   348
    val fp = BNF_FP_Def_Sugar.fp_sugar_of lthy rty_name
kuncar@60229
   349
    val fp = if is_some fp then the fp
kuncar@60229
   350
      else error ("code_dt: " ^ quote rty_name ^ " is not a datatype.")
kuncar@60229
   351
    val ctr_sugar = fp |> #fp_ctr_sugar |> #ctr_sugar
kuncar@60229
   352
    val ctrs = map (Ctr_Sugar.mk_ctr typs) (#ctrs ctr_sugar);
kuncar@60229
   353
    val qty_ctrs = map (Ctr_Sugar.mk_ctr qty_typs) (#ctrs ctr_sugar);
kuncar@60229
   354
    val ctr_Tss = map (dest_Const #> snd #> binder_types) ctrs;
kuncar@60229
   355
    val qty_ctr_Tss = map (dest_Const #> snd #> binder_types) qty_ctrs;
kuncar@60229
   356
kuncar@60229
   357
    val n = length ctrs;
kuncar@60229
   358
    val ks = 1 upto n;
kuncar@60229
   359
    val (xss, _) = mk_Freess "x" ctr_Tss lthy;
kuncar@60229
   360
kuncar@60229
   361
    fun sel_retT (rty' as Type (s, rtys'), qty' as Type (s', qtys')) =
kuncar@60229
   362
        if (rty', qty') = (rty, qty) then qty_isom else (if s = s'
kuncar@60229
   363
          then Type (s, map sel_retT (rtys' ~~ qtys')) else qty')
kuncar@60229
   364
      | sel_retT (_, qty') = qty';
kuncar@60229
   365
kuncar@60233
   366
    val sel_retTs = map2 (map2 (sel_retT oo pair)) ctr_Tss qty_ctr_Tss
kuncar@60233
   367
kuncar@60233
   368
    fun lazy_prove_code_dt (rty, qty) lthy =
kuncar@60233
   369
      if is_none (code_dt_of lthy (rty, qty)) then prove_code_dt (rty, qty) lthy |> fst else lthy;
kuncar@60233
   370
kuncar@60233
   371
    val lthy = fold2 (fold2 (lazy_prove_code_dt oo pair)) ctr_Tss sel_retTs lthy
kuncar@60233
   372
kuncar@60233
   373
    val sel_argss = @{map 4} (fn k => fn xs => @{map 2} (fn x => fn qty_ret => 
kuncar@60233
   374
      (k, qty_ret, (xs, x)))) ks xss xss sel_retTs;
kuncar@60229
   375
kuncar@60229
   376
    fun mk_sel_casex (_, _, (_, x)) = Ctr_Sugar.mk_case typs (x |> dest_Free |> snd) (#casex ctr_sugar);
kuncar@60229
   377
    val dis_casex = Ctr_Sugar.mk_case typs HOLogic.boolT (#casex ctr_sugar);
kuncar@60233
   378
    fun mk_sel_case_args lthy ctr_Tss ks (k, qty_ret, (xs, x)) =
kuncar@60229
   379
      let
kuncar@60229
   380
        val T = x |> dest_Free |> snd;
kuncar@60229
   381
        fun gen_undef_wit Ts wits =
kuncar@60233
   382
          case code_dt_of lthy (T, qty_ret) of
kuncar@60229
   383
            SOME code_dt =>
kuncar@60233
   384
              (fold_rev (Term.lambda o curry Free Name.uu) Ts (mk_witness_of_code_dt qty_ret code_dt),
kuncar@60229
   385
                wit_thm_of_code_dt code_dt :: wits)
kuncar@60229
   386
            | NONE => (fold_rev (Term.lambda o curry Free Name.uu) Ts (mk_undefined T), wits)
kuncar@60229
   387
      in
kuncar@60229
   388
        @{fold_map 2} (fn Ts => fn k' => fn wits =>
kuncar@60229
   389
          (if k = k' then (fold_rev Term.lambda xs x, wits) else gen_undef_wit Ts wits)) ctr_Tss ks []
kuncar@60229
   390
      end;
kuncar@60229
   391
    fun mk_sel_rhs arg =
kuncar@60229
   392
      let val (sel_rhs, wits) = mk_sel_case_args lthy ctr_Tss ks arg
kuncar@60229
   393
      in (arg |> #2, wits, list_comb (mk_sel_casex arg, sel_rhs)) end;
kuncar@60229
   394
    fun mk_dis_case_args args k  = map (fn (k', arg) => (if k = k'
kuncar@60229
   395
      then fold_rev Term.lambda arg @{const True} else fold_rev Term.lambda arg @{const False})) args;
kuncar@60229
   396
    val sel_rhs = map (map mk_sel_rhs) sel_argss
kuncar@60229
   397
    val dis_rhs = map (fn k => list_comb (dis_casex, mk_dis_case_args (ks ~~ xss) k)) ks
kuncar@60229
   398
    val dis_qty = qty_isom --> HOLogic.boolT;
kuncar@60229
   399
    val dis_names = map (fn k => Binding.qualified true ("dis" ^ string_of_int k) uTname) ks;
kuncar@60229
   400
kuncar@60229
   401
    val (diss, lthy) = @{fold_map 2} (fn b => fn rhs => fn lthy =>
kuncar@60229
   402
      lift_def ld_no_notes (b, NoSyn) dis_qty rhs (K all_tac) [] lthy
kuncar@60229
   403
      |> apfst (mk_lift_const_of_lift_def dis_qty)) dis_names dis_rhs lthy
kuncar@60229
   404
kuncar@60231
   405
    val unfold_lift_sel_rsp = @{lemma "(\<And>x. P1 x \<Longrightarrow> P2 (f x)) \<Longrightarrow> (rel_fun (eq_onp P1) (eq_onp P2)) f f"
kuncar@60231
   406
      by (simp add: eq_onp_same_args rel_fun_eq_onp_rel)}
kuncar@60231
   407
kuncar@60229
   408
    fun lift_sel_tac exhaust_rule dt_rules wits ctxt i =
kuncar@60231
   409
        (Method.insert_tac wits THEN' 
kuncar@60231
   410
         eq_onp_to_top_tac ctxt THEN' (* normalize *)
kuncar@60231
   411
         rtac unfold_lift_sel_rsp THEN'
kuncar@60231
   412
         case_tac exhaust_rule ctxt THEN_ALL_NEW (
kuncar@60231
   413
        EVERY' [hyp_subst_tac ctxt, (* does not kill wits because = was rewritten to eq_onp top *)
kuncar@60231
   414
        Raw_Simplifier.rewrite_goal_tac ctxt (map safe_mk_meta_eq dt_rules), 
kuncar@60229
   415
        REPEAT_DETERM o etac conjE, atac])) i
kuncar@60229
   416
    val pred_simps = Transfer.lookup_pred_data lthy (Tname rty) |> the |> Transfer.pred_simps
kuncar@60229
   417
    val sel_tac = lift_sel_tac (#exhaust ctr_sugar) (#case_thms ctr_sugar @ pred_simps)
kuncar@60229
   418
    val sel_names = map (fn (k, xs) => map (fn k' => Binding.qualified true
kuncar@60229
   419
      ("sel" ^ string_of_int k ^ string_of_int k') uTname) (1 upto length xs)) (ks ~~ ctr_Tss);
kuncar@60233
   420
    val (selss, lthy) = @{fold_map 2} (@{fold_map 2} (fn b => fn (qty_ret, wits, rhs) => fn lthy =>
kuncar@60231
   421
        lift_def_code_dt { code_dt = true, lift_config = ld_no_notes }
kuncar@60229
   422
        (b, NoSyn) (qty_isom --> qty_ret) rhs (HEADGOAL o sel_tac wits) [] lthy
kuncar@60229
   423
      |> apfst (mk_lift_const_of_lift_def (qty_isom --> qty_ret)))) sel_names sel_rhs lthy
kuncar@60229
   424
kuncar@60235
   425
    (* now we can execute the qty qty_isom isomorphism *)
kuncar@60229
   426
    fun mk_type_definition newT oldT RepC AbsC A =
kuncar@60229
   427
      let
kuncar@60229
   428
        val typedefC =
kuncar@60229
   429
          Const (@{const_name type_definition},
kuncar@60229
   430
            (newT --> oldT) --> (oldT --> newT) --> HOLogic.mk_setT oldT --> HOLogic.boolT);
kuncar@60229
   431
      in typedefC $ RepC $ AbsC $ A end;
kuncar@60229
   432
    val typedef_goal = mk_type_definition qty_isom qty rep_isom abs_isom (HOLogic.mk_UNIV qty) |>
kuncar@60229
   433
      HOLogic.mk_Trueprop;
kuncar@60231
   434
    fun typ_isom_tac ctxt i =
kuncar@60231
   435
      EVERY' [ SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms type_definition_def}),
kuncar@60231
   436
        DETERM o Transfer.transfer_tac true ctxt,
kuncar@60231
   437
          SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms eq_onp_top_eq_eq}) (* normalize *), 
kuncar@60231
   438
          Raw_Simplifier.rewrite_goal_tac ctxt 
kuncar@60231
   439
          (map safe_mk_meta_eq @{thms id_apply simp_thms Ball_def}),
kuncar@60231
   440
         rtac TrueI] i;
kuncar@60229
   441
kuncar@60229
   442
    val (_, transfer_lthy) = Proof_Context.note_thmss "" [((Binding.empty, []),
kuncar@60229
   443
      [(@{thms right_total_UNIV_transfer},[Transfer.transfer_add]),
kuncar@60229
   444
       (@{thms Domain_eq_top}, [Transfer.transfer_domain_add]) ])] lthy;
kuncar@60229
   445
kuncar@60229
   446
    val quot_thm_isom = Goal.prove_sorry transfer_lthy [] [] typedef_goal
kuncar@60229
   447
      (fn {context = ctxt, prems = _} => typ_isom_tac ctxt 1)
kuncar@60229
   448
      |> Thm.close_derivation
kuncar@60229
   449
      |> singleton (Variable.export transfer_lthy lthy)
kuncar@60229
   450
      |> (fn thm => @{thm UNIV_typedef_to_Quotient} OF [thm, @{thm reflexive}])
kuncar@60229
   451
    val qty_isom_name = Tname qty_isom;
kuncar@60229
   452
    val quot_isom_rep =
kuncar@60229
   453
      let
kuncar@60229
   454
        val (quotients : Lifting_Term.quotients) = Symtab.insert (Lifting_Info.quotient_eq) (qty_isom_name,
kuncar@60229
   455
          {quot_thm = quot_thm_isom, pcr_info = NONE}) Symtab.empty
kuncar@60229
   456
        val id_actions = { constr = K I, lift = K I, comp_lift = K I }
kuncar@60229
   457
      in
kuncar@60229
   458
        fn ctxt => fn (rty, qty) => Lifting_Term.prove_schematic_quot_thm id_actions quotients
kuncar@60229
   459
          ctxt (rty, qty) () |> fst |> Lifting_Term.force_qty_type ctxt qty
kuncar@60229
   460
          |> quot_thm_rep
kuncar@60229
   461
      end;
kuncar@60229
   462
    val x_lthy = lthy
kuncar@60229
   463
    val (x, lthy) = yield_singleton (mk_Frees "x") qty_isom lthy;
kuncar@60229
   464
kuncar@60229
   465
    fun mk_ctr ctr ctr_Ts sels =
kuncar@60229
   466
      let
kuncar@60229
   467
        val sel_ret_Ts = map (dest_Const #> snd #> body_type) sels;
kuncar@60229
   468
kuncar@60229
   469
        fun rep_isom lthy t (rty, qty) =
kuncar@60229
   470
          let
kuncar@60229
   471
            val rep = quot_isom_rep lthy (rty, qty)
kuncar@60229
   472
          in
kuncar@60229
   473
            if is_Const rep andalso (rep |> dest_Const |> fst) = @{const_name id} then
kuncar@60229
   474
              t else rep $ t
kuncar@60229
   475
          end;
kuncar@60229
   476
      in
kuncar@60229
   477
        @{fold 3} (fn sel => fn ctr_T => fn sel_ret_T => fn ctr =>
kuncar@60229
   478
          ctr $ rep_isom lthy (sel $ x) (ctr_T, sel_ret_T)) sels ctr_Ts sel_ret_Ts ctr
kuncar@60229
   479
      end;
kuncar@60229
   480
kuncar@60229
   481
    (* stolen from Metis *)
kuncar@60229
   482
    exception BREAK_LIST
kuncar@60229
   483
    fun break_list (x :: xs) = (x, xs)
kuncar@60229
   484
      | break_list _ = raise BREAK_LIST
kuncar@60229
   485
kuncar@60229
   486
    val (ctr, ctrs) = qty_ctrs |> rev |> break_list;
kuncar@60229
   487
    val (ctr_Ts, ctr_Tss) = qty_ctr_Tss |> rev |> break_list;
kuncar@60229
   488
    val (sel, rselss) = selss |> rev |> break_list;
kuncar@60229
   489
    val rdiss = rev diss |> tl;
kuncar@60229
   490
kuncar@60229
   491
    val first_ctr = mk_ctr ctr ctr_Ts sel;
kuncar@60229
   492
kuncar@60229
   493
    fun mk_If_ctr dis ctr ctr_Ts sel elsex = mk_If (dis$x) (mk_ctr ctr ctr_Ts sel) elsex;
kuncar@60229
   494
kuncar@60229
   495
    val rhs = @{fold 4} mk_If_ctr rdiss ctrs ctr_Tss rselss first_ctr;
kuncar@60229
   496
kuncar@60229
   497
    val rep_isom_code_goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (rep_isom$x, rhs));
kuncar@60229
   498
kuncar@60229
   499
    local
kuncar@60229
   500
      val rep_isom_code_tac_rules = map safe_mk_meta_eq @{thms refl id_apply if_splits simp_thms}
kuncar@60229
   501
    in
kuncar@60229
   502
      fun rep_isom_code_tac (ctr_sugar:Ctr_Sugar.ctr_sugar) ctxt i =
kuncar@60229
   503
        let
kuncar@60229
   504
          val exhaust = ctr_sugar |> #exhaust
kuncar@60229
   505
          val cases = ctr_sugar |> #case_thms
kuncar@60229
   506
          val map_ids = fp |> #fp_nesting_bnfs |> map BNF_Def.map_id0_of_bnf
kuncar@60229
   507
          val simp_rules = map safe_mk_meta_eq (cases @ map_ids) @ rep_isom_code_tac_rules
kuncar@60229
   508
        in
kuncar@60229
   509
          EVERY' [Transfer.gen_frees_tac [] ctxt, DETERM o (Transfer.transfer_tac true ctxt),
kuncar@60229
   510
            case_tac exhaust ctxt THEN_ALL_NEW EVERY' [hyp_subst_tac ctxt,
kuncar@60229
   511
              Raw_Simplifier.rewrite_goal_tac ctxt simp_rules, rtac TrueI ]] i
kuncar@60229
   512
        end
kuncar@60229
   513
    end
kuncar@60234
   514
    
kuncar@60234
   515
    (* stolen from bnf_fp_n2m.ML *)
kuncar@60234
   516
    fun force_typ ctxt T =
kuncar@60234
   517
      Term.map_types Type_Infer.paramify_vars
kuncar@60234
   518
      #> Type.constraint T
kuncar@60234
   519
      #> singleton (Type_Infer_Context.infer_types ctxt);
kuncar@60234
   520
kuncar@60234
   521
    (* The following tests that types in rty have corresponding arities imposed by constraints of
kuncar@60234
   522
       the datatype fp. Otherwise rep_isom_code_tac could fail (especially transfer in it) is such
kuncar@60234
   523
       a way that it is not easy to infer the problem with sorts.
kuncar@60234
   524
    *)
kuncar@60234
   525
    val _ = yield_singleton (mk_Frees "x") (#T fp) lthy |> fst |> force_typ lthy qty
kuncar@60229
   526
kuncar@60229
   527
    val rep_isom_code = Goal.prove_sorry lthy [] [] rep_isom_code_goal
kuncar@60229
   528
      (fn {context = ctxt, prems = _} => rep_isom_code_tac ctr_sugar ctxt 1)
kuncar@60229
   529
      |> Thm.close_derivation
kuncar@60229
   530
      |> singleton(Variable.export lthy x_lthy)
kuncar@60229
   531
    val lthy = x_lthy
kuncar@60229
   532
    val lthy =
kuncar@60229
   533
      lthy
kuncar@60229
   534
      |> snd o Local_Theory.note ((Binding.empty, @{attributes [code]}), [rep_isom_code])
kuncar@60229
   535
      |> Lifting_Setup.lifting_forget pointer
kuncar@60229
   536
  in
kuncar@60229
   537
    ((selss, diss, rep_isom_code), lthy)
kuncar@60229
   538
  end
kuncar@60229
   539
and constr qty (quot_thm, (lthy, rel_eq_onps)) =
kuncar@60229
   540
  let
kuncar@60229
   541
    val quot_thm = Lifting_Term.force_qty_type lthy qty quot_thm
kuncar@60229
   542
    val (rty, qty) = quot_thm_rty_qty quot_thm
kuncar@60229
   543
    val rty_name = Tname rty;
kuncar@60229
   544
    val pred_data = Transfer.lookup_pred_data lthy rty_name
kuncar@60229
   545
    val pred_data = if is_some pred_data then the pred_data
kuncar@60229
   546
      else error ("code_dt: " ^ quote rty_name ^ " is not a datatype.")
kuncar@60229
   547
    val rel_eq_onp = safe_mk_meta_eq (Transfer.rel_eq_onp pred_data);
kuncar@60231
   548
    val rel_eq_onps = insert Thm.eq_thm rel_eq_onp rel_eq_onps
kuncar@60229
   549
    val R_conv = Transfer.top_sweep_rewr_conv @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]}
kuncar@60229
   550
      then_conv Conv.rewr_conv rel_eq_onp
kuncar@60229
   551
    val quot_thm = Conv.fconv_rule(HOLogic.Trueprop_conv (Quotient_R_conv R_conv)) quot_thm;
kuncar@60229
   552
  in
kuncar@60229
   553
    if is_none (code_dt_of lthy (rty, qty)) then
kuncar@60229
   554
      let
kuncar@60229
   555
        val non_empty_pred = quot_thm RS @{thm type_definition_Quotient_not_empty}
kuncar@60229
   556
        val pred = quot_thm_rel quot_thm |> dest_comb |> snd;
kuncar@60229
   557
        val (pred, lthy) = yield_singleton (Variable.import_terms true) pred lthy;
kuncar@60229
   558
        val TFrees = Term.add_tfreesT qty []
kuncar@60229
   559
kuncar@60229
   560
        fun non_empty_typedef_tac non_empty_pred ctxt i =
kuncar@60231
   561
          (Method.insert_tac [non_empty_pred] THEN' 
kuncar@60231
   562
            SELECT_GOAL (Local_Defs.unfold_tac ctxt [mem_Collect_eq]) THEN' atac) i
kuncar@60229
   563
        val uTname = unique_Tname (rty, qty)
kuncar@60229
   564
        val Tdef_set = HOLogic.mk_Collect ("x", rty, pred $ Free("x", rty));
kuncar@60229
   565
        val ((_, tcode_dt), lthy) = conceal_naming_result (typedef (Binding.concealed uTname, TFrees, NoSyn)
kuncar@60231
   566
          Tdef_set NONE (fn lthy => HEADGOAL (non_empty_typedef_tac non_empty_pred lthy))) lthy;
kuncar@60229
   567
        val type_definition_thm = tcode_dt |> snd |> #type_definition;
kuncar@60229
   568
        val qty_isom = tcode_dt |> fst |> #abs_type;
kuncar@60229
   569
kuncar@60229
   570
        val config = { notes = false}
kuncar@60229
   571
        val (binding, lthy) = conceal_naming_result (Lifting_Setup.setup_by_typedef_thm
kuncar@60229
   572
          config type_definition_thm) lthy
kuncar@60229
   573
        val lthy = Local_Theory.restore lthy
kuncar@60229
   574
        val (wit, wit_thm) = mk_witness quot_thm;
kuncar@60229
   575
        val code_dt = mk_code_dt rty qty wit wit_thm NONE;
kuncar@60229
   576
        val lthy = lthy
kuncar@60229
   577
          |> update_code_dt code_dt
kuncar@60229
   578
          |> Local_Theory.restore
kuncar@60229
   579
          |> mk_rep_isom binding (rty, qty, qty_isom) |> snd
kuncar@60229
   580
      in
kuncar@60231
   581
        (quot_thm, (lthy, rel_eq_onps))
kuncar@60229
   582
      end
kuncar@60229
   583
    else
kuncar@60231
   584
      (quot_thm, (lthy, rel_eq_onps))
kuncar@60229
   585
  end
kuncar@60229
   586
and lift_def_code_dt config var qty rhs tac par_thms lthy = gen_lift_def (add_lift_def_code_dt config)
kuncar@60229
   587
  var qty rhs tac par_thms lthy
kuncar@60229
   588
kuncar@60229
   589
kuncar@60229
   590
(** from parsed parameters to the config record **)
kuncar@60229
   591
wenzelm@60239
   592
fun map_config_code_dt f1 f2 ({code_dt = code_dt, lift_config = lift_config}: config_code_dt) =
wenzelm@60239
   593
  {code_dt = f1 code_dt, lift_config = f2 lift_config}
kuncar@60229
   594
kuncar@60229
   595
fun update_config_code_dt nval = map_config_code_dt (K nval) I
kuncar@60229
   596
kuncar@60229
   597
val config_flags = [("code_dt", update_config_code_dt true)]
kuncar@60229
   598
kuncar@60229
   599
fun evaluate_params params =
kuncar@60229
   600
  let
kuncar@60229
   601
    fun eval_param param config =
kuncar@60229
   602
      case AList.lookup (op =) config_flags param of
kuncar@60229
   603
        SOME update => update config
kuncar@60229
   604
        | NONE => error ("Unknown parameter: " ^ (quote param))
kuncar@60229
   605
  in
kuncar@60229
   606
    fold eval_param params default_config_code_dt
kuncar@60229
   607
  end
kuncar@60229
   608
kuncar@60229
   609
(**
kuncar@60229
   610
kuncar@60229
   611
  lift_definition command. It opens a proof of a corresponding respectfulness
kuncar@60229
   612
  theorem in a user-friendly, readable form. Then add_lift_def_code_dt is called internally.
kuncar@60229
   613
kuncar@60229
   614
**)
kuncar@60229
   615
kuncar@60231
   616
local
kuncar@60231
   617
  val eq_onp_assms_tac_fixed_rules = map (Transfer.prep_transfer_domain_thm @{context})
kuncar@60231
   618
    [@{thm pcr_Domainp_total}, @{thm pcr_Domainp_par_left_total}, @{thm pcr_Domainp_par}, 
kuncar@60231
   619
      @{thm pcr_Domainp}]
kuncar@60231
   620
in
kuncar@60231
   621
fun mk_readable_rsp_thm_eq tm lthy =
kuncar@60231
   622
  let
kuncar@60231
   623
    val ctm = Thm.cterm_of lthy tm
kuncar@60231
   624
    
kuncar@60231
   625
    fun assms_rewr_conv tactic rule ct =
kuncar@60231
   626
      let
kuncar@60231
   627
        fun prove_extra_assms thm =
kuncar@60231
   628
          let
kuncar@60231
   629
            val assms = cprems_of thm
kuncar@60231
   630
            fun finish thm = if Thm.no_prems thm then SOME (Goal.conclude thm) else NONE
kuncar@60231
   631
            fun prove ctm = Option.mapPartial finish (SINGLE tactic (Goal.init ctm))
kuncar@60231
   632
          in
kuncar@60231
   633
            map_interrupt prove assms
kuncar@60231
   634
          end
kuncar@60231
   635
    
kuncar@60231
   636
        fun cconl_of thm = Drule.strip_imp_concl (Thm.cprop_of thm)
kuncar@60231
   637
        fun lhs_of thm = fst (Thm.dest_equals (cconl_of thm))
kuncar@60231
   638
        fun rhs_of thm = snd (Thm.dest_equals (cconl_of thm))
kuncar@60231
   639
        val rule1 = Thm.incr_indexes (Thm.maxidx_of_cterm ct + 1) rule;
kuncar@60231
   640
        val lhs = lhs_of rule1;
kuncar@60231
   641
        val rule2 = Thm.rename_boundvars (Thm.term_of lhs) (Thm.term_of ct) rule1;
kuncar@60231
   642
        val rule3 =
kuncar@60231
   643
          Thm.instantiate (Thm.match (lhs, ct)) rule2
kuncar@60231
   644
            handle Pattern.MATCH => raise CTERM ("assms_rewr_conv", [lhs, ct]);
kuncar@60231
   645
        val proved_assms = prove_extra_assms rule3
kuncar@60231
   646
      in
kuncar@60231
   647
        case proved_assms of
kuncar@60231
   648
          SOME proved_assms =>
kuncar@60231
   649
            let
kuncar@60231
   650
              val rule3 = proved_assms MRSL rule3
kuncar@60231
   651
              val rule4 =
kuncar@60231
   652
                if lhs_of rule3 aconvc ct then rule3
kuncar@60231
   653
                else
kuncar@60231
   654
                  let val ceq = Thm.dest_fun2 (Thm.cprop_of rule3)
kuncar@60231
   655
                  in rule3 COMP Thm.trivial (Thm.mk_binop ceq ct (rhs_of rule3)) end
kuncar@60231
   656
            in Thm.transitive rule4 (Thm.beta_conversion true (rhs_of rule4)) end
kuncar@60231
   657
          | NONE => Conv.no_conv ct
kuncar@60231
   658
      end
kuncar@60231
   659
kuncar@60231
   660
    fun assms_rewrs_conv tactic rules = Conv.first_conv (map (assms_rewr_conv tactic) rules)
kuncar@60231
   661
kuncar@60231
   662
    fun simp_arrows_conv ctm =
kuncar@60231
   663
      let
kuncar@60231
   664
        val unfold_conv = Conv.rewrs_conv 
kuncar@60231
   665
          [@{thm rel_fun_eq_eq_onp[THEN eq_reflection]}, 
kuncar@60231
   666
            @{thm rel_fun_eq_onp_rel[THEN eq_reflection]},
kuncar@60231
   667
            @{thm rel_fun_eq[THEN eq_reflection]},
kuncar@60231
   668
            @{thm rel_fun_eq_rel[THEN eq_reflection]}, 
kuncar@60231
   669
            @{thm rel_fun_def[THEN eq_reflection]}]
kuncar@60231
   670
        fun binop_conv2 cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
kuncar@60231
   671
        val eq_onp_assms_tac_rules = @{thm left_unique_OO} :: 
kuncar@60231
   672
            eq_onp_assms_tac_fixed_rules @ (Transfer.get_transfer_raw lthy)
kuncar@60231
   673
        val intro_top_rule = @{thm eq_onp_top_eq_eq[symmetric, THEN eq_reflection]}
kuncar@60231
   674
        val kill_tops = Transfer.top_sweep_rewr_conv [@{thm eq_onp_top_eq_eq[THEN eq_reflection]}]
kuncar@60231
   675
        val eq_onp_assms_tac = (CONVERSION kill_tops THEN' 
kuncar@60231
   676
          TRY o REPEAT_ALL_NEW (resolve_tac lthy eq_onp_assms_tac_rules) 
kuncar@60231
   677
          THEN_ALL_NEW (DETERM o Transfer.eq_tac lthy)) 1
kuncar@60231
   678
        val relator_eq_onp_conv = Conv.bottom_conv
kuncar@60231
   679
          (K (Conv.try_conv (assms_rewrs_conv eq_onp_assms_tac
kuncar@60231
   680
            (intro_top_rule :: Lifting_Info.get_relator_eq_onp_rules lthy)))) lthy
kuncar@60231
   681
          then_conv kill_tops
kuncar@60231
   682
        val relator_eq_conv = Conv.bottom_conv
kuncar@60231
   683
          (K (Conv.try_conv (Conv.rewrs_conv (Transfer.get_relator_eq lthy)))) lthy
kuncar@60231
   684
      in
kuncar@60231
   685
        case (Thm.term_of ctm) of
kuncar@60231
   686
          Const (@{const_name "rel_fun"}, _) $ _ $ _ => 
kuncar@60231
   687
            (binop_conv2 simp_arrows_conv simp_arrows_conv then_conv unfold_conv) ctm
kuncar@60231
   688
          | _ => (relator_eq_onp_conv then_conv relator_eq_conv) ctm
kuncar@60231
   689
      end
kuncar@60231
   690
    
kuncar@60231
   691
    val unfold_ret_val_invs = Conv.bottom_conv 
kuncar@60231
   692
      (K (Conv.try_conv (Conv.rewr_conv @{thm eq_onp_same_args[THEN eq_reflection]}))) lthy
kuncar@60231
   693
    val unfold_inv_conv = 
kuncar@60231
   694
      Conv.top_sweep_conv (K (Conv.rewr_conv @{thm eq_onp_def[THEN eq_reflection]})) lthy
kuncar@60231
   695
    val simp_conv = HOLogic.Trueprop_conv (Conv.fun2_conv simp_arrows_conv)
kuncar@60231
   696
    val univq_conv = Conv.rewr_conv @{thm HOL.all_simps(6)[symmetric, THEN eq_reflection]}
kuncar@60231
   697
    val univq_prenex_conv = Conv.top_conv (K (Conv.try_conv univq_conv)) lthy
kuncar@60231
   698
    val beta_conv = Thm.beta_conversion true
kuncar@60231
   699
    val eq_thm = 
kuncar@60231
   700
      (simp_conv then_conv univq_prenex_conv then_conv beta_conv then_conv unfold_ret_val_invs
kuncar@60231
   701
         then_conv unfold_inv_conv) ctm
kuncar@60231
   702
  in
kuncar@60231
   703
    Object_Logic.rulify lthy (eq_thm RS Drule.equal_elim_rule2)
kuncar@60231
   704
  end
kuncar@60231
   705
end
kuncar@60231
   706
kuncar@60231
   707
fun rename_to_tnames ctxt term =
kuncar@60231
   708
  let
kuncar@60231
   709
    fun all_typs (Const (@{const_name Pure.all}, _) $ Abs (_, T, t)) = T :: all_typs t
kuncar@60231
   710
      | all_typs _ = []
kuncar@60231
   711
kuncar@60231
   712
    fun rename (Const (@{const_name Pure.all}, T1) $ Abs (_, T2, t)) (new_name :: names) = 
kuncar@60231
   713
        (Const (@{const_name Pure.all}, T1) $ Abs (new_name, T2, rename t names)) 
kuncar@60231
   714
      | rename t _ = t
kuncar@60231
   715
kuncar@60231
   716
    val (fixed_def_t, _) = yield_singleton (Variable.importT_terms) term ctxt
kuncar@60231
   717
    val new_names = Old_Datatype_Prop.make_tnames (all_typs fixed_def_t)
kuncar@60231
   718
  in
kuncar@60231
   719
    rename term new_names
kuncar@60231
   720
  end
kuncar@60231
   721
kuncar@60235
   722
fun quot_thm_err ctxt (rty, qty) pretty_msg =
kuncar@60235
   723
  let
kuncar@60235
   724
    val error_msg = cat_lines
kuncar@60235
   725
       ["Lifting failed for the following types:",
kuncar@60235
   726
        Pretty.string_of (Pretty.block
kuncar@60235
   727
         [Pretty.str "Raw type:", Pretty.brk 2, Syntax.pretty_typ ctxt rty]),
kuncar@60235
   728
        Pretty.string_of (Pretty.block
kuncar@60235
   729
         [Pretty.str "Abstract type:", Pretty.brk 2, Syntax.pretty_typ ctxt qty]),
kuncar@60235
   730
        "",
kuncar@60235
   731
        (Pretty.string_of (Pretty.block
kuncar@60235
   732
         [Pretty.str "Reason:", Pretty.brk 2, pretty_msg]))]
kuncar@60235
   733
  in
kuncar@60235
   734
    error error_msg
kuncar@60235
   735
  end
kuncar@60235
   736
kuncar@60236
   737
fun check_rty_err ctxt (rty_schematic, rty_forced) (raw_var, rhs_raw) =
kuncar@60236
   738
  let
kuncar@60236
   739
    val (_, ctxt') = yield_singleton Proof_Context.read_vars raw_var ctxt
kuncar@60236
   740
    val rhs = (Syntax.check_term ctxt' o Syntax.parse_term ctxt') rhs_raw
kuncar@60236
   741
    val error_msg = cat_lines
kuncar@60236
   742
       ["Lifting failed for the following term:",
kuncar@60236
   743
        Pretty.string_of (Pretty.block
kuncar@60236
   744
         [Pretty.str "Term:", Pretty.brk 2, Syntax.pretty_term ctxt rhs]),
kuncar@60236
   745
        Pretty.string_of (Pretty.block
kuncar@60236
   746
         [Pretty.str "Type:", Pretty.brk 2, Syntax.pretty_typ ctxt rty_schematic]),
kuncar@60236
   747
        "",
kuncar@60236
   748
        (Pretty.string_of (Pretty.block
kuncar@60236
   749
         [Pretty.str "Reason:",
kuncar@60236
   750
          Pretty.brk 2,
kuncar@60236
   751
          Pretty.str "The type of the term cannot be instantiated to",
kuncar@60236
   752
          Pretty.brk 1,
kuncar@60236
   753
          Pretty.quote (Syntax.pretty_typ ctxt rty_forced),
kuncar@60236
   754
          Pretty.str "."]))]
kuncar@60236
   755
    in
kuncar@60236
   756
      error error_msg
kuncar@60236
   757
    end
kuncar@60236
   758
kuncar@60229
   759
fun lift_def_cmd (params, raw_var, rhs_raw, par_xthms) lthy =
kuncar@60229
   760
  let
kuncar@60229
   761
    val config = evaluate_params params
kuncar@60229
   762
    val ((binding, SOME qty, mx), lthy) = yield_singleton Proof_Context.read_vars raw_var lthy
kuncar@60229
   763
    val var = (binding, mx)
kuncar@60229
   764
    val rhs = (Syntax.check_term lthy o Syntax.parse_term lthy) rhs_raw
kuncar@60229
   765
    val par_thms = Attrib.eval_thms lthy par_xthms
kuncar@60229
   766
    val (goal, after_qed) = prepare_lift_def (add_lift_def_code_dt config) var qty rhs par_thms lthy
kuncar@60231
   767
    val (goal, after_qed) =
kuncar@60231
   768
      case goal of
kuncar@60231
   769
        NONE => (goal, K (after_qed Drule.dummy_thm))
kuncar@60231
   770
        | SOME prsp_tm =>
kuncar@60231
   771
          let
kuncar@60231
   772
            val readable_rsp_thm_eq = mk_readable_rsp_thm_eq prsp_tm lthy
kuncar@60231
   773
            val (readable_rsp_tm, _) = Logic.dest_implies (Thm.prop_of readable_rsp_thm_eq)
kuncar@60231
   774
            val readable_rsp_tm_tnames = rename_to_tnames lthy readable_rsp_tm
kuncar@60231
   775
        
kuncar@60231
   776
            fun after_qed' [[thm]] lthy = 
kuncar@60231
   777
              let
kuncar@60231
   778
                val internal_rsp_thm = Goal.prove lthy [] [] prsp_tm 
kuncar@60231
   779
                    (fn {context = ctxt, ...} =>
kuncar@60231
   780
                      rtac readable_rsp_thm_eq 1 THEN Proof_Context.fact_tac ctxt [thm] 1)
kuncar@60231
   781
              in
kuncar@60231
   782
                after_qed internal_rsp_thm lthy
kuncar@60231
   783
              end
kuncar@60231
   784
          in
kuncar@60231
   785
            (SOME readable_rsp_tm_tnames, after_qed')
kuncar@60236
   786
          end
kuncar@60236
   787
    fun after_qed_with_err_handling thmss ctxt = (after_qed thmss ctxt
kuncar@60236
   788
      handle Lifting_Term.QUOT_THM (rty, qty, msg) => quot_thm_err lthy (rty, qty) msg)
kuncar@60236
   789
      handle Lifting_Term.CHECK_RTY (rty_schematic, rty_forced) =>
kuncar@60236
   790
        check_rty_err lthy (rty_schematic, rty_forced) (raw_var, rhs_raw);
kuncar@60229
   791
  in
kuncar@60236
   792
    Proof.theorem NONE (snd oo after_qed_with_err_handling) [map (rpair []) (the_list goal)] lthy
kuncar@60229
   793
  end
kuncar@60229
   794
kuncar@60229
   795
fun lift_def_cmd_with_err_handling (params, (raw_var, rhs_raw, par_xthms)) lthy =
kuncar@60229
   796
  (lift_def_cmd (params, raw_var, rhs_raw, par_xthms) lthy
kuncar@60229
   797
    handle Lifting_Term.QUOT_THM (rty, qty, msg) => quot_thm_err lthy (rty, qty) msg)
kuncar@60229
   798
    handle Lifting_Term.CHECK_RTY (rty_schematic, rty_forced) =>
kuncar@60229
   799
      check_rty_err lthy (rty_schematic, rty_forced) (raw_var, rhs_raw);
kuncar@60229
   800
kuncar@60229
   801
val parse_param = Parse.name
kuncar@60229
   802
val parse_params = Scan.optional (Args.parens (Parse.list parse_param)) [];
kuncar@60229
   803
kuncar@60229
   804
(* parser and command *)
kuncar@60229
   805
val liftdef_parser =
kuncar@60229
   806
  parse_params --
kuncar@60229
   807
  (((Parse.binding -- (@{keyword "::"} |-- (Parse.typ >> SOME) -- Parse.opt_mixfix') >> Parse.triple2)
kuncar@60229
   808
    --| @{keyword "is"} -- Parse.term --
kuncar@60229
   809
      Scan.optional (@{keyword "parametric"} |-- Parse.!!! Parse.xthms1) []) >> Parse.triple1)
kuncar@60229
   810
kuncar@60229
   811
val _ =
kuncar@60229
   812
  Outer_Syntax.local_theory_to_proof @{command_keyword "lift_definition"}
kuncar@60229
   813
    "definition for constants over the quotient type"
kuncar@60229
   814
      (liftdef_parser >> lift_def_cmd_with_err_handling)
kuncar@60229
   815
kuncar@60229
   816
end