35 If :: "[bool, 'a, 'a] => 'a" ("(if (_)/ then (_)/ else (_))" 10) |
34 If :: "[bool, 'a, 'a] => 'a" ("(if (_)/ then (_)/ else (_))" 10) |
36 arbitrary :: 'a |
35 arbitrary :: 'a |
37 |
36 |
38 (* Binders *) |
37 (* Binders *) |
39 |
38 |
40 Eps :: "('a => bool) => 'a" |
|
41 The :: "('a => bool) => 'a" |
39 The :: "('a => bool) => 'a" |
42 All :: "('a => bool) => bool" (binder "ALL " 10) |
40 All :: "('a => bool) => bool" (binder "ALL " 10) |
43 Ex :: "('a => bool) => bool" (binder "EX " 10) |
41 Ex :: "('a => bool) => bool" (binder "EX " 10) |
44 Ex1 :: "('a => bool) => bool" (binder "EX! " 10) |
42 Ex1 :: "('a => bool) => bool" (binder "EX! " 10) |
45 Let :: "['a, 'a => 'b] => 'b" |
43 Let :: "['a, 'a => 'b] => 'b" |
77 abs :: "'a::minus => 'a" |
75 abs :: "'a::minus => 'a" |
78 inverse :: "'a::inverse => 'a" |
76 inverse :: "'a::inverse => 'a" |
79 divide :: "['a::inverse, 'a] => 'a" (infixl "'/" 70) |
77 divide :: "['a::inverse, 'a] => 'a" (infixl "'/" 70) |
80 |
78 |
81 syntax (xsymbols) |
79 syntax (xsymbols) |
82 abs :: "'a::minus => 'a" ("\<bar>_\<bar>") |
80 abs :: "'a::minus => 'a" ("\\<bar>_\\<bar>") |
83 syntax (HTML output) |
81 syntax (HTML output) |
84 abs :: "'a::minus => 'a" ("\<bar>_\<bar>") |
82 abs :: "'a::minus => 'a" ("\\<bar>_\\<bar>") |
85 |
83 |
86 axclass plus_ac0 < plus, zero |
84 axclass plus_ac0 < plus, zero |
87 commute: "x + y = y + x" |
85 commute: "x + y = y + x" |
88 assoc: "(x + y) + z = x + (y + z)" |
86 assoc: "(x + y) + z = x + (y + z)" |
89 zero: "0 + x = x" |
87 zero: "0 + x = x" |
114 "" :: "case_syn => cases_syn" ("_") |
111 "" :: "case_syn => cases_syn" ("_") |
115 "_case2" :: "[case_syn, cases_syn] => cases_syn" ("_/ | _") |
112 "_case2" :: "[case_syn, cases_syn] => cases_syn" ("_/ | _") |
116 |
113 |
117 translations |
114 translations |
118 "x ~= y" == "~ (x = y)" |
115 "x ~= y" == "~ (x = y)" |
119 "SOME x. P" == "Eps (%x. P)" |
|
120 "THE x. P" == "The (%x. P)" |
116 "THE x. P" == "The (%x. P)" |
121 "_Let (_binds b bs) e" == "_Let b (_Let bs e)" |
117 "_Let (_binds b bs) e" == "_Let b (_Let bs e)" |
122 "let x = a in e" == "Let a (%x. e)" |
118 "let x = a in e" == "Let a (%x. e)" |
123 |
119 |
124 syntax ("" output) |
120 syntax ("" output) |
125 "op =" :: "['a, 'a] => bool" ("(_ =/ _)" [51, 51] 50) |
121 "op =" :: "['a, 'a] => bool" ("(_ =/ _)" [51, 51] 50) |
126 "op ~=" :: "['a, 'a] => bool" ("(_ ~=/ _)" [51, 51] 50) |
122 "op ~=" :: "['a, 'a] => bool" ("(_ ~=/ _)" [51, 51] 50) |
127 |
123 |
128 syntax (symbols) |
124 syntax (symbols) |
129 Not :: "bool => bool" ("\<not> _" [40] 40) |
125 Not :: "bool => bool" ("\\<not> _" [40] 40) |
130 "op &" :: "[bool, bool] => bool" (infixr "\<and>" 35) |
126 "op &" :: "[bool, bool] => bool" (infixr "\\<and>" 35) |
131 "op |" :: "[bool, bool] => bool" (infixr "\<or>" 30) |
127 "op |" :: "[bool, bool] => bool" (infixr "\\<or>" 30) |
132 "op -->" :: "[bool, bool] => bool" (infixr "\<midarrow>\<rightarrow>" 25) |
128 "op -->" :: "[bool, bool] => bool" (infixr "\\<midarrow>\\<rightarrow>" 25) |
133 "op ~=" :: "['a, 'a] => bool" (infixl "\<noteq>" 50) |
129 "op ~=" :: "['a, 'a] => bool" (infixl "\\<noteq>" 50) |
134 "ALL " :: "[idts, bool] => bool" ("(3\<forall>_./ _)" [0, 10] 10) |
130 "ALL " :: "[idts, bool] => bool" ("(3\\<forall>_./ _)" [0, 10] 10) |
135 "EX " :: "[idts, bool] => bool" ("(3\<exists>_./ _)" [0, 10] 10) |
131 "EX " :: "[idts, bool] => bool" ("(3\\<exists>_./ _)" [0, 10] 10) |
136 "EX! " :: "[idts, bool] => bool" ("(3\<exists>!_./ _)" [0, 10] 10) |
132 "EX! " :: "[idts, bool] => bool" ("(3\\<exists>!_./ _)" [0, 10] 10) |
137 "_case1" :: "['a, 'b] => case_syn" ("(2_ \<Rightarrow>/ _)" 10) |
133 "_case1" :: "['a, 'b] => case_syn" ("(2_ \\<Rightarrow>/ _)" 10) |
138 (*"_case2" :: "[case_syn, cases_syn] => cases_syn" ("_/ \\<orelse> _")*) |
134 (*"_case2" :: "[case_syn, cases_syn] => cases_syn" ("_/ \\<orelse> _")*) |
139 |
135 |
140 syntax (input) |
|
141 "_Eps" :: "[pttrn, bool] => 'a" ("(3\<epsilon>_./ _)" [0, 10] 10) |
|
142 |
|
143 syntax (symbols output) |
136 syntax (symbols output) |
144 "op ~=" :: "['a, 'a] => bool" ("(_ \<noteq>/ _)" [51, 51] 50) |
137 "op ~=" :: "['a, 'a] => bool" ("(_ \\<noteq>/ _)" [51, 51] 50) |
145 |
138 |
146 syntax (xsymbols) |
139 syntax (xsymbols) |
147 "op -->" :: "[bool, bool] => bool" (infixr "\<longrightarrow>" 25) |
140 "op -->" :: "[bool, bool] => bool" (infixr "\\<longrightarrow>" 25) |
148 |
141 |
149 syntax (HTML output) |
142 syntax (HTML output) |
150 Not :: "bool => bool" ("\<not> _" [40] 40) |
143 Not :: "bool => bool" ("\\<not> _" [40] 40) |
151 |
144 |
152 syntax (HOL) |
145 syntax (HOL) |
153 "_Eps" :: "[pttrn, bool] => 'a" ("(3@ _./ _)" [0, 10] 10) |
|
154 "ALL " :: "[idts, bool] => bool" ("(3! _./ _)" [0, 10] 10) |
146 "ALL " :: "[idts, bool] => bool" ("(3! _./ _)" [0, 10] 10) |
155 "EX " :: "[idts, bool] => bool" ("(3? _./ _)" [0, 10] 10) |
147 "EX " :: "[idts, bool] => bool" ("(3? _./ _)" [0, 10] 10) |
156 "EX! " :: "[idts, bool] => bool" ("(3?! _./ _)" [0, 10] 10) |
148 "EX! " :: "[idts, bool] => bool" ("(3?! _./ _)" [0, 10] 10) |
157 |
149 |
158 |
150 |
171 (*Extensionality is built into the meta-logic, and this rule expresses |
163 (*Extensionality is built into the meta-logic, and this rule expresses |
172 a related property. It is an eta-expanded version of the traditional |
164 a related property. It is an eta-expanded version of the traditional |
173 rule, and similar to the ABS rule of HOL.*) |
165 rule, and similar to the ABS rule of HOL.*) |
174 ext: "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)" |
166 ext: "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)" |
175 |
167 |
176 someI: "P (x::'a) ==> P (SOME x. P x)" |
|
177 the_eq_trivial: "(THE x. x = a) = (a::'a)" |
168 the_eq_trivial: "(THE x. x = a) = (a::'a)" |
178 |
169 |
179 impI: "(P ==> Q) ==> P-->Q" |
170 impI: "(P ==> Q) ==> P-->Q" |
180 mp: "[| P-->Q; P |] ==> Q" |
171 mp: "[| P-->Q; P |] ==> Q" |
181 |
172 |
182 defs |
173 defs |
183 |
174 |
184 True_def: "True == ((%x::bool. x) = (%x. x))" |
175 True_def: "True == ((%x::bool. x) = (%x. x))" |
185 All_def: "All(P) == (P = (%x. True))" |
176 All_def: "All(P) == (P = (%x. True))" |
186 Ex_def: "Ex(P) == P (SOME x. P x)" |
177 Ex_def: "Ex(P) == !Q. (!x. P x --> Q) --> Q" |
187 False_def: "False == (!P. P)" |
178 False_def: "False == (!P. P)" |
188 not_def: "~ P == P-->False" |
179 not_def: "~ P == P-->False" |
189 and_def: "P & Q == !R. (P-->Q-->R) --> R" |
180 and_def: "P & Q == !R. (P-->Q-->R) --> R" |
190 or_def: "P | Q == !R. (P-->R) --> (Q-->R) --> R" |
181 or_def: "P | Q == !R. (P-->R) --> (Q-->R) --> R" |
191 Ex1_def: "Ex1(P) == ? x. P(x) & (! y. P(y) --> y=x)" |
182 Ex1_def: "Ex1(P) == ? x. P(x) & (! y. P(y) --> y=x)" |