src/HOL/Library/Saturated.thy
author wenzelm
Mon Dec 28 01:28:28 2015 +0100 (2015-12-28)
changeset 61945 1135b8de26c3
parent 61605 1bf7b186542e
child 63433 aa03b0487bf5
permissions -rw-r--r--
more symbols;
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
wenzelm@60500
     7
section \<open>Saturated arithmetic\<close>
haftmann@44819
     8
haftmann@44819
     9
theory Saturated
wenzelm@51542
    10
imports Numeral_Type "~~/src/HOL/Word/Type_Length"
haftmann@44819
    11
begin
haftmann@44819
    12
wenzelm@60500
    13
subsection \<open>The type of saturated naturals\<close>
haftmann@44819
    14
wenzelm@61260
    15
typedef (overloaded) ('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@54863
    44
  by (rule min.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
wenzelm@60679
    64
  by standard
wenzelm@60679
    65
    (auto simp add: less_eq_sat_def less_sat_def not_le sat_eq_iff min.coboundedI1 mult.commute)
haftmann@44819
    66
haftmann@44819
    67
end
haftmann@44819
    68
huffman@44849
    69
instantiation sat :: (len) "{minus, comm_semiring_1}"
haftmann@44819
    70
begin
haftmann@44819
    71
haftmann@44819
    72
definition
huffman@44883
    73
  "0 = Abs_sat' 0"
haftmann@44819
    74
haftmann@44819
    75
definition
huffman@44883
    76
  "1 = Abs_sat' 1"
haftmann@44819
    77
haftmann@44819
    78
lemma nat_of_zero_sat [simp, code abstract]:
haftmann@44819
    79
  "nat_of 0 = 0"
haftmann@44819
    80
  by (simp add: zero_sat_def)
haftmann@44819
    81
haftmann@44819
    82
lemma nat_of_one_sat [simp, code abstract]:
haftmann@44819
    83
  "nat_of 1 = min 1 (len_of TYPE('a))"
haftmann@44819
    84
  by (simp add: one_sat_def)
haftmann@44819
    85
haftmann@44819
    86
definition
huffman@44883
    87
  "x + y = Abs_sat' (nat_of x + nat_of y)"
haftmann@44819
    88
haftmann@44819
    89
lemma nat_of_plus_sat [simp, code abstract]:
haftmann@44819
    90
  "nat_of (x + y) = min (nat_of x + nat_of y) (len_of TYPE('a))"
haftmann@44819
    91
  by (simp add: plus_sat_def)
haftmann@44819
    92
haftmann@44819
    93
definition
huffman@44883
    94
  "x - y = Abs_sat' (nat_of x - nat_of y)"
haftmann@44819
    95
haftmann@44819
    96
lemma nat_of_minus_sat [simp, code abstract]:
haftmann@44819
    97
  "nat_of (x - y) = nat_of x - nat_of y"
haftmann@44819
    98
proof -
haftmann@44819
    99
  from nat_of_le_len_of [of x] have "nat_of x - nat_of y \<le> len_of TYPE('a)" by arith
haftmann@44819
   100
  then show ?thesis by (simp add: minus_sat_def)
haftmann@44819
   101
qed
haftmann@44819
   102
haftmann@44819
   103
definition
huffman@44883
   104
  "x * y = Abs_sat' (nat_of x * nat_of y)"
haftmann@44819
   105
haftmann@44819
   106
lemma nat_of_times_sat [simp, code abstract]:
haftmann@44819
   107
  "nat_of (x * y) = min (nat_of x * nat_of y) (len_of TYPE('a))"
haftmann@44819
   108
  by (simp add: times_sat_def)
haftmann@44819
   109
wenzelm@60679
   110
instance
wenzelm@60679
   111
proof
wenzelm@60679
   112
  fix a b c :: "'a::len sat"
haftmann@44819
   113
  show "a * b * c = a * (b * c)"
haftmann@44819
   114
  proof(cases "a = 0")
haftmann@44819
   115
    case True thus ?thesis by (simp add: sat_eq_iff)
haftmann@44819
   116
  next
haftmann@44819
   117
    case False show ?thesis
haftmann@44819
   118
    proof(cases "c = 0")
haftmann@44819
   119
      case True thus ?thesis by (simp add: sat_eq_iff)
haftmann@44819
   120
    next
wenzelm@60500
   121
      case False with \<open>a \<noteq> 0\<close> show ?thesis
haftmann@57512
   122
        by (simp add: sat_eq_iff nat_mult_min_left nat_mult_min_right mult.assoc min.assoc min.absorb2)
haftmann@44819
   123
    qed
haftmann@44819
   124
  qed
haftmann@44819
   125
  show "1 * a = a"
haftmann@44819
   126
    apply (simp add: sat_eq_iff)
haftmann@57512
   127
    apply (metis One_nat_def len_gt_0 less_Suc0 less_zeroE linorder_not_less min.absorb_iff1 min_nat_of_len_of nat_mult_1_right mult.commute)
haftmann@44819
   128
    done
haftmann@44819
   129
  show "(a + b) * c = a * c + b * c"
haftmann@44819
   130
  proof(cases "c = 0")
haftmann@44819
   131
    case True thus ?thesis by (simp add: sat_eq_iff)
haftmann@44819
   132
  next
haftmann@44819
   133
    case False thus ?thesis
haftmann@54863
   134
      by (simp add: sat_eq_iff nat_mult_min_left add_mult_distrib min_add_distrib_left min_add_distrib_right min.assoc min.absorb2)
haftmann@44819
   135
  qed
haftmann@44819
   136
qed (simp_all add: sat_eq_iff mult.commute)
haftmann@44819
   137
haftmann@44819
   138
end
haftmann@44819
   139
haftmann@44819
   140
instantiation sat :: (len) ordered_comm_semiring
haftmann@44819
   141
begin
haftmann@44819
   142
haftmann@44819
   143
instance
wenzelm@60679
   144
  by standard
wenzelm@60679
   145
    (auto simp add: less_eq_sat_def less_sat_def not_le sat_eq_iff min.coboundedI1 mult.commute)
haftmann@44819
   146
haftmann@44819
   147
end
haftmann@44819
   148
huffman@44883
   149
lemma Abs_sat'_eq_of_nat: "Abs_sat' n = of_nat n"
huffman@44849
   150
  by (rule sat_eqI, induct n, simp_all)
huffman@44849
   151
huffman@44883
   152
abbreviation Sat :: "nat \<Rightarrow> 'a::len sat" where
huffman@44883
   153
  "Sat \<equiv> of_nat"
huffman@44883
   154
huffman@44883
   155
lemma nat_of_Sat [simp]:
huffman@44883
   156
  "nat_of (Sat n :: ('a::len) sat) = min (len_of TYPE('a)) n"
huffman@44883
   157
  by (rule nat_of_Abs_sat' [unfolded Abs_sat'_eq_of_nat])
huffman@44883
   158
huffman@47108
   159
lemma [code_abbrev]:
huffman@47108
   160
  "of_nat (numeral k) = (numeral k :: 'a::len sat)"
huffman@47108
   161
  by simp
haftmann@44819
   162
wenzelm@60011
   163
context
wenzelm@60011
   164
begin
wenzelm@60011
   165
wenzelm@60011
   166
qualified definition sat_of_nat :: "nat \<Rightarrow> ('a::len) sat"
huffman@47108
   167
  where [code_abbrev]: "sat_of_nat = of_nat"
haftmann@44819
   168
haftmann@44819
   169
lemma [code abstract]:
huffman@47108
   170
  "nat_of (sat_of_nat n :: ('a::len) sat) = min (len_of TYPE('a)) n"
huffman@47108
   171
  by (simp add: sat_of_nat_def)
haftmann@44819
   172
wenzelm@60011
   173
end
wenzelm@60011
   174
haftmann@44819
   175
instance sat :: (len) finite
haftmann@44819
   176
proof
haftmann@44819
   177
  show "finite (UNIV::'a sat set)"
haftmann@44819
   178
    unfolding type_definition.univ [OF type_definition_sat]
haftmann@44819
   179
    using finite by simp
haftmann@44819
   180
qed
haftmann@44819
   181
haftmann@44819
   182
instantiation sat :: (len) equal
haftmann@44819
   183
begin
haftmann@44819
   184
wenzelm@60679
   185
definition "HOL.equal A B \<longleftrightarrow> nat_of A = nat_of B"
haftmann@44819
   186
wenzelm@60679
   187
instance
wenzelm@60679
   188
  by standard (simp add: equal_sat_def nat_of_inject)
haftmann@44819
   189
haftmann@44819
   190
end
haftmann@44819
   191
haftmann@44819
   192
instantiation sat :: (len) "{bounded_lattice, distrib_lattice}"
haftmann@44819
   193
begin
haftmann@44819
   194
wenzelm@60679
   195
definition "(inf :: 'a sat \<Rightarrow> 'a sat \<Rightarrow> 'a sat) = min"
wenzelm@60679
   196
definition "(sup :: 'a sat \<Rightarrow> 'a sat \<Rightarrow> 'a sat) = max"
wenzelm@60679
   197
definition "bot = (0 :: 'a sat)"
wenzelm@60679
   198
definition "top = Sat (len_of TYPE('a))"
haftmann@44819
   199
wenzelm@60679
   200
instance
wenzelm@60679
   201
  by standard
wenzelm@60679
   202
    (simp_all add: inf_sat_def sup_sat_def bot_sat_def top_sat_def max_min_distrib2,
wenzelm@60679
   203
      simp_all add: less_eq_sat_def)
haftmann@44819
   204
haftmann@44819
   205
end
haftmann@44819
   206
haftmann@51489
   207
instantiation sat :: (len) "{Inf, Sup}"
haftmann@44819
   208
begin
haftmann@44819
   209
wenzelm@60679
   210
definition "Inf = (semilattice_neutr_set.F min top :: 'a sat set \<Rightarrow> 'a sat)"
wenzelm@60679
   211
definition "Sup = (semilattice_neutr_set.F max bot :: 'a sat set \<Rightarrow> 'a sat)"
haftmann@51489
   212
haftmann@51489
   213
instance ..
haftmann@51489
   214
haftmann@51489
   215
end
haftmann@44819
   216
wenzelm@61605
   217
interpretation Inf_sat: semilattice_neutr_set min "top :: 'a::len sat"
ballarin@61566
   218
rewrites
haftmann@51489
   219
  "semilattice_neutr_set.F min (top :: 'a sat) = Inf"
haftmann@51489
   220
proof -
wenzelm@60679
   221
  show "semilattice_neutr_set min (top :: 'a sat)"
wenzelm@60679
   222
    by standard (simp add: min_def)
wenzelm@60679
   223
  show "semilattice_neutr_set.F min (top :: 'a sat) = Inf"
wenzelm@60679
   224
    by (simp add: Inf_sat_def)
haftmann@51489
   225
qed
haftmann@51489
   226
wenzelm@61605
   227
interpretation Sup_sat: semilattice_neutr_set max "bot :: 'a::len sat"
ballarin@61566
   228
rewrites
haftmann@51489
   229
  "semilattice_neutr_set.F max (bot :: 'a sat) = Sup"
haftmann@51489
   230
proof -
wenzelm@60679
   231
  show "semilattice_neutr_set max (bot :: 'a sat)"
wenzelm@60679
   232
    by standard (simp add: max_def bot.extremum_unique)
wenzelm@60679
   233
  show "semilattice_neutr_set.F max (bot :: 'a sat) = Sup"
wenzelm@60679
   234
    by (simp add: Sup_sat_def)
haftmann@51489
   235
qed
haftmann@51489
   236
haftmann@51489
   237
instance sat :: (len) complete_lattice
haftmann@51489
   238
proof 
haftmann@44819
   239
  fix x :: "'a sat"
haftmann@44819
   240
  fix A :: "'a sat set"
haftmann@44819
   241
  note finite
haftmann@44819
   242
  moreover assume "x \<in> A"
haftmann@51489
   243
  ultimately show "Inf A \<le> x"
haftmann@54863
   244
    by (induct A) (auto intro: min.coboundedI2)
haftmann@44819
   245
next
haftmann@44819
   246
  fix z :: "'a sat"
haftmann@44819
   247
  fix A :: "'a sat set"
haftmann@44819
   248
  note finite
haftmann@44819
   249
  moreover assume z: "\<And>x. x \<in> A \<Longrightarrow> z \<le> x"
haftmann@51489
   250
  ultimately show "z \<le> Inf A" by (induct A) simp_all
haftmann@44819
   251
next
haftmann@44819
   252
  fix x :: "'a sat"
haftmann@44819
   253
  fix A :: "'a sat set"
haftmann@44819
   254
  note finite
haftmann@44819
   255
  moreover assume "x \<in> A"
haftmann@51489
   256
  ultimately show "x \<le> Sup A"
haftmann@54863
   257
    by (induct A) (auto intro: max.coboundedI2)
haftmann@44819
   258
next
haftmann@44819
   259
  fix z :: "'a sat"
haftmann@44819
   260
  fix A :: "'a sat set"
haftmann@44819
   261
  note finite
haftmann@44819
   262
  moreover assume z: "\<And>x. x \<in> A \<Longrightarrow> x \<le> z"
haftmann@51489
   263
  ultimately show "Sup A \<le> z" by (induct A) auto
haftmann@52729
   264
next
haftmann@52729
   265
  show "Inf {} = (top::'a sat)"
haftmann@52729
   266
    by (auto simp: top_sat_def)
haftmann@52729
   267
  show "Sup {} = (bot::'a sat)"
haftmann@52729
   268
    by (auto simp: bot_sat_def)
haftmann@44819
   269
qed
haftmann@44819
   270
haftmann@44819
   271
end