[isabelle] HOLCF case syntax



Dear all,

I just updated

  https://sourceforge.net/projects/holcf-prelude/

(something similar to the Haskell Prelude based on HOLCF) to Isabelle2014.

As already reported earlier

  https://sourceforge.net/projects/holcf-prelude/

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 mean.

Any thoughts?

cheers

chris
theory Test
imports "~~/src/HOL/HOLCF/HOLCF"
begin

fun len
where
  "len xs = (case xs of [] \<Rightarrow> 0 | _ # xs \<Rightarrow> Suc (len xs))"

no_notation
  List.Nil ("[]")

domain 'a list ("[_]") =
  Nil ("[]") |
  Cons (lazy head :: 'a) (lazy tail :: "['a]") (infixr ":" 65)

fixrec bla
where
  "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]"
where
  "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))"

end



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.