src/HOL/Library/Saturated.thy
changeset 44819 fe33d6655186
child 44848 f4d0b060c7ca
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Saturated.thy	Wed Sep 07 23:55:40 2011 +0200
     1.3 @@ -0,0 +1,242 @@
     1.4 +(* Author: Brian Huffman *)
     1.5 +(* Author: Peter Gammie *)
     1.6 +(* Author: Florian Haftmann *)
     1.7 +
     1.8 +header {* Saturated arithmetic *}
     1.9 +
    1.10 +theory Saturated
    1.11 +imports Main "~~/src/HOL/Library/Numeral_Type" "~~/src/HOL/Word/Type_Length"
    1.12 +begin
    1.13 +
    1.14 +subsection {* The type of saturated naturals *}
    1.15 +
    1.16 +typedef (open) ('a::len) sat = "{.. len_of TYPE('a)}"
    1.17 +  morphisms nat_of Abs_sat
    1.18 +  by auto
    1.19 +
    1.20 +lemma sat_eqI:
    1.21 +  "nat_of m = nat_of n \<Longrightarrow> m = n"
    1.22 +  by (simp add: nat_of_inject)
    1.23 +
    1.24 +lemma sat_eq_iff:
    1.25 +  "m = n \<longleftrightarrow> nat_of m = nat_of n"
    1.26 +  by (simp add: nat_of_inject)
    1.27 +
    1.28 +lemma Abs_sa_nat_of [code abstype]:
    1.29 +  "Abs_sat (nat_of n) = n"
    1.30 +  by (fact nat_of_inverse)
    1.31 +
    1.32 +definition Sat :: "nat \<Rightarrow> 'a::len sat" where
    1.33 +  "Sat n = Abs_sat (min (len_of TYPE('a)) n)"
    1.34 +
    1.35 +lemma nat_of_Sat [simp]:
    1.36 +  "nat_of (Sat n :: ('a::len) sat) = min (len_of TYPE('a)) n"
    1.37 +  unfolding Sat_def by (rule Abs_sat_inverse) simp
    1.38 +
    1.39 +lemma nat_of_le_len_of [simp]:
    1.40 +  "nat_of (n :: ('a::len) sat) \<le> len_of TYPE('a)"
    1.41 +  using nat_of [where x = n] by simp
    1.42 +
    1.43 +lemma min_len_of_nat_of [simp]:
    1.44 +  "min (len_of TYPE('a)) (nat_of (n::('a::len) sat)) = nat_of n"
    1.45 +  by (rule min_max.inf_absorb2 [OF nat_of_le_len_of])
    1.46 +
    1.47 +lemma min_nat_of_len_of [simp]:
    1.48 +  "min (nat_of (n::('a::len) sat)) (len_of TYPE('a)) = nat_of n"
    1.49 +  by (subst min_max.inf.commute) simp
    1.50 +
    1.51 +lemma Sat_nat_of [simp]:
    1.52 +  "Sat (nat_of n) = n"
    1.53 +  by (simp add: Sat_def nat_of_inverse)
    1.54 +
    1.55 +instantiation sat :: (len) linorder
    1.56 +begin
    1.57 +
    1.58 +definition
    1.59 +  less_eq_sat_def: "x \<le> y \<longleftrightarrow> nat_of x \<le> nat_of y"
    1.60 +
    1.61 +definition
    1.62 +  less_sat_def: "x < y \<longleftrightarrow> nat_of x < nat_of y"
    1.63 +
    1.64 +instance
    1.65 +by default (auto simp add: less_eq_sat_def less_sat_def not_le sat_eq_iff min_max.le_infI1 nat_mult_commute)
    1.66 +
    1.67 +end
    1.68 +
    1.69 +instantiation sat :: (len) "{minus, comm_semiring_0, comm_semiring_1}"
    1.70 +begin
    1.71 +
    1.72 +definition
    1.73 +  "0 = Sat 0"
    1.74 +
    1.75 +definition
    1.76 +  "1 = Sat 1"
    1.77 +
    1.78 +lemma nat_of_zero_sat [simp, code abstract]:
    1.79 +  "nat_of 0 = 0"
    1.80 +  by (simp add: zero_sat_def)
    1.81 +
    1.82 +lemma nat_of_one_sat [simp, code abstract]:
    1.83 +  "nat_of 1 = min 1 (len_of TYPE('a))"
    1.84 +  by (simp add: one_sat_def)
    1.85 +
    1.86 +definition
    1.87 +  "x + y = Sat (nat_of x + nat_of y)"
    1.88 +
    1.89 +lemma nat_of_plus_sat [simp, code abstract]:
    1.90 +  "nat_of (x + y) = min (nat_of x + nat_of y) (len_of TYPE('a))"
    1.91 +  by (simp add: plus_sat_def)
    1.92 +
    1.93 +definition
    1.94 +  "x - y = Sat (nat_of x - nat_of y)"
    1.95 +
    1.96 +lemma nat_of_minus_sat [simp, code abstract]:
    1.97 +  "nat_of (x - y) = nat_of x - nat_of y"
    1.98 +proof -
    1.99 +  from nat_of_le_len_of [of x] have "nat_of x - nat_of y \<le> len_of TYPE('a)" by arith
   1.100 +  then show ?thesis by (simp add: minus_sat_def)
   1.101 +qed
   1.102 +
   1.103 +definition
   1.104 +  "x * y = Sat (nat_of x * nat_of y)"
   1.105 +
   1.106 +lemma nat_of_times_sat [simp, code abstract]:
   1.107 +  "nat_of (x * y) = min (nat_of x * nat_of y) (len_of TYPE('a))"
   1.108 +  by (simp add: times_sat_def)
   1.109 +
   1.110 +instance proof
   1.111 +  fix a b c :: "('a::len) sat"
   1.112 +  show "a * b * c = a * (b * c)"
   1.113 +  proof(cases "a = 0")
   1.114 +    case True thus ?thesis by (simp add: sat_eq_iff)
   1.115 +  next
   1.116 +    case False show ?thesis
   1.117 +    proof(cases "c = 0")
   1.118 +      case True thus ?thesis by (simp add: sat_eq_iff)
   1.119 +    next
   1.120 +      case False with `a \<noteq> 0` show ?thesis
   1.121 +        by (simp add: sat_eq_iff nat_mult_min_left nat_mult_min_right mult_assoc min_max.inf_assoc min_max.inf_absorb2)
   1.122 +    qed
   1.123 +  qed
   1.124 +next
   1.125 +  fix a :: "('a::len) sat"
   1.126 +  show "1 * a = a"
   1.127 +    apply (simp add: sat_eq_iff)
   1.128 +    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)
   1.129 +    done
   1.130 +next
   1.131 +  fix a b c :: "('a::len) sat"
   1.132 +  show "(a + b) * c = a * c + b * c"
   1.133 +  proof(cases "c = 0")
   1.134 +    case True thus ?thesis by (simp add: sat_eq_iff)
   1.135 +  next
   1.136 +    case False thus ?thesis
   1.137 +      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)
   1.138 +  qed
   1.139 +qed (simp_all add: sat_eq_iff mult.commute)
   1.140 +
   1.141 +end
   1.142 +
   1.143 +instantiation sat :: (len) ordered_comm_semiring
   1.144 +begin
   1.145 +
   1.146 +instance
   1.147 +by default (auto simp add: less_eq_sat_def less_sat_def not_le sat_eq_iff min_max.le_infI1 nat_mult_commute)
   1.148 +
   1.149 +end
   1.150 +
   1.151 +instantiation sat :: (len) number
   1.152 +begin
   1.153 +
   1.154 +definition
   1.155 +  number_of_sat_def [code del]: "number_of = Sat \<circ> nat"
   1.156 +
   1.157 +instance ..
   1.158 +
   1.159 +end
   1.160 +
   1.161 +lemma [code abstract]:
   1.162 +  "nat_of (number_of n :: ('a::len) sat) = min (nat n) (len_of TYPE('a))"
   1.163 +  unfolding number_of_sat_def by simp
   1.164 +
   1.165 +instance sat :: (len) finite
   1.166 +proof
   1.167 +  show "finite (UNIV::'a sat set)"
   1.168 +    unfolding type_definition.univ [OF type_definition_sat]
   1.169 +    using finite by simp
   1.170 +qed
   1.171 +
   1.172 +instantiation sat :: (len) equal
   1.173 +begin
   1.174 +
   1.175 +definition
   1.176 +  "HOL.equal A B \<longleftrightarrow> nat_of A = nat_of B"
   1.177 +
   1.178 +instance proof
   1.179 +qed (simp add: equal_sat_def nat_of_inject)
   1.180 +
   1.181 +end
   1.182 +
   1.183 +instantiation sat :: (len) "{bounded_lattice, distrib_lattice}"
   1.184 +begin
   1.185 +
   1.186 +definition
   1.187 +  "(inf :: 'a sat \<Rightarrow> 'a sat \<Rightarrow> 'a sat) = min"
   1.188 +
   1.189 +definition
   1.190 +  "(sup :: 'a sat \<Rightarrow> 'a sat \<Rightarrow> 'a sat) = max"
   1.191 +
   1.192 +definition
   1.193 +  "bot = (0 :: 'a sat)"
   1.194 +
   1.195 +definition
   1.196 +  "top = Sat (len_of TYPE('a))"
   1.197 +
   1.198 +instance proof
   1.199 +qed (simp_all add: inf_sat_def sup_sat_def bot_sat_def top_sat_def min_max.sup_inf_distrib1,
   1.200 +  simp_all add: less_eq_sat_def)
   1.201 +
   1.202 +end
   1.203 +
   1.204 +instantiation sat :: (len) complete_lattice
   1.205 +begin
   1.206 +
   1.207 +definition
   1.208 +  "Inf (A :: 'a sat set) = fold min top A"
   1.209 +
   1.210 +definition
   1.211 +  "Sup (A :: 'a sat set) = fold max bot A"
   1.212 +
   1.213 +instance proof
   1.214 +  fix x :: "'a sat"
   1.215 +  fix A :: "'a sat set"
   1.216 +  note finite
   1.217 +  moreover assume "x \<in> A"
   1.218 +  ultimately have "fold min top A \<le> min x top" by (rule min_max.fold_inf_le_inf)
   1.219 +  then show "Inf A \<le> x" by (simp add: Inf_sat_def)
   1.220 +next
   1.221 +  fix z :: "'a sat"
   1.222 +  fix A :: "'a sat set"
   1.223 +  note finite
   1.224 +  moreover assume z: "\<And>x. x \<in> A \<Longrightarrow> z \<le> x"
   1.225 +  ultimately have "min z top \<le> fold min top A" by (blast intro: min_max.inf_le_fold_inf)
   1.226 +  then show "z \<le> Inf A" by (simp add: Inf_sat_def min_def)
   1.227 +next
   1.228 +  fix x :: "'a sat"
   1.229 +  fix A :: "'a sat set"
   1.230 +  note finite
   1.231 +  moreover assume "x \<in> A"
   1.232 +  ultimately have "max x bot \<le> fold max bot A" by (rule min_max.sup_le_fold_sup)
   1.233 +  then show "x \<le> Sup A" by (simp add: Sup_sat_def)
   1.234 +next
   1.235 +  fix z :: "'a sat"
   1.236 +  fix A :: "'a sat set"
   1.237 +  note finite
   1.238 +  moreover assume z: "\<And>x. x \<in> A \<Longrightarrow> x \<le> z"
   1.239 +  ultimately have "fold max bot A \<le> max z bot" by (blast intro: min_max.fold_sup_le_sup)
   1.240 +  then show "Sup A \<le> z" by (simp add: Sup_sat_def max_def bot_unique)
   1.241 +qed
   1.242 +
   1.243 +end
   1.244 +
   1.245 +end