avoid concrete (anti)mono in theorem names since it could be the other way round
authorhaftmann
Sun Jan 28 16:38:48 2018 +0000 (16 months ago)
changeset 675255d04d7bcd5f6
parent 67524 a23c3ec2ff28
child 67526 a585c5b53576
avoid concrete (anti)mono in theorem names since it could be the other way round
NEWS
src/HOL/Lattices_Big.thy
     1.1 --- a/NEWS	Mon Jan 29 19:26:14 2018 +0100
     1.2 +++ b/NEWS	Sun Jan 28 16:38:48 2018 +0000
     1.3 @@ -169,6 +169,13 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Clarifed theorem names:
     1.8 +
     1.9 +  Min.antimono ~> Min.subset_imp
    1.10 +  Max.antimono ~> Max.subset_imp
    1.11 +
    1.12 +Minor INCOMPATIBILITY.
    1.13 +
    1.14  * A new command parametric_constant for proving parametricity of
    1.15  non-recursive definitions. For constants that are not fully parametric
    1.16  the command will infer conditions on relations (e.g., bi_unique,
     2.1 --- a/src/HOL/Lattices_Big.thy	Mon Jan 29 19:26:14 2018 +0100
     2.2 +++ b/src/HOL/Lattices_Big.thy	Sun Jan 28 16:38:48 2018 +0000
     2.3 @@ -132,7 +132,7 @@
     2.4  lemma bounded_iff:
     2.5    assumes "finite A" and "A \<noteq> {}"
     2.6    shows "x \<^bold>\<le> F A \<longleftrightarrow> (\<forall>a\<in>A. x \<^bold>\<le> a)"
     2.7 -  using assms by (induct rule: finite_ne_induct) (simp_all add: bounded_iff)
     2.8 +  using assms by (induct rule: finite_ne_induct) simp_all
     2.9  
    2.10  lemma boundedI:
    2.11    assumes "finite A"
    2.12 @@ -162,7 +162,7 @@
    2.13    qed
    2.14  qed
    2.15  
    2.16 -lemma antimono:
    2.17 +lemma subset_imp:
    2.18    assumes "A \<subseteq> B" and "A \<noteq> {}" and "finite B"
    2.19    shows "F B \<^bold>\<le> F A"
    2.20  proof (cases "A = B")
    2.21 @@ -256,7 +256,7 @@
    2.22  lemma bounded_iff:
    2.23    assumes "finite A"
    2.24    shows "x \<^bold>\<le> F A \<longleftrightarrow> (\<forall>a\<in>A. x \<^bold>\<le> a)"
    2.25 -  using assms by (induct A) (simp_all add: bounded_iff)
    2.26 +  using assms by (induct A) simp_all
    2.27  
    2.28  lemma boundedI:
    2.29    assumes "finite A"
    2.30 @@ -285,7 +285,7 @@
    2.31    qed
    2.32  qed
    2.33  
    2.34 -lemma antimono:
    2.35 +lemma subset_imp:
    2.36    assumes "A \<subseteq> B" and "finite B"
    2.37    shows "F B \<^bold>\<le> F A"
    2.38  proof (cases "A = B")
    2.39 @@ -648,12 +648,12 @@
    2.40  lemma Min_antimono:
    2.41    assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
    2.42    shows "Min N \<le> Min M"
    2.43 -  using assms by (fact Min.antimono)
    2.44 +  using assms by (fact Min.subset_imp)
    2.45  
    2.46  lemma Max_mono:
    2.47    assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
    2.48    shows "Max M \<le> Max N"
    2.49 -  using assms by (fact Max.antimono)
    2.50 +  using assms by (fact Max.subset_imp)
    2.51  
    2.52  end
    2.53