# HG changeset patch
# User traytel
# Date 1615296027 -3600
# Node ID 180981b879296c932be325a75d65633978f256bf
# Parent  d47c8a89c6a57a6f54bc686b62f139483782e65f
generalized confluence-based subdistributivity theorem for quotients;
new example that triggered the generalization

diff -r d47c8a89c6a5 -r 180981b87929 src/HOL/Datatype_Examples/Cyclic_List.thy
--- a/src/HOL/Datatype_Examples/Cyclic_List.thy	Tue Mar 09 11:50:21 2021 +0100
+++ b/src/HOL/Datatype_Examples/Cyclic_List.thy	Tue Mar 09 14:20:27 2021 +0100
@@ -26,8 +26,8 @@
 
 lemma retract_cyclic1:
   assumes "cyclic1 (map f xs) ys"
-  shows "\<exists>zs. cyclic xs zs \<and> ys = map f zs"
-  using assms by(auto simp add: cyclic1.simps rotate1_map intro: cyclic1.intros symclpI1)
+  shows "\<exists>zs. cyclic xs zs \<and> ys = map f zs \<and> set zs \<subseteq> set xs"
+  using assms by(force simp add: cyclic1.simps rotate1_map intro: cyclic1.intros symclpI1)
 
 lemma confluent_quotient_cyclic1:
   "confluent_quotient cyclic1 cyclic cyclic cyclic cyclic cyclic (map fst) (map snd) (map fst) (map snd) list_all2 list_all2 list_all2 set set"
diff -r d47c8a89c6a5 -r 180981b87929 src/HOL/Datatype_Examples/Free_Idempotent_Monoid.thy
--- a/src/HOL/Datatype_Examples/Free_Idempotent_Monoid.thy	Tue Mar 09 11:50:21 2021 +0100
+++ b/src/HOL/Datatype_Examples/Free_Idempotent_Monoid.thy	Tue Mar 09 14:20:27 2021 +0100
@@ -223,13 +223,13 @@
 
 lemma retract_cancel1_aux:
   assumes "cancel1 ys (map f xs)"
-  shows "\<exists>zs. cancel1 zs xs \<and> ys = map f zs"
+  shows "\<exists>zs. cancel1 zs xs \<and> ys = map f zs \<and> set zs \<subseteq> set xs"
   using assms
   by cases(fastforce simp add: map_eq_append_conv append_eq_map_conv intro: cancel1.intros)
 
 lemma retract_cancel1:
   assumes "cancel1 ys (map f xs)"
-  shows "\<exists>zs. eq xs zs \<and> ys = map f zs"
+  shows "\<exists>zs. eq xs zs \<and> ys = map f zs \<and> set zs \<subseteq> set xs"
   using retract_cancel1_aux[OF assms] by(blast intro: symclpI)
 
 lemma cancel1_set_eq:
diff -r d47c8a89c6a5 -r 180981b87929 src/HOL/Datatype_Examples/LDL.thy
--- a/src/HOL/Datatype_Examples/LDL.thy	Tue Mar 09 11:50:21 2021 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,339 +0,0 @@
-theory LDL imports
-  "HOL-Library.Confluent_Quotient"
-begin
-
-datatype 'a rexp = Atom 'a | Alt "'a rexp" "'a rexp" | Conc "'a rexp" "'a rexp" | Star "'a rexp"
-
-inductive ACI (infix "~" 64) where
-  a1: "Alt (Alt r s) t ~ Alt r (Alt s t)"
-| a2: "Alt r (Alt s t) ~ Alt (Alt r s) t"
-| c: "Alt r s ~ Alt s r"
-| i: "r ~ Alt r r"
-| R: "r ~ r"
-| A: "r ~ r' \<Longrightarrow> s ~ s' \<Longrightarrow> Alt r s ~ Alt r' s'"
-| C: "r ~ r' \<Longrightarrow> s ~ s' \<Longrightarrow> Conc r s ~ Conc r' s'"
-| S: "r ~ r' \<Longrightarrow> Star r ~ Star r'"
-
-declare ACI.intros[intro]
-
-abbreviation ACIcl (infix "~~" 64) where "(~~) \<equiv> equivclp (~)"
-
-lemma eq_set_preserves_inter:
-  fixes eq set
-  assumes "\<And>r s. eq r s \<Longrightarrow> set r = set s" and "Ss \<noteq> {}"
-  shows "(\<Inter>As\<in>Ss. {(x, x'). eq x x'} `` {x. set x \<subseteq> As}) \<subseteq> {(x, x'). eq x x'} `` {x. set x \<subseteq> \<Inter> Ss}"
-  using assms by (auto simp: subset_eq) metis
-
-lemma ACI_map_respects:
-  fixes f :: "'a \<Rightarrow> 'b" and r s :: "'a rexp"
-  assumes "r ~ s"
-  shows "map_rexp f r ~ map_rexp f s"
-  using assms by (induct r s rule: ACI.induct) auto
-
-lemma ACIcl_map_respects:
-  fixes f :: "'a \<Rightarrow> 'b" and r s :: "'a rexp"
-  assumes "r ~~ s"
-  shows "map_rexp f r ~~ map_rexp f s"
-  using assms by (induct rule: equivclp_induct) (auto intro: ACI_map_respects equivclp_trans)
-
-lemma ACI_set_eq:
-  fixes r s :: "'a rexp"
-  assumes "r ~ s"
-  shows "set_rexp r = set_rexp s"
-  using assms by (induct r s rule: ACI.induct) auto
-
-lemma ACIcl_set_eq:
-  fixes r s :: "'a rexp"
-  assumes "r ~~ s"
-  shows "set_rexp r = set_rexp s"
-  using assms by (induct rule: equivclp_induct) (auto dest: ACI_set_eq)
-
-lemma Alt_eq_map_rexp_iff:
-  "Alt r s = map_rexp f x \<longleftrightarrow> (\<exists>r' s'. x = Alt r' s' \<and> map_rexp f r' = r \<and> map_rexp f s' = s)"
-  "map_rexp f x = Alt r s \<longleftrightarrow> (\<exists>r' s'. x = Alt r' s' \<and> map_rexp f r' = r \<and> map_rexp f s' = s)"
-  by (cases x; auto)+
-
-lemma Conc_eq_map_rexp_iff:
-  "Conc r s = map_rexp f x \<longleftrightarrow> (\<exists>r' s'. x = Conc r' s' \<and> map_rexp f r' = r \<and> map_rexp f s' = s)"
-  "map_rexp f x = Conc r s \<longleftrightarrow> (\<exists>r' s'. x = Conc r' s' \<and> map_rexp f r' = r \<and> map_rexp f s' = s)"
-  by (cases x; auto)+
-
-lemma Star_eq_map_rexp_iff:
-  "Star r = map_rexp f x \<longleftrightarrow> (\<exists>r'. x = Star r' \<and> map_rexp f r' = r)"
-  "map_rexp f x = Star r \<longleftrightarrow> (\<exists>r'. x = Star r' \<and> map_rexp f r' = r)"
-  by (cases x; auto)+
-
-lemma AA: "r ~~ r' \<Longrightarrow> s ~~ s' \<Longrightarrow> Alt r s ~~ Alt r' s'"
-proof (induct rule: equivclp_induct)
-  case base
-  then show ?case
-    by (induct rule: equivclp_induct) (auto elim!: equivclp_trans)
-next
-  case (step s t)
-  then show ?case
-    by (auto elim!: equivclp_trans)
-qed
-
-lemma AAA: "(~)\<^sup>*\<^sup>* r  r' \<Longrightarrow> (~)\<^sup>*\<^sup>* s s' \<Longrightarrow> (~)\<^sup>*\<^sup>* (Alt r s) (Alt r' s')"
-proof (induct r r' rule: rtranclp.induct)
-  case (rtrancl_refl r)
-  then show ?case
-    by (induct s s' rule: rtranclp.induct)
-      (auto elim!: rtranclp.rtrancl_into_rtrancl)
-next
-  case (rtrancl_into_rtrancl a b c)
-  then show ?case
-    by (auto elim!: rtranclp.rtrancl_into_rtrancl)
-qed
-
-lemma CC: "r ~~ r' \<Longrightarrow> s ~~ s' \<Longrightarrow> Conc r s ~~ Conc r' s'"
-proof (induct rule: equivclp_induct)
-  case base
-  then show ?case
-    by (induct rule: equivclp_induct) (auto elim!: equivclp_trans)
-next
-  case (step s t)
-  then show ?case
-    by (auto elim!: equivclp_trans)
-qed
-
-lemma CCC: "(~)\<^sup>*\<^sup>* r r' \<Longrightarrow> (~)\<^sup>*\<^sup>* s s' \<Longrightarrow> (~)\<^sup>*\<^sup>* (Conc r s) (Conc r' s')"
-proof (induct r r' rule: rtranclp.induct)
-  case (rtrancl_refl r)
-  then show ?case
-    by (induct s s' rule: rtranclp.induct)
-      (auto elim!: rtranclp.rtrancl_into_rtrancl)
-next
-  case (rtrancl_into_rtrancl a b c)
-  then show ?case
-    by (auto elim!: rtranclp.rtrancl_into_rtrancl)
-qed
-
-lemma SS: "r ~~ r' \<Longrightarrow> Star r ~~ Star r'"
-proof (induct rule: equivclp_induct)
-  case (step s t)
-  then show ?case
-    by (auto elim!: equivclp_trans)
-qed auto
-
-lemma SSS: "(~)\<^sup>*\<^sup>* r r' \<Longrightarrow> (~)\<^sup>*\<^sup>* (Star r) (Star r')"
-proof (induct r r' rule: rtranclp.induct)
-  case (rtrancl_into_rtrancl a b c)
-  then show ?case
-    by (auto elim!: rtranclp.rtrancl_into_rtrancl)
-qed auto
-
-lemma map_rexp_ACI_inv: "map_rexp f x ~ y \<Longrightarrow> \<exists>z. x ~~ z \<and> y = map_rexp f z"
-proof (induct "map_rexp f x" y arbitrary: x rule: ACI.induct)
-  case (a1 r s t)
-  then obtain r' s' t' where "x = Alt (Alt r' s') t'"
-    "map_rexp f r' = r" "map_rexp f s' = s" "map_rexp f t' = t"
-    by (auto simp: Alt_eq_map_rexp_iff)
-  then show ?case
-    by (intro exI[of _ "Alt r' (Alt s' t')"]) auto
-next
-  case (a2 r s t)
-  then obtain r' s' t' where "x = Alt r' (Alt s' t')"
-    "map_rexp f r' = r" "map_rexp f s' = s" "map_rexp f t' = t"
-    by (auto simp: Alt_eq_map_rexp_iff)
-  then show ?case
-    by (intro exI[of _ "Alt (Alt r' s') t'"]) auto
-next
-  case (c r s)
-  then obtain r' s' where "x = Alt r' s'"
-    "map_rexp f r' = r" "map_rexp f s' = s"
-    by (auto simp: Alt_eq_map_rexp_iff)
-  then show ?case
-    by (intro exI[of _ "Alt s' r'"]) auto
-next
-  case (i r)
-  then show ?case
-    by (intro exI[of _ "Alt r r"]) auto
-next
-  case (R r)
-  then show ?case by (auto intro: exI[of _ r])
-next
-  case (A r rr s ss)
-  then obtain r' s' where "x = Alt r' s'"
-    "map_rexp f r' = r" "map_rexp f s' = s"
-    by (auto simp: Alt_eq_map_rexp_iff)
-  moreover from A(2)[OF this(2)[symmetric]] A(4)[OF this(3)[symmetric]] obtain rr' ss' where
-    "r' ~~ rr'" "rr = map_rexp f rr'" "s' ~~ ss'" "ss = map_rexp f ss'"
-    by blast
-  ultimately show ?case using A(1,3)
-    by (intro exI[of _ "Alt rr' ss'"]) (auto intro!: AA)
-next
-  case (C r rr s ss)
-  then obtain r' s' where "x = Conc r' s'"
-    "map_rexp f r' = r" "map_rexp f s' = s"
-    by (auto simp: Conc_eq_map_rexp_iff)
-  moreover from C(2)[OF this(2)[symmetric]] C(4)[OF this(3)[symmetric]] obtain rr' ss' where
-    "r' ~~ rr'" "rr = map_rexp f rr'" "s' ~~ ss'" "ss = map_rexp f ss'"
-    by blast
-  ultimately show ?case using C(1,3)
-    by (intro exI[of _ "Conc rr' ss'"]) (auto intro!: CC)
-next
-  case (S r rr)
-  then obtain r' where "x = Star r'" "map_rexp f r' = r"
-    by (auto simp: Star_eq_map_rexp_iff)
-  moreover from S(2)[OF this(2)[symmetric]] obtain rr' where "r' ~~ rr'" "rr = map_rexp f rr'"
-    by blast
-  ultimately show ?case
-    by (intro exI[of _ "Star rr'"]) (auto intro!: SS)
-qed
-
-lemma reflclp_ACI: "(~)\<^sup>=\<^sup>= = (~)"
-  unfolding fun_eq_iff
-  by auto
-
-lemma strong_confluentp_ACI: "strong_confluentp (~)"
-  apply (rule strong_confluentpI, unfold reflclp_ACI)
-  subgoal for x y z
-  proof (induct x y arbitrary: z rule: ACI.induct)
-    case (a1 r s t)
-    then show ?case
-      by (auto intro: AAA converse_rtranclp_into_rtranclp)
-  next
-    case (a2 r s t)
-    then show ?case
-      by (auto intro: AAA converse_rtranclp_into_rtranclp)
-  next
-    case (c r s)
-    then show ?case
-      by (cases rule: ACI.cases) (auto intro: AAA)
-  next
-    case (i r)
-    then show ?case
-      by (auto intro: AAA)
-  next
-    case (R r)
-    then show ?case
-      by auto
-  next
-    note A1 = ACI.A[OF _ R]
-    note A2 = ACI.A[OF R]
-    case (A r r' s s')
-    from A(5,1-4) show ?case
-    proof (cases rule: ACI.cases)
-      case inner: (a1 r'' s'')
-      from A(1,3) show ?thesis
-        unfolding inner
-      proof (elim ACI.cases[of _ r'], goal_cases Xa1 Xa2 XC XI XR XP XT XS)
-        case (Xa1 rr ss tt)
-        with A(3) show ?case
-          by (elim exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ A2[OF A2]], rotated])
-            (metis a1 a2 A1 r_into_rtranclp rtranclp.rtrancl_into_rtrancl)
-      next
-        case (Xa2 r s t)
-        then show ?case
-          by (elim exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ A2[OF A2]], rotated])
-            (metis a1 A1 r_into_rtranclp rtranclp.rtrancl_into_rtrancl)
-      next
-        case (XC r s)
-        then show ?case
-          by (elim exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ A2[OF A2]], rotated])
-            (metis a1 c A1 r_into_rtranclp rtranclp.rtrancl_into_rtrancl)
-      next
-        case (XI r)
-        then show ?case
-          apply (elim exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ ACI.A[OF i ACI.A[OF i]]], rotated])
-          apply hypsubst
-          apply (rule converse_rtranclp_into_rtranclp, rule a1)
-          apply (rule converse_rtranclp_into_rtranclp, rule a1)
-          apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a2)
-          apply (rule converse_rtranclp_into_rtranclp, rule A2, rule A1, rule c)
-          apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a1)
-          apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a1)
-          apply (rule converse_rtranclp_into_rtranclp, rule a2)
-          apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a2)
-          apply blast
-          done
-      qed auto
-    next
-      case inner: (a2 s'' t'')
-      with A(1,3) show ?thesis
-        unfolding inner
-      proof (elim ACI.cases[of _ s'], goal_cases Xa1 Xa2 XC XI XR XP XT XS)
-        case (Xa1 rr ss tt)
-        with A(3) show ?case
-          by (elim exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ A1[OF A1]], rotated])
-            (metis a2 A2 r_into_rtranclp rtranclp.rtrancl_into_rtrancl)
-      next
-        case (Xa2 r s t)
-        then show ?case
-          by (elim exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ A1[OF A1]], rotated])
-            (metis a1 a2 A2 r_into_rtranclp rtranclp.rtrancl_into_rtrancl)
-      next
-        case (XC r s)
-        then show ?case
-          by (elim exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ A1[OF A1]], rotated])
-            (metis a2 c A2 r_into_rtranclp rtranclp.rtrancl_into_rtrancl)
-      next
-        case (XI r)
-        then show ?case
-          apply (elim exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ ACI.A[OF ACI.A[OF _ i] i]], rotated])
-          apply hypsubst
-          apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a2)
-          apply (rule converse_rtranclp_into_rtranclp, rule A2, rule A1, rule c)
-          apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a1)
-          apply (rule converse_rtranclp_into_rtranclp, rule A2, rule A2, rule a1)
-          apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a2)
-          apply (rule converse_rtranclp_into_rtranclp, rule a2)
-          apply blast
-          done
-      qed auto
-    qed (auto 5 0 intro: AAA)
-  next
-    case (C r r' s s')
-    from C(5,1-4) show ?case
-      by (cases rule: ACI.cases) (auto 5 0 intro: CCC)
-  next
-    case (S r r')
-    from S(3,1,2) show ?case
-      by (cases rule: ACI.cases) (auto intro: SSS)
-  qed
-  done
-
-lemma confluent_quotient_ACI:
-  "confluent_quotient (~) (~~) (~~) (~~) (~~) (~~)
-     (map_rexp fst) (map_rexp snd) (map_rexp fst) (map_rexp snd)
-     rel_rexp rel_rexp rel_rexp set_rexp set_rexp"
-  by unfold_locales (auto dest: ACIcl_set_eq simp: rexp.in_rel rexp.rel_compp map_rexp_ACI_inv
-      intro: equivpI reflpI sympI transpI ACIcl_map_respects
-      strong_confluentp_imp_confluentp[OF strong_confluentp_ACI])
-
-inductive ACIEQ (infix "\<approx>" 64) where
-  a: "Alt (Alt r s) t \<approx> Alt r (Alt s t)"
-| c: "Alt r s \<approx> Alt s r"
-| i: "Alt r r \<approx> r"
-| A: "r \<approx> r' \<Longrightarrow> s \<approx> s' \<Longrightarrow> Alt r s \<approx> Alt r' s'"
-| C: "r \<approx> r' \<Longrightarrow> s \<approx> s' \<Longrightarrow> Conc r s \<approx> Conc r' s'"
-| S: "r \<approx> r' \<Longrightarrow> Star r \<approx> Star r'"
-| r: "r \<approx> r"
-| s: "r \<approx> s \<Longrightarrow> s \<approx> r"
-| t: "r \<approx> s \<Longrightarrow> s \<approx> t \<Longrightarrow> r \<approx> t"
-
-lemma ACIEQ_le_ACIcl: "r \<approx> s \<Longrightarrow> r ~~ s"
-  by (induct r s rule: ACIEQ.induct) (auto intro: AA CC SS equivclp_sym equivclp_trans)
-
-lemma ACI_le_ACIEQ: "r ~ s \<Longrightarrow> r \<approx> s"
-  by (induct r s rule: ACI.induct) (auto intro: ACIEQ.intros)
-
-lemma ACIcl_le_ACIEQ: "r ~~ s \<Longrightarrow> r \<approx> s"
-  by (induct rule: equivclp_induct) (auto 0 3 intro: ACIEQ.intros ACI_le_ACIEQ)
-
-lemma ACIEQ_alt: "(\<approx>) = (~~)"
-  by (simp add: ACIEQ_le_ACIcl ACIcl_le_ACIEQ antisym predicate2I)
-
-quotient_type 'a ACI_rexp = "'a rexp" / "(\<approx>)"
-  unfolding ACIEQ_alt by (auto intro!: equivpI reflpI sympI transpI)
-
-lift_bnf 'a ACI_rexp
-  unfolding ACIEQ_alt
-  subgoal for A Q by (rule confluent_quotient.subdistributivity[OF confluent_quotient_ACI])
-  subgoal for Ss by (intro eq_set_preserves_inter[rotated] ACIcl_set_eq; auto)
-  done
-
-datatype ldl = Prop string | And ldl ldl | Not ldl | Match "ldl ACI_rexp"
-
-end
\ No newline at end of file
diff -r d47c8a89c6a5 -r 180981b87929 src/HOL/Datatype_Examples/Regex_ACI.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Datatype_Examples/Regex_ACI.thy	Tue Mar 09 14:20:27 2021 +0100
@@ -0,0 +1,342 @@
+theory Regex_ACI
+  imports "HOL-Library.Confluent_Quotient"
+begin
+
+datatype 'a rexp = Zero | Eps | Atom 'a | Alt "'a rexp" "'a rexp" | Conc "'a rexp" "'a rexp" | Star "'a rexp"
+
+inductive ACI (infix "~" 64) where
+  a1: "Alt (Alt r s) t ~ Alt r (Alt s t)"
+| a2: "Alt r (Alt s t) ~ Alt (Alt r s) t"
+| c: "Alt r s ~ Alt s r"
+| i: "r ~ Alt r r"
+| R: "r ~ r"
+| A: "r ~ r' \<Longrightarrow> s ~ s' \<Longrightarrow> Alt r s ~ Alt r' s'"
+| C: "r ~ r' \<Longrightarrow> s ~ s' \<Longrightarrow> Conc r s ~ Conc r' s'"
+| S: "r ~ r' \<Longrightarrow> Star r ~ Star r'"
+
+declare ACI.intros[intro]
+
+abbreviation ACIcl (infix "~~" 64) where "(~~) \<equiv> equivclp (~)"
+
+lemma eq_set_preserves_inter:
+  fixes eq set
+  assumes "\<And>r s. eq r s \<Longrightarrow> set r = set s" and "Ss \<noteq> {}"
+  shows "(\<Inter>As\<in>Ss. {(x, x'). eq x x'} `` {x. set x \<subseteq> As}) \<subseteq> {(x, x'). eq x x'} `` {x. set x \<subseteq> \<Inter> Ss}"
+  using assms by (auto simp: subset_eq) metis
+
+lemma ACI_map_respects:
+  fixes f :: "'a \<Rightarrow> 'b" and r s :: "'a rexp"
+  assumes "r ~ s"
+  shows "map_rexp f r ~ map_rexp f s"
+  using assms by (induct r s rule: ACI.induct) auto
+
+lemma ACIcl_map_respects:
+  fixes f :: "'a \<Rightarrow> 'b" and r s :: "'a rexp"
+  assumes "r ~~ s"
+  shows "map_rexp f r ~~ map_rexp f s"
+  using assms by (induct rule: equivclp_induct) (auto intro: ACI_map_respects equivclp_trans)
+
+lemma ACI_set_eq:
+  fixes r s :: "'a rexp"
+  assumes "r ~ s"
+  shows "set_rexp r = set_rexp s"
+  using assms by (induct r s rule: ACI.induct) auto
+
+lemma ACIcl_set_eq:
+  fixes r s :: "'a rexp"
+  assumes "r ~~ s"
+  shows "set_rexp r = set_rexp s"
+  using assms by (induct rule: equivclp_induct) (auto dest: ACI_set_eq)
+
+lemma Alt_eq_map_rexp_iff:
+  "Alt r s = map_rexp f x \<longleftrightarrow> (\<exists>r' s'. x = Alt r' s' \<and> map_rexp f r' = r \<and> map_rexp f s' = s)"
+  "map_rexp f x = Alt r s \<longleftrightarrow> (\<exists>r' s'. x = Alt r' s' \<and> map_rexp f r' = r \<and> map_rexp f s' = s)"
+  by (cases x; auto)+
+
+lemma Conc_eq_map_rexp_iff:
+  "Conc r s = map_rexp f x \<longleftrightarrow> (\<exists>r' s'. x = Conc r' s' \<and> map_rexp f r' = r \<and> map_rexp f s' = s)"
+  "map_rexp f x = Conc r s \<longleftrightarrow> (\<exists>r' s'. x = Conc r' s' \<and> map_rexp f r' = r \<and> map_rexp f s' = s)"
+  by (cases x; auto)+
+
+lemma Star_eq_map_rexp_iff:
+  "Star r = map_rexp f x \<longleftrightarrow> (\<exists>r'. x = Star r' \<and> map_rexp f r' = r)"
+  "map_rexp f x = Star r \<longleftrightarrow> (\<exists>r'. x = Star r' \<and> map_rexp f r' = r)"
+  by (cases x; auto)+
+
+lemma AA: "r ~~ r' \<Longrightarrow> s ~~ s' \<Longrightarrow> Alt r s ~~ Alt r' s'"
+proof (induct rule: equivclp_induct)
+  case base
+  then show ?case
+    by (induct rule: equivclp_induct) (auto elim!: equivclp_trans)
+next
+  case (step s t)
+  then show ?case
+    by (auto elim!: equivclp_trans)
+qed
+
+lemma AAA: "(~)\<^sup>*\<^sup>* r  r' \<Longrightarrow> (~)\<^sup>*\<^sup>* s s' \<Longrightarrow> (~)\<^sup>*\<^sup>* (Alt r s) (Alt r' s')"
+proof (induct r r' rule: rtranclp.induct)
+  case (rtrancl_refl r)
+  then show ?case
+    by (induct s s' rule: rtranclp.induct)
+      (auto elim!: rtranclp.rtrancl_into_rtrancl)
+next
+  case (rtrancl_into_rtrancl a b c)
+  then show ?case
+    by (auto elim!: rtranclp.rtrancl_into_rtrancl)
+qed
+
+lemma CC: "r ~~ r' \<Longrightarrow> s ~~ s' \<Longrightarrow> Conc r s ~~ Conc r' s'"
+proof (induct rule: equivclp_induct)
+  case base
+  then show ?case
+    by (induct rule: equivclp_induct) (auto elim!: equivclp_trans)
+next
+  case (step s t)
+  then show ?case
+    by (auto elim!: equivclp_trans)
+qed
+
+lemma CCC: "(~)\<^sup>*\<^sup>* r r' \<Longrightarrow> (~)\<^sup>*\<^sup>* s s' \<Longrightarrow> (~)\<^sup>*\<^sup>* (Conc r s) (Conc r' s')"
+proof (induct r r' rule: rtranclp.induct)
+  case (rtrancl_refl r)
+  then show ?case
+    by (induct s s' rule: rtranclp.induct)
+      (auto elim!: rtranclp.rtrancl_into_rtrancl)
+next
+  case (rtrancl_into_rtrancl a b c)
+  then show ?case
+    by (auto elim!: rtranclp.rtrancl_into_rtrancl)
+qed
+
+lemma SS: "r ~~ r' \<Longrightarrow> Star r ~~ Star r'"
+proof (induct rule: equivclp_induct)
+  case (step s t)
+  then show ?case
+    by (auto elim!: equivclp_trans)
+qed auto
+
+lemma SSS: "(~)\<^sup>*\<^sup>* r r' \<Longrightarrow> (~)\<^sup>*\<^sup>* (Star r) (Star r')"
+proof (induct r r' rule: rtranclp.induct)
+  case (rtrancl_into_rtrancl a b c)
+  then show ?case
+    by (auto elim!: rtranclp.rtrancl_into_rtrancl)
+qed auto
+
+lemma map_rexp_ACI_inv: "map_rexp f x ~ y \<Longrightarrow> \<exists>z. x ~~ z \<and> y = map_rexp f z \<and> set_rexp z \<subseteq> set_rexp x"
+proof (induct "map_rexp f x" y arbitrary: x rule: ACI.induct)
+  case (a1 r s t)
+  then obtain r' s' t' where "x = Alt (Alt r' s') t'"
+    "map_rexp f r' = r" "map_rexp f s' = s" "map_rexp f t' = t"
+    by (auto simp: Alt_eq_map_rexp_iff)
+  then show ?case
+    by (intro exI[of _ "Alt r' (Alt s' t')"]) auto
+next
+  case (a2 r s t)
+  then obtain r' s' t' where "x = Alt r' (Alt s' t')"
+    "map_rexp f r' = r" "map_rexp f s' = s" "map_rexp f t' = t"
+    by (auto simp: Alt_eq_map_rexp_iff)
+  then show ?case
+    by (intro exI[of _ "Alt (Alt r' s') t'"]) auto
+next
+  case (c r s)
+  then obtain r' s' where "x = Alt r' s'"
+    "map_rexp f r' = r" "map_rexp f s' = s"
+    by (auto simp: Alt_eq_map_rexp_iff)
+  then show ?case
+    by (intro exI[of _ "Alt s' r'"]) auto
+next
+  case (i r)
+  then show ?case
+    by (intro exI[of _ "Alt r r"]) auto
+next
+  case (R r)
+  then show ?case by (auto intro: exI[of _ r])
+next
+  case (A r rr s ss)
+  then obtain r' s' where "x = Alt r' s'"
+    "map_rexp f r' = r" "map_rexp f s' = s"
+    by (auto simp: Alt_eq_map_rexp_iff)
+  moreover from A(2)[OF this(2)[symmetric]] A(4)[OF this(3)[symmetric]] obtain rr' ss' where
+    "r' ~~ rr'" "rr = map_rexp f rr'" "s' ~~ ss'" "ss = map_rexp f ss'"
+    "set_rexp rr' \<subseteq> set_rexp r'" "set_rexp ss' \<subseteq> set_rexp s'"
+    by blast
+  ultimately show ?case using A(1,3)
+    by (intro exI[of _ "Alt rr' ss'"]) (auto intro!: AA)
+next
+  case (C r rr s ss)
+  then obtain r' s' where "x = Conc r' s'"
+    "map_rexp f r' = r" "map_rexp f s' = s"
+    by (auto simp: Conc_eq_map_rexp_iff)
+  moreover from C(2)[OF this(2)[symmetric]] C(4)[OF this(3)[symmetric]] obtain rr' ss' where
+    "r' ~~ rr'" "rr = map_rexp f rr'" "s' ~~ ss'" "ss = map_rexp f ss'"
+    "set_rexp rr' \<subseteq> set_rexp r'" "set_rexp ss' \<subseteq> set_rexp s'"
+    by blast
+  ultimately show ?case using C(1,3)
+    by (intro exI[of _ "Conc rr' ss'"]) (auto intro!: CC)
+next
+  case (S r rr)
+  then obtain r' where "x = Star r'" "map_rexp f r' = r"
+    by (auto simp: Star_eq_map_rexp_iff)
+  moreover from S(2)[OF this(2)[symmetric]] obtain rr' where "r' ~~ rr'" "rr = map_rexp f rr'"
+    "set_rexp rr' \<subseteq> set_rexp r'"
+    by blast
+  ultimately show ?case
+    by (intro exI[of _ "Star rr'"]) (auto intro!: SS)
+qed
+
+lemma reflclp_ACI: "(~)\<^sup>=\<^sup>= = (~)"
+  unfolding fun_eq_iff
+  by auto
+
+lemma strong_confluentp_ACI: "strong_confluentp (~)"
+  apply (rule strong_confluentpI, unfold reflclp_ACI)
+  subgoal for x y z
+  proof (induct x y arbitrary: z rule: ACI.induct)
+    case (a1 r s t)
+    then show ?case
+      by (auto intro: AAA converse_rtranclp_into_rtranclp)
+  next
+    case (a2 r s t)
+    then show ?case
+      by (auto intro: AAA converse_rtranclp_into_rtranclp)
+  next
+    case (c r s)
+    then show ?case
+      by (cases rule: ACI.cases) (auto intro: AAA)
+  next
+    case (i r)
+    then show ?case
+      by (auto intro: AAA)
+  next
+    case (R r)
+    then show ?case
+      by auto
+  next
+    note A1 = ACI.A[OF _ R]
+    note A2 = ACI.A[OF R]
+    case (A r r' s s')
+    from A(5,1-4) show ?case
+    proof (cases rule: ACI.cases)
+      case inner: (a1 r'' s'')
+      from A(1,3) show ?thesis
+        unfolding inner
+      proof (elim ACI.cases[of _ r'], goal_cases Xa1 Xa2 XC XI XR XP XT XS)
+        case (Xa1 rr ss tt)
+        with A(3) show ?case
+          by (elim exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ A2[OF A2]], rotated])
+            (metis a1 a2 A1 r_into_rtranclp rtranclp.rtrancl_into_rtrancl)
+      next
+        case (Xa2 r s t)
+        then show ?case
+          by (elim exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ A2[OF A2]], rotated])
+            (metis a1 A1 r_into_rtranclp rtranclp.rtrancl_into_rtrancl)
+      next
+        case (XC r s)
+        then show ?case
+          by (elim exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ A2[OF A2]], rotated])
+            (metis a1 c A1 r_into_rtranclp rtranclp.rtrancl_into_rtrancl)
+      next
+        case (XI r)
+        then show ?case
+          apply (elim exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ ACI.A[OF i ACI.A[OF i]]], rotated])
+          apply hypsubst
+          apply (rule converse_rtranclp_into_rtranclp, rule a1)
+          apply (rule converse_rtranclp_into_rtranclp, rule a1)
+          apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a2)
+          apply (rule converse_rtranclp_into_rtranclp, rule A2, rule A1, rule c)
+          apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a1)
+          apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a1)
+          apply (rule converse_rtranclp_into_rtranclp, rule a2)
+          apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a2)
+          apply blast
+          done
+      qed auto
+    next
+      case inner: (a2 s'' t'')
+      with A(1,3) show ?thesis
+        unfolding inner
+      proof (elim ACI.cases[of _ s'], goal_cases Xa1 Xa2 XC XI XR XP XT XS)
+        case (Xa1 rr ss tt)
+        with A(3) show ?case
+          by (elim exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ A1[OF A1]], rotated])
+            (metis a2 A2 r_into_rtranclp rtranclp.rtrancl_into_rtrancl)
+      next
+        case (Xa2 r s t)
+        then show ?case
+          by (elim exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ A1[OF A1]], rotated])
+            (metis a1 a2 A2 r_into_rtranclp rtranclp.rtrancl_into_rtrancl)
+      next
+        case (XC r s)
+        then show ?case
+          by (elim exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ A1[OF A1]], rotated])
+            (metis a2 c A2 r_into_rtranclp rtranclp.rtrancl_into_rtrancl)
+      next
+        case (XI r)
+        then show ?case
+          apply (elim exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ ACI.A[OF ACI.A[OF _ i] i]], rotated])
+          apply hypsubst
+          apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a2)
+          apply (rule converse_rtranclp_into_rtranclp, rule A2, rule A1, rule c)
+          apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a1)
+          apply (rule converse_rtranclp_into_rtranclp, rule A2, rule A2, rule a1)
+          apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a2)
+          apply (rule converse_rtranclp_into_rtranclp, rule a2)
+          apply blast
+          done
+      qed auto
+    qed (auto 5 0 intro: AAA)
+  next
+    case (C r r' s s')
+    from C(5,1-4) show ?case
+      by (cases rule: ACI.cases) (auto 5 0 intro: CCC)
+  next
+    case (S r r')
+    from S(3,1,2) show ?case
+      by (cases rule: ACI.cases) (auto intro: SSS)
+  qed
+  done
+
+lemma confluent_quotient_ACI:
+  "confluent_quotient (~) (~~) (~~) (~~) (~~) (~~)
+     (map_rexp fst) (map_rexp snd) (map_rexp fst) (map_rexp snd)
+     rel_rexp rel_rexp rel_rexp set_rexp set_rexp"
+  by unfold_locales (auto dest: ACIcl_set_eq ACIcl_map_respects simp: rexp.in_rel rexp.rel_compp map_rexp_ACI_inv
+      intro: equivpI reflpI sympI transpI
+      strong_confluentp_imp_confluentp[OF strong_confluentp_ACI])
+
+inductive ACIEQ (infix "\<approx>" 64) where
+  a: "Alt (Alt r s) t \<approx> Alt r (Alt s t)"
+| c: "Alt r s \<approx> Alt s r"
+| i: "Alt r r \<approx> r"
+| A: "r \<approx> r' \<Longrightarrow> s \<approx> s' \<Longrightarrow> Alt r s \<approx> Alt r' s'"
+| C: "r \<approx> r' \<Longrightarrow> s \<approx> s' \<Longrightarrow> Conc r s \<approx> Conc r' s'"
+| S: "r \<approx> r' \<Longrightarrow> Star r \<approx> Star r'"
+| r: "r \<approx> r"
+| s: "r \<approx> s \<Longrightarrow> s \<approx> r"
+| t: "r \<approx> s \<Longrightarrow> s \<approx> t \<Longrightarrow> r \<approx> t"
+
+lemma ACIEQ_le_ACIcl: "r \<approx> s \<Longrightarrow> r ~~ s"
+  by (induct r s rule: ACIEQ.induct) (auto intro: AA CC SS equivclp_sym equivclp_trans)
+
+lemma ACI_le_ACIEQ: "r ~ s \<Longrightarrow> r \<approx> s"
+  by (induct r s rule: ACI.induct) (auto intro: ACIEQ.intros)
+
+lemma ACIcl_le_ACIEQ: "r ~~ s \<Longrightarrow> r \<approx> s"
+  by (induct rule: equivclp_induct) (auto 0 3 intro: ACIEQ.intros ACI_le_ACIEQ)
+
+lemma ACIEQ_alt: "(\<approx>) = (~~)"
+  by (simp add: ACIEQ_le_ACIcl ACIcl_le_ACIEQ antisym predicate2I)
+
+quotient_type 'a ACI_rexp = "'a rexp" / "(\<approx>)"
+  unfolding ACIEQ_alt by (auto intro!: equivpI reflpI sympI transpI)
+
+lift_bnf 'a ACI_rexp
+  unfolding ACIEQ_alt
+  subgoal for A Q by (rule confluent_quotient.subdistributivity[OF confluent_quotient_ACI])
+  subgoal for Ss by (intro eq_set_preserves_inter[rotated] ACIcl_set_eq; auto)
+  done
+
+datatype ldl = Prop string | And ldl ldl | Not ldl | Match "ldl ACI_rexp"
+
+end
\ No newline at end of file
diff -r d47c8a89c6a5 -r 180981b87929 src/HOL/Datatype_Examples/Regex_ACIDZ.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Datatype_Examples/Regex_ACIDZ.thy	Tue Mar 09 14:20:27 2021 +0100
@@ -0,0 +1,481 @@
+theory Regex_ACIDZ
+  imports "HOL-Library.Confluent_Quotient"
+begin
+
+datatype (discs_sels) 'a rexp = Zero | Eps | Atom 'a
+  | Alt "'a rexp" "'a rexp" | Conc "'a rexp" "'a rexp" | Star "'a rexp"
+
+fun elim_zeros where
+  "elim_zeros (Alt r s) =
+    (let r' = elim_zeros r; s' = elim_zeros s in
+     if r' = Zero then s' else if s' = Zero then r' else Alt r' s')"
+| "elim_zeros (Conc r s) = (let r' = elim_zeros r in if r' = Zero then Zero else Conc r' s)"
+| "elim_zeros r = r"
+
+fun distribute where
+  "distribute t (Alt r s) = Alt (distribute t r) (distribute t s)"
+| "distribute t (Conc r s) = Conc (distribute s r) t"
+| "distribute t r = Conc r t"
+
+inductive ACIDZ (infix "~" 64) where
+  a1: "Alt (Alt r s) t ~ Alt r (Alt s t)"
+| a2: "Alt r (Alt s t) ~ Alt (Alt r s) t"
+| c: "Alt r s ~ Alt s r"
+| i: "r ~ Alt r r"
+| z: "r ~ s \<Longrightarrow> r ~ elim_zeros s"
+| d: "Conc r t ~ distribute t r"
+| R: "r ~ r"
+| A: "r ~ r' \<Longrightarrow> s ~ s' \<Longrightarrow> Alt r s ~ Alt r' s'"
+| C: "r ~ r' \<Longrightarrow> Conc r s ~ Conc r' s"
+
+inductive_cases ACIDZ_AltE[elim]: "Alt r s ~ t"
+inductive_cases ACIDZ_ConcE[elim]: "Conc r s ~ t"
+inductive_cases ACIDZ_StarE[elim]: "Star r ~ t"
+
+declare ACIDZ.intros[intro]
+
+abbreviation ACIDZcl (infix "~~" 64) where "(~~) \<equiv> equivclp (~)"
+
+lemma map_rexp_distribute[simp]: "map_rexp f (distribute t r) = distribute (map_rexp f t) (map_rexp f r)"
+  by (induct r arbitrary: t) auto
+
+lemma set_rexp_distribute[simp]: "set_rexp (distribute t r) = set_rexp r \<union> set_rexp t"
+  by (induct r arbitrary: t) auto
+
+lemma Zero_eq_map_rexp_iff[simp]:
+  "Zero = map_rexp f x \<longleftrightarrow> x = Zero"
+  "map_rexp f x = Zero \<longleftrightarrow> x = Zero"
+  by (cases x; auto)+
+
+lemma Alt_eq_map_rexp_iff:
+  "Alt r s = map_rexp f x \<longleftrightarrow> (\<exists>r' s'. x = Alt r' s' \<and> map_rexp f r' = r \<and> map_rexp f s' = s)"
+  "map_rexp f x = Alt r s \<longleftrightarrow> (\<exists>r' s'. x = Alt r' s' \<and> map_rexp f r' = r \<and> map_rexp f s' = s)"
+  by (cases x; auto)+
+
+lemma map_rexp_elim_zeros[simp]: "map_rexp f (elim_zeros r) = elim_zeros (map_rexp f r)"
+  by (induct r rule: elim_zeros.induct) (auto simp: Let_def)
+
+lemma set_rexp_elim_zeros: "set_rexp (elim_zeros r) \<subseteq> set_rexp r"
+  by (induct r rule: elim_zeros.induct) (auto simp: Let_def)
+
+lemma ACIDZ_map_respects:
+  fixes f :: "'a \<Rightarrow> 'b" and r s :: "'a rexp"
+  assumes "r ~ s"
+  shows "map_rexp f r ~ map_rexp f s"
+  using assms by (induct r s rule: ACIDZ.induct) (auto simp: Let_def)
+
+lemma ACIDZcl_map_respects:
+  fixes f :: "'a \<Rightarrow> 'b" and r s :: "'a rexp"
+  assumes "r ~~ s"
+  shows "map_rexp f r ~~ map_rexp f s"
+  using assms by (induct rule: equivclp_induct) (auto intro: ACIDZ_map_respects equivclp_trans)
+
+lemma finite_set_rexp: "finite (set_rexp r)"
+  by (induct r) auto
+
+lemma ACIDZ_set_rexp: "r ~ s \<Longrightarrow> set_rexp s \<subseteq> set_rexp r"
+  by (induct r s rule: ACIDZ.induct) (auto dest: set_mp[OF set_rexp_elim_zeros] simp: Let_def)
+
+lemma ACIDZ_set_rexp': "(~)\<^sup>*\<^sup>* r s \<Longrightarrow> set_rexp s \<subseteq> set_rexp r"
+  by (induct rule: rtranclp.induct) (auto dest: ACIDZ_set_rexp)
+
+
+lemma Conc_eq_map_rexp_iff:
+  "Conc r s = map_rexp f x \<longleftrightarrow> (\<exists>r' s'. x = Conc r' s' \<and> map_rexp f r' = r \<and> map_rexp f s' = s)"
+  "map_rexp f x = Conc r s \<longleftrightarrow> (\<exists>r' s'. x = Conc r' s' \<and> map_rexp f r' = r \<and> map_rexp f s' = s)"
+  by (cases x; auto)+
+
+lemma Star_eq_map_rexp_iff:
+  "Star r = map_rexp f x \<longleftrightarrow> (\<exists>r'. x = Star r' \<and> map_rexp f r' = r)"
+  "map_rexp f x = Star r \<longleftrightarrow> (\<exists>r'. x = Star r' \<and> map_rexp f r' = r)"
+  by (cases x; auto)+
+
+lemma AAA: "(~)\<^sup>*\<^sup>* r  r' \<Longrightarrow> (~)\<^sup>*\<^sup>* s s' \<Longrightarrow> (~)\<^sup>*\<^sup>* (Alt r s) (Alt r' s')"
+proof (induct r r' rule: rtranclp.induct)
+  case (rtrancl_refl r)
+  then show ?case
+    by (induct s s' rule: rtranclp.induct)
+      (auto elim!: rtranclp.rtrancl_into_rtrancl)
+next
+  case (rtrancl_into_rtrancl a b c)
+  then show ?case
+    by (auto elim!: rtranclp.rtrancl_into_rtrancl)
+qed
+
+lemma CCC: "(~)\<^sup>*\<^sup>* r r' \<Longrightarrow> (~)\<^sup>*\<^sup>* (Conc r s) (Conc r' s)"
+proof (induct r r' rule: rtranclp.induct)
+  case (rtrancl_refl r)
+  then show ?case
+    by simp
+next
+  case (rtrancl_into_rtrancl a b c)
+  then show ?case
+    by (auto elim!: rtranclp.rtrancl_into_rtrancl)
+qed
+
+lemma map_rexp_ACIDZ_inv: "map_rexp f x ~ y \<Longrightarrow> \<exists>z. (~)\<^sup>*\<^sup>* x z \<and> y = map_rexp f z"
+proof (induct "map_rexp f x" y arbitrary: x rule: ACIDZ.induct)
+  case (a1 r s t)
+  then obtain r' s' t' where "x = Alt (Alt r' s') t'"
+    "map_rexp f r' = r" "map_rexp f s' = s" "map_rexp f t' = t"
+    by (auto simp: Alt_eq_map_rexp_iff)
+  then show ?case
+    by (intro exI[of _ "Alt r' (Alt s' t')"]) auto
+next
+  case (a2 r s t)
+  then obtain r' s' t' where "x = Alt r' (Alt s' t')"
+    "map_rexp f r' = r" "map_rexp f s' = s" "map_rexp f t' = t"
+    by (auto simp: Alt_eq_map_rexp_iff)
+  then show ?case
+    by (intro exI[of _ "Alt (Alt r' s') t'"]) auto
+next
+  case (c r s)
+  then obtain r' s' where "x = Alt r' s'"
+    "map_rexp f r' = r" "map_rexp f s' = s"
+    by (auto simp: Alt_eq_map_rexp_iff)
+  then show ?case
+    by (intro exI[of _ "Alt s' r'"]) auto
+next
+  case (i r)
+  then show ?case
+    by (intro exI[of _ "Alt r r"]) auto
+next
+  case (z r)
+  then show ?case
+    by (metis ACIDZ.z R map_rexp_elim_zeros rtranclp.simps)
+next
+  case (d r s)
+  then obtain r' s' where "x = Conc r' s'"
+    "map_rexp f r' = r" "map_rexp f s' = s"
+    by (auto simp: Conc_eq_map_rexp_iff)
+  then show ?case
+    by (intro exI[of _ "distribute s' r'"]) auto
+next
+  case (R r)
+  then show ?case by (auto intro: exI[of _ r])
+next
+  case (A r rr s ss)
+  then obtain r' s' where "x = Alt r' s'"
+    "map_rexp f r' = r" "map_rexp f s' = s"
+    by (auto simp: Alt_eq_map_rexp_iff)
+  moreover from A(2)[OF this(2)[symmetric]] A(4)[OF this(3)[symmetric]] obtain rr' ss' where
+    "(~)\<^sup>*\<^sup>* r' rr'" "rr = map_rexp f rr'" "(~)\<^sup>*\<^sup>* s' ss'" "ss = map_rexp f ss'"
+    by blast
+  ultimately show ?case using A(1,3)
+    by (intro exI[of _ "Alt rr' ss'"]) (auto intro!: AAA)
+next
+  case (C r rr s)
+  then obtain r' s' where "x = Conc r' s'"
+    "map_rexp f r' = r" "map_rexp f s' = s"
+    by (auto simp: Conc_eq_map_rexp_iff)
+  moreover from C(2)[OF this(2)[symmetric]] obtain rr' where
+    "(~)\<^sup>*\<^sup>* r' rr'" "rr = map_rexp f rr'"
+    by blast
+  ultimately show ?case using C(1,3)
+    by (intro exI[of _ "Conc rr' s'"]) (auto intro!: CCC)
+qed
+
+lemma reflclp_ACIDZ: "(~)\<^sup>=\<^sup>= = (~)"
+  unfolding fun_eq_iff
+  by auto
+
+lemma elim_zeros_distribute_Zero: "elim_zeros r = Zero \<Longrightarrow> elim_zeros (distribute t r) = Zero"
+  by (induct r arbitrary: t) (auto simp: Let_def split: if_splits)
+
+lemma elim_zeros_ACIDZ_Zero: "r ~ s \<Longrightarrow> elim_zeros r = Zero \<Longrightarrow> elim_zeros s = Zero"
+  by (induct r s rule: ACIDZ.induct) (auto simp: Let_def elim_zeros_distribute_Zero split: if_splits)
+
+lemma AZZ[simp]: "Alt Zero Zero ~ Zero"
+  by (metis elim_zeros.simps(3) elim_zeros_ACIDZ_Zero i z)
+
+lemma elim_zeros_idem[simp]: "elim_zeros (elim_zeros r) = elim_zeros r"
+  by (induct r rule: elim_zeros.induct) (auto simp: Let_def)
+
+lemma elim_zeros_distribute_idem: "elim_zeros (distribute s (elim_zeros r)) = elim_zeros (distribute s r)"
+  by (induct r arbitrary: s rule: elim_zeros.induct) (auto simp: Let_def)
+
+lemma zz: "r ~ s \<Longrightarrow> t = elim_zeros s \<Longrightarrow> r ~ t"
+  by (metis z)
+
+lemma elim_zeros_ACIDZ1: "r ~ s \<Longrightarrow> elim_zeros r ~ elim_zeros s"
+proof (induct r s rule: ACIDZ.induct)
+  case (c r s)
+  then show ?case by (auto simp: Let_def)
+next
+  case (d r t)
+  then show ?case
+    by (smt (z3) ACIDZ.d R distribute.simps(3) elim_zeros.simps(2) elim_zeros.simps(3) elim_zeros_distribute_idem z)
+next
+  case (A r r' s s')
+  then show ?case
+    by (auto 0 2 simp: Let_def dest: elim_zeros_ACIDZ_Zero elim: zz[OF ACIDZ.A])
+next
+  case (C r r' s)
+  then show ?case
+    by (smt (z3) ACIDZ.C elim_zeros.simps(2,3) z elim_zeros_ACIDZ_Zero)
+qed (auto simp: Let_def)
+
+lemma AA': "r ~ r' \<Longrightarrow> s ~ s' \<Longrightarrow> t = elim_zeros (Alt r' s') \<Longrightarrow> Alt r s ~ t"
+  by (auto simp del: elim_zeros.simps)
+
+lemma distribute_ACIDZ1: "r ~ r' \<Longrightarrow> distribute s r ~ elim_zeros (distribute s r')"
+proof (induct r r' arbitrary: s rule: ACIDZ.induct)
+  case (A r r' s s' u)
+  from A(2,4)[of u] show ?case
+    by (auto simp: Let_def elim: zz[OF ACIDZ.A])
+next
+  case (C r r' s)
+  then show ?case
+    by (smt (verit, best) ACIDZ.C distribute.simps(2,3) elim_zeros.simps(2,3) z)
+qed (auto simp del: elim_zeros.simps simp: elim_zeros_distribute_idem)
+
+lemma elim_zeros_ACIDZ: "r ~ s \<Longrightarrow> (~)\<^sup>*\<^sup>* (elim_zeros r) (elim_zeros s)"
+  using elim_zeros_ACIDZ1 by blast
+
+lemma elim_zeros_ACIDZ_rtranclp: "(~)\<^sup>*\<^sup>* r s \<Longrightarrow> (~)\<^sup>*\<^sup>* (elim_zeros r) (elim_zeros s)"
+  by (induct rule: rtranclp_induct) (auto elim!: rtranclp_trans elim_zeros_ACIDZ)
+
+lemma distribute_ACIDZ: "(~) r r' \<Longrightarrow> (~)\<^sup>*\<^sup>* (distribute s r) (elim_zeros (distribute s r'))"
+  by (metis distribute_ACIDZ1 rtranclp.simps)
+
+lemma ACIDZ_elim_zeros: "(~) r s \<Longrightarrow> elim_zeros r = Zero \<Longrightarrow> elim_zeros s = Zero"
+  by (meson elim_zeros_ACIDZ1 elim_zeros_ACIDZ_Zero)
+
+lemma ACIDZ_elim_zeros_rtranclp:
+  "(~)\<^sup>*\<^sup>* r s \<Longrightarrow> elim_zeros r = Zero \<Longrightarrow> elim_zeros s = Zero"
+  by (induct rule: rtranclp_induct) (auto elim: ACIDZ_elim_zeros)
+
+lemma Alt_elim_zeros[simp]:
+  "Alt (elim_zeros r) s ~ elim_zeros (Alt r s)"
+  "Alt r (elim_zeros s) ~ elim_zeros (Alt r s)"
+  by (smt (verit, ccfv_threshold) ACIDZ.simps elim_zeros.simps(1) elim_zeros_idem)+
+
+lemma strong_confluentp_ACIDZ: "strong_confluentp (~)"
+proof (rule strong_confluentpI, unfold reflclp_ACIDZ)
+  fix x y z :: "'a rexp"
+  assume "x ~ y" "x ~ z"
+  then show "\<exists>u. (~)\<^sup>*\<^sup>* y u \<and> z ~ u"
+  proof (induct x y arbitrary: z rule: ACIDZ.induct)
+    case (a1 r s t)
+    then show ?case
+      by (auto intro: AAA converse_rtranclp_into_rtranclp)
+  next
+    case (a2 r s t)
+    then show ?case
+      by (auto intro: AAA converse_rtranclp_into_rtranclp)
+  next
+    case (c r s)
+    then show ?case
+      by (cases rule: ACIDZ.cases)
+        (auto 0 4 intro: exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ R], rotated]
+          converse_rtranclp_into_rtranclp[where r="(~)", OF ACIDZ.c])
+  next
+    case (i r)
+    then show ?case
+      by (auto intro: AAA)
+  next
+    case (z r s)
+    then show ?case
+      by (meson ACIDZ.z elim_zeros_ACIDZ_rtranclp)
+  next
+    case (d r s t)
+    then show ?case
+      by (induct "Conc r s" t rule: ACIDZ.induct)
+        (force intro: exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ z], rotated]
+          exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ z[OF elim_zeros_ACIDZ1]], rotated]
+          distribute_ACIDZ1 elim!: rtranclp_trans)+
+  next
+    case (R r)
+    then show ?case
+      by auto
+  next
+    note A1 = ACIDZ.A[OF _ R]
+    note A2 = ACIDZ.A[OF R]
+    case (A r r' s s')
+    from A(5,1-4) show ?case
+    proof (induct "Alt r s" z rule: ACIDZ.induct)
+      case inner: (a1 r'' s'')
+      from A(1,3) show ?case
+        unfolding inner.hyps[symmetric]
+      proof (induct "Alt r'' s''" r' rule: ACIDZ.induct[consumes 1, case_names Xa1 Xa2 Xc Xi Xz Xd XR XA XC])
+        case Xa1
+        with A(3) show ?case
+          by (elim exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ A2[OF A2]], rotated])
+           (metis A1 a1 a2 r_into_rtranclp rtranclp.rtrancl_into_rtrancl)
+      next
+        case Xa2
+        then show ?case
+          by (elim exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ A2[OF A2]], rotated])
+            (metis a1 A1 r_into_rtranclp rtranclp.rtrancl_into_rtrancl)
+      next
+        case Xc
+        then show ?case
+          by (elim exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ A2[OF A2]], rotated])
+            (metis a1 c A1 r_into_rtranclp rtranclp.rtrancl_into_rtrancl)
+      next
+        case Xi
+        then show ?case
+          apply (elim exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ ACIDZ.A[OF i ACIDZ.A[OF i]]], rotated])
+          apply (rule converse_rtranclp_into_rtranclp, rule a1)
+          apply (rule converse_rtranclp_into_rtranclp, rule a1)
+          apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a2)
+          apply (rule converse_rtranclp_into_rtranclp, rule A2, rule A1, rule c)
+          apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a1)
+          apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a1)
+          apply (rule converse_rtranclp_into_rtranclp, rule a2)
+          apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a2)
+          apply blast
+          done
+      next
+        case Xz
+        with A show ?case
+          by (auto elim!: exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ z], rotated]
+            converse_rtranclp_into_rtranclp[rotated, OF elim_zeros_ACIDZ_rtranclp]
+            simp del: elim_zeros.simps)
+      qed auto
+    next
+      case inner: (a2 s'' t'')
+      from A(3,1) show ?case
+        unfolding inner.hyps[symmetric]
+      proof (induct "Alt s'' t''" s' rule: ACIDZ.induct[consumes 1, case_names Xa1 Xa2 Xc Xi Xz Xd XR XA XC])
+        case Xa1
+        with A(3) show ?case
+          by (elim exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ A1[OF A1]], rotated])
+            (metis a2 A2 r_into_rtranclp rtranclp.rtrancl_into_rtrancl)
+      next
+        case Xa2
+        then show ?case
+          by (elim exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ A1[OF A1]], rotated])
+            (metis a1 a2 A2 r_into_rtranclp rtranclp.rtrancl_into_rtrancl)
+      next
+        case Xc
+        then show ?case
+          by (elim exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ A1[OF A1]], rotated])
+            (metis a2 c A2 r_into_rtranclp rtranclp.rtrancl_into_rtrancl)
+      next
+        case Xi
+        then show ?case
+          apply (elim exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ ACIDZ.A[OF ACIDZ.A[OF _ i] i]], rotated])
+          apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a2)
+          apply (rule converse_rtranclp_into_rtranclp, rule A2, rule A1, rule c)
+          apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a1)
+          apply (rule converse_rtranclp_into_rtranclp, rule A2, rule A2, rule a1)
+          apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a2)
+          apply (rule converse_rtranclp_into_rtranclp, rule a2)
+          apply blast
+          done
+      next
+        case Xz
+        then show ?case
+          by (auto elim!: exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ z], rotated]
+            converse_rtranclp_into_rtranclp[rotated, OF elim_zeros_ACIDZ_rtranclp]
+            simp del: elim_zeros.simps)
+      qed auto
+    next
+      case (z rs) with A show ?case
+        by (auto elim!: rtranclp_trans
+          intro!: exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ elim_zeros_ACIDZ1], rotated])
+    qed (auto 5 0 intro: AAA)
+  next
+    case (C r r' s s')
+    from C(3,1-2) show ?case
+      by (induct "Conc r s" s' rule: ACIDZ.induct)
+        (auto intro: CCC elim!: rtranclp_trans
+          exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ elim_zeros_ACIDZ1], rotated]
+          exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ distribute_ACIDZ1], rotated])
+  qed
+qed
+
+lemma confluent_quotient_ACIDZ:
+  "confluent_quotient (~) (~~) (~~) (~~) (~~) (~~)
+     (map_rexp fst) (map_rexp snd) (map_rexp fst) (map_rexp snd)
+     rel_rexp rel_rexp rel_rexp set_rexp set_rexp"
+  by unfold_locales
+    (auto 4 4 dest: ACIDZ_set_rexp' simp: rexp.in_rel rexp.rel_compp dest: map_rexp_ACIDZ_inv intro: rtranclp_into_equivclp
+      intro: equivpI reflpI sympI transpI ACIDZcl_map_respects
+      strong_confluentp_imp_confluentp[OF strong_confluentp_ACIDZ])
+
+lemma wide_intersection_finite_ACIDZ: "wide_intersection_finite (~~) map_rexp set_rexp"
+  by unfold_locales
+    (auto intro: ACIDZcl_map_respects rexp.map_cong simp: rexp.map_id rexp.set_map finite_set_rexp)
+
+inductive ACIDZEQ (infix "\<approx>" 64) where
+  a: "Alt (Alt r s) t \<approx> Alt r (Alt s t)"
+| c: "Alt r s \<approx> Alt s r"
+| i: "Alt r r \<approx> r"
+| cz: "Conc Zero r \<approx> Zero"
+| az: "Alt Zero r \<approx> r"
+| d: "Conc (Alt r s) t \<approx> Alt (Conc r t) (Conc s t)"
+| A: "r \<approx> r' \<Longrightarrow> s \<approx> s' \<Longrightarrow> Alt r s \<approx> Alt r' s'"
+| C: "r \<approx> r' \<Longrightarrow> Conc r s \<approx> Conc r' s"
+| r: "r \<approx> r"
+| s: "r \<approx> s \<Longrightarrow> s \<approx> r"
+| t: "r \<approx> s \<Longrightarrow> s \<approx> t \<Longrightarrow> r \<approx> t"
+
+context begin
+
+private lemma AA: "r ~~ r' \<Longrightarrow> s ~~ s' \<Longrightarrow> Alt r s ~~ Alt r' s'"
+proof (induct rule: equivclp_induct)
+  case base
+  then show ?case
+    by (induct rule: equivclp_induct) (auto elim!: equivclp_trans)
+next
+  case (step s t)
+  then show ?case
+    by (auto elim!: equivclp_trans)
+qed
+
+private lemma CC: "r ~~ r' \<Longrightarrow> Conc r s ~~ Conc r' s"
+proof (induct rule: equivclp_induct)
+  case base
+  then show ?case
+    by simp
+next
+  case (step s t)
+  then show ?case
+    by (auto elim!: equivclp_trans)
+qed
+
+private lemma CZ: "Conc Zero r ~~ Zero"
+  by (smt (z3) R elim_zeros.simps(2) elim_zeros.simps(3) r_into_equivclp z)
+
+private lemma AZ: "Alt Zero r ~~ r"
+  by (smt (verit, ccfv_threshold) converse_r_into_equivclp converse_rtranclp_into_rtranclp
+    elim_zeros.simps(1) elim_zeros.simps(3) equivclp_def symclpI1 z R)
+
+private lemma D: "Conc (Alt r s) t ~~ Alt (Conc r t) (Conc s t)"
+  by (smt (verit, ccfv_threshold) AA ACIDZ.d converse_r_into_equivclp distribute.simps(1)
+    equivclp_sym rtranclp.simps rtranclp_equivclp)
+
+lemma ACIDZEQ_le_ACIDZcl: "r \<approx> s \<Longrightarrow> r ~~ s"
+  by (induct r s rule: ACIDZEQ.induct) (auto intro: AA CC AZ CZ D equivclp_sym equivclp_trans)
+
+end
+
+lemma ACIDZEQ_z[simp]: "r \<approx> elim_zeros r"
+  by (induct r rule: elim_zeros.induct) (auto 0 3 intro: ACIDZEQ.intros simp: Let_def)
+
+lemma ACIDZEQ_d[simp]: "Conc r s \<approx> distribute s r"
+  by (induct s r rule: distribute.induct) (auto 0 3 intro: ACIDZEQ.intros)
+
+lemma ACIDZ_le_ACIDZEQ: "r ~ s \<Longrightarrow> r \<approx> s"
+  by (induct r s rule: ACIDZ.induct) (auto 0 2 intro: ACIDZEQ.intros simp: Let_def)
+
+lemma ACIDZcl_le_ACIDZEQ: "r ~~ s \<Longrightarrow> r \<approx> s"
+  by (induct rule: equivclp_induct) (auto 0 3 intro: ACIDZEQ.intros ACIDZ_le_ACIDZEQ)
+
+lemma ACIDZEQ_alt: "(\<approx>) = (~~)"
+  by (simp add: ACIDZEQ_le_ACIDZcl ACIDZcl_le_ACIDZEQ antisym predicate2I)
+
+quotient_type 'a rexp_ACIDZ = "'a rexp" / "(\<approx>)"
+  unfolding ACIDZEQ_alt by (auto intro!: equivpI reflpI sympI transpI)
+
+lift_bnf 'a rexp_ACIDZ
+  unfolding ACIDZEQ_alt
+  subgoal for A Q by (rule confluent_quotient.subdistributivity[OF confluent_quotient_ACIDZ])
+  subgoal for Ss by (elim wide_intersection_finite.wide_intersection[OF wide_intersection_finite_ACIDZ])
+  done
+
+datatype ldl = Prop string | And ldl ldl | Not ldl | Match "ldl rexp_ACIDZ"
+
+end
diff -r d47c8a89c6a5 -r 180981b87929 src/HOL/Library/Confluent_Quotient.thy
--- a/src/HOL/Library/Confluent_Quotient.thy	Tue Mar 09 11:50:21 2021 +0100
+++ b/src/HOL/Library/Confluent_Quotient.thy	Tue Mar 09 14:20:27 2021 +0100
@@ -1,11 +1,116 @@
-theory Confluent_Quotient imports 
+theory Confluent_Quotient imports
   Confluence
 begin
 
-section \<open>Subdistributivity for quotients via confluence\<close>
+text \<open>Functors with finite setters preserve wide intersection for any equivalence relation that respects the mapper.\<close>
+
+lemma Inter_finite_subset:
+  assumes "\<forall>A \<in> \<A>. finite A"
+  shows "\<exists>\<B>\<subseteq>\<A>. finite \<B> \<and> (\<Inter>\<B>) = (\<Inter>\<A>)"
+proof(cases "\<A> = {}")
+  case False
+  then obtain A where A: "A \<in> \<A>" by auto
+  then have finA: "finite A" using assms by auto
+  hence fin: "finite (A - \<Inter>\<A>)" by(rule finite_subset[rotated]) auto
+  let ?P = "\<lambda>x A. A \<in> \<A> \<and> x \<notin> A"
+  define f where "f x = Eps (?P x)" for x
+  let ?\<B> = "insert A (f ` (A - \<Inter>\<A>))"
+  have "?P x (f x)" if "x \<in> A - \<Inter>\<A>" for x unfolding f_def by(rule someI_ex)(use that A in auto)
+  hence "(\<Inter>?\<B>) = (\<Inter>\<A>)" "?\<B> \<subseteq> \<A>" using A by auto
+  moreover have "finite ?\<B>" using fin by simp
+  ultimately show ?thesis by blast
+qed simp
+
+locale wide_intersection_finite =
+  fixes E :: "'Fa \<Rightarrow> 'Fa \<Rightarrow> bool"
+    and mapFa :: "('a \<Rightarrow> 'a) \<Rightarrow> 'Fa \<Rightarrow> 'Fa"
+    and setFa :: "'Fa \<Rightarrow> 'a set"
+  assumes equiv: "equivp E"
+    and map_E: "E x y \<Longrightarrow> E (mapFa f x) (mapFa f y)"
+    and map_id: "mapFa id x = x"
+    and map_cong: "\<forall>a\<in>setFa x. f a = g a \<Longrightarrow> mapFa f x = mapFa g x"
+    and set_map: "setFa (mapFa f x) = f ` setFa x"
+    and finite: "finite (setFa x)"
+begin
+
+lemma binary_intersection:
+  assumes "E y z" and y: "setFa y \<subseteq> Y" and z: "setFa z \<subseteq> Z" and a: "a \<in> Y" "a \<in> Z"
+  shows "\<exists>x. E x y \<and> setFa x \<subseteq> Y \<and> setFa x \<subseteq> Z"
+proof -
+  let ?f = "\<lambda>b. if b \<in> Z then b else a"
+  let ?u = "mapFa ?f y"
+  from \<open>E y z\<close> have "E ?u (mapFa ?f z)" by(rule map_E)
+  also have "mapFa ?f z = mapFa id z" by(rule map_cong)(use z in auto)
+  also have "\<dots> = z" by(rule map_id)
+  finally have "E ?u y" using \<open>E y z\<close> equivp_symp[OF equiv] equivp_transp[OF equiv] by blast
+  moreover have "setFa ?u \<subseteq> Y" using a y by(subst set_map) auto
+  moreover have "setFa ?u \<subseteq> Z" using a by(subst set_map) auto
+  ultimately show ?thesis by blast
+qed
+
+lemma finite_intersection:
+  assumes E: "\<forall>y\<in>A. E y z"
+    and fin: "finite A"
+    and sub: "\<forall>y\<in>A. setFa y \<subseteq> Y y \<and> a \<in> Y y"
+  shows "\<exists>x. E x z \<and> (\<forall>y\<in>A. setFa x \<subseteq> Y y)"
+  using fin E sub
+proof(induction)
+  case empty
+  then show ?case using equivp_reflp[OF equiv, of z] by(auto)
+next
+  case (insert y A)
+  then obtain x where x: "E x z" "\<forall>y\<in>A. setFa x \<subseteq> Y y \<and> a \<in> Y y" by auto
+  hence set_x: "setFa x \<subseteq> (\<Inter>y\<in>A. Y y)" "a \<in> (\<Inter>y\<in>A. Y y)" by auto
+  from insert.prems have "E y z" and set_y: "setFa y \<subseteq> Y y" "a \<in> Y y" by auto
+  from \<open>E y z\<close> \<open>E x z\<close> have "E x y" using equivp_symp[OF equiv] equivp_transp[OF equiv] by blast
+  from binary_intersection[OF this set_x(1) set_y(1) set_x(2) set_y(2)]
+  obtain x' where "E x' x" "setFa x' \<subseteq> \<Inter> (Y ` A)" "setFa x' \<subseteq> Y y" by blast
+  then show ?case using \<open>E x z\<close> equivp_transp[OF equiv] by blast
+qed
+
+lemma wide_intersection:
+  assumes inter_nonempty: "\<Inter> Ss \<noteq> {}"
+  shows "(\<Inter>As \<in> Ss. {(x, x'). E x x'} `` {x. setFa x \<subseteq> As}) \<subseteq> {(x, x'). E x x'} `` {x. setFa x \<subseteq> \<Inter> Ss}" (is "?lhs \<subseteq> ?rhs")
+proof
+  fix x
+  assume lhs: "x \<in> ?lhs"
+  from inter_nonempty obtain a where a: "\<forall>As \<in> Ss. a \<in> As" by auto
+  from lhs obtain y where y: "\<And>As. As \<in> Ss \<Longrightarrow> E (y As) x \<and> setFa (y As) \<subseteq> As"
+    by atomize_elim(rule choice, auto)
+  define Ts where "Ts = (\<lambda>As. insert a (setFa (y As))) ` Ss"
+  have Ts_subset: "(\<Inter>Ts) \<subseteq> (\<Inter>Ss)" using a unfolding Ts_def by(auto dest: y)
+  have Ts_finite: "\<forall>Bs \<in> Ts. finite Bs" unfolding Ts_def by(auto dest: y intro: finite)
+  from Inter_finite_subset[OF this] obtain Us
+    where Us: "Us \<subseteq> Ts" and finite_Us: "finite Us" and Int_Us: "(\<Inter>Us) \<subseteq> (\<Inter>Ts)" by force
+  let ?P = "\<lambda>U As. As \<in> Ss \<and> U = insert a (setFa (y As))"
+  define Y where "Y U = Eps (?P U)" for U
+  have Y: "?P U (Y U)" if "U \<in> Us" for U unfolding Y_def
+    by(rule someI_ex)(use that Us in \<open>auto simp add: Ts_def\<close>)
+  let ?f = "\<lambda>U. y (Y U)"
+  have *: "\<forall>z\<in>(?f ` Us). E z x" by(auto dest!: Y y)
+  have **: "\<forall>z\<in>(?f ` Us). setFa z \<subseteq> insert a (setFa z) \<and> a \<in> insert a (setFa z)" by auto
+  from finite_intersection[OF * _ **] finite_Us obtain u
+    where u: "E u x" and set_u: "\<forall>z\<in>(?f ` Us). setFa u \<subseteq> insert a (setFa z)" by auto
+  from set_u have "setFa u \<subseteq> (\<Inter> Us)" by(auto dest: Y)
+  with Int_Us Ts_subset have "setFa u \<subseteq> (\<Inter> Ss)" by auto
+  with u show "x \<in> ?rhs" by auto
+qed
+
+end
+
+text \<open>Subdistributivity for quotients via confluence\<close>
+
+lemma rtranclp_transp_reflp: "R\<^sup>*\<^sup>* = R" if "transp R" "reflp R"
+  apply(rule ext iffI)+
+  subgoal premises prems for x y using prems by(induction)(use that in \<open>auto intro: reflpD transpD\<close>)
+  subgoal by(rule r_into_rtranclp)
+  done
+
+lemma rtranclp_equivp: "R\<^sup>*\<^sup>* = R" if "equivp R"
+  using that by(simp add: rtranclp_transp_reflp equivp_reflp_symp_transp)
 
 locale confluent_quotient =
-  fixes R :: "'Fb \<Rightarrow> 'Fb \<Rightarrow> bool"
+  fixes Rb :: "'Fb \<Rightarrow> 'Fb \<Rightarrow> bool"
     and Ea :: "'Fa \<Rightarrow> 'Fa \<Rightarrow> bool"
     and Eb :: "'Fb \<Rightarrow> 'Fb \<Rightarrow> bool"
     and Ec :: "'Fc \<Rightarrow> 'Fc \<Rightarrow> bool"
@@ -20,12 +125,10 @@
     and rel_Fac :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> 'Fa \<Rightarrow> 'Fc \<Rightarrow> bool"
     and set_Fab :: "'Fab \<Rightarrow> ('a \<times> 'b) set"
     and set_Fbc :: "'Fbc \<Rightarrow> ('b \<times> 'c) set"
-  assumes confluent: "confluentp R"
-    and retract1_ab: "\<And>x y. R (\<pi>_Fabb x) y \<Longrightarrow> \<exists>z. Eab x z \<and> y = \<pi>_Fabb z"
-    and retract1_bc: "\<And>x y. R (\<pi>_Fbcb x) y \<Longrightarrow> \<exists>z. Ebc x z \<and> y = \<pi>_Fbcb z"
-    and generated: "Eb \<le> equivclp R"
-    and set_ab: "\<And>x y. Eab x y \<Longrightarrow> set_Fab x = set_Fab y"
-    and set_bc: "\<And>x y. Ebc x y \<Longrightarrow> set_Fbc x = set_Fbc y"
+  assumes confluent: "confluentp Rb"
+    and retract1_ab: "\<And>x y. Rb (\<pi>_Fabb x) y \<Longrightarrow> \<exists>z. Eab x z \<and> y = \<pi>_Fabb z \<and> set_Fab z \<subseteq> set_Fab x"
+    and retract1_bc: "\<And>x y. Rb (\<pi>_Fbcb x) y \<Longrightarrow> \<exists>z. Ebc x z \<and> y = \<pi>_Fbcb z \<and> set_Fbc z \<subseteq> set_Fbc x"
+    and generated_b: "Eb \<le> equivclp Rb"
     and transp_a: "transp Ea"
     and transp_c: "transp Ec"
     and equivp_ab: "equivp Eab"
@@ -37,10 +140,10 @@
     and \<pi>_Fbcc_respect: "rel_fun Ebc Ec \<pi>_Fbcc \<pi>_Fbcc"
 begin
 
-lemma retract_ab: "R\<^sup>*\<^sup>* (\<pi>_Fabb x) y \<Longrightarrow> \<exists>z. Eab x z \<and> y = \<pi>_Fabb z"
+lemma retract_ab: "Rb\<^sup>*\<^sup>* (\<pi>_Fabb x) y \<Longrightarrow> \<exists>z. Eab x z \<and> y = \<pi>_Fabb z \<and> set_Fab z \<subseteq> set_Fab x"
   by(induction rule: rtranclp_induct)(blast dest: retract1_ab intro: equivp_transp[OF equivp_ab] equivp_reflp[OF equivp_ab])+
 
-lemma retract_bc: "R\<^sup>*\<^sup>* (\<pi>_Fbcb x) y \<Longrightarrow> \<exists>z. Ebc x z \<and> y = \<pi>_Fbcb z"
+lemma retract_bc: "Rb\<^sup>*\<^sup>* (\<pi>_Fbcb x) y \<Longrightarrow> \<exists>z. Ebc x z \<and> y = \<pi>_Fbcb z \<and> set_Fbc z \<subseteq> set_Fbc x"
   by(induction rule: rtranclp_induct)(blast dest: retract1_bc intro: equivp_transp[OF equivp_bc] equivp_reflp[OF equivp_bc])+
 
 lemma subdistributivity: "rel_Fab A OO Eb OO rel_Fbc B \<le> Ea OO rel_Fac (A OO B) OO Ec"
@@ -51,21 +154,19 @@
     where xy: "set_Fab xy \<subseteq> {(a, b). A a b}" "x = \<pi>_Faba xy" "y = \<pi>_Fabb xy"
       and y'z: "set_Fbc y'z \<subseteq> {(a, b). B a b}" "y' = \<pi>_Fbcb y'z" "z = \<pi>_Fbcc y'z"
     by(auto simp add: in_rel_Fab in_rel_Fbc)
-  from \<open>Eb y y'\<close> have "equivclp R y y'" using generated by blast
-  then obtain u where u: "R\<^sup>*\<^sup>* y u" "R\<^sup>*\<^sup>* y' u"
+  from \<open>Eb y y'\<close> have "equivclp Rb y y'" using generated_b by blast
+  then obtain u where u: "Rb\<^sup>*\<^sup>* y u" "Rb\<^sup>*\<^sup>* y' u"
     unfolding semiconfluentp_equivclp[OF confluent[THEN confluentp_imp_semiconfluentp]]
     by(auto simp add: rtranclp_conversep)
   with xy y'z obtain xy' y'z'
-    where retract1: "Eab xy xy'" "\<pi>_Fabb xy' = u"
-      and retract2: "Ebc y'z y'z'" "\<pi>_Fbcb y'z' = u"
+    where retract1: "Eab xy xy'" "\<pi>_Fabb xy' = u" "set_Fab xy' \<subseteq> set_Fab xy"
+      and retract2: "Ebc y'z y'z'" "\<pi>_Fbcb y'z' = u" "set_Fbc y'z' \<subseteq> set_Fbc y'z"
     by(auto dest!: retract_ab retract_bc)
   from retract1(1) xy have "Ea x (\<pi>_Faba xy')" by(auto dest: \<pi>_Faba_respect[THEN rel_funD])
-  moreover have "rel_Fab A (\<pi>_Faba xy') u" using xy retract1
-    by(auto simp add: in_rel_Fab dest: set_ab)
-  moreover have "rel_Fbc B u (\<pi>_Fbcc y'z')" using y'z retract2
-    by(auto simp add: in_rel_Fbc dest: set_bc)
+  moreover have "rel_Fab A (\<pi>_Faba xy') u" using xy retract1 by(auto simp add: in_rel_Fab)
+  moreover have "rel_Fbc B u (\<pi>_Fbcc y'z')" using y'z retract2 by(auto simp add: in_rel_Fbc)
   moreover have "Ec (\<pi>_Fbcc y'z') z" using retract2 y'z equivp_symp[OF equivp_bc]
-    by(auto dest: \<pi>_Fbcc_respect[THEN rel_funD])
+    by(auto intro: \<pi>_Fbcc_respect[THEN rel_funD])
   ultimately show "(Ea OO rel_Fac (A OO B) OO Ec) x z" unfolding rel_compp by blast
 qed
 
diff -r d47c8a89c6a5 -r 180981b87929 src/HOL/Library/Dlist.thy
--- a/src/HOL/Library/Dlist.thy	Tue Mar 09 11:50:21 2021 +0100
+++ b/src/HOL/Library/Dlist.thy	Tue Mar 09 14:20:27 2021 +0100
@@ -277,9 +277,9 @@
   by(auto 4 4 simp add: Dlist.dlist_eq_def vimage2p_def
      intro: equivclp_trans converse_rtranclp_into_equivclp rtranclp_into_equivclp remdups_into_doubles)
 
-qualified lemma factor_double_map: "double (map f xs) ys \<Longrightarrow> \<exists>zs. Dlist.dlist_eq xs zs \<and> ys = map f zs"
+qualified lemma factor_double_map: "double (map f xs) ys \<Longrightarrow> \<exists>zs. Dlist.dlist_eq xs zs \<and> ys = map f zs \<and> set zs \<subseteq> set xs"
   by(auto simp add: double.simps Dlist.dlist_eq_def vimage2p_def map_eq_append_conv)
-    (metis list.simps(9) map_append remdups.simps(2) remdups_append2)
+    (metis (no_types, hide_lams) list.simps(9) map_append remdups.simps(2) remdups_append2 set_append set_eq_subset set_remdups)
 
 qualified lemma dlist_eq_set_eq: "Dlist.dlist_eq xs ys \<Longrightarrow> set xs = set ys"
   by(simp add: Dlist.dlist_eq_def vimage2p_def)(metis set_remdups)
@@ -294,7 +294,6 @@
     dest: factor_double_map dlist_eq_into_doubles[THEN predicate2D] dlist_eq_set_eq
     simp add: list.in_rel list.rel_compp dlist_eq_map_respect Dlist.equivp_dlist_eq equivp_imp_transp)
 
-
 lifting_update dlist.lifting
 lifting_forget dlist.lifting
 
diff -r d47c8a89c6a5 -r 180981b87929 src/HOL/ROOT
--- a/src/HOL/ROOT	Tue Mar 09 11:50:21 2021 +0100
+++ b/src/HOL/ROOT	Tue Mar 09 14:20:27 2021 +0100
@@ -875,7 +875,8 @@
     Stream_Processor
     Cyclic_List
     Free_Idempotent_Monoid
-    LDL
+    Regex_ACI
+    Regex_ACIDZ
     TLList
     Misc_Codatatype
     Misc_Datatype