
diff -r c6a9b4e4d548 -r 40bb0c4718a6 QuotMain.thy
--- a/QuotMain.thy	Mon Nov 09 13:47:46 2009 +0100
+++ b/QuotMain.thy	Mon Nov 09 15:23:33 2009 +0100
@@ -160,16 +160,6 @@
 (* lifting of constants *)
 use "quotient_def.ML"
 
-
-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 {* ATOMIZE *}
 
 lemma atomize_eqv[atomize]: 
@@ -340,6 +330,8 @@
   | _ => 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
@@ -349,7 +341,7 @@
 
 (*
 ML {*
-  text {*val r = term_of @{cpat "R::?'a list \<Rightarrow> ?'a list \<Rightarrow>bool"};*}
+  text {*val r = term_of @{cpat "R::?'a list \<Rightarrow> ?'a list \<Rightarrow> bool"};*}
   val r = Free ("R", dummyT);
   val t = (my_reg @{context} r @{typ "'a list"} @{term "\<forall>(x::'b list). P x"});
   val t2 = Syntax.check_term @{context} t;
@@ -372,7 +364,8 @@
   "(c \<longrightarrow> a) \<Longrightarrow> (a \<Longrightarrow> b \<longrightarrow> d) \<Longrightarrow> (a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)"
 by auto
 
-(*lemma equality_twice: "a = c \<Longrightarrow> b = d \<Longrightarrow> (a = b \<longrightarrow> c = d)"
+(*lemma equality_twice:
+  "a = c \<Longrightarrow> b = d \<Longrightarrow> (a = b \<longrightarrow> c = d)"
 by auto*)
 
 ML {*
@@ -381,27 +374,72 @@
     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},
-      (*rtac @{thm equality_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 HOL_ss) THEN' rtac rel_refl),
-      (rtac @{thm RIGHT_RES_FORALL_REGULAR})
-     ]);
-    val cthm = Goal.prove lthy [] [] goal 
-      (fn {context,...} => tac context 1);
+      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 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
 *}
 
 section {* RepAbs injection *}
+(*
+
+Injecting RepAbs means:
+
+  For abstractions:
+  * If the type of the abstraction doesn't need lifting we recurse.
+  * If it does we add RepAbs around the whole term and check if the
+    variable needs lifting.
+    * If it doesn't then we recurse
+    * If it does we recurse and put 'RepAbs' around all occurences
+      of the variable in the obtained subterm.
+  For applications:
+  * If the term is 'Respects' applied to anything we leave it unchanged
+  * If the term needs lifting and the head is a constant that we know
+    how to lift, we put a RepAbs and recurse
+  * If the term needs lifting and the head is a free applied to subterms
+    (if it is not applied we treated it in Abs branch) then we
+    put RepAbs and recurse
+  * Otherwise just recurse.
+
+The injection is done in the following phases:
+ 1) build_repabs_term inserts rep-abs pairs in the term
+ 2) we prove the equality between the original theorem and this one
+ 3) we use Pure.equal_elim_rule1 to get the new theorem.
+
+To prove that the old theorem implies the new one, we first
+atomize it and then try:
+
+ 1) theorems 'trans2' from the QUOT_TYPE
+ 2) remove lambdas from both sides (LAMBDA_RES_TAC)
+ 3) remove Ball/Bex
+ 4) use RSP theorems
+ 5) remove rep_abs from right side
+ 6) reflexivity
+ 7) split applications of lifted type (apply_rsp)
+ 8) split applications of non-lifted type (cong_tac)
+ 9) apply extentionality
+10) relation reflexive
+11) assumption
+12) proving obvious higher order equalities by simplifying fun_rel
+    (not sure if still needed?)
+13) unfolding lambda on one side
+14) simplifying (= ===> =) for simpler respectfullness
+
+*)
+
 
 (* Needed to have a meta-equality *)
 lemma id_def_sym: "(\<lambda>x. x) \<equiv> id"
@@ -489,9 +527,10 @@
   then (get_const flag (ty, (exchange_ty lthy rty qty 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_noexchange (negF flag) (rty,qty) lthy ty1, get_fun_noexchange flag (rty,qty) lthy ty2]
+        | Type (_, []) => (mk_identity ty, (ty, ty))
+        | Type ("fun" , [ty1, ty2]) =>
+                 get_fun_fun [get_fun_noexchange (negF flag) (rty, qty) lthy ty1,
+                 get_fun_noexchange flag (rty, qty) lthy ty2]
         | Type (s, tys) => get_fun_aux s (map (get_fun_noexchange flag (rty, qty) lthy) tys)
         | _ => raise ERROR ("no type variables"))
 end
@@ -582,7 +621,7 @@
     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]
+    @{thm Pure.equal_elim_rule1} OF [rt, thm]
   end
 *}
 
@@ -593,7 +632,7 @@
 *}
 
 ML {*
-fun build_repabs_term lthy thm constructors rty qty =
+fun build_repabs_term lthy thm consts rty qty =
   let
     val rty = Logic.varifyT rty;
     val qty = Logic.varifyT qty;
@@ -607,44 +646,44 @@
       val ty = fastype_of tm
     in Syntax.check_term lthy ((get_fun_new repF (rty, qty) lthy ty) $ (mk_abs tm)) end
 
-    fun is_constructor (Const (x, _)) = member (op =) constructors x
-      | is_constructor _ = false;
+    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
+        Abs (a as (_, vty, _)) =>
           let
-            val v' = mk_repabs v;
-            val t1 = Envir.beta_norm (t' $ v')
+            val (vs, t) = Term.dest_abs a;
+            val v = Free(vs, vty);
+            val t' = lambda v (build_aux lthy t)
           in
-            lambda v t1
+            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 this is not needed any more *)
+                  val t1 = Envir.beta_norm (t' $ v')
+                in
+                  lambda v t1
+                end)
           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_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
+      | 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))
@@ -675,14 +714,17 @@
     rtac @{thm FUN_QUOTIENT},
     rtac quot_thm,
     rtac @{thm IDENTITY_QUOTIENT},
-    (fn i => CHANGED (simp_tac (HOL_ss addsimps @{thms FUN_MAP_I}) i) THEN rtac @{thm IDENTITY_QUOTIENT} i)
+    (
+      fn i => CHANGED (simp_tac (HOL_ss addsimps @{thms FUN_MAP_I}) i) THEN
+      rtac @{thm IDENTITY_QUOTIENT} i
+    )
   ])
 *}
 
 ML {*
 fun LAMBDA_RES_TAC ctxt i st =
   (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of
-    (_ $ (_ $ (Abs(_,_,_))$(Abs(_,_,_)))) =>
+    (_ $ (_ $ (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
@@ -691,10 +733,10 @@
 ML {*
 fun WEAK_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})
-  | (_ $ (_ $ (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
@@ -715,9 +757,10 @@
 *}
 
 ML {*
-val res_forall_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
+val ball_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
   let
-    val _ $ (_ $ (Const (@{const_name Ball}, _) $ _) $ (Const (@{const_name Ball}, _) $ _)) = term_of concl
+    val _ $ (_ $ (Const (@{const_name Ball}, _) $ _) $
+                 (Const (@{const_name Ball}, _) $ _)) = term_of concl
   in
     ((simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
     THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
@@ -729,9 +772,10 @@
 *}
 
 ML {*
-val res_exists_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
+val bex_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
   let
-    val _ $ (_ $ (Const (@{const_name Bex}, _) $ _) $ (Const (@{const_name Bex}, _) $ _)) = term_of concl
+    val _ $ (_ $ (Const (@{const_name Bex}, _) $ _) $
+                 (Const (@{const_name Bex}, _) $ _)) = term_of concl
   in
     ((simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
     THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
@@ -745,13 +789,10 @@
 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,
+    ball_rsp_tac ctxt,
+    bex_rsp_tac ctxt,
     FIRST' (map rtac rsp_thms),
     (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])),
     rtac refl,
@@ -771,9 +812,9 @@
 *}
 
 ML {*
-fun repabs lthy thm constructors rty qty quot_thm reflex_thm trans_thm rsp_thms =
+fun repabs lthy thm consts rty qty quot_thm reflex_thm trans_thm rsp_thms =
   let
-    val rt = build_repabs_term lthy thm constructors rty qty;
+    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));
@@ -802,15 +843,15 @@
 
 text {* expects atomized definition *}
 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 lthy f
-    in
-      (simp_ids lthy thm) :: (add_lower_defs_aux lthy g)
-    end
-    handle _ => [simp_ids lthy thm]
+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 lthy f
+  in
+    (simp_ids lthy thm) :: (add_lower_defs_aux lthy g)
+  end
+  handle _ => [simp_ids lthy thm]
 *}
 
 ML {*
@@ -825,30 +866,31 @@
 *}
 
 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)
+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)
+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 {*
@@ -870,39 +912,39 @@
 *}
 
 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
-    | _ => ([], []);
+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
+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 {*
@@ -918,7 +960,8 @@
       (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_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
@@ -928,36 +971,36 @@
 
 ML {*
 fun applic_prs lthy rty qty absrep ty =
- let
+  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_new repF (rty, qty) lthy ty) $ tm) end;
-  fun mk_abs tm =
-    let
-      val ty = fastype_of tm
-    in Syntax.check_term lthy ((get_fun_new 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 = (Simplifier.context lthy' 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
+    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_new repF (rty, qty) lthy ty) $ tm) end;
+    fun mk_abs tm =
+      let
+        val ty = fastype_of tm
+      in Syntax.check_term lthy ((get_fun_new 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 = (Simplifier.context lthy' 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 {*
@@ -1032,13 +1075,13 @@
 
 
 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;
+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
 *}
 
 




