--- a/src/HOL/Codatatype/Tools/bnf_comp_tactics.ML Fri Sep 21 11:44:55 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_comp_tactics.ML Fri Sep 21 11:51:07 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 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 11:44:55 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_def_tactics.ML Fri Sep 21 11:51:07 2012 +0200
@@ -36,7 +36,7 @@
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};
-fun mk_in_mono_tac n = if n = 0 then rtac @{thm subset_UNIV} 1
+fun mk_in_mono_tac n = if n = 0 then rtac subset_UNIV 1
else (rtac subsetI THEN'
rtac CollectI) 1 THEN
REPEAT_DETERM (eresolve_tac [CollectE, conjE] 1) THEN
@@ -107,8 +107,8 @@
subst_tac ctxt [map_id] 1 THEN
(if n = 0 then rtac refl 1
else EVERY' [rtac @{thm arg_cong2[of _ _ _ _ Gr]},
- rtac equalityI, rtac @{thm subset_UNIV}, rtac subsetI, rtac CollectI,
- CONJ_WRAP' (K (rtac @{thm subset_UNIV})) (1 upto n), rtac refl] 1);
+ rtac equalityI, rtac subset_UNIV, rtac subsetI, rtac CollectI,
+ CONJ_WRAP' (K (rtac subset_UNIV)) (1 upto n), rtac refl] 1);
fun mk_rel_mono_tac rel_O_Grs in_mono {context = ctxt, prems = _} =
unfold_defs_tac ctxt rel_O_Grs THEN
--- a/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML Fri Sep 21 11:44:55 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML Fri Sep 21 11:51:07 2012 +0200
@@ -205,7 +205,7 @@
[etac @{thm UN_I}, atac]) 1;
fun mk_set_incl_hin_tac incls =
- if null incls then rtac @{thm subset_UNIV} 1
+ if null incls then rtac subset_UNIV 1
else EVERY' [rtac subsetI, rtac CollectI,
CONJ_WRAP' (fn incl => EVERY' [rtac subset_trans, etac incl, atac]) incls] 1;
@@ -534,7 +534,7 @@
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,
- rtac @{thm subset_UNIV}, rtac equalityD2, rtac @{thm Field_card_order},
+ rtac subset_UNIV, rtac equalityD2, rtac @{thm Field_card_order},
rtac sbd_card_order])) isNode_defs]) (1 upto n ~~ isNode_defs),
atac] 1
end;
@@ -1154,7 +1154,7 @@
rtac impI, REPEAT_DETERM o dtac @{thm meta_spec}, etac CollectE, etac @{thm meta_impE},
atac, etac exE, etac conjE, etac conjE, rtac bexI, rtac conjI,
etac @{thm fst_conv[THEN subst]}, etac @{thm snd_conv[THEN subst]},
- rtac CollectI, REPEAT_DETERM_N m o (rtac conjI THEN' rtac @{thm subset_UNIV}),
+ rtac CollectI, REPEAT_DETERM_N m o (rtac conjI THEN' rtac subset_UNIV),
CONJ_WRAP' (fn i' => EVERY' [rtac subsetI, rtac CollectI, dtac (mk_conjunctN n i'),
REPEAT_DETERM o etac allE, etac mp, rtac @{thm ssubst_mem[OF pair_collapse]}, atac])
ks])
@@ -1377,7 +1377,7 @@
SELECT_GOAL (unfold_defs_tac ctxt @{thms o_apply prod.cases}), rtac impI,
REPEAT_DETERM o eresolve_tac [CollectE, conjE],
rtac CollectI,
- REPEAT_DETERM_N m o (rtac conjI THEN' rtac @{thm subset_UNIV}),
+ REPEAT_DETERM_N m o (rtac conjI THEN' rtac subset_UNIV),
CONJ_WRAP' (fn set_natural =>
EVERY' [rtac ord_eq_le_trans, rtac trans, rtac set_natural,
rtac trans_fun_cong_image_id_id_apply, atac])
--- a/src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML Fri Sep 21 11:44:55 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML Fri Sep 21 11:51:07 2012 +0200
@@ -86,7 +86,6 @@
val id_apply = @{thm id_apply};
val meta_mp = @{thm meta_mp};
val ord_eq_le_trans = @{thm ord_eq_le_trans};
-val subset_UNIV = @{thm subset_UNIV};
val subset_trans = @{thm subset_trans};
val trans_fun_cong_image_id_id_apply = @{thm trans[OF fun_cong[OF image_id] id_apply]};
--- a/src/HOL/Codatatype/Tools/bnf_util.ML Fri Sep 21 11:44:55 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_util.ML Fri Sep 21 11:51:07 2012 +0200
@@ -123,6 +123,7 @@
val o_apply: thm
val set_mp: thm
val set_rev_mp: thm
+ val subset_UNIV: thm
val Pair_eqD: thm
val Pair_eqI: thm
val mk_sym: thm -> thm
@@ -524,6 +525,7 @@
val o_apply = @{thm o_apply};
val set_mp = @{thm set_mp};
val set_rev_mp = @{thm set_rev_mp};
+val subset_UNIV = @{thm subset_UNIV};
val Pair_eqD = @{thm iffD1[OF Pair_eq]};
val Pair_eqI = @{thm iffD2[OF Pair_eq]};