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