author | nipkow |
Fri, 07 Sep 2007 17:56:03 +0200 | |
changeset 24553 | 9b19da7b2b08 |
parent 24506 | 020db6ec334a |
child 24633 | 0a3a02066244 |
permissions | -rw-r--r-- |
923 | 1 |
(* Title: HOL/HOL.thy |
2 |
ID: $Id$ |
|
11750 | 3 |
Author: Tobias Nipkow, Markus Wenzel, and Larry Paulson |
4 |
*) |
|
923 | 5 |
|
11750 | 6 |
header {* The basis of Higher-Order Logic *} |
923 | 7 |
|
15131 | 8 |
theory HOL |
15140 | 9 |
imports CPure |
23163 | 10 |
uses |
23247 | 11 |
"~~/src/Tools/integer.ML" |
23553 | 12 |
("hologic.ML") |
23171 | 13 |
"~~/src/Tools/IsaPlanner/zipper.ML" |
14 |
"~~/src/Tools/IsaPlanner/isand.ML" |
|
15 |
"~~/src/Tools/IsaPlanner/rw_tools.ML" |
|
16 |
"~~/src/Tools/IsaPlanner/rw_inst.ML" |
|
23263 | 17 |
"~~/src/Provers/project_rule.ML" |
23163 | 18 |
"~~/src/Provers/induct_method.ML" |
23263 | 19 |
"~~/src/Provers/hypsubst.ML" |
20 |
"~~/src/Provers/splitter.ML" |
|
23163 | 21 |
"~~/src/Provers/classical.ML" |
22 |
"~~/src/Provers/blast.ML" |
|
23 |
"~~/src/Provers/clasimp.ML" |
|
23263 | 24 |
"~~/src/Provers/eqsubst.ML" |
23163 | 25 |
"~~/src/Provers/quantifier1.ML" |
26 |
("simpdata.ML") |
|
24280 | 27 |
"~~/src/Tools/code/code_name.ML" |
28 |
"~~/src/Tools/code/code_funcgr.ML" |
|
29 |
"~~/src/Tools/code/code_thingol.ML" |
|
30 |
"~~/src/Tools/code/code_target.ML" |
|
31 |
"~~/src/Tools/code/code_package.ML" |
|
24166 | 32 |
"~~/src/Tools/nbe.ML" |
15131 | 33 |
begin |
2260 | 34 |
|
11750 | 35 |
subsection {* Primitive logic *} |
36 |
||
37 |
subsubsection {* Core syntax *} |
|
2260 | 38 |
|
14854 | 39 |
classes type |
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12281
diff
changeset
|
40 |
defaultsort type |
3947 | 41 |
|
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12281
diff
changeset
|
42 |
global |
923 | 43 |
|
7357 | 44 |
typedecl bool |
923 | 45 |
|
46 |
arities |
|
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12281
diff
changeset
|
47 |
bool :: type |
20590
bf92900995f8
introduced syntactic classes; moved some setup to Pure/codegen, Pure/nbe or OperationalEquality.thy
haftmann
parents:
20453
diff
changeset
|
48 |
"fun" :: (type, type) type |
923 | 49 |
|
11750 | 50 |
judgment |
51 |
Trueprop :: "bool => prop" ("(_)" 5) |
|
923 | 52 |
|
11750 | 53 |
consts |
7357 | 54 |
Not :: "bool => bool" ("~ _" [40] 40) |
55 |
True :: bool |
|
56 |
False :: bool |
|
3947 | 57 |
arbitrary :: 'a |
923 | 58 |
|
11432
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
10489
diff
changeset
|
59 |
The :: "('a => bool) => 'a" |
7357 | 60 |
All :: "('a => bool) => bool" (binder "ALL " 10) |
61 |
Ex :: "('a => bool) => bool" (binder "EX " 10) |
|
62 |
Ex1 :: "('a => bool) => bool" (binder "EX! " 10) |
|
63 |
Let :: "['a, 'a => 'b] => 'b" |
|
923 | 64 |
|
22839 | 65 |
"op =" :: "['a, 'a] => bool" (infixl "=" 50) |
66 |
"op &" :: "[bool, bool] => bool" (infixr "&" 35) |
|
67 |
"op |" :: "[bool, bool] => bool" (infixr "|" 30) |
|
68 |
"op -->" :: "[bool, bool] => bool" (infixr "-->" 25) |
|
923 | 69 |
|
10432
3dfbc913d184
added axclass inverse and consts inverse, divide (infix "/");
wenzelm
parents:
10383
diff
changeset
|
70 |
local |
3dfbc913d184
added axclass inverse and consts inverse, divide (infix "/");
wenzelm
parents:
10383
diff
changeset
|
71 |
|
16587 | 72 |
consts |
73 |
If :: "[bool, 'a, 'a] => 'a" ("(if (_)/ then (_)/ else (_))" 10) |
|
2260 | 74 |
|
19656
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19607
diff
changeset
|
75 |
|
11750 | 76 |
subsubsection {* Additional concrete syntax *} |
2260 | 77 |
|
21210 | 78 |
notation (output) |
19656
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19607
diff
changeset
|
79 |
"op =" (infix "=" 50) |
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19607
diff
changeset
|
80 |
|
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19607
diff
changeset
|
81 |
abbreviation |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21250
diff
changeset
|
82 |
not_equal :: "['a, 'a] => bool" (infixl "~=" 50) where |
19656
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19607
diff
changeset
|
83 |
"x ~= y == ~ (x = y)" |
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19607
diff
changeset
|
84 |
|
21210 | 85 |
notation (output) |
19656
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19607
diff
changeset
|
86 |
not_equal (infix "~=" 50) |
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19607
diff
changeset
|
87 |
|
21210 | 88 |
notation (xsymbols) |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21250
diff
changeset
|
89 |
Not ("\<not> _" [40] 40) and |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21250
diff
changeset
|
90 |
"op &" (infixr "\<and>" 35) and |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21250
diff
changeset
|
91 |
"op |" (infixr "\<or>" 30) and |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21250
diff
changeset
|
92 |
"op -->" (infixr "\<longrightarrow>" 25) and |
19656
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19607
diff
changeset
|
93 |
not_equal (infix "\<noteq>" 50) |
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19607
diff
changeset
|
94 |
|
21210 | 95 |
notation (HTML output) |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21250
diff
changeset
|
96 |
Not ("\<not> _" [40] 40) and |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21250
diff
changeset
|
97 |
"op &" (infixr "\<and>" 35) and |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21250
diff
changeset
|
98 |
"op |" (infixr "\<or>" 30) and |
19656
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19607
diff
changeset
|
99 |
not_equal (infix "\<noteq>" 50) |
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19607
diff
changeset
|
100 |
|
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19607
diff
changeset
|
101 |
abbreviation (iff) |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21250
diff
changeset
|
102 |
iff :: "[bool, bool] => bool" (infixr "<->" 25) where |
19656
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19607
diff
changeset
|
103 |
"A <-> B == A = B" |
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19607
diff
changeset
|
104 |
|
21210 | 105 |
notation (xsymbols) |
19656
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19607
diff
changeset
|
106 |
iff (infixr "\<longleftrightarrow>" 25) |
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19607
diff
changeset
|
107 |
|
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19607
diff
changeset
|
108 |
|
4868 | 109 |
nonterminals |
923 | 110 |
letbinds letbind |
111 |
case_syn cases_syn |
|
112 |
||
113 |
syntax |
|
11432
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
10489
diff
changeset
|
114 |
"_The" :: "[pttrn, bool] => 'a" ("(3THE _./ _)" [0, 10] 10) |
923 | 115 |
|
7357 | 116 |
"_bind" :: "[pttrn, 'a] => letbind" ("(2_ =/ _)" 10) |
117 |
"" :: "letbind => letbinds" ("_") |
|
118 |
"_binds" :: "[letbind, letbinds] => letbinds" ("_;/ _") |
|
119 |
"_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" 10) |
|
923 | 120 |
|
9060
b0dd884b1848
rename @case to _case_syntax (improves on low-level errors);
wenzelm
parents:
8959
diff
changeset
|
121 |
"_case_syntax":: "['a, cases_syn] => 'b" ("(case _ of/ _)" 10) |
b0dd884b1848
rename @case to _case_syntax (improves on low-level errors);
wenzelm
parents:
8959
diff
changeset
|
122 |
"_case1" :: "['a, 'b] => case_syn" ("(2_ =>/ _)" 10) |
7357 | 123 |
"" :: "case_syn => cases_syn" ("_") |
9060
b0dd884b1848
rename @case to _case_syntax (improves on low-level errors);
wenzelm
parents:
8959
diff
changeset
|
124 |
"_case2" :: "[case_syn, cases_syn] => cases_syn" ("_/ | _") |
923 | 125 |
|
126 |
translations |
|
13764 | 127 |
"THE x. P" == "The (%x. P)" |
923 | 128 |
"_Let (_binds b bs) e" == "_Let b (_Let bs e)" |
1114 | 129 |
"let x = a in e" == "Let a (%x. e)" |
923 | 130 |
|
13763
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13723
diff
changeset
|
131 |
print_translation {* |
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13723
diff
changeset
|
132 |
(* To avoid eta-contraction of body: *) |
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13723
diff
changeset
|
133 |
[("The", fn [Abs abs] => |
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13723
diff
changeset
|
134 |
let val (x,t) = atomic_abs_tr' abs |
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13723
diff
changeset
|
135 |
in Syntax.const "_The" $ x $ t end)] |
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13723
diff
changeset
|
136 |
*} |
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13723
diff
changeset
|
137 |
|
12114
a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
12023
diff
changeset
|
138 |
syntax (xsymbols) |
11687 | 139 |
"_case1" :: "['a, 'b] => case_syn" ("(2_ \<Rightarrow>/ _)" 10) |
21524 | 140 |
|
141 |
notation (xsymbols) |
|
142 |
All (binder "\<forall>" 10) and |
|
143 |
Ex (binder "\<exists>" 10) and |
|
144 |
Ex1 (binder "\<exists>!" 10) |
|
2372 | 145 |
|
21524 | 146 |
notation (HTML output) |
147 |
All (binder "\<forall>" 10) and |
|
148 |
Ex (binder "\<exists>" 10) and |
|
149 |
Ex1 (binder "\<exists>!" 10) |
|
6340 | 150 |
|
21524 | 151 |
notation (HOL) |
152 |
All (binder "! " 10) and |
|
153 |
Ex (binder "? " 10) and |
|
154 |
Ex1 (binder "?! " 10) |
|
7238
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
7220
diff
changeset
|
155 |
|
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
7220
diff
changeset
|
156 |
|
11750 | 157 |
subsubsection {* Axioms and basic definitions *} |
2260 | 158 |
|
7357 | 159 |
axioms |
15380 | 160 |
eq_reflection: "(x=y) ==> (x==y)" |
923 | 161 |
|
15380 | 162 |
refl: "t = (t::'a)" |
6289 | 163 |
|
15380 | 164 |
ext: "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)" |
165 |
-- {*Extensionality is built into the meta-logic, and this rule expresses |
|
166 |
a related property. It is an eta-expanded version of the traditional |
|
167 |
rule, and similar to the ABS rule of HOL*} |
|
6289 | 168 |
|
11432
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
10489
diff
changeset
|
169 |
the_eq_trivial: "(THE x. x = a) = (a::'a)" |
923 | 170 |
|
15380 | 171 |
impI: "(P ==> Q) ==> P-->Q" |
172 |
mp: "[| P-->Q; P |] ==> Q" |
|
173 |
||
174 |
||
923 | 175 |
defs |
7357 | 176 |
True_def: "True == ((%x::bool. x) = (%x. x))" |
177 |
All_def: "All(P) == (P = (%x. True))" |
|
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11438
diff
changeset
|
178 |
Ex_def: "Ex(P) == !Q. (!x. P x --> Q) --> Q" |
7357 | 179 |
False_def: "False == (!P. P)" |
180 |
not_def: "~ P == P-->False" |
|
181 |
and_def: "P & Q == !R. (P-->Q-->R) --> R" |
|
182 |
or_def: "P | Q == !R. (P-->R) --> (Q-->R) --> R" |
|
183 |
Ex1_def: "Ex1(P) == ? x. P(x) & (! y. P(y) --> y=x)" |
|
923 | 184 |
|
7357 | 185 |
axioms |
186 |
iff: "(P-->Q) --> (Q-->P) --> (P=Q)" |
|
187 |
True_or_False: "(P=True) | (P=False)" |
|
923 | 188 |
|
189 |
defs |
|
24219 | 190 |
Let_def: "Let s f == f(s)" |
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11438
diff
changeset
|
191 |
if_def: "If P x y == THE z::'a. (P=True --> z=x) & (P=False --> z=y)" |
5069 | 192 |
|
14223
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14208
diff
changeset
|
193 |
finalconsts |
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14208
diff
changeset
|
194 |
"op =" |
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14208
diff
changeset
|
195 |
"op -->" |
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14208
diff
changeset
|
196 |
The |
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14208
diff
changeset
|
197 |
arbitrary |
22481
79c2724c36b5
added class "default" and expansion axioms for undefined
haftmann
parents:
22473
diff
changeset
|
198 |
|
79c2724c36b5
added class "default" and expansion axioms for undefined
haftmann
parents:
22473
diff
changeset
|
199 |
axiomatization |
79c2724c36b5
added class "default" and expansion axioms for undefined
haftmann
parents:
22473
diff
changeset
|
200 |
undefined :: 'a |
79c2724c36b5
added class "default" and expansion axioms for undefined
haftmann
parents:
22473
diff
changeset
|
201 |
|
22744
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22481
diff
changeset
|
202 |
axiomatization where |
22481
79c2724c36b5
added class "default" and expansion axioms for undefined
haftmann
parents:
22473
diff
changeset
|
203 |
undefined_fun: "undefined x = undefined" |
3320 | 204 |
|
19656
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19607
diff
changeset
|
205 |
|
22481
79c2724c36b5
added class "default" and expansion axioms for undefined
haftmann
parents:
22473
diff
changeset
|
206 |
subsubsection {* Generic classes and algebraic operations *} |
79c2724c36b5
added class "default" and expansion axioms for undefined
haftmann
parents:
22473
diff
changeset
|
207 |
|
79c2724c36b5
added class "default" and expansion axioms for undefined
haftmann
parents:
22473
diff
changeset
|
208 |
class default = type + |
79c2724c36b5
added class "default" and expansion axioms for undefined
haftmann
parents:
22473
diff
changeset
|
209 |
fixes default :: "'a" |
4868 | 210 |
|
22473 | 211 |
class zero = type + |
21524 | 212 |
fixes zero :: "'a" ("\<^loc>0") |
20713
823967ef47f1
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
haftmann
parents:
20698
diff
changeset
|
213 |
|
22473 | 214 |
class one = type + |
21524 | 215 |
fixes one :: "'a" ("\<^loc>1") |
20713
823967ef47f1
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
haftmann
parents:
20698
diff
changeset
|
216 |
|
823967ef47f1
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
haftmann
parents:
20698
diff
changeset
|
217 |
hide (open) const zero one |
20590
bf92900995f8
introduced syntactic classes; moved some setup to Pure/codegen, Pure/nbe or OperationalEquality.thy
haftmann
parents:
20453
diff
changeset
|
218 |
|
22473 | 219 |
class plus = type + |
21524 | 220 |
fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>+" 65) |
11750 | 221 |
|
22473 | 222 |
class minus = type + |
20590
bf92900995f8
introduced syntactic classes; moved some setup to Pure/codegen, Pure/nbe or OperationalEquality.thy
haftmann
parents:
20453
diff
changeset
|
223 |
fixes uminus :: "'a \<Rightarrow> 'a" |
21524 | 224 |
and minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>-" 65) |
20590
bf92900995f8
introduced syntactic classes; moved some setup to Pure/codegen, Pure/nbe or OperationalEquality.thy
haftmann
parents:
20453
diff
changeset
|
225 |
|
22473 | 226 |
class times = type + |
20713
823967ef47f1
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
haftmann
parents:
20698
diff
changeset
|
227 |
fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>*" 70) |
20590
bf92900995f8
introduced syntactic classes; moved some setup to Pure/codegen, Pure/nbe or OperationalEquality.thy
haftmann
parents:
20453
diff
changeset
|
228 |
|
22473 | 229 |
class inverse = type + |
20590
bf92900995f8
introduced syntactic classes; moved some setup to Pure/codegen, Pure/nbe or OperationalEquality.thy
haftmann
parents:
20453
diff
changeset
|
230 |
fixes inverse :: "'a \<Rightarrow> 'a" |
21524 | 231 |
and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>'/" 70) |
232 |
||
23878 | 233 |
class abs = type + |
234 |
fixes abs :: "'a \<Rightarrow> 'a" |
|
235 |
||
24506 | 236 |
class sgn = type + |
237 |
fixes sgn :: "'a \<Rightarrow> 'a" |
|
238 |
||
21524 | 239 |
notation |
240 |
uminus ("- _" [81] 80) |
|
241 |
||
242 |
notation (xsymbols) |
|
243 |
abs ("\<bar>_\<bar>") |
|
244 |
notation (HTML output) |
|
245 |
abs ("\<bar>_\<bar>") |
|
11750 | 246 |
|
23878 | 247 |
class ord = type + |
248 |
fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubseteq>" 50) |
|
249 |
and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubset>" 50) |
|
250 |
begin |
|
251 |
||
252 |
notation |
|
253 |
less_eq ("op \<^loc><=") and |
|
254 |
less_eq ("(_/ \<^loc><= _)" [51, 51] 50) and |
|
255 |
less ("op \<^loc><") and |
|
256 |
less ("(_/ \<^loc>< _)" [51, 51] 50) |
|
257 |
||
258 |
notation (xsymbols) |
|
259 |
less_eq ("op \<^loc>\<le>") and |
|
260 |
less_eq ("(_/ \<^loc>\<le> _)" [51, 51] 50) |
|
261 |
||
262 |
notation (HTML output) |
|
263 |
less_eq ("op \<^loc>\<le>") and |
|
264 |
less_eq ("(_/ \<^loc>\<le> _)" [51, 51] 50) |
|
265 |
||
266 |
abbreviation (input) |
|
267 |
greater (infix "\<^loc>>" 50) where |
|
268 |
"x \<^loc>> y \<equiv> y \<^loc>< x" |
|
269 |
||
270 |
abbreviation (input) |
|
271 |
greater_eq (infix "\<^loc>>=" 50) where |
|
272 |
"x \<^loc>>= y \<equiv> y \<^loc><= x" |
|
273 |
||
274 |
notation (input) |
|
275 |
greater_eq (infix "\<^loc>\<ge>" 50) |
|
276 |
||
277 |
definition |
|
278 |
Least :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" (binder "\<^loc>LEAST " 10) |
|
279 |
where |
|
280 |
"Least P == (THE x. P x \<and> (\<forall>y. P y \<longrightarrow> x \<^loc>\<le> y))" |
|
281 |
||
282 |
end |
|
283 |
||
284 |
notation |
|
285 |
less_eq ("op <=") and |
|
286 |
less_eq ("(_/ <= _)" [51, 51] 50) and |
|
287 |
less ("op <") and |
|
288 |
less ("(_/ < _)" [51, 51] 50) |
|
289 |
||
290 |
notation (xsymbols) |
|
291 |
less_eq ("op \<le>") and |
|
292 |
less_eq ("(_/ \<le> _)" [51, 51] 50) |
|
293 |
||
294 |
notation (HTML output) |
|
295 |
less_eq ("op \<le>") and |
|
296 |
less_eq ("(_/ \<le> _)" [51, 51] 50) |
|
297 |
||
298 |
abbreviation (input) |
|
299 |
greater (infix ">" 50) where |
|
300 |
"x > y \<equiv> y < x" |
|
301 |
||
302 |
abbreviation (input) |
|
303 |
greater_eq (infix ">=" 50) where |
|
304 |
"x >= y \<equiv> y <= x" |
|
305 |
||
306 |
notation (input) |
|
307 |
greater_eq (infix "\<ge>" 50) |
|
308 |
||
13456
42601eb7553f
special syntax for index "1" (plain numeral hidden by "1" symbol in HOL);
wenzelm
parents:
13438
diff
changeset
|
309 |
syntax |
42601eb7553f
special syntax for index "1" (plain numeral hidden by "1" symbol in HOL);
wenzelm
parents:
13438
diff
changeset
|
310 |
"_index1" :: index ("\<^sub>1") |
42601eb7553f
special syntax for index "1" (plain numeral hidden by "1" symbol in HOL);
wenzelm
parents:
13438
diff
changeset
|
311 |
translations |
14690 | 312 |
(index) "\<^sub>1" => (index) "\<^bsub>\<struct>\<^esub>" |
13456
42601eb7553f
special syntax for index "1" (plain numeral hidden by "1" symbol in HOL);
wenzelm
parents:
13438
diff
changeset
|
313 |
|
11750 | 314 |
typed_print_translation {* |
20713
823967ef47f1
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
haftmann
parents:
20698
diff
changeset
|
315 |
let |
823967ef47f1
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
haftmann
parents:
20698
diff
changeset
|
316 |
fun tr' c = (c, fn show_sorts => fn T => fn ts => |
823967ef47f1
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
haftmann
parents:
20698
diff
changeset
|
317 |
if T = dummyT orelse not (! show_types) andalso can Term.dest_Type T then raise Match |
823967ef47f1
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
haftmann
parents:
20698
diff
changeset
|
318 |
else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T); |
22993 | 319 |
in map tr' [@{const_syntax HOL.one}, @{const_syntax HOL.zero}] end; |
11750 | 320 |
*} -- {* show types that are presumably too general *} |
321 |
||
322 |
||
20944 | 323 |
subsection {* Fundamental rules *} |
324 |
||
20973 | 325 |
subsubsection {* Equality *} |
20944 | 326 |
|
327 |
text {* Thanks to Stephan Merz *} |
|
328 |
lemma subst: |
|
329 |
assumes eq: "s = t" and p: "P s" |
|
330 |
shows "P t" |
|
331 |
proof - |
|
332 |
from eq have meta: "s \<equiv> t" |
|
333 |
by (rule eq_reflection) |
|
334 |
from p show ?thesis |
|
335 |
by (unfold meta) |
|
336 |
qed |
|
15411 | 337 |
|
18457 | 338 |
lemma sym: "s = t ==> t = s" |
339 |
by (erule subst) (rule refl) |
|
15411 | 340 |
|
18457 | 341 |
lemma ssubst: "t = s ==> P s ==> P t" |
342 |
by (drule sym) (erule subst) |
|
15411 | 343 |
|
344 |
lemma trans: "[| r=s; s=t |] ==> r=t" |
|
18457 | 345 |
by (erule subst) |
15411 | 346 |
|
20944 | 347 |
lemma meta_eq_to_obj_eq: |
348 |
assumes meq: "A == B" |
|
349 |
shows "A = B" |
|
350 |
by (unfold meq) (rule refl) |
|
15411 | 351 |
|
21502 | 352 |
text {* Useful with @{text erule} for proving equalities from known equalities. *} |
20944 | 353 |
(* a = b |
15411 | 354 |
| | |
355 |
c = d *) |
|
356 |
lemma box_equals: "[| a=b; a=c; b=d |] ==> c=d" |
|
357 |
apply (rule trans) |
|
358 |
apply (rule trans) |
|
359 |
apply (rule sym) |
|
360 |
apply assumption+ |
|
361 |
done |
|
362 |
||
15524
2ef571f80a55
Moved oderings from HOL into the new Orderings.thy
nipkow
parents:
15481
diff
changeset
|
363 |
text {* For calculational reasoning: *} |
2ef571f80a55
Moved oderings from HOL into the new Orderings.thy
nipkow
parents:
15481
diff
changeset
|
364 |
|
2ef571f80a55
Moved oderings from HOL into the new Orderings.thy
nipkow
parents:
15481
diff
changeset
|
365 |
lemma forw_subst: "a = b ==> P b ==> P a" |
2ef571f80a55
Moved oderings from HOL into the new Orderings.thy
nipkow
parents:
15481
diff
changeset
|
366 |
by (rule ssubst) |
2ef571f80a55
Moved oderings from HOL into the new Orderings.thy
nipkow
parents:
15481
diff
changeset
|
367 |
|
2ef571f80a55
Moved oderings from HOL into the new Orderings.thy
nipkow
parents:
15481
diff
changeset
|
368 |
lemma back_subst: "P a ==> a = b ==> P b" |
2ef571f80a55
Moved oderings from HOL into the new Orderings.thy
nipkow
parents:
15481
diff
changeset
|
369 |
by (rule subst) |
2ef571f80a55
Moved oderings from HOL into the new Orderings.thy
nipkow
parents:
15481
diff
changeset
|
370 |
|
15411 | 371 |
|
20944 | 372 |
subsubsection {*Congruence rules for application*} |
15411 | 373 |
|
374 |
(*similar to AP_THM in Gordon's HOL*) |
|
375 |
lemma fun_cong: "(f::'a=>'b) = g ==> f(x)=g(x)" |
|
376 |
apply (erule subst) |
|
377 |
apply (rule refl) |
|
378 |
done |
|
379 |
||
380 |
(*similar to AP_TERM in Gordon's HOL and FOL's subst_context*) |
|
381 |
lemma arg_cong: "x=y ==> f(x)=f(y)" |
|
382 |
apply (erule subst) |
|
383 |
apply (rule refl) |
|
384 |
done |
|
385 |
||
15655 | 386 |
lemma arg_cong2: "\<lbrakk> a = b; c = d \<rbrakk> \<Longrightarrow> f a c = f b d" |
387 |
apply (erule ssubst)+ |
|
388 |
apply (rule refl) |
|
389 |
done |
|
390 |
||
15411 | 391 |
lemma cong: "[| f = g; (x::'a) = y |] ==> f(x) = g(y)" |
392 |
apply (erule subst)+ |
|
393 |
apply (rule refl) |
|
394 |
done |
|
395 |
||
396 |
||
20944 | 397 |
subsubsection {*Equality of booleans -- iff*} |
15411 | 398 |
|
21504 | 399 |
lemma iffI: assumes "P ==> Q" and "Q ==> P" shows "P=Q" |
400 |
by (iprover intro: iff [THEN mp, THEN mp] impI assms) |
|
15411 | 401 |
|
402 |
lemma iffD2: "[| P=Q; Q |] ==> P" |
|
18457 | 403 |
by (erule ssubst) |
15411 | 404 |
|
405 |
lemma rev_iffD2: "[| Q; P=Q |] ==> P" |
|
18457 | 406 |
by (erule iffD2) |
15411 | 407 |
|
21504 | 408 |
lemma iffD1: "Q = P \<Longrightarrow> Q \<Longrightarrow> P" |
409 |
by (drule sym) (rule iffD2) |
|
410 |
||
411 |
lemma rev_iffD1: "Q \<Longrightarrow> Q = P \<Longrightarrow> P" |
|
412 |
by (drule sym) (rule rev_iffD2) |
|
15411 | 413 |
|
414 |
lemma iffE: |
|
415 |
assumes major: "P=Q" |
|
21504 | 416 |
and minor: "[| P --> Q; Q --> P |] ==> R" |
18457 | 417 |
shows R |
418 |
by (iprover intro: minor impI major [THEN iffD2] major [THEN iffD1]) |
|
15411 | 419 |
|
420 |
||
20944 | 421 |
subsubsection {*True*} |
15411 | 422 |
|
423 |
lemma TrueI: "True" |
|
21504 | 424 |
unfolding True_def by (rule refl) |
15411 | 425 |
|
21504 | 426 |
lemma eqTrueI: "P ==> P = True" |
18457 | 427 |
by (iprover intro: iffI TrueI) |
15411 | 428 |
|
21504 | 429 |
lemma eqTrueE: "P = True ==> P" |
430 |
by (erule iffD2) (rule TrueI) |
|
15411 | 431 |
|
432 |
||
20944 | 433 |
subsubsection {*Universal quantifier*} |
15411 | 434 |
|
21504 | 435 |
lemma allI: assumes "!!x::'a. P(x)" shows "ALL x. P(x)" |
436 |
unfolding All_def by (iprover intro: ext eqTrueI assms) |
|
15411 | 437 |
|
438 |
lemma spec: "ALL x::'a. P(x) ==> P(x)" |
|
439 |
apply (unfold All_def) |
|
440 |
apply (rule eqTrueE) |
|
441 |
apply (erule fun_cong) |
|
442 |
done |
|
443 |
||
444 |
lemma allE: |
|
445 |
assumes major: "ALL x. P(x)" |
|
21504 | 446 |
and minor: "P(x) ==> R" |
447 |
shows R |
|
448 |
by (iprover intro: minor major [THEN spec]) |
|
15411 | 449 |
|
450 |
lemma all_dupE: |
|
451 |
assumes major: "ALL x. P(x)" |
|
21504 | 452 |
and minor: "[| P(x); ALL x. P(x) |] ==> R" |
453 |
shows R |
|
454 |
by (iprover intro: minor major major [THEN spec]) |
|
15411 | 455 |
|
456 |
||
21504 | 457 |
subsubsection {* False *} |
458 |
||
459 |
text {* |
|
460 |
Depends upon @{text spec}; it is impossible to do propositional |
|
461 |
logic before quantifiers! |
|
462 |
*} |
|
15411 | 463 |
|
464 |
lemma FalseE: "False ==> P" |
|
21504 | 465 |
apply (unfold False_def) |
466 |
apply (erule spec) |
|
467 |
done |
|
15411 | 468 |
|
21504 | 469 |
lemma False_neq_True: "False = True ==> P" |
470 |
by (erule eqTrueE [THEN FalseE]) |
|
15411 | 471 |
|
472 |
||
21504 | 473 |
subsubsection {* Negation *} |
15411 | 474 |
|
475 |
lemma notI: |
|
21504 | 476 |
assumes "P ==> False" |
15411 | 477 |
shows "~P" |
21504 | 478 |
apply (unfold not_def) |
479 |
apply (iprover intro: impI assms) |
|
480 |
done |
|
15411 | 481 |
|
482 |
lemma False_not_True: "False ~= True" |
|
21504 | 483 |
apply (rule notI) |
484 |
apply (erule False_neq_True) |
|
485 |
done |
|
15411 | 486 |
|
487 |
lemma True_not_False: "True ~= False" |
|
21504 | 488 |
apply (rule notI) |
489 |
apply (drule sym) |
|
490 |
apply (erule False_neq_True) |
|
491 |
done |
|
15411 | 492 |
|
493 |
lemma notE: "[| ~P; P |] ==> R" |
|
21504 | 494 |
apply (unfold not_def) |
495 |
apply (erule mp [THEN FalseE]) |
|
496 |
apply assumption |
|
497 |
done |
|
15411 | 498 |
|
21504 | 499 |
lemma notI2: "(P \<Longrightarrow> \<not> Pa) \<Longrightarrow> (P \<Longrightarrow> Pa) \<Longrightarrow> \<not> P" |
500 |
by (erule notE [THEN notI]) (erule meta_mp) |
|
15411 | 501 |
|
502 |
||
20944 | 503 |
subsubsection {*Implication*} |
15411 | 504 |
|
505 |
lemma impE: |
|
506 |
assumes "P-->Q" "P" "Q ==> R" |
|
507 |
shows "R" |
|
23553 | 508 |
by (iprover intro: assms mp) |
15411 | 509 |
|
510 |
(* Reduces Q to P-->Q, allowing substitution in P. *) |
|
511 |
lemma rev_mp: "[| P; P --> Q |] ==> Q" |
|
17589 | 512 |
by (iprover intro: mp) |
15411 | 513 |
|
514 |
lemma contrapos_nn: |
|
515 |
assumes major: "~Q" |
|
516 |
and minor: "P==>Q" |
|
517 |
shows "~P" |
|
17589 | 518 |
by (iprover intro: notI minor major [THEN notE]) |
15411 | 519 |
|
520 |
(*not used at all, but we already have the other 3 combinations *) |
|
521 |
lemma contrapos_pn: |
|
522 |
assumes major: "Q" |
|
523 |
and minor: "P ==> ~Q" |
|
524 |
shows "~P" |
|
17589 | 525 |
by (iprover intro: notI minor major notE) |
15411 | 526 |
|
527 |
lemma not_sym: "t ~= s ==> s ~= t" |
|
21250 | 528 |
by (erule contrapos_nn) (erule sym) |
529 |
||
530 |
lemma eq_neq_eq_imp_neq: "[| x = a ; a ~= b; b = y |] ==> x ~= y" |
|
531 |
by (erule subst, erule ssubst, assumption) |
|
15411 | 532 |
|
533 |
(*still used in HOLCF*) |
|
534 |
lemma rev_contrapos: |
|
535 |
assumes pq: "P ==> Q" |
|
536 |
and nq: "~Q" |
|
537 |
shows "~P" |
|
538 |
apply (rule nq [THEN contrapos_nn]) |
|
539 |
apply (erule pq) |
|
540 |
done |
|
541 |
||
20944 | 542 |
subsubsection {*Existential quantifier*} |
15411 | 543 |
|
544 |
lemma exI: "P x ==> EX x::'a. P x" |
|
545 |
apply (unfold Ex_def) |
|
17589 | 546 |
apply (iprover intro: allI allE impI mp) |
15411 | 547 |
done |
548 |
||
549 |
lemma exE: |
|
550 |
assumes major: "EX x::'a. P(x)" |
|
551 |
and minor: "!!x. P(x) ==> Q" |
|
552 |
shows "Q" |
|
553 |
apply (rule major [unfolded Ex_def, THEN spec, THEN mp]) |
|
17589 | 554 |
apply (iprover intro: impI [THEN allI] minor) |
15411 | 555 |
done |
556 |
||
557 |
||
20944 | 558 |
subsubsection {*Conjunction*} |
15411 | 559 |
|
560 |
lemma conjI: "[| P; Q |] ==> P&Q" |
|
561 |
apply (unfold and_def) |
|
17589 | 562 |
apply (iprover intro: impI [THEN allI] mp) |
15411 | 563 |
done |
564 |
||
565 |
lemma conjunct1: "[| P & Q |] ==> P" |
|
566 |
apply (unfold and_def) |
|
17589 | 567 |
apply (iprover intro: impI dest: spec mp) |
15411 | 568 |
done |
569 |
||
570 |
lemma conjunct2: "[| P & Q |] ==> Q" |
|
571 |
apply (unfold and_def) |
|
17589 | 572 |
apply (iprover intro: impI dest: spec mp) |
15411 | 573 |
done |
574 |
||
575 |
lemma conjE: |
|
576 |
assumes major: "P&Q" |
|
577 |
and minor: "[| P; Q |] ==> R" |
|
578 |
shows "R" |
|
579 |
apply (rule minor) |
|
580 |
apply (rule major [THEN conjunct1]) |
|
581 |
apply (rule major [THEN conjunct2]) |
|
582 |
done |
|
583 |
||
584 |
lemma context_conjI: |
|
23553 | 585 |
assumes "P" "P ==> Q" shows "P & Q" |
586 |
by (iprover intro: conjI assms) |
|
15411 | 587 |
|
588 |
||
20944 | 589 |
subsubsection {*Disjunction*} |
15411 | 590 |
|
591 |
lemma disjI1: "P ==> P|Q" |
|
592 |
apply (unfold or_def) |
|
17589 | 593 |
apply (iprover intro: allI impI mp) |
15411 | 594 |
done |
595 |
||
596 |
lemma disjI2: "Q ==> P|Q" |
|
597 |
apply (unfold or_def) |
|
17589 | 598 |
apply (iprover intro: allI impI mp) |
15411 | 599 |
done |
600 |
||
601 |
lemma disjE: |
|
602 |
assumes major: "P|Q" |
|
603 |
and minorP: "P ==> R" |
|
604 |
and minorQ: "Q ==> R" |
|
605 |
shows "R" |
|
17589 | 606 |
by (iprover intro: minorP minorQ impI |
15411 | 607 |
major [unfolded or_def, THEN spec, THEN mp, THEN mp]) |
608 |
||
609 |
||
20944 | 610 |
subsubsection {*Classical logic*} |
15411 | 611 |
|
612 |
lemma classical: |
|
613 |
assumes prem: "~P ==> P" |
|
614 |
shows "P" |
|
615 |
apply (rule True_or_False [THEN disjE, THEN eqTrueE]) |
|
616 |
apply assumption |
|
617 |
apply (rule notI [THEN prem, THEN eqTrueI]) |
|
618 |
apply (erule subst) |
|
619 |
apply assumption |
|
620 |
done |
|
621 |
||
622 |
lemmas ccontr = FalseE [THEN classical, standard] |
|
623 |
||
624 |
(*notE with premises exchanged; it discharges ~R so that it can be used to |
|
625 |
make elimination rules*) |
|
626 |
lemma rev_notE: |
|
627 |
assumes premp: "P" |
|
628 |
and premnot: "~R ==> ~P" |
|
629 |
shows "R" |
|
630 |
apply (rule ccontr) |
|
631 |
apply (erule notE [OF premnot premp]) |
|
632 |
done |
|
633 |
||
634 |
(*Double negation law*) |
|
635 |
lemma notnotD: "~~P ==> P" |
|
636 |
apply (rule classical) |
|
637 |
apply (erule notE) |
|
638 |
apply assumption |
|
639 |
done |
|
640 |
||
641 |
lemma contrapos_pp: |
|
642 |
assumes p1: "Q" |
|
643 |
and p2: "~P ==> ~Q" |
|
644 |
shows "P" |
|
17589 | 645 |
by (iprover intro: classical p1 p2 notE) |
15411 | 646 |
|
647 |
||
20944 | 648 |
subsubsection {*Unique existence*} |
15411 | 649 |
|
650 |
lemma ex1I: |
|
23553 | 651 |
assumes "P a" "!!x. P(x) ==> x=a" |
15411 | 652 |
shows "EX! x. P(x)" |
23553 | 653 |
by (unfold Ex1_def, iprover intro: assms exI conjI allI impI) |
15411 | 654 |
|
655 |
text{*Sometimes easier to use: the premises have no shared variables. Safe!*} |
|
656 |
lemma ex_ex1I: |
|
657 |
assumes ex_prem: "EX x. P(x)" |
|
658 |
and eq: "!!x y. [| P(x); P(y) |] ==> x=y" |
|
659 |
shows "EX! x. P(x)" |
|
17589 | 660 |
by (iprover intro: ex_prem [THEN exE] ex1I eq) |
15411 | 661 |
|
662 |
lemma ex1E: |
|
663 |
assumes major: "EX! x. P(x)" |
|
664 |
and minor: "!!x. [| P(x); ALL y. P(y) --> y=x |] ==> R" |
|
665 |
shows "R" |
|
666 |
apply (rule major [unfolded Ex1_def, THEN exE]) |
|
667 |
apply (erule conjE) |
|
17589 | 668 |
apply (iprover intro: minor) |
15411 | 669 |
done |
670 |
||
671 |
lemma ex1_implies_ex: "EX! x. P x ==> EX x. P x" |
|
672 |
apply (erule ex1E) |
|
673 |
apply (rule exI) |
|
674 |
apply assumption |
|
675 |
done |
|
676 |
||
677 |
||
20944 | 678 |
subsubsection {*THE: definite description operator*} |
15411 | 679 |
|
680 |
lemma the_equality: |
|
681 |
assumes prema: "P a" |
|
682 |
and premx: "!!x. P x ==> x=a" |
|
1d195de59497
removal of HOL_Lemmas |