49 "=" :: "['a, 'a] => bool" (infixl 50) |
48 "=" :: "['a, 'a] => bool" (infixl 50) |
50 & :: "[bool, bool] => bool" (infixr 35) |
49 & :: "[bool, bool] => bool" (infixr 35) |
51 "|" :: "[bool, bool] => bool" (infixr 30) |
50 "|" :: "[bool, bool] => bool" (infixr 30) |
52 --> :: "[bool, bool] => bool" (infixr 25) |
51 --> :: "[bool, bool] => bool" (infixr 25) |
53 |
52 |
|
53 local |
|
54 |
54 |
55 |
55 (* Overloaded Constants *) |
56 (* Overloaded Constants *) |
56 |
57 |
57 axclass zero < "term" |
58 axclass zero < "term" |
58 axclass plus < "term" |
59 axclass plus < "term" |
59 axclass minus < "term" |
60 axclass minus < "term" |
60 axclass times < "term" |
61 axclass times < "term" |
61 axclass power < "term" |
62 axclass inverse < "term" |
|
63 |
|
64 global |
62 |
65 |
63 consts |
66 consts |
64 "0" :: "('a::zero)" ("0") |
67 "0" :: "'a::zero" ("0") |
65 "+" :: "['a::plus, 'a] => 'a" (infixl 65) |
68 "+" :: "['a::plus, 'a] => 'a" (infixl 65) |
66 - :: "['a::minus, 'a] => 'a" (infixl 65) |
69 - :: "['a::minus, 'a] => 'a" (infixl 65) |
67 uminus :: "['a::minus] => 'a" ("- _" [81] 80) |
70 uminus :: "['a::minus] => 'a" ("- _" [81] 80) |
68 abs :: "('a::minus) => 'a" |
|
69 * :: "['a::times, 'a] => 'a" (infixl 70) |
71 * :: "['a::times, 'a] => 'a" (infixl 70) |
70 (*See Nat.thy for "^"*) |
72 |
|
73 local |
|
74 |
|
75 consts |
|
76 abs :: "'a::minus => 'a" |
|
77 inverse :: "'a::inverse => 'a" |
|
78 divide :: "['a::inverse, 'a] => 'a" (infixl "'/" 70) |
71 |
79 |
72 axclass plus_ac0 < plus, zero |
80 axclass plus_ac0 < plus, zero |
73 commute: "x + y = y + x" |
81 commute: "x + y = y + x" |
74 assoc: "(x + y) + z = x + (y + z)" |
82 assoc: "(x + y) + z = x + (y + z)" |
75 zero: "0 + x = x" |
83 zero: "0 + x = x" |
76 |
84 |
77 |
85 |
78 (** Additional concrete syntax **) |
86 (** Additional concrete syntax **) |
79 |
87 |
80 nonterminals |
88 nonterminals |
108 syntax ("" output) |
116 syntax ("" output) |
109 "op =" :: "['a, 'a] => bool" ("(_ =/ _)" [51, 51] 50) |
117 "op =" :: "['a, 'a] => bool" ("(_ =/ _)" [51, 51] 50) |
110 "op ~=" :: "['a, 'a] => bool" ("(_ ~=/ _)" [51, 51] 50) |
118 "op ~=" :: "['a, 'a] => bool" ("(_ ~=/ _)" [51, 51] 50) |
111 |
119 |
112 syntax (symbols) |
120 syntax (symbols) |
113 Not :: "bool => bool" ("\\<not> _" [40] 40) |
121 Not :: "bool => bool" ("\<not> _" [40] 40) |
114 "op &" :: "[bool, bool] => bool" (infixr "\\<and>" 35) |
122 "op &" :: "[bool, bool] => bool" (infixr "\<and>" 35) |
115 "op |" :: "[bool, bool] => bool" (infixr "\\<or>" 30) |
123 "op |" :: "[bool, bool] => bool" (infixr "\<or>" 30) |
116 "op -->" :: "[bool, bool] => bool" (infixr "\\<midarrow>\\<rightarrow>" 25) |
124 "op -->" :: "[bool, bool] => bool" (infixr "\<midarrow>\<rightarrow>" 25) |
117 "op ~=" :: "['a, 'a] => bool" (infixl "\\<noteq>" 50) |
125 "op ~=" :: "['a, 'a] => bool" (infixl "\<noteq>" 50) |
118 "ALL " :: "[idts, bool] => bool" ("(3\\<forall>_./ _)" [0, 10] 10) |
126 "ALL " :: "[idts, bool] => bool" ("(3\<forall>_./ _)" [0, 10] 10) |
119 "EX " :: "[idts, bool] => bool" ("(3\\<exists>_./ _)" [0, 10] 10) |
127 "EX " :: "[idts, bool] => bool" ("(3\<exists>_./ _)" [0, 10] 10) |
120 "EX! " :: "[idts, bool] => bool" ("(3\\<exists>!_./ _)" [0, 10] 10) |
128 "EX! " :: "[idts, bool] => bool" ("(3\<exists>!_./ _)" [0, 10] 10) |
121 "_case1" :: "['a, 'b] => case_syn" ("(2_ \\<Rightarrow>/ _)" 10) |
129 "_case1" :: "['a, 'b] => case_syn" ("(2_ \<Rightarrow>/ _)" 10) |
122 (*"_case2" :: "[case_syn, cases_syn] => cases_syn" ("_/ \\<orelse> _")*) |
130 (*"_case2" :: "[case_syn, cases_syn] => cases_syn" ("_/ \\<orelse> _")*) |
123 |
131 |
124 syntax (input) |
132 syntax (input) |
125 "_Eps" :: "[pttrn, bool] => 'a" ("(3\\<epsilon>_./ _)" [0, 10] 10) |
133 "_Eps" :: "[pttrn, bool] => 'a" ("(3\<epsilon>_./ _)" [0, 10] 10) |
126 |
134 |
127 syntax (symbols output) |
135 syntax (symbols output) |
128 "op ~=" :: "['a, 'a] => bool" ("(_ \\<noteq>/ _)" [51, 51] 50) |
136 "op ~=" :: "['a, 'a] => bool" ("(_ \<noteq>/ _)" [51, 51] 50) |
129 |
137 |
130 syntax (xsymbols) |
138 syntax (xsymbols) |
131 "op -->" :: "[bool, bool] => bool" (infixr "\\<longrightarrow>" 25) |
139 "op -->" :: "[bool, bool] => bool" (infixr "\<longrightarrow>" 25) |
132 |
140 |
133 syntax (HTML output) |
141 syntax (HTML output) |
134 Not :: "bool => bool" ("\\<not> _" [40] 40) |
142 Not :: "bool => bool" ("\<not> _" [40] 40) |
135 |
143 |
136 syntax (HOL) |
144 syntax (HOL) |
137 "_Eps" :: "[pttrn, bool] => 'a" ("(3@ _./ _)" [0, 10] 10) |
145 "_Eps" :: "[pttrn, bool] => 'a" ("(3@ _./ _)" [0, 10] 10) |
138 "ALL " :: "[idts, bool] => bool" ("(3! _./ _)" [0, 10] 10) |
146 "ALL " :: "[idts, bool] => bool" ("(3! _./ _)" [0, 10] 10) |
139 "EX " :: "[idts, bool] => bool" ("(3? _./ _)" [0, 10] 10) |
147 "EX " :: "[idts, bool] => bool" ("(3? _./ _)" [0, 10] 10) |
157 (*Extensionality is built into the meta-logic, and this rule expresses |
163 (*Extensionality is built into the meta-logic, and this rule expresses |
158 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 |
159 rule, and similar to the ABS rule of HOL.*) |
165 rule, and similar to the ABS rule of HOL.*) |
160 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)" |
161 |
167 |
162 someI: "P (x::'a) ==> P (@x. P x)" |
168 someI: "P (x::'a) ==> P (SOME x. P x)" |
163 |
169 |
164 impI: "(P ==> Q) ==> P-->Q" |
170 impI: "(P ==> Q) ==> P-->Q" |
165 mp: "[| P-->Q; P |] ==> Q" |
171 mp: "[| P-->Q; P |] ==> Q" |
166 |
172 |
167 defs |
173 defs |
168 |
174 |
169 True_def: "True == ((%x::bool. x) = (%x. x))" |
175 True_def: "True == ((%x::bool. x) = (%x. x))" |
170 All_def: "All(P) == (P = (%x. True))" |
176 All_def: "All(P) == (P = (%x. True))" |
171 Ex_def: "Ex(P) == P(@x. P(x))" |
177 Ex_def: "Ex(P) == P (SOME x. P x)" |
172 False_def: "False == (!P. P)" |
178 False_def: "False == (!P. P)" |
173 not_def: "~ P == P-->False" |
179 not_def: "~ P == P-->False" |
174 and_def: "P & Q == !R. (P-->Q-->R) --> R" |
180 and_def: "P & Q == !R. (P-->Q-->R) --> R" |
175 or_def: "P | Q == !R. (P-->R) --> (Q-->R) --> R" |
181 or_def: "P | Q == !R. (P-->R) --> (Q-->R) --> R" |
176 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)" |
182 True_or_False: "(P=True) | (P=False)" |
188 True_or_False: "(P=True) | (P=False)" |
183 |
189 |
184 defs |
190 defs |
185 (*misc definitions*) |
191 (*misc definitions*) |
186 Let_def: "Let s f == f(s)" |
192 Let_def: "Let s f == f(s)" |
187 if_def: "If P x y == @z::'a. (P=True --> z=x) & (P=False --> z=y)" |
193 if_def: "If P x y == SOME z::'a. (P=True --> z=x) & (P=False --> z=y)" |
188 |
194 |
189 (*arbitrary is completely unspecified, but is made to appear as a |
195 (*arbitrary is completely unspecified, but is made to appear as a |
190 definition syntactically*) |
196 definition syntactically*) |
191 arbitrary_def: "False ==> arbitrary == (@x. False)" |
197 arbitrary_def: "False ==> arbitrary == (SOME x. False)" |
192 |
198 |
193 |
199 |
194 |
200 |
195 (* theory and package setup *) |
201 (* theory and package setup *) |
196 |
202 |
197 use "HOL_lemmas.ML" |
203 use "HOL_lemmas.ML" |
198 |
204 |
199 lemma all_eq: "(!!x. P x) == Trueprop (ALL x. P x)" |
205 lemma atomize_all: "(!!x. P x) == Trueprop (ALL x. P x)" |
200 proof (rule equal_intr_rule) |
206 proof (rule equal_intr_rule) |
201 assume "!!x. P x" |
207 assume "!!x. P x" |
202 show "ALL x. P x" by (rule allI) |
208 show "ALL x. P x" by (rule allI) |
203 next |
209 next |
204 assume "ALL x. P x" |
210 assume "ALL x. P x" |
205 thus "!!x. P x" by (rule allE) |
211 thus "!!x. P x" by (rule allE) |
206 qed |
212 qed |
207 |
213 |
208 lemma imp_eq: "(A ==> B) == Trueprop (A --> B)" |
214 lemma atomize_imp: "(A ==> B) == Trueprop (A --> B)" |
209 proof (rule equal_intr_rule) |
215 proof (rule equal_intr_rule) |
210 assume r: "A ==> B" |
216 assume r: "A ==> B" |
211 show "A --> B" by (rule impI) (rule r) |
217 show "A --> B" by (rule impI) (rule r) |
212 next |
218 next |
213 assume "A --> B" and A |
219 assume "A --> B" and A |
214 thus B by (rule mp) |
220 thus B by (rule mp) |
215 qed |
221 qed |
216 |
222 |
217 lemmas atomize = all_eq imp_eq |
223 lemma atomize_eq: "(x == y) == Trueprop (x = y)" |
|
224 proof (rule equal_intr_rule) |
|
225 assume "x == y" |
|
226 show "x = y" by (unfold prems) (rule refl) |
|
227 next |
|
228 assume "x = y" |
|
229 thus "x == y" by (rule eq_reflection) |
|
230 qed |
|
231 |
|
232 lemmas atomize = atomize_all atomize_imp |
|
233 lemmas atomize' = atomize atomize_eq |
218 |
234 |
219 use "cladata.ML" |
235 use "cladata.ML" |
220 setup hypsubst_setup |
236 setup hypsubst_setup |
221 setup Classical.setup |
237 setup Classical.setup |
222 setup clasetup |
238 setup clasetup |