Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] [Isabelle 2019-RC0] explore/sketch

view this post on Zulip Email Gateway (Aug 22 2022 at 19:30):

From: Dominique Unruh <unruh@ut.ee>
Hi,

explore/sketch fail in certain situations when a variable with the same
name occurs quantified in the goal, and free in the lemma to be proven
(as often happens when applying transfer).

The following example shows this:

theory Scratch
  imports Main "HOL-ex.Sketch_and_Explore" "HOL-Library.Multiset"
begin

lemma "count M undefined > 0"
  apply transfer
explore - (* Fails. *)

lemma "count M undefined > 0"
  apply (transfer, rename_tac M')
explore - (* Works *)

view this post on Zulip Email Gateway (Aug 22 2022 at 19:43):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Dominique,

thanks for reporting this.

The upcoming RC2 shall contain
http://isabelle.in.tum.de/repos/isabelle/rev/129757af1096 which aims to
simulate the eigen context for a printed Isar statement properly.

This is one of the many lingering issues in this PoC implementation.

Cheers,
Florian
signature.asc

view this post on Zulip Email Gateway (Aug 22 2022 at 19:46):

From: Makarius <makarius@sketis.net>
This is actually part of current Isabelle2019-RC1.

Makarius

Last updated: Nov 21 2024 at 12:39 UTC