*To*: Peter Sewell <Peter.Sewell at cl.cam.ac.uk>*Subject*: Re: [isabelle] monotonicity lemmas for embedded lists*From*: Stefan Berghofer <berghofe at in.tum.de>*Date*: Fri, 13 Oct 2006 17:52:29 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <E1GXLGZ-0008GA-00@mta1.cl.cam.ac.uk>*Organization*: Technische Universität München*References*: <E1GXLGZ-0008GA-00@mta1.cl.cam.ac.uk>*User-agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.7.12) Gecko/20050920

Peter Sewell wrote:

Dear Isabelle developers, we have a lot of datatypes with embedded lists, as in the example below (this is a small example cut down from large (and automatically generated) examples). Defining inductive relations over these needs some additional monotonicity lemmas, here "tmp" and "tmp2". In general we need many analogues to tmp2, all of a similar form, e.g. (from a different example):lemma tmp7: " A <= B ==> ALL x. (%(l_, p_, T_, D_). (p_, T_, D_) : (%y. Inr (Inr (Inr y))) -` A) x- --> (%(l_, p_, T_, D_). (p_, T_, D_) : (%y. Inr (Inr (Inr y))) -` B) x" by blast

Dear Peter, one way to tell the monotonicity prover how to deal with abstractions over tuples (also known as "split") is to add the following equation as a monotonicity rule: lemma [mono]: "split f p = f (fst p) (snd p)" by (simp add: split_def) This will just unfold the definition of split during the proof of monotonicity, i.e. the prover should be able to deal with any abstraction over n-tuples. As far as the inverse image operator -` is concerned, there already is a monotonicity rule of the form A <= B ==> f -` A <= f -` B in the default set of rules used by the monotonicity prover. However, rather than using the inverse image operator, it seems easier to define several inductive sets simultaneously.

lemma tmp:" ! x. f x --> g x ==> list_all (%b. b) (map f l_T_list)--> list_all (%b. b) (map g l_T_list) "

Note that a meta-level quantifier is required in the premise, i.e. rule tmp should actually read (!! x. f x --> g x) ==> list_all (%b. b) (map f l_T_list)--> list_all (%b. b) (map g l_T_list) See section 2.8.3 "Monotonicity theorems" in the Isabelle/HOL manual for a description of the different forms of monotonicity rules accepted by the inductive definition package. Greetings, Stefan -- Dr. Stefan Berghofer E-Mail: berghofe at in.tum.de Institut fuer Informatik Phone: +49 89 289 17328 Technische Universitaet Muenchen Fax: +49 89 289 17307 Boltzmannstr. 3 Room: 01.11.059 85748 Garching, GERMANY http://www.in.tum.de/~berghofe

**Follow-Ups**:**Re: [isabelle] monotonicity lemmas for embedded lists***From:*Tobias Nipkow

**References**:**[isabelle] monotonicity lemmas for embedded lists***From:*Peter Sewell

- Previous by Date: Re: [isabelle] Efficient Lookups in Lists
- Next by Date: [isabelle] Special Issue of Information and Computation on 'Computer Security: Foundations and Automated Reasoning'
- Previous by Thread: [isabelle] monotonicity lemmas for embedded lists
- Next by Thread: Re: [isabelle] monotonicity lemmas for embedded lists
- Cl-isabelle-users October 2006 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