Cross Reference: /hets/Framework/specs/logics/propositional/model_theory/propmod.elf
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
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}.