(*  Title:      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 *)

   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 (LIFT_MATCH msg) => lift_match_error ctxt msg rtrm qtrm

   val inj_goal = inj_repabs_trm_chk ctxt (reg_goal, qtrm')

     handle (LIFT_MATCH 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 *)