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