# HG changeset patch # User wenzelm # Date 1728395092 -7200 # Node ID 9efe46ef839a960690ad34de6c0cb347cd907142 # Parent 5b201b24d99bec339f336b5c86b751eb4d81b2a9 avoid syntax clashes; diff -r 5b201b24d99b -r 9efe46ef839a src/HOL/Datatype_Examples/Derivation_Trees/Parallel_Composition.thy --- 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 \+\ 65) - -consts Nplus :: "N \ N \ N" (infixl \+\ 60) +consts Nplus :: "N \ N \ N" (infixl \\<^bold>+\ 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\Corecursive Definition of Parallel Composition\ -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 \ cont tr2)) \ @@ -40,7 +38,7 @@ apply(intro finite_imageI finite_cartesian_product finite_vimageI) using finite_cont by auto -lemma root_par: "root (tr1 \ tr2) = root tr1 + root tr2" +lemma root_par: "root (tr1 \ 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: