# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260968943 -3600
# Node ID ae562c2ad96b6404ebf6e72cac2e833f854991a8
# Parent  b85875d65b106ec1488a23976c206ff528dffbab# Parent  544b05e03ec0c00c65872ab02a26baf04ff08c25
merged

diff -r b85875d65b10 -r ae562c2ad96b FIXME-TODO
--- a/FIXME-TODO	Wed Dec 16 14:08:42 2009 +0100
+++ b/FIXME-TODO	Wed Dec 16 14:09:03 2009 +0100
@@ -47,3 +47,5 @@
 - Maybe quotient and equiv theorems like the ones for
   [QuotList, QuotOption, QuotPair...] could be automatically
   proven?
+
+- Examples: Finite multiset.
\ No newline at end of file
diff -r b85875d65b10 -r ae562c2ad96b Quot/Examples/LarryInt.thy
--- a/Quot/Examples/LarryInt.thy	Wed Dec 16 14:08:42 2009 +0100
+++ b/Quot/Examples/LarryInt.thy	Wed Dec 16 14:09:03 2009 +0100
@@ -22,30 +22,39 @@
 quotient_def
   One_int_def: "1::int" as "(1::nat, 0::nat)"
 
+definition
+  "add_raw \<equiv> \<lambda>(x, y) (u, v). (x + (u::nat), y + (v::nat))"
+
 quotient_def
   "(op +) :: int \<Rightarrow> int \<Rightarrow> int" 
 as 
-  "\<lambda>(x, y) (u, v). (x + (u::nat), y + (v::nat))"
+  "add_raw"
+
+definition
+  "uminus_raw \<equiv> \<lambda>(x::nat, y::nat). (y, x)"
 
 quotient_def
   "uminus :: int \<Rightarrow> int" 
 as 
-  "\<lambda>(x, y). (y::nat, x::nat)"
+  "uminus_raw"
 
 fun
-  mult_aux::"nat \<times> nat \<Rightarrow> nat \<times> nat \<Rightarrow> nat \<times> nat"
+  mult_raw::"nat \<times> nat \<Rightarrow> nat \<times> nat \<Rightarrow> nat \<times> nat"
 where
-  "mult_aux (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
+  "mult_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
 
 quotient_def
   "(op *) :: int \<Rightarrow> int \<Rightarrow> int" 
 as 
-  "mult_aux"
+  "mult_raw"
+
+definition
+  "le_raw \<equiv> \<lambda>(x, y) (u, v). (x+v \<le> u+(y::nat))"
 
 quotient_def 
   le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" 
 as 
-  "\<lambda>(x, y) (u, v). (x+v \<le> u+(y::nat))"
+  "le_raw"
 
 definition
   less_int_def: "z < (w::int) \<equiv> (z \<le> w & z \<noteq> w)"
@@ -59,133 +68,106 @@
 
 subsection{*Construction of the Integers*}
 
-abbreviation
-  "uminus_aux \<equiv> \<lambda>(x, y). (y::nat, x::nat)"
-
-lemma zminus_zminus_aux:
-  "uminus_aux (uminus_aux z) = z"
-  by (cases z) (simp)
+lemma zminus_zminus_raw:
+  "uminus_raw (uminus_raw z) = z"
+  by (cases z) (simp add: uminus_raw_def)
 
 lemma [quot_respect]:
-  shows "(intrel ===> intrel) uminus_aux uminus_aux"
-  by simp
+  shows "(intrel ===> intrel) uminus_raw uminus_raw"
+  by (simp add: uminus_raw_def)
   
 lemma zminus_zminus: 
   shows "- (- z) = (z::int)"
-apply(lifting zminus_zminus_aux)
-apply(injection)
-apply(rule quot_respect)
-apply(rule quot_respect)
+apply(lifting zminus_zminus_raw)
 done
-(* PROBLEM *)
 
-lemma zminus_0_aux:
-  shows "uminus_aux (0, 0) = (0, 0::nat)"
-by simp
+lemma zminus_0_raw:
+  shows "uminus_raw (0, 0) = (0, 0::nat)"
+by (simp add: uminus_raw_def)
 
 lemma zminus_0: "- 0 = (0::int)"
-apply(lifting zminus_0_aux)
-apply(injection)
-apply(rule quot_respect)
+apply(lifting zminus_0_raw)
 done
-(* PROBLEM *)
 
 subsection{*Integer Addition*}
 
-definition
-  "add_aux \<equiv> \<lambda>(x, y) (u, v). (x + (u::nat), y + (v::nat))"
-
-lemma zminus_zadd_distrib_aux:
-  shows "uminus_aux (add_aux z w) = add_aux (uminus_aux z) (uminus_aux w)"
+lemma zminus_zadd_distrib_raw:
+  shows "uminus_raw (add_raw z w) = add_raw (uminus_raw z) (uminus_raw w)"
 by (cases z, cases w)
-   (auto simp add: add_aux_def)
+   (auto simp add: add_raw_def uminus_raw_def)
 
 lemma [quot_respect]:
-  shows "(intrel ===> intrel ===> intrel) 
-            (\<lambda>(x, y) (u, v). (x + u, y + (v::nat)))  (\<lambda>(x, y) (u, v). (x + u, y + (v::nat)))"
-by simp
+  shows "(intrel ===> intrel ===> intrel) add_raw add_raw"
+by (simp add: add_raw_def)
 
 lemma zminus_zadd_distrib: 
   shows "- (z + w) = (- z) + (- w::int)"
-apply(lifting zminus_zadd_distrib_aux[simplified add_aux_def])
-apply(injection)
-apply(rule quot_respect)+
+apply(lifting zminus_zadd_distrib_raw)
 done
-(* PROBLEM *)
 
-lemma zadd_commute_aux:
-  shows "add_aux z w = add_aux w z"
+lemma zadd_commute_raw:
+  shows "add_raw z w = add_raw w z"
 by (cases z, cases w)
-   (simp add: add_aux_def)
+   (simp add: add_raw_def)
 
-lemma zadd_commute: 
+lemma zadd_commute:
   shows "(z::int) + w = w + z"
-apply(lifting zadd_commute_aux[simplified add_aux_def])
-apply(injection)
-apply(rule quot_respect)+
+apply(lifting zadd_commute_raw)
 done
-(* PROBLEM *)
 
-lemma zadd_assoc_aux:
-  shows "add_aux (add_aux z1 z2) z3 = add_aux z1 (add_aux z2 z3)"
-by (cases z1, cases z2, cases z3) (simp add: add_aux_def)
+lemma zadd_assoc_raw:
+  shows "add_raw (add_raw z1 z2) z3 = add_raw z1 (add_raw z2 z3)"
+by (cases z1, cases z2, cases z3) (simp add: add_raw_def)
 
 lemma zadd_assoc: "((z1::int) + z2) + z3 = z1 + (z2 + z3)"
-apply(lifting zadd_assoc_aux[simplified add_aux_def])
-apply(injection)
-apply(rule quot_respect)+
+apply(lifting zadd_assoc_raw)
 done
-(* PROBLEM *)
 
-lemma zadd_0_aux:
+lemma zadd_0_raw:
   fixes z::"nat \<times> nat"
-  shows "add_aux (0, 0) z = z"
-by (simp add: add_aux_def)
+  shows "add_raw (0, 0) z = z"
+by (simp add: add_raw_def)
 
 
 (*also for the instance declaration int :: plus_ac0*)
 lemma zadd_0: "(0::int) + z = z"
-apply(lifting zadd_0_aux[simplified add_aux_def])
-apply(injection)
-apply(rule quot_respect)+
+apply(lifting zadd_0_raw)
 done
 
-lemma zadd_zminus_inverse_aux:
-  shows "intrel (add_aux (uminus_aux z) z) (0, 0)"
-by (cases z) (simp add: add_aux_def)
+lemma zadd_zminus_inverse_raw:
+  shows "intrel (add_raw (uminus_raw z) z) (0, 0)"
+by (cases z) (simp add: add_raw_def uminus_raw_def)
 
 lemma zadd_zminus_inverse2: "(- z) + z = (0::int)"
-apply(lifting zadd_zminus_inverse_aux[simplified add_aux_def])
-apply(injection)
-apply(rule quot_respect)+
+apply(lifting zadd_zminus_inverse_raw)
 done
 
 subsection{*Integer Multiplication*}
 
-lemma zmult_zminus_aux:
-  shows "mult_aux (uminus_aux z) w = uminus_aux (mult_aux z w)"
+lemma zmult_zminus_raw:
+  shows "mult_raw (uminus_raw z) w = uminus_raw (mult_raw z w)"
 apply(cases z, cases w)
-apply(simp)
+apply(simp add:uminus_raw_def)
 done
 
-lemma mult_aux_fst:
+lemma mult_raw_fst:
   assumes a: "intrel x z"
-  shows "intrel (mult_aux x y) (mult_aux z y)"
+  shows "intrel (mult_raw x y) (mult_raw z y)"
 using a
 apply(cases x, cases y, cases z)
-apply(auto simp add: mult_aux.simps intrel.simps)
+apply(auto simp add: mult_raw.simps intrel.simps)
 apply(rename_tac u v w x y z)
 apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
 apply(simp add: mult_ac)
 apply(simp add: add_mult_distrib [symmetric])
 done
 
-lemma mult_aux_snd:
+lemma mult_raw_snd:
   assumes a: "intrel x z"
-  shows "intrel (mult_aux y x) (mult_aux y z)"
+  shows "intrel (mult_raw y x) (mult_raw y z)"
 using a
 apply(cases x, cases y, cases z)
-apply(auto simp add: mult_aux.simps intrel.simps)
+apply(auto simp add: mult_raw.simps intrel.simps)
 apply(rename_tac u v w x y z)
 apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
 apply(simp add: mult_ac)
@@ -193,51 +175,46 @@
 done
 
 lemma [quot_respect]:
-  shows "(intrel ===> intrel ===> intrel) mult_aux mult_aux"
+  shows "(intrel ===> intrel ===> intrel) mult_raw mult_raw"
 apply(simp only: fun_rel.simps)
 apply(rule allI | rule impI)+
 apply(rule equivp_transp[OF int_equivp])
-apply(rule mult_aux_fst)
+apply(rule mult_raw_fst)
 apply(assumption)
-apply(rule mult_aux_snd)
+apply(rule mult_raw_snd)
 apply(assumption)
 done
 
 lemma zmult_zminus: "(- z) * w = - (z * (w::int))"
-apply(lifting zmult_zminus_aux)
-apply(injection)
-apply(rule quot_respect)
-apply(rule quot_respect)
+apply(lifting zmult_zminus_raw)
 done
 
-lemma zmult_commute_aux: 
-  shows "mult_aux z w = mult_aux w z"
+lemma zmult_commute_raw: 
+  shows "mult_raw z w = mult_raw w z"
 apply(cases z, cases w)
 apply(simp add: add_ac mult_ac)
 done
 
 lemma zmult_commute: "(z::int) * w = w * z"
-by (lifting zmult_commute_aux)
+by (lifting zmult_commute_raw)
 
-lemma zmult_assoc_aux:
-  shows "mult_aux (mult_aux z1 z2) z3 = mult_aux z1 (mult_aux z2 z3)"
+lemma zmult_assoc_raw:
+  shows "mult_raw (mult_raw z1 z2) z3 = mult_raw z1 (mult_raw z2 z3)"
 apply(cases z1, cases z2, cases z3)
 apply(simp add: add_mult_distrib2 mult_ac)
 done
 
 lemma zmult_assoc: "((z1::int) * z2) * z3 = z1 * (z2 * z3)"
-by (lifting zmult_assoc_aux)
+by (lifting zmult_assoc_raw)
 
-lemma zadd_mult_distrib_aux:
-  shows "mult_aux (add_aux z1 z2) w = add_aux (mult_aux z1 w) (mult_aux z2 w)"
+lemma zadd_mult_distrib_raw:
+  shows "mult_raw (add_raw z1 z2) w = add_raw (mult_raw z1 w) (mult_raw z2 w)"
 apply(cases z1, cases z2, cases w)
-apply(simp add: add_mult_distrib2 mult_ac add_aux_def)
+apply(simp add: add_mult_distrib2 mult_ac add_raw_def)
 done
 
 lemma zadd_zmult_distrib: "((z1::int) + z2) * w = (z1 * w) + (z2 * w)"
-apply(lifting zadd_mult_distrib_aux[simplified add_aux_def])
-apply(injection)
-apply(rule quot_respect)+
+apply(lifting zadd_mult_distrib_raw)
 done
 
 lemma zadd_zmult_distrib2: "(w::int) * (z1 + z2) = (w * z1) + (w * z2)"
@@ -253,22 +230,22 @@
   zadd_zmult_distrib zadd_zmult_distrib2
   zdiff_zmult_distrib zdiff_zmult_distrib2
 
-lemma zmult_1_aux:
-  shows "mult_aux (1, 0) z = z"
+lemma zmult_1_raw:
+  shows "mult_raw (1, 0) z = z"
 apply(cases z)
 apply(auto)
 done
 
 lemma zmult_1: "(1::int) * z = z"
-apply(lifting zmult_1_aux)
+apply(lifting zmult_1_raw)
 done
 
 lemma zmult_1_right: "z * (1::int) = z"
 by (rule trans [OF zmult_commute zmult_1])
 
 lemma zero_not_one:
-  shows "(0, 0) \<noteq> (1::nat, 0::nat)"
-by simp
+  shows "\<not>(intrel (0, 0) (1::nat, 0::nat))"
+by auto
 
 text{*The Integers Form A Ring*}
 instance int :: comm_ring_1
@@ -283,58 +260,46 @@
   show "i * j = j * i" by (rule zmult_commute)
   show "1 * i = i" by (rule zmult_1) 
   show "(i + j) * k = i * k + j * k" by (simp add: int_distrib)
-  show "0 \<noteq> (1::int)" 
-    by (lifting zero_not_one) (auto) (* PROBLEM? regularize failed *)
+  show "0 \<noteq> (1::int)" by (lifting zero_not_one)
 qed
 
 
 subsection{*The @{text "\<le>"} Ordering*}
 
-abbreviation
-  "le_aux \<equiv> \<lambda>(x, y) (u, v). (x+v \<le> u+(y::nat))"
-
-lemma zle_refl_aux:
-  "le_aux w w"
+lemma zle_refl_raw:
+  "le_raw w w"
 apply(cases w)
-apply(simp)
+apply(simp add: le_raw_def)
 done
 
 lemma [quot_respect]:
-  shows "(intrel ===> intrel ===> op =) le_aux le_aux"
-by auto
+  shows "(intrel ===> intrel ===> op =) le_raw le_raw"
+by (auto) (simp_all add: le_raw_def)
 
 lemma zle_refl: "w \<le> (w::int)"
-apply(lifting zle_refl_aux)
-apply(injection)
-apply(rule quot_respect)
+apply(lifting zle_refl_raw)
 done
-(* PROBLEM *)
 
-lemma zle_trans_aux:
-  shows "\<lbrakk>le_aux i j; le_aux j k\<rbrakk> \<Longrightarrow> le_aux i k"
+lemma zle_trans_raw:
+  shows "\<lbrakk>le_raw i j; le_raw j k\<rbrakk> \<Longrightarrow> le_raw i k"
 apply(cases i, cases j, cases k)
 apply(auto)
+apply(simp add:le_raw_def)
 done
 
 lemma zle_trans: "\<lbrakk>i \<le> j; j \<le> k\<rbrakk> \<Longrightarrow> i \<le> (k::int)"
-apply(lifting zle_trans_aux)
-apply(injection)
-apply(rule quot_respect)+
+apply(lifting zle_trans_raw)
 done
-(* PROBLEM *)
 
-lemma zle_anti_sym_aux:
-  shows "\<lbrakk>le_aux z w; le_aux w z\<rbrakk> \<Longrightarrow> intrel z w"
+lemma zle_anti_sym_raw:
+  shows "\<lbrakk>le_raw z w; le_raw w z\<rbrakk> \<Longrightarrow> intrel z w"
 apply(cases z, cases w)
-apply(auto)
+apply(auto iff: le_raw_def)
 done
 
 lemma zle_anti_sym: "\<lbrakk>z \<le> w; w \<le> z\<rbrakk> \<Longrightarrow> z = (w::int)"
-apply(lifting zle_anti_sym_aux)
-apply(injection)
-apply(rule quot_respect)+
+apply(lifting zle_anti_sym_raw)
 done
-(* PROBLEM *)
 
 (* Axiom 'order_less_le' of class 'order': *)
 lemma zless_le: "((w::int) < z) = (w \<le> z & w \<noteq> z)"
@@ -347,61 +312,53 @@
 
 (* Axiom 'linorder_linear' of class 'linorder': *)
 
-lemma zle_linear_aux:
-  "le_aux z w \<or> le_aux w z"
+lemma zle_linear_raw:
+  "le_raw z w \<or> le_raw w z"
 apply(cases w, cases z)
-apply(auto)
+apply(auto iff: le_raw_def)
 done
 
 
 lemma zle_linear: "(z::int) \<le> w \<or> w \<le> z"
-apply(lifting zle_linear_aux)
-apply(injection)
-apply(rule quot_respect)+
+apply(lifting zle_linear_raw)
 done
 
 instance int :: linorder
 proof qed (rule zle_linear)
 
-lemma zadd_left_mono_aux:
-  shows "le_aux i j \<Longrightarrow> le_aux (add_aux k i) (add_aux k j)"
+lemma zadd_left_mono_raw:
+  shows "le_raw i j \<Longrightarrow> le_raw (add_raw k i) (add_raw k j)"
 apply(cases k)
-apply(auto simp add: add_aux_def)
+apply(auto simp add: add_raw_def le_raw_def)
 done
 
 lemma zadd_left_mono: "i \<le> j \<Longrightarrow> k + i \<le> k + (j::int)"
-apply(lifting zadd_left_mono_aux[simplified add_aux_def])
-apply(injection)
-apply(rule quot_respect)+
+apply(lifting zadd_left_mono_raw)
 done
-(* PROBLEM *)
 
 
 
 subsection{*Magnitide of an Integer, as a Natural Number: @{term nat}*}
 
-(* PROBLEM: this has to be a definition, not an abbreviation *)
-(* otherwise the lemma nat_le_eq_zle cannot be lifted        *)
-
-abbreviation
-  "nat_aux \<equiv> \<lambda>(x, y).x - (y::nat)"
+definition
+  "nat_raw \<equiv> \<lambda>(x, y).x - (y::nat)"
 
 quotient_def
   "nat2::int\<Rightarrow>nat"
 as
-  "nat_aux"
+  "nat_raw"
 
 abbreviation
-  "less_aux x y \<equiv> (le_aux x y \<and> \<not>(x = y))"
+  "less_raw x y \<equiv> (le_raw x y \<and> \<not>(x = y))"
 
-lemma nat_le_eq_zle_aux:
-  shows "less_aux (0, 0) w \<or> le_aux (0, 0) z \<Longrightarrow> (nat_aux w \<le> nat_aux z) = (le_aux w z)"
+lemma nat_le_eq_zle_raw:
+  shows "less_raw (0, 0) w \<or> le_raw (0, 0) z \<Longrightarrow> (nat_raw w \<le> nat_raw z) = (le_raw w z)"
 apply(auto)
 sorry
 
 lemma [quot_respect]:
-  shows "(intrel ===> op =) nat_aux nat_aux"
-apply(auto)
+  shows "(intrel ===> op =) nat_raw nat_raw"
+apply(auto iff: nat_raw_def)
 done
 
 ML {*
@@ -422,9 +379,7 @@
 
 lemma nat_le_eq_zle: "0 < w \<or> 0 \<le> z \<Longrightarrow> (nat2 w \<le> nat2 z) = (w\<le>z)"
 unfolding less_int_def
-apply(lifting nat_le_eq_zle_aux)
-apply(injection)
-apply(simp_all only: quot_respect)
+apply(lifting nat_le_eq_zle_raw)
 done
 
 end
diff -r b85875d65b10 -r ae562c2ad96b Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Wed Dec 16 14:08:42 2009 +0100
+++ b/Quot/QuotMain.thy	Wed Dec 16 14:09:03 2009 +0100
@@ -437,13 +437,10 @@
 *}
 
 ML {*
-fun solve_quotient_assums ctxt thm =
-let 
-  val goal = hd (Drule.strip_imp_prems (cprop_of thm)) 
-in
-  thm OF [Goal.prove_internal [] goal (fn _ => quotient_tac ctxt 1)]
-end
-handle _ => error "solve_quotient_assums failed. Maybe a quotient_thm is missing"
+fun solve_quotient_assum ctxt thm =
+  case Seq.pull (quotient_tac ctxt 1 thm) of
+    SOME (t, _) => t
+  | _ => error "solve_quotient_assum failed. Maybe a quotient_thm is missing"
 *}
 
 
@@ -859,9 +856,6 @@
 fun fun_map_tac ctxt = CONVERSION (fun_map_conv [] ctxt)
 *}
 
-(* Since the patterns for the lhs are different; there are 2 different make-insts *)
-(* 1: does  ? \<rightarrow> id *)
-(* 2: does  ? \<rightarrow> non-id *)
 ML {* 
 fun mk_abs u i t =
   if incr_boundvars i u aconv t then Bound i
@@ -873,24 +867,27 @@
 
 fun make_inst lhs t =
 let
-  val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs;
-  val _ $ (Abs (_, _, g)) = t;
-in 
-  (f, Abs ("x", T, mk_abs u 0 g)) 
+  val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs;
+  val _ $ (Abs (_, _, (_ $ g))) = t;
+in
+  (f, Abs ("x", T, mk_abs u 0 g))
 end
 
-fun make_inst2 lhs t =
+fun make_inst_id lhs t =
 let
-  val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs;
-  val _ $ (Abs (_, _, (_ $ g))) = t;
-in 
-  (f, Abs ("x", T, mk_abs u 0 g)) 
+  val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs;
+  val _ $ (Abs (_, _, g)) = t;
+in
+  (f, Abs ("x", T, mk_abs u 0 g))
 end
 *}
 
 ML {*
-(* FIXME / TODO this needs to be clarified *)
-
+(* Simplifies a redex using the 'lambda_prs' theorem. *)
+(* First instantiates the types and known subterms. *)
+(* Then solves the quotient assumptions to get Rep2 and Abs1 *)
+(* Finally instantiates the function f using make_inst *)
+(* If Rep2 is identity then the pattern is simpler and make_inst_id is used *)
 fun lambda_prs_simple_conv ctxt ctrm =
   case (term_of ctrm) of
    (Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _) =>
@@ -901,36 +898,11 @@
        val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_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 te = @{thm eq_reflection} OF [solve_quotient_assums ctxt (solve_quotient_assums ctxt lpi)]
-       val ti =
-         (let
-           val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te
-           val (insp, inst) = make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm)
-         in
-           Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts
-         end handle _ => (* TODO handle only Bind | Error "make_inst" *)
-         let
-           val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te
-           val _ = tracing ("ts rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ts)));
-           val _ = tracing ("redex:\n" ^ (Syntax.string_of_term ctxt (term_of ctrm)));
-           val (insp, inst) = make_inst2 (term_of (Thm.lhs_of ts)) (term_of ctrm)
-         in
-           Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts
-         end handle _ => (* TODO handle only Bind | Error "make_inst" *)
-         let
-           val (insp, inst) = make_inst2 (term_of (Thm.lhs_of te)) (term_of ctrm)
-           val td = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) te
-         in
-           MetaSimplifier.rewrite_rule (id_simps_get ctxt) td
-         end)
-       val _ = if not (Term.is_Const a2 andalso fst (dest_Const a2) = @{const_name "id"}) then
-                  (tracing "lambda_prs";
-                   tracing ("redex:\n" ^ (Syntax.string_of_term ctxt (term_of ctrm)));
-                   tracing ("lpi rule:\n" ^ (Syntax.string_of_term ctxt (prop_of lpi)));
-                   tracing ("te rule:\n" ^ (Syntax.string_of_term ctxt (prop_of te)));
-                   tracing ("ti rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ti))))
-               else ()
-
+       val te = @{thm eq_reflection} OF [solve_quotient_assum ctxt (solve_quotient_assum ctxt lpi)]
+       val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te
+       val make_inst = if ty_c = ty_d then make_inst_id else make_inst
+       val (insp, inst) = make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm)
+       val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts
      in
        Conv.rewr_conv ti ctrm
      end