Gergely Buday (Sep 25 2023 at 16:09): Gergely Buday (Sep 25 2023 at 16:09):It is clear that fun is for functions whose termination or totality is automatically proved.
For function-defined functions, the user should provide the measure function and the proof.
But: is there a difference between proving properties of fun and function functions?
It seems that Isabelle produces the same generated theorems: .cases, .elims, .psimps, .induct, .pelims, .pinduct, .simps .
Is there something special about function-defined functions?
Yutaka Nagashima (Sep 25 2023 at 22:06):I thought the fun keyword does not derive psimps?
Wolfgang Jeltsch (Sep 25 2023 at 22:21):That’s what I thought too. After all, you can’t have partially defined functions with fun, can you?
Manuel Eberl (Sep 26 2023 at 10:34):As far as I know, fun is function with an automatic termination proof, with an automatically derived termination measure.
The psimps, pinduct, pelims rules are derived by the function command. The termination command, after the termination proof is completed, then discharges the termination assumption from these partial rules and registers them as simps, induct, elims and hides the psimps, pinduct, pelims rules.
Manuel Eberl (Sep 26 2023 at 10:35):Since fun does function + termination, you don't ever see the psimps etc. if you use fun.
Gergely Buday (Sep 26 2023 at 12:44):Thanks, @Yutaka Nagashima @Wolfgang Jeltsch and @Manuel Eberl
Lukas Stevens (Sep 26 2023 at 13:10):This is explained in the function manual BTW.
20230926_15h10m12s_grim.png
Gergely Buday (Sep 28 2023 at 15:58):@Lukas Stevens If I was not clear: I am not interested in the termination of function-defined functions, but proving other properties of such a function.
Last updated: Nov 07 2025 at 16:23 UTC