Re: [isabelle] Cl-isabelle-users Digest, Vol 113, Issue 26



Hi peter . i did as you said but i don’t know exactly how to find the definition of fun_upd because Ctrl + Click on fun_upd it give me only a menu 
On 25 Nov 2014, at 16:20, cl-isabelle-users-request at lists.cam.ac.uk wrote:

> Send Cl-isabelle-users mailing list submissions to
> 	cl-isabelle-users at lists.cam.ac.uk
> 
> To subscribe or unsubscribe via the World Wide Web, visit
> 	https://lists.cam.ac.uk/mailman/listinfo/cl-isabelle-users
> or, via email, send a message with subject or body 'help' to
> 	cl-isabelle-users-request at lists.cam.ac.uk
> 
> You can reach the person managing the list at
> 	cl-isabelle-users-owner at lists.cam.ac.uk
> 
> When replying, please edit your Subject line so it is more specific
> than "Re: Contents of Cl-isabelle-users digest..."
> 
> 
> Today's Topics:
> 
>   1.  2-year postdoc position on security verification at TUM
>      (Tobias Nipkow)
>   2. Re:  Isar-Level cases command (Joachim Breitner)
>   3.  Define a fun (mahmoud abdelazim)
>   4. Re:  Define a fun (Buday Gergely)
>   5. Re:  Define a fun (Peter Lammich)
>   6.  Array (mahmoud abdelazim)
>   7. Re:  Array (Peter Lammich)
> 
> 
> ----------------------------------------------------------------------
> 
> Message: 1
> Date: Tue, 25 Nov 2014 12:13:18 +0100
> From: Tobias Nipkow <nipkow at in.tum.de>
> Subject: [isabelle] 2-year postdoc position on security verification
> 	at TUM
> To: Isabelle Users <isabelle-users at cl.cam.ac.uk>
> Message-ID: <5474644E.9020702 at in.tum.de>
> Content-Type: text/plain; charset="iso-8859-1"
> 
> A 2-year postdoc position on security verification is available at the
> Technical University of Munich, Chair for Logic and Verification (the Munich
> Isabelle group, http://www21.in.tum.de/). The research project focuses on the
> following topics:
> 
> - Design of a flexible framework for information-flow security specification
> 
> - Formalization of the framework in the Isabelle proof assistant
> 
> - Integration of interactive formal verification
>   with language-based analysis tools to obtain holistic security guarantees
> 
> - Application of the above to obtain the end-to-end verification of a
>   realistic web-based system: an (EasyChair-like) conference management system
> 
> For our current results see http://www4.in.tum.de/~popescua/pdf/CAV2014.pdf
> More details can be provided on request.
> 
> The candidate must hold a PhD in computer science or mathematics and have a
> track record of original research published in good conferences and
> journals. Mathematical maturity, as well as experience with verification and
> analysis tools (in particular, proof assistants) are both very welcome.
> 
> The intended start date is February 2015 but can be negotiated.
> 
> Interested candidates should send a CV, list of publications and a brief
> statement of research interests to Tobias Nipkow (nipkow at in tum de) and
> Andrei Popescu (a.popescu at mdx ac uk).
> 
> -------------- next part --------------
> A non-text attachment was scrubbed...
> Name: smime.p7s
> Type: application/pkcs7-signature
> Size: 5059 bytes
> Desc: S/MIME Cryptographic Signature
> Url : https://lists.cam.ac.uk/pipermail/cl-isabelle-users/attachments/20141125/01fd5f34/attachment.bin 
> 
> ------------------------------
> 
> Message: 2
> Date: Tue, 25 Nov 2014 12:39:42 +0100
> From: Joachim Breitner <breitner at kit.edu>
> Subject: Re: [isabelle] Isar-Level cases command
> To: cl-isabelle-users at lists.cam.ac.uk
> Message-ID: <1416915582.1435.16.camel at kit.edu>
> Content-Type: text/plain; charset="iso-8859-15"
> 
> Hi,
> 
> 
> Am Dienstag, den 25.11.2014, 11:39 +0100 schrieb Andreas Lochbihler:
>> Personally, I do not mind having to state the "show ?case" part, because it makes clear 
>> that you really need to do the case distinction to prove the whole case. In fact, I think 
>> that your case distinction in the example is not as it should be, because you only need it 
>> to for the unfolding of filter.
> 
> True, in this sense the example is a bit lacking. And you are rightly
> pointing out that fact that for showing an intermediate statement using
> case distinction the current scheme is useful. So I would not go as far
> to expect that
> 
>  cases ("xs")
>    case Nil
>    have P
>  next
>    case (Cons x xs')
>    have P
>  qed
> 
> to be equivalent to 
> 
>  have P
>  proof (cases "xs"))
>    case Nil
>    have P
>  next
>    case (Cons x xs')
>    have P
>  qed
> 
> and hence (heh) suggest this feature only for the case (heh) where one
> or more actual subgoals are shown (heh) in each case (heh).
> 
> (Although I would not dismiss the above if it turns out to be feasible).
> 
> Greetings,
> Joachim
> 
> 
> -- 
> Dipl.-Math. Dipl.-Inform. Joachim Breitner
> Wissenschaftlicher Mitarbeiter
> http://pp.ipd.kit.edu/~breitner
> -------------- next part --------------
> A non-text attachment was scrubbed...
> Name: not available
> Type: application/pgp-signature
> Size: 819 bytes
> Desc: This is a digitally signed message part
> Url : https://lists.cam.ac.uk/pipermail/cl-isabelle-users/attachments/20141125/aada4564/attachment.bin 
> 
> ------------------------------
> 
> Message: 3
> Date: Tue, 25 Nov 2014 13:57:29 +0100
> From: mahmoud abdelazim <m.abdelazim at icloud.com>
> Subject: [isabelle] Define a fun
> To: cl-isabelle-users at lists.cam.ac.uk
> Message-ID: <56DCCF37-33FD-48C3-82CC-E10B6889E5A3 at icloud.com>
> Content-Type: text/plain; charset=us-ascii
> 
> Hi 
> How to define a fun like fun_upd in Isabelle?
> thanks
> 
> 
> 
> ------------------------------
> 
> Message: 4
> Date: Tue, 25 Nov 2014 14:08:17 +0100
> From: Buday Gergely <gbuday at karolyrobert.hu>
> Subject: Re: [isabelle] Define a fun
> To: mahmoud abdelazim <m.abdelazim at icloud.com>,
> 	"cl-isabelle-users at lists.cam.ac.uk"
> 	<cl-isabelle-users at lists.cam.ac.uk>
> Message-ID:
> 	<C32D3449D568C445AB18C60817FABFE1012FD36B4550 at ingrid.foiskola.krf>
> Content-Type: text/plain; charset="us-ascii"
> 
> Dear Mahmoud,
> 
> could you please specify what your fun_upd would do?
> 
> - Gergely
> 
> -----Original Message-----
> From: cl-isabelle-users-bounces at lists.cam.ac.uk [mailto:cl-isabelle-users-bounces at lists.cam.ac.uk] On Behalf Of mahmoud abdelazim
> Sent: Tuesday, November 25, 2014 1:57 PM
> To: cl-isabelle-users at lists.cam.ac.uk
> Subject: [isabelle] Define a fun
> 
> Hi 
> How to define a fun like fun_upd in Isabelle?
> thanks
> 
> 
> 
> 
> ------------------------------
> 
> Message: 5
> Date: Tue, 25 Nov 2014 14:20:09 +0100
> From: Peter Lammich <lammich at in.tum.de>
> Subject: Re: [isabelle] Define a fun
> To: cl-isabelle-users at lists.cam.ac.uk
> Message-ID: <1416921609.5936.1.camel at lapbroy33>
> Content-Type: text/plain; charset="UTF-8"
> 
> You may look at how it is actually done in Isabelle:
>  In isabelle/jedit, type term "fun_upd", and goto its definition by
> Ctrl+Click on "fun_upd".
> 
> --
>  Peter
> 
> 
> On Di, 2014-11-25 at 13:57 +0100, mahmoud abdelazim wrote:
>> Hi 
>> How to define a fun like fun_upd in Isabelle?
>> thanks
>> 
> 
> 
> 
> 
> 
> ------------------------------
> 
> Message: 6
> Date: Tue, 25 Nov 2014 15:48:37 +0100
> From: mahmoud abdelazim <m.abdelazim at icloud.com>
> Subject: [isabelle] Array
> To: cl-isabelle-users at lists.cam.ac.uk
> Message-ID: <529E3FE3-6749-479E-AB9A-5DA7B0624DA0 at icloud.com>
> Content-Type: text/plain;	charset=utf-8
> 
> In Isabelle i can do that : 
> (?x. 0) (''x'':= 7,??z??:= 4)
> And i want to do the following :
> (?x. 0) (??Array'':= (1:=2, 2:=0, 3:=4),??z??:= 4)
> but i have problems, how can i  
> 
> ------------------------------
> 
> Message: 7
> Date: Tue, 25 Nov 2014 16:20:12 +0100
> From: Peter Lammich <lammich at in.tum.de>
> Subject: Re: [isabelle] Array
> To: cl-isabelle-users at lists.cam.ac.uk
> Message-ID: <1416928812.5936.5.camel at lapbroy33>
> Content-Type: text/plain; charset="UTF-8"
> 
> On Di, 2014-11-25 at 15:48 +0100, mahmoud abdelazim wrote:
>> In Isabelle i can do that : 
>> (?x. 0) (''x'':= 7,??z??:= 4)
>> And i want to do the following :
>> (?x. 0) (??Array'':= (1:=2, 2:=0, 3:=4),??z??:= 4)
>> but i have problems, how can i  
> 
> 
> "(1:=2, 2:=0, 3:=4)" is no valid syntax in isabelle. You have to apply
> the function update operator to some function, e.g.,
> 
> "(%x. 0)(1:=2, 2:=0, 3:=4)"
> 
> Alternatively, you could define your own syntax, 
> like the "<''x'':=1, ''y'' := 2>" in IMP/AExp
> 
> 
> --
>  Peter
> 
> 
> 
> 
> 
> End of Cl-isabelle-users Digest, Vol 113, Issue 26
> **************************************************





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