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 w
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 (%
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
> (merge
