Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Unbound schematic variable

Email Gateway (Aug 22 2022 at 15:14):

From: Sven Schneider <sven.schneider.pub@gmx.de>
Hi all,

I have some old 2014 theory files that I might want to update to the
current version.
Apparently something has changed and I am unable to find anything in the
NEWS about it.
Is there a minimal workaround that requires minimal effort?
There are very many instances of this sort in the proofs...

Best regards

example
==========================
theory Test
imports
Main
begin

lemma TEST: "foo"
apply(subgoal_tac "?X")

==========================

output
=============
"Unbound schematic variable: ?X"
=============

Email Gateway (Aug 22 2022 at 15:14):

From: Makarius <makarius@sketis.net>
The proper way to do it is via "eigen-context" like this:

apply (subgoal_tac "X" for X)

Unbound schematic variables violate the Isabelle/Isar context
discipline. The more tools are properly localized, the less they can
sneak into proof texts.

Here is also a relavant NEWS entry from Isabelle2015:

• Proof methods with explicit instantiation ("rule_tac", "subgoal_tac"
  etc.) allow an optional context of local variables ('for' declaration):
  these variables become schematic in the instantiated theorem; this
  behaviour is analogous to 'for' in attributes "where" and "of".
  Configuration option rule_insts_schematic (default false) controls use
  of schematic variables outside the context. Minor INCOMPATIBILITY,
  declare rule_insts_schematic = true temporarily and update to use local
  variable declarations or dummy patterns instead.

  Makarius

Last updated: Nov 21 2024 at 12:39 UTC