--- a/src/HOL/BNF/BNF_Def.thy Mon Jul 15 11:29:19 2013 +0200
+++ b/src/HOL/BNF/BNF_Def.thy Mon Jul 15 14:23:51 2013 +0200
@@ -171,9 +171,6 @@
lemma flip_pred: "A \<subseteq> Collect (split (R ^--1)) \<Longrightarrow> (%(x, y). (y, x)) ` A \<subseteq> Collect (split R)"
by auto
-lemma pointfreeE: "f o g = f' o g' \<Longrightarrow> f (g x) = f' (g' x)"
-unfolding o_def fun_eq_iff by simp
-
lemma Collect_split_mono: "A \<le> B \<Longrightarrow> Collect (split A) \<subseteq> Collect (split B)"
by auto
--- a/src/HOL/BNF/BNF_FP_Basic.thy Mon Jul 15 11:29:19 2013 +0200
+++ b/src/HOL/BNF/BNF_FP_Basic.thy Mon Jul 15 14:23:51 2013 +0200
@@ -35,18 +35,6 @@
lemma prod_all_impI_step: "(\<And>x. \<forall>y. P (x, y) \<longrightarrow> Q (x, y)) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x"
by auto
-lemma all_unit_eq: "(\<And>x. PROP P x) \<equiv> PROP P ()"
-by simp
-
-lemma all_prod_eq: "(\<And>x. PROP P x) \<equiv> (\<And>a b. PROP P (a, b))"
-by clarsimp
-
-lemma rev_bspec: "a \<in> A \<Longrightarrow> \<forall>z \<in> A. P z \<Longrightarrow> P a"
-by simp
-
-lemma Un_cong: "\<lbrakk>A = B; C = D\<rbrakk> \<Longrightarrow> A \<union> C = B \<union> D"
-by simp
-
lemma pointfree_idE: "f \<circ> g = id \<Longrightarrow> f (g x) = x"
unfolding o_def fun_eq_iff by simp
--- a/src/HOL/BNF/BNF_GFP.thy Mon Jul 15 11:29:19 2013 +0200
+++ b/src/HOL/BNF/BNF_GFP.thy Mon Jul 15 14:23:51 2013 +0200
@@ -247,11 +247,6 @@
lemma cpow_clists_czero: "\<lbrakk>A \<in> Field (cpow (clists r)) - {{}}; |A| =o czero\<rbrakk> \<Longrightarrow> False"
unfolding cpow_def clists_def card_of_ordIso_czero_iff_empty by auto
-lemma incl_UNION_I:
-assumes "i \<in> I" and "A \<subseteq> F i"
-shows "A \<subseteq> UNION I F"
-using assms by auto
-
lemma Nil_clists: "{[]} \<subseteq> Field (clists r)"
unfolding clists_def Field_card_of by auto
--- a/src/HOL/BNF/Countable_Type.thy Mon Jul 15 11:29:19 2013 +0200
+++ b/src/HOL/BNF/Countable_Type.thy Mon Jul 15 14:23:51 2013 +0200
@@ -92,10 +92,6 @@
"countable (rcset C)"
using Rep_cset by simp
-lemma rcset_inj[simp]:
-"rcset C = rcset D \<longleftrightarrow> C = D"
-by (metis acset_rcset)
-
lemma rcset_surj:
assumes "countable A"
shows "\<exists> C. rcset C = A"
--- a/src/HOL/BNF/More_BNFs.thy Mon Jul 15 11:29:19 2013 +0200
+++ b/src/HOL/BNF/More_BNFs.thy Mon Jul 15 14:23:51 2013 +0200
@@ -297,7 +297,7 @@
lemma rcset_to_rcset: "countable A \<Longrightarrow> rcset (the_inv rcset A) = A"
apply (rule f_the_inv_into_f)
-unfolding inj_on_def rcset_inj using rcset_surj by auto
+unfolding inj_on_def Rep_cset_inject using rcset_surj by auto
lemma Collect_Int_Times:
"{(x, y). R x y} \<inter> A \<times> B = {(x, y). R x y \<and> x \<in> A \<and> y \<in> B}"
--- a/src/HOL/BNF/Tools/bnf_comp_tactics.ML Mon Jul 15 11:29:19 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp_tactics.ML Mon Jul 15 14:23:51 2013 +0200
@@ -78,7 +78,7 @@
[rtac (Gset_map RS o_eq_dest_lhs), rtac sym, rtac trans_o_apply,
rtac trans_image_cong_o_apply, rtac trans_image_cong_o_apply,
rtac (@{thm image_cong} OF [Gset_map RS o_eq_dest_lhs RS arg_cong_Union, refl] RS trans),
- rtac @{thm trans[OF pointfreeE[OF Union_natural[symmetric]]]}, rtac arg_cong_Union,
+ rtac @{thm trans[OF comp_eq_dest[OF Union_natural[symmetric]]]}, rtac arg_cong_Union,
rtac @{thm trans[OF o_eq_dest_lhs[OF image_o_collect[symmetric]]]},
rtac @{thm fun_cong[OF arg_cong[of _ _ collect]]}] @
[REPEAT_DETERM_N (length set_maps) o EVERY' [rtac @{thm trans[OF image_insert]},
--- a/src/HOL/BNF/Tools/bnf_def_tactics.ML Mon Jul 15 11:29:19 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML Mon Jul 15 14:23:51 2013 +0200
@@ -45,7 +45,7 @@
fun mk_map_cong_tac ctxt cong0 =
(hyp_subst_tac ctxt THEN' rtac cong0 THEN'
REPEAT_DETERM o (dtac meta_spec THEN' etac meta_mp THEN' atac)) 1;
-fun mk_set_map' set_map = set_map RS @{thm pointfreeE};
+fun mk_set_map' set_map = set_map RS @{thm comp_eq_dest};
fun mk_in_mono_tac n = if n = 0 then rtac subset_UNIV 1
else (rtac subsetI THEN'
rtac CollectI) 1 THEN
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Mon Jul 15 11:29:19 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Mon Jul 15 14:23:51 2013 +0200
@@ -1174,7 +1174,7 @@
end;
val sumEN_thm' =
- unfold_thms lthy @{thms all_unit_eq}
+ unfold_thms lthy @{thms unit_all_eq1}
(Drule.instantiate' (map (SOME o certifyT lthy) ctr_prod_Ts) []
(mk_sumEN_balanced n))
|> Morphism.thm phi;
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Mon Jul 15 11:29:19 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Mon Jul 15 14:23:51 2013 +0200
@@ -78,7 +78,7 @@
fun mk_exhaust_tac ctxt n ctr_defs ctor_iff_dtor sumEN' =
unfold_thms_tac ctxt (ctor_iff_dtor :: ctr_defs) THEN HEADGOAL (rtac sumEN') THEN
- unfold_thms_tac ctxt @{thms all_prod_eq} THEN
+ unfold_thms_tac ctxt @{thms split_paired_all} THEN
HEADGOAL (EVERY' (maps (fn k => [select_prem_tac n (rotate_tac 1) k,
REPEAT_DETERM o dtac meta_spec, etac meta_mp, atac]) (1 upto n)));
--- a/src/HOL/BNF/Tools/bnf_gfp.ML Mon Jul 15 11:29:19 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML Mon Jul 15 14:23:51 2013 +0200
@@ -2219,7 +2219,7 @@
|> Thm.close_derivation)
goals cTs dtor_unfold_thms map_comp's map_cong0s;
in
- map_split (fn thm => (thm RS @{thm pointfreeE}, thm)) maps
+ map_split (fn thm => (thm RS @{thm comp_eq_dest}, thm)) maps
end;
val map_comp_thms =
--- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Mon Jul 15 11:29:19 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Mon Jul 15 14:23:51 2013 +0200
@@ -140,12 +140,14 @@
val snd_convol_fun_cong_sym = @{thm snd_convol} RS fun_cong RS sym;
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]};
-val Collect_splitD_set_mp = @{thm Collect_splitD[OF set_mp]}
+val Collect_splitD_set_mp = @{thm Collect_splitD[OF set_mp]};
+val rev_bspec = Drule.rotate_prems 1 bspec;
+val Un_cong = @{thm arg_cong2[of _ _ _ _ "op \<union>"]}
fun mk_coalg_set_tac coalg_def =
dtac (coalg_def RS iffD1) 1 THEN
REPEAT_DETERM (etac conjE 1) THEN
- EVERY' [dtac @{thm rev_bspec}, atac] 1 THEN
+ EVERY' [dtac rev_bspec, atac] 1 THEN
REPEAT_DETERM (eresolve_tac [CollectE, conjE] 1) THEN atac 1;
fun mk_mor_elim_tac mor_def =
@@ -183,7 +185,7 @@
EVERY' [rtac iffI, CONJ_WRAP' mor_tac morEs,
stac mor_def, rtac conjI, CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) morEs,
CONJ_WRAP' (fn i =>
- EVERY' [dtac (mk_conjunctN n i), rtac ballI, etac @{thm pointfreeE}]) (1 upto n)] 1
+ EVERY' [dtac (mk_conjunctN n i), rtac ballI, etac @{thm comp_eq_dest}]) (1 upto n)] 1
end;
fun mk_mor_str_tac ks mor_UNIV =
@@ -194,7 +196,7 @@
fun mk_set_incl_hset_tac def rec_Suc =
EVERY' (stac def ::
- map rtac [@{thm incl_UNION_I}, UNIV_I, @{thm ord_le_eq_trans}, @{thm Un_upper1},
+ map rtac [@{thm SUP_upper2}, UNIV_I, @{thm ord_le_eq_trans}, @{thm Un_upper1},
sym, rec_Suc]) 1;
fun mk_set_hset_incl_hset_tac n defs rec_Suc i =
@@ -238,10 +240,10 @@
(fn (rec_Suc, (morE, ((passive_set_maps, active_set_maps), coalg_sets))) =>
EVERY' [rtac impI, rtac (rec_Suc RS trans), rtac (rec_Suc RS trans RS sym),
if m = 0 then K all_tac
- else EVERY' [rtac @{thm Un_cong}, rtac box_equals,
+ else EVERY' [rtac Un_cong, rtac box_equals,
rtac (nth passive_set_maps (j - 1) RS sym),
rtac trans_fun_cong_image_id_id_apply, etac (morE RS arg_cong), atac],
- CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_cong}))
+ CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 Un_cong))
(fn (i, (set_map, coalg_set)) =>
EVERY' [rtac sym, rtac trans, rtac (refl RSN (2, @{thm UN_cong})),
etac (morE RS sym RS arg_cong RS trans), atac, rtac set_map,
@@ -360,7 +362,7 @@
EVERY' [rtac allI, rtac allI, rtac impI, etac @{thm UN_E}, dtac bspec, atac,
dtac conjunct2, dtac (mk_conjunctN n i), etac allE, etac allE, dtac mp,
atac, etac bexE, rtac bexI, atac, rtac in_mono,
- REPEAT_DETERM_N n o etac @{thm incl_UNION_I[OF _ subset_refl]},
+ REPEAT_DETERM_N n o etac @{thm SUP_upper2[OF _ subset_refl]},
atac]) (ks ~~ in_monos)] 1
end;
@@ -374,7 +376,7 @@
end;
fun mk_incl_lsbis_tac n i lsbis_def =
- EVERY' [rtac @{thm xt1(3)}, rtac lsbis_def, rtac @{thm incl_UNION_I}, rtac CollectI,
+ EVERY' [rtac @{thm xt1(3)}, rtac lsbis_def, rtac @{thm SUP_upper2}, rtac CollectI,
REPEAT_DETERM_N n o rtac exI, rtac conjI, rtac refl, atac, rtac equalityD2,
rtac (mk_nth_conv n i)] 1;
@@ -1122,8 +1124,8 @@
CONJ_WRAP' (fn (rec_Suc, (dtor_map, set_nats)) => EVERY'
[SELECT_GOAL (unfold_thms_tac ctxt
(rec_Suc :: dtor_map :: set_nats @ @{thms image_Un image_UN UN_simps(10)})),
- rtac @{thm Un_cong}, rtac refl,
- CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_cong}))
+ rtac Un_cong, rtac refl,
+ CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 Un_cong))
(fn i => EVERY' [rtac @{thm UN_cong[OF refl]},
REPEAT_DETERM o etac allE, etac (mk_conjunctN n i)]) (n downto 1)])
(rec_Sucs ~~ (dtor_maps ~~ set_mapss))] 1
--- a/src/HOL/BNF/Tools/bnf_lfp.ML Mon Jul 15 11:29:19 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML Mon Jul 15 14:23:51 2013 +0200
@@ -1451,7 +1451,7 @@
|> Thm.close_derivation)
goals ctor_fold_thms map_comp_id_thms map_cong0s;
in
- map (fn thm => thm RS @{thm pointfreeE}) maps
+ map (fn thm => thm RS @{thm comp_eq_dest}) maps
end;
val (ctor_map_unique_thms, ctor_map_unique_thm) =
--- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Mon Jul 15 11:29:19 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Mon Jul 15 14:23:51 2013 +0200
@@ -87,6 +87,8 @@
val ord_eq_le_trans = @{thm ord_eq_le_trans};
val subset_trans = @{thm subset_trans};
val trans_fun_cong_image_id_id_apply = @{thm trans[OF fun_cong[OF image_id] id_apply]};
+val rev_bspec = Drule.rotate_prems 1 bspec;
+val Un_cong = @{thm arg_cong2[of _ _ _ _ "op \<union>"]}
fun mk_alg_set_tac alg_def =
dtac (alg_def RS iffD1) 1 THEN
@@ -123,7 +125,7 @@
val fbetw_tac = EVERY' [rtac ballI, stac o_apply, etac bspec, etac bspec, atac];
fun mor_tac (set_map', map_comp_id) =
EVERY' [rtac ballI, stac o_apply, rtac trans,
- rtac trans, dtac @{thm rev_bspec}, atac, etac arg_cong,
+ rtac trans, dtac rev_bspec, atac, etac arg_cong,
REPEAT o eresolve_tac [CollectE, conjE], etac bspec, rtac CollectI] THEN'
CONJ_WRAP' (fn thm =>
FIRST' [rtac subset_UNIV,
@@ -147,7 +149,7 @@
(EVERY' [rtac ord_eq_le_trans, rtac thm, rtac subset_trans,
etac @{thm image_mono}, atac])]) set_map';
fun mor_tac (set_map', ((morE, map_comp_id), map_cong0L)) =
- EVERY' [rtac ballI, ftac @{thm rev_bspec}, atac,
+ EVERY' [rtac ballI, ftac rev_bspec, atac,
REPEAT o eresolve_tac [CollectE, conjE], rtac sym, rtac trans, rtac sym,
etac @{thm inverE}, etac bspec, rtac CollectI, Collect_tac set_map',
rtac trans, etac (morE RS arg_cong), rtac CollectI, Collect_tac set_map',
@@ -270,7 +272,7 @@
let
val minG_tac = EVERY' [rtac @{thm UN_cong}, rtac refl, dtac bspec, atac, etac arg_cong];
fun minH_tac thm =
- EVERY' [rtac @{thm Un_cong}, minG_tac, rtac @{thm image_cong}, rtac thm,
+ EVERY' [rtac Un_cong, minG_tac, rtac @{thm image_cong}, rtac thm,
REPEAT_DETERM_N (length in_congs) o minG_tac, rtac refl];
in
(rtac (worel RS (@{thm wo_rel.worec_fixpoint} RS fun_cong)) THEN' rtac ssubst THEN'
@@ -391,7 +393,7 @@
let
val n = length alg_sets;
val fbetw_tac =
- CONJ_WRAP' (K (EVERY' [rtac ballI, etac @{thm rev_bspec}, etac CollectE, atac])) alg_sets;
+ CONJ_WRAP' (K (EVERY' [rtac ballI, etac rev_bspec, etac CollectE, atac])) alg_sets;
val mor_tac =
CONJ_WRAP' (fn thm => EVERY' [rtac ballI, rtac thm]) str_init_defs;
fun alg_epi_tac ((alg_set, str_init_def), set_map') =
@@ -583,7 +585,7 @@
fun mk_ctor_map_unique_tac m mor_def fold_unique_mor map_comp_ids map_cong0s =
let
val n = length map_cong0s;
- fun mk_mor (comp_id, cong) = EVERY' [rtac ballI, rtac trans, etac @{thm pointfreeE},
+ fun mk_mor (comp_id, cong) = EVERY' [rtac ballI, rtac trans, etac @{thm comp_eq_dest},
rtac sym, rtac trans, rtac o_apply, rtac trans, rtac (comp_id RS arg_cong),
rtac (cong RS arg_cong),
REPEAT_DETERM_N m o rtac refl,
@@ -603,9 +605,9 @@
fun mk_UN thm = rtac (thm RS @{thm arg_cong[of _ _ Union]} RS trans) THEN'
rtac @{thm Union_image_eq};
in
- EVERY' [rtac (set RS @{thm pointfreeE} RS trans), rtac @{thm Un_cong},
+ EVERY' [rtac (set RS @{thm comp_eq_dest} RS trans), rtac Un_cong,
rtac (trans OF [set_map', trans_fun_cong_image_id_id_apply]),
- REPEAT_DETERM_N (n - 1) o rtac @{thm Un_cong},
+ REPEAT_DETERM_N (n - 1) o rtac Un_cong,
EVERY' (map mk_UN set_map's)] 1
end;
@@ -621,9 +623,9 @@
fun mk_set_nat cset ctor_map ctor_set set_nats =
EVERY' [rtac trans, rtac @{thm image_cong}, rtac ctor_set, rtac refl,
rtac sym, rtac (trans OF [ctor_map RS HOL_arg_cong cset, ctor_set RS trans]),
- rtac sym, EVERY' (map rtac (trans :: @{thms image_Un Un_cong})),
+ rtac sym, EVERY' (map rtac [trans, @{thm image_Un}, Un_cong]),
rtac sym, rtac (nth set_nats (i - 1)),
- REPEAT_DETERM_N (n - 1) o EVERY' (map rtac (trans :: @{thms image_Un Un_cong})),
+ REPEAT_DETERM_N (n - 1) o EVERY' (map rtac [trans, @{thm image_Un}, Un_cong]),
EVERY' (map useIH (drop m set_nats))];
in
(induct_tac THEN' EVERY' (map4 mk_set_nat csets ctor_maps ctor_sets set_map'ss)) 1