--- a/src/HOL/Codatatype/Tools/bnf_comp_tactics.ML Fri Sep 21 03:41:10 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_comp_tactics.ML Fri Sep 21 11:44:55 2012 +0200
@@ -56,7 +56,6 @@
val o_eq_dest_lhs = @{thm o_eq_dest_lhs};
val ordIso_transitive = @{thm ordIso_transitive};
val ordLeq_csum2 = @{thm ordLeq_csum2};
-val set_mp = @{thm set_mp};
val subset_UNIV = @{thm subset_UNIV};
val trans_image_cong_o_apply = @{thm trans[OF image_cong[OF o_apply refl]]};
val trans_o_apply = @{thm trans[OF o_apply]};
--- a/src/HOL/Codatatype/Tools/bnf_def_tactics.ML Fri Sep 21 03:41:10 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_def_tactics.ML Fri Sep 21 11:44:55 2012 +0200
@@ -33,8 +33,6 @@
open BNF_Util
open BNF_Tactics
-val set_mp = @{thm set_mp};
-
fun mk_id' id = mk_trans (fun_cong OF [id]) @{thm id_apply};
fun mk_comp' comp = @{thm o_eq_dest_lhs} OF [mk_sym comp];
fun mk_set_natural' set_natural = set_natural RS @{thm pointfreeE};
@@ -75,9 +73,9 @@
else unfold_defs_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN
EVERY' [rtac equalityI, rtac subsetI,
REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
- REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
+ REPEAT_DETERM o dtac Pair_eqD,
REPEAT_DETERM o etac conjE, hyp_subst_tac,
- rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl,
+ rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl,
rtac sym, rtac trans, rtac map_comp, rtac map_cong,
REPEAT_DETERM_N n o EVERY' [dtac @{thm set_rev_mp}, atac,
REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
@@ -89,7 +87,7 @@
REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
stac @{thm fst_conv}, atac]) set_naturals,
rtac @{thm subrelI}, etac CollectE, REPEAT_DETERM o eresolve_tac [exE, conjE],
- REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
+ REPEAT_DETERM o dtac Pair_eqD,
REPEAT_DETERM o etac conjE, hyp_subst_tac,
rtac allE, rtac subst, rtac @{thm wpull_def}, rtac map_wpull,
REPEAT_DETERM_N n o rtac @{thm wpull_Gr}, etac allE, etac impE, rtac conjI, atac,
@@ -99,7 +97,7 @@
rtac sym, rtac map_id', REPEAT_DETERM o eresolve_tac [bexE, conjE],
rtac @{thm relcompI}, rtac @{thm converseI},
REPEAT_DETERM_N 2 o EVERY' [rtac CollectI, rtac exI,
- rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, etac sym,
+ rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl, etac sym,
etac @{thm set_rev_mp}, rtac equalityD1, rtac in_cong,
REPEAT_DETERM_N n o rtac @{thm Gr_def}]] 1
end;
@@ -128,11 +126,11 @@
else unfold_defs_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN
EVERY' [rtac @{thm subrelI},
REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
- REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
+ REPEAT_DETERM o dtac Pair_eqD,
REPEAT_DETERM o etac conjE, hyp_subst_tac, rtac @{thm converseI},
rtac @{thm relcompI}, rtac @{thm converseI},
EVERY' (map (fn thm => EVERY' [rtac CollectI, rtac exI,
- rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, rtac trans,
+ rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl, rtac trans,
rtac map_cong, REPEAT_DETERM_N n o rtac thm,
rtac (map_comp RS sym), rtac CollectI,
CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
@@ -155,32 +153,32 @@
else unfold_defs_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN
EVERY' [rtac equalityI, rtac @{thm subrelI},
REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
- REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
+ REPEAT_DETERM o dtac Pair_eqD,
REPEAT_DETERM o etac conjE, hyp_subst_tac,
rtac @{thm relcompI}, rtac @{thm relcompI}, rtac @{thm converseI},
- rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl,
+ rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl,
rtac sym, rtac trans, rtac map_comp, rtac sym, rtac map_cong,
REPEAT_DETERM_N n o rtac @{thm fst_fstO},
in_tac @{thm fstO_in},
- rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl,
+ rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl,
rtac sym, rtac trans, rtac map_comp, rtac map_cong,
REPEAT_DETERM_N n o EVERY' [rtac trans, rtac o_apply, rtac ballE, rtac subst,
rtac @{thm csquare_def}, rtac @{thm csquare_fstO_sndO}, atac, etac notE,
etac set_mp, atac],
in_tac @{thm fstO_in},
rtac @{thm relcompI}, rtac @{thm converseI},
- rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl,
+ rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl,
rtac sym, rtac trans, rtac map_comp, rtac map_cong,
REPEAT_DETERM_N n o rtac o_apply,
in_tac @{thm sndO_in},
- rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl,
+ rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl,
rtac sym, rtac trans, rtac map_comp, rtac sym, rtac map_cong,
REPEAT_DETERM_N n o rtac @{thm snd_sndO},
in_tac @{thm sndO_in},
rtac @{thm subrelI},
REPEAT_DETERM o eresolve_tac [CollectE, @{thm relcompE}, @{thm converseE}],
REPEAT_DETERM o eresolve_tac [exE, conjE],
- REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
+ REPEAT_DETERM o dtac Pair_eqD,
REPEAT_DETERM o etac conjE, hyp_subst_tac,
rtac allE, rtac subst, rtac @{thm wppull_def}, rtac map_wppull,
CONJ_WRAP' (K (rtac @{thm wppull_fstO_sndO})) set_naturals,
@@ -188,7 +186,7 @@
REPEAT_DETERM o eresolve_tac [bexE, conjE],
rtac @{thm relcompI}, rtac @{thm converseI},
EVERY' (map (fn thm => EVERY' [rtac CollectI, rtac exI,
- rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, rtac sym, rtac trans,
+ rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl, rtac sym, rtac trans,
rtac trans, rtac map_cong, REPEAT_DETERM_N n o rtac thm,
rtac (map_comp RS sym), atac, atac]) [@{thm fst_fstO}, @{thm snd_sndO}])] 1
end;
--- a/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML Fri Sep 21 03:41:10 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML Fri Sep 21 11:44:55 2012 +0200
@@ -129,25 +129,20 @@
open BNF_FP
open BNF_GFP_Util
-val Pair_eq_subst_id = @{thm Pair_eq[THEN subst, of "%x. x"]};
val fst_convol_fun_cong_sym = @{thm fst_convol} RS fun_cong RS sym;
-val list_inject_subst_id = @{thm list.inject[THEN subst, of "%x. x"]};
+val list_inject_iffD1 = @{thm list.inject[THEN iffD1]};
val nat_induct = @{thm nat_induct};
val o_apply_trans_sym = o_apply RS trans RS sym;
val ord_eq_le_trans = @{thm ord_eq_le_trans};
val ord_eq_le_trans_trans_fun_cong_image_id_id_apply =
@{thm ord_eq_le_trans[OF trans[OF fun_cong[OF image_id] id_apply]]};
val ordIso_ordLeq_trans = @{thm ordIso_ordLeq_trans};
-val set_mp = @{thm set_mp};
-val set_rev_mp = @{thm set_rev_mp};
val snd_convol_fun_cong_sym = @{thm snd_convol} RS fun_cong RS sym;
-val ssubst_id = @{thm ssubst[of _ _ "%x. x"]};
-val subst_id = @{thm subst[of _ _ "%x. x"]};
val sum_case_weak_cong = @{thm sum_case_weak_cong};
val trans_fun_cong_image_id_id_apply = @{thm trans[OF fun_cong[OF image_id] id_apply]};
fun mk_coalg_set_tac coalg_def =
- dtac (coalg_def RS subst_id) 1 THEN
+ dtac (coalg_def RS iffD1) 1 THEN
REPEAT_DETERM (etac conjE 1) THEN
EVERY' [dtac @{thm rev_bspec}, atac] 1 THEN
REPEAT_DETERM (eresolve_tac [CollectE, conjE] 1) THEN atac 1;
@@ -291,7 +286,7 @@
dtac (rel_O_Gr RS equalityD1 RS set_mp),
REPEAT_DETERM o eresolve_tac [CollectE, @{thm relcompE}, @{thm converseE}],
REPEAT_DETERM o eresolve_tac [@{thm GrE}, exE, conjE],
- REPEAT_DETERM o dtac Pair_eq_subst_id,
+ REPEAT_DETERM o dtac Pair_eqD,
REPEAT_DETERM o etac conjE,
hyp_subst_tac,
REPEAT_DETERM o eresolve_tac [CollectE, conjE],
@@ -319,7 +314,7 @@
end;
fun mk_bis_converse_tac m bis_rel rel_congs rel_converses =
- EVERY' [stac bis_rel, dtac (bis_rel RS subst_id),
+ EVERY' [stac bis_rel, dtac (bis_rel RS iffD1),
REPEAT_DETERM o etac conjE, rtac conjI,
CONJ_WRAP' (K (EVERY' [rtac @{thm converse_shift}, etac subset_trans,
rtac equalityD2, rtac @{thm converse_Times}])) rel_congs,
@@ -333,7 +328,7 @@
rtac @{thm converseI}, etac mp, etac @{thm converseD}]) (rel_congs ~~ rel_converses)] 1;
fun mk_bis_O_tac m bis_rel rel_congs rel_Os =
- EVERY' [stac bis_rel, REPEAT_DETERM o dtac (bis_rel RS subst_id),
+ EVERY' [stac bis_rel, REPEAT_DETERM o dtac (bis_rel RS iffD1),
REPEAT_DETERM o etac conjE, rtac conjI,
CONJ_WRAP' (K (EVERY' [etac @{thm relcomp_subset_Sigma}, atac])) rel_congs,
CONJ_WRAP' (fn (rel_cong, rel_O) =>
@@ -343,7 +338,7 @@
REPEAT_DETERM_N (length rel_congs) o rtac refl,
rtac rel_O,
etac @{thm relcompE},
- REPEAT_DETERM o dtac Pair_eq_subst_id,
+ REPEAT_DETERM o dtac Pair_eqD,
etac conjE, hyp_subst_tac,
REPEAT_DETERM o etac allE, rtac @{thm relcompI},
etac mp, atac, etac mp, atac]) (rel_congs ~~ rel_Os)] 1;
@@ -391,17 +386,17 @@
rtac (mk_nth_conv n i)] 1;
fun mk_equiv_lsbis_tac sbis_lsbis lsbis_incl incl_lsbis bis_diag bis_converse bis_O =
- EVERY' [rtac (@{thm equiv_def} RS ssubst_id),
+ EVERY' [rtac (@{thm equiv_def} RS iffD2),
- rtac conjI, rtac (@{thm refl_on_def} RS ssubst_id),
+ rtac conjI, rtac (@{thm refl_on_def} RS iffD2),
rtac conjI, rtac lsbis_incl, rtac ballI, rtac set_mp,
rtac incl_lsbis, rtac bis_diag, atac, etac @{thm diagI},
- rtac conjI, rtac (@{thm sym_def} RS ssubst_id),
+ rtac conjI, rtac (@{thm sym_def} RS iffD2),
rtac allI, rtac allI, rtac impI, rtac set_mp,
rtac incl_lsbis, rtac bis_converse, rtac sbis_lsbis, etac @{thm converseI},
- rtac (@{thm trans_def} RS ssubst_id),
+ rtac (@{thm trans_def} RS iffD2),
rtac allI, rtac allI, rtac allI, rtac impI, rtac impI, rtac set_mp,
rtac incl_lsbis, rtac bis_O, rtac sbis_lsbis, rtac sbis_lsbis,
etac @{thm relcompI}, atac] 1;
@@ -535,7 +530,7 @@
hyp_subst_tac, etac @{thm emptyE}, rtac (@{thm Ffunc_def} RS equalityD2 RS set_mp),
rtac CollectI, rtac conjI, rtac ballI, dtac bspec, etac thin_rl, atac, dtac conjunct1,
CONJ_WRAP_GEN' (etac disjE) (fn (i, def) => EVERY'
- [rtac (mk_UnIN n i), dtac (def RS subst_id),
+ [rtac (mk_UnIN n i), dtac (def RS iffD1),
REPEAT_DETERM o eresolve_tac [exE, conjE], rtac @{thm image_eqI}, atac, rtac CollectI,
REPEAT_DETERM_N m o (rtac conjI THEN' atac),
CONJ_WRAP' (K (EVERY' [etac ord_eq_le_trans, rtac subset_trans,
@@ -547,9 +542,9 @@
fun mk_carT_set_tac n i carT_def strT_def isNode_def set_natural {context = ctxt, prems = _}=
EVERY' [dtac (carT_def RS equalityD1 RS set_mp),
REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
- dtac Pair_eq_subst_id,
+ dtac Pair_eqD,
etac conjE, hyp_subst_tac,
- dtac (isNode_def RS subst_id),
+ dtac (isNode_def RS iffD1),
REPEAT_DETERM o eresolve_tac [exE, conjE],
rtac (equalityD2 RS set_mp),
rtac (strT_def RS arg_cong RS trans),
@@ -573,8 +568,8 @@
rtac (mk_sum_casesN n i RS (Drule.instantiate' [cT] [] arg_cong) RS sym)]
else EVERY' [dtac (carT_def RS equalityD1 RS set_mp),
REPEAT_DETERM o eresolve_tac [CollectE, exE], etac conjE,
- dtac conjunct2, dtac Pair_eq_subst_id, etac conjE,
- hyp_subst_tac, dtac (isNode_def RS subst_id),
+ dtac conjunct2, dtac Pair_eqD, etac conjE,
+ hyp_subst_tac, dtac (isNode_def RS iffD1),
REPEAT_DETERM o eresolve_tac [exE, conjE],
rtac (mk_InN_not_InM i i' RS notE), etac (sym RS trans), atac]))
(ks ~~ (carT_defs ~~ isNode_defs));
@@ -719,8 +714,8 @@
CONJ_WRAP' (fn (i, ((Lev_0, rv_Nil), coalg_sets)) =>
EVERY' [rtac impI, REPEAT_DETERM o etac conjE,
dtac (Lev_0 RS equalityD1 RS set_mp), etac @{thm singletonE}, etac ssubst,
- rtac (rv_Nil RS arg_cong RS ssubst_id),
- rtac (mk_sum_casesN n i RS ssubst_id),
+ rtac (rv_Nil RS arg_cong RS iffD2),
+ rtac (mk_sum_casesN n i RS iffD2),
CONJ_WRAP' (fn thm => etac thm THEN' atac) (take m coalg_sets)])
(ks ~~ ((Lev_0s ~~ rv_Nils) ~~ coalg_setss)),
REPEAT_DETERM o rtac allI,
@@ -729,8 +724,8 @@
CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
(fn (i, (from_to_sbd, coalg_set)) =>
EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
- rtac (rv_Cons RS arg_cong RS ssubst_id),
- rtac (mk_sum_casesN n i RS arg_cong RS trans RS ssubst_id),
+ rtac (rv_Cons RS arg_cong RS iffD2),
+ rtac (mk_sum_casesN n i RS arg_cong RS trans RS iffD2),
etac (from_to_sbd RS arg_cong), REPEAT_DETERM o etac allE,
dtac (mk_conjunctN n i), etac mp, etac conjI, etac set_rev_mp,
etac coalg_set, atac])
@@ -802,7 +797,7 @@
hyp_subst_tac,
CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
(fn k => REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE] THEN'
- dtac list_inject_subst_id THEN' etac conjE THEN'
+ dtac list_inject_iffD1 THEN' etac conjE THEN'
(if k = i'
then EVERY' [dtac (mk_InN_inject n k), hyp_subst_tac, etac imageI]
else etac (mk_InN_not_InM i' k RS notE)))
@@ -822,10 +817,10 @@
dtac (Lev_Suc RS equalityD1 RS set_mp) THEN'
CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) (fn k =>
REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE] THEN'
- dtac list_inject_subst_id THEN' etac conjE THEN'
+ dtac list_inject_iffD1 THEN' etac conjE THEN'
(if k = i
then EVERY' [dtac (mk_InN_inject n i),
- dtac (Thm.permute_prems 0 2 (to_sbd_inj RS subst_id)),
+ dtac (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)),
atac, atac, hyp_subst_tac] THEN'
CONJ_WRAP' (fn i'' =>
EVERY' [rtac impI, dtac (sym RS trans),
@@ -957,7 +952,7 @@
rtac (mk_sum_casesN n i) THEN' rtac (mk_sum_casesN n i RS trans)),
rtac (map_comp_id RS trans), rtac (map_cong 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 ssubst, rtac @{thm Pair_eq}, rtac conjI,
+ DETERM o EVERY' [rtac trans, rtac o_apply, rtac Pair_eqI, rtac conjI,
rtac trans, rtac @{thm Shift_def},
rtac equalityI, rtac subsetI, etac thin_rl, etac thin_rl,
REPEAT_DETERM o eresolve_tac [CollectE, @{thm UN_E}], dtac length_Lev', dtac asm_rl,
@@ -965,9 +960,9 @@
rtac (@{thm length_Cons} RS arg_cong RS trans), rtac Lev_Suc,
CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) (fn i'' =>
EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
- dtac list_inject_subst_id, etac conjE,
+ dtac list_inject_iffD1, etac conjE,
if i' = i'' then EVERY' [dtac (mk_InN_inject n i'),
- dtac (Thm.permute_prems 0 2 (to_sbd_inj RS subst_id)),
+ dtac (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)),
atac, atac, hyp_subst_tac, etac @{thm UN_I[OF UNIV_I]}]
else etac (mk_InN_not_InM i' i'' RS notE)])
(rev ks),
@@ -980,9 +975,9 @@
dtac (Lev_Suc RS equalityD1 RS set_mp),
CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) (fn i'' =>
EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
- dtac list_inject_subst_id, etac conjE,
+ dtac list_inject_iffD1, etac conjE,
if i' = i'' then EVERY' [dtac (mk_InN_inject n i'),
- dtac (Thm.permute_prems 0 2 (to_sbd_inj RS subst_id)),
+ dtac (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)),
atac, atac, hyp_subst_tac, atac]
else etac (mk_InN_not_InM i' i'' RS notE)])
(rev ks),
@@ -1067,7 +1062,7 @@
CONJ_WRAP' (fn thm => rtac ballI THEN' etac (thm RS arg_cong RS sym)) Abs_inverses] 1;
fun mk_mor_coiter_tac m mor_UNIV unf_defs coiter_defs Abs_inverses morEs map_comp_ids map_congs =
- EVERY' [rtac ssubst_id, rtac mor_UNIV,
+ EVERY' [rtac iffD2, rtac mor_UNIV,
CONJ_WRAP' (fn ((Abs_inverse, morE), ((unf_def, coiter_def), (map_comp_id, map_cong))) =>
EVERY' [rtac ext, rtac (o_apply RS trans RS sym), rtac (unf_def RS trans),
rtac (coiter_def RS arg_cong RS trans), rtac (Abs_inverse RS arg_cong RS trans),
@@ -1082,7 +1077,7 @@
let
val n = length Rep_injects;
in
- EVERY' [rtac rev_mp, ftac (bis_def RS subst_id),
+ EVERY' [rtac rev_mp, ftac (bis_def RS iffD1),
REPEAT_DETERM o etac conjE, rtac bis_cong, rtac bis_O, rtac bis_converse,
rtac bis_Gr, rtac tcoalg, rtac mor_Rep, rtac bis_O, atac, rtac bis_Gr, rtac tcoalg,
rtac mor_Rep, REPEAT_DETERM_N n o etac @{thm relImage_Gr},
@@ -1456,7 +1451,7 @@
fun mk_wpull_tac m coalg_thePull mor_thePull_fst mor_thePull_snd mor_thePull_pick
mor_unique pick_cols hset_defs =
- EVERY' [rtac (@{thm wpull_def} RS ssubst_id), REPEAT_DETERM o rtac allI, rtac impI,
+ EVERY' [rtac (@{thm wpull_def} RS iffD2), REPEAT_DETERM o rtac allI, rtac impI,
REPEAT_DETERM o etac conjE, rtac bexI, rtac conjI,
rtac box_equals, rtac mor_unique,
rtac coalg_thePull, REPEAT_DETERM_N (m - 1) o etac conjI, atac,
--- a/src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML Fri Sep 21 03:41:10 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML Fri Sep 21 11:44:55 2012 +0200
@@ -86,15 +86,12 @@
val id_apply = @{thm id_apply};
val meta_mp = @{thm meta_mp};
val ord_eq_le_trans = @{thm ord_eq_le_trans};
-val set_mp = @{thm set_mp};
-val set_rev_mp = @{thm set_rev_mp};
val subset_UNIV = @{thm subset_UNIV};
val subset_trans = @{thm subset_trans};
-val subst_id = @{thm subst[of _ _ "\<lambda>x. x"]};
val trans_fun_cong_image_id_id_apply = @{thm trans[OF fun_cong[OF image_id] id_apply]};
fun mk_alg_set_tac alg_def =
- dtac (alg_def RS subst_id) 1 THEN
+ dtac (alg_def RS iffD1) 1 THEN
REPEAT_DETERM (etac conjE 1) THEN
EVERY' [etac bspec, rtac CollectI] 1 THEN
REPEAT_DETERM (etac conjI 1) THEN atac 1;
@@ -161,8 +158,8 @@
(EVERY' [rtac subst, rtac @{thm inver_pointfree}, etac @{thm inver_mono}, atac])];
in
(stac mor_def THEN'
- dtac (alg_def RS subst_id) THEN'
- dtac (alg_def RS subst_id) THEN'
+ dtac (alg_def RS iffD1) THEN'
+ dtac (alg_def RS iffD1) THEN'
REPEAT o etac conjE THEN'
rtac conjI THEN'
CONJ_WRAP' (K fbetw_tac) set_natural's THEN'
@@ -281,7 +278,7 @@
(rtac (worel RS (@{thm wo_rel.worec_fixpoint} RS fun_cong)) THEN' rtac ssubst 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 ssubst, rtac @{thm Pair_eq}, rtac conjI]) minH_tac in_congs) 1
+ CONJ_WRAP_GEN' (EVERY' [rtac Pair_eqI, rtac conjI]) minH_tac in_congs) 1
end;
fun mk_min_algs_mono_tac min_algs = EVERY' [stac @{thm relChain_def}, rtac allI, rtac allI,
--- a/src/HOL/Codatatype/Tools/bnf_util.ML Fri Sep 21 03:41:10 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_util.ML Fri Sep 21 11:44:55 2012 +0200
@@ -121,6 +121,10 @@
val ctrans: thm
val o_apply: thm
+ val set_mp: thm
+ val set_rev_mp: thm
+ val Pair_eqD: thm
+ val Pair_eqI: thm
val mk_sym: thm -> thm
val mk_trans: thm -> thm -> thm
val mk_unabs_def: int -> thm -> thm
@@ -518,6 +522,10 @@
(*TODO: antiquote heavily used theorems once*)
val ctrans = @{thm ordLeq_transitive};
val o_apply = @{thm o_apply};
+val set_mp = @{thm set_mp};
+val set_rev_mp = @{thm set_rev_mp};
+val Pair_eqD = @{thm iffD1[OF Pair_eq]};
+val Pair_eqI = @{thm iffD2[OF Pair_eq]};
fun mk_nthN 1 t 1 = t
| mk_nthN _ t 1 = HOLogic.mk_fst t