author  wenzelm 
Thu, 29 May 2008 23:46:40 +0200  
changeset 27019  9ad9d6554d05 
parent 25843  af0c90f54ebe 
child 27651  16a26996c30e 
permissions  rwrr 
24584  1 
(* Title: HOL/Tools/Qelim/presburger.ML 
23466  2 
ID: $Id$ 
3 
Author: Amine Chaieb, TU Muenchen 

4 
*) 

5 

6 
signature PRESBURGER = 

23499
7e27947d92d7
tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents:
23488
diff
changeset

7 
sig 
7e27947d92d7
tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents:
23488
diff
changeset

8 
val cooper_tac: bool > thm list > thm list > Proof.context > int > tactic 
23466  9 
end; 
10 

11 
structure Presburger : PRESBURGER = 

12 
struct 

13 

14 
open Conv; 

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

16 

23499
7e27947d92d7
tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents:
23488
diff
changeset

17 
fun strip_objimp ct = 
7e27947d92d7
tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents:
23488
diff
changeset

18 
(case Thm.term_of ct of 
7e27947d92d7
tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents:
23488
diff
changeset

19 
Const ("op >", _) $ _ $ _ => 
7e27947d92d7
tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents:
23488
diff
changeset

20 
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

21 
in A :: strip_objimp B end 
7e27947d92d7
tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents:
23488
diff
changeset

22 
 _ => [ct]); 
23466  23 

24 
fun strip_objall ct = 

25 
case term_of ct of 

26 
Const ("All", _) $ Abs (xn,xT,p) => 

27 
let val (a,(v,t')) = (apsnd (Thm.dest_abs (SOME xn)) o Thm.dest_comb) ct 

28 
in apfst (cons (a,v)) (strip_objall t') 

29 
end 

30 
 _ => ([],ct); 

31 

32 
local 

33 
val all_maxscope_ss = 

34 
HOL_basic_ss addsimps map (fn th => th RS sym) @{thms "all_simps"} 

35 
in 

23499
7e27947d92d7
tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents:
23488
diff
changeset

36 
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

37 
CSUBGOAL (fn (p', i) => 
23466  38 
let 
39 
val (qvs, p) = strip_objall (Thm.dest_arg p') 

40 
val (ps, c) = split_last (strip_objimp p) 

41 
val qs = filter P ps 

42 
val q = if P c then c else @{cterm "False"} 

43 
val ng = fold_rev (fn (a,v) => fn t => Thm.capply a (Thm.cabs v t)) qvs 

44 
(fold_rev (fn p => fn q => Thm.capply (Thm.capply @{cterm "op >"} p) q) qs q) 

45 
val g = Thm.capply (Thm.capply @{cterm "op ==>"} (Thm.capply @{cterm "Trueprop"} ng)) p' 

46 
val ntac = (case qs of [] => q aconvc @{cterm "False"} 

47 
 _ => false) 

48 
in 

23499
7e27947d92d7
tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents:
23488
diff
changeset

49 
if ntac then no_tac 
7e27947d92d7
tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents:
23488
diff
changeset

50 
else rtac (Goal.prove_internal [] g (K (blast_tac HOL_cs 1))) i 
23466  51 
end) 
52 
end; 

53 

54 
local 

24403
b7c3ee2ca184
More selective generalization : a*b is generalized whenever none of a and b is a number
chaieb
parents:
23880
diff
changeset

55 
fun isnum t = case t of 
b7c3ee2ca184
More selective generalization : a*b is generalized whenever none of a and b is a number
chaieb
parents:
23880
diff
changeset

56 
Const(@{const_name "HOL.zero"},_) => true 
b7c3ee2ca184
More selective generalization : a*b is generalized whenever none of a and b is a number
chaieb
parents:
23880
diff
changeset

57 
 Const(@{const_name "HOL.one"},_) => true 
b7c3ee2ca184
More selective generalization : a*b is generalized whenever none of a and b is a number
chaieb
parents:
23880
diff
changeset

58 
 @{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

59 
 @{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

60 
 @{term "int"}$s => isnum s 
25768  61 
 Const(@{const_name "HOL.uminus"},_)$s => isnum s 
24403
b7c3ee2ca184
More selective generalization : a*b is generalized whenever none of a and b is a number
chaieb
parents:
23880
diff
changeset

62 
 Const(@{const_name "HOL.plus"},_)$l$r => isnum l andalso isnum r 
b7c3ee2ca184
More selective generalization : a*b is generalized whenever none of a and b is a number
chaieb
parents:
23880
diff
changeset

63 
 Const(@{const_name "HOL.times"},_)$l$r => isnum l andalso isnum r 
b7c3ee2ca184
More selective generalization : a*b is generalized whenever none of a and b is a number
chaieb
parents:
23880
diff
changeset

64 
 Const(@{const_name "HOL.minus"},_)$l$r => isnum l andalso isnum r 
24996  65 
 Const(@{const_name "Power.power"},_)$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

66 
 Const(@{const_name "Divides.mod"},_)$l$r => isnum l andalso isnum r 
b7c3ee2ca184
More selective generalization : a*b is generalized whenever none of a and b is a number
chaieb
parents:
23880
diff
changeset

67 
 Const(@{const_name "Divides.div"},_)$l$r => isnum l andalso isnum r 
b7c3ee2ca184
More selective generalization : a*b is generalized whenever none of a and b is a number
chaieb
parents:
23880
diff
changeset

68 
 _ => 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

69 

23466  70 
fun ty cts t = 
25843  71 
if not (typ_of (ctyp_of_term t) mem [HOLogic.intT, HOLogic.natT, HOLogic.boolT]) then false 
23466  72 
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

73 
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

74 
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

75 
else not (member (op aconv) cts c) 
23466  76 
 c$_ => not (member (op aconv) cts c) 
77 
 c => not (member (op aconv) cts c) 

78 

79 
val term_constants = 

80 
let fun h acc t = case t of 

81 
Const _ => insert (op aconv) t acc 

82 
 a$b => h (h acc a) b 

83 
 Abs (_,_,t) => h acc t 

84 
 _ => acc 

85 
in h [] end; 

86 
in 

87 
fun is_relevant ctxt ct = 

25811  88 
gen_subset (op aconv) (term_constants (term_of ct) , snd (CooperData.get ctxt)) 
89 
andalso forall (fn Free (_,T) => T mem [@{typ "int"}, @{typ nat}]) (term_frees (term_of ct)) 

90 
andalso forall (fn Var (_,T) => T mem [@{typ "int"}, @{typ nat}]) (term_vars (term_of ct)); 

23466  91 

92 
fun int_nat_terms ctxt ct = 

93 
let 

94 
val cts = snd (CooperData.get ctxt) 

95 
fun h acc t = if ty cts t then insert (op aconvc) t acc else 

96 
case (term_of t) of 

97 
_$_ => h (h acc (Thm.dest_arg t)) (Thm.dest_fun t) 

98 
 Abs(_,_,_) => Thm.dest_abs NONE t > h acc > uncurry (remove (op aconvc)) 

99 
 _ => acc 

100 
in h [] ct end 

101 
end; 

102 

23499
7e27947d92d7
tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents:
23488
diff
changeset

103 
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

104 
let 
23466  105 
fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"} 
106 
fun gen x t = Thm.capply (all (ctyp_of_term x)) (Thm.cabs x t) 

107 
val ts = sort (fn (a,b) => Term.fast_term_ord (term_of a, term_of b)) (f p) 

108 
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

109 
in implies_intr p' (implies_elim st (fold forall_elim ts (assume p'))) end)); 
23466  110 

111 
local 

112 
val ss1 = comp_ss 

113 
addsimps simp_thms @ [@{thm "nat_number_of_def"}, @{thm "zdvd_int"}] 

114 
@ map (fn r => r RS sym) 

115 
[@{thm "int_int_eq"}, @{thm "zle_int"}, @{thm "zless_int"}, @{thm "zadd_int"}, 

116 
@{thm "zmult_int"}] 

117 
addsplits [@{thm "zdiff_int_split"}] 

118 

119 
val ss2 = HOL_basic_ss 

120 
addsimps [@{thm "nat_0_le"}, @{thm "int_nat_number_of"}, 

121 
@{thm "all_nat"}, @{thm "ex_nat"}, @{thm "number_of1"}, 

122 
@{thm "number_of2"}, @{thm "int_0"}, @{thm "int_1"}, @{thm "Suc_plus1"}] 

123 
addcongs [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}] 

124 
val div_mod_ss = HOL_basic_ss addsimps simp_thms 

125 
@ map (symmetric o mk_meta_eq) 

23469  126 
[@{thm "dvd_eq_mod_eq_0"}, @{thm "zdvd_iff_zmod_eq_0"}, @{thm "mod_add1_eq"}, 
127 
@{thm "mod_add_left_eq"}, @{thm "mod_add_right_eq"}, 

23466  128 
@{thm "zmod_zadd1_eq"}, @{thm "zmod_zadd_left_eq"}, 
129 
@{thm "zmod_zadd_right_eq"}, @{thm "div_add1_eq"}, @{thm "zdiv_zadd1_eq"}] 

130 
@ [@{thm "mod_self"}, @{thm "zmod_self"}, @{thm "DIVISION_BY_ZERO_MOD"}, 

131 
@{thm "DIVISION_BY_ZERO_DIV"}, @{thm "DIVISION_BY_ZERO"} RS conjunct1, 

132 
@{thm "DIVISION_BY_ZERO"} RS conjunct2, @{thm "zdiv_zero"}, @{thm "zmod_zero"}, 

133 
@{thm "div_0"}, @{thm "mod_0"}, @{thm "zdiv_1"}, @{thm "zmod_1"}, @{thm "div_1"}, 

134 
@{thm "mod_1"}, @{thm "Suc_plus1"}] 

23880  135 
@ @{thms add_ac} 
23466  136 
addsimprocs [cancel_div_mod_proc] 
137 
val splits_ss = comp_ss addsimps [@{thm "mod_div_equality'"}] addsplits 

138 
[@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"}, 

139 
@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}] 

140 
in 

23499
7e27947d92d7
tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents:
23488
diff
changeset

141 
fun nat_to_int_tac ctxt = 
7e27947d92d7
tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents:
23488
diff
changeset

142 
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

143 
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

144 
simp_tac (Simplifier.context ctxt comp_ss); 
23466  145 

23499
7e27947d92d7
tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents:
23488
diff
changeset

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

149 

150 

23499
7e27947d92d7
tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents:
23488
diff
changeset

151 
fun core_cooper_tac ctxt = CSUBGOAL (fn (p, i) => 
23466  152 
let 
153 
val cpth = 

154 
if !quick_and_dirty 

155 
then linzqe_oracle (ProofContext.theory_of ctxt) 

156 
(Envir.beta_norm (Pattern.eta_long [] (term_of (Thm.dest_arg p)))) 

157 
else arg_conv (Cooper.cooper_conv ctxt) p 

158 
val p' = Thm.rhs_of cpth 

159 
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

160 
in rtac th i end 
7e27947d92d7
tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents:
23488
diff
changeset

161 
handle Cooper.COOPER _ => no_tac); 
23466  162 

23499
7e27947d92d7
tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents:
23488
diff
changeset

163 
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

164 
(if q then I else TRY) (rtac TrueI i)); 
23466  165 

23499
7e27947d92d7
tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents:
23488
diff
changeset

166 
fun cooper_tac elim add_ths del_ths ctxt = 
27019  167 
let val ss = Simplifier.context ctxt (fst (CooperData.get ctxt)) delsimps del_ths addsimps add_ths 
23466  168 
in 
23499
7e27947d92d7
tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents:
23488
diff
changeset

169 
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 
25800
0298341876d0
Changed order of tactics in presburger  thinning before case splits
chaieb
parents:
25768
diff
changeset

174 
THEN_ALL_NEW (TRY o 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 
7e27947d92d7
tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents:
23488
diff
changeset

181 
THEN_ALL_NEW core_cooper_tac ctxt 
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; 