Re: [isabelle] termination on higher-oreder recursion function



Dear Li Yongjian,

your function was already proved terminating (automatically) by Isabelle/HOL's function package. Note, your usage of the "fun" command, which tries an automatic termination proof, as compared to the "function" command for manual termination proofs. Your usage of "termination proof" is superfluous, just remove that line.

cheers

chris

On 06/29/2012 07:54 PM, li yongjian wrote:
theory bdd imports "Main"
begin
datatype form =  Var nat | AndList "form list" | Xnor form form | BNot form


definition xnor :: "bool \<Rightarrow>bool \<Rightarrow> bool" where
   "xnor x y \<equiv> (x \<and>  y) \<or> ( ~ x \<and>~ y)"

fun evalf :: "(nat \<Rightarrow> bool) \<Rightarrow> form
\<Rightarrow> bool" where
   "evalf e (Var i) = e i"
| "evalf e (AndList L) = foldl conj True (map (evalf e)  L)"
| "evalf e (Xnor f1 f2) = xnor (evalf e f1) (evalf e f2)"
|"evalf e (BNot f) = (~ (evalf e f)) "
termination proof







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