101 impI "(P ==> Q) ==> P-->Q" |
101 impI "(P ==> Q) ==> P-->Q" |
102 mp "[| P-->Q; P |] ==> Q" |
102 mp "[| P-->Q; P |] ==> Q" |
103 |
103 |
104 (* Definitions *) |
104 (* Definitions *) |
105 |
105 |
106 True_def "True == ((%x::bool.x)=(%x.x))" |
106 True_def "True == ((%x::bool.x)=(%x.x))" |
107 All_def "All == (%P. P = (%x.True))" |
107 All_def "All(P) == (P = (%x.True))" |
108 Ex_def "Ex == (%P. P(@x.P(x)))" |
108 Ex_def "Ex(P) == P(@x.P(x))" |
109 False_def "False == (!P.P)" |
109 False_def "False == (!P.P)" |
110 not_def "not == (%P. P-->False)" |
110 not_def "~ P == P-->False" |
111 and_def "op & == (%P Q. !R. (P-->Q-->R) --> R)" |
111 and_def "P & Q == !R. (P-->Q-->R) --> R" |
112 or_def "op | == (%P Q. !R. (P-->R) --> (Q-->R) --> R)" |
112 or_def "P | Q == !R. (P-->R) --> (Q-->R) --> R" |
113 Ex1_def "Ex1 == (%P. ? x. P(x) & (! y. P(y) --> y=x))" |
113 Ex1_def "Ex1(P) == ? x. P(x) & (! y. P(y) --> y=x)" |
114 Let_def "Let(s, f) == f(s)" |
114 Let_def "Let(s,f) == f(s)" |
115 |
115 |
116 (* Axioms *) |
116 (* Axioms *) |
117 |
117 |
118 iff "(P-->Q) --> (Q-->P) --> (P=Q)" |
118 iff "(P-->Q) --> (Q-->P) --> (P=Q)" |
119 True_or_False "(P=True) | (P=False)" |
119 True_or_False "(P=True) | (P=False)" |
120 |
120 |
121 (* Misc Definitions *) |
121 (* Misc Definitions *) |
122 |
122 |
123 Inv_def "Inv == (%(f::'a=>'b) y. @x. f(x)=y)" |
123 Inv_def "Inv(f::'a=>'b) == (% y. @x. f(x)=y)" |
124 o_def "op o == (%(f::'b=>'c) g (x::'a). f(g(x)))" |
124 o_def "(f::'b=>'c) o g == (%(x::'a). f(g(x)))" |
125 |
125 if_def "if(P,x,y) == @z::'a. (P=True --> z=x) & (P=False --> z=y)" |
126 if_def "if == (%P x y.@z::'a. (P=True --> z=x) & (P=False --> z=y))" |
|
127 |
126 |
128 end |
127 end |
129 |
128 |
130 |
129 |
131 ML |
130 ML |