[isabelle] termination on higher-oreder recursion function



Dear all:
  I meet a problem on  termination of a higher-oreder recursion
function as follows:
Despite my efforts of reading the material on function definition
problems in the
doc directory of Isabelle,  I still cannot prove the following goals
on the termination of the
function evalf .
 Who can help me?

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.