# HG changeset patch
# User wenzelm
# Date 1394221587 -3600
# Node ID 52c22561996dac4bd60bb6a6216431b4b5a6e072
# Parent  61b0021ed674e42df6817f7eac9dbc736e29bd12
misc tuning;

diff -r 61b0021ed674 -r 52c22561996d src/HOL/Decision_Procs/cooper_tac.ML
--- a/src/HOL/Decision_Procs/cooper_tac.ML	Fri Mar 07 20:32:48 2014 +0100
+++ b/src/HOL/Decision_Procs/cooper_tac.ML	Fri Mar 07 20:46:27 2014 +0100
@@ -12,22 +12,6 @@
 
 val cooper_ss = simpset_of @{context};
 
-val nT = HOLogic.natT;
-val comp_arith = @{thms simp_thms}
-
-val zdvd_int = @{thm zdvd_int};
-val zdiff_int_split = @{thm zdiff_int_split};
-val split_zdiv = @{thm split_zdiv};
-val split_zmod = @{thm split_zmod};
-val mod_div_equality' = @{thm mod_div_equality'};
-val split_div' = @{thm split_div'};
-val Suc_eq_plus1 = @{thm Suc_eq_plus1};
-val mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
-val mod_add_right_eq = @{thm mod_add_right_eq} RS sym;
-val mod_add_eq = @{thm mod_add_eq} RS sym;
-val nat_div_add_eq = @{thm div_add1_eq} RS sym;
-val int_div_add_eq = @{thm zdiv_zadd1_eq} RS sym;
-
 fun prepare_for_linz q fm =
   let
     val ps = Logic.strip_params fm
@@ -42,53 +26,51 @@
     val np = length ps
     val (fm',np) = List.foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
       (List.foldr HOLogic.mk_imp c rhs, np) ps
-    val (vs, _) = List.partition (fn t => q orelse (type_of t) = nT)
+    val (vs, _) = List.partition (fn t => q orelse (type_of t) = @{typ nat})
       (Misc_Legacy.term_frees fm' @ Misc_Legacy.term_vars fm');
     val fm2 = List.foldr mk_all2 fm' vs
   in (fm2, np + length vs, length rhs) end;
 
 (*Object quantifier to meta --*)
-fun spec_step n th = if (n=0) then th else (spec_step (n-1) th) RS spec ;
+fun spec_step n th = if n = 0 then th else (spec_step (n - 1) th) RS spec;
 
 (* object implication to meta---*)
-fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp;
+fun mp_step n th = if n = 0 then th else (mp_step (n - 1) th) RS mp;
 
 
 fun linz_tac ctxt q = Object_Logic.atomize_prems_tac ctxt THEN' SUBGOAL (fn (g, i) =>
   let
-    val thy = Proof_Context.theory_of ctxt
+    val thy = Proof_Context.theory_of ctxt;
     (* Transform the term*)
-    val (t,np,nh) = prepare_for_linz q g
+    val (t, np, nh) = prepare_for_linz q g;
     (* Some simpsets for dealing with mod div abs and nat*)
     val mod_div_simpset =
       put_simpset HOL_basic_ss ctxt
-      addsimps [refl,mod_add_eq, mod_add_left_eq,
-          mod_add_right_eq,
-          nat_div_add_eq, int_div_add_eq,
-          @{thm mod_self},
-          @{thm div_by_0}, @{thm mod_by_0}, @{thm div_0}, @{thm mod_0},
-          @{thm div_by_1}, @{thm mod_by_1}, @{thm div_1}, @{thm mod_1},
-          Suc_eq_plus1]
+      addsimps @{thms refl mod_add_eq [symmetric] mod_add_left_eq [symmetric]
+          mod_add_right_eq [symmetric]
+          div_add1_eq [symmetric] zdiv_zadd1_eq [symmetric]
+          mod_self
+          div_by_0 mod_by_0 div_0 mod_0
+          div_by_1 mod_by_1 div_1 mod_1
+          Suc_eq_plus1}
       addsimps @{thms add_ac}
       addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}]
     val simpset0 =
       put_simpset HOL_basic_ss ctxt
-      addsimps [mod_div_equality', Suc_eq_plus1]
-      addsimps comp_arith
-      |> fold Splitter.add_split
-          [split_zdiv, split_zmod, split_div', @{thm "split_min"}, @{thm "split_max"}]
+      addsimps @{thms mod_div_equality' Suc_eq_plus1 simp_thms}
+      |> fold Splitter.add_split @{thms split_zdiv split_zmod split_div' split_min split_max}
     (* Simp rules for changing (n::int) to int n *)
     val simpset1 =
       put_simpset HOL_basic_ss ctxt
-      addsimps [zdvd_int] @ map (fn r => r RS sym)
-        [@{thm int_numeral}, @{thm int_int_eq}, @{thm zle_int}, @{thm zless_int}, @{thm zadd_int}, @{thm zmult_int}]
-      |> Splitter.add_split zdiff_int_split
+      addsimps @{thms zdvd_int} @
+        map (fn r => r RS sym) @{thms int_numeral int_int_eq zle_int zless_int zadd_int zmult_int}
+      |> Splitter.add_split @{thm zdiff_int_split}
     (*simp rules for elimination of int n*)
 
     val simpset2 =
       put_simpset HOL_basic_ss ctxt
       addsimps [@{thm nat_0_le}, @{thm all_nat}, @{thm ex_nat}, @{thm zero_le_numeral}, @{thm order_refl}(* FIXME: necessary? *), @{thm int_0}, @{thm int_1}]
-      |> fold Simplifier.add_cong [@{thm conj_le_cong}, @{thm imp_le_cong}]
+      |> fold Simplifier.add_cong @{thms conj_le_cong imp_le_cong}
     (* simp rules for elimination of abs *)
     val simpset3 = put_simpset HOL_basic_ss ctxt |> Splitter.add_split @{thm abs_split}
     val ct = cterm_of thy (HOLogic.mk_Trueprop t)
@@ -100,14 +82,16 @@
       (Thm.trivial ct))
     fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
     (* The result of the quantifier elimination *)
-    val (th, tac) = case (prop_of pre_thm) of
+    val (th, tac) =
+      (case (prop_of pre_thm) of
         Const ("==>", _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
-    let val pth = linzqe_oracle (cterm_of thy (Envir.eta_long [] t1))
-    in
-          ((pth RS iffD2) RS pre_thm,
-            assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))
-    end
-      | _ => (pre_thm, assm_tac i)
-  in rtac (((mp_step nh) o (spec_step np)) th) i THEN tac end);
+          let
+            val pth = linzqe_oracle (cterm_of thy (Envir.eta_long [] t1))
+          in
+            ((pth RS iffD2) RS pre_thm,
+              assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))
+          end
+      | _ => (pre_thm, assm_tac i))
+  in rtac (mp_step nh (spec_step np th)) i THEN tac end);
 
 end