57 True_def "True == False-->False" |
57 True_def "True == False-->False" |
58 iff_def "P<->Q == (P-->Q) & (Q-->P)" |
58 iff_def "P<->Q == (P-->Q) & (Q-->P)" |
59 |
59 |
60 (*Quantifiers*) |
60 (*Quantifiers*) |
61 |
61 |
62 allR "(!!x.$H |- $E, P(x), $F) ==> $H |- $E, ALL x.P(x), $F" |
62 allR "(!!x.$H |- $E, P(x), $F) ==> $H |- $E, ALL x. P(x), $F" |
63 allL "$H, P(x), $G, ALL x.P(x) |- $E ==> $H, ALL x.P(x), $G |- $E" |
63 allL "$H, P(x), $G, ALL x. P(x) |- $E ==> $H, ALL x. P(x), $G |- $E" |
64 |
64 |
65 exR "$H |- $E, P(x), $F, EX x.P(x) ==> $H |- $E, EX x.P(x), $F" |
65 exR "$H |- $E, P(x), $F, EX x. P(x) ==> $H |- $E, EX x. P(x), $F" |
66 exL "(!!x.$H, P(x), $G |- $E) ==> $H, EX x.P(x), $G |- $E" |
66 exL "(!!x.$H, P(x), $G |- $E) ==> $H, EX x. P(x), $G |- $E" |
67 |
67 |
68 (*Equality*) |
68 (*Equality*) |
69 |
69 |
70 refl "$H |- $E, a=a, $F" |
70 refl "$H |- $E, a=a, $F" |
71 sym "$H |- $E, a=b, $F ==> $H |- $E, b=a, $F" |
71 sym "$H |- $E, a=b, $F ==> $H |- $E, b=a, $F" |
73 |
73 |
74 |
74 |
75 (*Descriptions*) |
75 (*Descriptions*) |
76 |
76 |
77 The "[| $H |- $E, P(a), $F; !!x.$H, P(x) |- $E, x=a, $F |] ==> |
77 The "[| $H |- $E, P(a), $F; !!x.$H, P(x) |- $E, x=a, $F |] ==> |
78 $H |- $E, P(THE x.P(x)), $F" |
78 $H |- $E, P(THE x. P(x)), $F" |
79 end |
79 end |
80 |
80 |
81 ML |
81 ML |
82 |
82 |
83 val parse_translation = [("@Trueprop",Sequents.two_seq_tr "Trueprop")]; |
83 val parse_translation = [("@Trueprop",Sequents.two_seq_tr "Trueprop")]; |