Isar: Failed to retrieve literal fact

Question

I have the following code:

    assume H: "x ≠ xa ∧ x ∈ elems xs" (is "?H1 ∧ ?H2")
    hence "?H1" and "?H2" by auto
    from Cons.IH[OF `?H2` ] have 1: "∃ys zs. xs = ys @ x # zs ∧ x ∉ elems ys" by simp
    then obtain ys zs where 2: "xs = ys @ x # zs ∧ x ∉ elems ys" (is "?C1 ∧ ?C2") by blast
    hence "?C1" and "?C2" by auto
    from `?C1` have R1: "xa # xs = (xa # ys) @ x # zs" by simp
    from `x ≠ xa` and `x ∉ elems ys` have R2: "x ∉ elems (xa#ys)" by auto
    from R1 R2 show ?case by blast

Without the lines : hence "?H1" and "?H2" by auto and hence "?C1" and "?C2" by auto I cannot refer to the literal facts `?C1` and `?H2`. (I also cannot refer to the terms the "unkowns/abbreviations/metavariables/" ?<name> expand to; I get the same error. The metavariables are actually expanded to the literal facts they refer to in the error message (e.g. for `?H2` I get

Failed to retrieve literal fact⌂:
x ∈ elems xs

, so they must be in scope somehow??)

My question is:

• Why does this not work?
• is there a better workaround than my hence … by auto?

Answer 1

Expanding on Javier's comment, the (is "?H1 ∧ ?H2") creates two macro variables. Those are in scope, such as is ?case for instance. ?H1 and ?H2 refer to the terms x ≠ xa and x ∈ elems xs, but this does not mean that they are proven facts. What changes, are the term bindings, as you can inspect by:

assume H: "x ≠ xa ∧ x ∈ elems xs" (is "?H1 ∧ ?H2")
print_term_bindings
>>>>
?H1 ≡ ¬ x = xa
?H2 ≡ x ∈ elems xs
...

print_facts
>>>>
H: x ≠ xa ∧ x ∈ elems xs
...

Your snippet is just a sugared way of writing:

assume H: "x ≠ xa ∧ x ∈ elems xs"
hence "x ≠ xa" and "x ∈ elems xs" by auto
from Cons.IH[OF `x ∈ elems xs`] have 1: "∃ys zs. xs = ys @ x # zs ∧ x ∉ elems ys" by simp
then obtain ys zs where 2: "xs = ys @ x # zs ∧ x ∉ elems ys" by blast
hence "xs = ys @ x # zs" and "x ∉ elems ys" by auto
from `xs = ys @ x # zs` have R1: "xa # xs = (xa # ys) @ x # zs" by simp
from `x ≠ xa` and `x ∉ elems ys` have R2: "x ∉ elems (xa#ys)" by auto
from R1 R2 show [whatever ?case expands to] by blast

Clearly, this proof does not work if you drop the line hence "x ≠ xa" and "x ∈ elems xs" by auto, which proves the literal fact x ∈ elems xs. Without it, Isabelle cannot accept Cons.IH[OF `x ∈ elems xs`], which causes the error you cite.

Regarding the question of how to write an equivalent proof without the need for hence … by auto: You can't, really. There needs to be some proof that the conjuncts are facts.

The most lightweight way to refer to sub-conjuncts of facts as facts is with conjunct1/2[OF ...]: Just write from Cons.IH[OF conjunct2[OF H]] have... instead of from Cons.IH[OF `?H2`] have....

However, what you are emulating here through term bindings is actually the “array” feature of Isabelle's facts.

If one writes a fact as a chain of sub-facts H: ‹x ≠ xa› ‹x ∈ elems xs› instead of H: ‹x ≠ xa ∧ x ∈ elems xs›, one can afterwards refer to the first part as H(1) and to the second one as H(2). In your example, one would have to slightly adapt the surrounding proof (using safe or clarify) in order for the changed assumption to be okay. It would then read something like:

proof (..., safe)
  assume H: "x ≠ xa" "x ∈ elems xs"
  from Cons.IH[OF H(2)] have 1: "∃ys zs. xs = ys @ x # zs ∧ x ∉ elems ys" by simp
  then obtain ys zs where C: "xs = ys @ x # zs" "x ∉ elems ys" by blast
  from C(1) have R1: "xa # xs = (xa # ys) @ x # zs" by simp
  from `x ≠ xa` and `x ∉ elems ys` have R2: "x ∉ elems (xa#ys)" by auto
  from R1 R2 show ?case by blast
next ...

No macros for literal-fact names or unpacking needed!

My general experience is that there are very limited reasons to use the macros for naming literal facts when you can use the conventional naming of facts. Even more generally, most of the time when one can express a conjunction or an implication at the meta level, opting for meta will make life easier: assumes P: "a" "b" shows "c" is more handy than shows "a /\ b ==> c".