author | wenzelm |
Sun, 28 Oct 2001 21:14:56 +0100 | |
changeset 11977 | 2e7c54b86763 |
parent 11953 | f98623fdf6ef |
child 11989 | d4bcba4e080e |
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 |
|
7357 | 8 |
theory HOL = CPure |
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11438
diff
changeset
|
9 |
files ("HOL_lemmas.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML"): |
923 | 10 |
|
2260 | 11 |
|
11750 | 12 |
subsection {* Primitive logic *} |
13 |
||
14 |
subsubsection {* Core syntax *} |
|
2260 | 15 |
|
3947 | 16 |
global |
17 |
||
7357 | 18 |
classes "term" < logic |
19 |
defaultsort "term" |
|
923 | 20 |
|
7357 | 21 |
typedecl bool |
923 | 22 |
|
23 |
arities |
|
7357 | 24 |
bool :: "term" |
25 |
fun :: ("term", "term") "term" |
|
923 | 26 |
|
11750 | 27 |
judgment |
28 |
Trueprop :: "bool => prop" ("(_)" 5) |
|
923 | 29 |
|
11750 | 30 |
consts |
7357 | 31 |
Not :: "bool => bool" ("~ _" [40] 40) |
32 |
True :: bool |
|
33 |
False :: bool |
|
34 |
If :: "[bool, 'a, 'a] => 'a" ("(if (_)/ then (_)/ else (_))" 10) |
|
3947 | 35 |
arbitrary :: 'a |
923 | 36 |
|
11432
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
10489
diff
changeset
|
37 |
The :: "('a => bool) => 'a" |
7357 | 38 |
All :: "('a => bool) => bool" (binder "ALL " 10) |
39 |
Ex :: "('a => bool) => bool" (binder "EX " 10) |
|
40 |
Ex1 :: "('a => bool) => bool" (binder "EX! " 10) |
|
41 |
Let :: "['a, 'a => 'b] => 'b" |
|
923 | 42 |
|
7357 | 43 |
"=" :: "['a, 'a] => bool" (infixl 50) |
44 |
& :: "[bool, bool] => bool" (infixr 35) |
|
45 |
"|" :: "[bool, bool] => bool" (infixr 30) |
|
46 |
--> :: "[bool, bool] => bool" (infixr 25) |
|
923 | 47 |
|
10432
3dfbc913d184
added axclass inverse and consts inverse, divide (infix "/");
wenzelm
parents:
10383
diff
changeset
|
48 |
local |
3dfbc913d184
added axclass inverse and consts inverse, divide (infix "/");
wenzelm
parents:
10383
diff
changeset
|
49 |
|
2260 | 50 |
|
11750 | 51 |
subsubsection {* Additional concrete syntax *} |
2260 | 52 |
|
4868 | 53 |
nonterminals |
923 | 54 |
letbinds letbind |
55 |
case_syn cases_syn |
|
56 |
||
57 |
syntax |
|
7357 | 58 |
~= :: "['a, 'a] => bool" (infixl 50) |
11432
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
10489
diff
changeset
|
59 |
"_The" :: "[pttrn, bool] => 'a" ("(3THE _./ _)" [0, 10] 10) |
923 | 60 |
|
7357 | 61 |
"_bind" :: "[pttrn, 'a] => letbind" ("(2_ =/ _)" 10) |
62 |
"" :: "letbind => letbinds" ("_") |
|
63 |
"_binds" :: "[letbind, letbinds] => letbinds" ("_;/ _") |
|
64 |
"_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" 10) |
|
923 | 65 |
|
9060
b0dd884b1848
rename @case to _case_syntax (improves on low-level errors);
wenzelm
parents:
8959
diff
changeset
|
66 |
"_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
|
67 |
"_case1" :: "['a, 'b] => case_syn" ("(2_ =>/ _)" 10) |
7357 | 68 |
"" :: "case_syn => cases_syn" ("_") |
9060
b0dd884b1848
rename @case to _case_syntax (improves on low-level errors);
wenzelm
parents:
8959
diff
changeset
|
69 |
"_case2" :: "[case_syn, cases_syn] => cases_syn" ("_/ | _") |
923 | 70 |
|
71 |
translations |
|
7238
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
7220
diff
changeset
|
72 |
"x ~= y" == "~ (x = y)" |
11432
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
10489
diff
changeset
|
73 |
"THE x. P" == "The (%x. P)" |
923 | 74 |
"_Let (_binds b bs) e" == "_Let b (_Let bs e)" |
1114 | 75 |
"let x = a in e" == "Let a (%x. e)" |
923 | 76 |
|
3820 | 77 |
syntax ("" output) |
11687 | 78 |
"=" :: "['a, 'a] => bool" (infix 50) |
79 |
"~=" :: "['a, 'a] => bool" (infix 50) |
|
2260 | 80 |
|
81 |
syntax (symbols) |
|
11687 | 82 |
Not :: "bool => bool" ("\<not> _" [40] 40) |
83 |
"op &" :: "[bool, bool] => bool" (infixr "\<and>" 35) |
|
84 |
"op |" :: "[bool, bool] => bool" (infixr "\<or>" 30) |
|
85 |
"op -->" :: "[bool, bool] => bool" (infixr "\<midarrow>\<rightarrow>" 25) |
|
86 |
"op ~=" :: "['a, 'a] => bool" (infix "\<noteq>" 50) |
|
87 |
"ALL " :: "[idts, bool] => bool" ("(3\<forall>_./ _)" [0, 10] 10) |
|
88 |
"EX " :: "[idts, bool] => bool" ("(3\<exists>_./ _)" [0, 10] 10) |
|
89 |
"EX! " :: "[idts, bool] => bool" ("(3\<exists>!_./ _)" [0, 10] 10) |
|
90 |
"_case1" :: "['a, 'b] => case_syn" ("(2_ \<Rightarrow>/ _)" 10) |
|
9060
b0dd884b1848
rename @case to _case_syntax (improves on low-level errors);
wenzelm
parents:
8959
diff
changeset
|
91 |
(*"_case2" :: "[case_syn, cases_syn] => cases_syn" ("_/ \\<orelse> _")*) |
2372 | 92 |
|
3820 | 93 |
syntax (symbols output) |
11687 | 94 |
"op ~=" :: "['a, 'a] => bool" (infix "\<noteq>" 50) |
3820 | 95 |
|
6027
9dd06eeda95c
added new print_mode "xsymbols" for extended symbol support
oheimb
parents:
5786
diff
changeset
|
96 |
syntax (xsymbols) |
11687 | 97 |
"op -->" :: "[bool, bool] => bool" (infixr "\<longrightarrow>" 25) |
2260 | 98 |
|
6340 | 99 |
syntax (HTML output) |
11687 | 100 |
Not :: "bool => bool" ("\<not> _" [40] 40) |
6340 | 101 |
|
7238
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
7220
diff
changeset
|
102 |
syntax (HOL) |
7357 | 103 |
"ALL " :: "[idts, bool] => bool" ("(3! _./ _)" [0, 10] 10) |
104 |
"EX " :: "[idts, bool] => bool" ("(3? _./ _)" [0, 10] 10) |
|
105 |
"EX! " :: "[idts, bool] => bool" ("(3?! _./ _)" [0, 10] 10) |
|
7238
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
7220
diff
changeset
|
106 |
|
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
7220
diff
changeset
|
107 |
|
11750 | 108 |
subsubsection {* Axioms and basic definitions *} |
2260 | 109 |
|
7357 | 110 |
axioms |
111 |
eq_reflection: "(x=y) ==> (x==y)" |
|
923 | 112 |
|
7357 | 113 |
refl: "t = (t::'a)" |
114 |
subst: "[| s = t; P(s) |] ==> P(t::'a)" |
|
6289 | 115 |
|
7357 | 116 |
ext: "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)" |
11750 | 117 |
-- {* Extensionality is built into the meta-logic, and this rule expresses *} |
118 |
-- {* a related property. It is an eta-expanded version of the traditional *} |
|
119 |
-- {* rule, and similar to the ABS rule of HOL *} |
|
6289 | 120 |
|
11432
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
10489
diff
changeset
|
121 |
the_eq_trivial: "(THE x. x = a) = (a::'a)" |
923 | 122 |
|
7357 | 123 |
impI: "(P ==> Q) ==> P-->Q" |
124 |
mp: "[| P-->Q; P |] ==> Q" |
|
923 | 125 |
|
126 |
defs |
|
7357 | 127 |
True_def: "True == ((%x::bool. x) = (%x. x))" |
128 |
All_def: "All(P) == (P = (%x. True))" |
|
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11438
diff
changeset
|
129 |
Ex_def: "Ex(P) == !Q. (!x. P x --> Q) --> Q" |
7357 | 130 |
False_def: "False == (!P. P)" |
131 |
not_def: "~ P == P-->False" |
|
132 |
and_def: "P & Q == !R. (P-->Q-->R) --> R" |
|
133 |
or_def: "P | Q == !R. (P-->R) --> (Q-->R) --> R" |
|
134 |
Ex1_def: "Ex1(P) == ? x. P(x) & (! y. P(y) --> y=x)" |
|
923 | 135 |
|
7357 | 136 |
axioms |
137 |
iff: "(P-->Q) --> (Q-->P) --> (P=Q)" |
|
138 |
True_or_False: "(P=True) | (P=False)" |
|
923 | 139 |
|
140 |
defs |
|
7357 | 141 |
Let_def: "Let s f == f(s)" |
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11438
diff
changeset
|
142 |
if_def: "If P x y == THE z::'a. (P=True --> z=x) & (P=False --> z=y)" |
5069 | 143 |
|
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11438
diff
changeset
|
144 |
arbitrary_def: "False ==> arbitrary == (THE x. False)" |
11750 | 145 |
-- {* @{term arbitrary} is completely unspecified, but is made to appear as a |
146 |
definition syntactically *} |
|
923 | 147 |
|
3320 | 148 |
|
11750 | 149 |
subsubsection {* Generic algebraic operations *} |
4868 | 150 |
|
11750 | 151 |
axclass zero < "term" |
152 |
axclass one < "term" |
|
153 |
axclass plus < "term" |
|
154 |
axclass minus < "term" |
|
155 |
axclass times < "term" |
|
156 |
axclass inverse < "term" |
|
157 |
||
158 |
global |
|
159 |
||
160 |
consts |
|
161 |
"0" :: "'a::zero" ("0") |
|
162 |
"1" :: "'a::one" ("1") |
|
163 |
"+" :: "['a::plus, 'a] => 'a" (infixl 65) |
|
164 |
- :: "['a::minus, 'a] => 'a" (infixl 65) |
|
165 |
uminus :: "['a::minus] => 'a" ("- _" [81] 80) |
|
166 |
* :: "['a::times, 'a] => 'a" (infixl 70) |
|
167 |
||
168 |
local |
|
169 |
||
170 |
typed_print_translation {* |
|
171 |
let |
|
172 |
fun tr' c = (c, fn show_sorts => fn T => fn ts => |
|
173 |
if T = dummyT orelse not (! show_types) andalso can Term.dest_Type T then raise Match |
|
174 |
else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T); |
|
175 |
in [tr' "0", tr' "1"] end; |
|
176 |
*} -- {* show types that are presumably too general *} |
|
177 |
||
178 |
||
179 |
consts |
|
180 |
abs :: "'a::minus => 'a" |
|
181 |
inverse :: "'a::inverse => 'a" |
|
182 |
divide :: "['a::inverse, 'a] => 'a" (infixl "'/" 70) |
|
183 |
||
184 |
syntax (xsymbols) |
|
185 |
abs :: "'a::minus => 'a" ("\<bar>_\<bar>") |
|
186 |
syntax (HTML output) |
|
187 |
abs :: "'a::minus => 'a" ("\<bar>_\<bar>") |
|
188 |
||
189 |
axclass plus_ac0 < plus, zero |
|
190 |
commute: "x + y = y + x" |
|
191 |
assoc: "(x + y) + z = x + (y + z)" |
|
192 |
zero: "0 + x = x" |
|
193 |
||
194 |
||
195 |
subsection {* Theory and package setup *} |
|
196 |
||
197 |
subsubsection {* Basic lemmas *} |
|
4868 | 198 |
|
9736 | 199 |
use "HOL_lemmas.ML" |
11687 | 200 |
theorems case_split = case_split_thm [case_names True False] |
9869 | 201 |
|
11750 | 202 |
declare trans [trans] |
203 |
declare impE [CPure.elim] iffD1 [CPure.elim] iffD2 [CPure.elim] |
|
204 |
||
11438
3d9222b80989
declare trans [trans] (*overridden in theory Calculation*);
wenzelm
parents:
11432
diff
changeset
|
205 |
|
11750 | 206 |
subsubsection {* Atomizing meta-level connectives *} |
207 |
||
208 |
lemma atomize_all [atomize]: "(!!x. P x) == Trueprop (ALL x. P x)" |
|
9488 | 209 |
proof (rule equal_intr_rule) |
210 |
assume "!!x. P x" |
|
10383 | 211 |
show "ALL x. P x" by (rule allI) |
9488 | 212 |
next |
213 |
assume "ALL x. P x" |
|
10383 | 214 |
thus "!!x. P x" by (rule allE) |
9488 | 215 |
qed |
216 |
||
11750 | 217 |
lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A --> B)" |
9488 | 218 |
proof (rule equal_intr_rule) |
219 |
assume r: "A ==> B" |
|
10383 | 220 |
show "A --> B" by (rule impI) (rule r) |
9488 | 221 |
next |
222 |
assume "A --> B" and A |
|
10383 | 223 |
thus B by (rule mp) |
9488 | 224 |
qed |
225 |
||
11750 | 226 |
lemma atomize_eq [atomize]: "(x == y) == Trueprop (x = y)" |
10432
3dfbc913d184
added axclass inverse and consts inverse, divide (infix "/");
wenzelm
parents:
10383
diff
changeset
|
227 |
proof (rule equal_intr_rule) |
3dfbc913d184
added axclass inverse and consts inverse, divide (infix "/");
wenzelm
parents:
10383
diff
changeset
|
228 |
assume "x == y" |
3dfbc913d184
added axclass inverse and consts inverse, divide (infix "/");
wenzelm
parents:
10383
diff
changeset
|
229 |
show "x = y" by (unfold prems) (rule refl) |
3dfbc913d184
added axclass inverse and consts inverse, divide (infix "/");
wenzelm
parents:
10383
diff
changeset
|
230 |
next |
3dfbc913d184
added axclass inverse and consts inverse, divide (infix "/");
wenzelm
parents:
10383
diff
changeset
|
231 |
assume "x = y" |
3dfbc913d184
added axclass inverse and consts inverse, divide (infix "/");
wenzelm
parents:
10383
diff
changeset
|
232 |
thus "x == y" by (rule eq_reflection) |
3dfbc913d184
added axclass inverse and consts inverse, divide (infix "/");
wenzelm
parents:
10383
diff
changeset
|
233 |
qed |
3dfbc913d184
added axclass inverse and consts inverse, divide (infix "/");
wenzelm
parents:
10383
diff
changeset
|
234 |
|
11953 | 235 |
lemma atomize_conj [atomize]: "(!!C. (A ==> B ==> PROP C) ==> PROP C) == Trueprop (A & B)" |
236 |
proof (rule equal_intr_rule) |
|
237 |
assume "!!C. (A ==> B ==> PROP C) ==> PROP C" |
|
238 |
show "A & B" by (rule conjI) |
|
239 |
next |
|
240 |
fix C |
|
241 |
assume "A & B" |
|
242 |
assume "A ==> B ==> PROP C" |
|
243 |
thus "PROP C" |
|
244 |
proof this |
|
245 |
show A by (rule conjunct1) |
|
246 |
show B by (rule conjunct2) |
|
247 |
qed |
|
248 |
qed |
|
249 |
||
11750 | 250 |
|
251 |
subsubsection {* Classical Reasoner setup *} |
|
9529 | 252 |
|
10383 | 253 |
use "cladata.ML" |
254 |
setup hypsubst_setup |
|
11977 | 255 |
|
11770 | 256 |
declare atomize_all [symmetric, rulify] atomize_imp [symmetric, rulify] |
11977 | 257 |
|
10383 | 258 |
setup Classical.setup |
259 |
setup clasetup |
|
260 |
||
11977 | 261 |
declare ext [intro?] |
262 |
declare disjI1 [elim?] disjI2 [elim?] ex1_implies_ex [elim?] sym [elim?] |
|
263 |
||
9869 | 264 |
use "blastdata.ML" |
265 |
setup Blast.setup |
|
4868 | 266 |
|
11750 | 267 |
|
268 |
subsubsection {* Simplifier setup *} |
|
269 |
||
9869 | 270 |
use "simpdata.ML" |
271 |
setup Simplifier.setup |
|
272 |
setup "Simplifier.method_setup Splitter.split_modifiers" setup simpsetup |
|
273 |
setup Splitter.setup setup Clasimp.setup |
|
274 |
||
11750 | 275 |
|
11824
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
276 |
subsubsection {* Generic cases and induction *} |
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
277 |
|
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
278 |
constdefs |
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
279 |
inductive_forall :: "('a => bool) => bool" |
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
280 |
"inductive_forall P == \<forall>x. P x" |
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
281 |
inductive_implies :: "bool => bool => bool" |
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
282 |
"inductive_implies A B == A --> B" |
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
283 |
inductive_equal :: "'a => 'a => bool" |
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
284 |
"inductive_equal x y == x = y" |
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
285 |
inductive_conj :: "bool => bool => bool" |
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
286 |
"inductive_conj A B == A & B" |
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
287 |
|
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
288 |
lemma inductive_forall_eq: "(!!x. P x) == Trueprop (inductive_forall (\<lambda>x. P x))" |
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
289 |
by (simp only: atomize_all inductive_forall_def) |
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
290 |
|
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
291 |
lemma inductive_implies_eq: "(A ==> B) == Trueprop (inductive_implies A B)" |
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
292 |
by (simp only: atomize_imp inductive_implies_def) |
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
293 |
|
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
294 |
lemma inductive_equal_eq: "(x == y) == Trueprop (inductive_equal x y)" |
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
295 |
by (simp only: atomize_eq inductive_equal_def) |
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
296 |
|
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
297 |
lemma inductive_forall_conj: "inductive_forall (\<lambda>x. inductive_conj (A x) (B x)) = |
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
298 |
inductive_conj (inductive_forall A) (inductive_forall B)" |
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
299 |
by (unfold inductive_forall_def inductive_conj_def) blast |
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
300 |
|
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
301 |
lemma inductive_implies_conj: "inductive_implies C (inductive_conj A B) = |
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
302 |
inductive_conj (inductive_implies C A) (inductive_implies C B)" |
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
303 |
by (unfold inductive_implies_def inductive_conj_def) blast |
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
304 |
|
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
305 |
lemma inductive_conj_curry: "(inductive_conj A B ==> C) == (A ==> B ==> C)" |
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
306 |
by (simp only: atomize_imp atomize_eq inductive_conj_def) (rule equal_intr_rule, blast+) |
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
307 |
|
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
308 |
lemmas inductive_atomize = inductive_forall_eq inductive_implies_eq inductive_equal_eq |
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
309 |
lemmas inductive_rulify1 = inductive_atomize [symmetric, standard] |
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
310 |
lemmas inductive_rulify2 = |
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
311 |
inductive_forall_def inductive_implies_def inductive_equal_def inductive_conj_def |
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
312 |
lemmas inductive_conj = inductive_forall_conj inductive_implies_conj inductive_conj_curry |
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
313 |
|
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
314 |
hide const inductive_forall inductive_implies inductive_equal inductive_conj |
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
315 |
|
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
316 |
|
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
317 |
text {* Method setup. *} |
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
318 |
|
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
319 |
ML {* |
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
320 |
structure InductMethod = InductMethodFun |
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
321 |
(struct |
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
322 |
val dest_concls = HOLogic.dest_concls; |
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
323 |
val cases_default = thm "case_split"; |
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
324 |
val conjI = thm "conjI"; |
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
325 |
val atomize = thms "inductive_atomize"; |
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
326 |
val rulify1 = thms "inductive_rulify1"; |
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
327 |
val rulify2 = thms "inductive_rulify2"; |
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
328 |
end); |
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
329 |
*} |
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
330 |
|
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
331 |
setup InductMethod.setup |
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
332 |
|
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset
|
333 |
|
11750 | 334 |
subsection {* Order signatures and orders *} |
335 |
||
336 |
axclass |
|
337 |
ord < "term" |
|
338 |
||
339 |
syntax |
|
340 |
"op <" :: "['a::ord, 'a] => bool" ("op <") |
|
341 |
"op <=" :: "['a::ord, 'a] => bool" ("op <=") |
|
342 |
||
343 |
global |
|
344 |
||
345 |
consts |
|
346 |
"op <" :: "['a::ord, 'a] => bool" ("(_/ < _)" [50, 51] 50) |
|
347 |
"op <=" :: "['a::ord, 'a] => bool" ("(_/ <= _)" [50, 51] 50) |
|
348 |
||
349 |
local |
|
350 |
||
351 |
syntax (symbols) |
|
352 |
"op <=" :: "['a::ord, 'a] => bool" ("op \<le>") |
|
353 |
"op <=" :: "['a::ord, 'a] => bool" ("(_/ \<le> _)" [50, 51] 50) |
|
354 |
||
355 |
(*Tell blast about overloading of < and <= to reduce the risk of |
|
356 |
its applying a rule for the wrong type*) |
|
357 |
ML {* |
|
358 |
Blast.overloaded ("op <" , domain_type); |
|
359 |
Blast.overloaded ("op <=", domain_type); |
|
360 |
*} |
|
361 |
||
362 |
||
363 |
subsubsection {* Monotonicity *} |
|
364 |
||
365 |
constdefs |
|
366 |
mono :: "['a::ord => 'b::ord] => bool" |
|
367 |
"mono f == ALL A B. A <= B --> f A <= f B" |
|
368 |
||
369 |
lemma monoI [intro?]: "(!!A B. A <= B ==> f A <= f B) ==> mono f" |
|
370 |
by (unfold mono_def) blast |
|
371 |
||
372 |
lemma monoD [dest?]: "mono f ==> A <= B ==> f A <= f B" |
|
373 |
by (unfold mono_def) blast |
|
374 |
||
375 |
constdefs |
|
376 |
min :: "['a::ord, 'a] => 'a" |
|
377 |
"min a b == (if a <= b then a else b)" |
|
378 |
max :: "['a::ord, 'a] => 'a" |
|
379 |
"max a b == (if a <= b then b else a)" |
|
380 |
||
381 |
lemma min_leastL: "(!!x. least <= x) ==> min least x = least" |
|
382 |
by (simp add: min_def) |
|
383 |
||
384 |
lemma min_of_mono: |
|
385 |
"ALL x y. (f x <= f y) = (x <= y) ==> min (f m) (f n) = f (min m n)" |
|
386 |
by (simp add: min_def) |
|
387 |
||
388 |
lemma max_leastL: "(!!x. least <= x) ==> max least x = x" |
|
389 |
by (simp add: max_def) |
|
390 |
||
391 |
lemma max_of_mono: |
|
392 |
"ALL x y. (f x <= f y) = (x <= y) ==> max (f m) (f n) = f (max m n)" |
|
393 |
by (simp add: max_def) |
|
394 |
||
395 |
||
396 |
subsubsection "Orders" |
|
397 |
||
398 |
axclass order < ord |
|
399 |
order_refl [iff]: "x <= x" |
|
400 |
order_trans: "x <= y ==> y <= z ==> x <= z" |
|
401 |
order_antisym: "x <= y ==> y <= x ==> x = y" |
|
402 |
order_less_le: "(x < y) = (x <= y & x ~= y)" |
|
403 |
||
404 |
||
405 |
text {* Reflexivity. *} |
|
406 |
||
407 |
lemma order_eq_refl: "!!x::'a::order. x = y ==> x <= y" |
|
408 |
-- {* This form is useful with the classical reasoner. *} |
|
409 |
apply (erule ssubst) |
|
410 |
apply (rule order_refl) |
|
411 |
done |
|
412 |
||
413 |
lemma order_less_irrefl [simp]: "~ x < (x::'a::order)" |
|
414 |
by (simp add: order_less_le) |
|
415 |
||
416 |
lemma order_le_less: "((x::'a::order) <= y) = (x < y | x = y)" |
|
417 |
-- {* NOT suitable for iff, since it can cause PROOF FAILED. *} |
|
418 |
apply (simp add: order_less_le) |
|
419 |
apply (blast intro!: order_refl) |
|
420 |
done |
|
421 |
||
422 |
lemmas order_le_imp_less_or_eq = order_le_less [THEN iffD1, standard] |
|
423 |
||
424 |
lemma order_less_imp_le: "!!x::'a::order. x < y ==> x <= y" |
|
425 |
by (simp add: order_less_le) |
|
426 |
||
427 |
||
428 |
text {* Asymmetry. *} |
|
429 |
||
430 |
lemma order_less_not_sym: "(x::'a::order) < y ==> ~ (y < x)" |
|
431 |
by (simp add: order_less_le order_antisym) |
|
432 |
||
433 |
lemma order_less_asym: "x < (y::'a::order) ==> (~P ==> y < x) ==> P" |
|
434 |
apply (drule order_less_not_sym) |
|
435 |
apply (erule contrapos_np) |
|
436 |
apply simp |
|
437 |
done |
|
438 |
||
439 |
||
440 |
text {* Transitivity. *} |
|
441 |
||
442 |
lemma order_less_trans: "!!x::'a::order. [| x < y; y < z |] ==> x < z" |
|
443 |
apply (simp add: order_less_le) |
|
444 |
apply (blast intro: order_trans order_antisym) |
|
445 |
done |
|
446 |
||
447 |
lemma order_le_less_trans: "!!x::'a::order. [| x <= y; y < z |] ==> x < z" |
|
448 |
apply (simp add: order_less_le) |
|
449 |
apply (blast intro: order_trans order_antisym) |
|
450 |
done |
|
451 |
||
452 |
lemma order_less_le_trans: "!!x::'a::order. [| x < y; y <= z |] ==> x < z" |
|
453 |
apply (simp add: order_less_le) |
|
454 |
apply (blast intro: order_trans order_antisym) |
|
455 |
done |
|
456 |
||
457 |
||
458 |
text {* Useful for simplification, but too risky to include by default. *} |
|
459 |
||
460 |
lemma order_less_imp_not_less: "(x::'a::order) < y ==> (~ y < x) = True" |
|
461 |
by (blast elim: order_less_asym) |
|
462 |
||
463 |
lemma order_less_imp_triv: "(x::'a::order) < y ==> (y < x --> P) = True" |
|
464 |
by (blast elim: order_less_asym) |
|
465 |
||
466 |
lemma order_less_imp_not_eq: "(x::'a::order) < y ==> (x = y) = False" |
|
467 |
by auto |
|
468 |
||
469 |
lemma order_less_imp_not_eq2: "(x::'a::order) < y ==> (y = x) = False" |
|
470 |
by auto |
|
471 |
||
472 |
||
473 |
text {* Other operators. *} |
|
474 |
||
475 |
lemma min_leastR: "(!!x::'a::order. least <= x) ==> min x least = least" |
|
476 |
apply (simp add: min_def) |
|
477 |
apply (blast intro: order_antisym) |
|
478 |
done |
|
479 |
||
480 |
lemma max_leastR: "(!!x::'a::order. least <= x) ==> max x least = x" |
|
481 |
apply (simp add: max_def) |
|
482 |
apply (blast intro: order_antisym) |
|
483 |
done |
|
484 |
||
485 |
||
486 |
subsubsection {* Least value operator *} |
|
487 |
||
488 |
constdefs |
|
489 |
Least :: "('a::ord => bool) => 'a" (binder "LEAST " 10) |
|
490 |
"Least P == THE x. P x & (ALL y. P y --> x <= y)" |
|
491 |
-- {* We can no longer use LeastM because the latter requires Hilbert-AC. *} |
|
492 |
||
493 |
lemma LeastI2: |
|
494 |
"[| P (x::'a::order); |
|
495 |
!!y. P y ==> x <= y; |
|
496 |
!!x. [| P x; ALL y. P y --> x \<le> y |] ==> Q x |] |
|
497 |
==> Q (Least P)"; |
|
498 |
apply (unfold Least_def) |
|
499 |
apply (rule theI2) |
|
500 |
apply (blast intro: order_antisym)+ |
|
501 |
done |
|
502 |
||
503 |
lemma Least_equality: |
|
504 |
"[| P (k::'a::order); !!x. P x ==> k <= x |] ==> (LEAST x. P x) = k"; |
|
505 |
apply (simp add: Least_def) |
|
506 |
apply (rule the_equality) |
|
507 |
apply (auto intro!: order_antisym) |
|
508 |
done |
|
509 |
||
510 |
||
511 |
subsubsection "Linear / total orders" |
|
512 |
||
513 |
axclass linorder < order |
|
514 |
linorder_linear: "x <= y | y <= x" |
|
515 |
||
516 |
lemma linorder_less_linear: "!!x::'a::linorder. x<y | x=y | y<x" |
|
517 |
apply (simp add: order_less_le) |
|
518 |
apply (insert linorder_linear) |
|
519 |
apply blast |
|
520 |
done |
|
521 |
||
522 |
lemma linorder_cases [case_names less equal greater]: |
|
523 |
"((x::'a::linorder) < y ==> P) ==> (x = y ==> P) ==> (y < x ==> P) ==> P" |
|
524 |
apply (insert linorder_less_linear) |
|
525 |
apply blast |
|
526 |
done |
|
527 |
||
528 |
lemma linorder_not_less: "!!x::'a::linorder. (~ x < y) = (y <= x)" |
|
529 |
apply (simp add: order_less_le) |
|
530 |
apply (insert linorder_linear) |
|
531 |
apply (blast intro: order_antisym) |
|
532 |
done |
|
533 |
||
534 |
lemma linorder_not_le: "!!x::'a::linorder. (~ x <= y) = (y < x)" |
|
535 |
apply (simp add: order_less_le) |
|
536 |
apply (insert linorder_linear) |
|
537 |
apply (blast intro: order_antisym) |
|
538 |
done |
|
539 |
||
540 |
lemma linorder_neq_iff: "!!x::'a::linorder. (x ~= y) = (x<y | y<x)" |
|
541 |
apply (cut_tac x = x and y = y in linorder_less_linear) |
|
542 |
apply auto |
|
543 |
done |
|
544 |
||
545 |
lemma linorder_neqE: "x ~= (y::'a::linorder) ==> (x < y ==> R) ==> (y < x ==> R) ==> R" |
|
546 |
apply (simp add: linorder_neq_iff) |
|
547 |
apply blast |
|
548 |
done |
|
549 |
||
550 |
||
551 |
subsubsection "Min and max on (linear) orders" |
|
552 |
||
553 |
lemma min_same [simp]: "min (x::'a::order) x = x" |
|
554 |
by (simp add: min_def) |
|
555 |
||
556 |
lemma max_same [simp]: "max (x::'a::order) x = x" |
|
557 |
by (simp add: max_def) |
|
558 |
||
559 |
lemma le_max_iff_disj: "!!z::'a::linorder. (z <= max x y) = (z <= x | z <= y)" |
|
560 |
apply (simp add: max_def) |
|
561 |
apply (insert linorder_linear) |
|
562 |
apply (blast intro: order_trans) |
|
563 |
done |
|
564 |
||
565 |
lemma le_maxI1: "(x::'a::linorder) <= max x y" |
|
566 |
by (simp add: le_max_iff_disj) |
|
567 |
||
568 |
lemma le_maxI2: "(y::'a::linorder) <= max x y" |
|
569 |
-- {* CANNOT use with @{text "[intro!]"} because blast will give PROOF FAILED. *} |
|
570 |
by (simp add: le_max_iff_disj) |
|
571 |
||
572 |
lemma less_max_iff_disj: "!!z::'a::linorder. (z < max x y) = (z < x | z < y)" |
|
573 |
apply (simp add: max_def order_le_less) |
|
574 |
apply (insert linorder_less_linear) |
|
575 |
apply (blast intro: order_less_trans) |
|
576 |
done |
|
577 |
||
578 |
lemma max_le_iff_conj [simp]: |
|
579 |
"!!z::'a::linorder. (max x y <= z) = (x <= z & y <= z)" |
|
580 |
apply (simp add: max_def) |
|
581 |
apply (insert linorder_linear) |
|
582 |
apply (blast intro: order_trans) |
|
583 |
done |
|
584 |
||
585 |
lemma max_less_iff_conj [simp]: |
|
586 |
"!!z::'a::linorder. (max x y < z) = (x < z & y < z)" |
|
587 |
apply (simp add: order_le_less max_def) |
|
588 |
apply (insert linorder_less_linear) |
|
589 |
apply (blast intro: order_less_trans) |
|
590 |
done |
|
591 |
||
592 |
lemma le_min_iff_conj [simp]: |
|
593 |
"!!z::'a::linorder. (z <= min x y) = (z <= x & z <= y)" |
|
594 |
-- {* @{text "[iff]"} screws up a Q{text blast} in MiniML *} |
|
595 |
apply (simp add: min_def) |
|
596 |
apply (insert linorder_linear) |
|
597 |
apply (blast intro: order_trans) |
|
598 |
done |
|
599 |
||
600 |
lemma min_less_iff_conj [simp]: |
|
601 |
"!!z::'a::linorder. (z < min x y) = (z < x & z < y)" |
|
602 |
apply (simp add: order_le_less min_def) |
|
603 |
apply (insert linorder_less_linear) |
|
604 |
apply (blast intro: order_less_trans) |
|
605 |
done |
|
606 |
||
607 |
lemma min_le_iff_disj: "!!z::'a::linorder. (min x y <= z) = (x <= z | y <= z)" |
|
608 |
apply (simp add: min_def) |
|
609 |
apply (insert linorder_linear) |
|
610 |
apply (blast intro: order_trans) |
|
611 |
done |
|
612 |
||
613 |
lemma min_less_iff_disj: "!!z::'a::linorder. (min x y < z) = (x < z | y < z)" |
|
614 |
apply (simp add: min_def order_le_less) |
|
615 |
apply (insert linorder_less_linear) |
|
616 |
apply (blast intro: order_less_trans) |
|
617 |
done |
|
618 |
||
619 |
lemma split_min: |
|
620 |
"P (min (i::'a::linorder) j) = ((i <= j --> P(i)) & (~ i <= j --> P(j)))" |
|
621 |
by (simp add: min_def) |
|
622 |
||
623 |
lemma split_max: |
|
624 |
"P (max (i::'a::linorder) j) = ((i <= j --> P(j)) & (~ i <= j --> P(i)))" |
|
625 |
by (simp add: max_def) |
|
626 |
||
627 |
||
628 |
subsubsection "Bounded quantifiers" |
|
629 |
||
630 |
syntax |
|
631 |
"_lessAll" :: "[idt, 'a, bool] => bool" ("(3ALL _<_./ _)" [0, 0, 10] 10) |
|
632 |
"_lessEx" :: "[idt, 'a, bool] => bool" ("(3EX _<_./ _)" [0, 0, 10] 10) |
|
633 |
"_leAll" :: "[idt, 'a, bool] => bool" ("(3ALL _<=_./ _)" [0, 0, 10] 10) |
|
634 |
"_leEx" :: "[idt, 'a, bool] => bool" ("(3EX _<=_./ _)" [0, 0, 10] 10) |
|
635 |
||
636 |
syntax (symbols) |
|
637 |
"_lessAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_<_./ _)" [0, 0, 10] 10) |
|
638 |
"_lessEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_<_./ _)" [0, 0, 10] 10) |
|
639 |
"_leAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10) |
|
640 |
"_leEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<le>_./ _)" [0, 0, 10] 10) |
|
641 |
||
642 |
syntax (HOL) |
|
643 |
"_lessAll" :: "[idt, 'a, bool] => bool" ("(3! _<_./ _)" [0, 0, 10] 10) |
|
644 |
"_lessEx" :: "[idt, 'a, bool] => bool" ("(3? _<_./ _)" [0, 0, 10] 10) |
|
645 |
"_leAll" :: "[idt, 'a, bool] => bool" ("(3! _<=_./ _)" [0, 0, 10] 10) |
|
646 |
"_leEx" :: "[idt, 'a, bool] => bool" ("(3? _<=_./ _)" [0, 0, 10] 10) |
|
647 |
||
648 |
translations |
|
649 |
"ALL x<y. P" => "ALL x. x < y --> P" |
|
650 |
"EX x<y. P" => "EX x. x < y & P" |
|
651 |
"ALL x<=y. P" => "ALL x. x <= y --> P" |
|
652 |
"EX x<=y. P" => "EX x. x <= y & P" |
|
653 |
||
923 | 654 |
end |