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