Re: [isabelle-dev] Merge-Sort Implementation (and a question, on induction_schema)
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
Re: [isabelle-dev] Merge-Sort Implementation (and a question, on induction_schema)
Hi Andreas, taking was actually what I was searching for, thanks! I just found it strange to write (induct key xs rule: ...) when key staid the same all the time. cheers chris On 11/03/2011 12:40 PM, Andreas Lochbihler wrote: 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 ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
