Posted: Apr 03, 2012 10:04 am
by mizvekov
Still working on that goddamn example! :grin:
By the way, I found that having a theorem and a function like this helps a lot:
Code: Select all
-- |- (p ==> q) ==> (q ==> r) ==> p ==> r
hs :: Theorem String
hs = let
   step1  = Assume p
   step2  = Assume $ p :=>: q
   step3  = MP step2 step1
   step4  = Assume $ q :=>: r
   step5  = MP step4 step3
   step6  = discharge p step5
   step7  = discharge (q :=>: r) step6
   in verify step7

hyp_sylo :: Proof -> Proof -> Proof
hyp_sylo a b = let
   aT = concl a
   bT = concl b
   in case aT of
      p :=>: q1 ->
         case bT of
            q2 :=>: r ->
               if (q1 == q2) then
                  let step1 = matchMP (instL [p, q1, r] hs) a
                  in MP step1 b
               else error "hyp_sylo unmatched"
            _ -> error "hyp_sylo second"
      _ -> error "hyp_sylo first"

Am I on the right track here? :)