moved name duplicates to end of theory; reduced warning noise
authorhaftmann
Mon Jan 04 16:00:23 2010 +0100 (2010-01-04)
changeset 342503b619abaa67a
parent 34249 54621a41b03c
child 34251 cd642bb91f64
moved name duplicates to end of theory; reduced warning noise
src/HOL/Orderings.thy
     1.1 --- a/src/HOL/Orderings.thy	Mon Jan 04 14:10:13 2010 +0100
     1.2 +++ b/src/HOL/Orderings.thy	Mon Jan 04 16:00:23 2010 +0100
     1.3 @@ -550,44 +550,6 @@
     1.4  *}
     1.5  
     1.6  
     1.7 -subsection {* Name duplicates *}
     1.8 -
     1.9 -lemmas order_less_le = less_le
    1.10 -lemmas order_eq_refl = preorder_class.eq_refl
    1.11 -lemmas order_less_irrefl = preorder_class.less_irrefl
    1.12 -lemmas order_le_less = order_class.le_less
    1.13 -lemmas order_le_imp_less_or_eq = order_class.le_imp_less_or_eq
    1.14 -lemmas order_less_imp_le = preorder_class.less_imp_le
    1.15 -lemmas order_less_imp_not_eq = order_class.less_imp_not_eq
    1.16 -lemmas order_less_imp_not_eq2 = order_class.less_imp_not_eq2
    1.17 -lemmas order_neq_le_trans = order_class.neq_le_trans
    1.18 -lemmas order_le_neq_trans = order_class.le_neq_trans
    1.19 -
    1.20 -lemmas order_antisym = antisym
    1.21 -lemmas order_less_not_sym = preorder_class.less_not_sym
    1.22 -lemmas order_less_asym = preorder_class.less_asym
    1.23 -lemmas order_eq_iff = order_class.eq_iff
    1.24 -lemmas order_antisym_conv = order_class.antisym_conv
    1.25 -lemmas order_less_trans = preorder_class.less_trans
    1.26 -lemmas order_le_less_trans = preorder_class.le_less_trans
    1.27 -lemmas order_less_le_trans = preorder_class.less_le_trans
    1.28 -lemmas order_less_imp_not_less = preorder_class.less_imp_not_less
    1.29 -lemmas order_less_imp_triv = preorder_class.less_imp_triv
    1.30 -lemmas order_less_asym' = preorder_class.less_asym'
    1.31 -
    1.32 -lemmas linorder_linear = linear
    1.33 -lemmas linorder_less_linear = linorder_class.less_linear
    1.34 -lemmas linorder_le_less_linear = linorder_class.le_less_linear
    1.35 -lemmas linorder_le_cases = linorder_class.le_cases
    1.36 -lemmas linorder_not_less = linorder_class.not_less
    1.37 -lemmas linorder_not_le = linorder_class.not_le
    1.38 -lemmas linorder_neq_iff = linorder_class.neq_iff
    1.39 -lemmas linorder_neqE = linorder_class.neqE
    1.40 -lemmas linorder_antisym_conv1 = linorder_class.antisym_conv1
    1.41 -lemmas linorder_antisym_conv2 = linorder_class.antisym_conv2
    1.42 -lemmas linorder_antisym_conv3 = linorder_class.antisym_conv3
    1.43 -
    1.44 -
    1.45  subsection {* Bounded quantifiers *}
    1.46  
    1.47  syntax
    1.48 @@ -698,7 +660,7 @@
    1.49    assume r: "!!x y. x < y ==> f x < f y"
    1.50    assume "a < b" hence "f a < f b" by (rule r)
    1.51    also assume "f b < c"
    1.52 -  finally (order_less_trans) show ?thesis .
    1.53 +  finally (less_trans) show ?thesis .
    1.54  qed
    1.55  
    1.56  lemma order_less_subst1: "(a::'a::order) < f b ==> (b::'b::order) < c ==>
    1.57 @@ -707,7 +669,7 @@
    1.58    assume r: "!!x y. x < y ==> f x < f y"
    1.59    assume "a < f b"
    1.60    also assume "b < c" hence "f b < f c" by (rule r)
    1.61 -  finally (order_less_trans) show ?thesis .
    1.62 +  finally (less_trans) show ?thesis .
    1.63  qed
    1.64  
    1.65  lemma order_le_less_subst2: "(a::'a::order) <= b ==> f b < (c::'c::order) ==>
    1.66 @@ -716,7 +678,7 @@
    1.67    assume r: "!!x y. x <= y ==> f x <= f y"
    1.68    assume "a <= b" hence "f a <= f b" by (rule r)
    1.69    also assume "f b < c"
    1.70 -  finally (order_le_less_trans) show ?thesis .
    1.71 +  finally (le_less_trans) show ?thesis .
    1.72  qed
    1.73  
    1.74  lemma order_le_less_subst1: "(a::'a::order) <= f b ==> (b::'b::order) < c ==>
    1.75 @@ -725,7 +687,7 @@
    1.76    assume r: "!!x y. x < y ==> f x < f y"
    1.77    assume "a <= f b"
    1.78    also assume "b < c" hence "f b < f c" by (rule r)
    1.79 -  finally (order_le_less_trans) show ?thesis .
    1.80 +  finally (le_less_trans) show ?thesis .
    1.81  qed
    1.82  
    1.83  lemma order_less_le_subst2: "(a::'a::order) < b ==> f b <= (c::'c::order) ==>
    1.84 @@ -734,7 +696,7 @@
    1.85    assume r: "!!x y. x < y ==> f x < f y"
    1.86    assume "a < b" hence "f a < f b" by (rule r)
    1.87    also assume "f b <= c"
    1.88 -  finally (order_less_le_trans) show ?thesis .
    1.89 +  finally (less_le_trans) show ?thesis .
    1.90  qed
    1.91  
    1.92  lemma order_less_le_subst1: "(a::'a::order) < f b ==> (b::'b::order) <= c ==>
    1.93 @@ -743,7 +705,7 @@
    1.94    assume r: "!!x y. x <= y ==> f x <= f y"
    1.95    assume "a < f b"
    1.96    also assume "b <= c" hence "f b <= f c" by (rule r)
    1.97 -  finally (order_less_le_trans) show ?thesis .
    1.98 +  finally (less_le_trans) show ?thesis .
    1.99  qed
   1.100  
   1.101  lemma order_subst1: "(a::'a::order) <= f b ==> (b::'b::order) <= c ==>
   1.102 @@ -876,8 +838,6 @@
   1.103    ord_eq_less_trans
   1.104    trans
   1.105  
   1.106 -(* FIXME cleanup *)
   1.107 -
   1.108  text {* These support proving chains of decreasing inequalities
   1.109      a >= b >= c ... in Isar proofs. *}
   1.110  
   1.111 @@ -1070,12 +1030,12 @@
   1.112  
   1.113  lemma min_leastR: "(\<And>x\<Colon>'a\<Colon>order. least \<le> x) \<Longrightarrow> min x least = least"
   1.114  apply (simp add: min_def)
   1.115 -apply (blast intro: order_antisym)
   1.116 +apply (blast intro: antisym)
   1.117  done
   1.118  
   1.119  lemma max_leastR: "(\<And>x\<Colon>'a\<Colon>order. least \<le> x) \<Longrightarrow> max x least = x"
   1.120  apply (simp add: max_def)
   1.121 -apply (blast intro: order_antisym)
   1.122 +apply (blast intro: antisym)
   1.123  done
   1.124  
   1.125  
   1.126 @@ -1107,7 +1067,7 @@
   1.127  lemma wellorder_Least_lemma:
   1.128    fixes k :: 'a
   1.129    assumes "P k"
   1.130 -  shows "P (LEAST x. P x)" and "(LEAST x. P x) \<le> k"
   1.131 +  shows LeastI: "P (LEAST x. P x)" and Least_le: "(LEAST x. P x) \<le> k"
   1.132  proof -
   1.133    have "P (LEAST x. P x) \<and> (LEAST x. P x) \<le> k"
   1.134    using assms proof (induct k rule: less_induct)
   1.135 @@ -1132,9 +1092,6 @@
   1.136    then show "P (LEAST x. P x)" and "(LEAST x. P x) \<le> k" by auto
   1.137  qed
   1.138  
   1.139 -lemmas LeastI   = wellorder_Least_lemma(1)
   1.140 -lemmas Least_le = wellorder_Least_lemma(2)
   1.141 -
   1.142  -- "The following 3 lemmas are due to Brian Huffman"
   1.143  lemma LeastI_ex: "\<exists>x. P x \<Longrightarrow> P (Least P)"
   1.144    by (erule exE) (erule LeastI)
   1.145 @@ -1174,7 +1131,7 @@
   1.146    bot_bool_eq: "bot = False"
   1.147  
   1.148  instance proof
   1.149 -qed (auto simp add: le_bool_def less_bool_def top_bool_eq bot_bool_eq)
   1.150 +qed (auto simp add: bot_bool_eq top_bool_eq less_bool_def, auto simp add: le_bool_def)
   1.151  
   1.152  end
   1.153  
   1.154 @@ -1221,10 +1178,10 @@
   1.155  
   1.156  instance "fun" :: (type, preorder) preorder proof
   1.157  qed (auto simp add: le_fun_def less_fun_def
   1.158 -  intro: order_trans order_antisym intro!: ext)
   1.159 +  intro: order_trans antisym intro!: ext)
   1.160  
   1.161  instance "fun" :: (type, order) order proof
   1.162 -qed (auto simp add: le_fun_def intro: order_antisym ext)
   1.163 +qed (auto simp add: le_fun_def intro: antisym ext)
   1.164  
   1.165  instantiation "fun" :: (type, top) top
   1.166  begin
   1.167 @@ -1257,4 +1214,42 @@
   1.168  lemma le_funD: "f \<le> g \<Longrightarrow> f x \<le> g x"
   1.169    unfolding le_fun_def by simp
   1.170  
   1.171 +
   1.172 +subsection {* Name duplicates *}
   1.173 +
   1.174 +lemmas order_eq_refl = preorder_class.eq_refl
   1.175 +lemmas order_less_irrefl = preorder_class.less_irrefl
   1.176 +lemmas order_less_imp_le = preorder_class.less_imp_le
   1.177 +lemmas order_less_not_sym = preorder_class.less_not_sym
   1.178 +lemmas order_less_asym = preorder_class.less_asym
   1.179 +lemmas order_less_trans = preorder_class.less_trans
   1.180 +lemmas order_le_less_trans = preorder_class.le_less_trans
   1.181 +lemmas order_less_le_trans = preorder_class.less_le_trans
   1.182 +lemmas order_less_imp_not_less = preorder_class.less_imp_not_less
   1.183 +lemmas order_less_imp_triv = preorder_class.less_imp_triv
   1.184 +lemmas order_less_asym' = preorder_class.less_asym'
   1.185 +
   1.186 +lemmas order_less_le = order_class.less_le
   1.187 +lemmas order_le_less = order_class.le_less
   1.188 +lemmas order_le_imp_less_or_eq = order_class.le_imp_less_or_eq
   1.189 +lemmas order_less_imp_not_eq = order_class.less_imp_not_eq
   1.190 +lemmas order_less_imp_not_eq2 = order_class.less_imp_not_eq2
   1.191 +lemmas order_neq_le_trans = order_class.neq_le_trans
   1.192 +lemmas order_le_neq_trans = order_class.le_neq_trans
   1.193 +lemmas order_antisym = order_class.antisym
   1.194 +lemmas order_eq_iff = order_class.eq_iff
   1.195 +lemmas order_antisym_conv = order_class.antisym_conv
   1.196 +
   1.197 +lemmas linorder_linear = linorder_class.linear
   1.198 +lemmas linorder_less_linear = linorder_class.less_linear
   1.199 +lemmas linorder_le_less_linear = linorder_class.le_less_linear
   1.200 +lemmas linorder_le_cases = linorder_class.le_cases
   1.201 +lemmas linorder_not_less = linorder_class.not_less
   1.202 +lemmas linorder_not_le = linorder_class.not_le
   1.203 +lemmas linorder_neq_iff = linorder_class.neq_iff
   1.204 +lemmas linorder_neqE = linorder_class.neqE
   1.205 +lemmas linorder_antisym_conv1 = linorder_class.antisym_conv1
   1.206 +lemmas linorder_antisym_conv2 = linorder_class.antisym_conv2
   1.207 +lemmas linorder_antisym_conv3 = linorder_class.antisym_conv3
   1.208 +
   1.209  end