list - sset (cycle xs) = set xs の証明方法

Question

Isabelle の無限ストリーム データ型を扱う場合、この明らかに正しい補題が必要ですが、それを証明する方法がわかりません (私はまだ帰納法に精通していないため)。それを証明するにはどうすればいいですか？

lemma sset_cycle[simp]:
  "xs ≠ [] ⟹ sset (cycle xs) = set xs"

Answer 1

私自身は共導の専門家ではありませんが、ここでは共導は必要ありません。私もコードデータ型の専門家ではありませんが、とにかく、ここに証明があります:

lemma sset_cycle [simp]:
  assumes "xs ≠ []"
  shows   "sset (cycle xs) = set xs"
proof
  have "set xs ⊆ set xs ∪ sset (cycle xs)" by blast
  also have "… = sset (xs @- cycle xs)" by simp
  also from ‹xs ≠ []› have "xs @- cycle xs = cycle xs" 
    by (rule cycle_decomp [symmetric])
  finally show "set xs ⊆ sset (cycle xs)" .
next
  from assms have "cycle xs !! n ∈ set xs" for n
  proof (induction n arbitrary: xs)
    case (Suc n xs)
    have "tl xs @ [hd xs] ≠ []" by simp
    hence "cycle (tl xs @ [hd xs]) !! n ∈ set (tl xs @ [hd xs])" by (rule Suc.IH)
    also have "cycle (tl xs @ [hd xs]) !! n = cycle xs !! Suc n" by simp
    also have "set (tl xs @ [hd xs]) = set (hd xs # tl xs)" by simp
    also from ‹xs ≠ []› have "hd xs # tl xs = xs" by simp
    finally show ?case .
  qed simp_all
  thus "sset (cycle xs) ⊆ set xs" by (auto simp: sset_range)
qed

更新:次の証明は少し優れています。

lemma sset_cycle [simp]:
  assumes "xs ≠ []"
  shows   "sset (cycle xs) = set xs"
proof
  have "set xs ⊆ set xs ∪ sset (cycle xs)" by blast
  also have "… = sset (xs @- cycle xs)" by simp
  also from ‹xs ≠ []› have "xs @- cycle xs = cycle xs" 
    by (rule cycle_decomp [symmetric])
  finally show "set xs ⊆ sset (cycle xs)" .
next
  show "sset (cycle xs) ⊆ set xs"
  proof
    fix x assume "x ∈ sset (cycle xs)"
    from this and ‹xs ≠ []› show "x ∈ set xs"
    proof (induction "cycle xs" arbitrary: xs)
      case (stl x xs)
      have "x ∈ set (tl xs @ [hd xs])" by (intro stl) simp_all
      also have "set (tl xs @ [hd xs]) = set (hd xs # tl xs)" by simp
      also from ‹xs ≠ []› have "hd xs # tl xs = xs" by simp
      finally show ?case .
    qed simp_all
  qed
qed

Answer 2

Manuel Eberl によって提案されているように誘導をn使用して使用する代わりに、直接誘導を行うこともできます(ルール sset_induct を使用):op !!sset

lemma sset_cycle [simp]:
  assumes "xs ≠ []" 
  shows "sset (cycle xs) = set xs"
proof (intro set_eqI iffI)
  fix x
  assume "x ∈ sset (cycle xs)"
  from this assms show "x ∈ set xs"
    by (induction "cycle xs" arbitrary: xs rule: sset_induct) (case_tac xs; fastforce)+
next
  fix x
  assume "x ∈ set xs"
  with assms show "x ∈ sset (cycle xs)"
   by (metis UnI1 cycle_decomp sset_shift)
qed