src/HOL/Import/HOLLightCompat.thy
author Cezary Kaliszyk <kaliszyk@in.tum.de>
Wed Jul 13 00:43:07 2011 +0900 (2011-07-13)
changeset 43787 5be84619e4d4
parent 41589 bbd861837ebc
child 44633 8a2fd7418435
permissions -rw-r--r--
Update HOLLightCompat
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@43787
    25
  "\<forall>e f. \<exists>!fn. fn 0 = e \<and> (\<forall>n. fn (Suc n) = f (fn n) n)"
kaliszyk@43787
    26
  apply (intro allI)
kaliszyk@43787
    27
  apply (rule_tac a="nat_rec e (%n e. f e n)" in ex1I)
kaliszyk@43787
    28
  apply auto
kaliszyk@43787
    29
  apply (simp add: fun_eq_iff)
kaliszyk@43787
    30
  apply (intro allI)
kaliszyk@43787
    31
  apply (induct_tac xa)
kaliszyk@43787
    32
  apply simp_all
kaliszyk@43787
    33
  done
obua@17322
    34
kaliszyk@43787
    35
lemma SUC_INJ:
kaliszyk@43787
    36
  "\<forall>m n. Suc m = Suc n \<longleftrightarrow> m = n"
kaliszyk@43787
    37
  by auto
kaliszyk@43787
    38
kaliszyk@43787
    39
lemma PAIR:
kaliszyk@43787
    40
  "(fst x, snd x) = x"
obua@17322
    41
  by simp
obua@17322
    42
kaliszyk@43787
    43
lemma EXISTS_UNIQUE_THM:
kaliszyk@43787
    44
  "(Ex1 P) = (Ex P & (\<forall>x y. P x & P y --> (x = y)))"
kaliszyk@43787
    45
  by auto
kaliszyk@43787
    46
kaliszyk@43787
    47
lemma DEF__star_:
kaliszyk@43787
    48
  "op * = (SOME mult. (\<forall>n. mult 0 n = 0) \<and> (\<forall>m n. mult (Suc m) n = mult m n + n))"
kaliszyk@43787
    49
  apply (rule some_equality[symmetric])
kaliszyk@43787
    50
  apply auto
kaliszyk@43787
    51
  apply (rule ext)+
kaliszyk@43787
    52
  apply (induct_tac x)
kaliszyk@43787
    53
  apply auto
kaliszyk@43787
    54
  done
kaliszyk@43787
    55
kaliszyk@43787
    56
lemma DEF__slash__backslash_:
kaliszyk@43787
    57
  "(t1 \<and> t2) = ((\<lambda>f. f t1 t2 :: bool) = (\<lambda>f. f True True))"
kaliszyk@43787
    58
  unfolding fun_eq_iff
kaliszyk@43787
    59
  by (intro iffI, simp_all) (erule allE[of _ "(%a b. a \<and> b)"], simp)
kaliszyk@43787
    60
kaliszyk@43787
    61
lemma DEF__lessthan__equal_:
kaliszyk@43787
    62
  "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
    63
  apply (rule some_equality[symmetric])
kaliszyk@43787
    64
  apply auto[1]
kaliszyk@43787
    65
  apply (simp add: fun_eq_iff)
kaliszyk@43787
    66
  apply (intro allI)
kaliszyk@43787
    67
  apply (induct_tac xa)
kaliszyk@43787
    68
  apply auto
kaliszyk@43787
    69
  done
kaliszyk@43787
    70
kaliszyk@43787
    71
lemma DEF__lessthan_:
kaliszyk@43787
    72
  "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
    73
  apply (rule some_equality[symmetric])
kaliszyk@43787
    74
  apply auto[1]
kaliszyk@43787
    75
  apply (simp add: fun_eq_iff)
kaliszyk@43787
    76
  apply (intro allI)
kaliszyk@43787
    77
  apply (induct_tac xa)
kaliszyk@43787
    78
  apply auto
kaliszyk@43787
    79
  done
kaliszyk@43787
    80
kaliszyk@43787
    81
lemma DEF__greaterthan__equal_:
kaliszyk@43787
    82
  "(op \<ge>) = (%u ua. ua \<le> u)"
kaliszyk@43787
    83
  by (simp)
kaliszyk@43787
    84
kaliszyk@43787
    85
lemma DEF__greaterthan_:
kaliszyk@43787
    86
  "(op >) = (%u ua. ua < u)"
kaliszyk@43787
    87
  by (simp)
obua@17322
    88
kaliszyk@43787
    89
lemma DEF__equal__equal__greaterthan_:
kaliszyk@43787
    90
  "(t1 \<longrightarrow> t2) = ((t1 \<and> t2) = t1)"
kaliszyk@43787
    91
  by auto
kaliszyk@43787
    92
kaliszyk@43787
    93
lemma DEF_WF:
kaliszyk@43787
    94
  "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
    95
  unfolding fun_eq_iff
kaliszyk@43787
    96
  apply (intro allI, rule, intro allI impI, elim exE)
kaliszyk@43787
    97
  apply (drule_tac wfE_min[to_pred, unfolded mem_def])
kaliszyk@43787
    98
  apply assumption
kaliszyk@43787
    99
  prefer 2
kaliszyk@43787
   100
  apply assumption
kaliszyk@43787
   101
  apply auto[1]
kaliszyk@43787
   102
  apply (intro wfI_min[to_pred, unfolded mem_def])
kaliszyk@43787
   103
  apply (drule_tac x="Q" in spec)
kaliszyk@43787
   104
  apply auto
kaliszyk@43787
   105
  apply (rule_tac x="xb" in bexI)
kaliszyk@43787
   106
  apply (auto simp add: mem_def)
kaliszyk@43787
   107
  done
kaliszyk@43787
   108
kaliszyk@43787
   109
lemma DEF_UNIV: "UNIV = (%x. True)"
kaliszyk@43787
   110
  by (auto simp add: mem_def)
obua@17322
   111
kaliszyk@43787
   112
lemma DEF_UNIONS:
kaliszyk@43787
   113
  "Sup = (\<lambda>u. {ua. \<exists>x. (\<exists>ua. ua \<in> u \<and> x \<in> ua) \<and> ua = x})"
kaliszyk@43787
   114
  by (simp add: fun_eq_iff Collect_def)
kaliszyk@43787
   115
     (metis UnionE complete_lattice_class.Sup_upper mem_def predicate1D)
kaliszyk@43787
   116
kaliszyk@43787
   117
lemma DEF_UNION:
kaliszyk@43787
   118
  "op \<union> = (\<lambda>u ua. {ub. \<exists>x. (x \<in> u \<or> x \<in> ua) \<and> ub = x})"
kaliszyk@43787
   119
  by (auto simp add: mem_def fun_eq_iff Collect_def)
kaliszyk@43787
   120
kaliszyk@43787
   121
lemma DEF_SUBSET: "op \<subseteq> = (\<lambda>u ua. \<forall>x. x \<in> u \<longrightarrow> x \<in> ua)"
kaliszyk@43787
   122
  by (metis set_rev_mp subsetI)
kaliszyk@43787
   123
kaliszyk@43787
   124
lemma DEF_SND:
kaliszyk@43787
   125
  "snd = (\<lambda>p. SOME x. EX y. p = (y, x))"
kaliszyk@43787
   126
  unfolding fun_eq_iff
kaliszyk@43787
   127
  by (rule someI2) (auto intro: snd_conv[symmetric] someI2)
kaliszyk@43787
   128
kaliszyk@43787
   129
definition [simp, hol4rew]: "SETSPEC x P y \<longleftrightarrow> P & x = y"
kaliszyk@43787
   130
kaliszyk@43787
   131
lemma DEF_PSUBSET: "op \<subset> = (\<lambda>u ua. u \<subseteq> ua & u \<noteq> ua)"
kaliszyk@43787
   132
  by (auto simp add: mem_def fun_eq_iff)
kaliszyk@43787
   133
kaliszyk@43787
   134
definition [hol4rew]: "Pred n = n - (Suc 0)"
kaliszyk@43787
   135
kaliszyk@43787
   136
lemma DEF_PRE: "Pred = (SOME PRE. PRE 0 = 0 & (\<forall>n. PRE (Suc n) = n))"
obua@17322
   137
  apply (rule some_equality[symmetric])
obua@17322
   138
  apply (simp add: Pred_def)
obua@17322
   139
  apply (rule ext)
obua@17322
   140
  apply (induct_tac x)
obua@17322
   141
  apply (auto simp add: Pred_def)
obua@17322
   142
  done
obua@17322
   143
kaliszyk@43787
   144
lemma DEF_ONE_ONE:
kaliszyk@43787
   145
  "inj = (\<lambda>u. \<forall>x1 x2. u x1 = u x2 \<longrightarrow> x1 = x2)"
kaliszyk@43787
   146
  by (simp add: inj_on_def)
kaliszyk@43787
   147
kaliszyk@43787
   148
definition ODD'[hol4rew]: "(ODD :: nat \<Rightarrow> bool) = odd"
obua@17322
   149
kaliszyk@43787
   150
lemma DEF_ODD:
kaliszyk@43787
   151
  "odd = (SOME ODD. ODD 0 = False \<and> (\<forall>n. ODD (Suc n) = (\<not> ODD n)))"
kaliszyk@43787
   152
  apply (rule some_equality[symmetric])
kaliszyk@43787
   153
  apply simp
kaliszyk@43787
   154
  unfolding fun_eq_iff
kaliszyk@43787
   155
  apply (intro allI)
kaliszyk@43787
   156
  apply (induct_tac x)
kaliszyk@43787
   157
  apply simp_all
obua@17322
   158
  done
obua@17322
   159
kaliszyk@43787
   160
definition [hol4rew, simp]: "NUMERAL (x :: nat) = x"
kaliszyk@43787
   161
kaliszyk@43787
   162
lemma DEF_MOD:
kaliszyk@43787
   163
  "op mod = (SOME r. \<forall>m n. if n = (0 :: nat) then m div n = 0 \<and>
kaliszyk@43787
   164
     r m n = m else m = m div n * n + r m n \<and> r m n < n)"
kaliszyk@43787
   165
  apply (rule some_equality[symmetric])
kaliszyk@43787
   166
  apply (auto simp add: fun_eq_iff)
kaliszyk@43787
   167
  apply (case_tac "xa = 0")
kaliszyk@43787
   168
  apply auto
kaliszyk@43787
   169
  apply (drule_tac x="x" in spec)
kaliszyk@43787
   170
  apply (drule_tac x="xa" in spec)
kaliszyk@43787
   171
  apply auto
kaliszyk@43787
   172
  by (metis mod_less mod_mult_self2 nat_add_commute nat_mult_commute)
kaliszyk@43787
   173
kaliszyk@43787
   174
definition "MEASURE = (%u x y. (u x :: nat) < u y)"
kaliszyk@43787
   175
kaliszyk@43787
   176
lemma [hol4rew]:
kaliszyk@43787
   177
  "MEASURE u = (%a b. measure u (a, b))"
kaliszyk@43787
   178
  unfolding MEASURE_def measure_def fun_eq_iff inv_image_def Collect_def
kaliszyk@43787
   179
  by simp
kaliszyk@43787
   180
kaliszyk@43787
   181
definition
kaliszyk@43787
   182
  "LET f s = f s"
kaliszyk@43787
   183
kaliszyk@43787
   184
lemma [hol4rew]:
kaliszyk@43787
   185
  "LET f s = Let s f"
kaliszyk@43787
   186
  by (simp add: LET_def Let_def)
kaliszyk@43787
   187
kaliszyk@43787
   188
lemma DEF_INTERS:
kaliszyk@43787
   189
  "Inter = (\<lambda>u. {ua. \<exists>x. (\<forall>ua. ua \<in> u \<longrightarrow> x \<in> ua) \<and> ua = x})"
kaliszyk@43787
   190
  by (auto simp add: fun_eq_iff mem_def Collect_def)
kaliszyk@43787
   191
     (metis InterD InterI mem_def)+
kaliszyk@43787
   192
kaliszyk@43787
   193
lemma DEF_INTER:
kaliszyk@43787
   194
  "op \<inter> = (\<lambda>u ua. {ub. \<exists>x. (x \<in> u \<and> x \<in> ua) \<and> ub = x})"
kaliszyk@43787
   195
  by (auto simp add: mem_def fun_eq_iff Collect_def)
kaliszyk@43787
   196
kaliszyk@43787
   197
lemma DEF_INSERT:
kaliszyk@43787
   198
  "insert = (%u ua y. y \<in> ua | y = u)"
kaliszyk@43787
   199
  unfolding mem_def fun_eq_iff insert_code by blast
kaliszyk@43787
   200
kaliszyk@43787
   201
lemma DEF_IMAGE:
kaliszyk@43787
   202
  "op ` = (\<lambda>u ua. {ub. \<exists>y. (\<exists>x. x \<in> ua \<and> y = u x) \<and> ub = y})"
kaliszyk@43787
   203
  by (simp add: fun_eq_iff image_def Bex_def)
kaliszyk@43787
   204
kaliszyk@43787
   205
lemma DEF_GSPEC:
kaliszyk@43787
   206
  "Collect = (\<lambda>u. u)"
kaliszyk@43787
   207
  by (simp add: Collect_def ext)
kaliszyk@43787
   208
kaliszyk@43787
   209
lemma DEF_GEQ:
kaliszyk@43787
   210
  "(op =) = (op =)"
kaliszyk@43787
   211
  by simp
kaliszyk@43787
   212
kaliszyk@43787
   213
lemma DEF_GABS:
kaliszyk@43787
   214
  "Eps = Eps"
kaliszyk@43787
   215
  by simp
kaliszyk@43787
   216
kaliszyk@43787
   217
lemma DEF_FST:
kaliszyk@43787
   218
  "fst = (%p. SOME x. EX y. p = (x, y))"
kaliszyk@43787
   219
  unfolding fun_eq_iff
kaliszyk@43787
   220
  by (rule someI2) (auto intro: fst_conv[symmetric] someI2)
kaliszyk@43787
   221
kaliszyk@43787
   222
lemma DEF_FINITE:
kaliszyk@43787
   223
  "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
   224
  unfolding fun_eq_iff
kaliszyk@43787
   225
  apply (intro allI iffI impI)
kaliszyk@43787
   226
  apply (erule finite_induct)
kaliszyk@43787
   227
  apply auto[2]
kaliszyk@43787
   228
  apply (drule_tac x="finite" in spec)
kaliszyk@43787
   229
  apply auto
kaliszyk@43787
   230
  apply (metis Collect_def Collect_empty_eq finite.emptyI)
kaliszyk@43787
   231
  by (metis (no_types) finite.insertI predicate1I sup.commute sup_absorb1)
kaliszyk@43787
   232
kaliszyk@43787
   233
lemma DEF_FACT:
kaliszyk@43787
   234
  "fact = (SOME FACT. FACT 0 = 1 & (\<forall>n. FACT (Suc n) = Suc n * FACT n))"
kaliszyk@43787
   235
  apply (rule some_equality[symmetric])
kaliszyk@43787
   236
  apply (simp_all)
kaliszyk@43787
   237
  unfolding fun_eq_iff
kaliszyk@43787
   238
  apply (intro allI)
kaliszyk@43787
   239
  apply (induct_tac x)
kaliszyk@43787
   240
  apply simp_all
obua@17322
   241
  done
obua@17322
   242
kaliszyk@43787
   243
lemma DEF_EXP:
kaliszyk@43787
   244
  "power = (SOME EXP. (\<forall>m. EXP m 0 = 1) \<and> (\<forall>m n. EXP m (Suc n) = m * EXP m n))"
kaliszyk@43787
   245
  apply (rule some_equality[symmetric])
kaliszyk@43787
   246
  apply (simp_all)
kaliszyk@43787
   247
  unfolding fun_eq_iff
kaliszyk@43787
   248
  apply (intro allI)
kaliszyk@43787
   249
  apply (induct_tac xa)
kaliszyk@43787
   250
  apply simp_all
kaliszyk@43787
   251
  done
kaliszyk@43787
   252
kaliszyk@43787
   253
lemma DEF_EVEN:
kaliszyk@43787
   254
  "even = (SOME EVEN. EVEN 0 = True \<and> (\<forall>n. EVEN (Suc n) = (\<not> EVEN n)))"
kaliszyk@43787
   255
  apply (rule some_equality[symmetric])
kaliszyk@43787
   256
  apply simp
kaliszyk@43787
   257
  unfolding fun_eq_iff
kaliszyk@43787
   258
  apply (intro allI)
kaliszyk@43787
   259
  apply (induct_tac x)
kaliszyk@43787
   260
  apply simp_all
obua@17322
   261
  done
obua@17322
   262
kaliszyk@43787
   263
lemma DEF_EMPTY: "{} = (%x. False)"
kaliszyk@43787
   264
  unfolding fun_eq_iff empty_def
kaliszyk@43787
   265
  by auto
kaliszyk@43787
   266
kaliszyk@43787
   267
lemma DEF_DIV:
kaliszyk@43787
   268
  "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
   269
     else m = q m n * n + r m n \<and> r m n < n)"
kaliszyk@43787
   270
  apply (rule some_equality[symmetric])
kaliszyk@43787
   271
  apply (rule_tac x="op mod" in exI)
kaliszyk@43787
   272
  apply (auto simp add: fun_eq_iff)
kaliszyk@43787
   273
  apply (case_tac "xa = 0")
kaliszyk@43787
   274
  apply auto
kaliszyk@43787
   275
  apply (drule_tac x="x" in spec)
kaliszyk@43787
   276
  apply (drule_tac x="xa" in spec)
kaliszyk@43787
   277
  apply auto
kaliszyk@43787
   278
  by (metis div_mult_self2 gr_implies_not0 mod_div_trivial mod_less
kaliszyk@43787
   279
      nat_add_commute nat_mult_commute plus_nat.add_0)
kaliszyk@43787
   280
kaliszyk@43787
   281
definition [hol4rew]: "DISJOINT a b \<longleftrightarrow> a \<inter> b = {}"
kaliszyk@43787
   282
kaliszyk@43787
   283
lemma DEF_DISJOINT:
kaliszyk@43787
   284
  "DISJOINT = (%u ua. u \<inter> ua = {})"
kaliszyk@43787
   285
  by (auto simp add: DISJOINT_def_raw)
kaliszyk@43787
   286
kaliszyk@43787
   287
lemma DEF_DIFF:
kaliszyk@43787
   288
  "op - = (\<lambda>u ua. {ub. \<exists>x. (x \<in> u \<and> x \<notin> ua) \<and> ub = x})"
kaliszyk@43787
   289
  by (simp add: fun_eq_iff Collect_def)
kaliszyk@43787
   290
     (metis DiffE DiffI mem_def)
kaliszyk@43787
   291
kaliszyk@43787
   292
definition [hol4rew]: "DELETE s e = s - {e}"
kaliszyk@43787
   293
kaliszyk@43787
   294
lemma DEF_DELETE:
kaliszyk@43787
   295
  "DELETE = (\<lambda>u ua. {ub. \<exists>y. (y \<in> u \<and> y \<noteq> ua) \<and> ub = y})"
kaliszyk@43787
   296
  by (auto simp add: DELETE_def_raw)
kaliszyk@43787
   297
kaliszyk@43787
   298
lemma COND_DEF:
kaliszyk@43787
   299
  "(if b then t else f) = (SOME x. (b = True \<longrightarrow> x = t) \<and> (b = False \<longrightarrow> x = f))"
kaliszyk@43787
   300
  by auto
kaliszyk@43787
   301
kaliszyk@43787
   302
definition [simp]: "NUMERAL_BIT1 n = n + (n + Suc 0)"
kaliszyk@43787
   303
kaliszyk@43787
   304
lemma BIT1_DEF:
kaliszyk@43787
   305
  "NUMERAL_BIT1 = (%u. Suc (2 * u))"
kaliszyk@43787
   306
  by (auto)
kaliszyk@43787
   307
kaliszyk@43787
   308
definition [simp]: "NUMERAL_BIT0 (n :: nat) = n + n"
kaliszyk@43787
   309
kaliszyk@43787
   310
lemma BIT0_DEF:
kaliszyk@43787
   311
  "NUMERAL_BIT0 = (SOME BIT0. BIT0 0 = 0 \<and> (\<forall>n. BIT0 (Suc n) = Suc (Suc (BIT0 n))))"
kaliszyk@43787
   312
  apply (rule some_equality[symmetric])
kaliszyk@43787
   313
  apply auto
kaliszyk@43787
   314
  apply (rule ext)
kaliszyk@43787
   315
  apply (induct_tac x)
kaliszyk@43787
   316
  apply auto
kaliszyk@43787
   317
  done
kaliszyk@43787
   318
kaliszyk@43787
   319
lemma [hol4rew]:
kaliszyk@43787
   320
  "NUMERAL_BIT0 n = 2 * n"
kaliszyk@43787
   321
  "NUMERAL_BIT1 n = 2 * n + 1"
kaliszyk@43787
   322
  "2 * 0 = (0 :: nat)"
kaliszyk@43787
   323
  "2 * 1 = (2 :: nat)"
kaliszyk@43787
   324
  "0 + 1 = (1 :: nat)"
kaliszyk@43787
   325
  by simp_all
kaliszyk@43787
   326
kaliszyk@43787
   327
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
   328
  apply (rule some_equality[symmetric])
kaliszyk@43787
   329
  apply auto
kaliszyk@43787
   330
  apply (rule ext)+
kaliszyk@43787
   331
  apply (induct_tac xa)
kaliszyk@43787
   332
  apply auto
kaliszyk@43787
   333
  done
kaliszyk@43787
   334
kaliszyk@43787
   335
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
   336
  apply (rule some_equality[symmetric])
obua@17322
   337
  apply auto
obua@17322
   338
  apply (rule ext)+
obua@17322
   339
  apply (induct_tac x)
obua@17322
   340
  apply auto
obua@17322
   341
  done
obua@17322
   342
kaliszyk@43787
   343
lemmas [hol4rew] = id_apply
obua@17322
   344
kaliszyk@43787
   345
lemma DEF_CHOICE: "Eps = (%u. SOME x. x \<in> u)"
kaliszyk@43787
   346
  by (simp add: mem_def)
kaliszyk@43787
   347
kaliszyk@43787
   348
definition dotdot :: "nat => nat => nat => bool"
kaliszyk@43787
   349
  where "dotdot == %(u::nat) ua::nat. {ub::nat. EX x::nat. (u <= x & x <= ua) & ub = x}"
obua@17322
   350
kaliszyk@43787
   351
lemma DEF__dot__dot_: "dotdot = (%u ua. {ub. EX x. (u <= x & x <= ua) & ub = x})"
kaliszyk@43787
   352
  by (simp add: dotdot_def)
obua@17322
   353
kaliszyk@43787
   354
lemma [hol4rew]: "dotdot a b = {a..b}"
kaliszyk@43787
   355
  unfolding fun_eq_iff atLeastAtMost_def atLeast_def atMost_def dotdot_def
kaliszyk@43787
   356
  by (simp add: Collect_conj_eq)
kaliszyk@43787
   357
kaliszyk@43787
   358
definition [hol4rew,simp]: "INFINITE S \<longleftrightarrow> \<not> finite S"
kaliszyk@43787
   359
kaliszyk@43787
   360
lemma DEF_INFINITE: "INFINITE = (\<lambda>u. \<not>finite u)"
kaliszyk@43787
   361
  by (simp add: INFINITE_def_raw)
obua@17322
   362
obua@17322
   363
end