Set Theory and Jechcercises 1

Reading Jech and writing theorems and exercises here.

Reporting any changes I had to make outside of the two new files SetTheory2 and Jechcercises here:

• Type conversion from VariableLabel to LambdaTermTerm (KernelHelpers.scala:205)
• Make sPhi predicate in set theory axioms visible. Instantiation of comprehensionSchema is a pain without it (SetTheoryZAxioms.scala:14). (Is there a better option?)
• Added an Axiom of Infinity (SetTheoryZAxioms.scala)
• Changed SUBPROOF to take its source code info as implicits like most other objects. Otherwise they need to be manually carried during tactic development as well. (BasicStepTactic.scala:1094, ProofsHelpers.scala:37)

Other notes:

• the set intersection and difference proofs are practically identical. I might abstract them into a proof by predicate template of some sort later. Edit: This generic template now exists:

Theorem uniquenessByDefinition := ∃'z. ∀'t. elem('t, 'z) ⇔ 'schemPred('t) ⊢ ∃!'z. ∀'t. elem('t, 'z) ⇔ 'schemPred('t)

There is now a better version as a tactic (thanks @SimonGuilloud for the suggestion):

have(() |- existsOne(z, forall(t, in(t, z) <=> (in(t, x) /\ in(t, y))))) by UniqueComprehension(x, lambda(Seq(t, z), in(t, y)))