[isabelle] HOLCF case syntax
I just updated
(something similar to the Haskell Prelude based on HOLCF) to Isabelle2014.
As already reported earlier
I had some trouble adapting fixrecs involving case syntax.
This time it kind of worked. Only kind of, since it seems that it makes
a difference whether dummy variables ("_") are used in patterns of case
branches or not (without "_" everything seems to be fine).
Please find a small theory file attached that gives an example of what I
"len xs = (case xs of  \<Rightarrow> 0 | _ # xs \<Rightarrow> Suc (len xs))"
domain 'a list ("[_]") =
Nil ("") |
Cons (lazy head :: 'a) (lazy tail :: "['a]") (infixr ":" 65)
"bla\<cdot>xs\<cdot>y = (case xs of  \<Rightarrow> y | x : xs \<Rightarrow> y)"
fixrec scanr :: "('a \<rightarrow> 'b \<rightarrow> 'b) \<rightarrow> 'b \<rightarrow> ['a] \<rightarrow> ['b]"
"scanr\<cdot>f\<cdot>q0\<cdot> = q0:" |
"scanr\<cdot>f\<cdot>q0\<cdot>(x : xs) = (
let qs = scanr\<cdot>f\<cdot>q0\<cdot>xs in
(case qs of
 \<Rightarrow> \<bottom>
| q : qs' \<Rightarrow> f\<cdot>x\<cdot>q : qs))"
This archive was generated by a fusion of
Pipermail (Mailman edition) and