--- a/IntEx.thy	Mon Oct 26 11:55:36 2009 +0100
+++ b/IntEx.thy	Mon Oct 26 13:33:28 2009 +0100
@@ -103,7 +103,86 @@
 where
  "SIGN i = (if i = ZERO then ZERO else if (LESS ZERO i) then ONE else (NEG ONE))"
 
- 
+lemma plus_sym_pre:
+  shows "intrel (my_plus a b) (my_plus b a)"
+  sorry
+
+lemma equiv_intrel: "EQUIV intrel"
+  sorry
+
+lemma intrel_refl: "intrel a a"
+  sorry
+
+lemma ho_plus_rsp : "IntEx.intrel ===> IntEx.intrel ===> IntEx.intrel my_plus my_plus"
+  sorry
+
+ML {* val t_a = atomize_thm @{thm plus_sym_pre} *}
+ML {* val t_r = regularize t_a @{typ "nat \<times> nat"} @{term "intrel"} @{thm equiv_intrel} @{context} *}
+ML {* val consts = [@{const_name "my_plus"}] *}
+
+ML {*
+  val rt = build_repabs_term @{context} t_r consts @{typ "nat \<times> nat"} @{typ "my_int"}
+  val rg = Logic.mk_equals ((Thm.prop_of t_r), rt);
+*}
+ML {*
+fun r_mk_comb_tac_myint ctxt =
+  r_mk_comb_tac ctxt @{thm QUOTIENT_my_int} @{thm intrel_refl} @{thm QUOT_TYPE_I_my_int.R_trans2}
+   (@{thms ho_plus_rsp} @ @{thms ho_all_prs ho_ex_prs})
+*}
+ML {* val (g, thm, othm) =
+  Toplevel.program (fn () =>
+  repabs_eq @{context} t_r consts @{typ "nat \<times> nat"} @{typ "my_int"}
+   @{thm QUOTIENT_my_int} @{thm intrel_refl} @{thm QUOT_TYPE_I_my_int.R_trans2}
+   (@{thms ho_plus_rsp} @ @{thms ho_all_prs ho_ex_prs})
+  )
+*}
+ML {*
+  val t_t2 =
+  Toplevel.program (fn () =>
+    repabs_eq2 @{context} (g, thm, othm)
+  )
+*}
+ML {*
+ val lpi = Drule.instantiate'
+   [SOME @{ctyp "nat \<times> nat"}, NONE, SOME @{ctyp "bool"}, NONE] [] @{thm LAMBDA_PRS};
+*}
+prove lambda_prs_mn_b : {* concl_of lpi *}
+apply (tactic {* compose_tac (false, @{thm LAMBDA_PRS}, 2) 1 *})
+apply (tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *})
+apply (tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *})
+done
+
+ML {*
+  fun simp_lam_prs lthy thm =
+    simp_lam_prs lthy (eqsubst_thm lthy
+      @{thms HOL.sym[OF lambda_prs_mn_b,simplified]}
+    thm)
+    handle _ => thm
+*}
+ML {* t_t2 *}
+ML {* val t_l = simp_lam_prs @{context} t_t2 *}
+ML {* findabs @{typ "nat \<times> nat"} (prop_of (atomize_thm @{thm plus_sym_pre})) *}
+
+ML {*
+  fun simp_allex_prs lthy thm =
+    let
+      val rwf = @{thm FORALL_PRS[OF QUOTIENT_my_int]};
+      val rwfs = @{thm "HOL.sym"} OF [rwf];
+      val rwe = @{thm EXISTS_PRS[OF QUOTIENT_my_int]};
+      val rwes = @{thm "HOL.sym"} OF [rwe]
+    in
+      (simp_allex_prs lthy (eqsubst_thm lthy [rwfs, rwes] thm))
+    end
+    handle _ => thm
+*}
+
+ML {* val t_a = simp_allex_prs @{context} t_l *}
+
+ML {* val t_defs = @{thms PLUS_def} *}
+ML {* val t_defs_sym = add_lower_defs @{context} t_defs *}
+ML {* val t_d = MetaSimplifier.rewrite_rule t_defs_sym t_a *}
+ML {* val t_r = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_my_int.REPS_same} t_d *}
+ML {* ObjectLogic.rulify t_r *}
 
 lemma 
   fixes i j k::"my_int"

--- a/QuotMain.thy	Mon Oct 26 11:55:36 2009 +0100
+++ b/QuotMain.thy	Mon Oct 26 13:33:28 2009 +0100
@@ -709,6 +709,7 @@
     ),
     (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])),
     rtac refl,
+    rtac @{thm arg_cong2[of _ _ _ _ "op ="]},
     (instantiate_tac @{thm APPLY_RSP} ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])),
     rtac reflex_thm,
     atac,
@@ -787,5 +788,19 @@
   end
 *}
 
+text {* the proper way to do it *}
+ML {*
+  fun findabs rty tm =
+    case tm of
+      Abs(_, T, b) =>
+        let
+          val b' = subst_bound ((Free ("x", T)), b);
+          val tys = findabs rty b'
+          val ty = fastype_of tm
+        in if needs_lift rty ty then (ty :: tys) else tys
+        end
+    | f $ a => (findabs rty f) @ (findabs rty a)
+    | _ => []
+*}
 
 end