(*
Modelling Chin & Tarski Relation Algebras in dRA
*)
RA = dRA +
consts
le :: "[formula, formula] => prop" ("_ <= _" [6,6] 5)
ge :: "[formula, formula] => prop" ("_ >= _" [6,6] 5)
eq :: "[formula, formula] => prop" ("_ = _" [6,6] 5)
rules
(* definition of equality in terms of sequents *)
eqI "[| A |- B ; B |- A |] ==> A = B"
eqD1 "A = B ==> A |- B"
eqD2 "A = B ==> B |- A"
(*
eqE "[| A = B ; [| A |- B ; B |- A |] ==> PROP R |] ==> PROP R"
*)
(* definition of inequality in terms of equality *)
ledef "A <= B == A & B = A"
(* another definition of inequality in terms of equality *)
gedef "A >= B == A v B = A"
end