Re: [isabelle] monotonicity lemmas for embedded lists
Something related: one should always try to use "ALL x : set xs. P x"
rather than "list_all P xs".
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 blast
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.
! 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and