src/HOL/Orderings.thy
changeset 56508 af08160c5a4c
parent 56020 f92479477c52
child 56509 e050d42dc21d
     1.1 --- a/src/HOL/Orderings.thy	Thu Apr 10 11:06:45 2014 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Thu Apr 10 11:24:58 2014 +0200
     1.3 @@ -344,21 +344,19 @@
     1.4  subsection {* Reasoning tools setup *}
     1.5  
     1.6  ML {*
     1.7 -
     1.8  signature ORDERS =
     1.9  sig
    1.10    val print_structures: Proof.context -> unit
    1.11 -  val attrib_setup: theory -> theory
    1.12    val order_tac: Proof.context -> thm list -> int -> tactic
    1.13  end;
    1.14  
    1.15  structure Orders: ORDERS =
    1.16  struct
    1.17  
    1.18 -(** Theory and context data **)
    1.19 +(* context data *)
    1.20  
    1.21  fun struct_eq ((s1: string, ts1), (s2, ts2)) =
    1.22 -  (s1 = s2) andalso eq_list (op aconv) (ts1, ts2);
    1.23 +  s1 = s2 andalso eq_list (op aconv) (ts1, ts2);
    1.24  
    1.25  structure Data = Generic_Data
    1.26  (
    1.27 @@ -386,44 +384,52 @@
    1.28      Pretty.writeln (Pretty.big_list "order structures:" (map pretty_struct structs))
    1.29    end;
    1.30  
    1.31 -
    1.32 -(** Method **)
    1.33 +val _ =
    1.34 +  Outer_Syntax.improper_command @{command_spec "print_orders"}
    1.35 +    "print order structures available to transitivity reasoner"
    1.36 +    (Scan.succeed (Toplevel.unknown_context o
    1.37 +      Toplevel.keep (print_structures o Toplevel.context_of)));
    1.38  
    1.39 -fun struct_tac ((s, [eq, le, less]), thms) ctxt prems =
    1.40 +
    1.41 +(* tactics *)
    1.42 +
    1.43 +fun struct_tac ((s, ops), thms) ctxt facts =
    1.44    let
    1.45 +    val [eq, le, less] = ops;
    1.46      fun decomp thy (@{const Trueprop} $ t) =
    1.47 -      let
    1.48 -        fun excluded t =
    1.49 -          (* exclude numeric types: linear arithmetic subsumes transitivity *)
    1.50 -          let val T = type_of t
    1.51 -          in
    1.52 -            T = HOLogic.natT orelse T = HOLogic.intT orelse T = HOLogic.realT
    1.53 -          end;
    1.54 -        fun rel (bin_op $ t1 $ t2) =
    1.55 -              if excluded t1 then NONE
    1.56 -              else if Pattern.matches thy (eq, bin_op) then SOME (t1, "=", t2)
    1.57 -              else if Pattern.matches thy (le, bin_op) then SOME (t1, "<=", t2)
    1.58 -              else if Pattern.matches thy (less, bin_op) then SOME (t1, "<", t2)
    1.59 -              else NONE
    1.60 -          | rel _ = NONE;
    1.61 -        fun dec (Const (@{const_name Not}, _) $ t) = (case rel t
    1.62 -              of NONE => NONE
    1.63 -               | SOME (t1, rel, t2) => SOME (t1, "~" ^ rel, t2))
    1.64 -          | dec x = rel x;
    1.65 -      in dec t end
    1.66 -      | decomp thy _ = NONE;
    1.67 +          let
    1.68 +            fun excluded t =
    1.69 +              (* exclude numeric types: linear arithmetic subsumes transitivity *)
    1.70 +              let val T = type_of t
    1.71 +              in
    1.72 +                T = HOLogic.natT orelse T = HOLogic.intT orelse T = HOLogic.realT
    1.73 +              end;
    1.74 +            fun rel (bin_op $ t1 $ t2) =
    1.75 +                  if excluded t1 then NONE
    1.76 +                  else if Pattern.matches thy (eq, bin_op) then SOME (t1, "=", t2)
    1.77 +                  else if Pattern.matches thy (le, bin_op) then SOME (t1, "<=", t2)
    1.78 +                  else if Pattern.matches thy (less, bin_op) then SOME (t1, "<", t2)
    1.79 +                  else NONE
    1.80 +              | rel _ = NONE;
    1.81 +            fun dec (Const (@{const_name Not}, _) $ t) =
    1.82 +                  (case rel t of NONE =>
    1.83 +                    NONE
    1.84 +                  | SOME (t1, rel, t2) => SOME (t1, "~" ^ rel, t2))
    1.85 +              | dec x = rel x;
    1.86 +          in dec t end
    1.87 +      | decomp _ _ = NONE;
    1.88    in
    1.89 -    case s of
    1.90 -      "order" => Order_Tac.partial_tac decomp thms ctxt prems
    1.91 -    | "linorder" => Order_Tac.linear_tac decomp thms ctxt prems
    1.92 -    | _ => error ("Unknown kind of order `" ^ s ^ "' encountered in transitivity reasoner.")
    1.93 +    (case s of
    1.94 +      "order" => Order_Tac.partial_tac decomp thms ctxt facts
    1.95 +    | "linorder" => Order_Tac.linear_tac decomp thms ctxt facts
    1.96 +    | _ => error ("Unknown order kind " ^ quote s ^ " encountered in transitivity reasoner"))
    1.97    end
    1.98  
    1.99 -fun order_tac ctxt prems =
   1.100 -  FIRST' (map (fn s => CHANGED o struct_tac s ctxt prems) (Data.get (Context.Proof ctxt)));
   1.101 +fun order_tac ctxt facts =
   1.102 +  FIRST' (map (fn s => CHANGED o struct_tac s ctxt facts) (Data.get (Context.Proof ctxt)));
   1.103  
   1.104  
   1.105 -(** Attribute **)
   1.106 +(* attributes *)
   1.107  
   1.108  fun add_struct_thm s tag =
   1.109    Thm.declaration_attribute
   1.110 @@ -432,30 +438,19 @@
   1.111    Thm.declaration_attribute
   1.112      (fn _ => Data.map (AList.delete struct_eq s));
   1.113  
   1.114 -val attrib_setup =
   1.115 -  Attrib.setup @{binding order}
   1.116 -    (Scan.lift ((Args.add -- Args.name >> (fn (_, s) => SOME s) || Args.del >> K NONE) --|
   1.117 -      Args.colon (* FIXME || Scan.succeed true *) ) -- Scan.lift Args.name --
   1.118 -      Scan.repeat Args.term
   1.119 -      >> (fn ((SOME tag, n), ts) => add_struct_thm (n, ts) tag
   1.120 -           | ((NONE, n), ts) => del_struct (n, ts)))
   1.121 -    "theorems controlling transitivity reasoner";
   1.122 -
   1.123 -
   1.124 -(** Diagnostic command **)
   1.125 -
   1.126  val _ =
   1.127 -  Outer_Syntax.improper_command @{command_spec "print_orders"}
   1.128 -    "print order structures available to transitivity reasoner"
   1.129 -    (Scan.succeed (Toplevel.unknown_context o
   1.130 -      Toplevel.keep (print_structures o Toplevel.context_of)));
   1.131 +  Theory.setup
   1.132 +    (Attrib.setup @{binding order}
   1.133 +      (Scan.lift ((Args.add -- Args.name >> (fn (_, s) => SOME s) || Args.del >> K NONE) --|
   1.134 +        Args.colon (* FIXME || Scan.succeed true *) ) -- Scan.lift Args.name --
   1.135 +        Scan.repeat Args.term
   1.136 +        >> (fn ((SOME tag, n), ts) => add_struct_thm (n, ts) tag
   1.137 +             | ((NONE, n), ts) => del_struct (n, ts)))
   1.138 +      "theorems controlling transitivity reasoner");
   1.139  
   1.140  end;
   1.141 -
   1.142  *}
   1.143  
   1.144 -setup Orders.attrib_setup
   1.145 -
   1.146  method_setup order = {*
   1.147    Scan.succeed (fn ctxt => SIMPLE_METHOD' (Orders.order_tac ctxt []))
   1.148  *} "transitivity reasoner"