diff -r ea27275eba9a -r 44045c743bfe IntEx.thy
--- a/IntEx.thy	Tue Nov 24 12:25:04 2009 +0100
+++ b/IntEx.thy	Tue Nov 24 13:46:36 2009 +0100
@@ -195,11 +195,13 @@
   val thy = ProofContext.theory_of ctxt
   val rtrm' = HOLogic.dest_Trueprop rtrm
   val qtrm' = HOLogic.dest_Trueprop qtrm
+  val reg_goal = Syntax.check_term ctxt (REGULARIZE_trm ctxt rtrm' qtrm')
+  val inj_goal = Syntax.check_term ctxt (inj_REPABS ctxt (reg_goal, qtrm'))
 in
   Drule.instantiate' [] 
     [SOME (cterm_of thy rtrm'), 
-     SOME (cterm_of thy (Syntax.check_term ctxt (REGULARIZE_trm ctxt rtrm' qtrm'))),
-     SOME (cterm_of thy (Syntax.check_term ctxt (inj_REPABS ctxt (rtrm', qtrm'))))] 
+     SOME (cterm_of thy reg_goal),
+     SOME (cterm_of thy inj_goal)] 
   @{thm procedure}
 end
 
@@ -215,7 +217,40 @@
 
 lemma "\<forall>i j k. PLUS (PLUS i j) k = PLUS i (PLUS j k)"
 apply(tactic {* procedure_tac @{thm plus_assoc_pre} @{context} 1 *})
-sorry
+thm FORALL_PRS
+prefer 3
+(* phase 1 *)
+apply(subst FORALL_PRS[symmetric])
+apply(tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *})
+apply(subst FORALL_PRS[symmetric])
+apply(tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *})
+apply(subst FORALL_PRS[symmetric])
+apply(tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *})
+apply(subst LAMBDA_PRS)
+apply(tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *})
+apply(fold id_def)
+apply(tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *})
+apply(subst LAMBDA_PRS)
+apply(tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *})
+apply(fold id_def)
+apply(tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *})
+apply(subst LAMBDA_PRS)
+apply(tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *})
+apply(fold id_def)
+apply(tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *})
+(* phase 2 *)
+ML_prf {*
+ val lower = add_lower_defs @{context} @{thm PLUS_def}
+*}
+apply(tactic {* EqSubst.eqsubst_tac @{context} [0] lower 1*})
+apply(tactic {* EqSubst.eqsubst_tac @{context} [0] lower 1*})
+apply(tactic {* EqSubst.eqsubst_tac @{context} [0] lower 1*})
+apply(tactic {* EqSubst.eqsubst_tac @{context} [0] lower 1*})
+(* phase 3 *)
+apply(subst QUOT_TYPE_I_my_int.REPS_same)
+apply(rule refl)
+
+
 
 
 (*