(* 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"}, @{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"}]
@ 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 = (Thm.eta_long_conversion 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;