Email Gateway (Aug 19 2022 at 13:28): Email Gateway (Aug 19 2022 at 13:28):From: "Roger H." <s57076@hotmail.com>
Hi,
when i write
typedef larger_three = "{n :: nat. n > 3}"
definition b :: larger_three where
"b = Abs_larger_three 2"
i would like the compiler to reject this instantiation, cause 2 is not larger then 3.
My best solution for this is that the compiler behaves like it accepts it, but secretly makes it undefined:
typedef larger_three = "{n :: nat. n > 3}"
sorry
consts
constructNr :: "nat => larger_three"
defs
constructNr_def: "constructNr k ≡ if k > 3 then Abs_larger_three k else undefined"
definition b :: larger_three where
"b = constructNr 2"
lemma "b = undefined"
by (simp add: b_def constructNr_def)
I would like that the compiler immediately catches this as error, and not behaving as if accepting it and throwing it to undefined.
Can you help me?
Thank you
Email Gateway (Aug 19 2022 at 13:28):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Roger,
Higher-order logic is a logic of total functions, i.e., if you apply a function to an
argument, and the argument has the type that the function expects, then the application is
type-correct. 2 is a natural number and Abs_larger_three is a function from nat to
larger_three, so the application is type-correct. There's nothing you can do about this on
the level of the logic. If you want that, then you have to use some other logic, Agda and
Coq can express these kinds of things. But then you have to prove for every application of
Abs_larger_three that the argument is indeed greater than 3. For literal numbers, this may
be easy, but for "Abs_larger_three (some complicated expression)", you also have to prove
that "some complicated expression" is larger than 3.
Of course, you could try to tweak Isabelle's parser such that whenever Abs_larger_three is
applied to a literal numeral, it checks that the number is really greater than 3. But
apart from causing a lot of work, this can be fooled easily, e.g., "Abs_larger_three (id 2)".
You have already found the canonical solution of defining a "smart" function that tries to
somehow make some sense of unexpected input (although undefined is hardly any better than
the non-specification for Abs_larger_three).
Andreas
Last updated: Apr 16 2024 at 12:28 UTC