1) Is there a datatype for characters in isabelle? I would like to prove stuff about a real world grammar for a language of characters.
Yes, char, in List.
2) This is really basic but giving me a headache. How can I make an optional tuple? I tried "('a, 'a) option" but that didnt seem to work properly.
You are using Haskell syntax. Try "('a * 'a) option". Tobias