[isabelle-dev] Merge-Sort Implementation (and a question, on induction_schema)

[Andreas Lochbihler]

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.lochbihler at kit.edu
http://pp.info.uni-karlsruhe.de
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum 
in der Helmholtz-Gemeinschaft