# HG changeset patch # User Cezary Kaliszyk # Date 1257776613 -3600 # Node ID 40bb0c4718a69a6b739e63134f02f654324d35cf # Parent c6a9b4e4d548d89eb359c8d87314295e0964eafd Cleaning and commenting diff -r c6a9b4e4d548 -r 40bb0c4718a6 LFex.thy --- a/LFex.thy Mon Nov 09 13:47:46 2009 +0100 +++ b/LFex.thy Mon Nov 09 15:23:33 2009 +0100 @@ -180,6 +180,37 @@ where "perm_trm \ (perm::'x prm \ trm \ trm)" + + + + + + + + + +ML {* val defs = + @{thms TYP_def KPI_def TCONST_def TAPP_def TPI_def VAR_def CONS_def APP_def LAM_def + FV_kind_def FV_ty_def FV_trm_def perm_kind_def perm_ty_def perm_trm_def} +*} +ML {* val consts = lookup_quot_consts defs *} + +thm akind_aty_atrm.induct + +ML {* +val rty_qty_rel = + [(@{typ kind}, (@{typ KIND}, @{term akind})), + (@{typ ty}, (@{typ TY}, @{term aty})), + (@{typ trm}, (@{typ TRM}, @{term atrm}))] +*} + +print_quotients + +ML {* val rty = [@{typ }] +ML {* val defs_sym = flat (map (add_lower_defs @{context}) defs) *} +ML {* val t_a = atomize_thm @{thm akind_aty_atrm.induct} *} +prove {* build_regularize_goal t_a rty rel @{context} + end diff -r c6a9b4e4d548 -r 40bb0c4718a6 QuotMain.thy --- a/QuotMain.thy Mon Nov 09 13:47:46 2009 +0100 +++ b/QuotMain.thy Mon Nov 09 15:23:33 2009 +0100 @@ -160,16 +160,6 @@ (* lifting of constants *) use "quotient_def.ML" - -text {* FIXME: auxiliary function *} -ML {* -val no_vars = Thm.rule_attribute (fn context => fn th => - let - val ctxt = Variable.set_body false (Context.proof_of context); - val ((_, [th']), _) = Variable.import true [th] ctxt; - in th' end); -*} - section {* ATOMIZE *} lemma atomize_eqv[atomize]: @@ -340,6 +330,8 @@ | _ => trm *} +(* For polymorphic types we need to find the type of the Relation term. *) +(* TODO: we assume that the relation is a Constant. Is this always true? *) ML {* fun my_reg_inst lthy rel rty trm = case rel of @@ -349,7 +341,7 @@ (* ML {* - text {*val r = term_of @{cpat "R::?'a list \ ?'a list \bool"};*} + text {*val r = term_of @{cpat "R::?'a list \ ?'a list \ bool"};*} val r = Free ("R", dummyT); val t = (my_reg @{context} r @{typ "'a list"} @{term "\(x::'b list). P x"}); val t2 = Syntax.check_term @{context} t; @@ -372,7 +364,8 @@ "(c \ a) \ (a \ b \ d) \ (a \ b) \ (c \ d)" by auto -(*lemma equality_twice: "a = c \ b = d \ (a = b \ c = d)" +(*lemma equality_twice: + "a = c \ b = d \ (a = b \ c = d)" by auto*) ML {* @@ -381,27 +374,72 @@ val goal = build_regularize_goal thm rty rel lthy; fun tac ctxt = (ObjectLogic.full_atomize_tac) THEN' - REPEAT_ALL_NEW (FIRST' [ - rtac rel_refl, - atac, - rtac @{thm universal_twice}, - (rtac @{thm impI} THEN' atac), - rtac @{thm implication_twice}, - (*rtac @{thm equality_twice},*) - EqSubst.eqsubst_tac ctxt [0] - [(@{thm equiv_res_forall} OF [rel_eqv]), - (@{thm equiv_res_exists} OF [rel_eqv])], - (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl), - (rtac @{thm RIGHT_RES_FORALL_REGULAR}) - ]); - val cthm = Goal.prove lthy [] [] goal - (fn {context,...} => tac context 1); + REPEAT_ALL_NEW (FIRST' [ + rtac rel_refl, + atac, + rtac @{thm universal_twice}, + (rtac @{thm impI} THEN' atac), + rtac @{thm implication_twice}, + EqSubst.eqsubst_tac ctxt [0] + [(@{thm equiv_res_forall} OF [rel_eqv]), + (@{thm equiv_res_exists} OF [rel_eqv])], + (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl), + (rtac @{thm RIGHT_RES_FORALL_REGULAR}) + ]); + val cthm = Goal.prove lthy [] [] goal + (fn {context, ...} => tac context 1); in cthm OF [thm] end *} section {* RepAbs injection *} +(* + +Injecting RepAbs means: + + For abstractions: + * If the type of the abstraction doesn't need lifting we recurse. + * If it does we add RepAbs around the whole term and check if the + variable needs lifting. + * If it doesn't then we recurse + * If it does we recurse and put 'RepAbs' around all occurences + of the variable in the obtained subterm. + For applications: + * If the term is 'Respects' applied to anything we leave it unchanged + * If the term needs lifting and the head is a constant that we know + how to lift, we put a RepAbs and recurse + * If the term needs lifting and the head is a free applied to subterms + (if it is not applied we treated it in Abs branch) then we + put RepAbs and recurse + * Otherwise just recurse. + +The injection is done in the following phases: + 1) build_repabs_term inserts rep-abs pairs in the term + 2) we prove the equality between the original theorem and this one + 3) we use Pure.equal_elim_rule1 to get the new theorem. + +To prove that the old theorem implies the new one, we first +atomize it and then try: + + 1) theorems 'trans2' from the QUOT_TYPE + 2) remove lambdas from both sides (LAMBDA_RES_TAC) + 3) remove Ball/Bex + 4) use RSP theorems + 5) remove rep_abs from right side + 6) reflexivity + 7) split applications of lifted type (apply_rsp) + 8) split applications of non-lifted type (cong_tac) + 9) apply extentionality +10) relation reflexive +11) assumption +12) proving obvious higher order equalities by simplifying fun_rel + (not sure if still needed?) +13) unfolding lambda on one side +14) simplifying (= ===> =) for simpler respectfullness + +*) + (* Needed to have a meta-equality *) lemma id_def_sym: "(\x. x) \ id" @@ -489,9 +527,10 @@ then (get_const flag (ty, (exchange_ty lthy rty qty ty))) else (case ty of TFree _ => (mk_identity ty, (ty, ty)) - | Type (_, []) => (mk_identity ty, (ty, ty)) - | Type ("fun" , [ty1, ty2]) => - get_fun_fun [get_fun_noexchange (negF flag) (rty,qty) lthy ty1, get_fun_noexchange flag (rty,qty) lthy ty2] + | Type (_, []) => (mk_identity ty, (ty, ty)) + | Type ("fun" , [ty1, ty2]) => + get_fun_fun [get_fun_noexchange (negF flag) (rty, qty) lthy ty1, + get_fun_noexchange flag (rty, qty) lthy ty2] | Type (s, tys) => get_fun_aux s (map (get_fun_noexchange flag (rty, qty) lthy) tys) | _ => raise ERROR ("no type variables")) end @@ -582,7 +621,7 @@ val cgoal = cterm_of (ProofContext.theory_of ctxt) (Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a')) val rt = Toplevel.program (fn () => Goal.prove_internal [] cgoal (fn _ => tac)); in - @{thm Pure.equal_elim_rule1} OF [rt,thm] + @{thm Pure.equal_elim_rule1} OF [rt, thm] end *} @@ -593,7 +632,7 @@ *} ML {* -fun build_repabs_term lthy thm constructors rty qty = +fun build_repabs_term lthy thm consts rty qty = let val rty = Logic.varifyT rty; val qty = Logic.varifyT qty; @@ -607,44 +646,44 @@ val ty = fastype_of tm in Syntax.check_term lthy ((get_fun_new repF (rty, qty) lthy ty) $ (mk_abs tm)) end - fun is_constructor (Const (x, _)) = member (op =) constructors x - | is_constructor _ = false; + fun is_lifted_const (Const (x, _)) = member (op =) consts x + | is_lifted_const _ = false; fun build_aux lthy tm = case tm of - Abs (a as (_, vty, _)) => - let - val (vs, t) = Term.dest_abs a; - val v = Free(vs, vty); - val t' = lambda v (build_aux lthy t) - in - if (not (needs_lift rty (fastype_of tm))) then t' - else mk_repabs ( - if not (needs_lift rty vty) then t' - else + Abs (a as (_, vty, _)) => let - val v' = mk_repabs v; - val t1 = Envir.beta_norm (t' $ v') + val (vs, t) = Term.dest_abs a; + val v = Free(vs, vty); + val t' = lambda v (build_aux lthy t) in - lambda v t1 + if (not (needs_lift rty (fastype_of tm))) then t' + else mk_repabs ( + if not (needs_lift rty vty) then t' + else + let + val v' = mk_repabs v; + (* TODO: I believe this is not needed any more *) + val t1 = Envir.beta_norm (t' $ v') + in + lambda v t1 + end) end - ) - end - | x => - let - val (opp, tms0) = Term.strip_comb tm - val tms = map (build_aux lthy) tms0 - val ty = fastype_of tm - in - if (((fst (Term.dest_Const opp)) = @{const_name Respects}) handle _ => false) - then (list_comb (opp, (hd tms0) :: (tl tms))) - else if (is_constructor opp andalso needs_lift rty ty) then - mk_repabs (list_comb (opp,tms)) - else if ((Term.is_Free opp) andalso (length tms > 0) andalso (needs_lift rty ty)) then - mk_repabs(list_comb(opp,tms)) - else if tms = [] then opp - else list_comb(opp, tms) - end + | x => + case Term.strip_comb tm of + (Const(@{const_name Respects}, _), _) => tm + | (opp, tms0) => + let + val tms = map (build_aux lthy) tms0 + val ty = fastype_of tm + in + if (is_lifted_const opp andalso needs_lift rty ty) then + mk_repabs (list_comb (opp, tms)) + else if ((Term.is_Free opp) andalso (length tms > 0) andalso (needs_lift rty ty)) then + mk_repabs (list_comb (opp, tms)) + else if tms = [] then opp + else list_comb(opp, tms) + end in repeat_eqsubst_prop lthy @{thms id_def_sym} (build_aux lthy (Thm.prop_of thm)) @@ -675,14 +714,17 @@ rtac @{thm FUN_QUOTIENT}, rtac quot_thm, rtac @{thm IDENTITY_QUOTIENT}, - (fn i => CHANGED (simp_tac (HOL_ss addsimps @{thms FUN_MAP_I}) i) THEN rtac @{thm IDENTITY_QUOTIENT} i) + ( + fn i => CHANGED (simp_tac (HOL_ss addsimps @{thms FUN_MAP_I}) i) THEN + rtac @{thm IDENTITY_QUOTIENT} i + ) ]) *} ML {* fun LAMBDA_RES_TAC ctxt i st = (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of - (_ $ (_ $ (Abs(_,_,_))$(Abs(_,_,_)))) => + (_ $ (_ $ (Abs(_, _, _))$(Abs(_, _, _)))) => (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI}) | _ => fn _ => no_tac) i st @@ -691,10 +733,10 @@ ML {* fun WEAK_LAMBDA_RES_TAC ctxt i st = (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of - (_ $ (_ $ _$(Abs(_,_,_)))) => + (_ $ (_ $ _ $ (Abs(_, _, _)))) => (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI}) - | (_ $ (_ $ (Abs(_,_,_))$_)) => + | (_ $ (_ $ (Abs(_, _, _)) $ _)) => (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI}) | _ => fn _ => no_tac) i st @@ -715,9 +757,10 @@ *} ML {* -val res_forall_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} => +val ball_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} => let - val _ $ (_ $ (Const (@{const_name Ball}, _) $ _) $ (Const (@{const_name Ball}, _) $ _)) = term_of concl + val _ $ (_ $ (Const (@{const_name Ball}, _) $ _) $ + (Const (@{const_name Ball}, _) $ _)) = term_of concl in ((simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} @@ -729,9 +772,10 @@ *} ML {* -val res_exists_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} => +val bex_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} => let - val _ $ (_ $ (Const (@{const_name Bex}, _) $ _) $ (Const (@{const_name Bex}, _) $ _)) = term_of concl + val _ $ (_ $ (Const (@{const_name Bex}, _) $ _) $ + (Const (@{const_name Bex}, _) $ _)) = term_of concl in ((simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} @@ -745,13 +789,10 @@ ML {* fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms = (FIRST' [ -(* rtac @{thm FUN_QUOTIENT}, - rtac quot_thm, - rtac @{thm IDENTITY_QUOTIENT},*) rtac trans_thm, LAMBDA_RES_TAC ctxt, - res_forall_rsp_tac ctxt, - res_exists_rsp_tac ctxt, + ball_rsp_tac ctxt, + bex_rsp_tac ctxt, FIRST' (map rtac rsp_thms), (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])), rtac refl, @@ -771,9 +812,9 @@ *} ML {* -fun repabs lthy thm constructors rty qty quot_thm reflex_thm trans_thm rsp_thms = +fun repabs lthy thm consts rty qty quot_thm reflex_thm trans_thm rsp_thms = let - val rt = build_repabs_term lthy thm constructors rty qty; + val rt = build_repabs_term lthy thm consts rty qty; val rg = Logic.mk_equals ((Thm.prop_of thm), rt); fun tac ctxt = (ObjectLogic.full_atomize_tac) THEN' (REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms)); @@ -802,15 +843,15 @@ text {* expects atomized definition *} ML {* - fun add_lower_defs_aux lthy thm = - let - val e1 = @{thm fun_cong} OF [thm]; - val f = eqsubst_thm lthy @{thms fun_map.simps} e1; - val g = simp_ids lthy f - in - (simp_ids lthy thm) :: (add_lower_defs_aux lthy g) - end - handle _ => [simp_ids lthy thm] +fun add_lower_defs_aux lthy thm = + let + val e1 = @{thm fun_cong} OF [thm]; + val f = eqsubst_thm lthy @{thms fun_map.simps} e1; + val g = simp_ids lthy f + in + (simp_ids lthy thm) :: (add_lower_defs_aux lthy g) + end + handle _ => [simp_ids lthy thm] *} ML {* @@ -825,30 +866,31 @@ *} ML {* - fun findabs_all rty tm = - case tm of - Abs(_, T, b) => - let - val b' = subst_bound ((Free ("x", T)), b); - val tys = findabs_all rty b' - val ty = fastype_of tm - in if needs_lift rty ty then (ty :: tys) else tys - end - | f $ a => (findabs_all rty f) @ (findabs_all rty a) - | _ => []; - fun findabs rty tm = distinct (op =) (findabs_all rty tm) +fun findabs_all rty tm = + case tm of + Abs(_, T, b) => + let + val b' = subst_bound ((Free ("x", T)), b); + val tys = findabs_all rty b' + val ty = fastype_of tm + in if needs_lift rty ty then (ty :: tys) else tys + end + | f $ a => (findabs_all rty f) @ (findabs_all rty a) + | _ => []; +fun findabs rty tm = distinct (op =) (findabs_all rty tm) *} ML {* - fun findaps_all rty tm = - case tm of - Abs(_, T, b) => - findaps_all rty (subst_bound ((Free ("x", T)), b)) - | (f $ a) => (findaps_all rty f @ findaps_all rty a) - | Free (_, (T as (Type ("fun", (_ :: _))))) => (if needs_lift rty T then [T] else []) - | _ => []; - fun findaps rty tm = distinct (op =) (findaps_all rty tm) +fun findaps_all rty tm = + case tm of + Abs(_, T, b) => + findaps_all rty (subst_bound ((Free ("x", T)), b)) + | (f $ a) => (findaps_all rty f @ findaps_all rty a) + | Free (_, (T as (Type ("fun", (_ :: _))))) => + (if needs_lift rty T then [T] else []) + | _ => []; +fun findaps rty tm = distinct (op =) (findaps_all rty tm) *} ML {* @@ -870,39 +912,39 @@ *} ML {* - fun findallex_all rty qty tm = - case tm of - Const (@{const_name All}, T) $ (s as (Abs(_, _, b))) => - let - val (tya, tye) = findallex_all rty qty s - in if needs_lift rty T then - ((T :: tya), tye) - else (tya, tye) end - | Const (@{const_name Ex}, T) $ (s as (Abs(_, _, b))) => - let - val (tya, tye) = findallex_all rty qty s - in if needs_lift rty T then - (tya, (T :: tye)) - else (tya, tye) end - | Abs(_, T, b) => - findallex_all rty qty (subst_bound ((Free ("x", T)), b)) - | f $ a => - let - val (a1, e1) = findallex_all rty qty f; - val (a2, e2) = findallex_all rty qty a; - in (a1 @ a2, e1 @ e2) end - | _ => ([], []); +fun findallex_all rty qty tm = + case tm of + Const (@{const_name All}, T) $ (s as (Abs(_, _, b))) => + let + val (tya, tye) = findallex_all rty qty s + in if needs_lift rty T then + ((T :: tya), tye) + else (tya, tye) end + | Const (@{const_name Ex}, T) $ (s as (Abs(_, _, b))) => + let + val (tya, tye) = findallex_all rty qty s + in if needs_lift rty T then + (tya, (T :: tye)) + else (tya, tye) end + | Abs(_, T, b) => + findallex_all rty qty (subst_bound ((Free ("x", T)), b)) + | f $ a => + let + val (a1, e1) = findallex_all rty qty f; + val (a2, e2) = findallex_all rty qty a; + in (a1 @ a2, e1 @ e2) end + | _ => ([], []); *} ML {* - fun findallex lthy rty qty tm = - let - val (a, e) = findallex_all rty qty tm; - val (ad, ed) = (map domain_type a, map domain_type e); - val (au, eu) = (distinct (op =) ad, distinct (op =) ed); - val (rty, qty) = (Logic.varifyT rty, Logic.varifyT qty) - in - (map (exchange_ty lthy rty qty) au, map (exchange_ty lthy rty qty) eu) - end +fun findallex lthy rty qty tm = + let + val (a, e) = findallex_all rty qty tm; + val (ad, ed) = (map domain_type a, map domain_type e); + val (au, eu) = (distinct (op =) ad, distinct (op =) ed); + val (rty, qty) = (Logic.varifyT rty, Logic.varifyT qty) + in + (map (exchange_ty lthy rty qty) au, map (exchange_ty lthy rty qty) eu) + end *} ML {* @@ -918,7 +960,8 @@ (quotient_tac quot_thm); val gc = Drule.strip_imp_concl (cprop_of lpi); val t = Goal.prove_internal [] gc (fn _ => tac 1) - val t_noid = MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] t; + val t_noid = MetaSimplifier.rewrite_rule + [@{thm eq_reflection} OF @{thms id_apply}] t; val t_sym = @{thm "HOL.sym"} OF [t_noid]; val t_eq = @{thm "eq_reflection"} OF [t_sym] in @@ -928,36 +971,36 @@ ML {* fun applic_prs lthy rty qty absrep ty = - let + let val rty = Logic.varifyT rty; val qty = Logic.varifyT qty; - fun absty ty = - exchange_ty lthy rty qty ty - fun mk_rep tm = - let - val ty = exchange_ty lthy qty rty (fastype_of tm) - in Syntax.check_term lthy ((get_fun_new repF (rty, qty) lthy ty) $ tm) end; - fun mk_abs tm = - let - val ty = fastype_of tm - in Syntax.check_term lthy ((get_fun_new absF (rty, qty) lthy ty) $ tm) end - val (l, ltl) = Term.strip_type ty; - val nl = map absty l; - val vs = map (fn _ => "x") l; - val ((fname :: vfs), lthy') = Variable.variant_fixes ("f" :: vs) lthy; - val args = map Free (vfs ~~ nl); - val lhs = list_comb((Free (fname, nl ---> ltl)), args); - val rargs = map mk_rep args; - val f = Free (fname, nl ---> ltl); - val rhs = mk_abs (list_comb((mk_rep f), rargs)); - val eq = Logic.mk_equals (rhs, lhs); - val ceq = cterm_of (ProofContext.theory_of lthy') eq; - val sctxt = (Simplifier.context lthy' HOL_ss) addsimps (absrep :: @{thms fun_map.simps}); - val t = Goal.prove_internal [] ceq (fn _ => simp_tac sctxt 1) - val t_id = MetaSimplifier.rewrite_rule @{thms id_def_sym} t; - in - singleton (ProofContext.export lthy' lthy) t_id - end + fun absty ty = + exchange_ty lthy rty qty ty + fun mk_rep tm = + let + val ty = exchange_ty lthy qty rty (fastype_of tm) + in Syntax.check_term lthy ((get_fun_new repF (rty, qty) lthy ty) $ tm) end; + fun mk_abs tm = + let + val ty = fastype_of tm + in Syntax.check_term lthy ((get_fun_new absF (rty, qty) lthy ty) $ tm) end + val (l, ltl) = Term.strip_type ty; + val nl = map absty l; + val vs = map (fn _ => "x") l; + val ((fname :: vfs), lthy') = Variable.variant_fixes ("f" :: vs) lthy; + val args = map Free (vfs ~~ nl); + val lhs = list_comb((Free (fname, nl ---> ltl)), args); + val rargs = map mk_rep args; + val f = Free (fname, nl ---> ltl); + val rhs = mk_abs (list_comb((mk_rep f), rargs)); + val eq = Logic.mk_equals (rhs, lhs); + val ceq = cterm_of (ProofContext.theory_of lthy') eq; + val sctxt = (Simplifier.context lthy' HOL_ss) addsimps (absrep :: @{thms fun_map.simps}); + val t = Goal.prove_internal [] ceq (fn _ => simp_tac sctxt 1) + val t_id = MetaSimplifier.rewrite_rule @{thms id_def_sym} t; + in + singleton (ProofContext.export lthy' lthy) t_id + end *} ML {* @@ -1032,13 +1075,13 @@ ML {* - fun lift_thm_note qty qty_name rsp_thms defs thm name lthy = - let - val lifted_thm = lift_thm lthy qty qty_name rsp_thms defs thm; - val (_, lthy2) = note (name, lifted_thm) lthy; - in - lthy2 - end; +fun lift_thm_note qty qty_name rsp_thms defs thm name lthy = + let + val lifted_thm = lift_thm lthy qty qty_name rsp_thms defs thm; + val (_, lthy2) = note (name, lifted_thm) lthy; + in + lthy2 + end *} diff -r c6a9b4e4d548 -r 40bb0c4718a6 Unused.thy --- a/Unused.thy Mon Nov 09 13:47:46 2009 +0100 +++ b/Unused.thy Mon Nov 09 15:23:33 2009 +0100 @@ -86,3 +86,10 @@ apply (metis) done +ML {* +val no_vars = Thm.rule_attribute (fn context => fn th => + let + val ctxt = Variable.set_body false (Context.proof_of context); + val ((_, [th']), _) = Variable.import true [th] ctxt; + in th' end); +*}