--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Datatype_Examples/LDL.thy Sun Jan 19 07:50:35 2020 +0100
@@ -0,0 +1,339 @@
+theory LDL imports
+ "HOL-Library.Confluent_Quotient"
+begin
+
+datatype 'a rexp = Atom 'a | Alt "'a rexp" "'a rexp" | Conc "'a rexp" "'a rexp" | Star "'a rexp"
+
+inductive ACI (infix "~" 64) where
+ a1: "Alt (Alt r s) t ~ Alt r (Alt s t)"
+| a2: "Alt r (Alt s t) ~ Alt (Alt r s) t"
+| c: "Alt r s ~ Alt s r"
+| i: "r ~ Alt r r"
+| R: "r ~ r"
+| A: "r ~ r' \<Longrightarrow> s ~ s' \<Longrightarrow> Alt r s ~ Alt r' s'"
+| C: "r ~ r' \<Longrightarrow> s ~ s' \<Longrightarrow> Conc r s ~ Conc r' s'"
+| S: "r ~ r' \<Longrightarrow> Star r ~ Star r'"
+
+declare ACI.intros[intro]
+
+abbreviation ACIcl (infix "~~" 64) where "(~~) \<equiv> equivclp (~)"
+
+lemma eq_set_preserves_inter:
+ fixes eq set
+ assumes "\<And>r s. eq r s \<Longrightarrow> set r = set s" and "Ss \<noteq> {}"
+ shows "(\<Inter>As\<in>Ss. {(x, x'). eq x x'} `` {x. set x \<subseteq> As}) \<subseteq> {(x, x'). eq x x'} `` {x. set x \<subseteq> \<Inter> Ss}"
+ using assms by (auto simp: subset_eq) metis
+
+lemma ACI_map_respects:
+ fixes f :: "'a \<Rightarrow> 'b" and r s :: "'a rexp"
+ assumes "r ~ s"
+ shows "map_rexp f r ~ map_rexp f s"
+ using assms by (induct r s rule: ACI.induct) auto
+
+lemma ACIcl_map_respects:
+ fixes f :: "'a \<Rightarrow> 'b" and r s :: "'a rexp"
+ assumes "r ~~ s"
+ shows "map_rexp f r ~~ map_rexp f s"
+ using assms by (induct rule: equivclp_induct) (auto intro: ACI_map_respects equivclp_trans)
+
+lemma ACI_set_eq:
+ fixes r s :: "'a rexp"
+ assumes "r ~ s"
+ shows "set_rexp r = set_rexp s"
+ using assms by (induct r s rule: ACI.induct) auto
+
+lemma ACIcl_set_eq:
+ fixes r s :: "'a rexp"
+ assumes "r ~~ s"
+ shows "set_rexp r = set_rexp s"
+ using assms by (induct rule: equivclp_induct) (auto dest: ACI_set_eq)
+
+lemma Alt_eq_map_rexp_iff:
+ "Alt r s = map_rexp f x \<longleftrightarrow> (\<exists>r' s'. x = Alt r' s' \<and> map_rexp f r' = r \<and> map_rexp f s' = s)"
+ "map_rexp f x = Alt r s \<longleftrightarrow> (\<exists>r' s'. x = Alt r' s' \<and> map_rexp f r' = r \<and> map_rexp f s' = s)"
+ by (cases x; auto)+
+
+lemma Conc_eq_map_rexp_iff:
+ "Conc r s = map_rexp f x \<longleftrightarrow> (\<exists>r' s'. x = Conc r' s' \<and> map_rexp f r' = r \<and> map_rexp f s' = s)"
+ "map_rexp f x = Conc r s \<longleftrightarrow> (\<exists>r' s'. x = Conc r' s' \<and> map_rexp f r' = r \<and> map_rexp f s' = s)"
+ by (cases x; auto)+
+
+lemma Star_eq_map_rexp_iff:
+ "Star r = map_rexp f x \<longleftrightarrow> (\<exists>r'. x = Star r' \<and> map_rexp f r' = r)"
+ "map_rexp f x = Star r \<longleftrightarrow> (\<exists>r'. x = Star r' \<and> map_rexp f r' = r)"
+ by (cases x; auto)+
+
+lemma AA: "r ~~ r' \<Longrightarrow> s ~~ s' \<Longrightarrow> Alt r s ~~ Alt r' s'"
+proof (induct rule: equivclp_induct)
+ case base
+ then show ?case
+ by (induct rule: equivclp_induct) (auto elim!: equivclp_trans)
+next
+ case (step s t)
+ then show ?case
+ by (auto elim!: equivclp_trans)
+qed
+
+lemma AAA: "(~)\<^sup>*\<^sup>* r r' \<Longrightarrow> (~)\<^sup>*\<^sup>* s s' \<Longrightarrow> (~)\<^sup>*\<^sup>* (Alt r s) (Alt r' s')"
+proof (induct r r' rule: rtranclp.induct)
+ case (rtrancl_refl r)
+ then show ?case
+ by (induct s s' rule: rtranclp.induct)
+ (auto elim!: rtranclp.rtrancl_into_rtrancl)
+next
+ case (rtrancl_into_rtrancl a b c)
+ then show ?case
+ by (auto elim!: rtranclp.rtrancl_into_rtrancl)
+qed
+
+lemma CC: "r ~~ r' \<Longrightarrow> s ~~ s' \<Longrightarrow> Conc r s ~~ Conc r' s'"
+proof (induct rule: equivclp_induct)
+ case base
+ then show ?case
+ by (induct rule: equivclp_induct) (auto elim!: equivclp_trans)
+next
+ case (step s t)
+ then show ?case
+ by (auto elim!: equivclp_trans)
+qed
+
+lemma CCC: "(~)\<^sup>*\<^sup>* r r' \<Longrightarrow> (~)\<^sup>*\<^sup>* s s' \<Longrightarrow> (~)\<^sup>*\<^sup>* (Conc r s) (Conc r' s')"
+proof (induct r r' rule: rtranclp.induct)
+ case (rtrancl_refl r)
+ then show ?case
+ by (induct s s' rule: rtranclp.induct)
+ (auto elim!: rtranclp.rtrancl_into_rtrancl)
+next
+ case (rtrancl_into_rtrancl a b c)
+ then show ?case
+ by (auto elim!: rtranclp.rtrancl_into_rtrancl)
+qed
+
+lemma SS: "r ~~ r' \<Longrightarrow> Star r ~~ Star r'"
+proof (induct rule: equivclp_induct)
+ case (step s t)
+ then show ?case
+ by (auto elim!: equivclp_trans)
+qed auto
+
+lemma SSS: "(~)\<^sup>*\<^sup>* r r' \<Longrightarrow> (~)\<^sup>*\<^sup>* (Star r) (Star r')"
+proof (induct r r' rule: rtranclp.induct)
+ case (rtrancl_into_rtrancl a b c)
+ then show ?case
+ by (auto elim!: rtranclp.rtrancl_into_rtrancl)
+qed auto
+
+lemma map_rexp_ACI_inv: "map_rexp f x ~ y \<Longrightarrow> \<exists>z. x ~~ z \<and> y = map_rexp f z"
+proof (induct "map_rexp f x" y arbitrary: x rule: ACI.induct)
+ case (a1 r s t)
+ then obtain r' s' t' where "x = Alt (Alt r' s') t'"
+ "map_rexp f r' = r" "map_rexp f s' = s" "map_rexp f t' = t"
+ by (auto simp: Alt_eq_map_rexp_iff)
+ then show ?case
+ by (intro exI[of _ "Alt r' (Alt s' t')"]) auto
+next
+ case (a2 r s t)
+ then obtain r' s' t' where "x = Alt r' (Alt s' t')"
+ "map_rexp f r' = r" "map_rexp f s' = s" "map_rexp f t' = t"
+ by (auto simp: Alt_eq_map_rexp_iff)
+ then show ?case
+ by (intro exI[of _ "Alt (Alt r' s') t'"]) auto
+next
+ case (c r s)
+ then obtain r' s' where "x = Alt r' s'"
+ "map_rexp f r' = r" "map_rexp f s' = s"
+ by (auto simp: Alt_eq_map_rexp_iff)
+ then show ?case
+ by (intro exI[of _ "Alt s' r'"]) auto
+next
+ case (i r)
+ then show ?case
+ by (intro exI[of _ "Alt r r"]) auto
+next
+ case (R r)
+ then show ?case by (auto intro: exI[of _ r])
+next
+ case (A r rr s ss)
+ then obtain r' s' where "x = Alt r' s'"
+ "map_rexp f r' = r" "map_rexp f s' = s"
+ by (auto simp: Alt_eq_map_rexp_iff)
+ moreover from A(2)[OF this(2)[symmetric]] A(4)[OF this(3)[symmetric]] obtain rr' ss' where
+ "r' ~~ rr'" "rr = map_rexp f rr'" "s' ~~ ss'" "ss = map_rexp f ss'"
+ by blast
+ ultimately show ?case using A(1,3)
+ by (intro exI[of _ "Alt rr' ss'"]) (auto intro!: AA)
+next
+ case (C r rr s ss)
+ then obtain r' s' where "x = Conc r' s'"
+ "map_rexp f r' = r" "map_rexp f s' = s"
+ by (auto simp: Conc_eq_map_rexp_iff)
+ moreover from C(2)[OF this(2)[symmetric]] C(4)[OF this(3)[symmetric]] obtain rr' ss' where
+ "r' ~~ rr'" "rr = map_rexp f rr'" "s' ~~ ss'" "ss = map_rexp f ss'"
+ by blast
+ ultimately show ?case using C(1,3)
+ by (intro exI[of _ "Conc rr' ss'"]) (auto intro!: CC)
+next
+ case (S r rr)
+ then obtain r' where "x = Star r'" "map_rexp f r' = r"
+ by (auto simp: Star_eq_map_rexp_iff)
+ moreover from S(2)[OF this(2)[symmetric]] obtain rr' where "r' ~~ rr'" "rr = map_rexp f rr'"
+ by blast
+ ultimately show ?case
+ by (intro exI[of _ "Star rr'"]) (auto intro!: SS)
+qed
+
+lemma reflclp_ACI: "(~)\<^sup>=\<^sup>= = (~)"
+ unfolding fun_eq_iff
+ by auto
+
+lemma strong_confluentp_ACI: "strong_confluentp (~)"
+ apply (rule strong_confluentpI, unfold reflclp_ACI)
+ subgoal for x y z
+ proof (induct x y arbitrary: z rule: ACI.induct)
+ case (a1 r s t)
+ then show ?case
+ by (auto intro: AAA converse_rtranclp_into_rtranclp)
+ next
+ case (a2 r s t)
+ then show ?case
+ by (auto intro: AAA converse_rtranclp_into_rtranclp)
+ next
+ case (c r s)
+ then show ?case
+ by (cases rule: ACI.cases) (auto intro: AAA)
+ next
+ case (i r)
+ then show ?case
+ by (auto intro: AAA)
+ next
+ case (R r)
+ then show ?case
+ by auto
+ next
+ note A1 = ACI.A[OF _ R]
+ note A2 = ACI.A[OF R]
+ case (A r r' s s')
+ from A(5,1-4) show ?case
+ proof (cases rule: ACI.cases)
+ case inner: (a1 r'' s'')
+ from A(1,3) show ?thesis
+ unfolding inner
+ proof (elim ACI.cases[of _ r'], goal_cases Xa1 Xa2 XC XI XR XP XT XS)
+ case (Xa1 rr ss tt)
+ with A(3) show ?case
+ by (elim exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ A2[OF A2]], rotated])
+ (metis a1 a2 A1 r_into_rtranclp rtranclp.rtrancl_into_rtrancl)
+ next
+ case (Xa2 r s t)
+ then show ?case
+ by (elim exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ A2[OF A2]], rotated])
+ (metis a1 A1 r_into_rtranclp rtranclp.rtrancl_into_rtrancl)
+ next
+ case (XC r s)
+ then show ?case
+ by (elim exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ A2[OF A2]], rotated])
+ (metis a1 c A1 r_into_rtranclp rtranclp.rtrancl_into_rtrancl)
+ next
+ case (XI r)
+ then show ?case
+ apply (elim exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ ACI.A[OF i ACI.A[OF i]]], rotated])
+ apply hypsubst
+ apply (rule converse_rtranclp_into_rtranclp, rule a1)
+ apply (rule converse_rtranclp_into_rtranclp, rule a1)
+ apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a2)
+ apply (rule converse_rtranclp_into_rtranclp, rule A2, rule A1, rule c)
+ apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a1)
+ apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a1)
+ apply (rule converse_rtranclp_into_rtranclp, rule a2)
+ apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a2)
+ apply blast
+ done
+ qed auto
+ next
+ case inner: (a2 s'' t'')
+ with A(1,3) show ?thesis
+ unfolding inner
+ proof (elim ACI.cases[of _ s'], goal_cases Xa1 Xa2 XC XI XR XP XT XS)
+ case (Xa1 rr ss tt)
+ with A(3) show ?case
+ by (elim exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ A1[OF A1]], rotated])
+ (metis a2 A2 r_into_rtranclp rtranclp.rtrancl_into_rtrancl)
+ next
+ case (Xa2 r s t)
+ then show ?case
+ by (elim exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ A1[OF A1]], rotated])
+ (metis a1 a2 A2 r_into_rtranclp rtranclp.rtrancl_into_rtrancl)
+ next
+ case (XC r s)
+ then show ?case
+ by (elim exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ A1[OF A1]], rotated])
+ (metis a2 c A2 r_into_rtranclp rtranclp.rtrancl_into_rtrancl)
+ next
+ case (XI r)
+ then show ?case
+ apply (elim exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ ACI.A[OF ACI.A[OF _ i] i]], rotated])
+ apply hypsubst
+ apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a2)
+ apply (rule converse_rtranclp_into_rtranclp, rule A2, rule A1, rule c)
+ apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a1)
+ apply (rule converse_rtranclp_into_rtranclp, rule A2, rule A2, rule a1)
+ apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a2)
+ apply (rule converse_rtranclp_into_rtranclp, rule a2)
+ apply blast
+ done
+ qed auto
+ qed (auto 5 0 intro: AAA)
+ next
+ case (C r r' s s')
+ from C(5,1-4) show ?case
+ by (cases rule: ACI.cases) (auto 5 0 intro: CCC)
+ next
+ case (S r r')
+ from S(3,1,2) show ?case
+ by (cases rule: ACI.cases) (auto intro: SSS)
+ qed
+ done
+
+lemma confluent_quotient_ACI:
+ "confluent_quotient (~) (~~) (~~) (~~) (~~) (~~)
+ (map_rexp fst) (map_rexp snd) (map_rexp fst) (map_rexp snd)
+ rel_rexp rel_rexp rel_rexp set_rexp set_rexp"
+ by unfold_locales (auto dest: ACIcl_set_eq simp: rexp.in_rel rexp.rel_compp map_rexp_ACI_inv
+ intro: equivpI reflpI sympI transpI ACIcl_map_respects
+ strong_confluentp_imp_confluentp[OF strong_confluentp_ACI])
+
+inductive ACIEQ (infix "\<approx>" 64) where
+ a: "Alt (Alt r s) t \<approx> Alt r (Alt s t)"
+| c: "Alt r s \<approx> Alt s r"
+| i: "Alt r r \<approx> r"
+| A: "r \<approx> r' \<Longrightarrow> s \<approx> s' \<Longrightarrow> Alt r s \<approx> Alt r' s'"
+| C: "r \<approx> r' \<Longrightarrow> s \<approx> s' \<Longrightarrow> Conc r s \<approx> Conc r' s'"
+| S: "r \<approx> r' \<Longrightarrow> Star r \<approx> Star r'"
+| r: "r \<approx> r"
+| s: "r \<approx> s \<Longrightarrow> s \<approx> r"
+| t: "r \<approx> s \<Longrightarrow> s \<approx> t \<Longrightarrow> r \<approx> t"
+
+lemma ACIEQ_le_ACIcl: "r \<approx> s \<Longrightarrow> r ~~ s"
+ by (induct r s rule: ACIEQ.induct) (auto intro: AA CC SS equivclp_sym equivclp_trans)
+
+lemma ACI_le_ACIEQ: "r ~ s \<Longrightarrow> r \<approx> s"
+ by (induct r s rule: ACI.induct) (auto intro: ACIEQ.intros)
+
+lemma ACIcl_le_ACIEQ: "r ~~ s \<Longrightarrow> r \<approx> s"
+ by (induct rule: equivclp_induct) (auto 0 3 intro: ACIEQ.intros ACI_le_ACIEQ)
+
+lemma ACIEQ_alt: "(\<approx>) = (~~)"
+ by (simp add: ACIEQ_le_ACIcl ACIcl_le_ACIEQ antisym predicate2I)
+
+quotient_type 'a ACI_rexp = "'a rexp" / "(\<approx>)"
+ unfolding ACIEQ_alt by (auto intro!: equivpI reflpI sympI transpI)
+
+lift_bnf (no_warn_wits) 'a ACI_rexp
+ unfolding ACIEQ_alt
+ subgoal for A Q by (rule confluent_quotient.subdistributivity[OF confluent_quotient_ACI])
+ subgoal for Ss by (intro eq_set_preserves_inter[rotated] ACIcl_set_eq; auto)
+ done
+
+datatype ldl = Prop string | And ldl ldl | Not ldl | Match "ldl ACI_rexp"
+
+end
\ No newline at end of file