module Examples(examples) where
import FOL
import Text.Html

infixr -->

(-->) :: Formula -> Formula -> Formula
(-->) = Implies


examples :: [(String, Formula)]
examples = [ ("Law of excluded middle",
              (p `Or` Not p)
             )
           , ("Contraposition", 
              ((p-->q)-->(Not q --> Not p)))
           , ("Contradiction",
              p--> (Not p --> q)
             )
            , ("Pierce's law",
               ((p-->q) -->p)-->p
              )
           , ("Distributivity of ∧ over ∨", 
              (p`Or`(q`And`r)) --> ((p`Or`q)`And`(p`Or`r)))
--           , ("Distributivity of ∨ over ∧", 
--              (p`And`(q`Or`r)) --> ((p`And`q)`Or`(p`And`q)))
           , ("Distributivity of ∀ over ⇒",
              Forall "X" (pp "X" --> qq "X") -->
              (Forall "X" (pp "X") --> Forall "X" (qq "X"))
             )
--           , ("Distributivity of ∀ over ∧", 
--                    (Forall "X" ((pp "X")`And`(qq "X"))) --> 
--                    (Forall "X" (pp "X") `And`
--                     Forall "X" (qq "X"))
--             )
           , ("Moving ∃ across ∀",
                Exist "X" (Forall "Y" (Rel "p" [Var "X", Var "Y"])) -->
                Forall "Y" (Exist "X" (Rel "p" [Var "X", Var "Y"]))
             )
           , ("An example of Skolemization",
              (Forall "X" (Exist "Y" (Rel "p" [Var "X", Var "Y"])))
              --> Exist "Y" (Rel "p" [Fun "a" [], Var "Y"])
             )
           ]
    where p = Rel "p" []
          q = Rel "q" []
          r = Rel "r" []
          pp x = Rel "p" [Var x]
          qq x = Rel "q" [Var x]