diff -r fa810f01f7b5 -r 25c4223635f4 Attic/UnusedQuotMain.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/UnusedQuotMain.thy	Tue Jan 26 20:12:41 2010 +0100
@@ -0,0 +1,687 @@
+(* Code for getting the goal *)
+apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *})
+ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
+
+
+section {*  Infrastructure about definitions *}
+
+(* Does the same as 'subst' in a given theorem *)
+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 goal = Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a');
+    val cgoal = cterm_of (ProofContext.theory_of ctxt) goal
+    val rt = Goal.prove_internal [] cgoal (fn _ => tac);
+  in
+    @{thm equal_elim_rule1} OF [rt, thm]
+  end
+*}
+
+(* expects atomized definitions *)
+ML {*
+fun add_lower_defs_aux lthy thm =
+  let
+    val e1 = @{thm fun_cong} OF [thm];
+    val f = eqsubst_thm lthy @{thms fun_map.simps} e1;
+    val g = simp_ids f
+  in
+    (simp_ids thm) :: (add_lower_defs_aux lthy g)
+  end
+  handle _ => [simp_ids thm]
+*}
+
+ML {*
+fun add_lower_defs lthy def =
+  let
+    val def_pre_sym = symmetric def
+    val def_atom = atomize_thm def_pre_sym
+    val defs_all = add_lower_defs_aux lthy def_atom
+  in
+    map Thm.varifyT defs_all
+  end
+*}
+
+
+
+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"} *}
+
+
+ML {*
+fun applic_prs lthy absrep (rty, qty) =
+  let
+    fun mk_rep (T, T') tm = (Quotient_Def.get_fun repF lthy (T, T')) $ tm;
+    fun mk_abs (T, T') tm = (Quotient_Def.get_fun absF lthy (T, T')) $ tm;
+    val (raty, rgty) = Term.strip_type rty;
+    val (qaty, qgty) = Term.strip_type qty;
+    val vs = map (fn _ => "x") qaty;
+    val ((fname :: vfs), lthy') = Variable.variant_fixes ("f" :: vs) lthy;
+    val f = Free (fname, qaty ---> qgty);
+    val args = map Free (vfs ~~ qaty);
+    val rhs = list_comb(f, args);
+    val largs = map2 mk_rep (raty ~~ qaty) args;
+    val lhs = mk_abs (rgty, qgty) (list_comb((mk_rep (raty ---> rgty, qaty ---> qgty) f), largs));
+    val llhs = Syntax.check_term lthy lhs;
+    val eq = Logic.mk_equals (llhs, rhs);
+    val ceq = cterm_of (ProofContext.theory_of lthy') eq;
+    val sctxt = HOL_ss addsimps (@{thms fun_map.simps id_simps} @ absrep);
+    val t = Goal.prove_internal [] ceq (fn _ => simp_tac sctxt 1)
+    val t_id = MetaSimplifier.rewrite_rule @{thms id_simps} t;
+  in
+    singleton (ProofContext.export lthy' lthy) t_id
+  end
+*}
+
+ML {*
+fun find_aps_all rtm qtm =
+  case (rtm, qtm) of
+    (Abs(_, T1, s1), Abs(_, T2, s2)) =>
+      find_aps_all (subst_bound ((Free ("x", T1)), s1)) (subst_bound ((Free ("x", T2)), s2))
+  | (((f1 as (Free (_, T1))) $ a1), ((f2 as (Free (_, T2))) $ a2)) =>
+      let
+        val sub = (find_aps_all f1 f2) @ (find_aps_all a1 a2)
+      in
+        if T1 = T2 then sub else (T1, T2) :: sub
+      end
+  | ((f1 $ a1), (f2 $ a2)) => (find_aps_all f1 f2) @ (find_aps_all a1 a2)
+  | _ => [];
+
+fun find_aps rtm qtm = distinct (op =) (find_aps_all rtm qtm)
+*}
+
+
+
+ML {*
+fun lift_thm_goal lthy qty qty_name rsp_thms defs rthm goal =
+let
+  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 t_a = atomize_thm rthm;
+  val goal_a = atomize_goal (ProofContext.theory_of lthy) goal;
+  val t_r = regularize_goal lthy t_a rel_eqv rel_refl goal_a;
+  val t_t = repabs_goal lthy t_r rty quot rel_refl trans2 rsp_thms goal_a;
+  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 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 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 t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_id;
+  val t_d = repeat_eqsubst_thm lthy defs_sym t_d0;
+  val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d;
+  val t_rv = ObjectLogic.rulify t_r
+in
+  Thm.varifyT t_rv
+end
+*}
+
+ML {*
+fun lift_thm_goal_note lthy qty qty_name rsp_thms defs thm name goal =
+  let
+    val lifted_thm = lift_thm_goal lthy qty qty_name rsp_thms defs thm goal;
+    val (_, lthy2) = note (name, lifted_thm) lthy;
+  in
+    lthy2
+  end
+*}
+
+ML {*
+fun simp_ids_trm trm =
+  trm |>
+  MetaSimplifier.rewrite false @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id}
+  |> cprop_of |> Thm.dest_equals |> snd
+
+*}
+
+(* Unused part of the locale *)
+
+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
+
+
+
+