--- a/src/HOL/Tools/set_comprehension_pointfree.ML Tue Feb 10 14:29:36 2015 +0100
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML Tue Feb 10 14:48:26 2015 +0100
@@ -314,96 +314,99 @@
val collectI' = @{lemma "\<not> P a ==> a \<notin> {x. P x}" by auto}
val collectE' = @{lemma "a \<notin> {x. P x} ==> (\<not> P a ==> Q) ==> Q" by auto}
-fun elim_Collect_tac ctxt = dresolve_tac @{thms iffD1 [OF mem_Collect_eq]}
- THEN' (REPEAT_DETERM o (eresolve_tac @{thms exE}))
- THEN' REPEAT_DETERM o eresolve_tac @{thms conjE}
+fun elim_Collect_tac ctxt =
+ dresolve_tac ctxt @{thms iffD1 [OF mem_Collect_eq]}
+ THEN' (REPEAT_DETERM o (eresolve_tac ctxt @{thms exE}))
+ THEN' REPEAT_DETERM o eresolve_tac ctxt @{thms conjE}
THEN' TRY o hyp_subst_tac ctxt;
-fun intro_image_tac ctxt = resolve_tac @{thms image_eqI}
- THEN' (REPEAT_DETERM1 o
- (resolve_tac @{thms refl}
- ORELSE' resolve_tac @{thms arg_cong2 [OF refl, where f = "op =", OF prod.case, THEN iffD2]}
+fun intro_image_tac ctxt =
+ resolve_tac ctxt @{thms image_eqI}
+ THEN' (REPEAT_DETERM1 o
+ (resolve_tac ctxt @{thms refl}
+ ORELSE' resolve_tac ctxt @{thms arg_cong2 [OF refl, where f = "op =", OF prod.case, THEN iffD2]}
ORELSE' CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1
(HOLogic.Trueprop_conv
(HOLogic.eq_conv Conv.all_conv (Conv.rewr_conv (mk_meta_eq case_prod_distrib)))))) ctxt)))
-fun elim_image_tac ctxt = eresolve_tac @{thms imageE}
+fun elim_image_tac ctxt =
+ eresolve_tac ctxt @{thms imageE}
THEN' REPEAT_DETERM o CHANGED o
(TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms split_paired_all prod.case})
- THEN' REPEAT_DETERM o eresolve_tac @{thms Pair_inject}
+ THEN' REPEAT_DETERM o eresolve_tac ctxt @{thms Pair_inject}
THEN' TRY o hyp_subst_tac ctxt)
fun tac1_of_formula ctxt (Int (fm1, fm2)) =
- TRY o eresolve_tac @{thms conjE}
- THEN' resolve_tac @{thms IntI}
+ TRY o eresolve_tac ctxt @{thms conjE}
+ THEN' resolve_tac ctxt @{thms IntI}
THEN' (fn i => tac1_of_formula ctxt fm2 (i + 1))
THEN' tac1_of_formula ctxt fm1
| tac1_of_formula ctxt (Un (fm1, fm2)) =
- eresolve_tac @{thms disjE} THEN' resolve_tac @{thms UnI1}
+ eresolve_tac ctxt @{thms disjE} THEN' resolve_tac ctxt @{thms UnI1}
THEN' tac1_of_formula ctxt fm1
- THEN' resolve_tac @{thms UnI2}
+ THEN' resolve_tac ctxt @{thms UnI2}
THEN' tac1_of_formula ctxt fm2
| tac1_of_formula ctxt (Atom _) =
REPEAT_DETERM1 o (assume_tac ctxt
- ORELSE' resolve_tac @{thms SigmaI}
- ORELSE' ((resolve_tac @{thms CollectI} ORELSE' resolve_tac [collectI']) THEN'
+ ORELSE' resolve_tac ctxt @{thms SigmaI}
+ ORELSE' ((resolve_tac ctxt @{thms CollectI} ORELSE' resolve_tac ctxt [collectI']) THEN'
TRY o simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm prod.case}]))
- ORELSE' ((resolve_tac @{thms vimageI2} ORELSE' resolve_tac [vimageI2']) THEN'
+ ORELSE' ((resolve_tac ctxt @{thms vimageI2} ORELSE' resolve_tac ctxt [vimageI2']) THEN'
TRY o simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm prod.case}]))
- ORELSE' (resolve_tac @{thms image_eqI} THEN'
+ ORELSE' (resolve_tac ctxt @{thms image_eqI} THEN'
(REPEAT_DETERM o
- (resolve_tac @{thms refl}
- ORELSE' resolve_tac @{thms arg_cong2[OF refl, where f = "op =", OF prod.case, THEN iffD2]})))
- ORELSE' resolve_tac @{thms UNIV_I}
- ORELSE' resolve_tac @{thms iffD2[OF Compl_iff]}
+ (resolve_tac ctxt @{thms refl}
+ ORELSE' resolve_tac ctxt @{thms arg_cong2[OF refl, where f = "op =", OF prod.case, THEN iffD2]})))
+ ORELSE' resolve_tac ctxt @{thms UNIV_I}
+ ORELSE' resolve_tac ctxt @{thms iffD2[OF Compl_iff]}
ORELSE' assume_tac ctxt)
fun tac2_of_formula ctxt (Int (fm1, fm2)) =
- TRY o eresolve_tac @{thms IntE}
- THEN' TRY o resolve_tac @{thms conjI}
+ TRY o eresolve_tac ctxt @{thms IntE}
+ THEN' TRY o resolve_tac ctxt @{thms conjI}
THEN' (fn i => tac2_of_formula ctxt fm2 (i + 1))
THEN' tac2_of_formula ctxt fm1
| tac2_of_formula ctxt (Un (fm1, fm2)) =
- eresolve_tac @{thms UnE} THEN' resolve_tac @{thms disjI1}
+ eresolve_tac ctxt @{thms UnE} THEN' resolve_tac ctxt @{thms disjI1}
THEN' tac2_of_formula ctxt fm1
- THEN' resolve_tac @{thms disjI2}
+ THEN' resolve_tac ctxt @{thms disjI2}
THEN' tac2_of_formula ctxt fm2
| tac2_of_formula ctxt (Atom _) =
REPEAT_DETERM o
(assume_tac ctxt
- ORELSE' dresolve_tac @{thms iffD1[OF mem_Sigma_iff]}
- ORELSE' eresolve_tac @{thms conjE}
- ORELSE' ((eresolve_tac @{thms CollectE} ORELSE' eresolve_tac [collectE']) THEN'
+ ORELSE' dresolve_tac ctxt @{thms iffD1[OF mem_Sigma_iff]}
+ ORELSE' eresolve_tac ctxt @{thms conjE}
+ ORELSE' ((eresolve_tac ctxt @{thms CollectE} ORELSE' eresolve_tac ctxt [collectE']) THEN'
TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm prod.case}]) THEN'
- REPEAT_DETERM o eresolve_tac @{thms Pair_inject} THEN' TRY o hyp_subst_tac ctxt THEN'
- TRY o resolve_tac @{thms refl})
- ORELSE' (eresolve_tac @{thms imageE}
+ REPEAT_DETERM o eresolve_tac ctxt @{thms Pair_inject} THEN' TRY o hyp_subst_tac ctxt THEN'
+ TRY o resolve_tac ctxt @{thms refl})
+ ORELSE' (eresolve_tac ctxt @{thms imageE}
THEN' (REPEAT_DETERM o CHANGED o
(TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms split_paired_all prod.case})
- THEN' REPEAT_DETERM o eresolve_tac @{thms Pair_inject}
- THEN' TRY o hyp_subst_tac ctxt THEN' TRY o resolve_tac @{thms refl})))
- ORELSE' eresolve_tac @{thms ComplE}
- ORELSE' ((eresolve_tac @{thms vimageE} ORELSE' eresolve_tac [vimageE'])
+ THEN' REPEAT_DETERM o eresolve_tac ctxt @{thms Pair_inject}
+ THEN' TRY o hyp_subst_tac ctxt THEN' TRY o resolve_tac ctxt @{thms refl})))
+ ORELSE' eresolve_tac ctxt @{thms ComplE}
+ ORELSE' ((eresolve_tac ctxt @{thms vimageE} ORELSE' eresolve_tac ctxt [vimageE'])
THEN' TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm prod.case}])
- THEN' TRY o hyp_subst_tac ctxt THEN' TRY o resolve_tac @{thms refl}))
+ THEN' TRY o hyp_subst_tac ctxt THEN' TRY o resolve_tac ctxt @{thms refl}))
fun tac ctxt fm =
let
- val subset_tac1 = resolve_tac @{thms subsetI}
+ val subset_tac1 = resolve_tac ctxt @{thms subsetI}
THEN' elim_Collect_tac ctxt
THEN' intro_image_tac ctxt
THEN' tac1_of_formula ctxt fm
- val subset_tac2 = resolve_tac @{thms subsetI}
+ val subset_tac2 = resolve_tac ctxt @{thms subsetI}
THEN' elim_image_tac ctxt
- THEN' resolve_tac @{thms iffD2[OF mem_Collect_eq]}
- THEN' REPEAT_DETERM o resolve_tac @{thms exI}
- THEN' (TRY o REPEAT_ALL_NEW (resolve_tac @{thms conjI}))
- THEN' (K (TRY (FIRSTGOAL ((TRY o hyp_subst_tac ctxt) THEN' resolve_tac @{thms refl}))))
+ THEN' resolve_tac ctxt @{thms iffD2[OF mem_Collect_eq]}
+ THEN' REPEAT_DETERM o resolve_tac ctxt @{thms exI}
+ THEN' (TRY o REPEAT_ALL_NEW (resolve_tac ctxt @{thms conjI}))
+ THEN' (K (TRY (FIRSTGOAL ((TRY o hyp_subst_tac ctxt) THEN' resolve_tac ctxt @{thms refl}))))
THEN' (fn i => EVERY (rev (map_index (fn (j, f) =>
- REPEAT_DETERM (eresolve_tac @{thms IntE} (i + j)) THEN
+ REPEAT_DETERM (eresolve_tac ctxt @{thms IntE} (i + j)) THEN
tac2_of_formula ctxt f (i + j)) (strip_Int fm))))
in
- resolve_tac @{thms subset_antisym} THEN' subset_tac1 THEN' subset_tac2
+ resolve_tac ctxt @{thms subset_antisym} THEN' subset_tac1 THEN' subset_tac2
end;
@@ -430,14 +433,14 @@
fun is_eq th = is_some (try (HOLogic.dest_eq o HOLogic.dest_Trueprop) (prop_of th))
val unfold_thms = @{thms split_paired_all mem_Collect_eq prod.case}
fun tac ctxt =
- resolve_tac @{thms set_eqI}
+ resolve_tac ctxt @{thms set_eqI}
THEN' simp_tac (put_simpset HOL_basic_ss ctxt addsimps unfold_thms)
- THEN' resolve_tac @{thms iffI}
- THEN' REPEAT_DETERM o resolve_tac @{thms exI}
- THEN' resolve_tac @{thms conjI} THEN' resolve_tac @{thms refl} THEN' assume_tac ctxt
- THEN' REPEAT_DETERM o eresolve_tac @{thms exE}
- THEN' eresolve_tac @{thms conjE}
- THEN' REPEAT_DETERM o eresolve_tac @{thms Pair_inject}
+ THEN' resolve_tac ctxt @{thms iffI}
+ THEN' REPEAT_DETERM o resolve_tac ctxt @{thms exI}
+ THEN' resolve_tac ctxt @{thms conjI} THEN' resolve_tac ctxt @{thms refl} THEN' assume_tac ctxt
+ THEN' REPEAT_DETERM o eresolve_tac ctxt @{thms exE}
+ THEN' eresolve_tac ctxt @{thms conjE}
+ THEN' REPEAT_DETERM o eresolve_tac ctxt @{thms Pair_inject}
THEN' Subgoal.FOCUS (fn {prems, ...} =>
(* FIXME inner context!? *)
simp_tac (put_simpset HOL_basic_ss ctxt addsimps (filter is_eq prems)) 1) ctxt