src/HOL/Orderings.thy

 
 
 subsection {* Reasoning tools setup *}
 
 ML {*
-
 signature ORDERS =
 sig
   val print_structures: Proof.context -> unit
-  val attrib_setup: theory -> theory
   val order_tac: Proof.context -> thm list -> int -> tactic
 end;
 
 structure Orders: ORDERS =
 struct
 
-(** Theory and context data **)
+(* context data *)
 
 fun struct_eq ((s1: string, ts1), (s2, ts2)) =
-  (s1 = s2) andalso eq_list (op aconv) (ts1, 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:

        Pretty.enclose "(" ")" (Pretty.breaks (map pretty_term ts))];
   in
     Pretty.writeln (Pretty.big_list "order structures:" (map pretty_struct structs))
   end;
 
-
-(** Method **)
-
-fun struct_tac ((s, [eq, le, less]), thms) ctxt prems =
+val _ =
+  Outer_Syntax.improper_command @{command_spec "print_orders"}
+    "print order structures available to transitivity reasoner"
+    (Scan.succeed (Toplevel.unknown_context o
+      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 Trueprop} $ 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 Not}, _) $ t) = (case rel t
-              of NONE => NONE
-               | SOME (t1, rel, t2) => SOME (t1, "~" ^ rel, t2))
-          | dec x = rel x;
-      in dec t end
-      | decomp thy _ = NONE;
+          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 Not}, _) $ 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 prems
-    | "linorder" => Order_Tac.linear_tac decomp thms ctxt prems
-    | _ => error ("Unknown kind of order `" ^ s ^ "' encountered in transitivity reasoner.")
+    (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 prems =
-  FIRST' (map (fn s => CHANGED o struct_tac s ctxt prems) (Data.get (Context.Proof ctxt)));
-
-
-(** Attribute **)
+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_thm 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));
 
-val attrib_setup =
-  Attrib.setup @{binding order}
-    (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) => add_struct_thm (n, ts) tag
-           | ((NONE, n), ts) => del_struct (n, ts)))
-    "theorems controlling transitivity reasoner";
-
-
-(** Diagnostic command **)
-
 val _ =
-  Outer_Syntax.improper_command @{command_spec "print_orders"}
-    "print order structures available to transitivity reasoner"
-    (Scan.succeed (Toplevel.unknown_context o
-      Toplevel.keep (print_structures o Toplevel.context_of)));
+  Theory.setup
+    (Attrib.setup @{binding order}
+      (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) => add_struct_thm (n, ts) tag
+             | ((NONE, n), ts) => del_struct (n, ts)))
+      "theorems controlling transitivity reasoner");
 
 end;
-
 *}
-
-setup Orders.attrib_setup
 
 method_setup order = {*
   Scan.succeed (fn ctxt => SIMPLE_METHOD' (Orders.order_tac ctxt []))
 *} "transitivity reasoner"