[isabelle] monotonicity lemmas for embedded lists



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






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