Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Unexpected behaviour of lemmas x = ... for A


view this post on Zulip Email Gateway (Jul 29 2020 at 12:02):

From: Peter Lammich <lammich@in.tum.de>
Hello List.

I ran into the following unexpected (for me) behaviour:

consts f :: "'a ⇒ bool"

lemmas foo1 = conjI[where P="f A", OF _ conjI[where Q="f A"]] for A

Yields: ⟦f ?A; ?P; f ?Aa⟧ ⟹ f ?A ∧ ?P ∧ f ?Aa
Expected: ⟦f ?A; ?P; f ?A⟧ ⟹ f ?A ∧ ?P ∧ f ?A

(Note the duplication of ?A into ?A and ?Aa)

Question to the experts:
Is this behaviour intentional? If yes, why does it differ from what
context fixes A would do (see below)?

Analysis:
The "for" fixes the variable A, but not its type, which remains
schematic. As soon as an operation changes schematic names, like, e.g.,
the incr_indexes in OF, we have two variables A, with the same name
but different types. The export that happens afterwards will
disambiguate the names.

Workarounds:
Possibility 1: Specify the type of A completely.
Wildcards cannot be used!

lemmas foo3 = conjI[where P="f A", OF _ conjI[where Q="f A"]] for A
:: 'a
(* ⟦f ?A; ?P; f ?A⟧ ⟹ f ?A ∧ ?P ∧ f ?A *)

Wildcards don't work:
lemmas foo2 = conjI[where P="f A", OF _ conjI[where Q="f A"]] for A
:: "'a * _"
(* ⟦f ?A; ?P; f ?Aa⟧ ⟹ f ?A ∧ ?P ∧ f ?Aa *)

Possibility 2: Use context fixes:

context fixes A begin
lemmas foo4 = conjI[where P="f A", OF _ conjI[where Q="f A"]]
(* ⟦f A; ?P; f A⟧ ⟹ f A ∧ ?P ∧ f A *)
end
thm foo4
(* ⟦f ?A; ?P; f ?A⟧ ⟹ f ?A ∧ ?P ∧ f ?A *)

Best
Peter


Last updated: Sep 25 2021 at 09:17 UTC