list - 如何证明 sset (cycle xs) = set xs

Question

在使用 Isabelle 的无限流数据类型时，我需要这个显然是真的引理，但我无法弄清楚如何证明它（因为我还不精通共归纳法）。我将如何去证明它？

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

Answer 1

我自己不是联合归纳方面的专家，但这里不需要联合归纳。我也不是 codatatypes 方面的专家，但无论如何，这里有一个证明：

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和使用之外op !!，您还可以直接进行归纳sset（使用规则 sset_induct）：

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