From: "Kruse, Kevin" <kevin.kruse@rwth-aachen.de>

Hi,

I’m trying to execute the following code snippet:

value "(∀n::nat. (enat n) ≤ (4::enat) ⟶ (n≤6))"

To do this, I use the following code abbreviation, which transforms the universal quantifier into an bounded set (for the non-infinite case):

lemma bounded_enat_exec [code_abbrev]:"(if ((x::enat)=∞) then (∀n. P n)

else ((∀n∈{0..(the_enat(x))}. P n))) = (∀n::nat. enat n ≤ (x::enat) ⟶ P n)"

sorry

However, I can’t explain the behavior of Isabelle: If I’m writing e.g. “False” in the first if branch (which should never be entered), the code will execute (but the lemma is not provable). If I’m writing what I stated above, the code won’t execute (Error, that nat is not enumerable).

Is there an explanation, why this happens? (… and hopefully a solution?)

All the best,

Kevin

From: Manuel Eberl <eberlm@in.tum.de>

Code generation happens statically, so if you cannot generate code for

the "False" branch, you cannot generate code for the whole thing. Even

if the branch can never be entered in practice.

What you can do is to use `Code.abort`

in the False branch. Basically,

`Code.abort s f`

is defined to be equal to `f ()`

but does not generate

code for f. Instead, whenever Code.abort is encountered at run time, you

get an exception with the message s.

For your case, this works:

lemma bounded_enat_exec [code_unfold]:

"(∀n::nat. enat n ≤ x ⟶ P n) =

(if (x::enat) = ∞ then Code.abort STR ''infinite'' (λ_. ∀n∈UNIV. P n)

else (∀n∈{0..the_enat x}. P n))"

by auto

definition P :: "enat ⇒ bool" where "P x = (∀n::nat. enat n ≤ x ⟶ x ^ 2

= x)"

value "P 1"

I'm a bit puzzled why it doesn't work with just "∀n. P n" instead of

"∀n∈UNIV. P n". Perhaps one of our code generation experts can comment

on this (I CC'ed Florian).

Manuel

smime.p7s

From: Kevin Kruse <kevin.kruse@rwth-aachen.de>

Hi Manuel, thanks for the explanation/hint!

All the best

Kevin

Last updated: Dec 05 2021 at 23:19 UTC