--- a/QuotMain.thy Fri Nov 27 07:16:16 2009 +0100
+++ b/QuotMain.thy Fri Nov 27 08:15:23 2009 +0100
@@ -293,8 +293,7 @@
val rty = Logic.unvarifyT (#rtyp quotdata)
val rel = #rel quotdata
val rel_eqv = #equiv_thm quotdata
- val rel_refl_pre = @{thm EQUIV_REFL} OF [rel_eqv]
- val rel_refl = @{thm spec} OF [MetaSimplifier.rewrite_rule [@{thm REFL_def}] rel_refl_pre]
+ val rel_refl = @{thm EQUIV_REFL} OF [rel_eqv]
in
(rty, rel, rel_refl, rel_eqv)
end
@@ -494,7 +493,7 @@
(ObjectLogic.full_atomize_tac) THEN'
REPEAT_ALL_NEW (FIRST'
[(K (print_tac "start")) THEN' (K no_tac),
- DT ctxt "1" (rtac rel_refl),
+ DT ctxt "1" (FIRST' (map rtac rel_refl)),
DT ctxt "2" atac,
DT ctxt "3" (rtac @{thm universal_twice}),
DT ctxt "4" (rtac @{thm impI} THEN' atac),
@@ -503,7 +502,7 @@
[(@{thm equiv_res_forall} OF [rel_eqv]),
(@{thm equiv_res_exists} OF [rel_eqv])]),
(* For a = b \<longrightarrow> a \<approx> b *)
- DT ctxt "7" (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl),
+ DT ctxt "7" (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' (FIRST' (map rtac rel_refl))),
DT ctxt "8" (rtac @{thm RIGHT_RES_FORALL_REGULAR})
]);
*}
@@ -590,7 +589,7 @@
(rtac @{thm bex_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])),
rtac @{thm move_forall},
rtac @{thm move_exists},
- (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl)
+ (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' FIRST' (map rtac rel_refl))
])
end
*}
@@ -720,12 +719,13 @@
ML {*
-fun quotient_tac quot_thm =
+fun quotient_tac quot_thms =
REPEAT_ALL_NEW (FIRST' [
rtac @{thm FUN_QUOTIENT},
- rtac quot_thm,
+ FIRST' (map rtac quot_thms),
rtac @{thm IDENTITY_QUOTIENT},
(* For functional identity quotients, (op = ---> op =) *)
+ (* TODO: think about the other way around, if we need to shorten the relation *)
CHANGED o (simp_tac (HOL_ss addsimps @{thms id_simps}))
])
*}
@@ -803,7 +803,7 @@
*}
ML {*
-fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms =
+fun r_mk_comb_tac ctxt rty quot_thms rel_refl trans_thm rsp_thms =
(FIRST' [
rtac trans_thm,
LAMBDA_RES_TAC ctxt,
@@ -814,12 +814,12 @@
FIRST' (map rtac rsp_thms),
rtac refl,
(instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN'
- (RANGE [SOLVES' (quotient_tac quot_thm)])),
+ (RANGE [SOLVES' (quotient_tac quot_thms)])),
(APPLY_RSP_TAC rty ctxt THEN'
- (RANGE [SOLVES' (quotient_tac quot_thm), SOLVES' (quotient_tac quot_thm)])),
+ (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)])),
Cong_Tac.cong_tac @{thm cong},
rtac @{thm ext},
- rtac reflex_thm,
+ FIRST' (map rtac rel_refl),
atac,
SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})),
WEAK_LAMBDA_RES_TAC ctxt,
@@ -851,7 +851,7 @@
*)
ML {*
-fun r_mk_comb_tac' ctxt rty quot_thm reflex_thm trans_thm rsp_thms =
+fun r_mk_comb_tac' ctxt rty quot_thms reflex_thm trans_thm rsp_thms =
REPEAT_ALL_NEW (FIRST' [
(K (print_tac "start")) THEN' (K no_tac),
DT ctxt "1" (rtac trans_thm),
@@ -863,9 +863,9 @@
DT ctxt "7" (FIRST' (map rtac rsp_thms)),
DT ctxt "8" (rtac refl),
DT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt
- THEN' (RANGE [SOLVES' (quotient_tac quot_thm)]))),
+ THEN' (RANGE [SOLVES' (quotient_tac quot_thms)]))),
DT ctxt "A" ((APPLY_RSP_TAC rty ctxt THEN'
- (RANGE [SOLVES' (quotient_tac quot_thm), SOLVES' (quotient_tac quot_thm)]))),
+ (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)]))),
DT ctxt "B" (Cong_Tac.cong_tac @{thm cong}),
DT ctxt "C" (rtac @{thm ext}),
DT ctxt "D" (rtac reflex_thm),
@@ -898,7 +898,7 @@
val llhs = Syntax.check_term lthy lhs;
val eq = Logic.mk_equals (llhs, rhs);
val ceq = cterm_of (ProofContext.theory_of lthy') eq;
- val sctxt = HOL_ss addsimps (absrep :: @{thms fun_map.simps id_simps});
+ val sctxt = HOL_ss addsimps (@{thms fun_map.simps id_simps} @ absrep);
val t = Goal.prove_internal [] ceq (fn _ => simp_tac sctxt 1)
val t_id = MetaSimplifier.rewrite_rule @{thms id_simps} t;
in
@@ -950,7 +950,7 @@
*}
ML {*
-fun lambda_prs_conv1 ctxt quot ctrm =
+fun lambda_prs_conv1 ctxt quot_thms ctrm =
case (term_of ctrm) of ((Const (@{const_name "fun_map"}, _) $ r1 $ a2) $ (Abs _)) =>
let
val (_, [ty_b, ty_a]) = dest_Type (fastype_of r1);
@@ -962,7 +962,7 @@
val lpi = Drule.instantiate' tyinst tinst @{thm LAMBDA_PRS};
val tac =
(compose_tac (false, lpi, 2)) THEN_ALL_NEW
- (quotient_tac quot);
+ (quotient_tac quot_thms);
val gc = Drule.strip_imp_concl (cprop_of lpi);
val t = Goal.prove_internal [] gc (fn _ => tac 1)
val te = @{thm eq_reflection} OF [t]
@@ -1003,16 +1003,18 @@
*}
ML {*
-fun clean_tac lthy quot defs reps_same absrep aps =
+fun clean_tac lthy quot defs aps =
let
val lower = flat (map (add_lower_defs lthy) defs)
+ val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot
+ val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot
val aps_thms = map (applic_prs lthy absrep) aps
in
- EVERY' [TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot),
+ EVERY' [TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot),
lambda_prs_tac lthy quot,
TRY o REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] aps_thms),
TRY o REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] lower),
- simp_tac (HOL_ss addsimps [reps_same])]
+ simp_tac (HOL_ss addsimps reps_same)]
end
*}
@@ -1114,7 +1116,7 @@
ML {*
(* FIXME/TODO should only get as arguments the rthm like procedure_tac *)
-fun lift_tac lthy rthm rel_eqv rel_refl rty quot trans2 rsp_thms reps_same absrep defs =
+fun lift_tac lthy rthm rel_eqv rty quot trans2 rsp_thms defs =
ObjectLogic.full_atomize_tac
THEN' gen_frees_tac lthy
THEN' Subgoal.FOCUS (fn {context, concl, ...} =>
@@ -1122,13 +1124,14 @@
val rthm' = atomize_thm rthm
val rule = procedure_inst context (prop_of rthm') (term_of concl)
val aps = find_aps (prop_of rthm') (term_of concl)
+ val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) rel_eqv
in
EVERY1
[rtac rule,
RANGE [rtac rthm',
- regularize_tac lthy [rel_eqv] rel_refl,
+ regularize_tac lthy rel_eqv rel_refl,
REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms),
- clean_tac lthy quot defs reps_same absrep aps]]
+ clean_tac lthy quot defs aps]]
end) lthy
*}