c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%read "../../meta/sttifol.elf".
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%read "../syntax/prop.elf".
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%read "bool.elf".
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig PLMOD = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include STTIFOLEQ %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include Bool %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder}.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view Base-PLMOD : Base -> PLMOD = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder o := bool.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder ded := [F : bool] ded F eq 1.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder}.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view Truth-PLMOD : Truth -> PLMOD = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include Base-PLMOD.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder true := 1.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder}.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view Falsity-PLMOD : Falsity -> PLMOD = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include Base-PLMOD.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder false := 0.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder}.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view NEG-PLMOD : NEG -> PLMOD = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include Base-PLMOD.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder not := ¬.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder}.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view DISJ-PLMOD : DISJ -> PLMOD = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include Base-PLMOD.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder or := [A][B] A ∨ B.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder}.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view CONJ-PLMOD : CONJ -> PLMOD = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include Base-PLMOD.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder and := [A][B] A ∧ B.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder}.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view IMP-PLMOD : IMP -> PLMOD = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include Base-PLMOD.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder imp := [A][B] A ⇒ B.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder}.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view PL-PLMOD : PL -> PLMOD = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include Base-PLMOD.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include Truth-PLMOD.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include Falsity-PLMOD.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include NEG-PLMOD.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include IMP-PLMOD.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include CONJ-PLMOD.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include DISJ-PLMOD.
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova}.