# HG changeset patch
# User traytel
# Date 1579416635 -3600
# Node ID fce780f9c9c6a0e94082c385a108bce69504aa5f
# Parent  a3f7f00b4fd8c4b862f11f0b60a103b7579f04a5
new examples of BNF lifting across quotients using a new theory of confluence,
which simplifies the relator subdistributivity proof obligation
(a few new useful notions were added to HOL;
notably the symmetric and equivalence closures of a relation)

diff -r a3f7f00b4fd8 -r fce780f9c9c6 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Fri Jan 17 18:58:58 2020 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Sun Jan 19 07:50:35 2020 +0100
@@ -2996,7 +2996,9 @@
 
 text \<open>The @{command lift_bnf} command also supports quotient types. Here is an example
 that defines the option type as a quotient of the sum type. The proof obligations
-generated by @{command lift_bnf} for quotients are different from the ones for typedefs.\<close>
+generated by @{command lift_bnf} for quotients are different from the ones for typedefs.
+You can find additional examples of usages of @{command lift_bnf} for both quotients and subtypes
+in the session \emph{HOL-Datatype_Examples}.\<close>
 
     inductive ignore_Inl :: "'a + 'a \<Rightarrow> 'a + 'a \<Rightarrow> bool" where
       "ignore_Inl (Inl x) (Inl y)"
diff -r a3f7f00b4fd8 -r fce780f9c9c6 src/HOL/Datatype_Examples/Cyclic_List.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Datatype_Examples/Cyclic_List.thy	Sun Jan 19 07:50:35 2020 +0100
@@ -0,0 +1,43 @@
+theory Cyclic_List imports
+  "HOL-Library.Confluent_Quotient"
+begin
+
+inductive cyclic1 :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" for xs where
+  "cyclic1 xs (rotate1 xs)"
+
+abbreviation cyclic :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
+  "cyclic \<equiv> equivclp cyclic1"
+
+lemma cyclic_mapI: "cyclic xs ys \<Longrightarrow> cyclic (map f xs) (map f ys)"
+  by(induction rule: equivclp_induct)
+    (auto 4 4 elim!: cyclic1.cases simp add: rotate1_map[symmetric] intro: equivclp_into_equivclp cyclic1.intros)
+
+quotient_type 'a cyclic_list = "'a list" / cyclic by simp
+
+lemma map_respect_cyclic: includes lifting_syntax shows
+  "((=) ===> cyclic ===> cyclic) map map"
+  by(auto simp add: rel_fun_def cyclic_mapI)
+
+lemma confluentp_cyclic1: "confluentp cyclic1"
+  by(intro strong_confluentp_imp_confluentp strong_confluentpI)(auto simp add: cyclic1.simps)
+
+lemma cyclic_set_eq: "cyclic xs ys \<Longrightarrow> set xs = set ys"
+  by(induction rule: converse_equivclp_induct)(simp_all add: cyclic1.simps, safe, simp_all)
+
+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)
+
+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"
+  by(unfold_locales)
+    (auto dest: retract_cyclic1 cyclic_set_eq simp add: list.in_rel list.rel_compp map_respect_cyclic[THEN rel_funD, OF refl] confluentp_cyclic1 intro: rtranclp_mono[THEN predicate2D, OF symclp_greater])
+
+lift_bnf 'a cyclic_list [wits: "[]"]
+  subgoal by(rule confluent_quotient.subdistributivity[OF confluent_quotient_cyclic1])
+  subgoal by(force dest: cyclic_set_eq)
+  subgoal by(auto elim: allE[where x="[]"])
+  done
+
+end
diff -r a3f7f00b4fd8 -r fce780f9c9c6 src/HOL/Datatype_Examples/Dlist.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Datatype_Examples/Dlist.thy	Sun Jan 19 07:50:35 2020 +0100
@@ -0,0 +1,82 @@
+theory Dlist imports
+  "HOL-Library.Confluent_Quotient"
+begin
+
+context begin
+
+qualified definition dlist_eq where "dlist_eq = BNF_Def.vimage2p remdups remdups (=)"
+
+lemma equivp_dlist_eq: "equivp dlist_eq"
+  unfolding dlist_eq_def by(rule equivp_vimage2p)(rule identity_equivp)
+
+quotient_type 'a dlist = "'a list" / dlist_eq
+  by (rule equivp_dlist_eq)
+
+qualified inductive double :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
+  "double (xs @ ys) (xs @ x # ys)" if "x \<in> set ys"
+
+qualified lemma strong_confluentp_double: "strong_confluentp double"
+proof
+  fix xs ys zs :: "'a list"
+  assume ys: "double xs ys" and zs: "double xs zs"
+  consider (left) as y bs z cs where "xs = as @ bs @ cs" "ys = as @ y # bs @ cs" "zs = as @ bs @ z # cs" "y \<in> set (bs @ cs)" "z \<in> set cs"
+    | (right) as y bs z cs where "xs = as @ bs @ cs" "ys = as @ bs @ y # cs" "zs = as @ z # bs @ cs" "y \<in> set cs" "z \<in> set (bs @ cs)"
+  proof -
+    show thesis using ys zs
+      by(clarsimp simp add: double.simps append_eq_append_conv2)(auto intro: that)
+  qed
+  then show "\<exists>us. double\<^sup>*\<^sup>* ys us \<and> double\<^sup>=\<^sup>= zs us"
+  proof cases
+    case left
+    let ?us = "as @ y # bs @ z # cs"
+    have "double ys ?us" "double zs ?us" using left
+      by(auto 4 4 simp add: double.simps)(metis append_Cons append_assoc)+
+    then show ?thesis by blast
+  next
+    case right
+    let ?us = "as @ z # bs @ y # cs"
+    have "double ys ?us" "double zs ?us" using right
+      by(auto 4 4 simp add: double.simps)(metis append_Cons append_assoc)+
+    then show ?thesis by blast
+  qed
+qed
+
+qualified lemma double_Cons1 [simp]: "double xs (x # xs)" if "x \<in> set xs"
+  using double.intros[of x xs "[]"] that by simp
+
+qualified lemma double_Cons_same [simp]: "double xs ys \<Longrightarrow> double (x # xs) (x # ys)"
+  by(auto simp add: double.simps Cons_eq_append_conv)
+
+qualified lemma doubles_Cons_same: "double\<^sup>*\<^sup>* xs ys \<Longrightarrow> double\<^sup>*\<^sup>* (x # xs) (x # ys)"
+  by(induction rule: rtranclp_induct)(auto intro: rtranclp.rtrancl_into_rtrancl)
+
+qualified lemma remdups_into_doubles: "double\<^sup>*\<^sup>* (remdups xs) xs"
+  by(induction xs)(auto intro: doubles_Cons_same rtranclp.rtrancl_into_rtrancl)
+
+qualified lemma dlist_eq_into_doubles: "dlist_eq \<le> equivclp double"
+  by(auto 4 4 simp add: 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_eq xs zs \<and> ys = map f zs"
+  by(auto simp add: double.simps dlist_eq_def vimage2p_def map_eq_append_conv)
+    (metis list.simps(9) map_append remdups.simps(2) remdups_append2)
+
+qualified lemma dlist_eq_set_eq: "dlist_eq xs ys \<Longrightarrow> set xs = set ys"
+  by(simp add: dlist_eq_def vimage2p_def)(metis set_remdups)
+
+qualified lemma dlist_eq_map_respect: "dlist_eq xs ys \<Longrightarrow> dlist_eq (map f xs) (map f ys)"
+  by(clarsimp simp add: dlist_eq_def vimage2p_def)(metis remdups_map_remdups)
+
+qualified lemma confluent_quotient_dlist:
+  "confluent_quotient double dlist_eq dlist_eq dlist_eq dlist_eq dlist_eq (map fst) (map snd) (map fst) (map snd) list_all2 list_all2 list_all2 set set"
+  by(unfold_locales)(auto intro: strong_confluentp_imp_confluentp strong_confluentp_double 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 equivp_dlist_eq equivp_imp_transp)
+
+lift_bnf 'a dlist [wits: "[]"]
+  subgoal for A B by(rule confluent_quotient.subdistributivity[OF confluent_quotient_dlist])
+  subgoal by(force dest: dlist_eq_set_eq intro: equivp_reflp[OF equivp_dlist_eq])
+  subgoal by(auto simp add: dlist_eq_def vimage2p_def)
+  done
+
+end
+
+end
diff -r a3f7f00b4fd8 -r fce780f9c9c6 src/HOL/Datatype_Examples/Free_Idempotent_Monoid.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Datatype_Examples/Free_Idempotent_Monoid.thy	Sun Jan 19 07:50:35 2020 +0100
@@ -0,0 +1,265 @@
+theory Free_Idempotent_Monoid imports
+  "HOL-Library.Confluent_Quotient"
+begin
+
+inductive cancel1 :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
+where cancel1: "xs \<noteq> [] \<Longrightarrow> cancel1 (gs @ xs @ xs @ gs') (gs @ xs @ gs')"
+
+abbreviation cancel where "cancel \<equiv> cancel1\<^sup>*\<^sup>*"
+
+lemma cancel1_append_same1:
+  assumes "cancel1 xs ys"
+  shows "cancel1 (zs @ xs) (zs @ ys)"
+using assms
+proof cases
+  case (cancel1 ys gs gs')
+  from \<open>ys \<noteq> []\<close> have "cancel1 ((zs @ gs) @ ys @ ys @ gs') ((zs @ gs) @ ys @ gs')" ..
+  with cancel1 show ?thesis by simp
+qed
+
+lemma cancel_append_same1: "cancel (zs @ xs) (zs @ ys)" if "cancel xs ys"
+  using that by induction(blast intro: rtranclp.rtrancl_into_rtrancl cancel1_append_same1)+
+
+lemma cancel1_append_same2: "cancel1 xs ys \<Longrightarrow> cancel1 (xs @ zs) (ys @ zs)"
+by(cases rule: cancel1.cases)(auto intro: cancel1.intros)
+
+lemma cancel_append_same2: "cancel (xs @ zs) (ys @ zs)" if "cancel xs ys"
+  using that by induction(blast intro: rtranclp.rtrancl_into_rtrancl cancel1_append_same2)+
+
+lemma cancel1_same:
+  assumes "xs \<noteq> []"
+  shows "cancel1 (xs @ xs) xs"
+proof -
+  have "cancel1 ([] @ xs @ xs @ []) ([] @ xs @ [])" using assms ..
+  thus ?thesis by simp
+qed
+
+lemma cancel_same: "cancel (xs @ xs) xs"
+  by(cases "xs = []")(auto intro: cancel1_same)
+
+abbreviation (input) eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
+where "eq \<equiv> equivclp cancel1"
+
+lemma eq_sym: "eq x y \<Longrightarrow> eq y x"
+  by(rule equivclp_sym)
+
+lemma equivp_eq: "equivp eq" by simp
+
+lemma eq_append_same1: "eq xs' ys' \<Longrightarrow> eq (xs @ xs') (xs @ ys')"
+  by(induction rule: equivclp_induct)(auto intro: cancel1_append_same1 equivclp_into_equivclp)
+
+lemma append_eq_cong: "\<lbrakk>eq xs ys; eq xs' ys'\<rbrakk> \<Longrightarrow> eq (xs @ xs') (ys @ ys')"
+  by(induction rule: equivclp_induct)(auto intro: eq_append_same1 equivclp_into_equivclp cancel1_append_same2)
+
+
+quotient_type 'a fim = "'a list" / eq by simp
+
+instantiation fim :: (type) monoid_add begin
+lift_definition zero_fim :: "'a fim" is "[]" .
+lift_definition plus_fim :: "'a fim \<Rightarrow> 'a fim \<Rightarrow> 'a fim" is "(@)" by(rule append_eq_cong)
+instance by(intro_classes; transfer; simp)
+end
+
+lemma plus_idem_fim [simp]: fixes x :: "'a fim" shows "x + x = x"
+proof transfer
+  fix xs :: "'a list"
+  show "eq (xs @ xs) xs"
+  proof(cases "xs = []")
+    case False thus ?thesis using cancel1_same[of xs] by(auto)
+  qed simp
+qed
+
+
+inductive pcancel1 :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
+  pcancel1: "pcancel1 (concat xss) (concat yss)" if "list_all2 (\<lambda>xs ys. xs = ys \<or> xs = ys @ ys) xss yss"
+
+lemma cancel1_into_pcancel1: "pcancel1 xs ys" if "cancel1 xs ys"
+  using that
+proof cases
+  case (cancel1 xs gs gs')
+  let ?xss = "[gs, xs @ xs, gs']" and ?yss = "[gs, xs, gs']"
+  have "pcancel1 (concat ?xss) (concat ?yss)" by(rule pcancel1.intros) simp
+  then show ?thesis using cancel1 by simp
+qed
+
+lemma pcancel_into_cancel: "cancel1\<^sup>*\<^sup>* xs ys" if "pcancel1 xs ys"
+  using that
+proof cases
+  case (pcancel1 xss yss)
+  from pcancel1(3) show ?thesis unfolding pcancel1(1-2)
+    apply induction
+     apply simp
+    apply(auto intro: cancel_append_same1)
+    apply(rule rtranclp_trans)
+    apply(subst append_assoc[symmetric])
+     apply(rule cancel_append_same2)
+     apply(rule cancel_same)
+    apply(auto intro: cancel_append_same1)
+    done
+qed
+
+lemma pcancel1_cancel1_confluent:
+  assumes "pcancel1 xs ys"
+    and "cancel1 zs ys"
+  shows "\<exists>us. cancel us xs \<and> pcancel1 us zs"
+proof -
+  let ?P = "\<lambda>xs ys. xs = ys \<or> xs = ys @ ys"
+  consider ass as2 bs1 bss bs2 cs1 css ass' as2bs1 bss' bs2cs1 css'
+    where "ys = concat ass @ as2 @ bs1 @ concat bss @ bs2 @ cs1 @ concat css"
+     and "xs = concat ass' @ as2bs1 @ concat bss' @ bs2cs1 @ concat css'"
+     and "zs = concat ass @ as2 @ bs1 @ concat bss @ bs2 @ bs1 @ concat bss @ bs2 @ cs1 @ concat css"
+     and "list_all2 ?P ass' ass"
+     and "list_all2 ?P bss' bss"
+     and "list_all2 ?P css' css"
+     and "?P as2bs1 (as2 @ bs1)"
+     and "?P bs2cs1 (bs2 @ cs1)"
+   | ass as2 bs cs1 css ass' css'
+   where "ys = concat ass @ as2 @ bs @ cs1 @ concat css"
+     and "xs = concat ass' @ as2 @ bs @ cs1 @ as2 @ bs @ cs1 @ concat css'"
+     and "zs = concat ass @ as2 @ bs @ bs @ cs1 @ concat css"
+     and "list_all2 ?P ass' ass"
+     and "list_all2 ?P css' css"
+  proof -
+    from assms obtain xss bs as cs yss
+      where xs: "xs = concat xss" and zs: "zs = as @ bs @ bs @ cs"
+      and xss: "list_all2 (\<lambda>xs ys. xs = ys \<or> xs = ys @ ys) xss yss"
+      and ys: "ys = as @ bs @ cs"
+      and yss: "concat yss = as @ bs @ cs"
+      and bs: "bs \<noteq> []"
+      by(clarsimp simp add: pcancel1.simps cancel1.simps)
+    from yss bs obtain ass as2 BS bcss
+      where yss: "yss = ass @ (as2 @ BS) # bcss"
+       and as: "as = concat ass @ as2"
+       and eq: "bs @ cs = BS @ concat bcss"
+      by(auto simp add: concat_eq_append_conv split: if_split_asm)
+    define bcss' where "bcss' = (if bcss = [] then [[]] else bcss)"
+    have bcss': "bcss' \<noteq> []" by(simp add: bcss'_def)
+    from eq consider us where "bs = BS @ us" "concat bcss = us @ cs" "bcss \<noteq> []" |
+      "BS = bs @ cs" "bcss = []" |
+      us where "BS = bs @ us" "cs = us @ concat bcss"
+      by(cases "bcss = []")(auto simp add: append_eq_append_conv2)
+    then show thesis
+    proof cases
+      case 1
+      from 1(2,3) obtain bss bs2 cs1 css
+        where "bcss = bss @ (bs2 @ cs1) # css"
+          and us: "us = concat bss @ bs2"
+          and cs: "cs = cs1 @ concat css" by(auto simp add: concat_eq_append_conv)
+      with 1 xs xss ys yss zs as that(1)[of ass as2 BS bss bs2 cs1 css] show ?thesis
+        by(clarsimp simp add: list_all2_append2 list_all2_Cons2)
+    next
+      case 2
+      with xs xss ys yss zs as show ?thesis
+        using that(1)[of ass as2 bs "[]" "[]" "[]" "[cs]" _ "as2 @ bs" "[]" "[]" "[cs]"]
+        using that(2)[of ass as2 bs cs "[]"]
+        by(auto simp add: list_all2_append2 list_all2_Cons2)
+    next
+      case 3
+      with xs xss ys yss zs as show ?thesis
+        using that(1)[of ass as2 "[]" "[bs]" "[]" "us" "bcss" _ "as2" "[bs]"] that(2)[of ass as2 bs us bcss]
+        by(auto simp add: list_all2_append2 list_all2_Cons2)
+    qed
+  qed
+  then show ?thesis
+  proof cases
+    case 1
+    let ?us = "concat ass' @ as2bs1 @ concat bss' @ bs2 @ bs1 @ concat bss' @ bs2cs1 @ concat css'"
+    have "?us = concat (ass' @ [as2bs1] @ bss' @ [bs2 @ bs1] @ bss' @ [bs2cs1] @ css')" by simp
+    also have "pcancel1 \<dots> (concat (ass @ [as2 @ bs1] @ bss @ [bs2 @ bs1] @ bss @ [bs2 @ cs1] @ css))"
+      by(rule pcancel1.intros)(use 1 in \<open>simp add: list_all2_appendI\<close>)
+    also have "\<dots> = zs" using 1 by simp
+    also have "cancel ?us xs"
+    proof -
+      define as2b where "as2b = (if as2bs1 = as2 @ bs1 then as2 else as2 @ bs1 @ as2)"
+      have as2bs1: "as2bs1 = as2b @ bs1" using 1 by(auto simp add: as2b_def)
+      define b2cs where "b2cs = (if bs2cs1 = bs2 @ cs1 then cs1 else cs1 @ bs2 @ cs1)"
+      have bs2cs1: "bs2cs1 = bs2 @ b2cs" using 1 by(auto simp add: b2cs_def)
+      have "?us = (concat ass' @ as2b) @ ((bs1 @ concat bss' @ bs2) @ (bs1 @ concat bss' @ bs2)) @ b2cs @ concat css'"
+        by(simp add: as2bs1 bs2cs1)
+      also have "cancel \<dots> ((concat ass' @ as2b) @ (bs1 @ concat bss' @ bs2) @ b2cs @ concat css')"
+        by(rule cancel_append_same1 cancel_append_same2 cancel_same)+
+      also have "\<dots> = xs" using 1 bs2cs1 as2bs1 by simp
+      finally show ?thesis .
+    qed
+    ultimately show ?thesis by blast
+  next
+    case 2
+    let ?us = "concat ass' @ as2 @ bs @ bs @ cs1 @ as2 @ bs @ bs @ cs1 @ concat css'"
+    have "?us = concat (ass' @ [as2 @ bs @ bs @ cs1 @ as2 @ bs @ bs @ cs1] @ css')" by simp
+    also have "pcancel1 \<dots> (concat (ass @ [as2 @ bs @ bs @ cs1] @ css))"
+      by(intro pcancel1.intros list_all2_appendI)(simp_all add: 2)
+    also have "\<dots> = zs" using 2 by simp
+    also have "cancel ?us xs"
+    proof -
+      have "?us = (concat ass' @ as2) @ (bs @ bs) @ cs1 @ as2 @ bs @ bs @ cs1 @ concat css'" by simp
+      also have "cancel \<dots> ((concat ass' @ as2) @ bs @ cs1 @ as2 @ bs @ bs @ cs1 @ concat css')"
+        by(rule cancel_append_same1 cancel_append_same2 cancel_same)+
+      also have "\<dots> = (concat ass' @ as2 @ bs @ cs1 @ as2) @ (bs @ bs) @ cs1 @ concat css'" by simp
+      also have "cancel \<dots> ((concat ass' @ as2 @ bs @ cs1 @ as2) @ bs @ cs1 @ concat css')"
+        by(rule cancel_append_same1 cancel_append_same2 cancel_same)+
+      also have "\<dots> = xs" using 2 by simp
+      finally show ?thesis .
+    qed
+    ultimately show ?thesis by blast
+  qed
+qed
+
+lemma pcancel1_cancel_confluent:
+  assumes "pcancel1 xs ys"
+    and "cancel zs ys"
+  shows "\<exists>us. cancel us xs \<and> pcancel1 us zs"
+  using assms(2,1)
+  by(induction arbitrary: xs)(fastforce elim!: rtranclp_trans dest: pcancel1_cancel1_confluent)+
+
+lemma cancel1_semiconfluent:
+  assumes "cancel1 xs ys"
+    and "cancel zs ys"
+  shows "\<exists>us. cancel us xs \<and> cancel us zs"
+  using pcancel1_cancel_confluent[OF cancel1_into_pcancel1, OF assms]
+  by(blast intro: pcancel_into_cancel)
+
+lemma semiconfluentp_cancel1: "semiconfluentp cancel1\<inverse>\<inverse>"
+  by(auto simp add: semiconfluentp_def rtranclp_conversep dest: cancel1_semiconfluent)
+
+lemma retract_cancel1_aux:
+  assumes "cancel1 ys (map f xs)"
+  shows "\<exists>zs. cancel1 zs xs \<and> ys = map f zs"
+  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"
+  using retract_cancel1_aux[OF assms] by(blast intro: symclpI)
+
+lemma cancel1_set_eq:
+  assumes "cancel1 ys xs"
+  shows "set ys = set xs"
+  using assms by cases auto
+
+lemma eq_set_eq: "set xs = set ys" if "eq xs ys"
+  using that by(induction)(auto dest!: cancel1_set_eq elim!: symclpE)
+
+context includes lifting_syntax begin
+lemma map_respect_cancel1: "((=) ===> cancel1 ===> eq) map map"
+  by(auto 4 4 simp add: rel_fun_def cancel1.simps intro: symclpI cancel1.intros)
+
+lemma map_respect_eq: "((=) ===> eq ===> eq) map map"
+  apply(intro rel_funI; hypsubst)
+  subgoal for _ f x y
+    by(induction rule: equivclp_induct)
+      (auto dest: map_respect_cancel1[THEN rel_funD, THEN rel_funD, OF refl] intro: eq_sym equivclp_trans)
+  done
+end
+
+lemma confluent_quotient_fim:
+  "confluent_quotient cancel1\<inverse>\<inverse> eq eq eq eq eq (map fst) (map snd) (map fst) (map snd) list_all2 list_all2 list_all2 set set"
+  by(unfold_locales)(auto dest: retract_cancel1 eq_set_eq simp add: list.in_rel list.rel_compp map_respect_eq[THEN rel_funD, OF refl] semiconfluentp_imp_confluentp semiconfluentp_cancel1)+
+
+lift_bnf 'a fim [wits: "[]"]
+  subgoal for A B by(rule confluent_quotient.subdistributivity[OF confluent_quotient_fim])
+  subgoal by(force dest: eq_set_eq)
+  subgoal by(auto elim: allE[where x="[]"])
+  done
+
+end
diff -r a3f7f00b4fd8 -r fce780f9c9c6 src/HOL/Datatype_Examples/LDL.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Datatype_Examples/LDL.thy	Sun Jan 19 07:50:35 2020 +0100
@@ -0,0 +1,339 @@
+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 (no_warn_wits) '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 a3f7f00b4fd8 -r fce780f9c9c6 src/HOL/Equiv_Relations.thy
--- a/src/HOL/Equiv_Relations.thy	Fri Jan 17 18:58:58 2020 +0100
+++ b/src/HOL/Equiv_Relations.thy	Sun Jan 19 07:50:35 2020 +0100
@@ -484,6 +484,105 @@
 lemma equivp_transp: "equivp R \<Longrightarrow> R x y \<Longrightarrow> R y z \<Longrightarrow> R x z"
   by (erule equivpE, erule transpE)
 
+lemma equivp_rtranclp: "symp r \<Longrightarrow> equivp r\<^sup>*\<^sup>*"
+  by(intro equivpI reflpI sympI transpI)(auto dest: sympD[OF symp_rtranclp])
+
+lemmas equivp_rtranclp_symclp [simp] = equivp_rtranclp[OF symp_symclp]
+
+lemma equivp_vimage2p: "equivp R \<Longrightarrow> equivp (vimage2p f f R)"
+  by(auto simp add: equivp_def vimage2p_def dest: fun_cong)
+
+lemma equivp_imp_transp: "equivp R \<Longrightarrow> transp R"
+  by(simp add: equivp_reflp_symp_transp)
+
+
+subsection \<open>Equivalence closure\<close>
+
+definition equivclp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" where
+  "equivclp r = (symclp r)\<^sup>*\<^sup>*"
+
+lemma transp_equivclp [simp]: "transp (equivclp r)"
+  by(simp add: equivclp_def)
+
+lemma reflp_equivclp [simp]: "reflp (equivclp r)"
+  by(simp add: equivclp_def)
+
+lemma symp_equivclp [simp]: "symp (equivclp r)"
+  by(simp add: equivclp_def)
+
+lemma equivp_evquivclp [simp]: "equivp (equivclp r)"
+  by(simp add: equivpI)
+
+lemma tranclp_equivclp [simp]: "(equivclp r)\<^sup>+\<^sup>+ = equivclp r"
+  by(simp add: equivclp_def)
+
+lemma rtranclp_equivclp [simp]: "(equivclp r)\<^sup>*\<^sup>* = equivclp r"
+  by(simp add: equivclp_def)
+
+lemma symclp_equivclp [simp]: "symclp (equivclp r) = equivclp r"
+  by(simp add: equivclp_def symp_symclp_eq)
+
+lemma equivclp_symclp [simp]: "equivclp (symclp r) = equivclp r"
+  by(simp add: equivclp_def)
+
+lemma equivclp_conversep [simp]: "equivclp (conversep r) = equivclp r"
+  by(simp add: equivclp_def)
+
+lemma equivclp_sym [sym]: "equivclp r x y \<Longrightarrow> equivclp r y x"
+  by(rule sympD[OF symp_equivclp])
+
+lemma equivclp_OO_equivclp_le_equivclp: "equivclp r OO equivclp r \<le> equivclp r"
+  by(rule transp_relcompp_less_eq transp_equivclp)+
+
+lemma rtranlcp_le_equivclp: "r\<^sup>*\<^sup>* \<le> equivclp r"
+  unfolding equivclp_def by(rule rtranclp_mono)(simp add: symclp_pointfree)
+
+lemma rtranclp_conversep_le_equivclp: "r\<inverse>\<inverse>\<^sup>*\<^sup>* \<le> equivclp r"
+  unfolding equivclp_def by(rule rtranclp_mono)(simp add: symclp_pointfree)
+
+lemma symclp_rtranclp_le_equivclp: "symclp r\<^sup>*\<^sup>* \<le> equivclp r"
+  unfolding symclp_pointfree
+  by(rule le_supI)(simp_all add: rtranclp_conversep[symmetric] rtranlcp_le_equivclp rtranclp_conversep_le_equivclp)
+
+lemma r_OO_conversep_into_equivclp:
+  "r\<^sup>*\<^sup>* OO r\<inverse>\<inverse>\<^sup>*\<^sup>* \<le> equivclp r"
+  by(blast intro: order_trans[OF _ equivclp_OO_equivclp_le_equivclp] relcompp_mono rtranlcp_le_equivclp rtranclp_conversep_le_equivclp del: predicate2I)
+
+lemma equivclp_induct [consumes 1, case_names base step, induct pred: equivclp]:
+  assumes a: "equivclp r a b"
+    and cases: "P a" "\<And>y z. equivclp r a y \<Longrightarrow> r y z \<or> r z y \<Longrightarrow> P y \<Longrightarrow> P z"
+  shows "P b"
+  using a unfolding equivclp_def
+  by(induction rule: rtranclp_induct; fold equivclp_def; blast intro: cases elim: symclpE)
+
+lemma converse_equivclp_induct [consumes 1, case_names base step]:
+  assumes major: "equivclp r a b"
+    and cases: "P b" "\<And>y z. r y z \<or> r z y \<Longrightarrow> equivclp r z b \<Longrightarrow> P z \<Longrightarrow> P y"
+  shows "P a"
+  using major unfolding equivclp_def
+  by(induction rule: converse_rtranclp_induct; fold equivclp_def; blast intro: cases elim: symclpE)
+
+lemma equivclp_refl [simp]: "equivclp r x x"
+  by(rule reflpD[OF reflp_equivclp])
+
+lemma r_into_equivclp [intro]: "r x y \<Longrightarrow> equivclp r x y"
+  unfolding equivclp_def by(blast intro: symclpI)
+
+lemma converse_r_into_equivclp [intro]: "r y x \<Longrightarrow> equivclp r x y"
+  unfolding equivclp_def by(blast intro: symclpI)
+
+lemma rtranclp_into_equivclp: "r\<^sup>*\<^sup>* x y \<Longrightarrow> equivclp r x y"
+  using rtranlcp_le_equivclp[of r] by blast
+
+lemma converse_rtranclp_into_equivclp: "r\<^sup>*\<^sup>* y x \<Longrightarrow> equivclp r x y"
+  by(blast intro: equivclp_sym rtranclp_into_equivclp)
+
+lemma equivclp_into_equivclp: "\<lbrakk> equivclp r a b; r b c \<or> r c b \<rbrakk> \<Longrightarrow> equivclp r a c"
+  unfolding equivclp_def by(erule rtranclp.rtrancl_into_rtrancl)(auto intro: symclpI)
+
+lemma equivclp_trans [trans]: "\<lbrakk> equivclp r a b; equivclp r b c \<rbrakk> \<Longrightarrow> equivclp r a c"
+  using equivclp_OO_equivclp_le_equivclp[of r] by blast
+
 hide_const (open) proj
 
 end
diff -r a3f7f00b4fd8 -r fce780f9c9c6 src/HOL/Library/Confluence.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Confluence.thy	Sun Jan 19 07:50:35 2020 +0100
@@ -0,0 +1,77 @@
+theory Confluence imports
+  Main
+begin
+
+section \<open>Confluence\<close>
+
+definition semiconfluentp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
+  "semiconfluentp r \<longleftrightarrow> r\<inverse>\<inverse> OO r\<^sup>*\<^sup>* \<le> r\<^sup>*\<^sup>* OO r\<inverse>\<inverse>\<^sup>*\<^sup>*"
+
+definition confluentp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
+  "confluentp r \<longleftrightarrow> r\<inverse>\<inverse>\<^sup>*\<^sup>* OO r\<^sup>*\<^sup>* \<le> r\<^sup>*\<^sup>* OO r\<inverse>\<inverse>\<^sup>*\<^sup>*"
+
+definition strong_confluentp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
+  "strong_confluentp r \<longleftrightarrow> r\<inverse>\<inverse> OO r \<le> r\<^sup>*\<^sup>* OO (r\<inverse>\<inverse>)\<^sup>=\<^sup>="
+
+lemma semiconfluentpI [intro?]:
+  "semiconfluentp r" if "\<And>x y z. \<lbrakk> r x y; r\<^sup>*\<^sup>* x z \<rbrakk> \<Longrightarrow> \<exists>u. r\<^sup>*\<^sup>* y u \<and> r\<^sup>*\<^sup>* z u"
+  using that unfolding semiconfluentp_def rtranclp_conversep by blast
+
+lemma semiconfluentpD: "\<exists>u. r\<^sup>*\<^sup>* y u \<and> r\<^sup>*\<^sup>* z u" if "semiconfluentp r" "r x y" "r\<^sup>*\<^sup>* x z"
+  using that unfolding semiconfluentp_def rtranclp_conversep by blast
+
+lemma confluentpI:
+  "confluentp r" if "\<And>x y z. \<lbrakk> r\<^sup>*\<^sup>* x y; r\<^sup>*\<^sup>* x z \<rbrakk> \<Longrightarrow> \<exists>u. r\<^sup>*\<^sup>* y u \<and> r\<^sup>*\<^sup>* z u"
+  using that unfolding confluentp_def rtranclp_conversep by blast
+
+lemma confluentpD: "\<exists>u. r\<^sup>*\<^sup>* y u \<and> r\<^sup>*\<^sup>* z u" if "confluentp r" "r\<^sup>*\<^sup>* x y" "r\<^sup>*\<^sup>* x z"
+  using that unfolding confluentp_def rtranclp_conversep by blast
+
+lemma strong_confluentpI [intro?]:
+  "strong_confluentp r" if "\<And>x y z. \<lbrakk> r x y; r x z \<rbrakk> \<Longrightarrow> \<exists>u. r\<^sup>*\<^sup>* y u \<and> r\<^sup>=\<^sup>= z u"
+  using that unfolding strong_confluentp_def by blast
+
+lemma strong_confluentpD: "\<exists>u. r\<^sup>*\<^sup>* y u \<and> r\<^sup>=\<^sup>= z u" if "strong_confluentp r" "r x y" "r x z"
+  using that unfolding strong_confluentp_def by blast
+
+lemma semiconfluentp_imp_confluentp: "confluentp r" if r: "semiconfluentp r"
+proof(rule confluentpI)
+  show "\<exists>u. r\<^sup>*\<^sup>* y u \<and> r\<^sup>*\<^sup>* z u" if "r\<^sup>*\<^sup>* x y" "r\<^sup>*\<^sup>* x z" for x y z
+    using that(2,1)
+    by(induction arbitrary: y rule: converse_rtranclp_induct)
+      (blast intro: rtranclp_trans dest:  r[THEN semiconfluentpD])+
+qed
+
+lemma confluentp_imp_semiconfluentp: "semiconfluentp r" if "confluentp r"
+  using that by(auto intro!: semiconfluentpI dest: confluentpD[OF that])
+
+lemma confluentp_eq_semiconfluentp: "confluentp r \<longleftrightarrow> semiconfluentp r"
+  by(blast intro: semiconfluentp_imp_confluentp confluentp_imp_semiconfluentp)
+
+lemma confluentp_conv_strong_confluentp_rtranclp:
+  "confluentp r \<longleftrightarrow> strong_confluentp (r\<^sup>*\<^sup>*)"
+  by(auto simp add: confluentp_def strong_confluentp_def rtranclp_conversep)
+
+lemma strong_confluentp_into_semiconfluentp:
+  "semiconfluentp r" if r: "strong_confluentp r"
+proof
+  show "\<exists>u. r\<^sup>*\<^sup>* y u \<and> r\<^sup>*\<^sup>* z u" if "r x y" "r\<^sup>*\<^sup>* x z" for x y z
+    using that(2,1)
+    apply(induction arbitrary: y rule: converse_rtranclp_induct)
+    subgoal by blast
+    subgoal for a b c
+      by (drule (1) strong_confluentpD[OF r, of a c])(auto 10 0 intro: rtranclp_trans)
+    done
+qed
+
+lemma strong_confluentp_imp_confluentp: "confluentp r" if "strong_confluentp r"
+  unfolding confluentp_eq_semiconfluentp using that by(rule strong_confluentp_into_semiconfluentp)
+
+lemma semiconfluentp_equivclp: "equivclp r = r\<^sup>*\<^sup>* OO r\<inverse>\<inverse>\<^sup>*\<^sup>*" if r: "semiconfluentp r"
+proof(rule antisym[rotated] r_OO_conversep_into_equivclp predicate2I)+
+  show "(r\<^sup>*\<^sup>* OO r\<inverse>\<inverse>\<^sup>*\<^sup>*) x y" if "equivclp r x y" for x y using that unfolding equivclp_def rtranclp_conversep
+    by(induction rule: converse_rtranclp_induct)
+      (blast elim!: symclpE intro: converse_rtranclp_into_rtranclp rtranclp_trans dest: semiconfluentpD[OF r])+
+qed
+
+end
\ No newline at end of file
diff -r a3f7f00b4fd8 -r fce780f9c9c6 src/HOL/Library/Confluent_Quotient.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Confluent_Quotient.thy	Sun Jan 19 07:50:35 2020 +0100
@@ -0,0 +1,74 @@
+theory Confluent_Quotient imports 
+  Confluence
+begin
+
+section \<open>Subdistributivity for quotients via confluence\<close>
+
+locale confluent_quotient =
+  fixes R :: "'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"
+    and Eab :: "'Fab \<Rightarrow> 'Fab \<Rightarrow> bool"
+    and Ebc :: "'Fbc \<Rightarrow> 'Fbc \<Rightarrow> bool"
+    and \<pi>_Faba :: "'Fab \<Rightarrow> 'Fa"
+    and \<pi>_Fabb :: "'Fab \<Rightarrow> 'Fb"
+    and \<pi>_Fbcb :: "'Fbc \<Rightarrow> 'Fb"
+    and \<pi>_Fbcc :: "'Fbc \<Rightarrow> 'Fc"
+    and rel_Fab :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'Fa \<Rightarrow> 'Fb \<Rightarrow> bool"
+    and rel_Fbc :: "('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> 'Fb \<Rightarrow> 'Fc \<Rightarrow> bool"
+    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"
+    and transp_a: "transp Ea"
+    and transp_c: "transp Ec"
+    and equivp_ab: "equivp Eab"
+    and equivp_bc: "equivp Ebc"
+    and in_rel_Fab: "\<And>A x y. rel_Fab A x y \<longleftrightarrow> (\<exists>z. z \<in> {x. set_Fab x \<subseteq> {(x, y). A x y}} \<and> \<pi>_Faba z = x \<and> \<pi>_Fabb z = y)"
+    and in_rel_Fbc: "\<And>B x y. rel_Fbc B x y \<longleftrightarrow> (\<exists>z. z \<in> {x. set_Fbc x \<subseteq> {(x, y). B x y}} \<and> \<pi>_Fbcb z = x \<and> \<pi>_Fbcc z = y)"
+    and rel_compp: "\<And>A B. rel_Fac (A OO B) = rel_Fab A OO rel_Fbc B"
+    and \<pi>_Faba_respect: "rel_fun Eab Ea \<pi>_Faba \<pi>_Faba"
+    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"
+  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"
+  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"
+proof(rule predicate2I; elim relcomppE)
+  fix x y y' z
+  assume "rel_Fab A x y" and "Eb y y'" and "rel_Fbc B y' z"
+  then obtain xy y'z
+    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"
+    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"
+    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 "Ec (\<pi>_Fbcc y'z') z" using retract2 y'z equivp_symp[OF equivp_bc]
+    by(auto dest: \<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
+
+end
+
+end
\ No newline at end of file
diff -r a3f7f00b4fd8 -r fce780f9c9c6 src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Fri Jan 17 18:58:58 2020 +0100
+++ b/src/HOL/Library/Library.thy	Sun Jan 19 07:50:35 2020 +0100
@@ -14,6 +14,8 @@
   Combine_PER
   Complete_Partial_Order2
   Conditional_Parametricity
+  Confluence
+  Confluent_Quotient
   Countable
   Countable_Complete_Lattices
   Countable_Set_Type
diff -r a3f7f00b4fd8 -r fce780f9c9c6 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Jan 17 18:58:58 2020 +0100
+++ b/src/HOL/List.thy	Sun Jan 19 07:50:35 2020 +0100
@@ -1519,7 +1519,7 @@
     also have "\<dots> = Suc(card(Suc ` ?S))" using fin
       by (simp add: card_image)
     also have "\<dots> = card ?S'" using eq fin
-      by (simp add:card_insert_if) 
+      by (simp add:card_insert_if)
     finally show ?thesis .
   next
     assume "\<not> p x"
@@ -1663,6 +1663,30 @@
 lemma concat_injective: "concat xs = concat ys ==> length xs = length ys ==> \<forall>(x, y) \<in> set (zip xs ys). length x = length y ==> xs = ys"
   by (simp add: concat_eq_concat_iff)
 
+lemma concat_eq_appendD:
+  assumes "concat xss = ys @ zs" "xss \<noteq> []"
+  shows "\<exists>xss1 xs xs' xss2. xss = xss1 @ (xs @ xs') # xss2 \<and> ys = concat xss1 @ xs \<and> zs = xs' @ concat xss2"
+  using assms
+proof(induction xss arbitrary: ys)
+  case (Cons xs xss)
+  from Cons.prems consider
+    us where "xs @ us = ys" "concat xss = us @ zs" |
+    us where "xs = ys @ us" "us @ concat xss = zs"
+    by(auto simp add: append_eq_append_conv2)
+  then show ?case
+  proof cases
+    case 1
+    then show ?thesis using Cons.IH[OF 1(2)]
+      by(cases xss)(auto intro: exI[where x="[]"], metis append.assoc append_Cons concat.simps(2))
+  qed(auto intro: exI[where x="[]"])
+qed simp
+
+lemma concat_eq_append_conv:
+  "concat xss = ys @ zs \<longleftrightarrow>
+  (if xss = [] then ys = [] \<and> zs = []
+   else \<exists>xss1 xs xs' xss2. xss = xss1 @ (xs @ xs') # xss2 \<and> ys = concat xss1 @ xs \<and> zs = xs' @ concat xss2)"
+  by(auto dest: concat_eq_appendD)
+
 
 subsubsection \<open>\<^const>\<open>nth\<close>\<close>
 
@@ -1709,7 +1733,7 @@
   "(xs = ys) = (length xs = length ys \<and> (\<forall>i<length xs. xs!i = ys!i))"
 proof (induct xs arbitrary: ys)
   case (Cons x xs ys)
-  show ?case 
+  show ?case
   proof (cases ys)
     case (Cons y ys)
     then show ?thesis
@@ -2241,6 +2265,20 @@
     by (cases zs, auto)
 qed auto
 
+lemma map_eq_append_conv:
+  "map f xs = ys @ zs \<longleftrightarrow> (\<exists>us vs. xs = us @ vs \<and> ys = map f us \<and> zs = map f vs)"
+proof -
+  have "map f xs \<noteq> ys @ zs \<and> map f xs \<noteq> ys @ zs \<or> map f xs \<noteq> ys @ zs \<or> map f xs = ys @ zs \<and>
+    (\<exists>bs bsa. xs = bs @ bsa \<and> ys = map f bs \<and> zs = map f bsa)"
+    by (metis append_eq_conv_conj append_take_drop_id drop_map take_map)
+  then show ?thesis
+    using map_append by blast
+qed
+
+lemma append_eq_map_conv:
+  "ys @ zs = map f xs \<longleftrightarrow> (\<exists>us vs. xs = us @ vs \<and> ys = map f us \<and> zs = map f vs)"
+by (metis map_eq_append_conv)
+
 lemma take_add:  "take (i+j) xs = take i xs @ take j (drop i xs)"
 proof (induct xs arbitrary: i)
   case (Cons x xs i) then show ?case
@@ -2296,7 +2334,7 @@
     by (simp add: upd_conv_take_nth_drop take_Cons drop_take min_def diff_Suc split: nat.split)
 qed auto
 
-lemma drop_update_swap: 
+lemma drop_update_swap:
   assumes "m \<le> n" shows "drop m (xs[n := x]) = (drop m xs)[n-m := x]"
 proof (cases "n \<ge> length xs")
   case False
@@ -3351,7 +3389,7 @@
 apply(auto simp add: nth_Cons')
 done
 
-lemma upto_split1: 
+lemma upto_split1:
   "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> [i..k] = [i..j-1] @ [j..k]"
 proof (induction j rule: int_ge_induct)
   case base thus ?case by (simp add: upto_rec1)
@@ -3359,7 +3397,7 @@
   case step thus ?case using upto_rec1 upto_rec2 by simp
 qed
 
-lemma upto_split2: 
+lemma upto_split2:
   "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> [i..k] = [i..j] @ [j+1..k]"
 using upto_rec1 upto_rec2 upto_split1 by auto
 
@@ -3475,7 +3513,7 @@
   next
     case False
     then show ?thesis
-      using d anot \<open>i < length xs\<close> 
+      using d anot \<open>i < length xs\<close>
       apply (simp add: upd_conv_take_nth_drop)
       by (metis disjoint_insert(1) distinct_append id_take_nth_drop set_simps(2))
   qed
@@ -3612,6 +3650,10 @@
   "length (remdups (concat xss)) = card (\<Union>xs\<in>set xss. set xs)"
 by (simp add: distinct_card [symmetric])
 
+lemma remdups_append2:
+  "remdups (xs @ remdups ys) = remdups (xs @ ys)"
+by(induction xs) auto
+
 lemma length_remdups_card_conv: "length(remdups xs) = card(set xs)"
 proof -
   have xs: "concat[xs] = xs" by simp
@@ -4408,6 +4450,9 @@
 lemma rotate_rotate: "rotate m (rotate n xs) = rotate (m+n) xs"
 by(simp add:rotate_add)
 
+lemma rotate1_map: "rotate1 (map f xs) = map f (rotate1 xs)"
+by(cases xs) simp_all
+
 lemma rotate1_rotate_swap: "rotate1 (rotate n xs) = rotate n (rotate1 xs)"
 by(simp add:rotate_def funpow_swap1)
 
@@ -6155,7 +6200,7 @@
 next
   case (Cons a x y) then show ?case
     by (cases y) (force+)
-qed 
+qed
 
 lemma lexord_irrefl:
   "irrefl R \<Longrightarrow> irrefl (lexord R)"
diff -r a3f7f00b4fd8 -r fce780f9c9c6 src/HOL/Quotient.thy
--- a/src/HOL/Quotient.thy	Fri Jan 17 18:58:58 2020 +0100
+++ b/src/HOL/Quotient.thy	Sun Jan 19 07:50:35 2020 +0100
@@ -839,6 +839,12 @@
 lemma rel_conj_eq_onp: "equivp R \<Longrightarrow> rel_conj R (eq_onp P) \<le> R"
   by (auto simp: eq_onp_def transp_def equivp_def)
 
+lemma Quotient_Quotient3: "Quotient R Abs Rep T \<Longrightarrow> Quotient3 R Abs Rep"
+  unfolding Quotient_def Quotient3_def by blast
+
+lemma bnf_lift_Quotient_equivp: "Quotient R Abs Rep T \<and> equivp R \<Longrightarrow> True"
+  by auto
+
 ML_file "Tools/BNF/bnf_lift.ML"
 
 hide_fact
@@ -847,6 +853,7 @@
   relcompp_mem_Grp_neq_bot comp_projr_Inr in_rel_sum_in_image_projr subset_rel_sumI
   relcompp_eq_Grp_neq_bot rel_fun_rel_OO1 rel_fun_rel_OO2 rel_sum_eq2_nonempty rel_sum_eq3_nonempty
   hypsubst equivp_add_relconj Grp_conversep_eq_onp Grp_conversep_nonempty relcomppI2 rel_conj_eq_onp
+  bnf_lift_Quotient_equivp Quotient_Quotient3
 
 end
 
diff -r a3f7f00b4fd8 -r fce780f9c9c6 src/HOL/ROOT
--- a/src/HOL/ROOT	Fri Jan 17 18:58:58 2020 +0100
+++ b/src/HOL/ROOT	Sun Jan 19 07:50:35 2020 +0100
@@ -823,6 +823,10 @@
     Lift_BNF
     Milner_Tofte
     Stream_Processor
+    Cyclic_List
+    Dlist
+    Free_Idempotent_Monoid
+    LDL
     TLList
     Misc_Codatatype
     Misc_Datatype
diff -r a3f7f00b4fd8 -r fce780f9c9c6 src/HOL/Tools/BNF/bnf_lift.ML
--- a/src/HOL/Tools/BNF/bnf_lift.ML	Fri Jan 17 18:58:58 2020 +0100
+++ b/src/HOL/Tools/BNF/bnf_lift.ML	Sun Jan 19 07:50:35 2020 +0100
@@ -805,10 +805,10 @@
   end;
 
 
-fun quotient_bnf {equiv_rel, equiv_thm, quot_thm, ...} _ wits specs map_b rel_b pred_b opts lthy =
+fun quotient_bnf (equiv_thm, quot_thm) _ wits specs map_b rel_b pred_b opts lthy =
   let
     (* extract rep_G and abs_G *)
-    val (_, abs_G, rep_G) = strip3 quot_thm;
+    val (equiv_rel, abs_G, rep_G) = strip3 quot_thm;
     val (repT, absT) = dest_funT (fastype_of abs_G); (* ("?'a F", "?'a G") *)
     val absT_name = fst (dest_Type absT);
 
@@ -1944,8 +1944,19 @@
     val specs =
       map (apsnd (apsnd (the_default @{sort type} o Option.map (prepare_sort lthy)))) raw_specs;
 
-    val which_bnf = (case Quotient_Info.lookup_quotients lthy absT_name of
-        SOME qs => quotient_bnf qs
+    val which_bnf = (case (xthm_opt, Quotient_Info.lookup_quotients lthy absT_name) of
+        (NONE, SOME qs) => quotient_bnf (#equiv_thm qs, #quot_thm qs)
+      | (SOME _, _) =>
+          if can (fn thm => thm RS @{thm bnf_lift_Quotient_equivp}) input_thm
+          then quotient_bnf (input_thm RS conjunct2, input_thm RS conjunct1 RS @{thm Quotient_Quotient3})
+          else if can (fn thm => thm RS @{thm type_definition.Rep}) input_thm
+            then typedef_bnf
+            else Pretty.chunks [Pretty.para ("Expected theorem of either form:"),
+                Pretty.item [Syntax.pretty_term lthy @{term "Quotient R Abs Rep T \<and> equivp R"}],
+                Pretty.item [Syntax.pretty_term lthy @{term "type_definition Rep Abs A"}],
+                Pretty.para ("Got"), Pretty.item [Thm.pretty_thm lthy input_thm]]
+              |> Pretty.string_of
+              |> error
       | _ => typedef_bnf);
 
   in
diff -r a3f7f00b4fd8 -r fce780f9c9c6 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Fri Jan 17 18:58:58 2020 +0100
+++ b/src/HOL/Transitive_Closure.thy	Sun Jan 19 07:50:35 2020 +0100
@@ -538,7 +538,7 @@
     show ?thesis
       by (rule rtrancl_into_trancl1) (use step in auto)
   qed auto
-  ultimately show ?thesis 
+  ultimately show ?thesis
     by auto
 qed
 
@@ -619,7 +619,7 @@
 lemma trancl_range [simp]: "Range (r\<^sup>+) = Range r"
   unfolding Domain_converse [symmetric] by (simp add: trancl_converse [symmetric])
 
-lemma Not_Domain_rtrancl: 
+lemma Not_Domain_rtrancl:
   assumes "x \<notin> Domain R" shows "(x, y) \<in> R\<^sup>* \<longleftrightarrow> x = y"
 proof -
 have "(x, y) \<in> R\<^sup>* \<Longrightarrow> x = y"
@@ -661,7 +661,7 @@
 proof (induction rule: rtrancl_induct)
   case base
   show ?case
-    by (simp add: assms)   
+    by (simp add: assms)
 next
   case (step y z)
   with xz \<open>single_valued r\<close> show ?case
@@ -683,6 +683,17 @@
   apply (drule (2) rtranclp_into_tranclp2)
   done
 
+lemma rtranclp_conversep: "r\<inverse>\<inverse>\<^sup>*\<^sup>* = r\<^sup>*\<^sup>*\<inverse>\<inverse>"
+  by(auto simp add: fun_eq_iff intro: rtranclp_converseI rtranclp_converseD)
+
+lemmas symp_rtranclp = sym_rtrancl[to_pred]
+
+lemmas symp_conv_conversep_eq = sym_conv_converse_eq[to_pred]
+
+lemmas rtranclp_tranclp_absorb [simp] = rtrancl_trancl_absorb[to_pred]
+lemmas tranclp_rtranclp_absorb [simp] = trancl_rtrancl_absorb[to_pred]
+lemmas rtranclp_reflclp_absorb [simp] = rtrancl_reflcl_absorb[to_pred]
+
 lemmas trancl_rtrancl_trancl = tranclp_rtranclp_tranclp [to_set]
 
 lemmas transitive_closure_trans [trans] =
@@ -699,6 +710,47 @@
 
 declare trancl_into_rtrancl [elim]
 
+subsection \<open>Symmetric closure\<close>
+
+definition symclp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
+where "symclp r x y \<longleftrightarrow> r x y \<or> r y x"
+
+lemma symclpI [simp, intro?]:
+  shows symclpI1: "r x y \<Longrightarrow> symclp r x y"
+  and symclpI2: "r y x \<Longrightarrow> symclp r x y"
+by(simp_all add: symclp_def)
+
+lemma symclpE [consumes 1, cases pred]:
+  assumes "symclp r x y"
+  obtains (base) "r x y" | (sym) "r y x"
+using assms by(auto simp add: symclp_def)
+
+lemma symclp_pointfree: "symclp r = sup r r\<inverse>\<inverse>"
+  by(auto simp add: symclp_def fun_eq_iff)
+
+lemma symclp_greater: "r \<le> symclp r"
+  by(simp add: symclp_pointfree)
+
+lemma symclp_conversep [simp]: "symclp r\<inverse>\<inverse> = symclp r"
+  by(simp add: symclp_pointfree sup.commute)
+
+lemma symp_symclp [simp]: "symp (symclp r)"
+  by(auto simp add: symp_def elim: symclpE intro: symclpI)
+
+lemma symp_symclp_eq: "symp r \<Longrightarrow> symclp r = r"
+  by(simp add: symclp_pointfree symp_conv_conversep_eq)
+
+lemma symp_rtranclp_symclp [simp]: "symp (symclp r)\<^sup>*\<^sup>*"
+  by(simp add: symp_rtranclp)
+
+lemma rtranclp_symclp_sym [sym]: "(symclp r)\<^sup>*\<^sup>* x y \<Longrightarrow> (symclp r)\<^sup>*\<^sup>* y x"
+  by(rule sympD[OF symp_rtranclp_symclp])
+
+lemma symclp_idem [simp]: "symclp (symclp r) = symclp r"
+  by(simp add: symclp_pointfree sup_commute converse_join)
+
+lemma reflp_rtranclp [simp]: "reflp R\<^sup>*\<^sup>*"
+  using refl_rtrancl[to_pred, of R] reflp_refl_eq[of "{(x, y). R\<^sup>*\<^sup>* x y}"] by simp
 
 subsection \<open>The power operation on relations\<close>
 
@@ -1272,6 +1324,8 @@
     addSolver (mk_solver "Rtranclp" Tranclp_Tac.rtrancl_tac))
 \<close>
 
+lemma transp_rtranclp [simp]: "transp R\<^sup>*\<^sup>*"
+  by(auto simp add: transp_def)
 
 text \<open>Optional methods.\<close>