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