generalized confluence-based subdistributivity theorem for quotients;
new example that triggered the generalization
--- 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"
--- 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:
--- 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
--- /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
--- /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
--- 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
--- 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
--- 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