src/HOL/Computational_Algebra/Field_as_Ring.thy
author haftmann
Sun Oct 08 22:28:22 2017 +0200 (19 months ago)
changeset 66817 0b12755ccbb2
parent 65435 378175f44328
child 66838 17989f6bc7b2
permissions -rw-r--r--
euclidean rings need no normalization
     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, normalization_euclidean_semiring}"
    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, normalization_euclidean_semiring}"
    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, normalization_euclidean_semiring}"
    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