src/HOL/Import/HOLLightCompat.thy
author haftmann
Sat Mar 03 21:00:31 2012 +0100 (2012-03-03)
changeset 46782 d50855d9ea74
parent 44633 8a2fd7418435
permissions -rw-r--r--
spurious set/pred correction
obua@17322
     1
(*  Title:      HOL/Import/HOLLightCompat.thy
wenzelm@41589
     2
    Author:     Steven Obua and Sebastian Skalberg, TU Muenchen
kaliszyk@43787
     3
    Author:     Cezary Kaliszyk
obua@17322
     4
*)
obua@17322
     5
kaliszyk@43787
     6
theory HOLLightCompat
kaliszyk@43787
     7
imports Main Fact Parity "~~/src/HOL/Library/Infinite_Set"
kaliszyk@43787
     8
  HOLLightList HOLLightReal HOLLightInt HOL4Setup
kaliszyk@43787
     9
begin
kaliszyk@43787
    10
kaliszyk@43787
    11
(* list *)
kaliszyk@43787
    12
lemmas [hol4rew] = list_el_def member_def list_mem_def
kaliszyk@43787
    13
(* int *)
kaliszyk@43787
    14
lemmas [hol4rew] = int_coprime.simps int_gcd.simps hl_mod_def hl_div_def int_mod_def eqeq_def
kaliszyk@43787
    15
(* real *)
kaliszyk@43787
    16
lemma [hol4rew]:
kaliszyk@43787
    17
  "real (0::nat) = 0" "real (1::nat) = 1" "real (2::nat) = 2"
kaliszyk@43787
    18
  by simp_all
kaliszyk@43787
    19
kaliszyk@43787
    20
lemma one:
kaliszyk@43787
    21
  "\<forall>v. v = ()"
kaliszyk@43787
    22
  by simp
obua@17322
    23
kaliszyk@43787
    24
lemma num_Axiom:
kaliszyk@44633
    25
  "\<exists>!fn. fn 0 = e \<and> (\<forall>n. fn (Suc n) = f (fn n) n)"
kaliszyk@44633
    26
  apply (rule ex1I[of _ "nat_rec e (%n e. f e n)"])
kaliszyk@44633
    27
  apply (auto simp add: fun_eq_iff)
kaliszyk@44633
    28
  apply (induct_tac x)
kaliszyk@43787
    29
  apply simp_all
kaliszyk@43787
    30
  done
obua@17322
    31
kaliszyk@43787
    32
lemma SUC_INJ:
kaliszyk@43787
    33
  "\<forall>m n. Suc m = Suc n \<longleftrightarrow> m = n"
kaliszyk@44633
    34
  by simp
kaliszyk@43787
    35
kaliszyk@43787
    36
lemma PAIR:
kaliszyk@43787
    37
  "(fst x, snd x) = x"
obua@17322
    38
  by simp
obua@17322
    39
kaliszyk@43787
    40
lemma EXISTS_UNIQUE_THM:
kaliszyk@43787
    41
  "(Ex1 P) = (Ex P & (\<forall>x y. P x & P y --> (x = y)))"
kaliszyk@43787
    42
  by auto
kaliszyk@43787
    43
kaliszyk@43787
    44
lemma DEF__star_:
kaliszyk@43787
    45
  "op * = (SOME mult. (\<forall>n. mult 0 n = 0) \<and> (\<forall>m n. mult (Suc m) n = mult m n + n))"
kaliszyk@43787
    46
  apply (rule some_equality[symmetric])
kaliszyk@44633
    47
  apply (auto simp add: fun_eq_iff)
kaliszyk@43787
    48
  apply (induct_tac x)
kaliszyk@43787
    49
  apply auto
kaliszyk@43787
    50
  done
kaliszyk@43787
    51
kaliszyk@43787
    52
lemma DEF__slash__backslash_:
kaliszyk@43787
    53
  "(t1 \<and> t2) = ((\<lambda>f. f t1 t2 :: bool) = (\<lambda>f. f True True))"
kaliszyk@43787
    54
  unfolding fun_eq_iff
kaliszyk@43787
    55
  by (intro iffI, simp_all) (erule allE[of _ "(%a b. a \<and> b)"], simp)
kaliszyk@43787
    56
kaliszyk@43787
    57
lemma DEF__lessthan__equal_:
kaliszyk@43787
    58
  "op \<le> = (SOME u. (\<forall>m. u m 0 = (m = 0)) \<and> (\<forall>m n. u m (Suc n) = (m = Suc n \<or> u m n)))"
kaliszyk@43787
    59
  apply (rule some_equality[symmetric])
kaliszyk@43787
    60
  apply auto[1]
kaliszyk@43787
    61
  apply (simp add: fun_eq_iff)
kaliszyk@43787
    62
  apply (intro allI)
kaliszyk@43787
    63
  apply (induct_tac xa)
kaliszyk@43787
    64
  apply auto
kaliszyk@43787
    65
  done
kaliszyk@43787
    66
kaliszyk@43787
    67
lemma DEF__lessthan_:
kaliszyk@43787
    68
  "op < = (SOME u. (\<forall>m. u m 0 = False) \<and> (\<forall>m n. u m (Suc n) = (m = n \<or> u m n)))"
kaliszyk@43787
    69
  apply (rule some_equality[symmetric])
kaliszyk@43787
    70
  apply auto[1]
kaliszyk@43787
    71
  apply (simp add: fun_eq_iff)
kaliszyk@43787
    72
  apply (intro allI)
kaliszyk@43787
    73
  apply (induct_tac xa)
kaliszyk@43787
    74
  apply auto
kaliszyk@43787
    75
  done
kaliszyk@43787
    76
kaliszyk@43787
    77
lemma DEF__greaterthan__equal_:
kaliszyk@43787
    78
  "(op \<ge>) = (%u ua. ua \<le> u)"
kaliszyk@43787
    79
  by (simp)
kaliszyk@43787
    80
kaliszyk@43787
    81
lemma DEF__greaterthan_:
kaliszyk@43787
    82
  "(op >) = (%u ua. ua < u)"
kaliszyk@43787
    83
  by (simp)
obua@17322
    84
kaliszyk@43787
    85
lemma DEF__equal__equal__greaterthan_:
kaliszyk@43787
    86
  "(t1 \<longrightarrow> t2) = ((t1 \<and> t2) = t1)"
kaliszyk@43787
    87
  by auto
kaliszyk@43787
    88
kaliszyk@43787
    89
lemma DEF_WF:
kaliszyk@43787
    90
  "wfP = (\<lambda>u. \<forall>P. (\<exists>x. P x) \<longrightarrow> (\<exists>x. P x \<and> (\<forall>y. u y x \<longrightarrow> \<not> P y)))"
kaliszyk@43787
    91
  unfolding fun_eq_iff
kaliszyk@44633
    92
proof (intro allI iffI impI wfI_min[to_pred], elim exE wfE_min[to_pred])
kaliszyk@44633
    93
  fix P :: "'a \<Rightarrow> bool" and xa :: "'a"
kaliszyk@44633
    94
  assume "P xa"
kaliszyk@44633
    95
  then show "xa \<in> Collect P" by simp
kaliszyk@44633
    96
next
kaliszyk@44633
    97
  fix x P xa z
kaliszyk@44633
    98
  assume "P xa" "z \<in> {a. P a}" "\<And>y. x y z \<Longrightarrow> y \<notin> {a. P a}"
kaliszyk@44633
    99
  then show "\<exists>xa. P xa \<and> (\<forall>y. x y xa \<longrightarrow> \<not> P y)" by auto
kaliszyk@44633
   100
next
kaliszyk@44633
   101
  fix x :: "'a \<Rightarrow> 'a \<Rightarrow> bool" and xa :: "'a" and Q
kaliszyk@44633
   102
  assume a: "xa \<in> Q"
kaliszyk@44633
   103
  assume b: "\<forall>P. Ex P \<longrightarrow> (\<exists>xa. P xa \<and> (\<forall>y. x y xa \<longrightarrow> \<not> P y))"
kaliszyk@44633
   104
  then have "Ex (\<lambda>x. x \<in> Q) \<longrightarrow> (\<exists>xa. (\<lambda>x. x \<in> Q) xa \<and> (\<forall>y. x y xa \<longrightarrow> \<not> (\<lambda>x. x \<in> Q) y))" by auto
kaliszyk@44633
   105
  then show "\<exists>z\<in>Q. \<forall>y. x y z \<longrightarrow> y \<notin> Q" using a by auto
kaliszyk@44633
   106
qed
kaliszyk@43787
   107
kaliszyk@44633
   108
lemma DEF_UNIV: "top = (%x. True)"
kaliszyk@44633
   109
  by (rule ext) (simp add: top1I)
obua@17322
   110
kaliszyk@43787
   111
lemma DEF_UNIONS:
kaliszyk@43787
   112
  "Sup = (\<lambda>u. {ua. \<exists>x. (\<exists>ua. ua \<in> u \<and> x \<in> ua) \<and> ua = x})"
kaliszyk@44633
   113
  by (auto simp add: Union_eq)
kaliszyk@43787
   114
kaliszyk@43787
   115
lemma DEF_UNION:
kaliszyk@43787
   116
  "op \<union> = (\<lambda>u ua. {ub. \<exists>x. (x \<in> u \<or> x \<in> ua) \<and> ub = x})"
kaliszyk@44633
   117
  by auto
kaliszyk@43787
   118
kaliszyk@43787
   119
lemma DEF_SUBSET: "op \<subseteq> = (\<lambda>u ua. \<forall>x. x \<in> u \<longrightarrow> x \<in> ua)"
kaliszyk@43787
   120
  by (metis set_rev_mp subsetI)
kaliszyk@43787
   121
kaliszyk@43787
   122
lemma DEF_SND:
kaliszyk@43787
   123
  "snd = (\<lambda>p. SOME x. EX y. p = (y, x))"
kaliszyk@43787
   124
  unfolding fun_eq_iff
kaliszyk@43787
   125
  by (rule someI2) (auto intro: snd_conv[symmetric] someI2)
kaliszyk@43787
   126
kaliszyk@43787
   127
definition [simp, hol4rew]: "SETSPEC x P y \<longleftrightarrow> P & x = y"
kaliszyk@43787
   128
kaliszyk@43787
   129
lemma DEF_PSUBSET: "op \<subset> = (\<lambda>u ua. u \<subseteq> ua & u \<noteq> ua)"
kaliszyk@44633
   130
  by (metis psubset_eq)
kaliszyk@43787
   131
kaliszyk@43787
   132
definition [hol4rew]: "Pred n = n - (Suc 0)"
kaliszyk@43787
   133
kaliszyk@43787
   134
lemma DEF_PRE: "Pred = (SOME PRE. PRE 0 = 0 & (\<forall>n. PRE (Suc n) = n))"
obua@17322
   135
  apply (rule some_equality[symmetric])
obua@17322
   136
  apply (simp add: Pred_def)
obua@17322
   137
  apply (rule ext)
obua@17322
   138
  apply (induct_tac x)
obua@17322
   139
  apply (auto simp add: Pred_def)
obua@17322
   140
  done
obua@17322
   141
kaliszyk@43787
   142
lemma DEF_ONE_ONE:
kaliszyk@43787
   143
  "inj = (\<lambda>u. \<forall>x1 x2. u x1 = u x2 \<longrightarrow> x1 = x2)"
kaliszyk@43787
   144
  by (simp add: inj_on_def)
kaliszyk@43787
   145
kaliszyk@43787
   146
definition ODD'[hol4rew]: "(ODD :: nat \<Rightarrow> bool) = odd"
obua@17322
   147
kaliszyk@43787
   148
lemma DEF_ODD:
kaliszyk@43787
   149
  "odd = (SOME ODD. ODD 0 = False \<and> (\<forall>n. ODD (Suc n) = (\<not> ODD n)))"
kaliszyk@43787
   150
  apply (rule some_equality[symmetric])
kaliszyk@43787
   151
  apply simp
kaliszyk@43787
   152
  unfolding fun_eq_iff
kaliszyk@43787
   153
  apply (intro allI)
kaliszyk@43787
   154
  apply (induct_tac x)
kaliszyk@43787
   155
  apply simp_all
obua@17322
   156
  done
obua@17322
   157
kaliszyk@43787
   158
definition [hol4rew, simp]: "NUMERAL (x :: nat) = x"
kaliszyk@43787
   159
kaliszyk@43787
   160
lemma DEF_MOD:
kaliszyk@43787
   161
  "op mod = (SOME r. \<forall>m n. if n = (0 :: nat) then m div n = 0 \<and>
kaliszyk@43787
   162
     r m n = m else m = m div n * n + r m n \<and> r m n < n)"
kaliszyk@43787
   163
  apply (rule some_equality[symmetric])
kaliszyk@43787
   164
  apply (auto simp add: fun_eq_iff)
kaliszyk@43787
   165
  apply (case_tac "xa = 0")
kaliszyk@43787
   166
  apply auto
kaliszyk@43787
   167
  apply (drule_tac x="x" in spec)
kaliszyk@43787
   168
  apply (drule_tac x="xa" in spec)
kaliszyk@43787
   169
  apply auto
kaliszyk@43787
   170
  by (metis mod_less mod_mult_self2 nat_add_commute nat_mult_commute)
kaliszyk@43787
   171
kaliszyk@43787
   172
definition "MEASURE = (%u x y. (u x :: nat) < u y)"
kaliszyk@43787
   173
kaliszyk@43787
   174
lemma [hol4rew]:
kaliszyk@44633
   175
  "MEASURE u = (%a b. (a, b) \<in> measure u)"
kaliszyk@44633
   176
  unfolding MEASURE_def measure_def
kaliszyk@43787
   177
  by simp
kaliszyk@43787
   178
kaliszyk@43787
   179
definition
kaliszyk@43787
   180
  "LET f s = f s"
kaliszyk@43787
   181
kaliszyk@43787
   182
lemma [hol4rew]:
kaliszyk@43787
   183
  "LET f s = Let s f"
kaliszyk@43787
   184
  by (simp add: LET_def Let_def)
kaliszyk@43787
   185
kaliszyk@43787
   186
lemma DEF_INTERS:
kaliszyk@43787
   187
  "Inter = (\<lambda>u. {ua. \<exists>x. (\<forall>ua. ua \<in> u \<longrightarrow> x \<in> ua) \<and> ua = x})"
kaliszyk@44633
   188
  by auto
kaliszyk@43787
   189
kaliszyk@43787
   190
lemma DEF_INTER:
kaliszyk@43787
   191
  "op \<inter> = (\<lambda>u ua. {ub. \<exists>x. (x \<in> u \<and> x \<in> ua) \<and> ub = x})"
kaliszyk@44633
   192
  by auto
kaliszyk@43787
   193
kaliszyk@43787
   194
lemma DEF_INSERT:
haftmann@46782
   195
  "insert = (\<lambda>u ua. {y. y \<in> ua | y = u})"
haftmann@46782
   196
  by auto
kaliszyk@43787
   197
kaliszyk@43787
   198
lemma DEF_IMAGE:
kaliszyk@43787
   199
  "op ` = (\<lambda>u ua. {ub. \<exists>y. (\<exists>x. x \<in> ua \<and> y = u x) \<and> ub = y})"
kaliszyk@43787
   200
  by (simp add: fun_eq_iff image_def Bex_def)
kaliszyk@43787
   201
kaliszyk@43787
   202
lemma DEF_GEQ:
kaliszyk@43787
   203
  "(op =) = (op =)"
kaliszyk@43787
   204
  by simp
kaliszyk@43787
   205
kaliszyk@43787
   206
lemma DEF_GABS:
kaliszyk@43787
   207
  "Eps = Eps"
kaliszyk@43787
   208
  by simp
kaliszyk@43787
   209
kaliszyk@43787
   210
lemma DEF_FST:
kaliszyk@43787
   211
  "fst = (%p. SOME x. EX y. p = (x, y))"
kaliszyk@43787
   212
  unfolding fun_eq_iff
kaliszyk@43787
   213
  by (rule someI2) (auto intro: fst_conv[symmetric] someI2)
kaliszyk@43787
   214
kaliszyk@43787
   215
lemma DEF_FINITE:
kaliszyk@43787
   216
  "finite = (\<lambda>a. \<forall>FP. (\<forall>a. a = {} \<or> (\<exists>x s. a = insert x s \<and> FP s) \<longrightarrow> FP a) \<longrightarrow> FP a)"
kaliszyk@43787
   217
  unfolding fun_eq_iff
kaliszyk@43787
   218
  apply (intro allI iffI impI)
kaliszyk@43787
   219
  apply (erule finite_induct)
kaliszyk@43787
   220
  apply auto[2]
kaliszyk@43787
   221
  apply (drule_tac x="finite" in spec)
kaliszyk@44633
   222
  by (metis finite_insert infinite_imp_nonempty infinite_super predicate1I)
kaliszyk@43787
   223
kaliszyk@43787
   224
lemma DEF_FACT:
kaliszyk@43787
   225
  "fact = (SOME FACT. FACT 0 = 1 & (\<forall>n. FACT (Suc n) = Suc n * FACT n))"
kaliszyk@43787
   226
  apply (rule some_equality[symmetric])
kaliszyk@43787
   227
  apply (simp_all)
kaliszyk@43787
   228
  unfolding fun_eq_iff
kaliszyk@43787
   229
  apply (intro allI)
kaliszyk@43787
   230
  apply (induct_tac x)
kaliszyk@43787
   231
  apply simp_all
obua@17322
   232
  done
obua@17322
   233
kaliszyk@43787
   234
lemma DEF_EXP:
kaliszyk@43787
   235
  "power = (SOME EXP. (\<forall>m. EXP m 0 = 1) \<and> (\<forall>m n. EXP m (Suc n) = m * EXP m n))"
kaliszyk@43787
   236
  apply (rule some_equality[symmetric])
kaliszyk@43787
   237
  apply (simp_all)
kaliszyk@43787
   238
  unfolding fun_eq_iff
kaliszyk@43787
   239
  apply (intro allI)
kaliszyk@43787
   240
  apply (induct_tac xa)
kaliszyk@43787
   241
  apply simp_all
kaliszyk@43787
   242
  done
kaliszyk@43787
   243
kaliszyk@43787
   244
lemma DEF_EVEN:
kaliszyk@43787
   245
  "even = (SOME EVEN. EVEN 0 = True \<and> (\<forall>n. EVEN (Suc n) = (\<not> EVEN n)))"
kaliszyk@43787
   246
  apply (rule some_equality[symmetric])
kaliszyk@43787
   247
  apply simp
kaliszyk@43787
   248
  unfolding fun_eq_iff
kaliszyk@43787
   249
  apply (intro allI)
kaliszyk@43787
   250
  apply (induct_tac x)
kaliszyk@43787
   251
  apply simp_all
obua@17322
   252
  done
obua@17322
   253
kaliszyk@44633
   254
lemma DEF_EMPTY: "bot = (%x. False)"
kaliszyk@44633
   255
  by (rule ext) auto
kaliszyk@44633
   256
  
kaliszyk@43787
   257
lemma DEF_DIV:
kaliszyk@43787
   258
  "op div = (SOME q. \<exists>r. \<forall>m n. if n = (0 :: nat) then q m n = 0 \<and> r m n = m
kaliszyk@43787
   259
     else m = q m n * n + r m n \<and> r m n < n)"
kaliszyk@43787
   260
  apply (rule some_equality[symmetric])
kaliszyk@43787
   261
  apply (rule_tac x="op mod" in exI)
kaliszyk@43787
   262
  apply (auto simp add: fun_eq_iff)
kaliszyk@43787
   263
  apply (case_tac "xa = 0")
kaliszyk@43787
   264
  apply auto
kaliszyk@43787
   265
  apply (drule_tac x="x" in spec)
kaliszyk@43787
   266
  apply (drule_tac x="xa" in spec)
kaliszyk@43787
   267
  apply auto
kaliszyk@43787
   268
  by (metis div_mult_self2 gr_implies_not0 mod_div_trivial mod_less
kaliszyk@43787
   269
      nat_add_commute nat_mult_commute plus_nat.add_0)
kaliszyk@43787
   270
kaliszyk@43787
   271
definition [hol4rew]: "DISJOINT a b \<longleftrightarrow> a \<inter> b = {}"
kaliszyk@43787
   272
kaliszyk@43787
   273
lemma DEF_DISJOINT:
kaliszyk@43787
   274
  "DISJOINT = (%u ua. u \<inter> ua = {})"
kaliszyk@43787
   275
  by (auto simp add: DISJOINT_def_raw)
kaliszyk@43787
   276
kaliszyk@43787
   277
lemma DEF_DIFF:
kaliszyk@43787
   278
  "op - = (\<lambda>u ua. {ub. \<exists>x. (x \<in> u \<and> x \<notin> ua) \<and> ub = x})"
kaliszyk@44633
   279
  by (metis set_diff_eq)
kaliszyk@43787
   280
kaliszyk@43787
   281
definition [hol4rew]: "DELETE s e = s - {e}"
kaliszyk@43787
   282
kaliszyk@43787
   283
lemma DEF_DELETE:
kaliszyk@43787
   284
  "DELETE = (\<lambda>u ua. {ub. \<exists>y. (y \<in> u \<and> y \<noteq> ua) \<and> ub = y})"
kaliszyk@43787
   285
  by (auto simp add: DELETE_def_raw)
kaliszyk@43787
   286
kaliszyk@43787
   287
lemma COND_DEF:
kaliszyk@43787
   288
  "(if b then t else f) = (SOME x. (b = True \<longrightarrow> x = t) \<and> (b = False \<longrightarrow> x = f))"
kaliszyk@43787
   289
  by auto
kaliszyk@43787
   290
kaliszyk@43787
   291
definition [simp]: "NUMERAL_BIT1 n = n + (n + Suc 0)"
kaliszyk@43787
   292
kaliszyk@43787
   293
lemma BIT1_DEF:
kaliszyk@43787
   294
  "NUMERAL_BIT1 = (%u. Suc (2 * u))"
kaliszyk@43787
   295
  by (auto)
kaliszyk@43787
   296
kaliszyk@43787
   297
definition [simp]: "NUMERAL_BIT0 (n :: nat) = n + n"
kaliszyk@43787
   298
kaliszyk@43787
   299
lemma BIT0_DEF:
kaliszyk@43787
   300
  "NUMERAL_BIT0 = (SOME BIT0. BIT0 0 = 0 \<and> (\<forall>n. BIT0 (Suc n) = Suc (Suc (BIT0 n))))"
kaliszyk@43787
   301
  apply (rule some_equality[symmetric])
kaliszyk@43787
   302
  apply auto
kaliszyk@43787
   303
  apply (rule ext)
kaliszyk@43787
   304
  apply (induct_tac x)
kaliszyk@43787
   305
  apply auto
kaliszyk@43787
   306
  done
kaliszyk@43787
   307
kaliszyk@43787
   308
lemma [hol4rew]:
kaliszyk@43787
   309
  "NUMERAL_BIT0 n = 2 * n"
kaliszyk@43787
   310
  "NUMERAL_BIT1 n = 2 * n + 1"
kaliszyk@43787
   311
  "2 * 0 = (0 :: nat)"
kaliszyk@43787
   312
  "2 * 1 = (2 :: nat)"
kaliszyk@43787
   313
  "0 + 1 = (1 :: nat)"
kaliszyk@43787
   314
  by simp_all
kaliszyk@43787
   315
kaliszyk@43787
   316
lemma DEF_MINUS: "op - = (SOME sub. (\<forall>m. sub m 0 = m) & (\<forall>m n. sub m (Suc n) = sub m n - Suc 0))"
kaliszyk@43787
   317
  apply (rule some_equality[symmetric])
kaliszyk@43787
   318
  apply auto
kaliszyk@43787
   319
  apply (rule ext)+
kaliszyk@43787
   320
  apply (induct_tac xa)
kaliszyk@43787
   321
  apply auto
kaliszyk@43787
   322
  done
kaliszyk@43787
   323
kaliszyk@43787
   324
lemma DEF_PLUS: "op + = (SOME add. (\<forall>n. add 0 n = n) & (\<forall>m n. add (Suc m) n = Suc (add m n)))"
obua@17322
   325
  apply (rule some_equality[symmetric])
obua@17322
   326
  apply auto
obua@17322
   327
  apply (rule ext)+
obua@17322
   328
  apply (induct_tac x)
obua@17322
   329
  apply auto
obua@17322
   330
  done
obua@17322
   331
kaliszyk@43787
   332
lemmas [hol4rew] = id_apply
obua@17322
   333
haftmann@46782
   334
lemma DEF_CHOICE: "Eps = (%u. SOME x. u x)"
haftmann@46782
   335
  by simp
kaliszyk@43787
   336
kaliszyk@44633
   337
definition dotdot :: "nat => nat => nat set"
kaliszyk@44633
   338
  where "dotdot u ua = {ub. EX x. (u <= x & x <= ua) & ub = x}"
obua@17322
   339
kaliszyk@43787
   340
lemma [hol4rew]: "dotdot a b = {a..b}"
kaliszyk@43787
   341
  unfolding fun_eq_iff atLeastAtMost_def atLeast_def atMost_def dotdot_def
kaliszyk@43787
   342
  by (simp add: Collect_conj_eq)
kaliszyk@43787
   343
kaliszyk@43787
   344
definition [hol4rew,simp]: "INFINITE S \<longleftrightarrow> \<not> finite S"
kaliszyk@43787
   345
kaliszyk@43787
   346
lemma DEF_INFINITE: "INFINITE = (\<lambda>u. \<not>finite u)"
kaliszyk@43787
   347
  by (simp add: INFINITE_def_raw)
obua@17322
   348
obua@17322
   349
end
haftmann@46782
   350