Email Gateway (Aug 19 2022 at 07:57): Email Gateway (Aug 19 2022 at 07:57):From: li yongjian <lyj238@gmail.com>
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
Last updated: Apr 23 2024 at 12:29 UTC