src/HOL/Orderings.thy
changeset 61076 bdc1e2f0a86a
parent 60758 d8d85a8172b5
child 61169 4de9ff3ea29a
equal deleted inserted replaced
61075:f6b0d827240e 61076:bdc1e2f0a86a
  1032 subsection \<open>Monotonicity\<close>
  1032 subsection \<open>Monotonicity\<close>
  1033 
  1033 
  1034 context order
  1034 context order
  1035 begin
  1035 begin
  1036 
  1036 
  1037 definition mono :: "('a \<Rightarrow> 'b\<Colon>order) \<Rightarrow> bool" where
  1037 definition mono :: "('a \<Rightarrow> 'b::order) \<Rightarrow> bool" where
  1038   "mono f \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> f x \<le> f y)"
  1038   "mono f \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> f x \<le> f y)"
  1039 
  1039 
  1040 lemma monoI [intro?]:
  1040 lemma monoI [intro?]:
  1041   fixes f :: "'a \<Rightarrow> 'b\<Colon>order"
  1041   fixes f :: "'a \<Rightarrow> 'b::order"
  1042   shows "(\<And>x y. x \<le> y \<Longrightarrow> f x \<le> f y) \<Longrightarrow> mono f"
  1042   shows "(\<And>x y. x \<le> y \<Longrightarrow> f x \<le> f y) \<Longrightarrow> mono f"
  1043   unfolding mono_def by iprover
  1043   unfolding mono_def by iprover
  1044 
  1044 
  1045 lemma monoD [dest?]:
  1045 lemma monoD [dest?]:
  1046   fixes f :: "'a \<Rightarrow> 'b\<Colon>order"
  1046   fixes f :: "'a \<Rightarrow> 'b::order"
  1047   shows "mono f \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
  1047   shows "mono f \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
  1048   unfolding mono_def by iprover
  1048   unfolding mono_def by iprover
  1049 
  1049 
  1050 lemma monoE:
  1050 lemma monoE:
  1051   fixes f :: "'a \<Rightarrow> 'b\<Colon>order"
  1051   fixes f :: "'a \<Rightarrow> 'b::order"
  1052   assumes "mono f"
  1052   assumes "mono f"
  1053   assumes "x \<le> y"
  1053   assumes "x \<le> y"
  1054   obtains "f x \<le> f y"
  1054   obtains "f x \<le> f y"
  1055 proof
  1055 proof
  1056   from assms show "f x \<le> f y" by (simp add: mono_def)
  1056   from assms show "f x \<le> f y" by (simp add: mono_def)
  1057 qed
  1057 qed
  1058 
  1058 
  1059 definition antimono :: "('a \<Rightarrow> 'b\<Colon>order) \<Rightarrow> bool" where
  1059 definition antimono :: "('a \<Rightarrow> 'b::order) \<Rightarrow> bool" where
  1060   "antimono f \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> f x \<ge> f y)"
  1060   "antimono f \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> f x \<ge> f y)"
  1061 
  1061 
  1062 lemma antimonoI [intro?]:
  1062 lemma antimonoI [intro?]:
  1063   fixes f :: "'a \<Rightarrow> 'b\<Colon>order"
  1063   fixes f :: "'a \<Rightarrow> 'b::order"
  1064   shows "(\<And>x y. x \<le> y \<Longrightarrow> f x \<ge> f y) \<Longrightarrow> antimono f"
  1064   shows "(\<And>x y. x \<le> y \<Longrightarrow> f x \<ge> f y) \<Longrightarrow> antimono f"
  1065   unfolding antimono_def by iprover
  1065   unfolding antimono_def by iprover
  1066 
  1066 
  1067 lemma antimonoD [dest?]:
  1067 lemma antimonoD [dest?]:
  1068   fixes f :: "'a \<Rightarrow> 'b\<Colon>order"
  1068   fixes f :: "'a \<Rightarrow> 'b::order"
  1069   shows "antimono f \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<ge> f y"
  1069   shows "antimono f \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<ge> f y"
  1070   unfolding antimono_def by iprover
  1070   unfolding antimono_def by iprover
  1071 
  1071 
  1072 lemma antimonoE:
  1072 lemma antimonoE:
  1073   fixes f :: "'a \<Rightarrow> 'b\<Colon>order"
  1073   fixes f :: "'a \<Rightarrow> 'b::order"
  1074   assumes "antimono f"
  1074   assumes "antimono f"
  1075   assumes "x \<le> y"
  1075   assumes "x \<le> y"
  1076   obtains "f x \<ge> f y"
  1076   obtains "f x \<ge> f y"
  1077 proof
  1077 proof
  1078   from assms show "f x \<ge> f y" by (simp add: antimono_def)
  1078   from assms show "f x \<ge> f y" by (simp add: antimono_def)
  1079 qed
  1079 qed
  1080 
  1080 
  1081 definition strict_mono :: "('a \<Rightarrow> 'b\<Colon>order) \<Rightarrow> bool" where
  1081 definition strict_mono :: "('a \<Rightarrow> 'b::order) \<Rightarrow> bool" where
  1082   "strict_mono f \<longleftrightarrow> (\<forall>x y. x < y \<longrightarrow> f x < f y)"
  1082   "strict_mono f \<longleftrightarrow> (\<forall>x y. x < y \<longrightarrow> f x < f y)"
  1083 
  1083 
  1084 lemma strict_monoI [intro?]:
  1084 lemma strict_monoI [intro?]:
  1085   assumes "\<And>x y. x < y \<Longrightarrow> f x < f y"
  1085   assumes "\<And>x y. x < y \<Longrightarrow> f x < f y"
  1086   shows "strict_mono f"
  1086   shows "strict_mono f"
  1110 
  1110 
  1111 context linorder
  1111 context linorder
  1112 begin
  1112 begin
  1113 
  1113 
  1114 lemma mono_invE:
  1114 lemma mono_invE:
  1115   fixes f :: "'a \<Rightarrow> 'b\<Colon>order"
  1115   fixes f :: "'a \<Rightarrow> 'b::order"
  1116   assumes "mono f"
  1116   assumes "mono f"
  1117   assumes "f x < f y"
  1117   assumes "f x < f y"
  1118   obtains "x \<le> y"
  1118   obtains "x \<le> y"
  1119 proof
  1119 proof
  1120   show "x \<le> y"
  1120   show "x \<le> y"
  1178   by (simp add: min_def)
  1178   by (simp add: min_def)
  1179 
  1179 
  1180 lemma max_absorb2: "x \<le> y \<Longrightarrow> max x y = y"
  1180 lemma max_absorb2: "x \<le> y \<Longrightarrow> max x y = y"
  1181   by (simp add: max_def)
  1181   by (simp add: max_def)
  1182 
  1182 
  1183 lemma min_absorb2: "(y\<Colon>'a\<Colon>order) \<le> x \<Longrightarrow> min x y = y"
  1183 lemma min_absorb2: "(y::'a::order) \<le> x \<Longrightarrow> min x y = y"
  1184   by (simp add:min_def)
  1184   by (simp add:min_def)
  1185 
  1185 
  1186 lemma max_absorb1: "(y\<Colon>'a\<Colon>order) \<le> x \<Longrightarrow> max x y = x"
  1186 lemma max_absorb1: "(y::'a::order) \<le> x \<Longrightarrow> max x y = x"
  1187   by (simp add: max_def)
  1187   by (simp add: max_def)
  1188 
  1188 
  1189 
  1189 
  1190 subsection \<open>(Unique) top and bottom elements\<close>
  1190 subsection \<open>(Unique) top and bottom elements\<close>
  1191 
  1191 
  1407 
  1407 
  1408 definition
  1408 definition
  1409   le_bool_def [simp]: "P \<le> Q \<longleftrightarrow> P \<longrightarrow> Q"
  1409   le_bool_def [simp]: "P \<le> Q \<longleftrightarrow> P \<longrightarrow> Q"
  1410 
  1410 
  1411 definition
  1411 definition
  1412   [simp]: "(P\<Colon>bool) < Q \<longleftrightarrow> \<not> P \<and> Q"
  1412   [simp]: "(P::bool) < Q \<longleftrightarrow> \<not> P \<and> Q"
  1413 
  1413 
  1414 definition
  1414 definition
  1415   [simp]: "\<bottom> \<longleftrightarrow> False"
  1415   [simp]: "\<bottom> \<longleftrightarrow> False"
  1416 
  1416 
  1417 definition
  1417 definition
  1455 
  1455 
  1456 definition
  1456 definition
  1457   le_fun_def: "f \<le> g \<longleftrightarrow> (\<forall>x. f x \<le> g x)"
  1457   le_fun_def: "f \<le> g \<longleftrightarrow> (\<forall>x. f x \<le> g x)"
  1458 
  1458 
  1459 definition
  1459 definition
  1460   "(f\<Colon>'a \<Rightarrow> 'b) < g \<longleftrightarrow> f \<le> g \<and> \<not> (g \<le> f)"
  1460   "(f::'a \<Rightarrow> 'b) < g \<longleftrightarrow> f \<le> g \<and> \<not> (g \<le> f)"
  1461 
  1461 
  1462 instance ..
  1462 instance ..
  1463 
  1463 
  1464 end
  1464 end
  1465 
  1465 
  1618 lemmas linorder_antisym_conv1 = linorder_class.antisym_conv1
  1618 lemmas linorder_antisym_conv1 = linorder_class.antisym_conv1
  1619 lemmas linorder_antisym_conv2 = linorder_class.antisym_conv2
  1619 lemmas linorder_antisym_conv2 = linorder_class.antisym_conv2
  1620 lemmas linorder_antisym_conv3 = linorder_class.antisym_conv3
  1620 lemmas linorder_antisym_conv3 = linorder_class.antisym_conv3
  1621 
  1621 
  1622 end
  1622 end
  1623