src/HOL/Orderings.thy
 author wenzelm Sat Oct 06 16:50:04 2007 +0200 (2007-10-06) changeset 24867 e5b55d7be9bb parent 24748 ee0a0eb6b738 child 24920 2a45e400fdad permissions -rw-r--r--
simplified interfaces for outer syntax;
 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` wenzelm@24867 ` 349` ```val _ = ``` 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` wenzelm@24867 ` 357` ```val setup = ``` wenzelm@24867 ` 358` ``` Method.add_methods ``` wenzelm@24867 ` 359` ``` [("order", Method.ctxt_args (Method.SIMPLE_METHOD' o order_tac []), "transitivity reasoner")] #> ``` wenzelm@24867 ` 360` ``` Attrib.add_attributes [("order", attribute, "theorems controlling transitivity reasoner")]; ``` haftmann@21091 ` 361` haftmann@21091 ` 362` ```end; ``` ballarin@24641 ` 363` haftmann@21091 ` 364` ```*} ``` haftmann@21091 ` 365` ballarin@24641 ` 366` ```setup Orders.setup ``` ballarin@24641 ` 367` ballarin@24641 ` 368` ballarin@24641 ` 369` ```text {* Declarations to set up transitivity reasoner of partial and linear orders. *} ``` ballarin@24641 ` 370` ballarin@24641 ` 371` ```(* The type constraint on @{term op =} below is necessary since the operation ``` ballarin@24641 ` 372` ``` is not a parameter of the locale. *) ``` ballarin@24641 ` 373` ```lemmas (in order) ``` ballarin@24641 ` 374` ``` [order add less_reflE: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 375` ``` less_irrefl [THEN notE] ``` ballarin@24641 ` 376` ```lemmas (in order) ``` ballarin@24641 ` 377` ``` [order add le_refl: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 378` ``` order_refl ``` ballarin@24641 ` 379` ```lemmas (in order) ``` ballarin@24641 ` 380` ``` [order add less_imp_le: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 381` ``` less_imp_le ``` ballarin@24641 ` 382` ```lemmas (in order) ``` ballarin@24641 ` 383` ``` [order add eqI: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 384` ``` antisym ``` ballarin@24641 ` 385` ```lemmas (in order) ``` ballarin@24641 ` 386` ``` [order add eqD1: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 387` ``` eq_refl ``` ballarin@24641 ` 388` ```lemmas (in order) ``` ballarin@24641 ` 389` ``` [order add eqD2: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 390` ``` sym [THEN eq_refl] ``` ballarin@24641 ` 391` ```lemmas (in order) ``` ballarin@24641 ` 392` ``` [order add less_trans: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 393` ``` less_trans ``` ballarin@24641 ` 394` ```lemmas (in order) ``` ballarin@24641 ` 395` ``` [order add less_le_trans: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 396` ``` less_le_trans ``` ballarin@24641 ` 397` ```lemmas (in order) ``` ballarin@24641 ` 398` ``` [order add le_less_trans: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 399` ``` le_less_trans ``` ballarin@24641 ` 400` ```lemmas (in order) ``` ballarin@24641 ` 401` ``` [order add le_trans: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 402` ``` order_trans ``` ballarin@24641 ` 403` ```lemmas (in order) ``` ballarin@24641 ` 404` ``` [order add le_neq_trans: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 405` ``` le_neq_trans ``` ballarin@24641 ` 406` ```lemmas (in order) ``` ballarin@24641 ` 407` ``` [order add neq_le_trans: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 408` ``` neq_le_trans ``` ballarin@24641 ` 409` ```lemmas (in order) ``` ballarin@24641 ` 410` ``` [order add less_imp_neq: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 411` ``` less_imp_neq ``` ballarin@24641 ` 412` ```lemmas (in order) ``` ballarin@24641 ` 413` ``` [order add eq_neq_eq_imp_neq: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 414` ``` eq_neq_eq_imp_neq ``` ballarin@24641 ` 415` ```lemmas (in order) ``` ballarin@24641 ` 416` ``` [order add not_sym: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 417` ``` not_sym ``` ballarin@24641 ` 418` ballarin@24641 ` 419` ```lemmas (in linorder) [order del: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = _ ``` ballarin@24641 ` 420` ballarin@24641 ` 421` ```lemmas (in linorder) ``` ballarin@24641 ` 422` ``` [order add less_reflE: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 423` ``` less_irrefl [THEN notE] ``` ballarin@24641 ` 424` ```lemmas (in linorder) ``` ballarin@24641 ` 425` ``` [order add le_refl: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 426` ``` order_refl ``` ballarin@24641 ` 427` ```lemmas (in linorder) ``` ballarin@24641 ` 428` ``` [order add less_imp_le: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 429` ``` less_imp_le ``` ballarin@24641 ` 430` ```lemmas (in linorder) ``` ballarin@24641 ` 431` ``` [order add not_lessI: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 432` ``` not_less [THEN iffD2] ``` ballarin@24641 ` 433` ```lemmas (in linorder) ``` ballarin@24641 ` 434` ``` [order add not_leI: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 435` ``` not_le [THEN iffD2] ``` ballarin@24641 ` 436` ```lemmas (in linorder) ``` ballarin@24641 ` 437` ``` [order add not_lessD: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 438` ``` not_less [THEN iffD1] ``` ballarin@24641 ` 439` ```lemmas (in linorder) ``` ballarin@24641 ` 440` ``` [order add not_leD: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 441` ``` not_le [THEN iffD1] ``` ballarin@24641 ` 442` ```lemmas (in linorder) ``` ballarin@24641 ` 443` ``` [order add eqI: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 444` ``` antisym ``` ballarin@24641 ` 445` ```lemmas (in linorder) ``` ballarin@24641 ` 446` ``` [order add eqD1: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 447` ``` eq_refl ``` ballarin@24641 ` 448` ```lemmas (in linorder) ``` ballarin@24641 ` 449` ``` [order add eqD2: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 450` ``` sym [THEN eq_refl] ``` ballarin@24641 ` 451` ```lemmas (in linorder) ``` ballarin@24641 ` 452` ``` [order add less_trans: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 453` ``` less_trans ``` ballarin@24641 ` 454` ```lemmas (in linorder) ``` ballarin@24641 ` 455` ``` [order add less_le_trans: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 456` ``` less_le_trans ``` ballarin@24641 ` 457` ```lemmas (in linorder) ``` ballarin@24641 ` 458` ``` [order add le_less_trans: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 459` ``` le_less_trans ``` ballarin@24641 ` 460` ```lemmas (in linorder) ``` ballarin@24641 ` 461` ``` [order add le_trans: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 462` ``` order_trans ``` ballarin@24641 ` 463` ```lemmas (in linorder) ``` ballarin@24641 ` 464` ``` [order add le_neq_trans: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 465` ``` le_neq_trans ``` ballarin@24641 ` 466` ```lemmas (in linorder) ``` ballarin@24641 ` 467` ``` [order add neq_le_trans: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 468` ``` neq_le_trans ``` ballarin@24641 ` 469` ```lemmas (in linorder) ``` ballarin@24641 ` 470` ``` [order add less_imp_neq: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 471` ``` less_imp_neq ``` ballarin@24641 ` 472` ```lemmas (in linorder) ``` ballarin@24641 ` 473` ``` [order add eq_neq_eq_imp_neq: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 474` ``` eq_neq_eq_imp_neq ``` ballarin@24641 ` 475` ```lemmas (in linorder) ``` ballarin@24641 ` 476` ``` [order add not_sym: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = ``` ballarin@24641 ` 477` ``` not_sym ``` ballarin@24641 ` 478` ballarin@24641 ` 479` haftmann@21083 ` 480` ```setup {* ``` haftmann@21083 ` 481` ```let ``` haftmann@21083 ` 482` haftmann@21083 ` 483` ```fun prp t thm = (#prop (rep_thm thm) = t); ``` nipkow@15524 ` 484` haftmann@21083 ` 485` ```fun prove_antisym_le sg ss ((le as Const(_,T)) \$ r \$ s) = ``` haftmann@21083 ` 486` ``` let val prems = prems_of_ss ss; ``` haftmann@22916 ` 487` ``` val less = Const (@{const_name less}, T); ``` haftmann@21083 ` 488` ``` val t = HOLogic.mk_Trueprop(le \$ s \$ r); ``` haftmann@21083 ` 489` ``` in case find_first (prp t) prems of ``` haftmann@21083 ` 490` ``` NONE => ``` haftmann@21083 ` 491` ``` let val t = HOLogic.mk_Trueprop(HOLogic.Not \$ (less \$ r \$ s)) ``` haftmann@21083 ` 492` ``` in case find_first (prp t) prems of ``` haftmann@21083 ` 493` ``` NONE => NONE ``` haftmann@24422 ` 494` ``` | SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_class.antisym_conv1})) ``` haftmann@21083 ` 495` ``` end ``` haftmann@24422 ` 496` ``` | SOME thm => SOME(mk_meta_eq(thm RS @{thm order_class.antisym_conv})) ``` haftmann@21083 ` 497` ``` end ``` haftmann@21083 ` 498` ``` handle THM _ => NONE; ``` nipkow@15524 ` 499` haftmann@21083 ` 500` ```fun prove_antisym_less sg ss (NotC \$ ((less as Const(_,T)) \$ r \$ s)) = ``` haftmann@21083 ` 501` ``` let val prems = prems_of_ss ss; ``` haftmann@22916 ` 502` ``` val le = Const (@{const_name less_eq}, T); ``` haftmann@21083 ` 503` ``` val t = HOLogic.mk_Trueprop(le \$ r \$ s); ``` haftmann@21083 ` 504` ``` in case find_first (prp t) prems of ``` haftmann@21083 ` 505` ``` NONE => ``` haftmann@21083 ` 506` ``` let val t = HOLogic.mk_Trueprop(NotC \$ (less \$ s \$ r)) ``` haftmann@21083 ` 507` ``` in case find_first (prp t) prems of ``` haftmann@21083 ` 508` ``` NONE => NONE ``` haftmann@24422 ` 509` ``` | SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_class.antisym_conv3})) ``` haftmann@21083 ` 510` ``` end ``` haftmann@24422 ` 511` ``` | SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_class.antisym_conv2})) ``` haftmann@21083 ` 512` ``` end ``` haftmann@21083 ` 513` ``` handle THM _ => NONE; ``` nipkow@15524 ` 514` haftmann@21248 ` 515` ```fun add_simprocs procs thy = ``` haftmann@21248 ` 516` ``` (Simplifier.change_simpset_of thy (fn ss => ss ``` haftmann@21248 ` 517` ``` addsimprocs (map (fn (name, raw_ts, proc) => ``` haftmann@21248 ` 518` ``` Simplifier.simproc thy name raw_ts proc)) procs); thy); ``` haftmann@21248 ` 519` ```fun add_solver name tac thy = ``` haftmann@21248 ` 520` ``` (Simplifier.change_simpset_of thy (fn ss => ss addSolver ``` ballarin@24704 ` 521` ``` (mk_solver' name (fn ss => tac (MetaSimplifier.prems_of_ss ss) (MetaSimplifier.the_context ss)))); thy); ``` haftmann@21083 ` 522` haftmann@21083 ` 523` ```in ``` haftmann@21248 ` 524` ``` add_simprocs [ ``` haftmann@21248 ` 525` ``` ("antisym le", ["(x::'a::order) <= y"], prove_antisym_le), ``` haftmann@21248 ` 526` ``` ("antisym less", ["~ (x::'a::linorder) < y"], prove_antisym_less) ``` haftmann@21248 ` 527` ``` ] ``` ballarin@24641 ` 528` ``` #> add_solver "Transitivity" Orders.order_tac ``` haftmann@21248 ` 529` ``` (* Adding the transitivity reasoners also as safe solvers showed a slight ``` haftmann@21248 ` 530` ``` speed up, but the reasoning strength appears to be not higher (at least ``` haftmann@21248 ` 531` ``` no breaking of additional proofs in the entire HOL distribution, as ``` haftmann@21248 ` 532` ``` of 5 March 2004, was observed). *) ``` haftmann@21083 ` 533` ```end ``` haftmann@21083 ` 534` ```*} ``` nipkow@15524 ` 535` nipkow@15524 ` 536` haftmann@24422 ` 537` ```subsection {* Dense orders *} ``` haftmann@24422 ` 538` haftmann@24422 ` 539` ```class dense_linear_order = linorder + ``` haftmann@24422 ` 540` ``` assumes gt_ex: "\y. x \ y" ``` haftmann@24422 ` 541` ``` and lt_ex: "\y. y \ x" ``` haftmann@24422 ` 542` ``` and dense: "x \ y \ (\z. x \ z \ z \ y)" ``` haftmann@24422 ` 543` ``` (*see further theory Dense_Linear_Order*) ``` haftmann@24422 ` 544` ballarin@24641 ` 545` haftmann@24422 ` 546` ```lemma interval_empty_iff: ``` haftmann@24422 ` 547` ``` fixes x y z :: "'a\dense_linear_order" ``` haftmann@24422 ` 548` ``` shows "{y. x < y \ y < z} = {} \ \ x < z" ``` haftmann@24422 ` 549` ``` by (auto dest: dense) ``` haftmann@24422 ` 550` haftmann@24422 ` 551` ```subsection {* Name duplicates *} ``` haftmann@24422 ` 552` haftmann@24422 ` 553` ```lemmas order_less_le = less_le ``` haftmann@24422 ` 554` ```lemmas order_eq_refl = order_class.eq_refl ``` haftmann@24422 ` 555` ```lemmas order_less_irrefl = order_class.less_irrefl ``` haftmann@24422 ` 556` ```lemmas order_le_less = order_class.le_less ``` haftmann@24422 ` 557` ```lemmas order_le_imp_less_or_eq = order_class.le_imp_less_or_eq ``` haftmann@24422 ` 558` ```lemmas order_less_imp_le = order_class.less_imp_le ``` haftmann@24422 ` 559` ```lemmas order_less_imp_not_eq = order_class.less_imp_not_eq ``` haftmann@24422 ` 560` ```lemmas order_less_imp_not_eq2 = order_class.less_imp_not_eq2 ``` haftmann@24422 ` 561` ```lemmas order_neq_le_trans = order_class.neq_le_trans ``` haftmann@24422 ` 562` ```lemmas order_le_neq_trans = order_class.le_neq_trans ``` haftmann@24422 ` 563` haftmann@24422 ` 564` ```lemmas order_antisym = antisym ``` haftmann@24422 ` 565` ```lemmas order_less_not_sym = order_class.less_not_sym ``` haftmann@24422 ` 566` ```lemmas order_less_asym = order_class.less_asym ``` haftmann@24422 ` 567` ```lemmas order_eq_iff = order_class.eq_iff ``` haftmann@24422 ` 568` ```lemmas order_antisym_conv = order_class.antisym_conv ``` haftmann@24422 ` 569` ```lemmas order_less_trans = order_class.less_trans ``` haftmann@24422 ` 570` ```lemmas order_le_less_trans = order_class.le_less_trans ``` haftmann@24422 ` 571` ```lemmas order_less_le_trans = order_class.less_le_trans ``` haftmann@24422 ` 572` ```lemmas order_less_imp_not_less = order_class.less_imp_not_less ``` haftmann@24422 ` 573` ```lemmas order_less_imp_triv = order_class.less_imp_triv ``` haftmann@24422 ` 574` ```lemmas order_less_asym' = order_class.less_asym' ``` haftmann@24422 ` 575` haftmann@24422 ` 576` ```lemmas linorder_linear = linear ``` haftmann@24422 ` 577` ```lemmas linorder_less_linear = linorder_class.less_linear ``` haftmann@24422 ` 578` ```lemmas linorder_le_less_linear = linorder_class.le_less_linear ``` haftmann@24422 ` 579` ```lemmas linorder_le_cases = linorder_class.le_cases ``` haftmann@24422 ` 580` ```lemmas linorder_not_less = linorder_class.not_less ``` haftmann@24422 ` 581` ```lemmas linorder_not_le = linorder_class.not_le ``` haftmann@24422 ` 582` ```lemmas linorder_neq_iff = linorder_class.neq_iff ``` haftmann@24422 ` 583` ```lemmas linorder_neqE = linorder_class.neqE ``` haftmann@24422 ` 584` ```lemmas linorder_antisym_conv1 = linorder_class.antisym_conv1 ``` haftmann@24422 ` 585` ```lemmas linorder_antisym_conv2 = linorder_class.antisym_conv2 ``` haftmann@24422 ` 586` ```lemmas linorder_antisym_conv3 = linorder_class.antisym_conv3 ``` haftmann@24422 ` 587` haftmann@24422 ` 588` ```lemmas min_le_iff_disj = linorder_class.min_le_iff_disj ``` haftmann@24422 ` 589` ```lemmas le_max_iff_disj = linorder_class.le_max_iff_disj ``` haftmann@24422 ` 590` ```lemmas min_less_iff_disj = linorder_class.min_less_iff_disj ``` haftmann@24422 ` 591` ```lemmas less_max_iff_disj = linorder_class.less_max_iff_disj ``` haftmann@24422 ` 592` ```lemmas min_less_iff_conj [simp] = linorder_class.min_less_iff_conj ``` haftmann@24422 ` 593` ```lemmas max_less_iff_conj [simp] = linorder_class.max_less_iff_conj ``` haftmann@24422 ` 594` ```lemmas split_min = linorder_class.split_min ``` haftmann@24422 ` 595` ```lemmas split_max = linorder_class.split_max ``` haftmann@24422 ` 596` haftmann@24422 ` 597` haftmann@21083 ` 598` ```subsection {* Bounded quantifiers *} ``` haftmann@21083 ` 599` haftmann@21083 ` 600` ```syntax ``` wenzelm@21180 ` 601` ``` "_All_less" :: "[idt, 'a, bool] => bool" ("(3ALL _<_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 602` ``` "_Ex_less" :: "[idt, 'a, bool] => bool" ("(3EX _<_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 603` ``` "_All_less_eq" :: "[idt, 'a, bool] => bool" ("(3ALL _<=_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 604` ``` "_Ex_less_eq" :: "[idt, 'a, bool] => bool" ("(3EX _<=_./ _)" [0, 0, 10] 10) ``` haftmann@21083 ` 605` wenzelm@21180 ` 606` ``` "_All_greater" :: "[idt, 'a, bool] => bool" ("(3ALL _>_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 607` ``` "_Ex_greater" :: "[idt, 'a, bool] => bool" ("(3EX _>_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 608` ``` "_All_greater_eq" :: "[idt, 'a, bool] => bool" ("(3ALL _>=_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 609` ``` "_Ex_greater_eq" :: "[idt, 'a, bool] => bool" ("(3EX _>=_./ _)" [0, 0, 10] 10) ``` haftmann@21083 ` 610` haftmann@21083 ` 611` ```syntax (xsymbols) ``` wenzelm@21180 ` 612` ``` "_All_less" :: "[idt, 'a, bool] => bool" ("(3\_<_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 613` ``` "_Ex_less" :: "[idt, 'a, bool] => bool" ("(3\_<_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 614` ``` "_All_less_eq" :: "[idt, 'a, bool] => bool" ("(3\_\_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 615` ``` "_Ex_less_eq" :: "[idt, 'a, bool] => bool" ("(3\_\_./ _)" [0, 0, 10] 10) ``` haftmann@21083 ` 616` wenzelm@21180 ` 617` ``` "_All_greater" :: "[idt, 'a, bool] => bool" ("(3\_>_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 618` ``` "_Ex_greater" :: "[idt, 'a, bool] => bool" ("(3\_>_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 619` ``` "_All_greater_eq" :: "[idt, 'a, bool] => bool" ("(3\_\_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 620` ``` "_Ex_greater_eq" :: "[idt, 'a, bool] => bool" ("(3\_\_./ _)" [0, 0, 10] 10) ``` haftmann@21083 ` 621` haftmann@21083 ` 622` ```syntax (HOL) ``` wenzelm@21180 ` 623` ``` "_All_less" :: "[idt, 'a, bool] => bool" ("(3! _<_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 624` ``` "_Ex_less" :: "[idt, 'a, bool] => bool" ("(3? _<_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 625` ``` "_All_less_eq" :: "[idt, 'a, bool] => bool" ("(3! _<=_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 626` ``` "_Ex_less_eq" :: "[idt, 'a, bool] => bool" ("(3? _<=_./ _)" [0, 0, 10] 10) ``` haftmann@21083 ` 627` haftmann@21083 ` 628` ```syntax (HTML output) ``` wenzelm@21180 ` 629` ``` "_All_less" :: "[idt, 'a, bool] => bool" ("(3\_<_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 630` ``` "_Ex_less" :: "[idt, 'a, bool] => bool" ("(3\_<_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 631` ``` "_All_less_eq" :: "[idt, 'a, bool] => bool" ("(3\_\_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 632` ``` "_Ex_less_eq" :: "[idt, 'a, bool] => bool" ("(3\_\_./ _)" [0, 0, 10] 10) ``` haftmann@21083 ` 633` wenzelm@21180 ` 634` ``` "_All_greater" :: "[idt, 'a, bool] => bool" ("(3\_>_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 635` ``` "_Ex_greater" :: "[idt, 'a, bool] => bool" ("(3\_>_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 636` ``` "_All_greater_eq" :: "[idt, 'a, bool] => bool" ("(3\_\_./ _)" [0, 0, 10] 10) ``` wenzelm@21180 ` 637` ``` "_Ex_greater_eq" :: "[idt, 'a, bool] => bool" ("(3\_\_./ _)" [0, 0, 10] 10) ``` haftmann@21083 ` 638` haftmann@21083 ` 639` ```translations ``` haftmann@21083 ` 640` ``` "ALL x "ALL x. x < y \ P" ``` haftmann@21083 ` 641` ``` "EX x "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` ``` "ALL x>=y. P" => "ALL x. x >= y \ P" ``` haftmann@21083 ` 647` ``` "EX x>=y. P" => "EX x. x >= y \ P" ``` haftmann@21083 ` 648` haftmann@21083 ` 649` ```print_translation {* ``` haftmann@21083 ` 650` ```let ``` haftmann@22916 ` 651` ``` val All_binder = Syntax.binder_name @{const_syntax All}; ``` haftmann@22916 ` 652` ``` val Ex_binder = Syntax.binder_name @{const_syntax Ex}; ``` wenzelm@22377 ` 653` ``` val impl = @{const_syntax "op -->"}; ``` wenzelm@22377 ` 654` ``` val conj = @{const_syntax "op &"}; ``` haftmann@22916 ` 655` ``` val less = @{const_syntax less}; ``` haftmann@22916 ` 656` ``` val less_eq = @{const_syntax less_eq}; ``` wenzelm@21180 ` 657` wenzelm@21180 ` 658` ``` val trans = ``` wenzelm@21524 ` 659` ``` [((All_binder, impl, less), ("_All_less", "_All_greater")), ``` wenzelm@21524 ` 660` ``` ((All_binder, impl, less_eq), ("_All_less_eq", "_All_greater_eq")), ``` wenzelm@21524 ` 661` ``` ((Ex_binder, conj, less), ("_Ex_less", "_Ex_greater")), ``` wenzelm@21524 ` 662` ``` ((Ex_binder, conj, less_eq), ("_Ex_less_eq", "_Ex_greater_eq"))]; ``` wenzelm@21180 ` 663` krauss@22344 ` 664` ``` fun matches_bound v t = ``` krauss@22344 ` 665` ``` case t of (Const ("_bound", _) \$ Free (v', _)) => (v = v') ``` krauss@22344 ` 666` ``` | _ => false ``` krauss@22344 ` 667` ``` fun contains_var v = Term.exists_subterm (fn Free (x, _) => x = v | _ => false) ``` krauss@22344 ` 668` ``` fun mk v c n P = Syntax.const c \$ Syntax.mark_bound v \$ n \$ P ``` wenzelm@21180 ` 669` wenzelm@21180 ` 670` ``` fun tr' q = (q, ``` wenzelm@21180 ` 671` ``` fn [Const ("_bound", _) \$ Free (v, _), Const (c, _) \$ (Const (d, _) \$ t \$ u) \$ P] => ``` wenzelm@21180 ` 672` ``` (case AList.lookup (op =) trans (q, c, d) of ``` wenzelm@21180 ` 673` ``` NONE => raise Match ``` wenzelm@21180 ` 674` ``` | SOME (l, g) => ``` krauss@22344 ` 675` ``` if matches_bound v t andalso not (contains_var v u) then mk v l u P ``` krauss@22344 ` 676` ``` else if matches_bound v u andalso not (contains_var v t) then mk v g t P ``` krauss@22344 ` 677` ``` else raise Match) ``` wenzelm@21180 ` 678` ``` | _ => raise Match); ``` wenzelm@21524 ` 679` ```in [tr' All_binder, tr' Ex_binder] end ``` haftmann@21083 ` 680` ```*} ``` haftmann@21083 ` 681` haftmann@21083 ` 682` haftmann@21383 ` 683` ```subsection {* Transitivity reasoning *} ``` haftmann@21383 ` 684` haftmann@21383 ` 685` ```lemma ord_le_eq_trans: "a <= b ==> b = c ==> a <= c" ``` nipkow@23212 ` 686` ```by (rule subst) ``` haftmann@21383 ` 687` haftmann@21383 ` 688` ```lemma ord_eq_le_trans: "a = b ==> b <= c ==> a <= c" ``` nipkow@23212 ` 689` ```by (rule ssubst) ``` haftmann@21383 ` 690` haftmann@21383 ` 691` ```lemma ord_less_eq_trans: "a < b ==> b = c ==> a < c" ``` nipkow@23212 ` 692` ```by (rule subst) ``` haftmann@21383 ` 693` haftmann@21383 ` 694` ```lemma ord_eq_less_trans: "a = b ==> b < c ==> a < c" ``` nipkow@23212 ` 695` ```by (rule ssubst) ``` haftmann@21383 ` 696` haftmann@21383 ` 697` ```lemma order_less_subst2: "(a::'a::order) < b ==> f b < (c::'c::order) ==> ``` haftmann@21383 ` 698` ``` (!!x y. x < y ==> f x < f y) ==> f a < c" ``` haftmann@21383 ` 699` ```proof - ``` haftmann@21383 ` 700` ``` assume r: "!!x y. x < y ==> f x < f y" ``` haftmann@21383 ` 701` ``` assume "a < b" hence "f a < f b" by (rule r) ``` haftmann@21383 ` 702` ``` also assume "f b < c" ``` haftmann@21383 ` 703` ``` finally (order_less_trans) show ?thesis . ``` haftmann@21383 ` 704` ```qed ``` haftmann@21383 ` 705` haftmann@21383 ` 706` ```lemma order_less_subst1: "(a::'a::order) < f b ==> (b::'b::order) < c ==> ``` haftmann@21383 ` 707` ``` (!!x y. x < y ==> f x < f y) ==> a < f c" ``` haftmann@21383 ` 708` ```proof - ``` haftmann@21383 ` 709` ``` assume r: "!!x y. x < y ==> f x < f y" ``` haftmann@21383 ` 710` ``` assume "a < f b" ``` haftmann@21383 ` 711` ``` also assume "b < c" hence "f b < f c" by (rule r) ``` haftmann@21383 ` 712` ``` finally (order_less_trans) show ?thesis . ``` haftmann@21383 ` 713` ```qed ``` haftmann@21383 ` 714` haftmann@21383 ` 715` ```lemma order_le_less_subst2: "(a::'a::order) <= b ==> f b < (c::'c::order) ==> ``` haftmann@21383 ` 716` ``` (!!x y. x <= y ==> f x <= f y) ==> f a < c" ``` haftmann@21383 ` 717` ```proof - ``` haftmann@21383 ` 718` ``` assume r: "!!x y. x <= y ==> f x <= f y" ``` haftmann@21383 ` 719` ``` assume "a <= b" hence "f a <= f b" by (rule r) ``` haftmann@21383 ` 720` ``` also assume "f b < c" ``` haftmann@21383 ` 721` ``` finally (order_le_less_trans) show ?thesis . ``` haftmann@21383 ` 722` ```qed ``` haftmann@21383 ` 723` haftmann@21383 ` 724` ```lemma order_le_less_subst1: "(a::'a::order) <= f b ==> (b::'b::order) < c ==> ``` haftmann@21383 ` 725` ``` (!!x y. x < y ==> f x < f y) ==> a < f c" ``` haftmann@21383 ` 726` ```proof - ``` haftmann@21383 ` 727` ``` assume r: "!!x y. x < y ==> f x < f y" ``` haftmann@21383 ` 728` ``` assume "a <= f b" ``` haftmann@21383 ` 729` ``` also assume "b < c" hence "f b < f c" by (rule r) ``` haftmann@21383 ` 730` ``` finally (order_le_less_trans) show ?thesis . ``` haftmann@21383 ` 731` ```qed ``` haftmann@21383 ` 732` haftmann@21383 ` 733` ```lemma order_less_le_subst2: "(a::'a::order) < b ==> f b <= (c::'c::order) ==> ``` haftmann@21383 ` 734` ``` (!!x y. x < y ==> f x < f y) ==> f a < c" ``` haftmann@21383 ` 735` ```proof - ``` haftmann@21383 ` 736` ``` assume r: "!!x y. x < y ==> f x < f y" ``` haftmann@21383 ` 737` ``` assume "a < b" hence "f a < f b" by (rule r) ``` haftmann@21383 ` 738` ``` also assume "f b <= c" ``` haftmann@21383 ` 739` ``` finally (order_less_le_trans) show ?thesis . ``` haftmann@21383 ` 740` ```qed ``` haftmann@21383 ` 741` haftmann@21383 ` 742` ```lemma order_less_le_subst1: "(a::'a::order) < f b ==> (b::'b::order) <= c ==> ``` haftmann@21383 ` 743` ``` (!!x y. x <= y ==> f x <= f y) ==> a < f c" ``` haftmann@21383 ` 744` ```proof - ``` haftmann@21383 ` 745` ``` assume r: "!!x y. x <= y ==> f x <= f y" ``` haftmann@21383 ` 746` ``` assume "a < f b" ``` haftmann@21383 ` 747` ``` also assume "b <= c" hence "f b <= f c" by (rule r) ``` haftmann@21383 ` 748` ``` finally (order_less_le_trans) show ?thesis . ``` haftmann@21383 ` 749` ```qed ``` haftmann@21383 ` 750` haftmann@21383 ` 751` ```lemma order_subst1: "(a::'a::order) <= f b ==> (b::'b::order) <= c ==> ``` haftmann@21383 ` 752` ``` (!!x y. x <= y ==> f x <= f y) ==> a <= f c" ``` haftmann@21383 ` 753` ```proof - ``` haftmann@21383 ` 754` ``` assume r: "!!x y. x <= y ==> f x <= f y" ``` haftmann@21383 ` 755` ``` assume "a <= f b" ``` haftmann@21383 ` 756` ``` also assume "b <= c" hence "f b <= f c" by (rule r) ``` haftmann@21383 ` 757` ``` finally (order_trans) show ?thesis . ``` haftmann@21383 ` 758` ```qed ``` haftmann@21383 ` 759` haftmann@21383 ` 760` ```lemma order_subst2: "(a::'a::order) <= b ==> f b <= (c::'c::order) ==> ``` haftmann@21383 ` 761` ``` (!!x y. x <= y ==> f x <= f y) ==> f a <= c" ``` haftmann@21383 ` 762` ```proof - ``` haftmann@21383 ` 763` ``` assume r: "!!x y. x <= y ==> f x <= f y" ``` haftmann@21383 ` 764` ``` assume "a <= b" hence "f a <= f b" by (rule r) ``` haftmann@21383 ` 765` ``` also assume "f b <= c" ``` haftmann@21383 ` 766` ``` finally (order_trans) show ?thesis . ``` haftmann@21383 ` 767` ```qed ``` haftmann@21383 ` 768` haftmann@21383 ` 769` ```lemma ord_le_eq_subst: "a <= b ==> f b = c ==> ``` haftmann@21383 ` 770` ``` (!!x y. x <= y ==> f x <= f y) ==> f a <= c" ``` haftmann@21383 ` 771` ```proof - ``` haftmann@21383 ` 772` ``` assume r: "!!x y. x <= y ==> f x <= f y" ``` haftmann@21383 ` 773` ``` assume "a <= b" hence "f a <= f b" by (rule r) ``` haftmann@21383 ` 774` ``` also assume "f b = c" ``` haftmann@21383 ` 775` ``` finally (ord_le_eq_trans) show ?thesis . ``` haftmann@21383 ` 776` ```qed ``` haftmann@21383 ` 777` haftmann@21383 ` 778` ```lemma ord_eq_le_subst: "a = f b ==> b <= c ==> ``` haftmann@21383 ` 779` ``` (!!x y. x <= y ==> f x <= f y) ==> a <= f c" ``` haftmann@21383 ` 780` ```proof - ``` haftmann@21383 ` 781` ``` assume r: "!!x y. x <= y ==> f x <= f y" ``` haftmann@21383 ` 782` ``` assume "a = f b" ``` haftmann@21383 ` 783` ``` also assume "b <= c" hence "f b <= f c" by (rule r) ``` haftmann@21383 ` 784` ``` finally (ord_eq_le_trans) show ?thesis . ``` haftmann@21383 ` 785` ```qed ``` haftmann@21383 ` 786` haftmann@21383 ` 787` ```lemma ord_less_eq_subst: "a < b ==> f b = c ==> ``` haftmann@21383 ` 788` ``` (!!x y. x < y ==> f x < f y) ==> f a < c" ``` haftmann@21383 ` 789` ```proof - ``` haftmann@21383 ` 790` ``` assume r: "!!x y. x < y ==> f x < f y" ``` haftmann@21383 ` 791` ``` assume "a < b" hence "f a < f b" by (rule r) ``` haftmann@21383 ` 792` ``` also assume "f b = c" ``` haftmann@21383 ` 793` ``` finally (ord_less_eq_trans) show ?thesis . ``` haftmann@21383 ` 794` ```qed ``` haftmann@21383 ` 795` haftmann@21383 ` 796` ```lemma ord_eq_less_subst: "a = f b ==> b < c ==> ``` haftmann@21383 ` 797` ``` (!!x y. x < y ==> f x < f y) ==> a < f c" ``` haftmann@21383 ` 798` ```proof - ``` haftmann@21383 ` 799` ``` assume r: "!!x y. x < y ==> f x < f y" ``` haftmann@21383 ` 800` ``` assume "a = f b" ``` haftmann@21383 ` 801` ``` also assume "b < c" hence "f b < f c" by (rule r) ``` haftmann@21383 ` 802` ``` finally (ord_eq_less_trans) show ?thesis . ``` haftmann@21383 ` 803` ```qed ``` haftmann@21383 ` 804` haftmann@21383 ` 805` ```text {* ``` haftmann@21383 ` 806` ``` Note that this list of rules is in reverse order of priorities. ``` haftmann@21383 ` 807` ```*} ``` haftmann@21383 ` 808` haftmann@21383 ` 809` ```lemmas order_trans_rules [trans] = ``` haftmann@21383 ` 810` ``` order_less_subst2 ``` haftmann@21383 ` 811` ``` order_less_subst1 ``` haftmann@21383 ` 812` ``` order_le_less_subst2 ``` haftmann@21383 ` 813` ``` order_le_less_subst1 ``` haftmann@21383 ` 814` ``` order_less_le_subst2 ``` haftmann@21383 ` 815` ``` order_less_le_subst1 ``` haftmann@21383 ` 816` ``` order_subst2 ``` haftmann@21383 ` 817` ``` order_subst1 ``` haftmann@21383 ` 818` ``` ord_le_eq_subst ``` haftmann@21383 ` 819` ``` ord_eq_le_subst ``` haftmann@21383 ` 820` ``` ord_less_eq_subst ``` haftmann@21383 ` 821` ``` ord_eq_less_subst ``` haftmann@21383 ` 822` ``` forw_subst ``` haftmann@21383 ` 823` ``` back_subst ``` haftmann@21383 ` 824` ``` rev_mp ``` haftmann@21383 ` 825` ``` mp ``` haftmann@21383 ` 826` ``` order_neq_le_trans ``` haftmann@21383 ` 827` ``` order_le_neq_trans ``` haftmann@21383 ` 828` ``` order_less_trans ``` haftmann@21383 ` 829` ``` order_less_asym' ``` haftmann@21383 ` 830` ``` order_le_less_trans ``` haftmann@21383 ` 831` ``` order_less_le_trans ``` haftmann@21383 ` 832` ``` order_trans ``` haftmann@21383 ` 833` ``` order_antisym ``` haftmann@21383 ` 834` ``` ord_le_eq_trans ``` haftmann@21383 ` 835` ``` ord_eq_le_trans ``` haftmann@21383 ` 836` ``` ord_less_eq_trans ``` haftmann@21383 ` 837` ``` ord_eq_less_trans ``` haftmann@21383 ` 838` ``` trans ``` haftmann@21383 ` 839` haftmann@21083 ` 840` wenzelm@21180 ` 841` ```(* FIXME cleanup *) ``` wenzelm@21180 ` 842` haftmann@21083 ` 843` ```text {* These support proving chains of decreasing inequalities ``` haftmann@21083 ` 844` ``` a >= b >= c ... in Isar proofs. *} ``` haftmann@21083 ` 845` haftmann@21083 ` 846` ```lemma xt1: ``` haftmann@21083 ` 847` ``` "a = b ==> b > c ==> a > c" ``` 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` ``` "(x::'a::order) >= y ==> y >= x ==> x = y" ``` haftmann@21083 ` 852` ``` "(x::'a::order) >= y ==> y >= z ==> x >= z" ``` haftmann@21083 ` 853` ``` "(x::'a::order) > y ==> y >= z ==> x > z" ``` haftmann@21083 ` 854` ``` "(x::'a::order) >= y ==> y > z ==> x > z" ``` wenzelm@23417 ` 855` ``` "(a::'a::order) > b ==> b > a ==> P" ``` haftmann@21083 ` 856` ``` "(x::'a::order) > y ==> y > z ==> x > z" ``` haftmann@21083 ` 857` ``` "(a::'a::order) >= b ==> a ~= b ==> a > b" ``` haftmann@21083 ` 858` ``` "(a::'a::order) ~= b ==> a >= b ==> a > b" ``` haftmann@21083 ` 859` ``` "a = f b ==> b > c ==> (!!x y. x > y ==> f x > f y) ==> a > f c" ``` haftmann@21083 ` 860` ``` "a > b ==> f b = c ==> (!!x y. x > y ==> f x > f y) ==> f a > c" ``` haftmann@21083 ` 861` ``` "a = f b ==> b >= c ==> (!!x y. x >= y ==> f x >= f y) ==> a >= f c" ``` haftmann@21083 ` 862` ``` "a >= b ==> f b = c ==> (!! x y. x >= y ==> f x >= f y) ==> f a >= c" ``` haftmann@21083 ` 863` ```by auto ``` haftmann@21083 ` 864` haftmann@21083 ` 865` ```lemma xt2: ``` haftmann@21083 ` 866` ``` "(a::'a::order) >= f b ==> b >= c ==> (!!x y. x >= y ==> f x >= f y) ==> a >= f c" ``` haftmann@21083 ` 867` ```by (subgoal_tac "f b >= f c", force, force) ``` haftmann@21083 ` 868` haftmann@21083 ` 869` ```lemma xt3: "(a::'a::order) >= b ==> (f b::'b::order) >= c ==> ``` haftmann@21083 ` 870` ``` (!!x y. x >= y ==> f x >= f y) ==> f a >= c" ``` haftmann@21083 ` 871` ```by (subgoal_tac "f a >= f b", force, force) ``` haftmann@21083 ` 872` haftmann@21083 ` 873` ```lemma xt4: "(a::'a::order) > f b ==> (b::'b::order) >= c ==> ``` haftmann@21083 ` 874` ``` (!!x y. x >= y ==> f x >= f y) ==> a > f c" ``` haftmann@21083 ` 875` ```by (subgoal_tac "f b >= f c", force, force) ``` haftmann@21083 ` 876` haftmann@21083 ` 877` ```lemma xt5: "(a::'a::order) > b ==> (f b::'b::order) >= c==> ``` haftmann@21083 ` 878` ``` (!!x y. x > y ==> f x > f y) ==> f a > c" ``` haftmann@21083 ` 879` ```by (subgoal_tac "f a > f b", force, force) ``` haftmann@21083 ` 880` haftmann@21083 ` 881` ```lemma xt6: "(a::'a::order) >= f b ==> b > c ==> ``` haftmann@21083 ` 882` ``` (!!x y. x > y ==> f x > f y) ==> a > f c" ``` haftmann@21083 ` 883` ```by (subgoal_tac "f b > f c", force, force) ``` haftmann@21083 ` 884` haftmann@21083 ` 885` ```lemma xt7: "(a::'a::order) >= b ==> (f b::'b::order) > c ==> ``` haftmann@21083 ` 886` ``` (!!x y. x >= y ==> f x >= f y) ==> f a > c" ``` haftmann@21083 ` 887` ```by (subgoal_tac "f a >= f b", force, force) ``` haftmann@21083 ` 888` haftmann@21083 ` 889` ```lemma xt8: "(a::'a::order) > f b ==> (b::'b::order) > c ==> ``` haftmann@21083 ` 890` ``` (!!x y. x > y ==> f x > f y) ==> a > f c" ``` haftmann@21083 ` 891` ```by (subgoal_tac "f b > f c", force, force) ``` haftmann@21083 ` 892` haftmann@21083 ` 893` ```lemma xt9: "(a::'a::order) > b ==> (f b::'b::order) > c ==> ``` haftmann@21083 ` 894` ``` (!!x y. x > y ==> f x > f y) ==> f a > c" ``` haftmann@21083 ` 895` ```by (subgoal_tac "f a > f b", force, force) ``` haftmann@21083 ` 896` haftmann@21083 ` 897` ```lemmas xtrans = xt1 xt2 xt3 xt4 xt5 xt6 xt7 xt8 xt9 ``` haftmann@21083 ` 898` haftmann@21083 ` 899` ```(* ``` haftmann@21083 ` 900` ``` Since "a >= b" abbreviates "b <= a", the abbreviation "..." stands ``` haftmann@21083 ` 901` ``` for the wrong thing in an Isar proof. ``` haftmann@21083 ` 902` haftmann@21083 ` 903` ``` The extra transitivity rules can be used as follows: ``` haftmann@21083 ` 904` haftmann@21083 ` 905` ```lemma "(a::'a::order) > z" ``` haftmann@21083 ` 906` ```proof - ``` haftmann@21083 ` 907` ``` have "a >= b" (is "_ >= ?rhs") ``` haftmann@21083 ` 908` ``` sorry ``` haftmann@21083 ` 909` ``` also have "?rhs >= c" (is "_ >= ?rhs") ``` haftmann@21083 ` 910` ``` sorry ``` haftmann@21083 ` 911` ``` also (xtrans) have "?rhs = d" (is "_ = ?rhs") ``` haftmann@21083 ` 912` ``` sorry ``` haftmann@21083 ` 913` ``` also (xtrans) have "?rhs >= e" (is "_ >= ?rhs") ``` haftmann@21083 ` 914` ``` sorry ``` haftmann@21083 ` 915` ``` also (xtrans) have "?rhs > f" (is "_ > ?rhs") ``` haftmann@21083 ` 916` ``` sorry ``` haftmann@21083 ` 917` ``` also (xtrans) have "?rhs > z" ``` haftmann@21083 ` 918` ``` sorry ``` haftmann@21083 ` 919` ``` finally (xtrans) show ?thesis . ``` haftmann@21083 ` 920` ```qed ``` haftmann@21083 ` 921` haftmann@21083 ` 922` ``` Alternatively, one can use "declare xtrans [trans]" and then ``` haftmann@21083 ` 923` ``` leave out the "(xtrans)" above. ``` haftmann@21083 ` 924` ```*) ``` haftmann@21083 ` 925` haftmann@21546 ` 926` ```subsection {* Order on bool *} ``` haftmann@21546 ` 927` haftmann@22886 ` 928` ```instance bool :: order ``` haftmann@21546 ` 929` ``` le_bool_def: "P \ Q \ P \ Q" ``` haftmann@21546 ` 930` ``` less_bool_def: "P < Q \ P \ Q \ P \ Q" ``` haftmann@22916 ` 931` ``` by intro_classes (auto simp add: le_bool_def less_bool_def) ``` haftmann@24422 ` 932` ```lemmas [code func del] = le_bool_def less_bool_def ``` haftmann@21546 ` 933` haftmann@21546 ` 934` ```lemma le_boolI: "(P \ Q) \ P \ Q" ``` nipkow@23212 ` 935` ```by (simp add: le_bool_def) ``` haftmann@21546 ` 936` haftmann@21546 ` 937` ```lemma le_boolI': "P \ Q \ P \ Q" ``` nipkow@23212 ` 938` ```by (simp add: le_bool_def) ``` haftmann@21546 ` 939` haftmann@21546 ` 940` ```lemma le_boolE: "P \ Q \ P \ (Q \ R) \ R" ``` nipkow@23212 ` 941` ```by (simp add: le_bool_def) ``` haftmann@21546 ` 942` haftmann@21546 ` 943` ```lemma le_boolD: "P \ Q \ P \ Q" ``` nipkow@23212 ` 944` ```by (simp add: le_bool_def) ``` haftmann@21546 ` 945` haftmann@22348 ` 946` ```lemma [code func]: ``` haftmann@22348 ` 947` ``` "False \ b \ True" ``` haftmann@22348 ` 948` ``` "True \ b \ b" ``` haftmann@22348 ` 949` ``` "False < b \ b" ``` haftmann@22348 ` 950` ``` "True < b \ False" ``` haftmann@22348 ` 951` ``` unfolding le_bool_def less_bool_def by simp_all ``` haftmann@22348 ` 952` haftmann@22424 ` 953` haftmann@23881 ` 954` ```subsection {* Order on sets *} ``` haftmann@23881 ` 955` haftmann@23881 ` 956` ```instance set :: (type) order ``` haftmann@23881 ` 957` ``` by (intro_classes, ``` haftmann@23881 ` 958` ``` (assumption | rule subset_refl subset_trans subset_antisym psubset_eq)+) ``` haftmann@23881 ` 959` haftmann@23881 ` 960` ```lemmas basic_trans_rules [trans] = ``` haftmann@23881 ` 961` ``` order_trans_rules set_rev_mp set_mp ``` haftmann@23881 ` 962` haftmann@23881 ` 963` haftmann@23881 ` 964` ```subsection {* Order on functions *} ``` haftmann@23881 ` 965` haftmann@23881 ` 966` ```instance "fun" :: (type, ord) ord ``` haftmann@23881 ` 967` ``` le_fun_def: "f \ g \ \x. f x \ g x" ``` haftmann@23881 ` 968` ``` less_fun_def: "f < g \ f \ g \ f \ g" .. ``` haftmann@23881 ` 969` haftmann@23881 ` 970` ```lemmas [code func del] = le_fun_def less_fun_def ``` haftmann@23881 ` 971` haftmann@23881 ` 972` ```instance "fun" :: (type, order) order ``` haftmann@23881 ` 973` ``` by default ``` haftmann@23881 ` 974` ``` (auto simp add: le_fun_def less_fun_def expand_fun_eq ``` haftmann@23881 ` 975` ``` intro: order_trans order_antisym) ``` haftmann@23881 ` 976` haftmann@23881 ` 977` ```lemma le_funI: "(\x. f x \ g x) \ f \ g" ``` haftmann@23881 ` 978` ``` unfolding le_fun_def by simp ``` haftmann@23881 ` 979` haftmann@23881 ` 980` ```lemma le_funE: "f \ g \ (f x \ g x \ P) \ P" ``` haftmann@23881 ` 981` ``` unfolding le_fun_def by simp ``` haftmann@23881 ` 982` haftmann@23881 ` 983` ```lemma le_funD: "f \ g \ f x \ g x" ``` haftmann@23881 ` 984` ``` unfolding le_fun_def by simp ``` haftmann@23881 ` 985` haftmann@23881 ` 986` ```text {* ``` haftmann@23881 ` 987` ``` Handy introduction and elimination rules for @{text "\"} ``` haftmann@23881 ` 988` ``` on unary and binary predicates ``` haftmann@23881 ` 989` ```*} ``` haftmann@23881 ` 990` haftmann@23881 ` 991` ```lemma predicate1I [Pure.intro!, intro!]: ``` haftmann@23881 ` 992` ``` assumes PQ: "\x. P x \ Q x" ``` haftmann@23881 ` 993` ``` shows "P \ Q" ``` haftmann@23881 ` 994` ``` apply (rule le_funI) ``` haftmann@23881 ` 995` ``` apply (rule le_boolI) ``` haftmann@23881 ` 996` ``` apply (rule PQ) ``` haftmann@23881 ` 997` ``` apply assumption ``` haftmann@23881 ` 998` ``` done ``` haftmann@23881 ` 999` haftmann@23881 ` 1000` ```lemma predicate1D [Pure.dest, dest]: "P \ Q \ P x \ Q x" ``` haftmann@23881 ` 1001` ``` apply (erule le_funE) ``` haftmann@23881 ` 1002` ``` apply (erule le_boolE) ``` haftmann@23881 ` 1003` ``` apply assumption+ ``` haftmann@23881 ` 1004` ``` done ``` haftmann@23881 ` 1005` haftmann@23881 ` 1006` ```lemma predicate2I [Pure.intro!, intro!]: ``` haftmann@23881 ` 1007` ``` assumes PQ: "\x y. P x y \ Q x y" ``` haftmann@23881 ` 1008` ``` shows "P \ Q" ``` haftmann@23881 ` 1009` ``` apply (rule le_funI)+ ``` haftmann@23881 ` 1010` ``` apply (rule le_boolI) ``` haftmann@23881 ` 1011` ``` apply (rule PQ) ``` haftmann@23881 ` 1012` ``` apply assumption ``` haftmann@23881 ` 1013` ``` done ``` haftmann@23881 ` 1014` haftmann@23881 ` 1015` ```lemma predicate2D [Pure.dest, dest]: "P \ Q \ P x y \ Q x y" ``` haftmann@23881 ` 1016` ``` apply (erule le_funE)+ ``` haftmann@23881 ` 1017` ``` apply (erule le_boolE) ``` haftmann@23881 ` 1018` ``` apply assumption+ ``` haftmann@23881 ` 1019` ``` done ``` haftmann@23881 ` 1020` haftmann@23881 ` 1021` ```lemma rev_predicate1D: "P x ==> P <= Q ==> Q x" ``` haftmann@23881 ` 1022` ``` by (rule predicate1D) ``` haftmann@23881 ` 1023` haftmann@23881 ` 1024` ```lemma rev_predicate2D: "P x y ==> P <= Q ==> Q x y" ``` haftmann@23881 ` 1025` ``` by (rule predicate2D) ``` haftmann@23881 ` 1026` haftmann@23881 ` 1027` haftmann@23881 ` 1028` ```subsection {* Monotonicity, least value operator and min/max *} ``` haftmann@21083 ` 1029` haftmann@21216 ` 1030` ```locale mono = ``` haftmann@21216 ` 1031` ``` fixes f ``` haftmann@21216 ` 1032` ``` assumes mono: "A \ B \ f A \ f B" ``` haftmann@21216 ` 1033` haftmann@21216 ` 1034` ```lemmas monoI [intro?] = mono.intro ``` haftmann@21216 ` 1035` ``` and monoD [dest?] = mono.mono ``` haftmann@21083 ` 1036` haftmann@21383 ` 1037` ```lemma LeastI2_order: ``` haftmann@21383 ` 1038` ``` "[| P (x::'a::order); ``` haftmann@21383 ` 1039` ``` !!y. P y ==> x <= y; ``` haftmann@21383 ` 1040` ``` !!x. [| P x; ALL y. P y --> x \ y |] ==> Q x |] ``` haftmann@21383 ` 1041` ``` ==> Q (Least P)" ``` nipkow@23212 ` 1042` ```apply (unfold Least_def) ``` nipkow@23212 ` 1043` ```apply (rule theI2) ``` nipkow@23212 ` 1044` ``` apply (blast intro: order_antisym)+ ``` nipkow@23212 ` 1045` ```done ``` haftmann@21383 ` 1046` haftmann@23881 ` 1047` ```lemma Least_mono: ``` haftmann@23881 ` 1048` ``` "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y ``` haftmann@23881 ` 1049` ``` ==> (LEAST y. y : f ` S) = f (LEAST x. x : S)" ``` haftmann@23881 ` 1050` ``` -- {* Courtesy of Stephan Merz *} ``` haftmann@23881 ` 1051` ``` apply clarify ``` haftmann@23881 ` 1052` ``` apply (erule_tac P = "%x. x : S" in LeastI2_order, fast) ``` haftmann@23881 ` 1053` ``` apply (rule LeastI2_order) ``` haftmann@23881 ` 1054` ``` apply (auto elim: monoD intro!: order_antisym) ``` haftmann@23881 ` 1055` ``` done ``` haftmann@23881 ` 1056` haftmann@21383 ` 1057` ```lemma Least_equality: ``` nipkow@23212 ` 1058` ``` "[| P (k::'a::order); !!x. P x ==> k <= x |] ==> (LEAST x. P x) = k" ``` nipkow@23212 ` 1059` ```apply (simp add: Least_def) ``` nipkow@23212 ` 1060` ```apply (rule the_equality) ``` nipkow@23212 ` 1061` ```apply (auto intro!: order_antisym) ``` nipkow@23212 ` 1062` ```done ``` haftmann@21383 ` 1063` haftmann@21383 ` 1064` ```lemma min_leastL: "(!!x. least <= x) ==> min least x = least" ``` nipkow@23212 ` 1065` ```by (simp add: min_def) ``` haftmann@21383 ` 1066` haftmann@21383 ` 1067` ```lemma max_leastL: "(!!x. least <= x) ==> max least x = x" ``` nipkow@23212 ` 1068` ```by (simp add: max_def) ``` haftmann@21383 ` 1069` haftmann@21383 ` 1070` ```lemma min_leastR: "(\x\'a\order. least \ x) \ min x least = least" ``` nipkow@23212 ` 1071` ```apply (simp add: min_def) ``` nipkow@23212 ` 1072` ```apply (blast intro: order_antisym) ``` nipkow@23212 ` 1073` ```done ``` haftmann@21383 ` 1074` haftmann@21383 ` 1075` ```lemma max_leastR: "(\x\'a\order. least \ x) \ max x least = x" ``` nipkow@23212 ` 1076` ```apply (simp add: max_def) ``` nipkow@23212 ` 1077` ```apply (blast intro: order_antisym) ``` nipkow@23212 ` 1078` ```done ``` haftmann@21383 ` 1079` haftmann@21383 ` 1080` ```lemma min_of_mono: ``` nipkow@23212 ` 1081` ``` "(!!x y. (f x <= f y) = (x <= y)) ==> min (f m) (f n) = f (min m n)" ``` nipkow@23212 ` 1082` ```by (simp add: min_def) ``` haftmann@21383 ` 1083` haftmann@21383 ` 1084` ```lemma max_of_mono: ``` nipkow@23212 ` 1085` ``` "(!!x y. (f x <= f y) = (x <= y)) ==> max (f m) (f n) = f (max m n)" ``` nipkow@23212 ` 1086` ```by (simp add: max_def) ``` haftmann@21383 ` 1087` haftmann@22548 ` 1088` haftmann@22548 ` 1089` ```subsection {* legacy ML bindings *} ``` wenzelm@21673 ` 1090` wenzelm@21673 ` 1091` ```ML {* ``` haftmann@22548 ` 1092` ```val monoI = @{thm monoI}; ``` haftmann@22886 ` 1093` ```*} ``` wenzelm@21673 ` 1094` nipkow@15524 ` 1095` ```end ```