theory QuotMain
imports QuotScript Prove
uses ("quotient_info.ML")
     ("quotient.ML")
     ("quotient_def.ML")
begin


locale QUOT_TYPE =
  fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
  and   Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
  and   Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)"
  assumes equivp: "equivp R"
  and     rep_prop: "\<And>y. \<exists>x. Rep y = R x"
  and     rep_inverse: "\<And>x. Abs (Rep x) = x"
  and     abs_inverse: "\<And>x. (Rep (Abs (R x))) = (R x)"
  and     rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)"
begin

definition
  ABS::"'a \<Rightarrow> 'b"
where
  "ABS x \<equiv> Abs (R x)"

definition
  REP::"'b \<Rightarrow> 'a"
where
  "REP a = Eps (Rep a)"

lemma lem9:
  shows "R (Eps (R x)) = R x"
proof -
  have a: "R x x" using equivp by (simp add: equivp_reflp_symp_transp reflp_def)
  then have "R x (Eps (R x))" by (rule someI)
  then show "R (Eps (R x)) = R x"
    using equivp unfolding equivp_def by simp
qed

theorem thm10:
  shows "ABS (REP a) \<equiv> a"
  apply  (rule eq_reflection)
  unfolding ABS_def REP_def
proof -
  from rep_prop
  obtain x where eq: "Rep a = R x" by auto
  have "Abs (R (Eps (Rep a))) = Abs (R (Eps (R x)))" using eq by simp
  also have "\<dots> = Abs (R x)" using lem9 by simp
  also have "\<dots> = Abs (Rep a)" using eq by simp
  also have "\<dots> = a" using rep_inverse by simp
  finally
  show "Abs (R (Eps (Rep a))) = a" by simp
qed

lemma REP_refl:
  shows "R (REP a) (REP a)"
unfolding REP_def
by (simp add: equivp[simplified equivp_def])

lemma lem7:
  shows "(R x = R y) = (Abs (R x) = Abs (R y))"
apply(rule iffI)
apply(simp)
apply(drule rep_inject[THEN iffD2])
apply(simp add: abs_inverse)
done

theorem thm11:
  shows "R r r' = (ABS r = ABS r')"
unfolding ABS_def
by (simp only: equivp[simplified equivp_def] lem7)


lemma REP_ABS_rsp:
  shows "R f (REP (ABS g)) = R f g"
  and   "R (REP (ABS g)) f = R g f"
by (simp_all add: thm10 thm11)

lemma Quotient:
  "Quotient R ABS REP"
apply(unfold Quotient_def)
apply(simp add: thm10)
apply(simp add: REP_refl)
apply(subst thm11[symmetric])
apply(simp add: equivp[simplified equivp_def])
done

lemma R_trans:
  assumes ab: "R a b"
  and     bc: "R b c"
  shows "R a c"
proof -
  have tr: "transp R" using equivp equivp_reflp_symp_transp[of R] by simp
  moreover have ab: "R a b" by fact
  moreover have bc: "R b c" by fact
  ultimately show "R a c" unfolding transp_def by blast
qed

lemma R_sym:
  assumes ab: "R a b"
  shows "R b a"
proof -
  have re: "symp R" using equivp equivp_reflp_symp_transp[of R] by simp
  then show "R b a" using ab unfolding symp_def by blast
qed

lemma R_trans2:
  assumes ac: "R a c"
  and     bd: "R b d"
  shows "R a b = R c d"
using ac bd
by (blast intro: R_trans R_sym)

lemma REPS_same:
  shows "R (REP a) (REP b) \<equiv> (a = b)"
proof -
  have "R (REP a) (REP b) = (a = b)"
  proof
    assume as: "R (REP a) (REP b)"
    from rep_prop
    obtain x y
      where eqs: "Rep a = R x" "Rep b = R y" by blast
    from eqs have "R (Eps (R x)) (Eps (R y))" using as unfolding REP_def by simp
    then have "R x (Eps (R y))" using lem9 by simp
    then have "R (Eps (R y)) x" using R_sym by blast
    then have "R y x" using lem9 by simp
    then have "R x y" using R_sym by blast
    then have "ABS x = ABS y" using thm11 by simp
    then have "Abs (Rep a) = Abs (Rep b)" using eqs unfolding ABS_def by simp
    then show "a = b" using rep_inverse by simp
  next
    assume ab: "a = b"
    have "reflp R" using equivp equivp_reflp_symp_transp[of R] by simp
    then show "R (REP a) (REP b)" unfolding reflp_def using ab by auto
  qed
  then show "R (REP a) (REP b) \<equiv> (a = b)" by simp
qed

end

section {* type definition for the quotient type *}

(* the auxiliary data for the quotient types *)
use "quotient_info.ML"

declare [[map "fun" = (fun_map, fun_rel)]]

lemmas [quot_thm] = fun_quotient 

lemmas [quot_respect] = quot_rel_rsp

(* fun_map is not here since equivp is not true *)
lemmas [quot_equiv] = identity_equivp

(* definition of the quotient types *)
(* FIXME: should be called quotient_typ.ML *)
use "quotient.ML"

(* lifting of constants *)
use "quotient_def.ML"

section {* Simset setup *}

(* Since HOL_basic_ss is too "big" for us, *)
(* we set up our own minimal simpset.      *)
ML {*
fun  mk_minimal_ss ctxt =
  Simplifier.context ctxt empty_ss
    setsubgoaler asm_simp_tac
    setmksimps (mksimps [])
*}

ML {*
fun OF1 thm1 thm2 = thm2 RS thm1
*}

section {* Atomize Infrastructure *}

lemma atomize_eqv[atomize]:
  shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"
proof
  assume "A \<equiv> B"
  then show "Trueprop A \<equiv> Trueprop B" by unfold
next
  assume *: "Trueprop A \<equiv> Trueprop B"
  have "A = B"
  proof (cases A)
    case True
    have "A" by fact
    then show "A = B" using * by simp
  next
    case False
    have "\<not>A" by fact
    then show "A = B" using * by auto
  qed
  then show "A \<equiv> B" by (rule eq_reflection)
qed

ML {*
fun atomize_thm thm =
let
  val thm' = Thm.freezeT (forall_intr_vars thm)
  val thm'' = ObjectLogic.atomize (cprop_of thm')
in
  @{thm equal_elim_rule1} OF [thm'', thm']
end
*}

section {* Infrastructure about id *}

lemmas [id_simps] =
  fun_map_id[THEN eq_reflection]
  id_apply[THEN eq_reflection]
  id_def[THEN eq_reflection,symmetric]

section {* Debugging infrastructure for testing tactics *}

ML {*
fun my_print_tac ctxt s i thm =
let
  val prem_str = nth (prems_of thm) (i - 1)
                 |> Syntax.string_of_term ctxt
                 handle Subscript => "no subgoal"
  val _ = tracing (s ^ "\n" ^ prem_str)
in
  Seq.single thm
end *}

ML {*
fun DT ctxt s tac i thm =
let
  val before_goal = nth (prems_of thm) (i - 1)
                    |> Syntax.string_of_term ctxt
  val before_msg = ["before: " ^ s, before_goal, "after: " ^ s]
                   |> cat_lines
in 
  EVERY [tac i, my_print_tac ctxt before_msg i] thm
end

fun NDT ctxt s tac thm = tac thm  
*}

section {* Matching of Terms and Types *}

ML {*
fun struct_match_typ (ty, ty') =
  case (ty, ty') of
    (_, TVar _) => true
  | (TFree x, TFree x') => x = x'
  | (Type (s, tys), Type (s', tys')) => 
       s = s' andalso 
       if (length tys = length tys') 
       then (List.all struct_match_typ (tys ~~ tys')) 
       else false
  | _ => false

fun struct_match_term (trm, trm') = 
   case (trm, trm') of 
     (_, Var _) => true
   | (Const (s, ty), Const (s', ty')) => s = s' andalso struct_match_typ (ty, ty')
   | (Free (x, ty), Free (x', ty')) => x = x' andalso struct_match_typ (ty, ty')
   | (Bound i, Bound j) => i = j
   | (Abs (_, T, t), Abs (_, T', t')) => struct_match_typ (T, T') andalso struct_match_term (t, t')
   | (t $ s, t' $ s') => struct_match_term (t, t') andalso struct_match_term (s, s') 
   | _ => false
*}

section {* Computation of the Regularize Goal *} 

(*
Regularizing an rtrm means:
 - quantifiers over a type that needs lifting are replaced by
   bounded quantifiers, for example:
      \<forall>x. P     \<Longrightarrow>     \<forall>x \<in> (Respects R). P  /  All (Respects R) P

   the relation R is given by the rty and qty;
 
 - abstractions over a type that needs lifting are replaced
   by bounded abstractions:
      \<lambda>x. P     \<Longrightarrow>     Ball (Respects R) (\<lambda>x. P)

 - equalities over the type being lifted are replaced by
   corresponding relations:
      A = B     \<Longrightarrow>     A \<approx> B

   example with more complicated types of A, B:
      A = B     \<Longrightarrow>     (op = \<Longrightarrow> op \<approx>) A B
*)

ML {*
(* builds the relation that is the argument of respects *)
fun mk_resp_arg lthy (rty, qty) =
let
  val thy = ProofContext.theory_of lthy
in  
  if rty = qty
  then HOLogic.eq_const rty
  else
    case (rty, qty) of
      (Type (s, tys), Type (s', tys')) =>
       if s = s' 
       then let
              val SOME map_info = maps_lookup thy s
              val args = map (mk_resp_arg lthy) (tys ~~ tys')
            in
              list_comb (Const (#relfun map_info, dummyT), args) 
            end  
       else let  
              val SOME qinfo = quotdata_lookup_thy thy s'
              (* FIXME: check in this case that the rty and qty *)
              (* FIXME: correspond to each other *)
              val (s, _) = dest_Const (#rel qinfo)
              (* FIXME: the relation should only be the string        *)
              (* FIXME: and the type needs to be calculated as below; *)
              (* FIXME: maybe one should actually have a term         *)
              (* FIXME: and one needs to force it to have this type   *)
            in
              Const (s, rty --> rty --> @{typ bool})
            end
      | _ => HOLogic.eq_const dummyT 
             (* FIXME: check that the types correspond to each other? *)
end
*}

ML {*
val mk_babs = Const (@{const_name Babs}, dummyT)
val mk_ball = Const (@{const_name Ball}, dummyT)
val mk_bex  = Const (@{const_name Bex}, dummyT)
val mk_resp = Const (@{const_name Respects}, dummyT)
*}

ML {*
(* - applies f to the subterm of an abstraction,   *)
(*   otherwise to the given term,                  *)
(* - used by regularize, therefore abstracted      *)
(*   variables do not have to be treated specially *)

fun apply_subt f trm1 trm2 =
  case (trm1, trm2) of
    (Abs (x, T, t), Abs (x', T', t')) => Abs (x, T, f t t')
  | _ => f trm1 trm2

(* the major type of All and Ex quantifiers *)
fun qnt_typ ty = domain_type (domain_type ty)  
*}

ML {*
(* produces a regularized version of rtrm     *)
(* - the result is contains dummyT            *)
(* - does not need any special treatment of   *)
(*   bound variables                          *)

fun regularize_trm lthy rtrm qtrm =
  case (rtrm, qtrm) of
    (Abs (x, ty, t), Abs (x', ty', t')) =>
       let
         val subtrm = Abs(x, ty, regularize_trm lthy t t')
       in
         if ty = ty' then subtrm
         else mk_babs $ (mk_resp $ mk_resp_arg lthy (ty, ty')) $ subtrm
       end

  | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') =>
       let
         val subtrm = apply_subt (regularize_trm lthy) t t'
       in
         if ty = ty' then Const (@{const_name "All"}, ty) $ subtrm
         else mk_ball $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm
       end

  | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') =>
       let
         val subtrm = apply_subt (regularize_trm lthy) t t'
       in
         if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm
         else mk_bex $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm
       end

  | (* equalities need to be replaced by appropriate equivalence relations *) 
    (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) =>
         if ty = ty' then rtrm
         else mk_resp_arg lthy (domain_type ty, domain_type ty') 

  | (* in this case we check whether the given equivalence relation is correct *) 
    (rel, Const (@{const_name "op ="}, ty')) =>
       let 
         val exc = LIFT_MATCH "regularise (relation mismatch)"
         val rel_ty = (fastype_of rel) handle TERM _ => raise exc 
         val rel' = mk_resp_arg lthy (domain_type rel_ty, domain_type ty') 
       in 
         if rel' = rel then rtrm else raise exc
       end  
  | (_, Const (s, Type(st, _))) =>
       let 
         fun same_name (Const (s, _)) (Const (s', _)) = (s = s')
           | same_name _ _ = false
       in
         (* TODO/FIXME: This test is not enough *)
         if same_name rtrm qtrm then rtrm
         else 
           let 
             val exc1 = LIFT_MATCH ("regularize (constant " ^ s ^ "(" ^ st ^ ") not found)")
             val exc2 = LIFT_MATCH ("regularize (constant " ^ s ^ "(" ^ st ^ ") mismatch)")
             val thy = ProofContext.theory_of lthy
             val rtrm' = (#rconst (qconsts_lookup thy qtrm)) handle NotFound => raise exc1
           in 
             if struct_match_term (rtrm, rtrm') then rtrm else
               let
                 val _ = tracing (Syntax.string_of_term @{context} rtrm);
                 val _ = tracing (Syntax.string_of_term @{context} rtrm');
               in raise exc2 end
           end
       end 

  | (t1 $ t2, t1' $ t2') =>
       (regularize_trm lthy t1 t1') $ (regularize_trm lthy t2 t2')

  | (Free (x, ty), Free (x', ty')) => 
       (* this case cannot arrise as we start with two fully atomized terms *)
       raise (LIFT_MATCH "regularize (frees)")

  | (Bound i, Bound i') =>
       if i = i' then rtrm 
       else raise (LIFT_MATCH "regularize (bounds mismatch)")

  | (rt, qt) =>
       raise (LIFT_MATCH "regularize failed (default)")
*}

section {* Regularize Tactic *}

ML {*
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
*}

ML {*
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)
*}

ML {*
fun matching_prs thy pat trm =
let
  val univ = Unify.matchers thy [(pat, trm)]
  val SOME (env, _) = Seq.pull univ
  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
*}

ML {*
fun calculate_instance ctxt thm redex R1 R2 =
let
  val thy = ProofContext.theory_of ctxt
  val goal = Const (@{const_name "equivp"}, dummyT) $ R2  
             |> Syntax.check_term ctxt
             |> HOLogic.mk_Trueprop 
  val eqv_prem = Goal.prove ctxt [] [] goal (fn {context,...} => equiv_tac context 1)
  val thm = (@{thm eq_reflection} OF [thm OF [eqv_prem]])
  val R1c = cterm_of thy R1
  val thmi = Drule.instantiate' [] [SOME R1c] thm
  val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) redex
  val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi)
in
  SOME thm2
end
handle _ => NONE
(* FIXME/TODO: what is the place where the exception is raised: matching_prs? *)
*}

ML {*
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_instance ctxt @{thm ball_reg_eqv_range} redex R1 R2
  | (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $ 
      (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>  
        calculate_instance ctxt @{thm bex_reg_eqv_range} redex R1 R2
  | _ => NONE
end
*}

lemma eq_imp_rel: 
  shows "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b"
by (simp add: equivp_reflp)

(* Regularize Tactic *)

(* 0. preliminary simplification step according to *)
thm ball_reg_eqv bex_reg_eqv babs_reg_eqv (* the latter of no use *)
    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-equality (which need to be instantiated to avoid loops *)
thm eq_imp_rel
(* 5. then simplification like 0 *)
(* finally jump back to 1 *)


ML {*
fun regularize_tac ctxt =
let
  val thy = ProofContext.theory_of ctxt
  val pat_ball = @{term "Ball (Respects (R1 ===> R2)) P"}
  val pat_bex  = @{term "Bex (Respects (R1 ===> R2)) P"}
  val simproc = Simplifier.simproc_i thy "" [pat_ball, pat_bex] (K (ball_bex_range_simproc))
  val simpset = (mk_minimal_ss ctxt) 
                       addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv}
                       addsimprocs [simproc] addSolver equiv_solver
  (* TODO: Make sure that there are no list_rel, pair_rel etc involved *)
  (* can this cause loops in equiv_tac ? *)
  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
*}

section {* Calculation of the Injected Goal *}

(*
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. This in combination
      with the RepAbs above will let us change the type of the
      abstraction with rewriting.
  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.
*)

ML {*
fun mk_repabs lthy (T, T') trm = 
  Quotient_Def.get_fun repF lthy (T, T') 
    $ (Quotient_Def.get_fun absF lthy (T, T') $ trm)
*}

ML {*
(* bound variables need to be treated properly,    *)
(* as the type of subterms need to be calculated   *)
(* in the abstraction case                         *)

fun inj_repabs_trm lthy (rtrm, qtrm) =
 case (rtrm, qtrm) of
    (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') =>
       Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm lthy (t, t'))

  | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') =>
       Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm lthy (t, t'))

  | (Const (@{const_name "Babs"}, T) $ r $ t, t' as (Abs _)) =>
      let
        val rty = fastype_of rtrm
        val qty = fastype_of qtrm
      in
        mk_repabs lthy (rty, qty) (Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm lthy (t, t')))
      end

  | (Abs (x, T, t), Abs (x', T', t')) =>
      let
        val rty = fastype_of rtrm
        val qty = fastype_of qtrm
        val (y, s) = Term.dest_abs (x, T, t)
        val (_, s') = Term.dest_abs (x', T', t')
        val yvar = Free (y, T)
        val result = Term.lambda_name (y, yvar) (inj_repabs_trm lthy (s, s'))
      in
        if rty = qty then result
        else mk_repabs lthy (rty, qty) result
      end

  | (t $ s, t' $ s') =>  
       (inj_repabs_trm lthy (t, t')) $ (inj_repabs_trm lthy (s, s'))

  | (Free (_, T), Free (_, T')) => 
        if T = T' then rtrm 
        else mk_repabs lthy (T, T') rtrm

  | (_, Const (@{const_name "op ="}, _)) => rtrm

    (* FIXME: check here that rtrm is the corresponding definition for the const *)
    (* Hasn't it already been checked in regularize? *)
  | (_, Const (_, T')) =>
      let
        val rty = fastype_of rtrm
      in 
        if rty = T' then rtrm
        else mk_repabs lthy (rty, T') rtrm
      end   
  
  | _ => raise (LIFT_MATCH "injection")
*}

section {* Injection Tactic *}

ML {*
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
*}

ML {*
fun solve_quotient_assums ctxt thm =
let 
  val goal = hd (Drule.strip_imp_prems (cprop_of thm)) 
in
  thm OF [Goal.prove_internal [] goal (fn _ => quotient_tac ctxt 1)]
end
handle _ => error "solve_quotient_assums failed. Maybe a quotient_thm is missing"
*}

definition
  "QUOT_TRUE x \<equiv> True"

ML {*
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))) => (f, a)
    | SOME _ => error "find_qt_asm: no pair"
    | NONE => error "find_qt_asm: no assumption"
  end
*}

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

 1) theorems 'trans2' from the appropriate QUOT_TYPE
 2) remove lambdas from both sides: lambda_rsp_tac
 3) remove Ball/Bex from the right hand side
 4) use user-supplied RSP theorems
 5) remove rep_abs from the right side
 6) reflexivity of equality
 7) split applications of lifted type (apply_rsp)
 8) split applications of non-lifted type (cong_tac)
 9) apply extentionality
 A) reflexivity of the relation
 B) assumption
    (Lambdas under respects may have left us some assumptions)
 C) proving obvious higher order equalities by simplifying fun_rel
    (not sure if it is still needed?)
 D) unfolding lambda on one side
 E) simplifying (= ===> =) for simpler respectfulness

*)

lemma quot_true_dests:
  shows QT_all: "QUOT_TRUE (All P) \<Longrightarrow> QUOT_TRUE P"
  and   QT_ex:  "QUOT_TRUE (Ex P) \<Longrightarrow> QUOT_TRUE P"
  and   QT_lam: "QUOT_TRUE (\<lambda>x. P x) \<Longrightarrow> (\<And>x. QUOT_TRUE  (P x))"
  and   QT_ext: "(\<And>x. QUOT_TRUE (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (QUOT_TRUE a \<Longrightarrow> f = g)"
by (simp_all add: QUOT_TRUE_def ext)

lemma QUOT_TRUE_i: "(QUOT_TRUE (a :: bool) \<Longrightarrow> P) \<Longrightarrow> P"
by (simp add: QUOT_TRUE_def)

lemma QUOT_TRUE_imp: "QUOT_TRUE a \<equiv> QUOT_TRUE b"
by (simp add: QUOT_TRUE_def)

ML {*
fun quot_true_conv1 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 QUOT_TRUE_imp}
    in
      Conv.rewr_conv thm ctrm
    end
*}

ML {*
fun quot_true_conv ctxt fnctn ctrm =
  case (term_of ctrm) of
    (Const (@{const_name QUOT_TRUE}, _) $ _) =>
      quot_true_conv1 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
*}

ML {*
fun quot_true_tac ctxt fnctn = CONVERSION
    ((Conv.params_conv ~1 (fn ctxt =>
       (Conv.prems_conv ~1 (quot_true_conv ctxt fnctn)))) ctxt)
*}

ML {* fun dest_comb (f $ a) = (f, a) *}
ML {* fun dest_bcomb ((_ $ l) $ r) = (l, r) *}
(* TODO: Can this be done easier? *)
ML {*
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)))
*}

ML {*
fun dest_fun_type (Type("fun", [T, S])) = (T, S)
  | dest_fun_type _ = error "dest_fun_type"
*}

ML {*
val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl
*}

ML {*
val apply_rsp_tac =
  Subgoal.FOCUS (fn {concl, asms, context,...} =>
    case ((HOLogic.dest_Trueprop (term_of concl))) of
      ((R2 $ (f $ x) $ (g $ y))) =>
        (let
          val (asmf, asma) = find_qt_asm (map term_of asms);
        in
          if (fastype_of asmf) = (fastype_of f) then no_tac else let
            val ty_a = fastype_of x;
            val ty_b = fastype_of asma;
            val ty_c = range_type (type_of f);
            val thy = ProofContext.theory_of context;
            val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c];
            val thm = Drule.instantiate' ty_inst [] @{thm apply_rsp}
            val te = solve_quotient_assums context thm
            val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y];
            val thm = Drule.instantiate' [] t_inst te
          in
            compose_tac (false, thm, 2) 1
          end
        end
        handle ERROR "find_qt_asm: no pair" => no_tac)
    | _ => no_tac)
*}

ML {*
fun equals_rsp_tac R ctxt =
  let
    val t = domain_type (fastype_of R);
    val thy = ProofContext.theory_of ctxt
    val thm = Drule.instantiate' [SOME (ctyp_of thy t)] [SOME (cterm_of thy R)] @{thm equals_rsp}
  in
    rtac thm THEN' RANGE [quotient_tac ctxt]
  end
  handle THM _ => K no_tac | TYPE _ => K no_tac | TERM _ => K no_tac
*}

ML {*
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 thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp}
           val te = solve_quotient_assums ctxt thm
         in
           rtac te i
         end
         handle _ => no_tac)
    | _ => no_tac)
*}

ML {*
fun inj_repabs_tac_match ctxt = SUBGOAL (fn (goal, i) =>
(case (bare_concl goal) of
    (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *)
  ((Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _))
      => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam

    (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
| (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\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> (Ball\<dots>x) = (Ball\<dots>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\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
| 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\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> (Bex\<dots>x) = (Bex\<dots>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 (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *)
    (* observe ---> *)
| _ $ _ $ _
    => (rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt) ORELSE' rep_abs_rsp_tac ctxt

| _ => error "inj_repabs_tac not a relation"
) i)
*}

ML {*
fun inj_repabs_step_tac ctxt rel_refl =
  (FIRST' [
    NDT ctxt "0" (inj_repabs_tac_match ctxt),
    (* R (t $ \<dots>) (t' $ \<dots>) ----> apply_rsp   provided type of t needs lifting *)
    
    NDT ctxt "A" (apply_rsp_tac ctxt THEN'
                 RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)]),

    (* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong   provided type of t does not need lifting *)
    (* merge with previous tactic *)
    NDT ctxt "C" (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 =) (\<lambda>x\<dots>) (\<lambda>x\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
    NDT ctxt "D" (rtac @{thm ext} THEN' quot_true_tac ctxt unlam),
    
    (* resolving with R x y assumptions *)
    NDT ctxt "E" (atac),
    
    (* reflexivity of the basic relations *)
    (* R \<dots> \<dots> *)
    NDT ctxt "F" (resolve_tac rel_refl)
    ])
*}

ML {*
fun inj_repabs_tac ctxt =
let
  val rel_refl = map (OF1 @{thm equivp_reflp}) (equiv_rules_get ctxt)
in
  inj_repabs_step_tac ctxt rel_refl
end

fun all_inj_repabs_tac ctxt =
  REPEAT_ALL_NEW (inj_repabs_tac ctxt)
*}

section {* Cleaning of the Theorem *}

ML {*
fun fun_map_simple_conv xs ctxt 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 ctxt) 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)
*}

(* Since the patterns for the lhs are different; there are 3 different make-insts *)
(* 1: does  ? \<rightarrow> id *)
(* 2: does id \<rightarrow> ? *)
(* 3: does  ? \<rightarrow> ? *)
ML {*
fun make_inst lhs t =
  let
    val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs;
    val _ $ (Abs (_, _, g)) = t;
    fun mk_abs i t =
      if incr_boundvars i u aconv t then Bound i
      else (case t of
        t1 $ t2 => mk_abs i t1 $ mk_abs i t2
      | Abs (s, T, t') => Abs (s, T, mk_abs (i + 1) t')
      | Bound j => if i = j then error "make_inst" else t
      | _ => t);
  in (f, Abs ("x", T, mk_abs 0 g)) end;
*}

ML {*
fun make_inst2 lhs t =
  let
    val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs;
    val _ $ (Abs (_, _, (_ $ g))) = t;
    fun mk_abs i t =
      if incr_boundvars i u aconv t then Bound i
      else (case t of
        t1 $ t2 => mk_abs i t1 $ mk_abs i t2
      | Abs (s, T, t') => Abs (s, T, mk_abs (i + 1) t')
      | Bound j => if i = j then error "make_inst" else t
      | _ => t);
  in (f, Abs ("x", T, mk_abs 0 g)) end;
*}

ML {*
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}
       val te = @{thm eq_reflection} OF [solve_quotient_assums ctxt (solve_quotient_assums ctxt lpi)]
       val ti =
         (let
           val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te
           val (insp, inst) = make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm)
         in
           Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts
         end handle _ => (* TODO handle only Bind | Error "make_inst" *)
         let
           val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te
           val _ = tracing ("ts rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ts)));
           val _ = tracing ("redex:\n" ^ (Syntax.string_of_term ctxt (term_of ctrm)));
           val (insp, inst) = make_inst2 (term_of (Thm.lhs_of ts)) (term_of ctrm)
         in
           Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts
         end handle _ => (* TODO handle only Bind | Error "make_inst" *)
         let
           val (insp, inst) = make_inst2 (term_of (Thm.lhs_of te)) (term_of ctrm)
           val td = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) te
         in
           MetaSimplifier.rewrite_rule (id_simps_get ctxt) td
         end);
       val _ = if not (Term.is_Const a2 andalso fst (dest_Const a2) = @{const_name "id"}) then
                  (tracing "lambda_prs";
                   tracing ("redex:\n" ^ (Syntax.string_of_term ctxt (term_of ctrm)));
                   tracing ("lpi rule:\n" ^ (Syntax.string_of_term ctxt (prop_of lpi)));
                   tracing ("te rule:\n" ^ (Syntax.string_of_term ctxt (prop_of te)));
                   tracing ("ti rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ti))))
               else ()

     in
       Conv.rewr_conv ti ctrm
     end
     handle _ => Conv.all_conv ctrm)
  | _ => Conv.all_conv ctrm
*}

ML {*
val lambda_prs_conv =
  More_Conv.top_conv lambda_prs_simple_conv

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                                  *)
thm fun_map.simps
(* 3. simplification with *)
thm lambda_prs
(* 4. simplification with *)
thm Quotient_abs_rep Quotient_rel_rep id_simps 
(* 5. Test for refl *)

ML {*
fun clean_tac lthy =
  let
    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 thms1 = defs @ (prs_rules_get lthy) @ @{thms babs_prs all_prs ex_prs}
    val thms2 = @{thms Quotient_abs_rep Quotient_rel_rep} @ (id_simps_get lthy) 
    fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
  in
    EVERY' [simp_tac (simps thms1),
            fun_map_tac lthy,
            lambda_prs_tac lthy,
            simp_tac (simps thms2),
            TRY o rtac refl]
  end
*}

section {* Tactic for genralisation of free variables in a goal *}

ML {*
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)  
*}

section {* 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                *)
(*                                          *)
(* - b is the regularization step           *)
(* - c is the rep/abs injection step        *)
(* - d is the cleaning part                 *)

lemma lifting_procedure:
  assumes a: "A"
  and     b: "A \<longrightarrow> B"
  and     c: "B = C"
  and     d: "C = D"
  shows   "D"
using a b c d
by simp

ML {*
fun lift_match_error ctxt fun_str rtrm qtrm =
let
  val rtrm_str = Syntax.string_of_term ctxt rtrm
  val qtrm_str = Syntax.string_of_term ctxt qtrm
  val msg = [enclose "[" "]" fun_str, "The quotient theorem\n", qtrm_str, 
             "and the lifted theorem\n", rtrm_str, "do not match"]
in
  error (space_implode " " msg)
end
*}

ML {* 
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 = 
        Syntax.check_term ctxt (regularize_trm ctxt rtrm' qtrm')
        handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm
  val inj_goal = 
        Syntax.check_term ctxt (inj_repabs_trm ctxt (reg_goal, qtrm'))
        handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm
in
  Drule.instantiate' []
    [SOME (cterm_of thy rtrm'),
     SOME (cterm_of thy reg_goal),
     SOME (cterm_of thy inj_goal)] @{thm lifting_procedure}
end
*}

ML {*
(* the tactic leaves three subgoals to be proved *)
fun procedure_tac ctxt rthm =
  ObjectLogic.full_atomize_tac
  THEN' gen_frees_tac ctxt
  THEN' CSUBGOAL (fn (goal, i) =>
    let
      val rthm' = atomize_thm rthm
      val rule = procedure_inst ctxt (prop_of rthm') (term_of goal)
      val bare_goal = snd (Thm.dest_comb goal)
      val quot_weak = Drule.instantiate' [] [SOME bare_goal] @{thm QUOT_TRUE_i}
    in
      (rtac rule THEN' RANGE [rtac rthm', K all_tac, rtac quot_weak]) i
    end)
*}

(* automatic proofs *)
ML {*
fun SOLVES' tac = tac THEN_ALL_NEW (K no_tac)

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 xs = RANGE (map WARN xs)
*}

ML {*
fun lift_tac ctxt rthm =
  procedure_tac ctxt rthm
  THEN' RANGE_WARN [(regularize_tac ctxt,     "Regularize proof failed."),
                    (all_inj_repabs_tac ctxt, "Injection proof failed."),
                    (clean_tac ctxt,          "Cleaning proof failed.")]
*}

section {* methods / interface *}
ML {*
fun mk_method1 tac thm ctxt =
  SIMPLE_METHOD (HEADGOAL (tac ctxt thm)) 

fun mk_method2 tac ctxt =
  SIMPLE_METHOD (HEADGOAL (tac ctxt)) 
*}

method_setup lifting =
  {* Attrib.thm >> (mk_method1 lift_tac) *}
  {* Lifting of theorems to quotient types. *}

method_setup lifting_setup =
  {* Attrib.thm >> (mk_method1 procedure_tac) *}
  {* Sets up the three goals for the lifting procedure. *}

method_setup regularize =
  {* Scan.succeed (mk_method2 regularize_tac)  *}
  {* Proves automatically the regularization goals from the lifting procedure. *}

method_setup injection =
  {* Scan.succeed (mk_method2 all_inj_repabs_tac) *}
  {* Proves automatically the rep/abs injection goals from the lifting procedure. *}

method_setup cleaning =
  {* Scan.succeed (mk_method2 clean_tac) *}
  {* Proves automatically the cleaning goals from the lifting procedure. *}

end

