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.