[isabelle-dev] Circular reasoning via multithreading seems too easy

[Lars Hupel]

> Tending global state (normally via Synchronized.var and not the raw
> Unsynchronized.ref) has been part of the normal routine of Isabelle
> maintenance in the last 10 years. At the beginning almost nothing
> worked, but around 2008/2009 it became routine. Today we have a fairly
> robust system, with lots of user tools that are mostly thread-safe.

For whatever it's worth, here's the same example with "Synchronized.var"
and without a data race:

ML‹
  fun get_some var =
    case Synchronized.value var of
      NONE => (@{print} "defer"; get_some var)
    | SOME v => v

  fun set var x =
    Synchronized.change var (K x)

  val thm: thm option Synchronized.var = Synchronized.var "hello" NONE;

  val _ =
    set thm (SOME
      (Goal.prove_future @{context} [] [] @{prop "False"}
        (fn {context, ...} =>
          ALLGOALS (resolve_tac context [get_some thm]))))
›

lemma F: False
  by (tactic ‹resolve_tac @{context} [get_some thm] 1›)