Email Gateway (Aug 23 2022 at 09:27): Email Gateway (Aug 23 2022 at 09:27):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: Nov 21 2024 at 12:39 UTC