datatype 'a list =
Nil
| Cons 'a "'a list" (infixl "#" 65)
The symmetry of list is lost in above definition ,
which also cause the proof of list property extremely hard
If you look at the page 10 to 15 of
http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2011/doc/tutorial.pdf
you'll find the prove rev (rev x) = x is quite long ,
with the introduction of 5 lemma.
but if we defined list symmetrically , we don't need to define append function , and prove of rev(rev x ) = x is just a piece of cake.
following is the Isabelle code:
theory List1
imports Datatype
begin
datatype 'a list =
S 'a
| Cons "'a list" "'a list" (infixl "#" 65)
primrec rev :: "'a list \
"rev (S x ) = S x "
| "rev (x # y) = rev y # rev x "
theorem rev_rev [simp] : "rev (rev x ) = x "
apply (induct_tac x)
apply(auto)
done
Problem :
I cannot prove associative of # .
This makes me understand why lists are defined as cons a (list a) ,
because cons a ( cons b (cons c nil)) is the normal form.
and you can prove associative from the normal form.
while my way of defining list do not have normal form.
