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.



On 06/29/2012 07:54 PM, li yongjian wrote:
theory bdd imports "Main"
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.