I have a function which is matching on lists:
fun merge where
‹merge [] [] = []› |
‹merge (v#vs) [] = (v#vs)› |
‹merge [] (v#vs) = (v#vs)› |
‹merge (x#xs) (y#ys) =
(if x < y then x # merge xs (y#ys) else y # merge (x#xs) ys)›
When I'm trying to prove the correctness of this I'm having difficulties with induction based on this:
...
lemma sorted_merge:
assumes s_xs: "sorted(xs)"
and s_ys: "sorted(ys)"
shows ‹sorted(merge xs ys)›
proof (induction xs ys rule: merge.induct [case_names base xs ys both])
case base then show "?case" by auto
next
case xs
show "?case"
proof -
The issue is that I can prove that this case for sorted(merge xs []) but this doesn't satisify sorted(merge (v#vs) []) which is the proof goal.
Hence how do I fix xs to be v#vs, or to otherwise refer to the case analysed xs for this specific case?
Hence how do I fix xs to be
v#vs, or to otherwise refer to the case analysedxsfor this specific case?
This is explained in section 6.5 of the reference manual of Isabelle2020 (Isar-ref):
... By using the explicit form
case (c y1 ... ym)... the proof author is able to chose local names that fit nicely into the current context ...
Thus, in your case, you can use something similar to
fun merge where
‹merge [] [] = []›
| ‹merge (v#vs) [] = (v#vs)›
| ‹merge [] (v#vs) = (v#vs)›
| ‹merge (x#xs) (y#ys) =
(if x < y then x # merge xs (y#ys) else y # merge (x#xs) ys)›
lemma sorted_merge:
assumes s_xs: "sorted(xs)" and s_ys: "sorted(ys)"
shows ‹sorted(merge xs ys)›
using assms
proof(induction xs ys rule: merge.induct[case_names base xs ys both])
case base then show ?case by auto
next
case (xs v vs) then show ?case by auto
next
case (ys v vs) then show ?case by auto
next
case (both x xs y ys)
show ?case
proof(cases ‹x < y›)
case True with both(1,3,4) show ?thesis by (induction xs) force+
next
case False with both(2,3,4) show ?thesis by (induction ys) force+
qed
qed
Isabelle version: Isabelle2020