src/HOL/Tools/Presburger/presburger.ML

tuned;

(*  Title:      HOL/Tools/Presburger/presburger.ML
    ID:         $Id$
    Author:     Amine Chaieb, TU Muenchen
*)

signature PRESBURGER =
 sig
  val cooper_tac: bool -> thm list -> thm list -> Proof.context -> int -> Tactical.tactic
end;

structure Presburger : PRESBURGER = 
struct

open Conv;
val comp_ss = HOL_ss addsimps @{thms "Groebner_Basis.comp_arith"};

fun strip_imp_cprems ct = 
 case term_of ct of 
  Const ("==>", _) $ _ $ _ => Thm.dest_arg1 ct :: strip_imp_cprems (Thm.dest_arg ct)
| _ => [];

val cprems_of = strip_imp_cprems o cprop_of;

fun strip_objimp ct = 
 case term_of ct of 
  Const ("op -->", _) $ _ $ _ => Thm.dest_arg1 ct :: strip_objimp (Thm.dest_arg ct)
| _ => [ct];

fun strip_objall ct = 
 case term_of ct of 
  Const ("All", _) $ Abs (xn,xT,p) => 
   let val (a,(v,t')) = (apsnd (Thm.dest_abs (SOME xn)) o Thm.dest_comb) ct
   in apfst (cons (a,v)) (strip_objall t')
   end
| _ => ([],ct);

local
  val all_maxscope_ss = 
     HOL_basic_ss addsimps map (fn th => th RS sym) @{thms "all_simps"}
in
fun thin_prems_tac P i =  simp_tac all_maxscope_ss i THEN
  (fn st => case try (nth (cprems_of st)) (i - 1) of
    NONE => no_tac st
  | SOME p' => 
    let
     val (qvs, p) = strip_objall (Thm.dest_arg p')
     val (ps, c) = split_last (strip_objimp p)
     val qs = filter P ps
     val q = if P c then c else @{cterm "False"}
     val ng = fold_rev (fn (a,v) => fn t => Thm.capply a (Thm.cabs v t)) qvs 
         (fold_rev (fn p => fn q => Thm.capply (Thm.capply @{cterm "op -->"} p) q) qs q)
     val g = Thm.capply (Thm.capply @{cterm "op ==>"} (Thm.capply @{cterm "Trueprop"} ng)) p'
     val ntac = (case qs of [] => q aconvc @{cterm "False"}
                         | _ => false)
    in 
    if ntac then no_tac st
      else rtac (Goal.prove_internal [] g (K (blast_tac HOL_cs 1))) i st 
    end)
end;

local
 fun ty cts t = 
 if not (typ_of (ctyp_of_term t) mem [HOLogic.intT, HOLogic.natT]) then false 
    else case term_of t of 
      c$_$_ => not (member (op aconv) cts c)
    | c$_ => not (member (op aconv) cts c)
    | c => not (member (op aconv) cts c)
    | _ => true

 val term_constants =
  let fun h acc t = case t of
    Const _ => insert (op aconv) t acc
  | a$b => h (h acc a) b
  | Abs (_,_,t) => h acc t
  | _ => acc
 in h [] end;
in 
fun is_relevant ctxt ct = 
  gen_subset (op aconv) (term_constants (term_of ct) , snd (CooperData.get ctxt))
 andalso forall (fn Free (_,T) => T = HOLogic.intT) (term_frees (term_of ct))
 andalso forall (fn Var (_,T) => T = HOLogic.intT) (term_vars (term_of ct));

fun int_nat_terms ctxt ct =
 let 
  val cts = snd (CooperData.get ctxt)
  fun h acc t = if ty cts t then insert (op aconvc) t acc else
   case (term_of t) of
    _$_ => h (h acc (Thm.dest_arg t)) (Thm.dest_fun t)
  | Abs(_,_,_) => Thm.dest_abs NONE t ||> h acc |> uncurry (remove (op aconvc))
  | _ => acc
 in h [] ct end
end;

fun generalize_tac ctxt f i st = 
 case try (nth (cprems_of st)) (i - 1) of
    NONE => all_tac st
  | SOME p => 
   let 
   fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"}
   fun gen x t = Thm.capply (all (ctyp_of_term x)) (Thm.cabs x t)
   val ts = sort (fn (a,b) => Term.fast_term_ord (term_of a, term_of b)) (f p)
   val p' = fold_rev gen ts p
 in Seq.of_list [implies_intr p' (implies_elim st (fold forall_elim ts (assume p')))]
 end;

local
val ss1 = comp_ss
  addsimps simp_thms @ [@{thm "nat_number_of_def"}, @{thm "zdvd_int"}] 
      @ map (fn r => r RS sym) 
        [@{thm "int_int_eq"}, @{thm "zle_int"}, @{thm "zless_int"}, @{thm "zadd_int"}, 
         @{thm "zmult_int"}]
    addsplits [@{thm "zdiff_int_split"}]

val ss2 = HOL_basic_ss
  addsimps [@{thm "nat_0_le"}, @{thm "int_nat_number_of"},
            @{thm "all_nat"}, @{thm "ex_nat"}, @{thm "number_of1"}, 
            @{thm "number_of2"}, @{thm "int_0"}, @{thm "int_1"}, @{thm "Suc_plus1"}]
  addcongs [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}]
val div_mod_ss = HOL_basic_ss addsimps simp_thms 
  @ map (symmetric o mk_meta_eq) 
    [@{thm "dvd_eq_mod_eq_0"}, @{thm "zdvd_iff_zmod_eq_0"}, mod_add1_eq, 
     mod_add_left_eq, mod_add_right_eq, 
     @{thm "zmod_zadd1_eq"}, @{thm "zmod_zadd_left_eq"}, 
     @{thm "zmod_zadd_right_eq"}, @{thm "div_add1_eq"}, @{thm "zdiv_zadd1_eq"}]
  @ [@{thm "mod_self"}, @{thm "zmod_self"}, @{thm "DIVISION_BY_ZERO_MOD"}, 
     @{thm "DIVISION_BY_ZERO_DIV"}, @{thm "DIVISION_BY_ZERO"} RS conjunct1, 
     @{thm "DIVISION_BY_ZERO"} RS conjunct2, @{thm "zdiv_zero"}, @{thm "zmod_zero"}, 
     @{thm "div_0"}, @{thm "mod_0"}, @{thm "zdiv_1"}, @{thm "zmod_1"}, @{thm "div_1"}, 
     @{thm "mod_1"}, @{thm "Suc_plus1"}]
  @ add_ac
 addsimprocs [cancel_div_mod_proc]
 val splits_ss = comp_ss addsimps [@{thm "mod_div_equality'"}] addsplits 
     [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"}, 
      @{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}]
in
fun nat_to_int_tac ctxt i = 
  simp_tac (Simplifier.context ctxt ss1) i THEN 
  simp_tac (Simplifier.context ctxt ss2) i THEN 
  TRY (simp_tac (Simplifier.context ctxt comp_ss) i);

fun div_mod_tac  ctxt i = simp_tac (Simplifier.context ctxt div_mod_ss) i;
fun splits_tac ctxt i = simp_tac (Simplifier.context ctxt splits_ss) i;
end;


fun eta_beta_tac ctxt i st = case try (nth (cprems_of st)) (i - 1) of
   NONE => no_tac st
 | SOME p => 
   let
    val eq = (eta_conv (ProofContext.theory_of ctxt) then_conv Thm.beta_conversion true) p
    val p' = Thm.rhs_of eq
    val th = implies_intr p' (equal_elim (symmetric eq) (assume p'))
   in rtac th i st
   end;



fun core_cooper_tac ctxt i st = 
 case try (nth (cprems_of st)) (i - 1) of
   NONE => all_tac st
 | SOME p => 
   let 
    val cpth = 
       if !quick_and_dirty 
       then linzqe_oracle (ProofContext.theory_of ctxt) 
             (Envir.beta_norm (Pattern.eta_long [] (term_of (Thm.dest_arg p))))
       else arg_conv (Cooper.cooper_conv ctxt) p
    val p' = Thm.rhs_of cpth
    val th = implies_intr p' (equal_elim (symmetric cpth) (assume p'))
   in rtac th i st end
   handle Cooper.COOPER _ => no_tac st;

fun nogoal_tac i st = case try (nth (cprems_of st)) (i - 1) of
   NONE => no_tac st
 | SOME _ => all_tac st

fun finish_tac q i st = case try (nth (cprems_of st)) (i - 1) of
   NONE => all_tac st
 | SOME _ => (if q then I else TRY) (rtac TrueI i) st

fun cooper_tac elim add_ths del_ths ctxt i = 
let val ss = fst (CooperData.get ctxt) delsimps del_ths addsimps add_ths
in
nogoal_tac i 
THEN (EVERY o (map TRY))
 [ObjectLogic.full_atomize_tac i,
  eta_beta_tac ctxt i,
  simp_tac ss  i,
  generalize_tac ctxt (int_nat_terms ctxt) i,
  ObjectLogic.full_atomize_tac i,
  div_mod_tac ctxt i,
  splits_tac ctxt i,
  simp_tac ss i,
  eta_beta_tac ctxt i,
  nat_to_int_tac ctxt i, 
  thin_prems_tac (is_relevant ctxt) i]
THEN core_cooper_tac ctxt i THEN finish_tac elim i
end;

end;