*To*: Viorel Preoteasa <viorel.preoteasa at gmail.com>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] evaluation of expressions*From*: Andreas Lochbihler <mail at andreas-lochbihler.de>*Date*: Fri, 1 Mar 2019 21:25:24 +0100*In-reply-to*: <247137bc-d9b0-3f0a-b175-6d679d0c8557@gmail.com>*References*: <875B1B8C-280D-413D-A1F1-2C98D2FC785D@gmail.com> <0F563D2E-1CDD-411A-BED7-1614D1DE0882@uibk.ac.at> <16c07875-31b3-adf4-e098-b27a537d71e3@gmail.com> <d0e84b6ff7e1485cae265938dcaf5ac6@chalmers.se> <247137bc-d9b0-3f0a-b175-6d679d0c8557@gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:60.0) Gecko/20100101 Thunderbird/60.2.1

Dear Viorel,

Andreas On 01/03/2019 09:54, Viorel Preoteasa wrote:

Hello,I have a lemma of the following form: "g (S f) = f" and I would like to use it evaluatefor example "g (S Suc) 3" usingvalue "g (S Suc) 3"Is it possible to achieve this behavior? Simplification works OK, but I need also a quickway to calculate this kind of expressions.Next is the complete example definition "S f x = f x" lemma S_simp: "S f = f" by (simp add: S_def fun_eq_iff) definition "g A = (SOME f . A = S f)" lemma g_S_simp[code,simp]: "g (S f) = f" by (simp add: g_def S_simp) lemma "g (S Suc) 3 = 4" by (simp) (*this works OK*) value "g (S Suc) 3" (*this gives Wellsortedness error*) Best regards, Viorel Preoteasa On 19/02/2019 15.14, Thomas Sewell wrote:I recall the addition of the signed words, and maybe I can add some information.I think that "'a signed word" and "'a word" are equivalent for all key operations. Thesigned variant was added as part of an adjustment of the C-to-Isabelle parser, so thatin the resulting code it was possible to tell whether the variables were designatedsigned or unsigned in C. Note that most arithmetic is exactly the same.Also note that the outer type constructor is word, that is, "32 signed word" is aninstance of "'a word" where the length parameter is "32 signed". To make use of this, Ithink you want to define some kind of is_signed class with a class constant of typebool, and ensure that "32 signed" is signed, and that each numeral type counts asunsigned. Finally, you can lift that to a query on the outer word type.I think that all might work, but I haven't tried any of it. Cheers, Thomas. ------------------------------------------------------------------------*From:* cl-isabelle-users-bounces at lists.cam.ac.uk<cl-isabelle-users-bounces at lists.cam.ac.uk> on behalf of Viorel Preoteasa<viorel.preoteasa at gmail.com>*Sent:* Tuesday, February 19, 2019 10:40:26 AM *To:* Thiemann, René *Cc:* cl-isabelle-users at lists.cam.ac.uk *Subject:* Re: [isabelle] signed and unsigned words Dear René, Thank you for your message. On 18/02/2019 15.18, Thiemann, René wrote: > Dear Viorel, >> it is difficult to test your problem, since the “signed” and “usigned” types aresomething that I do neither find in the distribution nor in the AFP.The definition of the signed type is here: https://www.isa-afp.org/browser_info/current/AFP/Word_Lib/Signed_Words.html and the definition of unsigned is identical. > > Hence, I can only blindly guess: >> There might be a problem in your definition of “overflow_add” which uses the generic“to_int”, not a specific implementation.> This will work if “to_int” is defined as a class-constant (class some_name = fixesto_int :: …), but I’m not sure whether your approach via “consts to_int” is supportedwith code-generation.> > So, you might try to reformulate the definition of to_int via class and instantiation. This was my first attempt, but I did not manage the instantiation of class overflow as 'a signed word . Now I have implemented a different solution. I created a new copy of the type 'a word: typedef (overloaded) 'a::len sword = "UNIV::'a word set" morphisms sword_to_word word_to_sword by auto and I lifted all operations from word to sword. This seems to work, but I am interested to find the best possible solution. Best regards, Viorel > > Best regards, > René >>> I need new types of signed and unsigned words with operations (+, -, ...) identicalwith the operations on words, but with a new operation:>> >> overflow_add a b which is defined differently for signed and unsigned words. >> >> Basically I need the two types to be instantiations of the following class: >> >> class overflow = plus + >> fixes overflow_add:: "'a ⇒ 'a ⇒ bool" >> >> I tried something inspired from the AFP entry "Finite Machine Word Library": >> >> type_synonym 'a sword = "'a signed word" >> type_synonym 'a uword = "'a usigned word" >> >> consts to_int :: "'a word ⇒ int" >> >> overloading >> to_int_sword ≡ "to_int:: 'a sword ⇒ int" >> to_int_uword ≡ "to_int::'a uword ⇒ int" >> begin >> definition "to_int_sword (a:: 'a::len sword) = sint a" >> definition "to_int_uword (a:: 'a::len uword) = uint a" >> end >> >> instantiation word :: (len0) overflow >> begin >> definition "overflow_add a b = (to_int (a::'a word) + to_int b = to_int (a + b))" >> instance .. >> end >> >> this seems to work, but I don't know how to get code generation for overflow_add: >> >> value "overflow_add (-2::4 sword) (-3)" >> >> gives the error: >> >> No code equations for to_int

**Follow-Ups**:**Re: [isabelle] evaluation of expressions***From:*Manuel Eberl

**References**:**[isabelle] evaluation of expressions***From:*Viorel Preoteasa

- Previous by Date: Re: [isabelle] Trivial lemma requires syntactic fiddling
- Next by Date: Re: [isabelle] evaluation of expressions
- Previous by Thread: [isabelle] evaluation of expressions
- Next by Thread: Re: [isabelle] evaluation of expressions
- Cl-isabelle-users March 2019 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