Email Gateway (Aug 18 2022 at 20:17): Email Gateway (Aug 18 2022 at 20:17):From: li yongjian <lyj238@gmail.com>
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
Email Gateway (Aug 18 2022 at 20:17):From: Christian Sternagel <c-sterna@jaist.ac.jp>
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
Last updated: Apr 19 2024 at 16:20 UTC