*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] monotonicity lemmas for embedded lists*From*: Peter Sewell <Peter.Sewell at cl.cam.ac.uk>*Date*: Tue, 10 Oct 2006 18:19:43 +0100*Cc*: Peter.Sewell at cl.cam.ac.uk

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 with different Inr/Inl sequences depending on the structure of the definitions. Lemma tmp is key but has a uniform shape, whereas tmp2 and its analogues have varying shapes but are solved with blast. This suggests to the naive user that if the monotonicity prover just tried blast before giving up, we would only need the general lemma tmp, making life much simpler. Is it possible to turn that on? Alternatively, is there some smart way to express tmp2 and analogues in a uniform way (i.e. as a single lemma) that would be acceptable to the inductive package? Or we can rephrase the usages of List.list_all etc if that would help? many thanks, Peter %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% theory out imports Main begin (** syntax *) types index = "nat" datatype a = a_unit | a_tuple "a list" | a_proj "a" "index" datatype t = t_unit | t_tuple "t list" (** definitions *) (*defns Jtype *) consts at :: "(a*t) set" 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) " apply(induct_tac l_T_list, auto) done lemma tmp2: "A <= B ==> ALL x. (%(a_, t_). (a_, t_) : A) x --> (%(a_, t_). (a_, t_) : B) x" by blast inductive at intros (* defn at *) at_1I: " ( a_unit , t_unit ) : at" at_2I: "[|(List.list_all (% b . b) ((List.map (%(a_,t_). ( a_ , t_ ) : at) a_t_list)))|] ==> ( (a_tuple ((List.map (%(a_,t_).a_) a_t_list))) , (t_tuple ((List.map (%(a_,t_) .t_) a_t_list))) ) : at" at_3I: "[| ( a , (t_tuple (t_list)) ) : at|] ==> ( (a_proj a i) , ((%t_ . t_) (List.nth t_list (i))) ) : at" monos tmp tmp2 end ------- End of Forwarded Message

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

- Previous by Date: Re: [isabelle] Rep problem
- Next by Date: [isabelle] Isabelle Installation problem
- Previous by Thread: Re: [isabelle] Efficient Lookups in 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