src/HOL/NSA/HyperNat.thy
author huffman
Fri Mar 30 12:32:35 2012 +0200 (2012-03-30)
changeset 47220 52426c62b5d0
parent 42463 f270e3e18be5
child 57512 cc97b347b301
permissions -rw-r--r--
replace lemmas eval_nat_numeral with a simpler reformulation
huffman@27468
     1
(*  Title       : HyperNat.thy
huffman@27468
     2
    Author      : Jacques D. Fleuriot
huffman@27468
     3
    Copyright   : 1998  University of Cambridge
huffman@27468
     4
huffman@27468
     5
Converted to Isar and polished by lcp    
huffman@27468
     6
*)
huffman@27468
     7
huffman@27468
     8
header{*Hypernatural numbers*}
huffman@27468
     9
huffman@27468
    10
theory HyperNat
huffman@27468
    11
imports StarDef
huffman@27468
    12
begin
huffman@27468
    13
wenzelm@42463
    14
type_synonym hypnat = "nat star"
huffman@27468
    15
huffman@27468
    16
abbreviation
huffman@27468
    17
  hypnat_of_nat :: "nat => nat star" where
huffman@27468
    18
  "hypnat_of_nat == star_of"
huffman@27468
    19
huffman@27468
    20
definition
huffman@27468
    21
  hSuc :: "hypnat => hypnat" where
haftmann@37765
    22
  hSuc_def [transfer_unfold]: "hSuc = *f* Suc"
huffman@27468
    23
huffman@27468
    24
subsection{*Properties Transferred from Naturals*}
huffman@27468
    25
huffman@27468
    26
lemma hSuc_not_zero [iff]: "\<And>m. hSuc m \<noteq> 0"
huffman@27468
    27
by transfer (rule Suc_not_Zero)
huffman@27468
    28
huffman@27468
    29
lemma zero_not_hSuc [iff]: "\<And>m. 0 \<noteq> hSuc m"
huffman@27468
    30
by transfer (rule Zero_not_Suc)
huffman@27468
    31
huffman@27468
    32
lemma hSuc_hSuc_eq [iff]: "\<And>m n. (hSuc m = hSuc n) = (m = n)"
huffman@27468
    33
by transfer (rule nat.inject)
huffman@27468
    34
huffman@27468
    35
lemma zero_less_hSuc [iff]: "\<And>n. 0 < hSuc n"
huffman@27468
    36
by transfer (rule zero_less_Suc)
huffman@27468
    37
huffman@27468
    38
lemma hypnat_minus_zero [simp]: "!!z. z - z = (0::hypnat)"
huffman@27468
    39
by transfer (rule diff_self_eq_0)
huffman@27468
    40
huffman@27468
    41
lemma hypnat_diff_0_eq_0 [simp]: "!!n. (0::hypnat) - n = 0"
huffman@27468
    42
by transfer (rule diff_0_eq_0)
huffman@27468
    43
huffman@27468
    44
lemma hypnat_add_is_0 [iff]: "!!m n. (m+n = (0::hypnat)) = (m=0 & n=0)"
huffman@27468
    45
by transfer (rule add_is_0)
huffman@27468
    46
huffman@27468
    47
lemma hypnat_diff_diff_left: "!!i j k. (i::hypnat) - j - k = i - (j+k)"
huffman@27468
    48
by transfer (rule diff_diff_left)
huffman@27468
    49
huffman@27468
    50
lemma hypnat_diff_commute: "!!i j k. (i::hypnat) - j - k = i-k-j"
huffman@27468
    51
by transfer (rule diff_commute)
huffman@27468
    52
huffman@27468
    53
lemma hypnat_diff_add_inverse [simp]: "!!m n. ((n::hypnat) + m) - n = m"
huffman@27468
    54
by transfer (rule diff_add_inverse)
huffman@27468
    55
huffman@27468
    56
lemma hypnat_diff_add_inverse2 [simp]:  "!!m n. ((m::hypnat) + n) - n = m"
huffman@27468
    57
by transfer (rule diff_add_inverse2)
huffman@27468
    58
huffman@27468
    59
lemma hypnat_diff_cancel [simp]: "!!k m n. ((k::hypnat) + m) - (k+n) = m - n"
huffman@27468
    60
by transfer (rule diff_cancel)
huffman@27468
    61
huffman@27468
    62
lemma hypnat_diff_cancel2 [simp]: "!!k m n. ((m::hypnat) + k) - (n+k) = m - n"
huffman@27468
    63
by transfer (rule diff_cancel2)
huffman@27468
    64
huffman@27468
    65
lemma hypnat_diff_add_0 [simp]: "!!m n. (n::hypnat) - (n+m) = (0::hypnat)"
huffman@27468
    66
by transfer (rule diff_add_0)
huffman@27468
    67
huffman@27468
    68
lemma hypnat_diff_mult_distrib: "!!k m n. ((m::hypnat) - n) * k = (m * k) - (n * k)"
huffman@27468
    69
by transfer (rule diff_mult_distrib)
huffman@27468
    70
huffman@27468
    71
lemma hypnat_diff_mult_distrib2: "!!k m n. (k::hypnat) * (m - n) = (k * m) - (k * n)"
huffman@27468
    72
by transfer (rule diff_mult_distrib2)
huffman@27468
    73
huffman@27468
    74
lemma hypnat_le_zero_cancel [iff]: "!!n. (n \<le> (0::hypnat)) = (n = 0)"
huffman@27468
    75
by transfer (rule le_0_eq)
huffman@27468
    76
huffman@27468
    77
lemma hypnat_mult_is_0 [simp]: "!!m n. (m*n = (0::hypnat)) = (m=0 | n=0)"
huffman@27468
    78
by transfer (rule mult_is_0)
huffman@27468
    79
huffman@27468
    80
lemma hypnat_diff_is_0_eq [simp]: "!!m n. ((m::hypnat) - n = 0) = (m \<le> n)"
huffman@27468
    81
by transfer (rule diff_is_0_eq)
huffman@27468
    82
huffman@27468
    83
lemma hypnat_not_less0 [iff]: "!!n. ~ n < (0::hypnat)"
huffman@27468
    84
by transfer (rule not_less0)
huffman@27468
    85
huffman@27468
    86
lemma hypnat_less_one [iff]:
huffman@27468
    87
      "!!n. (n < (1::hypnat)) = (n=0)"
huffman@27468
    88
by transfer (rule less_one)
huffman@27468
    89
huffman@27468
    90
lemma hypnat_add_diff_inverse: "!!m n. ~ m<n ==> n+(m-n) = (m::hypnat)"
huffman@27468
    91
by transfer (rule add_diff_inverse)
huffman@27468
    92
huffman@27468
    93
lemma hypnat_le_add_diff_inverse [simp]: "!!m n. n \<le> m ==> n+(m-n) = (m::hypnat)"
huffman@27468
    94
by transfer (rule le_add_diff_inverse)
huffman@27468
    95
huffman@27468
    96
lemma hypnat_le_add_diff_inverse2 [simp]: "!!m n. n\<le>m ==> (m-n)+n = (m::hypnat)"
huffman@27468
    97
by transfer (rule le_add_diff_inverse2)
huffman@27468
    98
huffman@27468
    99
declare hypnat_le_add_diff_inverse2 [OF order_less_imp_le]
huffman@27468
   100
huffman@27468
   101
lemma hypnat_le0 [iff]: "!!n. (0::hypnat) \<le> n"
huffman@27468
   102
by transfer (rule le0)
huffman@27468
   103
huffman@27468
   104
lemma hypnat_le_add1 [simp]: "!!x n. (x::hypnat) \<le> x + n"
huffman@27468
   105
by transfer (rule le_add1)
huffman@27468
   106
huffman@27468
   107
lemma hypnat_add_self_le [simp]: "!!x n. (x::hypnat) \<le> n + x"
huffman@27468
   108
by transfer (rule le_add2)
huffman@27468
   109
huffman@27468
   110
lemma hypnat_add_one_self_less [simp]: "(x::hypnat) < x + (1::hypnat)"
huffman@27468
   111
by (insert add_strict_left_mono [OF zero_less_one], auto)
huffman@27468
   112
huffman@27468
   113
lemma hypnat_neq0_conv [iff]: "!!n. (n \<noteq> 0) = (0 < (n::hypnat))"
huffman@27468
   114
by transfer (rule neq0_conv)
huffman@27468
   115
huffman@27468
   116
lemma hypnat_gt_zero_iff: "((0::hypnat) < n) = ((1::hypnat) \<le> n)"
huffman@27468
   117
by (auto simp add: linorder_not_less [symmetric])
huffman@27468
   118
huffman@27468
   119
lemma hypnat_gt_zero_iff2: "(0 < n) = (\<exists>m. n = m + (1::hypnat))"
huffman@27468
   120
apply safe
huffman@27468
   121
 apply (rule_tac x = "n - (1::hypnat) " in exI)
huffman@27468
   122
 apply (simp add: hypnat_gt_zero_iff) 
huffman@27468
   123
apply (insert add_le_less_mono [OF _ zero_less_one, of 0], auto) 
huffman@27468
   124
done
huffman@27468
   125
huffman@27468
   126
lemma hypnat_add_self_not_less: "~ (x + y < (x::hypnat))"
huffman@27468
   127
by (simp add: linorder_not_le [symmetric] add_commute [of x]) 
huffman@27468
   128
huffman@27468
   129
lemma hypnat_diff_split:
huffman@27468
   130
    "P(a - b::hypnat) = ((a<b --> P 0) & (ALL d. a = b + d --> P d))"
huffman@27468
   131
    -- {* elimination of @{text -} on @{text hypnat} *}
huffman@27468
   132
proof (cases "a<b" rule: case_split)
huffman@27468
   133
  case True
huffman@27468
   134
    thus ?thesis
huffman@27468
   135
      by (auto simp add: hypnat_add_self_not_less order_less_imp_le 
huffman@27468
   136
                         hypnat_diff_is_0_eq [THEN iffD2])
huffman@27468
   137
next
huffman@27468
   138
  case False
huffman@27468
   139
    thus ?thesis
huffman@27468
   140
      by (auto simp add: linorder_not_less dest: order_le_less_trans) 
huffman@27468
   141
qed
huffman@27468
   142
huffman@27468
   143
subsection{*Properties of the set of embedded natural numbers*}
huffman@27468
   144
huffman@27468
   145
lemma of_nat_eq_star_of [simp]: "of_nat = star_of"
huffman@27468
   146
proof
huffman@27468
   147
  fix n :: nat
huffman@27468
   148
  show "of_nat n = star_of n" by transfer simp
huffman@27468
   149
qed
huffman@27468
   150
huffman@27468
   151
lemma Nats_eq_Standard: "(Nats :: nat star set) = Standard"
huffman@27468
   152
by (auto simp add: Nats_def Standard_def)
huffman@27468
   153
huffman@27468
   154
lemma hypnat_of_nat_mem_Nats [simp]: "hypnat_of_nat n \<in> Nats"
huffman@27468
   155
by (simp add: Nats_eq_Standard)
huffman@27468
   156
huffman@27468
   157
lemma hypnat_of_nat_one [simp]: "hypnat_of_nat (Suc 0) = (1::hypnat)"
huffman@27468
   158
by transfer simp
huffman@27468
   159
huffman@27468
   160
lemma hypnat_of_nat_Suc [simp]:
huffman@27468
   161
     "hypnat_of_nat (Suc n) = hypnat_of_nat n + (1::hypnat)"
huffman@27468
   162
by transfer simp
huffman@27468
   163
huffman@27468
   164
lemma of_nat_eq_add [rule_format]:
huffman@27468
   165
     "\<forall>d::hypnat. of_nat m = of_nat n + d --> d \<in> range of_nat"
huffman@27468
   166
apply (induct n) 
huffman@27468
   167
apply (auto simp add: add_assoc) 
huffman@27468
   168
apply (case_tac x) 
huffman@27468
   169
apply (auto simp add: add_commute [of 1]) 
huffman@27468
   170
done
huffman@27468
   171
huffman@27468
   172
lemma Nats_diff [simp]: "[|a \<in> Nats; b \<in> Nats|] ==> (a-b :: hypnat) \<in> Nats"
huffman@27468
   173
by (simp add: Nats_eq_Standard)
huffman@27468
   174
huffman@27468
   175
huffman@27468
   176
subsection{*Infinite Hypernatural Numbers -- @{term HNatInfinite}*}
huffman@27468
   177
huffman@27468
   178
definition
huffman@27468
   179
  (* the set of infinite hypernatural numbers *)
huffman@27468
   180
  HNatInfinite :: "hypnat set" where
huffman@27468
   181
  "HNatInfinite = {n. n \<notin> Nats}"
huffman@27468
   182
huffman@27468
   183
lemma Nats_not_HNatInfinite_iff: "(x \<in> Nats) = (x \<notin> HNatInfinite)"
huffman@27468
   184
by (simp add: HNatInfinite_def)
huffman@27468
   185
huffman@27468
   186
lemma HNatInfinite_not_Nats_iff: "(x \<in> HNatInfinite) = (x \<notin> Nats)"
huffman@27468
   187
by (simp add: HNatInfinite_def)
huffman@27468
   188
huffman@27468
   189
lemma star_of_neq_HNatInfinite: "N \<in> HNatInfinite \<Longrightarrow> star_of n \<noteq> N"
huffman@27468
   190
by (auto simp add: HNatInfinite_def Nats_eq_Standard)
huffman@27468
   191
huffman@27468
   192
lemma star_of_Suc_lessI:
huffman@27468
   193
  "\<And>N. \<lbrakk>star_of n < N; star_of (Suc n) \<noteq> N\<rbrakk> \<Longrightarrow> star_of (Suc n) < N"
huffman@27468
   194
by transfer (rule Suc_lessI)
huffman@27468
   195
huffman@27468
   196
lemma star_of_less_HNatInfinite:
huffman@27468
   197
  assumes N: "N \<in> HNatInfinite"
huffman@27468
   198
  shows "star_of n < N"
huffman@27468
   199
proof (induct n)
huffman@27468
   200
  case 0
huffman@27468
   201
  from N have "star_of 0 \<noteq> N" by (rule star_of_neq_HNatInfinite)
huffman@27468
   202
  thus "star_of 0 < N" by simp
huffman@27468
   203
next
huffman@27468
   204
  case (Suc n)
huffman@27468
   205
  from N have "star_of (Suc n) \<noteq> N" by (rule star_of_neq_HNatInfinite)
huffman@27468
   206
  with Suc show "star_of (Suc n) < N" by (rule star_of_Suc_lessI)
huffman@27468
   207
qed
huffman@27468
   208
huffman@27468
   209
lemma star_of_le_HNatInfinite: "N \<in> HNatInfinite \<Longrightarrow> star_of n \<le> N"
huffman@27468
   210
by (rule star_of_less_HNatInfinite [THEN order_less_imp_le])
huffman@27468
   211
huffman@27468
   212
subsubsection {* Closure Rules *}
huffman@27468
   213
huffman@27468
   214
lemma Nats_less_HNatInfinite: "\<lbrakk>x \<in> Nats; y \<in> HNatInfinite\<rbrakk> \<Longrightarrow> x < y"
huffman@27468
   215
by (auto simp add: Nats_def star_of_less_HNatInfinite)
huffman@27468
   216
huffman@27468
   217
lemma Nats_le_HNatInfinite: "\<lbrakk>x \<in> Nats; y \<in> HNatInfinite\<rbrakk> \<Longrightarrow> x \<le> y"
huffman@27468
   218
by (rule Nats_less_HNatInfinite [THEN order_less_imp_le])
huffman@27468
   219
huffman@27468
   220
lemma zero_less_HNatInfinite: "x \<in> HNatInfinite \<Longrightarrow> 0 < x"
huffman@27468
   221
by (simp add: Nats_less_HNatInfinite)
huffman@27468
   222
huffman@27468
   223
lemma one_less_HNatInfinite: "x \<in> HNatInfinite \<Longrightarrow> 1 < x"
huffman@27468
   224
by (simp add: Nats_less_HNatInfinite)
huffman@27468
   225
huffman@27468
   226
lemma one_le_HNatInfinite: "x \<in> HNatInfinite \<Longrightarrow> 1 \<le> x"
huffman@27468
   227
by (simp add: Nats_le_HNatInfinite)
huffman@27468
   228
huffman@27468
   229
lemma zero_not_mem_HNatInfinite [simp]: "0 \<notin> HNatInfinite"
huffman@27468
   230
by (simp add: HNatInfinite_def)
huffman@27468
   231
huffman@27468
   232
lemma Nats_downward_closed:
huffman@27468
   233
  "\<lbrakk>x \<in> Nats; (y::hypnat) \<le> x\<rbrakk> \<Longrightarrow> y \<in> Nats"
huffman@27468
   234
apply (simp only: linorder_not_less [symmetric])
huffman@27468
   235
apply (erule contrapos_np)
huffman@27468
   236
apply (drule HNatInfinite_not_Nats_iff [THEN iffD2])
huffman@27468
   237
apply (erule (1) Nats_less_HNatInfinite)
huffman@27468
   238
done
huffman@27468
   239
huffman@27468
   240
lemma HNatInfinite_upward_closed:
huffman@27468
   241
  "\<lbrakk>x \<in> HNatInfinite; x \<le> y\<rbrakk> \<Longrightarrow> y \<in> HNatInfinite"
huffman@27468
   242
apply (simp only: HNatInfinite_not_Nats_iff)
huffman@27468
   243
apply (erule contrapos_nn)
huffman@27468
   244
apply (erule (1) Nats_downward_closed)
huffman@27468
   245
done
huffman@27468
   246
huffman@27468
   247
lemma HNatInfinite_add: "x \<in> HNatInfinite \<Longrightarrow> x + y \<in> HNatInfinite"
huffman@27468
   248
apply (erule HNatInfinite_upward_closed)
huffman@27468
   249
apply (rule hypnat_le_add1)
huffman@27468
   250
done
huffman@27468
   251
huffman@27468
   252
lemma HNatInfinite_add_one: "x \<in> HNatInfinite \<Longrightarrow> x + 1 \<in> HNatInfinite"
huffman@27468
   253
by (rule HNatInfinite_add)
huffman@27468
   254
huffman@27468
   255
lemma HNatInfinite_diff:
huffman@27468
   256
  "\<lbrakk>x \<in> HNatInfinite; y \<in> Nats\<rbrakk> \<Longrightarrow> x - y \<in> HNatInfinite"
huffman@27468
   257
apply (frule (1) Nats_le_HNatInfinite)
huffman@27468
   258
apply (simp only: HNatInfinite_not_Nats_iff)
huffman@27468
   259
apply (erule contrapos_nn)
huffman@27468
   260
apply (drule (1) Nats_add, simp)
huffman@27468
   261
done
huffman@27468
   262
huffman@27468
   263
lemma HNatInfinite_is_Suc: "x \<in> HNatInfinite ==> \<exists>y. x = y + (1::hypnat)"
huffman@27468
   264
apply (rule_tac x = "x - (1::hypnat) " in exI)
huffman@27468
   265
apply (simp add: Nats_le_HNatInfinite)
huffman@27468
   266
done
huffman@27468
   267
huffman@27468
   268
huffman@27468
   269
subsection{*Existence of an infinite hypernatural number*}
huffman@27468
   270
huffman@27468
   271
definition
huffman@27468
   272
  (* omega is in fact an infinite hypernatural number = [<1,2,3,...>] *)
huffman@27468
   273
  whn :: hypnat where
huffman@27468
   274
  hypnat_omega_def: "whn = star_n (%n::nat. n)"
huffman@27468
   275
huffman@27468
   276
lemma hypnat_of_nat_neq_whn: "hypnat_of_nat n \<noteq> whn"
huffman@27468
   277
by (simp add: hypnat_omega_def star_of_def star_n_eq_iff)
huffman@27468
   278
huffman@27468
   279
lemma whn_neq_hypnat_of_nat: "whn \<noteq> hypnat_of_nat n"
huffman@27468
   280
by (simp add: hypnat_omega_def star_of_def star_n_eq_iff)
huffman@27468
   281
huffman@27468
   282
lemma whn_not_Nats [simp]: "whn \<notin> Nats"
huffman@27468
   283
by (simp add: Nats_def image_def whn_neq_hypnat_of_nat)
huffman@27468
   284
huffman@27468
   285
lemma HNatInfinite_whn [simp]: "whn \<in> HNatInfinite"
huffman@27468
   286
by (simp add: HNatInfinite_def)
huffman@27468
   287
huffman@27468
   288
lemma lemma_unbounded_set [simp]: "{n::nat. m < n} \<in> FreeUltrafilterNat"
nipkow@29920
   289
apply (insert finite_atMost [of m])
huffman@27468
   290
apply (drule FreeUltrafilterNat.finite)
huffman@27468
   291
apply (drule FreeUltrafilterNat.not_memD)
nipkow@29920
   292
apply (simp add: Collect_neg_eq [symmetric] linorder_not_le atMost_def)
huffman@27468
   293
done
huffman@27468
   294
huffman@27468
   295
lemma Compl_Collect_le: "- {n::nat. N \<le> n} = {n. n < N}"
huffman@27468
   296
by (simp add: Collect_neg_eq [symmetric] linorder_not_le) 
huffman@27468
   297
huffman@27468
   298
lemma hypnat_of_nat_eq:
huffman@27468
   299
     "hypnat_of_nat m  = star_n (%n::nat. m)"
huffman@27468
   300
by (simp add: star_of_def)
huffman@27468
   301
huffman@27468
   302
lemma SHNat_eq: "Nats = {n. \<exists>N. n = hypnat_of_nat N}"
huffman@27468
   303
by (simp add: Nats_def image_def)
huffman@27468
   304
huffman@27468
   305
lemma Nats_less_whn: "n \<in> Nats \<Longrightarrow> n < whn"
huffman@27468
   306
by (simp add: Nats_less_HNatInfinite)
huffman@27468
   307
huffman@27468
   308
lemma Nats_le_whn: "n \<in> Nats \<Longrightarrow> n \<le> whn"
huffman@27468
   309
by (simp add: Nats_le_HNatInfinite)
huffman@27468
   310
huffman@27468
   311
lemma hypnat_of_nat_less_whn [simp]: "hypnat_of_nat n < whn"
huffman@27468
   312
by (simp add: Nats_less_whn)
huffman@27468
   313
huffman@27468
   314
lemma hypnat_of_nat_le_whn [simp]: "hypnat_of_nat n \<le> whn"
huffman@27468
   315
by (simp add: Nats_le_whn)
huffman@27468
   316
huffman@27468
   317
lemma hypnat_zero_less_hypnat_omega [simp]: "0 < whn"
huffman@27468
   318
by (simp add: Nats_less_whn)
huffman@27468
   319
huffman@27468
   320
lemma hypnat_one_less_hypnat_omega [simp]: "1 < whn"
huffman@27468
   321
by (simp add: Nats_less_whn)
huffman@27468
   322
huffman@27468
   323
huffman@27468
   324
subsubsection{*Alternative characterization of the set of infinite hypernaturals*}
huffman@27468
   325
huffman@27468
   326
text{* @{term "HNatInfinite = {N. \<forall>n \<in> Nats. n < N}"}*}
huffman@27468
   327
huffman@27468
   328
(*??delete? similar reasoning in hypnat_omega_gt_SHNat above*)
huffman@27468
   329
lemma HNatInfinite_FreeUltrafilterNat_lemma:
huffman@27468
   330
  assumes "\<forall>N::nat. {n. f n \<noteq> N} \<in> FreeUltrafilterNat"
huffman@27468
   331
  shows "{n. N < f n} \<in> FreeUltrafilterNat"
huffman@27468
   332
apply (induct N)
huffman@27468
   333
using assms
huffman@27468
   334
apply (drule_tac x = 0 in spec, simp)
huffman@27468
   335
using assms
huffman@27468
   336
apply (drule_tac x = "Suc N" in spec)
huffman@27468
   337
apply (elim ultra, auto)
huffman@27468
   338
done
huffman@27468
   339
huffman@27468
   340
lemma HNatInfinite_iff: "HNatInfinite = {N. \<forall>n \<in> Nats. n < N}"
huffman@27468
   341
apply (safe intro!: Nats_less_HNatInfinite)
huffman@27468
   342
apply (auto simp add: HNatInfinite_def)
huffman@27468
   343
done
huffman@27468
   344
huffman@27468
   345
huffman@27468
   346
subsubsection{*Alternative Characterization of @{term HNatInfinite} using 
huffman@27468
   347
Free Ultrafilter*}
huffman@27468
   348
huffman@27468
   349
lemma HNatInfinite_FreeUltrafilterNat:
huffman@27468
   350
     "star_n X \<in> HNatInfinite ==> \<forall>u. {n. u < X n}:  FreeUltrafilterNat"
huffman@27468
   351
apply (auto simp add: HNatInfinite_iff SHNat_eq)
huffman@27468
   352
apply (drule_tac x="star_of u" in spec, simp)
huffman@27468
   353
apply (simp add: star_of_def star_less_def starP2_star_n)
huffman@27468
   354
done
huffman@27468
   355
huffman@27468
   356
lemma FreeUltrafilterNat_HNatInfinite:
huffman@27468
   357
     "\<forall>u. {n. u < X n}:  FreeUltrafilterNat ==> star_n X \<in> HNatInfinite"
huffman@27468
   358
by (auto simp add: star_less_def starP2_star_n HNatInfinite_iff SHNat_eq hypnat_of_nat_eq)
huffman@27468
   359
huffman@27468
   360
lemma HNatInfinite_FreeUltrafilterNat_iff:
huffman@27468
   361
     "(star_n X \<in> HNatInfinite) = (\<forall>u. {n. u < X n}:  FreeUltrafilterNat)"
huffman@27468
   362
by (rule iffI [OF HNatInfinite_FreeUltrafilterNat 
huffman@27468
   363
                 FreeUltrafilterNat_HNatInfinite])
huffman@27468
   364
huffman@27468
   365
subsection {* Embedding of the Hypernaturals into other types *}
huffman@27468
   366
huffman@27468
   367
definition
huffman@27468
   368
  of_hypnat :: "hypnat \<Rightarrow> 'a::semiring_1_cancel star" where
haftmann@37765
   369
  of_hypnat_def [transfer_unfold]: "of_hypnat = *f* of_nat"
huffman@27468
   370
huffman@27468
   371
lemma of_hypnat_0 [simp]: "of_hypnat 0 = 0"
huffman@27468
   372
by transfer (rule of_nat_0)
huffman@27468
   373
huffman@27468
   374
lemma of_hypnat_1 [simp]: "of_hypnat 1 = 1"
huffman@27468
   375
by transfer (rule of_nat_1)
huffman@27468
   376
huffman@27468
   377
lemma of_hypnat_hSuc: "\<And>m. of_hypnat (hSuc m) = 1 + of_hypnat m"
huffman@27468
   378
by transfer (rule of_nat_Suc)
huffman@27468
   379
huffman@27468
   380
lemma of_hypnat_add [simp]:
huffman@27468
   381
  "\<And>m n. of_hypnat (m + n) = of_hypnat m + of_hypnat n"
huffman@27468
   382
by transfer (rule of_nat_add)
huffman@27468
   383
huffman@27468
   384
lemma of_hypnat_mult [simp]:
huffman@27468
   385
  "\<And>m n. of_hypnat (m * n) = of_hypnat m * of_hypnat n"
huffman@27468
   386
by transfer (rule of_nat_mult)
huffman@27468
   387
huffman@27468
   388
lemma of_hypnat_less_iff [simp]:
haftmann@35028
   389
  "\<And>m n. (of_hypnat m < (of_hypnat n::'a::linordered_semidom star)) = (m < n)"
huffman@27468
   390
by transfer (rule of_nat_less_iff)
huffman@27468
   391
huffman@27468
   392
lemma of_hypnat_0_less_iff [simp]:
haftmann@35028
   393
  "\<And>n. (0 < (of_hypnat n::'a::linordered_semidom star)) = (0 < n)"
huffman@27468
   394
by transfer (rule of_nat_0_less_iff)
huffman@27468
   395
huffman@27468
   396
lemma of_hypnat_less_0_iff [simp]:
haftmann@35028
   397
  "\<And>m. \<not> (of_hypnat m::'a::linordered_semidom star) < 0"
huffman@27468
   398
by transfer (rule of_nat_less_0_iff)
huffman@27468
   399
huffman@27468
   400
lemma of_hypnat_le_iff [simp]:
haftmann@35028
   401
  "\<And>m n. (of_hypnat m \<le> (of_hypnat n::'a::linordered_semidom star)) = (m \<le> n)"
huffman@27468
   402
by transfer (rule of_nat_le_iff)
huffman@27468
   403
huffman@27468
   404
lemma of_hypnat_0_le_iff [simp]:
haftmann@35028
   405
  "\<And>n. 0 \<le> (of_hypnat n::'a::linordered_semidom star)"
huffman@27468
   406
by transfer (rule of_nat_0_le_iff)
huffman@27468
   407
huffman@27468
   408
lemma of_hypnat_le_0_iff [simp]:
haftmann@35028
   409
  "\<And>m. ((of_hypnat m::'a::linordered_semidom star) \<le> 0) = (m = 0)"
huffman@27468
   410
by transfer (rule of_nat_le_0_iff)
huffman@27468
   411
huffman@27468
   412
lemma of_hypnat_eq_iff [simp]:
haftmann@35028
   413
  "\<And>m n. (of_hypnat m = (of_hypnat n::'a::linordered_semidom star)) = (m = n)"
huffman@27468
   414
by transfer (rule of_nat_eq_iff)
huffman@27468
   415
huffman@27468
   416
lemma of_hypnat_eq_0_iff [simp]:
haftmann@35028
   417
  "\<And>m. ((of_hypnat m::'a::linordered_semidom star) = 0) = (m = 0)"
huffman@27468
   418
by transfer (rule of_nat_eq_0_iff)
huffman@27468
   419
huffman@27468
   420
lemma HNatInfinite_of_hypnat_gt_zero:
haftmann@35028
   421
  "N \<in> HNatInfinite \<Longrightarrow> (0::'a::linordered_semidom star) < of_hypnat N"
huffman@27468
   422
by (rule ccontr, simp add: linorder_not_less)
huffman@27468
   423
huffman@27468
   424
end