theory QuotMain
imports QuotScript QuotList Prove
uses ("quotient.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 equiv: "EQUIV 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 equiv by (simp add: EQUIV_REFL_SYM_TRANS REFL_def)
  then have "R x (Eps (R x))" by (rule someI)
  then show "R (Eps (R x)) = R x"
    using equiv unfolding EQUIV_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: equiv[simplified EQUIV_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: equiv[simplified EQUIV_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: equiv[simplified EQUIV_def])
done

lemma R_trans:
  assumes ab: "R a b"
  and     bc: "R b c"
  shows "R a c"
proof -
  have tr: "TRANS R" using equiv EQUIV_REFL_SYM_TRANS[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 TRANS_def by blast
qed

lemma R_sym:
  assumes ab: "R a b"
  shows "R b a"
proof -
  have re: "SYM R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp
  then show "R b a" using ab unfolding SYM_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 "REFL R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp
    then show "R (REP a) (REP b)" unfolding REFL_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 *}

use "quotient.ML"

declare [[map list = (map, LIST_REL)]]
declare [[map * = (prod_fun, prod_rel)]]
declare [[map "fun" = (fun_map, FUN_REL)]]

ML {* maps_lookup @{theory} "List.list" *}
ML {* maps_lookup @{theory} "*" *}
ML {* maps_lookup @{theory} "fun" *}

text {* FIXME: auxiliary function *}
ML {*
val no_vars = Thm.rule_attribute (fn context => fn th =>
  let
    val ctxt = Variable.set_body false (Context.proof_of context);
    val ((_, [th']), _) = Variable.import true [th] ctxt;
  in th' end);
*}

section {* lifting of constants *}

ML {*
fun lookup_snd _ [] _ = NONE
  | lookup_snd eq ((value, key)::xs) key' =
      if eq (key', key) then SOME value
      else lookup_snd eq xs key';

fun lookup_qenv qenv qty =
  (case (AList.lookup (op =) qenv qty) of
    SOME rty => SOME (qty, rty)
  | NONE => NONE)
*}

ML {*
(* calculates the aggregate abs and rep functions for a given type; 
   repF is for constants' arguments; absF is for constants;
   function types need to be treated specially, since repF and absF
   change
*)
datatype flag = absF | repF

fun negF absF = repF
  | negF repF = absF

fun get_fun flag qenv lthy ty =
let
  
  fun get_fun_aux s fs_tys =
  let
    val (fs, tys) = split_list fs_tys
    val (otys, ntys) = split_list tys
    val oty = Type (s, otys)
    val nty = Type (s, ntys)
    val ftys = map (op -->) tys
  in
   (case (maps_lookup (ProofContext.theory_of lthy) s) of
      SOME info => (list_comb (Const (#mapfun info, ftys ---> (oty --> nty)), fs), (oty, nty))
    | NONE      => raise ERROR ("no map association for type " ^ s))
  end

  fun get_fun_fun fs_tys =
  let
    val (fs, tys) = split_list fs_tys
    val ([oty1, oty2], [nty1, nty2]) = split_list tys
    val oty = nty1 --> oty2
    val nty = oty1 --> nty2
    val ftys = map (op -->) tys
  in
    (list_comb (Const (@{const_name "fun_map"}, ftys ---> oty --> nty), fs), (oty, nty))
  end

  fun get_const flag (qty, rty) =
  let 
    val thy = ProofContext.theory_of lthy
    val qty_name = Long_Name.base_name (fst (dest_Type qty))
  in
    case flag of
      absF => (Const (Sign.full_bname thy ("ABS_" ^ qty_name), rty --> qty), (rty, qty))
    | repF => (Const (Sign.full_bname thy ("REP_" ^ qty_name), qty --> rty), (qty, rty))
  end

  fun mk_identity ty = Abs ("", ty, Bound 0)

in
  if (AList.defined (op =) qenv ty)
  then (get_const flag (the (lookup_qenv qenv ty)))
  else (case ty of
          TFree _ => (mk_identity ty, (ty, ty))
        | Type (_, []) => (mk_identity ty, (ty, ty)) 
        | Type ("fun" , [ty1, ty2]) => 
                 get_fun_fun [get_fun (negF flag) qenv lthy ty1, get_fun flag qenv lthy ty2]
        | Type (s, tys) => get_fun_aux s (map (get_fun flag qenv lthy) tys)
        | _ => raise ERROR ("no type variables")
       )
end
*}


text {* produces the definition for a lifted constant *}

ML {*
fun get_const_def nconst otrm qenv lthy =
let
  val ty = fastype_of nconst
  val (arg_tys, res_ty) = strip_type ty

  val rep_fns = map (fst o get_fun repF qenv lthy) arg_tys
  val abs_fn  = (fst o get_fun absF qenv lthy) res_ty

  fun mk_fun_map (t1,t2) = Const (@{const_name "fun_map"}, dummyT) $ t1 $ t2

  val fns = Library.foldr mk_fun_map (rep_fns, abs_fn)
            |> Syntax.check_term lthy
in
  fns $ otrm
end
*}


ML {*
fun exchange_ty qenv ty =
  case (lookup_snd (op =) qenv ty) of
    SOME qty => qty
  | NONE =>
    (case ty of
       Type (s, tys) => Type (s, map (exchange_ty qenv) tys)
      | _ => ty
    )
*}

ML {* 
fun ppair lthy (ty1, ty2) =
  "(" ^ (Syntax.string_of_typ lthy ty1) ^ "," ^ (Syntax.string_of_typ lthy ty2) ^ ")"
*}

ML {*
fun print_env qenv lthy =
  map (ppair lthy) qenv
  |> commas
  |> tracing
*}

ML {*
fun make_const_def nconst_bname otrm mx qenv lthy =
let
  val otrm_ty = fastype_of otrm
  val nconst_ty = exchange_ty qenv otrm_ty
  val nconst = Const (Binding.name_of nconst_bname, nconst_ty)
  val def_trm = get_const_def nconst otrm qenv lthy

  val _ = print_env qenv lthy
  val _ = Syntax.string_of_typ lthy otrm_ty |> tracing
  val _ = Syntax.string_of_typ lthy nconst_ty |> tracing
  val _ = Syntax.string_of_term lthy def_trm |> tracing
in
  define (nconst_bname, mx, def_trm) lthy
end
*}

ML {*
fun build_qenv lthy qtys = 
let
  val qenv = map (fn {qtyp, rtyp, ...} => (qtyp, rtyp)) (quotdata_lookup lthy)
  val tsig = Sign.tsig_of (ProofContext.theory_of lthy)
  
  fun find_assoc ((qty', rty')::rest) qty =
        let 
          val inst = Type.typ_match tsig (qty', qty) Vartab.empty
        in
           (Envir.norm_type inst qty, Envir.norm_type inst rty')
        end
    | find_assoc [] qty =
        let 
          val qtystr =  quote (Syntax.string_of_typ lthy qty)
        in
          error (implode ["Quotient type ", qtystr, " does not exists"])
        end
in
  map (find_assoc qenv) qtys
end
*}

ML {*
val qd_parser = 
  (Args.parens (OuterParse.$$$ "for" |-- (Scan.repeat OuterParse.typ))) --
    (SpecParse.constdecl -- (SpecParse.opt_thm_name ":" -- OuterParse.prop))
*}

ML {*
fun parse_qd_spec (qtystrs, ((bind, tystr, mx), (attr__, propstr))) lthy = 
let
  val qtys = map (Syntax.check_typ lthy o Syntax.parse_typ lthy) qtystrs
  val qenv = build_qenv lthy qtys
  val qty = Syntax.parse_typ lthy (the tystr) |> Syntax.check_typ lthy
  val prop = Syntax.parse_prop lthy propstr |> Syntax.check_prop lthy
  val (lhs, rhs) = Logic.dest_equals prop
in
  make_const_def bind rhs mx qenv lthy |> snd
end
*}

ML {*
val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants"
  OuterKeyword.thy_decl (qd_parser >> parse_qd_spec)
*}

(* ML {* show_all_types := true *} *)

section {* ATOMIZE *}

text {*
  Unabs_def converts a definition given as

    c \<equiv> %x. %y. f x y

  to a theorem of the form

    c x y \<equiv> f x y

  This function is needed to rewrite the right-hand
  side to the left-hand side.
*}

ML {*
fun unabs_def ctxt def =
let
  val (lhs, rhs) = Thm.dest_equals (cprop_of def)
  val xs = strip_abs_vars (term_of rhs)
  val (_, ctxt') = Variable.add_fixes (map fst xs) ctxt

  val thy = ProofContext.theory_of ctxt'
  val cxs = map (cterm_of thy o Free) xs
  val new_lhs = Drule.list_comb (lhs, cxs)

  fun get_conv [] = Conv.rewr_conv def
    | get_conv (x::xs) = Conv.fun_conv (get_conv xs)
in
  get_conv xs new_lhs |>
  singleton (ProofContext.export ctxt' ctxt)
end
*}

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 Pure.equal_elim_rule1} OF [thm'', thm']
end
*}

ML {* atomize_thm @{thm list.induct} *}

section {* REGULARIZE *}

text {* tyRel takes a type and builds a relation that a quantifier over this
  type needs to respect. *}
ML {*
fun matches (ty1, ty2) =
  Type.raw_instance (ty1, Logic.varifyT ty2);

fun tyRel ty rty rel lthy =
  if matches (rty, ty)
  then rel
  else (case ty of
          Type (s, tys) =>
            let
              val tys_rel = map (fn ty => ty --> ty --> @{typ bool}) tys;
              val ty_out = ty --> ty --> @{typ bool};
              val tys_out = tys_rel ---> ty_out;
            in
            (case (maps_lookup (ProofContext.theory_of lthy) s) of
               SOME (info) => list_comb (Const (#relfun info, tys_out), map (fn ty => tyRel ty rty rel lthy) tys)
             | NONE  => HOLogic.eq_const ty
            )
            end
        | _ => HOLogic.eq_const ty)
*}

definition
  Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
where
  "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)"
(* TODO: Consider defining it with an "if"; sth like:
   Babs p m = \<lambda>x. if x \<in> p then m x else undefined
*)

ML {*
fun needs_lift (rty as Type (rty_s, _)) ty =
  case ty of
    Type (s, tys) =>
      (s = rty_s) orelse (exists (needs_lift rty) tys)
  | _ => false

*}

ML {*
fun mk_babs ty ty' = Const (@{const_name "Babs"}, [ty' --> @{typ bool}, ty] ---> ty)
fun mk_ball ty = Const (@{const_name "Ball"}, [ty, ty] ---> @{typ bool})
fun mk_bex ty = Const (@{const_name "Bex"}, [ty, ty] ---> @{typ bool})
fun mk_resp ty = Const (@{const_name Respects}, [[ty, ty] ---> @{typ bool}, ty] ---> @{typ bool})
*}

(* applies f to the subterm of an abstractions, otherwise to the given term *)
ML {*
fun apply_subt f trm =
  case trm of
    Abs (x, T, t) => 
       let 
         val (x', t') = Term.dest_abs (x, T, t)
       in
         Term.absfree (x', T, f t') 
       end
  | _ => f trm
*}

(* FIXME: if there are more than one quotient, then you have to look up the relation *)
ML {*
fun my_reg lthy rel rty trm =
  case trm of
    Abs (x, T, t) =>
       if (needs_lift rty T) then
         let
            val rrel = tyRel T rty rel lthy
         in
           (mk_babs (fastype_of trm) T) $ (mk_resp T $ rrel) $ (apply_subt (my_reg lthy rel rty) trm)
         end
       else
         Abs(x, T, (apply_subt (my_reg lthy rel rty) t))
  | Const (@{const_name "All"}, ty) $ (t as Abs (x, T, _)) =>
       let
          val ty1 = domain_type ty
          val ty2 = domain_type ty1
          val rrel = tyRel T rty rel lthy
       in
         if (needs_lift rty T) then
           (mk_ball ty1) $ (mk_resp ty2 $ rrel) $ (apply_subt (my_reg lthy rel rty) t)
         else
           Const (@{const_name "All"}, ty) $ apply_subt (my_reg lthy rel rty) t
       end
  | Const (@{const_name "Ex"}, ty) $ (t as Abs (x, T, _)) =>
       let
          val ty1 = domain_type ty
          val ty2 = domain_type ty1
          val rrel = tyRel T rty rel lthy
       in
         if (needs_lift rty T) then
           (mk_bex ty1) $ (mk_resp ty2 $ rrel) $ (apply_subt (my_reg lthy rel rty) t)
         else
           Const (@{const_name "Ex"}, ty) $ apply_subt (my_reg lthy rel rty) t
       end
  | Const (@{const_name "op ="}, ty) $ t =>
      if needs_lift rty (fastype_of t) then
        (tyRel (fastype_of t) rty rel lthy) $ t
      else Const (@{const_name "op ="}, ty) $ (my_reg lthy rel rty t)
  | t1 $ t2 => (my_reg lthy rel rty t1) $ (my_reg lthy rel rty t2)
  | _ => trm
*}

text {* Assumes that the given theorem is atomized *}
ML {*
  fun build_regularize_goal thm rty rel lthy =
     Logic.mk_implies
       ((prop_of thm),
       (my_reg lthy rel rty (prop_of thm)))
*}

lemma universal_twice: "(\<And>x. (P x \<longrightarrow> Q x)) \<Longrightarrow> ((\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x))"
apply (auto)
done

lemma implication_twice: "(c \<longrightarrow> a) \<Longrightarrow> (a \<Longrightarrow> b \<longrightarrow> d) \<Longrightarrow> (a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)"
apply (auto)
done

ML {*
fun regularize thm rty rel rel_eqv rel_refl lthy =
  let
    val g = build_regularize_goal thm rty rel lthy;
    fun tac ctxt =
      (ObjectLogic.full_atomize_tac) THEN'
     REPEAT_ALL_NEW (FIRST' [
      rtac rel_refl,
      atac,
      rtac @{thm universal_twice},
      (rtac @{thm impI} THEN' atac),
      rtac @{thm implication_twice},
      EqSubst.eqsubst_tac ctxt [0]
        [(@{thm equiv_res_forall} OF [rel_eqv]),
         (@{thm equiv_res_exists} OF [rel_eqv])],
      (rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl),
      (rtac @{thm RIGHT_RES_FORALL_REGULAR})
     ]);
    val cthm = Goal.prove lthy [] [] g (fn x => tac (#context x) 1);
  in
    cthm OF [thm]
  end
*}

section {* RepAbs injection *}

(* Needed to have a meta-equality *)
lemma id_def_sym: "(\<lambda>x. x) \<equiv> id"
by (simp add: id_def)

ML {*
fun old_exchange_ty rty qty ty =
  if ty = rty
  then qty
  else
     (case ty of
        Type (s, tys) => Type (s, map (old_exchange_ty rty qty) tys)
      | _ => ty
     )
*}

ML {*
fun old_get_fun flag rty qty lthy ty =
  get_fun flag [(qty, rty)] lthy ty 

fun old_make_const_def nconst_bname otrm mx rty qty lthy =
  make_const_def nconst_bname otrm mx [(qty, rty)] lthy
*}

text {* Does the same as 'subst' in a given prop or theorem *}
ML {*
fun eqsubst_prop ctxt thms t =
  let
    val goalstate = Goal.init (cterm_of (ProofContext.theory_of ctxt) t)
    val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of
      NONE => error "eqsubst_prop"
    | SOME th => cprem_of th 1
  in term_of a' end
*}

ML {*
  fun repeat_eqsubst_prop ctxt thms t =
    repeat_eqsubst_prop ctxt thms (eqsubst_prop ctxt thms t)
    handle _ => t
*}


ML {*
fun eqsubst_thm ctxt thms thm =
  let
    val goalstate = Goal.init (Thm.cprop_of thm)
    val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of
      NONE => error "eqsubst_thm"
    | SOME th => cprem_of th 1
    val tac = (EqSubst.eqsubst_tac ctxt [0] thms 1) THEN simp_tac HOL_ss 1
    val cgoal = cterm_of (ProofContext.theory_of ctxt) (Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a'))
    val rt = Toplevel.program (fn () => Goal.prove_internal [] cgoal (fn _ => tac));
  in
    @{thm Pure.equal_elim_rule1} OF [rt,thm]
  end
*}

ML {*
  fun repeat_eqsubst_thm ctxt thms thm =
    repeat_eqsubst_thm ctxt thms (eqsubst_thm ctxt thms thm)
    handle _ => thm
*}

ML {*
fun build_repabs_term lthy thm constructors rty qty =
  let
    fun mk_rep tm =
      let
        val ty = old_exchange_ty rty qty (fastype_of tm)
      in fst (old_get_fun repF rty qty lthy ty) $ tm end

    fun mk_abs tm =
      let
        val ty = old_exchange_ty rty qty (fastype_of tm) in
      fst (old_get_fun absF rty qty lthy ty) $ tm end

    fun is_constructor (Const (x, _)) = member (op =) constructors x
      | is_constructor _ = false;

    fun build_aux lthy tm =
      case tm of
      Abs (a as (_, vty, _)) =>
      let
        val (vs, t) = Term.dest_abs a;
        val v = Free(vs, vty);
        val t' = lambda v (build_aux lthy t)
      in
      if (not (needs_lift rty (fastype_of tm))) then t'
      else mk_rep (mk_abs (
        if not (needs_lift rty vty) then t'
        else
          let
            val v' = mk_rep (mk_abs v);
            val t1 = Envir.beta_norm (t' $ v')
          in
            lambda v t1
          end
      ))
      end
    | x =>
      let
        val (opp, tms0) = Term.strip_comb tm
        val tms = map (build_aux lthy) tms0
        val ty = fastype_of tm
      in
        if (((fst (Term.dest_Const opp)) = @{const_name Respects}) handle _ => false)
          then (list_comb (opp, (hd tms0) :: (tl tms)))
      else if (is_constructor opp andalso needs_lift rty ty) then
          mk_rep (mk_abs (list_comb (opp,tms)))
        else if ((Term.is_Free opp) andalso (length tms > 0) andalso (needs_lift rty ty)) then
          mk_rep(mk_abs(list_comb(opp,tms)))
        else if tms = [] then opp
        else list_comb(opp, tms)
      end
  in
    repeat_eqsubst_prop lthy @{thms id_def_sym}
      (build_aux lthy (Thm.prop_of thm))
  end
*}

text {* Assumes that it is given a regularized theorem *}
ML {*
fun build_repabs_goal ctxt thm cons rty qty =
  Logic.mk_equals ((Thm.prop_of thm), (build_repabs_term ctxt thm cons rty qty))
*}

ML {*
fun instantiate_tac thm = Subgoal.FOCUS (fn {concl, ...} =>
let
  val pat = Drule.strip_imp_concl (cprop_of thm)
  val insts = Thm.match (pat, concl)
in
  rtac (Drule.instantiate insts thm) 1
end
handle _ => no_tac
)
*}

ML {*
fun res_forall_rsp_tac ctxt =
  (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
  THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
  THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN'
  (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
*}

ML {*
fun res_exists_rsp_tac ctxt =
  (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
  THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
  THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN'
  (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
*}


ML {*
fun quotient_tac quot_thm =
  REPEAT_ALL_NEW (FIRST' [
    rtac @{thm FUN_QUOTIENT},
    rtac quot_thm,
    rtac @{thm IDENTITY_QUOTIENT}
  ])
*}

ML {*
fun LAMBDA_RES_TAC ctxt i st =
  (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of
    (_ $ (_ $ (Abs(_,_,_))$(Abs(_,_,_)))) =>
      (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
      (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
  | _ => fn _ => no_tac) i st
*}

ML {*
fun WEAK_LAMBDA_RES_TAC ctxt i st =
  (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of
    (_ $ (_ $ _$(Abs(_,_,_)))) =>
      (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
      (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
  | (_ $ (_ $ (Abs(_,_,_))$_)) =>
      (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
      (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
  | _ => fn _ => no_tac) i st
*}

ML {*
fun APPLY_RSP_TAC rty = Subgoal.FOCUS (fn {concl, ...} =>
  let
    val (_ $ (R $ (f $ _) $ (_ $ _))) = term_of concl;
    val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP});
    val insts = Thm.match (pat, concl)
in
  if needs_lift rty (type_of f) then
    rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1
  else no_tac
end
handle _ => no_tac)
*}

ML {*
fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms =
  (FIRST' [
    rtac @{thm FUN_QUOTIENT},
    rtac quot_thm,
    rtac @{thm IDENTITY_QUOTIENT},
    rtac trans_thm,
    LAMBDA_RES_TAC ctxt,
    res_forall_rsp_tac ctxt,
    res_exists_rsp_tac ctxt,
    (
     (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps rsp_thms))
     THEN_ALL_NEW (fn _ => no_tac)
    ),
    (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])),
    rtac refl,
(*    rtac @{thm arg_cong2[of _ _ _ _ "op ="]},*)
    (APPLY_RSP_TAC rty ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])),
    Cong_Tac.cong_tac @{thm cong},
    rtac @{thm ext},
    rtac reflex_thm,
    atac,
    (
     (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
     THEN_ALL_NEW (fn _ => no_tac)
    ),
    WEAK_LAMBDA_RES_TAC ctxt
    ])
*}

ML {*
fun repabs lthy thm constructors rty qty quot_thm reflex_thm trans_thm rsp_thms =
  let
    val rt = build_repabs_term lthy thm constructors rty qty;
    val rg = Logic.mk_equals ((Thm.prop_of thm), rt);
    fun tac ctxt = (ObjectLogic.full_atomize_tac) THEN'
      (REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms));
    val cthm = Goal.prove lthy [] [] rg (fn x => tac (#context x) 1);
  in
    @{thm Pure.equal_elim_rule1} OF [cthm, thm]
  end
*}

section {* Cleaning the goal *}

lemma prod_fun_id: "prod_fun id id = id"
  apply (simp add: prod_fun_def)
done
lemma map_id: "map id x = x"
  apply (induct x)
  apply (simp_all add: map.simps)
done

text {* expects atomized definition *}
ML {*
  fun add_lower_defs_aux ctxt thm =
    let
      val e1 = @{thm fun_cong} OF [thm];
      val f = eqsubst_thm ctxt @{thms fun_map.simps} e1;
      val g = MetaSimplifier.rewrite_rule @{thms id_def_sym} f;
      val h = repeat_eqsubst_thm ctxt @{thms FUN_MAP_I id_apply prod_fun_id map_id} g
    in
      thm :: (add_lower_defs_aux ctxt h)
    end
    handle _ => [thm]
*}

ML {*
fun add_lower_defs ctxt defs =
  let
    val defs_pre_sym = map symmetric defs
    val defs_atom = map atomize_thm defs_pre_sym
    val defs_all = flat (map (add_lower_defs_aux ctxt) defs_atom)
  in
    map Thm.varifyT defs_all
  end
*}

ML {*
  fun findabs_all rty tm =
    case tm of
      Abs(_, T, b) =>
        let
          val b' = subst_bound ((Free ("x", T)), b);
          val tys = findabs_all rty b'
          val ty = fastype_of tm
        in if needs_lift rty ty then (ty :: tys) else tys
        end
    | f $ a => (findabs_all rty f) @ (findabs_all rty a)
    | _ => [];
  fun findabs rty tm = distinct (op =) (findabs_all rty tm)
*}


ML {*
  fun findaps_all rty tm =
    case tm of
      Abs(_, T, b) =>
        findaps_all rty (subst_bound ((Free ("x", T)), b))
    | (f $ a) => (findaps_all rty f @ findaps_all rty a)
    | Free (_, (T as (Type ("fun", (_ :: _))))) => (if needs_lift rty T then [T] else [])
    | _ => [];
  fun findaps rty tm = distinct (op =) (findaps_all rty tm)
*}

ML {*
fun make_simp_prs_thm lthy quot_thm thm typ =
  let
    val (_, [lty, rty]) = dest_Type typ;
    val thy = ProofContext.theory_of lthy;
    val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty)
    val inst = [SOME lcty, NONE, SOME rcty];
    val lpi = Drule.instantiate' inst [] thm;
    val tac =
      (compose_tac (false, lpi, 2)) THEN_ALL_NEW
      (quotient_tac quot_thm);
    val t = Goal.prove lthy [] [] (concl_of lpi) (fn _ => tac 1);
  in
    MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] t
  end
*}

ML {*
  fun simp_allex_prs lthy quot thm =
    let
      val rwf = @{thm FORALL_PRS} OF [quot];
      val rwfs = @{thm "HOL.sym"} OF [rwf];
      val rwe = @{thm EXISTS_PRS} OF [quot];
      val rwes = @{thm "HOL.sym"} OF [rwe]
    in
      (simp_allex_prs lthy quot (eqsubst_thm lthy [rwfs, rwes] thm))
    end
    handle _ => thm
*}

ML {*
fun lookup_quot_data lthy qty =
  let
    val SOME quotdata = find_first (fn x => matches ((#qtyp x), qty)) (quotdata_lookup lthy)
    val rty = Logic.unvarifyT (#rtyp quotdata)
    val rel = #rel quotdata
    val rel_eqv = #equiv_thm quotdata
    val rel_refl_pre = @{thm EQUIV_REFL} OF [rel_eqv]
    val rel_refl = @{thm spec} OF [MetaSimplifier.rewrite_rule [@{thm REFL_def}] rel_refl_pre]
  in
    (rty, rel, rel_refl, rel_eqv)
  end
*}

ML {*
fun lookup_quot_thms lthy qty_name =
  let
    val thy = ProofContext.theory_of lthy;
    val trans2 = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".R_trans2")
    val reps_same = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".REPS_same")
    val quot = PureThy.get_thm thy ("QUOTIENT_" ^ qty_name)
  in
    (trans2, reps_same, quot)
  end
*}

ML {*
fun lookup_quot_consts defs =
  let
    fun dest_term (a $ b) = (a, b);
    val def_terms = map (snd o Logic.dest_equals o concl_of) defs;
  in
    map (fst o dest_Const o snd o dest_term) def_terms
  end
*}

ML {*
fun lift_thm lthy qty qty_name rsp_thms defs t = let
  val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data lthy qty;
  val (trans2, reps_same, quot) = lookup_quot_thms lthy qty_name;
  val consts = lookup_quot_consts defs;
  val t_a = atomize_thm t;
  val t_r = regularize t_a rty rel rel_eqv rel_refl lthy;
  val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms;
  val abs = findabs rty (prop_of t_a);
  val aps = findaps rty (prop_of t_a);
  val app_prs_thms = map (make_simp_prs_thm lthy quot @{thm APP_PRS}) aps;
  val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs;
  val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_t;
  val t_a = simp_allex_prs lthy quot t_l;
  val defs_sym = add_lower_defs lthy defs;
  val t_d = repeat_eqsubst_thm lthy defs_sym t_a;
  val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d;
in
  ObjectLogic.rulify t_r
end
*}


end