David,
I think you got some help with this from Roger off the list. I am replying on
the list in case you still haven't solved your problem.
It looks like you want your law of cases to be a rule that given 훤 ⊢ p ⇒ r and
훥 ⊢ q ⇒ r infers 훤, 훥 ⊢ p ∨ q ⇒ r. Your proposed implementation doesn't
I was hoping this would work for applying the Law of Cases to a proof, but
it adds q to the list of premises.
What could I do to remove that?
=SML
fun law_of_cases th1 th2 =
let
val D⇒ (tm,_) = dest_term (concl th1)
in asm_elim tm (undisch_rule th1)(undisch_rule th2)
end;
val L0 = asm_rule ⌜p ∨
