src/HOL/Computational_Algebra/Field_as_Ring.thy
changeset 65417 fc41a5650fb1
child 65435 378175f44328
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Computational_Algebra/Field_as_Ring.thy	Thu Apr 06 21:37:13 2017 +0200
     1.3 @@ -0,0 +1,120 @@
     1.4 +(*  Title:      HOL/Library/Field_as_Ring.thy
     1.5 +    Author:     Manuel Eberl
     1.6 +*)
     1.7 +
     1.8 +theory Field_as_Ring
     1.9 +imports 
    1.10 +  Complex_Main
    1.11 +  Euclidean_Algorithm
    1.12 +begin
    1.13 +
    1.14 +context field
    1.15 +begin
    1.16 +
    1.17 +subclass idom_divide ..
    1.18 +
    1.19 +definition normalize_field :: "'a \<Rightarrow> 'a" 
    1.20 +  where [simp]: "normalize_field x = (if x = 0 then 0 else 1)"
    1.21 +definition unit_factor_field :: "'a \<Rightarrow> 'a" 
    1.22 +  where [simp]: "unit_factor_field x = x"
    1.23 +definition euclidean_size_field :: "'a \<Rightarrow> nat" 
    1.24 +  where [simp]: "euclidean_size_field x = (if x = 0 then 0 else 1)"
    1.25 +definition mod_field :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    1.26 +  where [simp]: "mod_field x y = (if y = 0 then x else 0)"
    1.27 +
    1.28 +end
    1.29 +
    1.30 +instantiation real :: unique_euclidean_ring
    1.31 +begin
    1.32 +
    1.33 +definition [simp]: "normalize_real = (normalize_field :: real \<Rightarrow> _)"
    1.34 +definition [simp]: "unit_factor_real = (unit_factor_field :: real \<Rightarrow> _)"
    1.35 +definition [simp]: "euclidean_size_real = (euclidean_size_field :: real \<Rightarrow> _)"
    1.36 +definition [simp]: "uniqueness_constraint_real = (top :: real \<Rightarrow> real \<Rightarrow> bool)"
    1.37 +definition [simp]: "modulo_real = (mod_field :: real \<Rightarrow> _)"
    1.38 +
    1.39 +instance
    1.40 +  by standard
    1.41 +    (simp_all add: dvd_field_iff divide_simps split: if_splits)
    1.42 +
    1.43 +end
    1.44 +
    1.45 +instantiation real :: euclidean_ring_gcd
    1.46 +begin
    1.47 +
    1.48 +definition gcd_real :: "real \<Rightarrow> real \<Rightarrow> real" where
    1.49 +  "gcd_real = Euclidean_Algorithm.gcd"
    1.50 +definition lcm_real :: "real \<Rightarrow> real \<Rightarrow> real" where
    1.51 +  "lcm_real = Euclidean_Algorithm.lcm"
    1.52 +definition Gcd_real :: "real set \<Rightarrow> real" where
    1.53 + "Gcd_real = Euclidean_Algorithm.Gcd"
    1.54 +definition Lcm_real :: "real set \<Rightarrow> real" where
    1.55 + "Lcm_real = Euclidean_Algorithm.Lcm"
    1.56 +
    1.57 +instance by standard (simp_all add: gcd_real_def lcm_real_def Gcd_real_def Lcm_real_def)
    1.58 +
    1.59 +end
    1.60 +
    1.61 +instantiation rat :: unique_euclidean_ring
    1.62 +begin
    1.63 +
    1.64 +definition [simp]: "normalize_rat = (normalize_field :: rat \<Rightarrow> _)"
    1.65 +definition [simp]: "unit_factor_rat = (unit_factor_field :: rat \<Rightarrow> _)"
    1.66 +definition [simp]: "euclidean_size_rat = (euclidean_size_field :: rat \<Rightarrow> _)"
    1.67 +definition [simp]: "uniqueness_constraint_rat = (top :: rat \<Rightarrow> rat \<Rightarrow> bool)"
    1.68 +definition [simp]: "modulo_rat = (mod_field :: rat \<Rightarrow> _)"
    1.69 +
    1.70 +instance
    1.71 +  by standard
    1.72 +    (simp_all add: dvd_field_iff divide_simps split: if_splits)
    1.73 +
    1.74 +end
    1.75 +
    1.76 +instantiation rat :: euclidean_ring_gcd
    1.77 +begin
    1.78 +
    1.79 +definition gcd_rat :: "rat \<Rightarrow> rat \<Rightarrow> rat" where
    1.80 +  "gcd_rat = Euclidean_Algorithm.gcd"
    1.81 +definition lcm_rat :: "rat \<Rightarrow> rat \<Rightarrow> rat" where
    1.82 +  "lcm_rat = Euclidean_Algorithm.lcm"
    1.83 +definition Gcd_rat :: "rat set \<Rightarrow> rat" where
    1.84 + "Gcd_rat = Euclidean_Algorithm.Gcd"
    1.85 +definition Lcm_rat :: "rat set \<Rightarrow> rat" where
    1.86 + "Lcm_rat = Euclidean_Algorithm.Lcm"
    1.87 +
    1.88 +instance by standard (simp_all add: gcd_rat_def lcm_rat_def Gcd_rat_def Lcm_rat_def)
    1.89 +
    1.90 +end
    1.91 +
    1.92 +instantiation complex :: unique_euclidean_ring
    1.93 +begin
    1.94 +
    1.95 +definition [simp]: "normalize_complex = (normalize_field :: complex \<Rightarrow> _)"
    1.96 +definition [simp]: "unit_factor_complex = (unit_factor_field :: complex \<Rightarrow> _)"
    1.97 +definition [simp]: "euclidean_size_complex = (euclidean_size_field :: complex \<Rightarrow> _)"
    1.98 +definition [simp]: "uniqueness_constraint_complex = (top :: complex \<Rightarrow> complex \<Rightarrow> bool)"
    1.99 +definition [simp]: "modulo_complex = (mod_field :: complex \<Rightarrow> _)"
   1.100 +
   1.101 +instance
   1.102 +  by standard
   1.103 +    (simp_all add: dvd_field_iff divide_simps split: if_splits)
   1.104 +
   1.105 +end
   1.106 +
   1.107 +instantiation complex :: euclidean_ring_gcd
   1.108 +begin
   1.109 +
   1.110 +definition gcd_complex :: "complex \<Rightarrow> complex \<Rightarrow> complex" where
   1.111 +  "gcd_complex = Euclidean_Algorithm.gcd"
   1.112 +definition lcm_complex :: "complex \<Rightarrow> complex \<Rightarrow> complex" where
   1.113 +  "lcm_complex = Euclidean_Algorithm.lcm"
   1.114 +definition Gcd_complex :: "complex set \<Rightarrow> complex" where
   1.115 + "Gcd_complex = Euclidean_Algorithm.Gcd"
   1.116 +definition Lcm_complex :: "complex set \<Rightarrow> complex" where
   1.117 + "Lcm_complex = Euclidean_Algorithm.Lcm"
   1.118 +
   1.119 +instance by standard (simp_all add: gcd_complex_def lcm_complex_def Gcd_complex_def Lcm_complex_def)
   1.120 +
   1.121 +end
   1.122 +
   1.123 +end