17 |
17 |
18 arities |
18 arities |
19 o :: logic |
19 o :: logic |
20 |
20 |
21 consts |
21 consts |
22 True,False :: "o" |
22 True,False :: "o" |
23 "=" :: "['a,'a] => o" (infixl 50) |
23 "=" :: "['a,'a] => o" (infixl 50) |
24 "Not" :: "o => o" ("~ _" [40] 40) |
24 "Not" :: "o => o" ("~ _" [40] 40) |
25 "&" :: "[o,o] => o" (infixr 35) |
25 "&" :: "[o,o] => o" (infixr 35) |
26 "|" :: "[o,o] => o" (infixr 30) |
26 "|" :: "[o,o] => o" (infixr 30) |
27 "-->","<->" :: "[o,o] => o" (infixr 25) |
27 "-->","<->" :: "[o,o] => o" (infixr 25) |
28 The :: "('a => o) => 'a" (binder "THE " 10) |
28 The :: "('a => o) => 'a" (binder "THE " 10) |
29 All :: "('a => o) => o" (binder "ALL " 10) |
29 All :: "('a => o) => o" (binder "ALL " 10) |
30 Ex :: "('a => o) => o" (binder "EX " 10) |
30 Ex :: "('a => o) => o" (binder "EX " 10) |
31 |
31 |
32 (*Representation of sequents*) |
32 (*Representation of sequents*) |
33 Trueprop :: "[sobj=>sobj,sobj=>sobj] => prop" |
33 Trueprop :: "[sobj=>sobj,sobj=>sobj] => prop" |
34 Seqof :: "o => sobj=>sobj" |
34 Seqof :: "o => sobj=>sobj" |
35 "@Trueprop" :: "[sequence,sequence] => prop" ("((_)/ |- (_))" [6,6] 5) |
35 "@Trueprop" :: "[sequence,sequence] => prop" ("((_)/ |- (_))" [6,6] 5) |
36 "@MtSeq" :: "sequence" ("" [] 1000) |
36 "@MtSeq" :: "sequence" ("" [] 1000) |
37 "@NmtSeq" :: "[seqobj,seqcont] => sequence" ("__" [] 1000) |
37 "@NmtSeq" :: "[seqobj,seqcont] => sequence" ("__" [] 1000) |
38 "@MtSeqCont" :: "seqcont" ("" [] 1000) |
38 "@MtSeqCont" :: "seqcont" ("" [] 1000) |
39 "@SeqCont" :: "[seqobj,seqcont] => seqcont" (",/ __" [] 1000) |
39 "@SeqCont" :: "[seqobj,seqcont] => seqcont" (",/ __" [] 1000) |
40 "" :: "o => seqobj" ("_" [] 1000) |
40 "" :: "o => seqobj" ("_" [] 1000) |
41 "@SeqId" :: "id => seqobj" ("$_" [] 1000) |
41 "@SeqId" :: "id => seqobj" ("$_" [] 1000) |
42 "@SeqVar" :: "var => seqobj" ("$_") |
42 "@SeqVar" :: "var => seqobj" ("$_") |
43 |
43 |
44 rules |
44 rules |
45 (*Structural rules*) |
45 (*Structural rules*) |
46 |
46 |
47 basic "$H, P, $G |- $E, P, $F" |
47 basic "$H, P, $G |- $E, P, $F" |
48 |
48 |
49 thinR "$H |- $E, $F ==> $H |- $E, P, $F" |
49 thinR "$H |- $E, $F ==> $H |- $E, P, $F" |
50 thinL "$H, $G |- $E ==> $H, P, $G |- $E" |
50 thinL "$H, $G |- $E ==> $H, P, $G |- $E" |
51 |
51 |
52 cut "[| $H |- $E, P; $H, P |- $E |] ==> $H |- $E" |
52 cut "[| $H |- $E, P; $H, P |- $E |] ==> $H |- $E" |
53 |
53 |
54 (*Propositional rules*) |
54 (*Propositional rules*) |
55 |
55 |
56 conjR "[| $H|- $E, P, $F; $H|- $E, Q, $F |] ==> $H|- $E, P&Q, $F" |
56 conjR "[| $H|- $E, P, $F; $H|- $E, Q, $F |] ==> $H|- $E, P&Q, $F" |
57 conjL "$H, P, Q, $G |- $E ==> $H, P & Q, $G |- $E" |
57 conjL "$H, P, Q, $G |- $E ==> $H, P & Q, $G |- $E" |
58 |
58 |
59 disjR "$H |- $E, P, Q, $F ==> $H |- $E, P|Q, $F" |
59 disjR "$H |- $E, P, Q, $F ==> $H |- $E, P|Q, $F" |
60 disjL "[| $H, P, $G |- $E; $H, Q, $G |- $E |] ==> $H, P|Q, $G |- $E" |
60 disjL "[| $H, P, $G |- $E; $H, Q, $G |- $E |] ==> $H, P|Q, $G |- $E" |
61 |
61 |
62 impR "$H, P |- $E, Q, $F ==> $H |- $E, P-->Q, $F" |
62 impR "$H, P |- $E, Q, $F ==> $H |- $E, P-->Q, $F" |
63 impL "[| $H,$G |- $E,P; $H, Q, $G |- $E |] ==> $H, P-->Q, $G |- $E" |
63 impL "[| $H,$G |- $E,P; $H, Q, $G |- $E |] ==> $H, P-->Q, $G |- $E" |
64 |
64 |
65 notR "$H, P |- $E, $F ==> $H |- $E, ~P, $F" |
65 notR "$H, P |- $E, $F ==> $H |- $E, ~P, $F" |
66 notL "$H, $G |- $E, P ==> $H, ~P, $G |- $E" |
66 notL "$H, $G |- $E, P ==> $H, ~P, $G |- $E" |
67 |
67 |
68 FalseL "$H, False, $G |- $E" |
68 FalseL "$H, False, $G |- $E" |
69 |
69 |
70 True_def "True == False-->False" |
70 True_def "True == False-->False" |
71 iff_def "P<->Q == (P-->Q) & (Q-->P)" |
71 iff_def "P<->Q == (P-->Q) & (Q-->P)" |
72 |
72 |
73 (*Quantifiers*) |
73 (*Quantifiers*) |
74 |
74 |
75 allR "(!!x.$H |- $E, P(x), $F) ==> $H |- $E, ALL x.P(x), $F" |
75 allR "(!!x.$H |- $E, P(x), $F) ==> $H |- $E, ALL x.P(x), $F" |
76 allL "$H, P(x), $G, ALL x.P(x) |- $E ==> $H, ALL x.P(x), $G |- $E" |
76 allL "$H, P(x), $G, ALL x.P(x) |- $E ==> $H, ALL x.P(x), $G |- $E" |
77 |
77 |
78 exR "$H |- $E, P(x), $F, EX x.P(x) ==> $H |- $E, EX x.P(x), $F" |
78 exR "$H |- $E, P(x), $F, EX x.P(x) ==> $H |- $E, EX x.P(x), $F" |
79 exL "(!!x.$H, P(x), $G |- $E) ==> $H, EX x.P(x), $G |- $E" |
79 exL "(!!x.$H, P(x), $G |- $E) ==> $H, EX x.P(x), $G |- $E" |
80 |
80 |
81 (*Equality*) |
81 (*Equality*) |
82 |
82 |
83 refl "$H |- $E, a=a, $F" |
83 refl "$H |- $E, a=a, $F" |
84 sym "$H |- $E, a=b, $F ==> $H |- $E, b=a, $F" |
84 sym "$H |- $E, a=b, $F ==> $H |- $E, b=a, $F" |
85 trans "[| $H|- $E, a=b, $F; $H|- $E, b=c, $F |] ==> $H|- $E, a=c, $F" |
85 trans "[| $H|- $E, a=b, $F; $H|- $E, b=c, $F |] ==> $H|- $E, a=c, $F" |
86 |
86 |
87 |
87 |
88 (*Descriptions*) |
88 (*Descriptions*) |