# HG changeset patch # User Cezary Kaliszyk # Date 1259343524 -3600 # Node ID 1f2c8be84be7fd31aaff32bd984cea4933d514d6 # Parent 2b64936f8fab293fdd0c5ad3802639c5d36ec751# Parent dcfe009c98aa7da00d1520d18d7b228a282ea7d0 Merge diff -r 2b64936f8fab -r 1f2c8be84be7 FSet.thy --- a/FSet.thy Fri Nov 27 18:38:09 2009 +0100 +++ b/FSet.thy Fri Nov 27 18:38:44 2009 +0100 @@ -347,10 +347,14 @@ apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *}) apply(tactic {* regularize_tac @{context} [rel_eqv] [rel_refl] 1 *}) prefer 2 -apply (tactic {* clean_tac @{context} [quot] defs [(@{typ "('a list \ bool)"},@{typ "('a fset \ bool)"})] 1 *}) +apply (tactic {* clean_tac @{context} [quot] defs + [(@{typ "('a list \ bool)"},@{typ "('a fset \ bool)"})] 1 *}) apply(tactic {* r_mk_comb_tac' @{context} rty [quot] rel_refl trans2 rsp_thms 1*}) done + + + quotient_def fset_rec::"'a \ ('b \ 'b fset \ 'a \ 'a) \ 'b fset \ 'a" where diff -r 2b64936f8fab -r 1f2c8be84be7 QuotMain.thy --- a/QuotMain.thy Fri Nov 27 18:38:09 2009 +0100 +++ b/QuotMain.thy Fri Nov 27 18:38:44 2009 +0100 @@ -505,7 +505,7 @@ (ObjectLogic.full_atomize_tac) THEN' REPEAT_ALL_NEW (FIRST' [(K (print_tac "start")) THEN' (K no_tac), - DT ctxt "1" (FIRST' (map rtac rel_refl)), + DT ctxt "1" (resolve_tac rel_refl), DT ctxt "2" atac, DT ctxt "3" (rtac @{thm universal_twice}), DT ctxt "4" (rtac @{thm impI} THEN' atac), @@ -514,7 +514,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' (FIRST' (map rtac rel_refl))), + DT ctxt "7" (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' (resolve_tac rel_refl)), DT ctxt "8" (rtac @{thm RIGHT_RES_FORALL_REGULAR}) ]); *} @@ -572,11 +572,10 @@ (* FIXME: OPTION_EQUIV, PAIR_EQUIV, ... *) ML {* fun equiv_tac rel_eqvs = - REPEAT_ALL_NEW(FIRST' [ - FIRST' (map rtac rel_eqvs), - rtac @{thm IDENTITY_EQUIV}, - rtac @{thm LIST_EQUIV} - ]) + REPEAT_ALL_NEW (FIRST' + [resolve_tac rel_eqvs, + rtac @{thm IDENTITY_EQUIV}, + rtac @{thm LIST_EQUIV}]) *} ML {* @@ -593,16 +592,15 @@ (ObjectLogic.full_atomize_tac) THEN' (simp_tac ((Simplifier.context ctxt empty_ss) addsimps subs)) THEN' - REPEAT_ALL_NEW (FIRST' [ - (rtac @{thm RIGHT_RES_FORALL_REGULAR}), - (rtac @{thm LEFT_RES_EXISTS_REGULAR}), - (resolve_tac (Inductive.get_monos ctxt)), - (rtac @{thm ball_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])), - (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' FIRST' (map rtac rel_refl)) - ]) + REPEAT_ALL_NEW (FIRST' + [(rtac @{thm RIGHT_RES_FORALL_REGULAR}), + (rtac @{thm LEFT_RES_EXISTS_REGULAR}), + (resolve_tac (Inductive.get_monos ctxt)), + (rtac @{thm ball_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])), + (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' (resolve_tac rel_refl))]) end *} @@ -732,14 +730,13 @@ ML {* fun quotient_tac quot_thms = - REPEAT_ALL_NEW (FIRST' [ - rtac @{thm FUN_QUOTIENT}, - 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})) - ]) + REPEAT_ALL_NEW (FIRST' + [rtac @{thm FUN_QUOTIENT}, + resolve_tac 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}))]) *} ML {* @@ -817,21 +814,21 @@ ML {* fun r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms = (FIRST' [ - FIRST' (map rtac trans2), + resolve_tac trans2, LAMBDA_RES_TAC ctxt, rtac @{thm RES_FORALL_RSP}, ball_rsp_tac ctxt, rtac @{thm RES_EXISTS_RSP}, bex_rsp_tac ctxt, - FIRST' (map rtac rsp_thms), - rtac refl, + resolve_tac rsp_thms, + rtac @{thm refl}, (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [SOLVES' (quotient_tac quot_thms)])), (APPLY_RSP_TAC rty ctxt THEN' (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)])), Cong_Tac.cong_tac @{thm cong}, rtac @{thm ext}, - FIRST' (map rtac rel_refl), + resolve_tac rel_refl, atac, SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})), WEAK_LAMBDA_RES_TAC ctxt, @@ -863,24 +860,24 @@ *) ML {* -fun r_mk_comb_tac' ctxt rty quot_thms reflex_thm trans_thm rsp_thms = +fun r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms = REPEAT_ALL_NEW (FIRST' [ (K (print_tac "start")) THEN' (K no_tac), - DT ctxt "1" (rtac trans_thm), + DT ctxt "1" (resolve_tac trans2), DT ctxt "2" (LAMBDA_RES_TAC ctxt), DT ctxt "3" (rtac @{thm RES_FORALL_RSP}), DT ctxt "4" (ball_rsp_tac ctxt), DT ctxt "5" (rtac @{thm RES_EXISTS_RSP}), DT ctxt "6" (bex_rsp_tac ctxt), - DT ctxt "7" (FIRST' (map rtac rsp_thms)), - DT ctxt "8" (rtac refl), + DT ctxt "7" (resolve_tac rsp_thms), + DT ctxt "8" (rtac @{thm refl}), DT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [SOLVES' (quotient_tac quot_thms)]))), DT ctxt "A" ((APPLY_RSP_TAC rty ctxt THEN' (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), + DT ctxt "D" (resolve_tac rel_refl), DT ctxt "E" (atac), DT ctxt "F" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))), DT ctxt "G" (WEAK_LAMBDA_RES_TAC ctxt), @@ -938,7 +935,7 @@ ML {* fun allex_prs_tac lthy quot = (EqSubst.eqsubst_tac lthy [0] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]}) - THEN' (quotient_tac quot); + THEN' (quotient_tac quot) *} ML {*