# Re: [isabelle] How does one reason about the subset of a list?

Hello,
I corrected the specification and simplified it so that P is valid on the entire list (to make the proof simpler for me).
P now looks like:
constdefs
"P (xs::nat list) Y == \<forall>i < length xs. xs!i \<le> Y"
And the lemma I am trying to prove is:
lemma "P xs Y \<longrightarrow> (\<forall> j. j < (length xs - 1) \<longrightarrow> P (listswap xs j (j+1)) Y)"
And I am still using the listswap and listswap_length.
I have tried to prove that lemma in different ways and failed.
The formulation of the proof which reflects my current try looks like:
lemma "P xs Y \<longrightarrow> (\<forall> j. j < (length xs - 1) \<longrightarrow> P (listswap xs j (j+1)) Y)"
proof (simp add: listswap_length P_def)
have "P xs Y \<longrightarrow> (\<forall> j. Suc j < length xs \<longrightarrow>
(\<forall>i. i < length xs \<longrightarrow>
(i \<noteq> j \<and> i \<noteq> (Suc j)
\<longrightarrow> (listswap xs j (Suc j))!i \<le> Y))) "
by (simp add: listswap_def P_def)
also have "P xs Y \<longrightarrow> (\<forall> j. Suc j < length xs \<longrightarrow>
(\<forall>i. i = j \<longrightarrow> (listswap xs j (Suc j))!j \<le> Y))"
by (simp add: listswap_def P_def)
oops
also have "P xs Y \<longrightarrow> (\<forall> j. Suc j < length xs \<longrightarrow>
(\<forall>i. (i = (Suc j)) \<longrightarrow> (listswap xs j (Suc j))!(Suc j) \<le> Y))"
by (simp add: listswap_def P_def)
finally show ?thesis apply ()
qed
With the oops showing where it breaks.
Isn't this a valid way of breaking down this proof?
Thanks for your help!
Regards,
Primrose
P.S: Also how do you convert the X-Symbols to ascii?

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*