ML {*

fun repeat_eqsubst_thm ctxt thms thm =

  repeat_eqsubst_thm ctxt thms (eqsubst_thm ctxt thms thm)

  handle _ => thm

*}

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

*}

text {* tyRel takes a type and builds a relation that a quantifier over this

  type needs to respect. *}

ML {*

fun tyRel ty rty rel lthy =

  if Sign.typ_instance (ProofContext.theory_of lthy) (ty, rty)

  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)

*}

(* 

ML {* cterm_of @{theory} 

  (tyRel @{typ "'a \<Rightarrow> 'a list \<Rightarrow> 't \<Rightarrow> 't"} (Logic.varifyT @{typ "'a list"}) 

         @{term "f::('a list \<Rightarrow> 'a list \<Rightarrow> bool)"} @{context}) 

*} 

*)

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   (* FIXME: t should be regularised too *)

      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

*}

(* For polymorphic types we need to find the type of the Relation term. *)

(* TODO: we assume that the relation is a Constant. Is this always true? *)

ML {*

fun my_reg_inst lthy rel rty trm =

  case rel of

    Const (n, _) => Syntax.check_term lthy

      (my_reg lthy (Const (n, dummyT)) (Logic.varifyT rty) trm)

*}

(*

ML {*

  val r = Free ("R", dummyT);

  val t = (my_reg_inst @{context} r @{typ "'a list"} @{term "\<forall>(x::'b list). P x"});

  val t2 = Syntax.check_term @{context} t;

  cterm_of @{theory} t2

*}

*)

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_inst lthy rel rty (prop_of thm)))

*}

ML {*

fun regularize thm rty rel rel_eqv rel_refl lthy =

  let

    val goal = 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])],

        (* For a = b \<longrightarrow> a \<approx> b *)

        (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl),

        (rtac @{thm RIGHT_RES_FORALL_REGULAR})

      ]);

    val cthm = Goal.prove lthy [] [] goal

      (fn {context, ...} => tac context 1);

  in

    cthm OF [thm]

  end

*}

(*consts Rl :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"

axioms Rl_eq: "EQUIV Rl"

quotient ql = "'a list" / "Rl"

  by (rule Rl_eq)

ML {*

  ctyp_of @{theory} (exchange_ty @{context} (Logic.varifyT @{typ "'a list"}) (Logic.varifyT @{typ "'a ql"}) @{typ "nat list \<Rightarrow> (nat \<times> nat) list"});

  ctyp_of @{theory} (exchange_ty @{context} (Logic.varifyT @{typ "nat \<times> nat"}) (Logic.varifyT @{typ "int"}) @{typ "nat list \<Rightarrow> (nat \<times> nat) list"})

*}

*)

ML {*

(* returns all subterms where two types differ *)

fun diff (T, S) Ds =

  case (T, S) of

    (TVar v, TVar u) => if v = u then Ds else (T, S)::Ds 

  | (TFree x, TFree y) => if x = y then Ds else (T, S)::Ds

  | (Type (a, Ts), Type (b, Us)) => 

      if a = b then diffs (Ts, Us) Ds else (T, S)::Ds

  | _ => (T, S)::Ds

and diffs (T::Ts, U::Us) Ds = diffs (Ts, Us) (diff (T, U) Ds)

  | diffs ([], []) Ds = Ds

  | diffs _ _ = error "Unequal length of type arguments"

*}

ML {*

fun build_repabs_term lthy thm consts rty qty =

  let

    (* TODO: The rty and qty stored in the quotient_info should

       be varified, so this will soon not be needed *)

    val rty = Logic.varifyT rty;

    val qty = Logic.varifyT qty;

  fun mk_abs tm =

    let

      val ty = fastype_of tm

    in Syntax.check_term lthy ((get_fun_OLD absF (rty, qty) lthy ty) $ tm) end

  fun mk_repabs tm =

    let

      val ty = fastype_of tm

    in Syntax.check_term lthy ((get_fun_OLD repF (rty, qty) lthy ty) $ (mk_abs tm)) end

    fun is_lifted_const (Const (x, _)) = member (op =) consts x

      | is_lifted_const _ = 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_repabs (

              if not (needs_lift rty vty) then t'

              else

                let

                  val v' = mk_repabs v;

                  (* TODO: I believe 'beta' is not needed any more *)

                  val t1 = (* Envir.beta_norm *) (t' $ v')

                in

                  lambda v t1

                end)

          end

      | x =>

        case Term.strip_comb tm of

          (Const(@{const_name Respects}, _), _) => tm

        | (opp, tms0) =>

          let

            val tms = map (build_aux lthy) tms0

            val ty = fastype_of tm

          in

            if (is_lifted_const opp andalso needs_lift rty ty) then

            mk_repabs (list_comb (opp, tms))

            else if ((Term.is_Free opp) andalso (length tms > 0) andalso (needs_lift rty ty)) then

              mk_repabs (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 {* Builds provable goals for regularized theorems *}

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 repabs lthy thm consts rty qty quot_thm reflex_thm trans_thm rsp_thms =

  let

    val rt = build_repabs_term lthy thm consts 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

*}

(* TODO: Check if it behaves properly with varifyed rty *)

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)

*}

(* Currently useful only for LAMBDA_PRS *)

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 gc = Drule.strip_imp_concl (cprop_of lpi);

    val t = Goal.prove_internal [] gc (fn _ => tac 1)

  in

    MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] t

  end

*}

ML {*

fun findallex_all rty qty tm =

  case tm of

    Const (@{const_name All}, T) $ (s as (Abs(_, _, b))) =>

      let

        val (tya, tye) = findallex_all rty qty s

      in if needs_lift rty T then

        ((T :: tya), tye)

      else (tya, tye) end

  | Const (@{const_name Ex}, T) $ (s as (Abs(_, _, b))) =>

      let

        val (tya, tye) = findallex_all rty qty s

      in if needs_lift rty T then

        (tya, (T :: tye))

      else (tya, tye) end

  | Abs(_, T, b) =>

      findallex_all rty qty (subst_bound ((Free ("x", T)), b))

  | f $ a =>

      let

        val (a1, e1) = findallex_all rty qty f;

        val (a2, e2) = findallex_all rty qty a;

      in (a1 @ a2, e1 @ e2) end

  | _ => ([], []);

*}

ML {*

fun findallex lthy rty qty tm =

  let

    val (a, e) = findallex_all rty qty tm;

    val (ad, ed) = (map domain_type a, map domain_type e);

    val (au, eu) = (distinct (op =) ad, distinct (op =) ed);

    val (rty, qty) = (Logic.varifyT rty, Logic.varifyT qty)

  in

    (map (exchange_ty lthy rty qty) au, map (exchange_ty lthy rty qty) eu)

  end

*}

ML {*

fun make_allex_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 = [NONE, SOME lcty];

    val lpi = Drule.instantiate' inst [] thm;

    val tac =

      (compose_tac (false, lpi, 1)) THEN_ALL_NEW

      (quotient_tac quot_thm);

    val gc = Drule.strip_imp_concl (cprop_of lpi);

    val t = Goal.prove_internal [] gc (fn _ => tac 1)

    val t_noid = MetaSimplifier.rewrite_rule

      [@{thm eq_reflection} OF @{thms id_apply}] t;

    val t_sym = @{thm "HOL.sym"} OF [t_noid];

    val t_eq = @{thm "eq_reflection"} OF [t_sym]

  in

    t_eq

  end

*}

ML {*

fun lift_thm lthy qty qty_name rsp_thms defs rthm = 

let

  val _ = tracing ("raw theorem:\n" ^ Syntax.string_of_term lthy (prop_of rthm))

  val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data lthy qty;

  val (trans2, reps_same, absrep, quot) = lookup_quot_thms lthy qty_name;

  val consts = lookup_quot_consts defs;

  val t_a = atomize_thm rthm;

  val _ = tracing ("raw atomized theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_a))

  val t_r = regularize t_a rty rel rel_eqv rel_refl lthy;

  val _ = tracing ("regularised theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_r))

  val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms;

  val _ = tracing ("rep/abs injected theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_t))

  val (alls, exs) = findallex lthy rty qty (prop_of t_a);

  val allthms = map (make_allex_prs_thm lthy quot @{thm FORALL_PRS}) alls

  val exthms = map (make_allex_prs_thm lthy quot @{thm EXISTS_PRS}) exs

  val t_a = MetaSimplifier.rewrite_rule (allthms @ exthms) t_t

  val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_a))

  val abs = findabs rty (prop_of t_a);

  val aps = findaps rty (prop_of t_a);

  val app_prs_thms = map (applic_prs lthy rty qty absrep) 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_a;

  val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_l))

  val defs_sym = flat (map (add_lower_defs lthy) defs);

  val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym;

  val t_id = simp_ids lthy t_l;

  val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_id))

  val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_id;

  val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_d0))

  val t_d = repeat_eqsubst_thm lthy defs_sym t_d0;

  val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_d))

  val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d;

  val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_r))

  val t_rv = ObjectLogic.rulify t_r

  val _ = tracing ("lifted theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_rv))

in

  Thm.varifyT t_rv

end

*}

ML {*

fun lift_thm_note qty qty_name rsp_thms defs thm name lthy =

  let

    val lifted_thm = lift_thm lthy qty qty_name rsp_thms defs thm;

    val (_, lthy2) = note (name, lifted_thm) lthy;

  in

    lthy2

  end

*}

ML {*

fun regularize_goal lthy thm rel_eqv rel_refl qtrm =

  let

    val reg_trm = mk_REGULARIZE_goal lthy (prop_of thm) qtrm;

    fun tac lthy = regularize_tac lthy rel_eqv rel_refl;

    val cthm = Goal.prove lthy [] [] reg_trm

      (fn {context, ...} => tac context 1);

  in

    cthm OF [thm]

  end

*}

ML {*

fun repabs_goal lthy thm rty quot_thm reflex_thm trans_thm rsp_thms qtrm =

  let

    val rg = Syntax.check_term lthy (mk_inj_REPABS_goal lthy ((prop_of thm), qtrm));

    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

*}

ML {*

fun atomize_goal thy gl =

  let

    val vars = map Free (Term.add_frees gl []);

    val all = if fastype_of gl = @{typ bool} then HOLogic.all_const else Term.all;

    fun lambda_all (var as Free(_, T)) trm = (all T) $ lambda var trm;

    val glv = fold lambda_all vars gl

    val gla = (term_of o snd o Thm.dest_equals o cprop_of) (ObjectLogic.atomize (cterm_of thy glv))

    val glf = Type.legacy_freeze gla

  in

    if fastype_of gl = @{typ bool} then @{term Trueprop} $ glf else glf

  end

*}

ML {* atomize_goal @{theory} @{term "x memb [] = False"} *}

ML {* atomize_goal @{theory} @{term "x = xa ? a # x = a # xa"} *}