misc tuning;
authorwenzelm
Fri Mar 07 20:46:27 2014 +0100 (2014-03-07)
changeset 5598752c22561996d
parent 55986 61b0021ed674
child 55988 ffe88d72afae
misc tuning;
src/HOL/Decision_Procs/cooper_tac.ML
     1.1 --- a/src/HOL/Decision_Procs/cooper_tac.ML	Fri Mar 07 20:32:48 2014 +0100
     1.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML	Fri Mar 07 20:46:27 2014 +0100
     1.3 @@ -12,22 +12,6 @@
     1.4  
     1.5  val cooper_ss = simpset_of @{context};
     1.6  
     1.7 -val nT = HOLogic.natT;
     1.8 -val comp_arith = @{thms simp_thms}
     1.9 -
    1.10 -val zdvd_int = @{thm zdvd_int};
    1.11 -val zdiff_int_split = @{thm zdiff_int_split};
    1.12 -val split_zdiv = @{thm split_zdiv};
    1.13 -val split_zmod = @{thm split_zmod};
    1.14 -val mod_div_equality' = @{thm mod_div_equality'};
    1.15 -val split_div' = @{thm split_div'};
    1.16 -val Suc_eq_plus1 = @{thm Suc_eq_plus1};
    1.17 -val mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
    1.18 -val mod_add_right_eq = @{thm mod_add_right_eq} RS sym;
    1.19 -val mod_add_eq = @{thm mod_add_eq} RS sym;
    1.20 -val nat_div_add_eq = @{thm div_add1_eq} RS sym;
    1.21 -val int_div_add_eq = @{thm zdiv_zadd1_eq} RS sym;
    1.22 -
    1.23  fun prepare_for_linz q fm =
    1.24    let
    1.25      val ps = Logic.strip_params fm
    1.26 @@ -42,53 +26,51 @@
    1.27      val np = length ps
    1.28      val (fm',np) = List.foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
    1.29        (List.foldr HOLogic.mk_imp c rhs, np) ps
    1.30 -    val (vs, _) = List.partition (fn t => q orelse (type_of t) = nT)
    1.31 +    val (vs, _) = List.partition (fn t => q orelse (type_of t) = @{typ nat})
    1.32        (Misc_Legacy.term_frees fm' @ Misc_Legacy.term_vars fm');
    1.33      val fm2 = List.foldr mk_all2 fm' vs
    1.34    in (fm2, np + length vs, length rhs) end;
    1.35  
    1.36  (*Object quantifier to meta --*)
    1.37 -fun spec_step n th = if (n=0) then th else (spec_step (n-1) th) RS spec ;
    1.38 +fun spec_step n th = if n = 0 then th else (spec_step (n - 1) th) RS spec;
    1.39  
    1.40  (* object implication to meta---*)
    1.41 -fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp;
    1.42 +fun mp_step n th = if n = 0 then th else (mp_step (n - 1) th) RS mp;
    1.43  
    1.44  
    1.45  fun linz_tac ctxt q = Object_Logic.atomize_prems_tac ctxt THEN' SUBGOAL (fn (g, i) =>
    1.46    let
    1.47 -    val thy = Proof_Context.theory_of ctxt
    1.48 +    val thy = Proof_Context.theory_of ctxt;
    1.49      (* Transform the term*)
    1.50 -    val (t,np,nh) = prepare_for_linz q g
    1.51 +    val (t, np, nh) = prepare_for_linz q g;
    1.52      (* Some simpsets for dealing with mod div abs and nat*)
    1.53      val mod_div_simpset =
    1.54        put_simpset HOL_basic_ss ctxt
    1.55 -      addsimps [refl,mod_add_eq, mod_add_left_eq,
    1.56 -          mod_add_right_eq,
    1.57 -          nat_div_add_eq, int_div_add_eq,
    1.58 -          @{thm mod_self},
    1.59 -          @{thm div_by_0}, @{thm mod_by_0}, @{thm div_0}, @{thm mod_0},
    1.60 -          @{thm div_by_1}, @{thm mod_by_1}, @{thm div_1}, @{thm mod_1},
    1.61 -          Suc_eq_plus1]
    1.62 +      addsimps @{thms refl mod_add_eq [symmetric] mod_add_left_eq [symmetric]
    1.63 +          mod_add_right_eq [symmetric]
    1.64 +          div_add1_eq [symmetric] zdiv_zadd1_eq [symmetric]
    1.65 +          mod_self
    1.66 +          div_by_0 mod_by_0 div_0 mod_0
    1.67 +          div_by_1 mod_by_1 div_1 mod_1
    1.68 +          Suc_eq_plus1}
    1.69        addsimps @{thms add_ac}
    1.70        addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}]
    1.71      val simpset0 =
    1.72        put_simpset HOL_basic_ss ctxt
    1.73 -      addsimps [mod_div_equality', Suc_eq_plus1]
    1.74 -      addsimps comp_arith
    1.75 -      |> fold Splitter.add_split
    1.76 -          [split_zdiv, split_zmod, split_div', @{thm "split_min"}, @{thm "split_max"}]
    1.77 +      addsimps @{thms mod_div_equality' Suc_eq_plus1 simp_thms}
    1.78 +      |> fold Splitter.add_split @{thms split_zdiv split_zmod split_div' split_min split_max}
    1.79      (* Simp rules for changing (n::int) to int n *)
    1.80      val simpset1 =
    1.81        put_simpset HOL_basic_ss ctxt
    1.82 -      addsimps [zdvd_int] @ map (fn r => r RS sym)
    1.83 -        [@{thm int_numeral}, @{thm int_int_eq}, @{thm zle_int}, @{thm zless_int}, @{thm zadd_int}, @{thm zmult_int}]
    1.84 -      |> Splitter.add_split zdiff_int_split
    1.85 +      addsimps @{thms zdvd_int} @
    1.86 +        map (fn r => r RS sym) @{thms int_numeral int_int_eq zle_int zless_int zadd_int zmult_int}
    1.87 +      |> Splitter.add_split @{thm zdiff_int_split}
    1.88      (*simp rules for elimination of int n*)
    1.89  
    1.90      val simpset2 =
    1.91        put_simpset HOL_basic_ss ctxt
    1.92        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}]
    1.93 -      |> fold Simplifier.add_cong [@{thm conj_le_cong}, @{thm imp_le_cong}]
    1.94 +      |> fold Simplifier.add_cong @{thms conj_le_cong imp_le_cong}
    1.95      (* simp rules for elimination of abs *)
    1.96      val simpset3 = put_simpset HOL_basic_ss ctxt |> Splitter.add_split @{thm abs_split}
    1.97      val ct = cterm_of thy (HOLogic.mk_Trueprop t)
    1.98 @@ -100,14 +82,16 @@
    1.99        (Thm.trivial ct))
   1.100      fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
   1.101      (* The result of the quantifier elimination *)
   1.102 -    val (th, tac) = case (prop_of pre_thm) of
   1.103 +    val (th, tac) =
   1.104 +      (case (prop_of pre_thm) of
   1.105          Const ("==>", _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
   1.106 -    let val pth = linzqe_oracle (cterm_of thy (Envir.eta_long [] t1))
   1.107 -    in
   1.108 -          ((pth RS iffD2) RS pre_thm,
   1.109 -            assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))
   1.110 -    end
   1.111 -      | _ => (pre_thm, assm_tac i)
   1.112 -  in rtac (((mp_step nh) o (spec_step np)) th) i THEN tac end);
   1.113 +          let
   1.114 +            val pth = linzqe_oracle (cterm_of thy (Envir.eta_long [] t1))
   1.115 +          in
   1.116 +            ((pth RS iffD2) RS pre_thm,
   1.117 +              assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))
   1.118 +          end
   1.119 +      | _ => (pre_thm, assm_tac i))
   1.120 +  in rtac (mp_step nh (spec_step np th)) i THEN tac end);
   1.121  
   1.122  end