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
