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

[Andreas Lochbihler]

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.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