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