Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] obtain command failure

Email Gateway (Aug 18 2022 at 12:26):

From: Makarius <makarius@sketis.net>
Since inx is polymorphic, special care is required when writing closed
expression without any syntactic correlation via fixed variables -- bound
variables (like e, x) and constants (like inx) do not propagate type
constraints.

It works with explicit type constraints, e.g. like this:

lemma "~ (EX e :: 'a * nat. e : inx)"
proof
assume "EX x :: 'a * nat. x : inx"
then obtain x :: "'a * nat" where "x : inx" ..
oops

BTW, you can use pattern comprehension when defining the "inx" set.
E.g. like this:

definition "inx = {(s :: 'a, n :: nat). True}"

Makarius

Last updated: May 03 2024 at 08:18 UTC