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
authorkuncar
Sat May 02 13:58:06 2015 +0200 (2015-05-02)
changeset 602310daab758e087
parent 60230 4857d553c52c
child 60232 29ac1c6a1fbb
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
src/HOL/Tools/Lifting/lifting_def.ML
src/HOL/Tools/Lifting/lifting_def_code_dt.ML
src/HOL/Tools/Lifting/lifting_setup.ML
     1.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Mon Apr 13 15:27:34 2015 +0200
     1.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Sat May 02 13:58:06 2015 +0200
     1.3 @@ -37,7 +37,7 @@
     1.4      (binding * mixfix -> typ -> term -> thm -> thm list -> Proof.context -> 
     1.5        lift_def * local_theory) -> 
     1.6      binding * mixfix -> typ -> term -> thm list -> local_theory -> 
     1.7 -    term option * (thm list list -> Proof.context -> lift_def * local_theory)
     1.8 +    term option * (thm -> Proof.context -> lift_def * local_theory)
     1.9  
    1.10    val gen_lift_def:
    1.11      (binding * mixfix -> typ -> term -> thm -> thm list -> local_theory -> 
    1.12 @@ -616,112 +616,6 @@
    1.13        ||> Local_Theory.restore
    1.14    end
    1.15  
    1.16 -local
    1.17 -  val eq_onp_assms_tac_fixed_rules = map (Transfer.prep_transfer_domain_thm @{context})
    1.18 -    [@{thm pcr_Domainp_total}, @{thm pcr_Domainp_par_left_total}, @{thm pcr_Domainp_par}, 
    1.19 -      @{thm pcr_Domainp}]
    1.20 -in
    1.21 -fun mk_readable_rsp_thm_eq tm lthy =
    1.22 -  let
    1.23 -    val ctm = Thm.cterm_of lthy tm
    1.24 -    
    1.25 -    fun assms_rewr_conv tactic rule ct =
    1.26 -      let
    1.27 -        fun prove_extra_assms thm =
    1.28 -          let
    1.29 -            val assms = cprems_of thm
    1.30 -            fun finish thm = if Thm.no_prems thm then SOME (Goal.conclude thm) else NONE
    1.31 -            fun prove ctm = Option.mapPartial finish (SINGLE tactic (Goal.init ctm))
    1.32 -          in
    1.33 -            map_interrupt prove assms
    1.34 -          end
    1.35 -    
    1.36 -        fun cconl_of thm = Drule.strip_imp_concl (Thm.cprop_of thm)
    1.37 -        fun lhs_of thm = fst (Thm.dest_equals (cconl_of thm))
    1.38 -        fun rhs_of thm = snd (Thm.dest_equals (cconl_of thm))
    1.39 -        val rule1 = Thm.incr_indexes (Thm.maxidx_of_cterm ct + 1) rule;
    1.40 -        val lhs = lhs_of rule1;
    1.41 -        val rule2 = Thm.rename_boundvars (Thm.term_of lhs) (Thm.term_of ct) rule1;
    1.42 -        val rule3 =
    1.43 -          Thm.instantiate (Thm.match (lhs, ct)) rule2
    1.44 -            handle Pattern.MATCH => raise CTERM ("assms_rewr_conv", [lhs, ct]);
    1.45 -        val proved_assms = prove_extra_assms rule3
    1.46 -      in
    1.47 -        case proved_assms of
    1.48 -          SOME proved_assms =>
    1.49 -            let
    1.50 -              val rule3 = proved_assms MRSL rule3
    1.51 -              val rule4 =
    1.52 -                if lhs_of rule3 aconvc ct then rule3
    1.53 -                else
    1.54 -                  let val ceq = Thm.dest_fun2 (Thm.cprop_of rule3)
    1.55 -                  in rule3 COMP Thm.trivial (Thm.mk_binop ceq ct (rhs_of rule3)) end
    1.56 -            in Thm.transitive rule4 (Thm.beta_conversion true (rhs_of rule4)) end
    1.57 -          | NONE => Conv.no_conv ct
    1.58 -      end
    1.59 -
    1.60 -    fun assms_rewrs_conv tactic rules = Conv.first_conv (map (assms_rewr_conv tactic) rules)
    1.61 -
    1.62 -    fun simp_arrows_conv ctm =
    1.63 -      let
    1.64 -        val unfold_conv = Conv.rewrs_conv 
    1.65 -          [@{thm rel_fun_eq_eq_onp[THEN eq_reflection]}, 
    1.66 -            @{thm rel_fun_eq_onp_rel[THEN eq_reflection]},
    1.67 -            @{thm rel_fun_eq[THEN eq_reflection]},
    1.68 -            @{thm rel_fun_eq_rel[THEN eq_reflection]}, 
    1.69 -            @{thm rel_fun_def[THEN eq_reflection]}]
    1.70 -        fun binop_conv2 cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
    1.71 -        val eq_onp_assms_tac_rules = @{thm left_unique_OO} :: 
    1.72 -            eq_onp_assms_tac_fixed_rules @ (Transfer.get_transfer_raw lthy)
    1.73 -        val intro_top_rule = @{thm eq_onp_top_eq_eq[symmetric, THEN eq_reflection]}
    1.74 -        val kill_tops = Transfer.top_sweep_rewr_conv [@{thm eq_onp_top_eq_eq[THEN eq_reflection]}]
    1.75 -        val eq_onp_assms_tac = (CONVERSION kill_tops THEN' 
    1.76 -          TRY o REPEAT_ALL_NEW (resolve_tac lthy eq_onp_assms_tac_rules) 
    1.77 -          THEN_ALL_NEW (DETERM o Transfer.eq_tac lthy)) 1
    1.78 -        val relator_eq_onp_conv = Conv.bottom_conv
    1.79 -          (K (Conv.try_conv (assms_rewrs_conv eq_onp_assms_tac
    1.80 -            (intro_top_rule :: Lifting_Info.get_relator_eq_onp_rules lthy)))) lthy
    1.81 -          then_conv kill_tops
    1.82 -        val relator_eq_conv = Conv.bottom_conv
    1.83 -          (K (Conv.try_conv (Conv.rewrs_conv (Transfer.get_relator_eq lthy)))) lthy
    1.84 -      in
    1.85 -        case (Thm.term_of ctm) of
    1.86 -          Const (@{const_name "rel_fun"}, _) $ _ $ _ => 
    1.87 -            (binop_conv2 simp_arrows_conv simp_arrows_conv then_conv unfold_conv) ctm
    1.88 -          | _ => (relator_eq_onp_conv then_conv relator_eq_conv) ctm
    1.89 -      end
    1.90 -    
    1.91 -    val unfold_ret_val_invs = Conv.bottom_conv 
    1.92 -      (K (Conv.try_conv (Conv.rewr_conv @{thm eq_onp_same_args[THEN eq_reflection]}))) lthy
    1.93 -    val unfold_inv_conv = 
    1.94 -      Conv.top_sweep_conv (K (Conv.rewr_conv @{thm eq_onp_def[THEN eq_reflection]})) lthy
    1.95 -    val simp_conv = HOLogic.Trueprop_conv (Conv.fun2_conv simp_arrows_conv)
    1.96 -    val univq_conv = Conv.rewr_conv @{thm HOL.all_simps(6)[symmetric, THEN eq_reflection]}
    1.97 -    val univq_prenex_conv = Conv.top_conv (K (Conv.try_conv univq_conv)) lthy
    1.98 -    val beta_conv = Thm.beta_conversion true
    1.99 -    val eq_thm = 
   1.100 -      (simp_conv then_conv univq_prenex_conv then_conv beta_conv then_conv unfold_ret_val_invs
   1.101 -         then_conv unfold_inv_conv) ctm
   1.102 -  in
   1.103 -    Object_Logic.rulify lthy (eq_thm RS Drule.equal_elim_rule2)
   1.104 -  end
   1.105 -end
   1.106 -
   1.107 -fun rename_to_tnames ctxt term =
   1.108 -  let
   1.109 -    fun all_typs (Const (@{const_name Pure.all}, _) $ Abs (_, T, t)) = T :: all_typs t
   1.110 -      | all_typs _ = []
   1.111 -
   1.112 -    fun rename (Const (@{const_name Pure.all}, T1) $ Abs (_, T2, t)) (new_name :: names) = 
   1.113 -        (Const (@{const_name Pure.all}, T1) $ Abs (new_name, T2, rename t names)) 
   1.114 -      | rename t _ = t
   1.115 -
   1.116 -    val (fixed_def_t, _) = yield_singleton (Variable.importT_terms) term ctxt
   1.117 -    val new_names = Old_Datatype_Prop.make_tnames (all_typs fixed_def_t)
   1.118 -  in
   1.119 -    rename term new_names
   1.120 -  end
   1.121 -
   1.122  (* This is not very cheap way of getting the rules but we have only few active
   1.123    liftings in the current setting *)
   1.124  fun get_cr_pcr_eqs ctxt =
   1.125 @@ -756,23 +650,7 @@
   1.126    in
   1.127      case opt_proven_rsp_thm of
   1.128        SOME thm => (NONE, K (after_qed thm))
   1.129 -      | NONE =>  
   1.130 -        let
   1.131 -          val readable_rsp_thm_eq = mk_readable_rsp_thm_eq prsp_tm lthy
   1.132 -          val (readable_rsp_tm, _) = Logic.dest_implies (Thm.prop_of readable_rsp_thm_eq)
   1.133 -          val readable_rsp_tm_tnames = rename_to_tnames lthy readable_rsp_tm
   1.134 -      
   1.135 -          fun after_qed' thm_list lthy = 
   1.136 -            let
   1.137 -              val internal_rsp_thm = Goal.prove lthy [] [] prsp_tm 
   1.138 -                  (fn {context = ctxt, ...} =>
   1.139 -                    rtac readable_rsp_thm_eq 1 THEN Proof_Context.fact_tac ctxt (hd thm_list) 1)
   1.140 -            in
   1.141 -              after_qed internal_rsp_thm lthy
   1.142 -            end
   1.143 -        in
   1.144 -          (SOME readable_rsp_tm_tnames, after_qed')
   1.145 -        end 
   1.146 +      | NONE => (SOME prsp_tm, after_qed) 
   1.147    end
   1.148  
   1.149  fun gen_lift_def add_lift_def var qty rhs tac par_thms lthy =
   1.150 @@ -785,9 +663,9 @@
   1.151            val rsp_thm = Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} => tac ctxt)
   1.152              |> Thm.close_derivation
   1.153          in
   1.154 -          after_qed [[rsp_thm]] lthy
   1.155 +          after_qed rsp_thm lthy
   1.156          end
   1.157 -      | NONE => after_qed [[Drule.dummy_thm]] lthy
   1.158 +      | NONE => after_qed Drule.dummy_thm lthy
   1.159    end
   1.160  
   1.161  fun lift_def config var qty rhs tac par_thms lthy = gen_lift_def (add_lift_def config)
     2.1 --- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Mon Apr 13 15:27:34 2015 +0200
     2.2 +++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Sat May 02 13:58:06 2015 +0200
     2.3 @@ -46,8 +46,10 @@
     2.4  
     2.5  structure Lifting_Def_Code_Dt: LIFTING_DEF_CODE_DT =
     2.6  struct
     2.7 +                                                                       
     2.8 +open Ctr_Sugar_Util BNF_Util BNF_FP_Util BNF_FP_Def_Sugar Lifting_Def Lifting_Util
     2.9  
    2.10 -open Ctr_Sugar_Util BNF_Util BNF_FP_Util BNF_FP_Def_Sugar Lifting_Def Lifting_Util
    2.11 +infix 0 MRSL
    2.12  
    2.13  (** data structures **)
    2.14  
    2.15 @@ -272,7 +274,7 @@
    2.16              val f'_qty = strip_type qty |> fst |> rpair qty_isom |> op --->
    2.17              val f'_rsp_rel = Lifting_Term.equiv_relation lthy (rty, f'_qty);
    2.18              val rsp = rsp_thm_of_lift_def lift_def
    2.19 -            val rel_eq_onps_conv = HOLogic.Trueprop_conv (ret_rel_conv (R_conv rel_eq_onps))
    2.20 +            val rel_eq_onps_conv = HOLogic.Trueprop_conv (Conv.fun2_conv (ret_rel_conv (R_conv rel_eq_onps)))
    2.21              val rsp_norm = Conv.fconv_rule rel_eq_onps_conv rsp
    2.22              val f'_rsp_goal = HOLogic.mk_Trueprop (f'_rsp_rel $ rhs $ rhs);
    2.23              val f'_rsp = Goal.prove_sorry lthy [] [] f'_rsp_goal
    2.24 @@ -366,20 +368,31 @@
    2.25        lift_def ld_no_notes (b, NoSyn) dis_qty rhs (K all_tac) [] lthy
    2.26        |> apfst (mk_lift_const_of_lift_def dis_qty)) dis_names dis_rhs lthy
    2.27  
    2.28 +    fun eq_onp_to_top_tac ctxt = SELECT_GOAL (Local_Defs.unfold_tac ctxt 
    2.29 +      (@{thm eq_onp_top_eq_eq[symmetric]} :: Lifting_Info.get_relator_eq_onp_rules ctxt))
    2.30 +
    2.31 +    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"
    2.32 +      by (simp add: eq_onp_same_args rel_fun_eq_onp_rel)}
    2.33 +
    2.34      fun lift_sel_tac exhaust_rule dt_rules wits ctxt i =
    2.35 -      (Method.insert_tac wits THEN' case_tac exhaust_rule ctxt THEN_ALL_NEW (
    2.36 -      EVERY' [hyp_subst_tac ctxt, Raw_Simplifier.rewrite_goal_tac ctxt (map safe_mk_meta_eq dt_rules),
    2.37 +        (Method.insert_tac wits THEN' 
    2.38 +         eq_onp_to_top_tac ctxt THEN' (* normalize *)
    2.39 +         rtac unfold_lift_sel_rsp THEN'
    2.40 +         case_tac exhaust_rule ctxt THEN_ALL_NEW (
    2.41 +        EVERY' [hyp_subst_tac ctxt, (* does not kill wits because = was rewritten to eq_onp top *)
    2.42 +        Raw_Simplifier.rewrite_goal_tac ctxt (map safe_mk_meta_eq dt_rules), 
    2.43          REPEAT_DETERM o etac conjE, atac])) i
    2.44      val pred_simps = Transfer.lookup_pred_data lthy (Tname rty) |> the |> Transfer.pred_simps
    2.45      val sel_tac = lift_sel_tac (#exhaust ctr_sugar) (#case_thms ctr_sugar @ pred_simps)
    2.46      val sel_names = map (fn (k, xs) => map (fn k' => Binding.qualified true
    2.47        ("sel" ^ string_of_int k ^ string_of_int k') uTname) (1 upto length xs)) (ks ~~ ctr_Tss);
    2.48      val (selss, lthy) = @{fold_map 2} (@{fold_map 2} (fn b => fn ((_, qty_ret), wits, rhs) => fn lthy =>
    2.49 -      lift_def_code_dt { code_dt = true, lift_config = ld_no_notes }
    2.50 +        lift_def_code_dt { code_dt = true, lift_config = ld_no_notes }
    2.51          (b, NoSyn) (qty_isom --> qty_ret) rhs (HEADGOAL o sel_tac wits) [] lthy
    2.52        |> apfst (mk_lift_const_of_lift_def (qty_isom --> qty_ret)))) sel_names sel_rhs lthy
    2.53  
    2.54 -    fun lift_isom_tac ctxt = Local_Defs.unfold_tac ctxt [id_apply] THEN HEADGOAL atac;
    2.55 +    fun lift_isom_tac ctxt = HEADGOAL (eq_onp_to_top_tac ctxt
    2.56 +      THEN' (rtac @{thm id_transfer}));
    2.57  
    2.58      val (rep_isom_lift_def, lthy) = lift_def ld_no_notes (Binding.qualified true "Rep_isom" uTname, NoSyn)
    2.59        (qty_isom --> qty) (HOLogic.id_const rty) lift_isom_tac [] lthy
    2.60 @@ -387,7 +400,6 @@
    2.61      val (abs_isom, lthy) = lift_def ld_no_notes (Binding.qualified true "Abs_isom" uTname, NoSyn)
    2.62        (qty --> qty_isom) (HOLogic.id_const rty) lift_isom_tac [] lthy
    2.63        |> apfst (mk_lift_const_of_lift_def (qty --> qty_isom));
    2.64 -
    2.65      fun mk_type_definition newT oldT RepC AbsC A =
    2.66        let
    2.67          val typedefC =
    2.68 @@ -398,12 +410,13 @@
    2.69      val rep_isom = lift_const_of_lift_def rep_isom_lift_def
    2.70      val typedef_goal = mk_type_definition qty_isom qty rep_isom abs_isom (HOLogic.mk_UNIV qty) |>
    2.71        HOLogic.mk_Trueprop;
    2.72 -
    2.73 -      fun typ_isom_tac ctxt i =
    2.74 -        EVERY' [ SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms type_definition_def}),
    2.75 -          DETERM o Transfer.transfer_tac true ctxt, Raw_Simplifier.rewrite_goal_tac ctxt
    2.76 -            (map safe_mk_meta_eq @{thms id_apply simp_thms Ball_def}),
    2.77 -           rtac TrueI] i;
    2.78 +    fun typ_isom_tac ctxt i =
    2.79 +      EVERY' [ SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms type_definition_def}),
    2.80 +        DETERM o Transfer.transfer_tac true ctxt,
    2.81 +          SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms eq_onp_top_eq_eq}) (* normalize *), 
    2.82 +          Raw_Simplifier.rewrite_goal_tac ctxt 
    2.83 +          (map safe_mk_meta_eq @{thms id_apply simp_thms Ball_def}),
    2.84 +         rtac TrueI] i;
    2.85  
    2.86      val (_, transfer_lthy) = Proof_Context.note_thmss "" [((Binding.empty, []),
    2.87        [(@{thms right_total_UNIV_transfer},[Transfer.transfer_add]),
    2.88 @@ -414,9 +427,8 @@
    2.89        |> Thm.close_derivation
    2.90        |> singleton (Variable.export transfer_lthy lthy)
    2.91        |> (fn thm => @{thm UNIV_typedef_to_Quotient} OF [thm, @{thm reflexive}])
    2.92 -
    2.93      val qty_isom_name = Tname qty_isom;
    2.94 -
    2.95 +    
    2.96      val quot_isom_rep =
    2.97        let
    2.98          val (quotients : Lifting_Term.quotients) = Symtab.insert (Lifting_Info.quotient_eq) (qty_isom_name,
    2.99 @@ -485,7 +497,6 @@
   2.100        (fn {context = ctxt, prems = _} => rep_isom_code_tac ctr_sugar ctxt 1)
   2.101        |> Thm.close_derivation
   2.102        |> singleton(Variable.export lthy x_lthy)
   2.103 -
   2.104      val lthy = x_lthy
   2.105      val pointer = Lifting_Setup.pointer_of_bundle_binding lthy qty_isom_bundle
   2.106      fun code_dt phi context = code_dt_of lthy (rty, qty) |> the |>
   2.107 @@ -510,6 +521,7 @@
   2.108      val pred_data = if is_some pred_data then the pred_data
   2.109        else error ("code_dt: " ^ quote rty_name ^ " is not a datatype.")
   2.110      val rel_eq_onp = safe_mk_meta_eq (Transfer.rel_eq_onp pred_data);
   2.111 +    val rel_eq_onps = insert Thm.eq_thm rel_eq_onp rel_eq_onps
   2.112      val R_conv = Transfer.top_sweep_rewr_conv @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]}
   2.113        then_conv Conv.rewr_conv rel_eq_onp
   2.114      val quot_thm = Conv.fconv_rule(HOLogic.Trueprop_conv (Quotient_R_conv R_conv)) quot_thm;
   2.115 @@ -522,12 +534,12 @@
   2.116          val TFrees = Term.add_tfreesT qty []
   2.117  
   2.118          fun non_empty_typedef_tac non_empty_pred ctxt i =
   2.119 -          (SELECT_GOAL (Local_Defs.unfold_tac ctxt [mem_Collect_eq]) THEN' rtac non_empty_pred) i
   2.120 -
   2.121 +          (Method.insert_tac [non_empty_pred] THEN' 
   2.122 +            SELECT_GOAL (Local_Defs.unfold_tac ctxt [mem_Collect_eq]) THEN' atac) i
   2.123          val uTname = unique_Tname (rty, qty)
   2.124          val Tdef_set = HOLogic.mk_Collect ("x", rty, pred $ Free("x", rty));
   2.125          val ((_, tcode_dt), lthy) = conceal_naming_result (typedef (Binding.concealed uTname, TFrees, NoSyn)
   2.126 -          Tdef_set NONE (fn lthy => non_empty_typedef_tac non_empty_pred lthy 1)) lthy;
   2.127 +          Tdef_set NONE (fn lthy => HEADGOAL (non_empty_typedef_tac non_empty_pred lthy))) lthy;
   2.128          val type_definition_thm = tcode_dt |> snd |> #type_definition;
   2.129          val qty_isom = tcode_dt |> fst |> #abs_type;
   2.130  
   2.131 @@ -542,10 +554,10 @@
   2.132            |> Local_Theory.restore
   2.133            |> mk_rep_isom binding (rty, qty, qty_isom) |> snd
   2.134        in
   2.135 -        (quot_thm, (lthy, rel_eq_onp :: rel_eq_onps))
   2.136 +        (quot_thm, (lthy, rel_eq_onps))
   2.137        end
   2.138      else
   2.139 -      (quot_thm, (lthy, rel_eq_onp :: rel_eq_onps))
   2.140 +      (quot_thm, (lthy, rel_eq_onps))
   2.141    end
   2.142  and lift_def_code_dt config var qty rhs tac par_thms lthy = gen_lift_def (add_lift_def_code_dt config)
   2.143    var qty rhs tac par_thms lthy
   2.144 @@ -577,6 +589,112 @@
   2.145  
   2.146  **)
   2.147  
   2.148 +local
   2.149 +  val eq_onp_assms_tac_fixed_rules = map (Transfer.prep_transfer_domain_thm @{context})
   2.150 +    [@{thm pcr_Domainp_total}, @{thm pcr_Domainp_par_left_total}, @{thm pcr_Domainp_par}, 
   2.151 +      @{thm pcr_Domainp}]
   2.152 +in
   2.153 +fun mk_readable_rsp_thm_eq tm lthy =
   2.154 +  let
   2.155 +    val ctm = Thm.cterm_of lthy tm
   2.156 +    
   2.157 +    fun assms_rewr_conv tactic rule ct =
   2.158 +      let
   2.159 +        fun prove_extra_assms thm =
   2.160 +          let
   2.161 +            val assms = cprems_of thm
   2.162 +            fun finish thm = if Thm.no_prems thm then SOME (Goal.conclude thm) else NONE
   2.163 +            fun prove ctm = Option.mapPartial finish (SINGLE tactic (Goal.init ctm))
   2.164 +          in
   2.165 +            map_interrupt prove assms
   2.166 +          end
   2.167 +    
   2.168 +        fun cconl_of thm = Drule.strip_imp_concl (Thm.cprop_of thm)
   2.169 +        fun lhs_of thm = fst (Thm.dest_equals (cconl_of thm))
   2.170 +        fun rhs_of thm = snd (Thm.dest_equals (cconl_of thm))
   2.171 +        val rule1 = Thm.incr_indexes (Thm.maxidx_of_cterm ct + 1) rule;
   2.172 +        val lhs = lhs_of rule1;
   2.173 +        val rule2 = Thm.rename_boundvars (Thm.term_of lhs) (Thm.term_of ct) rule1;
   2.174 +        val rule3 =
   2.175 +          Thm.instantiate (Thm.match (lhs, ct)) rule2
   2.176 +            handle Pattern.MATCH => raise CTERM ("assms_rewr_conv", [lhs, ct]);
   2.177 +        val proved_assms = prove_extra_assms rule3
   2.178 +      in
   2.179 +        case proved_assms of
   2.180 +          SOME proved_assms =>
   2.181 +            let
   2.182 +              val rule3 = proved_assms MRSL rule3
   2.183 +              val rule4 =
   2.184 +                if lhs_of rule3 aconvc ct then rule3
   2.185 +                else
   2.186 +                  let val ceq = Thm.dest_fun2 (Thm.cprop_of rule3)
   2.187 +                  in rule3 COMP Thm.trivial (Thm.mk_binop ceq ct (rhs_of rule3)) end
   2.188 +            in Thm.transitive rule4 (Thm.beta_conversion true (rhs_of rule4)) end
   2.189 +          | NONE => Conv.no_conv ct
   2.190 +      end
   2.191 +
   2.192 +    fun assms_rewrs_conv tactic rules = Conv.first_conv (map (assms_rewr_conv tactic) rules)
   2.193 +
   2.194 +    fun simp_arrows_conv ctm =
   2.195 +      let
   2.196 +        val unfold_conv = Conv.rewrs_conv 
   2.197 +          [@{thm rel_fun_eq_eq_onp[THEN eq_reflection]}, 
   2.198 +            @{thm rel_fun_eq_onp_rel[THEN eq_reflection]},
   2.199 +            @{thm rel_fun_eq[THEN eq_reflection]},
   2.200 +            @{thm rel_fun_eq_rel[THEN eq_reflection]}, 
   2.201 +            @{thm rel_fun_def[THEN eq_reflection]}]
   2.202 +        fun binop_conv2 cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
   2.203 +        val eq_onp_assms_tac_rules = @{thm left_unique_OO} :: 
   2.204 +            eq_onp_assms_tac_fixed_rules @ (Transfer.get_transfer_raw lthy)
   2.205 +        val intro_top_rule = @{thm eq_onp_top_eq_eq[symmetric, THEN eq_reflection]}
   2.206 +        val kill_tops = Transfer.top_sweep_rewr_conv [@{thm eq_onp_top_eq_eq[THEN eq_reflection]}]
   2.207 +        val eq_onp_assms_tac = (CONVERSION kill_tops THEN' 
   2.208 +          TRY o REPEAT_ALL_NEW (resolve_tac lthy eq_onp_assms_tac_rules) 
   2.209 +          THEN_ALL_NEW (DETERM o Transfer.eq_tac lthy)) 1
   2.210 +        val relator_eq_onp_conv = Conv.bottom_conv
   2.211 +          (K (Conv.try_conv (assms_rewrs_conv eq_onp_assms_tac
   2.212 +            (intro_top_rule :: Lifting_Info.get_relator_eq_onp_rules lthy)))) lthy
   2.213 +          then_conv kill_tops
   2.214 +        val relator_eq_conv = Conv.bottom_conv
   2.215 +          (K (Conv.try_conv (Conv.rewrs_conv (Transfer.get_relator_eq lthy)))) lthy
   2.216 +      in
   2.217 +        case (Thm.term_of ctm) of
   2.218 +          Const (@{const_name "rel_fun"}, _) $ _ $ _ => 
   2.219 +            (binop_conv2 simp_arrows_conv simp_arrows_conv then_conv unfold_conv) ctm
   2.220 +          | _ => (relator_eq_onp_conv then_conv relator_eq_conv) ctm
   2.221 +      end
   2.222 +    
   2.223 +    val unfold_ret_val_invs = Conv.bottom_conv 
   2.224 +      (K (Conv.try_conv (Conv.rewr_conv @{thm eq_onp_same_args[THEN eq_reflection]}))) lthy
   2.225 +    val unfold_inv_conv = 
   2.226 +      Conv.top_sweep_conv (K (Conv.rewr_conv @{thm eq_onp_def[THEN eq_reflection]})) lthy
   2.227 +    val simp_conv = HOLogic.Trueprop_conv (Conv.fun2_conv simp_arrows_conv)
   2.228 +    val univq_conv = Conv.rewr_conv @{thm HOL.all_simps(6)[symmetric, THEN eq_reflection]}
   2.229 +    val univq_prenex_conv = Conv.top_conv (K (Conv.try_conv univq_conv)) lthy
   2.230 +    val beta_conv = Thm.beta_conversion true
   2.231 +    val eq_thm = 
   2.232 +      (simp_conv then_conv univq_prenex_conv then_conv beta_conv then_conv unfold_ret_val_invs
   2.233 +         then_conv unfold_inv_conv) ctm
   2.234 +  in
   2.235 +    Object_Logic.rulify lthy (eq_thm RS Drule.equal_elim_rule2)
   2.236 +  end
   2.237 +end
   2.238 +
   2.239 +fun rename_to_tnames ctxt term =
   2.240 +  let
   2.241 +    fun all_typs (Const (@{const_name Pure.all}, _) $ Abs (_, T, t)) = T :: all_typs t
   2.242 +      | all_typs _ = []
   2.243 +
   2.244 +    fun rename (Const (@{const_name Pure.all}, T1) $ Abs (_, T2, t)) (new_name :: names) = 
   2.245 +        (Const (@{const_name Pure.all}, T1) $ Abs (new_name, T2, rename t names)) 
   2.246 +      | rename t _ = t
   2.247 +
   2.248 +    val (fixed_def_t, _) = yield_singleton (Variable.importT_terms) term ctxt
   2.249 +    val new_names = Old_Datatype_Prop.make_tnames (all_typs fixed_def_t)
   2.250 +  in
   2.251 +    rename term new_names
   2.252 +  end
   2.253 +
   2.254  fun lift_def_cmd (params, raw_var, rhs_raw, par_xthms) lthy =
   2.255    let
   2.256      val config = evaluate_params params
   2.257 @@ -585,6 +703,26 @@
   2.258      val rhs = (Syntax.check_term lthy o Syntax.parse_term lthy) rhs_raw
   2.259      val par_thms = Attrib.eval_thms lthy par_xthms
   2.260      val (goal, after_qed) = prepare_lift_def (add_lift_def_code_dt config) var qty rhs par_thms lthy
   2.261 +    val (goal, after_qed) =
   2.262 +      case goal of
   2.263 +        NONE => (goal, K (after_qed Drule.dummy_thm))
   2.264 +        | SOME prsp_tm =>
   2.265 +          let
   2.266 +            val readable_rsp_thm_eq = mk_readable_rsp_thm_eq prsp_tm lthy
   2.267 +            val (readable_rsp_tm, _) = Logic.dest_implies (Thm.prop_of readable_rsp_thm_eq)
   2.268 +            val readable_rsp_tm_tnames = rename_to_tnames lthy readable_rsp_tm
   2.269 +        
   2.270 +            fun after_qed' [[thm]] lthy = 
   2.271 +              let
   2.272 +                val internal_rsp_thm = Goal.prove lthy [] [] prsp_tm 
   2.273 +                    (fn {context = ctxt, ...} =>
   2.274 +                      rtac readable_rsp_thm_eq 1 THEN Proof_Context.fact_tac ctxt [thm] 1)
   2.275 +              in
   2.276 +                after_qed internal_rsp_thm lthy
   2.277 +              end
   2.278 +          in
   2.279 +            (SOME readable_rsp_tm_tnames, after_qed')
   2.280 +          end 
   2.281    in
   2.282      Proof.theorem NONE (snd oo after_qed) [map (rpair []) (the_list goal)] lthy
   2.283    end
     3.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML	Mon Apr 13 15:27:34 2015 +0200
     3.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Sat May 02 13:58:06 2015 +0200
     3.3 @@ -777,7 +777,6 @@
     3.4      fun check_qty qty = if not (is_Type qty) 
     3.5            then error "The abstract type must be a type constructor."
     3.6            else ()
     3.7 -    val config = { notes = true }       
     3.8     
     3.9      fun setup_quotient () = 
    3.10        let
    3.11 @@ -786,7 +785,7 @@
    3.12          val opt_par_thm = Option.map (singleton (Attrib.eval_thms lthy)) opt_par_xthm
    3.13          val _ = check_qty (snd (quot_thm_rty_qty input_thm))
    3.14        in
    3.15 -        setup_by_quotient config input_thm opt_reflp_thm opt_par_thm lthy |> snd
    3.16 +        setup_by_quotient default_config input_thm opt_reflp_thm opt_par_thm lthy |> snd
    3.17        end
    3.18  
    3.19      fun setup_typedef () = 
    3.20 @@ -799,7 +798,7 @@
    3.21            | NONE => (
    3.22              case opt_par_xthm of
    3.23                SOME _ => error "The parametricity theorem cannot be specified if the type_definition theorem is used."
    3.24 -              | NONE => setup_by_typedef_thm config input_thm lthy |> snd
    3.25 +              | NONE => setup_by_typedef_thm default_config input_thm lthy |> snd
    3.26            )
    3.27        end
    3.28    in