Hi Christian,
I am not completely sure what you mean. It is possible to leave key out of the
conclusion in sequences_induct.
lemma sequences_induct[case_names Nil singleton IH]:
assumes "P []" and "!!x. P [x]"
and "!!a b xs. [| key b < key a ==> P (drop_desc key b xs);
~ key b < key a ==> P (drop_asc key b xs) |]
==> P (a # b # xs)"
shows "P xs"
using assms by (induction_schema)(pat_completeness, lexicographic_order)
However, when you apply this rule using induct, key is not instantiated by
unification. In order to use the "case Nil" syntax in Isar proofs, you must
explicitly instantiate key in the induction method via the taking clause.
Otherwise, key is left as an unbound variable in the goal state.
For example:
proof(induct xs taking: "concrete_key" rule: sequences_induct)
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
