author | haftmann |
Thu, 18 Nov 2010 17:01:16 +0100 | |
changeset 40607 | 30d512bf47a7 |
parent 39246 | 9e58f0499f57 |
child 41413 | 64cd30d6b0b8 |
permissions | -rw-r--r-- |
14620
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset
|
1 |
(* Title: HOL/Import/HOL4Compat.thy |
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset
|
2 |
Author: Sebastian Skalberg (TU Muenchen) |
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset
|
3 |
*) |
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset
|
4 |
|
30660 | 5 |
theory HOL4Compat |
32479 | 6 |
imports HOL4Setup Complex_Main "~~/src/HOL/Old_Number_Theory/Primes" ContNotDenum |
19064 | 7 |
begin |
14516 | 8 |
|
37596 | 9 |
abbreviation (input) mem (infixl "mem" 55) where "x mem xs \<equiv> List.member xs x" |
30660 | 10 |
no_notation differentiable (infixl "differentiable" 60) |
11 |
no_notation sums (infixr "sums" 80) |
|
12 |
||
14516 | 13 |
lemma EXISTS_UNIQUE_DEF: "(Ex1 P) = (Ex P & (ALL x y. P x & P y --> (x = y)))" |
14 |
by auto |
|
15 |
||
16 |
lemma COND_DEF:"(If b t f) = (@x. ((b = True) --> (x = t)) & ((b = False) --> (x = f)))" |
|
17 |
by auto |
|
18 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset
|
19 |
definition LET :: "['a \<Rightarrow> 'b,'a] \<Rightarrow> 'b" where |
14516 | 20 |
"LET f s == f s" |
21 |
||
22 |
lemma [hol4rew]: "LET f s = Let s f" |
|
23 |
by (simp add: LET_def Let_def) |
|
24 |
||
25 |
lemmas [hol4rew] = ONE_ONE_rew |
|
26 |
||
27 |
lemma bool_case_DEF: "(bool_case x y b) = (if b then x else y)" |
|
30660 | 28 |
by simp |
14516 | 29 |
|
30 |
lemma INR_INL_11: "(ALL y x. (Inl x = Inl y) = (x = y)) & (ALL y x. (Inr x = Inr y) = (x = y))" |
|
31 |
by safe |
|
32 |
||
17188 | 33 |
(*lemma INL_neq_INR: "ALL v1 v2. Sum_Type.Inr v2 ~= Sum_Type.Inl v1" |
34 |
by simp*) |
|
35 |
||
39246 | 36 |
primrec ISL :: "'a + 'b => bool" where |
14516 | 37 |
"ISL (Inl x) = True" |
39246 | 38 |
| "ISL (Inr x) = False" |
14516 | 39 |
|
39246 | 40 |
primrec ISR :: "'a + 'b => bool" where |
14516 | 41 |
"ISR (Inl x) = False" |
39246 | 42 |
| "ISR (Inr x) = True" |
14516 | 43 |
|
44 |
lemma ISL: "(ALL x. ISL (Inl x)) & (ALL y. ~ISL (Inr y))" |
|
45 |
by simp |
|
46 |
||
47 |
lemma ISR: "(ALL x. ISR (Inr x)) & (ALL y. ~ISR (Inl y))" |
|
48 |
by simp |
|
49 |
||
39246 | 50 |
primrec OUTL :: "'a + 'b => 'a" where |
14516 | 51 |
"OUTL (Inl x) = x" |
52 |
||
39246 | 53 |
primrec OUTR :: "'a + 'b => 'b" where |
14516 | 54 |
"OUTR (Inr x) = x" |
55 |
||
56 |
lemma OUTL: "OUTL (Inl x) = x" |
|
57 |
by simp |
|
58 |
||
59 |
lemma OUTR: "OUTR (Inr x) = x" |
|
60 |
by simp |
|
61 |
||
62 |
lemma sum_case_def: "(ALL f g x. sum_case f g (Inl x) = f x) & (ALL f g y. sum_case f g (Inr y) = g y)" |
|
63 |
by simp; |
|
64 |
||
65 |
lemma one: "ALL v. v = ()" |
|
66 |
by simp; |
|
67 |
||
68 |
lemma option_case_def: "(!u f. option_case u f None = u) & (!u f x. option_case u f (Some x) = f x)" |
|
69 |
by simp |
|
70 |
||
30235
58d147683393
Made Option a separate theory and renamed option_map to Option.map
nipkow
parents:
29044
diff
changeset
|
71 |
lemma OPTION_MAP_DEF: "(!f x. Option.map f (Some x) = Some (f x)) & (!f. Option.map f None = None)" |
14516 | 72 |
by simp |
73 |
||
39246 | 74 |
primrec IS_SOME :: "'a option => bool" where |
14516 | 75 |
"IS_SOME (Some x) = True" |
39246 | 76 |
| "IS_SOME None = False" |
14516 | 77 |
|
39246 | 78 |
primrec IS_NONE :: "'a option => bool" where |
14516 | 79 |
"IS_NONE (Some x) = False" |
39246 | 80 |
| "IS_NONE None = True" |
14516 | 81 |
|
82 |
lemma IS_NONE_DEF: "(!x. IS_NONE (Some x) = False) & (IS_NONE None = True)" |
|
83 |
by simp |
|
84 |
||
85 |
lemma IS_SOME_DEF: "(!x. IS_SOME (Some x) = True) & (IS_SOME None = False)" |
|
86 |
by simp |
|
87 |
||
39246 | 88 |
primrec OPTION_JOIN :: "'a option option => 'a option" where |
14516 | 89 |
"OPTION_JOIN None = None" |
39246 | 90 |
| "OPTION_JOIN (Some x) = x" |
14516 | 91 |
|
92 |
lemma OPTION_JOIN_DEF: "(OPTION_JOIN None = None) & (ALL x. OPTION_JOIN (Some x) = x)" |
|
39246 | 93 |
by simp |
14516 | 94 |
|
95 |
lemma PAIR: "(fst x,snd x) = x" |
|
96 |
by simp |
|
97 |
||
40607 | 98 |
lemma PAIR_MAP: "map_pair f g p = (f (fst p),g (snd p))" |
99 |
by (simp add: map_pair_def split_def) |
|
14516 | 100 |
|
101 |
lemma pair_case_def: "split = split" |
|
102 |
..; |
|
103 |
||
104 |
lemma LESS_OR_EQ: "m <= (n::nat) = (m < n | m = n)" |
|
105 |
by auto |
|
106 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset
|
107 |
definition nat_gt :: "nat => nat => bool" where |
14516 | 108 |
"nat_gt == %m n. n < m" |
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset
|
109 |
|
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset
|
110 |
definition nat_ge :: "nat => nat => bool" where |
14516 | 111 |
"nat_ge == %m n. nat_gt m n | m = n" |
112 |
||
113 |
lemma [hol4rew]: "nat_gt m n = (n < m)" |
|
114 |
by (simp add: nat_gt_def) |
|
115 |
||
116 |
lemma [hol4rew]: "nat_ge m n = (n <= m)" |
|
117 |
by (auto simp add: nat_ge_def nat_gt_def) |
|
118 |
||
119 |
lemma GREATER_DEF: "ALL m n. (n < m) = (n < m)" |
|
120 |
by simp |
|
121 |
||
122 |
lemma GREATER_OR_EQ: "ALL m n. n <= (m::nat) = (n < m | m = n)" |
|
123 |
by auto |
|
124 |
||
125 |
lemma LESS_DEF: "m < n = (? P. (!n. P (Suc n) --> P n) & P m & ~P n)" |
|
126 |
proof safe |
|
127 |
assume "m < n" |
|
128 |
def P == "%n. n <= m" |
|
129 |
have "(!n. P (Suc n) \<longrightarrow> P n) & P m & ~P n" |
|
130 |
proof (auto simp add: P_def) |
|
131 |
assume "n <= m" |
|
132 |
from prems |
|
133 |
show False |
|
134 |
by auto |
|
135 |
qed |
|
136 |
thus "? P. (!n. P (Suc n) \<longrightarrow> P n) & P m & ~P n" |
|
137 |
by auto |
|
138 |
next |
|
139 |
fix P |
|
140 |
assume alln: "!n. P (Suc n) \<longrightarrow> P n" |
|
141 |
assume pm: "P m" |
|
142 |
assume npn: "~P n" |
|
143 |
have "!k q. q + k = m \<longrightarrow> P q" |
|
144 |
proof |
|
145 |
fix k |
|
146 |
show "!q. q + k = m \<longrightarrow> P q" |
|
147 |
proof (induct k,simp_all) |
|
23389 | 148 |
show "P m" by fact |
14516 | 149 |
next |
150 |
fix k |
|
151 |
assume ind: "!q. q + k = m \<longrightarrow> P q" |
|
152 |
show "!q. Suc (q + k) = m \<longrightarrow> P q" |
|
153 |
proof (rule+) |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
154 |
fix q |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
155 |
assume "Suc (q + k) = m" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
156 |
hence "(Suc q) + k = m" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
157 |
by simp |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
158 |
with ind |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
159 |
have psq: "P (Suc q)" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
160 |
by simp |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
161 |
from alln |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
162 |
have "P (Suc q) --> P q" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
163 |
.. |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
164 |
with psq |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
165 |
show "P q" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
166 |
by simp |
14516 | 167 |
qed |
168 |
qed |
|
169 |
qed |
|
170 |
hence "!q. q + (m - n) = m \<longrightarrow> P q" |
|
171 |
.. |
|
172 |
hence hehe: "n + (m - n) = m \<longrightarrow> P n" |
|
173 |
.. |
|
174 |
show "m < n" |
|
175 |
proof (rule classical) |
|
176 |
assume "~(m<n)" |
|
177 |
hence "n <= m" |
|
178 |
by simp |
|
179 |
with hehe |
|
180 |
have "P n" |
|
181 |
by simp |
|
182 |
with npn |
|
183 |
show "m < n" |
|
184 |
.. |
|
185 |
qed |
|
186 |
qed; |
|
187 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset
|
188 |
definition FUNPOW :: "('a => 'a) => nat => 'a => 'a" where |
30971 | 189 |
"FUNPOW f n == f ^^ n" |
14516 | 190 |
|
30971 | 191 |
lemma FUNPOW: "(ALL f x. (f ^^ 0) x = x) & |
192 |
(ALL f n x. (f ^^ Suc n) x = (f ^^ n) (f x))" |
|
30952
7ab2716dd93b
power operation on functions with syntax o^; power operation on relations with syntax ^^
haftmann
parents:
30660
diff
changeset
|
193 |
by (simp add: funpow_swap1) |
14516 | 194 |
|
30971 | 195 |
lemma [hol4rew]: "FUNPOW f n = f ^^ n" |
14516 | 196 |
by (simp add: FUNPOW_def) |
197 |
||
198 |
lemma ADD: "(!n. (0::nat) + n = n) & (!m n. Suc m + n = Suc (m + n))" |
|
199 |
by simp |
|
200 |
||
201 |
lemma MULT: "(!n. (0::nat) * n = 0) & (!m n. Suc m * n = m * n + n)" |
|
202 |
by simp |
|
203 |
||
204 |
lemma SUB: "(!m. (0::nat) - m = 0) & (!m n. (Suc m) - n = (if m < n then 0 else Suc (m - n)))" |
|
30952
7ab2716dd93b
power operation on functions with syntax o^; power operation on relations with syntax ^^
haftmann
parents:
30660
diff
changeset
|
205 |
by (simp) arith |
14516 | 206 |
|
207 |
lemma MAX_DEF: "max (m::nat) n = (if m < n then n else m)" |
|
208 |
by (simp add: max_def) |
|
209 |
||
210 |
lemma MIN_DEF: "min (m::nat) n = (if m < n then m else n)" |
|
211 |
by (simp add: min_def) |
|
212 |
||
213 |
lemma DIVISION: "(0::nat) < n --> (!k. (k = k div n * n + k mod n) & k mod n < n)" |
|
214 |
by simp |
|
215 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset
|
216 |
definition ALT_ZERO :: nat where |
14516 | 217 |
"ALT_ZERO == 0" |
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset
|
218 |
|
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset
|
219 |
definition NUMERAL_BIT1 :: "nat \<Rightarrow> nat" where |
14516 | 220 |
"NUMERAL_BIT1 n == n + (n + Suc 0)" |
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset
|
221 |
|
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset
|
222 |
definition NUMERAL_BIT2 :: "nat \<Rightarrow> nat" where |
14516 | 223 |
"NUMERAL_BIT2 n == n + (n + Suc (Suc 0))" |
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset
|
224 |
|
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset
|
225 |
definition NUMERAL :: "nat \<Rightarrow> nat" where |
14516 | 226 |
"NUMERAL x == x" |
227 |
||
228 |
lemma [hol4rew]: "NUMERAL ALT_ZERO = 0" |
|
229 |
by (simp add: ALT_ZERO_def NUMERAL_def) |
|
230 |
||
231 |
lemma [hol4rew]: "NUMERAL (NUMERAL_BIT1 ALT_ZERO) = 1" |
|
232 |
by (simp add: ALT_ZERO_def NUMERAL_BIT1_def NUMERAL_def) |
|
233 |
||
234 |
lemma [hol4rew]: "NUMERAL (NUMERAL_BIT2 ALT_ZERO) = 2" |
|
235 |
by (simp add: ALT_ZERO_def NUMERAL_BIT2_def NUMERAL_def) |
|
236 |
||
237 |
lemma EXP: "(!m. m ^ 0 = (1::nat)) & (!m n. m ^ Suc n = m * (m::nat) ^ n)" |
|
238 |
by auto |
|
239 |
||
240 |
lemma num_case_def: "(!b f. nat_case b f 0 = b) & (!b f n. nat_case b f (Suc n) = f n)" |
|
241 |
by simp; |
|
242 |
||
243 |
lemma divides_def: "(a::nat) dvd b = (? q. b = q * a)" |
|
244 |
by (auto simp add: dvd_def); |
|
245 |
||
246 |
lemma list_case_def: "(!v f. list_case v f [] = v) & (!v f a0 a1. list_case v f (a0#a1) = f a0 a1)" |
|
247 |
by simp |
|
248 |
||
39246 | 249 |
primrec list_size :: "('a \<Rightarrow> nat) \<Rightarrow> 'a list \<Rightarrow> nat" where |
250 |
"list_size f [] = 0" |
|
251 |
| "list_size f (a0#a1) = 1 + (f a0 + list_size f a1)" |
|
14516 | 252 |
|
39246 | 253 |
lemma list_size_def': "(!f. list_size f [] = 0) & |
14516 | 254 |
(!f a0 a1. list_size f (a0#a1) = 1 + (f a0 + list_size f a1))" |
255 |
by simp |
|
256 |
||
257 |
lemma list_case_cong: "! M M' v f. M = M' & (M' = [] \<longrightarrow> v = v') & |
|
258 |
(!a0 a1. (M' = a0#a1) \<longrightarrow> (f a0 a1 = f' a0 a1)) --> |
|
259 |
(list_case v f M = list_case v' f' M')" |
|
260 |
proof clarify |
|
261 |
fix M M' v f |
|
262 |
assume "M' = [] \<longrightarrow> v = v'" |
|
263 |
and "!a0 a1. M' = a0 # a1 \<longrightarrow> f a0 a1 = f' a0 a1" |
|
264 |
show "list_case v f M' = list_case v' f' M'" |
|
265 |
proof (rule List.list.case_cong) |
|
266 |
show "M' = M'" |
|
267 |
.. |
|
268 |
next |
|
269 |
assume "M' = []" |
|
270 |
with prems |
|
271 |
show "v = v'" |
|
272 |
by auto |
|
273 |
next |
|
274 |
fix a0 a1 |
|
275 |
assume "M' = a0 # a1" |
|
276 |
with prems |
|
277 |
show "f a0 a1 = f' a0 a1" |
|
278 |
by auto |
|
279 |
qed |
|
280 |
qed |
|
281 |
||
282 |
lemma list_Axiom: "ALL f0 f1. EX fn. (fn [] = f0) & (ALL a0 a1. fn (a0#a1) = f1 a0 a1 (fn a1))" |
|
283 |
proof safe |
|
284 |
fix f0 f1 |
|
285 |
def fn == "list_rec f0 f1" |
|
286 |
have "fn [] = f0 & (ALL a0 a1. fn (a0 # a1) = f1 a0 a1 (fn a1))" |
|
287 |
by (simp add: fn_def) |
|
288 |
thus "EX fn. fn [] = f0 & (ALL a0 a1. fn (a0 # a1) = f1 a0 a1 (fn a1))" |
|
289 |
by auto |
|
290 |
qed |
|
291 |
||
292 |
lemma list_Axiom_old: "EX! fn. (fn [] = x) & (ALL h t. fn (h#t) = f (fn t) h t)" |
|
293 |
proof safe |
|
294 |
def fn == "list_rec x (%h t r. f r h t)" |
|
295 |
have "fn [] = x & (ALL h t. fn (h # t) = f (fn t) h t)" |
|
296 |
by (simp add: fn_def) |
|
297 |
thus "EX fn. fn [] = x & (ALL h t. fn (h # t) = f (fn t) h t)" |
|
298 |
by auto |
|
299 |
next |
|
300 |
fix fn1 fn2 |
|
301 |
assume "ALL h t. fn1 (h # t) = f (fn1 t) h t" |
|
302 |
assume "ALL h t. fn2 (h # t) = f (fn2 t) h t" |
|
303 |
assume "fn2 [] = fn1 []" |
|
304 |
show "fn1 = fn2" |
|
305 |
proof |
|
306 |
fix xs |
|
307 |
show "fn1 xs = fn2 xs" |
|
308 |
by (induct xs,simp_all add: prems) |
|
309 |
qed |
|
310 |
qed |
|
311 |
||
37596 | 312 |
lemma NULL_DEF: "(List.null [] = True) & (!h t. List.null (h # t) = False)" |
313 |
by (simp add: null_def) |
|
14516 | 314 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset
|
315 |
definition sum :: "nat list \<Rightarrow> nat" where |
14516 | 316 |
"sum l == foldr (op +) l 0" |
317 |
||
318 |
lemma SUM: "(sum [] = 0) & (!h t. sum (h#t) = h + sum t)" |
|
319 |
by (simp add: sum_def) |
|
320 |
||
321 |
lemma APPEND: "(!l. [] @ l = l) & (!l1 l2 h. (h#l1) @ l2 = h# l1 @ l2)" |
|
322 |
by simp |
|
323 |
||
324 |
lemma FLAT: "(concat [] = []) & (!h t. concat (h#t) = h @ (concat t))" |
|
325 |
by simp |
|
326 |
||
327 |
lemma LENGTH: "(length [] = 0) & (!h t. length (h#t) = Suc (length t))" |
|
328 |
by simp |
|
329 |
||
330 |
lemma MAP: "(!f. map f [] = []) & (!f h t. map f (h#t) = f h#map f t)" |
|
331 |
by simp |
|
332 |
||
37596 | 333 |
lemma MEM: "(!x. List.member [] x = False) & (!x h t. List.member (h#t) x = ((x = h) | List.member t x))" |
334 |
by (simp add: member_def) |
|
14516 | 335 |
|
336 |
lemma FILTER: "(!P. filter P [] = []) & (!P h t. |
|
337 |
filter P (h#t) = (if P h then h#filter P t else filter P t))" |
|
338 |
by simp |
|
339 |
||
340 |
lemma REPLICATE: "(ALL x. replicate 0 x = []) & |
|
341 |
(ALL n x. replicate (Suc n) x = x # replicate n x)" |
|
342 |
by simp |
|
343 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset
|
344 |
definition FOLDR :: "[['a,'b]\<Rightarrow>'b,'b,'a list] \<Rightarrow> 'b" where |
14516 | 345 |
"FOLDR f e l == foldr f l e" |
346 |
||
347 |
lemma [hol4rew]: "FOLDR f e l = foldr f l e" |
|
348 |
by (simp add: FOLDR_def) |
|
349 |
||
350 |
lemma FOLDR: "(!f e. foldr f [] e = e) & (!f e x l. foldr f (x#l) e = f x (foldr f l e))" |
|
351 |
by simp |
|
352 |
||
353 |
lemma FOLDL: "(!f e. foldl f e [] = e) & (!f e x l. foldl f e (x#l) = foldl f (f e x) l)" |
|
354 |
by simp |
|
355 |
||
356 |
lemma EVERY_DEF: "(!P. list_all P [] = True) & (!P h t. list_all P (h#t) = (P h & list_all P t))" |
|
357 |
by simp |
|
358 |
||
37596 | 359 |
lemma list_exists_DEF: "(!P. list_ex P [] = False) & (!P h t. list_ex P (h#t) = (P h | list_ex P t))" |
14516 | 360 |
by simp |
361 |
||
39246 | 362 |
primrec map2 :: "[['a,'b]\<Rightarrow>'c,'a list,'b list] \<Rightarrow> 'c list" where |
14516 | 363 |
map2_Nil: "map2 f [] l2 = []" |
39246 | 364 |
| map2_Cons: "map2 f (x#xs) l2 = f x (hd l2) # map2 f xs (tl l2)" |
14516 | 365 |
|
366 |
lemma MAP2: "(!f. map2 f [] [] = []) & (!f h1 t1 h2 t2. map2 f (h1#t1) (h2#t2) = f h1 h2#map2 f t1 t2)" |
|
367 |
by simp |
|
368 |
||
369 |
lemma list_INDUCT: "\<lbrakk> P [] ; !t. P t \<longrightarrow> (!h. P (h#t)) \<rbrakk> \<Longrightarrow> !l. P l" |
|
370 |
proof |
|
371 |
fix l |
|
372 |
assume "P []" |
|
373 |
assume allt: "!t. P t \<longrightarrow> (!h. P (h # t))" |
|
374 |
show "P l" |
|
375 |
proof (induct l) |
|
23389 | 376 |
show "P []" by fact |
14516 | 377 |
next |
378 |
fix h t |
|
379 |
assume "P t" |
|
380 |
with allt |
|
381 |
have "!h. P (h # t)" |
|
382 |
by auto |
|
383 |
thus "P (h # t)" |
|
384 |
.. |
|
385 |
qed |
|
386 |
qed |
|
387 |
||
388 |
lemma list_CASES: "(l = []) | (? t h. l = h#t)" |
|
389 |
by (induct l,auto) |
|
390 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset
|
391 |
definition ZIP :: "'a list * 'b list \<Rightarrow> ('a * 'b) list" where |
14516 | 392 |
"ZIP == %(a,b). zip a b" |
393 |
||
394 |
lemma ZIP: "(zip [] [] = []) & |
|
395 |
(!x1 l1 x2 l2. zip (x1#l1) (x2#l2) = (x1,x2)#zip l1 l2)" |
|
396 |
by simp |
|
397 |
||
398 |
lemma [hol4rew]: "ZIP (a,b) = zip a b" |
|
399 |
by (simp add: ZIP_def) |
|
400 |
||
39246 | 401 |
primrec unzip :: "('a * 'b) list \<Rightarrow> 'a list * 'b list" where |
14516 | 402 |
unzip_Nil: "unzip [] = ([],[])" |
39246 | 403 |
| unzip_Cons: "unzip (xy#xys) = (let zs = unzip xys in (fst xy # fst zs,snd xy # snd zs))" |
14516 | 404 |
|
405 |
lemma UNZIP: "(unzip [] = ([],[])) & |
|
406 |
(!x l. unzip (x#l) = (fst x#fst (unzip l),snd x#snd (unzip l)))" |
|
407 |
by (simp add: Let_def) |
|
408 |
||
409 |
lemma REVERSE: "(rev [] = []) & (!h t. rev (h#t) = (rev t) @ [h])" |
|
410 |
by simp; |
|
411 |
||
412 |
lemma REAL_SUP_ALLPOS: "\<lbrakk> ALL x. P (x::real) \<longrightarrow> 0 < x ; EX x. P x; EX z. ALL x. P x \<longrightarrow> x < z \<rbrakk> \<Longrightarrow> EX s. ALL y. (EX x. P x & y < x) = (y < s)" |
|
413 |
proof safe |
|
414 |
fix x z |
|
415 |
assume allx: "ALL x. P x \<longrightarrow> 0 < x" |
|
416 |
assume px: "P x" |
|
417 |
assume allx': "ALL x. P x \<longrightarrow> x < z" |
|
418 |
have "EX s. ALL y. (EX x : Collect P. y < x) = (y < s)" |
|
419 |
proof (rule posreal_complete) |
|
420 |
show "ALL x : Collect P. 0 < x" |
|
421 |
proof safe |
|
422 |
fix x |
|
423 |
assume "P x" |
|
424 |
from allx |
|
425 |
have "P x \<longrightarrow> 0 < x" |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
426 |
.. |
14516 | 427 |
thus "0 < x" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
428 |
by (simp add: prems) |
14516 | 429 |
qed |
430 |
next |
|
431 |
from px |
|
432 |
show "EX x. x : Collect P" |
|
433 |
by auto |
|
434 |
next |
|
435 |
from allx' |
|
436 |
show "EX y. ALL x : Collect P. x < y" |
|
437 |
apply simp |
|
438 |
.. |
|
439 |
qed |
|
440 |
thus "EX s. ALL y. (EX x. P x & y < x) = (y < s)" |
|
441 |
by simp |
|
442 |
qed |
|
443 |
||
444 |
lemma REAL_10: "~((1::real) = 0)" |
|
445 |
by simp |
|
446 |
||
447 |
lemma REAL_ADD_ASSOC: "(x::real) + (y + z) = x + y + z" |
|
448 |
by simp |
|
449 |
||
450 |
lemma REAL_MUL_ASSOC: "(x::real) * (y * z) = x * y * z" |
|
451 |
by simp |
|
452 |
||
453 |
lemma REAL_ADD_LINV: "-x + x = (0::real)" |
|
454 |
by simp |
|
455 |
||
456 |
lemma REAL_MUL_LINV: "x ~= (0::real) ==> inverse x * x = 1" |
|
457 |
by simp |
|
458 |
||
459 |
lemma REAL_LT_TOTAL: "((x::real) = y) | x < y | y < x" |
|
460 |
by auto; |
|
461 |
||
462 |
lemma [hol4rew]: "real (0::nat) = 0" |
|
463 |
by simp |
|
464 |
||
465 |
lemma [hol4rew]: "real (1::nat) = 1" |
|
466 |
by simp |
|
467 |
||
468 |
lemma [hol4rew]: "real (2::nat) = 2" |
|
469 |
by simp |
|
470 |
||
471 |
lemma real_lte: "((x::real) <= y) = (~(y < x))" |
|
472 |
by auto |
|
473 |
||
474 |
lemma real_of_num: "((0::real) = 0) & (!n. real (Suc n) = real n + 1)" |
|
475 |
by (simp add: real_of_nat_Suc) |
|
476 |
||
477 |
lemma abs: "abs (x::real) = (if 0 <= x then x else -x)" |
|
15003 | 478 |
by (simp add: abs_if) |
14516 | 479 |
|
480 |
lemma pow: "(!x::real. x ^ 0 = 1) & (!x::real. ALL n. x ^ (Suc n) = x * x ^ n)" |
|
15003 | 481 |
by simp |
14516 | 482 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset
|
483 |
definition real_gt :: "real => real => bool" where |
14516 | 484 |
"real_gt == %x y. y < x" |
485 |
||
486 |
lemma [hol4rew]: "real_gt x y = (y < x)" |
|
487 |
by (simp add: real_gt_def) |
|
488 |
||
489 |
lemma real_gt: "ALL x (y::real). (y < x) = (y < x)" |
|
490 |
by simp |
|
491 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset
|
492 |
definition real_ge :: "real => real => bool" where |
14516 | 493 |
"real_ge x y == y <= x" |
494 |
||
495 |
lemma [hol4rew]: "real_ge x y = (y <= x)" |
|
496 |
by (simp add: real_ge_def) |
|
497 |
||
498 |
lemma real_ge: "ALL x y. (y <= x) = (y <= x)" |
|
499 |
by simp |
|
500 |
||
501 |
end |