{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE MultiParamTypeClasses #-}

-- |

-- Module      : OAlg.Structure.Lattice.Proposition

-- Description : propositions on lattices.

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

-- 

-- propositions on lattices.

module OAlg.Structure.Lattice.Proposition
  ( -- * Lattice

    prpLattice, prpLatticeDisjunction, prpLatticeConjunction

    -- * Erasable Lattice

  -- , prpErasableLattice


    -- * Bool

  , prpLatticeBool

  )
  where

import OAlg.Prelude

import OAlg.Structure.Oriented.Opposite
import OAlg.Structure.PartiallyOrdered
import OAlg.Structure.Lattice.Definition

--------------------------------------------------------------------------------

-- prpLatticeDisjunction -


-- | validity of disjunction in a lattice.

prpLatticeDisjunction :: (Lattice a, Show a) => a -> a -> a -> Statement
prpLatticeDisjunction :: forall a. (Lattice a, Show a) => a -> a -> a -> Statement
prpLatticeDisjunction a
a a
b a
c = String -> Label
Label String
"LatticeDisjunction" Label -> Statement -> Statement
:<=>:
  [Statement] -> Statement
And [ String -> Label
Label String
"a <<= (a || b)"
          Label -> Statement -> Statement
:<=>: (a
a a -> a -> Bool
forall a. PartiallyOrdered a => a -> a -> Bool
<<= a
ab) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"a"String -> String -> Parameter
:=a -> String
forall a. Show a => a -> String
show a
a,String
"b"String -> String -> Parameter
:=a -> String
forall a. Show a => a -> String
show a
b]
      , String -> Label
Label String
"b <<= (a || b)"
          Label -> Statement -> Statement
:<=>: (a
b a -> a -> Bool
forall a. PartiallyOrdered a => a -> a -> Bool
<<= a
ab) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"a"String -> String -> Parameter
:=a -> String
forall a. Show a => a -> String
show a
a,String
"b"String -> String -> Parameter
:=a -> String
forall a. Show a => a -> String
show a
b]
      , String -> Label
Label String
"(a <<= z) && (b <<= z) ~> (a || b) <<= z"
        Label -> Statement -> Statement
:<=>:     (((a
a a -> a -> Bool
forall a. PartiallyOrdered a => a -> a -> Bool
<<= a
z) Bool -> Bool -> Bool
forall a. Logical a => a -> a -> a
&& (a
b a -> a -> Bool
forall a. PartiallyOrdered a => a -> a -> Bool
<<= a
z)) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"a"String -> String -> Parameter
:=a -> String
forall a. Show a => a -> String
show a
a,String
"b"String -> String -> Parameter
:=a -> String
forall a. Show a => a -> String
show a
b,String
"z"String -> String -> Parameter
:=a -> String
forall a. Show a => a -> String
show a
z])
              Statement -> Statement -> Statement
:=> (a
ab a -> a -> Bool
forall a. PartiallyOrdered a => a -> a -> Bool
<<= a
z) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"a"String -> String -> Parameter
:=a -> String
forall a. Show a => a -> String
show a
a,String
"b"String -> String -> Parameter
:=a -> String
forall a. Show a => a -> String
show a
b,String
"z"String -> String -> Parameter
:=a -> String
forall a. Show a => a -> String
show a
z]
      ]
  where ab :: a
ab = a
a a -> a -> a
forall a. Logical a => a -> a -> a
|| a
b
        z :: a
z  = a
ab a -> a -> a
forall a. Logical a => a -> a -> a
|| a
c

--------------------------------------------------------------------------------

-- prpLatticeConjunction -


-- | validity of conjunction in a lattice.

prpLatticeConjunction :: (Lattice a, Show a) => a -> a -> a -> Statement
prpLatticeConjunction :: forall a. (Lattice a, Show a) => a -> a -> a -> Statement
prpLatticeConjunction a
a a
b a
c = String -> Label
Label String
"LatticeConjunction" Label -> Statement -> Statement
:<=>:
  Op a -> Op a -> Op a -> Statement
forall a. (Lattice a, Show a) => a -> a -> a -> Statement
prpLatticeDisjunction (a -> Op a
forall x. x -> Op x
Op a
a) (a -> Op a
forall x. x -> Op x
Op a
b) (a -> Op a
forall x. x -> Op x
Op a
c)

--------------------------------------------------------------------------------

-- prpLattice -


-- | validity of a lattice.

prpLattice :: (Lattice a,Show a) => X a -> Statement
prpLattice :: forall a. (Lattice a, Show a) => X a -> Statement
prpLattice X a
xa = String -> Label
Prp String
"Lattice" Label -> Statement -> Statement
:<=>:
  [Statement] -> Statement
And [ X (a, a, a) -> ((a, a, a) -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (a, a, a)
xaaa
          (\(a
a,a
b,a
c) -> [Statement] -> Statement
And [ a -> a -> a -> Statement
forall a. (Lattice a, Show a) => a -> a -> a -> Statement
prpLatticeDisjunction a
a a
b a
c
                           , a -> a -> a -> Statement
forall a. (Lattice a, Show a) => a -> a -> a -> Statement
prpLatticeConjunction a
a a
b a
c
                           ]
          )
      ]
  where xaaa :: X (a, a, a)
xaaa = X a -> X a -> X a -> X (a, a, a)
forall a b c. X a -> X b -> X c -> X (a, b, c)
xTupple3 X a
xa X a
xa X a
xa

--------------------------------------------------------------------------------

-- prpLatticeBool -


-- | validity of 'Bool as a erasable lattice

prpLatticeBool :: Statement
prpLatticeBool :: Statement
prpLatticeBool = String -> Label
Prp String
"LatticeBool" Label -> Statement -> Statement
:<=>: X Bool -> Statement
forall a. (Lattice a, Show a) => X a -> Statement
prpLattice X Bool
xBool