equal
deleted
inserted
replaced
5 header {* Compatibility theorems for HOL Light lists *} |
5 header {* Compatibility theorems for HOL Light lists *} |
6 |
6 |
7 theory HOLLightList |
7 theory HOLLightList |
8 imports List |
8 imports List |
9 begin |
9 begin |
|
10 |
|
11 lemma FINITE_SET_OF_LIST: |
|
12 "finite (set l)" |
|
13 by simp |
10 |
14 |
11 lemma AND_ALL2: |
15 lemma AND_ALL2: |
12 "(list_all2 P l m \<and> list_all2 Q l m) = list_all2 (\<lambda>x y. P x y \<and> Q x y) l m" |
16 "(list_all2 P l m \<and> list_all2 Q l m) = list_all2 (\<lambda>x y. P x y \<and> Q x y) l m" |
13 by (induct l m rule: list_induct2') auto |
17 by (induct l m rule: list_induct2') auto |
14 |
18 |
296 apply (induct_tac x) |
300 apply (induct_tac x) |
297 apply simp_all |
301 apply simp_all |
298 done |
302 done |
299 |
303 |
300 lemma IN_SET_OF_LIST: |
304 lemma IN_SET_OF_LIST: |
301 "ALL x l. (x\<in>set l) = list_mem x l" |
305 "(x : set l) = (x : set l)" |
302 by (simp add: member_def) |
306 by simp |
303 |
307 |
304 lemma DEF_BUTLAST: |
308 lemma DEF_BUTLAST: |
305 "butlast = (SOME B. B [] = [] \<and> (\<forall>h t. B (h # t) = (if t = [] then [] else h # B t)))" |
309 "butlast = (SOME B. B [] = [] \<and> (\<forall>h t. B (h # t) = (if t = [] then [] else h # B t)))" |
306 apply (rule some_equality[symmetric]) |
310 apply (rule some_equality[symmetric]) |
307 apply auto |
311 apply auto |