src/HOL/Computational_Algebra/Field_as_Ring.thy
 author wenzelm Fri Apr 07 21:17:18 2017 +0200 (2017-04-07) changeset 65435 378175f44328 parent 65417 fc41a5650fb1 child 66817 0b12755ccbb2 permissions -rw-r--r--
```     1 (*  Title:      HOL/Computational_Algebra/Field_as_Ring.thy
```
```     2     Author:     Manuel Eberl
```
```     3 *)
```
```     4
```
```     5 theory Field_as_Ring
```
```     6 imports
```
```     7   Complex_Main
```
```     8   Euclidean_Algorithm
```
```     9 begin
```
```    10
```
```    11 context field
```
```    12 begin
```
```    13
```
```    14 subclass idom_divide ..
```
```    15
```
```    16 definition normalize_field :: "'a \<Rightarrow> 'a"
```
```    17   where [simp]: "normalize_field x = (if x = 0 then 0 else 1)"
```
```    18 definition unit_factor_field :: "'a \<Rightarrow> 'a"
```
```    19   where [simp]: "unit_factor_field x = x"
```
```    20 definition euclidean_size_field :: "'a \<Rightarrow> nat"
```
```    21   where [simp]: "euclidean_size_field x = (if x = 0 then 0 else 1)"
```
```    22 definition mod_field :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
```
```    23   where [simp]: "mod_field x y = (if y = 0 then x else 0)"
```
```    24
```
```    25 end
```
```    26
```
```    27 instantiation real :: unique_euclidean_ring
```
```    28 begin
```
```    29
```
```    30 definition [simp]: "normalize_real = (normalize_field :: real \<Rightarrow> _)"
```
```    31 definition [simp]: "unit_factor_real = (unit_factor_field :: real \<Rightarrow> _)"
```
```    32 definition [simp]: "euclidean_size_real = (euclidean_size_field :: real \<Rightarrow> _)"
```
```    33 definition [simp]: "uniqueness_constraint_real = (top :: real \<Rightarrow> real \<Rightarrow> bool)"
```
```    34 definition [simp]: "modulo_real = (mod_field :: real \<Rightarrow> _)"
```
```    35
```
```    36 instance
```
```    37   by standard
```
```    38     (simp_all add: dvd_field_iff divide_simps split: if_splits)
```
```    39
```
```    40 end
```
```    41
```
```    42 instantiation real :: euclidean_ring_gcd
```
```    43 begin
```
```    44
```
```    45 definition gcd_real :: "real \<Rightarrow> real \<Rightarrow> real" where
```
```    46   "gcd_real = Euclidean_Algorithm.gcd"
```
```    47 definition lcm_real :: "real \<Rightarrow> real \<Rightarrow> real" where
```
```    48   "lcm_real = Euclidean_Algorithm.lcm"
```
```    49 definition Gcd_real :: "real set \<Rightarrow> real" where
```
```    50  "Gcd_real = Euclidean_Algorithm.Gcd"
```
```    51 definition Lcm_real :: "real set \<Rightarrow> real" where
```
```    52  "Lcm_real = Euclidean_Algorithm.Lcm"
```
```    53
```
```    54 instance by standard (simp_all add: gcd_real_def lcm_real_def Gcd_real_def Lcm_real_def)
```
```    55
```
```    56 end
```
```    57
```
```    58 instantiation rat :: unique_euclidean_ring
```
```    59 begin
```
```    60
```
```    61 definition [simp]: "normalize_rat = (normalize_field :: rat \<Rightarrow> _)"
```
```    62 definition [simp]: "unit_factor_rat = (unit_factor_field :: rat \<Rightarrow> _)"
```
```    63 definition [simp]: "euclidean_size_rat = (euclidean_size_field :: rat \<Rightarrow> _)"
```
```    64 definition [simp]: "uniqueness_constraint_rat = (top :: rat \<Rightarrow> rat \<Rightarrow> bool)"
```
```    65 definition [simp]: "modulo_rat = (mod_field :: rat \<Rightarrow> _)"
```
```    66
```
```    67 instance
```
```    68   by standard
```
```    69     (simp_all add: dvd_field_iff divide_simps split: if_splits)
```
```    70
```
```    71 end
```
```    72
```
```    73 instantiation rat :: euclidean_ring_gcd
```
```    74 begin
```
```    75
```
```    76 definition gcd_rat :: "rat \<Rightarrow> rat \<Rightarrow> rat" where
```
```    77   "gcd_rat = Euclidean_Algorithm.gcd"
```
```    78 definition lcm_rat :: "rat \<Rightarrow> rat \<Rightarrow> rat" where
```
```    79   "lcm_rat = Euclidean_Algorithm.lcm"
```
```    80 definition Gcd_rat :: "rat set \<Rightarrow> rat" where
```
```    81  "Gcd_rat = Euclidean_Algorithm.Gcd"
```
```    82 definition Lcm_rat :: "rat set \<Rightarrow> rat" where
```
```    83  "Lcm_rat = Euclidean_Algorithm.Lcm"
```
```    84
```
```    85 instance by standard (simp_all add: gcd_rat_def lcm_rat_def Gcd_rat_def Lcm_rat_def)
```
```    86
```
```    87 end
```
```    88
```
```    89 instantiation complex :: unique_euclidean_ring
```
```    90 begin
```
```    91
```
```    92 definition [simp]: "normalize_complex = (normalize_field :: complex \<Rightarrow> _)"
```
```    93 definition [simp]: "unit_factor_complex = (unit_factor_field :: complex \<Rightarrow> _)"
```
```    94 definition [simp]: "euclidean_size_complex = (euclidean_size_field :: complex \<Rightarrow> _)"
```
```    95 definition [simp]: "uniqueness_constraint_complex = (top :: complex \<Rightarrow> complex \<Rightarrow> bool)"
```
```    96 definition [simp]: "modulo_complex = (mod_field :: complex \<Rightarrow> _)"
```
```    97
```
```    98 instance
```
```    99   by standard
```
```   100     (simp_all add: dvd_field_iff divide_simps split: if_splits)
```
```   101
```
```   102 end
```
```   103
```
```   104 instantiation complex :: euclidean_ring_gcd
```
```   105 begin
```
```   106
```
```   107 definition gcd_complex :: "complex \<Rightarrow> complex \<Rightarrow> complex" where
```
```   108   "gcd_complex = Euclidean_Algorithm.gcd"
```
```   109 definition lcm_complex :: "complex \<Rightarrow> complex \<Rightarrow> complex" where
```
```   110   "lcm_complex = Euclidean_Algorithm.lcm"
```
```   111 definition Gcd_complex :: "complex set \<Rightarrow> complex" where
```
```   112  "Gcd_complex = Euclidean_Algorithm.Gcd"
```
```   113 definition Lcm_complex :: "complex set \<Rightarrow> complex" where
```
```   114  "Lcm_complex = Euclidean_Algorithm.Lcm"
```
```   115
```
```   116 instance by standard (simp_all add: gcd_complex_def lcm_complex_def Gcd_complex_def Lcm_complex_def)
```
```   117
```
```   118 end
```
```   119
```
```   120 end
```