src/HOL/Library/Saturated.thy
author haftmann
Wed Jul 18 20:51:21 2018 +0200 (11 months ago)
changeset 68658 16cc1161ad7f
parent 63762 6920b1885eff
child 70185 ac1706cdde25
permissions -rw-r--r--
tuned equation
     1 (*  Title:      HOL/Library/Saturated.thy
     2     Author:     Brian Huffman
     3     Author:     Peter Gammie
     4     Author:     Florian Haftmann
     5 *)
     6 
     7 section \<open>Saturated arithmetic\<close>
     8 
     9 theory Saturated
    10 imports Numeral_Type Type_Length
    11 begin
    12 
    13 subsection \<open>The type of saturated naturals\<close>
    14 
    15 typedef (overloaded) ('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.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.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 standard
    65     (auto simp add: less_eq_sat_def less_sat_def not_le sat_eq_iff min.coboundedI1 mult.commute)
    66 
    67 end
    68 
    69 instantiation sat :: (len) "{minus, comm_semiring_1}"
    70 begin
    71 
    72 definition
    73   "0 = Abs_sat' 0"
    74 
    75 definition
    76   "1 = Abs_sat' 1"
    77 
    78 lemma nat_of_zero_sat [simp, code abstract]:
    79   "nat_of 0 = 0"
    80   by (simp add: zero_sat_def)
    81 
    82 lemma nat_of_one_sat [simp, code abstract]:
    83   "nat_of 1 = min 1 (len_of TYPE('a))"
    84   by (simp add: one_sat_def)
    85 
    86 definition
    87   "x + y = Abs_sat' (nat_of x + nat_of y)"
    88 
    89 lemma nat_of_plus_sat [simp, code abstract]:
    90   "nat_of (x + y) = min (nat_of x + nat_of y) (len_of TYPE('a))"
    91   by (simp add: plus_sat_def)
    92 
    93 definition
    94   "x - y = Abs_sat' (nat_of x - nat_of y)"
    95 
    96 lemma nat_of_minus_sat [simp, code abstract]:
    97   "nat_of (x - y) = nat_of x - nat_of y"
    98 proof -
    99   from nat_of_le_len_of [of x] have "nat_of x - nat_of y \<le> len_of TYPE('a)" by arith
   100   then show ?thesis by (simp add: minus_sat_def)
   101 qed
   102 
   103 definition
   104   "x * y = Abs_sat' (nat_of x * nat_of y)"
   105 
   106 lemma nat_of_times_sat [simp, code abstract]:
   107   "nat_of (x * y) = min (nat_of x * nat_of y) (len_of TYPE('a))"
   108   by (simp add: times_sat_def)
   109 
   110 instance
   111 proof
   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
   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 standard
   145     (auto simp add: less_eq_sat_def less_sat_def not_le sat_eq_iff min.coboundedI1 mult.commute)
   146 
   147 end
   148 
   149 lemma Abs_sat'_eq_of_nat: "Abs_sat' n = of_nat n"
   150   by (rule sat_eqI, induct n, simp_all)
   151 
   152 abbreviation Sat :: "nat \<Rightarrow> 'a::len sat" where
   153   "Sat \<equiv> of_nat"
   154 
   155 lemma nat_of_Sat [simp]:
   156   "nat_of (Sat n :: ('a::len) sat) = min (len_of TYPE('a)) n"
   157   by (rule nat_of_Abs_sat' [unfolded Abs_sat'_eq_of_nat])
   158 
   159 lemma [code_abbrev]:
   160   "of_nat (numeral k) = (numeral k :: 'a::len sat)"
   161   by simp
   162 
   163 context
   164 begin
   165 
   166 qualified definition sat_of_nat :: "nat \<Rightarrow> ('a::len) sat"
   167   where [code_abbrev]: "sat_of_nat = of_nat"
   168 
   169 lemma [code abstract]:
   170   "nat_of (sat_of_nat n :: ('a::len) sat) = min (len_of TYPE('a)) n"
   171   by (simp add: sat_of_nat_def)
   172 
   173 end
   174 
   175 instance sat :: (len) finite
   176 proof
   177   show "finite (UNIV::'a sat set)"
   178     unfolding type_definition.univ [OF type_definition_sat]
   179     using finite by simp
   180 qed
   181 
   182 instantiation sat :: (len) equal
   183 begin
   184 
   185 definition "HOL.equal A B \<longleftrightarrow> nat_of A = nat_of B"
   186 
   187 instance
   188   by standard (simp add: equal_sat_def nat_of_inject)
   189 
   190 end
   191 
   192 instantiation sat :: (len) "{bounded_lattice, distrib_lattice}"
   193 begin
   194 
   195 definition "(inf :: 'a sat \<Rightarrow> 'a sat \<Rightarrow> 'a sat) = min"
   196 definition "(sup :: 'a sat \<Rightarrow> 'a sat \<Rightarrow> 'a sat) = max"
   197 definition "bot = (0 :: 'a sat)"
   198 definition "top = Sat (len_of TYPE('a))"
   199 
   200 instance
   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 
   205 end
   206 
   207 instantiation sat :: (len) "{Inf, Sup}"
   208 begin
   209 
   210 definition "Inf = (semilattice_neutr_set.F min top :: 'a sat set \<Rightarrow> 'a sat)"
   211 definition "Sup = (semilattice_neutr_set.F max bot :: 'a sat set \<Rightarrow> 'a sat)"
   212 
   213 instance ..
   214 
   215 end
   216 
   217 interpretation Inf_sat: semilattice_neutr_set min "top :: 'a::len sat"
   218   rewrites "semilattice_neutr_set.F min (top :: 'a sat) = Inf"
   219 proof -
   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)
   224 qed
   225 
   226 interpretation Sup_sat: semilattice_neutr_set max "bot :: 'a::len sat"
   227   rewrites "semilattice_neutr_set.F max (bot :: 'a sat) = Sup"
   228 proof -
   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)
   233 qed
   234 
   235 instance sat :: (len) complete_lattice
   236 proof 
   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)
   243 next
   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
   249 next
   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)
   256 next
   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
   262 next
   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)
   267 qed
   268 
   269 end