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