Theory TopoS_Util

theory TopoS_Util
imports Main
begin

lemma finite_ne_subset_induct [case_names singleton insert, consumes 2]:
  assumes "finite F" and "F ≠ {}" and "F ⊆ A"
  assumes "⋀x. x ∈ A ⟹ P {x}"
    and "⋀x F. finite F ⟹ F ≠ {} ⟹ x ∈ A ⟹ x ∉ F ⟹ P F  ⟹ P (insert x F)"
  shows "P F"
using assms
proof induct
  case empty then show ?case by simp
next
  case (insert x F) then show ?case by cases auto
qed


(*lemma from afp collections Misc*)
lemma set_union_code:
  "set xs ∪ set ys = set (xs @ ys)"
  by auto

end