src/HOL/Library/Numeral_Type.thy
changeset 47108 2a1953f0d20d
parent 46868 6c250adbe101
child 48063 f02b4302d5dd
equal deleted inserted replaced
47107:35807a5d8dc2 47108:2a1953f0d20d
    63     unfolding type_definition.univ [OF type_definition_bit1]
    63     unfolding type_definition.univ [OF type_definition_bit1]
    64     by simp
    64     by simp
    65   show "2 \<le> CARD('a bit1)"
    65   show "2 \<le> CARD('a bit1)"
    66     by simp
    66     by simp
    67 qed
    67 qed
    68 
       
    69 
    68 
    70 subsection {* Locales for for modular arithmetic subtypes *}
    69 subsection {* Locales for for modular arithmetic subtypes *}
    71 
    70 
    72 locale mod_type =
    71 locale mod_type =
    73   fixes n :: int
    72   fixes n :: int
   135 
   134 
   136 end
   135 end
   137 
   136 
   138 locale mod_ring = mod_type n Rep Abs
   137 locale mod_ring = mod_type n Rep Abs
   139   for n :: int
   138   for n :: int
   140   and Rep :: "'a::{number_ring} \<Rightarrow> int"
   139   and Rep :: "'a::{comm_ring_1} \<Rightarrow> int"
   141   and Abs :: "int \<Rightarrow> 'a::{number_ring}"
   140   and Abs :: "int \<Rightarrow> 'a::{comm_ring_1}"
   142 begin
   141 begin
   143 
   142 
   144 lemma of_nat_eq: "of_nat k = Abs (int k mod n)"
   143 lemma of_nat_eq: "of_nat k = Abs (int k mod n)"
   145 apply (induct k)
   144 apply (induct k)
   146 apply (simp add: zero_def)
   145 apply (simp add: zero_def)
   150 lemma of_int_eq: "of_int z = Abs (z mod n)"
   149 lemma of_int_eq: "of_int z = Abs (z mod n)"
   151 apply (cases z rule: int_diff_cases)
   150 apply (cases z rule: int_diff_cases)
   152 apply (simp add: Rep_simps of_nat_eq diff_def zmod_simps)
   151 apply (simp add: Rep_simps of_nat_eq diff_def zmod_simps)
   153 done
   152 done
   154 
   153 
   155 lemma Rep_number_of:
   154 lemma Rep_numeral:
   156   "Rep (number_of w) = number_of w mod n"
   155   "Rep (numeral w) = numeral w mod n"
   157 by (simp add: number_of_eq of_int_eq Rep_Abs_mod)
   156 using of_int_eq [of "numeral w"]
   158 
   157 by (simp add: Rep_inject_sym Rep_Abs_mod)
   159 lemma iszero_number_of:
   158 
   160   "iszero (number_of w::'a) \<longleftrightarrow> number_of w mod n = 0"
   159 lemma iszero_numeral:
   161 by (simp add: Rep_simps number_of_eq of_int_eq iszero_def zero_def)
   160   "iszero (numeral w::'a) \<longleftrightarrow> numeral w mod n = 0"
       
   161 by (simp add: Rep_inject_sym Rep_numeral Rep_0 iszero_def)
   162 
   162 
   163 lemma cases:
   163 lemma cases:
   164   assumes 1: "\<And>z. \<lbrakk>(x::'a) = of_int z; 0 \<le> z; z < n\<rbrakk> \<Longrightarrow> P"
   164   assumes 1: "\<And>z. \<lbrakk>(x::'a) = of_int z; 0 \<le> z; z < n\<rbrakk> \<Longrightarrow> P"
   165   shows "P"
   165   shows "P"
   166 apply (cases x rule: type_definition.Abs_cases [OF type])
   166 apply (cases x rule: type_definition.Abs_cases [OF type])
   173 by (cases x rule: cases) simp
   173 by (cases x rule: cases) simp
   174 
   174 
   175 end
   175 end
   176 
   176 
   177 
   177 
   178 subsection {* Number ring instances *}
   178 subsection {* Ring class instances *}
   179 
   179 
   180 text {*
   180 text {*
   181   Unfortunately a number ring instance is not possible for
   181   Unfortunately @{text ring_1} instance is not possible for
   182   @{typ num1}, since 0 and 1 are not distinct.
   182   @{typ num1}, since 0 and 1 are not distinct.
   183 *}
   183 *}
   184 
   184 
   185 instantiation num1 :: "{comm_ring,comm_monoid_mult,number}"
   185 instantiation num1 :: "{comm_ring,comm_monoid_mult,numeral}"
   186 begin
   186 begin
   187 
   187 
   188 lemma num1_eq_iff: "(x::num1) = (y::num1) \<longleftrightarrow> True"
   188 lemma num1_eq_iff: "(x::num1) = (y::num1) \<longleftrightarrow> True"
   189   by (induct x, induct y) simp
   189   by (induct x, induct y) simp
   190 
   190 
   250 apply (rule minus_bit1_def [unfolded Abs_bit1'_def])
   250 apply (rule minus_bit1_def [unfolded Abs_bit1'_def])
   251 apply (rule uminus_bit1_def [unfolded Abs_bit1'_def])
   251 apply (rule uminus_bit1_def [unfolded Abs_bit1'_def])
   252 done
   252 done
   253 
   253 
   254 instance bit0 :: (finite) comm_ring_1
   254 instance bit0 :: (finite) comm_ring_1
   255   by (rule bit0.comm_ring_1)+
   255   by (rule bit0.comm_ring_1)
   256 
   256 
   257 instance bit1 :: (finite) comm_ring_1
   257 instance bit1 :: (finite) comm_ring_1
   258   by (rule bit1.comm_ring_1)+
   258   by (rule bit1.comm_ring_1)
   259 
       
   260 instantiation bit0 and bit1 :: (finite) number_ring
       
   261 begin
       
   262 
       
   263 definition "(number_of w :: _ bit0) = of_int w"
       
   264 
       
   265 definition "(number_of w :: _ bit1) = of_int w"
       
   266 
       
   267 instance proof
       
   268 qed (rule number_of_bit0_def number_of_bit1_def)+
       
   269 
       
   270 end
       
   271 
   259 
   272 interpretation bit0:
   260 interpretation bit0:
   273   mod_ring "int CARD('a::finite bit0)"
   261   mod_ring "int CARD('a::finite bit0)"
   274            "Rep_bit0 :: 'a::finite bit0 \<Rightarrow> int"
   262            "Rep_bit0 :: 'a::finite bit0 \<Rightarrow> int"
   275            "Abs_bit0 :: int \<Rightarrow> 'a::finite bit0"
   263            "Abs_bit0 :: int \<Rightarrow> 'a::finite bit0"
   287 lemmas bit1_cases [case_names of_int, cases type: bit1] = bit1.cases
   275 lemmas bit1_cases [case_names of_int, cases type: bit1] = bit1.cases
   288 
   276 
   289 lemmas bit0_induct [case_names of_int, induct type: bit0] = bit0.induct
   277 lemmas bit0_induct [case_names of_int, induct type: bit0] = bit0.induct
   290 lemmas bit1_induct [case_names of_int, induct type: bit1] = bit1.induct
   278 lemmas bit1_induct [case_names of_int, induct type: bit1] = bit1.induct
   291 
   279 
   292 lemmas bit0_iszero_number_of [simp] = bit0.iszero_number_of
   280 lemmas bit0_iszero_numeral [simp] = bit0.iszero_numeral
   293 lemmas bit1_iszero_number_of [simp] = bit1.iszero_number_of
   281 lemmas bit1_iszero_numeral [simp] = bit1.iszero_numeral
   294 
   282 
       
   283 declare eq_numeral_iff_iszero [where 'a="('a::finite) bit0", standard, simp]
       
   284 declare eq_numeral_iff_iszero [where 'a="('a::finite) bit1", standard, simp]
   295 
   285 
   296 subsection {* Syntax *}
   286 subsection {* Syntax *}
   297 
   287 
   298 syntax
   288 syntax
   299   "_NumeralType" :: "num_token => type"  ("_")
   289   "_NumeralType" :: "num_token => type"  ("_")