[isabelle-dev] Merge-Sort Implementation (and a question, on induction_schema)
andreas.lochbihler at kit.edu
Thu Nov 3 12:40:16 CET 2011
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.
proof(induct xs taking: "concrete_key" rule: sequences_induct)
Karlsruher Institut für Technologie
Adenauerring 20a, Geb. 50.41, Raum 031
Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum
in der Helmholtz-Gemeinschaft
More information about the isabelle-dev