Re: [isabelle] typedef



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.


 - Johannes








This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.