src/HOL/Library/Saturated.thy
author haftmann
Tue Mar 26 20:49:57 2013 +0100 (2013-03-26)
changeset 51540 eea5c4ca4a0e
parent 51489 f738e6dbd844
child 51545 6f6012f430fc
permissions -rw-r--r--
explicit sublocale dependency for Min/Max yields more appropriate Min/Max prefix for a couple of facts
wenzelm@45692
     1
(*  Title:      HOL/Library/Saturated.thy
wenzelm@45692
     2
    Author:     Brian Huffman
wenzelm@45692
     3
    Author:     Peter Gammie
wenzelm@45692
     4
    Author:     Florian Haftmann
wenzelm@45692
     5
*)
haftmann@44819
     6
haftmann@44819
     7
header {* Saturated arithmetic *}
haftmann@44819
     8
haftmann@44819
     9
theory Saturated
haftmann@44819
    10
imports Main "~~/src/HOL/Library/Numeral_Type" "~~/src/HOL/Word/Type_Length"
haftmann@44819
    11
begin
haftmann@44819
    12
haftmann@44819
    13
subsection {* The type of saturated naturals *}
haftmann@44819
    14
wenzelm@49834
    15
typedef ('a::len) sat = "{.. len_of TYPE('a)}"
haftmann@44819
    16
  morphisms nat_of Abs_sat
haftmann@44819
    17
  by auto
haftmann@44819
    18
haftmann@44819
    19
lemma sat_eqI:
haftmann@44819
    20
  "nat_of m = nat_of n \<Longrightarrow> m = n"
haftmann@44819
    21
  by (simp add: nat_of_inject)
haftmann@44819
    22
haftmann@44819
    23
lemma sat_eq_iff:
haftmann@44819
    24
  "m = n \<longleftrightarrow> nat_of m = nat_of n"
haftmann@44819
    25
  by (simp add: nat_of_inject)
haftmann@44819
    26
huffman@44883
    27
lemma Abs_sat_nat_of [code abstype]:
haftmann@44819
    28
  "Abs_sat (nat_of n) = n"
haftmann@44819
    29
  by (fact nat_of_inverse)
haftmann@44819
    30
huffman@44883
    31
definition Abs_sat' :: "nat \<Rightarrow> 'a::len sat" where
huffman@44883
    32
  "Abs_sat' n = Abs_sat (min (len_of TYPE('a)) n)"
haftmann@44819
    33
huffman@44883
    34
lemma nat_of_Abs_sat' [simp]:
huffman@44883
    35
  "nat_of (Abs_sat' n :: ('a::len) sat) = min (len_of TYPE('a)) n"
huffman@44883
    36
  unfolding Abs_sat'_def by (rule Abs_sat_inverse) simp
haftmann@44819
    37
haftmann@44819
    38
lemma nat_of_le_len_of [simp]:
haftmann@44819
    39
  "nat_of (n :: ('a::len) sat) \<le> len_of TYPE('a)"
haftmann@44819
    40
  using nat_of [where x = n] by simp
haftmann@44819
    41
haftmann@44819
    42
lemma min_len_of_nat_of [simp]:
haftmann@44819
    43
  "min (len_of TYPE('a)) (nat_of (n::('a::len) sat)) = nat_of n"
haftmann@44819
    44
  by (rule min_max.inf_absorb2 [OF nat_of_le_len_of])
haftmann@44819
    45
haftmann@44819
    46
lemma min_nat_of_len_of [simp]:
haftmann@44819
    47
  "min (nat_of (n::('a::len) sat)) (len_of TYPE('a)) = nat_of n"
haftmann@51540
    48
  by (subst min.commute) simp
haftmann@44819
    49
huffman@44883
    50
lemma Abs_sat'_nat_of [simp]:
huffman@44883
    51
  "Abs_sat' (nat_of n) = n"
huffman@44883
    52
  by (simp add: Abs_sat'_def nat_of_inverse)
haftmann@44819
    53
haftmann@44819
    54
instantiation sat :: (len) linorder
haftmann@44819
    55
begin
haftmann@44819
    56
haftmann@44819
    57
definition
haftmann@44819
    58
  less_eq_sat_def: "x \<le> y \<longleftrightarrow> nat_of x \<le> nat_of y"
haftmann@44819
    59
haftmann@44819
    60
definition
haftmann@44819
    61
  less_sat_def: "x < y \<longleftrightarrow> nat_of x < nat_of y"
haftmann@44819
    62
haftmann@44819
    63
instance
haftmann@44819
    64
by default (auto simp add: less_eq_sat_def less_sat_def not_le sat_eq_iff min_max.le_infI1 nat_mult_commute)
haftmann@44819
    65
haftmann@44819
    66
end
haftmann@44819
    67
huffman@44849
    68
instantiation sat :: (len) "{minus, comm_semiring_1}"
haftmann@44819
    69
begin
haftmann@44819
    70
haftmann@44819
    71
definition
huffman@44883
    72
  "0 = Abs_sat' 0"
haftmann@44819
    73
haftmann@44819
    74
definition
huffman@44883
    75
  "1 = Abs_sat' 1"
haftmann@44819
    76
haftmann@44819
    77
lemma nat_of_zero_sat [simp, code abstract]:
haftmann@44819
    78
  "nat_of 0 = 0"
haftmann@44819
    79
  by (simp add: zero_sat_def)
haftmann@44819
    80
haftmann@44819
    81
lemma nat_of_one_sat [simp, code abstract]:
haftmann@44819
    82
  "nat_of 1 = min 1 (len_of TYPE('a))"
haftmann@44819
    83
  by (simp add: one_sat_def)
haftmann@44819
    84
haftmann@44819
    85
definition
huffman@44883
    86
  "x + y = Abs_sat' (nat_of x + nat_of y)"
haftmann@44819
    87
haftmann@44819
    88
lemma nat_of_plus_sat [simp, code abstract]:
haftmann@44819
    89
  "nat_of (x + y) = min (nat_of x + nat_of y) (len_of TYPE('a))"
haftmann@44819
    90
  by (simp add: plus_sat_def)
haftmann@44819
    91
haftmann@44819
    92
definition
huffman@44883
    93
  "x - y = Abs_sat' (nat_of x - nat_of y)"
haftmann@44819
    94
haftmann@44819
    95
lemma nat_of_minus_sat [simp, code abstract]:
haftmann@44819
    96
  "nat_of (x - y) = nat_of x - nat_of y"
haftmann@44819
    97
proof -
haftmann@44819
    98
  from nat_of_le_len_of [of x] have "nat_of x - nat_of y \<le> len_of TYPE('a)" by arith
haftmann@44819
    99
  then show ?thesis by (simp add: minus_sat_def)
haftmann@44819
   100
qed
haftmann@44819
   101
haftmann@44819
   102
definition
huffman@44883
   103
  "x * y = Abs_sat' (nat_of x * nat_of y)"
haftmann@44819
   104
haftmann@44819
   105
lemma nat_of_times_sat [simp, code abstract]:
haftmann@44819
   106
  "nat_of (x * y) = min (nat_of x * nat_of y) (len_of TYPE('a))"
haftmann@44819
   107
  by (simp add: times_sat_def)
haftmann@44819
   108
haftmann@44819
   109
instance proof
haftmann@44819
   110
  fix a b c :: "('a::len) sat"
haftmann@44819
   111
  show "a * b * c = a * (b * c)"
haftmann@44819
   112
  proof(cases "a = 0")
haftmann@44819
   113
    case True thus ?thesis by (simp add: sat_eq_iff)
haftmann@44819
   114
  next
haftmann@44819
   115
    case False show ?thesis
haftmann@44819
   116
    proof(cases "c = 0")
haftmann@44819
   117
      case True thus ?thesis by (simp add: sat_eq_iff)
haftmann@44819
   118
    next
haftmann@44819
   119
      case False with `a \<noteq> 0` show ?thesis
haftmann@44819
   120
        by (simp add: sat_eq_iff nat_mult_min_left nat_mult_min_right mult_assoc min_max.inf_assoc min_max.inf_absorb2)
haftmann@44819
   121
    qed
haftmann@44819
   122
  qed
haftmann@44819
   123
next
haftmann@44819
   124
  fix a :: "('a::len) sat"
haftmann@44819
   125
  show "1 * a = a"
haftmann@44819
   126
    apply (simp add: sat_eq_iff)
haftmann@44819
   127
    apply (metis One_nat_def len_gt_0 less_Suc0 less_zeroE linorder_not_less min_max.le_iff_inf min_nat_of_len_of nat_mult_1_right nat_mult_commute)
haftmann@44819
   128
    done
haftmann@44819
   129
next
haftmann@44819
   130
  fix a b c :: "('a::len) sat"
haftmann@44819
   131
  show "(a + b) * c = a * c + b * c"
haftmann@44819
   132
  proof(cases "c = 0")
haftmann@44819
   133
    case True thus ?thesis by (simp add: sat_eq_iff)
haftmann@44819
   134
  next
haftmann@44819
   135
    case False thus ?thesis
huffman@44848
   136
      by (simp add: sat_eq_iff nat_mult_min_left add_mult_distrib min_add_distrib_left min_add_distrib_right min_max.inf_assoc min_max.inf_absorb2)
haftmann@44819
   137
  qed
haftmann@44819
   138
qed (simp_all add: sat_eq_iff mult.commute)
haftmann@44819
   139
haftmann@44819
   140
end
haftmann@44819
   141
haftmann@44819
   142
instantiation sat :: (len) ordered_comm_semiring
haftmann@44819
   143
begin
haftmann@44819
   144
haftmann@44819
   145
instance
haftmann@44819
   146
by default (auto simp add: less_eq_sat_def less_sat_def not_le sat_eq_iff min_max.le_infI1 nat_mult_commute)
haftmann@44819
   147
haftmann@44819
   148
end
haftmann@44819
   149
huffman@44883
   150
lemma Abs_sat'_eq_of_nat: "Abs_sat' n = of_nat n"
huffman@44849
   151
  by (rule sat_eqI, induct n, simp_all)
huffman@44849
   152
huffman@44883
   153
abbreviation Sat :: "nat \<Rightarrow> 'a::len sat" where
huffman@44883
   154
  "Sat \<equiv> of_nat"
huffman@44883
   155
huffman@44883
   156
lemma nat_of_Sat [simp]:
huffman@44883
   157
  "nat_of (Sat n :: ('a::len) sat) = min (len_of TYPE('a)) n"
huffman@44883
   158
  by (rule nat_of_Abs_sat' [unfolded Abs_sat'_eq_of_nat])
huffman@44883
   159
huffman@47108
   160
lemma [code_abbrev]:
huffman@47108
   161
  "of_nat (numeral k) = (numeral k :: 'a::len sat)"
huffman@47108
   162
  by simp
haftmann@44819
   163
huffman@47108
   164
definition sat_of_nat :: "nat \<Rightarrow> ('a::len) sat"
huffman@47108
   165
  where [code_abbrev]: "sat_of_nat = of_nat"
haftmann@44819
   166
haftmann@44819
   167
lemma [code abstract]:
huffman@47108
   168
  "nat_of (sat_of_nat n :: ('a::len) sat) = min (len_of TYPE('a)) n"
huffman@47108
   169
  by (simp add: sat_of_nat_def)
haftmann@44819
   170
haftmann@44819
   171
instance sat :: (len) finite
haftmann@44819
   172
proof
haftmann@44819
   173
  show "finite (UNIV::'a sat set)"
haftmann@44819
   174
    unfolding type_definition.univ [OF type_definition_sat]
haftmann@44819
   175
    using finite by simp
haftmann@44819
   176
qed
haftmann@44819
   177
haftmann@44819
   178
instantiation sat :: (len) equal
haftmann@44819
   179
begin
haftmann@44819
   180
haftmann@44819
   181
definition
haftmann@44819
   182
  "HOL.equal A B \<longleftrightarrow> nat_of A = nat_of B"
haftmann@44819
   183
haftmann@44819
   184
instance proof
haftmann@44819
   185
qed (simp add: equal_sat_def nat_of_inject)
haftmann@44819
   186
haftmann@44819
   187
end
haftmann@44819
   188
haftmann@44819
   189
instantiation sat :: (len) "{bounded_lattice, distrib_lattice}"
haftmann@44819
   190
begin
haftmann@44819
   191
haftmann@44819
   192
definition
haftmann@44819
   193
  "(inf :: 'a sat \<Rightarrow> 'a sat \<Rightarrow> 'a sat) = min"
haftmann@44819
   194
haftmann@44819
   195
definition
haftmann@44819
   196
  "(sup :: 'a sat \<Rightarrow> 'a sat \<Rightarrow> 'a sat) = max"
haftmann@44819
   197
haftmann@44819
   198
definition
haftmann@44819
   199
  "bot = (0 :: 'a sat)"
haftmann@44819
   200
haftmann@44819
   201
definition
haftmann@44819
   202
  "top = Sat (len_of TYPE('a))"
haftmann@44819
   203
haftmann@44819
   204
instance proof
haftmann@44819
   205
qed (simp_all add: inf_sat_def sup_sat_def bot_sat_def top_sat_def min_max.sup_inf_distrib1,
haftmann@44819
   206
  simp_all add: less_eq_sat_def)
haftmann@44819
   207
haftmann@44819
   208
end
haftmann@44819
   209
haftmann@51489
   210
instantiation sat :: (len) "{Inf, Sup}"
haftmann@44819
   211
begin
haftmann@44819
   212
haftmann@44819
   213
definition
haftmann@51489
   214
  "Inf = (semilattice_neutr_set.F min top :: 'a sat set \<Rightarrow> 'a sat)"
haftmann@44819
   215
haftmann@44819
   216
definition
haftmann@51489
   217
  "Sup = (semilattice_neutr_set.F max bot :: 'a sat set \<Rightarrow> 'a sat)"
haftmann@51489
   218
haftmann@51489
   219
instance ..
haftmann@51489
   220
haftmann@51489
   221
end
haftmann@44819
   222
haftmann@51489
   223
interpretation Inf_sat!: semilattice_neutr_set min "top :: 'a::len sat"
haftmann@51489
   224
where
haftmann@51489
   225
  "semilattice_neutr_set.F min (top :: 'a sat) = Inf"
haftmann@51489
   226
proof -
haftmann@51489
   227
  show "semilattice_neutr_set min (top :: 'a sat)" by default (simp add: min_def)
haftmann@51489
   228
  show "semilattice_neutr_set.F min (top :: 'a sat) = Inf" by (simp add: Inf_sat_def)
haftmann@51489
   229
qed
haftmann@51489
   230
haftmann@51489
   231
interpretation Sup_sat!: semilattice_neutr_set max "bot :: 'a::len sat"
haftmann@51489
   232
where
haftmann@51489
   233
  "semilattice_neutr_set.F max (bot :: 'a sat) = Sup"
haftmann@51489
   234
proof -
haftmann@51489
   235
  show "semilattice_neutr_set max (bot :: 'a sat)" by default (simp add: max_def bot.extremum_unique)
haftmann@51489
   236
  show "semilattice_neutr_set.F max (bot :: 'a sat) = Sup" by (simp add: Sup_sat_def)
haftmann@51489
   237
qed
haftmann@51489
   238
haftmann@51489
   239
instance sat :: (len) complete_lattice
haftmann@51489
   240
proof 
haftmann@44819
   241
  fix x :: "'a sat"
haftmann@44819
   242
  fix A :: "'a sat set"
haftmann@44819
   243
  note finite
haftmann@44819
   244
  moreover assume "x \<in> A"
haftmann@51489
   245
  ultimately show "Inf A \<le> x"
haftmann@51489
   246
    by (induct A) (auto intro: min_max.le_infI2)
haftmann@44819
   247
next
haftmann@44819
   248
  fix z :: "'a sat"
haftmann@44819
   249
  fix A :: "'a sat set"
haftmann@44819
   250
  note finite
haftmann@44819
   251
  moreover assume z: "\<And>x. x \<in> A \<Longrightarrow> z \<le> x"
haftmann@51489
   252
  ultimately show "z \<le> Inf A" by (induct A) simp_all
haftmann@44819
   253
next
haftmann@44819
   254
  fix x :: "'a sat"
haftmann@44819
   255
  fix A :: "'a sat set"
haftmann@44819
   256
  note finite
haftmann@44819
   257
  moreover assume "x \<in> A"
haftmann@51489
   258
  ultimately show "x \<le> Sup A"
haftmann@51489
   259
    by (induct A) (auto intro: min_max.le_supI2)
haftmann@44819
   260
next
haftmann@44819
   261
  fix z :: "'a sat"
haftmann@44819
   262
  fix A :: "'a sat set"
haftmann@44819
   263
  note finite
haftmann@44819
   264
  moreover assume z: "\<And>x. x \<in> A \<Longrightarrow> x \<le> z"
haftmann@51489
   265
  ultimately show "Sup A \<le> z" by (induct A) auto
haftmann@44819
   266
qed
haftmann@44819
   267
huffman@47108
   268
hide_const (open) sat_of_nat
huffman@47108
   269
haftmann@44819
   270
end
haftmann@51489
   271