--- a/src/HOL/Library/FSet.thy Thu Aug 29 17:47:29 2024 +0200
+++ b/src/HOL/Library/FSet.thy Fri Aug 30 10:44:48 2024 +0100
@@ -1175,15 +1175,13 @@
lemma atomize_fBall:
"(\<And>x. x |\<in>| A ==> P x) == Trueprop (fBall A (\<lambda>x. P x))"
-apply (simp only: atomize_all atomize_imp)
-apply (rule equal_intr_rule)
- by (transfer, simp)+
+ by (simp add: Set.atomize_ball)
lemma fBall_mono[mono]: "P \<le> Q \<Longrightarrow> fBall S P \<le> fBall S Q"
-by auto
+ by auto
lemma fBex_mono[mono]: "P \<le> Q \<Longrightarrow> fBex S P \<le> fBex S Q"
-by auto
+ by auto
end
@@ -1552,7 +1550,7 @@
lemma fset_strong_cases:
obtains "xs = {||}"
| ys x where "x |\<notin>| ys" and "xs = finsert x ys"
-by transfer blast
+ by auto
lemma fset_induct2:
"P {||} {||} \<Longrightarrow>
@@ -1560,12 +1558,7 @@
(\<And>y ys. y |\<notin>| ys \<Longrightarrow> P {||} (finsert y ys)) \<Longrightarrow>
(\<And>x xs y ys. \<lbrakk>P xs ys; x |\<notin>| xs; y |\<notin>| ys\<rbrakk> \<Longrightarrow> P (finsert x xs) (finsert y ys)) \<Longrightarrow>
P xsa ysa"
- apply (induct xsa arbitrary: ysa)
- apply (induct_tac x rule: fset_induct_stronger)
- apply simp_all
- apply (induct_tac xa rule: fset_induct_stronger)
- apply simp_all
- done
+by (induct xsa arbitrary: ysa; metis fset_induct_stronger)
subsection \<open>Lemmas depending on induction\<close>
@@ -1583,25 +1576,16 @@
lemma rel_fset_alt_def: "rel_fset R = (\<lambda>A B. (\<forall>x.\<exists>y. x|\<in>|A \<longrightarrow> y|\<in>|B \<and> R x y)
\<and> (\<forall>y. \<exists>x. y|\<in>|B \<longrightarrow> x|\<in>|A \<and> R x y))"
-apply (rule ext)+
-apply transfer'
-apply (subst rel_set_def[unfolded fun_eq_iff])
-by blast
+ by transfer' (metis (no_types, opaque_lifting) rel_set_def)
lemma finite_rel_set:
assumes fin: "finite X" "finite Z"
assumes R_S: "rel_set (R OO S) X Z"
shows "\<exists>Y. finite Y \<and> rel_set R X Y \<and> rel_set S Y Z"
proof -
- obtain f where f: "\<forall>x\<in>X. R x (f x) \<and> (\<exists>z\<in>Z. S (f x) z)"
- apply atomize_elim
- apply (subst bchoice_iff[symmetric])
- using R_S[unfolded rel_set_def OO_def] by blast
-
- obtain g where g: "\<forall>z\<in>Z. S (g z) z \<and> (\<exists>x\<in>X. R x (g z))"
- apply atomize_elim
- apply (subst bchoice_iff[symmetric])
- using R_S[unfolded rel_set_def OO_def] by blast
+ obtain f g where f: "\<forall>x\<in>X. R x (f x) \<and> (\<exists>z\<in>Z. S (f x) z)"
+ and g: "\<forall>z\<in>Z. S (g z) z \<and> (\<exists>x\<in>X. R x (g z))"
+ using R_S[unfolded rel_set_def OO_def] by metis
let ?Y = "f ` X \<union> g ` Z"
have "finite ?Y" by (simp add: fin)
@@ -1713,13 +1697,13 @@
lemma ffilter_transfer [transfer_rule]:
assumes "bi_unique A"
shows "((A ===> (=)) ===> rel_fset A ===> rel_fset A) ffilter ffilter"
- using assms unfolding rel_fun_def
- using Lifting_Set.filter_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast
+ using assms Lifting_Set.filter_transfer
+ unfolding rel_fun_def by (metis ffilter.rep_eq rel_fset.rep_eq)
lemma card_transfer [transfer_rule]:
"bi_unique A \<Longrightarrow> (rel_fset A ===> (=)) fcard fcard"
- unfolding rel_fun_def
- using card_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast
+ using card_transfer unfolding rel_fun_def
+ by (metis fcard.rep_eq rel_fset.rep_eq)
end
@@ -1735,13 +1719,10 @@
lemma rel_fset_alt:
"rel_fset R a b \<longleftrightarrow> (\<forall>t \<in> fset a. \<exists>u \<in> fset b. R t u) \<and> (\<forall>t \<in> fset b. \<exists>u \<in> fset a. R u t)"
-by transfer (simp add: rel_set_def)
+ by transfer (simp add: rel_set_def)
lemma fset_to_fset: "finite A \<Longrightarrow> fset (the_inv fset A) = A"
-apply (rule f_the_inv_into_f[unfolded inj_on_def])
-apply (simp add: fset_inject)
-apply (rule range_eqI Abs_fset_inverse[symmetric] CollectI)+
-.
+ by (metis CollectI f_the_inv_into_f fset_cases fset_cong inj_onI rangeI)
lemma rel_fset_aux:
"(\<forall>t \<in> fset a. \<exists>u \<in> fset b. R t u) \<and> (\<forall>u \<in> fset b. \<exists>t \<in> fset a. R t u) \<longleftrightarrow>
@@ -1762,10 +1743,7 @@
qed (auto simp add: *)
next
assume ?R thus ?L unfolding Grp_def relcompp.simps conversep.simps
- apply (simp add: subset_eq Ball_def)
- apply (rule conjI)
- apply (transfer, clarsimp, metis snd_conv)
- by (transfer, clarsimp, metis fst_conv)
+ using Product_Type.Collect_case_prodD by blast
qed
bnf "'a fset"
@@ -1790,7 +1768,7 @@
done
lemma rel_fset_fset: "rel_set \<chi> (fset A1) (fset A2) = rel_fset \<chi> A1 A2"
- by transfer (rule refl)
+ by (simp add: rel_fset.rep_eq)
end
@@ -1802,11 +1780,13 @@
subsection \<open>Size setup\<close>
-context includes fset.lifting begin
+context includes fset.lifting
+begin
lift_definition size_fset :: "('a \<Rightarrow> nat) \<Rightarrow> 'a fset \<Rightarrow> nat" is "\<lambda>f. sum (Suc \<circ> f)" .
end
-instantiation fset :: (type) size begin
+instantiation fset :: (type) size
+begin
definition size_fset where
size_fset_overloaded_def: "size_fset = FSet.size_fset (\<lambda>_. 0)"
instance ..
@@ -1821,8 +1801,8 @@
folded size_fset_overloaded_def])
lemma fset_size_o_map: "inj f \<Longrightarrow> size_fset g \<circ> fimage f = size_fset (g \<circ> f)"
- apply (subst fun_eq_iff)
- including fset.lifting by transfer (auto intro: sum.reindex_cong subset_inj_on)
+ unfolding fun_eq_iff
+ by (simp add: inj_def inj_onI sum.reindex)
setup \<open>
BNF_LFP_Size.register_size_global \<^type_name>\<open>fset\<close> \<^const_name>\<open>size_fset\<close>
@@ -1902,16 +1882,11 @@
subsubsection \<open>Countability\<close>
lemma exists_fset_of_list: "\<exists>xs. fset_of_list xs = S"
-including fset.lifting
-by transfer (rule finite_list)
+ including fset.lifting
+ by transfer (rule finite_list)
lemma fset_of_list_surj[simp, intro]: "surj fset_of_list"
-proof -
- have "x \<in> range fset_of_list" for x :: "'a fset"
- unfolding image_iff
- using exists_fset_of_list by fastforce
- thus ?thesis by auto
-qed
+ by (metis exists_fset_of_list surj_def)
instance fset :: (countable) countable
proof