add `crunches` lifting syntax

[lsf37]

Raf's idea: one thing that is annoying to type in crunches is longer lambda expressions in crunches, e.g. the common pattern

"%s. P (machine_state s)"

We could add syntax for doing this automatically, e.g.

crunches some_fun
  for machine_state: (lift) "machine_state"

to be equivalent to

crunches some_fun
  for machine_state: "%s. P (machine_state s)"

Edit: Raf suggested (lift) instead of (lifted). Bit shorter and I think it fits better.

[lsf37]

And as soon as I was typing this out, it occurred to me that we can easily do this with an input abbreviation. E.g.

abbreviation lifted where "lifted P f == %s. P (f s)"

Maybe lifted is not the best name, and it could also be syntax instead of a function application. Really it's just P o f unfolded, but we do want the unfolded from in Hoare triples. If we go for syntax, it'd have to be an ASCII symbol that is easy to type, otherwise we're not really gaining anything. If we went for lifted, the crunches invocation would be

crunches some_fun
  for machine_state: "lifted P machine_state"

This is still longer than version above, but it would also work in lemmas, e.g. we could write

  "some_fun {| lifted P machine_state |}"

We could of course have both. Raf's original name was P, which is even shorter and would make more sense when the lifted abbreviation exists, e.g.:

crunches some_fun
  for machine_state: (P) "machine_state"

[lsf37]

Potential syntax form: P<machine_state>