--- a/IntEx.thy Tue Nov 24 13:46:36 2009 +0100
+++ b/IntEx.thy Tue Nov 24 14:16:57 2009 +0100
@@ -215,41 +215,53 @@
end)
*}
+ML {*
+val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} @{typ "my_int"}
+val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int"
+*}
+
+(* FIXME: allex_prs and lambda_prs can be one function *)
+
+ML {*
+fun allex_prs_tac lthy quot =
+ (EqSubst.eqsubst_tac lthy [0] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]})
+ THEN' (quotient_tac quot);
+*}
+
+ML {*
+fun lambda_prs_tac lthy quot =
+ (EqSubst.eqsubst_tac lthy [0] @{thms LAMBDA_PRS}
+ THEN' (RANGE [quotient_tac quot, quotient_tac quot]));
+*}
+
+ML {*
+fun clean_tac lthy quot defs reps_same =
+ let
+ val lower = flat (map (add_lower_defs lthy) defs)
+ in
+ (REPEAT_ALL_NEW (allex_prs_tac lthy quot)) THEN'
+ (REPEAT_ALL_NEW (lambda_prs_tac lthy quot)) THEN'
+ (REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] lower)) THEN'
+ (simp_tac (HOL_ss addsimps [reps_same]))
+ end
+*}
+
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 *})
-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 *})
+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 *})
+apply(tactic {* clean_tac @{context} quot @{thms PLUS_def} reps_same 1 *})
+done
+
+apply(tactic {* REPEAT_ALL_NEW (allex_prs_tac @{context} quot) 1 *})
+apply(tactic {* REPEAT_ALL_NEW (lambda_prs_tac @{context} quot) 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)
-
+apply(tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] lower) 1*})
+apply(tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *})
+done