diff -r a6f3e1b08494 -r b6873d123f9b Attic/Quot/quotient_tacs.ML
--- a/Attic/Quot/quotient_tacs.ML	Sat May 12 21:05:59 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,665 +0,0 @@
-(*  Title:      HOL/Tools/Quotient/quotient_tacs.thy
-    Author:     Cezary Kaliszyk and Christian Urban
-
-Tactics for solving goal arising from lifting theorems to quotient
-types.
-*)
-
-signature QUOTIENT_TACS =
-sig
-  val regularize_tac: Proof.context -> int -> tactic
-  val injection_tac: Proof.context -> int -> tactic
-  val all_injection_tac: Proof.context -> int -> tactic
-  val clean_tac: Proof.context -> int -> tactic
-  val procedure_tac: Proof.context -> thm -> int -> tactic
-  val lift_tac: Proof.context -> thm list -> int -> tactic
-  val quotient_tac: Proof.context -> int -> tactic
-  val quot_true_tac: Proof.context -> (term -> term) -> int -> tactic
-  val lifted_attrib: attribute
-end;
-
-structure Quotient_Tacs: QUOTIENT_TACS =
-struct
-
-open Quotient_Info;
-open Quotient_Term;
-
-
-(** various helper fuctions **)
-
-(* Since HOL_basic_ss is too "big" for us, we *)
-(* need to set up our own minimal simpset.    *)
-fun mk_minimal_ss ctxt =
-  Simplifier.context ctxt empty_ss
-    setsubgoaler asm_simp_tac
-    setmksimps (mksimps [])
-
-(* composition of two theorems, used in maps *)
-fun OF1 thm1 thm2 = thm2 RS thm1
-
-(* prints a warning, if the subgoal is not solved *)
-fun WARN (tac, msg) i st =
- case Seq.pull (SOLVED' tac i st) of
-     NONE    => (warning msg; Seq.single st)
-   | seqcell => Seq.make (fn () => seqcell)
-
-fun RANGE_WARN tacs = RANGE (map WARN tacs)
-
-fun atomize_thm thm =
-let
-  val thm' = Thm.freezeT (forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? *)
-  val thm'' = Object_Logic.atomize (cprop_of thm')
-in
-  @{thm equal_elim_rule1} OF [thm'', thm']
-end
-
-
-
-(*** Regularize Tactic ***)
-
-(** solvers for equivp and quotient assumptions **)
-
-fun equiv_tac ctxt =
-  REPEAT_ALL_NEW (resolve_tac (equiv_rules_get ctxt))
-
-fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss)
-val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac
-
-fun quotient_tac ctxt =
-  (REPEAT_ALL_NEW (FIRST'
-    [rtac @{thm identity_quotient},
-     resolve_tac (quotient_rules_get ctxt)]))
-
-fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)
-val quotient_solver =
-  Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac
-
-fun solve_quotient_assm ctxt thm =
-  case Seq.pull (quotient_tac ctxt 1 thm) of
-    SOME (t, _) => t
-  | _ => error "Solve_quotient_assm failed. Possibly a quotient theorem is missing."
-
-
-fun prep_trm thy (x, (T, t)) =
-  (cterm_of thy (Var (x, T)), cterm_of thy t)
-
-fun prep_ty thy (x, (S, ty)) =
-  (ctyp_of thy (TVar (x, S)), ctyp_of thy ty)
-
-fun get_match_inst thy pat trm =
-let
-  val univ = Unify.matchers thy [(pat, trm)]
-  val SOME (env, _) = Seq.pull univ           (* raises Bind, if no unifier *)  (* FIXME fragile *)
-  val tenv = Vartab.dest (Envir.term_env env)
-  val tyenv = Vartab.dest (Envir.type_env env)
-in
-  (map (prep_ty thy) tyenv, map (prep_trm thy) tenv)
-end
-
-(* Calculates the instantiations for the lemmas:
-
-      ball_reg_eqv_range and bex_reg_eqv_range
-
-   Since the left-hand-side contains a non-pattern '?P (f ?x)'
-   we rely on unification/instantiation to check whether the
-   theorem applies and return NONE if it doesn't.
-*)
-fun calculate_inst ctxt ball_bex_thm redex R1 R2 =
-let
-  val thy = ProofContext.theory_of ctxt
-  fun get_lhs thm = fst (Logic.dest_equals (Thm.concl_of thm))
-  val ty_inst = map (SOME o ctyp_of thy) [domain_type (fastype_of R2)]
-  val trm_inst = map (SOME o cterm_of thy) [R2, R1]
-in
-  case try (Drule.instantiate' ty_inst trm_inst) ball_bex_thm of
-    NONE => NONE
-  | SOME thm' =>
-      (case try (get_match_inst thy (get_lhs thm')) redex of
-        NONE => NONE
-      | SOME inst2 => try (Drule.instantiate inst2) thm')
-end
-
-fun ball_bex_range_simproc ss redex =
-let
-  val ctxt = Simplifier.the_context ss
-in
-  case redex of
-    (Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $
-      (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>
-        calculate_inst ctxt @{thm ball_reg_eqv_range[THEN eq_reflection]} redex R1 R2
-
-  | (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $
-      (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>
-        calculate_inst ctxt @{thm bex_reg_eqv_range[THEN eq_reflection]} redex R1 R2
-
-  | _ => NONE
-end
-
-(* Regularize works as follows:
-
-  0. preliminary simplification step according to
-     ball_reg_eqv bex_reg_eqv babs_reg_eqv ball_reg_eqv_range bex_reg_eqv_range
-
-  1. eliminating simple Ball/Bex instances (ball_reg_right bex_reg_left)
-
-  2. monos
-
-  3. commutation rules for ball and bex (ball_all_comm bex_ex_comm)
-
-  4. then rel-equalities, which need to be instantiated with 'eq_imp_rel'
-     to avoid loops
-
-  5. then simplification like 0
-
-  finally jump back to 1
-*)
-
-fun regularize_tac ctxt =
-let
-  val thy = ProofContext.theory_of ctxt
-  val ball_pat = @{term "Ball (Respects (R1 ===> R2)) P"}
-  val bex_pat  = @{term "Bex (Respects (R1 ===> R2)) P"}
-  val simproc = Simplifier.simproc_i thy "" [ball_pat, bex_pat] (K (ball_bex_range_simproc))
-  val simpset = (mk_minimal_ss ctxt)
-                       addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp}
-                       addsimprocs [simproc]
-                       addSolver equiv_solver addSolver quotient_solver
-  val eq_imp_rel = @{lemma "equivp R ==> a = b --> R a b" by (simp add: equivp_reflp)}
-  val eq_eqvs = map (OF1 eq_imp_rel) (equiv_rules_get ctxt)
-in
-  simp_tac simpset THEN'
-  REPEAT_ALL_NEW (CHANGED o FIRST'
-    [resolve_tac @{thms ball_reg_right bex_reg_left bex1_bexeq_reg},
-     resolve_tac (Inductive.get_monos ctxt),
-     resolve_tac @{thms ball_all_comm bex_ex_comm},
-     resolve_tac eq_eqvs,
-     simp_tac simpset])
-end
-
-
-
-(*** Injection Tactic ***)
-
-(* Looks for Quot_True assumptions, and in case its parameter
-   is an application, it returns the function and the argument.
-*)
-fun find_qt_asm asms =
-let
-  fun find_fun trm =
-    case trm of
-      (Const(@{const_name Trueprop}, _) $ (Const (@{const_name Quot_True}, _) $ _)) => true
-    | _ => false
-in
- case find_first find_fun asms of
-   SOME (_ $ (_ $ (f $ a))) => SOME (f, a)
- | _ => NONE
-end
-
-fun quot_true_simple_conv ctxt fnctn ctrm =
-  case (term_of ctrm) of
-    (Const (@{const_name Quot_True}, _) $ x) =>
-    let
-      val fx = fnctn x;
-      val thy = ProofContext.theory_of ctxt;
-      val cx = cterm_of thy x;
-      val cfx = cterm_of thy fx;
-      val cxt = ctyp_of thy (fastype_of x);
-      val cfxt = ctyp_of thy (fastype_of fx);
-      val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QT_imp}
-    in
-      Conv.rewr_conv thm ctrm
-    end
-
-fun quot_true_conv ctxt fnctn ctrm =
-  case (term_of ctrm) of
-    (Const (@{const_name Quot_True}, _) $ _) =>
-      quot_true_simple_conv ctxt fnctn ctrm
-  | _ $ _ => Conv.comb_conv (quot_true_conv ctxt fnctn) ctrm
-  | Abs _ => Conv.abs_conv (fn (_, ctxt) => quot_true_conv ctxt fnctn) ctxt ctrm
-  | _ => Conv.all_conv ctrm
-
-fun quot_true_tac ctxt fnctn =
-   CONVERSION
-    ((Conv.params_conv ~1 (fn ctxt =>
-       (Conv.prems_conv ~1 (quot_true_conv ctxt fnctn)))) ctxt)
-
-fun dest_comb (f $ a) = (f, a)
-fun dest_bcomb ((_ $ l) $ r) = (l, r)
-
-fun unlam t =
-  case t of
-    (Abs a) => snd (Term.dest_abs a)
-  | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0)))
-
-fun dest_fun_type (Type("fun", [T, S])) = (T, S)
-  | dest_fun_type _ = error "dest_fun_type"
-
-val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl
-
-(* We apply apply_rsp only in case if the type needs lifting.
-   This is the case if the type of the data in the Quot_True
-   assumption is different from the corresponding type in the goal.
-*)
-val apply_rsp_tac =
-  Subgoal.FOCUS (fn {concl, asms, context,...} =>
-  let
-    val bare_concl = HOLogic.dest_Trueprop (term_of concl)
-    val qt_asm = find_qt_asm (map term_of asms)
-  in
-    case (bare_concl, qt_asm) of
-      (R2 $ (f $ x) $ (g $ y), SOME (qt_fun, qt_arg)) =>
-         if fastype_of qt_fun = fastype_of f
-         then no_tac
-         else
-           let
-             val ty_x = fastype_of x
-             val ty_b = fastype_of qt_arg
-             val ty_f = range_type (fastype_of f)
-             val thy = ProofContext.theory_of context
-             val ty_inst = map (SOME o (ctyp_of thy)) [ty_x, ty_b, ty_f]
-             val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y];
-             val inst_thm = Drule.instantiate' ty_inst
-               ([NONE, NONE, NONE] @ t_inst) @{thm apply_rsp}
-           in
-             (rtac inst_thm THEN' quotient_tac context) 1
-           end
-    | _ => no_tac
-  end)
-
-(* Instantiates and applies 'equals_rsp'. Since the theorem is
-   complex we rely on instantiation to tell us if it applies
-*)
-fun equals_rsp_tac R ctxt =
-let
-  val thy = ProofContext.theory_of ctxt
-in
-  case try (cterm_of thy) R of (* There can be loose bounds in R *)
-    SOME ctm =>
-      let
-        val ty = domain_type (fastype_of R)
-      in
-        case try (Drule.instantiate' [SOME (ctyp_of thy ty)]
-          [SOME (cterm_of thy R)]) @{thm equals_rsp} of
-          SOME thm => rtac thm THEN' quotient_tac ctxt
-        | NONE => K no_tac
-      end
-  | _ => K no_tac
-end
-
-fun rep_abs_rsp_tac ctxt =
-  SUBGOAL (fn (goal, i) =>
-    case (try bare_concl goal) of
-      SOME (rel $ _ $ (rep $ (abs $ _))) =>
-        let
-          val thy = ProofContext.theory_of ctxt;
-          val (ty_a, ty_b) = dest_fun_type (fastype_of abs);
-          val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b];
-        in
-          case try (map (SOME o (cterm_of thy))) [rel, abs, rep] of
-            SOME t_inst =>
-              (case try (Drule.instantiate' ty_inst t_inst) @{thm rep_abs_rsp} of
-                SOME inst_thm => (rtac inst_thm THEN' quotient_tac ctxt) i
-              | NONE => no_tac)
-          | NONE => no_tac
-        end
-    | _ => no_tac)
-
-
-
-(* Injection means to prove that the regularised theorem implies
-   the abs/rep injected one.
-
-   The deterministic part:
-    - remove lambdas from both sides
-    - prove Ball/Bex/Babs equalities using ball_rsp, bex_rsp, babs_rsp
-    - prove Ball/Bex relations unfolding fun_rel_id
-    - reflexivity of equality
-    - prove equality of relations using equals_rsp
-    - use user-supplied RSP theorems
-    - solve 'relation of relations' goals using quot_rel_rsp
-    - remove rep_abs from the right side
-      (Lambdas under respects may have left us some assumptions)
-
-   Then in order:
-    - split applications of lifted type (apply_rsp)
-    - split applications of non-lifted type (cong_tac)
-    - apply extentionality
-    - assumption
-    - reflexivity of the relation
-*)
-fun injection_match_tac ctxt = SUBGOAL (fn (goal, i) =>
-(case (bare_concl goal) of
-    (* (R1 ===> R2) (%x...) (%x...) ----> [|R1 x y|] ==> R2 (...x) (...y) *)
-  (Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _)
-      => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
-
-    (* (op =) (Ball...) (Ball...) ----> (op =) (...) (...) *)
-| (Const (@{const_name "op ="},_) $
-    (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
-    (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
-      => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all}
-
-    (* (R1 ===> op =) (Ball...) (Ball...) ----> [|R1 x y|] ==> (Ball...x) = (Ball...y) *)
-| (Const (@{const_name fun_rel}, _) $ _ $ _) $
-    (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
-    (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
-      => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
-
-    (* (op =) (Bex...) (Bex...) ----> (op =) (...) (...) *)
-| Const (@{const_name "op ="},_) $
-    (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
-    (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
-      => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex}
-
-    (* (R1 ===> op =) (Bex...) (Bex...) ----> [|R1 x y|] ==> (Bex...x) = (Bex...y) *)
-| (Const (@{const_name fun_rel}, _) $ _ $ _) $
-    (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
-    (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
-      => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
-
-| (Const (@{const_name fun_rel}, _) $ _ $ _) $
-    (Const(@{const_name Bex1_rel},_) $ _) $ (Const(@{const_name Bex1_rel},_) $ _)
-      => rtac @{thm bex1_rel_rsp} THEN' quotient_tac ctxt
-
-| (_ $
-    (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
-    (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
-      => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt]
-
-| Const (@{const_name "op ="},_) $ (R $ _ $ _) $ (_ $ _ $ _) =>
-   (rtac @{thm refl} ORELSE'
-    (equals_rsp_tac R ctxt THEN' RANGE [
-       quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]))
-
-    (* reflexivity of operators arising from Cong_tac *)
-| Const (@{const_name "op ="},_) $ _ $ _ => rtac @{thm refl}
-
-   (* respectfulness of constants; in particular of a simple relation *)
-| _ $ (Const _) $ (Const _)  (* fun_rel, list_rel, etc but not equality *)
-    => resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt
-
-    (* R (...) (Rep (Abs ...)) ----> R (...) (...) *)
-    (* observe fun_map *)
-| _ $ _ $ _
-    => (rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt)
-       ORELSE' rep_abs_rsp_tac ctxt
-
-| _ => K no_tac
-) i)
-
-fun injection_step_tac ctxt rel_refl =
- FIRST' [
-    injection_match_tac ctxt,
-
-    (* R (t $ ...) (t' $ ...) ----> apply_rsp   provided type of t needs lifting *)
-    apply_rsp_tac ctxt THEN'
-                 RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)],
-
-    (* (op =) (t $ ...) (t' $ ...) ----> Cong   provided type of t does not need lifting *)
-    (* merge with previous tactic *)
-    Cong_Tac.cong_tac @{thm cong} THEN'
-                 RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)],
-
-    (* (op =) (%x...) (%y...) ----> (op =) (...) (...) *)
-    rtac @{thm ext} THEN' quot_true_tac ctxt unlam,
-
-    (* resolving with R x y assumptions *)
-    atac,
-
-    (* reflexivity of the basic relations *)
-    (* R ... ... *)
-    resolve_tac rel_refl]
-
-fun injection_tac ctxt =
-let
-  val rel_refl = map (OF1 @{thm equivp_reflp}) (equiv_rules_get ctxt)
-in
-  injection_step_tac ctxt rel_refl
-end
-
-fun all_injection_tac ctxt =
-  REPEAT_ALL_NEW (injection_tac ctxt)
-
-
-
-(*** Cleaning of the Theorem ***)
-
-(* expands all fun_maps, except in front of the (bound) variables listed in xs *)
-fun fun_map_simple_conv xs ctrm =
-  case (term_of ctrm) of
-    ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) =>
-        if member (op=) xs h
-        then Conv.all_conv ctrm
-        else Conv.rewr_conv @{thm fun_map_def[THEN eq_reflection]} ctrm
-  | _ => Conv.all_conv ctrm
-
-fun fun_map_conv xs ctxt ctrm =
-  case (term_of ctrm) of
-      _ $ _ => (Conv.comb_conv (fun_map_conv xs ctxt) then_conv
-                fun_map_simple_conv xs) ctrm
-    | Abs _ => Conv.abs_conv (fn (x, ctxt) => fun_map_conv ((term_of x)::xs) ctxt) ctxt ctrm
-    | _ => Conv.all_conv ctrm
-
-fun fun_map_tac ctxt = CONVERSION (fun_map_conv [] ctxt)
-
-(* custom matching functions *)
-fun mk_abs u i t =
-  if incr_boundvars i u aconv t then Bound i else
-  case t of
-    t1 $ t2 => mk_abs u i t1 $ mk_abs u i t2
-  | Abs (s, T, t') => Abs (s, T, mk_abs u (i + 1) t')
-  | Bound j => if i = j then error "make_inst" else t
-  | _ => t
-
-fun make_inst lhs t =
-let
-  val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs;
-  val _ $ (Abs (_, _, (_ $ g))) = t;
-in
-  (f, Abs ("x", T, mk_abs u 0 g))
-end
-
-fun make_inst_id lhs t =
-let
-  val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs;
-  val _ $ (Abs (_, _, g)) = t;
-in
-  (f, Abs ("x", T, mk_abs u 0 g))
-end
-
-(* Simplifies a redex using the 'lambda_prs' theorem.
-   First instantiates the types and known subterms.
-   Then solves the quotient assumptions to get Rep2 and Abs1
-   Finally instantiates the function f using make_inst
-   If Rep2 is an identity then the pattern is simpler and
-   make_inst_id is used
-*)
-fun lambda_prs_simple_conv ctxt ctrm =
-  case (term_of ctrm) of
-    (Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _) =>
-      let
-        val thy = ProofContext.theory_of ctxt
-        val (ty_b, ty_a) = dest_fun_type (fastype_of r1)
-        val (ty_c, ty_d) = dest_fun_type (fastype_of a2)
-        val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d]
-        val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
-        val thm1 = Drule.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]}
-        val thm2 = solve_quotient_assm ctxt (solve_quotient_assm ctxt thm1)
-        val thm3 = MetaSimplifier.rewrite_rule @{thms id_apply[THEN eq_reflection]} thm2
-        val (insp, inst) =
-          if ty_c = ty_d
-          then make_inst_id (term_of (Thm.lhs_of thm3)) (term_of ctrm)
-          else make_inst (term_of (Thm.lhs_of thm3)) (term_of ctrm)
-        val thm4 = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) thm3
-      in
-        Conv.rewr_conv thm4 ctrm
-      end
-  | _ => Conv.all_conv ctrm
-
-fun lambda_prs_conv ctxt = More_Conv.top_conv lambda_prs_simple_conv ctxt
-fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt)
-
-
-(* Cleaning consists of:
-
-  1. unfolding of ---> in front of everything, except
-     bound variables (this prevents lambda_prs from
-     becoming stuck)
-
-  2. simplification with lambda_prs
-
-  3. simplification with:
-
-      - Quotient_abs_rep Quotient_rel_rep
-        babs_prs all_prs ex_prs ex1_prs
-
-      - id_simps and preservation lemmas and
-
-      - symmetric versions of the definitions
-        (that is definitions of quotient constants
-         are folded)
-
-  4. test for refl
-*)
-fun clean_tac lthy =
-let
-  val defs = map (symmetric o #def) (qconsts_dest lthy)
-  val prs = prs_rules_get lthy
-  val ids = id_simps_get lthy
-  val thms = @{thms Quotient_abs_rep Quotient_rel_rep babs_prs all_prs ex_prs ex1_prs} @ ids @ prs @ defs
-
-  val ss = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
-in
-  EVERY' [fun_map_tac lthy,
-          lambda_prs_tac lthy,
-          simp_tac ss,
-          TRY o rtac refl]
-end
-
-
-
-(** Tactic for Generalising Free Variables in a Goal **)
-
-fun inst_spec ctrm =
-   Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}
-
-fun inst_spec_tac ctrms =
-  EVERY' (map (dtac o inst_spec) ctrms)
-
-fun all_list xs trm =
-  fold (fn (x, T) => fn t' => HOLogic.mk_all (x, T, t')) xs trm
-
-fun apply_under_Trueprop f =
-  HOLogic.dest_Trueprop #> f #> HOLogic.mk_Trueprop
-
-fun gen_frees_tac ctxt =
-  SUBGOAL (fn (concl, i) =>
-    let
-      val thy = ProofContext.theory_of ctxt
-      val vrs = Term.add_frees concl []
-      val cvrs = map (cterm_of thy o Free) vrs
-      val concl' = apply_under_Trueprop (all_list vrs) concl
-      val goal = Logic.mk_implies (concl', concl)
-      val rule = Goal.prove ctxt [] [] goal
-        (K (EVERY1 [inst_spec_tac (rev cvrs), atac]))
-    in
-      rtac rule i
-    end)
-
-
-(** The General Shape of the Lifting Procedure **)
-
-(* - A is the original raw theorem
-   - B is the regularized theorem
-   - C is the rep/abs injected version of B
-   - D is the lifted theorem
-
-   - 1st prem is the regularization step
-   - 2nd prem is the rep/abs injection step
-   - 3rd prem is the cleaning part
-
-   the Quot_True premise in 2nd records the lifted theorem
-*)
-val lifting_procedure_thm =
-  @{lemma  "[|A;
-              A --> B;
-              Quot_True D ==> B = C;
-              C = D|] ==> D"
-      by (simp add: Quot_True_def)}
-
-fun lift_match_error ctxt msg rtrm qtrm =
-let
-  val rtrm_str = Syntax.string_of_term ctxt rtrm
-  val qtrm_str = Syntax.string_of_term ctxt qtrm
-  val msg = cat_lines [enclose "[" "]" msg, "The quotient theorem", qtrm_str,
-    "", "does not match with original theorem", rtrm_str]
-in
-  error msg
-end
-
-fun procedure_inst ctxt rtrm qtrm =
-let
-  val thy = ProofContext.theory_of ctxt
-  val rtrm' = HOLogic.dest_Trueprop rtrm
-  val qtrm' = HOLogic.dest_Trueprop qtrm
-  val reg_goal = regularize_trm_chk ctxt (rtrm', qtrm')
-    handle (ERROR msg) => lift_match_error ctxt msg rtrm qtrm
-  val inj_goal = inj_repabs_trm_chk ctxt (reg_goal, qtrm')
-    handle (ERROR msg) => lift_match_error ctxt msg rtrm qtrm
-in
-  Drule.instantiate' []
-    [SOME (cterm_of thy rtrm'),
-     SOME (cterm_of thy reg_goal),
-     NONE,
-     SOME (cterm_of thy inj_goal)] lifting_procedure_thm
-end
-
-(* the tactic leaves three subgoals to be proved *)
-fun procedure_tac ctxt rthm =
-  Object_Logic.full_atomize_tac
-  THEN' gen_frees_tac ctxt
-  THEN' SUBGOAL (fn (goal, i) =>
-    let
-      val rthm' = atomize_thm rthm
-      val rule = procedure_inst ctxt (prop_of rthm') goal
-    in
-      (rtac rule THEN' rtac rthm') i
-    end)
-
-
-(* Automatic Proofs *)
-
-val msg1 = "The regularize proof failed."
-val msg2 = cat_lines ["The injection proof failed.",
-                      "This is probably due to missing respects lemmas.",
-                      "Try invoking the injection method manually to see",
-                      "which lemmas are missing."]
-val msg3 = "The cleaning proof failed."
-
-fun lift_tac ctxt rthms =
-let
-  fun mk_tac rthm =
-    procedure_tac ctxt rthm
-    THEN' RANGE_WARN
-      [(regularize_tac ctxt, msg1),
-       (all_injection_tac ctxt, msg2),
-       (clean_tac ctxt, msg3)]
-in
-  simp_tac (mk_minimal_ss ctxt) (* unfolding multiple &&& *)
-  THEN' RANGE (map mk_tac rthms)
-end
-
-(* An Attribute which automatically constructs the qthm *)
-fun lifted_attrib_aux context thm =
-let
-  val ctxt = Context.proof_of context
-  val ((_, [thm']), ctxt') = Variable.import false [thm] ctxt
-  val goal = (quotient_lift_all ctxt' o prop_of) thm'
-in
-  Goal.prove ctxt' [] [] goal (K (lift_tac ctxt' [thm] 1))
-  |> singleton (ProofContext.export ctxt' ctxt)
-end;
-
-val lifted_attrib = Thm.rule_attribute lifted_attrib_aux
-
-end; (* structure *)