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 -> int -> tactic
    val quotient_tac: Proof.context -> int -> tactic
    val quot_true_tac: Proof.context -> (term -> term) -> int -> tactic
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

(* makes sure a subgoal is solved *)
fun SOLVES' tac = tac THEN_ALL_NEW (K no_tac)

(* prints a warning, if the subgoal is not solved *)
fun WARN (tac, msg) i st =
 case Seq.pull ((SOLVES' 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'' = ObjectLogic.atomize (cprop_of thm')
in
  @{thm equal_elim_rule1} OF [thm'', thm']
end



(*** Regularize Tactic ***)

(** solvers for equivp and quotient assumptions **)

(* FIXME / TODO: should this SOLVES' the goal, like with quotient_tac? *)
(* FIXME / TODO: none of te examples break if added                    *)
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

(* FIXME / TODO: test whether DETERM makes any runtime-difference *)
(* FIXME / TODO: reason: the tactic might back-track over the two alternatives in FIRST' *)
fun quotient_tac ctxt = SOLVES'
  (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
  fun get_lhs thm = fst (Logic.dest_equals (Thm.concl_of thm))
  val thy = ProofContext.theory_of ctxt
  val typ_inst1 = map (SOME o ctyp_of thy) [domain_type (fastype_of R2)]
  val trm_inst1 = map (SOME o cterm_of thy) [R2, R1]
in
  (case try (Drule.instantiate' typ_inst1 trm_inst1) 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

(* 0. preliminary simplification step according to *)
(*    thm ball_reg_eqv bex_reg_eqv babs_reg_eqv    *)
(*        ball_reg_eqv_range bex_reg_eqv_range     *)
(*                                                 *)
(* 1. eliminating simple Ball/Bex instances        *)
(*    thm ball_reg_right bex_reg_left              *)
(*                                                 *)
(* 2. monos                                        *)
(*                                                 *)
(* 3. commutation rules for ball and bex           *)
(*    thm ball_all_comm bex_ex_comm                *)
(*                                                 *)
(* 4. then rel-equalities, which need to be        *)
(*    instantiated with the followig theorem       *)
(*    to avoid loops:                              *)
(*    thm eq_imp_rel                               *)
(*                                                 *)
(* 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_eqvs = map (OF1 @{thm 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},
     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 assumtions, 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
(* TODO: Again, can one specify more concretely        *)
(* TODO: in terms of R when no_tac should be returned? *)

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)


(*
To prove that the regularised theorem implies the abs/rep injected,
we try:

 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 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.simps[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)


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 lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]}
        val te = solve_quotient_assm ctxt (solve_quotient_assm ctxt lpi)
        val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te
        val (insp, inst) =
          if ty_c = ty_d
          then make_inst_id (term_of (Thm.lhs_of ts)) (term_of ctrm)
          else make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm)
        val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts
      in
        Conv.rewr_conv ti 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. folding of definitions and preservation lemmas;
    and simplification with babs_prs all_prs ex_prs

 2. unfolding of ---> in front of everything, except
    bound variables
    (this prevents lambda_prs from becoming stuck)

 3. simplification with lambda_prs

 4. simplification with Quotient_abs_rep Quotient_rel_rep id_simps

 5. test for refl *)
fun clean_tac lthy =
let
  (* FIXME/TODO produce defs with lthy, like prs and ids *)
  val thy = ProofContext.theory_of lthy;
  val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy)
  (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *)
  val prs = prs_rules_get lthy
  val ids = id_simps_get lthy
  
  fun mk_simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
  val ss1 = mk_simps (defs @ prs @ @{thms babs_prs all_prs ex_prs})
  val ss2 = mk_simps (@{thms Quotient_abs_rep Quotient_rel_rep} @ ids) 
in
  EVERY' [simp_tac ss1,
          fun_map_tac lthy,
          lambda_prs_tac lthy,
          simp_tac ss2,
          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 str 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 "[" "]" str, "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 str) => lift_match_error ctxt str rtrm qtrm
  val inj_goal = inj_repabs_trm_chk ctxt (reg_goal, qtrm')
    handle (LIFT_MATCH str) => lift_match_error ctxt str 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 =
  ObjectLogic.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 = "Regularize proof failed."
val msg2 = cat_lines ["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 = "Cleaning proof failed."

fun lift_tac ctxt rthm =
  procedure_tac ctxt rthm
  THEN' RANGE_WARN 
     [(regularize_tac ctxt, msg1),
      (all_injection_tac ctxt, msg2),
      (clean_tac ctxt, msg3)]

end; (* structure *)
