[Merged by Bors] - fix(ModelTheory): make some defs into abbrevs

[ChrisHughes24]

---

Formula is currently an abbreviation for BoundedFormula. There were some definitions like not which were defined on both BoundedFormula and Formula, and I have made the Formula versions into abbrev so there is no need to duplicate simp lemmas.

A concrete advantage of this PR is that the following lemma is proved by simp with the lemma Formula.realize_not where it wasn't before.

example (φ : L.Formula α) (v : α → M) :
    Formula.Realize (∼ φ) v ↔ ¬φ.Realize v := by
  simp

[ADedecker]

Is there a reason not to delete the simp lemmas that you are talking about in this PR? E.g FirstOrder.Language.Formula.realize_not if I understand correctly?

Otherwise LGTM

bors d+

[bors]

✌️ ChrisHughes24 can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[ChrisHughes24]

The issue is that the simp lemmas didn't trigger because there were two definitions of not on Formula, both BoundedFormula.not and Formula.not, which are equal, and since Formula is reducible it's easy to end up with the wrong one. So the lemmas stand, but I did make a mistake in my description and I should have written Formula.realize_not instead of Sentence.realize_not

[ChrisHughes24]

bors merge

[ADedecker]

Ah right I understand now. Thanks!

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style