# HG changeset patch
# User wenzelm
# Date 1397124025 -7200
# Node ID e050d42dc21db303080200216abb0d24584045ee
# Parent  af08160c5a4cfdb8202fb40872cfa665b6abef6b
modernized simproc_setup;

diff -r af08160c5a4c -r e050d42dc21d src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Thu Apr 10 11:24:58 2014 +0200
+++ b/src/HOL/Orderings.thy	Thu Apr 10 12:00:25 2014 +0200
@@ -541,64 +541,64 @@
 
 end
 
-
 setup {*
-let
-
-fun prp t thm = Thm.prop_of thm = t;  (* FIXME aconv!? *)
+  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).*)
+*}
 
-fun prove_antisym_le ctxt ((le as Const(_,T)) $ r $ s) =
-  let val prems = Simplifier.prems_of ctxt;
-      val less = Const (@{const_name less}, 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 linorder_class.antisym_conv1}))
-         end
-     | SOME thm => SOME(mk_meta_eq(thm RS @{thm order_class.antisym_conv}))
-  end
-  handle THM _ => NONE;
+ML {*
+local
+  fun prp t thm = Thm.prop_of thm = t;  (* FIXME proper aconv!? *)
+in
 
-fun prove_antisym_less ctxt (NotC $ ((less as Const(_,T)) $ r $ s)) =
-  let val prems = Simplifier.prems_of ctxt;
-      val le = Const (@{const_name less_eq}, 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 linorder_class.antisym_conv2}))
-  end
-  handle THM _ => NONE;
+fun antisym_le_simproc ctxt ct =
+  (case term_of ct of
+    (le as Const (_, T)) $ r $ s =>
+     (let
+        val prems = Simplifier.prems_of ctxt;
+        val less = Const (@{const_name less}, 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 linorder_class.antisym_conv1})))
+             end
+         | SOME thm => SOME (mk_meta_eq (thm RS @{thm order_class.antisym_conv})))
+      end handle THM _ => NONE)
+  | _ => NONE);
 
-fun add_simprocs procs thy =
-  map_theory_simpset (fn ctxt => ctxt
-    addsimprocs (map (fn (name, raw_ts, proc) =>
-      Simplifier.simproc_global thy name raw_ts proc) procs)) thy;
-
-fun add_solver name tac =
-  map_theory_simpset (fn ctxt0 => ctxt0 addSolver
-    mk_solver name (fn ctxt => tac ctxt (Simplifier.prems_of ctxt)));
+fun antisym_less_simproc ctxt ct =
+  (case term_of ct of
+    NotC $ ((less as Const(_,T)) $ r $ s) =>
+     (let
+       val prems = Simplifier.prems_of ctxt;
+       val le = Const (@{const_name less_eq}, 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 linorder_class.antisym_conv2})))
+      end handle THM _ => NONE)
+  | _ => NONE);
 
-in
-  add_simprocs [
-       ("antisym le", ["(x::'a::order) <= y"], prove_antisym_le),
-       ("antisym less", ["~ (x::'a::linorder) < y"], prove_antisym_less)
-     ]
-  #> add_solver "Transitivity" Orders.order_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
+end;
 *}
 
+simproc_setup antisym_le ("(x::'a::order) \<le> y") = "K antisym_le_simproc"
+simproc_setup antisym_less ("\<not> (x::'a::linorder) < y") = "K antisym_less_simproc"
+
 
 subsection {* Bounded quantifiers *}