src/HOL/Library/Saturated.thy
author huffman
Thu Sep 08 19:35:23 2011 -0700 (2011-09-08)
changeset 44849 41fddafe20d5
parent 44848 f4d0b060c7ca
child 44883 a7f9c97378b3
permissions -rw-r--r--
Library/Saturated.thy: number_semiring class instance
haftmann@44819
     1
(* Author: Brian Huffman *)
haftmann@44819
     2
(* Author: Peter Gammie *)
haftmann@44819
     3
(* Author: Florian Haftmann *)
haftmann@44819
     4
haftmann@44819
     5
header {* Saturated arithmetic *}
haftmann@44819
     6
haftmann@44819
     7
theory Saturated
haftmann@44819
     8
imports Main "~~/src/HOL/Library/Numeral_Type" "~~/src/HOL/Word/Type_Length"
haftmann@44819
     9
begin
haftmann@44819
    10
haftmann@44819
    11
subsection {* The type of saturated naturals *}
haftmann@44819
    12
haftmann@44819
    13
typedef (open) ('a::len) sat = "{.. len_of TYPE('a)}"
haftmann@44819
    14
  morphisms nat_of Abs_sat
haftmann@44819
    15
  by auto
haftmann@44819
    16
haftmann@44819
    17
lemma sat_eqI:
haftmann@44819
    18
  "nat_of m = nat_of n \<Longrightarrow> m = n"
haftmann@44819
    19
  by (simp add: nat_of_inject)
haftmann@44819
    20
haftmann@44819
    21
lemma sat_eq_iff:
haftmann@44819
    22
  "m = n \<longleftrightarrow> nat_of m = nat_of n"
haftmann@44819
    23
  by (simp add: nat_of_inject)
haftmann@44819
    24
haftmann@44819
    25
lemma Abs_sa_nat_of [code abstype]:
haftmann@44819
    26
  "Abs_sat (nat_of n) = n"
haftmann@44819
    27
  by (fact nat_of_inverse)
haftmann@44819
    28
haftmann@44819
    29
definition Sat :: "nat \<Rightarrow> 'a::len sat" where
haftmann@44819
    30
  "Sat n = Abs_sat (min (len_of TYPE('a)) n)"
haftmann@44819
    31
haftmann@44819
    32
lemma nat_of_Sat [simp]:
haftmann@44819
    33
  "nat_of (Sat n :: ('a::len) sat) = min (len_of TYPE('a)) n"
haftmann@44819
    34
  unfolding Sat_def by (rule Abs_sat_inverse) simp
haftmann@44819
    35
haftmann@44819
    36
lemma nat_of_le_len_of [simp]:
haftmann@44819
    37
  "nat_of (n :: ('a::len) sat) \<le> len_of TYPE('a)"
haftmann@44819
    38
  using nat_of [where x = n] by simp
haftmann@44819
    39
haftmann@44819
    40
lemma min_len_of_nat_of [simp]:
haftmann@44819
    41
  "min (len_of TYPE('a)) (nat_of (n::('a::len) sat)) = nat_of n"
haftmann@44819
    42
  by (rule min_max.inf_absorb2 [OF nat_of_le_len_of])
haftmann@44819
    43
haftmann@44819
    44
lemma min_nat_of_len_of [simp]:
haftmann@44819
    45
  "min (nat_of (n::('a::len) sat)) (len_of TYPE('a)) = nat_of n"
haftmann@44819
    46
  by (subst min_max.inf.commute) simp
haftmann@44819
    47
haftmann@44819
    48
lemma Sat_nat_of [simp]:
haftmann@44819
    49
  "Sat (nat_of n) = n"
haftmann@44819
    50
  by (simp add: Sat_def nat_of_inverse)
haftmann@44819
    51
haftmann@44819
    52
instantiation sat :: (len) linorder
haftmann@44819
    53
begin
haftmann@44819
    54
haftmann@44819
    55
definition
haftmann@44819
    56
  less_eq_sat_def: "x \<le> y \<longleftrightarrow> nat_of x \<le> nat_of y"
haftmann@44819
    57
haftmann@44819
    58
definition
haftmann@44819
    59
  less_sat_def: "x < y \<longleftrightarrow> nat_of x < nat_of y"
haftmann@44819
    60
haftmann@44819
    61
instance
haftmann@44819
    62
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
    63
haftmann@44819
    64
end
haftmann@44819
    65
huffman@44849
    66
instantiation sat :: (len) "{minus, comm_semiring_1}"
haftmann@44819
    67
begin
haftmann@44819
    68
haftmann@44819
    69
definition
haftmann@44819
    70
  "0 = Sat 0"
haftmann@44819
    71
haftmann@44819
    72
definition
haftmann@44819
    73
  "1 = Sat 1"
haftmann@44819
    74
haftmann@44819
    75
lemma nat_of_zero_sat [simp, code abstract]:
haftmann@44819
    76
  "nat_of 0 = 0"
haftmann@44819
    77
  by (simp add: zero_sat_def)
haftmann@44819
    78
haftmann@44819
    79
lemma nat_of_one_sat [simp, code abstract]:
haftmann@44819
    80
  "nat_of 1 = min 1 (len_of TYPE('a))"
haftmann@44819
    81
  by (simp add: one_sat_def)
haftmann@44819
    82
haftmann@44819
    83
definition
haftmann@44819
    84
  "x + y = Sat (nat_of x + nat_of y)"
haftmann@44819
    85
haftmann@44819
    86
lemma nat_of_plus_sat [simp, code abstract]:
haftmann@44819
    87
  "nat_of (x + y) = min (nat_of x + nat_of y) (len_of TYPE('a))"
haftmann@44819
    88
  by (simp add: plus_sat_def)
haftmann@44819
    89
haftmann@44819
    90
definition
haftmann@44819
    91
  "x - y = Sat (nat_of x - nat_of y)"
haftmann@44819
    92
haftmann@44819
    93
lemma nat_of_minus_sat [simp, code abstract]:
haftmann@44819
    94
  "nat_of (x - y) = nat_of x - nat_of y"
haftmann@44819
    95
proof -
haftmann@44819
    96
  from nat_of_le_len_of [of x] have "nat_of x - nat_of y \<le> len_of TYPE('a)" by arith
haftmann@44819
    97
  then show ?thesis by (simp add: minus_sat_def)
haftmann@44819
    98
qed
haftmann@44819
    99
haftmann@44819
   100
definition
haftmann@44819
   101
  "x * y = Sat (nat_of x * nat_of y)"
haftmann@44819
   102
haftmann@44819
   103
lemma nat_of_times_sat [simp, code abstract]:
haftmann@44819
   104
  "nat_of (x * y) = min (nat_of x * nat_of y) (len_of TYPE('a))"
haftmann@44819
   105
  by (simp add: times_sat_def)
haftmann@44819
   106
haftmann@44819
   107
instance proof
haftmann@44819
   108
  fix a b c :: "('a::len) sat"
haftmann@44819
   109
  show "a * b * c = a * (b * c)"
haftmann@44819
   110
  proof(cases "a = 0")
haftmann@44819
   111
    case True thus ?thesis by (simp add: sat_eq_iff)
haftmann@44819
   112
  next
haftmann@44819
   113
    case False show ?thesis
haftmann@44819
   114
    proof(cases "c = 0")
haftmann@44819
   115
      case True thus ?thesis by (simp add: sat_eq_iff)
haftmann@44819
   116
    next
haftmann@44819
   117
      case False with `a \<noteq> 0` show ?thesis
haftmann@44819
   118
        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
   119
    qed
haftmann@44819
   120
  qed
haftmann@44819
   121
next
haftmann@44819
   122
  fix a :: "('a::len) sat"
haftmann@44819
   123
  show "1 * a = a"
haftmann@44819
   124
    apply (simp add: sat_eq_iff)
haftmann@44819
   125
    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
   126
    done
haftmann@44819
   127
next
haftmann@44819
   128
  fix a b c :: "('a::len) sat"
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
huffman@44848
   134
      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
   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
haftmann@44819
   144
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
   145
haftmann@44819
   146
end
haftmann@44819
   147
huffman@44849
   148
lemma Sat_eq_of_nat: "Sat n = of_nat n"
huffman@44849
   149
  by (rule sat_eqI, induct n, simp_all)
huffman@44849
   150
huffman@44849
   151
instantiation sat :: (len) number_semiring
haftmann@44819
   152
begin
haftmann@44819
   153
haftmann@44819
   154
definition
haftmann@44819
   155
  number_of_sat_def [code del]: "number_of = Sat \<circ> nat"
haftmann@44819
   156
huffman@44849
   157
instance
huffman@44849
   158
  by default (simp add: number_of_sat_def Sat_eq_of_nat)
haftmann@44819
   159
haftmann@44819
   160
end
haftmann@44819
   161
haftmann@44819
   162
lemma [code abstract]:
haftmann@44819
   163
  "nat_of (number_of n :: ('a::len) sat) = min (nat n) (len_of TYPE('a))"
haftmann@44819
   164
  unfolding number_of_sat_def by simp
haftmann@44819
   165
haftmann@44819
   166
instance sat :: (len) finite
haftmann@44819
   167
proof
haftmann@44819
   168
  show "finite (UNIV::'a sat set)"
haftmann@44819
   169
    unfolding type_definition.univ [OF type_definition_sat]
haftmann@44819
   170
    using finite by simp
haftmann@44819
   171
qed
haftmann@44819
   172
haftmann@44819
   173
instantiation sat :: (len) equal
haftmann@44819
   174
begin
haftmann@44819
   175
haftmann@44819
   176
definition
haftmann@44819
   177
  "HOL.equal A B \<longleftrightarrow> nat_of A = nat_of B"
haftmann@44819
   178
haftmann@44819
   179
instance proof
haftmann@44819
   180
qed (simp add: equal_sat_def nat_of_inject)
haftmann@44819
   181
haftmann@44819
   182
end
haftmann@44819
   183
haftmann@44819
   184
instantiation sat :: (len) "{bounded_lattice, distrib_lattice}"
haftmann@44819
   185
begin
haftmann@44819
   186
haftmann@44819
   187
definition
haftmann@44819
   188
  "(inf :: 'a sat \<Rightarrow> 'a sat \<Rightarrow> 'a sat) = min"
haftmann@44819
   189
haftmann@44819
   190
definition
haftmann@44819
   191
  "(sup :: 'a sat \<Rightarrow> 'a sat \<Rightarrow> 'a sat) = max"
haftmann@44819
   192
haftmann@44819
   193
definition
haftmann@44819
   194
  "bot = (0 :: 'a sat)"
haftmann@44819
   195
haftmann@44819
   196
definition
haftmann@44819
   197
  "top = Sat (len_of TYPE('a))"
haftmann@44819
   198
haftmann@44819
   199
instance proof
haftmann@44819
   200
qed (simp_all add: inf_sat_def sup_sat_def bot_sat_def top_sat_def min_max.sup_inf_distrib1,
haftmann@44819
   201
  simp_all add: less_eq_sat_def)
haftmann@44819
   202
haftmann@44819
   203
end
haftmann@44819
   204
haftmann@44819
   205
instantiation sat :: (len) complete_lattice
haftmann@44819
   206
begin
haftmann@44819
   207
haftmann@44819
   208
definition
haftmann@44819
   209
  "Inf (A :: 'a sat set) = fold min top A"
haftmann@44819
   210
haftmann@44819
   211
definition
haftmann@44819
   212
  "Sup (A :: 'a sat set) = fold max bot A"
haftmann@44819
   213
haftmann@44819
   214
instance proof
haftmann@44819
   215
  fix x :: "'a sat"
haftmann@44819
   216
  fix A :: "'a sat set"
haftmann@44819
   217
  note finite
haftmann@44819
   218
  moreover assume "x \<in> A"
haftmann@44819
   219
  ultimately have "fold min top A \<le> min x top" by (rule min_max.fold_inf_le_inf)
haftmann@44819
   220
  then show "Inf A \<le> x" by (simp add: Inf_sat_def)
haftmann@44819
   221
next
haftmann@44819
   222
  fix z :: "'a sat"
haftmann@44819
   223
  fix A :: "'a sat set"
haftmann@44819
   224
  note finite
haftmann@44819
   225
  moreover assume z: "\<And>x. x \<in> A \<Longrightarrow> z \<le> x"
haftmann@44819
   226
  ultimately have "min z top \<le> fold min top A" by (blast intro: min_max.inf_le_fold_inf)
haftmann@44819
   227
  then show "z \<le> Inf A" by (simp add: Inf_sat_def min_def)
haftmann@44819
   228
next
haftmann@44819
   229
  fix x :: "'a sat"
haftmann@44819
   230
  fix A :: "'a sat set"
haftmann@44819
   231
  note finite
haftmann@44819
   232
  moreover assume "x \<in> A"
haftmann@44819
   233
  ultimately have "max x bot \<le> fold max bot A" by (rule min_max.sup_le_fold_sup)
haftmann@44819
   234
  then show "x \<le> Sup A" by (simp add: Sup_sat_def)
haftmann@44819
   235
next
haftmann@44819
   236
  fix z :: "'a sat"
haftmann@44819
   237
  fix A :: "'a sat set"
haftmann@44819
   238
  note finite
haftmann@44819
   239
  moreover assume z: "\<And>x. x \<in> A \<Longrightarrow> x \<le> z"
haftmann@44819
   240
  ultimately have "fold max bot A \<le> max z bot" by (blast intro: min_max.fold_sup_le_sup)
haftmann@44819
   241
  then show "Sup A \<le> z" by (simp add: Sup_sat_def max_def bot_unique)
haftmann@44819
   242
qed
haftmann@44819
   243
haftmann@44819
   244
end
haftmann@44819
   245
haftmann@44819
   246
end