slightly generalized type class hierarchy concerning unit factors, to allow for lean polynomial normalization
authorhaftmann
Mon Jan 09 18:53:06 2017 +0100 (2017-01-09)
changeset 64848c50db2128048
parent 64847 54f5afc9c413
child 64849 766db3539859
slightly generalized type class hierarchy concerning unit factors, to allow for lean polynomial normalization
src/HOL/Code_Numeral.thy
src/HOL/Divides.thy
src/HOL/Library/Polynomial.thy
src/HOL/Library/Polynomial_Factorial.thy
src/HOL/Number_Theory/Euclidean_Algorithm.thy
src/HOL/Rings.thy
     1.1 --- a/src/HOL/Code_Numeral.thy	Mon Jan 09 15:54:48 2017 +0000
     1.2 +++ b/src/HOL/Code_Numeral.thy	Mon Jan 09 18:53:06 2017 +0100
     1.3 @@ -225,7 +225,7 @@
     1.4    "of_nat (nat_of_integer k) = max 0 k"
     1.5    by transfer auto
     1.6  
     1.7 -instantiation integer :: "{ring_div, normalization_semidom}"
     1.8 +instantiation integer :: normalization_semidom
     1.9  begin
    1.10  
    1.11  lift_definition normalize_integer :: "integer \<Rightarrow> integer"
    1.12 @@ -245,7 +245,16 @@
    1.13    .
    1.14  
    1.15  declare divide_integer.rep_eq [simp]
    1.16 +  
    1.17 +instance
    1.18 +  by (standard; transfer)
    1.19 +    (auto simp add: mult_sgn_abs sgn_mult abs_eq_iff')
    1.20  
    1.21 +end
    1.22 +
    1.23 +instantiation integer :: ring_div
    1.24 +begin
    1.25 +  
    1.26  lift_definition modulo_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
    1.27    is "modulo :: int \<Rightarrow> int \<Rightarrow> int"
    1.28    .
    1.29 @@ -253,7 +262,7 @@
    1.30  declare modulo_integer.rep_eq [simp]
    1.31  
    1.32  instance
    1.33 -  by standard (transfer, simp add: mult_sgn_abs sgn_mult)+
    1.34 +  by (standard; transfer) simp_all
    1.35  
    1.36  end
    1.37  
     2.1 --- a/src/HOL/Divides.thy	Mon Jan 09 15:54:48 2017 +0000
     2.2 +++ b/src/HOL/Divides.thy	Mon Jan 09 18:53:06 2017 +0100
     2.3 @@ -1812,7 +1812,7 @@
     2.4    assume "l \<noteq> 0"
     2.5    then show "k * l div l = k"
     2.6      by (auto simp add: eucl_rel_int_iff ac_simps intro: div_int_unique [of _ _ _ 0])
     2.7 -qed (simp_all add: sgn_mult mult_sgn_abs abs_sgn_eq)
     2.8 +qed (auto simp add: sgn_mult mult_sgn_abs abs_eq_iff')
     2.9  
    2.10  end
    2.11  
     3.1 --- a/src/HOL/Library/Polynomial.thy	Mon Jan 09 15:54:48 2017 +0000
     3.2 +++ b/src/HOL/Library/Polynomial.thy	Mon Jan 09 18:53:06 2017 +0100
     3.3 @@ -17,14 +17,13 @@
     3.4  lemma quotient_of_denom_pos': "snd (quotient_of x) > 0"
     3.5    using quotient_of_denom_pos [OF surjective_pairing] .
     3.6    
     3.7 -lemma of_int_divide_in_Ints: 
     3.8 -  "b dvd a \<Longrightarrow> of_int a div of_int b \<in> (\<int> :: 'a :: idom_divide set)"
     3.9 -proof (cases "of_int b = (0 :: 'a)")
    3.10 -  case False
    3.11 -  assume "b dvd a"
    3.12 -  then obtain c where "a = b * c" ..
    3.13 -  with \<open>of_int b \<noteq> (0::'a)\<close> show ?thesis by simp
    3.14 -qed auto
    3.15 +lemma (in idom_divide) of_int_divide_in_Ints: 
    3.16 +  "of_int a div of_int b \<in> \<int>" if "b dvd a"
    3.17 +proof -
    3.18 +  from that obtain c where "a = b * c" ..
    3.19 +  then show ?thesis
    3.20 +    by (cases "of_int b = 0") simp_all
    3.21 +qed
    3.22  
    3.23    
    3.24  subsection \<open>Auxiliary: operations for lists (later) representing coefficients\<close>
    3.25 @@ -3423,59 +3422,104 @@
    3.26        by force
    3.27  qed
    3.28  
    3.29 -instantiation poly :: ("{normalization_semidom, idom_divide}") normalization_semidom
    3.30 +instantiation poly :: ("{semidom_divide_unit_factor, idom_divide}") normalization_semidom
    3.31  begin
    3.32  
    3.33  definition unit_factor_poly :: "'a poly \<Rightarrow> 'a poly"
    3.34 -  where "unit_factor_poly p = monom (unit_factor (lead_coeff p)) 0"
    3.35 +  where "unit_factor_poly p = [:unit_factor (lead_coeff p):]"
    3.36  
    3.37  definition normalize_poly :: "'a poly \<Rightarrow> 'a poly"
    3.38 -  where "normalize_poly p = map_poly (\<lambda>x. x div unit_factor (lead_coeff p)) p"
    3.39 +  where "normalize p = p div [:unit_factor (lead_coeff p):]"
    3.40  
    3.41  instance proof
    3.42    fix p :: "'a poly"
    3.43    show "unit_factor p * normalize p = p"
    3.44 -    by (cases "p = 0")
    3.45 -       (simp_all add: unit_factor_poly_def normalize_poly_def monom_0 
    3.46 -          smult_conv_map_poly map_poly_map_poly o_def)
    3.47 +  proof (cases "p = 0")
    3.48 +    case True
    3.49 +    then show ?thesis
    3.50 +      by (simp add: unit_factor_poly_def normalize_poly_def)
    3.51 +  next
    3.52 +    case False
    3.53 +    then have "lead_coeff p \<noteq> 0"
    3.54 +      by simp
    3.55 +    then have *: "unit_factor (lead_coeff p) \<noteq> 0"
    3.56 +      using unit_factor_is_unit [of "lead_coeff p"] by auto
    3.57 +    then have "unit_factor (lead_coeff p) dvd 1"
    3.58 +      by (auto intro: unit_factor_is_unit)
    3.59 +    then have **: "unit_factor (lead_coeff p) dvd c" for c
    3.60 +      by (rule dvd_trans) simp
    3.61 +    have ***: "unit_factor (lead_coeff p) * (c div unit_factor (lead_coeff p)) = c" for c
    3.62 +    proof -
    3.63 +      from ** obtain b where "c = unit_factor (lead_coeff p) * b" ..
    3.64 +      then show ?thesis
    3.65 +        using False * by simp
    3.66 +    qed
    3.67 +    have "p div [:unit_factor (lead_coeff p):] =
    3.68 +      map_poly (\<lambda>c. c div unit_factor (lead_coeff p)) p"
    3.69 +      by (simp add: const_poly_dvd_iff div_const_poly_conv_map_poly **)
    3.70 +    then show ?thesis
    3.71 +      by (simp add: normalize_poly_def unit_factor_poly_def
    3.72 +        smult_conv_map_poly map_poly_map_poly o_def ***)
    3.73 +  qed
    3.74  next
    3.75    fix p :: "'a poly"
    3.76    assume "is_unit p"
    3.77 -  then obtain c where p: "p = [:c:]" "is_unit c"
    3.78 +  then obtain c where p: "p = [:c:]" "c dvd 1"
    3.79      by (auto simp: is_unit_poly_iff)
    3.80 -  thus "normalize p = 1"
    3.81 -    by (simp add: normalize_poly_def map_poly_pCons is_unit_normalize one_poly_def)
    3.82 +  then show "unit_factor p = p"
    3.83 +    by (simp add: unit_factor_poly_def monom_0 is_unit_unit_factor)
    3.84  next
    3.85    fix p :: "'a poly" assume "p \<noteq> 0"
    3.86 -  thus "is_unit (unit_factor p)"
    3.87 -    by (simp add: unit_factor_poly_def monom_0 is_unit_poly_iff)
    3.88 +  then show "is_unit (unit_factor p)"
    3.89 +    by (simp add: unit_factor_poly_def monom_0 is_unit_poly_iff unit_factor_is_unit)
    3.90  qed (simp_all add: normalize_poly_def unit_factor_poly_def monom_0 lead_coeff_mult unit_factor_mult)
    3.91  
    3.92  end
    3.93  
    3.94 -lemma normalize_poly_eq_div:
    3.95 -  "normalize p = p div [:unit_factor (lead_coeff p):]"
    3.96 -proof (cases "p = 0")
    3.97 -  case False
    3.98 -  thus ?thesis
    3.99 -    by (subst div_const_poly_conv_map_poly)
   3.100 -       (auto simp: normalize_poly_def const_poly_dvd_iff)
   3.101 -qed (auto simp: normalize_poly_def)
   3.102 +lemma normalize_poly_eq_map_poly:
   3.103 +  "normalize p = map_poly (\<lambda>x. x div unit_factor (lead_coeff p)) p"
   3.104 +proof -
   3.105 +  have "[:unit_factor (lead_coeff p):] dvd p"
   3.106 +    by (metis unit_factor_poly_def unit_factor_self)
   3.107 +  then show ?thesis
   3.108 +    by (simp add: normalize_poly_def div_const_poly_conv_map_poly)
   3.109 +qed
   3.110 +
   3.111 +lemma coeff_normalize [simp]:
   3.112 +  "coeff (normalize p) n = coeff p n div unit_factor (lead_coeff p)"
   3.113 +  by (simp add: normalize_poly_eq_map_poly coeff_map_poly)
   3.114 +
   3.115 +class field_unit_factor = field + unit_factor +
   3.116 +  assumes unit_factor_field [simp]: "unit_factor = id"
   3.117 +begin
   3.118 +
   3.119 +subclass semidom_divide_unit_factor
   3.120 +proof
   3.121 +  fix a
   3.122 +  assume "a \<noteq> 0"
   3.123 +  then have "1 = a * inverse a"
   3.124 +    by simp
   3.125 +  then have "a dvd 1" ..
   3.126 +  then show "unit_factor a dvd 1"
   3.127 +    by simp
   3.128 +qed simp_all
   3.129 +
   3.130 +end
   3.131  
   3.132  lemma unit_factor_pCons:
   3.133 -  "unit_factor (pCons a p) = (if p = 0 then monom (unit_factor a) 0 else unit_factor p)"
   3.134 +  "unit_factor (pCons a p) = (if p = 0 then [:unit_factor a:] else unit_factor p)"
   3.135    by (simp add: unit_factor_poly_def)
   3.136  
   3.137  lemma normalize_monom [simp]:
   3.138    "normalize (monom a n) = monom (normalize a) n"
   3.139 -  by (cases "a = 0") (simp_all add: map_poly_monom normalize_poly_def degree_monom_eq)
   3.140 +  by (cases "a = 0") (simp_all add: map_poly_monom normalize_poly_eq_map_poly degree_monom_eq)
   3.141  
   3.142  lemma unit_factor_monom [simp]:
   3.143 -  "unit_factor (monom a n) = monom (unit_factor a) 0"
   3.144 +  "unit_factor (monom a n) = [:unit_factor a:]"
   3.145    by (cases "a = 0") (simp_all add: unit_factor_poly_def degree_monom_eq)
   3.146  
   3.147  lemma normalize_const_poly: "normalize [:c:] = [:normalize c:]"
   3.148 -  by (simp add: normalize_poly_def map_poly_pCons)
   3.149 +  by (simp add: normalize_poly_eq_map_poly map_poly_pCons)
   3.150  
   3.151  lemma normalize_smult: "normalize (smult c p) = smult (normalize c) (normalize p)"
   3.152  proof -
     4.1 --- a/src/HOL/Library/Polynomial_Factorial.thy	Mon Jan 09 15:54:48 2017 +0000
     4.2 +++ b/src/HOL/Library/Polynomial_Factorial.thy	Mon Jan 09 18:53:06 2017 +0100
     4.3 @@ -520,8 +520,8 @@
     4.4         (simp_all add: unit_factor_field_poly_def normalize_field_poly_def)
     4.5  next
     4.6    fix p :: "'a poly" assume "is_unit p"
     4.7 -  thus "normalize_field_poly p = 1"
     4.8 -    by (elim is_unit_polyE) (auto simp: normalize_field_poly_def monom_0 one_poly_def field_simps)
     4.9 +  then show "unit_factor_field_poly p = p"
    4.10 +    by (elim is_unit_polyE) (auto simp: unit_factor_field_poly_def monom_0 one_poly_def field_simps)
    4.11  next
    4.12    fix p :: "'a poly" assume "p \<noteq> 0"
    4.13    thus "is_unit (unit_factor_field_poly p)"
    4.14 @@ -566,7 +566,7 @@
    4.15  proof -
    4.16    have A: "class.comm_semiring_1 op * 1 op + (0 :: 'a poly)" ..
    4.17    have B: "class.normalization_semidom op div op + op - (0 :: 'a poly) op * 1 
    4.18 -             normalize_field_poly unit_factor_field_poly" ..
    4.19 +             unit_factor_field_poly normalize_field_poly" ..
    4.20    from field_poly.in_prime_factors_imp_prime [of p x] assms
    4.21      show ?thesis unfolding prime_elem_def dvd_field_poly
    4.22        comm_semiring_1.prime_elem_def[OF A] normalization_semidom.prime_def[OF B] by blast
     5.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Mon Jan 09 15:54:48 2017 +0000
     5.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Mon Jan 09 18:53:06 2017 +0100
     5.3 @@ -71,7 +71,7 @@
     5.4  
     5.5  lemma semiring_gcd:
     5.6    "class.semiring_gcd one zero times gcd lcm
     5.7 -    divide plus minus normalize unit_factor"
     5.8 +    divide plus minus unit_factor normalize"
     5.9  proof
    5.10    show "gcd a b dvd a"
    5.11      and "gcd a b dvd b" for a b
    5.12 @@ -97,12 +97,12 @@
    5.13  qed
    5.14  
    5.15  interpretation semiring_gcd one zero times gcd lcm
    5.16 -  divide plus minus normalize unit_factor
    5.17 +  divide plus minus unit_factor normalize
    5.18    by (fact semiring_gcd)
    5.19    
    5.20  lemma semiring_Gcd:
    5.21    "class.semiring_Gcd one zero times gcd lcm Gcd Lcm
    5.22 -    divide plus minus normalize unit_factor"
    5.23 +    divide plus minus unit_factor normalize"
    5.24  proof -
    5.25    show ?thesis
    5.26    proof
    5.27 @@ -180,13 +180,13 @@
    5.28  qed
    5.29  
    5.30  interpretation semiring_Gcd one zero times gcd lcm Gcd Lcm
    5.31 -    divide plus minus normalize unit_factor
    5.32 +    divide plus minus unit_factor normalize
    5.33    by (fact semiring_Gcd)
    5.34  
    5.35  subclass factorial_semiring
    5.36  proof -
    5.37    show "class.factorial_semiring divide plus minus zero times one
    5.38 -     normalize unit_factor"
    5.39 +     unit_factor normalize"
    5.40    proof (standard, rule factorial_semiring_altI_aux) -- \<open>FIXME rule\<close>
    5.41      fix x assume "x \<noteq> 0"
    5.42      thus "finite {p. p dvd x \<and> normalize p = p}"
    5.43 @@ -406,7 +406,7 @@
    5.44    interpret semiring_Gcd 1 0 times
    5.45      Euclidean_Algorithm.gcd Euclidean_Algorithm.lcm
    5.46      Euclidean_Algorithm.Gcd Euclidean_Algorithm.Lcm
    5.47 -    divide plus minus normalize unit_factor
    5.48 +    divide plus minus unit_factor normalize
    5.49      rewrites "dvd.dvd op * = Rings.dvd"
    5.50      by (fact semiring_Gcd) (simp add: dvd.dvd_def dvd_def fun_eq_iff)
    5.51    show [simp]: "Euclidean_Algorithm.gcd = (gcd :: 'a \<Rightarrow> _)"
    5.52 @@ -558,7 +558,7 @@
    5.53    interpret semiring_Gcd 1 0 times
    5.54      "Euclidean_Algorithm.gcd" "Euclidean_Algorithm.lcm"
    5.55      "Euclidean_Algorithm.Gcd" "Euclidean_Algorithm.Lcm"
    5.56 -    divide plus minus normalize unit_factor
    5.57 +    divide plus minus unit_factor normalize
    5.58      rewrites "dvd.dvd op * = Rings.dvd"
    5.59      by (fact semiring_Gcd) (simp add: dvd.dvd_def dvd_def fun_eq_iff)
    5.60    show [simp]: "(Euclidean_Algorithm.gcd :: nat \<Rightarrow> _) = gcd"
    5.61 @@ -590,7 +590,7 @@
    5.62    interpret semiring_Gcd 1 0 times
    5.63      "Euclidean_Algorithm.gcd" "Euclidean_Algorithm.lcm"
    5.64      "Euclidean_Algorithm.Gcd" "Euclidean_Algorithm.Lcm"
    5.65 -    divide plus minus normalize unit_factor
    5.66 +    divide plus minus unit_factor normalize
    5.67      rewrites "dvd.dvd op * = Rings.dvd"
    5.68      by (fact semiring_Gcd) (simp add: dvd.dvd_def dvd_def fun_eq_iff)
    5.69    show [simp]: "(Euclidean_Algorithm.gcd :: int \<Rightarrow> _) = gcd"
     6.1 --- a/src/HOL/Rings.thy	Mon Jan 09 15:54:48 2017 +0000
     6.2 +++ b/src/HOL/Rings.thy	Mon Jan 09 18:53:06 2017 +0100
     6.3 @@ -1156,15 +1156,20 @@
     6.4  
     6.5  end
     6.6  
     6.7 -class normalization_semidom = algebraic_semidom +
     6.8 +class unit_factor =
     6.9 +  fixes unit_factor :: "'a \<Rightarrow> 'a"
    6.10 +
    6.11 +class semidom_divide_unit_factor = semidom_divide + unit_factor +
    6.12 +  assumes unit_factor_0 [simp]: "unit_factor 0 = 0"
    6.13 +    and is_unit_unit_factor: "a dvd 1 \<Longrightarrow> unit_factor a = a"
    6.14 +    and unit_factor_is_unit: "a \<noteq> 0 \<Longrightarrow> unit_factor a dvd 1"
    6.15 +    and unit_factor_mult: "unit_factor (a * b) = unit_factor a * unit_factor b"
    6.16 +  -- \<open>This fine-grained hierarchy will later on allow lean normalization of polynomials\<close>
    6.17 +  
    6.18 +class normalization_semidom = algebraic_semidom + semidom_divide_unit_factor +
    6.19    fixes normalize :: "'a \<Rightarrow> 'a"
    6.20 -    and unit_factor :: "'a \<Rightarrow> 'a"
    6.21    assumes unit_factor_mult_normalize [simp]: "unit_factor a * normalize a = a"
    6.22      and normalize_0 [simp]: "normalize 0 = 0"
    6.23 -    and unit_factor_0 [simp]: "unit_factor 0 = 0"
    6.24 -    and is_unit_normalize: "is_unit a  \<Longrightarrow> normalize a = 1"
    6.25 -    and unit_factor_is_unit [iff]: "a \<noteq> 0 \<Longrightarrow> is_unit (unit_factor a)"
    6.26 -    and unit_factor_mult: "unit_factor (a * b) = unit_factor a * unit_factor b"
    6.27  begin
    6.28  
    6.29  text \<open>
    6.30 @@ -1176,6 +1181,8 @@
    6.31    think about equality of normalized values rather than associated elements.
    6.32  \<close>
    6.33  
    6.34 +declare unit_factor_is_unit [iff]
    6.35 +  
    6.36  lemma unit_factor_dvd [simp]: "a \<noteq> 0 \<Longrightarrow> unit_factor a dvd b"
    6.37    by (rule unit_imp_dvd) simp
    6.38  
    6.39 @@ -1207,13 +1214,45 @@
    6.40    then show ?lhs by simp
    6.41  qed
    6.42  
    6.43 -lemma is_unit_unit_factor:
    6.44 +lemma div_unit_factor [simp]: "a div unit_factor a = normalize a"
    6.45 +proof (cases "a = 0")
    6.46 +  case True
    6.47 +  then show ?thesis by simp
    6.48 +next
    6.49 +  case False
    6.50 +  then have "unit_factor a \<noteq> 0"
    6.51 +    by simp
    6.52 +  with nonzero_mult_div_cancel_left
    6.53 +  have "unit_factor a * normalize a div unit_factor a = normalize a"
    6.54 +    by blast
    6.55 +  then show ?thesis by simp
    6.56 +qed
    6.57 +
    6.58 +lemma normalize_div [simp]: "normalize a div a = 1 div unit_factor a"
    6.59 +proof (cases "a = 0")
    6.60 +  case True
    6.61 +  then show ?thesis by simp
    6.62 +next
    6.63 +  case False
    6.64 +  have "normalize a div a = normalize a div (unit_factor a * normalize a)"
    6.65 +    by simp
    6.66 +  also have "\<dots> = 1 div unit_factor a"
    6.67 +    using False by (subst is_unit_div_mult_cancel_right) simp_all
    6.68 +  finally show ?thesis .
    6.69 +qed
    6.70 +
    6.71 +lemma is_unit_normalize:
    6.72    assumes "is_unit a"
    6.73 -  shows "unit_factor a = a"
    6.74 +  shows "normalize a = 1"
    6.75  proof -
    6.76 -  from assms have "normalize a = 1" by (rule is_unit_normalize)
    6.77 -  moreover from unit_factor_mult_normalize have "unit_factor a * normalize a = a" .
    6.78 -  ultimately show ?thesis by simp
    6.79 +  from assms have "unit_factor a = a"
    6.80 +    by (rule is_unit_unit_factor)
    6.81 +  moreover from assms have "a \<noteq> 0"
    6.82 +    by auto
    6.83 +  moreover have "normalize a = a div unit_factor a"
    6.84 +    by simp
    6.85 +  ultimately show ?thesis
    6.86 +    by simp
    6.87  qed
    6.88  
    6.89  lemma unit_factor_1 [simp]: "unit_factor 1 = 1"
    6.90 @@ -1251,32 +1290,6 @@
    6.91    then show ?thesis by simp
    6.92  qed
    6.93  
    6.94 -lemma div_unit_factor [simp]: "a div unit_factor a = normalize a"
    6.95 -proof (cases "a = 0")
    6.96 -  case True
    6.97 -  then show ?thesis by simp
    6.98 -next
    6.99 -  case False
   6.100 -  then have "unit_factor a \<noteq> 0" by simp
   6.101 -  with nonzero_mult_div_cancel_left
   6.102 -  have "unit_factor a * normalize a div unit_factor a = normalize a"
   6.103 -    by blast
   6.104 -  then show ?thesis by simp
   6.105 -qed
   6.106 -
   6.107 -lemma normalize_div [simp]: "normalize a div a = 1 div unit_factor a"
   6.108 -proof (cases "a = 0")
   6.109 -  case True
   6.110 -  then show ?thesis by simp
   6.111 -next
   6.112 -  case False
   6.113 -  have "normalize a div a = normalize a div (unit_factor a * normalize a)"
   6.114 -    by simp
   6.115 -  also have "\<dots> = 1 div unit_factor a"
   6.116 -    using False by (subst is_unit_div_mult_cancel_right) simp_all
   6.117 -  finally show ?thesis .
   6.118 -qed
   6.119 -
   6.120  lemma mult_one_div_unit_factor [simp]: "a * (1 div unit_factor b) = a div unit_factor b"
   6.121    by (cases "b = 0") simp_all
   6.122  
   6.123 @@ -1823,6 +1836,14 @@
   6.124  proposition abs_eq_iff: "\<bar>x\<bar> = \<bar>y\<bar> \<longleftrightarrow> x = y \<or> x = -y"
   6.125    by (auto simp add: abs_if split: if_split_asm)
   6.126  
   6.127 +lemma abs_eq_iff':
   6.128 +  "\<bar>a\<bar> = b \<longleftrightarrow> b \<ge> 0 \<and> (a = b \<or> a = - b)"
   6.129 +  by (cases "a \<ge> 0") auto
   6.130 +
   6.131 +lemma eq_abs_iff':
   6.132 +  "a = \<bar>b\<bar> \<longleftrightarrow> a \<ge> 0 \<and> (b = a \<or> b = - a)"
   6.133 +  using abs_eq_iff' [of b a] by auto
   6.134 +
   6.135  lemma sum_squares_ge_zero: "0 \<le> x * x + y * y"
   6.136    by (intro add_nonneg_nonneg zero_le_square)
   6.137