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