# HG changeset patch
# User haftmann
# Date 1163011570 -3600
# Node ID 3fd22b0939ffdf898ae87886a69143a4aa4222f2
# Parent  f91699b807c32b6dc917f41476ebabdc8b10849b
abstract ordering theories

diff -r f91699b807c3 -r 3fd22b0939ff src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Wed Nov 08 13:51:03 2006 +0100
+++ b/src/HOL/Orderings.thy	Wed Nov 08 19:46:10 2006 +0100
@@ -75,7 +75,18 @@
   assumes refl [iff]: "x \<sqsubseteq> x"
   and trans: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z"
   and antisym: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> x \<Longrightarrow> x = y"
-  and less_le: "(x \<sqsubset> y) = (x \<sqsubseteq> y \<and> x \<noteq> y)"
+  and less_le: "x \<sqsubset> y \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<noteq> y"
+begin
+
+abbreviation (input)
+  greater_eq (infixl "\<sqsupseteq>" 50)
+  "x \<sqsupseteq> y \<equiv> y \<sqsubseteq> x"
+
+abbreviation (input)
+  greater (infixl "\<sqsupset>" 50)
+  "x \<sqsupset> y \<equiv> y \<sqsubset> x"
+
+end
 
 axclass order < ord
   order_refl [iff]: "x <= x"
@@ -89,90 +100,86 @@
 apply(rule order_refl, erule (1) order_trans, erule (1) order_antisym, rule order_less_le)
 done
 
+context partial_order
+begin
+
 text {* Reflexivity. *}
 
-lemma order_eq_refl: "(x \<Colon> 'a\<Colon>order) = y \<Longrightarrow> x \<le> y"
+lemma eq_refl: "x = y \<Longrightarrow> x \<sqsubseteq> y"
     -- {* This form is useful with the classical reasoner. *}
-  apply (erule ssubst)
-  apply (rule order_refl)
-  done
+  by (erule ssubst) (rule refl)
 
-lemma order_less_irrefl [iff]: "~ x < (x::'a::order)"
-  by (simp add: order_less_le)
+lemma less_irrefl [iff]: "\<not> x \<sqsubset> x"
+  by (simp add: less_le)
 
-lemma order_le_less: "((x::'a::order) <= y) = (x < y | x = y)"
+lemma le_less: "x \<sqsubseteq> y \<longleftrightarrow> x \<sqsubset> y \<or> x = y"
     -- {* NOT suitable for iff, since it can cause PROOF FAILED. *}
-  apply (simp add: order_less_le, blast)
-  done
+  by (simp add: less_le) blast
 
-lemmas order_le_imp_less_or_eq = order_le_less [THEN iffD1, standard]
+lemma le_imp_less_or_eq: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubset> y \<or> x = y"
+  unfolding less_le by blast
 
-lemma order_less_imp_le: "!!x::'a::order. x < y ==> x <= y"
-  by (simp add: order_less_le)
+lemma less_imp_le: "x \<sqsubset> y \<Longrightarrow> x \<sqsubseteq> y"
+  unfolding less_le by blast
+
 
 text {* Asymmetry. *}
 
-lemma order_less_not_sym: "(x::'a::order) < y ==> ~ (y < x)"
-  by (simp add: order_less_le order_antisym)
+lemma less_not_sym: "x \<sqsubset> y \<Longrightarrow> \<not> (y \<sqsubset> x)"
+  by (simp add: less_le antisym)
 
-lemma order_less_asym: "x < (y::'a::order) ==> (~P ==> y < x) ==> P"
-  apply (drule order_less_not_sym)
-  apply (erule contrapos_np, simp)
-  done
+lemma less_asym: "x \<sqsubset> y \<Longrightarrow> (\<not> P \<Longrightarrow> y \<sqsubset> x) \<Longrightarrow> P"
+  by (drule less_not_sym, erule contrapos_np) simp
 
-lemma order_eq_iff: "!!x::'a::order. (x = y) = (x \<le> y & y \<le> x)"
-by (blast intro: order_antisym)
+lemma eq_iff: "x = y \<longleftrightarrow> x \<sqsubseteq> y \<and> y \<sqsubseteq> x"
+  by (blast intro: antisym)
 
-lemma order_antisym_conv: "(y::'a::order) <= x ==> (x <= y) = (x = y)"
-by(blast intro:order_antisym)
+lemma antisym_conv: "y \<sqsubseteq> x \<Longrightarrow> x \<sqsubseteq> y \<longleftrightarrow> x = y"
+  by (blast intro: antisym)
 
-lemma less_imp_neq: "[| (x::'a::order) < y |] ==> x ~= y"
-  by (erule contrapos_pn, erule subst, rule order_less_irrefl)
+lemma less_imp_neq: "x \<sqsubset> y \<Longrightarrow> x \<noteq> y"
+  by (erule contrapos_pn, erule subst, rule less_irrefl)
+
 
 text {* Transitivity. *}
 
-lemma order_less_trans: "!!x::'a::order. [| x < y; y < z |] ==> x < z"
-  apply (simp add: order_less_le)
-  apply (blast intro: order_trans order_antisym)
-  done
+lemma less_trans: "\<lbrakk> x \<sqsubset> y; y \<sqsubset> z \<rbrakk> \<Longrightarrow> x \<sqsubset> z"
+  by (simp add: less_le) (blast intro: trans antisym)
 
-lemma order_le_less_trans: "!!x::'a::order. [| x <= y; y < z |] ==> x < z"
-  apply (simp add: order_less_le)
-  apply (blast intro: order_trans order_antisym)
-  done
+lemma le_less_trans: "\<lbrakk> x \<sqsubseteq> y; y \<sqsubset> z \<rbrakk> \<Longrightarrow> x \<sqsubset> z"
+  by (simp add: less_le) (blast intro: trans antisym)
 
-lemma order_less_le_trans: "!!x::'a::order. [| x < y; y <= z |] ==> x < z"
-  apply (simp add: order_less_le)
-  apply (blast intro: order_trans order_antisym)
-  done
+lemma less_le_trans: "\<lbrakk> x \<sqsubset> y; y \<sqsubseteq> z \<rbrakk> \<Longrightarrow> x \<sqsubset> z"
+  by (simp add: less_le) (blast intro: trans antisym)
 
-lemma eq_neq_eq_imp_neq: "[| x = a ; a ~= b; b = y |] ==> x ~= y"
-  by (erule subst, erule ssubst, assumption)
 
 text {* Useful for simplification, but too risky to include by default. *}
 
-lemma order_less_imp_not_less: "(x::'a::order) < y ==>  (~ y < x) = True"
-  by (blast elim: order_less_asym)
+lemma less_imp_not_less: "x \<sqsubset> y \<Longrightarrow> (\<not> y \<sqsubset> x) \<longleftrightarrow> True"
+  by (blast elim: less_asym)
 
-lemma order_less_imp_triv: "(x::'a::order) < y ==>  (y < x --> P) = True"
-  by (blast elim: order_less_asym)
+lemma less_imp_triv: "x \<sqsubset> y \<Longrightarrow> (y \<sqsubset> x \<longrightarrow> P) \<longleftrightarrow> True"
+  by (blast elim: less_asym)
 
-lemma order_less_imp_not_eq: "(x::'a::order) < y ==>  (x = y) = False"
+lemma less_imp_not_eq: "x \<sqsubset> y \<Longrightarrow> (x = y) \<longleftrightarrow> False"
   by auto
 
-lemma order_less_imp_not_eq2: "(x::'a::order) < y ==>  (y = x) = False"
+lemma less_imp_not_eq2: "x \<sqsubset> y \<Longrightarrow> (y = x) \<longleftrightarrow> False"
   by auto
 
+
 text {* Transitivity rules for calculational reasoning *}
 
-lemma order_neq_le_trans: "a ~= b ==> (a::'a::order) <= b ==> a < b"
-  by (simp add: order_less_le)
+lemma neq_le_trans: "\<lbrakk> a \<noteq> b; a \<sqsubseteq> b \<rbrakk> \<Longrightarrow> a \<sqsubset> b"
+  by (simp add: less_le)
 
-lemma order_le_neq_trans: "(a::'a::order) <= b ==> a ~= b ==> a < b"
-  by (simp add: order_less_le)
+lemma le_neq_trans: "\<lbrakk> a \<sqsubseteq> b; a \<noteq> b \<rbrakk> \<Longrightarrow> a \<sqsubset> b"
+  by (simp add: less_le)
 
-lemma order_less_asym': "(a::'a::order) < b ==> b < a ==> P"
-  by (rule order_less_asym)
+lemma less_asym': "\<lbrakk> a \<sqsubset> b; b \<sqsubset> a \<rbrakk> \<Longrightarrow> P"
+  by (rule less_asym)
+
+end
 
 
 subsection {* Linear (total) orderings *}
@@ -187,59 +194,98 @@
   linear_order ["op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool" "op < \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool"]
   by unfold_locales (rule linorder_linear)
 
-lemma linorder_less_linear: "!!x::'a::linorder. x<y | x=y | y<x"
-  apply (simp add: order_less_le)
-  apply (insert linorder_linear, blast)
+context linear_order
+begin
+
+lemma trichotomy: "x \<sqsubset> y \<or> x = y \<or> y \<sqsubset> x"
+  unfolding less_le using less_le linear by blast 
+
+lemma le_less_linear: "x \<sqsubseteq> y \<or> y \<sqsubset> x"
+  by (simp add: le_less trichotomy)
+
+lemma le_cases [case_names le ge]:
+  "\<lbrakk> x \<sqsubseteq> y \<Longrightarrow> P; y \<sqsubseteq> x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
+  using linear by blast
+
+lemma cases [case_names less equal greater]:
+    "\<lbrakk> x \<sqsubset> y \<Longrightarrow> P; x = y \<Longrightarrow> P; y \<sqsubset> x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
+  using trichotomy by blast
+
+lemma not_less: "\<not> x \<sqsubset> y \<longleftrightarrow> y \<sqsubseteq> x"
+  apply (simp add: less_le)
+  using linear apply (blast intro: antisym)
   done
 
-lemma linorder_le_less_linear: "!!x::'a::linorder. x\<le>y | y<x"
-  by (simp add: order_le_less linorder_less_linear)
-
-lemma linorder_le_cases [case_names le ge]:
-    "((x::'a::linorder) \<le> y ==> P) ==> (y \<le> x ==> P) ==> P"
-  by (insert linorder_linear, blast)
-
-lemma linorder_cases [case_names less equal greater]:
-    "((x::'a::linorder) < y ==> P) ==> (x = y ==> P) ==> (y < x ==> P) ==> P"
-  by (insert linorder_less_linear, blast)
-
-lemma linorder_not_less: "!!x::'a::linorder. (~ x < y) = (y <= x)"
-  apply (simp add: order_less_le)
-  apply (insert linorder_linear)
-  apply (blast intro: order_antisym)
+lemma not_le: "\<not> x \<sqsubseteq> y \<longleftrightarrow> y \<sqsubset> x"
+  apply (simp add: less_le)
+  using linear apply (blast intro: antisym)
   done
 
-lemma linorder_not_le: "!!x::'a::linorder. (~ x <= y) = (y < x)"
-  apply (simp add: order_less_le)
-  apply (insert linorder_linear)
-  apply (blast intro: order_antisym)
-  done
+lemma neq_iff: "x \<noteq> y \<longleftrightarrow> x \<sqsubset> y \<or> y \<sqsubset> x"
+  by (cut_tac x = x and y = y in trichotomy, auto)
 
-lemma linorder_neq_iff: "!!x::'a::linorder. (x ~= y) = (x<y | y<x)"
-by (cut_tac x = x and y = y in linorder_less_linear, auto)
+lemma neqE: "\<lbrakk> x \<noteq> y; x \<sqsubset> y \<Longrightarrow> R; y \<sqsubset> x \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
+  by (simp add: neq_iff) blast
 
-lemma linorder_neqE: "x ~= (y::'a::linorder) ==> (x < y ==> R) ==> (y < x ==> R) ==> R"
-by (simp add: linorder_neq_iff, blast)
-
-lemma linorder_antisym_conv1: "~ (x::'a::linorder) < y ==> (x <= y) = (x = y)"
-by(blast intro:order_antisym dest:linorder_not_less[THEN iffD1])
+lemma antisym_conv1: "\<not> x \<sqsubset> y \<Longrightarrow> x \<sqsubseteq> y \<longleftrightarrow> x = y"
+  by (blast intro: antisym dest: not_less [THEN iffD1])
 
-lemma linorder_antisym_conv2: "(x::'a::linorder) <= y ==> (~ x < y) = (x = y)"
-by(blast intro:order_antisym dest:linorder_not_less[THEN iffD1])
+lemma antisym_conv2: "x \<sqsubseteq> y \<Longrightarrow> \<not> x \<sqsubset> y \<longleftrightarrow> x = y"
+  by (blast intro: antisym dest: not_less [THEN iffD1])
 
-lemma linorder_antisym_conv3: "~ (y::'a::linorder) < x ==> (~ x < y) = (x = y)"
-by(blast intro:order_antisym dest:linorder_not_less[THEN iffD1])
+lemma antisym_conv3: "\<not> y \<sqsubset> x \<Longrightarrow> \<not> x \<sqsubset> y \<longleftrightarrow> x = y"
+  by (blast intro: antisym dest: not_less [THEN iffD1])
 
 text{*Replacing the old Nat.leI*}
-lemma leI: "~ x < y ==> y <= (x::'a::linorder)"
-  by (simp only: linorder_not_less)
+lemma leI: "\<not> x \<sqsubset> y \<Longrightarrow> y \<sqsubseteq> x"
+  unfolding not_less .
 
-lemma leD: "y <= (x::'a::linorder) ==> ~ x < y"
-  by (simp only: linorder_not_less)
+lemma leD: "y \<sqsubseteq> x \<Longrightarrow> \<not> x \<sqsubset> y"
+  unfolding not_less .
 
 (*FIXME inappropriate name (or delete altogether)*)
-lemma not_leE: "~ y <= (x::'a::linorder) ==> x < y"
-  by (simp only: linorder_not_le)
+lemma not_leE: "\<not> y \<sqsubseteq> x \<Longrightarrow> x \<sqsubset> y"
+  unfolding not_le .
+
+end
+
+
+subsection {* Name duplicates *}
+
+lemmas order_eq_refl [where 'b = "?'a::order"] = order.eq_refl
+lemmas order_less_irrefl [where 'b = "?'a::order"] = order.less_irrefl
+lemmas order_le_less [where 'b = "?'a::order"] = order.le_less
+lemmas order_le_imp_less_or_eq [where 'b = "?'a::order"] = order.le_imp_less_or_eq
+lemmas order_less_imp_le [where 'b = "?'a::order"] = order.less_imp_le
+lemmas order_less_not_sym [where 'b = "?'a::order"] = order.less_not_sym
+lemmas order_less_asym [where 'b = "?'a::order"] = order.less_asym
+lemmas order_eq_iff [where 'b = "?'a::order"] = order.eq_iff
+lemmas order_antisym_conv [where 'b = "?'a::order"] = order.antisym_conv
+lemmas less_imp_neq [where 'b = "?'a::order"] = order.less_imp_neq
+lemmas order_less_trans [where 'b = "?'a::order"] = order.less_trans
+lemmas order_le_less_trans [where 'b = "?'a::order"] = order.le_less_trans
+lemmas order_less_le_trans [where 'b = "?'a::order"] = order.less_le_trans
+lemmas order_less_imp_not_less [where 'b = "?'a::order"] = order.less_imp_not_less
+lemmas order_less_imp_triv [where 'b = "?'a::order"] = order.less_imp_triv
+lemmas order_less_imp_not_eq [where 'b = "?'a::order"] = order.less_imp_not_eq
+lemmas order_less_imp_not_eq2 [where 'b = "?'a::order"] = order.less_imp_not_eq2
+lemmas order_neq_le_trans [where 'b = "?'a::order"] = order.neq_le_trans
+lemmas order_le_neq_trans [where 'b = "?'a::order"] = order.le_neq_trans
+lemmas order_less_asym' [where 'b = "?'a::order"] = order.less_asym'
+lemmas linorder_less_linear [where 'b = "?'a::linorder"] = linorder.trichotomy
+lemmas linorder_le_less_linear [where 'b = "?'a::linorder"] = linorder.le_less_linear
+lemmas linorder_le_cases [where 'b = "?'a::linorder"] = linorder.le_cases
+lemmas linorder_cases [where 'b = "?'a::linorder"] = linorder.cases
+lemmas linorder_not_less [where 'b = "?'a::linorder"] = linorder.not_less
+lemmas linorder_not_le [where 'b = "?'a::linorder"] = linorder.not_le
+lemmas linorder_neq_iff [where 'b = "?'a::linorder"] = linorder.neq_iff
+lemmas linorder_neqE [where 'b = "?'a::linorder"] = linorder.neqE
+lemmas linorder_antisym_conv1 [where 'b = "?'a::linorder"] = linorder.antisym_conv1
+lemmas linorder_antisym_conv2 [where 'b = "?'a::linorder"] = linorder.antisym_conv2
+lemmas linorder_antisym_conv3 [where 'b = "?'a::linorder"] = linorder.antisym_conv3
+lemmas leI [where 'b = "?'a::linorder"] = linorder.leI
+lemmas leD [where 'b = "?'a::linorder"] = linorder.leD
+lemmas not_leE [where 'b = "?'a::linorder"] = linorder.not_leE
 
 
 subsection {* Reasoning tools setup *}
@@ -248,75 +294,78 @@
 local
 
 fun decomp_gen sort thy (Trueprop $ t) =
-  let fun of_sort t = let val T = type_of t in
+  let
+    fun of_sort t =
+      let
+        val T = type_of t
+      in
         (* exclude numeric types: linear arithmetic subsumes transitivity *)
-        T <> HOLogic.natT andalso T <> HOLogic.intT andalso
-        T <> HOLogic.realT andalso Sign.of_sort thy (T, sort) end
-  fun dec (Const ("Not", _) $ t) = (
-	  case dec t of
-	    NONE => NONE
-	  | SOME (t1, rel, t2) => SOME (t1, "~" ^ rel, t2))
-	| dec (Const ("op =",  _) $ t1 $ t2) =
-	    if of_sort t1
-	    then SOME (t1, "=", t2)
-	    else NONE
-	| dec (Const ("Orderings.less_eq",  _) $ t1 $ t2) =
-	    if of_sort t1
-	    then SOME (t1, "<=", t2)
-	    else NONE
-	| dec (Const ("Orderings.less",  _) $ t1 $ t2) =
-	    if of_sort t1
-	    then SOME (t1, "<", t2)
-	    else NONE
-	| dec _ = NONE
+        T <> HOLogic.natT andalso T <> HOLogic.intT
+          andalso T <> HOLogic.realT andalso Sign.of_sort thy (T, sort)
+      end;
+    fun dec (Const ("Not", _) $ t) = (case dec t
+          of NONE => NONE
+           | SOME (t1, rel, t2) => SOME (t1, "~" ^ rel, t2))
+      | dec (Const ("op =",  _) $ t1 $ t2) =
+          if of_sort t1
+          then SOME (t1, "=", t2)
+          else NONE
+      | dec (Const ("Orderings.less_eq",  _) $ t1 $ t2) =
+          if of_sort t1
+          then SOME (t1, "<=", t2)
+          else NONE
+      | dec (Const ("Orderings.less",  _) $ t1 $ t2) =
+          if of_sort t1
+          then SOME (t1, "<", t2)
+          else NONE
+      | dec _ = NONE;
   in dec t end;
 
 in
 
-structure Quasi_Tac = Quasi_Tac_Fun (
 (* The setting up of Quasi_Tac serves as a demo.  Since there is no
    class for quasi orders, the tactics Quasi_Tac.trans_tac and
    Quasi_Tac.quasi_tac are not of much use. *)
-  struct
-    val le_trans = thm "order_trans";
-    val le_refl = thm "order_refl";
-    val eqD1 = thm "order_eq_refl";
-    val eqD2 = thm "sym" RS thm "order_eq_refl";
-    val less_reflE = thm "order_less_irrefl" RS thm "notE";
-    val less_imp_le = thm "order_less_imp_le";
-    val le_neq_trans = thm "order_le_neq_trans";
-    val neq_le_trans = thm "order_neq_le_trans";
-    val less_imp_neq = thm "less_imp_neq";
-    val decomp_trans = decomp_gen ["Orderings.order"];
-    val decomp_quasi = decomp_gen ["Orderings.order"];
 
-  end);
+structure Quasi_Tac = Quasi_Tac_Fun (
+struct
+  val le_trans = thm "order_trans";
+  val le_refl = thm "order_refl";
+  val eqD1 = thm "order_eq_refl";
+  val eqD2 = thm "sym" RS thm "order_eq_refl";
+  val less_reflE = thm "order_less_irrefl" RS thm "notE";
+  val less_imp_le = thm "order_less_imp_le";
+  val le_neq_trans = thm "order_le_neq_trans";
+  val neq_le_trans = thm "order_neq_le_trans";
+  val less_imp_neq = thm "less_imp_neq";
+  val decomp_trans = decomp_gen ["Orderings.order"];
+  val decomp_quasi = decomp_gen ["Orderings.order"];
+end);
 
 structure Order_Tac = Order_Tac_Fun (
-  struct
-    val less_reflE = thm "order_less_irrefl" RS thm "notE";
-    val le_refl = thm "order_refl";
-    val less_imp_le = thm "order_less_imp_le";
-    val not_lessI = thm "linorder_not_less" RS thm "iffD2";
-    val not_leI = thm "linorder_not_le" RS thm "iffD2";
-    val not_lessD = thm "linorder_not_less" RS thm "iffD1";
-    val not_leD = thm "linorder_not_le" RS thm "iffD1";
-    val eqI = thm "order_antisym";
-    val eqD1 = thm "order_eq_refl";
-    val eqD2 = thm "sym" RS thm "order_eq_refl";
-    val less_trans = thm "order_less_trans";
-    val less_le_trans = thm "order_less_le_trans";
-    val le_less_trans = thm "order_le_less_trans";
-    val le_trans = thm "order_trans";
-    val le_neq_trans = thm "order_le_neq_trans";
-    val neq_le_trans = thm "order_neq_le_trans";
-    val less_imp_neq = thm "less_imp_neq";
-    val eq_neq_eq_imp_neq = thm "eq_neq_eq_imp_neq";
-    val not_sym = thm "not_sym";
-    val decomp_part = decomp_gen ["Orderings.order"];
-    val decomp_lin = decomp_gen ["Orderings.linorder"];
-
-  end);
+struct
+  val less_reflE = thm "order_less_irrefl" RS thm "notE";
+  val le_refl = thm "order_refl";
+  val less_imp_le = thm "order_less_imp_le";
+  val not_lessI = thm "linorder_not_less" RS thm "iffD2";
+  val not_leI = thm "linorder_not_le" RS thm "iffD2";
+  val not_lessD = thm "linorder_not_less" RS thm "iffD1";
+  val not_leD = thm "linorder_not_le" RS thm "iffD1";
+  val eqI = thm "order_antisym";
+  val eqD1 = thm "order_eq_refl";
+  val eqD2 = thm "sym" RS thm "order_eq_refl";
+  val less_trans = thm "order_less_trans";
+  val less_le_trans = thm "order_less_le_trans";
+  val le_less_trans = thm "order_le_less_trans";
+  val le_trans = thm "order_trans";
+  val le_neq_trans = thm "order_le_neq_trans";
+  val neq_le_trans = thm "order_neq_le_trans";
+  val less_imp_neq = thm "less_imp_neq";
+  val eq_neq_eq_imp_neq = thm "eq_neq_eq_imp_neq";
+  val not_sym = thm "not_sym";
+  val decomp_part = decomp_gen ["Orderings.order"];
+  val decomp_lin = decomp_gen ["Orderings.linorder"];
+end);
 
 end;
 *}
@@ -361,21 +410,25 @@
   end
   handle THM _ => NONE;
 
-val antisym_le = Simplifier.simproc (the_context())
-  "antisym le" ["(x::'a::order) <= y"] prove_antisym_le;
-val antisym_less = Simplifier.simproc (the_context())
-  "antisym less" ["~ (x::'a::linorder) < y"] prove_antisym_less;
+fun add_simprocs procs thy =
+  (Simplifier.change_simpset_of thy (fn ss => ss
+    addsimprocs (map (fn (name, raw_ts, proc) =>
+      Simplifier.simproc thy name raw_ts proc)) procs); thy);
+fun add_solver name tac thy =
+  (Simplifier.change_simpset_of thy (fn ss => ss addSolver
+    (mk_solver name (K tac))); thy);
 
 in
-  (fn thy => (Simplifier.change_simpset_of thy
-    (fn ss => ss
-       addsimprocs [antisym_le, antisym_less]
-       addSolver (mk_solver "Trans_linear" (fn _ => Order_Tac.linear_tac))
-       addSolver (mk_solver "Trans_partial" (fn _ => Order_Tac.partial_tac)))
-       (* 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). *); thy))
+  add_simprocs [
+       ("antisym le", ["(x::'a::order) <= y"], prove_antisym_le),
+       ("antisym less", ["~ (x::'a::linorder) < y"], prove_antisym_less)
+     ]
+  #> add_solver "Trans_linear" Order_Tac.linear_tac
+  #> add_solver "Trans_partial" Order_Tac.partial_tac
+  (* 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). *)
 end
 *}