Email Gateway (Aug 19 2022 at 13:27): Email Gateway (Aug 19 2022 at 13:27):From: "Roger H." <s57076@hotmail.com>
Hi,
i want to create a datatype
typedef less_three = {n€N. n<3}
Now, when we write
definition my_number :: nat, where "my_number = 0.5"
then we get an error "0.5 is not a nat"
Now i want to get the same error with the type above less_three, meaning if i write
definition other_number :: three, where "other_number = 4" (*)
then i want to get an error that "4 is not a less_three" (cause its larger)
so basically an automatic type warning.
What bothers me is that the equation (*) above is just accepted by isabelle although its bad typed.
I have an idea what Rep and Abs do from the tutorial so i kinda understand, but still do you think u can give me an idea how to make the equation (*) produce an error?
Thank you!
Email Gateway (Aug 19 2022 at 13:27):From: Johannes Hölzl <hoelzl@in.tum.de>
Hi Roger,
Am Mittwoch, den 08.01.2014, 12:10 +0200 schrieb Roger H.:
i want to create a datatype
typedef less_three = {n€N. n<3}
(Small note: It is easier to read if you directly copy&paste the Isar
sources from jEdit. "€" looks very strange, and your examples don't
match HOL syntax nor your own definitions. )
Now, when we write
definition my_number :: nat, where "my_number = 0.5"
then we get an error "0.5 is not a nat"
Which Isabelle version are you using?
theory Scratch
imports Complex_Main
begin
definition n :: nat where "n = 0.5"
Results into:
Bad head of lhs: existing constant "real"
The error(s) above occurred in definition:
"real n ≡ 5 / 10"
This is a little strange: what happens is that Isabelle sees that
n as a natural number does not support division "5 / 10", so it
translates it into a real number. But this does result into a term not
suitable for definitions.
Now i want to get the same error with the type above less_three, meaning if i write
definition other_number :: three, where "other_number = 4" (*)
then i want to get an error that "4 is not a less_three" (cause its larger)
so basically an automatic type warning.
Actually it produces an error:
theory Scratch imports Complex_Main begin
typedef three = "{n::nat. n <= 3}"
sorry
definition x :: three where "x = 4"
gives
Type unification failed: No type arity three :: numeral
(there is a longer text from type coercion which we can ignore)
To support this you need to instantiate less_three with numerals. When
you add this your definition works.
What you want to do is not possible with the existing infrastructure.
Either your type allows numerals, then you need to convert each number
into your type (of course you can use module arithmetic to fit it into a
finite range). You can however avoid negative numerals and decimal point
numerals by not supporting unary minus or division.
What bothers me is that the equation (*) above is just accepted by isabelle although its bad typed.
No the typing is correct. The semantics are strange, but this is exactly
what Isabelle is for. You can proof:
nat_of_three x ~= 4
(assuming a translation function nat_of_three :: three => nat)
I have an idea what Rep and Abs do from the tutorial so i kinda understand, but still do you
think u can give me an idea how to make the equation (*) produce an error?
Use the logic, not the type system! Otherwise you may need dependent
types.
Last updated: Apr 16 2024 at 08:18 UTC