src/HOL/Library/Numeral_Type.thy
changeset 30960 fec1a04b7220
parent 30729 461ee3e49ad3
child 31021 53642251a04f
     1.1 --- a/src/HOL/Library/Numeral_Type.thy	Wed Apr 22 19:09:19 2009 +0200
     1.2 +++ b/src/HOL/Library/Numeral_Type.thy	Wed Apr 22 19:09:21 2009 +0200
     1.3 @@ -154,8 +154,8 @@
     1.4  
     1.5  locale mod_type =
     1.6    fixes n :: int
     1.7 -  and Rep :: "'a::{zero,one,plus,times,uminus,minus,power} \<Rightarrow> int"
     1.8 -  and Abs :: "int \<Rightarrow> 'a::{zero,one,plus,times,uminus,minus,power}"
     1.9 +  and Rep :: "'a::{zero,one,plus,times,uminus,minus} \<Rightarrow> int"
    1.10 +  and Abs :: "int \<Rightarrow> 'a::{zero,one,plus,times,uminus,minus}"
    1.11    assumes type: "type_definition Rep Abs {0..<n}"
    1.12    and size1: "1 < n"
    1.13    and zero_def: "0 = Abs 0"
    1.14 @@ -164,14 +164,13 @@
    1.15    and mult_def: "x * y = Abs ((Rep x * Rep y) mod n)"
    1.16    and diff_def: "x - y = Abs ((Rep x - Rep y) mod n)"
    1.17    and minus_def: "- x = Abs ((- Rep x) mod n)"
    1.18 -  and power_def: "x ^ k = Abs (Rep x ^ k mod n)"
    1.19  begin
    1.20  
    1.21  lemma size0: "0 < n"
    1.22  by (cut_tac size1, simp)
    1.23  
    1.24  lemmas definitions =
    1.25 -  zero_def one_def add_def mult_def minus_def diff_def power_def
    1.26 +  zero_def one_def add_def mult_def minus_def diff_def
    1.27  
    1.28  lemma Rep_less_n: "Rep x < n"
    1.29  by (rule type_definition.Rep [OF type, simplified, THEN conjunct2])
    1.30 @@ -227,8 +226,8 @@
    1.31  
    1.32  locale mod_ring = mod_type +
    1.33    constrains n :: int
    1.34 -  and Rep :: "'a::{number_ring,power} \<Rightarrow> int"
    1.35 -  and Abs :: "int \<Rightarrow> 'a::{number_ring,power}"
    1.36 +  and Rep :: "'a::{number_ring} \<Rightarrow> int"
    1.37 +  and Abs :: "int \<Rightarrow> 'a::{number_ring}"
    1.38  begin
    1.39  
    1.40  lemma of_nat_eq: "of_nat k = Abs (int k mod n)"
    1.41 @@ -272,7 +271,7 @@
    1.42    @{typ num1}, since 0 and 1 are not distinct.
    1.43  *}
    1.44  
    1.45 -instantiation num1 :: "{comm_ring,comm_monoid_mult,number,recpower}"
    1.46 +instantiation num1 :: "{comm_ring,comm_monoid_mult,number}"
    1.47  begin
    1.48  
    1.49  lemma num1_eq_iff: "(x::num1) = (y::num1) \<longleftrightarrow> True"
    1.50 @@ -284,7 +283,7 @@
    1.51  end
    1.52  
    1.53  instantiation
    1.54 -  bit0 and bit1 :: (finite) "{zero,one,plus,times,uminus,minus,power}"
    1.55 +  bit0 and bit1 :: (finite) "{zero,one,plus,times,uminus,minus}"
    1.56  begin
    1.57  
    1.58  definition Abs_bit0' :: "int \<Rightarrow> 'a bit0" where
    1.59 @@ -299,7 +298,6 @@
    1.60  definition "x * y = Abs_bit0' (Rep_bit0 x * Rep_bit0 y)"
    1.61  definition "x - y = Abs_bit0' (Rep_bit0 x - Rep_bit0 y)"
    1.62  definition "- x = Abs_bit0' (- Rep_bit0 x)"
    1.63 -definition "x ^ k = Abs_bit0' (Rep_bit0 x ^ k)"
    1.64  
    1.65  definition "0 = Abs_bit1 0"
    1.66  definition "1 = Abs_bit1 1"
    1.67 @@ -307,7 +305,6 @@
    1.68  definition "x * y = Abs_bit1' (Rep_bit1 x * Rep_bit1 y)"
    1.69  definition "x - y = Abs_bit1' (Rep_bit1 x - Rep_bit1 y)"
    1.70  definition "- x = Abs_bit1' (- Rep_bit1 x)"
    1.71 -definition "x ^ k = Abs_bit1' (Rep_bit1 x ^ k)"
    1.72  
    1.73  instance ..
    1.74  
    1.75 @@ -326,7 +323,6 @@
    1.76  apply (rule times_bit0_def [unfolded Abs_bit0'_def])
    1.77  apply (rule minus_bit0_def [unfolded Abs_bit0'_def])
    1.78  apply (rule uminus_bit0_def [unfolded Abs_bit0'_def])
    1.79 -apply (rule power_bit0_def [unfolded Abs_bit0'_def])
    1.80  done
    1.81  
    1.82  interpretation bit1:
    1.83 @@ -342,7 +338,6 @@
    1.84  apply (rule times_bit1_def [unfolded Abs_bit1'_def])
    1.85  apply (rule minus_bit1_def [unfolded Abs_bit1'_def])
    1.86  apply (rule uminus_bit1_def [unfolded Abs_bit1'_def])
    1.87 -apply (rule power_bit1_def [unfolded Abs_bit1'_def])
    1.88  done
    1.89  
    1.90  instance bit0 :: (finite) "{comm_ring_1,recpower}"
    1.91 @@ -386,9 +381,6 @@
    1.92  lemmas bit0_iszero_number_of [simp] = bit0.iszero_number_of
    1.93  lemmas bit1_iszero_number_of [simp] = bit1.iszero_number_of
    1.94  
    1.95 -declare power_Suc [where ?'a="'a::finite bit0", standard, simp]
    1.96 -declare power_Suc [where ?'a="'a::finite bit1", standard, simp]
    1.97 -
    1.98  
    1.99  subsection {* Syntax *}
   1.100