Email Gateway (Aug 19 2022 at 13:02): Email Gateway (Aug 19 2022 at 13:02):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Was probably already the same with prior version, still a quick comment on
document generation.
When a proof contains a “sorry” and the proof is closed with an “oops”,
that's not really cheating, so may be building a document from a theory
containing not so real cheating, could terminate successfully without a
“Cheating requires quick_and_dirty mode!”.
Email Gateway (Aug 19 2022 at 13:02):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
I don't know if it's on purpose or not, at least surprising, an example of
what may be returned by Sledgehammer:
proof -
have "t1 ≅ t2 ⟶ ω (t1 ∖ c) ≅ ω (t2 ∖ c)"
using eqt rec by auto
qed
There is no show/thus.
With this case, the goal was:
"¬ t1 ≅ t2 ∨ ω (t1 ∖ c) ≅ ω (t2 ∖ c)"
I just added
thus "¬ t1 ≅ t2 ∨ ω (t1 ∖ c) ≅ ω (t2 ∖ c)" by simp
… which it forgets.
The similar happens from time to time.
Email Gateway (Aug 19 2022 at 13:02):From: Peter Lammich <lammich@in.tum.de>
On Mo, 2013-12-16 at 04:45 +0100, Yannick Duchêne (Hibou57) wrote:
Le Fri, 06 Dec 2013 12:00:51 +0100, Makarius
<makarius@sketis.net> a écrit:Isabelle2013-2 is now available.
[…]
Was probably already the same with prior version, still a quick comment on
document generation.When a proof contains a “sorry” and the proof is closed with an “oops”,
that's not really cheating, so may be building a document from a theory
containing not so real cheating, could terminate successfully without a
“Cheating requires quick_and_dirty mode!”.
I guess that this is technically nearly impossible, as "sorry" already
"proves" theorems in the kernel, that may escape the proof before you
abort it with oops.
>
Email Gateway (Aug 19 2022 at 13:05):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
I found what is I believe an issue with Sledgehammer and its “Isar proofs”
option.
In the test theory below (also as attached file), if I move the caret next
to “using r1 r2” then in the Sledgehammer pan, check “Isar proofs”, then
click “Apply”, something strange happens: if first run up to displaying a
proof, then something appears in the output pan saying “ENTER MATCH”, then
the content in the Sledgehammer pan disappears then the content of the
output pan is back to what is was just before it displayed “ENTER MATCH”
and Sledgehammer continue running and cannot be stopped with “Cancel”.
The issue does not occur if “Isar proofs” is not checked.
Test.thy:
theory Test
imports BNF
begin
declare [[rule_trace]]
type_synonym 'a pp = "['a, 'a] ⇒ bool"
inductive ppinduct :: "'a pp ⇒ 'a list pp" where
r1: "ppinduct _ [] []"
| r2: "⟦f h1 h2; ppinduct f t1 t2⟧ ⟹ ppinduct f (h1 # t1) (h2 # t2)"
lemma "ppinduct f (h # t) [] ⟹ False" using r1 r2
end
Test.thy
Email Gateway (Aug 19 2022 at 13:05):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
By the way, I've made an error as I forget the “for” part in the sample
case which I noticed it in the real case when I failed with a proof. I
fixed the sample in the while to see if it behave the same, and it
differs. With this case, the issue does not occur. The original case is
still an issue, as it should behave correctly in all circumstances, even
with definitions not written as intended.
Test_2.thy (also as attached file):
theory Test_2
imports BNF
begin
declare [[rule_trace]]
type_synonym 'a pp = "['a, 'a] ⇒ bool"
inductive ppinduct :: "'a pp ⇒ 'a list pp" for f where
r1: "ppinduct f [] []"
| r2: "⟦f h1 h2; ppinduct f t1 t2⟧ ⟹ ppinduct f (h1 # t1) (h2 # t2)"
lemma "ppinduct f (h # t) [] ⟹ False" using r1 r2
end
Test_2.thy
Email Gateway (Aug 19 2022 at 13:15):From: Makarius <makarius@sketis.net>
Isabelle2013-2 is now available.
This version supersedes Isabelle2013-1, which in turn consolidated
Isabelle2013 and introduced numerous improvements. See the NEWS file
in the distribution for more details. Some highlights are:
Significantly improved Isabelle/jEdit Prover IDE.
Consolidated multi-platform support: Linux, Windows, Mac OS X.
Added and updated manuals: datatypes, implementation, isar-ref, jedit.
New Spec_Check tool: Quickcheck for Isabelle/ML.
HOL library enhancements: Complex_Main, HOL-Library,
HOL-Multivariate_Analysis.
HOL tool enhancements: Codegenerator, Function, Lifting, Transfer,
Nitpick, Sledgehammer.
HOL-BNF: significantly improved BNF-based (co)datatype package.
You may get Isabelle2013-2 from the following mirror sites:
Cambridge (UK) http://www.cl.cam.ac.uk/research/hvg/Isabelle/
Munich (Germany) http://isabelle.in.tum.de/
Sydney (Australia) http://mirror.cse.unsw.edu.au/pub/isabelle/
Email Gateway (Aug 19 2022 at 13:15):From: Makarius <makarius@sketis.net>
Thanks to everybody who participated in the second round of testing.
Don't forget to dispose your local copies of any "RC" versions, and update
to the proper release.
Makarius
Last updated: Apr 24 2024 at 01:07 UTC