summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson <lp15@cam.ac.uk> |

Sun, 22 Mar 2020 19:02:39 +0000 | |

changeset 71586 | e30dbfa53b0d |

parent 71585 | 4b1021677f15 |

child 71587 | 3904cfde1aa9 |

new-style Greater lemmas

src/HOL/Computational_Algebra/Polynomial.thy | file | annotate | diff | comparison | revisions | |

src/HOL/Computational_Algebra/Polynomial_Factorial.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/Computational_Algebra/Polynomial.thy Sun Mar 22 17:21:16 2020 +0000 +++ b/src/HOL/Computational_Algebra/Polynomial.thy Sun Mar 22 19:02:39 2020 +0000 @@ -4367,11 +4367,11 @@ define m where "m = (GREATEST m. \<not>c dvd coeff b m)" assume "\<not>[:c:] dvd b" hence A: "\<exists>i. \<not>c dvd coeff b i" by (subst (asm) const_poly_dvd_iff) blast - have B: "\<forall>i. \<not>c dvd coeff b i \<longrightarrow> i \<le> degree b" + have B: "\<And>i. \<not>c dvd coeff b i \<Longrightarrow> i \<le> degree b" by (auto intro: le_degree) have coeff_m: "\<not>c dvd coeff b m" unfolding m_def by (rule GreatestI_ex_nat[OF A B]) have "i \<le> m" if "\<not>c dvd coeff b i" for i - unfolding m_def by (rule Greatest_le_nat[OF that B]) + unfolding m_def by (metis (mono_tags, lifting) B Greatest_le_nat that) hence dvd_b: "c dvd coeff b i" if "i > m" for i using that by force have "c dvd coeff a i" for i

--- a/src/HOL/Computational_Algebra/Polynomial_Factorial.thy Sun Mar 22 17:21:16 2020 +0000 +++ b/src/HOL/Computational_Algebra/Polynomial_Factorial.thy Sun Mar 22 19:02:39 2020 +0000 @@ -286,11 +286,11 @@ define m where "m = (GREATEST m. \<not>c dvd coeff b m)" assume "\<not>[:c:] dvd b" hence A: "\<exists>i. \<not>c dvd coeff b i" by (subst (asm) const_poly_dvd_iff) blast - have B: "\<forall>i. \<not>c dvd coeff b i \<longrightarrow> i \<le> degree b" + have B: "\<And>i. \<not>c dvd coeff b i \<Longrightarrow> i \<le> degree b" by (auto intro: le_degree) have coeff_m: "\<not>c dvd coeff b m" unfolding m_def by (rule GreatestI_ex_nat[OF A B]) have "i \<le> m" if "\<not>c dvd coeff b i" for i - unfolding m_def by (rule Greatest_le_nat[OF that B]) + unfolding m_def by (blast intro!: Greatest_le_nat that B) hence dvd_b: "c dvd coeff b i" if "i > m" for i using that by force have "c dvd coeff a i" for i