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