[isabelle] "Illegal equation head" ---an error in func definition



Dear Isabelle experts:
     I meet a problem in function definition as follows, which I cannot solve
 Can anybody solve it?
    In fact, the code defintion is corresponding to a fragment of  FL
code, which is a function programming.

   *** Illegal equation head. Expected "simpBp"
*** \<And>simpBP f h l. simpBP (BNot f) h l = simpBP f l h
*** At command "fun" (line 13 of "/media/3012-1D97/bdd/mybdd.thy")

The proof script
eory bdd imports "Main"
begin
datatype form =  Var nat | AndList "form list" | Xnor form form | BNot
form | T |F

type_synonym varSet="nat list"
type_synonym triple="form\<times>form\<times>form"
type_synonym tripleSet="triple list"

fun simpBp ::"form \<Rightarrow> form\<Rightarrow>form\<Rightarrow>tripleSet"
  where
"simpBp (Var n)  h l   =[(Var n,h,l)]"
|"simpBP  (BNot f) h l=simpBP f  l h"

--------------------------------------------------------------------------------------------
Note that for the case (BNot f), the right is f, the order should
decrease, but Isabelle cannot accept such a definition?

best regards!
lyj





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