equal
deleted
inserted
replaced
13 by auto |
13 by auto |
14 |
14 |
15 lemma COND_DEF:"(If b t f) = (@x. ((b = True) --> (x = t)) & ((b = False) --> (x = f)))" |
15 lemma COND_DEF:"(If b t f) = (@x. ((b = True) --> (x = t)) & ((b = False) --> (x = f)))" |
16 by auto |
16 by auto |
17 |
17 |
18 constdefs |
18 definition LET :: "['a \<Rightarrow> 'b,'a] \<Rightarrow> 'b" where |
19 LET :: "['a \<Rightarrow> 'b,'a] \<Rightarrow> 'b" |
|
20 "LET f s == f s" |
19 "LET f s == f s" |
21 |
20 |
22 lemma [hol4rew]: "LET f s = Let s f" |
21 lemma [hol4rew]: "LET f s = Let s f" |
23 by (simp add: LET_def Let_def) |
22 by (simp add: LET_def Let_def) |
24 |
23 |
117 ..; |
116 ..; |
118 |
117 |
119 lemma LESS_OR_EQ: "m <= (n::nat) = (m < n | m = n)" |
118 lemma LESS_OR_EQ: "m <= (n::nat) = (m < n | m = n)" |
120 by auto |
119 by auto |
121 |
120 |
122 constdefs |
121 definition nat_gt :: "nat => nat => bool" where |
123 nat_gt :: "nat => nat => bool" |
|
124 "nat_gt == %m n. n < m" |
122 "nat_gt == %m n. n < m" |
125 nat_ge :: "nat => nat => bool" |
123 |
|
124 definition nat_ge :: "nat => nat => bool" where |
126 "nat_ge == %m n. nat_gt m n | m = n" |
125 "nat_ge == %m n. nat_gt m n | m = n" |
127 |
126 |
128 lemma [hol4rew]: "nat_gt m n = (n < m)" |
127 lemma [hol4rew]: "nat_gt m n = (n < m)" |
129 by (simp add: nat_gt_def) |
128 by (simp add: nat_gt_def) |
130 |
129 |
198 show "m < n" |
197 show "m < n" |
199 .. |
198 .. |
200 qed |
199 qed |
201 qed; |
200 qed; |
202 |
201 |
203 constdefs |
202 definition FUNPOW :: "('a => 'a) => nat => 'a => 'a" where |
204 FUNPOW :: "('a => 'a) => nat => 'a => 'a" |
|
205 "FUNPOW f n == f ^^ n" |
203 "FUNPOW f n == f ^^ n" |
206 |
204 |
207 lemma FUNPOW: "(ALL f x. (f ^^ 0) x = x) & |
205 lemma FUNPOW: "(ALL f x. (f ^^ 0) x = x) & |
208 (ALL f n x. (f ^^ Suc n) x = (f ^^ n) (f x))" |
206 (ALL f n x. (f ^^ Suc n) x = (f ^^ n) (f x))" |
209 by (simp add: funpow_swap1) |
207 by (simp add: funpow_swap1) |
227 by (simp add: min_def) |
225 by (simp add: min_def) |
228 |
226 |
229 lemma DIVISION: "(0::nat) < n --> (!k. (k = k div n * n + k mod n) & k mod n < n)" |
227 lemma DIVISION: "(0::nat) < n --> (!k. (k = k div n * n + k mod n) & k mod n < n)" |
230 by simp |
228 by simp |
231 |
229 |
232 constdefs |
230 definition ALT_ZERO :: nat where |
233 ALT_ZERO :: nat |
|
234 "ALT_ZERO == 0" |
231 "ALT_ZERO == 0" |
235 NUMERAL_BIT1 :: "nat \<Rightarrow> nat" |
232 |
|
233 definition NUMERAL_BIT1 :: "nat \<Rightarrow> nat" where |
236 "NUMERAL_BIT1 n == n + (n + Suc 0)" |
234 "NUMERAL_BIT1 n == n + (n + Suc 0)" |
237 NUMERAL_BIT2 :: "nat \<Rightarrow> nat" |
235 |
|
236 definition NUMERAL_BIT2 :: "nat \<Rightarrow> nat" where |
238 "NUMERAL_BIT2 n == n + (n + Suc (Suc 0))" |
237 "NUMERAL_BIT2 n == n + (n + Suc (Suc 0))" |
239 NUMERAL :: "nat \<Rightarrow> nat" |
238 |
|
239 definition NUMERAL :: "nat \<Rightarrow> nat" where |
240 "NUMERAL x == x" |
240 "NUMERAL x == x" |
241 |
241 |
242 lemma [hol4rew]: "NUMERAL ALT_ZERO = 0" |
242 lemma [hol4rew]: "NUMERAL ALT_ZERO = 0" |
243 by (simp add: ALT_ZERO_def NUMERAL_def) |
243 by (simp add: ALT_ZERO_def NUMERAL_def) |
244 |
244 |
327 qed |
327 qed |
328 |
328 |
329 lemma NULL_DEF: "(null [] = True) & (!h t. null (h # t) = False)" |
329 lemma NULL_DEF: "(null [] = True) & (!h t. null (h # t) = False)" |
330 by simp |
330 by simp |
331 |
331 |
332 constdefs |
332 definition sum :: "nat list \<Rightarrow> nat" where |
333 sum :: "nat list \<Rightarrow> nat" |
|
334 "sum l == foldr (op +) l 0" |
333 "sum l == foldr (op +) l 0" |
335 |
334 |
336 lemma SUM: "(sum [] = 0) & (!h t. sum (h#t) = h + sum t)" |
335 lemma SUM: "(sum [] = 0) & (!h t. sum (h#t) = h + sum t)" |
337 by (simp add: sum_def) |
336 by (simp add: sum_def) |
338 |
337 |
357 |
356 |
358 lemma REPLICATE: "(ALL x. replicate 0 x = []) & |
357 lemma REPLICATE: "(ALL x. replicate 0 x = []) & |
359 (ALL n x. replicate (Suc n) x = x # replicate n x)" |
358 (ALL n x. replicate (Suc n) x = x # replicate n x)" |
360 by simp |
359 by simp |
361 |
360 |
362 constdefs |
361 definition FOLDR :: "[['a,'b]\<Rightarrow>'b,'b,'a list] \<Rightarrow> 'b" where |
363 FOLDR :: "[['a,'b]\<Rightarrow>'b,'b,'a list] \<Rightarrow> 'b" |
|
364 "FOLDR f e l == foldr f l e" |
362 "FOLDR f e l == foldr f l e" |
365 |
363 |
366 lemma [hol4rew]: "FOLDR f e l = foldr f l e" |
364 lemma [hol4rew]: "FOLDR f e l = foldr f l e" |
367 by (simp add: FOLDR_def) |
365 by (simp add: FOLDR_def) |
368 |
366 |
416 qed |
414 qed |
417 |
415 |
418 lemma list_CASES: "(l = []) | (? t h. l = h#t)" |
416 lemma list_CASES: "(l = []) | (? t h. l = h#t)" |
419 by (induct l,auto) |
417 by (induct l,auto) |
420 |
418 |
421 constdefs |
419 definition ZIP :: "'a list * 'b list \<Rightarrow> ('a * 'b) list" where |
422 ZIP :: "'a list * 'b list \<Rightarrow> ('a * 'b) list" |
|
423 "ZIP == %(a,b). zip a b" |
420 "ZIP == %(a,b). zip a b" |
424 |
421 |
425 lemma ZIP: "(zip [] [] = []) & |
422 lemma ZIP: "(zip [] [] = []) & |
426 (!x1 l1 x2 l2. zip (x1#l1) (x2#l2) = (x1,x2)#zip l1 l2)" |
423 (!x1 l1 x2 l2. zip (x1#l1) (x2#l2) = (x1,x2)#zip l1 l2)" |
427 by simp |
424 by simp |
512 by (simp add: abs_if) |
509 by (simp add: abs_if) |
513 |
510 |
514 lemma pow: "(!x::real. x ^ 0 = 1) & (!x::real. ALL n. x ^ (Suc n) = x * x ^ n)" |
511 lemma pow: "(!x::real. x ^ 0 = 1) & (!x::real. ALL n. x ^ (Suc n) = x * x ^ n)" |
515 by simp |
512 by simp |
516 |
513 |
517 constdefs |
514 definition real_gt :: "real => real => bool" where |
518 real_gt :: "real => real => bool" |
|
519 "real_gt == %x y. y < x" |
515 "real_gt == %x y. y < x" |
520 |
516 |
521 lemma [hol4rew]: "real_gt x y = (y < x)" |
517 lemma [hol4rew]: "real_gt x y = (y < x)" |
522 by (simp add: real_gt_def) |
518 by (simp add: real_gt_def) |
523 |
519 |
524 lemma real_gt: "ALL x (y::real). (y < x) = (y < x)" |
520 lemma real_gt: "ALL x (y::real). (y < x) = (y < x)" |
525 by simp |
521 by simp |
526 |
522 |
527 constdefs |
523 definition real_ge :: "real => real => bool" where |
528 real_ge :: "real => real => bool" |
|
529 "real_ge x y == y <= x" |
524 "real_ge x y == y <= x" |
530 |
525 |
531 lemma [hol4rew]: "real_ge x y = (y <= x)" |
526 lemma [hol4rew]: "real_ge x y = (y <= x)" |
532 by (simp add: real_ge_def) |
527 by (simp add: real_ge_def) |
533 |
528 |