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_induct) seems to be "wrong" for induction_schema. Maybe because
> of an additional assumption? Any ideas?
Induction_schema is picky about the order of assumptions. Additional assumptions
(typically those for consumes) must be fed into the induction_schema method
*after* the inductive cases. Moreover, in your lemma sorted_merge_induct, "P"
must not take "key" as argument because all inductive cases simply pass "key" on
to "P". Otherwise, induction_schema does not terminate. Note that it is not
necessary to have the "key" parameter either because unification instantiates
"key" when it consumes the first assumption.
Here's how sorted_merge_induct works with induction_schema:
lemma sorted_merge_induct[consumes 1, case_names Nil IH]:
fixes key::"'b \<Rightarrow> 'a"
assumes "sorted (map key xs)"
and "\<And>xs. P xs []"
and "\<And>xs y ys. sorted (map key xs) \<Longrightarrow>
P (dropWhile (\<lambda>x. key x \<le> key y) xs) ys
\<Longrightarrow> P xs (y#ys)"
shows "P xs ys"
using assms(2-) assms(1)
apply(induction_schema)
Andreas
--
Karlsruher Institut für Technologie
IPD Snelting
Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 031
76131 Karlsruhe
Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbih...@kit.edu
http://pp.info.uni-karlsruhe.de
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum
in der Helmholtz-Gemeinschaft
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
