src/HOL/Library/Saturated.thy
author haftmann
Wed Sep 07 23:55:40 2011 +0200 (2011-09-07)
changeset 44819 fe33d6655186
child 44848 f4d0b060c7ca
permissions -rw-r--r--
theory of saturated naturals contributed by Peter Gammie
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
haftmann@44819
    66
instantiation sat :: (len) "{minus, comm_semiring_0, 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
haftmann@44819
   134
      by (simp add: sat_eq_iff nat_mult_min_left add_mult_distrib nat_add_min_left nat_add_min_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
haftmann@44819
   148
instantiation sat :: (len) number
haftmann@44819
   149
begin
haftmann@44819
   150
haftmann@44819
   151
definition
haftmann@44819
   152
  number_of_sat_def [code del]: "number_of = Sat \<circ> nat"
haftmann@44819
   153
haftmann@44819
   154
instance ..
haftmann@44819
   155
haftmann@44819
   156
end
haftmann@44819
   157
haftmann@44819
   158
lemma [code abstract]:
haftmann@44819
   159
  "nat_of (number_of n :: ('a::len) sat) = min (nat n) (len_of TYPE('a))"
haftmann@44819
   160
  unfolding number_of_sat_def by simp
haftmann@44819
   161
haftmann@44819
   162
instance sat :: (len) finite
haftmann@44819
   163
proof
haftmann@44819
   164
  show "finite (UNIV::'a sat set)"
haftmann@44819
   165
    unfolding type_definition.univ [OF type_definition_sat]
haftmann@44819
   166
    using finite by simp
haftmann@44819
   167
qed
haftmann@44819
   168
haftmann@44819
   169
instantiation sat :: (len) equal
haftmann@44819
   170
begin
haftmann@44819
   171
haftmann@44819
   172
definition
haftmann@44819
   173
  "HOL.equal A B \<longleftrightarrow> nat_of A = nat_of B"
haftmann@44819
   174
haftmann@44819
   175
instance proof
haftmann@44819
   176
qed (simp add: equal_sat_def nat_of_inject)
haftmann@44819
   177
haftmann@44819
   178
end
haftmann@44819
   179
haftmann@44819
   180
instantiation sat :: (len) "{bounded_lattice, distrib_lattice}"
haftmann@44819
   181
begin
haftmann@44819
   182
haftmann@44819
   183
definition
haftmann@44819
   184
  "(inf :: 'a sat \<Rightarrow> 'a sat \<Rightarrow> 'a sat) = min"
haftmann@44819
   185
haftmann@44819
   186
definition
haftmann@44819
   187
  "(sup :: 'a sat \<Rightarrow> 'a sat \<Rightarrow> 'a sat) = max"
haftmann@44819
   188
haftmann@44819
   189
definition
haftmann@44819
   190
  "bot = (0 :: 'a sat)"
haftmann@44819
   191
haftmann@44819
   192
definition
haftmann@44819
   193
  "top = Sat (len_of TYPE('a))"
haftmann@44819
   194
haftmann@44819
   195
instance proof
haftmann@44819
   196
qed (simp_all add: inf_sat_def sup_sat_def bot_sat_def top_sat_def min_max.sup_inf_distrib1,
haftmann@44819
   197
  simp_all add: less_eq_sat_def)
haftmann@44819
   198
haftmann@44819
   199
end
haftmann@44819
   200
haftmann@44819
   201
instantiation sat :: (len) complete_lattice
haftmann@44819
   202
begin
haftmann@44819
   203
haftmann@44819
   204
definition
haftmann@44819
   205
  "Inf (A :: 'a sat set) = fold min top A"
haftmann@44819
   206
haftmann@44819
   207
definition
haftmann@44819
   208
  "Sup (A :: 'a sat set) = fold max bot A"
haftmann@44819
   209
haftmann@44819
   210
instance proof
haftmann@44819
   211
  fix x :: "'a sat"
haftmann@44819
   212
  fix A :: "'a sat set"
haftmann@44819
   213
  note finite
haftmann@44819
   214
  moreover assume "x \<in> A"
haftmann@44819
   215
  ultimately have "fold min top A \<le> min x top" by (rule min_max.fold_inf_le_inf)
haftmann@44819
   216
  then show "Inf A \<le> x" by (simp add: Inf_sat_def)
haftmann@44819
   217
next
haftmann@44819
   218
  fix z :: "'a sat"
haftmann@44819
   219
  fix A :: "'a sat set"
haftmann@44819
   220
  note finite
haftmann@44819
   221
  moreover assume z: "\<And>x. x \<in> A \<Longrightarrow> z \<le> x"
haftmann@44819
   222
  ultimately have "min z top \<le> fold min top A" by (blast intro: min_max.inf_le_fold_inf)
haftmann@44819
   223
  then show "z \<le> Inf A" by (simp add: Inf_sat_def min_def)
haftmann@44819
   224
next
haftmann@44819
   225
  fix x :: "'a sat"
haftmann@44819
   226
  fix A :: "'a sat set"
haftmann@44819
   227
  note finite
haftmann@44819
   228
  moreover assume "x \<in> A"
haftmann@44819
   229
  ultimately have "max x bot \<le> fold max bot A" by (rule min_max.sup_le_fold_sup)
haftmann@44819
   230
  then show "x \<le> Sup A" by (simp add: Sup_sat_def)
haftmann@44819
   231
next
haftmann@44819
   232
  fix z :: "'a sat"
haftmann@44819
   233
  fix A :: "'a sat set"
haftmann@44819
   234
  note finite
haftmann@44819
   235
  moreover assume z: "\<And>x. x \<in> A \<Longrightarrow> x \<le> z"
haftmann@44819
   236
  ultimately have "fold max bot A \<le> max z bot" by (blast intro: min_max.fold_sup_le_sup)
haftmann@44819
   237
  then show "Sup A \<le> z" by (simp add: Sup_sat_def max_def bot_unique)
haftmann@44819
   238
qed
haftmann@44819
   239
haftmann@44819
   240
end
haftmann@44819
   241
haftmann@44819
   242
end