% 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