--- a/IntEx.thy	Fri Nov 20 13:03:01 2009 +0100
+++ b/IntEx.thy	Sat Nov 21 02:49:39 2009 +0100
@@ -8,10 +8,13 @@
   "intrel (x, y) (u, v) = (x + v = u + y)"
 
 quotient my_int = "nat \<times> nat" / intrel
+  and    my_int' = "nat \<times> nat" / intrel
   apply(unfold EQUIV_def)
   apply(auto simp add: mem_def expand_fun_eq)
   done
 
+thm my_int_equiv
+
 print_theorems
 print_quotients
 
@@ -98,6 +101,7 @@
 term LE
 thm LE_def
 
+
 definition
   LESS :: "my_int \<Rightarrow> my_int \<Rightarrow> bool"
 where
@@ -149,12 +153,33 @@
   val test = lift_thm_my_int @{context} @{thm plus_sym_pre} 
 *}
 
-
 ML {*
-  val aqtrm = HOLogic.dest_Trueprop (prop_of (atomize_thm test))
-  val artrm = HOLogic.dest_Trueprop (prop_of (atomize_thm @{thm plus_sym_pre})) 
+  val aqtrm = (prop_of (atomize_thm test))
+  val artrm = (prop_of (atomize_thm @{thm plus_sym_pre})) 
+  val reg_artm = mk_REGULARIZE_goal @{context} artrm aqtrm
 *}
 
+prove {* reg_artm  *}
+apply(tactic {* ObjectLogic.full_atomize_tac 1 *})
+apply(tactic {* REGULARIZE_tac' @{context} @{thm "TrueI"} @{thm my_int_equiv} *})
+done
+
+(*
+ML {*
+fun inj_REPABS lthy rtrm qtrm =
+  case (rtrm, qtrm) of
+    (Abs (x, T, t), Abs (x', T', t')) =>
+    if T = T'
+    then Abs (x, T, inj_REPABS lthy t t')
+    else 
+      let 
+         
+      in
+
+      end
+  | _ => rtrm
+*}
+*)
 
 lemma plus_assoc_pre:
   shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)"
@@ -164,8 +189,17 @@
   apply (simp)
   done
 
-ML {* lift_thm_my_int @{context} @{thm plus_assoc_pre} *}
+ML {* val test2 = lift_thm_my_int @{context} @{thm plus_assoc_pre} *}
 
+ML {*
+  val aqtrm = (prop_of (atomize_thm test2))
+  val artrm = (prop_of (atomize_thm @{thm plus_assoc_pre})) 
+*}
+
+prove {* mk_REGULARIZE_goal @{context} artrm aqtrm  *}
+apply(tactic {* ObjectLogic.full_atomize_tac 1 *})
+apply(tactic {* REGULARIZE_tac' @{context} @{thm "TrueI"} @{thm my_int_equiv} *})
+done