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
```