
diff -r 4fcbbb5b3b58 -r f78aa16daae5 QuotMain.thy
--- a/QuotMain.thy	Wed Nov 25 14:25:29 2009 +0100
+++ b/QuotMain.thy	Wed Nov 25 15:20:10 2009 +0100
@@ -201,32 +201,7 @@
 
 ML {* atomize_thm @{thm list.induct} *}
 
-section {* RepAbs injection *}
-(*
-
-To prove that the old theorem implies the new one, we first
-atomize it and then try:
-
- 1) theorems 'trans2' from the appropriate QUOT_TYPE
- 2) remove lambdas from both sides (LAMBDA_RES_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
-10) reflexivity of the relation
-11) assumption
-    (Lambdas under respects may have left us some assumptions)
-12) proving obvious higher order equalities by simplifying fun_rel
-    (not sure if it is still needed?)
-13) unfolding lambda on one side
-14) simplifying (= ===> =) for simpler respectfullness
-
-*)
-
-
+section {* infrastructure about id *}
 
 (* Need to have a meta-equality *)
 lemma id_def_sym: "(\<lambda>x. x) \<equiv> id"
@@ -234,21 +209,6 @@
 (* TODO: can be also obtained with: *)
 ML {* symmetric (eq_reflection OF @{thms id_def}) *}
 
-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 CHANGED' tac = (fn i => CHANGED (tac i))
-*}
-
 lemma prod_fun_id: "prod_fun id id \<equiv> id"
 by (rule eq_reflection) (simp add: prod_fun_def)
 
@@ -260,124 +220,11 @@
 done
 
 ML {*
-fun quotient_tac quot_thm =
-  REPEAT_ALL_NEW (FIRST' [
-    rtac @{thm FUN_QUOTIENT},
-    rtac quot_thm,
-    rtac @{thm IDENTITY_QUOTIENT},
-    (* For functional identity quotients, (op = ---> op =) *)
-    CHANGED' (
-      (simp_tac (HOL_ss addsimps @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id}
-      )))
-  ])
-*}
-
-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 {* (* Legacy *)
-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 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 {*
-val ball_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
-  let
-    val _ $ (_ $ (Const (@{const_name Ball}, _) $ _) $
-                 (Const (@{const_name Ball}, _) $ _)) = term_of concl
-  in
-    ((simp_tac (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 (HOL_ss addsimps @{thms FUN_REL.simps}))) 1
-  end
-  handle _ => no_tac)
-*}
-
-ML {*
-val bex_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
-  let
-    val _ $ (_ $ (Const (@{const_name Bex}, _) $ _) $
-                 (Const (@{const_name Bex}, _) $ _)) = term_of concl
-  in
-    ((simp_tac (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 (HOL_ss addsimps @{thms FUN_REL.simps}))) 1
-  end
-  handle _ => no_tac)
-*}
-
-ML {*
-fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
-*}
-
-ML {*
-fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms =
-  (FIRST' [
-    rtac trans_thm,
-    LAMBDA_RES_TAC ctxt,
-    ball_rsp_tac ctxt,
-    bex_rsp_tac ctxt,
-    FIRST' (map rtac rsp_thms),
-    rtac refl,
-    (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [SOLVES' (quotient_tac quot_thm)])),
-    (APPLY_RSP_TAC rty ctxt THEN' (RANGE [SOLVES' (quotient_tac quot_thm), SOLVES' (quotient_tac quot_thm)])),
-    Cong_Tac.cong_tac @{thm cong},
-    rtac @{thm ext},
-    rtac reflex_thm,
-    atac,
-    SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})),
-    WEAK_LAMBDA_RES_TAC ctxt,
-    CHANGED' (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}))
-    ])
-*}
-
-section {* Cleaning the goal *}
-
-
-ML {*
 fun simp_ids lthy thm =
   MetaSimplifier.rewrite_rule @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id} thm
 *}
 
-text {* Does the same as 'subst' in a given prop or theorem *}
+section {* Does the same as 'subst' in a given theorem *}
 
 ML {*
 fun eqsubst_thm ctxt thms thm =
@@ -395,6 +242,8 @@
   end
 *}
 
+section {*  Infrastructure about definitions *}
+
 text {* expects atomized definition *}
 ML {*
 fun add_lower_defs_aux lthy thm =
@@ -419,140 +268,7 @@
   end
 *}
 
-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)
-*}
-
-
-
-(* changes (?'a ?'b raw) (?'a ?'b quo) (int 'b raw \<Rightarrow> bool) to (int 'b quo \<Rightarrow> bool) *)
-ML {*
-fun exchange_ty lthy rty qty ty =
-  let
-    val thy = ProofContext.theory_of lthy
-  in
-    if Sign.typ_instance thy (ty, rty) then
-      let
-        val inst = Sign.typ_match thy (rty, ty) Vartab.empty
-      in
-        Envir.subst_type inst qty
-      end
-    else
-      let
-        val (s, tys) = dest_Type ty
-      in
-        Type (s, map (exchange_ty lthy rty qty) tys)
-      end
-  end
-  handle TYPE _ => ty (* for dest_Type *)
-*}
-
-
-ML {*
-fun find_matching_types rty ty =
-  if Type.raw_instance (Logic.varifyT ty, rty)
-  then [ty]
-  else
-    let val (s, tys) = dest_Type ty in
-    flat (map (find_matching_types rty) tys)
-    end
-    handle TYPE _ => []
-*}
-
-ML {*
-fun negF absF = repF
-  | negF repF = absF
-
-fun get_fun flag qenv lthy ty =
-let
-  
-  fun get_fun_aux s fs =
-   (case (maps_lookup (ProofContext.theory_of lthy) s) of
-      SOME info => list_comb (Const (#mapfun info, dummyT), fs)
-    | NONE      => error ("no map association for type " ^ s))
-
-  fun get_const flag qty =
-  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), dummyT)
-    | repF => Const (Sign.full_bname thy ("REP_" ^ qty_name), dummyT)
-  end
-
-  fun mk_identity ty = Abs ("", ty, Bound 0)
-
-in
-  if (AList.defined (op=) qenv ty)
-  then (get_const flag ty)
-  else (case ty of
-          TFree _ => mk_identity ty
-        | Type (_, []) => mk_identity ty 
-        | Type ("fun" , [ty1, ty2]) => 
-            let
-              val fs_ty1 = get_fun (negF flag) qenv lthy ty1
-              val fs_ty2 = get_fun flag qenv lthy ty2
-            in  
-              get_fun_aux "fun" [fs_ty1, fs_ty2]
-            end 
-        | Type (s, tys) => get_fun_aux s (map (get_fun flag qenv lthy) tys)
-        | _ => error ("no type variables allowed"))
-end
-*}
-
-ML {*
-fun get_fun_OLD flag (rty, qty) lthy ty =
-  let
-    val tys = find_matching_types rty ty;
-    val qenv = map (fn t => (exchange_ty lthy rty qty t, t)) tys;
-    val xchg_ty = exchange_ty lthy rty qty ty
-  in
-    get_fun flag qenv lthy xchg_ty
-  end
-*}
-
-ML {*
-fun applic_prs lthy rty qty absrep ty =
-  let
-    val rty = Logic.varifyT rty;
-    val qty = Logic.varifyT qty;
-    fun absty ty =
-      exchange_ty lthy rty qty ty
-    fun mk_rep tm =
-      let
-        val ty = exchange_ty lthy qty rty (fastype_of tm)
-      in Syntax.check_term lthy ((get_fun_OLD repF (rty, qty) lthy ty) $ tm) end;
-    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
-    val (l, ltl) = Term.strip_type ty;
-    val nl = map absty l;
-    val vs = map (fn _ => "x") l;
-    val ((fname :: vfs), lthy') = Variable.variant_fixes ("f" :: vs) lthy;
-    val args = map Free (vfs ~~ nl);
-    val lhs = list_comb((Free (fname, nl ---> ltl)), args);
-    val rargs = map mk_rep args;
-    val f = Free (fname, nl ---> ltl);
-    val rhs = mk_abs (list_comb((mk_rep f), rargs));
-    val eq = Logic.mk_equals (rhs, lhs);
-    val ceq = cterm_of (ProofContext.theory_of lthy') eq;
-    val sctxt = HOL_ss addsimps (absrep :: @{thms fun_map.simps});
-    val t = Goal.prove_internal [] ceq (fn _ => simp_tac sctxt 1)
-    val t_id = MetaSimplifier.rewrite_rule @{thms id_def_sym} t;
-  in
-    singleton (ProofContext.export lthy' lthy) t_id
-  end
-*}
+section {* infrastructure about collecting theorems for calling lifting *}
 
 ML {*
 fun lookup_quot_data lthy qty =
@@ -947,6 +663,402 @@
   Logic.mk_equals (rtrm, Syntax.check_term lthy (inj_REPABS lthy (rtrm, qtrm)))
 *}
 
+section {* RepAbs injection tactic *}
+(*
+
+To prove that the regularised theorem implies the abs/rep injected, we first
+atomize it and then try:
+
+ 1) theorems 'trans2' from the appropriate QUOT_TYPE
+ 2) remove lambdas from both sides (LAMBDA_RES_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
+10) reflexivity of the relation
+11) assumption
+    (Lambdas under respects may have left us some assumptions)
+12) proving obvious higher order equalities by simplifying fun_rel
+    (not sure if it is still needed?)
+13) unfolding lambda on one side
+14) simplifying (= ===> =) for simpler respectfullness
+
+*)
+
+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 CHANGED' tac = (fn i => CHANGED (tac i))
+*}
+
+ML {*
+fun quotient_tac quot_thm =
+  REPEAT_ALL_NEW (FIRST' [
+    rtac @{thm FUN_QUOTIENT},
+    rtac quot_thm,
+    rtac @{thm IDENTITY_QUOTIENT},
+    (* For functional identity quotients, (op = ---> op =) *)
+    CHANGED' (
+      (simp_tac (HOL_ss addsimps @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id}
+      )))
+  ])
+*}
+
+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 {* (* Legacy *)
+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 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 {*
+val ball_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
+  let
+    val _ $ (_ $ (Const (@{const_name Ball}, _) $ _) $
+                 (Const (@{const_name Ball}, _) $ _)) = term_of concl
+  in
+    ((simp_tac (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 (HOL_ss addsimps @{thms FUN_REL.simps}))) 1
+  end
+  handle _ => no_tac)
+*}
+
+ML {*
+val bex_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
+  let
+    val _ $ (_ $ (Const (@{const_name Bex}, _) $ _) $
+                 (Const (@{const_name Bex}, _) $ _)) = term_of concl
+  in
+    ((simp_tac (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 (HOL_ss addsimps @{thms FUN_REL.simps}))) 1
+  end
+  handle _ => no_tac)
+*}
+
+ML {*
+fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
+*}
+
+ML {*
+fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms =
+  (FIRST' [
+    rtac trans_thm,
+    LAMBDA_RES_TAC ctxt,
+    ball_rsp_tac ctxt,
+    bex_rsp_tac ctxt,
+    FIRST' (map rtac rsp_thms),
+    rtac refl,
+    (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [SOLVES' (quotient_tac quot_thm)])),
+    (APPLY_RSP_TAC rty ctxt THEN' (RANGE [SOLVES' (quotient_tac quot_thm), SOLVES' (quotient_tac quot_thm)])),
+    Cong_Tac.cong_tac @{thm cong},
+    rtac @{thm ext},
+    rtac reflex_thm,
+    atac,
+    SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})),
+    WEAK_LAMBDA_RES_TAC ctxt,
+    CHANGED' (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}))
+    ])
+*}
+
+
+(****************************************)
+(* cleaning of the theorem              *)
+(****************************************)
+
+
+
+(* changes (?'a ?'b raw) (?'a ?'b quo) (int 'b raw \<Rightarrow> bool) to (int 'b quo \<Rightarrow> bool) *)
+ML {*
+fun exchange_ty lthy rty qty ty =
+  let
+    val thy = ProofContext.theory_of lthy
+  in
+    if Sign.typ_instance thy (ty, rty) then
+      let
+        val inst = Sign.typ_match thy (rty, ty) Vartab.empty
+      in
+        Envir.subst_type inst qty
+      end
+    else
+      let
+        val (s, tys) = dest_Type ty
+      in
+        Type (s, map (exchange_ty lthy rty qty) tys)
+      end
+  end
+  handle TYPE _ => ty (* for dest_Type *)
+*}
+
+
+ML {*
+fun find_matching_types rty ty =
+  if Type.raw_instance (Logic.varifyT ty, rty)
+  then [ty]
+  else
+    let val (s, tys) = dest_Type ty in
+    flat (map (find_matching_types rty) tys)
+    end
+    handle TYPE _ => []
+*}
+
+ML {*
+fun negF absF = repF
+  | negF repF = absF
+
+fun get_fun flag qenv lthy ty =
+let
+  
+  fun get_fun_aux s fs =
+   (case (maps_lookup (ProofContext.theory_of lthy) s) of
+      SOME info => list_comb (Const (#mapfun info, dummyT), fs)
+    | NONE      => error ("no map association for type " ^ s))
+
+  fun get_const flag qty =
+  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), dummyT)
+    | repF => Const (Sign.full_bname thy ("REP_" ^ qty_name), dummyT)
+  end
+
+  fun mk_identity ty = Abs ("", ty, Bound 0)
+
+in
+  if (AList.defined (op=) qenv ty)
+  then (get_const flag ty)
+  else (case ty of
+          TFree _ => mk_identity ty
+        | Type (_, []) => mk_identity ty 
+        | Type ("fun" , [ty1, ty2]) => 
+            let
+              val fs_ty1 = get_fun (negF flag) qenv lthy ty1
+              val fs_ty2 = get_fun flag qenv lthy ty2
+            in  
+              get_fun_aux "fun" [fs_ty1, fs_ty2]
+            end 
+        | Type (s, tys) => get_fun_aux s (map (get_fun flag qenv lthy) tys)
+        | _ => error ("no type variables allowed"))
+end
+*}
+
+ML {*
+fun get_fun_OLD flag (rty, qty) lthy ty =
+  let
+    val tys = find_matching_types rty ty;
+    val qenv = map (fn t => (exchange_ty lthy rty qty t, t)) tys;
+    val xchg_ty = exchange_ty lthy rty qty ty
+  in
+    get_fun flag qenv lthy xchg_ty
+  end
+*}
+
+ML {*
+fun applic_prs lthy rty qty absrep ty =
+  let
+    val rty = Logic.varifyT rty;
+    val qty = Logic.varifyT qty;
+    fun absty ty =
+      exchange_ty lthy rty qty ty
+    fun mk_rep tm =
+      let
+        val ty = exchange_ty lthy qty rty (fastype_of tm)
+      in Syntax.check_term lthy ((get_fun_OLD repF (rty, qty) lthy ty) $ tm) end;
+    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
+    val (l, ltl) = Term.strip_type ty;
+    val nl = map absty l;
+    val vs = map (fn _ => "x") l;
+    val ((fname :: vfs), lthy') = Variable.variant_fixes ("f" :: vs) lthy;
+    val args = map Free (vfs ~~ nl);
+    val lhs = list_comb((Free (fname, nl ---> ltl)), args);
+    val rargs = map mk_rep args;
+    val f = Free (fname, nl ---> ltl);
+    val rhs = mk_abs (list_comb((mk_rep f), rargs));
+    val eq = Logic.mk_equals (rhs, lhs);
+    val ceq = cterm_of (ProofContext.theory_of lthy') eq;
+    val sctxt = HOL_ss addsimps (absrep :: @{thms fun_map.simps});
+    val t = Goal.prove_internal [] ceq (fn _ => simp_tac sctxt 1)
+    val t_id = MetaSimplifier.rewrite_rule @{thms id_def_sym} t;
+  in
+    singleton (ProofContext.export lthy' lthy) t_id
+  end
+*}
+
+
+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 {*
+(* FIXME: allex_prs and lambda_prs can be one function *)
+fun allex_prs_tac lthy quot =
+  (EqSubst.eqsubst_tac lthy [0] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]})
+  THEN' (quotient_tac quot);
+*}
+
+ML {*
+let
+   val parser = Args.context -- Scan.lift Args.name_source
+   fun term_pat (ctxt, str) =
+      str |> ProofContext.read_term_pattern ctxt
+          |> ML_Syntax.print_term
+          |> ML_Syntax.atomic
+in
+   ML_Antiquote.inline "term_pat" (parser >> term_pat)
+end
+*}
+
+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 lambda_prs_conv1 ctxt quot ctrm =
+  case (term_of ctrm) of ((Const (@{const_name "fun_map"}, _) $ r1 $ a2) $ (Abs _)) =>
+  let
+    val (_, [ty_b, ty_a]) = dest_Type (fastype_of r1);
+    val (_, [ty_c, ty_d]) = dest_Type (fastype_of a2);
+    val thy = ProofContext.theory_of ctxt;
+    val [cty_a, cty_b, cty_c, cty_d] = map (ctyp_of thy) [ty_a, ty_b, ty_c, ty_d]
+    val tyinst = [SOME cty_a, SOME cty_b, SOME cty_c, SOME cty_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 tac =
+      (compose_tac (false, lpi, 2)) THEN_ALL_NEW
+      (quotient_tac quot);
+    val gc = Drule.strip_imp_concl (cprop_of lpi);
+    val t = Goal.prove_internal [] gc (fn _ => tac 1)
+    val te = @{thm eq_reflection} OF [t]
+    val ts = MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] te
+    val tl = Thm.lhs_of ts
+(*    val _ = tracing (Syntax.string_of_term @{context} (term_of ctrm));*)
+(*    val _ = tracing (Syntax.string_of_term @{context} (term_of tl));*)
+    val insts = matching_prs (ProofContext.theory_of ctxt) (term_of tl) (term_of ctrm);
+    val ti = Drule.eta_contraction_rule (Drule.instantiate insts ts);
+(*    val _ = tracing (Syntax.string_of_term @{context} (term_of (cprop_of ti)));*)
+  in
+    Conv.rewr_conv ti ctrm
+  end
+(* TODO: We can add a proper error message... *)
+  handle Bind => Conv.all_conv ctrm
+
+*}
+
+(* quot stands for the QUOTIENT theorems: *) 
+(* could be potentially all of them       *)
+ML {*
+fun lambda_prs_conv ctxt quot ctrm =
+  case (term_of ctrm) of
+    (Const (@{const_name "fun_map"}, _) $ _ $ _) $ (Abs _) =>
+      (Conv.arg_conv (Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt)
+      then_conv (lambda_prs_conv1 ctxt quot)) ctrm
+  | _ $ _ => Conv.comb_conv (lambda_prs_conv ctxt quot) ctrm
+  | Abs _ => Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt ctrm
+  | _ => Conv.all_conv ctrm
+*}
+
+ML {*
+fun lambda_prs_tac ctxt quot = CSUBGOAL (fn (goal, i) =>
+  CONVERSION
+    (Conv.params_conv ~1 (fn ctxt =>
+       (Conv.prems_conv ~1 (lambda_prs_conv ctxt quot) then_conv
+          Conv.concl_conv ~1 (lambda_prs_conv ctxt quot))) ctxt) i)
+*}
+
+ML {*
+fun clean_tac lthy quot defs reps_same =
+  let
+    val lower = flat (map (add_lower_defs lthy) defs)
+  in
+    EVERY' [TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot), 
+            lambda_prs_tac lthy quot,
+            (* TODO: cleaning according to app_prs *)
+            TRY o REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] lower),
+            simp_tac (HOL_ss addsimps [reps_same])]
+  end
+*}
 
 (* Genralisation of free variables in a goal *)
 
@@ -1047,119 +1159,12 @@
         end) ctxt
 *}
 
-
-
-ML {*
-(* FIXME: allex_prs and lambda_prs can be one function *)
-fun allex_prs_tac lthy quot =
-  (EqSubst.eqsubst_tac lthy [0] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]})
-  THEN' (quotient_tac quot);
-*}
-
-ML {*
-let
-   val parser = Args.context -- Scan.lift Args.name_source
-   fun term_pat (ctxt, str) =
-      str |> ProofContext.read_term_pattern ctxt
-          |> ML_Syntax.print_term
-          |> ML_Syntax.atomic
-in
-   ML_Antiquote.inline "term_pat" (parser >> term_pat)
-end
-*}
-
-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 lambda_prs_conv1 ctxt quot ctrm =
-  case (term_of ctrm) of ((Const (@{const_name "fun_map"}, _) $ r1 $ a2) $ (Abs _)) =>
-  let
-    val (_, [ty_b, ty_a]) = dest_Type (fastype_of r1);
-    val (_, [ty_c, ty_d]) = dest_Type (fastype_of a2);
-    val thy = ProofContext.theory_of ctxt;
-    val [cty_a, cty_b, cty_c, cty_d] = map (ctyp_of thy) [ty_a, ty_b, ty_c, ty_d]
-    val tyinst = [SOME cty_a, SOME cty_b, SOME cty_c, SOME cty_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 tac =
-      (compose_tac (false, lpi, 2)) THEN_ALL_NEW
-      (quotient_tac quot);
-    val gc = Drule.strip_imp_concl (cprop_of lpi);
-    val t = Goal.prove_internal [] gc (fn _ => tac 1)
-    val te = @{thm eq_reflection} OF [t]
-    val ts = MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] te
-    val tl = Thm.lhs_of ts
-(*    val _ = tracing (Syntax.string_of_term @{context} (term_of ctrm));*)
-(*    val _ = tracing (Syntax.string_of_term @{context} (term_of tl));*)
-    val insts = matching_prs (ProofContext.theory_of ctxt) (term_of tl) (term_of ctrm);
-    val ti = Drule.eta_contraction_rule (Drule.instantiate insts ts);
-(*    val _ = tracing (Syntax.string_of_term @{context} (term_of (cprop_of ti)));*)
-  in
-    Conv.rewr_conv ti ctrm
-  end
-(* TODO: We can add a proper error message... *)
-  handle Bind => Conv.all_conv ctrm
-
-*}
-ML {*
-fun lambda_prs_conv ctxt quot ctrm =
-  case (term_of ctrm) of
-    (Const (@{const_name "fun_map"}, _) $ r1 $ a2) $ (Abs (_, _, x)) =>
-      (Conv.arg_conv (Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt)
-      then_conv (lambda_prs_conv1 ctxt quot)) ctrm
-  | _ $ _ => Conv.comb_conv (lambda_prs_conv ctxt quot) ctrm
-  | Abs _ => Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt ctrm
-  | _ => Conv.all_conv ctrm
-*}
-
-ML {*
-fun lambda_prs_tac ctxt quot = CSUBGOAL (fn (goal, i) =>
-  CONVERSION
-    (Conv.params_conv ~1 (fn ctxt =>
-       (Conv.prems_conv ~1 (lambda_prs_conv ctxt quot) then_conv
-          Conv.concl_conv ~1 (lambda_prs_conv ctxt quot))) ctxt) i)
-*}
-
-ML {*
-  fun TRY' tac = fn i => TRY (tac i)
-*}
-
-ML {*
-fun clean_tac lthy quot defs reps_same =
-  let
-    val lower = flat (map (add_lower_defs lthy) defs)
-  in
-    TRY' (REPEAT_ALL_NEW (allex_prs_tac lthy quot)) THEN'
-    TRY' (lambda_prs_tac lthy quot) THEN'
-    TRY' (REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] lower)) THEN'
-    simp_tac (HOL_ss addsimps [reps_same])
-  end
-*}
-
 ML {*
 fun lift_tac lthy thm rel_eqv rel_refl rty quot trans2 rsp_thms reps_same defs =
-  (procedure_tac thm lthy) THEN'
-  (regularize_tac lthy rel_eqv rel_refl) THEN'
-  (REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms)) THEN'
-  (clean_tac lthy quot defs reps_same)
+  procedure_tac thm lthy THEN'
+  RANGE [regularize_tac lthy rel_eqv rel_refl,
+         REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms), 
+         clean_tac lthy quot defs reps_same]
 *}
 
 




