src/HOL/Library/Numeral_Type.thy
changeset 47108 2a1953f0d20d
parent 46868 6c250adbe101
child 48063 f02b4302d5dd
     1.1 --- a/src/HOL/Library/Numeral_Type.thy	Sat Mar 24 16:27:04 2012 +0100
     1.2 +++ b/src/HOL/Library/Numeral_Type.thy	Sun Mar 25 20:15:39 2012 +0200
     1.3 @@ -66,7 +66,6 @@
     1.4      by simp
     1.5  qed
     1.6  
     1.7 -
     1.8  subsection {* Locales for for modular arithmetic subtypes *}
     1.9  
    1.10  locale mod_type =
    1.11 @@ -137,8 +136,8 @@
    1.12  
    1.13  locale mod_ring = mod_type n Rep Abs
    1.14    for n :: int
    1.15 -  and Rep :: "'a::{number_ring} \<Rightarrow> int"
    1.16 -  and Abs :: "int \<Rightarrow> 'a::{number_ring}"
    1.17 +  and Rep :: "'a::{comm_ring_1} \<Rightarrow> int"
    1.18 +  and Abs :: "int \<Rightarrow> 'a::{comm_ring_1}"
    1.19  begin
    1.20  
    1.21  lemma of_nat_eq: "of_nat k = Abs (int k mod n)"
    1.22 @@ -152,13 +151,14 @@
    1.23  apply (simp add: Rep_simps of_nat_eq diff_def zmod_simps)
    1.24  done
    1.25  
    1.26 -lemma Rep_number_of:
    1.27 -  "Rep (number_of w) = number_of w mod n"
    1.28 -by (simp add: number_of_eq of_int_eq Rep_Abs_mod)
    1.29 +lemma Rep_numeral:
    1.30 +  "Rep (numeral w) = numeral w mod n"
    1.31 +using of_int_eq [of "numeral w"]
    1.32 +by (simp add: Rep_inject_sym Rep_Abs_mod)
    1.33  
    1.34 -lemma iszero_number_of:
    1.35 -  "iszero (number_of w::'a) \<longleftrightarrow> number_of w mod n = 0"
    1.36 -by (simp add: Rep_simps number_of_eq of_int_eq iszero_def zero_def)
    1.37 +lemma iszero_numeral:
    1.38 +  "iszero (numeral w::'a) \<longleftrightarrow> numeral w mod n = 0"
    1.39 +by (simp add: Rep_inject_sym Rep_numeral Rep_0 iszero_def)
    1.40  
    1.41  lemma cases:
    1.42    assumes 1: "\<And>z. \<lbrakk>(x::'a) = of_int z; 0 \<le> z; z < n\<rbrakk> \<Longrightarrow> P"
    1.43 @@ -175,14 +175,14 @@
    1.44  end
    1.45  
    1.46  
    1.47 -subsection {* Number ring instances *}
    1.48 +subsection {* Ring class instances *}
    1.49  
    1.50  text {*
    1.51 -  Unfortunately a number ring instance is not possible for
    1.52 +  Unfortunately @{text ring_1} instance is not possible for
    1.53    @{typ num1}, since 0 and 1 are not distinct.
    1.54  *}
    1.55  
    1.56 -instantiation num1 :: "{comm_ring,comm_monoid_mult,number}"
    1.57 +instantiation num1 :: "{comm_ring,comm_monoid_mult,numeral}"
    1.58  begin
    1.59  
    1.60  lemma num1_eq_iff: "(x::num1) = (y::num1) \<longleftrightarrow> True"
    1.61 @@ -252,22 +252,10 @@
    1.62  done
    1.63  
    1.64  instance bit0 :: (finite) comm_ring_1
    1.65 -  by (rule bit0.comm_ring_1)+
    1.66 +  by (rule bit0.comm_ring_1)
    1.67  
    1.68  instance bit1 :: (finite) comm_ring_1
    1.69 -  by (rule bit1.comm_ring_1)+
    1.70 -
    1.71 -instantiation bit0 and bit1 :: (finite) number_ring
    1.72 -begin
    1.73 -
    1.74 -definition "(number_of w :: _ bit0) = of_int w"
    1.75 -
    1.76 -definition "(number_of w :: _ bit1) = of_int w"
    1.77 -
    1.78 -instance proof
    1.79 -qed (rule number_of_bit0_def number_of_bit1_def)+
    1.80 -
    1.81 -end
    1.82 +  by (rule bit1.comm_ring_1)
    1.83  
    1.84  interpretation bit0:
    1.85    mod_ring "int CARD('a::finite bit0)"
    1.86 @@ -289,9 +277,11 @@
    1.87  lemmas bit0_induct [case_names of_int, induct type: bit0] = bit0.induct
    1.88  lemmas bit1_induct [case_names of_int, induct type: bit1] = bit1.induct
    1.89  
    1.90 -lemmas bit0_iszero_number_of [simp] = bit0.iszero_number_of
    1.91 -lemmas bit1_iszero_number_of [simp] = bit1.iszero_number_of
    1.92 +lemmas bit0_iszero_numeral [simp] = bit0.iszero_numeral
    1.93 +lemmas bit1_iszero_numeral [simp] = bit1.iszero_numeral
    1.94  
    1.95 +declare eq_numeral_iff_iszero [where 'a="('a::finite) bit0", standard, simp]
    1.96 +declare eq_numeral_iff_iszero [where 'a="('a::finite) bit1", standard, simp]
    1.97  
    1.98  subsection {* Syntax *}
    1.99