Dear Christian,
I ironed out the apply-style snippets and simplified some proofs. Also
Christian's pointer to induction_schema significantly shortened the
proof of an induction schema I use (sequences_induct).
induction_schema is really useful! However, another induction schema
I was about to suggest the same as Andreas. For what it is
worth, here is my proof of this lemma.
lemma sorted_merge_induct[consumes 1, case_names Nil IH]:
fixes key::'b = 'a
assumes sorted (map key xs)
and !!xs. P xs []
and !!xs y ys. sorted (map key xs) == P (dropWhile (%x. key x
Thnx Andreas and Christian,
that worked fine! One minor thing: in the proof of sequences_induct, is
it possible to use induction_schema such that 'key' is not needed as
argument when applying the resulting induction rule using induct?
cheers
chris
On 11/02/2011 01:08 PM, Christian Urban
