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