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 "not == (%P. P-->False)" |
111 and_def "op & = (%P Q. !R. (P-->Q-->R) --> R)" |
111 and_def "op & == (%P Q. !R. (P-->Q-->R) --> R)" |
112 or_def "op | = (%P Q. !R. (P-->R) --> (Q-->R) --> R)" |
112 or_def "op | == (%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 "op o == (%(f::'b=>'c) g (x::'a). f(g(x)))" |
125 |
125 |
126 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 |
127 |
128 end |
128 end |
129 |
129 |
130 |
130 |
131 ML |
131 ML |