Instantiating axioms about Sequents explicitly

Note: This is a re-asking of the second question here, which turned out to be less related to the first question (answered there) than I thought it would.

Consider the following minimal development based on the Isabelle Sequents library:

theory Test
  imports Pure Sequents.Sequents
begin

syntax "_Trueprop"    :: "two_seqe" ("((_)/ ⊢ (_))" [6,6] 5)
consts Trueprop :: two_seqi
parse_translation ‹[  (@{syntax_const "_Trueprop"}, K (two_seq_tr @{const_syntax Trueprop}))  ]›
print_translation ‹[  (@{const_syntax Trueprop}, K (two_seq_tr' @{syntax_const "_Trueprop"}))  ]›

axiomatization where
  xch : "⋀A B C D. $A, $B, $C ⊢ $D  ⟹  $C, $B, $A ⊢ $D"

lemma xch0 : "$A, $C ⊢ $D  ⟹  $C, $A ⊢ $D"
  apply (rule xch[of A _ C D] ; assumption)  done

lemma xch1 : "$A, P, $C ⊢ $D  ⟹  $C, P, $A ⊢ $D"
  apply (rule xch[of A _ C D] ; assumption)  done

lemma xch2 : "$A, P, Q, $C ⊢ $D  ⟹  $C, P, Q, $A ⊢ $D"
  apply (rule xch[of A _ C D] ; assumption)  done

These proofs work (in fact, they work even without the of annotations). However, I want to know what I could write in place of the _s to be maximally explicit. That is, how do I write "the empty sequence" or "the sequence containing only P" or "the sequence containing only P, Q"? It doesn't work to write "" for xch0, nor P or "P" for xch1, nor "P, Q" for xch2, and I can't figure out from the source of Sequents what explicit syntax these notations are abbreviations for.

Solution

The sequences on the left hand side of ⊢ are internally represented as function applications. This ensures that higher-order unification can instantiate schematic variables in theorems with arbitrarily many consecutive elements. So $A, $B, $C ⊢ $D are interally represented as Trueprop (%s. A (B (C s))) (%s. D s).

So in your first lemma, B gets instantiated by the identity function %x. x.

Individual elements of object type o are transformed into this applicative format using the constant SeqO' and Seq1' declared at the start of the Sequents theory. The $ marker indicates that the parser should not insert such a constant.

So in your second lemma, B is instantiated with SeqO'(P). In the third lemma, B must be instantiated with the sequence of P and Q, which is expressed represented by %s. SeqO'(P, SeqO'(Q, s)). The notations <<P>> and <<P, Q>> denote the same and are preferable.

You can look at the internal representation of a sequent using Isabelle/ML via

ML {* @term{"$A, P, $C ⊢ $D"} *}

That's how I figured out what was going on.