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