# HG changeset patch # User traytel # Date 1615296027 -3600 # Node ID 180981b879296c932be325a75d65633978f256bf # Parent d47c8a89c6a57a6f54bc686b62f139483782e65f generalized confluence-based subdistributivity theorem for quotients; new example that triggered the generalization diff -r d47c8a89c6a5 -r 180981b87929 src/HOL/Datatype_Examples/Cyclic_List.thy --- a/src/HOL/Datatype_Examples/Cyclic_List.thy Tue Mar 09 11:50:21 2021 +0100 +++ b/src/HOL/Datatype_Examples/Cyclic_List.thy Tue Mar 09 14:20:27 2021 +0100 @@ -26,8 +26,8 @@ lemma retract_cyclic1: assumes "cyclic1 (map f xs) ys" - shows "\zs. cyclic xs zs \ ys = map f zs" - using assms by(auto simp add: cyclic1.simps rotate1_map intro: cyclic1.intros symclpI1) + shows "\zs. cyclic xs zs \ ys = map f zs \ set zs \ set xs" + using assms by(force simp add: cyclic1.simps rotate1_map intro: cyclic1.intros symclpI1) lemma confluent_quotient_cyclic1: "confluent_quotient cyclic1 cyclic cyclic cyclic cyclic cyclic (map fst) (map snd) (map fst) (map snd) list_all2 list_all2 list_all2 set set" diff -r d47c8a89c6a5 -r 180981b87929 src/HOL/Datatype_Examples/Free_Idempotent_Monoid.thy --- a/src/HOL/Datatype_Examples/Free_Idempotent_Monoid.thy Tue Mar 09 11:50:21 2021 +0100 +++ b/src/HOL/Datatype_Examples/Free_Idempotent_Monoid.thy Tue Mar 09 14:20:27 2021 +0100 @@ -223,13 +223,13 @@ lemma retract_cancel1_aux: assumes "cancel1 ys (map f xs)" - shows "\zs. cancel1 zs xs \ ys = map f zs" + shows "\zs. cancel1 zs xs \ ys = map f zs \ set zs \ 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 "\zs. eq xs zs \ ys = map f zs" + shows "\zs. eq xs zs \ ys = map f zs \ set zs \ set xs" using retract_cancel1_aux[OF assms] by(blast intro: symclpI) lemma cancel1_set_eq: diff -r d47c8a89c6a5 -r 180981b87929 src/HOL/Datatype_Examples/LDL.thy --- a/src/HOL/Datatype_Examples/LDL.thy Tue Mar 09 11:50:21 2021 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,339 +0,0 @@ -theory LDL imports - "HOL-Library.Confluent_Quotient" -begin - -datatype 'a rexp = Atom 'a | Alt "'a rexp" "'a rexp" | Conc "'a rexp" "'a rexp" | Star "'a rexp" - -inductive ACI (infix "~" 64) where - a1: "Alt (Alt r s) t ~ Alt r (Alt s t)" -| a2: "Alt r (Alt s t) ~ Alt (Alt r s) t" -| c: "Alt r s ~ Alt s r" -| i: "r ~ Alt r r" -| R: "r ~ r" -| A: "r ~ r' \ s ~ s' \ Alt r s ~ Alt r' s'" -| C: "r ~ r' \ s ~ s' \ Conc r s ~ Conc r' s'" -| S: "r ~ r' \ Star r ~ Star r'" - -declare ACI.intros[intro] - -abbreviation ACIcl (infix "~~" 64) where "(~~) \ equivclp (~)" - -lemma eq_set_preserves_inter: - fixes eq set - assumes "\r s. eq r s \ set r = set s" and "Ss \ {}" - shows "(\As\Ss. {(x, x'). eq x x'} `` {x. set x \ As}) \ {(x, x'). eq x x'} `` {x. set x \ \ Ss}" - using assms by (auto simp: subset_eq) metis - -lemma ACI_map_respects: - fixes f :: "'a \ '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 \ '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 \ (\r' s'. x = Alt r' s' \ map_rexp f r' = r \ map_rexp f s' = s)" - "map_rexp f x = Alt r s \ (\r' s'. x = Alt r' s' \ map_rexp f r' = r \ map_rexp f s' = s)" - by (cases x; auto)+ - -lemma Conc_eq_map_rexp_iff: - "Conc r s = map_rexp f x \ (\r' s'. x = Conc r' s' \ map_rexp f r' = r \ map_rexp f s' = s)" - "map_rexp f x = Conc r s \ (\r' s'. x = Conc r' s' \ map_rexp f r' = r \ map_rexp f s' = s)" - by (cases x; auto)+ - -lemma Star_eq_map_rexp_iff: - "Star r = map_rexp f x \ (\r'. x = Star r' \ map_rexp f r' = r)" - "map_rexp f x = Star r \ (\r'. x = Star r' \ map_rexp f r' = r)" - by (cases x; auto)+ - -lemma AA: "r ~~ r' \ s ~~ s' \ 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' \ (~)\<^sup>*\<^sup>* s s' \ (~)\<^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' \ s ~~ s' \ 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' \ (~)\<^sup>*\<^sup>* s s' \ (~)\<^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' \ 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' \ (~)\<^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 \ \z. x ~~ z \ 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 = "\x. _ x \ _ ~ 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 = "\x. _ x \ _ ~ 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 = "\x. _ x \ _ ~ 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 = "\x. _ x \ _ ~ 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 = "\x. _ x \ _ ~ 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 = "\x. _ x \ _ ~ 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 = "\x. _ x \ _ ~ 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 = "\x. _ x \ _ ~ 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 "\" 64) where - a: "Alt (Alt r s) t \ Alt r (Alt s t)" -| c: "Alt r s \ Alt s r" -| i: "Alt r r \ r" -| A: "r \ r' \ s \ s' \ Alt r s \ Alt r' s'" -| C: "r \ r' \ s \ s' \ Conc r s \ Conc r' s'" -| S: "r \ r' \ Star r \ Star r'" -| r: "r \ r" -| s: "r \ s \ s \ r" -| t: "r \ s \ s \ t \ r \ t" - -lemma ACIEQ_le_ACIcl: "r \ s \ r ~~ s" - by (induct r s rule: ACIEQ.induct) (auto intro: AA CC SS equivclp_sym equivclp_trans) - -lemma ACI_le_ACIEQ: "r ~ s \ r \ s" - by (induct r s rule: ACI.induct) (auto intro: ACIEQ.intros) - -lemma ACIcl_le_ACIEQ: "r ~~ s \ r \ s" - by (induct rule: equivclp_induct) (auto 0 3 intro: ACIEQ.intros ACI_le_ACIEQ) - -lemma ACIEQ_alt: "(\) = (~~)" - by (simp add: ACIEQ_le_ACIcl ACIcl_le_ACIEQ antisym predicate2I) - -quotient_type 'a ACI_rexp = "'a rexp" / "(\)" - unfolding ACIEQ_alt by (auto intro!: equivpI reflpI sympI transpI) - -lift_bnf 'a ACI_rexp - unfolding ACIEQ_alt - subgoal for A Q by (rule confluent_quotient.subdistributivity[OF confluent_quotient_ACI]) - subgoal for Ss by (intro eq_set_preserves_inter[rotated] ACIcl_set_eq; auto) - done - -datatype ldl = Prop string | And ldl ldl | Not ldl | Match "ldl ACI_rexp" - -end \ No newline at end of file diff -r d47c8a89c6a5 -r 180981b87929 src/HOL/Datatype_Examples/Regex_ACI.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Datatype_Examples/Regex_ACI.thy Tue Mar 09 14:20:27 2021 +0100 @@ -0,0 +1,342 @@ +theory Regex_ACI + imports "HOL-Library.Confluent_Quotient" +begin + +datatype 'a rexp = Zero | Eps | Atom 'a | Alt "'a rexp" "'a rexp" | Conc "'a rexp" "'a rexp" | Star "'a rexp" + +inductive ACI (infix "~" 64) where + a1: "Alt (Alt r s) t ~ Alt r (Alt s t)" +| a2: "Alt r (Alt s t) ~ Alt (Alt r s) t" +| c: "Alt r s ~ Alt s r" +| i: "r ~ Alt r r" +| R: "r ~ r" +| A: "r ~ r' \ s ~ s' \ Alt r s ~ Alt r' s'" +| C: "r ~ r' \ s ~ s' \ Conc r s ~ Conc r' s'" +| S: "r ~ r' \ Star r ~ Star r'" + +declare ACI.intros[intro] + +abbreviation ACIcl (infix "~~" 64) where "(~~) \ equivclp (~)" + +lemma eq_set_preserves_inter: + fixes eq set + assumes "\r s. eq r s \ set r = set s" and "Ss \ {}" + shows "(\As\Ss. {(x, x'). eq x x'} `` {x. set x \ As}) \ {(x, x'). eq x x'} `` {x. set x \ \ Ss}" + using assms by (auto simp: subset_eq) metis + +lemma ACI_map_respects: + fixes f :: "'a \ '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 \ '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 \ (\r' s'. x = Alt r' s' \ map_rexp f r' = r \ map_rexp f s' = s)" + "map_rexp f x = Alt r s \ (\r' s'. x = Alt r' s' \ map_rexp f r' = r \ map_rexp f s' = s)" + by (cases x; auto)+ + +lemma Conc_eq_map_rexp_iff: + "Conc r s = map_rexp f x \ (\r' s'. x = Conc r' s' \ map_rexp f r' = r \ map_rexp f s' = s)" + "map_rexp f x = Conc r s \ (\r' s'. x = Conc r' s' \ map_rexp f r' = r \ map_rexp f s' = s)" + by (cases x; auto)+ + +lemma Star_eq_map_rexp_iff: + "Star r = map_rexp f x \ (\r'. x = Star r' \ map_rexp f r' = r)" + "map_rexp f x = Star r \ (\r'. x = Star r' \ map_rexp f r' = r)" + by (cases x; auto)+ + +lemma AA: "r ~~ r' \ s ~~ s' \ 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' \ (~)\<^sup>*\<^sup>* s s' \ (~)\<^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' \ s ~~ s' \ 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' \ (~)\<^sup>*\<^sup>* s s' \ (~)\<^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' \ 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' \ (~)\<^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 \ \z. x ~~ z \ y = map_rexp f z \ set_rexp z \ 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' \ set_rexp r'" "set_rexp ss' \ 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' \ set_rexp r'" "set_rexp ss' \ 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' \ 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 = "\x. _ x \ _ ~ 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 = "\x. _ x \ _ ~ 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 = "\x. _ x \ _ ~ 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 = "\x. _ x \ _ ~ 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 = "\x. _ x \ _ ~ 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 = "\x. _ x \ _ ~ 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 = "\x. _ x \ _ ~ 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 = "\x. _ x \ _ ~ 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 "\" 64) where + a: "Alt (Alt r s) t \ Alt r (Alt s t)" +| c: "Alt r s \ Alt s r" +| i: "Alt r r \ r" +| A: "r \ r' \ s \ s' \ Alt r s \ Alt r' s'" +| C: "r \ r' \ s \ s' \ Conc r s \ Conc r' s'" +| S: "r \ r' \ Star r \ Star r'" +| r: "r \ r" +| s: "r \ s \ s \ r" +| t: "r \ s \ s \ t \ r \ t" + +lemma ACIEQ_le_ACIcl: "r \ s \ r ~~ s" + by (induct r s rule: ACIEQ.induct) (auto intro: AA CC SS equivclp_sym equivclp_trans) + +lemma ACI_le_ACIEQ: "r ~ s \ r \ s" + by (induct r s rule: ACI.induct) (auto intro: ACIEQ.intros) + +lemma ACIcl_le_ACIEQ: "r ~~ s \ r \ s" + by (induct rule: equivclp_induct) (auto 0 3 intro: ACIEQ.intros ACI_le_ACIEQ) + +lemma ACIEQ_alt: "(\) = (~~)" + by (simp add: ACIEQ_le_ACIcl ACIcl_le_ACIEQ antisym predicate2I) + +quotient_type 'a ACI_rexp = "'a rexp" / "(\)" + unfolding ACIEQ_alt by (auto intro!: equivpI reflpI sympI transpI) + +lift_bnf 'a ACI_rexp + unfolding ACIEQ_alt + subgoal for A Q by (rule confluent_quotient.subdistributivity[OF confluent_quotient_ACI]) + subgoal for Ss by (intro eq_set_preserves_inter[rotated] ACIcl_set_eq; auto) + done + +datatype ldl = Prop string | And ldl ldl | Not ldl | Match "ldl ACI_rexp" + +end \ No newline at end of file diff -r d47c8a89c6a5 -r 180981b87929 src/HOL/Datatype_Examples/Regex_ACIDZ.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Datatype_Examples/Regex_ACIDZ.thy Tue Mar 09 14:20:27 2021 +0100 @@ -0,0 +1,481 @@ +theory Regex_ACIDZ + imports "HOL-Library.Confluent_Quotient" +begin + +datatype (discs_sels) 'a rexp = Zero | Eps | Atom 'a + | Alt "'a rexp" "'a rexp" | Conc "'a rexp" "'a rexp" | Star "'a rexp" + +fun elim_zeros where + "elim_zeros (Alt r s) = + (let r' = elim_zeros r; s' = elim_zeros s in + if r' = Zero then s' else if s' = Zero then r' else Alt r' s')" +| "elim_zeros (Conc r s) = (let r' = elim_zeros r in if r' = Zero then Zero else Conc r' s)" +| "elim_zeros r = r" + +fun distribute where + "distribute t (Alt r s) = Alt (distribute t r) (distribute t s)" +| "distribute t (Conc r s) = Conc (distribute s r) t" +| "distribute t r = Conc r t" + +inductive ACIDZ (infix "~" 64) where + a1: "Alt (Alt r s) t ~ Alt r (Alt s t)" +| a2: "Alt r (Alt s t) ~ Alt (Alt r s) t" +| c: "Alt r s ~ Alt s r" +| i: "r ~ Alt r r" +| z: "r ~ s \ r ~ elim_zeros s" +| d: "Conc r t ~ distribute t r" +| R: "r ~ r" +| A: "r ~ r' \ s ~ s' \ Alt r s ~ Alt r' s'" +| C: "r ~ r' \ 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 "(~~) \ 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 \ set_rexp t" + by (induct r arbitrary: t) auto + +lemma Zero_eq_map_rexp_iff[simp]: + "Zero = map_rexp f x \ x = Zero" + "map_rexp f x = Zero \ x = Zero" + by (cases x; auto)+ + +lemma Alt_eq_map_rexp_iff: + "Alt r s = map_rexp f x \ (\r' s'. x = Alt r' s' \ map_rexp f r' = r \ map_rexp f s' = s)" + "map_rexp f x = Alt r s \ (\r' s'. x = Alt r' s' \ map_rexp f r' = r \ 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) \ set_rexp r" + by (induct r rule: elim_zeros.induct) (auto simp: Let_def) + +lemma ACIDZ_map_respects: + fixes f :: "'a \ '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 \ '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 \ set_rexp s \ 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 \ set_rexp s \ 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 \ (\r' s'. x = Conc r' s' \ map_rexp f r' = r \ map_rexp f s' = s)" + "map_rexp f x = Conc r s \ (\r' s'. x = Conc r' s' \ map_rexp f r' = r \ map_rexp f s' = s)" + by (cases x; auto)+ + +lemma Star_eq_map_rexp_iff: + "Star r = map_rexp f x \ (\r'. x = Star r' \ map_rexp f r' = r)" + "map_rexp f x = Star r \ (\r'. x = Star r' \ map_rexp f r' = r)" + by (cases x; auto)+ + +lemma AAA: "(~)\<^sup>*\<^sup>* r r' \ (~)\<^sup>*\<^sup>* s s' \ (~)\<^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' \ (~)\<^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 \ \z. (~)\<^sup>*\<^sup>* x z \ 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 \ 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 \ elim_zeros r = Zero \ 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 \ t = elim_zeros s \ r ~ t" + by (metis z) + +lemma elim_zeros_ACIDZ1: "r ~ s \ 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' \ s ~ s' \ t = elim_zeros (Alt r' s') \ Alt r s ~ t" + by (auto simp del: elim_zeros.simps) + +lemma distribute_ACIDZ1: "r ~ r' \ 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 \ (~)\<^sup>*\<^sup>* (elim_zeros r) (elim_zeros s)" + using elim_zeros_ACIDZ1 by blast + +lemma elim_zeros_ACIDZ_rtranclp: "(~)\<^sup>*\<^sup>* r s \ (~)\<^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' \ (~)\<^sup>*\<^sup>* (distribute s r) (elim_zeros (distribute s r'))" + by (metis distribute_ACIDZ1 rtranclp.simps) + +lemma ACIDZ_elim_zeros: "(~) r s \ elim_zeros r = Zero \ elim_zeros s = Zero" + by (meson elim_zeros_ACIDZ1 elim_zeros_ACIDZ_Zero) + +lemma ACIDZ_elim_zeros_rtranclp: + "(~)\<^sup>*\<^sup>* r s \ elim_zeros r = Zero \ 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 "\u. (~)\<^sup>*\<^sup>* y u \ 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 = "\x. _ x \ _ ~ 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 = "\x. _ x \ _ ~ x", OF conjI[OF _ z], rotated] + exI[where P = "\x. _ x \ _ ~ 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 = "\x. _ x \ _ ~ 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 = "\x. _ x \ _ ~ 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 = "\x. _ x \ _ ~ 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 = "\x. _ x \ _ ~ 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 = "\x. _ x \ _ ~ 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 = "\x. _ x \ _ ~ 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 = "\x. _ x \ _ ~ 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 = "\x. _ x \ _ ~ 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 = "\x. _ x \ _ ~ 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 = "\x. _ x \ _ ~ 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 = "\x. _ x \ _ ~ 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 = "\x. _ x \ _ ~ x", OF conjI[OF _ elim_zeros_ACIDZ1], rotated] + exI[where P = "\x. _ x \ _ ~ 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 "\" 64) where + a: "Alt (Alt r s) t \ Alt r (Alt s t)" +| c: "Alt r s \ Alt s r" +| i: "Alt r r \ r" +| cz: "Conc Zero r \ Zero" +| az: "Alt Zero r \ r" +| d: "Conc (Alt r s) t \ Alt (Conc r t) (Conc s t)" +| A: "r \ r' \ s \ s' \ Alt r s \ Alt r' s'" +| C: "r \ r' \ Conc r s \ Conc r' s" +| r: "r \ r" +| s: "r \ s \ s \ r" +| t: "r \ s \ s \ t \ r \ t" + +context begin + +private lemma AA: "r ~~ r' \ s ~~ s' \ 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' \ 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 \ s \ 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 \ 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 \ distribute s r" + by (induct s r rule: distribute.induct) (auto 0 3 intro: ACIDZEQ.intros) + +lemma ACIDZ_le_ACIDZEQ: "r ~ s \ r \ s" + by (induct r s rule: ACIDZ.induct) (auto 0 2 intro: ACIDZEQ.intros simp: Let_def) + +lemma ACIDZcl_le_ACIDZEQ: "r ~~ s \ r \ s" + by (induct rule: equivclp_induct) (auto 0 3 intro: ACIDZEQ.intros ACIDZ_le_ACIDZEQ) + +lemma ACIDZEQ_alt: "(\) = (~~)" + by (simp add: ACIDZEQ_le_ACIDZcl ACIDZcl_le_ACIDZEQ antisym predicate2I) + +quotient_type 'a rexp_ACIDZ = "'a rexp" / "(\)" + unfolding ACIDZEQ_alt by (auto intro!: equivpI reflpI sympI transpI) + +lift_bnf 'a rexp_ACIDZ + unfolding ACIDZEQ_alt + subgoal for A Q by (rule confluent_quotient.subdistributivity[OF confluent_quotient_ACIDZ]) + subgoal for Ss by (elim wide_intersection_finite.wide_intersection[OF wide_intersection_finite_ACIDZ]) + done + +datatype ldl = Prop string | And ldl ldl | Not ldl | Match "ldl rexp_ACIDZ" + +end diff -r d47c8a89c6a5 -r 180981b87929 src/HOL/Library/Confluent_Quotient.thy --- a/src/HOL/Library/Confluent_Quotient.thy Tue Mar 09 11:50:21 2021 +0100 +++ b/src/HOL/Library/Confluent_Quotient.thy Tue Mar 09 14:20:27 2021 +0100 @@ -1,11 +1,116 @@ -theory Confluent_Quotient imports +theory Confluent_Quotient imports Confluence begin -section \Subdistributivity for quotients via confluence\ +text \Functors with finite setters preserve wide intersection for any equivalence relation that respects the mapper.\ + +lemma Inter_finite_subset: + assumes "\A \ \. finite A" + shows "\\\\. finite \ \ (\\) = (\\)" +proof(cases "\ = {}") + case False + then obtain A where A: "A \ \" by auto + then have finA: "finite A" using assms by auto + hence fin: "finite (A - \\)" by(rule finite_subset[rotated]) auto + let ?P = "\x A. A \ \ \ x \ A" + define f where "f x = Eps (?P x)" for x + let ?\ = "insert A (f ` (A - \\))" + have "?P x (f x)" if "x \ A - \\" for x unfolding f_def by(rule someI_ex)(use that A in auto) + hence "(\?\) = (\\)" "?\ \ \" using A by auto + moreover have "finite ?\" using fin by simp + ultimately show ?thesis by blast +qed simp + +locale wide_intersection_finite = + fixes E :: "'Fa \ 'Fa \ bool" + and mapFa :: "('a \ 'a) \ 'Fa \ 'Fa" + and setFa :: "'Fa \ 'a set" + assumes equiv: "equivp E" + and map_E: "E x y \ E (mapFa f x) (mapFa f y)" + and map_id: "mapFa id x = x" + and map_cong: "\a\setFa x. f a = g a \ 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 \ Y" and z: "setFa z \ Z" and a: "a \ Y" "a \ Z" + shows "\x. E x y \ setFa x \ Y \ setFa x \ Z" +proof - + let ?f = "\b. if b \ Z then b else a" + let ?u = "mapFa ?f y" + from \E y z\ 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 "\ = z" by(rule map_id) + finally have "E ?u y" using \E y z\ equivp_symp[OF equiv] equivp_transp[OF equiv] by blast + moreover have "setFa ?u \ Y" using a y by(subst set_map) auto + moreover have "setFa ?u \ Z" using a by(subst set_map) auto + ultimately show ?thesis by blast +qed + +lemma finite_intersection: + assumes E: "\y\A. E y z" + and fin: "finite A" + and sub: "\y\A. setFa y \ Y y \ a \ Y y" + shows "\x. E x z \ (\y\A. setFa x \ 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" "\y\A. setFa x \ Y y \ a \ Y y" by auto + hence set_x: "setFa x \ (\y\A. Y y)" "a \ (\y\A. Y y)" by auto + from insert.prems have "E y z" and set_y: "setFa y \ Y y" "a \ Y y" by auto + from \E y z\ \E x z\ 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' \ \ (Y ` A)" "setFa x' \ Y y" by blast + then show ?case using \E x z\ equivp_transp[OF equiv] by blast +qed + +lemma wide_intersection: + assumes inter_nonempty: "\ Ss \ {}" + shows "(\As \ Ss. {(x, x'). E x x'} `` {x. setFa x \ As}) \ {(x, x'). E x x'} `` {x. setFa x \ \ Ss}" (is "?lhs \ ?rhs") +proof + fix x + assume lhs: "x \ ?lhs" + from inter_nonempty obtain a where a: "\As \ Ss. a \ As" by auto + from lhs obtain y where y: "\As. As \ Ss \ E (y As) x \ setFa (y As) \ As" + by atomize_elim(rule choice, auto) + define Ts where "Ts = (\As. insert a (setFa (y As))) ` Ss" + have Ts_subset: "(\Ts) \ (\Ss)" using a unfolding Ts_def by(auto dest: y) + have Ts_finite: "\Bs \ Ts. finite Bs" unfolding Ts_def by(auto dest: y intro: finite) + from Inter_finite_subset[OF this] obtain Us + where Us: "Us \ Ts" and finite_Us: "finite Us" and Int_Us: "(\Us) \ (\Ts)" by force + let ?P = "\U As. As \ Ss \ U = insert a (setFa (y As))" + define Y where "Y U = Eps (?P U)" for U + have Y: "?P U (Y U)" if "U \ Us" for U unfolding Y_def + by(rule someI_ex)(use that Us in \auto simp add: Ts_def\) + let ?f = "\U. y (Y U)" + have *: "\z\(?f ` Us). E z x" by(auto dest!: Y y) + have **: "\z\(?f ` Us). setFa z \ insert a (setFa z) \ a \ insert a (setFa z)" by auto + from finite_intersection[OF * _ **] finite_Us obtain u + where u: "E u x" and set_u: "\z\(?f ` Us). setFa u \ insert a (setFa z)" by auto + from set_u have "setFa u \ (\ Us)" by(auto dest: Y) + with Int_Us Ts_subset have "setFa u \ (\ Ss)" by auto + with u show "x \ ?rhs" by auto +qed + +end + +text \Subdistributivity for quotients via confluence\ + +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 \auto intro: reflpD transpD\) + 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 \ 'Fb \ bool" + fixes Rb :: "'Fb \ 'Fb \ bool" and Ea :: "'Fa \ 'Fa \ bool" and Eb :: "'Fb \ 'Fb \ bool" and Ec :: "'Fc \ 'Fc \ bool" @@ -20,12 +125,10 @@ and rel_Fac :: "('a \ 'c \ bool) \ 'Fa \ 'Fc \ bool" and set_Fab :: "'Fab \ ('a \ 'b) set" and set_Fbc :: "'Fbc \ ('b \ 'c) set" - assumes confluent: "confluentp R" - and retract1_ab: "\x y. R (\_Fabb x) y \ \z. Eab x z \ y = \_Fabb z" - and retract1_bc: "\x y. R (\_Fbcb x) y \ \z. Ebc x z \ y = \_Fbcb z" - and generated: "Eb \ equivclp R" - and set_ab: "\x y. Eab x y \ set_Fab x = set_Fab y" - and set_bc: "\x y. Ebc x y \ set_Fbc x = set_Fbc y" + assumes confluent: "confluentp Rb" + and retract1_ab: "\x y. Rb (\_Fabb x) y \ \z. Eab x z \ y = \_Fabb z \ set_Fab z \ set_Fab x" + and retract1_bc: "\x y. Rb (\_Fbcb x) y \ \z. Ebc x z \ y = \_Fbcb z \ set_Fbc z \ set_Fbc x" + and generated_b: "Eb \ equivclp Rb" and transp_a: "transp Ea" and transp_c: "transp Ec" and equivp_ab: "equivp Eab" @@ -37,10 +140,10 @@ and \_Fbcc_respect: "rel_fun Ebc Ec \_Fbcc \_Fbcc" begin -lemma retract_ab: "R\<^sup>*\<^sup>* (\_Fabb x) y \ \z. Eab x z \ y = \_Fabb z" +lemma retract_ab: "Rb\<^sup>*\<^sup>* (\_Fabb x) y \ \z. Eab x z \ y = \_Fabb z \ set_Fab z \ 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>* (\_Fbcb x) y \ \z. Ebc x z \ y = \_Fbcb z" +lemma retract_bc: "Rb\<^sup>*\<^sup>* (\_Fbcb x) y \ \z. Ebc x z \ y = \_Fbcb z \ set_Fbc z \ 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 \ Ea OO rel_Fac (A OO B) OO Ec" @@ -51,21 +154,19 @@ where xy: "set_Fab xy \ {(a, b). A a b}" "x = \_Faba xy" "y = \_Fabb xy" and y'z: "set_Fbc y'z \ {(a, b). B a b}" "y' = \_Fbcb y'z" "z = \_Fbcc y'z" by(auto simp add: in_rel_Fab in_rel_Fbc) - from \Eb y y'\ 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 \Eb y y'\ 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'" "\_Fabb xy' = u" - and retract2: "Ebc y'z y'z'" "\_Fbcb y'z' = u" + where retract1: "Eab xy xy'" "\_Fabb xy' = u" "set_Fab xy' \ set_Fab xy" + and retract2: "Ebc y'z y'z'" "\_Fbcb y'z' = u" "set_Fbc y'z' \ set_Fbc y'z" by(auto dest!: retract_ab retract_bc) from retract1(1) xy have "Ea x (\_Faba xy')" by(auto dest: \_Faba_respect[THEN rel_funD]) - moreover have "rel_Fab A (\_Faba xy') u" using xy retract1 - by(auto simp add: in_rel_Fab dest: set_ab) - moreover have "rel_Fbc B u (\_Fbcc y'z')" using y'z retract2 - by(auto simp add: in_rel_Fbc dest: set_bc) + moreover have "rel_Fab A (\_Faba xy') u" using xy retract1 by(auto simp add: in_rel_Fab) + moreover have "rel_Fbc B u (\_Fbcc y'z')" using y'z retract2 by(auto simp add: in_rel_Fbc) moreover have "Ec (\_Fbcc y'z') z" using retract2 y'z equivp_symp[OF equivp_bc] - by(auto dest: \_Fbcc_respect[THEN rel_funD]) + by(auto intro: \_Fbcc_respect[THEN rel_funD]) ultimately show "(Ea OO rel_Fac (A OO B) OO Ec) x z" unfolding rel_compp by blast qed diff -r d47c8a89c6a5 -r 180981b87929 src/HOL/Library/Dlist.thy --- a/src/HOL/Library/Dlist.thy Tue Mar 09 11:50:21 2021 +0100 +++ b/src/HOL/Library/Dlist.thy Tue Mar 09 14:20:27 2021 +0100 @@ -277,9 +277,9 @@ by(auto 4 4 simp add: Dlist.dlist_eq_def vimage2p_def intro: equivclp_trans converse_rtranclp_into_equivclp rtranclp_into_equivclp remdups_into_doubles) -qualified lemma factor_double_map: "double (map f xs) ys \ \zs. Dlist.dlist_eq xs zs \ ys = map f zs" +qualified lemma factor_double_map: "double (map f xs) ys \ \zs. Dlist.dlist_eq xs zs \ ys = map f zs \ set zs \ 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 \ set xs = set ys" by(simp add: Dlist.dlist_eq_def vimage2p_def)(metis set_remdups) @@ -294,7 +294,6 @@ dest: factor_double_map dlist_eq_into_doubles[THEN predicate2D] dlist_eq_set_eq simp add: list.in_rel list.rel_compp dlist_eq_map_respect Dlist.equivp_dlist_eq equivp_imp_transp) - lifting_update dlist.lifting lifting_forget dlist.lifting diff -r d47c8a89c6a5 -r 180981b87929 src/HOL/ROOT --- a/src/HOL/ROOT Tue Mar 09 11:50:21 2021 +0100 +++ b/src/HOL/ROOT Tue Mar 09 14:20:27 2021 +0100 @@ -875,7 +875,8 @@ Stream_Processor Cyclic_List Free_Idempotent_Monoid - LDL + Regex_ACI + Regex_ACIDZ TLList Misc_Codatatype Misc_Datatype