Email Gateway (Aug 18 2022 at 09:47): Email Gateway (Aug 18 2022 at 09:47):From: Peter Sewell <Peter.Sewell@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
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
Email Gateway (Aug 18 2022 at 09:48):From: Stefan Berghofer <berghofe@in.tum.de>
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
Email Gateway (Aug 18 2022 at 09:48):From: Tobias Nipkow <nipkow@in.tum.de>
Something related: one should always try to use "ALL x : set xs. P x"
rather than "list_all P xs".
Tobias
Stefan Berghofer schrieb:
Last updated: May 03 2024 at 08:18 UTC