*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] typedef*From*: Johannes Hölzl <hoelzl at in.tum.de>*Date*: Wed, 08 Jan 2014 15:09:44 +0100*In-reply-to*: <DUB124-W43F28810FC84111B050C638FB10@phx.gbl>*Organization*: TU München*References*: <DUB124-W43F28810FC84111B050C638FB10@phx.gbl>

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

**References**:**[isabelle] typedef***From:*Roger H .

- Previous by Date: Re: [isabelle] partial function
- Next by Date: [isabelle] A postdoc/programmer position at AIST, Amagasaki Japan
- Previous by Thread: [isabelle] typedef
- Next by Thread: [isabelle] partial function
- Cl-isabelle-users January 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list