Email Gateway (Aug 18 2022 at 19:16): Email Gateway (Aug 18 2022 at 19:16):From: Christian Sternagel <c-sterna@jaist.ac.jp>
Hi there,
recently I experienced some strange behavior (Isabelle2011-1 in jedit)
which is reproduced in the small example below:
notepad begin
fix l le B
interpret preorder l le sorry
moreover have "B" sorry
ultimately have "class.preorder l le & B" by blast
end
in the "ultimately" line but before "by blast", the current state looks
as follows:
proof (prove): step 8
using this:
class.preorder l le
B
goal (1 subgoal):
1. class.preorder l le & B
but blast (and auto, .., simp, force, best, ...) does not solve the
goal. If I write instead
notepad begin
fix l le B
interpret preorder l le sorry
have "B" sorry
from class.preorder l le and B
have "class.preorder l le & B" by blast
end
everything works fine. The corresponding state is
proof (prove): step 7
using this:
class.preorder l le
B
goal (1 subgoal):
1. class.preorder l le ∧ B
So the only immediately conceivable difference is "step 7" instead of
"step 8".
cheers
chris
Email Gateway (Aug 18 2022 at 19:16):From: Brian Huffman <huffman@in.tum.de>
At this point in your proof script, try
ML_val {* Thm.concl_of @{thm this} *}
and you will see that there is a constant "prop :: prop => prop"
wrapped around the conclusion of this fact, outside the "Trueprop".
Then try
ML_val {* Thm.concl_of @{thm class.preorder l le} *}
And you will see that no "prop" constant is there.
Perhaps Makarius can say more about what this "prop" constant is for,
and why it appears in the theorem exported by the interpret command.
Email Gateway (Aug 18 2022 at 19:18):From: Makarius <makarius@sketis.net>
Locale interpretation essentially needs to discharge "hyps" from local
theorems, by establishing a suitable "witness". To preserve the literal
structure of the same, without the usual normalization of regular results,
the internal goal statement is protected via the funny prop constant.
(This device is explained in the Isar implementation manual section 2.3.2;
it is useful for extraordinary situations in ML, but should normally never
be encountered in end-user proof documents.)
The confusion above stems from the accident that 'interpret' exposes this
internal result to the Isar proof context via "this". (I have gone
through all reachable Isabelle example and found a few more such
misunderstandings, where forward chaining was done after 'interpret'
without any effect, and eliminated them.)
Note that after "interpret foobar" the context knows about the fact
"foobar_axioms" in the proven instance; the same works for any other
imported substructures, not just part that was visible in the auxiliary
goal state.
Makarius
Last updated: Apr 19 2024 at 01:05 UTC