title: Isabelle: generic datatypes and equivalence
body: <p>I'm just starting making my type generic in Isabelle now i get funny error messages once i start using parenthesis.</p>
  
  <pre><code>theory Scratch
  imports Main
  begin
  no_notation plus (infixl "+" 65)
  
  datatype typeA = aa
  datatype typeB = bb
  datatype ('a, 'b) genericType = cc | 
                                  plus 'a 'b (infixr "+" 35)
  
  lemma test1 : "x + y ≡ x + y"
  by auto
  lemma test2 : "x + y + z ≡ x + y + z"
  by auto
  lemma test3 : "x + (y + z) ≡ x + y + z"
  by auto
  lemma test4 : "(x + y) + z ≡ x + y + z"
  lemma test5 : "(aa + aa) + aa ≡ aa + aa + aa"
  lemma test6 : "(cc + cc) + cc ≡ cc + cc + cc"
  lemma test7 : "(cc + aa) + cc ≡ cc + aa + cc"
  lemma test8 : "(aa + cc) + cc ≡ cc + aa + cc"
  </code></pre>
  
  <p>Everything is fine with test1-3, but test 4 and 5 result in this error: </p>
  
  <pre><code>Type unification failed: Occurs check!
  
  Type error in application: incompatible operand type
  
  Operator:  op ≡ ((x + y) + z) :: ((??'a, ??'b) genericType, ??'c) genericType ⇒ prop
  Operand:   x + y + z :: (??'a, (??'b, ??'c) genericType) genericType
  </code></pre>
  
  <p>and respectivly:</p>
  
  <pre><code>Type unification failed: Clash of types "typeA" and "(_, _) genericType"
  
  Type error in application: incompatible operand type
  
  Operator:  op ≡ ((aa + aa) + aa) :: ((typeA, typeA) genericType, typeA) genericType ⇒ prop
  Operand:   aa + aa + aa :: (typeA, (typeA, typeA) genericType) genericType
  </code></pre>
  
  <p>test6 and weirdly test7/8 are fine again. Any more replacement of "cc" with "aa" leads to the same problem though.</p>
  
  <p>PS: can i somehow specifiy the types 'a and 'b?</p>