feat: tauSTr

[PieterCuijpers]

Separating the series of tau steps from the saturation relation to benefit the definition of branching bisimulation later.

Not sure if this counts as a feat: or refactor:, since it is a relatively small change and should not touch anything outside the scope of the file at the moment.

[PieterCuijpers]

I've updated the file to use #231
Still in doubt a bit on how to use @[grind] correctly.
When do you use "scoped" and which modifier (=, =, ->, .) should I use when?

Also, the naming of theorems is a bit confusing wrt the STr relation.
Do I name a theorem foo_sTr or foo_STr?
I'm personally inclided towards the latter, and tried to use it consistently, but since theorems generally prefer small letters I'm not sure if that is correct.

[chenson2018]

When do you use "scoped"

In CSLib we typically use scoped for almost all grind rules. Note that if this would put something in too deep of a namespace with a regular annotation, you can add it afterwards like attribute [grind] foo. (Soon there will be "grind sets" that make this easier)

which modifier (=, =, ->, .) should I use when?

See this page for a full description of patterns.

Also, the naming of theorems is a bit confusing wrt the STr relation. Do I name a theorem foo_sTr or foo_STr? I'm personally inclided towards the latter, and tried to use it consistently, but since theorems generally prefer small letters I'm not sure if that is correct.

We try to follow the Mathlib naming conventions but I will readily admit these don't come naturally to me for these oddly cased names. I think the relevant rule is:

5. When something named with UpperCamelCase is part of something named with snake_case, it is referenced in lowerCamelCase.

[PieterCuijpers]

See this page for a full description of patterns.

Hm... maybe it is better if I leave out @[grind] altogether for the time being?
I have some incling of the choices I should make, but I also realize that the wrong choice might mess things up thoroughly.

What is better for this PR, just leaving it out, or making an educated guess and hoping you will catch it if its wrong?

[fmontesi]

You can test what grind is doing by using the ? modifier, which will tell you the grind pattern being created. So you can try @[scoped grind? =>], @[scoped grind .], etc. and check what you prefer.