wenzelm@23466
|
1 |
(* Title: HOL/Tools/Presburger/presburger.ML
|
wenzelm@23466
|
2 |
ID: $Id$
|
wenzelm@23466
|
3 |
Author: Amine Chaieb, TU Muenchen
|
wenzelm@23466
|
4 |
*)
|
wenzelm@23466
|
5 |
|
wenzelm@23466
|
6 |
signature PRESBURGER =
|
wenzelm@23499
|
7 |
sig
|
wenzelm@23499
|
8 |
val cooper_tac: bool -> thm list -> thm list -> Proof.context -> int -> tactic
|
wenzelm@23466
|
9 |
end;
|
wenzelm@23466
|
10 |
|
wenzelm@23466
|
11 |
structure Presburger : PRESBURGER =
|
wenzelm@23466
|
12 |
struct
|
wenzelm@23466
|
13 |
|
wenzelm@23466
|
14 |
open Conv;
|
wenzelm@23466
|
15 |
val comp_ss = HOL_ss addsimps @{thms "Groebner_Basis.comp_arith"};
|
wenzelm@23466
|
16 |
|
wenzelm@23499
|
17 |
fun strip_objimp ct =
|
wenzelm@23499
|
18 |
(case Thm.term_of ct of
|
wenzelm@23499
|
19 |
Const ("op -->", _) $ _ $ _ =>
|
wenzelm@23499
|
20 |
let val (A, B) = Thm.dest_binop ct
|
wenzelm@23499
|
21 |
in A :: strip_objimp B end
|
wenzelm@23499
|
22 |
| _ => [ct]);
|
wenzelm@23466
|
23 |
|
wenzelm@23466
|
24 |
fun strip_objall ct =
|
wenzelm@23466
|
25 |
case term_of ct of
|
wenzelm@23466
|
26 |
Const ("All", _) $ Abs (xn,xT,p) =>
|
wenzelm@23466
|
27 |
let val (a,(v,t')) = (apsnd (Thm.dest_abs (SOME xn)) o Thm.dest_comb) ct
|
wenzelm@23466
|
28 |
in apfst (cons (a,v)) (strip_objall t')
|
wenzelm@23466
|
29 |
end
|
wenzelm@23466
|
30 |
| _ => ([],ct);
|
wenzelm@23466
|
31 |
|
wenzelm@23466
|
32 |
local
|
wenzelm@23466
|
33 |
val all_maxscope_ss =
|
wenzelm@23466
|
34 |
HOL_basic_ss addsimps map (fn th => th RS sym) @{thms "all_simps"}
|
wenzelm@23466
|
35 |
in
|
wenzelm@23499
|
36 |
fun thin_prems_tac P = simp_tac all_maxscope_ss THEN'
|
wenzelm@23499
|
37 |
CSUBGOAL (fn (p', i) =>
|
wenzelm@23466
|
38 |
let
|
wenzelm@23466
|
39 |
val (qvs, p) = strip_objall (Thm.dest_arg p')
|
wenzelm@23466
|
40 |
val (ps, c) = split_last (strip_objimp p)
|
wenzelm@23466
|
41 |
val qs = filter P ps
|
wenzelm@23466
|
42 |
val q = if P c then c else @{cterm "False"}
|
wenzelm@23466
|
43 |
val ng = fold_rev (fn (a,v) => fn t => Thm.capply a (Thm.cabs v t)) qvs
|
wenzelm@23466
|
44 |
(fold_rev (fn p => fn q => Thm.capply (Thm.capply @{cterm "op -->"} p) q) qs q)
|
wenzelm@23466
|
45 |
val g = Thm.capply (Thm.capply @{cterm "op ==>"} (Thm.capply @{cterm "Trueprop"} ng)) p'
|
wenzelm@23466
|
46 |
val ntac = (case qs of [] => q aconvc @{cterm "False"}
|
wenzelm@23466
|
47 |
| _ => false)
|
wenzelm@23466
|
48 |
in
|
wenzelm@23499
|
49 |
if ntac then no_tac
|
wenzelm@23499
|
50 |
else rtac (Goal.prove_internal [] g (K (blast_tac HOL_cs 1))) i
|
wenzelm@23466
|
51 |
end)
|
wenzelm@23466
|
52 |
end;
|
wenzelm@23466
|
53 |
|
wenzelm@23466
|
54 |
local
|
chaieb@24403
|
55 |
fun isnum t = case t of
|
chaieb@24403
|
56 |
Const(@{const_name "HOL.zero"},_) => true
|
chaieb@24403
|
57 |
| Const(@{const_name "HOL.one"},_) => true
|
chaieb@24403
|
58 |
| @{term "Suc"}$s => isnum s
|
chaieb@24403
|
59 |
| @{term "nat"}$s => isnum s
|
chaieb@24403
|
60 |
| @{term "int"}$s => isnum s
|
chaieb@24403
|
61 |
| Const(@{const_name "uminus"},_)$s => isnum s
|
chaieb@24403
|
62 |
| Const(@{const_name "HOL.plus"},_)$l$r => isnum l andalso isnum r
|
chaieb@24403
|
63 |
| Const(@{const_name "HOL.times"},_)$l$r => isnum l andalso isnum r
|
chaieb@24403
|
64 |
| Const(@{const_name "HOL.minus"},_)$l$r => isnum l andalso isnum r
|
chaieb@24403
|
65 |
| Const(@{const_name "Nat.power"},_)$l$r => isnum l andalso isnum r
|
chaieb@24403
|
66 |
| Const(@{const_name "Divides.mod"},_)$l$r => isnum l andalso isnum r
|
chaieb@24403
|
67 |
| Const(@{const_name "Divides.div"},_)$l$r => isnum l andalso isnum r
|
chaieb@24403
|
68 |
| _ => can HOLogic.dest_number t orelse can HOLogic.dest_nat t
|
chaieb@24403
|
69 |
|
wenzelm@23466
|
70 |
fun ty cts t =
|
wenzelm@23466
|
71 |
if not (typ_of (ctyp_of_term t) mem [HOLogic.intT, HOLogic.natT]) then false
|
wenzelm@23466
|
72 |
else case term_of t of
|
chaieb@24403
|
73 |
c$l$r => if c mem [@{term"op *::int => _"}, @{term"op *::nat => _"}]
|
chaieb@24403
|
74 |
then not (isnum l orelse isnum r)
|
chaieb@24403
|
75 |
else not (member (op aconv) cts c)
|
wenzelm@23466
|
76 |
| c$_ => not (member (op aconv) cts c)
|
wenzelm@23466
|
77 |
| c => not (member (op aconv) cts c)
|
wenzelm@23466
|
78 |
|
wenzelm@23466
|
79 |
val term_constants =
|
wenzelm@23466
|
80 |
let fun h acc t = case t of
|
wenzelm@23466
|
81 |
Const _ => insert (op aconv) t acc
|
wenzelm@23466
|
82 |
| a$b => h (h acc a) b
|
wenzelm@23466
|
83 |
| Abs (_,_,t) => h acc t
|
wenzelm@23466
|
84 |
| _ => acc
|
wenzelm@23466
|
85 |
in h [] end;
|
wenzelm@23466
|
86 |
in
|
wenzelm@23466
|
87 |
fun is_relevant ctxt ct =
|
wenzelm@23466
|
88 |
gen_subset (op aconv) (term_constants (term_of ct) , snd (CooperData.get ctxt))
|
wenzelm@23466
|
89 |
andalso forall (fn Free (_,T) => T = HOLogic.intT) (term_frees (term_of ct))
|
wenzelm@23466
|
90 |
andalso forall (fn Var (_,T) => T = HOLogic.intT) (term_vars (term_of ct));
|
wenzelm@23466
|
91 |
|
wenzelm@23466
|
92 |
fun int_nat_terms ctxt ct =
|
wenzelm@23466
|
93 |
let
|
wenzelm@23466
|
94 |
val cts = snd (CooperData.get ctxt)
|
wenzelm@23466
|
95 |
fun h acc t = if ty cts t then insert (op aconvc) t acc else
|
wenzelm@23466
|
96 |
case (term_of t) of
|
wenzelm@23466
|
97 |
_$_ => h (h acc (Thm.dest_arg t)) (Thm.dest_fun t)
|
wenzelm@23466
|
98 |
| Abs(_,_,_) => Thm.dest_abs NONE t ||> h acc |> uncurry (remove (op aconvc))
|
wenzelm@23466
|
99 |
| _ => acc
|
wenzelm@23466
|
100 |
in h [] ct end
|
wenzelm@23466
|
101 |
end;
|
wenzelm@23466
|
102 |
|
wenzelm@23499
|
103 |
fun generalize_tac f = CSUBGOAL (fn (p, i) => PRIMITIVE (fn st =>
|
wenzelm@23499
|
104 |
let
|
wenzelm@23466
|
105 |
fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"}
|
wenzelm@23466
|
106 |
fun gen x t = Thm.capply (all (ctyp_of_term x)) (Thm.cabs x t)
|
wenzelm@23466
|
107 |
val ts = sort (fn (a,b) => Term.fast_term_ord (term_of a, term_of b)) (f p)
|
wenzelm@23466
|
108 |
val p' = fold_rev gen ts p
|
wenzelm@23499
|
109 |
in implies_intr p' (implies_elim st (fold forall_elim ts (assume p'))) end));
|
wenzelm@23466
|
110 |
|
wenzelm@23466
|
111 |
local
|
wenzelm@23466
|
112 |
val ss1 = comp_ss
|
wenzelm@23466
|
113 |
addsimps simp_thms @ [@{thm "nat_number_of_def"}, @{thm "zdvd_int"}]
|
wenzelm@23466
|
114 |
@ map (fn r => r RS sym)
|
wenzelm@23466
|
115 |
[@{thm "int_int_eq"}, @{thm "zle_int"}, @{thm "zless_int"}, @{thm "zadd_int"},
|
wenzelm@23466
|
116 |
@{thm "zmult_int"}]
|
wenzelm@23466
|
117 |
addsplits [@{thm "zdiff_int_split"}]
|
wenzelm@23466
|
118 |
|
wenzelm@23466
|
119 |
val ss2 = HOL_basic_ss
|
wenzelm@23466
|
120 |
addsimps [@{thm "nat_0_le"}, @{thm "int_nat_number_of"},
|
wenzelm@23466
|
121 |
@{thm "all_nat"}, @{thm "ex_nat"}, @{thm "number_of1"},
|
wenzelm@23466
|
122 |
@{thm "number_of2"}, @{thm "int_0"}, @{thm "int_1"}, @{thm "Suc_plus1"}]
|
wenzelm@23466
|
123 |
addcongs [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}]
|
wenzelm@23466
|
124 |
val div_mod_ss = HOL_basic_ss addsimps simp_thms
|
wenzelm@23466
|
125 |
@ map (symmetric o mk_meta_eq)
|
huffman@23469
|
126 |
[@{thm "dvd_eq_mod_eq_0"}, @{thm "zdvd_iff_zmod_eq_0"}, @{thm "mod_add1_eq"},
|
huffman@23469
|
127 |
@{thm "mod_add_left_eq"}, @{thm "mod_add_right_eq"},
|
wenzelm@23466
|
128 |
@{thm "zmod_zadd1_eq"}, @{thm "zmod_zadd_left_eq"},
|
wenzelm@23466
|
129 |
@{thm "zmod_zadd_right_eq"}, @{thm "div_add1_eq"}, @{thm "zdiv_zadd1_eq"}]
|
wenzelm@23466
|
130 |
@ [@{thm "mod_self"}, @{thm "zmod_self"}, @{thm "DIVISION_BY_ZERO_MOD"},
|
wenzelm@23466
|
131 |
@{thm "DIVISION_BY_ZERO_DIV"}, @{thm "DIVISION_BY_ZERO"} RS conjunct1,
|
wenzelm@23466
|
132 |
@{thm "DIVISION_BY_ZERO"} RS conjunct2, @{thm "zdiv_zero"}, @{thm "zmod_zero"},
|
wenzelm@23466
|
133 |
@{thm "div_0"}, @{thm "mod_0"}, @{thm "zdiv_1"}, @{thm "zmod_1"}, @{thm "div_1"},
|
wenzelm@23466
|
134 |
@{thm "mod_1"}, @{thm "Suc_plus1"}]
|
haftmann@23880
|
135 |
@ @{thms add_ac}
|
wenzelm@23466
|
136 |
addsimprocs [cancel_div_mod_proc]
|
wenzelm@23466
|
137 |
val splits_ss = comp_ss addsimps [@{thm "mod_div_equality'"}] addsplits
|
wenzelm@23466
|
138 |
[@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"},
|
wenzelm@23466
|
139 |
@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}]
|
wenzelm@23466
|
140 |
in
|
wenzelm@23499
|
141 |
fun nat_to_int_tac ctxt =
|
wenzelm@23499
|
142 |
simp_tac (Simplifier.context ctxt ss1) THEN_ALL_NEW
|
wenzelm@23499
|
143 |
simp_tac (Simplifier.context ctxt ss2) THEN_ALL_NEW
|
wenzelm@23499
|
144 |
simp_tac (Simplifier.context ctxt comp_ss);
|
wenzelm@23466
|
145 |
|
wenzelm@23499
|
146 |
fun div_mod_tac ctxt i = simp_tac (Simplifier.context ctxt div_mod_ss) i;
|
wenzelm@23466
|
147 |
fun splits_tac ctxt i = simp_tac (Simplifier.context ctxt splits_ss) i;
|
wenzelm@23466
|
148 |
end;
|
wenzelm@23466
|
149 |
|
wenzelm@23466
|
150 |
|
wenzelm@23499
|
151 |
fun core_cooper_tac ctxt = CSUBGOAL (fn (p, i) =>
|
wenzelm@23466
|
152 |
let
|
wenzelm@23466
|
153 |
val cpth =
|
wenzelm@23466
|
154 |
if !quick_and_dirty
|
wenzelm@23466
|
155 |
then linzqe_oracle (ProofContext.theory_of ctxt)
|
wenzelm@23466
|
156 |
(Envir.beta_norm (Pattern.eta_long [] (term_of (Thm.dest_arg p))))
|
wenzelm@23466
|
157 |
else arg_conv (Cooper.cooper_conv ctxt) p
|
wenzelm@23466
|
158 |
val p' = Thm.rhs_of cpth
|
wenzelm@23466
|
159 |
val th = implies_intr p' (equal_elim (symmetric cpth) (assume p'))
|
wenzelm@23499
|
160 |
in rtac th i end
|
wenzelm@23499
|
161 |
handle Cooper.COOPER _ => no_tac);
|
wenzelm@23466
|
162 |
|
wenzelm@23499
|
163 |
fun finish_tac q = SUBGOAL (fn (_, i) =>
|
wenzelm@23499
|
164 |
(if q then I else TRY) (rtac TrueI i));
|
wenzelm@23466
|
165 |
|
wenzelm@23499
|
166 |
fun cooper_tac elim add_ths del_ths ctxt =
|
wenzelm@23466
|
167 |
let val ss = fst (CooperData.get ctxt) delsimps del_ths addsimps add_ths
|
wenzelm@23466
|
168 |
in
|
wenzelm@23499
|
169 |
ObjectLogic.full_atomize_tac
|
wenzelm@23530
|
170 |
THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
|
wenzelm@23499
|
171 |
THEN_ALL_NEW simp_tac ss
|
wenzelm@23499
|
172 |
THEN_ALL_NEW (TRY o generalize_tac (int_nat_terms ctxt))
|
wenzelm@23499
|
173 |
THEN_ALL_NEW ObjectLogic.full_atomize_tac
|
wenzelm@23499
|
174 |
THEN_ALL_NEW div_mod_tac ctxt
|
wenzelm@23499
|
175 |
THEN_ALL_NEW splits_tac ctxt
|
wenzelm@23499
|
176 |
THEN_ALL_NEW simp_tac ss
|
wenzelm@23530
|
177 |
THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
|
wenzelm@23499
|
178 |
THEN_ALL_NEW nat_to_int_tac ctxt
|
wenzelm@23499
|
179 |
THEN_ALL_NEW (TRY o thin_prems_tac (is_relevant ctxt))
|
wenzelm@23499
|
180 |
THEN_ALL_NEW core_cooper_tac ctxt
|
wenzelm@23499
|
181 |
THEN_ALL_NEW finish_tac elim
|
wenzelm@23466
|
182 |
end;
|
wenzelm@23466
|
183 |
|
wenzelm@23466
|
184 |
end;
|