--- a/src/HOL/Finite_Set.thy Mon May 31 20:27:45 2021 +0000
+++ b/src/HOL/Finite_Set.thy Tue Jun 01 19:46:34 2021 +0200
@@ -710,21 +710,23 @@
subsection \<open>A basic fold functional for finite sets\<close>
-text \<open>The intended behaviour is
- \<open>fold f z {x\<^sub>1, \<dots>, x\<^sub>n} = f x\<^sub>1 (\<dots> (f x\<^sub>n z)\<dots>)\<close>
- if \<open>f\<close> is ``left-commutative'':
+text \<open>
+ The intended behaviour is \<open>fold f z {x\<^sub>1, \<dots>, x\<^sub>n} = f x\<^sub>1 (\<dots> (f x\<^sub>n z)\<dots>)\<close>
+ if \<open>f\<close> is ``left-commutative''.
+ The commutativity requirement is relativised to the carrier set \<open>S\<close>:
\<close>
-locale comp_fun_commute =
+locale comp_fun_commute_on =
+ fixes S :: "'a set"
fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
- assumes comp_fun_commute: "f y \<circ> f x = f x \<circ> f y"
+ assumes comp_fun_commute_on: "x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> f y \<circ> f x = f x \<circ> f y"
begin
-lemma fun_left_comm: "f y (f x z) = f x (f y z)"
- using comp_fun_commute by (simp add: fun_eq_iff)
+lemma fun_left_comm: "x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> f y (f x z) = f x (f y z)"
+ using comp_fun_commute_on by (simp add: fun_eq_iff)
-lemma commute_left_comp: "f y \<circ> (f x \<circ> g) = f x \<circ> (f y \<circ> g)"
- by (simp add: o_assoc comp_fun_commute)
+lemma commute_left_comp: "x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> f y \<circ> (f x \<circ> g) = f x \<circ> (f y \<circ> g)"
+ by (simp add: o_assoc comp_fun_commute_on)
end
@@ -776,7 +778,7 @@
by (subst fold_graph_closed_eq[where B=B and g=g]) (auto simp: that)
text \<open>
- A tempting alternative for the definiens is
+ A tempting alternative for the definition is
\<^term>\<open>if finite A then THE y. fold_graph f z A y else e\<close>.
It allows the removal of finiteness assumptions from the theorems
\<open>fold_comm\<close>, \<open>fold_reindex\<close> and \<open>fold_distrib\<close>.
@@ -789,7 +791,7 @@
subsubsection \<open>From \<^const>\<open>fold_graph\<close> to \<^term>\<open>fold\<close>\<close>
-context comp_fun_commute
+context comp_fun_commute_on
begin
lemma fold_graph_finite:
@@ -798,7 +800,10 @@
using assms by induct simp_all
lemma fold_graph_insertE_aux:
- "fold_graph f z A y \<Longrightarrow> a \<in> A \<Longrightarrow> \<exists>y'. y = f a y' \<and> fold_graph f z (A - {a}) y'"
+ assumes "A \<subseteq> S"
+ assumes "fold_graph f z A y" "a \<in> A"
+ shows "\<exists>y'. y = f a y' \<and> fold_graph f z (A - {a}) y'"
+ using assms(2-,1)
proof (induct set: fold_graph)
case emptyI
then show ?case by simp
@@ -812,8 +817,9 @@
case False
then obtain y' where y: "y = f a y'" and y': "fold_graph f z (A - {a}) y'"
using insertI by auto
- have "f x y = f a (f x y')"
- unfolding y by (rule fun_left_comm)
+ from insertI have "x \<in> S" "a \<in> S" by auto
+ then have "f x y = f a (f x y')"
+ unfolding y by (intro fun_left_comm; simp)
moreover have "fold_graph f z (insert x A - {a}) (f x y')"
using y' and \<open>x \<noteq> a\<close> and \<open>x \<notin> A\<close>
by (simp add: insert_Diff_if fold_graph.insertI)
@@ -823,35 +829,41 @@
qed
lemma fold_graph_insertE:
+ assumes "insert x A \<subseteq> S"
assumes "fold_graph f z (insert x A) v" and "x \<notin> A"
obtains y where "v = f x y" and "fold_graph f z A y"
- using assms by (auto dest: fold_graph_insertE_aux [OF _ insertI1])
+ using assms by (auto dest: fold_graph_insertE_aux[OF \<open>insert x A \<subseteq> S\<close> _ insertI1])
-lemma fold_graph_determ: "fold_graph f z A x \<Longrightarrow> fold_graph f z A y \<Longrightarrow> y = x"
+lemma fold_graph_determ:
+ assumes "A \<subseteq> S"
+ assumes "fold_graph f z A x" "fold_graph f z A y"
+ shows "y = x"
+ using assms(2-,1)
proof (induct arbitrary: y set: fold_graph)
case emptyI
then show ?case by fast
next
case (insertI x A y v)
- from \<open>fold_graph f z (insert x A) v\<close> and \<open>x \<notin> A\<close>
+ from \<open>insert x A \<subseteq> S\<close> and \<open>fold_graph f z (insert x A) v\<close> and \<open>x \<notin> A\<close>
obtain y' where "v = f x y'" and "fold_graph f z A y'"
by (rule fold_graph_insertE)
- from \<open>fold_graph f z A y'\<close> have "y' = y"
- by (rule insertI)
+ from \<open>fold_graph f z A y'\<close> insertI have "y' = y"
+ by simp
with \<open>v = f x y'\<close> show "v = f x y"
by simp
qed
-lemma fold_equality: "fold_graph f z A y \<Longrightarrow> fold f z A = y"
+lemma fold_equality: "A \<subseteq> S \<Longrightarrow> fold_graph f z A y \<Longrightarrow> fold f z A = y"
by (cases "finite A") (auto simp add: fold_def intro: fold_graph_determ dest: fold_graph_finite)
lemma fold_graph_fold:
+ assumes "A \<subseteq> S"
assumes "finite A"
shows "fold_graph f z A (fold f z A)"
proof -
- from assms have "\<exists>x. fold_graph f z A x"
+ from \<open>finite A\<close> have "\<exists>x. fold_graph f z A x"
by (rule finite_imp_fold_graph)
- moreover note fold_graph_determ
+ moreover note fold_graph_determ[OF \<open>A \<subseteq> S\<close>]
ultimately have "\<exists>!x. fold_graph f z A x"
by (rule ex_ex1I)
then have "fold_graph f z A (The (fold_graph f z A))"
@@ -871,12 +883,13 @@
text \<open>The various recursion equations for \<^const>\<open>fold\<close>:\<close>
lemma fold_insert [simp]:
+ assumes "insert x A \<subseteq> S"
assumes "finite A" and "x \<notin> A"
shows "fold f z (insert x A) = f x (fold f z A)"
-proof (rule fold_equality)
+proof (rule fold_equality[OF \<open>insert x A \<subseteq> S\<close>])
fix z
- from \<open>finite A\<close> have "fold_graph f z A (fold f z A)"
- by (rule fold_graph_fold)
+ from \<open>insert x A \<subseteq> S\<close> \<open>finite A\<close> have "fold_graph f z A (fold f z A)"
+ by (blast intro: fold_graph_fold)
with \<open>x \<notin> A\<close> have "fold_graph f z (insert x A) (f x (fold f z A))"
by (rule fold_graph.insertI)
then show "fold_graph f z (insert x A) (f x (fold f z A))"
@@ -886,20 +899,33 @@
declare (in -) empty_fold_graphE [rule del] fold_graph.intros [rule del]
\<comment> \<open>No more proofs involve these.\<close>
-lemma fold_fun_left_comm: "finite A \<Longrightarrow> f x (fold f z A) = fold f (f x z) A"
+lemma fold_fun_left_comm:
+ assumes "insert x A \<subseteq> S" "finite A"
+ shows "f x (fold f z A) = fold f (f x z) A"
+ using assms(2,1)
proof (induct rule: finite_induct)
case empty
then show ?case by simp
next
- case insert
- then show ?case
- by (simp add: fun_left_comm [of x])
+ case (insert y F)
+ then have "fold f (f x z) (insert y F) = f y (fold f (f x z) F)"
+ by simp
+ also have "\<dots> = f x (f y (fold f z F))"
+ using insert by (simp add: fun_left_comm[where ?y=x])
+ also have "\<dots> = f x (fold f z (insert y F))"
+ proof -
+ from insert have "insert y F \<subseteq> S" by simp
+ from fold_insert[OF this] insert show ?thesis by simp
+ qed
+ finally show ?case ..
qed
-lemma fold_insert2: "finite A \<Longrightarrow> x \<notin> A \<Longrightarrow> fold f z (insert x A) = fold f (f x z) A"
+lemma fold_insert2:
+ "insert x A \<subseteq> S \<Longrightarrow> finite A \<Longrightarrow> x \<notin> A \<Longrightarrow> fold f z (insert x A) = fold f (f x z) A"
by (simp add: fold_fun_left_comm)
lemma fold_rec:
+ assumes "A \<subseteq> S"
assumes "finite A" and "x \<in> A"
shows "fold f z A = f x (fold f z (A - {x}))"
proof -
@@ -908,11 +934,12 @@
then have "fold f z A = fold f z (insert x (A - {x}))"
by simp
also have "\<dots> = f x (fold f z (A - {x}))"
- by (rule fold_insert) (simp add: \<open>finite A\<close>)+
+ by (rule fold_insert) (use assms in \<open>auto\<close>)
finally show ?thesis .
qed
lemma fold_insert_remove:
+ assumes "insert x A \<subseteq> S"
assumes "finite A"
shows "fold f z (insert x A) = f x (fold f z (A - {x}))"
proof -
@@ -921,20 +948,77 @@
moreover have "x \<in> insert x A"
by auto
ultimately have "fold f z (insert x A) = f x (fold f z (insert x A - {x}))"
- by (rule fold_rec)
+ using \<open>insert x A \<subseteq> S\<close> by (blast intro: fold_rec)
then show ?thesis
by simp
qed
lemma fold_set_union_disj:
+ assumes "A \<subseteq> S" "B \<subseteq> S"
assumes "finite A" "finite B" "A \<inter> B = {}"
shows "Finite_Set.fold f z (A \<union> B) = Finite_Set.fold f (Finite_Set.fold f z A) B"
- using assms(2,1,3) by induct simp_all
+ using \<open>finite B\<close> assms(1,2,3,5)
+proof induct
+ case (insert x F)
+ have "fold f z (A \<union> insert x F) = f x (fold f (fold f z A) F)"
+ using insert by auto
+ also have "\<dots> = fold f (fold f z A) (insert x F)"
+ using insert by (blast intro: fold_insert[symmetric])
+ finally show ?case .
+qed simp
+
end
text \<open>Other properties of \<^const>\<open>fold\<close>:\<close>
+lemma fold_graph_image:
+ assumes "inj_on g A"
+ shows "fold_graph f z (g ` A) = fold_graph (f \<circ> g) z A"
+proof
+ fix w
+ show "fold_graph f z (g ` A) w = fold_graph (f o g) z A w"
+ proof
+ assume "fold_graph f z (g ` A) w"
+ then show "fold_graph (f \<circ> g) z A w"
+ using assms
+ proof (induct "g ` A" w arbitrary: A)
+ case emptyI
+ then show ?case by (auto intro: fold_graph.emptyI)
+ next
+ case (insertI x A r B)
+ from \<open>inj_on g B\<close> \<open>x \<notin> A\<close> \<open>insert x A = image g B\<close> obtain x' A'
+ where "x' \<notin> A'" and [simp]: "B = insert x' A'" "x = g x'" "A = g ` A'"
+ by (rule inj_img_insertE)
+ from insertI.prems have "fold_graph (f \<circ> g) z A' r"
+ by (auto intro: insertI.hyps)
+ with \<open>x' \<notin> A'\<close> have "fold_graph (f \<circ> g) z (insert x' A') ((f \<circ> g) x' r)"
+ by (rule fold_graph.insertI)
+ then show ?case
+ by simp
+ qed
+ next
+ assume "fold_graph (f \<circ> g) z A w"
+ then show "fold_graph f z (g ` A) w"
+ using assms
+ proof induct
+ case emptyI
+ then show ?case
+ by (auto intro: fold_graph.emptyI)
+ next
+ case (insertI x A r)
+ from \<open>x \<notin> A\<close> insertI.prems have "g x \<notin> g ` A"
+ by auto
+ moreover from insertI have "fold_graph f z (g ` A) r"
+ by simp
+ ultimately have "fold_graph f z (insert (g x) (g ` A)) (f (g x) r)"
+ by (rule fold_graph.insertI)
+ then show ?case
+ by simp
+ qed
+ qed
+qed
+
lemma fold_image:
assumes "inj_on g A"
shows "fold f z (g ` A) = fold (f \<circ> g) z A"
@@ -944,70 +1028,26 @@
by (auto dest: finite_imageD simp add: fold_def)
next
case True
- have "fold_graph f z (g ` A) = fold_graph (f \<circ> g) z A"
- proof
- fix w
- show "fold_graph f z (g ` A) w \<longleftrightarrow> fold_graph (f \<circ> g) z A w" (is "?P \<longleftrightarrow> ?Q")
- proof
- assume ?P
- then show ?Q
- using assms
- proof (induct "g ` A" w arbitrary: A)
- case emptyI
- then show ?case by (auto intro: fold_graph.emptyI)
- next
- case (insertI x A r B)
- from \<open>inj_on g B\<close> \<open>x \<notin> A\<close> \<open>insert x A = image g B\<close> obtain x' A'
- where "x' \<notin> A'" and [simp]: "B = insert x' A'" "x = g x'" "A = g ` A'"
- by (rule inj_img_insertE)
- from insertI.prems have "fold_graph (f \<circ> g) z A' r"
- by (auto intro: insertI.hyps)
- with \<open>x' \<notin> A'\<close> have "fold_graph (f \<circ> g) z (insert x' A') ((f \<circ> g) x' r)"
- by (rule fold_graph.insertI)
- then show ?case
- by simp
- qed
- next
- assume ?Q
- then show ?P
- using assms
- proof induct
- case emptyI
- then show ?case
- by (auto intro: fold_graph.emptyI)
- next
- case (insertI x A r)
- from \<open>x \<notin> A\<close> insertI.prems have "g x \<notin> g ` A"
- by auto
- moreover from insertI have "fold_graph f z (g ` A) r"
- by simp
- ultimately have "fold_graph f z (insert (g x) (g ` A)) (f (g x) r)"
- by (rule fold_graph.insertI)
- then show ?case
- by simp
- qed
- qed
- qed
- with True assms show ?thesis
- by (auto simp add: fold_def)
+ then show ?thesis
+ by (auto simp add: fold_def fold_graph_image[OF assms])
qed
lemma fold_cong:
- assumes "comp_fun_commute f" "comp_fun_commute g"
- and "finite A"
+ assumes "comp_fun_commute_on S f" "comp_fun_commute_on S g"
+ and "A \<subseteq> S" "finite A"
and cong: "\<And>x. x \<in> A \<Longrightarrow> f x = g x"
and "s = t" and "A = B"
shows "fold f s A = fold g t B"
proof -
have "fold f s A = fold g s A"
- using \<open>finite A\<close> cong
+ using \<open>finite A\<close> \<open>A \<subseteq> S\<close> cong
proof (induct A)
case empty
then show ?case by simp
next
case insert
- interpret f: comp_fun_commute f by (fact \<open>comp_fun_commute f\<close>)
- interpret g: comp_fun_commute g by (fact \<open>comp_fun_commute g\<close>)
+ interpret f: comp_fun_commute_on S f by (fact \<open>comp_fun_commute_on S f\<close>)
+ interpret g: comp_fun_commute_on S g by (fact \<open>comp_fun_commute_on S g\<close>)
from insert show ?case by simp
qed
with assms show ?thesis by simp
@@ -1016,14 +1056,15 @@
text \<open>A simplified version for idempotent functions:\<close>
-locale comp_fun_idem = comp_fun_commute +
- assumes comp_fun_idem: "f x \<circ> f x = f x"
+locale comp_fun_idem_on = comp_fun_commute_on +
+ assumes comp_fun_idem_on: "x \<in> S \<Longrightarrow> f x \<circ> f x = f x"
begin
-lemma fun_left_idem: "f x (f x z) = f x z"
- using comp_fun_idem by (simp add: fun_eq_iff)
+lemma fun_left_idem: "x \<in> S \<Longrightarrow> f x (f x z) = f x z"
+ using comp_fun_idem_on by (simp add: fun_eq_iff)
lemma fold_insert_idem:
+ assumes "insert x A \<subseteq> S"
assumes fin: "finite A"
shows "fold f z (insert x A) = f x (fold f z A)"
proof cases
@@ -1031,33 +1072,42 @@
then obtain B where "A = insert x B" and "x \<notin> B"
by (rule set_insert)
then show ?thesis
- using assms by (simp add: comp_fun_idem fun_left_idem)
+ using assms by (simp add: comp_fun_idem_on fun_left_idem)
next
assume "x \<notin> A"
then show ?thesis
- using assms by simp
+ using assms by auto
qed
declare fold_insert [simp del] fold_insert_idem [simp]
-lemma fold_insert_idem2: "finite A \<Longrightarrow> fold f z (insert x A) = fold f (f x z) A"
+lemma fold_insert_idem2: "insert x A \<subseteq> S \<Longrightarrow> finite A \<Longrightarrow> fold f z (insert x A) = fold f (f x z) A"
by (simp add: fold_fun_left_comm)
end
-subsubsection \<open>Liftings to \<open>comp_fun_commute\<close> etc.\<close>
-
-lemma (in comp_fun_commute) comp_comp_fun_commute: "comp_fun_commute (f \<circ> g)"
- by standard (simp_all add: comp_fun_commute)
+subsubsection \<open>Liftings to \<open>comp_fun_commute_on\<close> etc.\<close>
+
+lemma (in comp_fun_commute_on) comp_comp_fun_commute_on:
+ "range g \<subseteq> S \<Longrightarrow> comp_fun_commute_on R (f \<circ> g)"
+ by standard (force intro: comp_fun_commute_on)
-lemma (in comp_fun_idem) comp_comp_fun_idem: "comp_fun_idem (f \<circ> g)"
- by (rule comp_fun_idem.intro, rule comp_comp_fun_commute, unfold_locales)
- (simp_all add: comp_fun_idem)
+lemma (in comp_fun_idem_on) comp_comp_fun_idem_on:
+ assumes "range g \<subseteq> S"
+ shows "comp_fun_idem_on R (f \<circ> g)"
+proof
+ interpret f_g: comp_fun_commute_on R "f o g"
+ by (fact comp_comp_fun_commute_on[OF \<open>range g \<subseteq> S\<close>])
+ show "x \<in> R \<Longrightarrow> y \<in> R \<Longrightarrow> (f \<circ> g) y \<circ> (f \<circ> g) x = (f \<circ> g) x \<circ> (f \<circ> g) y" for x y
+ by (fact f_g.comp_fun_commute_on)
+qed (use \<open>range g \<subseteq> S\<close> in \<open>force intro: comp_fun_idem_on\<close>)
-lemma (in comp_fun_commute) comp_fun_commute_funpow: "comp_fun_commute (\<lambda>x. f x ^^ g x)"
+lemma (in comp_fun_commute_on) comp_fun_commute_on_funpow:
+ "comp_fun_commute_on S (\<lambda>x. f x ^^ g x)"
proof
- show "f y ^^ g y \<circ> f x ^^ g x = f x ^^ g x \<circ> f y ^^ g y" for x y
+ fix x y assume "x \<in> S" "y \<in> S"
+ show "f y ^^ g y \<circ> f x ^^ g x = f x ^^ g x \<circ> f y ^^ g y"
proof (cases "x = y")
case True
then show ?thesis by simp
@@ -1082,8 +1132,8 @@
by auto
from Suc h_def have "g y = Suc (h y)"
by simp
- then show ?case
- by (simp add: comp_assoc hyp) (simp add: o_assoc comp_fun_commute)
+ with \<open>x \<in> S\<close> \<open>y \<in> S\<close> show ?case
+ by (simp add: comp_assoc hyp) (simp add: o_assoc comp_fun_commute_on)
qed
define h where "h z = (if z = x then g x - 1 else g z)" for z
with Suc have "n = h x"
@@ -1101,6 +1151,67 @@
qed
+subsubsection \<open>\<^term>\<open>UNIV\<close> as carrier set\<close>
+
+locale comp_fun_commute =
+ fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
+ assumes comp_fun_commute: "f y \<circ> f x = f x \<circ> f y"
+begin
+
+lemma (in -) comp_fun_commute_def': "comp_fun_commute f = comp_fun_commute_on UNIV f"
+ unfolding comp_fun_commute_def comp_fun_commute_on_def by blast
+
+text \<open>
+ We abuse the \<open>rewrites\<close> functionality of locales to remove trivial assumptions that
+ result from instantiating the carrier set to \<^term>\<open>UNIV\<close>.
+\<close>
+sublocale comp_fun_commute_on UNIV f
+ rewrites "\<And>X. (X \<subseteq> UNIV) \<equiv> True"
+ and "\<And>x. x \<in> UNIV \<equiv> True"
+ and "\<And>P. (True \<Longrightarrow> P) \<equiv> Trueprop P"
+ and "\<And>P Q. (True \<Longrightarrow> PROP P \<Longrightarrow> PROP Q) \<equiv> (PROP P \<Longrightarrow> True \<Longrightarrow> PROP Q)"
+proof -
+ show "comp_fun_commute_on UNIV f"
+ by standard (simp add: comp_fun_commute)
+qed simp_all
+
+end
+
+lemma (in comp_fun_commute) comp_comp_fun_commute: "comp_fun_commute (f o g)"
+ unfolding comp_fun_commute_def' by (fact comp_comp_fun_commute_on)
+
+lemma (in comp_fun_commute) comp_fun_commute_funpow: "comp_fun_commute (\<lambda>x. f x ^^ g x)"
+ unfolding comp_fun_commute_def' by (fact comp_fun_commute_on_funpow)
+
+locale comp_fun_idem = comp_fun_commute +
+ assumes comp_fun_idem: "f x o f x = f x"
+begin
+
+lemma (in -) comp_fun_idem_def': "comp_fun_idem f = comp_fun_idem_on UNIV f"
+ unfolding comp_fun_idem_on_def comp_fun_idem_def comp_fun_commute_def'
+ unfolding comp_fun_idem_axioms_def comp_fun_idem_on_axioms_def
+ by blast
+
+text \<open>
+ Again, we abuse the \<open>rewrites\<close> functionality of locales to remove trivial assumptions that
+ result from instantiating the carrier set to \<^term>\<open>UNIV\<close>.
+\<close>
+sublocale comp_fun_idem_on UNIV f
+ rewrites "\<And>X. (X \<subseteq> UNIV) \<equiv> True"
+ and "\<And>x. x \<in> UNIV \<equiv> True"
+ and "\<And>P. (True \<Longrightarrow> P) \<equiv> Trueprop P"
+ and "\<And>P Q. (True \<Longrightarrow> PROP P \<Longrightarrow> PROP Q) \<equiv> (PROP P \<Longrightarrow> True \<Longrightarrow> PROP Q)"
+proof -
+ show "comp_fun_idem_on UNIV f"
+ by standard (simp_all add: comp_fun_idem comp_fun_commute)
+qed simp_all
+
+end
+
+lemma (in comp_fun_idem) comp_comp_fun_idem: "comp_fun_idem (f o g)"
+ unfolding comp_fun_idem_def' by (fact comp_comp_fun_idem_on)
+
+
subsubsection \<open>Expressing set operations via \<^const>\<open>fold\<close>\<close>
lemma comp_fun_commute_const: "comp_fun_commute (\<lambda>_. f)"
@@ -1150,8 +1261,12 @@
assumes "finite A"
shows "Set.filter P A = fold (\<lambda>x A'. if P x then Set.insert x A' else A') {} A"
using assms
- by induct
- (auto simp add: Set.filter_def comp_fun_commute.fold_insert[OF comp_fun_commute_filter_fold])
+proof -
+ interpret commute_insert: comp_fun_commute "(\<lambda>x A'. if P x then Set.insert x A' else A')"
+ by (fact comp_fun_commute_filter_fold)
+ from \<open>finite A\<close> show ?thesis
+ by induct (auto simp add: Set.filter_def)
+qed
lemma inter_Set_filter:
assumes "finite B"
@@ -1190,7 +1305,7 @@
qed
lemma comp_fun_commute_Pow_fold: "comp_fun_commute (\<lambda>x A. A \<union> Set.insert x ` A)"
- by (clarsimp simp: fun_eq_iff comp_fun_commute_def) blast (* somewhat slow *)
+ by (clarsimp simp: fun_eq_iff comp_fun_commute_def) blast
lemma Pow_fold:
assumes "finite A"
@@ -1219,9 +1334,12 @@
lemma product_fold:
assumes "finite A" "finite B"
shows "A \<times> B = fold (\<lambda>x z. fold (\<lambda>y. Set.insert (x, y)) z B) {} A"
- using assms unfolding Sigma_def
- by (induct A)
- (simp_all add: comp_fun_commute.fold_insert[OF comp_fun_commute_product_fold] fold_union_pair)
+proof -
+ interpret commute_product: comp_fun_commute "(\<lambda>x z. fold (\<lambda>y. Set.insert (x, y)) z B)"
+ by (fact comp_fun_commute_product_fold[OF \<open>finite B\<close>])
+ from assms show ?thesis unfolding Sigma_def
+ by (induct A) (simp_all add: fold_union_pair)
+qed
context complete_lattice
begin
@@ -1309,61 +1427,67 @@
subsubsection \<open>The natural case\<close>
-locale folding =
+locale folding_on =
+ fixes S :: "'a set"
fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" and z :: "'b"
- assumes comp_fun_commute: "f y \<circ> f x = f x \<circ> f y"
+ assumes comp_fun_commute_on: "x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> f y o f x = f x o f y"
begin
-interpretation fold?: comp_fun_commute f
- by standard (use comp_fun_commute in \<open>simp add: fun_eq_iff\<close>)
+interpretation fold?: comp_fun_commute_on S f
+ by standard (simp add: comp_fun_commute_on)
definition F :: "'a set \<Rightarrow> 'b"
- where eq_fold: "F A = fold f z A"
+ where eq_fold: "F A = Finite_Set.fold f z A"
-lemma empty [simp]:"F {} = z"
+lemma empty [simp]: "F {} = z"
by (simp add: eq_fold)
lemma infinite [simp]: "\<not> finite A \<Longrightarrow> F A = z"
by (simp add: eq_fold)
lemma insert [simp]:
- assumes "finite A" and "x \<notin> A"
+ assumes "insert x A \<subseteq> S" and "finite A" and "x \<notin> A"
shows "F (insert x A) = f x (F A)"
proof -
from fold_insert assms
- have "fold f z (insert x A) = f x (fold f z A)" by simp
+ have "Finite_Set.fold f z (insert x A)
+ = f x (Finite_Set.fold f z A)"
+ by simp
with \<open>finite A\<close> show ?thesis by (simp add: eq_fold fun_eq_iff)
qed
lemma remove:
- assumes "finite A" and "x \<in> A"
+ assumes "A \<subseteq> S" and "finite A" and "x \<in> A"
shows "F A = f x (F (A - {x}))"
proof -
from \<open>x \<in> A\<close> obtain B where A: "A = insert x B" and "x \<notin> B"
by (auto dest: mk_disjoint_insert)
moreover from \<open>finite A\<close> A have "finite B" by simp
- ultimately show ?thesis by simp
+ ultimately show ?thesis
+ using \<open>A \<subseteq> S\<close> by auto
qed
-lemma insert_remove: "finite A \<Longrightarrow> F (insert x A) = f x (F (A - {x}))"
- by (cases "x \<in> A") (simp_all add: remove insert_absorb)
+lemma insert_remove:
+ assumes "insert x A \<subseteq> S" and "finite A"
+ shows "F (insert x A) = f x (F (A - {x}))"
+ using assms by (cases "x \<in> A") (simp_all add: remove insert_absorb)
end
subsubsection \<open>With idempotency\<close>
-locale folding_idem = folding +
- assumes comp_fun_idem: "f x \<circ> f x = f x"
+locale folding_idem_on = folding_on +
+ assumes comp_fun_idem_on: "x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> f x \<circ> f x = f x"
begin
declare insert [simp del]
-interpretation fold?: comp_fun_idem f
- by standard (insert comp_fun_commute comp_fun_idem, simp add: fun_eq_iff)
+interpretation fold?: comp_fun_idem_on S f
+ by standard (simp_all add: comp_fun_commute_on comp_fun_idem_on)
lemma insert_idem [simp]:
- assumes "finite A"
+ assumes "insert x A \<subseteq> S" and "finite A"
shows "F (insert x A) = f x (F A)"
proof -
from fold_insert_idem assms
@@ -1373,6 +1497,57 @@
end
+subsubsection \<open>\<^term>\<open>UNIV\<close> as the carrier set\<close>
+
+locale folding =
+ fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" and z :: "'b"
+ assumes comp_fun_commute: "f y \<circ> f x = f x \<circ> f y"
+begin
+
+lemma (in -) folding_def': "folding f = folding_on UNIV f"
+ unfolding folding_def folding_on_def by blast
+
+text \<open>
+ Again, we abuse the \<open>rewrites\<close> functionality of locales to remove trivial assumptions that
+ result from instantiating the carrier set to \<^term>\<open>UNIV\<close>.
+\<close>
+sublocale folding_on UNIV f
+ rewrites "\<And>X. (X \<subseteq> UNIV) \<equiv> True"
+ and "\<And>x. x \<in> UNIV \<equiv> True"
+ and "\<And>P. (True \<Longrightarrow> P) \<equiv> Trueprop P"
+ and "\<And>P Q. (True \<Longrightarrow> PROP P \<Longrightarrow> PROP Q) \<equiv> (PROP P \<Longrightarrow> True \<Longrightarrow> PROP Q)"
+proof -
+ show "folding_on UNIV f"
+ by standard (simp add: comp_fun_commute)
+qed simp_all
+
+end
+
+locale folding_idem = folding +
+ assumes comp_fun_idem: "f x \<circ> f x = f x"
+begin
+
+lemma (in -) folding_idem_def': "folding_idem f = folding_idem_on UNIV f"
+ unfolding folding_idem_def folding_def' folding_idem_on_def
+ unfolding folding_idem_axioms_def folding_idem_on_axioms_def
+ by blast
+
+text \<open>
+ Again, we abuse the \<open>rewrites\<close> functionality of locales to remove trivial assumptions that
+ result from instantiating the carrier set to \<^term>\<open>UNIV\<close>.
+\<close>
+sublocale folding_idem_on UNIV f
+ rewrites "\<And>X. (X \<subseteq> UNIV) \<equiv> True"
+ and "\<And>x. x \<in> UNIV \<equiv> True"
+ and "\<And>P. (True \<Longrightarrow> P) \<equiv> Trueprop P"
+ and "\<And>P Q. (True \<Longrightarrow> PROP P \<Longrightarrow> PROP Q) \<equiv> (PROP P \<Longrightarrow> True \<Longrightarrow> PROP Q)"
+proof -
+ show "folding_idem_on UNIV f"
+ by standard (simp add: comp_fun_idem)
+qed simp_all
+
+end
+
subsection \<open>Finite cardinality\<close>
@@ -1384,7 +1559,7 @@
\<close>
global_interpretation card: folding "\<lambda>_. Suc" 0
- defines card = "folding.F (\<lambda>_. Suc) 0"
+ defines card = "folding_on.F (\<lambda>_. Suc) 0"
by standard rule
lemma card_insert_disjoint: "finite A \<Longrightarrow> x \<notin> A \<Longrightarrow> card (insert x A) = Suc (card A)"
--- a/src/HOL/Library/AList.thy Mon May 31 20:27:45 2021 +0000
+++ b/src/HOL/Library/AList.thy Tue Jun 01 19:46:34 2021 +0200
@@ -423,6 +423,9 @@
finally show ?thesis .
qed
+lemma graph_map_of: "Map.graph (map_of al) = set (clearjunk al)"
+ by (metis distinct_clearjunk graph_map_of_if_distinct_ran map_of_clearjunk)
+
lemma clearjunk_update: "clearjunk (update k v al) = update k v (clearjunk al)"
by (induct al rule: clearjunk.induct) (simp_all add: delete_update)
--- a/src/HOL/Library/AList_Mapping.thy Mon May 31 20:27:45 2021 +0000
+++ b/src/HOL/Library/AList_Mapping.thy Tue Jun 01 19:46:34 2021 +0200
@@ -34,6 +34,25 @@
"Mapping.ordered_keys (Mapping xs) = sort (remdups (map fst xs))"
by (simp only: ordered_keys_def keys_Mapping sorted_list_of_set_sort_remdups) simp
+lemma entries_Mapping [code]:
+ "Mapping.entries (Mapping xs) = set (AList.clearjunk xs)"
+ by transfer (fact graph_map_of)
+
+lemma ordered_entries_Mapping [code]:
+ "Mapping.ordered_entries (Mapping xs) = sort_key fst (AList.clearjunk xs)"
+proof -
+ have distinct: "distinct (sort_key fst (AList.clearjunk xs))"
+ using distinct_clearjunk distinct_map distinct_sort by blast
+ note folding_Map_graph.idem_if_sorted_distinct[where ?m="map_of xs", OF _ sorted_sort_key distinct]
+ then show ?thesis
+ unfolding ordered_entries_def
+ by (transfer fixing: xs) (auto simp: graph_map_of)
+qed
+
+lemma fold_Mapping [code]:
+ "Mapping.fold f (Mapping xs) a = List.fold (case_prod f) (sort_key fst (AList.clearjunk xs)) a"
+ by (simp add: Mapping.fold_def ordered_entries_Mapping)
+
lemma size_Mapping [code]: "Mapping.size (Mapping xs) = length (remdups (map fst xs))"
by (simp add: size_def length_remdups_card_conv dom_map_of_conv_image_fst)
--- a/src/HOL/Library/FSet.thy Mon May 31 20:27:45 2021 +0000
+++ b/src/HOL/Library/FSet.thy Tue Jun 01 19:46:34 2021 +0200
@@ -726,7 +726,8 @@
"\<And>x. x |\<in>| A \<Longrightarrow> f x = g x"
and "s = t" and "A = B"
shows "ffold f s A = ffold g t B"
-using assms by transfer (metis Finite_Set.fold_cong)
+ using assms[unfolded comp_fun_commute_def']
+ by transfer (meson Finite_Set.fold_cong subset_UNIV)
context comp_fun_idem
begin
--- a/src/HOL/Library/Finite_Lattice.thy Mon May 31 20:27:45 2021 +0000
+++ b/src/HOL/Library/Finite_Lattice.thy Tue Jun 01 19:46:34 2021 +0200
@@ -170,15 +170,36 @@
context finite_distrib_lattice_complete
begin
subclass finite_distrib_lattice
- apply standard
- apply (simp_all add: Inf_def Sup_def bot_def top_def)
- apply (metis (mono_tags) insert_UNIV local.Sup_fin.eq_fold local.bot_def local.finite_UNIV local.top_def)
- apply (simp add: comp_fun_idem.fold_insert_idem local.comp_fun_idem_inf)
- apply (metis (mono_tags) insert_UNIV local.Inf_fin.eq_fold local.finite_UNIV)
- apply (simp add: comp_fun_idem.fold_insert_idem local.comp_fun_idem_sup)
- apply (metis (mono_tags) insert_UNIV local.Inf_fin.eq_fold local.finite_UNIV)
- apply (metis (mono_tags) insert_UNIV local.Sup_fin.eq_fold local.finite_UNIV)
- done
+proof -
+ show "class.finite_distrib_lattice Inf Sup inf (\<le>) (<) sup bot top"
+ proof
+ show "bot = Inf UNIV"
+ unfolding bot_def top_def Inf_def
+ using Inf_fin.eq_fold Inf_fin.insert inf.absorb2 by force
+ next
+ show "top = Sup UNIV"
+ unfolding bot_def top_def Sup_def
+ using Sup_fin.eq_fold Sup_fin.insert by force
+ next
+ show "Inf {} = Sup UNIV"
+ unfolding Inf_def Sup_def bot_def top_def
+ using Sup_fin.eq_fold Sup_fin.insert by force
+ next
+ show "Sup {} = Inf UNIV"
+ unfolding Inf_def Sup_def bot_def top_def
+ using Inf_fin.eq_fold Inf_fin.insert inf.absorb2 by force
+ next
+ interpret comp_fun_idem_inf: comp_fun_idem inf
+ by (fact comp_fun_idem_inf)
+ show "Inf (insert a A) = inf a (Inf A)" for a A
+ using comp_fun_idem_inf.fold_insert_idem Inf_def finite by simp
+ next
+ interpret comp_fun_idem_sup: comp_fun_idem sup
+ by (fact comp_fun_idem_sup)
+ show "Sup (insert a A) = sup a (Sup A)" for a A
+ using comp_fun_idem_sup.fold_insert_idem Sup_def finite by simp
+ qed
+qed
end
instance finite_distrib_lattice_complete \<subseteq> complete_distrib_lattice ..
--- a/src/HOL/Library/Mapping.thy Mon May 31 20:27:45 2021 +0000
+++ b/src/HOL/Library/Mapping.thy Tue Jun 01 19:46:34 2021 +0200
@@ -5,7 +5,7 @@
section \<open>An abstract view on maps for code generation.\<close>
theory Mapping
-imports Main
+imports Main AList
begin
subsection \<open>Parametricity transfer rules\<close>
@@ -43,6 +43,16 @@
shows "((A ===> rel_option B) ===> rel_set A) dom dom"
unfolding dom_def [abs_def] Option.is_none_def [symmetric] by transfer_prover
+lemma graph_parametric:
+ assumes "bi_total A"
+ shows "((A ===> rel_option B) ===> rel_set (rel_prod A B)) Map.graph Map.graph"
+proof
+ fix f g assume "(A ===> rel_option B) f g"
+ with assms[unfolded bi_total_def] show "rel_set (rel_prod A B) (Map.graph f) (Map.graph g)"
+ unfolding graph_def rel_set_def rel_fun_def
+ by auto (metis option_rel_Some1 option_rel_Some2)+
+qed
+
lemma map_of_parametric [transfer_rule]:
assumes [transfer_rule]: "bi_unique R1"
shows "(list_all2 (rel_prod R1 R2) ===> R1 ===> rel_option R2) map_of map_of"
@@ -129,6 +139,9 @@
lift_definition keys :: "('a, 'b) mapping \<Rightarrow> 'a set"
is dom parametric dom_parametric .
+lift_definition entries :: "('a, 'b) mapping \<Rightarrow> ('a \<times> 'b) set"
+ is Map.graph parametric graph_parametric .
+
lift_definition tabulate :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) mapping"
is "\<lambda>ks f. (map_of (List.map (\<lambda>k. (k, f k)) ks))" parametric tabulate_parametric .
@@ -166,6 +179,13 @@
definition ordered_keys :: "('a::linorder, 'b) mapping \<Rightarrow> 'a list"
where "ordered_keys m = (if finite (keys m) then sorted_list_of_set (keys m) else [])"
+definition ordered_entries :: "('a::linorder, 'b) mapping \<Rightarrow> ('a \<times> 'b) list"
+ where "ordered_entries m = (if finite (entries m) then sorted_key_list_of_set fst (entries m)
+ else [])"
+
+definition fold :: "('a::linorder \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> 'c \<Rightarrow> 'c"
+ where "fold f m a = List.fold (case_prod f) (ordered_entries m) a"
+
definition is_empty :: "('a, 'b) mapping \<Rightarrow> bool"
where "is_empty m \<longleftrightarrow> keys m = {}"
@@ -462,7 +482,13 @@
by transfer rule
lemma keys_empty [simp]: "keys empty = {}"
- by transfer simp
+ by transfer (fact dom_empty)
+
+lemma in_keysD: "k \<in> keys m \<Longrightarrow> \<exists>v. lookup m k = Some v"
+ by transfer (fact domD)
+
+lemma in_entriesI: "lookup m k = Some v \<Longrightarrow> (k, v) \<in> entries m"
+ by transfer (fact in_graphI)
lemma keys_update [simp]: "keys (update k v m) = insert k (keys m)"
by transfer simp
@@ -515,7 +541,7 @@
"finite (keys m) \<Longrightarrow> k \<notin> keys m \<Longrightarrow>
ordered_keys (update k v m) = insort k (ordered_keys m)"
by (simp_all add: ordered_keys_def)
- (auto simp only: sorted_list_of_set_insert [symmetric] insert_absorb)
+ (auto simp only: sorted_list_of_set_insert_remove[symmetric] insert_absorb)
lemma ordered_keys_delete [simp]: "ordered_keys (delete k m) = remove1 k (ordered_keys m)"
proof (cases "finite (keys m)")
@@ -559,14 +585,14 @@
lemma ordered_keys_bulkload [simp]: "ordered_keys (bulkload ks) = [0..<length ks]"
by (simp add: ordered_keys_def)
-lemma tabulate_fold: "tabulate xs f = fold (\<lambda>k m. update k (f k) m) xs empty"
+lemma tabulate_fold: "tabulate xs f = List.fold (\<lambda>k m. update k (f k) m) xs empty"
proof transfer
fix f :: "'a \<Rightarrow> 'b" and xs
have "map_of (List.map (\<lambda>k. (k, f k)) xs) = foldr (\<lambda>k m. m(k \<mapsto> f k)) xs Map.empty"
by (simp add: foldr_map comp_def map_of_foldr)
- also have "foldr (\<lambda>k m. m(k \<mapsto> f k)) xs = fold (\<lambda>k m. m(k \<mapsto> f k)) xs"
+ also have "foldr (\<lambda>k m. m(k \<mapsto> f k)) xs = List.fold (\<lambda>k m. m(k \<mapsto> f k)) xs"
by (rule foldr_fold) (simp add: fun_eq_iff)
- ultimately show "map_of (List.map (\<lambda>k. (k, f k)) xs) = fold (\<lambda>k m. m(k \<mapsto> f k)) xs Map.empty"
+ ultimately show "map_of (List.map (\<lambda>k. (k, f k)) xs) = List.fold (\<lambda>k m. m(k \<mapsto> f k)) xs Map.empty"
by simp
qed
@@ -647,10 +673,262 @@
end
+subsubsection \<open>@{term [source] entries}, @{term [source] ordered_entries},
+ and @{term [source] fold}\<close>
+
+context linorder
+begin
+
+sublocale folding_Map_graph: folding_insort_key "(\<le>)" "(<)" "Map.graph m" fst for m
+ by unfold_locales (fact inj_on_fst_graph)
+
+end
+
+lemma sorted_fst_list_of_set_insort_Map_graph[simp]:
+ assumes "finite (dom m)" "fst x \<notin> dom m"
+ shows "sorted_key_list_of_set fst (insert x (Map.graph m))
+ = insort_key fst x (sorted_key_list_of_set fst (Map.graph m))"
+proof(cases x)
+ case (Pair k v)
+ with \<open>fst x \<notin> dom m\<close> have "Map.graph m \<subseteq> Map.graph (m(k \<mapsto> v))"
+ by(auto simp: graph_def)
+ moreover from Pair \<open>fst x \<notin> dom m\<close> have "(k, v) \<notin> Map.graph m"
+ using graph_domD by fastforce
+ ultimately show ?thesis
+ using Pair assms folding_Map_graph.sorted_key_list_of_set_insert[where ?m="m(k \<mapsto> v)"]
+ by auto
+qed
+
+lemma sorted_fst_list_of_set_insort_insert_Map_graph[simp]:
+ assumes "finite (dom m)" "fst x \<notin> dom m"
+ shows "sorted_key_list_of_set fst (insert x (Map.graph m))
+ = insort_insert_key fst x (sorted_key_list_of_set fst (Map.graph m))"
+proof(cases x)
+ case (Pair k v)
+ with \<open>fst x \<notin> dom m\<close> have "Map.graph m \<subseteq> Map.graph (m(k \<mapsto> v))"
+ by(auto simp: graph_def)
+ with assms Pair show ?thesis
+ unfolding sorted_fst_list_of_set_insort_Map_graph[OF assms] insort_insert_key_def
+ using folding_Map_graph.set_sorted_key_list_of_set in_graphD by (fastforce split: if_splits)
+qed
+
+lemma linorder_finite_Map_induct[consumes 1, case_names empty update]:
+ fixes m :: "'a::linorder \<rightharpoonup> 'b"
+ assumes "finite (dom m)"
+ assumes "P Map.empty"
+ assumes "\<And>k v m. \<lbrakk> finite (dom m); k \<notin> dom m; (\<And>k'. k' \<in> dom m \<Longrightarrow> k' \<le> k); P m \<rbrakk>
+ \<Longrightarrow> P (m(k \<mapsto> v))"
+ shows "P m"
+proof -
+ let ?key_list = "\<lambda>m. sorted_list_of_set (dom m)"
+ from assms(1,2) show ?thesis
+ proof(induction "length (?key_list m)" arbitrary: m)
+ case 0
+ then have "sorted_list_of_set (dom m) = []"
+ by auto
+ with \<open>finite (dom m)\<close> have "m = Map.empty"
+ by auto
+ with \<open>P Map.empty\<close> show ?case by simp
+ next
+ case (Suc n)
+ then obtain x xs where x_xs: "sorted_list_of_set (dom m) = xs @ [x]"
+ by (metis append_butlast_last_id length_greater_0_conv zero_less_Suc)
+ have "sorted_list_of_set (dom (m(x := None))) = xs"
+ proof -
+ have "distinct (xs @ [x])"
+ by (metis sorted_list_of_set.distinct_sorted_key_list_of_set x_xs)
+ then have "remove1 x (xs @ [x]) = xs"
+ by (simp add: remove1_append)
+ with \<open>finite (dom m)\<close> x_xs show ?thesis
+ by (simp add: sorted_list_of_set_remove)
+ qed
+ moreover have "k \<le> x" if "k \<in> dom (m(x := None))" for k
+ proof -
+ from x_xs have "sorted (xs @ [x])"
+ by (metis sorted_list_of_set.sorted_sorted_key_list_of_set)
+ moreover from \<open>k \<in> dom (m(x := None))\<close> have "k \<in> set xs"
+ using \<open>finite (dom m)\<close> \<open>sorted_list_of_set (dom (m(x := None))) = xs\<close>
+ by auto
+ ultimately show "k \<le> x"
+ by (simp add: sorted_append)
+ qed
+ moreover from \<open>finite (dom m)\<close> have "finite (dom (m(x := None)))" "x \<notin> dom (m(x := None))"
+ by simp_all
+ moreover have "P (m(x := None))"
+ using Suc \<open>sorted_list_of_set (dom (m(x := None))) = xs\<close> x_xs by auto
+ ultimately show ?case
+ using assms(3)[where ?m="m(x := None)"] by (metis fun_upd_triv fun_upd_upd not_Some_eq)
+ qed
+qed
+
+lemma delete_insort_fst[simp]: "AList.delete k (insort_key fst (k, v) xs) = AList.delete k xs"
+ by (induction xs) simp_all
+
+lemma insort_fst_delete: "\<lbrakk> fst x \<noteq> k2; sorted (List.map fst xs) \<rbrakk>
+ \<Longrightarrow> insort_key fst x (AList.delete k2 xs) = AList.delete k2 (insort_key fst x xs)"
+ by (induction xs) (fastforce simp add: insort_is_Cons order_trans)+
+
+lemma sorted_fst_list_of_set_Map_graph_fun_upd_None[simp]:
+ "sorted_key_list_of_set fst (Map.graph (m(k := None)))
+ = AList.delete k (sorted_key_list_of_set fst (Map.graph m))"
+proof(cases "finite (Map.graph m)")
+ assume "finite (Map.graph m)"
+ from this[unfolded finite_graph_iff_finite_dom] show ?thesis
+ proof(induction rule: finite_Map_induct)
+ let ?list_of="sorted_key_list_of_set fst"
+ case (update k2 v2 m)
+ note [simp] = \<open>k2 \<notin> dom m\<close> \<open>finite (dom m)\<close>
+
+ have right_eq: "AList.delete k (?list_of (Map.graph (m(k2 \<mapsto> v2))))
+ = AList.delete k (insort_key fst (k2, v2) (?list_of (Map.graph m)))"
+ by simp
+
+ show ?case
+ proof(cases "k = k2")
+ case True
+ then have "?list_of (Map.graph ((m(k2 \<mapsto> v2))(k := None)))
+ = AList.delete k (insort_key fst (k2, v2) (?list_of (Map.graph m)))"
+ using fst_graph_eq_dom update.IH by auto
+ then show ?thesis
+ using right_eq by metis
+ next
+ case False
+ then have "AList.delete k (insort_key fst (k2, v2) (?list_of (Map.graph m)))
+ = insort_key fst (k2, v2) (?list_of (Map.graph (m(k := None))))"
+ by (auto simp add: insort_fst_delete update.IH
+ folding_Map_graph.sorted_sorted_key_list_of_set[OF subset_refl])
+ also have "\<dots> = ?list_of (insert (k2, v2) (Map.graph (m(k := None))))"
+ by auto
+ also from False \<open>k2 \<notin> dom m\<close> have "\<dots> = ?list_of (Map.graph ((m(k2 \<mapsto> v2))(k := None)))"
+ by (metis graph_map_upd domIff fun_upd_triv fun_upd_twist)
+ finally show ?thesis using right_eq by metis
+ qed
+ qed simp
+qed simp
+
+lemma entries_lookup: "entries m = Map.graph (lookup m)"
+ by transfer rule
+
+lemma entries_empty[simp]: "entries empty = {}"
+ by transfer (fact graph_empty)
+
+lemma finite_entries_iff_finite_keys[simp]:
+ "finite (entries m) = finite (keys m)"
+ by transfer (fact finite_graph_iff_finite_dom)
+
+lemma entries_update[simp]:
+ "entries (update k v m) = insert (k, v) (entries (delete k m))"
+ by transfer (fact graph_map_upd)
+
+lemma Mapping_delete_if_notin_keys[simp]:
+ "k \<notin> Mapping.keys m \<Longrightarrow> delete k m = m"
+ by transfer simp
+
+lemma entries_delete:
+ "entries (delete k m) = {e \<in> entries m. fst e \<noteq> k}"
+ by transfer (fact graph_fun_upd_None)
+
+lemma entries_of_alist[simp]:
+ "distinct (List.map fst xs) \<Longrightarrow> entries (of_alist xs) = set xs"
+ by transfer (fact graph_map_of_if_distinct_ran)
+
+lemma entries_keysD:
+ "x \<in> entries m \<Longrightarrow> fst x \<in> keys m"
+ by transfer (fact graph_domD)
+
+lemma finite_keys_entries[simp]:
+ "finite (keys (update k v m)) = finite (keys m)"
+ by transfer simp
+
+lemma set_ordered_entries[simp]:
+ "finite (Mapping.keys m) \<Longrightarrow> set (ordered_entries m) = entries m"
+ unfolding ordered_entries_def
+ by transfer (auto simp: folding_Map_graph.set_sorted_key_list_of_set[OF subset_refl])
+
+lemma distinct_ordered_entries[simp]: "distinct (List.map fst (ordered_entries m))"
+ unfolding ordered_entries_def
+ by transfer (simp add: folding_Map_graph.distinct_sorted_key_list_of_set[OF subset_refl])
+
+lemma sorted_ordered_entries[simp]: "sorted (List.map fst (ordered_entries m))"
+ unfolding ordered_entries_def
+ by transfer (auto intro: folding_Map_graph.sorted_sorted_key_list_of_set)
+
+lemma ordered_entries_infinite[simp]:
+ "\<not> finite (Mapping.keys m) \<Longrightarrow> ordered_entries m = []"
+ by (simp add: ordered_entries_def)
+
+lemma ordered_entries_empty[simp]: "ordered_entries empty = []"
+ by (simp add: ordered_entries_def)
+
+lemma ordered_entries_update[simp]:
+ assumes "finite (keys m)"
+ shows "ordered_entries (update k v m)
+ = insort_insert_key fst (k, v) (AList.delete k (ordered_entries m))"
+proof -
+ let ?list_of="sorted_key_list_of_set fst" and ?insort="insort_insert_key fst"
+
+ have *: "?list_of (insert (k, v) (Map.graph (m(k := None))))
+ = ?insort (k, v) (AList.delete k (?list_of (Map.graph m)))" if "finite (dom m)" for m
+ proof -
+ from \<open>finite (dom m)\<close> have "?list_of (insert (k, v) (Map.graph (m(k := None))))
+ = ?insort (k, v) (?list_of (Map.graph (m(k := None))))"
+ by (intro sorted_fst_list_of_set_insort_insert_Map_graph) (simp_all add: subset_insertI)
+ then show ?thesis by simp
+ qed
+ from assms show ?thesis
+ unfolding ordered_entries_def
+ apply (transfer fixing: k v) using "*" by auto
+qed
+
+lemma ordered_entries_delete[simp]:
+ "ordered_entries (delete k m) = AList.delete k (ordered_entries m)"
+ unfolding ordered_entries_def by transfer auto
+
+lemma fold_empty[simp]: "fold f empty a = a"
+ unfolding fold_def by simp
+
+lemma insort_key_is_snoc_if_sorted_and_distinct:
+ assumes "sorted (List.map f xs)" "f y \<notin> f ` set xs" "\<forall>x \<in> set xs. f x \<le> f y"
+ shows "insort_key f y xs = xs @ [y]"
+ using assms by (induction xs) (auto dest!: insort_is_Cons)
+
+lemma fold_update:
+ assumes "finite (keys m)"
+ assumes "k \<notin> keys m" "\<And>k'. k' \<in> keys m \<Longrightarrow> k' \<le> k"
+ shows "fold f (update k v m) a = f k v (fold f m a)"
+proof -
+ from assms have k_notin_entries: "k \<notin> fst ` set (ordered_entries m)"
+ using entries_keysD by fastforce
+ with assms have "ordered_entries (update k v m)
+ = insort_insert_key fst (k, v) (ordered_entries m)"
+ by simp
+ also from k_notin_entries have "\<dots> = ordered_entries m @ [(k, v)]"
+ proof -
+ from assms have "\<forall>x \<in> set (ordered_entries m). fst x \<le> fst (k, v)"
+ unfolding ordered_entries_def
+ by transfer (fastforce simp: folding_Map_graph.set_sorted_key_list_of_set[OF order_refl]
+ dest: graph_domD)
+ from insort_key_is_snoc_if_sorted_and_distinct[OF _ _ this] k_notin_entries show ?thesis
+ unfolding insort_insert_key_def by auto
+ qed
+ finally show ?thesis unfolding fold_def by simp
+qed
+
+lemma linorder_finite_Mapping_induct[consumes 1, case_names empty update]:
+ fixes m :: "('a::linorder, 'b) mapping"
+ assumes "finite (keys m)"
+ assumes "P empty"
+ assumes "\<And>k v m.
+ \<lbrakk> finite (keys m); k \<notin> keys m; (\<And>k'. k' \<in> keys m \<Longrightarrow> k' \<le> k); P m \<rbrakk>
+ \<Longrightarrow> P (update k v m)"
+ shows "P m"
+ using assms by transfer (simp add: linorder_finite_Map_induct)
+
subsection \<open>Code generator setup\<close>
hide_const (open) empty is_empty rep lookup lookup_default filter update delete ordered_keys
keys size replace default map_entry map_default tabulate bulkload map map_values combine of_alist
+ entries ordered_entries fold
end
--- a/src/HOL/Library/Multiset.thy Mon May 31 20:27:45 2021 +0000
+++ b/src/HOL/Library/Multiset.thy Tue Jun 01 19:46:34 2021 +0200
@@ -1610,7 +1610,7 @@
by (simp add: not_in_iff)
from False have "Finite_Set.fold (\<lambda>y. f y ^^ count (add_mset x M) y) s (set_mset M) =
Finite_Set.fold (\<lambda>y. f y ^^ count M y) s (set_mset M)"
- by (auto intro!: Finite_Set.fold_cong comp_fun_commute_funpow)
+ by (auto intro!: Finite_Set.fold_cong comp_fun_commute_on_funpow)
with False * show ?thesis
by (simp add: fold_mset_def del: count_add_mset)
next
@@ -1619,7 +1619,7 @@
from N_def True have *: "set_mset M = insert x N" "x \<notin> N" "finite N" by auto
then have "Finite_Set.fold (\<lambda>y. f y ^^ count (add_mset x M) y) s N =
Finite_Set.fold (\<lambda>y. f y ^^ count M y) s N"
- by (auto intro!: Finite_Set.fold_cong comp_fun_commute_funpow)
+ by (auto intro!: Finite_Set.fold_cong comp_fun_commute_on_funpow)
with * show ?thesis by (simp add: fold_mset_def del: count_add_mset) simp
qed
qed
@@ -1984,7 +1984,7 @@
by (induct xs) simp_all
global_interpretation mset_set: folding add_mset "{#}"
- defines mset_set = "folding.F add_mset {#}"
+ defines mset_set = "folding_on.F add_mset {#}"
by standard (simp add: fun_eq_iff)
lemma sum_multiset_singleton [simp]: "sum (\<lambda>n. {#n#}) A = mset_set A"
--- a/src/HOL/Library/RBT.thy Mon May 31 20:27:45 2021 +0000
+++ b/src/HOL/Library/RBT.thy Tue Jun 01 19:46:34 2021 +0200
@@ -196,6 +196,9 @@
lemma distinct_entries: "distinct (List.map fst (entries t))"
by transfer (simp add: distinct_entries)
+lemma sorted_entries: "sorted (List.map fst (entries t))"
+ by (transfer) (simp add: rbt_sorted_entries)
+
lemma non_empty_keys: "t \<noteq> empty \<Longrightarrow> keys t \<noteq> []"
by transfer (simp add: non_empty_rbt_keys)
--- a/src/HOL/Library/RBT_Mapping.thy Mon May 31 20:27:45 2021 +0000
+++ b/src/HOL/Library/RBT_Mapping.thy Tue Jun 01 19:46:34 2021 +0200
@@ -57,6 +57,24 @@
unfolding ordered_keys_def
by (transfer fixing: t) (auto simp add: lookup_keys intro: sorted_distinct_set_unique)
+lemma Map_graph_lookup: "Map.graph (RBT.lookup t) = set (RBT.entries t)"
+ by (metis RBT.distinct_entries RBT.map_of_entries graph_map_of_if_distinct_ran)
+
+lemma entries_Mapping [code]: "Mapping.entries (Mapping t) = set (RBT.entries t)"
+ by (transfer fixing: t) (fact Map_graph_lookup)
+
+lemma ordered_entries_Mapping [code]: "Mapping.ordered_entries (Mapping t) = RBT.entries t"
+proof -
+ note folding_Map_graph.idem_if_sorted_distinct[
+ where ?m="RBT.lookup t", OF _ _ folding_Map_graph.distinct_if_distinct_map]
+ then show ?thesis
+ unfolding ordered_entries_def
+ by (transfer fixing: t) (auto simp: Map_graph_lookup distinct_entries sorted_entries)
+qed
+
+lemma fold_Mapping [code]: "Mapping.fold f (Mapping t) a = RBT.fold f t a"
+ by (simp add: Mapping.fold_def fold_fold ordered_entries_Mapping)
+
lemma Mapping_size_card_keys: (*FIXME*)
"Mapping.size m = card (Mapping.keys m)"
unfolding size_def by transfer simp
@@ -100,7 +118,7 @@
lemma equal_Mapping [code]:
"HOL.equal (Mapping t1) (Mapping t2) \<longleftrightarrow> RBT.entries t1 = RBT.entries t2"
- by (transfer fixing: t1 t2) (simp add: entries_lookup)
+ by (transfer fixing: t1 t2) (simp add: RBT.entries_lookup)
lemma [code nbe]:
"HOL.equal (x :: (_, _) mapping) x \<longleftrightarrow> True"
--- a/src/HOL/Library/RBT_Set.thy Mon May 31 20:27:45 2021 +0000
+++ b/src/HOL/Library/RBT_Set.thy Tue Jun 01 19:46:34 2021 +0200
@@ -58,6 +58,8 @@
assumes "comp_fun_commute f"
shows "Finite_Set.fold f A (set (RBT.entries t)) = RBT.fold (curry f) t A"
proof -
+ interpret comp_fun_commute: comp_fun_commute f
+ by (fact assms)
have *: "remdups (RBT.entries t) = RBT.entries t"
using distinct_entries distinct_map by (auto intro: distinct_remdups_id)
show ?thesis using assms by (auto simp: fold_def_alt comp_fun_commute.fold_set_fold_remdups *)
--- a/src/HOL/Lifting_Set.thy Mon May 31 20:27:45 2021 +0000
+++ b/src/HOL/Lifting_Set.thy Tue Jun 01 19:46:34 2021 +0200
@@ -329,4 +329,44 @@
shows "rel_set R (\<Union>(f ` A)) (\<Union>(g ` B))"
by transfer_prover
+context
+ includes lifting_syntax
+begin
+
+lemma fold_graph_transfer[transfer_rule]:
+ assumes "bi_unique R" "right_total R"
+ shows "((R ===> (=) ===> (=)) ===> (=) ===> rel_set R ===> (=) ===> (=)) fold_graph fold_graph"
+proof(intro rel_funI)
+ fix f1 :: "'a \<Rightarrow> 'c \<Rightarrow> 'c" and f2 :: "'b \<Rightarrow> 'c \<Rightarrow> 'c"
+ assume rel_f: "(R ===> (=) ===> (=)) f1 f2"
+ fix z1 z2 :: 'c assume [simp]: "z1 = z2"
+ fix A1 A2 assume rel_A: "rel_set R A1 A2"
+ fix y1 y2 :: 'c assume [simp]: "y1 = y2"
+
+ from \<open>bi_unique R\<close> \<open>right_total R\<close> have The_y: "\<forall>y. \<exists>!x. R x y"
+ unfolding bi_unique_def right_total_def by auto
+ define r where "r \<equiv> \<lambda>y. THE x. R x y"
+
+ from The_y have r_y: "R (r y) y" for y
+ unfolding r_def using the_equality by fastforce
+ with assms rel_A have "inj_on r A2" "A1 = r ` A2"
+ unfolding r_def rel_set_def inj_on_def bi_unique_def
+ apply(auto simp: image_iff) by metis+
+ with \<open>bi_unique R\<close> rel_f r_y have "(f1 o r) y = f2 y" for y
+ unfolding bi_unique_def rel_fun_def by auto
+ then have "(f1 o r) = f2"
+ by blast
+ then show "fold_graph f1 z1 A1 y1 = fold_graph f2 z2 A2 y2"
+ by (fastforce simp: fold_graph_image[OF \<open>inj_on r A2\<close>] \<open>A1 = r ` A2\<close>)
+qed
+
+lemma fold_transfer[transfer_rule]:
+ assumes [transfer_rule]: "bi_unique R" "right_total R"
+ shows "((R ===> (=) ===> (=)) ===> (=) ===> rel_set R ===> (=)) Finite_Set.fold Finite_Set.fold"
+ unfolding Finite_Set.fold_def
+ by transfer_prover
+
end
+
+
+end
--- a/src/HOL/List.thy Mon May 31 20:27:45 2021 +0000
+++ b/src/HOL/List.thy Tue Jun 01 19:46:34 2021 +0200
@@ -3124,13 +3124,16 @@
text \<open>\<^const>\<open>Finite_Set.fold\<close> and \<^const>\<open>fold\<close>\<close>
-lemma (in comp_fun_commute) fold_set_fold_remdups:
- "Finite_Set.fold f y (set xs) = fold f (remdups xs) y"
- by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_left_comm insert_absorb)
-
-lemma (in comp_fun_idem) fold_set_fold:
- "Finite_Set.fold f y (set xs) = fold f xs y"
- by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_left_comm)
+lemma (in comp_fun_commute_on) fold_set_fold_remdups:
+ assumes "set xs \<subseteq> S"
+ shows "Finite_Set.fold f y (set xs) = fold f (remdups xs) y"
+ by (rule sym, use assms in \<open>induct xs arbitrary: y\<close>)
+ (simp_all add: insert_absorb fold_fun_left_comm)
+
+lemma (in comp_fun_idem_on) fold_set_fold:
+ assumes "set xs \<subseteq> S"
+ shows "Finite_Set.fold f y (set xs) = fold f xs y"
+ by (rule sym, use assms in \<open>induct xs arbitrary: y\<close>) (simp_all add: fold_fun_left_comm)
lemma union_set_fold [code]: "set xs \<union> A = fold Set.insert xs A"
proof -
@@ -5785,6 +5788,10 @@
lemma distinct_insort: "distinct (insort_key f x xs) = (x \<notin> set xs \<and> distinct xs)"
by(induct xs)(auto simp: set_insort_key)
+lemma distinct_insort_key:
+ "distinct (map f (insort_key f x xs)) = (f x \<notin> f ` set xs \<and> (distinct (map f xs)))"
+by (induct xs) (auto simp: set_insort_key)
+
lemma distinct_sort[simp]: "distinct (sort_key f xs) = distinct xs"
by (induct xs) (simp_all add: distinct_insort)
@@ -5897,8 +5904,8 @@
"filter P (sort_key f xs) = sort_key f (filter P xs)"
by (induct xs) (simp_all add: filter_insort_triv filter_insort)
-lemma remove1_insort [simp]:
- "remove1 x (insort x xs) = xs"
+lemma remove1_insort_key [simp]:
+ "remove1 x (insort_key f x xs) = xs"
by (induct xs) simp_all
end
@@ -6087,98 +6094,149 @@
qed
-subsubsection \<open>\<open>sorted_list_of_set\<close>\<close>
-
-text\<open>This function maps (finite) linearly ordered sets to sorted
-lists. Warning: in most cases it is not a good idea to convert from
-sets to lists but one should convert in the other direction (via
-\<^const>\<open>set\<close>).\<close>
-
-context linorder
+subsubsection \<open>\<open>sorted_key_list_of_set\<close>\<close>
+
+text\<open>
+ This function maps (finite) linearly ordered sets to sorted lists.
+ The linear order is obtained by a key function that maps the elements of the set to a type
+ that is linearly ordered.
+ Warning: in most cases it is not a good idea to convert from
+ sets to lists but one should convert in the other direction (via \<^const>\<open>set\<close>).
+
+ Note: this is a generalisation of the older \<open>sorted_list_of_set\<close> that is obtained by setting
+ the key function to the identity. Consequently, new theorems should be added to the locale
+ below. They should also be aliased to more convenient names for use with \<open>sorted_list_of_set\<close>
+ as seen further below.
+\<close>
+
+definition (in linorder) sorted_key_list_of_set :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'b list"
+ where "sorted_key_list_of_set f \<equiv> folding_on.F (insort_key f) []"
+
+locale folding_insort_key = lo?: linorder "less_eq :: 'a \<Rightarrow> 'a \<Rightarrow> bool" less
+ for less_eq (infix "\<preceq>" 50) and less (infix "\<prec>" 50) +
+ fixes S
+ fixes f :: "'b \<Rightarrow> 'a"
+ assumes inj_on: "inj_on f S"
begin
-definition sorted_list_of_set :: "'a set \<Rightarrow> 'a list" where
- "sorted_list_of_set = folding.F insort []"
-
-sublocale sorted_list_of_set: folding insort Nil
-rewrites
- "folding.F insort [] = sorted_list_of_set"
+lemma insort_key_commute:
+ "x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> insort_key f y o insort_key f x = insort_key f x o insort_key f y"
+proof(rule ext, goal_cases)
+ case (1 xs)
+ with inj_on show ?case by (induction xs) (auto simp: inj_onD)
+qed
+
+sublocale fold_insort_key: folding_on S "insort_key f" "[]"
+ rewrites "folding_on.F (insort_key f) [] = sorted_key_list_of_set f"
proof -
- interpret comp_fun_commute insort by (fact comp_fun_commute_insort)
- show "folding insort" by standard (fact comp_fun_commute)
- show "folding.F insort [] = sorted_list_of_set" by (simp only: sorted_list_of_set_def)
-qed
-
-lemma sorted_list_of_set_empty:
- "sorted_list_of_set {} = []"
- by (fact sorted_list_of_set.empty)
-
-lemma sorted_list_of_set_insert [simp]:
- "finite A \<Longrightarrow> sorted_list_of_set (insert x A) = insort x (sorted_list_of_set (A - {x}))"
- by (fact sorted_list_of_set.insert_remove)
-
-lemma sorted_list_of_set_eq_Nil_iff [simp]:
- "finite A \<Longrightarrow> sorted_list_of_set A = [] \<longleftrightarrow> A = {}"
- by (auto simp: sorted_list_of_set.remove)
-
-lemma set_sorted_list_of_set [simp]:
- "finite A \<Longrightarrow> set (sorted_list_of_set A) = A"
- by(induct A rule: finite_induct) (simp_all add: set_insort_key)
-
-lemma sorted_sorted_list_of_set [simp]: "sorted (sorted_list_of_set A)"
+ show "folding_on S (insort_key f)"
+ by standard (simp add: insort_key_commute)
+qed (simp add: sorted_key_list_of_set_def)
+
+lemma idem_if_sorted_distinct:
+ assumes "set xs \<subseteq> S" and "sorted (map f xs)" "distinct xs"
+ shows "sorted_key_list_of_set f (set xs) = xs"
+proof(cases "S = {}")
+ case True
+ then show ?thesis using \<open>set xs \<subseteq> S\<close> by auto
+next
+ case False
+ with assms show ?thesis
+ proof(induction xs)
+ case (Cons a xs)
+ with Cons show ?case by (cases xs) auto
+ qed simp
+qed
+
+lemma sorted_key_list_of_set_empty:
+ "sorted_key_list_of_set f {} = []"
+ by (fact fold_insort_key.empty)
+
+lemma sorted_key_list_of_set_insert:
+ assumes "insert x A \<subseteq> S" and "finite A" "x \<notin> A"
+ shows "sorted_key_list_of_set f (insert x A)
+ = insort_key f x (sorted_key_list_of_set f A)"
+ using assms by (fact fold_insort_key.insert)
+
+lemma sorted_key_list_of_set_insert_remove [simp]:
+ assumes "insert x A \<subseteq> S" and "finite A"
+ shows "sorted_key_list_of_set f (insert x A)
+ = insort_key f x (sorted_key_list_of_set f (A - {x}))"
+ using assms by (fact fold_insort_key.insert_remove)
+
+lemma sorted_key_list_of_set_eq_Nil_iff [simp]:
+ assumes "A \<subseteq> S" and "finite A"
+ shows "sorted_key_list_of_set f A = [] \<longleftrightarrow> A = {}"
+ using assms by (auto simp: fold_insort_key.remove)
+
+lemma set_sorted_key_list_of_set [simp]:
+ assumes "A \<subseteq> S" and "finite A"
+ shows "set (sorted_key_list_of_set f A) = A"
+ using assms(2,1)
+ by (induct A rule: finite_induct) (simp_all add: set_insort_key)
+
+lemma sorted_sorted_key_list_of_set [simp]:
+ assumes "A \<subseteq> S"
+ shows "sorted (map f (sorted_key_list_of_set f A))"
proof (cases "finite A")
- case True thus ?thesis by(induction A) (simp_all add: sorted_insort)
+ case True thus ?thesis using \<open>A \<subseteq> S\<close>
+ by (induction A) (simp_all add: sorted_insort_key)
next
case False thus ?thesis by simp
qed
-lemma distinct_sorted_list_of_set [simp]: "distinct (sorted_list_of_set A)"
+lemma distinct_if_distinct_map: "distinct (map f xs) \<Longrightarrow> distinct xs"
+ using inj_on by (simp add: distinct_map)
+
+lemma distinct_sorted_key_list_of_set [simp]:
+ assumes "A \<subseteq> S"
+ shows "distinct (map f (sorted_key_list_of_set f A))"
proof (cases "finite A")
- case True thus ?thesis by(induction A) (simp_all add: distinct_insort)
-next
+ case True thus ?thesis using \<open>A \<subseteq> S\<close> inj_on
+ by (induction A) (force simp: distinct_insort_key dest: inj_onD)+
+ next
case False thus ?thesis by simp
qed
-lemma length_sorted_list_of_set [simp]: "length (sorted_list_of_set A) = card A"
+lemma length_sorted_key_list_of_set [simp]:
+ assumes "A \<subseteq> S"
+ shows "length (sorted_key_list_of_set f A) = card A"
proof (cases "finite A")
case True
- then show ?thesis
- by(metis distinct_card distinct_sorted_list_of_set set_sorted_list_of_set)
+ with assms inj_on show ?thesis
+ using distinct_card[symmetric, OF distinct_sorted_key_list_of_set]
+ by (auto simp: subset_inj_on intro!: card_image)
qed auto
-lemmas sorted_list_of_set = set_sorted_list_of_set sorted_sorted_list_of_set distinct_sorted_list_of_set
-
-lemma sorted_list_of_set_sort_remdups [code]:
- "sorted_list_of_set (set xs) = sort (remdups xs)"
-proof -
- interpret comp_fun_commute insort by (fact comp_fun_commute_insort)
- show ?thesis by (simp add: sorted_list_of_set.eq_fold sort_conv_fold fold_set_fold_remdups)
-qed
-
-lemma sorted_list_of_set_remove:
- assumes "finite A"
- shows "sorted_list_of_set (A - {x}) = remove1 x (sorted_list_of_set A)"
+lemmas sorted_key_list_of_set =
+ set_sorted_key_list_of_set sorted_sorted_key_list_of_set distinct_sorted_key_list_of_set
+
+lemma sorted_key_list_of_set_remove:
+ assumes "insert x A \<subseteq> S" and "finite A"
+ shows "sorted_key_list_of_set f (A - {x}) = remove1 x (sorted_key_list_of_set f A)"
proof (cases "x \<in> A")
- case False with assms have "x \<notin> set (sorted_list_of_set A)" by simp
+ case False with assms have "x \<notin> set (sorted_key_list_of_set f A)" by simp
with False show ?thesis by (simp add: remove1_idem)
next
case True then obtain B where A: "A = insert x B" by (rule Set.set_insert)
with assms show ?thesis by simp
qed
-lemma strict_sorted_list_of_set [simp]: "sorted_wrt (<) (sorted_list_of_set A)"
- by (simp add: strict_sorted_iff)
+lemma strict_sorted_key_list_of_set [simp]:
+ "A \<subseteq> S \<Longrightarrow> sorted_wrt (\<prec>) (map f (sorted_key_list_of_set f A))"
+ by (cases "finite A") (auto simp: strict_sorted_iff subset_inj_on[OF inj_on])
lemma finite_set_strict_sorted:
- assumes "finite A"
- obtains l where "sorted_wrt (<) l" "set l = A" "length l = card A"
- by (metis assms distinct_card distinct_sorted_list_of_set set_sorted_list_of_set strict_sorted_list_of_set)
-
-lemma strict_sorted_equal:
+ assumes "A \<subseteq> S" and "finite A"
+ obtains l where "sorted_wrt (\<prec>) (map f l)" "set l = A" "length l = card A"
+ using assms
+ by (meson length_sorted_key_list_of_set set_sorted_key_list_of_set strict_sorted_key_list_of_set)
+
+lemma (in linorder) strict_sorted_equal:
assumes "sorted_wrt (<) xs"
- and "sorted_wrt (<) ys"
- and "set ys = set xs"
- shows "ys = xs"
+ and "sorted_wrt (<) ys"
+ and "set ys = set xs"
+ shows "ys = xs"
using assms
proof (induction xs arbitrary: ys)
case (Cons x xs)
@@ -6197,22 +6255,73 @@
using local.Cons by blast
qed
qed auto
-
-lemma strict_sorted_equal_Uniq: "\<exists>\<^sub>\<le>\<^sub>1xs. sorted_wrt (<) xs \<and> set xs = A"
+
+lemma (in linorder) strict_sorted_equal_Uniq: "\<exists>\<^sub>\<le>\<^sub>1xs. sorted_wrt (<) xs \<and> set xs = A"
by (simp add: Uniq_def strict_sorted_equal)
-lemma sorted_list_of_set_inject:
- assumes "sorted_list_of_set A = sorted_list_of_set B" "finite A" "finite B"
+lemma sorted_key_list_of_set_inject:
+ assumes "A \<subseteq> S" "B \<subseteq> S"
+ assumes "sorted_key_list_of_set f A = sorted_key_list_of_set f B" "finite A" "finite B"
shows "A = B"
- using assms set_sorted_list_of_set by fastforce
-
-lemma sorted_list_of_set_unique:
- assumes "finite A"
- shows "sorted_wrt (<) l \<and> set l = A \<and> length l = card A \<longleftrightarrow> sorted_list_of_set A = l"
- using assms strict_sorted_equal by force
+ using assms set_sorted_key_list_of_set by metis
+
+lemma sorted_key_list_of_set_unique:
+ assumes "A \<subseteq> S" and "finite A"
+ shows "sorted_wrt (\<prec>) (map f l) \<and> set l = A \<and> length l = card A
+ \<longleftrightarrow> sorted_key_list_of_set f A = l"
+ using assms
+ by (auto simp: strict_sorted_iff card_distinct idem_if_sorted_distinct)
end
+context linorder
+begin
+
+definition "sorted_list_of_set \<equiv> sorted_key_list_of_set (\<lambda>x::'a. x)"
+
+text \<open>
+ We abuse the \<open>rewrites\<close> functionality of locales to remove trivial assumptions that result
+ from instantiating the key function to the identity.
+\<close>
+sublocale sorted_list_of_set: folding_insort_key "(\<le>)" "(<)" UNIV "(\<lambda>x. x)"
+ rewrites "sorted_key_list_of_set (\<lambda>x. x) = sorted_list_of_set"
+ and "\<And>xs. map (\<lambda>x. x) xs \<equiv> xs"
+ and "\<And>X. (X \<subseteq> UNIV) \<equiv> True"
+ and "\<And>x. x \<in> UNIV \<equiv> True"
+ and "\<And>P. (True \<Longrightarrow> P) \<equiv> Trueprop P"
+ and "\<And>P Q. (True \<Longrightarrow> PROP P \<Longrightarrow> PROP Q) \<equiv> (PROP P \<Longrightarrow> True \<Longrightarrow> PROP Q)"
+proof -
+ show "folding_insort_key (\<le>) (<) UNIV (\<lambda>x. x)"
+ by standard simp
+qed (simp_all add: sorted_list_of_set_def)
+
+text \<open>Alias theorems for backwards compatibility and ease of use.\<close>
+lemmas sorted_list_of_set = sorted_list_of_set.sorted_key_list_of_set and
+ sorted_list_of_set_empty = sorted_list_of_set.sorted_key_list_of_set_empty and
+ sorted_list_of_set_insert = sorted_list_of_set.sorted_key_list_of_set_insert and
+ sorted_list_of_set_insert_remove = sorted_list_of_set.sorted_key_list_of_set_insert_remove and
+ sorted_list_of_set_eq_Nil_iff = sorted_list_of_set.sorted_key_list_of_set_eq_Nil_iff and
+ set_sorted_list_of_set = sorted_list_of_set.set_sorted_key_list_of_set and
+ sorted_sorted_list_of_set = sorted_list_of_set.sorted_sorted_key_list_of_set and
+ distinct_sorted_list_of_set = sorted_list_of_set.distinct_sorted_key_list_of_set and
+ length_sorted_list_of_set = sorted_list_of_set.length_sorted_key_list_of_set and
+ sorted_list_of_set_remove = sorted_list_of_set.sorted_key_list_of_set_remove and
+ strict_sorted_list_of_set = sorted_list_of_set.strict_sorted_key_list_of_set and
+ sorted_list_of_set_inject = sorted_list_of_set.sorted_key_list_of_set_inject and
+ sorted_list_of_set_unique = sorted_list_of_set.sorted_key_list_of_set_unique and
+ finite_set_strict_sorted = sorted_list_of_set.finite_set_strict_sorted
+
+lemma sorted_list_of_set_sort_remdups [code]:
+ "sorted_list_of_set (set xs) = sort (remdups xs)"
+proof -
+ interpret comp_fun_commute insort by (fact comp_fun_commute_insort)
+ show ?thesis
+ by (simp add: sorted_list_of_set.fold_insort_key.eq_fold sort_conv_fold fold_set_fold_remdups)
+qed
+
+end
+
+
lemma sorted_list_of_set_range [simp]:
"sorted_list_of_set {m..<n} = [m..<n]"
by (rule sorted_distinct_set_unique) simp_all
@@ -6228,7 +6337,8 @@
lemma sorted_list_of_set_nonempty:
assumes "finite A" "A \<noteq> {}"
shows "sorted_list_of_set A = Min A # sorted_list_of_set (A - {Min A})"
- using assms by (auto simp: less_le simp flip: sorted_list_of_set_unique intro: Min_in)
+ using assms
+ by (auto simp: less_le simp flip: sorted_list_of_set.sorted_key_list_of_set_unique intro: Min_in)
lemma sorted_list_of_set_greaterThanLessThan:
assumes "Suc i < j"
--- a/src/HOL/Map.thy Mon May 31 20:27:45 2021 +0000
+++ b/src/HOL/Map.thy Tue Jun 01 19:46:34 2021 +0200
@@ -42,6 +42,10 @@
"ran m = {b. \<exists>a. m a = Some b}"
definition
+ graph :: "('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<times> 'b) set" where
+ "graph m = {(a, b) | a b. m a = Some b}"
+
+definition
map_le :: "('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> bool" (infix "\<subseteq>\<^sub>m" 50) where
"(m\<^sub>1 \<subseteq>\<^sub>m m\<^sub>2) \<longleftrightarrow> (\<forall>a \<in> dom m\<^sub>1. m\<^sub>1 a = m\<^sub>2 a)"
@@ -660,6 +664,9 @@
unfolding ran_def
by force
+lemma fun_upd_None_if_notin_dom[simp]: "k \<notin> dom m \<Longrightarrow> m(k := None) = m"
+ by auto
+
lemma ran_map_add:
assumes "dom m1 \<inter> dom m2 = {}"
shows "ran (m1 ++ m2) = ran m1 \<union> ran m2"
@@ -710,6 +717,62 @@
lemma ran_map_option: "ran (\<lambda>x. map_option f (m x)) = f ` ran m"
by (auto simp add: ran_def)
+subsection \<open>@{term [source] graph}\<close>
+
+lemma graph_empty[simp]: "graph empty = {}"
+ unfolding graph_def by simp
+
+lemma in_graphI: "m k = Some v \<Longrightarrow> (k, v) \<in> graph m"
+ unfolding graph_def by blast
+
+lemma in_graphD: "(k, v) \<in> graph m \<Longrightarrow> m k = Some v"
+ unfolding graph_def by blast
+
+lemma graph_map_upd[simp]: "graph (m(k \<mapsto> v)) = insert (k, v) (graph (m(k := None)))"
+ unfolding graph_def by (auto split: if_splits)
+
+lemma graph_fun_upd_None: "graph (m(k := None)) = {e \<in> graph m. fst e \<noteq> k}"
+ unfolding graph_def by (auto split: if_splits)
+
+lemma graph_restrictD:
+ assumes "(k, v) \<in> graph (m |` A)"
+ shows "k \<in> A" and "m k = Some v"
+ using assms unfolding graph_def
+ by (auto simp: restrict_map_def split: if_splits)
+
+lemma graph_map_comp[simp]: "graph (m1 \<circ>\<^sub>m m2) = graph m2 O graph m1"
+ unfolding graph_def by (auto simp: map_comp_Some_iff relcomp_unfold)
+
+lemma graph_map_add: "dom m1 \<inter> dom m2 = {} \<Longrightarrow> graph (m1 ++ m2) = graph m1 \<union> graph m2"
+ unfolding graph_def using map_add_comm by force
+
+lemma graph_eq_to_snd_dom: "graph m = (\<lambda>x. (x, the (m x))) ` dom m"
+ unfolding graph_def dom_def by force
+
+lemma fst_graph_eq_dom: "fst ` graph m = dom m"
+ unfolding graph_eq_to_snd_dom by force
+
+lemma graph_domD: "x \<in> graph m \<Longrightarrow> fst x \<in> dom m"
+ using fst_graph_eq_dom by (metis imageI)
+
+lemma snd_graph_ran: "snd ` graph m = ran m"
+ unfolding graph_def ran_def by force
+
+lemma graph_ranD: "x \<in> graph m \<Longrightarrow> snd x \<in> ran m"
+ using snd_graph_ran by (metis imageI)
+
+lemma finite_graph_map_of: "finite (graph (map_of al))"
+ unfolding graph_eq_to_snd_dom finite_dom_map_of
+ using finite_dom_map_of by blast
+
+lemma graph_map_of_if_distinct_ran: "distinct (map fst al) \<Longrightarrow> graph (map_of al) = set al"
+ unfolding graph_def by auto
+
+lemma finite_graph_iff_finite_dom[simp]: "finite (graph m) = finite (dom m)"
+ by (metis graph_eq_to_snd_dom finite_imageI fst_graph_eq_dom)
+
+lemma inj_on_fst_graph: "inj_on fst (graph m)"
+ unfolding graph_def inj_on_def by force
subsection \<open>\<open>map_le\<close>\<close>
@@ -857,6 +920,23 @@
qed
qed
-hide_const (open) Map.empty
+lemma finite_Map_induct[consumes 1, case_names empty update]:
+ assumes "finite (dom m)"
+ assumes "P Map.empty"
+ assumes "\<And>k v m. finite (dom m) \<Longrightarrow> k \<notin> dom m \<Longrightarrow> P m \<Longrightarrow> P (m(k \<mapsto> v))"
+ shows "P m"
+ using assms(1)
+proof(induction "dom m" arbitrary: m rule: finite_induct)
+ case empty
+ then show ?case using assms(2) unfolding dom_def by simp
+next
+ case (insert x F)
+ then have "finite (dom (m(x:=None)))" "x \<notin> dom (m(x:=None))" "P (m(x:=None))"
+ by (metis Diff_insert_absorb dom_fun_upd)+
+ with assms(3)[OF this] show ?case
+ by (metis fun_upd_triv fun_upd_upd option.exhaust)
+qed
+
+hide_const (open) Map.empty Map.graph
end
--- a/src/HOL/Relation.thy Mon May 31 20:27:45 2021 +0000
+++ b/src/HOL/Relation.thy Tue Jun 01 19:46:34 2021 +0200
@@ -1242,9 +1242,12 @@
assumes "finite R" "finite S"
shows "R O S = Finite_Set.fold
(\<lambda>(x,y) A. Finite_Set.fold (\<lambda>(w,z) A'. if y = w then Set.insert (x,z) A' else A') A S) {} R"
- using assms
- by (induct R)
- (auto simp: comp_fun_commute.fold_insert comp_fun_commute_relcomp_fold insert_relcomp_fold
- cong: if_cong)
+proof -
+ interpret commute_relcomp_fold: comp_fun_commute
+ "(\<lambda>(x, y) A. Finite_Set.fold (\<lambda>(w, z) A'. if y = w then insert (x, z) A' else A') A S)"
+ by (fact comp_fun_commute_relcomp_fold[OF \<open>finite S\<close>])
+ from assms show ?thesis
+ by (induct R) (auto simp: comp_fun_commute_relcomp_fold insert_relcomp_fold cong: if_cong)
+qed
end
--- a/src/HOL/Topological_Spaces.thy Mon May 31 20:27:45 2021 +0000
+++ b/src/HOL/Topological_Spaces.thy Tue Jun 01 19:46:34 2021 +0200
@@ -35,7 +35,7 @@
using open_Union [of "B ` A"] by simp
lemma open_Inter [continuous_intros, intro]: "finite S \<Longrightarrow> \<forall>T\<in>S. open T \<Longrightarrow> open (\<Inter>S)"
- by (induct set: finite) auto
+ by (induction set: finite) auto
lemma open_INT [continuous_intros, intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. open (B x) \<Longrightarrow> open (\<Inter>x\<in>A. B x)"
using open_Inter [of "B ` A"] by simp