author wenzelm Fri Mar 07 20:46:27 2014 +0100 (2014-03-07) changeset 55987 52c22561996d parent 55986 61b0021ed674 child 55988 ffe88d72afae
misc tuning;
```     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.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.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.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.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.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.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
```