Email Gateway (Aug 18 2022 at 10:28): Email Gateway (Aug 18 2022 at 10:28):From: John Ridgway <john@jacelridge.com>
I have a problem with simplification in Isabelle/Isar with HOL.
Specifically, given the following, the attempt to apply(simp) goes
into never-never-land. Can anyone explain to me why, or tell me how
to fix it?
Peace
theory temp = Main:
consts
fib :: "(nat * nat) set";
inductive fib
intros
"(0, 1) : fib"
"(1, 1) : fib"
"[| (n, fn) : fib; (n+1, fnp1) : fib |] ==> (n+2, fn+fnp1) : fib";
lemma temp: "
[|
(n, fn) : fib;
! fn'.
((n, fn') : fib -->
fn' = fn);
fn2 = fn + 1
|]
==>
epsilon2 = epsilon_90";
apply(simp);
Email Gateway (Aug 18 2022 at 10:28):From: Alexander Krauss <krauss@in.tum.de>
John,
Specifically, given the following, the attempt to apply(simp) goes into
never-never-land. Can anyone explain to me why, or tell me how to fix it?
[...]
lemma temp: "
[|
(n, fn) : fib;
! fn'.
((n, fn') : fib -->
fn' = fn);
fn2 = fn + 1
|]
==>
epsilon2 = epsilon_90";apply(simp);
From the trace, it seems that the following happens:
Premise 2 is turned around (probably in order not to match
everything), resulting in the conditional rewrite rule
"(n, ?fn') : fib ==> fn == ?fn'"
That rule matches the "fn" in premise 3, and since premise 1 matches
the condition, "?fn'" is instantiated to "fn", hence "fn" gets rewritten
to itself, which is then repeated.
To avoid this situation, you can either change your theorem statement,
or use one of the modifiers "no_asm", "no_asm_use" or "no_asm_simp".
They are explained in Section 3.1.5. in the tutorial.
Hope this helps,
Alex
Last updated: May 03 2024 at 04:19 UTC