*To*: Roger H. <s57076 at hotmail.com>, "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Reformulation question typedef*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Thu, 9 Jan 2014 15:55:10 +0100*In-reply-to*: <DUB124-W14750C6172E06CA35214068FB00@phx.gbl>*References*: <DUB124-W14750C6172E06CA35214068FB00@phx.gbl>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.2.0

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 On 09/01/14 15:39, Roger H. wrote: > 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 > >

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

- Previous by Date: [isabelle] Reformulation question typedef
- Next by Date: [isabelle] typedef proof method
- Previous by Thread: [isabelle] Reformulation question typedef
- Next by Thread: [isabelle] typedef proof method
- 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