[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?
theory out imports Main begin
(** syntax *)
types index = "nat"
| a_tuple "a list"
| a_proj "a" "index"
| t_tuple "t list"
(** definitions *)
(*defns Jtype *)
at :: "(a*t) set"
! 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
(* 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 of Forwarded Message
This archive was generated by a fusion of
Pipermail (Mailman edition) and