equal
deleted
inserted
replaced
104 "" :: case_syn => cases_syn ("_") |
104 "" :: case_syn => cases_syn ("_") |
105 "@case2" :: [case_syn, cases_syn] => cases_syn ("_/ | _") |
105 "@case2" :: [case_syn, cases_syn] => cases_syn ("_/ | _") |
106 |
106 |
107 translations |
107 translations |
108 "x ~= y" == "~ (x = y)" |
108 "x ~= y" == "~ (x = y)" |
109 "@ x.b" == "Eps (%x. b)" |
109 "@ x. b" == "Eps (%x. b)" |
110 "ALL xs. P" => "! xs. P" |
110 "ALL xs. P" => "! xs. P" |
111 "EX xs. P" => "? xs. P" |
111 "EX xs. P" => "? xs. P" |
112 "EX! xs. P" => "?! xs. P" |
112 "EX! xs. P" => "?! xs. P" |
113 "_Let (_binds b bs) e" == "_Let b (_Let bs e)" |
113 "_Let (_binds b bs) e" == "_Let b (_Let bs e)" |
114 "let x = a in e" == "Let a (%x. e)" |
114 "let x = a in e" == "Let a (%x. e)" |
147 |
147 |
148 (* Basic Rules *) |
148 (* Basic Rules *) |
149 |
149 |
150 refl "t = (t::'a)" |
150 refl "t = (t::'a)" |
151 subst "[| s = t; P(s) |] ==> P(t::'a)" |
151 subst "[| s = t; P(s) |] ==> P(t::'a)" |
152 ext "(!!x::'a. (f(x)::'b) = g(x)) ==> (%x.f(x)) = (%x.g(x))" |
152 ext "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)" |
153 selectI "P(x::'a) ==> P(@x.P(x))" |
153 selectI "P (x::'a) ==> P (@x. P x)" |
154 |
154 |
155 impI "(P ==> Q) ==> P-->Q" |
155 impI "(P ==> Q) ==> P-->Q" |
156 mp "[| P-->Q; P |] ==> Q" |
156 mp "[| P-->Q; P |] ==> Q" |
157 |
157 |
158 defs |
158 defs |
159 |
159 |
160 True_def "True == ((%x::bool.x)=(%x.x))" |
160 True_def "True == ((%x::bool. x) = (%x. x))" |
161 All_def "All(P) == (P = (%x.True))" |
161 All_def "All(P) == (P = (%x. True))" |
162 Ex_def "Ex(P) == P(@x.P(x))" |
162 Ex_def "Ex(P) == P(@x. P(x))" |
163 False_def "False == (!P.P)" |
163 False_def "False == (!P. P)" |
164 not_def "~ P == P-->False" |
164 not_def "~ P == P-->False" |
165 and_def "P & Q == !R. (P-->Q-->R) --> R" |
165 and_def "P & Q == !R. (P-->Q-->R) --> R" |
166 or_def "P | Q == !R. (P-->R) --> (Q-->R) --> R" |
166 or_def "P | Q == !R. (P-->R) --> (Q-->R) --> R" |
167 Ex1_def "Ex1(P) == ? x. P(x) & (! y. P(y) --> y=x)" |
167 Ex1_def "Ex1(P) == ? x. P(x) & (! y. P(y) --> y=x)" |
168 |
168 |