Rewrite Nat to {x ∈ Int : 0 ≤ x} instead of n ∈ Nat to (n ∈ Int ∧ 0 ≤ n).

[kape1395]

This PR tries to address https://github.com/tlaplus/tlapm/issues/133.

The idea is to rewrite Nat as a value instead of its use in expressions like n ∈ Nat. So expressions like [P -> Nat] are also rewritten. E.g. the following lemma was failing before this change (while the same with a instead of Nat was passing):

lemma
  fixes p :: "c" and f and i
  assumes "f ∈ [p → Nat]" and "i ∈ p"
  shows "f[i] ∈ Nat"
  using assms by auto

All the tests are still passing (tests, community modules, examples repo). The isabelle/examples/AtomicBakeryG.thy example still fails, but now the first error is at line 535 instead of 325.

[muenchnerkindl]

@kape1395 I went over your changes and made some minor changes. For example, I commented out lemma bspec' ''' in SetTheory because it didn't seem to make any difference anymore. Also, I fixed exampleAtomicBakeryG''', which pointed to some missing rewrite rules for symmetric cases etc. Not terribly proud of it (it is slow, and it was never pretty), but at least it works again. At some steps, I had to add bspec''' as a safe elimination rule (elim!''') to make the proof work, which seems to indicate that some more optimization is needed in this respect.

[kape1395]

@muenchnerkindl, @damiendoligez, suddenly, I started getting this error on all the Isabelle invocations, even on the branches that were working previously.

https://github.com/polyml/polyml/blob/90c0dbb2514e1498819da4c14bbeff62481e2149/libpolyml/savestate.cpp#L1141

That timestamp check sounds strange to me, but these lines have been here for 15 years already. Have you seen something similar?

[muenchnerkindl]

@kape1395 I have never seen this. There was a message sent to the Isabelle list about two years ago [1], but it was then retracted, saying it had been sent "in error", so not really helpful.

[1] https://mailman46.in.tum.de/pipermail/isabelle-dev/2022-September/017655.html

[kape1395]

On the error The parent for this saved state does not match or has been changed. I resolved this by removing ~/.isabelle/ on my machine. Probably that's an interference of interactive sessions with the solver's state. Maybe I'll try to set $USER_HOME to the current directory when invoking the Isabelle backend to avoid such a confusion in the future.