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

[Christian Sternagel]

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
>