UnusedQuotMain.thy
changeset 379 57bde65f6eb2
child 381 991db758a72d
equal deleted inserted replaced
378:86fba2c4eeef 379:57bde65f6eb2
       
     1 
       
     2 text {* tyRel takes a type and builds a relation that a quantifier over this
       
     3   type needs to respect. *}
       
     4 ML {*
       
     5 fun tyRel ty rty rel lthy =
       
     6   if Sign.typ_instance (ProofContext.theory_of lthy) (ty, rty)
       
     7   then rel
       
     8   else (case ty of
       
     9           Type (s, tys) =>
       
    10             let
       
    11               val tys_rel = map (fn ty => ty --> ty --> @{typ bool}) tys;
       
    12               val ty_out = ty --> ty --> @{typ bool};
       
    13               val tys_out = tys_rel ---> ty_out;
       
    14             in
       
    15             (case (maps_lookup (ProofContext.theory_of lthy) s) of
       
    16                SOME (info) => list_comb (Const (#relfun info, tys_out),
       
    17                               map (fn ty => tyRel ty rty rel lthy) tys)
       
    18              | NONE  => HOLogic.eq_const ty
       
    19             )
       
    20             end
       
    21         | _ => HOLogic.eq_const ty)
       
    22 *}
       
    23 
       
    24 (* 
       
    25 ML {* cterm_of @{theory} 
       
    26   (tyRel @{typ "'a \<Rightarrow> 'a list \<Rightarrow> 't \<Rightarrow> 't"} (Logic.varifyT @{typ "'a list"}) 
       
    27          @{term "f::('a list \<Rightarrow> 'a list \<Rightarrow> bool)"} @{context}) 
       
    28 *} 
       
    29 *)
       
    30 
       
    31 
       
    32 ML {*
       
    33 fun mk_babs ty ty' = Const (@{const_name "Babs"}, [ty' --> @{typ bool}, ty] ---> ty)
       
    34 fun mk_ball ty = Const (@{const_name "Ball"}, [ty, ty] ---> @{typ bool})
       
    35 fun mk_bex ty = Const (@{const_name "Bex"}, [ty, ty] ---> @{typ bool})
       
    36 fun mk_resp ty = Const (@{const_name Respects}, [[ty, ty] ---> @{typ bool}, ty] ---> @{typ bool})
       
    37 *}
       
    38 
       
    39 (* applies f to the subterm of an abstractions, otherwise to the given term *)
       
    40 ML {*
       
    41 fun apply_subt f trm =
       
    42   case trm of
       
    43     Abs (x, T, t) => 
       
    44        let 
       
    45          val (x', t') = Term.dest_abs (x, T, t)
       
    46        in
       
    47          Term.absfree (x', T, f t') 
       
    48        end
       
    49   | _ => f trm
       
    50 *}
       
    51 
       
    52 
       
    53 
       
    54 (* FIXME: if there are more than one quotient, then you have to look up the relation *)
       
    55 ML {*
       
    56 fun my_reg lthy rel rty trm =
       
    57   case trm of
       
    58     Abs (x, T, t) =>
       
    59        if (needs_lift rty T) then
       
    60          let
       
    61             val rrel = tyRel T rty rel lthy
       
    62          in
       
    63            (mk_babs (fastype_of trm) T) $ (mk_resp T $ rrel) $ (apply_subt (my_reg lthy rel rty) trm)
       
    64          end
       
    65        else
       
    66          Abs(x, T, (apply_subt (my_reg lthy rel rty) t))
       
    67   | Const (@{const_name "All"}, ty) $ (t as Abs (x, T, _)) =>
       
    68        let
       
    69           val ty1 = domain_type ty
       
    70           val ty2 = domain_type ty1
       
    71           val rrel = tyRel T rty rel lthy
       
    72        in
       
    73          if (needs_lift rty T) then
       
    74            (mk_ball ty1) $ (mk_resp ty2 $ rrel) $ (apply_subt (my_reg lthy rel rty) t)
       
    75          else
       
    76            Const (@{const_name "All"}, ty) $ apply_subt (my_reg lthy rel rty) t
       
    77        end
       
    78   | Const (@{const_name "Ex"}, ty) $ (t as Abs (x, T, _)) =>
       
    79        let
       
    80           val ty1 = domain_type ty
       
    81           val ty2 = domain_type ty1
       
    82           val rrel = tyRel T rty rel lthy
       
    83        in
       
    84          if (needs_lift rty T) then
       
    85            (mk_bex ty1) $ (mk_resp ty2 $ rrel) $ (apply_subt (my_reg lthy rel rty) t)
       
    86          else
       
    87            Const (@{const_name "Ex"}, ty) $ apply_subt (my_reg lthy rel rty) t
       
    88        end
       
    89   | Const (@{const_name "op ="}, ty) $ t =>
       
    90       if needs_lift rty (fastype_of t) then
       
    91         (tyRel (fastype_of t) rty rel lthy) $ t   (* FIXME: t should be regularised too *)
       
    92       else Const (@{const_name "op ="}, ty) $ (my_reg lthy rel rty t)
       
    93   | t1 $ t2 => (my_reg lthy rel rty t1) $ (my_reg lthy rel rty t2)
       
    94   | _ => trm
       
    95 *}
       
    96 
       
    97 (* For polymorphic types we need to find the type of the Relation term. *)
       
    98 (* TODO: we assume that the relation is a Constant. Is this always true? *)
       
    99 ML {*
       
   100 fun my_reg_inst lthy rel rty trm =
       
   101   case rel of
       
   102     Const (n, _) => Syntax.check_term lthy
       
   103       (my_reg lthy (Const (n, dummyT)) (Logic.varifyT rty) trm)
       
   104 *}
       
   105 
       
   106 (*
       
   107 ML {*
       
   108   val r = Free ("R", dummyT);
       
   109   val t = (my_reg_inst @{context} r @{typ "'a list"} @{term "\<forall>(x::'b list). P x"});
       
   110   val t2 = Syntax.check_term @{context} t;
       
   111   cterm_of @{theory} t2
       
   112 *}
       
   113 *)
       
   114 
       
   115 text {* Assumes that the given theorem is atomized *}
       
   116 ML {*
       
   117   fun build_regularize_goal thm rty rel lthy =
       
   118      Logic.mk_implies
       
   119        ((prop_of thm),
       
   120        (my_reg_inst lthy rel rty (prop_of thm)))
       
   121 *}
       
   122 
       
   123 ML {*
       
   124 fun regularize thm rty rel rel_eqv rel_refl lthy =
       
   125   let
       
   126     val goal = build_regularize_goal thm rty rel lthy;
       
   127     fun tac ctxt =
       
   128       (ObjectLogic.full_atomize_tac) THEN'
       
   129       REPEAT_ALL_NEW (FIRST' [
       
   130         rtac rel_refl,
       
   131         atac,
       
   132         rtac @{thm universal_twice},
       
   133         (rtac @{thm impI} THEN' atac),
       
   134         rtac @{thm implication_twice},
       
   135         EqSubst.eqsubst_tac ctxt [0]
       
   136           [(@{thm equiv_res_forall} OF [rel_eqv]),
       
   137            (@{thm equiv_res_exists} OF [rel_eqv])],
       
   138         (* For a = b \<longrightarrow> a \<approx> b *)
       
   139         (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl),
       
   140         (rtac @{thm RIGHT_RES_FORALL_REGULAR})
       
   141       ]);
       
   142     val cthm = Goal.prove lthy [] [] goal
       
   143       (fn {context, ...} => tac context 1);
       
   144   in
       
   145     cthm OF [thm]
       
   146   end
       
   147 *}
       
   148 
       
   149 (*consts Rl :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
       
   150 axioms Rl_eq: "EQUIV Rl"
       
   151 
       
   152 quotient ql = "'a list" / "Rl"
       
   153   by (rule Rl_eq)
       
   154 ML {*
       
   155   ctyp_of @{theory} (exchange_ty @{context} (Logic.varifyT @{typ "'a list"}) (Logic.varifyT @{typ "'a ql"}) @{typ "nat list \<Rightarrow> (nat \<times> nat) list"});
       
   156   ctyp_of @{theory} (exchange_ty @{context} (Logic.varifyT @{typ "nat \<times> nat"}) (Logic.varifyT @{typ "int"}) @{typ "nat list \<Rightarrow> (nat \<times> nat) list"})
       
   157 *}
       
   158 *)
       
   159 
       
   160 ML {*
       
   161 (* returns all subterms where two types differ *)
       
   162 fun diff (T, S) Ds =
       
   163   case (T, S) of
       
   164     (TVar v, TVar u) => if v = u then Ds else (T, S)::Ds 
       
   165   | (TFree x, TFree y) => if x = y then Ds else (T, S)::Ds
       
   166   | (Type (a, Ts), Type (b, Us)) => 
       
   167       if a = b then diffs (Ts, Us) Ds else (T, S)::Ds
       
   168   | _ => (T, S)::Ds
       
   169 and diffs (T::Ts, U::Us) Ds = diffs (Ts, Us) (diff (T, U) Ds)
       
   170   | diffs ([], []) Ds = Ds
       
   171   | diffs _ _ = error "Unequal length of type arguments"
       
   172 
       
   173 *}
       
   174 
       
   175 ML {*
       
   176 fun build_repabs_term lthy thm consts rty qty =
       
   177   let
       
   178     (* TODO: The rty and qty stored in the quotient_info should
       
   179        be varified, so this will soon not be needed *)
       
   180     val rty = Logic.varifyT rty;
       
   181     val qty = Logic.varifyT qty;
       
   182 
       
   183   fun mk_abs tm =
       
   184     let
       
   185       val ty = fastype_of tm
       
   186     in Syntax.check_term lthy ((get_fun_OLD absF (rty, qty) lthy ty) $ tm) end
       
   187   fun mk_repabs tm =
       
   188     let
       
   189       val ty = fastype_of tm
       
   190     in Syntax.check_term lthy ((get_fun_OLD repF (rty, qty) lthy ty) $ (mk_abs tm)) end
       
   191 
       
   192     fun is_lifted_const (Const (x, _)) = member (op =) consts x
       
   193       | is_lifted_const _ = false;
       
   194 
       
   195     fun build_aux lthy tm =
       
   196       case tm of
       
   197         Abs (a as (_, vty, _)) =>
       
   198           let
       
   199             val (vs, t) = Term.dest_abs a;
       
   200             val v = Free(vs, vty);
       
   201             val t' = lambda v (build_aux lthy t)
       
   202           in
       
   203             if (not (needs_lift rty (fastype_of tm))) then t'
       
   204             else mk_repabs (
       
   205               if not (needs_lift rty vty) then t'
       
   206               else
       
   207                 let
       
   208                   val v' = mk_repabs v;
       
   209                   (* TODO: I believe 'beta' is not needed any more *)
       
   210                   val t1 = (* Envir.beta_norm *) (t' $ v')
       
   211                 in
       
   212                   lambda v t1
       
   213                 end)
       
   214           end
       
   215       | x =>
       
   216         case Term.strip_comb tm of
       
   217           (Const(@{const_name Respects}, _), _) => tm
       
   218         | (opp, tms0) =>
       
   219           let
       
   220             val tms = map (build_aux lthy) tms0
       
   221             val ty = fastype_of tm
       
   222           in
       
   223             if (is_lifted_const opp andalso needs_lift rty ty) then
       
   224             mk_repabs (list_comb (opp, tms))
       
   225             else if ((Term.is_Free opp) andalso (length tms > 0) andalso (needs_lift rty ty)) then
       
   226               mk_repabs (list_comb (opp, tms))
       
   227             else if tms = [] then opp
       
   228             else list_comb(opp, tms)
       
   229           end
       
   230   in
       
   231     repeat_eqsubst_prop lthy @{thms id_def_sym}
       
   232       (build_aux lthy (Thm.prop_of thm))
       
   233   end
       
   234 *}
       
   235 
       
   236 text {* Builds provable goals for regularized theorems *}
       
   237 ML {*
       
   238 fun build_repabs_goal ctxt thm cons rty qty =
       
   239   Logic.mk_equals ((Thm.prop_of thm), (build_repabs_term ctxt thm cons rty qty))
       
   240 *}
       
   241 
       
   242 ML {*
       
   243 fun repabs lthy thm consts rty qty quot_thm reflex_thm trans_thm rsp_thms =
       
   244   let
       
   245     val rt = build_repabs_term lthy thm consts rty qty;
       
   246     val rg = Logic.mk_equals ((Thm.prop_of thm), rt);
       
   247     fun tac ctxt = (ObjectLogic.full_atomize_tac) THEN'
       
   248       (REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms));
       
   249     val cthm = Goal.prove lthy [] [] rg (fn x => tac (#context x) 1);
       
   250   in
       
   251     @{thm Pure.equal_elim_rule1} OF [cthm, thm]
       
   252   end
       
   253 *}
       
   254 
       
   255 
       
   256 (* TODO: Check if it behaves properly with varifyed rty *)
       
   257 ML {*
       
   258 fun findabs_all rty tm =
       
   259   case tm of
       
   260     Abs(_, T, b) =>
       
   261       let
       
   262         val b' = subst_bound ((Free ("x", T)), b);
       
   263         val tys = findabs_all rty b'
       
   264         val ty = fastype_of tm
       
   265       in if needs_lift rty ty then (ty :: tys) else tys
       
   266       end
       
   267   | f $ a => (findabs_all rty f) @ (findabs_all rty a)
       
   268   | _ => [];
       
   269 fun findabs rty tm = distinct (op =) (findabs_all rty tm)
       
   270 *}
       
   271 
       
   272 
       
   273 (* Currently useful only for LAMBDA_PRS *)
       
   274 ML {*
       
   275 fun make_simp_prs_thm lthy quot_thm thm typ =
       
   276   let
       
   277     val (_, [lty, rty]) = dest_Type typ;
       
   278     val thy = ProofContext.theory_of lthy;
       
   279     val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty)
       
   280     val inst = [SOME lcty, NONE, SOME rcty];
       
   281     val lpi = Drule.instantiate' inst [] thm;
       
   282     val tac =
       
   283       (compose_tac (false, lpi, 2)) THEN_ALL_NEW
       
   284       (quotient_tac quot_thm);
       
   285     val gc = Drule.strip_imp_concl (cprop_of lpi);
       
   286     val t = Goal.prove_internal [] gc (fn _ => tac 1)
       
   287   in
       
   288     MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] t
       
   289   end
       
   290 *}
       
   291 
       
   292 ML {*
       
   293 fun findallex_all rty qty tm =
       
   294   case tm of
       
   295     Const (@{const_name All}, T) $ (s as (Abs(_, _, b))) =>
       
   296       let
       
   297         val (tya, tye) = findallex_all rty qty s
       
   298       in if needs_lift rty T then
       
   299         ((T :: tya), tye)
       
   300       else (tya, tye) end
       
   301   | Const (@{const_name Ex}, T) $ (s as (Abs(_, _, b))) =>
       
   302       let
       
   303         val (tya, tye) = findallex_all rty qty s
       
   304       in if needs_lift rty T then
       
   305         (tya, (T :: tye))
       
   306       else (tya, tye) end
       
   307   | Abs(_, T, b) =>
       
   308       findallex_all rty qty (subst_bound ((Free ("x", T)), b))
       
   309   | f $ a =>
       
   310       let
       
   311         val (a1, e1) = findallex_all rty qty f;
       
   312         val (a2, e2) = findallex_all rty qty a;
       
   313       in (a1 @ a2, e1 @ e2) end
       
   314   | _ => ([], []);
       
   315 *}
       
   316 
       
   317 ML {*
       
   318 fun findallex lthy rty qty tm =
       
   319   let
       
   320     val (a, e) = findallex_all rty qty tm;
       
   321     val (ad, ed) = (map domain_type a, map domain_type e);
       
   322     val (au, eu) = (distinct (op =) ad, distinct (op =) ed);
       
   323     val (rty, qty) = (Logic.varifyT rty, Logic.varifyT qty)
       
   324   in
       
   325     (map (exchange_ty lthy rty qty) au, map (exchange_ty lthy rty qty) eu)
       
   326   end
       
   327 *}
       
   328 
       
   329 ML {*
       
   330 fun make_allex_prs_thm lthy quot_thm thm typ =
       
   331   let
       
   332     val (_, [lty, rty]) = dest_Type typ;
       
   333     val thy = ProofContext.theory_of lthy;
       
   334     val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty)
       
   335     val inst = [NONE, SOME lcty];
       
   336     val lpi = Drule.instantiate' inst [] thm;
       
   337     val tac =
       
   338       (compose_tac (false, lpi, 1)) THEN_ALL_NEW
       
   339       (quotient_tac quot_thm);
       
   340     val gc = Drule.strip_imp_concl (cprop_of lpi);
       
   341     val t = Goal.prove_internal [] gc (fn _ => tac 1)
       
   342     val t_noid = MetaSimplifier.rewrite_rule
       
   343       [@{thm eq_reflection} OF @{thms id_apply}] t;
       
   344     val t_sym = @{thm "HOL.sym"} OF [t_noid];
       
   345     val t_eq = @{thm "eq_reflection"} OF [t_sym]
       
   346   in
       
   347     t_eq
       
   348   end
       
   349 *}
       
   350 
       
   351 ML {*
       
   352 fun lift_thm lthy qty qty_name rsp_thms defs rthm = 
       
   353 let
       
   354   val _ = tracing ("raw theorem:\n" ^ Syntax.string_of_term lthy (prop_of rthm))
       
   355 
       
   356   val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data lthy qty;
       
   357   val (trans2, reps_same, absrep, quot) = lookup_quot_thms lthy qty_name;
       
   358   val consts = lookup_quot_consts defs;
       
   359   val t_a = atomize_thm rthm;
       
   360 
       
   361   val _ = tracing ("raw atomized theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_a))
       
   362 
       
   363   val t_r = regularize t_a rty rel rel_eqv rel_refl lthy;
       
   364 
       
   365   val _ = tracing ("regularised theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_r))
       
   366 
       
   367   val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms;
       
   368 
       
   369   val _ = tracing ("rep/abs injected theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_t))
       
   370 
       
   371   val (alls, exs) = findallex lthy rty qty (prop_of t_a);
       
   372   val allthms = map (make_allex_prs_thm lthy quot @{thm FORALL_PRS}) alls
       
   373   val exthms = map (make_allex_prs_thm lthy quot @{thm EXISTS_PRS}) exs
       
   374   val t_a = MetaSimplifier.rewrite_rule (allthms @ exthms) t_t
       
   375 
       
   376   val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_a))
       
   377 
       
   378   val abs = findabs rty (prop_of t_a);
       
   379   val aps = findaps rty (prop_of t_a);
       
   380   val app_prs_thms = map (applic_prs lthy rty qty absrep) aps;
       
   381   val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs;
       
   382   val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_a;
       
   383   
       
   384   val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_l))
       
   385 
       
   386   val defs_sym = flat (map (add_lower_defs lthy) defs);
       
   387   val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym;
       
   388   val t_id = simp_ids lthy t_l;
       
   389 
       
   390   val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_id))
       
   391 
       
   392   val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_id;
       
   393 
       
   394   val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_d0))
       
   395 
       
   396   val t_d = repeat_eqsubst_thm lthy defs_sym t_d0;
       
   397 
       
   398   val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_d))
       
   399 
       
   400   val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d;
       
   401 
       
   402   val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_r))
       
   403 
       
   404   val t_rv = ObjectLogic.rulify t_r
       
   405 
       
   406   val _ = tracing ("lifted theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_rv))
       
   407 in
       
   408   Thm.varifyT t_rv
       
   409 end
       
   410 *}
       
   411 
       
   412 ML {*
       
   413 fun lift_thm_note qty qty_name rsp_thms defs thm name lthy =
       
   414   let
       
   415     val lifted_thm = lift_thm lthy qty qty_name rsp_thms defs thm;
       
   416     val (_, lthy2) = note (name, lifted_thm) lthy;
       
   417   in
       
   418     lthy2
       
   419   end
       
   420 *}
       
   421 
       
   422 
       
   423 ML {*
       
   424 fun regularize_goal lthy thm rel_eqv rel_refl qtrm =
       
   425   let
       
   426     val reg_trm = mk_REGULARIZE_goal lthy (prop_of thm) qtrm;
       
   427     fun tac lthy = regularize_tac lthy rel_eqv rel_refl;
       
   428     val cthm = Goal.prove lthy [] [] reg_trm
       
   429       (fn {context, ...} => tac context 1);
       
   430   in
       
   431     cthm OF [thm]
       
   432   end
       
   433 *}
       
   434 
       
   435 ML {*
       
   436 fun repabs_goal lthy thm rty quot_thm reflex_thm trans_thm rsp_thms qtrm =
       
   437   let
       
   438     val rg = Syntax.check_term lthy (mk_inj_REPABS_goal lthy ((prop_of thm), qtrm));
       
   439     fun tac ctxt = (ObjectLogic.full_atomize_tac) THEN'
       
   440       (REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms));
       
   441     val cthm = Goal.prove lthy [] [] rg (fn x => tac (#context x) 1);
       
   442   in
       
   443     @{thm Pure.equal_elim_rule1} OF [cthm, thm]
       
   444   end
       
   445 *}
       
   446 
       
   447 ML {*
       
   448 fun lift_thm_goal lthy qty qty_name rsp_thms defs rthm goal =
       
   449 let
       
   450   val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data lthy qty;
       
   451   val (trans2, reps_same, absrep, quot) = lookup_quot_thms lthy qty_name;
       
   452   val t_a = atomize_thm rthm;
       
   453   val goal_a = atomize_goal (ProofContext.theory_of lthy) goal;
       
   454   val t_r = regularize_goal lthy t_a rel_eqv rel_refl goal_a;
       
   455   val t_t = repabs_goal lthy t_r rty quot rel_refl trans2 rsp_thms goal_a;
       
   456   val (alls, exs) = findallex lthy rty qty (prop_of t_a);
       
   457   val allthms = map (make_allex_prs_thm lthy quot @{thm FORALL_PRS}) alls
       
   458   val exthms = map (make_allex_prs_thm lthy quot @{thm EXISTS_PRS}) exs
       
   459   val t_a = MetaSimplifier.rewrite_rule (allthms @ exthms) t_t
       
   460   val abs = findabs rty (prop_of t_a);
       
   461   val aps = findaps rty (prop_of t_a);
       
   462   val app_prs_thms = map (applic_prs lthy rty qty absrep) aps;
       
   463   val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs;
       
   464   val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_a;
       
   465   val defs_sym = flat (map (add_lower_defs lthy) defs);
       
   466   val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym;
       
   467   val t_id = simp_ids lthy t_l;
       
   468   val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_id;
       
   469   val t_d = repeat_eqsubst_thm lthy defs_sym t_d0;
       
   470   val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d;
       
   471   val t_rv = ObjectLogic.rulify t_r
       
   472 in
       
   473   Thm.varifyT t_rv
       
   474 end
       
   475 *}
       
   476 
       
   477 ML {*
       
   478 fun lift_thm_goal_note lthy qty qty_name rsp_thms defs thm name goal =
       
   479   let
       
   480     val lifted_thm = lift_thm_goal lthy qty qty_name rsp_thms defs thm goal;
       
   481     val (_, lthy2) = note (name, lifted_thm) lthy;
       
   482   in
       
   483     lthy2
       
   484   end
       
   485 *}
       
   486