diff -r 1f2c8be84be7 -r 2f0ad33f0241 IntEx.thy
--- a/IntEx.thy	Fri Nov 27 18:38:44 2009 +0100
+++ b/IntEx.thy	Sat Nov 28 02:54:24 2009 +0100
@@ -140,13 +140,46 @@
 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int"; *}
 ML {* val consts = lookup_quot_consts defs *}
 
-ML {*
-fun lift_tac_fset lthy t =
-  lift_tac lthy t [rel_eqv] rty [quot] rsp_thms defs
-*}
+ML {* fun lift_tac_intex lthy t = lift_tac lthy t [rel_eqv] rty [quot] rsp_thms defs *}
+
+
+ML {* fun r_mk_comb_tac_intex lthy = r_mk_comb_tac' lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
+ML {* fun all_r_mk_comb_tac_intex lthy = all_r_mk_comb_tac lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
+
+
+lemma cheat: "P" sorry
 
 lemma "PLUS a b = PLUS b a"
-by (tactic {* lift_tac_fset @{context} @{thm plus_sym_pre} 1 *})
+apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *})
+apply(tactic {* regularize_tac @{context} [rel_eqv] [rel_refl] 1 *})
+prefer 2
+ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
+ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *}
+apply(tactic {* clean_tac @{context} [quot] defs aps 1 *})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* all_r_mk_comb_tac_intex @{context} 1*})
+done
 
 lemma plus_assoc_pre:
   shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)"
@@ -157,8 +190,13 @@
   done
 
 lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)"
-by (tactic {* lift_tac_fset @{context} @{thm plus_assoc_pre} 1 *})
-
+apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *})
+apply(tactic {* regularize_tac @{context} [rel_eqv] [rel_refl] 1 *})
+apply(tactic {* all_r_mk_comb_tac_intex @{context} 1*}) 
+ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
+ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *}
+apply(tactic {* clean_tac @{context} [quot] defs aps 1 *})
+done
 
 lemma ho_tst: "foldl my_plus x [] = x"
 apply simp
@@ -171,7 +209,7 @@
 sorry
 
 lemma "foldl PLUS x [] = x"
-apply (tactic {* lift_tac_fset @{context} @{thm ho_tst} 1 *})
+apply (tactic {* lift_tac_intex @{context} @{thm ho_tst} 1 *})
 apply (simp_all only: map_prs foldl_prs)
 sorry
 
@@ -191,8 +229,11 @@
 lemma "PLUS (PLUS i j) k = PLUS i (PLUS j k)"
 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *})
 apply(tactic {* regularize_tac @{context} [rel_eqv] [rel_refl] 1 *})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty [quot] [rel_refl] [trans2] rsp_thms) 1 *})
-oops
+apply(tactic {* all_r_mk_comb_tac_intex @{context} 1*}) 
+ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
+ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *}
+apply(tactic {* clean_tac @{context} [quot] defs aps 1 *})
+done
 
 
 (*