src/HOL/Import/HOLLightList.thy
 author nipkow Mon Jan 30 21:49:41 2012 +0100 (2012-01-30) changeset 46372 6fa9cdb8b850 parent 45827 66c68453455c permissions -rw-r--r--
```     1 (*  Title:      HOL/Import/HOLLightList.thy
```
```     2     Author:     Cezary Kaliszyk
```
```     3 *)
```
```     4
```
```     5 header {* Compatibility theorems for HOL Light lists *}
```
```     6
```
```     7 theory HOLLightList
```
```     8 imports List
```
```     9 begin
```
```    10
```
```    11 lemma FINITE_SET_OF_LIST:
```
```    12   "finite (set l)"
```
```    13   by simp
```
```    14
```
```    15 lemma AND_ALL2:
```
```    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"
```
```    17   by (induct l m rule: list_induct2') auto
```
```    18
```
```    19 lemma MEM_EXISTS_EL:
```
```    20   "(x \<in> set l) = (\<exists>i<length l. x = l ! i)"
```
```    21   by (auto simp add: in_set_conv_nth)
```
```    22
```
```    23 lemma INJECTIVE_MAP:
```
```    24   "(\<forall>l m. map f l = map f m --> l = m) = (\<forall>x y. f x = f y --> x = y)"
```
```    25 proof (intro iffI allI impI)
```
```    26   fix x y
```
```    27   assume "\<forall>l m. map f l = map f m \<longrightarrow> l = m" "f x = f y"
```
```    28   then show "x = y"
```
```    29     by (drule_tac x="[x]" in spec) (drule_tac x="[y]" in spec, simp)
```
```    30 next
```
```    31   fix l m
```
```    32   assume a: "\<forall>x y. f x = f y \<longrightarrow> x = y"
```
```    33   assume "map f l = map f m"
```
```    34   then show "l = m"
```
```    35     by (induct l m rule: list_induct2') (simp_all add: a)
```
```    36 qed
```
```    37
```
```    38 lemma SURJECTIVE_MAP:
```
```    39   "(\<forall>m. EX l. map f l = m) = (\<forall>y. EX x. f x = y)"
```
```    40   apply (intro iffI allI)
```
```    41   apply (drule_tac x="[y]" in spec)
```
```    42   apply (elim exE)
```
```    43   apply (case_tac l)
```
```    44   apply simp
```
```    45   apply (rule_tac x="a" in exI)
```
```    46   apply simp
```
```    47   apply (induct_tac m)
```
```    48   apply simp
```
```    49   apply (drule_tac x="a" in spec)
```
```    50   apply (elim exE)
```
```    51   apply (rule_tac x="x # l" in exI)
```
```    52   apply simp
```
```    53   done
```
```    54
```
```    55 lemma LENGTH_TL:
```
```    56   "l \<noteq> [] \<longrightarrow> length (tl l) = length l - 1"
```
```    57   by simp
```
```    58
```
```    59 lemma DEF_APPEND:
```
```    60   "op @ = (SOME APPEND. (\<forall>l. APPEND [] l = l) \<and> (\<forall>h t l. APPEND (h # t) l = h # APPEND t l))"
```
```    61   apply (rule some_equality[symmetric])
```
```    62   apply (auto simp add: fun_eq_iff)
```
```    63   apply (induct_tac x)
```
```    64   apply simp_all
```
```    65   done
```
```    66
```
```    67 lemma DEF_REVERSE:
```
```    68   "rev = (SOME REVERSE. REVERSE [] = [] \<and> (\<forall>l x. REVERSE (x # l) = (REVERSE l) @ [x]))"
```
```    69   apply (rule some_equality[symmetric])
```
```    70   apply (auto simp add: fun_eq_iff)
```
```    71   apply (induct_tac x)
```
```    72   apply simp_all
```
```    73   done
```
```    74
```
```    75 lemma DEF_LENGTH:
```
```    76   "length = (SOME LENGTH. LENGTH [] = 0 \<and> (\<forall>h t. LENGTH (h # t) = Suc (LENGTH t)))"
```
```    77   apply (rule some_equality[symmetric])
```
```    78   apply (auto simp add: fun_eq_iff)
```
```    79   apply (induct_tac x)
```
```    80   apply simp_all
```
```    81   done
```
```    82
```
```    83 lemma DEF_MAP:
```
```    84   "map = (SOME MAP. (\<forall>f. MAP f [] = []) \<and> (\<forall>f h t. MAP f (h # t) = f h # MAP f t))"
```
```    85   apply (rule some_equality[symmetric])
```
```    86   apply (auto simp add: fun_eq_iff)
```
```    87   apply (induct_tac xa)
```
```    88   apply simp_all
```
```    89   done
```
```    90
```
```    91 lemma DEF_REPLICATE:
```
```    92   "replicate =
```
```    93     (SOME REPLICATE. (\<forall>x. REPLICATE 0 x = []) \<and> (\<forall>n x. REPLICATE (Suc n) x = x # REPLICATE n x))"
```
```    94   apply (rule some_equality[symmetric])
```
```    95   apply (auto simp add: fun_eq_iff)
```
```    96   apply (induct_tac x)
```
```    97   apply simp_all
```
```    98   done
```
```    99
```
```   100 lemma DEF_ITLIST:
```
```   101   "foldr = (SOME ITLIST. (\<forall>f b. ITLIST f [] b = b) \<and> (\<forall>h f t b. ITLIST f (h # t) b = f h (ITLIST f t b)))"
```
```   102   apply (rule some_equality[symmetric])
```
```   103   apply (auto simp add: fun_eq_iff)
```
```   104   apply (induct_tac xa)
```
```   105   apply simp_all
```
```   106   done
```
```   107
```
```   108 lemma DEF_ALL2: "list_all2 =
```
```   109   (SOME ALL2.
```
```   110     (\<forall>P l2. ALL2 P [] l2 = (l2 = [])) \<and>
```
```   111     (\<forall>h1 P t1 l2.
```
```   112       ALL2 P (h1 # t1) l2 = (if l2 = [] then False else P h1 (hd l2) \<and> ALL2 P t1 (tl l2))))"
```
```   113   apply (rule some_equality[symmetric])
```
```   114   apply (auto)
```
```   115   apply (case_tac l2, simp_all)
```
```   116   apply (case_tac l2, simp_all)
```
```   117   apply (case_tac l2, simp_all)
```
```   118   apply (simp add: fun_eq_iff)
```
```   119   apply (intro allI)
```
```   120   apply (induct_tac xa xb rule: list_induct2')
```
```   121   apply simp_all
```
```   122   done
```
```   123
```
```   124 lemma ALL2:
```
```   125  "list_all2 P [] [] = True \<and>
```
```   126   list_all2 P (h1 # t1) [] = False \<and>
```
```   127   list_all2 P [] (h2 # t2) = False \<and>
```
```   128   list_all2 P (h1 # t1) (h2 # t2) = (P h1 h2 \<and> list_all2 P t1 t2)"
```
```   129   by simp
```
```   130
```
```   131 lemma DEF_FILTER:
```
```   132   "filter = (SOME FILTER. (\<forall>P. FILTER P [] = []) \<and>
```
```   133      (\<forall>h P t. FILTER P (h # t) = (if P h then h # FILTER P t else FILTER P t)))"
```
```   134   apply (rule some_equality[symmetric])
```
```   135   apply (auto simp add: fun_eq_iff)
```
```   136   apply (induct_tac xa)
```
```   137   apply simp_all
```
```   138   done
```
```   139
```
```   140 fun map2 where
```
```   141   "map2 f [] [] = []"
```
```   142 | "map2 f (h1 # t1) (h2 # t2) = (f h1 h2) # (map2 f t1 t2)"
```
```   143
```
```   144 lemma MAP2:
```
```   145   "map2 f [] [] = [] \<and> map2 f (h1 # t1) (h2 # t2) = f h1 h2 # map2 f t1 t2"
```
```   146   by simp
```
```   147
```
```   148 fun fold2 where
```
```   149   "fold2 f [] [] b = b"
```
```   150 | "fold2 f (h1 # t1) (h2 # t2) b = f h1 h2 (fold2 f t1 t2 b)"
```
```   151
```
```   152 lemma ITLIST2:
```
```   153   "fold2 f [] [] b = b \<and> fold2 f (h1 # t1) (h2 # t2) b = f h1 h2 (fold2 f t1 t2 b)"
```
```   154   by simp
```
```   155
```
```   156 definition [simp]: "list_el x xs = nth xs x"
```
```   157
```
```   158 lemma ZIP:
```
```   159   "zip [] [] = [] \<and> zip (h1 # t1) (h2 # t2) = (h1, h2) # (zip t1 t2)"
```
```   160   by simp
```
```   161
```
```   162 lemma LAST_CLAUSES:
```
```   163   "last [h] = h \<and> last (h # k # t) = last (k # t)"
```
```   164   by simp
```
```   165
```
```   166 lemma DEF_NULL:
```
```   167   "List.null = (SOME NULL. NULL [] = True \<and> (\<forall>h t. NULL (h # t) = False))"
```
```   168   apply (rule some_equality[symmetric])
```
```   169   apply (auto simp add: fun_eq_iff null_def)
```
```   170   apply (case_tac x)
```
```   171   apply simp_all
```
```   172   done
```
```   173
```
```   174 lemma DEF_ALL:
```
```   175   "list_all = (SOME u. (\<forall>P. u P [] = True) \<and> (\<forall>h P t. u P (h # t) = (P h \<and> u P t)))"
```
```   176   apply (rule some_equality[symmetric])
```
```   177   apply auto[1]
```
```   178   apply (simp add: fun_eq_iff)
```
```   179   apply (intro allI)
```
```   180   apply (induct_tac xa)
```
```   181   apply simp_all
```
```   182   done
```
```   183
```
```   184 lemma MAP_EQ:
```
```   185   "list_all (\<lambda>x. f x = g x) l \<longrightarrow> map f l = map g l"
```
```   186   by (induct l) auto
```
```   187
```
```   188 definition [simp]: "list_mem x xs = List.member xs x"
```
```   189
```
```   190 lemma DEF_MEM:
```
```   191   "list_mem = (SOME MEM. (\<forall>x. MEM x [] = False) \<and> (\<forall>h x t. MEM x (h # t) = (x = h \<or> MEM x t)))"
```
```   192   apply (rule some_equality[symmetric])
```
```   193   apply (auto simp add: member_def)[1]
```
```   194   apply (simp add: fun_eq_iff)
```
```   195   apply (intro allI)
```
```   196   apply (induct_tac xa)
```
```   197   apply (simp_all add: member_def)
```
```   198   done
```
```   199
```
```   200 lemma DEF_EX:
```
```   201   "list_ex = (SOME u. (\<forall>P. u P [] = False) \<and> (\<forall>h P t. u P (h # t) = (P h \<or> u P t)))"
```
```   202   apply (rule some_equality[symmetric])
```
```   203   apply (auto)
```
```   204   apply (simp add: fun_eq_iff)
```
```   205   apply (intro allI)
```
```   206   apply (induct_tac xa)
```
```   207   apply (simp_all)
```
```   208   done
```
```   209
```
```   210 lemma ALL_IMP:
```
```   211   "(\<forall>x. x \<in> set l \<and> P x \<longrightarrow> Q x) \<and> list_all P l \<longrightarrow> list_all Q l"
```
```   212   by (simp add: list_all_iff)
```
```   213
```
```   214 lemma NOT_EX: "(\<not> list_ex P l) = list_all (\<lambda>x. \<not> P x) l"
```
```   215   by (simp add: list_all_iff list_ex_iff)
```
```   216
```
```   217 lemma NOT_ALL: "(\<not> list_all P l) = list_ex (\<lambda>x. \<not> P x) l"
```
```   218   by (simp add: list_all_iff list_ex_iff)
```
```   219
```
```   220 lemma ALL_MAP: "list_all P (map f l) = list_all (P o f) l"
```
```   221   by (simp add: list_all_iff)
```
```   222
```
```   223 lemma ALL_T: "list_all (\<lambda>x. True) l"
```
```   224   by (simp add: list_all_iff)
```
```   225
```
```   226 lemma MAP_EQ_ALL2: "list_all2 (\<lambda>x y. f x = f y) l m \<longrightarrow> map f l = map f m"
```
```   227   by (induct l m rule: list_induct2') simp_all
```
```   228
```
```   229 lemma ALL2_MAP: "list_all2 P (map f l) l = list_all (\<lambda>a. P (f a) a) l"
```
```   230   by (induct l) simp_all
```
```   231
```
```   232 lemma MAP_EQ_DEGEN: "list_all (\<lambda>x. f x = x) l --> map f l = l"
```
```   233   by (induct l) simp_all
```
```   234
```
```   235 lemma ALL2_AND_RIGHT:
```
```   236    "list_all2 (\<lambda>x y. P x \<and> Q x y) l m = (list_all P l \<and> list_all2 Q l m)"
```
```   237   by (induct l m rule: list_induct2') auto
```
```   238
```
```   239 lemma ITLIST_EXTRA:
```
```   240   "foldr f (l @ [a]) b = foldr f l (f a b)"
```
```   241   by simp
```
```   242
```
```   243 lemma ALL_MP:
```
```   244   "list_all (\<lambda>x. P x \<longrightarrow> Q x) l \<and> list_all P l \<longrightarrow> list_all Q l"
```
```   245   by (simp add: list_all_iff)
```
```   246
```
```   247 lemma AND_ALL:
```
```   248   "(list_all P l \<and> list_all Q l) = list_all (\<lambda>x. P x \<and> Q x) l"
```
```   249   by (auto simp add: list_all_iff)
```
```   250
```
```   251 lemma EX_IMP:
```
```   252   "(\<forall>x. x\<in>set l \<and> P x \<longrightarrow> Q x) \<and> list_ex P l \<longrightarrow> list_ex Q l"
```
```   253   by (auto simp add: list_ex_iff)
```
```   254
```
```   255 lemma ALL_MEM:
```
```   256   "(\<forall>x. x\<in>set l \<longrightarrow> P x) = list_all P l"
```
```   257   by (auto simp add: list_all_iff)
```
```   258
```
```   259 lemma EX_MAP:
```
```   260   "ALL P f l. list_ex P (map f l) = list_ex (P o f) l"
```
```   261   by (simp add: list_ex_iff)
```
```   262
```
```   263 lemma EXISTS_EX:
```
```   264   "\<forall>P l. (EX x. list_ex (P x) l) = list_ex (\<lambda>s. EX x. P x s) l"
```
```   265   by (auto simp add: list_ex_iff)
```
```   266
```
```   267 lemma FORALL_ALL:
```
```   268   "\<forall>P l. (\<forall>x. list_all (P x) l) = list_all (\<lambda>s. \<forall>x. P x s) l"
```
```   269   by (auto simp add: list_all_iff)
```
```   270
```
```   271 lemma MEM_APPEND: "\<forall>x l1 l2. (x\<in>set (l1 @ l2)) = (x\<in>set l1 \<or> x\<in>set l2)"
```
```   272   by simp
```
```   273
```
```   274 lemma MEM_MAP: "\<forall>f y l. (y\<in>set (map f l)) = (EX x. x\<in>set l \<and> y = f x)"
```
```   275   by auto
```
```   276
```
```   277 lemma MEM_FILTER: "\<forall>P l x. (x\<in>set (filter P l)) = (P x \<and> x\<in>set l)"
```
```   278   by auto
```
```   279
```
```   280 lemma EX_MEM: "(EX x. P x \<and> x\<in>set l) = list_ex P l"
```
```   281   by (auto simp add: list_ex_iff)
```
```   282
```
```   283 lemma ALL2_MAP2:
```
```   284   "list_all2 P (map f l) (map g m) = list_all2 (\<lambda>x y. P (f x) (g y)) l m"
```
```   285   by (simp add: list_all2_map1 list_all2_map2)
```
```   286
```
```   287 lemma ALL2_ALL:
```
```   288   "list_all2 P l l = list_all (\<lambda>x. P x x) l"
```
```   289   by (induct l) simp_all
```
```   290
```
```   291 lemma LENGTH_MAP2:
```
```   292   "length l = length m \<longrightarrow> length (map2 f l m) = length m"
```
```   293   by (induct l m rule: list_induct2') simp_all
```
```   294
```
```   295 lemma DEF_set_of_list:
```
```   296   "set = (SOME sol. sol [] = {} \<and> (\<forall>h t. sol (h # t) = insert h (sol t)))"
```
```   297   apply (rule some_equality[symmetric])
```
```   298   apply (simp_all)
```
```   299   apply (rule ext)
```
```   300   apply (induct_tac x)
```
```   301   apply simp_all
```
```   302   done
```
```   303
```
```   304 lemma IN_SET_OF_LIST:
```
```   305   "(x : set l) = (x : set l)"
```
```   306   by simp
```
```   307
```
```   308 lemma DEF_BUTLAST:
```
```   309   "butlast = (SOME B. B [] = [] \<and> (\<forall>h t. B (h # t) = (if t = [] then [] else h # B t)))"
```
```   310   apply (rule some_equality[symmetric])
```
```   311   apply auto
```
```   312   apply (rule ext)
```
```   313   apply (induct_tac x)
```
```   314   apply auto
```
```   315   done
```
```   316
```
```   317 lemma MONO_ALL:
```
```   318   "(ALL x. P x \<longrightarrow> Q x) \<longrightarrow> list_all P l \<longrightarrow> list_all Q l"
```
```   319   by (simp add: list_all_iff)
```
```   320
```
```   321 lemma EL_TL: "l \<noteq> [] \<Longrightarrow> tl l ! x = l ! (x + 1)"
```
```   322   by (induct l) (simp_all)
```
```   323
```
```   324 (* Assume the same behaviour outside of the usual domain.
```
```   325    For HD, LAST, EL it follows from "undefined = SOME _. False".
```
```   326
```
```   327    The definitions of TL and ZIP are different for empty lists.
```
```   328  *)
```
```   329 axiomatization where
```
```   330   DEF_HD: "hd = (SOME HD. \<forall>t h. HD (h # t) = h)"
```
```   331
```
```   332 axiomatization where
```
```   333   DEF_LAST: "last =
```
```   334     (SOME LAST. \<forall>h t. LAST (h # t) = (if t = [] then h else LAST t))"
```
```   335
```
```   336 axiomatization where
```
```   337   DEF_EL: "list_el =
```
```   338     (SOME EL. (\<forall>l. EL 0 l = hd l) \<and> (\<forall>n l. EL (Suc n) l = EL n (tl l)))"
```
```   339
```
```   340 end
```