Issue title: [KIP] - kprove should use the `claim` keyword
 Issue body: Introduce a new keyword in K called `claim` which is used to mark things that are to be proved, in anticipation of having claims not just in one module.

```
claim <k> LHS => RHS ... </k>
```

How should `kompile` treat `claim`:

-  Ignore them: 
-  Prove them at `kompile` time: 1
-  Treat them as semantic (trusted) rules: 
-  Error: 11111

Will treat as error.

How should `kprove` treat `rule` declared _outside_ the main module and _not_ on a simplification rule:

-   Ignore: 
-   Error: 1
-   Deprecation warning: 1111
-   Trusted claim: 

We'll use a deprecation warning then, saying that they should replace `rule` with `claim` (haskell backend already knows the `trusted` keyword, so that can continue working with the `claim` keyword).
 Comments: 
 Comment 0: Basically, what this entails:

* Create a new `Claim` class in outer.scala
* Modify the outer parser to parse claim-type bubbles
* Modify the inner parser to convert claim-type bubbles into `Claim` objects.
* Remove the `specificationSteps` method and modify the kompile pipeline so that it supports the `Claim` class and applies the relevant specification steps to claims.
* Insert a check in kompile that reports an error if the user puts a claim in a definition.
* Disable this check in the kprove pipeline
* Insert a check in the kprove pipeline that looks for `Rule` objects in the specification module that do not have the simplification attribute, and report a deprecation warning.
* Kprove treats `Rule` and `Claim` the same for now.
 Comment 1: How do I differentiate between modules from the spec files and the definition files?
The spec files include the definition and now I'm giving warning messages for all rules.
I'm asking about the broad picture: where do you see the line between the spec files and the definition?
 Comment 2: Anything imported by the main spec module but not imported by the main module of the definition that was kompiled should be considered a spec module.
 Comment 3: @radumereuta: What is SpecificationStep supposed to do? It compiles a claim, it should be the same for any claim, but is different for Java/Haskell backend. @dwightguth: remove this, in favor of just having each Kompilation step decide how to handle rules/claims different (since we will now have separate Rule/Claim classes which the Kompilation classes can look at). Pass at very beginning of Kompilation process which transforms certain rules into claims if they are the deprecated cases discussed above (and emit the warnings).

@radumereuta how long to kompile K? @dwightguth takes a minute or two the first time with `-Dhaskell.backend.skip` and `-DskipTests`. Don't delete Haskell backend build products and it should be OK to run quickly.
{'source': 'GithubIssues', 'repo_name_with_owner': 'runtimeverification/k', 'issue_id': 658413887, 'repo_stars': 325.0}