2

I am trying to prove the theorem [] |- p /\ q <=> q /\ p :thm using SML with HOL Inference Rules. Here's the SML code:

val thm1 = ASSUME ``p:bool /\ q:bool``;
val thm2 = ASSUME ``p:bool``;
val thm3 = ASSUME ``q:bool``;
val thm4 = CONJ thm2 thm3;
val thm5 = CONJ thm3 thm2;
val thm6 = DISCH ``(q:bool/\p:bool)`` thm4;
val thm7 = DISCH ``(p:bool/\q:bool)`` thm5;
val thm8 = IMP_ANTISYM_RULE thm6 thm7;

The result of the above code produces :

val thm8 =  [(p :bool), (q :bool)] |- (q :bool) /\ (p :bool) <=> p /\ q: thm

What am I doing wrong?

Ionuț G. Stan
  • 176,118
  • 18
  • 189
  • 202
Tuffie
  • 71
  • 2

1 Answers1

1

The problem with your final theorem is that you still have p and q as assumptions, introduced via thm2 and thm3, whereas you can and should obtain them from thm1.

The first theorem you need is something like p /\ q ==> p. I found the appropriate rule by skimming through the description (sec. 2.3.24). It's called CONJUNCT1.

Using it, we can obtain p as a theorem from thm1:

val thmp = CONJUNCT1 thm1;

The same idea works to get q as a theorem from thm1:

val thmq = CONJUNCT2 thm1;

And then you can apply your idea for thm5:

val thm5 = CONJ thmq thmp;

The important thing here is that we do not use p derived from p (thm2) and q derived from q (thm3) but rather p derived from p /\ q and q derived from p /\ q (setting show_assumes := true; may help to see this more clearly).

Finally, we apply your idea for thm7:

val thm7 = DISCH ``p /\ q`` thm5;

to obtain the first half of the desired result, but with no extraneous assumptions.

The second half is obtained in a similar way:

val thm9 = ASSUME (``q /\ p``);
val thmp2 = CONJUNCT2 thm9;
val thmq2 = CONJUNCT1 thm9;
val thm6 =  DISCH ``q /\ p`` (CONJ thmp2 thmq2);

And then your idea for thm8 works perfectly:

val thm8 = IMP_ANTISYM_RULE thm7 thm6;
tbrk
  • 1,290
  • 1
  • 13
  • 20