--- a/src/HOL/Relation.thy Tue Oct 08 17:26:31 2024 +0200
+++ b/src/HOL/Relation.thy Tue Oct 08 22:56:27 2024 +0200
@@ -969,11 +969,14 @@
subsubsection \<open>Composition\<close>
-inductive_set relcomp :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'c) set \<Rightarrow> ('a \<times> 'c) set" (infixr \<open>O\<close> 75)
+inductive_set relcomp :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'c) set \<Rightarrow> ('a \<times> 'c) set"
for r :: "('a \<times> 'b) set" and s :: "('b \<times> 'c) set"
- where relcompI [intro]: "(a, b) \<in> r \<Longrightarrow> (b, c) \<in> s \<Longrightarrow> (a, c) \<in> r O s"
+ where relcompI [intro]: "(a, b) \<in> r \<Longrightarrow> (b, c) \<in> s \<Longrightarrow> (a, c) \<in> relcomp r s"
-notation relcompp (infixr \<open>OO\<close> 75)
+open_bundle relcomp_syntax
+begin
+notation relcomp (infixr \<open>O\<close> 75) and relcompp (infixr \<open>OO\<close> 75)
+end
lemmas relcomppI = relcompp.intros
@@ -1074,15 +1077,19 @@
subsubsection \<open>Converse\<close>
-inductive_set converse :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'a) set" (\<open>(\<open>notation=\<open>postfix -1\<close>\<close>_\<inverse>)\<close> [1000] 999)
+inductive_set converse :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'a) set"
for r :: "('a \<times> 'b) set"
- where "(a, b) \<in> r \<Longrightarrow> (b, a) \<in> r\<inverse>"
+ where "(a, b) \<in> r \<Longrightarrow> (b, a) \<in> converse r"
-notation conversep (\<open>(\<open>notation=\<open>postfix -1-1\<close>\<close>_\<inverse>\<inverse>)\<close> [1000] 1000)
-
+open_bundle converse_syntax
+begin
+notation
+ converse (\<open>(\<open>notation=\<open>postfix -1\<close>\<close>_\<inverse>)\<close> [1000] 999) and
+ conversep (\<open>(\<open>notation=\<open>postfix -1-1\<close>\<close>_\<inverse>\<inverse>)\<close> [1000] 1000)
notation (ASCII)
converse (\<open>(\<open>notation=\<open>postfix -1\<close>\<close>_^-1)\<close> [1000] 999) and
conversep (\<open>(\<open>notation=\<open>postfix -1-1\<close>\<close>_^--1)\<close> [1000] 1000)
+end
lemma converseI [sym]: "(a, b) \<in> r \<Longrightarrow> (b, a) \<in> r\<inverse>"
by (fact converse.intros)