src/HOL/Orderings.thy
 author wenzelm Thu Oct 04 20:29:42 2007 +0200 (2007-10-04) changeset 24850 0cfd722ab579 parent 24748 ee0a0eb6b738 child 24867 e5b55d7be9bb permissions -rw-r--r--
Name.uu, Name.aT;
 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/order.ML" ``` nipkow@15524 ` 12` ```begin ``` nipkow@15524 ` 13` haftmann@22841 ` 14` ```subsection {* Partial orders *} ``` nipkow@15524 ` 15` haftmann@22841 ` 16` ```class order = ord + ``` haftmann@24748 ` 17` ``` assumes less_le: "x \<^loc>< y \ x \<^loc>\ y \ x \ y" ``` haftmann@24748 ` 18` ``` and order_refl [iff]: "x \<^loc>\ x" ``` haftmann@24748 ` 19` ``` and order_trans: "x \<^loc>\ y \ y \<^loc>\ z \ x \<^loc>\ z" ``` haftmann@24748 ` 20` ``` assumes antisym: "x \<^loc>\ y \ y \<^loc>\ x \ x = y" ``` haftmann@22841 ` 21` haftmann@21248 ` 22` ```begin ``` haftmann@21248 ` 23` haftmann@24748 ` 24` ```notation (input) ``` haftmann@24748 ` 25` ``` less_eq (infix "\" 50) ``` haftmann@24748 ` 26` ```and ``` haftmann@24748 ` 27` ``` less (infix "\" 50) ``` haftmann@24748 ` 28` nipkow@15524 ` 29` ```text {* Reflexivity. *} ``` nipkow@15524 ` 30` haftmann@22841 ` 31` ```lemma eq_refl: "x = y \ x \<^loc>\ y" ``` nipkow@15524 ` 32` ``` -- {* This form is useful with the classical reasoner. *} ``` nipkow@23212 ` 33` ```by (erule ssubst) (rule order_refl) ``` nipkow@15524 ` 34` haftmann@22841 ` 35` ```lemma less_irrefl [iff]: "\ x \<^loc>< x" ``` nipkow@23212 ` 36` ```by (simp add: less_le) ``` nipkow@15524 ` 37` haftmann@22841 ` 38` ```lemma le_less: "x \<^loc>\ y \ x \<^loc>< y \ x = y" ``` nipkow@15524 ` 39` ``` -- {* NOT suitable for iff, since it can cause PROOF FAILED. *} ``` nipkow@23212 ` 40` ```by (simp add: less_le) blast ``` nipkow@15524 ` 41` haftmann@22841 ` 42` ```lemma le_imp_less_or_eq: "x \<^loc>\ y \ x \<^loc>< y \ x = y" ``` nipkow@23212 ` 43` ```unfolding less_le by blast ``` nipkow@15524 ` 44` haftmann@22841 ` 45` ```lemma less_imp_le: "x \<^loc>< y \ x \<^loc>\ y" ``` nipkow@23212 ` 46` ```unfolding less_le by blast ``` haftmann@21248 ` 47` haftmann@22841 ` 48` ```lemma less_imp_neq: "x \<^loc>< y \ x \ y" ``` nipkow@23212 ` 49` ```by (erule contrapos_pn, erule subst, rule less_irrefl) ``` haftmann@21329 ` 50` haftmann@21329 ` 51` haftmann@21329 ` 52` ```text {* Useful for simplification, but too risky to include by default. *} ``` haftmann@21329 ` 53` haftmann@22841 ` 54` ```lemma less_imp_not_eq: "x \<^loc>< y \ (x = y) \ False" ``` nipkow@23212 ` 55` ```by auto ``` haftmann@21329 ` 56` haftmann@22841 ` 57` ```lemma less_imp_not_eq2: "x \<^loc>< y \ (y = x) \ False" ``` nipkow@23212 ` 58` ```by auto ``` haftmann@21329 ` 59` haftmann@21329 ` 60` haftmann@21329 ` 61` ```text {* Transitivity rules for calculational reasoning *} ``` haftmann@21329 ` 62` haftmann@22841 ` 63` ```lemma neq_le_trans: "a \ b \ a \<^loc>\ b \ a \<^loc>< b" ``` nipkow@23212 ` 64` ```by (simp add: less_le) ``` haftmann@21329 ` 65` haftmann@22841 ` 66` ```lemma le_neq_trans: "a \<^loc>\ b \ a \ b \ a \<^loc>< b" ``` nipkow@23212 ` 67` ```by (simp add: less_le) ``` haftmann@21329 ` 68` nipkow@15524 ` 69` nipkow@15524 ` 70` ```text {* Asymmetry. *} ``` nipkow@15524 ` 71` haftmann@22841 ` 72` ```lemma less_not_sym: "x \<^loc>< y \ \ (y \<^loc>< x)" ``` nipkow@23212 ` 73` ```by (simp add: less_le antisym) ``` nipkow@15524 ` 74` haftmann@22841 ` 75` ```lemma less_asym: "x \<^loc>< y \ (\ P \ y \<^loc>< x) \ P" ``` nipkow@23212 ` 76` ```by (drule less_not_sym, erule contrapos_np) simp ``` nipkow@15524 ` 77` haftmann@22841 ` 78` ```lemma eq_iff: "x = y \ x \<^loc>\ y \ y \<^loc>\ x" ``` nipkow@23212 ` 79` ```by (blast intro: antisym) ``` nipkow@15524 ` 80` haftmann@22841 ` 81` ```lemma antisym_conv: "y \<^loc>\ x \ x \<^loc>\ y \ x = y" ``` nipkow@23212 ` 82` ```by (blast intro: antisym) ``` nipkow@15524 ` 83` haftmann@22841 ` 84` ```lemma less_imp_neq: "x \<^loc>< y \ x \ y" ``` nipkow@23212 ` 85` ```by (erule contrapos_pn, erule subst, rule less_irrefl) ``` haftmann@21248 ` 86` haftmann@21083 ` 87` nipkow@15524 ` 88` ```text {* Transitivity. *} ``` nipkow@15524 ` 89` haftmann@22841 ` 90` ```lemma less_trans: "x \<^loc>< y \ y \<^loc>< z \ x \<^loc>< z" ``` nipkow@23212 ` 91` ```by (simp add: less_le) (blast intro: order_trans antisym) ``` nipkow@15524 ` 92` haftmann@22841 ` 93` ```lemma le_less_trans: "x \<^loc>\ y \ y \<^loc>< z \ x \<^loc>< z" ``` nipkow@23212 ` 94` ```by (simp add: less_le) (blast intro: order_trans antisym) ``` nipkow@15524 ` 95` haftmann@22841 ` 96` ```lemma less_le_trans: "x \<^loc>< y \ y \<^loc>\ z \ x \<^loc>< z" ``` nipkow@23212 ` 97` ```by (simp add: less_le) (blast intro: order_trans antisym) ``` nipkow@15524 ` 98` nipkow@15524 ` 99` nipkow@15524 ` 100` ```text {* Useful for simplification, but too risky to include by default. *} ``` nipkow@15524 ` 101` haftmann@22841 ` 102` ```lemma less_imp_not_less: "x \<^loc>< y \ (\ y \<^loc>< x) \ True" ``` nipkow@23212 ` 103` ```by (blast elim: less_asym) ``` nipkow@15524 ` 104` haftmann@22841 ` 105` ```lemma less_imp_triv: "x \<^loc>< y \ (y \<^loc>< x \ P) \ True" ``` nipkow@23212 ` 106` ```by (blast elim: less_asym) ``` nipkow@15524 ` 107` haftmann@21248 ` 108` haftmann@21083 ` 109` ```text {* Transitivity rules for calculational reasoning *} ``` nipkow@15524 ` 110` haftmann@22841 ` 111` ```lemma less_asym': "a \<^loc>< b \ b \<^loc>< a \ P" ``` nipkow@23212 ` 112` ```by (rule less_asym) ``` haftmann@21248 ` 113` haftmann@22916 ` 114` haftmann@22916 ` 115` ```text {* Reverse order *} ``` haftmann@22916 ` 116` haftmann@22916 ` 117` ```lemma order_reverse: ``` haftmann@23018 ` 118` ``` "order (\x y. y \<^loc>\ x) (\x y. y \<^loc>< x)" ``` nipkow@23212 ` 119` ```by unfold_locales ``` nipkow@23212 ` 120` ``` (simp add: less_le, auto intro: antisym order_trans) ``` haftmann@22916 ` 121` haftmann@21248 ` 122` ```end ``` nipkow@15524 ` 123` haftmann@21329 ` 124` haftmann@21329 ` 125` ```subsection {* Linear (total) orders *} ``` haftmann@21329 ` 126` haftmann@22316 ` 127` ```class linorder = order + ``` haftmann@21216 ` 128` ``` assumes linear: "x \ y \ y \ x" ``` haftmann@21248 ` 129` ```begin ``` haftmann@21248 ` 130` haftmann@22841 ` 131` ```lemma less_linear: "x \<^loc>< y \ x = y \ y \<^loc>< x" ``` nipkow@23212 ` 132` ```unfolding less_le using less_le linear by blast ``` haftmann@21248 ` 133` haftmann@22841 ` 134` ```lemma le_less_linear: "x \<^loc>\ y \ y \<^loc>< x" ``` nipkow@23212 ` 135` ```by (simp add: le_less less_linear) ``` haftmann@21248 ` 136` haftmann@21248 ` 137` ```lemma le_cases [case_names le ge]: ``` haftmann@22841 ` 138` ``` "(x \<^loc>\ y \ P) \ (y \<^loc>\ x \ P) \ P" ``` nipkow@23212 ` 139` ```using linear by blast ``` haftmann@21248 ` 140` haftmann@22384 ` 141` ```lemma linorder_cases [case_names less equal greater]: ``` nipkow@23212 ` 142` ``` "(x \<^loc>< y \ P) \ (x = y \ P) \ (y \<^loc>< x \ P) \ P" ``` nipkow@23212 ` 143` ```using less_linear by blast ``` haftmann@21248 ` 144` haftmann@22841 ` 145` ```lemma not_less: "\ x \<^loc>< y \ y \<^loc>\ x" ``` nipkow@23212 ` 146` ```apply (simp add: less_le) ``` nipkow@23212 ` 147` ```using linear apply (blast intro: antisym) ``` nipkow@23212 ` 148` ```done ``` nipkow@23212 ` 149` nipkow@23212 ` 150` ```lemma not_less_iff_gr_or_eq: ``` nipkow@23212 ` 151` ``` "\(x \<^loc>< y) \ (x \<^loc>> y | x = y)" ``` nipkow@23212 ` 152` ```apply(simp add:not_less le_less) ``` nipkow@23212 ` 153` ```apply blast ``` nipkow@23212 ` 154` ```done ``` nipkow@15524 ` 155` haftmann@22841 ` 156` ```lemma not_le: "\ x \<^loc>\ y \ y \<^loc>< x" ``` nipkow@23212 ` 157` ```apply (simp add: less_le) ``` nipkow@23212 ` 158` ```using linear apply (blast intro: antisym) ``` nipkow@23212 ` 159` ```done ``` nipkow@15524 ` 160` haftmann@22841 ` 161` ```lemma neq_iff: "x \ y \ x \<^loc>< y \ y \<^loc>< x" ``` nipkow@23212 ` 162` ```by (cut_tac x = x and y = y in less_linear, auto) ``` nipkow@15524 ` 163` haftmann@22841 ` 164` ```lemma neqE: "x \ y \ (x \<^loc>< y \ R) \ (y \<^loc>< x \ R) \ R" ``` nipkow@23212 ` 165` ```by (simp add: neq_iff) blast ``` nipkow@15524 ` 166` haftmann@22841 ` 167` ```lemma antisym_conv1: "\ x \<^loc>< y \ x \<^loc>\ y \ x = y" ``` nipkow@23212 ` 168` ```by (blast intro: antisym dest: not_less [THEN iffD1]) ``` nipkow@15524 ` 169` haftmann@22841 ` 170` ```lemma antisym_conv2: "x \<^loc>\ y \ \ x \<^loc>< y \ x = y" ``` nipkow@23212 ` 171` ```by (blast intro: antisym dest: not_less [THEN iffD1]) ``` nipkow@15524 ` 172` haftmann@22841 ` 173` ```lemma antisym_conv3: "\ y \<^loc>< x \ \ x \<^loc>< y \ x = y" ``` nipkow@23212 ` 174` ```by (blast intro: antisym dest: not_less [THEN iffD1]) ``` nipkow@15524 ` 175` paulson@16796 ` 176` ```text{*Replacing the old Nat.leI*} ``` haftmann@22841 ` 177` ```lemma leI: "\ x \<^loc>< y \ y \<^loc>\ x" ``` nipkow@23212 ` 178` ```unfolding not_less . ``` paulson@16796 ` 179` haftmann@22841 ` 180` ```lemma leD: "y \<^loc>\ x \ \ x \<^loc>< y" ``` nipkow@23212 ` 181` ```unfolding not_less . ``` paulson@16796 ` 182` paulson@16796 ` 183` ```(*FIXME inappropriate name (or delete altogether)*) ``` haftmann@22841 ` 184` ```lemma not_leE: "\ y \<^loc>\ x \ x \<^loc>< y" ``` nipkow@23212 ` 185` ```unfolding not_le . ``` haftmann@21248 ` 186` haftmann@22916 ` 187` haftmann@22916 ` 188` ```text {* Reverse order *} ``` haftmann@22916 ` 189` haftmann@22916 ` 190` ```lemma linorder_reverse: ``` haftmann@23018 ` 191` ``` "linorder (\x y. y \<^loc>\ x) (\x y. y \<^loc>< x)" ``` nipkow@23212 ` 192` ```by unfold_locales ``` nipkow@23212 ` 193` ``` (simp add: less_le, auto intro: antisym order_trans simp add: linear) ``` haftmann@22916 ` 194` haftmann@22916 ` 195` haftmann@23881 ` 196` ```text {* min/max *} ``` haftmann@23881 ` 197` haftmann@23881 ` 198` ```text {* for historic reasons, definitions are done in context ord *} ``` haftmann@23881 ` 199` haftmann@23881 ` 200` ```definition (in ord) ``` haftmann@23881 ` 201` ``` min :: "'a \ 'a \ 'a" where ``` haftmann@23948 ` 202` ``` [code unfold, code inline del]: "min a b = (if a \<^loc>\ b then a else b)" ``` haftmann@23881 ` 203` haftmann@23881 ` 204` ```definition (in ord) ``` haftmann@23881 ` 205` ``` max :: "'a \ 'a \ 'a" where ``` haftmann@23948 ` 206` ``` [code unfold, code inline del]: "max a b = (if a \<^loc>\ b then b else a)" ``` haftmann@22384 ` 207` haftmann@21383 ` 208` ```lemma min_le_iff_disj: ``` haftmann@22841 ` 209` ``` "min x y \<^loc>\ z \ x \<^loc>\ z \ y \<^loc>\ z" ``` nipkow@23212 ` 210` ```unfolding min_def using linear by (auto intro: order_trans) ``` haftmann@21383 ` 211` haftmann@21383 ` 212` ```lemma le_max_iff_disj: ``` haftmann@22841 ` 213` ``` "z \<^loc>\ max x y \ z \<^loc>\ x \ z \<^loc>\ y" ``` nipkow@23212 ` 214` ```unfolding max_def using linear by (auto intro: order_trans) ``` haftmann@21383 ` 215` haftmann@21383 ` 216` ```lemma min_less_iff_disj: ``` haftmann@22841 ` 217` ``` "min x y \<^loc>< z \ x \<^loc>< z \ y \<^loc>< z" ``` nipkow@23212 ` 218` ```unfolding min_def le_less using less_linear by (auto intro: less_trans) ``` haftmann@21383 ` 219` haftmann@21383 ` 220` ```lemma less_max_iff_disj: ``` haftmann@22841 ` 221` ``` "z \<^loc>< max x y \ z \<^loc>< x \ z \<^loc>< y" ``` nipkow@23212 ` 222` ```unfolding max_def le_less using less_linear by (auto intro: less_trans) ``` haftmann@21383 ` 223` haftmann@21383 ` 224` ```lemma min_less_iff_conj [simp]: ``` haftmann@22841 ` 225` ``` "z \<^loc>< min x y \ z \<^loc>< x \ z \<^loc>< y" ``` nipkow@23212 ` 226` ```unfolding min_def le_less using less_linear by (auto intro: less_trans) ``` haftmann@21383 ` 227` haftmann@21383 ` 228` ```lemma max_less_iff_conj [simp]: ``` haftmann@22841 ` 229` ``` "max x y \<^loc>< z \ x \<^loc>< z \ y \<^loc>< z" ``` nipkow@23212 ` 230` ```unfolding max_def le_less using less_linear by (auto intro: less_trans) ``` haftmann@21383 ` 231` paulson@24286 ` 232` ```lemma split_min [noatp]: ``` haftmann@22841 ` 233` ``` "P (min i j) \ (i \<^loc>\ j \ P i) \ (\ i \<^loc>\ j \ P j)" ``` nipkow@23212 ` 234` ```by (simp add: min_def) ``` haftmann@21383 ` 235` paulson@24286 ` 236` ```lemma split_max [noatp]: ``` haftmann@22841 ` 237` ``` "P (max i j) \ (i \<^loc>\ j \ P j) \ (\ i \<^loc>\ j \ P i)" ``` nipkow@23212 ` 238` ```by (simp add: max_def) ``` haftmann@21383 ` 239` haftmann@21248 ` 240` ```end ``` haftmann@21248 ` 241` haftmann@23948 ` 242` haftmann@21083 ` 243` ```subsection {* Reasoning tools setup *} ``` haftmann@21083 ` 244` haftmann@21091 ` 245` ```ML {* ``` haftmann@21091 ` 246` ballarin@24641 ` 247` ```signature ORDERS = ``` ballarin@24641 ` 248` ```sig ``` ballarin@24641 ` 249` ``` val print_structures: Proof.context -> unit ``` ballarin@24641 ` 250` ``` val setup: theory -> theory ``` ballarin@24704 ` 251` ``` val order_tac: thm list -> Proof.context -> int -> tactic ``` ballarin@24641 ` 252` ```end; ``` haftmann@21091 ` 253` ballarin@24641 ` 254` ```structure Orders: ORDERS = ``` haftmann@21248 ` 255` ```struct ``` ballarin@24641 ` 256` ballarin@24641 ` 257` ```(** Theory and context data **) ``` ballarin@24641 ` 258` ballarin@24641 ` 259` ```fun struct_eq ((s1: string, ts1), (s2, ts2)) = ``` ballarin@24641 ` 260` ``` (s1 = s2) andalso eq_list (op aconv) (ts1, ts2); ``` ballarin@24641 ` 261` ballarin@24641 ` 262` ```structure Data = GenericDataFun ``` ballarin@24641 ` 263` ```( ``` ballarin@24641 ` 264` ``` type T = ((string * term list) * Order_Tac.less_arith) list; ``` ballarin@24641 ` 265` ``` (* Order structures: ``` ballarin@24641 ` 266` ``` identifier of the structure, list of operations and record of theorems ``` ballarin@24641 ` 267` ``` needed to set up the transitivity reasoner, ``` ballarin@24641 ` 268` ``` identifier and operations identify the structure uniquely. *) ``` ballarin@24641 ` 269` ``` val empty = []; ``` ballarin@24641 ` 270` ``` val extend = I; ``` ballarin@24641 ` 271` ``` fun merge _ = AList.join struct_eq (K fst); ``` ballarin@24641 ` 272` ```); ``` ballarin@24641 ` 273` ballarin@24641 ` 274` ```fun print_structures ctxt = ``` ballarin@24641 ` 275` ``` let ``` ballarin@24641 ` 276` ``` val structs = Data.get (Context.Proof ctxt); ``` ballarin@24641 ` 277` ``` fun pretty_term t = Pretty.block ``` ballarin@24641 ` 278` ``` [Pretty.quote (ProofContext.pretty_term ctxt t), Pretty.brk 1, ``` ballarin@24641 ` 279` ``` Pretty.str "::", Pretty.brk 1, ``` ballarin@24641 ` 280` ``` Pretty.quote (ProofContext.pretty_typ ctxt (type_of t))]; ``` ballarin@24641 ` 281` ``` fun pretty_struct ((s, ts), _) = Pretty.block ``` ballarin@24641 ` 282` ``` [Pretty.str s, Pretty.str ":", Pretty.brk 1, ``` ballarin@24641 ` 283` ``` Pretty.enclose "(" ")" (Pretty.breaks (map pretty_term ts))]; ``` ballarin@24641 ` 284` ``` in ``` ballarin@24641 ` 285` ``` Pretty.writeln (Pretty.big_list "Order structures:" (map pretty_struct structs)) ``` ballarin@24641 ` 286` ``` end; ``` ballarin@24641 ` 287` ballarin@24641 ` 288` ballarin@24641 ` 289` ```(** Method **) ``` haftmann@21091 ` 290` ballarin@24704 ` 291` ```fun struct_tac ((s, [eq, le, less]), thms) prems = ``` ballarin@24641 ` 292` ``` let ``` ballarin@24641 ` 293` ``` fun decomp thy (Trueprop \$ t) = ``` ballarin@24641 ` 294` ``` let ``` ballarin@24641 ` 295` ``` fun excluded t = ``` ballarin@24641 ` 296` ``` (* exclude numeric types: linear arithmetic subsumes transitivity *) ``` ballarin@24641 ` 297` ``` let val T = type_of t ``` ballarin@24641 ` 298` ``` in ``` ballarin@24641 ` 299` ``` T = HOLogic.natT orelse T = HOLogic.intT orelse T = HOLogic.realT ``` ballarin@24641 ` 300` ``` end; ``` ballarin@24741 ` 301` ``` fun rel (bin_op \$ t1 \$ t2) = ``` ballarin@24641 ` 302` ``` if excluded t1 then NONE ``` ballarin@24641 ` 303` ``` else if Pattern.matches thy (eq, bin_op) then SOME (t1, "=", t2) ``` ballarin@24641 ` 304` ``` else if Pattern.matches thy (le, bin_op) then SOME (t1, "<=", t2) ``` ballarin@24641 ` 305` ``` else if Pattern.matches thy (less, bin_op) then SOME (t1, "<", t2) ``` ballarin@24641 ` 306` ``` else NONE ``` ballarin@24741 ` 307` ``` | rel _ = NONE; ``` ballarin@24741 ` 308` ``` fun dec (Const (@{const_name Not}, _) \$ t) = (case rel t ``` ballarin@24741 ` 309` ``` of NONE => NONE ``` ballarin@24741 ` 310` ``` | SOME (t1, rel, t2) => SOME (t1, "~" ^ rel, t2)) ``` ballarin@24741 ` 311` ``` | dec x = rel x; ``` ballarin@24641 ` 312` ``` in dec t end; ``` ballarin@24641 ` 313` ``` in ``` ballarin@24641 ` 314` ``` case s of ``` ballarin@24704 ` 315` ``` "order" => Order_Tac.partial_tac decomp thms prems ``` ballarin@24704 ` 316` ``` | "linorder" => Order_Tac.linear_tac decomp thms prems ``` ballarin@24641 ` 317` ``` | _ => error ("Unknown kind of order `" ^ s ^ "' encountered in transitivity reasoner.") ``` ballarin@24641 ` 318` ``` end ``` ballarin@24641 ` 319` ballarin@24704 ` 320` ```fun order_tac prems ctxt = ``` ballarin@24704 ` 321` ``` FIRST' (map (fn s => CHANGED o struct_tac s prems) (Data.get (Context.Proof ctxt))); ``` ballarin@24641 ` 322` ballarin@24641 ` 323` ballarin@24641 ` 324` ```(** Attribute **) ``` ballarin@24641 ` 325` ballarin@24641 ` 326` ```fun add_struct_thm s tag = ``` ballarin@24641 ` 327` ``` Thm.declaration_attribute ``` ballarin@24641 ` 328` ``` (fn thm => Data.map (AList.map_default struct_eq (s, Order_Tac.empty TrueI) (Order_Tac.update tag thm))); ``` ballarin@24641 ` 329` ```fun del_struct s = ``` ballarin@24641 ` 330` ``` Thm.declaration_attribute ``` ballarin@24641 ` 331` ``` (fn _ => Data.map (AList.delete struct_eq s)); ``` ballarin@24641 ` 332` ballarin@24641 ` 333` ```val attribute = Attrib.syntax ``` ballarin@24641 ` 334` ``` (Scan.lift ((Args.add -- Args.name >> (fn (_, s) => SOME s) || ``` ballarin@24641 ` 335` ``` Args.del >> K NONE) --| Args.colon (* FIXME || ``` ballarin@24641 ` 336` ``` Scan.succeed true *) ) -- Scan.lift Args.name -- ``` ballarin@24641 ` 337` ``` Scan.repeat Args.term ``` ballarin@24641 ` 338` ``` >> (fn ((SOME tag, n), ts) => add_struct_thm (n, ts) tag ``` ballarin@24641 ` 339` ``` | ((NONE, n), ts) => del_struct (n, ts))); ``` ballarin@24641 ` 340` ballarin@24641 ` 341` ballarin@24641 ` 342` ```(** Diagnostic command **) ``` ballarin@24641 ` 343` ballarin@24641 ` 344` ```val print = Toplevel.unknown_context o ``` ballarin@24641 ` 345` ``` Toplevel.keep (Toplevel.node_case ``` ballarin@24641 ` 346` ``` (Context.cases (print_structures o ProofContext.init) print_structures) ``` ballarin@24641 ` 347` ``` (print_structures o Proof.context_of)); ``` ballarin@24641 ` 348` ballarin@24641 ` 349` ```val printP = ``` ballarin@24641 ` 350` ``` OuterSyntax.improper_command "print_orders" ``` ballarin@24641 ` 351` ``` "print order structures available to transitivity reasoner" OuterKeyword.diag ``` ballarin@24641 ` 352` ``` (Scan.succeed (Toplevel.no_timing o print)); ``` ballarin@24641 ` 353` ballarin@24641 ` 354` ballarin@24641 ` 355` ```(** Setup **) ``` ballarin@24641 ` 356` ballarin@24641 ` 357` ```val setup = let val _ = OuterSyntax.add_parsers [printP] in ``` ballarin@24704 ` 358` ``` Method.add_methods [("order", Method.ctxt_args (Method.SIMPLE_METHOD' o order_tac []), ``` ballarin@24641 ` 359` ``` "normalisation of algebraic structure")] #> ``` ballarin@24641 ` 360` ``` Attrib.add_attributes [("order", attribute, "theorems controlling transitivity reasoner")] ``` ballarin@24641 ` 361` ``` end; ``` haftmann@21091 ` 362` haftmann@21091 ` 363` ```end; ``` ballarin@24641 ` 364` haftmann@21091 ` 365` ```*} ``` haftmann@21091 ` 366` ballarin@24641 ` 367` ```setup Orders.setup ``` ballarin@24641 ` 368` ballarin@24641 ` 369` ballarin@24641 ` 370` ```text {* Declarations to set up transitivity reasoner of partial and linear orders. *} ``` ballarin@24641 ` 371` ballarin@24641 ` 372` ```(* The type constraint on @{term op =} below is necessary since the operation ``` ballarin@24641 ` 373` ``` is not a parameter of the locale. *) ``` ballarin@24641 ` 374` ```lemmas (in order) ``` ballarin@24641 ` 375` ``` [order add less_reflE: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 376` ``` less_irrefl [THEN notE] ``` ballarin@24641 ` 377` ```lemmas (in order) ``` ballarin@24641 ` 378` ``` [order add le_refl: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 379` ``` order_refl ``` ballarin@24641 ` 380` ```lemmas (in order) ``` ballarin@24641 ` 381` ``` [order add less_imp_le: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 382` ``` less_imp_le ``` ballarin@24641 ` 383` ```lemmas (in order) ``` ballarin@24641 ` 384` ``` [order add eqI: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 385` ``` antisym ``` ballarin@24641 ` 386` ```lemmas (in order) ``` ballarin@24641 ` 387` ``` [order add eqD1: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 388` ``` eq_refl ``` ballarin@24641 ` 389` ```lemmas (in order) ``` ballarin@24641 ` 390` ``` [order add eqD2: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 391` ``` sym [THEN eq_refl] ``` ballarin@24641 ` 392` ```lemmas (in order) ``` ballarin@24641 ` 393` ``` [order add less_trans: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 394` ``` less_trans ``` ballarin@24641 ` 395` ```lemmas (in order) ``` ballarin@24641 ` 396` ``` [order add less_le_trans: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 397` ``` less_le_trans ``` ballarin@24641 ` 398` ```lemmas (in order) ``` ballarin@24641 ` 399` ``` [order add le_less_trans: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 400` ``` le_less_trans ``` ballarin@24641 ` 401` ```lemmas (in order) ``` ballarin@24641 ` 402` ``` [order add le_trans: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 403` ``` order_trans ``` ballarin@24641 ` 404` ```lemmas (in order) ``` ballarin@24641 ` 405` ``` [order add le_neq_trans: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 406` ``` le_neq_trans ``` ballarin@24641 ` 407` ```lemmas (in order) ``` ballarin@24641 ` 408` ``` [order add neq_le_trans: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 409` ``` neq_le_trans ``` ballarin@24641 ` 410` ```lemmas (in order) ``` ballarin@24641 ` 411` ``` [order add less_imp_neq: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 412` ``` less_imp_neq ``` ballarin@24641 ` 413` ```lemmas (in order) ``` ballarin@24641 ` 414` ``` [order add eq_neq_eq_imp_neq: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 415` ``` eq_neq_eq_imp_neq ``` ballarin@24641 ` 416` ```lemmas (in order) ``` ballarin@24641 ` 417` ``` [order add not_sym: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 418` ``` not_sym ``` ballarin@24641 ` 419` ballarin@24641 ` 420` ```lemmas (in linorder) [order del: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = _ ``` ballarin@24641 ` 421` ballarin@24641 ` 422` ```lemmas (in linorder) ``` ballarin@24641 ` 423` ``` [order add less_reflE: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 424` ``` less_irrefl [THEN notE] ``` ballarin@24641 ` 425` ```lemmas (in linorder) ``` ballarin@24641 ` 426` ``` [order add le_refl: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 427` ``` order_refl ``` ballarin@24641 ` 428` ```lemmas (in linorder) ``` ballarin@24641 ` 429` ``` [order add less_imp_le: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 430` ``` less_imp_le ``` ballarin@24641 ` 431` ```lemmas (in linorder) ``` ballarin@24641 ` 432` ``` [order add not_lessI: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 433` ``` not_less [THEN iffD2] ``` ballarin@24641 ` 434` ```lemmas (in linorder) ``` ballarin@24641 ` 435` ``` [order add not_leI: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 436` ``` not_le [THEN iffD2] ``` ballarin@24641 ` 437` ```lemmas (in linorder) ``` ballarin@24641 ` 438` ``` [order add not_lessD: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 439` ``` not_less [THEN iffD1] ``` ballarin@24641 ` 440` ```lemmas (in linorder) ``` ballarin@24641 ` 441` ``` [order add not_leD: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 442` ``` not_le [THEN iffD1] ``` ballarin@24641 ` 443` ```lemmas (in linorder) ``` ballarin@24641 ` 444` ``` [order add eqI: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 445` ``` antisym ``` ballarin@24641 ` 446` ```lemmas (in linorder) ``` ballarin@24641 ` 447` ``` [order add eqD1: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 448` ``` eq_refl ``` ballarin@24641 ` 449` ```lemmas (in linorder) ``` ballarin@24641 ` 450` ``` [order add eqD2: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 451` ``` sym [THEN eq_refl] ``` ballarin@24641 ` 452` ```lemmas (in linorder) ``` ballarin@24641 ` 453` ``` [order add less_trans: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 454` ``` less_trans ``` ballarin@24641 ` 455` ```lemmas (in linorder) ``` ballarin@24641 ` 456` ``` [order add less_le_trans: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 457` ``` less_le_trans ``` ballarin@24641 ` 458` ```lemmas (in linorder) ``` ballarin@24641 ` 459` ``` [order add le_less_trans: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 460` ``` le_less_trans ``` ballarin@24641 ` 461` ```lemmas (in linorder) ``` ballarin@24641 ` 462` ``` [order add le_trans: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 463` ``` order_trans ``` ballarin@24641 ` 464` ```lemmas (in linorder) ``` ballarin@24641 ` 465` ``` [order add le_neq_trans: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 466` ``` le_neq_trans ``` ballarin@24641 ` 467` ```lemmas (in linorder) ``` ballarin@24641 ` 468` ``` [order add neq_le_trans: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 469` ``` neq_le_trans ``` ballarin@24641 ` 470` ```lemmas (in linorder) ``` ballarin@24641 ` 471` ``` [order add less_imp_neq: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 472` ``` less_imp_neq ``` ballarin@24641 ` 473` ```lemmas (in linorder) ``` ballarin@24641 ` 474` ``` [order add eq_neq_eq_imp_neq: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 475` ``` eq_neq_eq_imp_neq ``` ballarin@24641 ` 476` ```lemmas (in linorder) ``` ballarin@24641 ` 477` ``` [order add not_sym: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 478` ``` not_sym ``` ballarin@24641 ` 479` ballarin@24641 ` 480` haftmann@21083 ` 481` ```setup {* ``` haftmann@21083 ` 482` ```let ``` haftmann@21083 ` 483` haftmann@21083 ` 484` ```fun prp t thm = (#prop (rep_thm thm) = t); ``` nipkow@15524 ` 485` haftmann@21083 ` 486` ```fun prove_antisym_le sg ss ((le as Const(_,T)) \$ r \$ s) = ``` haftmann@21083 ` 487` ``` let val prems = prems_of_ss ss; ``` haftmann@22916 ` 488` ``` val less = Const (@{const_name less}, T); ``` haftmann@21083 ` 489` ``` val t = HOLogic.mk_Trueprop(le \$ s \$ r); ``` haftmann@21083 ` 490` ``` in case find_first (prp t) prems of ``` haftmann@21083 ` 491` ``` NONE => ``` haftmann@21083 ` 492` ``` let val t = HOLogic.mk_Trueprop(HOLogic.Not \$ (less \$ r \$ s)) ``` haftmann@21083 ` 493` ``` in case find_first (prp t) prems of ``` haftmann@21083 ` 494` ``` NONE => NONE ``` haftmann@24422 ` 495` ``` | SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_class.antisym_conv1})) ``` haftmann@21083 ` 496` ``` end ``` haftmann@24422 ` 497` ``` | SOME thm => SOME(mk_meta_eq(thm RS @{thm order_class.antisym_conv})) ``` haftmann@21083 ` 498` ``` end ``` haftmann@21083 ` 499` ``` handle THM _ => NONE; ``` nipkow@15524 ` 500` haftmann@21083 ` 501` ```fun prove_antisym_less sg ss (NotC \$ ((less as Const(_,T)) \$ r \$ s)) = ``` haftmann@21083 ` 502` ``` let val prems = prems_of_ss ss; ``` haftmann@22916 ` 503` ``` val le = Const (@{const_name less_eq}, T); ``` haftmann@21083 ` 504` ``` val t = HOLogic.mk_Trueprop(le \$ r \$ s); ``` haftmann@21083 ` 505` ``` in case find_first (prp t) prems of ``` haftmann@21083 ` 506` ``` NONE => ``` haftmann@21083 ` 507` ``` let val t = HOLogic.mk_Trueprop(NotC \$ (less \$ s \$ r)) ``` haftmann@21083 ` 508` ``` in case find_first (prp t) prems of ``` haftmann@21083 ` 509` ``` NONE => NONE ``` haftmann@24422 ` 510` ``` | SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_class.antisym_conv3})) ``` haftmann@21083 ` 511` ``` end ``` haftmann@24422 ` 512` ``` | SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_class.antisym_conv2})) ``` haftmann@21083 ` 513` ``` end ``` haftmann@21083 ` 514` ``` handle THM _ => NONE; ``` nipkow@15524 ` 515` haftmann@21248 ` 516` ```fun add_simprocs procs thy = ``` haftmann@21248 ` 517` ``` (Simplifier.change_simpset_of thy (fn ss => ss ``` haftmann@21248 ` 518` ``` addsimprocs (map (fn (name, raw_ts, proc) => ``` haftmann@21248 ` 519` ``` Simplifier.simproc thy name raw_ts proc)) procs); thy); ``` haftmann@21248 ` 520` ```fun add_solver name tac thy = ``` haftmann@21248 ` 521` ``` (Simplifier.change_simpset_of thy (fn ss => ss addSolver ``` ballarin@24704 ` 522` ``` (mk_solver' name (fn ss => tac (MetaSimplifier.prems_of_ss ss) (MetaSimplifier.the_context ss)))); thy); ``` haftmann@21083 ` 523` haftmann@21083 ` 524` ```in ``` haftmann@21248 ` 525` ``` add_simprocs [ ``` haftmann@21248 ` 526` ``` ("antisym le", ["(x::'a::order) <= y"], prove_antisym_le), ``` haftmann@21248 ` 527` ``` ("antisym less", ["~ (x::'a::linorder) < y"], prove_antisym_less) ``` haftmann@21248 ` 528` ``` ] ``` ballarin@24641 ` 529` ``` #> add_solver "Transitivity" Orders.order_tac ``` haftmann@21248 ` 530` ``` (* Adding the transitivity reasoners also as safe solvers showed a slight ``` haftmann@21248 ` 531` ``` speed up, but the reasoning strength appears to be not higher (at least ``` haftmann@21248 ` 532` ``` no breaking of additional proofs in the entire HOL distribution, as ``` haftmann@21248 ` 533` ``` of 5 March 2004, was observed). *) ``` haftmann@21083 ` 534` ```end ``` haftmann@21083 ` 535` ```*} ``` nipkow@15524 ` 536` nipkow@15524 ` 537` haftmann@24422 ` 538` ```subsection {* Dense orders *} ``` haftmann@24422 ` 539` haftmann@24422 ` 540` ```class dense_linear_order = linorder + ``` haftmann@24422 ` 541` ``` assumes gt_ex: "\y. x \ y" ``` haftmann@24422 ` 542` ``` and lt_ex: "\y. y \ x" ``` haftmann@24422 ` 543` ``` and dense: "x \ y \ (\z. x \ z \ z \ y)" ``` haftmann@24422 ` 544` ``` (*see further theory Dense_Linear_Order*) ``` haftmann@24422 ` 545` ballarin@24641 ` 546` haftmann@24422 ` 547` ```lemma interval_empty_iff: ``` haftmann@24422 ` 548` ``` fixes x y z :: "'a\dense_linear_order" ``` haftmann@24422 ` 549` ``` shows "{y. x < y \ y < z} = {} \ \ x < z" ``` haftmann@24422 ` 550` ``` by (auto dest: dense) ``` haftmann@24422 ` 551` haftmann@24422 ` 552` ```subsection {* Name duplicates *} ``` haftmann@24422 ` 553` haftmann@24422 ` 554` ```lemmas order_less_le = less_le ``` haftmann@24422 ` 555` ```lemmas order_eq_refl = order_class.eq_refl ``` haftmann@24422 ` 556` ```lemmas order_less_irrefl = order_class.less_irrefl ``` haftmann@24422 ` 557` ```lemmas order_le_less = order_class.le_less ``` haftmann@24422 ` 558` ```lemmas order_le_imp_less_or_eq = order_class.le_imp_less_or_eq ``` haftmann@24422 ` 559` ```lemmas order_less_imp_le = order_class.less_imp_le ``` haftmann@24422 ` 560` ```lemmas order_less_imp_not_eq = order_class.less_imp_not_eq ``` haftmann@24422 ` 561` ```lemmas order_less_imp_not_eq2 = order_class.less_imp_not_eq2 ``` haftmann@24422 ` 562` ```lemmas order_neq_le_trans = order_class.neq_le_trans ``` haftmann@24422 ` 563` ```lemmas order_le_neq_trans = order_class.le_neq_trans ``` haftmann@24422 ` 564` haftmann@24422 ` 565` ```lemmas order_antisym = antisym ``` haftmann@24422 ` 566` ```lemmas order_less_not_sym = order_class.less_not_sym ``` haftmann@24422 ` 567` ```lemmas order_less_asym = order_class.less_asym ``` haftmann@24422 ` 568` ```lemmas order_eq_iff = order_class.eq_iff ``` haftmann@24422 ` 569` ```lemmas order_antisym_conv = order_class.antisym_conv ``` haftmann@24422 ` 570` ```lemmas order_less_trans = order_class.less_trans ``` haftmann@24422 ` 571` ```lemmas order_le_less_trans = order_class.le_less_trans ``` haftmann@24422 ` 572` ```lemmas order_less_le_trans = order_class.less_le_trans ``` haftmann@24422 ` 573` ```lemmas order_less_imp_not_less = order_class.less_imp_not_less ``` haftmann@24422 ` 574` ```lemmas order_less_imp_triv = order_class.less_imp_triv ``` haftmann@24422 ` 575` ```lemmas order_less_asym' = order_class.less_asym' ``` haftmann@24422 ` 576` haftmann@24422 ` 577` ```lemmas linorder_linear = linear ``` haftmann@24422 ` 578` ```lemmas linorder_less_linear = linorder_class.less_linear ``` haftmann@24422 ` 579` ```lemmas linorder_le_less_linear = linorder_class.le_less_linear ``` haftmann@24422 ` 580` ```lemmas linorder_le_cases = linorder_class.le_cases ``` haftmann@24422 ` 581` ```lemmas linorder_not_less = linorder_class.not_less ``` haftmann@24422 ` 582` ```lemmas linorder_not_le = linorder_class.not_le ``` haftmann@24422 ` 583` ```lemmas linorder_neq_iff = linorder_class.neq_iff ``` haftmann@24422 ` 584` ```lemmas linorder_neqE = linorder_class.neqE ``` haftmann@24422 ` 585` ```lemmas linorder_antisym_conv1 = linorder_class.antisym_conv1 ``` haftmann@24422 ` 586` ```lemmas linorder_antisym_conv2 = linorder_class.antisym_conv2 ``` haftmann@24422 ` 587` ```lemmas linorder_antisym_conv3 = linorder_class.antisym_conv3 ``` haftmann@24422 ` 588` haftmann@24422 ` 589` ```lemmas min_le_iff_disj = linorder_class.min_le_iff_disj ``` haftmann@24422 ` 590` ```lemmas le_max_iff_disj = linorder_class.le_max_iff_disj ``` haftmann@24422 ` 591` ```lemmas min_less_iff_disj = linorder_class.min_less_iff_disj ``` haftmann@24422 ` 592` ```lemmas less_max_iff_disj = linorder_class.less_max_iff_disj ``` haftmann@24422 ` 593` ```lemmas min_less_iff_conj [simp] = linorder_class.min_less_iff_conj ``` haftmann@24422 ` 594` ```lemmas max_less_iff_conj [simp] = linorder_class.max_less_iff_conj ``` haftmann@24422 ` 595` ```lemmas split_min = linorder_class.split_min ``` haftmann@24422 ` 596` ```lemmas split_max = linorder_class.split_max ``` haftmann@24422 ` 597` haftmann@24422 ` 598` haftmann@21083 ` 599` ```subsection {* Bounded quantifiers *} ``` haftmann@21083 ` 600` haftmann@21083 ` 601` ```syntax ``` wenzelm@21180 ` 602` ``` "_All_less" :: "[idt, 'a, bool] => bool" ("(3ALL _<_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 603` ``` "_Ex_less" :: "[idt, 'a, bool] => bool" ("(3EX _<_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 604` ``` "_All_less_eq" :: "[idt, 'a, bool] => bool" ("(3ALL _<=_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 605` ``` "_Ex_less_eq" :: "[idt, 'a, bool] => bool" ("(3EX _<=_./ _)" [0, 0, 10] 10) ``` haftmann@21083 ` 606` wenzelm@21180 ` 607` ``` "_All_greater" :: "[idt, 'a, bool] => bool" ("(3ALL _>_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 608` ``` "_Ex_greater" :: "[idt, 'a, bool] => bool" ("(3EX _>_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 609` ``` "_All_greater_eq" :: "[idt, 'a, bool] => bool" ("(3ALL _>=_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 610` ``` "_Ex_greater_eq" :: "[idt, 'a, bool] => bool" ("(3EX _>=_./ _)" [0, 0, 10] 10) ``` haftmann@21083 ` 611` haftmann@21083 ` 612` ```syntax (xsymbols) ``` wenzelm@21180 ` 613` ``` "_All_less" :: "[idt, 'a, bool] => bool" ("(3\_<_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 614` ``` "_Ex_less" :: "[idt, 'a, bool] => bool" ("(3\_<_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 615` ``` "_All_less_eq" :: "[idt, 'a, bool] => bool" ("(3\_\_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 616` ``` "_Ex_less_eq" :: "[idt, 'a, bool] => bool" ("(3\_\_./ _)" [0, 0, 10] 10) ``` haftmann@21083 ` 617` wenzelm@21180 ` 618` ``` "_All_greater" :: "[idt, 'a, bool] => bool" ("(3\_>_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 619` ``` "_Ex_greater" :: "[idt, 'a, bool] => bool" ("(3\_>_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 620` ``` "_All_greater_eq" :: "[idt, 'a, bool] => bool" ("(3\_\_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 621` ``` "_Ex_greater_eq" :: "[idt, 'a, bool] => bool" ("(3\_\_./ _)" [0, 0, 10] 10) ``` haftmann@21083 ` 622` haftmann@21083 ` 623` ```syntax (HOL) ``` wenzelm@21180 ` 624` ``` "_All_less" :: "[idt, 'a, bool] => bool" ("(3! _<_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 625` ``` "_Ex_less" :: "[idt, 'a, bool] => bool" ("(3? _<_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 626` ``` "_All_less_eq" :: "[idt, 'a, bool] => bool" ("(3! _<=_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 627` ``` "_Ex_less_eq" :: "[idt, 'a, bool] => bool" ("(3? _<=_./ _)" [0, 0, 10] 10) ``` haftmann@21083 ` 628` haftmann@21083 ` 629` ```syntax (HTML output) ``` wenzelm@21180 ` 630` ``` "_All_less" :: "[idt, 'a, bool] => bool" ("(3\_<_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 631` ``` "_Ex_less" :: "[idt, 'a, bool] => bool" ("(3\_<_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 632` ``` "_All_less_eq" :: "[idt, 'a, bool] => bool" ("(3\_\_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 633` ``` "_Ex_less_eq" :: "[idt, 'a, bool] => bool" ("(3\_\_./ _)" [0, 0, 10] 10) ``` haftmann@21083 ` 634` wenzelm@21180 ` 635` ``` "_All_greater" :: "[idt, 'a, bool] => bool" ("(3\_>_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 636` ``` "_Ex_greater" :: "[idt, 'a, bool] => bool" ("(3\_>_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 637` ``` "_All_greater_eq" :: "[idt, 'a, bool] => bool" ("(3\_\_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 638` ``` "_Ex_greater_eq" :: "[idt, 'a, bool] => bool" ("(3\_\_./ _)" [0, 0, 10] 10) ``` haftmann@21083 ` 639` haftmann@21083 ` 640` ```translations ``` haftmann@21083 ` 641` ``` "ALL x "ALL x. x < y \ P" ``` haftmann@21083 ` 642` ``` "EX x "EX x. x < y \ P" ``` haftmann@21083 ` 643` ``` "ALL x<=y. P" => "ALL x. x <= y \ P" ``` haftmann@21083 ` 644` ``` "EX x<=y. P" => "EX x. x <= y \ P" ``` haftmann@21083 ` 645` ``` "ALL x>y. P" => "ALL x. x > y \ P" ``` haftmann@21083 ` 646` ``` "EX x>y. P" => "EX x. x > y \ P" ``` haftmann@21083 ` 647` ``` "ALL x>=y. P" => "ALL x. x >= y \ P" ``` haftmann@21083 ` 648` ``` "EX x>=y. P" => "EX x. x >= y \ P" ``` haftmann@21083 ` 649` haftmann@21083 ` 650` ```print_translation {* ``` haftmann@21083 ` 651` ```let ``` haftmann@22916 ` 652` ``` val All_binder = Syntax.binder_name @{const_syntax All}; ``` haftmann@22916 ` 653` ``` val Ex_binder = Syntax.binder_name @{const_syntax Ex}; ``` wenzelm@22377 ` 654` ``` val impl = @{const_syntax "op -->"}; ``` wenzelm@22377 ` 655` ``` val conj = @{const_syntax "op &"}; ``` haftmann@22916 ` 656` ``` val less = @{const_syntax less}; ``` haftmann@22916 ` 657` ``` val less_eq = @{const_syntax less_eq}; ``` wenzelm@21180 ` 658` wenzelm@21180 ` 659` ``` val trans = ``` wenzelm@21524 ` 660` ``` [((All_binder, impl, less), ("_All_less", "_All_greater")), ``` wenzelm@21524 ` 661` ``` ((All_binder, impl, less_eq), ("_All_less_eq", "_All_greater_eq")), ``` wenzelm@21524 ` 662` ``` ((Ex_binder, conj, less), ("_Ex_less", "_Ex_greater")), ``` wenzelm@21524 ` 663` ``` ((Ex_binder, conj, less_eq), ("_Ex_less_eq", "_Ex_greater_eq"))]; ``` wenzelm@21180 ` 664` krauss@22344 ` 665` ``` fun matches_bound v t = ``` krauss@22344 ` 666` ``` case t of (Const ("_bound", _) \$ Free (v', _)) => (v = v') ``` krauss@22344 ` 667` ``` | _ => false ``` krauss@22344 ` 668` ``` fun contains_var v = Term.exists_subterm (fn Free (x, _) => x = v | _ => false) ``` krauss@22344 ` 669` ``` fun mk v c n P = Syntax.const c \$ Syntax.mark_bound v \$ n \$ P ``` wenzelm@21180 ` 670` wenzelm@21180 ` 671` ``` fun tr' q = (q, ``` wenzelm@21180 ` 672` ``` fn [Const ("_bound", _) \$ Free (v, _), Const (c, _) \$ (Const (d, _) \$ t \$ u) \$ P] => ``` wenzelm@21180 ` 673` ``` (case AList.lookup (op =) trans (q, c, d) of ``` wenzelm@21180 ` 674` ``` NONE => raise Match ``` wenzelm@21180 ` 675` ``` | SOME (l, g) => ``` krauss@22344 ` 676` ``` if matches_bound v t andalso not (contains_var v u) then mk v l u P ``` krauss@22344 ` 677` ``` else if matches_bound v u andalso not (contains_var v t) then mk v g t P ``` krauss@22344 ` 678` ``` else raise Match) ``` wenzelm@21180 ` 679` ``` | _ => raise Match); ``` wenzelm@21524 ` 680` ```in [tr' All_binder, tr' Ex_binder] end ``` haftmann@21083 ` 681` ```*} ``` haftmann@21083 ` 682` haftmann@21083 ` 683` haftmann@21383 ` 684` ```subsection {* Transitivity reasoning *} ``` haftmann@21383 ` 685` haftmann@21383 ` 686` ```lemma ord_le_eq_trans: "a <= b ==> b = c ==> a <= c" ``` nipkow@23212 ` 687` ```by (rule subst) ``` haftmann@21383 ` 688` haftmann@21383 ` 689` ```lemma ord_eq_le_trans: "a = b ==> b <= c ==> a <= c" ``` nipkow@23212 ` 690` ```by (rule ssubst) ``` haftmann@21383 ` 691` haftmann@21383 ` 692` ```lemma ord_less_eq_trans: "a < b ==> b = c ==> a < c" ``` nipkow@23212 ` 693` ```by (rule subst) ``` haftmann@21383 ` 694` haftmann@21383 ` 695` ```lemma ord_eq_less_trans: "a = b ==> b < c ==> a < c" ``` nipkow@23212 ` 696` ```by (rule ssubst) ``` haftmann@21383 ` 697` haftmann@21383 ` 698` ```lemma order_less_subst2: "(a::'a::order) < b ==> f b < (c::'c::order) ==> ``` haftmann@21383 ` 699` ``` (!!x y. x < y ==> f x < f y) ==> f a < c" ``` haftmann@21383 ` 700` ```proof - ``` haftmann@21383 ` 701` ``` assume r: "!!x y. x < y ==> f x < f y" ``` haftmann@21383 ` 702` ``` assume "a < b" hence "f a < f b" by (rule r) ``` haftmann@21383 ` 703` ``` also assume "f b < c" ``` haftmann@21383 ` 704` ``` finally (order_less_trans) show ?thesis . ``` haftmann@21383 ` 705` ```qed ``` haftmann@21383 ` 706` haftmann@21383 ` 707` ```lemma order_less_subst1: "(a::'a::order) < f b ==> (b::'b::order) < c ==> ``` haftmann@21383 ` 708` ``` (!!x y. x < y ==> f x < f y) ==> a < f c" ``` haftmann@21383 ` 709` ```proof - ``` haftmann@21383 ` 710` ``` assume r: "!!x y. x < y ==> f x < f y" ``` haftmann@21383 ` 711` ``` assume "a < f b" ``` haftmann@21383 ` 712` ``` also assume "b < c" hence "f b < f c" by (rule r) ``` haftmann@21383 ` 713` ``` finally (order_less_trans) show ?thesis . ``` haftmann@21383 ` 714` ```qed ``` haftmann@21383 ` 715` haftmann@21383 ` 716` ```lemma order_le_less_subst2: "(a::'a::order) <= b ==> f b < (c::'c::order) ==> ``` haftmann@21383 ` 717` ``` (!!x y. x <= y ==> f x <= f y) ==> f a < c" ``` haftmann@21383 ` 718` ```proof - ``` haftmann@21383 ` 719` ``` assume r: "!!x y. x <= y ==> f x <= f y" ``` haftmann@21383 ` 720` ``` assume "a <= b" hence "f a <= f b" by (rule r) ``` haftmann@21383 ` 721` ``` also assume "f b < c" ``` haftmann@21383 ` 722` ``` finally (order_le_less_trans) show ?thesis . ``` haftmann@21383 ` 723` ```qed ``` haftmann@21383 ` 724` haftmann@21383 ` 725` ```lemma order_le_less_subst1: "(a::'a::order) <= f b ==> (b::'b::order) < c ==> ``` haftmann@21383 ` 726` ``` (!!x y. x < y ==> f x < f y) ==> a < f c" ``` haftmann@21383 ` 727` ```proof - ``` haftmann@21383 ` 728` ``` assume r: "!!x y. x < y ==> f x < f y" ``` haftmann@21383 ` 729` ``` assume "a <= f b" ``` haftmann@21383 ` 730` ``` also assume "b < c" hence "f b < f c" by (rule r) ``` haftmann@21383 ` 731` ``` finally (order_le_less_trans) show ?thesis . ``` haftmann@21383 ` 732` ```qed ``` haftmann@21383 ` 733` haftmann@21383 ` 734` ```lemma order_less_le_subst2: "(a::'a::order) < b ==> f b <= (c::'c::order) ==> ``` haftmann@21383 ` 735` ``` (!!x y. x < y ==> f x < f y) ==> f a < c" ``` haftmann@21383 ` 736` ```proof - ``` haftmann@21383 ` 737` ``` assume r: "!!x y. x < y ==> f x < f y" ``` haftmann@21383 ` 738` ``` assume "a < b" hence "f a < f b" by (rule r) ``` haftmann@21383 ` 739` ``` also assume "f b <= c" ``` haftmann@21383 ` 740` ``` finally (order_less_le_trans) show ?thesis . ``` haftmann@21383 ` 741` ```qed ``` haftmann@21383 ` 742` haftmann@21383 ` 743` ```lemma order_less_le_subst1: "(a::'a::order) < f b ==> (b::'b::order) <= c ==> ``` haftmann@21383 ` 744` ``` (!!x y. x <= y ==> f x <= f y) ==> a < f c" ``` haftmann@21383 ` 745` ```proof - ``` haftmann@21383 ` 746` ``` assume r: "!!x y. x <= y ==> f x <= f y" ``` haftmann@21383 ` 747` ``` assume "a < f b" ``` haftmann@21383 ` 748` ``` also assume "b <= c" hence "f b <= f c" by (rule r) ``` haftmann@21383 ` 749` ``` finally (order_less_le_trans) show ?thesis . ``` haftmann@21383 ` 750` ```qed ``` haftmann@21383 ` 751` haftmann@21383 ` 752` ```lemma order_subst1: "(a::'a::order) <= f b ==> (b::'b::order) <= c ==> ``` haftmann@21383 ` 753` ``` (!!x y. x <= y ==> f x <= f y) ==> a <= f c" ``` haftmann@21383 ` 754` ```proof - ``` haftmann@21383 ` 755` ``` assume r: "!!x y. x <= y ==> f x <= f y" ``` haftmann@21383 ` 756` ``` assume "a <= f b" ``` haftmann@21383 ` 757` ``` also assume "b <= c" hence "f b <= f c" by (rule r) ``` haftmann@21383 ` 758` ``` finally (order_trans) show ?thesis . ``` haftmann@21383 ` 759` ```qed ``` haftmann@21383 ` 760` haftmann@21383 ` 761` ```lemma order_subst2: "(a::'a::order) <= b ==> f b <= (c::'c::order) ==> ``` haftmann@21383 ` 762` ``` (!!x y. x <= y ==> f x <= f y) ==> f a <= c" ``` haftmann@21383 ` 763` ```proof - ``` haftmann@21383 ` 764` ``` assume r: "!!x y. x <= y ==> f x <= f y" ``` haftmann@21383 ` 765` ``` assume "a <= b" hence "f a <= f b" by (rule r) ``` haftmann@21383 ` 766` ``` also assume "f b <= c" ``` haftmann@21383 ` 767` ``` finally (order_trans) show ?thesis . ``` haftmann@21383 ` 768` ```qed ``` haftmann@21383 ` 769` haftmann@21383 ` 770` ```lemma ord_le_eq_subst: "a <= b ==> f b = c ==> ``` haftmann@21383 ` 771` ``` (!!x y. x <= y ==> f x <= f y) ==> f a <= c" ``` haftmann@21383 ` 772` ```proof - ``` haftmann@21383 ` 773` ``` assume r: "!!x y. x <= y ==> f x <= f y" ``` haftmann@21383 ` 774` ``` assume "a <= b" hence "f a <= f b" by (rule r) ``` haftmann@21383 ` 775` ``` also assume "f b = c" ``` haftmann@21383 ` 776` ``` finally (ord_le_eq_trans) show ?thesis . ``` haftmann@21383 ` 777` ```qed ``` haftmann@21383 ` 778` haftmann@21383 ` 779` ```lemma ord_eq_le_subst: "a = f b ==> b <= c ==> ``` haftmann@21383 ` 780` ``` (!!x y. x <= y ==> f x <= f y) ==> a <= f c" ``` haftmann@21383 ` 781` ```proof - ``` haftmann@21383 ` 782` ``` assume r: "!!x y. x <= y ==> f x <= f y" ``` haftmann@21383 ` 783` ``` assume "a = f b" ``` haftmann@21383 ` 784` ``` also assume "b <= c" hence "f b <= f c" by (rule r) ``` haftmann@21383 ` 785` ``` finally (ord_eq_le_trans) show ?thesis . ``` haftmann@21383 ` 786` ```qed ``` haftmann@21383 ` 787` haftmann@21383 ` 788` ```lemma ord_less_eq_subst: "a < b ==> f b = c ==> ``` haftmann@21383 ` 789` ``` (!!x y. x < y ==> f x < f y) ==> f a < c" ``` haftmann@21383 ` 790` ```proof - ``` haftmann@21383 ` 791` ``` assume r: "!!x y. x < y ==> f x < f y" ``` haftmann@21383 ` 792` ``` assume "a < b" hence "f a < f b" by (rule r) ``` haftmann@21383 ` 793` ``` also assume "f b = c" ``` haftmann@21383 ` 794` ``` finally (ord_less_eq_trans) show ?thesis . ``` haftmann@21383 ` 795` ```qed ``` haftmann@21383 ` 796` haftmann@21383 ` 797` ```lemma ord_eq_less_subst: "a = f b ==> b < c ==> ``` haftmann@21383 ` 798` ``` (!!x y. x < y ==> f x < f y) ==> a < f c" ``` haftmann@21383 ` 799` ```proof - ``` haftmann@21383 ` 800` ``` assume r: "!!x y. x < y ==> f x < f y" ``` haftmann@21383 ` 801` ``` assume "a = f b" ``` haftmann@21383 ` 802` ``` also assume "b < c" hence "f b < f c" by (rule r) ``` haftmann@21383 ` 803` ``` finally (ord_eq_less_trans) show ?thesis . ``` haftmann@21383 ` 804` ```qed ``` haftmann@21383 ` 805` haftmann@21383 ` 806` ```text {* ``` haftmann@21383 ` 807` ``` Note that this list of rules is in reverse order of priorities. ``` haftmann@21383 ` 808` ```*} ``` haftmann@21383 ` 809` haftmann@21383 ` 810` ```lemmas order_trans_rules [trans] = ``` haftmann@21383 ` 811` ``` order_less_subst2 ``` haftmann@21383 ` 812` ``` order_less_subst1 ``` haftmann@21383 ` 813` ``` order_le_less_subst2 ``` haftmann@21383 ` 814` ``` order_le_less_subst1 ``` haftmann@21383 ` 815` ``` order_less_le_subst2 ``` haftmann@21383 ` 816` ``` order_less_le_subst1 ``` haftmann@21383 ` 817` ``` order_subst2 ``` haftmann@21383 ` 818` ``` order_subst1 ``` haftmann@21383 ` 819` ``` ord_le_eq_subst ``` haftmann@21383 ` 820` ``` ord_eq_le_subst ``` haftmann@21383 ` 821` ``` ord_less_eq_subst ``` haftmann@21383 ` 822` ``` ord_eq_less_subst ``` haftmann@21383 ` 823` ``` forw_subst ``` haftmann@21383 ` 824` ``` back_subst ``` haftmann@21383 ` 825` ``` rev_mp ``` haftmann@21383 ` 826` ``` mp ``` haftmann@21383 ` 827` ``` order_neq_le_trans ``` haftmann@21383 ` 828` ``` order_le_neq_trans ``` haftmann@21383 ` 829` ``` order_less_trans ``` haftmann@21383 ` 830` ``` order_less_asym' ``` haftmann@21383 ` 831` ``` order_le_less_trans ``` haftmann@21383 ` 832` ``` order_less_le_trans ``` haftmann@21383 ` 833` ``` order_trans ``` haftmann@21383 ` 834` ``` order_antisym ``` haftmann@21383 ` 835` ``` ord_le_eq_trans ``` haftmann@21383 ` 836` ``` ord_eq_le_trans ``` haftmann@21383 ` 837` ``` ord_less_eq_trans ``` haftmann@21383 ` 838` ``` ord_eq_less_trans ``` haftmann@21383 ` 839` ``` trans ``` haftmann@21383 ` 840` haftmann@21083 ` 841` wenzelm@21180 ` 842` ```(* FIXME cleanup *) ``` wenzelm@21180 ` 843` haftmann@21083 ` 844` ```text {* These support proving chains of decreasing inequalities ``` haftmann@21083 ` 845` ``` a >= b >= c ... in Isar proofs. *} ``` haftmann@21083 ` 846` haftmann@21083 ` 847` ```lemma xt1: ``` haftmann@21083 ` 848` ``` "a = b ==> b > c ==> a > c" ``` haftmann@21083 ` 849` ``` "a > b ==> b = c ==> a > c" ``` haftmann@21083 ` 850` ``` "a = b ==> b >= c ==> a >= c" ``` haftmann@21083 ` 851` ``` "a >= b ==> b = c ==> a >= c" ``` haftmann@21083 ` 852` ``` "(x::'a::order) >= y ==> y >= x ==> x = y" ``` haftmann@21083 ` 853` ``` "(x::'a::order) >= y ==> y >= z ==> x >= z" ``` haftmann@21083 ` 854` ``` "(x::'a::order) > y ==> y >= z ==> x > z" ``` haftmann@21083 ` 855` ``` "(x::'a::order) >= y ==> y > z ==> x > z" ``` wenzelm@23417 ` 856` ``` "(a::'a::order) > b ==> b > a ==> P" ``` haftmann@21083 ` 857` ``` "(x::'a::order) > y ==> y > z ==> x > z" ``` haftmann@21083 ` 858` ``` "(a::'a::order) >= b ==> a ~= b ==> a > b" ``` haftmann@21083 ` 859` ``` "(a::'a::order) ~= b ==> a >= b ==> a > b" ``` haftmann@21083 ` 860` ``` "a = f b ==> b > c ==> (!!x y. x > y ==> f x > f y) ==> a > f c" ``` haftmann@21083 ` 861` ``` "a > b ==> f b = c ==> (!!x y. x > y ==> f x > f y) ==> f a > c" ``` haftmann@21083 ` 862` ``` "a = f b ==> b >= c ==> (!!x y. x >= y ==> f x >= f y) ==> a >= f c" ``` haftmann@21083 ` 863` ``` "a >= b ==> f b = c ==> (!! x y. x >= y ==> f x >= f y) ==> f a >= c" ``` haftmann@21083 ` 864` ```by auto ``` haftmann@21083 ` 865` haftmann@21083 ` 866` ```lemma xt2: ``` haftmann@21083 ` 867` ``` "(a::'a::order) >= f b ==> b >= c ==> (!!x y. x >= y ==> f x >= f y) ==> a >= f c" ``` haftmann@21083 ` 868` ```by (subgoal_tac "f b >= f c", force, force) ``` haftmann@21083 ` 869` haftmann@21083 ` 870` ```lemma xt3: "(a::'a::order) >= b ==> (f b::'b::order) >= c ==> ``` haftmann@21083 ` 871` ``` (!!x y. x >= y ==> f x >= f y) ==> f a >= c" ``` haftmann@21083 ` 872` ```by (subgoal_tac "f a >= f b", force, force) ``` haftmann@21083 ` 873` haftmann@21083 ` 874` ```lemma xt4: "(a::'a::order) > f b ==> (b::'b::order) >= c ==> ``` haftmann@21083 ` 875` ``` (!!x y. x >= y ==> f x >= f y) ==> a > f c" ``` haftmann@21083 ` 876` ```by (subgoal_tac "f b >= f c", force, force) ``` haftmann@21083 ` 877` haftmann@21083 ` 878` ```lemma xt5: "(a::'a::order) > b ==> (f b::'b::order) >= c==> ``` haftmann@21083 ` 879` ``` (!!x y. x > y ==> f x > f y) ==> f a > c" ``` haftmann@21083 ` 880` ```by (subgoal_tac "f a > f b", force, force) ``` haftmann@21083 ` 881` haftmann@21083 ` 882` ```lemma xt6: "(a::'a::order) >= f b ==> b > c ==> ``` haftmann@21083 ` 883` ``` (!!x y. x > y ==> f x > f y) ==> a > f c" ``` haftmann@21083 ` 884` ```by (subgoal_tac "f b > f c", force, force) ``` haftmann@21083 ` 885` haftmann@21083 ` 886` ```lemma xt7: "(a::'a::order) >= b ==> (f b::'b::order) > c ==> ``` haftmann@21083 ` 887` ``` (!!x y. x >= y ==> f x >= f y) ==> f a > c" ``` haftmann@21083 ` 888` ```by (subgoal_tac "f a >= f b", force, force) ``` haftmann@21083 ` 889` haftmann@21083 ` 890` ```lemma xt8: "(a::'a::order) > f b ==> (b::'b::order) > c ==> ``` haftmann@21083 ` 891` ``` (!!x y. x > y ==> f x > f y) ==> a > f c" ``` haftmann@21083 ` 892` ```by (subgoal_tac "f b > f c", force, force) ``` haftmann@21083 ` 893` haftmann@21083 ` 894` ```lemma xt9: "(a::'a::order) > b ==> (f b::'b::order) > c ==> ``` haftmann@21083 ` 895` ``` (!!x y. x > y ==> f x > f y) ==> f a > c" ``` haftmann@21083 ` 896` ```by (subgoal_tac "f a > f b", force, force) ``` haftmann@21083 ` 897` haftmann@21083 ` 898` ```lemmas xtrans = xt1 xt2 xt3 xt4 xt5 xt6 xt7 xt8 xt9 ``` haftmann@21083 ` 899` haftmann@21083 ` 900` ```(* ``` haftmann@21083 ` 901` ``` Since "a >= b" abbreviates "b <= a", the abbreviation "..." stands ``` haftmann@21083 ` 902` ``` for the wrong thing in an Isar proof. ``` haftmann@21083 ` 903` haftmann@21083 ` 904` ``` The extra transitivity rules can be used as follows: ``` haftmann@21083 ` 905` haftmann@21083 ` 906` ```lemma "(a::'a::order) > z" ``` haftmann@21083 ` 907` ```proof - ``` haftmann@21083 ` 908` ``` have "a >= b" (is "_ >= ?rhs") ``` haftmann@21083 ` 909` ``` sorry ``` haftmann@21083 ` 910` ``` also have "?rhs >= c" (is "_ >= ?rhs") ``` haftmann@21083 ` 911` ``` sorry ``` haftmann@21083 ` 912` ``` also (xtrans) have "?rhs = d" (is "_ = ?rhs") ``` haftmann@21083 ` 913` ``` sorry ``` haftmann@21083 ` 914` ``` also (xtrans) have "?rhs >= e" (is "_ >= ?rhs") ``` haftmann@21083 ` 915` ``` sorry ``` haftmann@21083 ` 916` ``` also (xtrans) have "?rhs > f" (is "_ > ?rhs") ``` haftmann@21083 ` 917` ``` sorry ``` haftmann@21083 ` 918` ``` also (xtrans) have "?rhs > z" ``` haftmann@21083 ` 919` ``` sorry ``` haftmann@21083 ` 920` ``` finally (xtrans) show ?thesis . ``` haftmann@21083 ` 921` ```qed ``` haftmann@21083 ` 922` haftmann@21083 ` 923` ``` Alternatively, one can use "declare xtrans [trans]" and then ``` haftmann@21083 ` 924` ``` leave out the "(xtrans)" above. ``` haftmann@21083 ` 925` ```*) ``` haftmann@21083 ` 926` haftmann@21546 ` 927` ```subsection {* Order on bool *} ``` haftmann@21546 ` 928` haftmann@22886 ` 929` ```instance bool :: order ``` haftmann@21546 ` 930` ``` le_bool_def: "P \ Q \ P \ Q" ``` haftmann@21546 ` 931` ``` less_bool_def: "P < Q \ P \ Q \ P \ Q" ``` haftmann@22916 ` 932` ``` by intro_classes (auto simp add: le_bool_def less_bool_def) ``` haftmann@24422 ` 933` ```lemmas [code func del] = le_bool_def less_bool_def ``` haftmann@21546 ` 934` haftmann@21546 ` 935` ```lemma le_boolI: "(P \ Q) \ P \ Q" ``` nipkow@23212 ` 936` ```by (simp add: le_bool_def) ``` haftmann@21546 ` 937` haftmann@21546 ` 938` ```lemma le_boolI': "P \ Q \ P \ Q" ``` nipkow@23212 ` 939` ```by (simp add: le_bool_def) ``` haftmann@21546 ` 940` haftmann@21546 ` 941` ```lemma le_boolE: "P \ Q \ P \ (Q \ R) \ R" ``` nipkow@23212 ` 942` ```by (simp add: le_bool_def) ``` haftmann@21546 ` 943` haftmann@21546 ` 944` ```lemma le_boolD: "P \ Q \ P \ Q" ``` nipkow@23212 ` 945` ```by (simp add: le_bool_def) ``` haftmann@21546 ` 946` haftmann@22348 ` 947` ```lemma [code func]: ``` haftmann@22348 ` 948` ``` "False \ b \ True" ``` haftmann@22348 ` 949` ``` "True \ b \ b" ``` haftmann@22348 ` 950` ``` "False < b \ b" ``` haftmann@22348 ` 951` ``` "True < b \ False" ``` haftmann@22348 ` 952` ``` unfolding le_bool_def less_bool_def by simp_all ``` haftmann@22348 ` 953` haftmann@22424 ` 954` haftmann@23881 ` 955` ```subsection {* Order on sets *} ``` haftmann@23881 ` 956` haftmann@23881 ` 957` ```instance set :: (type) order ``` haftmann@23881 ` 958` ``` by (intro_classes, ``` haftmann@23881 ` 959` ``` (assumption | rule subset_refl subset_trans subset_antisym psubset_eq)+) ``` haftmann@23881 ` 960` haftmann@23881 ` 961` ```lemmas basic_trans_rules [trans] = ``` haftmann@23881 ` 962` ``` order_trans_rules set_rev_mp set_mp ``` haftmann@23881 ` 963` haftmann@23881 ` 964` haftmann@23881 ` 965` ```subsection {* Order on functions *} ``` haftmann@23881 ` 966` haftmann@23881 ` 967` ```instance "fun" :: (type, ord) ord ``` haftmann@23881 ` 968` ``` le_fun_def: "f \ g \ \x. f x \ g x" ``` haftmann@23881 ` 969` ``` less_fun_def: "f < g \ f \ g \ f \ g" .. ``` haftmann@23881 ` 970` haftmann@23881 ` 971` ```lemmas [code func del] = le_fun_def less_fun_def ``` haftmann@23881 ` 972` haftmann@23881 ` 973` ```instance "fun" :: (type, order) order ``` haftmann@23881 ` 974` ``` by default ``` haftmann@23881 ` 975` ``` (auto simp add: le_fun_def less_fun_def expand_fun_eq ``` haftmann@23881 ` 976` ``` intro: order_trans order_antisym) ``` haftmann@23881 ` 977` haftmann@23881 ` 978` ```lemma le_funI: "(\x. f x \ g x) \ f \ g" ``` haftmann@23881 ` 979` ``` unfolding le_fun_def by simp ``` haftmann@23881 ` 980` haftmann@23881 ` 981` ```lemma le_funE: "f \ g \ (f x \ g x \ P) \ P" ``` haftmann@23881 ` 982` ``` unfolding le_fun_def by simp ``` haftmann@23881 ` 983` haftmann@23881 ` 984` ```lemma le_funD: "f \ g \ f x \ g x" ``` haftmann@23881 ` 985` ``` unfolding le_fun_def by simp ``` haftmann@23881 ` 986` haftmann@23881 ` 987` ```text {* ``` haftmann@23881 ` 988` ``` Handy introduction and elimination rules for @{text "\"} ``` haftmann@23881 ` 989` ``` on unary and binary predicates ``` haftmann@23881 ` 990` ```*} ``` haftmann@23881 ` 991` haftmann@23881 ` 992` ```lemma predicate1I [Pure.intro!, intro!]: ``` haftmann@23881 ` 993` ``` assumes PQ: "\x. P x \ Q x" ``` haftmann@23881 ` 994` ``` shows "P \ Q" ``` haftmann@23881 ` 995` ``` apply (rule le_funI) ``` haftmann@23881 ` 996` ``` apply (rule le_boolI) ``` haftmann@23881 ` 997` ``` apply (rule PQ) ``` haftmann@23881 ` 998` ``` apply assumption ``` haftmann@23881 ` 999` ``` done ``` haftmann@23881 ` 1000` haftmann@23881 ` 1001` ```lemma predicate1D [Pure.dest, dest]: "P \ Q \ P x \ Q x" ``` haftmann@23881 ` 1002` ``` apply (erule le_funE) ``` haftmann@23881 ` 1003` ``` apply (erule le_boolE) ``` haftmann@23881 ` 1004` ``` apply assumption+ ``` haftmann@23881 ` 1005` ``` done ``` haftmann@23881 ` 1006` haftmann@23881 ` 1007` ```lemma predicate2I [Pure.intro!, intro!]: ``` haftmann@23881 ` 1008` ``` assumes PQ: "\x y. P x y \ Q x y" ``` haftmann@23881 ` 1009` ``` shows "P \ Q" ``` haftmann@23881 ` 1010` ``` apply (rule le_funI)+ ``` haftmann@23881 ` 1011` ``` apply (rule le_boolI) ``` haftmann@23881 ` 1012` ``` apply (rule PQ) ``` haftmann@23881 ` 1013` ``` apply assumption ``` haftmann@23881 ` 1014` ``` done ``` haftmann@23881 ` 1015` haftmann@23881 ` 1016` ```lemma predicate2D [Pure.dest, dest]: "P \ Q \ P x y \ Q x y" ``` haftmann@23881 ` 1017` ``` apply (erule le_funE)+ ``` haftmann@23881 ` 1018` ``` apply (erule le_boolE) ``` haftmann@23881 ` 1019` ``` apply assumption+ ``` haftmann@23881 ` 1020` ``` done ``` haftmann@23881 ` 1021` haftmann@23881 ` 1022` ```lemma rev_predicate1D: "P x ==> P <= Q ==> Q x" ``` haftmann@23881 ` 1023` ``` by (rule predicate1D) ``` haftmann@23881 ` 1024` haftmann@23881 ` 1025` ```lemma rev_predicate2D: "P x y ==> P <= Q ==> Q x y" ``` haftmann@23881 ` 1026` ``` by (rule predicate2D) ``` haftmann@23881 ` 1027` haftmann@23881 ` 1028` haftmann@23881 ` 1029` ```subsection {* Monotonicity, least value operator and min/max *} ``` haftmann@21083 ` 1030` haftmann@21216 ` 1031` ```locale mono = ``` haftmann@21216 ` 1032` ``` fixes f ``` haftmann@21216 ` 1033` ``` assumes mono: "A \ B \ f A \ f B" ``` haftmann@21216 ` 1034` haftmann@21216 ` 1035` ```lemmas monoI [intro?] = mono.intro ``` haftmann@21216 ` 1036` ``` and monoD [dest?] = mono.mono ``` haftmann@21083 ` 1037` haftmann@21383 ` 1038` ```lemma LeastI2_order: ``` haftmann@21383 ` 1039` ``` "[| P (x::'a::order); ``` haftmann@21383 ` 1040` ``` !!y. P y ==> x <= y; ``` haftmann@21383 ` 1041` ``` !!x. [| P x; ALL y. P y --> x \ y |] ==> Q x |] ``` haftmann@21383 ` 1042` ``` ==> Q (Least P)" ``` nipkow@23212 ` 1043` ```apply (unfold Least_def) ``` nipkow@23212 ` 1044` ```apply (rule theI2) ``` nipkow@23212 ` 1045` ``` apply (blast intro: order_antisym)+ ``` nipkow@23212 ` 1046` ```done ``` haftmann@21383 ` 1047` haftmann@23881 ` 1048` ```lemma Least_mono: ``` haftmann@23881 ` 1049` ``` "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y ``` haftmann@23881 ` 1050` ``` ==> (LEAST y. y : f ` S) = f (LEAST x. x : S)" ``` haftmann@23881 ` 1051` ``` -- {* Courtesy of Stephan Merz *} ``` haftmann@23881 ` 1052` ``` apply clarify ``` haftmann@23881 ` 1053` ``` apply (erule_tac P = "%x. x : S" in LeastI2_order, fast) ``` haftmann@23881 ` 1054` ``` apply (rule LeastI2_order) ``` haftmann@23881 ` 1055` ``` apply (auto elim: monoD intro!: order_antisym) ``` haftmann@23881 ` 1056` ``` done ``` haftmann@23881 ` 1057` haftmann@21383 ` 1058` ```lemma Least_equality: ``` nipkow@23212 ` 1059` ``` "[| P (k::'a::order); !!x. P x ==> k <= x |] ==> (LEAST x. P x) = k" ``` nipkow@23212 ` 1060` ```apply (simp add: Least_def) ``` nipkow@23212 ` 1061` ```apply (rule the_equality) ``` nipkow@23212 ` 1062` ```apply (auto intro!: order_antisym) ``` nipkow@23212 ` 1063` ```done ``` haftmann@21383 ` 1064` haftmann@21383 ` 1065` ```lemma min_leastL: "(!!x. least <= x) ==> min least x = least" ``` nipkow@23212 ` 1066` ```by (simp add: min_def) ``` haftmann@21383 ` 1067` haftmann@21383 ` 1068` ```lemma max_leastL: "(!!x. least <= x) ==> max least x = x" ``` nipkow@23212 ` 1069` ```by (simp add: max_def) ``` haftmann@21383 ` 1070` haftmann@21383 ` 1071` ```lemma min_leastR: "(\x\'a\order. least \ x) \ min x least = least" ``` nipkow@23212 ` 1072` ```apply (simp add: min_def) ``` nipkow@23212 ` 1073` ```apply (blast intro: order_antisym) ``` nipkow@23212 ` 1074` ```done ``` haftmann@21383 ` 1075` haftmann@21383 ` 1076` ```lemma max_leastR: "(\x\'a\order. least \ x) \ max x least = x" ``` nipkow@23212 ` 1077` ```apply (simp add: max_def) ``` nipkow@23212 ` 1078` ```apply (blast intro: order_antisym) ``` nipkow@23212 ` 1079` ```done ``` haftmann@21383 ` 1080` haftmann@21383 ` 1081` ```lemma min_of_mono: ``` nipkow@23212 ` 1082` ``` "(!!x y. (f x <= f y) = (x <= y)) ==> min (f m) (f n) = f (min m n)" ``` nipkow@23212 ` 1083` ```by (simp add: min_def) ``` haftmann@21383 ` 1084` haftmann@21383 ` 1085` ```lemma max_of_mono: ``` nipkow@23212 ` 1086` ``` "(!!x y. (f x <= f y) = (x <= y)) ==> max (f m) (f n) = f (max m n)" ``` nipkow@23212 ` 1087` ```by (simp add: max_def) ``` haftmann@21383 ` 1088` haftmann@22548 ` 1089` haftmann@22548 ` 1090` ```subsection {* legacy ML bindings *} ``` wenzelm@21673 ` 1091` wenzelm@21673 ` 1092` ```ML {* ``` haftmann@22548 ` 1093` ```val monoI = @{thm monoI}; ``` haftmann@22886 ` 1094` ```*} ``` wenzelm@21673 ` 1095` nipkow@15524 ` 1096` ```end ```