src/HOL/Tools/Lifting/lifting_def.ML
author wenzelm
Sun May 03 14:35:48 2015 +0200 (2015-05-03)
changeset 60239 755e11e2e15d
parent 60231 0daab758e087
child 60784 4f590c08fd5d
permissions -rw-r--r--
make SML/NJ more happy;
     1 (*  Title:      HOL/Tools/Lifting/lifting_def.ML
     2     Author:     Ondrej Kuncar
     3 
     4 Definitions for constants on quotient types.
     5 *)
     6 
     7 signature LIFTING_DEF =
     8 sig
     9   datatype code_eq = UNKNOWN_EQ | NONE_EQ | ABS_EQ | REP_EQ
    10   type lift_def
    11   val rty_of_lift_def: lift_def -> typ
    12   val qty_of_lift_def: lift_def -> typ
    13   val rhs_of_lift_def: lift_def -> term
    14   val lift_const_of_lift_def: lift_def -> term
    15   val def_thm_of_lift_def: lift_def -> thm
    16   val rsp_thm_of_lift_def: lift_def -> thm
    17   val abs_eq_of_lift_def: lift_def -> thm
    18   val rep_eq_of_lift_def: lift_def -> thm option
    19   val code_eq_of_lift_def: lift_def -> code_eq
    20   val transfer_rules_of_lift_def: lift_def -> thm list
    21   val morph_lift_def: morphism -> lift_def -> lift_def
    22   val inst_of_lift_def: Proof.context -> typ -> lift_def -> lift_def
    23   val mk_lift_const_of_lift_def: typ -> lift_def -> term
    24 
    25   type config = { notes: bool }
    26   val map_config: (bool -> bool) -> config -> config
    27   val default_config: config
    28 
    29   val generate_parametric_transfer_rule:
    30     Proof.context -> thm -> thm -> thm
    31 
    32   val add_lift_def: 
    33     config -> binding * mixfix -> typ -> term -> thm -> thm list -> local_theory -> 
    34       lift_def * local_theory
    35   
    36   val prepare_lift_def:
    37     (binding * mixfix -> typ -> term -> thm -> thm list -> Proof.context -> 
    38       lift_def * local_theory) -> 
    39     binding * mixfix -> typ -> term -> thm list -> local_theory -> 
    40     term option * (thm -> Proof.context -> lift_def * local_theory)
    41 
    42   val gen_lift_def:
    43     (binding * mixfix -> typ -> term -> thm -> thm list -> local_theory -> 
    44       lift_def * local_theory) -> 
    45     binding * mixfix -> typ -> term -> (Proof.context -> tactic) -> thm list -> 
    46     local_theory -> lift_def * local_theory
    47 
    48   val lift_def: 
    49     config -> binding * mixfix -> typ -> term -> (Proof.context -> tactic) -> thm list -> 
    50     local_theory -> lift_def * local_theory
    51 
    52   val can_generate_code_cert: thm -> bool
    53 end
    54 
    55 structure Lifting_Def: LIFTING_DEF =
    56 struct
    57 
    58 open Lifting_Util
    59 
    60 infix 0 MRSL
    61 
    62 datatype code_eq = UNKNOWN_EQ | NONE_EQ | ABS_EQ | REP_EQ
    63 
    64 datatype lift_def = LIFT_DEF of {
    65   rty: typ,
    66   qty: typ,
    67   rhs: term,
    68   lift_const: term,
    69   def_thm: thm,
    70   rsp_thm: thm,
    71   abs_eq: thm,
    72   rep_eq: thm option,
    73   code_eq: code_eq,
    74   transfer_rules: thm list
    75 };
    76 
    77 fun rep_lift_def (LIFT_DEF lift_def) = lift_def;
    78 val rty_of_lift_def = #rty o rep_lift_def;
    79 val qty_of_lift_def = #qty o rep_lift_def;
    80 val rhs_of_lift_def = #rhs o rep_lift_def;
    81 val lift_const_of_lift_def = #lift_const o rep_lift_def;
    82 val def_thm_of_lift_def = #def_thm o rep_lift_def;
    83 val rsp_thm_of_lift_def = #rsp_thm o rep_lift_def;
    84 val abs_eq_of_lift_def = #abs_eq o rep_lift_def;
    85 val rep_eq_of_lift_def = #rep_eq o rep_lift_def;
    86 val code_eq_of_lift_def = #code_eq o rep_lift_def;
    87 val transfer_rules_of_lift_def = #transfer_rules o rep_lift_def;
    88 
    89 fun mk_lift_def rty qty rhs lift_const def_thm rsp_thm abs_eq rep_eq code_eq transfer_rules =
    90   LIFT_DEF {rty = rty, qty = qty,
    91             rhs = rhs, lift_const = lift_const,
    92             def_thm = def_thm, rsp_thm = rsp_thm, abs_eq = abs_eq, rep_eq = rep_eq, 
    93             code_eq = code_eq, transfer_rules = transfer_rules };
    94 
    95 fun map_lift_def f1 f2 f3 f4 f5 f6 f7 f8 f9 f10
    96   (LIFT_DEF {rty = rty, qty = qty, rhs = rhs, lift_const = lift_const,
    97   def_thm = def_thm, rsp_thm = rsp_thm, abs_eq = abs_eq, rep_eq = rep_eq, code_eq = code_eq,
    98   transfer_rules = transfer_rules }) =
    99   LIFT_DEF {rty = f1 rty, qty = f2 qty, rhs = f3 rhs, lift_const = f4 lift_const,
   100             def_thm = f5 def_thm, rsp_thm = f6 rsp_thm, abs_eq = f7 abs_eq, rep_eq = f8 rep_eq,
   101             code_eq = f9 code_eq, transfer_rules = f10 transfer_rules }
   102 
   103 fun morph_lift_def phi =
   104   let
   105     val mtyp = Morphism.typ phi
   106     val mterm = Morphism.term phi
   107     val mthm = Morphism.thm phi
   108   in
   109     map_lift_def mtyp mtyp mterm mterm mthm mthm mthm (Option.map mthm) I (map mthm)
   110   end
   111 
   112 fun mk_inst_of_lift_def qty lift_def = Vartab.empty |> Type.raw_match (qty_of_lift_def lift_def, qty)
   113 
   114 fun mk_lift_const_of_lift_def qty lift_def = Envir.subst_term_types (mk_inst_of_lift_def qty lift_def)
   115   (lift_const_of_lift_def lift_def)
   116 
   117 fun inst_of_lift_def ctxt qty lift_def =  mk_inst_of_lift_def qty lift_def
   118   |> instT_morphism ctxt |> (fn phi => morph_lift_def phi lift_def)
   119 
   120 (* Config *)
   121 
   122 type config = { notes: bool };
   123 fun map_config f1 { notes = notes } = { notes = f1 notes }
   124 val default_config = { notes = true };
   125 
   126 (* Reflexivity prover *)
   127 
   128 fun mono_eq_prover ctxt prop =
   129   let
   130     val refl_rules = Lifting_Info.get_reflexivity_rules ctxt
   131     val transfer_rules = Transfer.get_transfer_raw ctxt
   132     
   133     fun main_tac i = (REPEAT_ALL_NEW (DETERM o resolve_tac ctxt refl_rules) THEN_ALL_NEW 
   134       (REPEAT_ALL_NEW (DETERM o resolve_tac ctxt transfer_rules))) i
   135   in
   136     SOME (Goal.prove ctxt [] [] prop (K (main_tac 1)))
   137       handle ERROR _ => NONE
   138   end
   139 
   140 fun try_prove_refl_rel ctxt rel =
   141   let
   142     fun mk_ge_eq x =
   143       let
   144         val T = fastype_of x
   145       in
   146         Const (@{const_name "less_eq"}, T --> T --> HOLogic.boolT) $ 
   147           (Const (@{const_name HOL.eq}, T)) $ x
   148       end;
   149     val goal = HOLogic.mk_Trueprop (mk_ge_eq rel);
   150   in
   151      mono_eq_prover ctxt goal
   152   end;
   153 
   154 fun try_prove_reflexivity ctxt prop =
   155   let
   156     val cprop = Thm.cterm_of ctxt prop
   157     val rule = @{thm ge_eq_refl}
   158     val concl_pat = Drule.strip_imp_concl (Thm.cprop_of rule)
   159     val insts = Thm.first_order_match (concl_pat, cprop)
   160     val rule = Drule.instantiate_normalize insts rule
   161     val prop = hd (Thm.prems_of rule)
   162   in
   163     case mono_eq_prover ctxt prop of
   164       SOME thm => SOME (thm RS rule)
   165       | NONE => NONE
   166   end
   167 
   168 (* 
   169   Generates a parametrized transfer rule.
   170   transfer_rule - of the form T t f
   171   parametric_transfer_rule - of the form par_R t' t
   172   
   173   Result: par_T t' f, after substituing op= for relations in par_R that relate
   174     a type constructor to the same type constructor, it is a merge of (par_R' OO T) t' f
   175     using Lifting_Term.merge_transfer_relations
   176 *)
   177 
   178 fun generate_parametric_transfer_rule ctxt transfer_rule parametric_transfer_rule =
   179   let
   180     fun preprocess ctxt thm =
   181       let
   182         val tm = (strip_args 2 o HOLogic.dest_Trueprop o Thm.concl_of) thm;
   183         val param_rel = (snd o dest_comb o fst o dest_comb) tm;
   184         val free_vars = Term.add_vars param_rel [];
   185         
   186         fun make_subst (var as (_, typ)) subst = 
   187           let
   188             val [rty, rty'] = binder_types typ
   189           in
   190             if (Term.is_TVar rty andalso is_Type rty') then
   191               (Var var, HOLogic.eq_const rty')::subst
   192             else
   193               subst
   194           end;
   195         
   196         val subst = fold make_subst free_vars [];
   197         val csubst = map (apply2 (Thm.cterm_of ctxt)) subst;
   198         val inst_thm = Drule.cterm_instantiate csubst thm;
   199       in
   200         Conv.fconv_rule 
   201           ((Conv.concl_conv (Thm.nprems_of inst_thm) o
   202             HOLogic.Trueprop_conv o Conv.fun2_conv o Conv.arg1_conv)
   203             (Raw_Simplifier.rewrite ctxt false (Transfer.get_sym_relator_eq ctxt))) inst_thm
   204       end
   205 
   206     fun inst_relcomppI ctxt ant1 ant2 =
   207       let
   208         val t1 = (HOLogic.dest_Trueprop o Thm.concl_of) ant1
   209         val t2 = (HOLogic.dest_Trueprop o Thm.prop_of) ant2
   210         val fun1 = Thm.cterm_of ctxt (strip_args 2 t1)
   211         val args1 = map (Thm.cterm_of ctxt) (get_args 2 t1)
   212         val fun2 = Thm.cterm_of ctxt (strip_args 2 t2)
   213         val args2 = map (Thm.cterm_of ctxt) (get_args 1 t2)
   214         val relcomppI = Drule.incr_indexes2 ant1 ant2 @{thm relcomppI}
   215         val vars = (rev (Term.add_vars (Thm.prop_of relcomppI) []))
   216         val subst = map (apfst (Thm.cterm_of ctxt o Var)) (vars ~~ ([fun1] @ args1 @ [fun2] @ args2))
   217       in
   218         Drule.cterm_instantiate subst relcomppI
   219       end
   220 
   221     fun zip_transfer_rules ctxt thm =
   222       let
   223         fun mk_POS ty = Const (@{const_name POS}, ty --> ty --> HOLogic.boolT)
   224         val rel = (Thm.dest_fun2 o Thm.dest_arg o Thm.cprop_of) thm
   225         val typ = Thm.typ_of_cterm rel
   226         val POS_const = Thm.cterm_of ctxt (mk_POS typ)
   227         val var = Thm.cterm_of ctxt (Var (("X", Thm.maxidx_of_cterm rel + 1), typ))
   228         val goal =
   229           Thm.apply (Thm.cterm_of ctxt HOLogic.Trueprop) (Thm.apply (Thm.apply POS_const rel) var)
   230       in
   231         [Lifting_Term.merge_transfer_relations ctxt goal, thm] MRSL @{thm POS_apply}
   232       end
   233      
   234     val thm =
   235       inst_relcomppI ctxt parametric_transfer_rule transfer_rule
   236         OF [parametric_transfer_rule, transfer_rule]
   237     val preprocessed_thm = preprocess ctxt thm
   238     val orig_ctxt = ctxt
   239     val (fixed_thm, ctxt) = yield_singleton (apfst snd oo Variable.import true) preprocessed_thm ctxt
   240     val assms = cprems_of fixed_thm
   241     val add_transfer_rule = Thm.attribute_declaration Transfer.transfer_add
   242     val (prems, ctxt) = fold_map Thm.assume_hyps assms ctxt
   243     val ctxt = Context.proof_map (fold add_transfer_rule prems) ctxt
   244     val zipped_thm =
   245       fixed_thm
   246       |> undisch_all
   247       |> zip_transfer_rules ctxt
   248       |> implies_intr_list assms
   249       |> singleton (Variable.export ctxt orig_ctxt)
   250   in
   251     zipped_thm
   252   end
   253 
   254 fun print_generate_transfer_info msg = 
   255   let
   256     val error_msg = cat_lines 
   257       ["Generation of a parametric transfer rule failed.",
   258       (Pretty.string_of (Pretty.block
   259          [Pretty.str "Reason:", Pretty.brk 2, msg]))]
   260   in
   261     error error_msg
   262   end
   263 
   264 fun map_ter _ x [] = x
   265     | map_ter f _ xs = map f xs
   266 
   267 fun generate_transfer_rules lthy quot_thm rsp_thm def_thm par_thms =
   268   let
   269     val transfer_rule =
   270       ([quot_thm, rsp_thm, def_thm] MRSL @{thm Quotient_to_transfer})
   271       |> Lifting_Term.parametrize_transfer_rule lthy
   272   in
   273     (map_ter (generate_parametric_transfer_rule lthy transfer_rule) [transfer_rule] par_thms
   274     handle Lifting_Term.MERGE_TRANSFER_REL msg => (print_generate_transfer_info msg; [transfer_rule]))
   275   end
   276 
   277 (* Generation of the code certificate from the rsp theorem *)
   278 
   279 fun get_body_types (Type ("fun", [_, U]), Type ("fun", [_, V])) = get_body_types (U, V)
   280   | get_body_types (U, V)  = (U, V)
   281 
   282 fun get_binder_types (Type ("fun", [T, U]), Type ("fun", [V, W])) = (T, V) :: get_binder_types (U, W)
   283   | get_binder_types _ = []
   284 
   285 fun get_binder_types_by_rel (Const (@{const_name "rel_fun"}, _) $ _ $ S) (Type ("fun", [T, U]), Type ("fun", [V, W])) = 
   286     (T, V) :: get_binder_types_by_rel S (U, W)
   287   | get_binder_types_by_rel _ _ = []
   288 
   289 fun get_body_type_by_rel (Const (@{const_name "rel_fun"}, _) $ _ $ S) (Type ("fun", [_, U]), Type ("fun", [_, V])) = 
   290     get_body_type_by_rel S (U, V)
   291   | get_body_type_by_rel _ (U, V)  = (U, V)
   292 
   293 fun get_binder_rels (Const (@{const_name "rel_fun"}, _) $ R $ S) = R :: get_binder_rels S
   294   | get_binder_rels _ = []
   295 
   296 fun force_rty_type ctxt rty rhs = 
   297   let
   298     val thy = Proof_Context.theory_of ctxt
   299     val rhs_schematic = singleton (Variable.polymorphic ctxt) rhs
   300     val rty_schematic = fastype_of rhs_schematic
   301     val match = Sign.typ_match thy (rty_schematic, rty) Vartab.empty
   302   in
   303     Envir.subst_term_types match rhs_schematic
   304   end
   305 
   306 fun unabs_def ctxt def = 
   307   let
   308     val (_, rhs) = Thm.dest_equals (Thm.cprop_of def)
   309     fun dest_abs (Abs (var_name, T, _)) = (var_name, T)
   310       | dest_abs tm = raise TERM("get_abs_var",[tm])
   311     val (var_name, T) = dest_abs (Thm.term_of rhs)
   312     val (new_var_names, ctxt') = Variable.variant_fixes [var_name] ctxt
   313     val refl_thm = Thm.reflexive (Thm.cterm_of ctxt' (Free (hd new_var_names, T)))
   314   in
   315     Thm.combination def refl_thm |>
   316     singleton (Proof_Context.export ctxt' ctxt)
   317   end
   318 
   319 fun unabs_all_def ctxt def = 
   320   let
   321     val (_, rhs) = Thm.dest_equals (Thm.cprop_of def)
   322     val xs = strip_abs_vars (Thm.term_of rhs)
   323   in  
   324     fold (K (unabs_def ctxt)) xs def
   325   end
   326 
   327 val map_fun_unfolded = 
   328   @{thm map_fun_def[abs_def]} |>
   329   unabs_def @{context} |>
   330   unabs_def @{context} |>
   331   Local_Defs.unfold @{context} [@{thm comp_def}]
   332 
   333 fun unfold_fun_maps ctm =
   334   let
   335     fun unfold_conv ctm =
   336       case (Thm.term_of ctm) of
   337         Const (@{const_name "map_fun"}, _) $ _ $ _ => 
   338           (Conv.arg_conv unfold_conv then_conv Conv.rewr_conv map_fun_unfolded) ctm
   339         | _ => Conv.all_conv ctm
   340   in
   341     (Conv.fun_conv unfold_conv) ctm
   342   end
   343 
   344 fun unfold_fun_maps_beta ctm =
   345   let val try_beta_conv = Conv.try_conv (Thm.beta_conversion false)
   346   in 
   347     (unfold_fun_maps then_conv try_beta_conv) ctm 
   348   end
   349 
   350 fun prove_rel ctxt rsp_thm (rty, qty) =
   351   let
   352     val ty_args = get_binder_types (rty, qty)
   353     fun disch_arg args_ty thm = 
   354       let
   355         val quot_thm = Lifting_Term.prove_quot_thm ctxt args_ty
   356       in
   357         [quot_thm, thm] MRSL @{thm apply_rsp''}
   358       end
   359   in
   360     fold disch_arg ty_args rsp_thm
   361   end
   362 
   363 exception CODE_CERT_GEN of string
   364 
   365 fun simplify_code_eq ctxt def_thm = 
   366   Local_Defs.unfold ctxt [@{thm o_apply}, @{thm map_fun_def}, @{thm id_apply}] def_thm
   367 
   368 (*
   369   quot_thm - quotient theorem (Quotient R Abs Rep T).
   370   returns: whether the Lifting package is capable to generate code for the abstract type
   371     represented by quot_thm
   372 *)
   373 
   374 fun can_generate_code_cert quot_thm  =
   375   case quot_thm_rel quot_thm of
   376     Const (@{const_name HOL.eq}, _) => true
   377     | Const (@{const_name eq_onp}, _) $ _  => true
   378     | _ => false
   379 
   380 fun generate_rep_eq ctxt def_thm rsp_thm (rty, qty) =
   381   let
   382     val unfolded_def = Conv.fconv_rule (Conv.arg_conv unfold_fun_maps_beta) def_thm
   383     val unabs_def = unabs_all_def ctxt unfolded_def
   384   in  
   385     if body_type rty = body_type qty then 
   386       SOME (simplify_code_eq ctxt (unabs_def RS @{thm meta_eq_to_obj_eq}))
   387     else 
   388       let
   389         val quot_thm = Lifting_Term.prove_quot_thm ctxt (get_body_types (rty, qty))
   390         val rel_fun = prove_rel ctxt rsp_thm (rty, qty)
   391         val rep_abs_thm = [quot_thm, rel_fun] MRSL @{thm Quotient_rep_abs_eq}
   392       in
   393         case mono_eq_prover ctxt (hd (Thm.prems_of rep_abs_thm)) of
   394           SOME mono_eq_thm =>
   395             let
   396               val rep_abs_eq = mono_eq_thm RS rep_abs_thm
   397               val rep = Thm.cterm_of ctxt (quot_thm_rep quot_thm)
   398               val rep_refl = Thm.reflexive rep RS @{thm meta_eq_to_obj_eq}
   399               val repped_eq = [rep_refl, unabs_def RS @{thm meta_eq_to_obj_eq}] MRSL @{thm cong}
   400               val code_cert = [repped_eq, rep_abs_eq] MRSL trans
   401             in
   402               SOME (simplify_code_eq ctxt code_cert)
   403             end
   404           | NONE => NONE
   405       end
   406   end
   407 
   408 fun generate_abs_eq ctxt def_thm rsp_thm quot_thm =
   409   let
   410     val abs_eq_with_assms =
   411       let
   412         val (rty, qty) = quot_thm_rty_qty quot_thm
   413         val rel = quot_thm_rel quot_thm
   414         val ty_args = get_binder_types_by_rel rel (rty, qty)
   415         val body_type = get_body_type_by_rel rel (rty, qty)
   416         val quot_ret_thm = Lifting_Term.prove_quot_thm ctxt body_type
   417         
   418         val rep_abs_folded_unmapped_thm = 
   419           let
   420             val rep_id = [quot_thm, def_thm] MRSL @{thm Quotient_Rep_eq}
   421             val ctm = Thm.dest_equals_lhs (Thm.cprop_of rep_id)
   422             val unfolded_maps_eq = unfold_fun_maps ctm
   423             val t1 = [quot_thm, def_thm, rsp_thm] MRSL @{thm Quotient_rep_abs_fold_unmap}
   424             val prems_pat = (hd o Drule.cprems_of) t1
   425             val insts = Thm.first_order_match (prems_pat, Thm.cprop_of unfolded_maps_eq)
   426           in
   427             unfolded_maps_eq RS (Drule.instantiate_normalize insts t1)
   428           end
   429       in
   430         rep_abs_folded_unmapped_thm
   431         |> fold (fn _ => fn thm => thm RS @{thm rel_funD2}) ty_args
   432         |> (fn x => x RS (@{thm Quotient_rel_abs2} OF [quot_ret_thm]))
   433       end
   434     
   435     val prem_rels = get_binder_rels (quot_thm_rel quot_thm);
   436     val proved_assms = prem_rels |> map (try_prove_refl_rel ctxt) 
   437       |> map_index (apfst (fn x => x + 1)) |> filter (is_some o snd) |> map (apsnd the) 
   438       |> map (apsnd (fn assm => assm RS @{thm ge_eq_refl}))
   439     val abs_eq = fold_rev (fn (i, assm) => fn thm => assm RSN (i, thm)) proved_assms abs_eq_with_assms
   440   in
   441     simplify_code_eq ctxt abs_eq
   442   end
   443 
   444 
   445 fun register_code_eq_thy abs_eq_thm opt_rep_eq_thm (rty, qty) thy =
   446   let
   447     fun no_abstr (t $ u) = no_abstr t andalso no_abstr u
   448       | no_abstr (Abs (_, _, t)) = no_abstr t
   449       | no_abstr (Const (name, _)) = not (Code.is_abstr thy name)
   450       | no_abstr _ = true
   451     fun is_valid_eq eqn = can (Code.assert_eqn thy) (mk_meta_eq eqn, true) 
   452       andalso no_abstr (Thm.prop_of eqn)
   453     fun is_valid_abs_eq abs_eq = can (Code.assert_abs_eqn thy NONE) (mk_meta_eq abs_eq)
   454 
   455   in
   456     if is_valid_eq abs_eq_thm then
   457       (ABS_EQ, Code.add_default_eqn abs_eq_thm thy)
   458     else
   459       let
   460         val (rty_body, qty_body) = get_body_types (rty, qty)
   461       in
   462         if rty_body = qty_body then
   463           (REP_EQ, Code.add_default_eqn (the opt_rep_eq_thm) thy)
   464         else
   465           if is_some opt_rep_eq_thm andalso is_valid_abs_eq (the opt_rep_eq_thm)
   466           then
   467             (REP_EQ, Code.add_abs_default_eqn (the opt_rep_eq_thm) thy)
   468           else
   469             (NONE_EQ, thy)
   470       end
   471   end
   472 
   473 local
   474   fun no_no_code ctxt (rty, qty) =
   475     if same_type_constrs (rty, qty) then
   476       forall (no_no_code ctxt) (Targs rty ~~ Targs qty)
   477     else
   478       if is_Type qty then
   479         if Lifting_Info.is_no_code_type ctxt (Tname qty) then false
   480         else 
   481           let 
   482             val (rty', rtyq) = Lifting_Term.instantiate_rtys ctxt (rty, qty)
   483             val (rty's, rtyqs) = (Targs rty', Targs rtyq)
   484           in
   485             forall (no_no_code ctxt) (rty's ~~ rtyqs)
   486           end
   487       else
   488         true
   489 
   490   fun encode_code_eq ctxt abs_eq opt_rep_eq (rty, qty) = 
   491     let
   492       fun mk_type typ = typ |> Logic.mk_type |> Thm.cterm_of ctxt |> Drule.mk_term
   493     in
   494       Conjunction.intr_balanced [abs_eq, (the_default TrueI opt_rep_eq), mk_type rty, mk_type qty]
   495     end
   496   
   497   exception DECODE
   498     
   499   fun decode_code_eq thm =
   500     if Thm.nprems_of thm > 0 then raise DECODE 
   501     else
   502       let
   503         val [abs_eq, rep_eq, rty, qty] = Conjunction.elim_balanced 4 thm
   504         val opt_rep_eq = if Thm.eq_thm_prop (rep_eq, TrueI) then NONE else SOME rep_eq
   505         fun dest_type typ = typ |> Drule.dest_term |> Thm.term_of |> Logic.dest_type
   506       in
   507         (abs_eq, opt_rep_eq, (dest_type rty, dest_type qty)) 
   508       end
   509   
   510   structure Data = Generic_Data
   511   (
   512     type T = code_eq option
   513     val empty = NONE
   514     val extend = I
   515     fun merge _ = NONE
   516   );
   517 
   518   fun register_encoded_code_eq thm thy =
   519     let
   520       val (abs_eq_thm, opt_rep_eq_thm, (rty, qty)) = decode_code_eq thm
   521       val (code_eq, thy) = register_code_eq_thy abs_eq_thm opt_rep_eq_thm (rty, qty) thy
   522     in
   523       Context.theory_map (Data.put (SOME code_eq)) thy
   524     end
   525     handle DECODE => thy
   526   
   527   val register_code_eq_attribute = Thm.declaration_attribute
   528     (fn thm => Context.mapping (register_encoded_code_eq thm) I)
   529   val register_code_eq_attrib = Attrib.internal (K register_code_eq_attribute)
   530 
   531 in
   532 
   533 fun register_code_eq abs_eq_thm opt_rep_eq_thm (rty, qty) lthy =
   534   let
   535     val encoded_code_eq = encode_code_eq lthy abs_eq_thm opt_rep_eq_thm (rty, qty)
   536   in
   537     if no_no_code lthy (rty, qty) then
   538       let
   539         val lthy = (snd oo Local_Theory.note) 
   540           ((Binding.empty, [register_code_eq_attrib]), [encoded_code_eq]) lthy
   541         val opt_code_eq = Data.get (Context.Theory (Proof_Context.theory_of lthy))
   542         val code_eq = if is_some opt_code_eq then the opt_code_eq 
   543           else UNKNOWN_EQ (* UNKNOWN_EQ means that we are in a locale and we do not know
   544             which code equation is going to be used. This is going to be resolved at the
   545             point when an interpretation of the locale is executed. *)
   546         val lthy = Local_Theory.declaration {syntax = false, pervasive = true} 
   547           (K (Data.put NONE)) lthy
   548       in
   549         (code_eq, lthy)
   550       end
   551     else
   552       (NONE_EQ, lthy)
   553   end
   554 end
   555             
   556 (*
   557   Defines an operation on an abstract type in terms of a corresponding operation 
   558     on a representation type.
   559 
   560   var - a binding and a mixfix of the new constant being defined
   561   qty - an abstract type of the new constant
   562   rhs - a term representing the new constant on the raw level
   563   rsp_thm - a respectfulness theorem in the internal tagged form (like '(R ===> R ===> R) f f'),
   564     i.e. "(Lifting_Term.equiv_relation (fastype_of rhs, qty)) $ rhs $ rhs"
   565   par_thms - a parametricity theorem for rhs
   566 *)
   567 
   568 fun add_lift_def (config: config) var qty rhs rsp_thm par_thms lthy =
   569   let
   570     val rty = fastype_of rhs
   571     val quot_thm = Lifting_Term.prove_quot_thm lthy (rty, qty)
   572     val absrep_trm =  quot_thm_abs quot_thm
   573     val rty_forced = (domain_type o fastype_of) absrep_trm
   574     val forced_rhs = force_rty_type lthy rty_forced rhs
   575     val lhs = Free (Binding.name_of (#1 var), qty)
   576     val prop = Logic.mk_equals (lhs, absrep_trm $ forced_rhs)
   577     val (_, prop') = Local_Defs.cert_def lthy prop
   578     val (_, newrhs) = Local_Defs.abs_def prop'
   579     val var = (#notes config = false ? apfst Binding.concealed) var
   580     val def_name = if #notes config then Thm.def_binding (#1 var) else Binding.empty
   581     
   582     val ((lift_const, (_ , def_thm)), lthy) = 
   583       Local_Theory.define (var, ((def_name, []), newrhs)) lthy
   584 
   585     val transfer_rules = generate_transfer_rules lthy quot_thm rsp_thm def_thm par_thms
   586 
   587     val abs_eq_thm = generate_abs_eq lthy def_thm rsp_thm quot_thm
   588     val opt_rep_eq_thm = generate_rep_eq lthy def_thm rsp_thm (rty_forced, qty)
   589 
   590     fun qualify defname suffix = Binding.qualified true suffix defname
   591 
   592     fun notes names =
   593       let
   594         val lhs_name = (#1 var)
   595         val rsp_thmN = qualify lhs_name "rsp"
   596         val abs_eq_thmN = qualify lhs_name "abs_eq"
   597         val rep_eq_thmN = qualify lhs_name "rep_eq"
   598         val transfer_ruleN = qualify lhs_name "transfer"
   599         val notes = 
   600           [(rsp_thmN, [], [rsp_thm]), 
   601           (transfer_ruleN, @{attributes [transfer_rule]}, transfer_rules),
   602           (abs_eq_thmN, [], [abs_eq_thm])] 
   603           @ (case opt_rep_eq_thm of SOME rep_eq_thm => [(rep_eq_thmN, [], [rep_eq_thm])] | NONE => [])
   604       in
   605         if names then map (fn (name, attrs, thms) => ((name, []), [(thms, attrs)])) notes
   606         else map_filter (fn (_, attrs, thms) => if null attrs then NONE 
   607           else SOME ((Binding.empty, []), [(thms, attrs)])) notes
   608       end
   609     val (code_eq, lthy) = register_code_eq abs_eq_thm opt_rep_eq_thm (rty_forced, qty) lthy
   610     val lift_def = mk_lift_def rty_forced qty newrhs lift_const def_thm rsp_thm abs_eq_thm 
   611           opt_rep_eq_thm code_eq transfer_rules
   612   in
   613     lthy
   614       |> Local_Theory.notes (notes (#notes config)) |> snd
   615       |> ` (fn lthy => morph_lift_def (Local_Theory.target_morphism lthy) lift_def)
   616       ||> Local_Theory.restore
   617   end
   618 
   619 (* This is not very cheap way of getting the rules but we have only few active
   620   liftings in the current setting *)
   621 fun get_cr_pcr_eqs ctxt =
   622   let
   623     fun collect (data : Lifting_Info.quotient) l =
   624       if is_some (#pcr_info data) 
   625       then ((Thm.symmetric o safe_mk_meta_eq o #pcr_cr_eq o the o #pcr_info) data :: l) 
   626       else l
   627     val table = Lifting_Info.get_quotients ctxt
   628   in
   629     Symtab.fold (fn (_, data) => fn l => collect data l) table []
   630   end
   631 
   632 fun prepare_lift_def add_lift_def var qty rhs par_thms lthy =
   633   let
   634     val rsp_rel = Lifting_Term.equiv_relation lthy (fastype_of rhs, qty)
   635     val rty_forced = (domain_type o fastype_of) rsp_rel;
   636     val forced_rhs = force_rty_type lthy rty_forced rhs;
   637     val cr_to_pcr_conv = HOLogic.Trueprop_conv (Conv.fun2_conv 
   638       (Raw_Simplifier.rewrite lthy false (get_cr_pcr_eqs lthy)))
   639     val (prsp_tm, rsp_prsp_eq) = HOLogic.mk_Trueprop (rsp_rel $ forced_rhs $ forced_rhs)
   640       |> Thm.cterm_of lthy
   641       |> cr_to_pcr_conv
   642       |> `Thm.concl_of
   643       |>> Logic.dest_equals
   644       |>> snd
   645     val to_rsp = rsp_prsp_eq RS Drule.equal_elim_rule2
   646     val opt_proven_rsp_thm = try_prove_reflexivity lthy prsp_tm
   647     
   648     fun after_qed internal_rsp_thm lthy = 
   649       add_lift_def var qty rhs (internal_rsp_thm RS to_rsp) par_thms lthy
   650   in
   651     case opt_proven_rsp_thm of
   652       SOME thm => (NONE, K (after_qed thm))
   653       | NONE => (SOME prsp_tm, after_qed) 
   654   end
   655 
   656 fun gen_lift_def add_lift_def var qty rhs tac par_thms lthy =
   657   let
   658     val (goal, after_qed) = prepare_lift_def add_lift_def var qty rhs par_thms lthy
   659   in
   660     case goal of
   661       SOME goal => 
   662         let 
   663           val rsp_thm = Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} => tac ctxt)
   664             |> Thm.close_derivation
   665         in
   666           after_qed rsp_thm lthy
   667         end
   668       | NONE => after_qed Drule.dummy_thm lthy
   669   end
   670 
   671 fun lift_def config var qty rhs tac par_thms lthy = gen_lift_def (add_lift_def config)
   672   var qty rhs tac par_thms lthy
   673 
   674 end (* structure *)