[isabelle-dev] Merge-Sort Implementation (and a question, on induction_schema)
andreas.lochbihler at kit.edu
Wed Nov 2 12:40:49 CET 2011
> 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)
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