我正在尝试[] |- p /\ q <=> q /\ p :thm
使用带有 HOL 推理规则的 SML 来证明该定理。这是 SML 代码:
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;
上述代码的结果产生:
val thm8 = [(p :bool), (q :bool)] |- (q :bool) /\ (p :bool) <=> p /\ q: thm
我究竟做错了什么?