--- a/src/HOL/Datatype_Examples/Derivation_Trees/Parallel_Composition.thy Tue Oct 08 15:44:11 2024 +0200
+++ b/src/HOL/Datatype_Examples/Derivation_Trees/Parallel_Composition.thy Tue Oct 08 15:44:52 2024 +0200
@@ -11,17 +11,15 @@
imports DTree
begin
-no_notation plus_class.plus (infixl \<open>+\<close> 65)
-
-consts Nplus :: "N \<Rightarrow> N \<Rightarrow> N" (infixl \<open>+\<close> 60)
+consts Nplus :: "N \<Rightarrow> N \<Rightarrow> N" (infixl \<open>\<^bold>+\<close> 60)
axiomatization where
- Nplus_comm: "(a::N) + b = b + (a::N)"
-and Nplus_assoc: "((a::N) + b) + c = a + (b + c)"
+ Nplus_comm: "(a::N) \<^bold>+ b = b \<^bold>+ (a::N)"
+and Nplus_assoc: "((a::N) \<^bold>+ b) \<^bold>+ c = a \<^bold>+ (b \<^bold>+ c)"
subsection\<open>Corecursive Definition of Parallel Composition\<close>
-fun par_r where "par_r (tr1,tr2) = root tr1 + root tr2"
+fun par_r where "par_r (tr1,tr2) = root tr1 \<^bold>+ root tr2"
fun par_c where
"par_c (tr1,tr2) =
Inl ` (Inl -` (cont tr1 \<union> cont tr2)) \<union>
@@ -40,7 +38,7 @@
apply(intro finite_imageI finite_cartesian_product finite_vimageI)
using finite_cont by auto
-lemma root_par: "root (tr1 \<parallel> tr2) = root tr1 + root tr2"
+lemma root_par: "root (tr1 \<parallel> tr2) = root tr1 \<^bold>+ root tr2"
using unfold(1)[of par_r par_c "(tr1,tr2)"] unfolding par_def par_r.simps by simp
lemma cont_par: