[isabelle] How do I write the sequent |- P in Isar using theorem


I'm trying to make some connections between logic vocabulary and Isar.

From https://en.wikipedia.org/wiki/Sequent, I get the sentence

   On the other hand an empty antecedent is assumed to be true, i.e.,
   |- Sigma means that Sigma follows without any assumptions...

I'm trying to determine the right connection between sequent assumptions and the meta-logic operator "==>", and how to restate a proved theorem with Isar, THM, to accurately represent the sequent ( |- THM).

Say I have a sequent (A, B |- C), then I'm wanting to say that the following Isar is a correct translation of that sequent:

  assumes A and B
  shows C

For any theorem THM I've proved in Isar, I'm trying to trivially restate it as a sequent, |- THM, but have the restatement have some meaning, not be an exact restatement.

For example, say I prove this:

theorem iffIi_1:
  assumes "A --> B" and "B --> A"
  shows "A =  B"

I'd like to restate the theorem using the identifier iffIi_1, but as I said above, I don't know how, so I restate it like this:

theorem iffIi_2:
  "(A --> B) ==> (B --> A) ==> (A = B)"
by(rule iffIi)

Here, I want to say that this represents the sequent ( |- "(A --> B) ==> (B --> A) ==> (A = B)" ).

I've been thinking that the statements of iffIi_1 and iffIi_2 must be exactly the same, but now I try the following and it doesn't work:

  assumes "A --> B" and "B --> A"
  shows "A = B"
by(rule iffIi)

I had started thinking `assumes "A --> B" and "B --> A"` was synonymous with "(A --> B) ==> (B --> A)".


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.