Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Orderings.thy Sprache: Isabelle

Original von: Isabelle^©

(* Title: HOL/Orderings.thy
 Author: Tobias Nipkow, Markus Wenzel, and Larry Paulson
*)

section \<open>Abstract orderings\<close>

theory Orderings
imports HOL
keywords "print_orders" :: diag
begin

ML_file \<open>~~/src/Provers/order.ML\<close>

subsection \<open>Abstract ordering\<close>

locale ordering =
 fixes less_eq :: "'a \ 'a \ bool" (infix "\<^bold>\" 50)
 and less :: "'a \ 'a \ bool" (infix "\<^bold><" 50)
 assumes strict_iff_order: "a \<^bold>\ b \ a \ b"
 assumes refl: "a \<^bold>\ a" \ \not \iff\: makes problems due to multiple (dual) interpretations\
 and antisym: "a \<^bold>\ b \ b \<^bold>\ a \ a = b"
 and trans: "a \<^bold>\ b \ b \<^bold>\ c \ a \<^bold>\ c"
begin

lemma strict_implies_order:
 "a \<^bold>\ b"
 by (simp add: strict_iff_order)

lemma strict_implies_not_eq:
 "a \<^bold>\ b \ a \<^bold>< b"
 by (simp add: strict_iff_order)

lemma order_iff_strict:
 "a \<^bold>\ b \ a \<^bold> \<open>not \<open>iff\<close>: makes problems due to multiple (dual) interpretations\<close>
 "\ a \<^bold>< a"
 by (simp add: strict_iff_order)

lemma asym:
 "a \<^bold>< a \ False"
 by (auto simp add: strict_iff_order intro: antisym)

lemma strict_trans1:
 "a \<^bold>\ b \ b \<^bold>< c \ a \<^bold>< c"
 by (auto simp add: strict_iff_order intro: trans antisym)

lemma strict_trans2:
 "a \<^bold>\ c \ a \<^bold>< c"
 by (auto simp add: strict_iff_order intro: trans antisym)

lemma strict_trans:
 "a \<^bold>< c \ a \<^bold>< c"
 by (auto intro: strict_trans1 strict_implies_order)

lemma eq_iff: "a = b \ a \<^bold>\ b \ b \<^bold>\ a"
 by (auto simp add: refl intro: antisym)

end

text \<open>Alternative introduction rule with bias towards strict order\<close>

lemma ordering_strictI:
 fixes less_eq (infix "\<^bold>\" 50)
 and less (infix "\<^bold><" 50)
 assumes less_eq_less: "\a b. a \<^bold>\ b \ a \<^bold>< a"
 assumes irrefl: "\a. \ a \<^bold>< a"
 assumes trans: "\a b c. a \<^bold>< c \ a \<^bold>< c"
 shows "ordering less_eq less"
proof
 fix a b
 show "a \<^bold>\ b \ a \ b"
 by (auto simp add: less_eq_less asym irrefl)
next
 fix a
 show "a \<^bold>\ a"
 by (auto simp add: less_eq_less)
next
 fix a b c
 assume "a \<^bold>\ b" and "b \<^bold>\ c" then show "a \<^bold>\ c"
 by (auto simp add: less_eq_less intro: trans)
next
 fix a b
 assume "a \<^bold>\ b" and "b \<^bold>\ a" then show "a = b"
 by (auto simp add: less_eq_less asym)
qed

lemma ordering_dualI:
 fixes less_eq (infix "\<^bold>\" 50)
 and less (infix "\<^bold><" 50)
 assumes "ordering (\a b. b \<^bold>\ a) (\a b. b \<^bold>< a)"
 shows "ordering less_eq less"
proof -
 from assms interpret ordering "\a b. b \<^bold>\ a" "\a b. b \<^bold>< a" .
 show ?thesis
 by standard (auto simp: strict_iff_order refl intro: antisym trans)
qed

locale ordering_top = ordering +
 fixes top :: "'a" ("\<^bold>\")
 assumes extremum [simp]: "a \<^bold>\ \<^bold>\"
begin

lemma extremum_uniqueI:
 "\<^bold>\ \<^bold>\ a \ a = \<^bold>\"
 by (rule antisym) auto

lemma extremum_unique:
 "\<^bold>\ \<^bold>\ a \ a = \<^bold>\"
 by (auto intro: antisym)

lemma extremum_strict [simp]:
 "\ (\<^bold>\ \<^bold>< a)"
 using extremum [of a] by (auto simp add: order_iff_strict intro: asym irrefl)

lemma not_eq_extremum:
 "a \ \<^bold>\ \ a \<^bold>< \<^bold>\"
 by (auto simp add: order_iff_strict intro: not_eq_order_implies_strict extremum)

end

subsection \<open>Syntactic orders\<close>

class ord =
 fixes less_eq :: "'a \ 'a \ bool"
 and less :: "'a \ 'a \ bool"
begin

notation
 less_eq ("'(\')") and
 less_eq ("(_/ \ _)" [51, 51] 50) and
 less ("'(<')") and
 less ("(_/ < _)" [51, 51] 50)

abbreviation (input)
 greater_eq (infix "\" 50)
 where "x \ y \ y \ x"

abbreviation (input)
 greater (infix ">" 50)
 where "x > y \ y < x"

notation (ASCII)
 less_eq ("'(<=')") and
 less_eq ("(_/ <= _)" [51, 51] 50)

notation (input)
 greater_eq (infix ">=" 50)

end

subsection \<open>Quasi orders\<close>

class preorder = ord +
 assumes less_le_not_le: "x < y \ x \ y \ \ (y \ x)"
 and order_refl [iff]: "x \ x"
 and order_trans: "x \ y \ y \ z \ x \ z"
begin

text \<open>Reflexivity.\<close>

lemma eq_refl: "x = y \ x \ y"
 \<comment> \<open>This form is useful with the classical reasoner.\<close>
by (erule ssubst) (rule order_refl)

lemma less_irrefl [iff]: "\ x < x"
by (simp add: less_le_not_le)

lemma less_imp_le: "x < y \ x \ y"
by (simp add: less_le_not_le)

text \<open>Asymmetry.\<close>

lemma less_not_sym: "x < y \ \ (y < x)"
by (simp add: less_le_not_le)

lemma less_asym: "x < y \ (\ P \ y < x) \ P"
by (drule less_not_sym, erule contrapos_np) simp

text \<open>Transitivity.\<close>

lemma less_trans: "x < y \ y < z \ x < z"
by (auto simp add: less_le_not_le intro: order_trans)

lemma le_less_trans: "x \ y \ y < z \ x < z"
by (auto simp add: less_le_not_le intro: order_trans)

lemma less_le_trans: "x < y \ y \ z \ x < z"
by (auto simp add: less_le_not_le intro: order_trans)

text \<open>Useful for simplification, but too risky to include by default.\<close>

lemma less_imp_not_less: "x < y \ (\ y < x) \ True"
by (blast elim: less_asym)

lemma less_imp_triv: "x < y \ (y < x \ P) \ True"
by (blast elim: less_asym)

text \<open>Transitivity rules for calculational reasoning\<close>

lemma less_asym': "a Dual order\<close>

lemma dual_preorder:
 "class.preorder (\) (>)"
 by standard (auto simp add: less_le_not_le intro: order_trans)

end

subsection \<open>Partial orders\<close>

class order = preorder +
 assumes antisym: "x \ y \ y \ x \ x = y"
begin

lemma less_le: "x < y \ x \ y \ x \ y"
 by (auto simp add: less_le_not_le intro: antisym)

sublocale order: ordering less_eq less + dual_order: ordering greater_eq greater
proof -
 interpret ordering less_eq less
 by standard (auto intro: antisym order_trans simp add: less_le)
 show "ordering less_eq less"
 by (fact ordering_axioms)
 then show "ordering greater_eq greater"
 by (rule ordering_dualI)
qed

text \<open>Reflexivity.\<close>

lemma le_less: "x \ y \ x < y \ x = y"
 \<comment> \<open>NOT suitable for iff, since it can cause PROOF FAILED.\<close>
by (fact order.order_iff_strict)

lemma le_imp_less_or_eq: "x \ y \ x < y \ x = y"
by (simp add: less_le)

text \<open>Useful for simplification, but too risky to include by default.\<close>

lemma less_imp_not_eq: "x < y \ (x = y) \ False"
by auto

lemma less_imp_not_eq2: "x < y \ (y = x) \ False"
by auto

text \<open>Transitivity rules for calculational reasoning\<close>

lemma neq_le_trans: "a \ b \ a \ b \ a < b"
by (fact order.not_eq_order_implies_strict)

lemma le_neq_trans: "a \ b \ a \ b \ a < b"
by (rule order.not_eq_order_implies_strict)

text \<open>Asymmetry.\<close>

lemma eq_iff: "x = y \ x \ y \ y \ x"
 by (fact order.eq_iff)

lemma antisym_conv: "y \ x \ x \ y \ x = y"
 by (simp add: eq_iff)

lemma less_imp_neq: "x < y \ x \ y"
 by (fact order.strict_implies_not_eq)

lemma antisym_conv1: "\ x < y \ x \ y \ x = y"
 by (simp add: local.le_less)

lemma antisym_conv2: "x \ y \ \ x < y \ x = y"
 by (simp add: local.less_le)

lemma leD: "y \ x \ \ x < y"
 by (auto simp: less_le antisym)

text \<open>Least value operator\<close>

definition (in ord)
 Least :: "('a \ bool) \ 'a" (binder "LEAST " 10) where
 "Least P = (THE x. P x \ (\y. P y \ x \ y))"

lemma Least_equality:
 assumes "P x"
 and "\y. P y \ x \ y"
 shows "Least P = x"
unfolding Least_def by (rule the_equality)
 (blast intro: assms antisym)+

lemma LeastI2_order:
 assumes "P x"
 and "\y. P y \ x \ y"
 and "\x. P x \ \y. P y \ x \ y \ Q x"
 shows "Q (Least P)"
unfolding Least_def by (rule theI2)
 (blast intro: assms antisym)+

lemma Least_ex1:
 assumes "\!x. P x \ (\y. P y \ x \ y)"
 shows Least1I: "P (Least P)" and Least1_le: "P z \ Least P \ z"
 using theI'[OF assms]
 unfolding Least_def
 by auto

text \<open>Greatest value operator\<close>

definition Greatest :: "('a \ bool) \ 'a" (binder "GREATEST " 10) where
"Greatest P = (THE x. P x \ (\y. P y \ x \ y))"

lemma GreatestI2_order:
 "\ P x;
 \<And>y. P y \<Longrightarrow> x \<ge> y;
 \<And>x. \<lbrakk> P x; \<forall>y. P y \<longrightarrow> x \<ge> y \<rbrakk> \<Longrightarrow> Q x \<rbrakk>
 \<Longrightarrow> Q (Greatest P)"
unfolding Greatest_def
by (rule theI2) (blast intro: antisym)+

lemma Greatest_equality:
 "\ P x; \y. P y \ x \ y \ \ Greatest P = x"
unfolding Greatest_def
by (rule the_equality) (blast intro: antisym)+

end

lemma ordering_orderI:
 fixes less_eq (infix "\<^bold>\" 50)
 and less (infix "\<^bold><" 50)
 assumes "ordering less_eq less"
 shows "class.order less_eq less"
proof -
 from assms interpret ordering less_eq less .
 show ?thesis
 by standard (auto intro: antisym trans simp add: refl strict_iff_order)
qed

lemma order_strictI:
 fixes less (infix "\" 50)
 and less_eq (infix "\" 50)
 assumes "\a b. a \ b \ a \ b \ a = b"
 assumes "\a b. a \ b \ \ b \ a"
 assumes "\a. \ a \ a"
 assumes "\a b c. a \ b \ b \ c \ a \ c"
 shows "class.order less_eq less"
 by (rule ordering_orderI) (rule ordering_strictI, (fact assms)+)

context order
begin

text \<open>Dual order\<close>

lemma dual_order:
 "class.order (\) (>)"
 using dual_order.ordering_axioms by (rule ordering_orderI)

end

subsection \<open>Linear (total) orders\<close>

class linorder = order +
 assumes linear: "x \ y \ y \ x"
begin

lemma less_linear: "x < y \ x = y \ y < x"
unfolding less_le using less_le linear by blast

lemma le_less_linear: "x \ y \ y < x"
by (simp add: le_less less_linear)

lemma le_cases [case_names le ge]:
 "(x \ y \ P) \ (y \ x \ P) \ P"
using linear by blast

lemma (in linorder) le_cases3:
 "\\x \ y; y \ z\ \ P; \y \ x; x \ z\ \ P; \x \ z; z \ y\ \ P;
 \<lbrakk>z \<le> y; y \<le> x\<rbrakk> \<Longrightarrow> P; \<lbrakk>y \<le> z; z \<le> x\<rbrakk> \<Longrightarrow> P; \<lbrakk>z \<le> x; x \<le> y\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
by (blast intro: le_cases)

lemma linorder_cases [case_names less equal greater]:
 "(x < y \ P) \ (x = y \ P) \ (y < x \ P) \ P"
using less_linear by blast

lemma linorder_wlog[case_names le sym]:
 "(\a b. a \ b \ P a b) \ (\a b. P b a \ P a b) \ P a b"
 by (cases rule: le_cases[of a b]) blast+

lemma not_less: "\ x < y \ y \ x"
 unfolding less_le
 using linear by (blast intro: antisym)

lemma not_less_iff_gr_or_eq: "$x < y) \ (x > y \ x = y)"
 by (auto simp add:not_less le_less)

lemma not_le: "\ x \ y \ y < x"
 unfolding less_le
 using linear by (blast intro: antisym)

lemma neq_iff: "x \ y \ x < y \ y < x"
by (cut_tac x = x and y = y in less_linear, auto)

lemma neqE: "x \ y \ (x < y \ R) \ (y < x \ R) \ R"
by (simp add: neq_iff) blast

lemma antisym_conv3: "\ y < x \ \ x < y \ x = y"
by (blast intro: antisym dest: not_less [THEN iffD1])

lemma leI: "\ x < y \ y \ x"
unfolding not_less .

lemma not_le_imp_less: "\ y \ x \ x < y"
unfolding not_le .

lemma linorder_less_wlog[case_names less refl sym]:
 "\\a b. a Dual order\<close>

lemma dual_linorder:
 "class.linorder ($ (>)"
by (rule class.linorder.intro, rule dual_order) (unfold_locales, rule linear)

end

text \<open>Alternative introduction rule with bias towards strict order\<close>

lemma linorder_strictI:
 fixes less_eq (infix "\<^bold>\" 50)
 and less (infix "\<^bold><" 50)
 assumes "class.order less_eq less"
 assumes trichotomy: "\a b. a \<^bold>< a"
 shows "class.linorder less_eq less"
proof -
 interpret order less_eq less
 by (fact \<open>class.order less_eq less\<close>)
 show ?thesis
 proof
 fix a b
 show "a \<^bold>\ b \ b \<^bold>\ a"
 using trichotomy by (auto simp add: le_less)
 qed
qed

subsection \<open>Reasoning tools setup\<close>

ML \<open>
signature ORDERS =
sig
 val print_structures: Proof.context -> unit
 val order_tac: Proof.context -> thm list -> int -> tactic
 val add_struct: string * term list -> string -> attribute
 val del_struct: string * term list -> attribute
end;

structure Orders: ORDERS =
struct

(* context data *)

fun struct_eq ((s1: string, ts1), (s2, ts2)) =
 s1 = s2 andalso eq_list (op aconv) (ts1, ts2);

structure Data = Generic_Data
(
 type T = ((string * term list) * Order_Tac.less_arith) list;
 (* Order structures:
 identifier of the structure, list of operations and record of theorems
 needed to set up the transitivity reasoner,
 identifier and operations identify the structure uniquely. *)
 val empty = [];
 val extend = I;
 fun merge data = AList.join struct_eq (K fst) data;
);

fun print_structures ctxt =
 let
 val structs = Data.get (Context.Proof ctxt);
 fun pretty_term t = Pretty.block
 [Pretty.quote (Syntax.pretty_term ctxt t), Pretty.brk 1,
 Pretty.str "::", Pretty.brk 1,
 Pretty.quote (Syntax.pretty_typ ctxt (type_of t))];
 fun pretty_struct ((s, ts), _) = Pretty.block
 [Pretty.str s, Pretty.str ":", Pretty.brk 1,
 Pretty.enclose "(" ")" (Pretty.breaks (map pretty_term ts))];
 in
 Pretty.writeln (Pretty.big_list "order structures:" (map pretty_struct structs))
 end;

val _ =
 Outer_Syntax.command \<^command_keyword>\<open>print_orders\<close>
 "print order structures available to transitivity reasoner"
 (Scan.succeed (Toplevel.keep (print_structures o Toplevel.context_of)));

(* tactics *)

fun struct_tac ((s, ops), thms) ctxt facts =
 let
 val [eq, le, less] = ops;
 fun decomp thy (\<^const>\<open>Trueprop\<close> $ t) =
 let
 fun excluded t =
 (* exclude numeric types: linear arithmetic subsumes transitivity *)
 let val T = type_of t
 in
 T = HOLogic.natT orelse T = HOLogic.intT orelse T = HOLogic.realT
 end;
 fun rel (bin_op $ t1 $ t2) =
 if excluded t1 then NONE
 else if Pattern.matches thy (eq, bin_op) then SOME (t1, "=", t2)
 else if Pattern.matches thy (le, bin_op) then SOME (t1, "<=", t2)
 else if Pattern.matches thy (less, bin_op) then SOME (t1, "<", t2)
 else NONE
 | rel _ = NONE;
 fun dec (Const (\<^const_name>\<open>Not\<close>, _) $ t) =
 (case rel t of NONE =>
 NONE
 | SOME (t1, rel, t2) => SOME (t1, "~" ^ rel, t2))
 | dec x = rel x;
 in dec t end
 | decomp _ _ = NONE;
 in
 (case s of
 "order" => Order_Tac.partial_tac decomp thms ctxt facts
 | "linorder" => Order_Tac.linear_tac decomp thms ctxt facts
 | _ => error ("Unknown order kind " ^ quote s ^ " encountered in transitivity reasoner"))
 end

fun order_tac ctxt facts =
 FIRST' (map (fn s => CHANGED o struct_tac s ctxt facts) (Data.get (Context.Proof ctxt)));

(* attributes *)

fun add_struct s tag =
 Thm.declaration_attribute
 (fn thm => Data.map (AList.map_default struct_eq (s, Order_Tac.empty TrueI) (Order_Tac.update tag thm)));
fun del_struct s =
 Thm.declaration_attribute
 (fn _ => Data.map (AList.delete struct_eq s));

end;
\<close>

attribute_setup order = \<open>
 Scan.lift ((Args.add -- Args.name >> (fn (_, s) => SOME s) || Args.del >> K NONE) --|
 Args.colon (* FIXME || Scan.succeed true *) ) -- Scan.lift Args.name --
 Scan.repeat Args.term
 >> (fn ((SOME tag, n), ts) => Orders.add_struct (n, ts) tag
 | ((NONE, n), ts) => Orders.del_struct (n, ts))
\<close> "theorems controlling transitivity reasoner"

method_setup order = \<open>
 Scan.succeed (fn ctxt => SIMPLE_METHOD' (Orders.order_tac ctxt []))
\<close> "transitivity reasoner"

text \<open>Declarations to set up transitivity reasoner of partial and linear orders.\<close>

context order
begin

(* The type constraint on @{term (=}) below is necessary since the operation
 is not a parameter of the locale. *)

declare less_irrefl [THEN notE, order add less_reflE: order "(=) :: 'a \ 'a \ bool" "(<=)" "(<)"]

declare order_refl [order add le_refl: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]

declare less_imp_le [order add less_imp_le: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]

declare antisym [order add eqI: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]

declare eq_refl [order add eqD1: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]

declare sym [THEN eq_refl, order add eqD2: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]

declare less_trans [order add less_trans: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]

declare less_le_trans [order add less_le_trans: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]

declare le_less_trans [order add le_less_trans: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]

declare order_trans [order add le_trans: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]

declare le_neq_trans [order add le_neq_trans: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]

declare neq_le_trans [order add neq_le_trans: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]

declare less_imp_neq [order add less_imp_neq: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]

declare eq_neq_eq_imp_neq [order add eq_neq_eq_imp_neq: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]

declare not_sym [order add not_sym: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]

end

context linorder
begin

declare [[order del: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]]

declare less_irrefl [THEN notE, order add less_reflE: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]

declare order_refl [order add le_refl: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]

declare less_imp_le [order add less_imp_le: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]

declare not_less [THEN iffD2, order add not_lessI: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]

declare not_le [THEN iffD2, order add not_leI: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]

declare not_less [THEN iffD1, order add not_lessD: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]

declare not_le [THEN iffD1, order add not_leD: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]

declare antisym [order add eqI: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]

declare eq_refl [order add eqD1: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]

declare sym [THEN eq_refl, order add eqD2: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]

declare less_trans [order add less_trans: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]

declare less_le_trans [order add less_le_trans: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]

declare le_less_trans [order add le_less_trans: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]

declare order_trans [order add le_trans: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]

declare le_neq_trans [order add le_neq_trans: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]

declare neq_le_trans [order add neq_le_trans: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]

declare less_imp_neq [order add less_imp_neq: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]

declare eq_neq_eq_imp_neq [order add eq_neq_eq_imp_neq: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]

declare not_sym [order add not_sym: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]

end

setup \<open>
 map_theory_simpset (fn ctxt0 => ctxt0 addSolver
 mk_solver "Transitivity" (fn ctxt => Orders.order_tac ctxt (Simplifier.prems_of ctxt)))
 (*Adding the transitivity reasoners also as safe solvers showed a slight
 speed up, but the reasoning strength appears to be not higher (at least
 no breaking of additional proofs in the entire HOL distribution, as
 of 5 March 2004, was observed).*)
\<close>

ML \<open>
local
 fun prp t thm = Thm.prop_of thm = t; (* FIXME proper aconv!? *)
in

fun antisym_le_simproc ctxt ct =
 (case Thm.term_of ct of
 (le as Const (_, T)) $ r $ s =>
 (let
 val prems = Simplifier.prems_of ctxt;
 val less = Const (\<^const_name>\<open>less\<close>, T);
 val t = HOLogic.mk_Trueprop(le $ s $ r);
 in
 (case find_first (prp t) prems of
 NONE =>
 let val t = HOLogic.mk_Trueprop(HOLogic.Not $ (less $ r $ s)) in
 (case find_first (prp t) prems of
 NONE => NONE
 | SOME thm => SOME(mk_meta_eq(thm RS @{thm antisym_conv1})))
 end
 | SOME thm => SOME (mk_meta_eq (thm RS @{thm order_class.antisym_conv})))
 end handle THM _ => NONE)
 | _ => NONE);

fun antisym_less_simproc ctxt ct =
 (case Thm.term_of ct of
 NotC $ ((less as Const(_,T)) $ r $ s) =>
 (let
 val prems = Simplifier.prems_of ctxt;
 val le = Const (\<^const_name>\<open>less_eq\<close>, T);
 val t = HOLogic.mk_Trueprop(le $ r $ s);
 in
 (case find_first (prp t) prems of
 NONE =>
 let val t = HOLogic.mk_Trueprop (NotC $ (less $ s $ r)) in
 (case find_first (prp t) prems of
 NONE => NONE
 | SOME thm => SOME (mk_meta_eq(thm RS @{thm linorder_class.antisym_conv3})))
 end
 | SOME thm => SOME (mk_meta_eq (thm RS @{thm antisym_conv2})))
 end handle THM _ => NONE)
 | _ => NONE);

end;
\<close>

simproc_setup antisym_le ("(x::'a::order) \ y") = "K antisym_le_simproc"
simproc_setup antisym_less ("\ (x::'a::linorder) < y") = "K antisym_less_simproc"

subsection \<open>Bounded quantifiers\<close>

syntax (ASCII)
 "_All_less" :: "[idt, 'a, bool] => bool" ("(3ALL _<_./ _)" [0, 0, 10] 10)
 "_Ex_less" :: "[idt, 'a, bool] => bool" ("(3EX _<_./ _)" [0, 0, 10] 10)
 "_All_less_eq" :: "[idt, 'a, bool] => bool" ("(3ALL _<=_./ _)" [0, 0, 10] 10)
 "_Ex_less_eq" :: "[idt, 'a, bool] => bool" ("(3EX _<=_./ _)" [0, 0, 10] 10)

 "_All_greater" :: "[idt, 'a, bool] => bool" ("(3ALL _>_./ _)" [0, 0, 10] 10)
 "_Ex_greater" :: "[idt, 'a, bool] => bool" ("(3EX _>_./ _)" [0, 0, 10] 10)
 "_All_greater_eq" :: "[idt, 'a, bool] => bool" ("(3ALL _>=_./ _)" [0, 0, 10] 10)
 "_Ex_greater_eq" :: "[idt, 'a, bool] => bool" ("(3EX _>=_./ _)" [0, 0, 10] 10)

 "_All_neq" :: "[idt, 'a, bool] => bool" ("(3ALL _~=_./ _)" [0, 0, 10] 10)
 "_Ex_neq" :: "[idt, 'a, bool] => bool" ("(3EX _~=_./ _)" [0, 0, 10] 10)

syntax
 "_All_less" :: "[idt, 'a, bool] => bool" ("(3\_<_./ _)" [0, 0, 10] 10)
 "_Ex_less" :: "[idt, 'a, bool] => bool" ("(3\_<_./ _)" [0, 0, 10] 10)
 "_All_less_eq" :: "[idt, 'a, bool] => bool" ("(3\_\_./ _)" [0, 0, 10] 10)
 "_Ex_less_eq" :: "[idt, 'a, bool] => bool" ("(3\_\_./ _)" [0, 0, 10] 10)

 "_All_greater" :: "[idt, 'a, bool] => bool" ("(3\_>_./ _)" [0, 0, 10] 10)
 "_Ex_greater" :: "[idt, 'a, bool] => bool" ("(3\_>_./ _)" [0, 0, 10] 10)
 "_All_greater_eq" :: "[idt, 'a, bool] => bool" ("(3\_\_./ _)" [0, 0, 10] 10)
 "_Ex_greater_eq" :: "[idt, 'a, bool] => bool" ("(3\_\_./ _)" [0, 0, 10] 10)

 "_All_neq" :: "[idt, 'a, bool] => bool" ("(3\_\_./ _)" [0, 0, 10] 10)
 "_Ex_neq" :: "[idt, 'a, bool] => bool" ("(3\_\_./ _)" [0, 0, 10] 10)

syntax (input)
 "_All_less" :: "[idt, 'a, bool] => bool" ("(3! _<_./ _)" [0, 0, 10] 10)
 "_Ex_less" :: "[idt, 'a, bool] => bool" ("(3? _<_./ _)" [0, 0, 10] 10)
 "_All_less_eq" :: "[idt, 'a, bool] => bool" ("(3! _<=_./ _)" [0, 0, 10] 10)
 "_Ex_less_eq" :: "[idt, 'a, bool] => bool" ("(3? _<=_./ _)" [0, 0, 10] 10)
 "_All_neq" :: "[idt, 'a, bool] => bool" ("(3! _~=_./ _)" [0, 0, 10] 10)
 "_Ex_neq" :: "[idt, 'a, bool] => bool" ("(3? _~=_./ _)" [0, 0, 10] 10)

translations
 "\x "\x. x < y \ P"
 "\x "\x. x < y \ P"
 "\x\y. P" \ "\x. x \ y \ P"
 "\x\y. P" \ "\x. x \ y \ P"
 "\x>y. P" \ "\x. x > y \ P"
 "\x>y. P" \ "\x. x > y \ P"
 "\x\y. P" \ "\x. x \ y \ P"
 "\x\y. P" \ "\x. x \ y \ P"
 "\x\y. P" \ "\x. x \ y \ P"
 "\x\y. P" \ "\x. x \ y \ P"

print_translation \<open>
let
 val All_binder = Mixfix.binder_name \<^const_syntax>\<open>All\<close>;
 val Ex_binder = Mixfix.binder_name \<^const_syntax>\<open>Ex\<close>;
 val impl = \<^const_syntax>\<open>HOL.implies\<close>;
 val conj = \<^const_syntax>\<open>HOL.conj\<close>;
 val less = \<^const_syntax>\<open>less\<close>;
 val less_eq = \<^const_syntax>\<open>less_eq\<close>;

 val trans =
 [((All_binder, impl, less),
 (\<^syntax_const>\<open>_All_less\<close>, \<^syntax_const>\<open>_All_greater\<close>)),
 ((All_binder, impl, less_eq),
 (\<^syntax_const>\<open>_All_less_eq\<close>, \<^syntax_const>\<open>_All_greater_eq\<close>)),
 ((Ex_binder, conj, less),
 (\<^syntax_const>\<open>_Ex_less\<close>, \<^syntax_const>\<open>_Ex_greater\<close>)),
 ((Ex_binder, conj, less_eq),
 (\<^syntax_const>\<open>_Ex_less_eq\<close>, \<^syntax_const>\<open>_Ex_greater_eq\<close>))];

 fun matches_bound v t =
 (case t of
 Const (\<^syntax_const>\<open>_bound\<close>, _) $ Free (v', _) => v = v'
 | _ => false);
 fun contains_var v = Term.exists_subterm (fn Free (x, _) => x = v | _ => false);
 fun mk x c n P = Syntax.const c $ Syntax_Trans.mark_bound_body x $ n $ P;

 fun tr' q = (q, fn _ =>
 (fn [Const (\<^syntax_const>\<open>_bound\<close>, _) $ Free (v, T),
 Const (c, _) $ (Const (d, _) $ t $ u) $ P] =>
 (case AList.lookup (=) trans (q, c, d) of
 NONE => raise Match
 | SOME (l, g) =>
 if matches_bound v t andalso not (contains_var v u) then mk (v, T) l u P
 else if matches_bound v u andalso not (contains_var v t) then mk (v, T) g t P
 else raise Match)
 | _ => raise Match));
in [tr' All_binder, tr' Ex_binder] end
\<close>

subsection \<open>Transitivity reasoning\<close>

context ord
begin

lemma ord_le_eq_trans: "a \ b \ b = c \ a \ c"
 by (rule subst)

lemma ord_eq_le_trans: "a = b \ b \ c \ a \ c"
 by (rule ssubst)

lemma ord_less_eq_trans: "a f b < (c::'c::order) ==>
 (!!x y. x < y ==> f x < f y) ==> f a < c"
proof -
 assume r: "!!x y. x < y ==> f x < f y"
 assume "a < b" hence "f a < f b" by (rule r)
 also assume "f b < c"
 finally (less_trans) show ?thesis .
qed

lemma order_less_subst1: "(a::'a::order) < f b ==> (b::'b::order) < c ==>
 (!!x y. x < y ==> f x < f y) ==> a < f c"
proof -
 assume r: "!!x y. x < y ==> f x < f y"
 assume "a < f b"
 also assume "b < c" hence "f b < f c" by (rule r)
 finally (less_trans) show ?thesis .
qed

lemma order_le_less_subst2: "(a::'a::order) <= b ==> f b < (c::'c::order) ==>
 (!!x y. x <= y ==> f x <= f y) ==> f a < c"
proof -
 assume r: "!!x y. x <= y ==> f x <= f y"
 assume "a <= b" hence "f a <= f b" by (rule r)
 also assume "f b < c"
 finally (le_less_trans) show ?thesis .
qed

lemma order_le_less_subst1: "(a::'a::order) <= f b ==> (b::'b::order) < c ==>
 (!!x y. x < y ==> f x < f y) ==> a < f c"
proof -
 assume r: "!!x y. x < y ==> f x < f y"
 assume "a <= f b"
 also assume "b < c" hence "f b < f c" by (rule r)
 finally (le_less_trans) show ?thesis .
qed

lemma order_less_le_subst2: "(a::'a::order) f b <= (c::'c::order) ==>
 (!!x y. x < y ==> f x < f y) ==> f a < c"
proof -
 assume r: "!!x y. x < y ==> f x < f y"
 assume "a < b" hence "f a < f b" by (rule r)
 also assume "f b <= c"
 finally (less_le_trans) show ?thesis .
qed

lemma order_less_le_subst1: "(a::'a::order) < f b ==> (b::'b::order) <= c ==>
 (!!x y. x <= y ==> f x <= f y) ==> a < f c"
proof -
 assume r: "!!x y. x <= y ==> f x <= f y"
 assume "a < f b"
 also assume "b <= c" hence "f b <= f c" by (rule r)
 finally (less_le_trans) show ?thesis .
qed

lemma order_subst1: "(a::'a::order) <= f b ==> (b::'b::order) <= c ==>
 (!!x y. x <= y ==> f x <= f y) ==> a <= f c"
proof -
 assume r: "!!x y. x <= y ==> f x <= f y"
 assume "a <= f b"
 also assume "b <= c" hence "f b <= f c" by (rule r)
 finally (order_trans) show ?thesis .
qed

lemma order_subst2: "(a::'a::order) <= b ==> f b <= (c::'c::order) ==>
 (!!x y. x <= y ==> f x <= f y) ==> f a <= c"
proof -
 assume r: "!!x y. x <= y ==> f x <= f y"
 assume "a <= b" hence "f a <= f b" by (rule r)
 also assume "f b <= c"
 finally (order_trans) show ?thesis .
qed

lemma ord_le_eq_subst: "a <= b ==> f b = c ==>
 (!!x y. x <= y ==> f x <= f y) ==> f a <= c"
proof -
 assume r: "!!x y. x <= y ==> f x <= f y"
 assume "a <= b" hence "f a <= f b" by (rule r)
 also assume "f b = c"
 finally (ord_le_eq_trans) show ?thesis .
qed

lemma ord_eq_le_subst: "a = f b ==> b <= c ==>
 (!!x y. x <= y ==> f x <= f y) ==> a <= f c"
proof -
 assume r: "!!x y. x <= y ==> f x <= f y"
 assume "a = f b"
 also assume "b <= c" hence "f b <= f c" by (rule r)
 finally (ord_eq_le_trans) show ?thesis .
qed

lemma ord_less_eq_subst: "a f b = c ==>
 (!!x y. x < y ==> f x < f y) ==> f a < c"
proof -
 assume r: "!!x y. x < y ==> f x < f y"
 assume "a < b" hence "f a < f b" by (rule r)
 also assume "f b = c"
 finally (ord_less_eq_trans) show ?thesis .
qed

lemma ord_eq_less_subst: "a = f b ==> b < c ==>
 (!!x y. x < y ==> f x < f y) ==> a < f c"
proof -
 assume r: "!!x y. x < y ==> f x < f y"
 assume "a = f b"
 also assume "b < c" hence "f b < f c" by (rule r)
 finally (ord_eq_less_trans) show ?thesis .
qed

text \<open>
 Note that this list of rules is in reverse order of priorities.
\<close>

lemmas [trans] =
 order_less_subst2
 order_less_subst1
 order_le_less_subst2
 order_le_less_subst1
 order_less_le_subst2
 order_less_le_subst1
 order_subst2
 order_subst1
 ord_le_eq_subst
 ord_eq_le_subst
 ord_less_eq_subst
 ord_eq_less_subst
 forw_subst
 back_subst
 rev_mp
 mp

lemmas (in order) [trans] =
 neq_le_trans
 le_neq_trans

lemmas (in preorder) [trans] =
 less_trans
 less_asym'
 le_less_trans
 less_le_trans
 order_trans

lemmas (in order) [trans] =
 antisym

lemmas (in ord) [trans] =
 ord_le_eq_trans
 ord_eq_le_trans
 ord_less_eq_trans
 ord_eq_less_trans

lemmas [trans] =
 trans

lemmas order_trans_rules =
 order_less_subst2
 order_less_subst1
 order_le_less_subst2
 order_le_less_subst1
 order_less_le_subst2
 order_less_le_subst1
 order_subst2
 order_subst1
 ord_le_eq_subst
 ord_eq_le_subst
 ord_less_eq_subst
 ord_eq_less_subst
 forw_subst
 back_subst
 rev_mp
 mp
 neq_le_trans
 le_neq_trans
 less_trans
 less_asym'
 le_less_trans
 less_le_trans
 order_trans
 antisym
 ord_le_eq_trans
 ord_eq_le_trans
 ord_less_eq_trans
 ord_eq_less_trans
 trans

text \<open>These support proving chains of decreasing inequalities
 a >= b >= c ... in Isar proofs.\<close>

lemma xt1 [no_atp]:
 "a = b \ b > c \ a > c"
 "a > b \ b = c \ a > c"
 "a = b \ b \ c \ a \ c"
 "a \ b \ b = c \ a \ c"
 "(x::'a::order) \ y \ y \ x \ x = y"
 "(x::'a::order) \ y \ y \ z \ x \ z"
 "(x::'a::order) > y \ y \ z \ x > z"
 "(x::'a::order) \ y \ y > z \ x > z"
 "(a::'a::order) > b \ b > a \ P"
 "(x::'a::order) > y \ y > z \ x > z"
 "(a::'a::order) \ b \ a \ b \ a > b"
 "(a::'a::order) \ b \ a \ b \ a > b"
 "a = f b \ b > c \ (\x y. x > y \ f x > f y) \ a > f c"
 "a > b \ f b = c \ (\x y. x > y \ f x > f y) \ f a > c"
 "a = f b \ b \ c \ (\x y. x \ y \ f x \ f y) \ a \ f c"
 "a \ b \ f b = c \ (\x y. x \ y \ f x \ f y) \ f a \ c"
 by auto

lemma xt2 [no_atp]:
 "(a::'a::order) >= f b ==> b >= c ==> (!!x y. x >= y ==> f x >= f y) ==> a >= f c"
by (subgoal_tac "f b >= f c", force, force)

lemma xt3 [no_atp]: "(a::'a::order) >= b ==> (f b::'b::order) >= c ==>
 (!!x y. x >= y ==> f x >= f y) ==> f a >= c"
by (subgoal_tac "f a >= f b", force, force)

lemma xt4 [no_atp]: "(a::'a::order) > f b ==> (b::'b::order) >= c ==>
 (!!x y. x >= y ==> f x >= f y) ==> a > f c"
by (subgoal_tac "f b >= f c", force, force)

lemma xt5 [no_atp]: "(a::'a::order) > b ==> (f b::'b::order) >= c==>
 (!!x y. x > y ==> f x > f y) ==> f a > c"
by (subgoal_tac "f a > f b", force, force)

lemma xt6 [no_atp]: "(a::'a::order) >= f b ==> b > c ==>
 (!!x y. x > y ==> f x > f y) ==> a > f c"
by (subgoal_tac "f b > f c", force, force)

lemma xt7 [no_atp]: "(a::'a::order) >= b ==> (f b::'b::order) > c ==>
 (!!x y. x >= y ==> f x >= f y) ==> f a > c"
by (subgoal_tac "f a >= f b", force, force)

lemma xt8 [no_atp]: "(a::'a::order) > f b ==> (b::'b::order) > c ==>
 (!!x y. x > y ==> f x > f y) ==> a > f c"
by (subgoal_tac "f b > f c", force, force)

lemma xt9 [no_atp]: "(a::'a::order) > b ==> (f b::'b::order) > c ==>
 (!!x y. x > y ==> f x > f y) ==> f a > c"
by (subgoal_tac "f a > f b", force, force)

lemmas xtrans = xt1 xt2 xt3 xt4 xt5 xt6 xt7 xt8 xt9

(*
 Since "a >= b" abbreviates "b <= a", the abbreviation "..." stands
 for the wrong thing in an Isar proof.

 The extra transitivity rules can be used as follows:

lemma "(a::'a::order) > z"
proof -
 have "a >= b" (is "_ >= ?rhs")
 sorry
 also have "?rhs >= c" (is "_ >= ?rhs")
 sorry
 also (xtrans) have "?rhs = d" (is "_ = ?rhs")
 sorry
 also (xtrans) have "?rhs >= e" (is "_ >= ?rhs")
 sorry
 also (xtrans) have "?rhs > f" (is "_ > ?rhs")
 sorry
 also (xtrans) have "?rhs > z"
 sorry
 finally (xtrans) show ?thesis .
qed

 Alternatively, one can use "declare xtrans [trans]" and then
 leave out the "(xtrans)" above.
*)

subsection \<open>Monotonicity\<close>

context order
begin

definition mono :: "('a \ 'b::order) \ bool" where
 "mono f \ (\x y. x \ y \ f x \ f y)"

lemma monoI [intro?]:
 fixes f :: "'a \ 'b::order"
 shows "(\x y. x \ y \ f x \ f y) \ mono f"
 unfolding mono_def by iprover

lemma monoD [dest?]:
 fixes f :: "'a \ 'b::order"
 shows "mono f \ x \ y \ f x \ f y"
 unfolding mono_def by iprover

lemma monoE:
 fixes f :: "'a \ 'b::order"
 assumes "mono f"
 assumes "x \ y"
 obtains "f x \ f y"
proof
 from assms show "f x \ f y" by (simp add: mono_def)
qed

definition antimono :: "('a \ 'b::order) \ bool" where
 "antimono f \ (\x y. x \ y \ f x \ f y)"

lemma antimonoI [intro?]:
 fixes f :: "'a \ 'b::order"
 shows "(\x y. x \ y \ f x \ f y) \ antimono f"
 unfolding antimono_def by iprover

lemma antimonoD [dest?]:
 fixes f :: "'a \ 'b::order"
 shows "antimono f \ x \ y \ f x \ f y"
 unfolding antimono_def by iprover

lemma antimonoE:
 fixes f :: "'a \ 'b::order"
 assumes "antimono f"
 assumes "x \ y"
 obtains "f x \ f y"
proof
 from assms show "f x \ f y" by (simp add: antimono_def)
qed

definition strict_mono :: "('a \ 'b::order) \ bool" where
 "strict_mono f \ (\x y. x < y \ f x < f y)"

lemma strict_monoI [intro?]:
 assumes "\x y. x < y \ f x < f y"
 shows "strict_mono f"
 using assms unfolding strict_mono_def by auto

lemma strict_monoD [dest?]:
 "strict_mono f \ x < y \ f x < f y"
 unfolding strict_mono_def by auto

lemma strict_mono_mono [dest?]:
 assumes "strict_mono f"
 shows "mono f"
proof (rule monoI)
 fix x y
 assume "x \ y"
 show "f x \ f y"
 proof (cases "x = y")
 case True then show ?thesis by simp
 next
 case False with \<open>x \<le> y\<close> have "x < y" by simp
 with assms strict_monoD have "f x < f y" by auto
 then show ?thesis by simp
 qed
qed

end

context linorder
begin

lemma mono_invE:
 fixes f :: "'a \ 'b::order"
 assumes "mono f"
 assumes "f x < f y"
 obtains "x \ y"
proof
 show "x \ y"
 proof (rule ccontr)
 assume "\ x \ y"
 then have "y \ x" by simp
 with \<open>mono f\<close> obtain "f y \<le> f x" by (rule monoE)
 with \<open>f x < f y\<close> show False by simp
 qed
qed

lemma mono_strict_invE:
 fixes f :: "'a \ 'b::order"
 assumes "mono f"
 assumes "f x < f y"
 obtains "x < y"
proof
 show "x < y"
 proof (rule ccontr)
 assume "\ x < y"
 then have "y \ x" by simp
 with \<open>mono f\<close> obtain "f y \<le> f x" by (rule monoE)
 with \<open>f x < f y\<close> show False by simp
 qed
qed

lemma strict_mono_eq:
 assumes "strict_mono f"
 shows "f x = f y \ x = y"
proof
 assume "f x = f y"
 show "x = y" proof (cases x y rule: linorder_cases)
 case less with assms strict_monoD have "f x < f y" by auto
 with \<open>f x = f y\<close> show ?thesis by simp
 next
 case equal then show ?thesis .
 next
 case greater with assms strict_monoD have "f y < f x" by auto
 with \<open>f x = f y\<close> show ?thesis by simp
 qed
qed simp

lemma strict_mono_less_eq:
 assumes "strict_mono f"
 shows "f x \ f y \ x \ y"
proof
 assume "x \ y"
 with assms strict_mono_mono monoD show "f x \ f y" by auto
next
 assume "f x \ f y"
 show "x \ y" proof (rule ccontr)
 assume "\ x \ y" then have "y < x" by simp
 with assms strict_monoD have "f y < f x" by auto
 with \<open>f x \<le> f y\<close> show False by simp
 qed
qed

lemma strict_mono_less:
 assumes "strict_mono f"
 shows "f x < f y \ x < y"
 using assms
 by (auto simp add: less_le Orderings.less_le strict_mono_eq strict_mono_less_eq)

end

subsection \<open>min and max -- fundamental\<close>

definition (in ord) min :: "'a \ 'a \ 'a" where
 "min a b = (if a \ b then a else b)"

definition (in ord) max :: "'a \ 'a \ 'a" where
 "max a b = (if a \ b then b else a)"

lemma min_absorb1: "x \ y \ min x y = x"
 by (simp add: min_def)

lemma max_absorb2: "x \ y \ max x y = y"
 by (simp add: max_def)

lemma min_absorb2: "(y::'a::order) \ x \ min x y = y"
 by (simp add:min_def)

lemma max_absorb1: "(y::'a::order) \ x \ max x y = x"
 by (simp add: max_def)

lemma max_min_same [simp]:
 fixes x y :: "'a :: linorder"
 shows "max x (min x y) = x" "max (min x y) x = x" "max (min x y) y = y" "max y (min x y) = y"
by(auto simp add: max_def min_def)

subsection \<open>(Unique) top and bottom elements\<close>

class bot =
 fixes bot :: 'a ("\")

class order_bot = order + bot +
 assumes bot_least: "\ \ a"
begin

sublocale bot: ordering_top greater_eq greater bot
 by standard (fact bot_least)

lemma le_bot:
 "a \ \ \ a = \"
 by (fact bot.extremum_uniqueI)

lemma bot_unique:
 "a \ \ \ a = \"
 by (fact bot.extremum_unique)

lemma not_less_bot:
 "\ a < \"
 by (fact bot.extremum_strict)

lemma bot_less:
 "a \ \ \ \ < a"
 by (fact bot.not_eq_extremum)

lemma max_bot[simp]: "max bot x = x"
by(simp add: max_def bot_unique)

lemma max_bot2[simp]: "max x bot = x"
by(simp add: max_def bot_unique)

lemma min_bot[simp]: "min bot x = bot"
by(simp add: min_def bot_unique)

lemma min_bot2[simp]: "min x bot = bot"
by(simp add: min_def bot_unique)

end

class top =
 fixes top :: 'a ("\")

class order_top = order + top +
 assumes top_greatest: "a \ \"
begin

sublocale top: ordering_top less_eq less top
 by standard (fact top_greatest)

lemma top_le:
 "\ \ a \ a = \"
 by (fact top.extremum_uniqueI)

lemma top_unique:
 "\ \ a \ a = \"
 by (fact top.extremum_unique)

lemma not_top_less:
 "\ \ < a"
 by (fact top.extremum_strict)

lemma less_top:
 "a \ \ \ a < \"
 by (fact top.not_eq_extremum)

lemma max_top[simp]: "max top x = top"
by(simp add: max_def top_unique)

lemma max_top2[simp]: "max x top = top"
by(simp add: max_def top_unique)

lemma min_top[simp]: "min top x = x"
by(simp add: min_def top_unique)

lemma min_top2[simp]: "min x top = x"
by(simp add: min_def top_unique)

end

subsection \<open>Dense orders\<close>

class dense_order = order +
 assumes dense: "x < y \ (\z. x < z \ z < y)"

class dense_linorder = linorder + dense_order
begin

lemma dense_le:
 fixes y z :: 'a
 assumes "\x. x < y \ x \ z"
 shows "y \ z"
proof (rule ccontr)
 assume "\ ?thesis"
 hence "z < y" by simp
 from dense[OF this]
 obtain x where "x < y" and "z < x" by safe
 moreover have "x \ z" using assms[OF \x < y\] .
 ultimately show False by auto
qed

lemma dense_le_bounded:
 fixes x y z :: 'a
 assumes "x < y"
 assumes *: "\w. \ x < w ; w < y \ \ w \ z"
 shows "y \ z"
proof (rule dense_le)
 fix w assume "w < y"
 from dense[OF \<open>x < y\<close>] obtain u where "x < u" "u < y" by safe
 from linear[of u w]
 show "w \ z"
 proof (rule disjE)
 assume "u \ w"
 from less_le_trans[OF \<open>x < u\<close> \<open>u \<le> w\<close>] \<open>w < y\<close>
 show "w \ z" by (rule *)
 next
 assume "w \ u"
 from \<open>w \<le> u\<close> *[OF \<open>x < u\<close> \<open>u < y\<close>]
 show "w \ z" by (rule order_trans)
 qed
qed

lemma dense_ge:
 fixes y z :: 'a
 assumes "\x. z < x \ y \ x"
 shows "y \ z"
proof (rule ccontr)
 assume "\ ?thesis"
 hence "z < y" by simp
 from dense[OF this]
 obtain x where "x < y" and "z < x" by safe
 moreover have "y \ x" using assms[OF \z < x\] .
 ultimately show False by auto
qed

lemma dense_ge_bounded:
 fixes x y z :: 'a
 assumes "z < x"
 assumes *: "\w. \ z < w ; w < x \ \ y \ w"
 shows "y \ z"
proof (rule dense_ge)
 fix w assume "z < w"
 from dense[OF \<open>z < x\<close>] obtain u where "z < u" "u < x" by safe
 from linear[of u w]
 show "y \ w"
 proof (rule disjE)
 assume "w \ u"
 from \<open>z < w\<close> le_less_trans[OF \<open>w \<le> u\<close> \<open>u < x\<close>]
 show "y \ w" by (rule *)
 next
 assume "u \ w"
 from *[OF \<open>z < u\<close> \<open>u < x\<close>] \<open>u \<le> w\<close>
 show "y \ w" by (rule order_trans)
 qed
qed

end

class no_top = order +
 assumes gt_ex: "\y. x < y"

class no_bot = order +
 assumes lt_ex: "\y. y < x"

class unbounded_dense_linorder = dense_linorder + no_top + no_bot

subsection \<open>Wellorders\<close>

class wellorder = linorder +
 assumes less_induct [case_names less]: "(\x. (\y. y < x \ P y) \ P x) \ P a"
begin

lemma wellorder_Least_lemma:
 fixes k :: 'a
 assumes "P k"
 shows LeastI: "P (LEAST x. P x)" and Least_le: "(LEAST x. P x) \ k"
proof -
 have "P (LEAST x. P x) \ (LEAST x. P x) \ k"
 using assms proof (induct k rule: less_induct)
 case (less x) then have "P x" by simp
 show ?case proof (rule classical)
 assume assm: "\ (P (LEAST a. P a) \ (LEAST a. P a) \ x)"
 have "\y. P y \ x \ y"
 proof (rule classical)
 fix y
 assume "P y" and "\ x \ y"
 with less have "P (LEAST a. P a)" and "(LEAST a. P a) \ y"
 by (auto simp add: not_le)
 with assm have "x < (LEAST a. P a)" and "(LEAST a. P a) \ y"
 by auto
 then show "x \ y" by auto
 qed
 with \<open>P x\<close> have Least: "(LEAST a. P a) = x"
 by (rule Least_equality)
 with \<open>P x\<close> show ?thesis by simp
 qed
 qed
 then show "P (LEAST x. P x)" and "(LEAST x. P x) \ k" by auto
qed

\<comment> \<open>The following 3 lemmas are due to Brian Huffman\<close>
lemma LeastI_ex: "\x. P x \ P (Least P)"
 by (erule exE) (erule LeastI)

lemma LeastI2:
 "P a \ (\x. P x \ Q x) \ Q (Least P)"
 by (blast intro: LeastI)

lemma LeastI2_ex:
 "\a. P a \ (\x. P x \ Q x) \ Q (Least P)"
 by (blast intro: LeastI_ex)

lemma LeastI2_wellorder:
 assumes "P a"
 and "\a. \ P a; \b. P b \ a \ b \ \ Q a"
 shows "Q (Least P)"
proof (rule LeastI2_order)
 show "P (Least P)" using \<open>P a\<close> by (rule LeastI)
next
 fix y assume "P y" thus "Least P \ y" by (rule Least_le)
next
 fix x assume "P x" "\y. P y \ x \ y" thus "Q x" by (rule assms(2))
qed

lemma LeastI2_wellorder_ex:
 assumes "\x. P x"
 and "\a. \ P a; \b. P b \ a \ b \ \ Q a"
 shows "Q (Least P)"
using assms by clarify (blast intro!: LeastI2_wellorder)

lemma not_less_Least: "k < (LEAST x. P x) \ \ P k"
apply (simp add: not_le [symmetric])
apply (erule contrapos_nn)
apply (erule Least_le)
done

lemma exists_least_iff: "(\n. P n) \ (\n. P n \ (\m < n. \ P m))" (is "?lhs \ ?rhs")
proof
 assume ?rhs thus ?lhs by blast
next
 assume H: ?lhs then obtain n where n: "P n" by blast
 let ?x = "Least P"
 { fix m assume m: "m < ?x"
 from not_less_Least[OF m] have "\ P m" . }
 with LeastI_ex[OF H] show ?rhs by blast
qed

end

subsection \<open>Order on \<^typ>\<open>bool\<close>\<close>

instantiation bool :: "{order_bot, order_top, linorder}"
begin

definition
 le_bool_def [simp]: "P \ Q \ P \ Q"

definition
 [simp]: "(P::bool) < Q \ \ P \ Q"

definition
 [simp]: "\ \ False"

definition
 [simp]: "\ \ True"

instance proof
qed auto

end

lemma le_boolI: "(P \ Q) \ P \ Q"
 by simp

lemma le_boolI': "P \ Q \ P \ Q"
 by simp

lemma le_boolE: "P \ Q \ P \ (Q \ R) \ R"
 by simp

lemma le_boolD: "P \ Q \ P \ Q"
 by simp

lemma bot_boolE: "\ \ P"
 by simp

lemma top_boolI: \<top>
 by simp

lemma [code]:
 "False \ b \ True"
 "True \ b \ b"
 "False Order on \<^typ>\<open>_ \<Rightarrow> _\<close>\<close>

instantiation "fun" :: (type, ord) ord
begin

definition
 le_fun_def: "f \ g \ (\x. f x \ g x)"

definition
 "(f::'a \ 'b) < g \ f \ g \ \ (g \ f)"

instance ..

end

instance "fun" :: (type, preorder) preorder proof
qed (auto simp add: le_fun_def less_fun_def
 intro: order_trans antisym)

instance "fun" :: (type, order) order proof
qed (auto simp add: le_fun_def intro: antisym)

instantiation "fun" :: (type, bot) bot
begin

definition
 "\ = (\x. \)"

instance ..

end

instantiation "fun" :: (type, order_bot) order_bot
begin

lemma bot_apply [simp, code]:
 "\ x = \"
 by (simp add: bot_fun_def)

instance proof
qed (simp add: le_fun_def)

end

instantiation "fun" :: (type, top) top
begin

definition
 [no_atp]: "\ = (\x. \)"

instance ..

end

instantiation "fun" :: (type, order_top) order_top
begin

lemma top_apply [simp, code]:
 "\ x = \"
 by (simp add: top_fun_def)

instance proof
qed (simp add: le_fun_def)

end

lemma le_funI: "(\x. f x \ g x) \ f \ g"
 unfolding le_fun_def by simp

lemma le_funE: "f \ g \ (f x \ g x \ P) \ P"
 unfolding le_fun_def by simp

lemma le_funD: "f \ g \ f x \ g x"
 by (rule le_funE)

lemma mono_compose: "mono Q \ mono (\i x. Q i (f x))"
 unfolding mono_def le_fun_def by auto

subsection \<open>Order on unary and binary predicates\<close>

lemma predicate1I:
 assumes PQ: "\x. P x \ Q x"
 shows "P \ Q"
 apply (rule le_funI)
 apply (rule le_boolI)
 apply (rule PQ)
 apply assumption
 done

lemma predicate1D:
 "P \ Q \ P x \ Q x"
 apply (erule le_funE)
 apply (erule le_boolE)
 apply assumption+
 done

lemma rev_predicate1D:
 "P x \ P \ Q \ Q x"
 by (rule predicate1D)

lemma predicate2I:
 assumes PQ: "\x y. P x y \ Q x y"
 shows "P \ Q"
 apply (rule le_funI)+
 apply (rule le_boolI)
 apply (rule PQ)
 apply assumption
 done

lemma predicate2D:
 "P \ Q \ P x y \ Q x y"
 apply (erule le_funE)+
 apply (erule le_boolE)
 apply assumption+
 done

lemma rev_predicate2D:
 "P x y \ P \ Q \ Q x y"
 by (rule predicate2D)

lemma bot1E [no_atp]: "\ x \ P"
 by (simp add: bot_fun_def)

lemma bot2E: "\ x y \ P"
 by (simp add: bot_fun_def)

lemma top1I: "\ x"
 by (simp add: top_fun_def)

lemma top2I: "\ x y"
 by (simp add: top_fun_def)

subsection \<open>Name duplicates\<close>

lemmas order_eq_refl = preorder_class.eq_refl
lemmas order_less_irrefl = preorder_class.less_irrefl
lemmas order_less_imp_le = preorder_class.less_imp_le
lemmas order_less_not_sym = preorder_class.less_not_sym
lemmas order_less_asym = preorder_class.less_asym
lemmas order_less_trans = preorder_class.less_trans
lemmas order_le_less_trans = preorder_class.le_less_trans
lemmas order_less_le_trans = preorder_class.less_le_trans
lemmas order_less_imp_not_less = preorder_class.less_imp_not_less
lemmas order_less_imp_triv = preorder_class.less_imp_triv
lemmas order_less_asym' = preorder_class.less_asym'

lemmas order_less_le = order_class.less_le
lemmas order_le_less = order_class.le_less
lemmas order_le_imp_less_or_eq = order_class.le_imp_less_or_eq
lemmas order_less_imp_not_eq = order_class.less_imp_not_eq
lemmas order_less_imp_not_eq2 = order_class.less_imp_not_eq2
lemmas order_neq_le_trans = order_class.neq_le_trans
lemmas order_le_neq_trans = order_class.le_neq_trans
lemmas order_antisym = order_class.antisym
lemmas order_eq_iff = order_class.eq_iff
lemmas order_antisym_conv = order_class.antisym_conv

lemmas linorder_linear = linorder_class.linear
lemmas linorder_less_linear = linorder_class.less_linear
lemmas linorder_le_less_linear = linorder_class.le_less_linear
lemmas linorder_le_cases = linorder_class.le_cases
lemmas linorder_not_less = linorder_class.not_less
lemmas linorder_not_le = linorder_class.not_le
lemmas linorder_neq_iff = linorder_class.neq_iff
lemmas linorder_neqE = linorder_class.neqE

end

¤ Dauer der Verarbeitung: 0.76 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.