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} @ (id_simps_get ctxt)

                       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 (bare_concl goal) of 

      (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];

           val t_inst = map (SOME o (cterm_of thy)) [rel, abs, rep];

           val inst_thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp}

         in

           (rtac inst_thm THEN' quotient_tac ctxt) i

         end

         handle THM _ => no_tac | TYPE _ => no_tac) (* TODO: same here *)

    | _ => no_tac)

(*

we try:

    (Lambdas under respects may have left us some assumptions)

*)

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

  simp_tac ((mk_minimal_ss ctxt) addsimps (id_simps_get ctxt)) (* HACK? *) 

  THEN' 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

     handle _ => Conv.all_conv ctrm) (* TODO: another catch all - can this be improved? *)

  | _ => 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)

(* 1. folding of definitions and preservation lemmas;  *)

(*    and simplification with                          *)

(*    thm babs_prs all_prs ex_prs                      *)

(*                                                     *) 

(* 2. unfolding of ---> in front of everything, except *)

(*    bound variables (this prevents lambda_prs from   *)

(*    becoming stuck)                                  *)

(*    thm fun_map.simps                                *)

(*                                                     *)

(* 3. simplification with                              *)

(*    thm lambda_prs                                   *)

(*                                                     *)

(* 4. simplification with                              *)

(*    thm Quotient_abs_rep Quotient_rel_rep id_simps   *) 

(*                                                     *)