Email Gateway (Mar 24 2022 at 09:40): Email Gateway (Mar 24 2022 at 09:40):From: Michael Stampone <michaelstampone@gmail.com>
I would like to understand how I can evaluate "stuff.P." Please help if you
have the knowledge. I've been trying to figure this out for several hours.
I realize that one clunky solution is to basically make the same argument
for P over and over, but I would much rather instantiate than duplicate
code. I tried every combination of "lemmas [code]" and "lemmas
[code_unfold]" I could think of, but I don't really know what I'm doing
when it comes to code generation. Please help, this is really bothering me!
theory Scratch imports Main begin
locale foo =
fixes f :: "nat ⇒ nat"
assumes a1: "f x < f (Suc x)"
begin
function P :: "nat ⇒ nat ⇒ bool" where
"P x y = (if f x < y then P (Suc x) y else f x = y)"
apply auto
done
termination P
apply (relation "measure (λ(x, y). y - f x)")
apply auto
apply (simp add: a1 diff_less_mono2)
done
end
fun g :: "nat ⇒ nat" where "g x = 2 * x"
interpretation stuff: foo "g"
apply unfold_locales
apply auto
done
value "stuff.P 0 0"
end
Email Gateway (Mar 24 2022 at 12:06):From: Michael Stampone <michaelstampone@gmail.com>
I just wanted to confirm that Section 8.4 from the code gen manual solves
my problem. I just evaluated "stuff.P" and couldn't be happier.
Email Gateway (Mar 24 2022 at 12:06):From: Michael Stampone <michaelstampone@gmail.com>
Peter Gammie,
Thank you so much for the quick response! Not expected, but appreciated!
I'm pretty sure that section 8.4 from the code gen manual is exactly what I
needed. I wouldn't have found that so quickly without your help. This
mattered a great deal to me. I sometimes get truly distraught when I can't
figure something out. Can I PayPal you $20? Feel free to message my
personal email with your username, email, or whatever.
Last updated: Jul 15 2022 at 23:21 UTC