% Some simple theorems about finite sets declare sorts E, S declare variables e, e1, e2: E, x, y, z: S declare operators {}: -> S {__}: E -> S insert: E, S -> S __ \union __: S, S -> S __ \in __: E, S -> Bool __ \subseteq __: S, S -> Bool .. % Axioms set name setAxioms assert sort S generated by {}, insert; {e} = insert(e, {}); ~(e \in {}); e \in insert(e1, x) <=> e = e1 \/ e \in x; {} \subseteq x; insert(e, x) \subseteq y <=> e \in y /\ x \subseteq y; e \in (x \union y) <=> e \in x \/ e \in y .. set name extensionality assert \A e (e \in x <=> e \in y) => x = y % Two easy theorems set name setTheorems prove e \in {e} qed prove \E x \A e (e \in x <=> e = e1 \/ e = e2) resume by specializing x to insert(e2, {e1}) qed % Theorems about union (proved using extensionality) prove x \union {} = x instantiate y by x \union {} in extensionality qed prove x \union insert(e, y) = insert(e, x \union y) resume by contradiction critical-pairs *Hyp with extensionality qed prove ac \union resume by contradiction critical-pairs *Hyp with extensionality resume by contradiction critical-pairs *Hyp with extensionality qed % Theorems about subset set proof-methods normalization, => prove e \in x /\ x \subseteq y => e \in y by induction on x resume by case ec = e1c complete qed prove x \subseteq y /\ y \subseteq x => x = y prove e \in xc <=> e \in yc by <=> complete complete instantiate x by xc, y by yc in extensionality qed prove (x \union y) \subseteq z <=> x \subseteq z /\ y \subseteq z by induction on x qed % Alternate induction rule prove sort S generated by {}, {__}, \union resume by induction set name lemma critical-pairs *GenHyp with *GenHyp critical-pairs *InductHyp with lemma qed % Two more theorems about subset prove x \subseteq (x \union y) by induction on x using setTheorems qed prove x \subseteq x critical-pairs setTheorems with setTheorems qed