Grace/Cumulus/Set/Finite.g17

Open in Workbench Download source

Imports

Basic

Declarations

• insert def
• doubleton def
• singleton.membership theorem derivation
• union2.membership theorem derivation
• union2.right theorem derivation
• union2.commutative theorem derivation
• union2.idempotent theorem derivation
• union2.associative theorem derivation
• insert.membership theorem derivation
• insert.self theorem derivation
• insert.contains theorem derivation
• doubleton.membership theorem derivation
• insert.restore theorem derivation

Source

1-- Finite set constructions2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Set.Finite8import Basic910namespace FiniteSet1112def insert (x A : Set) : Set := {x} ∪ A13def doubleton (x y : Set) : Set := {x} ∪ {y}1415theorem singleton.membership (x a : Set)16  shows x ∈ {a} ↔ x = a17proof18  simp [singleton, pair.membership]1920theorem union2.membership (x A B : Set)21  shows x ∈ A ∪ B ↔ (x ∈ A ∨ x ∈ B)22proof23  simp [union2, set.union, pair.membership]2425theorem union2.right (x A B : Set)26  requires hx : x ∈ B27  shows x ∈ A ∪ B28proof29  simp3031theorem union2.commutative (A B : Set)32  shows A ∪ B = B ∪ A33proof34  ext y35  simp3637theorem union2.idempotent (A : Set)38  shows A ∪ A = A39proof40  ext y41  simp4243theorem union2.associative (A B C : Set)44  shows (A ∪ B) ∪ C = A ∪ (B ∪ C)45proof46  ext y47  simp4849theorem insert.membership (x y A : Set)50  shows x ∈ insert(y, A) ↔ (x = y ∨ x ∈ A)51proof52  simp [insert, union2.membership, singleton.membership]5354theorem insert.self (x A : Set)55  shows x ∈ insert(x, A)56proof57  simp5859theorem insert.contains (x y A : Set)60  requires hx : x ∈ A61  shows x ∈ insert(y, A)62proof63  simp6465theorem doubleton.membership (x a b : Set)66  shows x ∈ doubleton(a, b) ↔ (x = a ∨ x = b)67proof68  simp [doubleton, union2.membership, singleton.membership]6970theorem insert.restore (V x : Set)71  requires member : x ∈ V72  shows insert(x, V ∖ {x}) = V73proof74  ext y75  simp7677end FiniteSet7879export open Grace.Cumulus.Set.Finite.FiniteSet80