--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Sun Apr 27 19:32:55 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Apr 28 00:54:30 2014 +0200
@@ -1179,8 +1179,6 @@
fun mk_rel_inject_thm ((ctr_def', cxIn), (_, cyIn)) =
mk_rel_thm (unfold_thms lthy @{thms eq_sym_Unity_conv}) [ctr_def'] cxIn cyIn;
- val rel_inject_thms = map mk_rel_inject_thm (op ~~ rel_infos);
-
fun mk_half_rel_distinct_thm ((xctr_def', cxIn), (yctr_def', cyIn)) =
mk_rel_thm (fn thm => thm RS @{thm eq_False[THEN iffD1]}) [xctr_def', yctr_def']
cxIn cyIn;
@@ -1189,6 +1187,7 @@
flip_rels lthy live thm
RS (rel_flip RS sym RS @{thm arg_cong[of _ _ Not]} RS iffD2);
+ val rel_inject_thms = map mk_rel_inject_thm (op ~~ rel_infos);
val half_rel_distinct_thmss =
map (map mk_half_rel_distinct_thm) (mk_half_pairss rel_infos);
val other_half_rel_distinct_thmss =
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Sun Apr 27 19:32:55 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Mon Apr 28 00:54:30 2014 +0200
@@ -42,7 +42,7 @@
@{thms UN_empty UN_insert Un_empty_left Un_empty_right Un_iff UN_simps(10) UN_iff
Union_Un_distrib image_iff o_apply map_prod_simp
mem_Collect_eq prod_set_simps map_sum.simps sum_set_simps};
-val sumprod_thms_rel = @{thms rel_prod_apply rel_sum_simps id_apply};
+val sumprod_thms_rel = @{thms rel_sum_simps rel_prod_apply prod.inject id_apply conj_assoc};
fun hhf_concl_conv cv ctxt ct =
(case Thm.term_of ct of
@@ -82,7 +82,7 @@
fun mk_inject_tac ctxt ctr_def ctor_inject abs_inject =
unfold_thms_tac ctxt [ctr_def] THEN
HEADGOAL (rtac (ctor_inject RS ssubst)) THEN
- unfold_thms_tac ctxt (abs_inject :: @{thms sum.inject Pair_eq conj_assoc}) THEN
+ unfold_thms_tac ctxt (abs_inject :: @{thms sum.inject prod.inject conj_assoc}) THEN
HEADGOAL (rtac refl);
val rec_unfold_thms =
@@ -155,8 +155,7 @@
SELECT_GOAL (unfold_thms_tac ctxt (pre_rel_def :: fp_abs_inverse :: abs_inverse :: dtor_ctor ::
sels @ sumprod_thms_rel @ @{thms o_apply vimage2p_def})) THEN'
(atac ORELSE' REPEAT o etac conjE THEN'
- full_simp_tac
- (ss_only (@{thm prod.inject} :: no_refl discs @ rel_eqs @ more_simp_thms) ctxt) THEN'
+ full_simp_tac (ss_only (no_refl discs @ rel_eqs @ more_simp_thms) ctxt) THEN'
REPEAT o etac conjE THEN_MAYBE' REPEAT o hyp_subst_tac ctxt THEN'
REPEAT o (resolve_tac [refl, conjI] ORELSE' atac));
--- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Sun Apr 27 19:32:55 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Mon Apr 28 00:54:30 2014 +0200
@@ -288,7 +288,7 @@
REPEAT_DETERM_N (length rel_congs) o rtac @{thm relcompp_in_rel},
rtac (rel_OO RS sym RS @{thm eq_refl} RS @{thm predicate2D}),
etac @{thm relcompE},
- REPEAT_DETERM o dtac Pair_eqD,
+ REPEAT_DETERM o dtac prod_injectD,
etac conjE, hyp_subst_tac ctxt,
REPEAT_DETERM o etac allE, rtac @{thm relcomppI},
etac mp, atac, etac mp, atac]) (rel_congs ~~ rel_OOs)] 1;
@@ -607,7 +607,7 @@
rtac (mk_sum_caseN n i) THEN' rtac (mk_sum_caseN n i RS trans)),
rtac (map_comp_id RS trans), rtac (map_cong0 OF replicate m refl),
EVERY' (map3 (fn i' => fn to_sbd_inj => fn from_to_sbd =>
- DETERM o EVERY' [rtac trans, rtac o_apply, rtac Pair_eqI, rtac conjI,
+ DETERM o EVERY' [rtac trans, rtac o_apply, rtac prod_injectI, rtac conjI,
rtac trans, rtac @{thm Shift_def},
rtac equalityI, rtac subsetI, etac thin_rl,
REPEAT_DETERM o eresolve_tac [CollectE, @{thm UN_E}], dtac length_Lev', dtac asm_rl,
@@ -969,7 +969,7 @@
dtac set_rev_mp, etac @{thm image_mono}, etac imageE,
dtac @{thm ssubst_mem[OF pair_collapse]},
REPEAT_DETERM o eresolve_tac (CollectE :: conjE ::
- @{thms case_prodE iffD1[OF Pair_eq, elim_format]}),
+ @{thms case_prodE iffD1[OF prod.inject, elim_format]}),
hyp_subst_tac ctxt,
dtac (in_Jrel RS iffD1),
dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE,
@@ -984,8 +984,8 @@
rtac map_cong0, REPEAT_DETERM_N m o rtac @{thm fun_cong[OF comp_id]},
EVERY' (map (fn in_Jrel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,
dtac @{thm ssubst_mem[OF pair_collapse]},
- REPEAT_DETERM o
- eresolve_tac (CollectE :: conjE :: @{thms case_prodE iffD1[OF Pair_eq, elim_format]}),
+ REPEAT_DETERM o eresolve_tac (CollectE :: conjE ::
+ @{thms case_prodE iffD1[OF prod.inject, elim_format]}),
hyp_subst_tac ctxt, dtac (in_Jrel RS iffD1),
dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE, atac]) in_Jrels),
atac]]
--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Sun Apr 27 19:32:55 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Mon Apr 28 00:54:30 2014 +0200
@@ -204,7 +204,7 @@
(rtac (worel RS (@{thm wo_rel.worec_fixpoint} RS fun_cong)) THEN' rtac iffD2 THEN'
rtac meta_eq_to_obj_eq THEN' rtac (worel RS @{thm wo_rel.adm_wo_def}) THEN'
REPEAT_DETERM_N 3 o rtac allI THEN' rtac impI THEN'
- CONJ_WRAP_GEN' (EVERY' [rtac Pair_eqI, rtac conjI]) minH_tac in_congs) 1
+ CONJ_WRAP_GEN' (EVERY' [rtac prod_injectI, rtac conjI]) minH_tac in_congs) 1
end;
fun mk_min_algs_mono_tac ctxt min_algs = EVERY' [rtac relChainD, rtac allI, rtac allI, rtac impI,
@@ -679,7 +679,7 @@
dtac set_rev_mp, etac @{thm image_mono}, etac imageE,
dtac @{thm ssubst_mem[OF pair_collapse]},
REPEAT_DETERM o eresolve_tac (CollectE :: conjE ::
- @{thms case_prodE iffD1[OF Pair_eq, elim_format]}),
+ @{thms case_prodE iffD1[OF prod.inject, elim_format]}),
hyp_subst_tac ctxt,
dtac (in_Irel RS iffD1), dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE,
TRY o
@@ -693,8 +693,8 @@
REPEAT_DETERM_N m o rtac @{thm fun_cong[OF comp_id]},
EVERY' (map (fn in_Irel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,
dtac @{thm ssubst_mem[OF pair_collapse]},
- REPEAT_DETERM o
- eresolve_tac (CollectE :: conjE :: @{thms case_prodE iffD1[OF Pair_eq, elim_format]}),
+ REPEAT_DETERM o eresolve_tac (CollectE :: conjE ::
+ @{thms case_prodE iffD1[OF prod.inject, elim_format]}),
hyp_subst_tac ctxt,
dtac (in_Irel RS iffD1), dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE, atac])
in_Irels),
--- a/src/HOL/Tools/BNF/bnf_util.ML Sun Apr 27 19:32:55 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML Mon Apr 28 00:54:30 2014 +0200
@@ -123,8 +123,8 @@
val mk_ordLeq_csum: int -> int -> thm -> thm
val mk_UnIN: int -> int -> thm
- val Pair_eqD: thm
- val Pair_eqI: thm
+ val prod_injectD: thm
+ val prod_injectI: thm
val ctrans: thm
val id_apply: thm
val meta_mp: thm
@@ -518,8 +518,8 @@
fun mk_sym thm = thm RS sym;
(*TODO: antiquote heavily used theorems once*)
-val Pair_eqD = @{thm iffD1[OF Pair_eq]};
-val Pair_eqI = @{thm iffD2[OF Pair_eq]};
+val prod_injectD = @{thm iffD1[OF prod.inject]};
+val prod_injectI = @{thm iffD2[OF prod.inject]};
val ctrans = @{thm ordLeq_transitive};
val id_apply = @{thm id_apply};
val meta_mp = @{thm meta_mp};