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 use any
rules that "know" about disjunction. The rule that corresponds to this law of
cases is ∨_elim, which states the law of implication elimination in the sequent
calculus presentation of natural deduction in the usual way (using the
turnstile rather than ⇒ to represent the implications). You can implement your
law of cases using ∨_elim as shown below.
Regards,
Rob.
fun law_of_cases th1 th2 = (* 𝛤 ⊢ p ⇒ r, 𝛥 ⊢ q ⇒ r *)
let val (p, _) = (dest_⇒ o concl) th1;
val (q, _) = (dest_⇒ o concl) th2;
val p_or_q = mk_∨(p, q); (* p ∨ q *)
val th3 = asm_rule p_or_q; (* p ∨ q ⊢ p ∨ q *)
val th4 = undisch_rule th1; (* 𝛤, p ⊢ r,*)
val th5 = undisch_rule th2; (* 𝛥, q ⊢ r *)
val th6 = ∨_elim th3 th4 th5; (* 𝛤, 𝛥, p ∨ q ⊢ r *)
val th7 = disch_rule p_or_q th6; (* 𝛤, 𝛥 ⊢ p ∨ q ⇒ r *)
in th7
end;
val L1 = asm_rule ⌜p ⇒ r⌝;
val L2 = asm_rule ⌜q ⇒ r⌝;
law_of_cases L1 L2;
(*
Result:
val it = p ⇒ r, q ⇒ r ⊢ p ∨ q ⇒ r: THM
*)
> On 31 Mar 2020, at 17:10, David Topham <[email protected]> wrote:
>
> 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
> [email protected]
> http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
_______________________________________________
Proofpower mailing list
[email protected]
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
