src/HOL/Tools/Qelim/presburger.ML

fixed title

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

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

structure Presburger : PRESBURGER = 
struct

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

fun strip_objimp ct =
  (case Thm.term_of ct of
    Const ("op -->", _) $ _ $ _ =>
      let val (A, B) = Thm.dest_binop ct
      in A :: strip_objimp B end
  | _ => [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 = simp_tac all_maxscope_ss THEN'
  CSUBGOAL (fn (p', i) =>
    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
      else rtac (Goal.prove_internal [] g (K (blast_tac HOL_cs 1))) i
    end)
end;

local
 fun isnum t = case t of 
   Const(@{const_name "HOL.zero"},_) => true
 | Const(@{const_name "HOL.one"},_) => true
 | @{term "Suc"}$s => isnum s
 | @{term "nat"}$s => isnum s
 | @{term "int"}$s => isnum s
 | Const(@{const_name "uminus"},_)$s => isnum s
 | Const(@{const_name "HOL.plus"},_)$l$r => isnum l andalso isnum r
 | Const(@{const_name "HOL.times"},_)$l$r => isnum l andalso isnum r
 | Const(@{const_name "HOL.minus"},_)$l$r => isnum l andalso isnum r
 | Const(@{const_name "Nat.power"},_)$l$r => isnum l andalso isnum r
 | Const(@{const_name "Divides.mod"},_)$l$r => isnum l andalso isnum r
 | Const(@{const_name "Divides.div"},_)$l$r => isnum l andalso isnum r
 | _ => can HOLogic.dest_number t orelse can HOLogic.dest_nat t

 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$l$r => if c mem [@{term"op *::int => _"}, @{term"op *::nat => _"}] 
               then not (isnum l orelse isnum r)
               else not (member (op aconv) cts c)
    | c$_ => not (member (op aconv) cts c)
    | c => not (member (op aconv) cts c)

 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 f = CSUBGOAL (fn (p, i) => PRIMITIVE (fn st =>
 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 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"}, @{thm "mod_add1_eq"}, 
     @{thm "mod_add_left_eq"}, @{thm "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"}]
  @ @{thms 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 = 
  simp_tac (Simplifier.context ctxt ss1) THEN_ALL_NEW
  simp_tac (Simplifier.context ctxt ss2) THEN_ALL_NEW
  simp_tac (Simplifier.context ctxt comp_ss);

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 core_cooper_tac ctxt = CSUBGOAL (fn (p, i) =>
   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 end
   handle Cooper.COOPER _ => no_tac);

fun finish_tac q = SUBGOAL (fn (_, i) =>
  (if q then I else TRY) (rtac TrueI i));

fun cooper_tac elim add_ths del_ths ctxt =
let val ss = fst (CooperData.get ctxt) delsimps del_ths addsimps add_ths
in
  ObjectLogic.full_atomize_tac
  THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
  THEN_ALL_NEW simp_tac ss
  THEN_ALL_NEW (TRY o generalize_tac (int_nat_terms ctxt))
  THEN_ALL_NEW ObjectLogic.full_atomize_tac
  THEN_ALL_NEW div_mod_tac ctxt
  THEN_ALL_NEW splits_tac ctxt
  THEN_ALL_NEW simp_tac ss
  THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
  THEN_ALL_NEW nat_to_int_tac ctxt
  THEN_ALL_NEW (TRY o thin_prems_tac (is_relevant ctxt))
  THEN_ALL_NEW core_cooper_tac ctxt
  THEN_ALL_NEW finish_tac elim
end;

end;