Created
August 25, 2014 15:04
-
-
Save javra/11b9a6770cab2e17559d to your computer and use it in GitHub Desktop.
remdups_adj another lemma
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
lemma remdups_adj_obtain_adjacency: | |
assumes "i + 1 < length (remdups_adj xs)" "length xs > 0" | |
obtains j where "j + 1 < length xs" | |
"(remdups_adj xs) ! i = xs ! j" "(remdups_adj xs) ! (i + 1) = xs ! (j + 1)" | |
using assms proof (induction xs arbitrary: i thesis) | |
case Nil | |
hence False by (metis length_greater_0_conv) | |
thus thesis.. | |
next | |
case (Cons x xs) | |
hence "xs ≠ []" using Divides.div_less Suc_eq_plus1 Zero_not_Suc div_eq_dividend_iff list.size(3,4) plus_nat.add_0 remdups_adj.simps(2) by metis | |
then obtain y xs' where xs:"xs = y # xs'" by (metis list.exhaust) | |
from `xs ≠ []` have lenxs:"length xs > 0" by simp | |
from xs have rem:"remdups_adj (x # xs) = (if x = y then remdups_adj (y # xs') else x # remdups_adj (y # xs'))" using remdups_adj.simps(3) by auto | |
show thesis | |
proof (cases "x = y") | |
case True | |
with rem xs have rem2:"remdups_adj (x # xs) = remdups_adj xs" by auto | |
with Cons(3) have "i + 1 < length (remdups_adj xs)" by simp | |
with Cons.IH lenxs obtain k where j:"k + 1 < length xs" "remdups_adj xs ! i = xs ! k" | |
"remdups_adj xs ! (i + 1) = xs ! (k + 1)" by auto | |
thus thesis using Cons(2) rem2 by auto | |
next | |
case False | |
with rem xs have rem2:"remdups_adj (x # xs) = x # remdups_adj xs" by auto | |
show thesis | |
proof (cases i) | |
case 0 | |
have "0 + 1 < length (x # xs)" using lenxs by auto | |
moreover have "remdups_adj (x # xs) ! i = (x # xs) ! 0" | |
proof - | |
have "remdups_adj (x # xs) ! i = (x # remdups_adj (y # xs')) ! 0" using xs rem2 0 by simp | |
also have "… = x" by simp | |
also have "… = (x # xs) ! 0" by simp | |
finally show ?thesis. | |
qed | |
moreover have "remdups_adj (x # xs) ! (i + 1) = (x # xs) ! (0 + 1)" | |
proof - | |
have "remdups_adj (x # xs) ! (i + 1) = (x # remdups_adj (y # xs')) ! 1" using xs rem2 0 by simp | |
also have "… = remdups_adj (y # xs') ! 0" by simp | |
also have "… = (y # (remdups (y # xs'))) ! 0" by (metis nth_Cons' remdups_adj_Cons_alt) | |
also have "… = y" by simp | |
also have "… = (x # xs) ! (0 + 1)" unfolding xs by simp | |
finally show ?thesis. | |
qed | |
ultimately show thesis by (rule Cons.prems(1)) | |
next | |
case (Suc k) | |
with Cons(3) have "k + 1 < length (remdups_adj (x # xs)) - 1" by auto | |
also have "… ≤ length (remdups_adj xs) + 1 - 1" by (metis One_nat_def le_refl list.size(4) rem2) | |
also have "… = length (remdups_adj xs)" by simp | |
finally have "k + 1 < length (remdups_adj xs)". | |
with Cons.IH lenxs obtain j where j:"j + 1 < length xs" "remdups_adj xs ! k = xs ! j" | |
"remdups_adj xs ! (k + 1) = xs ! (j + 1)" by auto | |
from j(1) have "Suc j + 1 < length (x # xs)" by simp | |
moreover have "remdups_adj (x # xs) ! i = (x # xs) ! (Suc j)" | |
proof - | |
have "remdups_adj (x # xs) ! i = (x # remdups_adj xs) ! i" using rem2 by simp | |
also have "… = (remdups_adj xs) ! k" using Suc by simp | |
also have "… = xs ! j" using j(2) . | |
also have "… = (x # xs) ! (Suc j)" by simp | |
finally show ?thesis . | |
qed | |
moreover have "remdups_adj (x # xs) ! (i + 1) = (x # xs) ! (Suc j + 1)" | |
proof - | |
have "remdups_adj (x # xs) ! (i + 1) = (x # remdups_adj xs) ! (i + 1)" using rem2 by simp | |
also have "… = (remdups_adj xs) ! (k + 1)" using Suc by simp | |
also have "… = xs ! (j + 1)" using j(3). | |
also have "… = (x # xs) ! (Suc j + 1)" by simp | |
finally show ?thesis. | |
qed | |
ultimately show thesis by (rule Cons.prems(1)) | |
qed | |
qed | |
qed |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment