*To*: Stefan Berghofer <berghofe at in.tum.de>*Subject*: Re: [isabelle] monotonicity lemmas for embedded lists*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Fri, 13 Oct 2006 18:52:14 +0200*Cc*: Peter Sewell <Peter.Sewell at cl.cam.ac.uk>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <452FB63D.2080307@in.tum.de>*References*: <E1GXLGZ-0008GA-00@mta1.cl.cam.ac.uk> <452FB63D.2080307@in.tum.de>*User-agent*: Thunderbird 1.5.0.2 (Macintosh/20060308)

Tobias Stefan Berghofer schrieb:

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 blastDear 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

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

**Re: [isabelle] monotonicity lemmas for embedded lists***From:*Stefan Berghofer

- Previous by Date: [isabelle] Special Issue of Information and Computation on 'Computer Security: Foundations and Automated Reasoning'
- Next by Date: [isabelle] inverse definition in modulo p
- Previous by Thread: Re: [isabelle] monotonicity lemmas for embedded lists
- Next by Thread: [isabelle] Isabelle Installation problem
- 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