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 ∨ q⌝; val L1 = asm_rule ⌜p⇒r⌝; val L2 = asm_rule ⌜q⇒r⌝; law_of_cases L1 L2; =GFT :) val L0 = p ∨ q ⊢ p ∨ q: THM :) val L1 = p ⇒ r ⊢ p ⇒ r: THM :) val L2 = q ⇒ r ⊢ q ⇒ r: THM :) val it = p ⇒ r, q ⇒ r, q ⊢ r: THM
_______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
