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