diff -r 5a9bdf81672d -r 3f3927f793d4 QuotMain.thy --- 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 \ a \ 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 *}