src/HOL/Orderings.thy
 changeset 61076 bdc1e2f0a86a parent 60758 d8d85a8172b5 child 61169 4de9ff3ea29a
equal 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`