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



You have to make up your mind if the function is called simpBp or simpBP.

Tobias

Am 27/07/2012 09:23, schrieb li yongjian:
> 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.