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