src/HOL/Orderings.thy
 author haftmann Fri Jul 20 14:28:25 2007 +0200 (2007-07-20) changeset 23881 851c74f1bb69 parent 23417 42c1a89b45c1 child 23948 261bd4678076 permissions -rw-r--r--
moved class ord from Orderings.thy to HOL.thy
 nipkow@15524 ` 1` ```(* Title: HOL/Orderings.thy ``` nipkow@15524 ` 2` ``` ID: \$Id\$ ``` nipkow@15524 ` 3` ``` Author: Tobias Nipkow, Markus Wenzel, and Larry Paulson ``` nipkow@15524 ` 4` ```*) ``` nipkow@15524 ` 5` haftmann@21329 ` 6` ```header {* Syntactic and abstract orders *} ``` nipkow@15524 ` 7` nipkow@15524 ` 8` ```theory Orderings ``` haftmann@23881 ` 9` ```imports Set Fun ``` haftmann@23263 ` 10` ```uses ``` haftmann@23263 ` 11` ``` (*"~~/src/Provers/quasi.ML"*) ``` haftmann@23263 ` 12` ``` "~~/src/Provers/order.ML" ``` nipkow@15524 ` 13` ```begin ``` nipkow@15524 ` 14` haftmann@22841 ` 15` ```subsection {* Partial orders *} ``` nipkow@15524 ` 16` haftmann@22841 ` 17` ```class order = ord + ``` haftmann@22316 ` 18` ``` assumes less_le: "x \ y \ x \ y \ x \ y" ``` haftmann@22384 ` 19` ``` and order_refl [iff]: "x \ x" ``` haftmann@22384 ` 20` ``` and order_trans: "x \ y \ y \ z \ x \ z" ``` haftmann@22841 ` 21` ``` assumes antisym: "x \ y \ y \ x \ x = y" ``` haftmann@22841 ` 22` haftmann@21248 ` 23` ```begin ``` haftmann@21248 ` 24` nipkow@15524 ` 25` ```text {* Reflexivity. *} ``` nipkow@15524 ` 26` haftmann@22841 ` 27` ```lemma eq_refl: "x = y \ x \<^loc>\ y" ``` nipkow@15524 ` 28` ``` -- {* This form is useful with the classical reasoner. *} ``` nipkow@23212 ` 29` ```by (erule ssubst) (rule order_refl) ``` nipkow@15524 ` 30` haftmann@22841 ` 31` ```lemma less_irrefl [iff]: "\ x \<^loc>< x" ``` nipkow@23212 ` 32` ```by (simp add: less_le) ``` nipkow@15524 ` 33` haftmann@22841 ` 34` ```lemma le_less: "x \<^loc>\ y \ x \<^loc>< y \ x = y" ``` nipkow@15524 ` 35` ``` -- {* NOT suitable for iff, since it can cause PROOF FAILED. *} ``` nipkow@23212 ` 36` ```by (simp add: less_le) blast ``` nipkow@15524 ` 37` haftmann@22841 ` 38` ```lemma le_imp_less_or_eq: "x \<^loc>\ y \ x \<^loc>< y \ x = y" ``` nipkow@23212 ` 39` ```unfolding less_le by blast ``` nipkow@15524 ` 40` haftmann@22841 ` 41` ```lemma less_imp_le: "x \<^loc>< y \ x \<^loc>\ y" ``` nipkow@23212 ` 42` ```unfolding less_le by blast ``` haftmann@21248 ` 43` haftmann@22841 ` 44` ```lemma less_imp_neq: "x \<^loc>< y \ x \ y" ``` nipkow@23212 ` 45` ```by (erule contrapos_pn, erule subst, rule less_irrefl) ``` haftmann@21329 ` 46` haftmann@21329 ` 47` haftmann@21329 ` 48` ```text {* Useful for simplification, but too risky to include by default. *} ``` haftmann@21329 ` 49` haftmann@22841 ` 50` ```lemma less_imp_not_eq: "x \<^loc>< y \ (x = y) \ False" ``` nipkow@23212 ` 51` ```by auto ``` haftmann@21329 ` 52` haftmann@22841 ` 53` ```lemma less_imp_not_eq2: "x \<^loc>< y \ (y = x) \ False" ``` nipkow@23212 ` 54` ```by auto ``` haftmann@21329 ` 55` haftmann@21329 ` 56` haftmann@21329 ` 57` ```text {* Transitivity rules for calculational reasoning *} ``` haftmann@21329 ` 58` haftmann@22841 ` 59` ```lemma neq_le_trans: "a \ b \ a \<^loc>\ b \ a \<^loc>< b" ``` nipkow@23212 ` 60` ```by (simp add: less_le) ``` haftmann@21329 ` 61` haftmann@22841 ` 62` ```lemma le_neq_trans: "a \<^loc>\ b \ a \ b \ a \<^loc>< b" ``` nipkow@23212 ` 63` ```by (simp add: less_le) ``` haftmann@21329 ` 64` nipkow@15524 ` 65` nipkow@15524 ` 66` ```text {* Asymmetry. *} ``` nipkow@15524 ` 67` haftmann@22841 ` 68` ```lemma less_not_sym: "x \<^loc>< y \ \ (y \<^loc>< x)" ``` nipkow@23212 ` 69` ```by (simp add: less_le antisym) ``` nipkow@15524 ` 70` haftmann@22841 ` 71` ```lemma less_asym: "x \<^loc>< y \ (\ P \ y \<^loc>< x) \ P" ``` nipkow@23212 ` 72` ```by (drule less_not_sym, erule contrapos_np) simp ``` nipkow@15524 ` 73` haftmann@22841 ` 74` ```lemma eq_iff: "x = y \ x \<^loc>\ y \ y \<^loc>\ x" ``` nipkow@23212 ` 75` ```by (blast intro: antisym) ``` nipkow@15524 ` 76` haftmann@22841 ` 77` ```lemma antisym_conv: "y \<^loc>\ x \ x \<^loc>\ y \ x = y" ``` nipkow@23212 ` 78` ```by (blast intro: antisym) ``` nipkow@15524 ` 79` haftmann@22841 ` 80` ```lemma less_imp_neq: "x \<^loc>< y \ x \ y" ``` nipkow@23212 ` 81` ```by (erule contrapos_pn, erule subst, rule less_irrefl) ``` haftmann@21248 ` 82` haftmann@21083 ` 83` nipkow@15524 ` 84` ```text {* Transitivity. *} ``` nipkow@15524 ` 85` haftmann@22841 ` 86` ```lemma less_trans: "x \<^loc>< y \ y \<^loc>< z \ x \<^loc>< z" ``` nipkow@23212 ` 87` ```by (simp add: less_le) (blast intro: order_trans antisym) ``` nipkow@15524 ` 88` haftmann@22841 ` 89` ```lemma le_less_trans: "x \<^loc>\ y \ y \<^loc>< z \ x \<^loc>< z" ``` nipkow@23212 ` 90` ```by (simp add: less_le) (blast intro: order_trans antisym) ``` nipkow@15524 ` 91` haftmann@22841 ` 92` ```lemma less_le_trans: "x \<^loc>< y \ y \<^loc>\ z \ x \<^loc>< z" ``` nipkow@23212 ` 93` ```by (simp add: less_le) (blast intro: order_trans antisym) ``` nipkow@15524 ` 94` nipkow@15524 ` 95` nipkow@15524 ` 96` ```text {* Useful for simplification, but too risky to include by default. *} ``` nipkow@15524 ` 97` haftmann@22841 ` 98` ```lemma less_imp_not_less: "x \<^loc>< y \ (\ y \<^loc>< x) \ True" ``` nipkow@23212 ` 99` ```by (blast elim: less_asym) ``` nipkow@15524 ` 100` haftmann@22841 ` 101` ```lemma less_imp_triv: "x \<^loc>< y \ (y \<^loc>< x \ P) \ True" ``` nipkow@23212 ` 102` ```by (blast elim: less_asym) ``` nipkow@15524 ` 103` haftmann@21248 ` 104` haftmann@21083 ` 105` ```text {* Transitivity rules for calculational reasoning *} ``` nipkow@15524 ` 106` haftmann@22841 ` 107` ```lemma less_asym': "a \<^loc>< b \ b \<^loc>< a \ P" ``` nipkow@23212 ` 108` ```by (rule less_asym) ``` haftmann@21248 ` 109` haftmann@22916 ` 110` haftmann@22916 ` 111` ```text {* Reverse order *} ``` haftmann@22916 ` 112` haftmann@22916 ` 113` ```lemma order_reverse: ``` haftmann@23018 ` 114` ``` "order (\x y. y \<^loc>\ x) (\x y. y \<^loc>< x)" ``` nipkow@23212 ` 115` ```by unfold_locales ``` nipkow@23212 ` 116` ``` (simp add: less_le, auto intro: antisym order_trans) ``` haftmann@22916 ` 117` haftmann@21248 ` 118` ```end ``` nipkow@15524 ` 119` haftmann@21329 ` 120` haftmann@21329 ` 121` ```subsection {* Linear (total) orders *} ``` haftmann@21329 ` 122` haftmann@22316 ` 123` ```class linorder = order + ``` haftmann@21216 ` 124` ``` assumes linear: "x \ y \ y \ x" ``` haftmann@21248 ` 125` ```begin ``` haftmann@21248 ` 126` haftmann@22841 ` 127` ```lemma less_linear: "x \<^loc>< y \ x = y \ y \<^loc>< x" ``` nipkow@23212 ` 128` ```unfolding less_le using less_le linear by blast ``` haftmann@21248 ` 129` haftmann@22841 ` 130` ```lemma le_less_linear: "x \<^loc>\ y \ y \<^loc>< x" ``` nipkow@23212 ` 131` ```by (simp add: le_less less_linear) ``` haftmann@21248 ` 132` haftmann@21248 ` 133` ```lemma le_cases [case_names le ge]: ``` haftmann@22841 ` 134` ``` "(x \<^loc>\ y \ P) \ (y \<^loc>\ x \ P) \ P" ``` nipkow@23212 ` 135` ```using linear by blast ``` haftmann@21248 ` 136` haftmann@22384 ` 137` ```lemma linorder_cases [case_names less equal greater]: ``` nipkow@23212 ` 138` ``` "(x \<^loc>< y \ P) \ (x = y \ P) \ (y \<^loc>< x \ P) \ P" ``` nipkow@23212 ` 139` ```using less_linear by blast ``` haftmann@21248 ` 140` haftmann@22841 ` 141` ```lemma not_less: "\ x \<^loc>< y \ y \<^loc>\ x" ``` nipkow@23212 ` 142` ```apply (simp add: less_le) ``` nipkow@23212 ` 143` ```using linear apply (blast intro: antisym) ``` nipkow@23212 ` 144` ```done ``` nipkow@23212 ` 145` nipkow@23212 ` 146` ```lemma not_less_iff_gr_or_eq: ``` nipkow@23212 ` 147` ``` "\(x \<^loc>< y) \ (x \<^loc>> y | x = y)" ``` nipkow@23212 ` 148` ```apply(simp add:not_less le_less) ``` nipkow@23212 ` 149` ```apply blast ``` nipkow@23212 ` 150` ```done ``` nipkow@15524 ` 151` haftmann@22841 ` 152` ```lemma not_le: "\ x \<^loc>\ y \ y \<^loc>< x" ``` nipkow@23212 ` 153` ```apply (simp add: less_le) ``` nipkow@23212 ` 154` ```using linear apply (blast intro: antisym) ``` nipkow@23212 ` 155` ```done ``` nipkow@15524 ` 156` haftmann@22841 ` 157` ```lemma neq_iff: "x \ y \ x \<^loc>< y \ y \<^loc>< x" ``` nipkow@23212 ` 158` ```by (cut_tac x = x and y = y in less_linear, auto) ``` nipkow@15524 ` 159` haftmann@22841 ` 160` ```lemma neqE: "x \ y \ (x \<^loc>< y \ R) \ (y \<^loc>< x \ R) \ R" ``` nipkow@23212 ` 161` ```by (simp add: neq_iff) blast ``` nipkow@15524 ` 162` haftmann@22841 ` 163` ```lemma antisym_conv1: "\ x \<^loc>< y \ x \<^loc>\ y \ x = y" ``` nipkow@23212 ` 164` ```by (blast intro: antisym dest: not_less [THEN iffD1]) ``` nipkow@15524 ` 165` haftmann@22841 ` 166` ```lemma antisym_conv2: "x \<^loc>\ y \ \ x \<^loc>< y \ x = y" ``` nipkow@23212 ` 167` ```by (blast intro: antisym dest: not_less [THEN iffD1]) ``` nipkow@15524 ` 168` haftmann@22841 ` 169` ```lemma antisym_conv3: "\ y \<^loc>< x \ \ x \<^loc>< y \ x = y" ``` nipkow@23212 ` 170` ```by (blast intro: antisym dest: not_less [THEN iffD1]) ``` nipkow@15524 ` 171` paulson@16796 ` 172` ```text{*Replacing the old Nat.leI*} ``` haftmann@22841 ` 173` ```lemma leI: "\ x \<^loc>< y \ y \<^loc>\ x" ``` nipkow@23212 ` 174` ```unfolding not_less . ``` paulson@16796 ` 175` haftmann@22841 ` 176` ```lemma leD: "y \<^loc>\ x \ \ x \<^loc>< y" ``` nipkow@23212 ` 177` ```unfolding not_less . ``` paulson@16796 ` 178` paulson@16796 ` 179` ```(*FIXME inappropriate name (or delete altogether)*) ``` haftmann@22841 ` 180` ```lemma not_leE: "\ y \<^loc>\ x \ x \<^loc>< y" ``` nipkow@23212 ` 181` ```unfolding not_le . ``` haftmann@21248 ` 182` haftmann@22916 ` 183` haftmann@22916 ` 184` ```text {* Reverse order *} ``` haftmann@22916 ` 185` haftmann@22916 ` 186` ```lemma linorder_reverse: ``` haftmann@23018 ` 187` ``` "linorder (\x y. y \<^loc>\ x) (\x y. y \<^loc>< x)" ``` nipkow@23212 ` 188` ```by unfold_locales ``` nipkow@23212 ` 189` ``` (simp add: less_le, auto intro: antisym order_trans simp add: linear) ``` haftmann@22916 ` 190` haftmann@22916 ` 191` haftmann@23881 ` 192` ```text {* min/max *} ``` haftmann@23881 ` 193` haftmann@23881 ` 194` ```text {* for historic reasons, definitions are done in context ord *} ``` haftmann@23881 ` 195` haftmann@23881 ` 196` ```definition (in ord) ``` haftmann@23881 ` 197` ``` min :: "'a \ 'a \ 'a" where ``` haftmann@23881 ` 198` ``` "min a b = (if a \<^loc>\ b then a else b)" ``` haftmann@23881 ` 199` haftmann@23881 ` 200` ```definition (in ord) ``` haftmann@23881 ` 201` ``` max :: "'a \ 'a \ 'a" where ``` haftmann@23881 ` 202` ``` "max a b = (if a \<^loc>\ b then b else a)" ``` haftmann@23881 ` 203` haftmann@23881 ` 204` ```lemmas (in -) min_def [code func, code unfold, code inline del] = min_def [folded ord_class.min] ``` haftmann@23881 ` 205` ```lemmas (in -) max_def [code func, code unfold, code inline del] = max_def [folded ord_class.max] ``` haftmann@22384 ` 206` haftmann@21383 ` 207` ```lemma min_le_iff_disj: ``` haftmann@22841 ` 208` ``` "min x y \<^loc>\ z \ x \<^loc>\ z \ y \<^loc>\ z" ``` nipkow@23212 ` 209` ```unfolding min_def using linear by (auto intro: order_trans) ``` haftmann@21383 ` 210` haftmann@21383 ` 211` ```lemma le_max_iff_disj: ``` haftmann@22841 ` 212` ``` "z \<^loc>\ max x y \ z \<^loc>\ x \ z \<^loc>\ y" ``` nipkow@23212 ` 213` ```unfolding max_def using linear by (auto intro: order_trans) ``` haftmann@21383 ` 214` haftmann@21383 ` 215` ```lemma min_less_iff_disj: ``` haftmann@22841 ` 216` ``` "min x y \<^loc>< z \ x \<^loc>< z \ y \<^loc>< z" ``` nipkow@23212 ` 217` ```unfolding min_def le_less using less_linear by (auto intro: less_trans) ``` haftmann@21383 ` 218` haftmann@21383 ` 219` ```lemma less_max_iff_disj: ``` haftmann@22841 ` 220` ``` "z \<^loc>< max x y \ z \<^loc>< x \ z \<^loc>< y" ``` nipkow@23212 ` 221` ```unfolding max_def le_less using less_linear by (auto intro: less_trans) ``` haftmann@21383 ` 222` haftmann@21383 ` 223` ```lemma min_less_iff_conj [simp]: ``` haftmann@22841 ` 224` ``` "z \<^loc>< min x y \ z \<^loc>< x \ z \<^loc>< y" ``` nipkow@23212 ` 225` ```unfolding min_def le_less using less_linear by (auto intro: less_trans) ``` haftmann@21383 ` 226` haftmann@21383 ` 227` ```lemma max_less_iff_conj [simp]: ``` haftmann@22841 ` 228` ``` "max x y \<^loc>< z \ x \<^loc>< z \ y \<^loc>< z" ``` nipkow@23212 ` 229` ```unfolding max_def le_less using less_linear by (auto intro: less_trans) ``` haftmann@21383 ` 230` haftmann@21383 ` 231` ```lemma split_min: ``` haftmann@22841 ` 232` ``` "P (min i j) \ (i \<^loc>\ j \ P i) \ (\ i \<^loc>\ j \ P j)" ``` nipkow@23212 ` 233` ```by (simp add: min_def) ``` haftmann@21383 ` 234` haftmann@21383 ` 235` ```lemma split_max: ``` haftmann@22841 ` 236` ``` "P (max i j) \ (i \<^loc>\ j \ P j) \ (\ i \<^loc>\ j \ P i)" ``` nipkow@23212 ` 237` ```by (simp add: max_def) ``` haftmann@21383 ` 238` haftmann@21248 ` 239` ```end ``` haftmann@21248 ` 240` haftmann@22916 ` 241` ```subsection {* Name duplicates -- including min/max interpretation *} ``` haftmann@21248 ` 242` haftmann@22384 ` 243` ```lemmas order_less_le = less_le ``` haftmann@22841 ` 244` ```lemmas order_eq_refl = order_class.eq_refl ``` haftmann@22841 ` 245` ```lemmas order_less_irrefl = order_class.less_irrefl ``` haftmann@22841 ` 246` ```lemmas order_le_less = order_class.le_less ``` haftmann@22841 ` 247` ```lemmas order_le_imp_less_or_eq = order_class.le_imp_less_or_eq ``` haftmann@22841 ` 248` ```lemmas order_less_imp_le = order_class.less_imp_le ``` haftmann@22841 ` 249` ```lemmas order_less_imp_not_eq = order_class.less_imp_not_eq ``` haftmann@22841 ` 250` ```lemmas order_less_imp_not_eq2 = order_class.less_imp_not_eq2 ``` haftmann@22841 ` 251` ```lemmas order_neq_le_trans = order_class.neq_le_trans ``` haftmann@22841 ` 252` ```lemmas order_le_neq_trans = order_class.le_neq_trans ``` haftmann@22316 ` 253` haftmann@22384 ` 254` ```lemmas order_antisym = antisym ``` haftmann@22316 ` 255` ```lemmas order_less_not_sym = order_class.less_not_sym ``` haftmann@22316 ` 256` ```lemmas order_less_asym = order_class.less_asym ``` haftmann@22316 ` 257` ```lemmas order_eq_iff = order_class.eq_iff ``` haftmann@22316 ` 258` ```lemmas order_antisym_conv = order_class.antisym_conv ``` haftmann@22316 ` 259` ```lemmas order_less_trans = order_class.less_trans ``` haftmann@22316 ` 260` ```lemmas order_le_less_trans = order_class.le_less_trans ``` haftmann@22316 ` 261` ```lemmas order_less_le_trans = order_class.less_le_trans ``` haftmann@22316 ` 262` ```lemmas order_less_imp_not_less = order_class.less_imp_not_less ``` haftmann@22316 ` 263` ```lemmas order_less_imp_triv = order_class.less_imp_triv ``` haftmann@22316 ` 264` ```lemmas order_less_asym' = order_class.less_asym' ``` haftmann@22316 ` 265` haftmann@22384 ` 266` ```lemmas linorder_linear = linear ``` haftmann@22316 ` 267` ```lemmas linorder_less_linear = linorder_class.less_linear ``` haftmann@22316 ` 268` ```lemmas linorder_le_less_linear = linorder_class.le_less_linear ``` haftmann@22316 ` 269` ```lemmas linorder_le_cases = linorder_class.le_cases ``` haftmann@22316 ` 270` ```lemmas linorder_not_less = linorder_class.not_less ``` haftmann@22316 ` 271` ```lemmas linorder_not_le = linorder_class.not_le ``` haftmann@22316 ` 272` ```lemmas linorder_neq_iff = linorder_class.neq_iff ``` haftmann@22316 ` 273` ```lemmas linorder_neqE = linorder_class.neqE ``` haftmann@22316 ` 274` ```lemmas linorder_antisym_conv1 = linorder_class.antisym_conv1 ``` haftmann@22316 ` 275` ```lemmas linorder_antisym_conv2 = linorder_class.antisym_conv2 ``` haftmann@22316 ` 276` ```lemmas linorder_antisym_conv3 = linorder_class.antisym_conv3 ``` paulson@16796 ` 277` haftmann@23087 ` 278` ```lemmas min_le_iff_disj = linorder_class.min_le_iff_disj [folded ord_class.min] ``` haftmann@23087 ` 279` ```lemmas le_max_iff_disj = linorder_class.le_max_iff_disj [folded ord_class.max] ``` haftmann@23087 ` 280` ```lemmas min_less_iff_disj = linorder_class.min_less_iff_disj [folded ord_class.min] ``` haftmann@23087 ` 281` ```lemmas less_max_iff_disj = linorder_class.less_max_iff_disj [folded ord_class.max] ``` haftmann@23087 ` 282` ```lemmas min_less_iff_conj [simp] = linorder_class.min_less_iff_conj [folded ord_class.min] ``` haftmann@23087 ` 283` ```lemmas max_less_iff_conj [simp] = linorder_class.max_less_iff_conj [folded ord_class.max] ``` haftmann@23087 ` 284` ```lemmas split_min = linorder_class.split_min [folded ord_class.min] ``` haftmann@23087 ` 285` ```lemmas split_max = linorder_class.split_max [folded ord_class.max] ``` haftmann@22916 ` 286` haftmann@21083 ` 287` haftmann@21083 ` 288` ```subsection {* Reasoning tools setup *} ``` haftmann@21083 ` 289` haftmann@21091 ` 290` ```ML {* ``` haftmann@21091 ` 291` ```local ``` haftmann@21091 ` 292` haftmann@21091 ` 293` ```fun decomp_gen sort thy (Trueprop \$ t) = ``` haftmann@21248 ` 294` ``` let ``` haftmann@21248 ` 295` ``` fun of_sort t = ``` haftmann@21248 ` 296` ``` let ``` haftmann@21248 ` 297` ``` val T = type_of t ``` haftmann@21248 ` 298` ``` in ``` haftmann@21091 ` 299` ``` (* exclude numeric types: linear arithmetic subsumes transitivity *) ``` haftmann@21248 ` 300` ``` T <> HOLogic.natT andalso T <> HOLogic.intT ``` haftmann@21248 ` 301` ``` andalso T <> HOLogic.realT andalso Sign.of_sort thy (T, sort) ``` haftmann@21248 ` 302` ``` end; ``` haftmann@22916 ` 303` ``` fun dec (Const (@{const_name Not}, _) \$ t) = (case dec t ``` haftmann@21248 ` 304` ``` of NONE => NONE ``` haftmann@21248 ` 305` ``` | SOME (t1, rel, t2) => SOME (t1, "~" ^ rel, t2)) ``` haftmann@22916 ` 306` ``` | dec (Const (@{const_name "op ="}, _) \$ t1 \$ t2) = ``` haftmann@21248 ` 307` ``` if of_sort t1 ``` haftmann@21248 ` 308` ``` then SOME (t1, "=", t2) ``` haftmann@21248 ` 309` ``` else NONE ``` haftmann@23881 ` 310` ``` | dec (Const (@{const_name HOL.less_eq}, _) \$ t1 \$ t2) = ``` haftmann@21248 ` 311` ``` if of_sort t1 ``` haftmann@21248 ` 312` ``` then SOME (t1, "<=", t2) ``` haftmann@21248 ` 313` ``` else NONE ``` haftmann@23881 ` 314` ``` | dec (Const (@{const_name HOL.less}, _) \$ t1 \$ t2) = ``` haftmann@21248 ` 315` ``` if of_sort t1 ``` haftmann@21248 ` 316` ``` then SOME (t1, "<", t2) ``` haftmann@21248 ` 317` ``` else NONE ``` haftmann@21248 ` 318` ``` | dec _ = NONE; ``` haftmann@21091 ` 319` ``` in dec t end; ``` haftmann@21091 ` 320` haftmann@21091 ` 321` ```in ``` haftmann@21091 ` 322` haftmann@22841 ` 323` ```(* sorry - there is no preorder class ``` haftmann@21248 ` 324` ```structure Quasi_Tac = Quasi_Tac_Fun ( ``` haftmann@21248 ` 325` ```struct ``` haftmann@21248 ` 326` ``` val le_trans = thm "order_trans"; ``` haftmann@21248 ` 327` ``` val le_refl = thm "order_refl"; ``` haftmann@21248 ` 328` ``` val eqD1 = thm "order_eq_refl"; ``` haftmann@21248 ` 329` ``` val eqD2 = thm "sym" RS thm "order_eq_refl"; ``` haftmann@21248 ` 330` ``` val less_reflE = thm "order_less_irrefl" RS thm "notE"; ``` haftmann@21248 ` 331` ``` val less_imp_le = thm "order_less_imp_le"; ``` haftmann@21248 ` 332` ``` val le_neq_trans = thm "order_le_neq_trans"; ``` haftmann@21248 ` 333` ``` val neq_le_trans = thm "order_neq_le_trans"; ``` haftmann@21248 ` 334` ``` val less_imp_neq = thm "less_imp_neq"; ``` haftmann@22738 ` 335` ``` val decomp_trans = decomp_gen ["Orderings.preorder"]; ``` haftmann@22738 ` 336` ``` val decomp_quasi = decomp_gen ["Orderings.preorder"]; ``` haftmann@22841 ` 337` ```end);*) ``` haftmann@21091 ` 338` haftmann@21091 ` 339` ```structure Order_Tac = Order_Tac_Fun ( ``` haftmann@21248 ` 340` ```struct ``` haftmann@21248 ` 341` ``` val less_reflE = thm "order_less_irrefl" RS thm "notE"; ``` haftmann@21248 ` 342` ``` val le_refl = thm "order_refl"; ``` haftmann@21248 ` 343` ``` val less_imp_le = thm "order_less_imp_le"; ``` haftmann@21248 ` 344` ``` val not_lessI = thm "linorder_not_less" RS thm "iffD2"; ``` haftmann@21248 ` 345` ``` val not_leI = thm "linorder_not_le" RS thm "iffD2"; ``` haftmann@21248 ` 346` ``` val not_lessD = thm "linorder_not_less" RS thm "iffD1"; ``` haftmann@21248 ` 347` ``` val not_leD = thm "linorder_not_le" RS thm "iffD1"; ``` haftmann@21248 ` 348` ``` val eqI = thm "order_antisym"; ``` haftmann@21248 ` 349` ``` val eqD1 = thm "order_eq_refl"; ``` haftmann@21248 ` 350` ``` val eqD2 = thm "sym" RS thm "order_eq_refl"; ``` haftmann@21248 ` 351` ``` val less_trans = thm "order_less_trans"; ``` haftmann@21248 ` 352` ``` val less_le_trans = thm "order_less_le_trans"; ``` haftmann@21248 ` 353` ``` val le_less_trans = thm "order_le_less_trans"; ``` haftmann@21248 ` 354` ``` val le_trans = thm "order_trans"; ``` haftmann@21248 ` 355` ``` val le_neq_trans = thm "order_le_neq_trans"; ``` haftmann@21248 ` 356` ``` val neq_le_trans = thm "order_neq_le_trans"; ``` haftmann@21248 ` 357` ``` val less_imp_neq = thm "less_imp_neq"; ``` haftmann@21248 ` 358` ``` val eq_neq_eq_imp_neq = thm "eq_neq_eq_imp_neq"; ``` haftmann@21248 ` 359` ``` val not_sym = thm "not_sym"; ``` haftmann@21248 ` 360` ``` val decomp_part = decomp_gen ["Orderings.order"]; ``` haftmann@21248 ` 361` ``` val decomp_lin = decomp_gen ["Orderings.linorder"]; ``` haftmann@21248 ` 362` ```end); ``` haftmann@21091 ` 363` haftmann@21091 ` 364` ```end; ``` haftmann@21091 ` 365` ```*} ``` haftmann@21091 ` 366` haftmann@21083 ` 367` ```setup {* ``` haftmann@21083 ` 368` ```let ``` haftmann@21083 ` 369` haftmann@21083 ` 370` ```fun prp t thm = (#prop (rep_thm thm) = t); ``` nipkow@15524 ` 371` haftmann@21083 ` 372` ```fun prove_antisym_le sg ss ((le as Const(_,T)) \$ r \$ s) = ``` haftmann@21083 ` 373` ``` let val prems = prems_of_ss ss; ``` haftmann@22916 ` 374` ``` val less = Const (@{const_name less}, T); ``` haftmann@21083 ` 375` ``` val t = HOLogic.mk_Trueprop(le \$ s \$ r); ``` haftmann@21083 ` 376` ``` in case find_first (prp t) prems of ``` haftmann@21083 ` 377` ``` NONE => ``` haftmann@21083 ` 378` ``` let val t = HOLogic.mk_Trueprop(HOLogic.Not \$ (less \$ r \$ s)) ``` haftmann@21083 ` 379` ``` in case find_first (prp t) prems of ``` haftmann@21083 ` 380` ``` NONE => NONE ``` haftmann@22738 ` 381` ``` | SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_antisym_conv1})) ``` haftmann@21083 ` 382` ``` end ``` haftmann@22738 ` 383` ``` | SOME thm => SOME(mk_meta_eq(thm RS @{thm order_antisym_conv})) ``` haftmann@21083 ` 384` ``` end ``` haftmann@21083 ` 385` ``` handle THM _ => NONE; ``` nipkow@15524 ` 386` haftmann@21083 ` 387` ```fun prove_antisym_less sg ss (NotC \$ ((less as Const(_,T)) \$ r \$ s)) = ``` haftmann@21083 ` 388` ``` let val prems = prems_of_ss ss; ``` haftmann@22916 ` 389` ``` val le = Const (@{const_name less_eq}, T); ``` haftmann@21083 ` 390` ``` val t = HOLogic.mk_Trueprop(le \$ r \$ s); ``` haftmann@21083 ` 391` ``` in case find_first (prp t) prems of ``` haftmann@21083 ` 392` ``` NONE => ``` haftmann@21083 ` 393` ``` let val t = HOLogic.mk_Trueprop(NotC \$ (less \$ s \$ r)) ``` haftmann@21083 ` 394` ``` in case find_first (prp t) prems of ``` haftmann@21083 ` 395` ``` NONE => NONE ``` haftmann@22738 ` 396` ``` | SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_antisym_conv3})) ``` haftmann@21083 ` 397` ``` end ``` haftmann@22738 ` 398` ``` | SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_antisym_conv2})) ``` haftmann@21083 ` 399` ``` end ``` haftmann@21083 ` 400` ``` handle THM _ => NONE; ``` nipkow@15524 ` 401` haftmann@21248 ` 402` ```fun add_simprocs procs thy = ``` haftmann@21248 ` 403` ``` (Simplifier.change_simpset_of thy (fn ss => ss ``` haftmann@21248 ` 404` ``` addsimprocs (map (fn (name, raw_ts, proc) => ``` haftmann@21248 ` 405` ``` Simplifier.simproc thy name raw_ts proc)) procs); thy); ``` haftmann@21248 ` 406` ```fun add_solver name tac thy = ``` haftmann@21248 ` 407` ``` (Simplifier.change_simpset_of thy (fn ss => ss addSolver ``` haftmann@21248 ` 408` ``` (mk_solver name (K tac))); thy); ``` haftmann@21083 ` 409` haftmann@21083 ` 410` ```in ``` haftmann@21248 ` 411` ``` add_simprocs [ ``` haftmann@21248 ` 412` ``` ("antisym le", ["(x::'a::order) <= y"], prove_antisym_le), ``` haftmann@21248 ` 413` ``` ("antisym less", ["~ (x::'a::linorder) < y"], prove_antisym_less) ``` haftmann@21248 ` 414` ``` ] ``` haftmann@21248 ` 415` ``` #> add_solver "Trans_linear" Order_Tac.linear_tac ``` haftmann@21248 ` 416` ``` #> add_solver "Trans_partial" Order_Tac.partial_tac ``` haftmann@21248 ` 417` ``` (* Adding the transitivity reasoners also as safe solvers showed a slight ``` haftmann@21248 ` 418` ``` speed up, but the reasoning strength appears to be not higher (at least ``` haftmann@21248 ` 419` ``` no breaking of additional proofs in the entire HOL distribution, as ``` haftmann@21248 ` 420` ``` of 5 March 2004, was observed). *) ``` haftmann@21083 ` 421` ```end ``` haftmann@21083 ` 422` ```*} ``` nipkow@15524 ` 423` nipkow@15524 ` 424` haftmann@21083 ` 425` ```subsection {* Bounded quantifiers *} ``` haftmann@21083 ` 426` haftmann@21083 ` 427` ```syntax ``` wenzelm@21180 ` 428` ``` "_All_less" :: "[idt, 'a, bool] => bool" ("(3ALL _<_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 429` ``` "_Ex_less" :: "[idt, 'a, bool] => bool" ("(3EX _<_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 430` ``` "_All_less_eq" :: "[idt, 'a, bool] => bool" ("(3ALL _<=_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 431` ``` "_Ex_less_eq" :: "[idt, 'a, bool] => bool" ("(3EX _<=_./ _)" [0, 0, 10] 10) ``` haftmann@21083 ` 432` wenzelm@21180 ` 433` ``` "_All_greater" :: "[idt, 'a, bool] => bool" ("(3ALL _>_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 434` ``` "_Ex_greater" :: "[idt, 'a, bool] => bool" ("(3EX _>_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 435` ``` "_All_greater_eq" :: "[idt, 'a, bool] => bool" ("(3ALL _>=_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 436` ``` "_Ex_greater_eq" :: "[idt, 'a, bool] => bool" ("(3EX _>=_./ _)" [0, 0, 10] 10) ``` haftmann@21083 ` 437` haftmann@21083 ` 438` ```syntax (xsymbols) ``` wenzelm@21180 ` 439` ``` "_All_less" :: "[idt, 'a, bool] => bool" ("(3\_<_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 440` ``` "_Ex_less" :: "[idt, 'a, bool] => bool" ("(3\_<_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 441` ``` "_All_less_eq" :: "[idt, 'a, bool] => bool" ("(3\_\_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 442` ``` "_Ex_less_eq" :: "[idt, 'a, bool] => bool" ("(3\_\_./ _)" [0, 0, 10] 10) ``` haftmann@21083 ` 443` wenzelm@21180 ` 444` ``` "_All_greater" :: "[idt, 'a, bool] => bool" ("(3\_>_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 445` ``` "_Ex_greater" :: "[idt, 'a, bool] => bool" ("(3\_>_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 446` ``` "_All_greater_eq" :: "[idt, 'a, bool] => bool" ("(3\_\_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 447` ``` "_Ex_greater_eq" :: "[idt, 'a, bool] => bool" ("(3\_\_./ _)" [0, 0, 10] 10) ``` haftmann@21083 ` 448` haftmann@21083 ` 449` ```syntax (HOL) ``` wenzelm@21180 ` 450` ``` "_All_less" :: "[idt, 'a, bool] => bool" ("(3! _<_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 451` ``` "_Ex_less" :: "[idt, 'a, bool] => bool" ("(3? _<_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 452` ``` "_All_less_eq" :: "[idt, 'a, bool] => bool" ("(3! _<=_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 453` ``` "_Ex_less_eq" :: "[idt, 'a, bool] => bool" ("(3? _<=_./ _)" [0, 0, 10] 10) ``` haftmann@21083 ` 454` haftmann@21083 ` 455` ```syntax (HTML output) ``` wenzelm@21180 ` 456` ``` "_All_less" :: "[idt, 'a, bool] => bool" ("(3\_<_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 457` ``` "_Ex_less" :: "[idt, 'a, bool] => bool" ("(3\_<_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 458` ``` "_All_less_eq" :: "[idt, 'a, bool] => bool" ("(3\_\_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 459` ``` "_Ex_less_eq" :: "[idt, 'a, bool] => bool" ("(3\_\_./ _)" [0, 0, 10] 10) ``` haftmann@21083 ` 460` wenzelm@21180 ` 461` ``` "_All_greater" :: "[idt, 'a, bool] => bool" ("(3\_>_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 462` ``` "_Ex_greater" :: "[idt, 'a, bool] => bool" ("(3\_>_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 463` ``` "_All_greater_eq" :: "[idt, 'a, bool] => bool" ("(3\_\_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 464` ``` "_Ex_greater_eq" :: "[idt, 'a, bool] => bool" ("(3\_\_./ _)" [0, 0, 10] 10) ``` haftmann@21083 ` 465` haftmann@21083 ` 466` ```translations ``` haftmann@21083 ` 467` ``` "ALL x "ALL x. x < y \ P" ``` haftmann@21083 ` 468` ``` "EX x "EX x. x < y \ P" ``` haftmann@21083 ` 469` ``` "ALL x<=y. P" => "ALL x. x <= y \ P" ``` haftmann@21083 ` 470` ``` "EX x<=y. P" => "EX x. x <= y \ P" ``` haftmann@21083 ` 471` ``` "ALL x>y. P" => "ALL x. x > y \ P" ``` haftmann@21083 ` 472` ``` "EX x>y. P" => "EX x. x > y \ P" ``` haftmann@21083 ` 473` ``` "ALL x>=y. P" => "ALL x. x >= y \ P" ``` haftmann@21083 ` 474` ``` "EX x>=y. P" => "EX x. x >= y \ P" ``` haftmann@21083 ` 475` haftmann@21083 ` 476` ```print_translation {* ``` haftmann@21083 ` 477` ```let ``` haftmann@22916 ` 478` ``` val All_binder = Syntax.binder_name @{const_syntax All}; ``` haftmann@22916 ` 479` ``` val Ex_binder = Syntax.binder_name @{const_syntax Ex}; ``` wenzelm@22377 ` 480` ``` val impl = @{const_syntax "op -->"}; ``` wenzelm@22377 ` 481` ``` val conj = @{const_syntax "op &"}; ``` haftmann@22916 ` 482` ``` val less = @{const_syntax less}; ``` haftmann@22916 ` 483` ``` val less_eq = @{const_syntax less_eq}; ``` wenzelm@21180 ` 484` wenzelm@21180 ` 485` ``` val trans = ``` wenzelm@21524 ` 486` ``` [((All_binder, impl, less), ("_All_less", "_All_greater")), ``` wenzelm@21524 ` 487` ``` ((All_binder, impl, less_eq), ("_All_less_eq", "_All_greater_eq")), ``` wenzelm@21524 ` 488` ``` ((Ex_binder, conj, less), ("_Ex_less", "_Ex_greater")), ``` wenzelm@21524 ` 489` ``` ((Ex_binder, conj, less_eq), ("_Ex_less_eq", "_Ex_greater_eq"))]; ``` wenzelm@21180 ` 490` krauss@22344 ` 491` ``` fun matches_bound v t = ``` krauss@22344 ` 492` ``` case t of (Const ("_bound", _) \$ Free (v', _)) => (v = v') ``` krauss@22344 ` 493` ``` | _ => false ``` krauss@22344 ` 494` ``` fun contains_var v = Term.exists_subterm (fn Free (x, _) => x = v | _ => false) ``` krauss@22344 ` 495` ``` fun mk v c n P = Syntax.const c \$ Syntax.mark_bound v \$ n \$ P ``` wenzelm@21180 ` 496` wenzelm@21180 ` 497` ``` fun tr' q = (q, ``` wenzelm@21180 ` 498` ``` fn [Const ("_bound", _) \$ Free (v, _), Const (c, _) \$ (Const (d, _) \$ t \$ u) \$ P] => ``` wenzelm@21180 ` 499` ``` (case AList.lookup (op =) trans (q, c, d) of ``` wenzelm@21180 ` 500` ``` NONE => raise Match ``` wenzelm@21180 ` 501` ``` | SOME (l, g) => ``` krauss@22344 ` 502` ``` if matches_bound v t andalso not (contains_var v u) then mk v l u P ``` krauss@22344 ` 503` ``` else if matches_bound v u andalso not (contains_var v t) then mk v g t P ``` krauss@22344 ` 504` ``` else raise Match) ``` wenzelm@21180 ` 505` ``` | _ => raise Match); ``` wenzelm@21524 ` 506` ```in [tr' All_binder, tr' Ex_binder] end ``` haftmann@21083 ` 507` ```*} ``` haftmann@21083 ` 508` haftmann@21083 ` 509` haftmann@21383 ` 510` ```subsection {* Transitivity reasoning *} ``` haftmann@21383 ` 511` haftmann@21383 ` 512` ```lemma ord_le_eq_trans: "a <= b ==> b = c ==> a <= c" ``` nipkow@23212 ` 513` ```by (rule subst) ``` haftmann@21383 ` 514` haftmann@21383 ` 515` ```lemma ord_eq_le_trans: "a = b ==> b <= c ==> a <= c" ``` nipkow@23212 ` 516` ```by (rule ssubst) ``` haftmann@21383 ` 517` haftmann@21383 ` 518` ```lemma ord_less_eq_trans: "a < b ==> b = c ==> a < c" ``` nipkow@23212 ` 519` ```by (rule subst) ``` haftmann@21383 ` 520` haftmann@21383 ` 521` ```lemma ord_eq_less_trans: "a = b ==> b < c ==> a < c" ``` nipkow@23212 ` 522` ```by (rule ssubst) ``` haftmann@21383 ` 523` haftmann@21383 ` 524` ```lemma order_less_subst2: "(a::'a::order) < b ==> f b < (c::'c::order) ==> ``` haftmann@21383 ` 525` ``` (!!x y. x < y ==> f x < f y) ==> f a < c" ``` haftmann@21383 ` 526` ```proof - ``` haftmann@21383 ` 527` ``` assume r: "!!x y. x < y ==> f x < f y" ``` haftmann@21383 ` 528` ``` assume "a < b" hence "f a < f b" by (rule r) ``` haftmann@21383 ` 529` ``` also assume "f b < c" ``` haftmann@21383 ` 530` ``` finally (order_less_trans) show ?thesis . ``` haftmann@21383 ` 531` ```qed ``` haftmann@21383 ` 532` haftmann@21383 ` 533` ```lemma order_less_subst1: "(a::'a::order) < f b ==> (b::'b::order) < c ==> ``` haftmann@21383 ` 534` ``` (!!x y. x < y ==> f x < f y) ==> a < f c" ``` haftmann@21383 ` 535` ```proof - ``` haftmann@21383 ` 536` ``` assume r: "!!x y. x < y ==> f x < f y" ``` haftmann@21383 ` 537` ``` assume "a < f b" ``` haftmann@21383 ` 538` ``` also assume "b < c" hence "f b < f c" by (rule r) ``` haftmann@21383 ` 539` ``` finally (order_less_trans) show ?thesis . ``` haftmann@21383 ` 540` ```qed ``` haftmann@21383 ` 541` haftmann@21383 ` 542` ```lemma order_le_less_subst2: "(a::'a::order) <= b ==> f b < (c::'c::order) ==> ``` haftmann@21383 ` 543` ``` (!!x y. x <= y ==> f x <= f y) ==> f a < c" ``` haftmann@21383 ` 544` ```proof - ``` haftmann@21383 ` 545` ``` assume r: "!!x y. x <= y ==> f x <= f y" ``` haftmann@21383 ` 546` ``` assume "a <= b" hence "f a <= f b" by (rule r) ``` haftmann@21383 ` 547` ``` also assume "f b < c" ``` haftmann@21383 ` 548` ``` finally (order_le_less_trans) show ?thesis . ``` haftmann@21383 ` 549` ```qed ``` haftmann@21383 ` 550` haftmann@21383 ` 551` ```lemma order_le_less_subst1: "(a::'a::order) <= f b ==> (b::'b::order) < c ==> ``` haftmann@21383 ` 552` ``` (!!x y. x < y ==> f x < f y) ==> a < f c" ``` haftmann@21383 ` 553` ```proof - ``` haftmann@21383 ` 554` ``` assume r: "!!x y. x < y ==> f x < f y" ``` haftmann@21383 ` 555` ``` assume "a <= f b" ``` haftmann@21383 ` 556` ``` also assume "b < c" hence "f b < f c" by (rule r) ``` haftmann@21383 ` 557` ``` finally (order_le_less_trans) show ?thesis . ``` haftmann@21383 ` 558` ```qed ``` haftmann@21383 ` 559` haftmann@21383 ` 560` ```lemma order_less_le_subst2: "(a::'a::order) < b ==> f b <= (c::'c::order) ==> ``` haftmann@21383 ` 561` ``` (!!x y. x < y ==> f x < f y) ==> f a < c" ``` haftmann@21383 ` 562` ```proof - ``` haftmann@21383 ` 563` ``` assume r: "!!x y. x < y ==> f x < f y" ``` haftmann@21383 ` 564` ``` assume "a < b" hence "f a < f b" by (rule r) ``` haftmann@21383 ` 565` ``` also assume "f b <= c" ``` haftmann@21383 ` 566` ``` finally (order_less_le_trans) show ?thesis . ``` haftmann@21383 ` 567` ```qed ``` haftmann@21383 ` 568` haftmann@21383 ` 569` ```lemma order_less_le_subst1: "(a::'a::order) < f b ==> (b::'b::order) <= c ==> ``` haftmann@21383 ` 570` ``` (!!x y. x <= y ==> f x <= f y) ==> a < f c" ``` haftmann@21383 ` 571` ```proof - ``` haftmann@21383 ` 572` ``` assume r: "!!x y. x <= y ==> f x <= f y" ``` haftmann@21383 ` 573` ``` assume "a < f b" ``` haftmann@21383 ` 574` ``` also assume "b <= c" hence "f b <= f c" by (rule r) ``` haftmann@21383 ` 575` ``` finally (order_less_le_trans) show ?thesis . ``` haftmann@21383 ` 576` ```qed ``` haftmann@21383 ` 577` haftmann@21383 ` 578` ```lemma order_subst1: "(a::'a::order) <= f b ==> (b::'b::order) <= c ==> ``` haftmann@21383 ` 579` ``` (!!x y. x <= y ==> f x <= f y) ==> a <= f c" ``` haftmann@21383 ` 580` ```proof - ``` haftmann@21383 ` 581` ``` assume r: "!!x y. x <= y ==> f x <= f y" ``` haftmann@21383 ` 582` ``` assume "a <= f b" ``` haftmann@21383 ` 583` ``` also assume "b <= c" hence "f b <= f c" by (rule r) ``` haftmann@21383 ` 584` ``` finally (order_trans) show ?thesis . ``` haftmann@21383 ` 585` ```qed ``` haftmann@21383 ` 586` haftmann@21383 ` 587` ```lemma order_subst2: "(a::'a::order) <= b ==> f b <= (c::'c::order) ==> ``` haftmann@21383 ` 588` ``` (!!x y. x <= y ==> f x <= f y) ==> f a <= c" ``` haftmann@21383 ` 589` ```proof - ``` haftmann@21383 ` 590` ``` assume r: "!!x y. x <= y ==> f x <= f y" ``` haftmann@21383 ` 591` ``` assume "a <= b" hence "f a <= f b" by (rule r) ``` haftmann@21383 ` 592` ``` also assume "f b <= c" ``` haftmann@21383 ` 593` ``` finally (order_trans) show ?thesis . ``` haftmann@21383 ` 594` ```qed ``` haftmann@21383 ` 595` haftmann@21383 ` 596` ```lemma ord_le_eq_subst: "a <= b ==> f b = c ==> ``` haftmann@21383 ` 597` ``` (!!x y. x <= y ==> f x <= f y) ==> f a <= c" ``` haftmann@21383 ` 598` ```proof - ``` haftmann@21383 ` 599` ``` assume r: "!!x y. x <= y ==> f x <= f y" ``` haftmann@21383 ` 600` ``` assume "a <= b" hence "f a <= f b" by (rule r) ``` haftmann@21383 ` 601` ``` also assume "f b = c" ``` haftmann@21383 ` 602` ``` finally (ord_le_eq_trans) show ?thesis . ``` haftmann@21383 ` 603` ```qed ``` haftmann@21383 ` 604` haftmann@21383 ` 605` ```lemma ord_eq_le_subst: "a = f b ==> b <= c ==> ``` haftmann@21383 ` 606` ``` (!!x y. x <= y ==> f x <= f y) ==> a <= f c" ``` haftmann@21383 ` 607` ```proof - ``` haftmann@21383 ` 608` ``` assume r: "!!x y. x <= y ==> f x <= f y" ``` haftmann@21383 ` 609` ``` assume "a = f b" ``` haftmann@21383 ` 610` ``` also assume "b <= c" hence "f b <= f c" by (rule r) ``` haftmann@21383 ` 611` ``` finally (ord_eq_le_trans) show ?thesis . ``` haftmann@21383 ` 612` ```qed ``` haftmann@21383 ` 613` haftmann@21383 ` 614` ```lemma ord_less_eq_subst: "a < b ==> f b = c ==> ``` haftmann@21383 ` 615` ``` (!!x y. x < y ==> f x < f y) ==> f a < c" ``` haftmann@21383 ` 616` ```proof - ``` haftmann@21383 ` 617` ``` assume r: "!!x y. x < y ==> f x < f y" ``` haftmann@21383 ` 618` ``` assume "a < b" hence "f a < f b" by (rule r) ``` haftmann@21383 ` 619` ``` also assume "f b = c" ``` haftmann@21383 ` 620` ``` finally (ord_less_eq_trans) show ?thesis . ``` haftmann@21383 ` 621` ```qed ``` haftmann@21383 ` 622` haftmann@21383 ` 623` ```lemma ord_eq_less_subst: "a = f b ==> b < c ==> ``` haftmann@21383 ` 624` ``` (!!x y. x < y ==> f x < f y) ==> a < f c" ``` haftmann@21383 ` 625` ```proof - ``` haftmann@21383 ` 626` ``` assume r: "!!x y. x < y ==> f x < f y" ``` haftmann@21383 ` 627` ``` assume "a = f b" ``` haftmann@21383 ` 628` ``` also assume "b < c" hence "f b < f c" by (rule r) ``` haftmann@21383 ` 629` ``` finally (ord_eq_less_trans) show ?thesis . ``` haftmann@21383 ` 630` ```qed ``` haftmann@21383 ` 631` haftmann@21383 ` 632` ```text {* ``` haftmann@21383 ` 633` ``` Note that this list of rules is in reverse order of priorities. ``` haftmann@21383 ` 634` ```*} ``` haftmann@21383 ` 635` haftmann@21383 ` 636` ```lemmas order_trans_rules [trans] = ``` haftmann@21383 ` 637` ``` order_less_subst2 ``` haftmann@21383 ` 638` ``` order_less_subst1 ``` haftmann@21383 ` 639` ``` order_le_less_subst2 ``` haftmann@21383 ` 640` ``` order_le_less_subst1 ``` haftmann@21383 ` 641` ``` order_less_le_subst2 ``` haftmann@21383 ` 642` ``` order_less_le_subst1 ``` haftmann@21383 ` 643` ``` order_subst2 ``` haftmann@21383 ` 644` ``` order_subst1 ``` haftmann@21383 ` 645` ``` ord_le_eq_subst ``` haftmann@21383 ` 646` ``` ord_eq_le_subst ``` haftmann@21383 ` 647` ``` ord_less_eq_subst ``` haftmann@21383 ` 648` ``` ord_eq_less_subst ``` haftmann@21383 ` 649` ``` forw_subst ``` haftmann@21383 ` 650` ``` back_subst ``` haftmann@21383 ` 651` ``` rev_mp ``` haftmann@21383 ` 652` ``` mp ``` haftmann@21383 ` 653` ``` order_neq_le_trans ``` haftmann@21383 ` 654` ``` order_le_neq_trans ``` haftmann@21383 ` 655` ``` order_less_trans ``` haftmann@21383 ` 656` ``` order_less_asym' ``` haftmann@21383 ` 657` ``` order_le_less_trans ``` haftmann@21383 ` 658` ``` order_less_le_trans ``` haftmann@21383 ` 659` ``` order_trans ``` haftmann@21383 ` 660` ``` order_antisym ``` haftmann@21383 ` 661` ``` ord_le_eq_trans ``` haftmann@21383 ` 662` ``` ord_eq_le_trans ``` haftmann@21383 ` 663` ``` ord_less_eq_trans ``` haftmann@21383 ` 664` ``` ord_eq_less_trans ``` haftmann@21383 ` 665` ``` trans ``` haftmann@21383 ` 666` haftmann@21083 ` 667` wenzelm@21180 ` 668` ```(* FIXME cleanup *) ``` wenzelm@21180 ` 669` haftmann@21083 ` 670` ```text {* These support proving chains of decreasing inequalities ``` haftmann@21083 ` 671` ``` a >= b >= c ... in Isar proofs. *} ``` haftmann@21083 ` 672` haftmann@21083 ` 673` ```lemma xt1: ``` haftmann@21083 ` 674` ``` "a = b ==> b > c ==> a > c" ``` haftmann@21083 ` 675` ``` "a > b ==> b = c ==> a > c" ``` haftmann@21083 ` 676` ``` "a = b ==> b >= c ==> a >= c" ``` haftmann@21083 ` 677` ``` "a >= b ==> b = c ==> a >= c" ``` haftmann@21083 ` 678` ``` "(x::'a::order) >= y ==> y >= x ==> x = y" ``` haftmann@21083 ` 679` ``` "(x::'a::order) >= y ==> y >= z ==> x >= z" ``` haftmann@21083 ` 680` ``` "(x::'a::order) > y ==> y >= z ==> x > z" ``` haftmann@21083 ` 681` ``` "(x::'a::order) >= y ==> y > z ==> x > z" ``` wenzelm@23417 ` 682` ``` "(a::'a::order) > b ==> b > a ==> P" ``` haftmann@21083 ` 683` ``` "(x::'a::order) > y ==> y > z ==> x > z" ``` haftmann@21083 ` 684` ``` "(a::'a::order) >= b ==> a ~= b ==> a > b" ``` haftmann@21083 ` 685` ``` "(a::'a::order) ~= b ==> a >= b ==> a > b" ``` haftmann@21083 ` 686` ``` "a = f b ==> b > c ==> (!!x y. x > y ==> f x > f y) ==> a > f c" ``` haftmann@21083 ` 687` ``` "a > b ==> f b = c ==> (!!x y. x > y ==> f x > f y) ==> f a > c" ``` haftmann@21083 ` 688` ``` "a = f b ==> b >= c ==> (!!x y. x >= y ==> f x >= f y) ==> a >= f c" ``` haftmann@21083 ` 689` ``` "a >= b ==> f b = c ==> (!! x y. x >= y ==> f x >= f y) ==> f a >= c" ``` haftmann@21083 ` 690` ```by auto ``` haftmann@21083 ` 691` haftmann@21083 ` 692` ```lemma xt2: ``` haftmann@21083 ` 693` ``` "(a::'a::order) >= f b ==> b >= c ==> (!!x y. x >= y ==> f x >= f y) ==> a >= f c" ``` haftmann@21083 ` 694` ```by (subgoal_tac "f b >= f c", force, force) ``` haftmann@21083 ` 695` haftmann@21083 ` 696` ```lemma xt3: "(a::'a::order) >= b ==> (f b::'b::order) >= c ==> ``` haftmann@21083 ` 697` ``` (!!x y. x >= y ==> f x >= f y) ==> f a >= c" ``` haftmann@21083 ` 698` ```by (subgoal_tac "f a >= f b", force, force) ``` haftmann@21083 ` 699` haftmann@21083 ` 700` ```lemma xt4: "(a::'a::order) > f b ==> (b::'b::order) >= c ==> ``` haftmann@21083 ` 701` ``` (!!x y. x >= y ==> f x >= f y) ==> a > f c" ``` haftmann@21083 ` 702` ```by (subgoal_tac "f b >= f c", force, force) ``` haftmann@21083 ` 703` haftmann@21083 ` 704` ```lemma xt5: "(a::'a::order) > b ==> (f b::'b::order) >= c==> ``` haftmann@21083 ` 705` ``` (!!x y. x > y ==> f x > f y) ==> f a > c" ``` haftmann@21083 ` 706` ```by (subgoal_tac "f a > f b", force, force) ``` haftmann@21083 ` 707` haftmann@21083 ` 708` ```lemma xt6: "(a::'a::order) >= f b ==> b > c ==> ``` haftmann@21083 ` 709` ``` (!!x y. x > y ==> f x > f y) ==> a > f c" ``` haftmann@21083 ` 710` ```by (subgoal_tac "f b > f c", force, force) ``` haftmann@21083 ` 711` haftmann@21083 ` 712` ```lemma xt7: "(a::'a::order) >= b ==> (f b::'b::order) > c ==> ``` haftmann@21083 ` 713` ``` (!!x y. x >= y ==> f x >= f y) ==> f a > c" ``` haftmann@21083 ` 714` ```by (subgoal_tac "f a >= f b", force, force) ``` haftmann@21083 ` 715` haftmann@21083 ` 716` ```lemma xt8: "(a::'a::order) > f b ==> (b::'b::order) > c ==> ``` haftmann@21083 ` 717` ``` (!!x y. x > y ==> f x > f y) ==> a > f c" ``` haftmann@21083 ` 718` ```by (subgoal_tac "f b > f c", force, force) ``` haftmann@21083 ` 719` haftmann@21083 ` 720` ```lemma xt9: "(a::'a::order) > b ==> (f b::'b::order) > c ==> ``` haftmann@21083 ` 721` ``` (!!x y. x > y ==> f x > f y) ==> f a > c" ``` haftmann@21083 ` 722` ```by (subgoal_tac "f a > f b", force, force) ``` haftmann@21083 ` 723` haftmann@21083 ` 724` ```lemmas xtrans = xt1 xt2 xt3 xt4 xt5 xt6 xt7 xt8 xt9 ``` haftmann@21083 ` 725` haftmann@21083 ` 726` ```(* ``` haftmann@21083 ` 727` ``` Since "a >= b" abbreviates "b <= a", the abbreviation "..." stands ``` haftmann@21083 ` 728` ``` for the wrong thing in an Isar proof. ``` haftmann@21083 ` 729` haftmann@21083 ` 730` ``` The extra transitivity rules can be used as follows: ``` haftmann@21083 ` 731` haftmann@21083 ` 732` ```lemma "(a::'a::order) > z" ``` haftmann@21083 ` 733` ```proof - ``` haftmann@21083 ` 734` ``` have "a >= b" (is "_ >= ?rhs") ``` haftmann@21083 ` 735` ``` sorry ``` haftmann@21083 ` 736` ``` also have "?rhs >= c" (is "_ >= ?rhs") ``` haftmann@21083 ` 737` ``` sorry ``` haftmann@21083 ` 738` ``` also (xtrans) have "?rhs = d" (is "_ = ?rhs") ``` haftmann@21083 ` 739` ``` sorry ``` haftmann@21083 ` 740` ``` also (xtrans) have "?rhs >= e" (is "_ >= ?rhs") ``` haftmann@21083 ` 741` ``` sorry ``` haftmann@21083 ` 742` ``` also (xtrans) have "?rhs > f" (is "_ > ?rhs") ``` haftmann@21083 ` 743` ``` sorry ``` haftmann@21083 ` 744` ``` also (xtrans) have "?rhs > z" ``` haftmann@21083 ` 745` ``` sorry ``` haftmann@21083 ` 746` ``` finally (xtrans) show ?thesis . ``` haftmann@21083 ` 747` ```qed ``` haftmann@21083 ` 748` haftmann@21083 ` 749` ``` Alternatively, one can use "declare xtrans [trans]" and then ``` haftmann@21083 ` 750` ``` leave out the "(xtrans)" above. ``` haftmann@21083 ` 751` ```*) ``` haftmann@21083 ` 752` haftmann@21546 ` 753` ```subsection {* Order on bool *} ``` haftmann@21546 ` 754` haftmann@22886 ` 755` ```instance bool :: order ``` haftmann@21546 ` 756` ``` le_bool_def: "P \ Q \ P \ Q" ``` haftmann@21546 ` 757` ``` less_bool_def: "P < Q \ P \ Q \ P \ Q" ``` haftmann@22916 ` 758` ``` by intro_classes (auto simp add: le_bool_def less_bool_def) ``` haftmann@21546 ` 759` haftmann@21546 ` 760` ```lemma le_boolI: "(P \ Q) \ P \ Q" ``` nipkow@23212 ` 761` ```by (simp add: le_bool_def) ``` haftmann@21546 ` 762` haftmann@21546 ` 763` ```lemma le_boolI': "P \ Q \ P \ Q" ``` nipkow@23212 ` 764` ```by (simp add: le_bool_def) ``` haftmann@21546 ` 765` haftmann@21546 ` 766` ```lemma le_boolE: "P \ Q \ P \ (Q \ R) \ R" ``` nipkow@23212 ` 767` ```by (simp add: le_bool_def) ``` haftmann@21546 ` 768` haftmann@21546 ` 769` ```lemma le_boolD: "P \ Q \ P \ Q" ``` nipkow@23212 ` 770` ```by (simp add: le_bool_def) ``` haftmann@21546 ` 771` haftmann@22348 ` 772` ```lemma [code func]: ``` haftmann@22348 ` 773` ``` "False \ b \ True" ``` haftmann@22348 ` 774` ``` "True \ b \ b" ``` haftmann@22348 ` 775` ``` "False < b \ b" ``` haftmann@22348 ` 776` ``` "True < b \ False" ``` haftmann@22348 ` 777` ``` unfolding le_bool_def less_bool_def by simp_all ``` haftmann@22348 ` 778` haftmann@22424 ` 779` haftmann@23881 ` 780` ```subsection {* Order on sets *} ``` haftmann@23881 ` 781` haftmann@23881 ` 782` ```instance set :: (type) order ``` haftmann@23881 ` 783` ``` by (intro_classes, ``` haftmann@23881 ` 784` ``` (assumption | rule subset_refl subset_trans subset_antisym psubset_eq)+) ``` haftmann@23881 ` 785` haftmann@23881 ` 786` ```lemmas basic_trans_rules [trans] = ``` haftmann@23881 ` 787` ``` order_trans_rules set_rev_mp set_mp ``` haftmann@23881 ` 788` haftmann@23881 ` 789` haftmann@23881 ` 790` ```subsection {* Order on functions *} ``` haftmann@23881 ` 791` haftmann@23881 ` 792` ```instance "fun" :: (type, ord) ord ``` haftmann@23881 ` 793` ``` le_fun_def: "f \ g \ \x. f x \ g x" ``` haftmann@23881 ` 794` ``` less_fun_def: "f < g \ f \ g \ f \ g" .. ``` haftmann@23881 ` 795` haftmann@23881 ` 796` ```lemmas [code func del] = le_fun_def less_fun_def ``` haftmann@23881 ` 797` haftmann@23881 ` 798` ```instance "fun" :: (type, order) order ``` haftmann@23881 ` 799` ``` by default ``` haftmann@23881 ` 800` ``` (auto simp add: le_fun_def less_fun_def expand_fun_eq ``` haftmann@23881 ` 801` ``` intro: order_trans order_antisym) ``` haftmann@23881 ` 802` haftmann@23881 ` 803` ```lemma le_funI: "(\x. f x \ g x) \ f \ g" ``` haftmann@23881 ` 804` ``` unfolding le_fun_def by simp ``` haftmann@23881 ` 805` haftmann@23881 ` 806` ```lemma le_funE: "f \ g \ (f x \ g x \ P) \ P" ``` haftmann@23881 ` 807` ``` unfolding le_fun_def by simp ``` haftmann@23881 ` 808` haftmann@23881 ` 809` ```lemma le_funD: "f \ g \ f x \ g x" ``` haftmann@23881 ` 810` ``` unfolding le_fun_def by simp ``` haftmann@23881 ` 811` haftmann@23881 ` 812` ```text {* ``` haftmann@23881 ` 813` ``` Handy introduction and elimination rules for @{text "\"} ``` haftmann@23881 ` 814` ``` on unary and binary predicates ``` haftmann@23881 ` 815` ```*} ``` haftmann@23881 ` 816` haftmann@23881 ` 817` ```lemma predicate1I [Pure.intro!, intro!]: ``` haftmann@23881 ` 818` ``` assumes PQ: "\x. P x \ Q x" ``` haftmann@23881 ` 819` ``` shows "P \ Q" ``` haftmann@23881 ` 820` ``` apply (rule le_funI) ``` haftmann@23881 ` 821` ``` apply (rule le_boolI) ``` haftmann@23881 ` 822` ``` apply (rule PQ) ``` haftmann@23881 ` 823` ``` apply assumption ``` haftmann@23881 ` 824` ``` done ``` haftmann@23881 ` 825` haftmann@23881 ` 826` ```lemma predicate1D [Pure.dest, dest]: "P \ Q \ P x \ Q x" ``` haftmann@23881 ` 827` ``` apply (erule le_funE) ``` haftmann@23881 ` 828` ``` apply (erule le_boolE) ``` haftmann@23881 ` 829` ``` apply assumption+ ``` haftmann@23881 ` 830` ``` done ``` haftmann@23881 ` 831` haftmann@23881 ` 832` ```lemma predicate2I [Pure.intro!, intro!]: ``` haftmann@23881 ` 833` ``` assumes PQ: "\x y. P x y \ Q x y" ``` haftmann@23881 ` 834` ``` shows "P \ Q" ``` haftmann@23881 ` 835` ``` apply (rule le_funI)+ ``` haftmann@23881 ` 836` ``` apply (rule le_boolI) ``` haftmann@23881 ` 837` ``` apply (rule PQ) ``` haftmann@23881 ` 838` ``` apply assumption ``` haftmann@23881 ` 839` ``` done ``` haftmann@23881 ` 840` haftmann@23881 ` 841` ```lemma predicate2D [Pure.dest, dest]: "P \ Q \ P x y \ Q x y" ``` haftmann@23881 ` 842` ``` apply (erule le_funE)+ ``` haftmann@23881 ` 843` ``` apply (erule le_boolE) ``` haftmann@23881 ` 844` ``` apply assumption+ ``` haftmann@23881 ` 845` ``` done ``` haftmann@23881 ` 846` haftmann@23881 ` 847` ```lemma rev_predicate1D: "P x ==> P <= Q ==> Q x" ``` haftmann@23881 ` 848` ``` by (rule predicate1D) ``` haftmann@23881 ` 849` haftmann@23881 ` 850` ```lemma rev_predicate2D: "P x y ==> P <= Q ==> Q x y" ``` haftmann@23881 ` 851` ``` by (rule predicate2D) ``` haftmann@23881 ` 852` haftmann@23881 ` 853` haftmann@23881 ` 854` ```subsection {* Monotonicity, least value operator and min/max *} ``` haftmann@21083 ` 855` haftmann@21216 ` 856` ```locale mono = ``` haftmann@21216 ` 857` ``` fixes f ``` haftmann@21216 ` 858` ``` assumes mono: "A \ B \ f A \ f B" ``` haftmann@21216 ` 859` haftmann@21216 ` 860` ```lemmas monoI [intro?] = mono.intro ``` haftmann@21216 ` 861` ``` and monoD [dest?] = mono.mono ``` haftmann@21083 ` 862` haftmann@21383 ` 863` ```lemma LeastI2_order: ``` haftmann@21383 ` 864` ``` "[| P (x::'a::order); ``` haftmann@21383 ` 865` ``` !!y. P y ==> x <= y; ``` haftmann@21383 ` 866` ``` !!x. [| P x; ALL y. P y --> x \ y |] ==> Q x |] ``` haftmann@21383 ` 867` ``` ==> Q (Least P)" ``` nipkow@23212 ` 868` ```apply (unfold Least_def) ``` nipkow@23212 ` 869` ```apply (rule theI2) ``` nipkow@23212 ` 870` ``` apply (blast intro: order_antisym)+ ``` nipkow@23212 ` 871` ```done ``` haftmann@21383 ` 872` haftmann@23881 ` 873` ```lemma Least_mono: ``` haftmann@23881 ` 874` ``` "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y ``` haftmann@23881 ` 875` ``` ==> (LEAST y. y : f ` S) = f (LEAST x. x : S)" ``` haftmann@23881 ` 876` ``` -- {* Courtesy of Stephan Merz *} ``` haftmann@23881 ` 877` ``` apply clarify ``` haftmann@23881 ` 878` ``` apply (erule_tac P = "%x. x : S" in LeastI2_order, fast) ``` haftmann@23881 ` 879` ``` apply (rule LeastI2_order) ``` haftmann@23881 ` 880` ``` apply (auto elim: monoD intro!: order_antisym) ``` haftmann@23881 ` 881` ``` done ``` haftmann@23881 ` 882` haftmann@21383 ` 883` ```lemma Least_equality: ``` nipkow@23212 ` 884` ``` "[| P (k::'a::order); !!x. P x ==> k <= x |] ==> (LEAST x. P x) = k" ``` nipkow@23212 ` 885` ```apply (simp add: Least_def) ``` nipkow@23212 ` 886` ```apply (rule the_equality) ``` nipkow@23212 ` 887` ```apply (auto intro!: order_antisym) ``` nipkow@23212 ` 888` ```done ``` haftmann@21383 ` 889` haftmann@21383 ` 890` ```lemma min_leastL: "(!!x. least <= x) ==> min least x = least" ``` nipkow@23212 ` 891` ```by (simp add: min_def) ``` haftmann@21383 ` 892` haftmann@21383 ` 893` ```lemma max_leastL: "(!!x. least <= x) ==> max least x = x" ``` nipkow@23212 ` 894` ```by (simp add: max_def) ``` haftmann@21383 ` 895` haftmann@21383 ` 896` ```lemma min_leastR: "(\x\'a\order. least \ x) \ min x least = least" ``` nipkow@23212 ` 897` ```apply (simp add: min_def) ``` nipkow@23212 ` 898` ```apply (blast intro: order_antisym) ``` nipkow@23212 ` 899` ```done ``` haftmann@21383 ` 900` haftmann@21383 ` 901` ```lemma max_leastR: "(\x\'a\order. least \ x) \ max x least = x" ``` nipkow@23212 ` 902` ```apply (simp add: max_def) ``` nipkow@23212 ` 903` ```apply (blast intro: order_antisym) ``` nipkow@23212 ` 904` ```done ``` haftmann@21383 ` 905` haftmann@21383 ` 906` ```lemma min_of_mono: ``` nipkow@23212 ` 907` ``` "(!!x y. (f x <= f y) = (x <= y)) ==> min (f m) (f n) = f (min m n)" ``` nipkow@23212 ` 908` ```by (simp add: min_def) ``` haftmann@21383 ` 909` haftmann@21383 ` 910` ```lemma max_of_mono: ``` nipkow@23212 ` 911` ``` "(!!x y. (f x <= f y) = (x <= y)) ==> max (f m) (f n) = f (max m n)" ``` nipkow@23212 ` 912` ```by (simp add: max_def) ``` haftmann@21383 ` 913` haftmann@22548 ` 914` haftmann@22548 ` 915` ```subsection {* legacy ML bindings *} ``` wenzelm@21673 ` 916` wenzelm@21673 ` 917` ```ML {* ``` haftmann@22548 ` 918` ```val monoI = @{thm monoI}; ``` haftmann@22886 ` 919` ```*} ``` wenzelm@21673 ` 920` nipkow@15524 ` 921` ```end ```