modernized simproc_setup;
authorwenzelm
Thu Apr 10 12:00:25 2014 +0200 (2014-04-10)
changeset 56509e050d42dc21d
parent 56508 af08160c5a4c
child 56510 aec722524c33
modernized simproc_setup;
src/HOL/Orderings.thy
     1.1 --- a/src/HOL/Orderings.thy	Thu Apr 10 11:24:58 2014 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Thu Apr 10 12:00:25 2014 +0200
     1.3 @@ -541,64 +541,64 @@
     1.4  
     1.5  end
     1.6  
     1.7 -
     1.8  setup {*
     1.9 -let
    1.10 -
    1.11 -fun prp t thm = Thm.prop_of thm = t;  (* FIXME aconv!? *)
    1.12 +  map_theory_simpset (fn ctxt0 => ctxt0 addSolver
    1.13 +    mk_solver "Transitivity" (fn ctxt => Orders.order_tac ctxt (Simplifier.prems_of ctxt)))
    1.14 +  (*Adding the transitivity reasoners also as safe solvers showed a slight
    1.15 +    speed up, but the reasoning strength appears to be not higher (at least
    1.16 +    no breaking of additional proofs in the entire HOL distribution, as
    1.17 +    of 5 March 2004, was observed).*)
    1.18 +*}
    1.19  
    1.20 -fun prove_antisym_le ctxt ((le as Const(_,T)) $ r $ s) =
    1.21 -  let val prems = Simplifier.prems_of ctxt;
    1.22 -      val less = Const (@{const_name less}, T);
    1.23 -      val t = HOLogic.mk_Trueprop(le $ s $ r);
    1.24 -  in case find_first (prp t) prems of
    1.25 -       NONE =>
    1.26 -         let val t = HOLogic.mk_Trueprop(HOLogic.Not $ (less $ r $ s))
    1.27 -         in case find_first (prp t) prems of
    1.28 -              NONE => NONE
    1.29 -            | SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_class.antisym_conv1}))
    1.30 -         end
    1.31 -     | SOME thm => SOME(mk_meta_eq(thm RS @{thm order_class.antisym_conv}))
    1.32 -  end
    1.33 -  handle THM _ => NONE;
    1.34 +ML {*
    1.35 +local
    1.36 +  fun prp t thm = Thm.prop_of thm = t;  (* FIXME proper aconv!? *)
    1.37 +in
    1.38  
    1.39 -fun prove_antisym_less ctxt (NotC $ ((less as Const(_,T)) $ r $ s)) =
    1.40 -  let val prems = Simplifier.prems_of ctxt;
    1.41 -      val le = Const (@{const_name less_eq}, T);
    1.42 -      val t = HOLogic.mk_Trueprop(le $ r $ s);
    1.43 -  in case find_first (prp t) prems of
    1.44 -       NONE =>
    1.45 -         let val t = HOLogic.mk_Trueprop(NotC $ (less $ s $ r))
    1.46 -         in case find_first (prp t) prems of
    1.47 -              NONE => NONE
    1.48 -            | SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_class.antisym_conv3}))
    1.49 -         end
    1.50 -     | SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_class.antisym_conv2}))
    1.51 -  end
    1.52 -  handle THM _ => NONE;
    1.53 +fun antisym_le_simproc ctxt ct =
    1.54 +  (case term_of ct of
    1.55 +    (le as Const (_, T)) $ r $ s =>
    1.56 +     (let
    1.57 +        val prems = Simplifier.prems_of ctxt;
    1.58 +        val less = Const (@{const_name less}, T);
    1.59 +        val t = HOLogic.mk_Trueprop(le $ s $ r);
    1.60 +      in
    1.61 +        (case find_first (prp t) prems of
    1.62 +          NONE =>
    1.63 +            let val t = HOLogic.mk_Trueprop(HOLogic.Not $ (less $ r $ s)) in
    1.64 +              (case find_first (prp t) prems of
    1.65 +                NONE => NONE
    1.66 +              | SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_class.antisym_conv1})))
    1.67 +             end
    1.68 +         | SOME thm => SOME (mk_meta_eq (thm RS @{thm order_class.antisym_conv})))
    1.69 +      end handle THM _ => NONE)
    1.70 +  | _ => NONE);
    1.71  
    1.72 -fun add_simprocs procs thy =
    1.73 -  map_theory_simpset (fn ctxt => ctxt
    1.74 -    addsimprocs (map (fn (name, raw_ts, proc) =>
    1.75 -      Simplifier.simproc_global thy name raw_ts proc) procs)) thy;
    1.76 -
    1.77 -fun add_solver name tac =
    1.78 -  map_theory_simpset (fn ctxt0 => ctxt0 addSolver
    1.79 -    mk_solver name (fn ctxt => tac ctxt (Simplifier.prems_of ctxt)));
    1.80 +fun antisym_less_simproc ctxt ct =
    1.81 +  (case term_of ct of
    1.82 +    NotC $ ((less as Const(_,T)) $ r $ s) =>
    1.83 +     (let
    1.84 +       val prems = Simplifier.prems_of ctxt;
    1.85 +       val le = Const (@{const_name less_eq}, T);
    1.86 +       val t = HOLogic.mk_Trueprop(le $ r $ s);
    1.87 +      in
    1.88 +        (case find_first (prp t) prems of
    1.89 +          NONE =>
    1.90 +            let val t = HOLogic.mk_Trueprop (NotC $ (less $ s $ r)) in
    1.91 +              (case find_first (prp t) prems of
    1.92 +                NONE => NONE
    1.93 +              | SOME thm => SOME (mk_meta_eq(thm RS @{thm linorder_class.antisym_conv3})))
    1.94 +            end
    1.95 +        | SOME thm => SOME (mk_meta_eq (thm RS @{thm linorder_class.antisym_conv2})))
    1.96 +      end handle THM _ => NONE)
    1.97 +  | _ => NONE);
    1.98  
    1.99 -in
   1.100 -  add_simprocs [
   1.101 -       ("antisym le", ["(x::'a::order) <= y"], prove_antisym_le),
   1.102 -       ("antisym less", ["~ (x::'a::linorder) < y"], prove_antisym_less)
   1.103 -     ]
   1.104 -  #> add_solver "Transitivity" Orders.order_tac
   1.105 -  (* Adding the transitivity reasoners also as safe solvers showed a slight
   1.106 -     speed up, but the reasoning strength appears to be not higher (at least
   1.107 -     no breaking of additional proofs in the entire HOL distribution, as
   1.108 -     of 5 March 2004, was observed). *)
   1.109 -end
   1.110 +end;
   1.111  *}
   1.112  
   1.113 +simproc_setup antisym_le ("(x::'a::order) \<le> y") = "K antisym_le_simproc"
   1.114 +simproc_setup antisym_less ("\<not> (x::'a::linorder) < y") = "K antisym_less_simproc"
   1.115 +
   1.116  
   1.117  subsection {* Bounded quantifiers *}
   1.118