# Theory DL_Missing_Finite_Set

theory DL_Missing_Finite_Set
imports Main
```(* Author: Alexander Bentkamp, Universität des Saarlandes
*)
section ‹Missing Lemmas of Finite\_Set›
theory DL_Missing_Finite_Set
imports Main
begin

lemma card_even[simp]: "card {a ∈ Collect even. a < 2 * n} = n"
proof (induction n)
case 0
then show ?case by auto
next
case (Suc n)
have "{a ∈ Collect even. a < 2 * Suc n} = insert (2*n) {a ∈ Collect even. a < 2 * n}"
using le_eq_less_or_eq less_Suc_eq_le subset_antisym by force
show ?case
unfolding ‹{a ∈ Collect even. a < 2 * Suc n} = insert (2*n) {a ∈ Collect even. a < 2 * n}›
using Suc card_insert_disjoint[of "{a ∈ Collect even. a < 2 * n}" "2*n"]
qed

lemma card_odd[simp]: "card {a ∈ Collect odd. a < 2 * n} = n"
proof (induction n)
case 0
then show ?case by auto
next
case (Suc n)
have "{a ∈ Collect odd. a < 2 * Suc n} = insert (2*n+1) {a ∈ Collect odd. a < 2 * n}"
using le_eq_less_or_eq less_Suc_eq_le subset_antisym by force
show ?case
unfolding ‹{a ∈ Collect odd. a < 2 * Suc n} = insert (2*n+1) {a ∈ Collect odd. a < 2 * n}›
using Suc card_insert_disjoint[of "{a ∈ Collect even. a < 2 * n}" "2*n"]