--- a/src/HOL/Orderings.thy Thu Apr 10 11:06:45 2014 +0200
+++ b/src/HOL/Orderings.thy Thu Apr 10 11:24:58 2014 +0200
@@ -344,21 +344,19 @@
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
(
@@ -386,44 +384,52 @@
Pretty.writeln (Pretty.big_list "order structures:" (map pretty_struct structs))
end;
-
-(** Method **)
+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)));
-fun struct_tac ((s, [eq, le, less]), thms) ctxt prems =
+
+(* 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)));
+fun order_tac ctxt facts =
+ FIRST' (map (fn s => CHANGED o struct_tac s ctxt facts) (Data.get (Context.Proof ctxt)));
-(** Attribute **)
+(* attributes *)
fun add_struct_thm s tag =
Thm.declaration_attribute
@@ -432,30 +438,19 @@
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"