# HG changeset patch
# User nipkow
# Date 1622569594 -7200
# Node ID 9db620f007fab45cad634020f69d17b155042c87
# Parent  26c0ccf17f318614a645ec9136edea1e845989e2
More general fold function for maps

diff -r 26c0ccf17f31 -r 9db620f007fa src/HOL/Finite_Set.thy
--- 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)"
diff -r 26c0ccf17f31 -r 9db620f007fa src/HOL/Library/AList.thy
--- 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)
 
diff -r 26c0ccf17f31 -r 9db620f007fa src/HOL/Library/AList_Mapping.thy
--- 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)
 
diff -r 26c0ccf17f31 -r 9db620f007fa src/HOL/Library/FSet.thy
--- 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
diff -r 26c0ccf17f31 -r 9db620f007fa src/HOL/Library/Finite_Lattice.thy
--- 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 ..
diff -r 26c0ccf17f31 -r 9db620f007fa src/HOL/Library/Mapping.thy
--- 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
diff -r 26c0ccf17f31 -r 9db620f007fa src/HOL/Library/Multiset.thy
--- 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"
diff -r 26c0ccf17f31 -r 9db620f007fa src/HOL/Library/RBT.thy
--- 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)
 
diff -r 26c0ccf17f31 -r 9db620f007fa src/HOL/Library/RBT_Mapping.thy
--- 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"
diff -r 26c0ccf17f31 -r 9db620f007fa src/HOL/Library/RBT_Set.thy
--- 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 *)
diff -r 26c0ccf17f31 -r 9db620f007fa src/HOL/Lifting_Set.thy
--- 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
diff -r 26c0ccf17f31 -r 9db620f007fa src/HOL/List.thy
--- 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" 
diff -r 26c0ccf17f31 -r 9db620f007fa src/HOL/Map.thy
--- 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
diff -r 26c0ccf17f31 -r 9db620f007fa src/HOL/Relation.thy
--- 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
diff -r 26c0ccf17f31 -r 9db620f007fa src/HOL/Topological_Spaces.thy
--- 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