author  wenzelm 
Fri, 27 Aug 2010 17:59:40 +0200  
changeset 38808  89ae86205739 
parent 38795  848be46708dc 
child 38864  4abe644fcea5 
permissions  rwrr 
24584  1 
(* Title: HOL/Tools/Qelim/cooper.ML 
23466  2 
Author: Amine Chaieb, TU Muenchen 
36802  3 

4 
Presburger arithmetic by Cooper's algorithm. 

23466  5 
*) 
6 

36799  7 
signature COOPER = 
36798  8 
sig 
9 
type entry 

10 
val get: Proof.context > entry 

11 
val del: term list > attribute 

12 
val add: term list > attribute 

37117
59cee8807c29
eliminated various catchall exception patterns, guessing at the concrete exeptions that are intended here;
wenzelm
parents:
36945
diff
changeset

13 
exception COOPER of string 
36804  14 
val conv: Proof.context > conv 
15 
val tac: bool > thm list > thm list > Proof.context > int > tactic 

16 
val method: (Proof.context > Method.method) context_parser 

36798  17 
val setup: theory > theory 
23466  18 
end; 
19 

36799  20 
structure Cooper: COOPER = 
36798  21 
struct 
22 

36799  23 
type entry = simpset * term list; 
36798  24 

25 
val allowed_consts = 

26 
[@{term "op + :: int => _"}, @{term "op + :: nat => _"}, 

27 
@{term "op  :: int => _"}, @{term "op  :: nat => _"}, 

28 
@{term "op * :: int => _"}, @{term "op * :: nat => _"}, 

29 
@{term "op div :: int => _"}, @{term "op div :: nat => _"}, 

30 
@{term "op mod :: int => _"}, @{term "op mod :: nat => _"}, 

38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

31 
@{term HOL.conj}, @{term HOL.disj}, @{term HOL.implies}, 
36798  32 
@{term "op = :: int => _"}, @{term "op = :: nat => _"}, @{term "op = :: bool => _"}, 
33 
@{term "op < :: int => _"}, @{term "op < :: nat => _"}, 

34 
@{term "op <= :: int => _"}, @{term "op <= :: nat => _"}, 

35 
@{term "op dvd :: int => _"}, @{term "op dvd :: nat => _"}, 

36 
@{term "abs :: int => _"}, 

37 
@{term "max :: int => _"}, @{term "max :: nat => _"}, 

38 
@{term "min :: int => _"}, @{term "min :: nat => _"}, 

39 
@{term "uminus :: int => _"}, (*@ {term "uminus :: nat => _"},*) 

37388  40 
@{term "Not"}, @{term Suc}, 
36798  41 
@{term "Ex :: (int => _) => _"}, @{term "Ex :: (nat => _) => _"}, 
42 
@{term "All :: (int => _) => _"}, @{term "All :: (nat => _) => _"}, 

43 
@{term "nat"}, @{term "int"}, 

44 
@{term "Int.Bit0"}, @{term "Int.Bit1"}, 

45 
@{term "Int.Pls"}, @{term "Int.Min"}, 

46 
@{term "Int.number_of :: int => int"}, @{term "Int.number_of :: int => nat"}, 

47 
@{term "0::int"}, @{term "1::int"}, @{term "0::nat"}, @{term "1::nat"}, 

48 
@{term "True"}, @{term "False"}]; 

49 

50 
structure Data = Generic_Data 

51 
( 

52 
type T = simpset * term list; 

53 
val empty = (HOL_ss, allowed_consts); 

54 
val extend = I; 

55 
fun merge ((ss1, ts1), (ss2, ts2)) = 

56 
(merge_ss (ss1, ss2), Library.merge (op aconv) (ts1, ts2)); 

57 
); 

58 

59 
val get = Data.get o Context.Proof; 

60 

61 
fun add ts = Thm.declaration_attribute (fn th => fn context => 

62 
context > Data.map (fn (ss,ts') => 

63 
(ss addsimps [th], merge (op aconv) (ts',ts) ))) 

64 

65 
fun del ts = Thm.declaration_attribute (fn th => fn context => 

66 
context > Data.map (fn (ss,ts') => 

67 
(ss delsimps [th], subtract (op aconv) ts' ts ))) 

68 

27018  69 
fun simp_thms_conv ctxt = 
35410  70 
Simplifier.rewrite (Simplifier.context ctxt HOL_basic_ss addsimps @{thms simp_thms}); 
23484  71 
val FWD = Drule.implies_elim_list; 
23466  72 

73 
val true_tm = @{cterm "True"}; 

74 
val false_tm = @{cterm "False"}; 

75 
val zdvd1_eq = @{thm "zdvd1_eq"}; 

76 
val presburger_ss = @{simpset} addsimps [zdvd1_eq]; 

30595
c87a3350f5a9
proper spacing before ML antiquotations  note that @ may be part of symbolic ML identifiers;
wenzelm
parents:
30448
diff
changeset

77 
val lin_ss = presburger_ss addsimps (@{thm dvd_eq_mod_eq_0} :: zdvd1_eq :: @{thms zadd_ac}); 
23689
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23582
diff
changeset

78 

23466  79 
val iT = HOLogic.intT 
80 
val bT = HOLogic.boolT; 

36831
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset

81 
val dest_number = HOLogic.dest_number #> snd; 
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset

82 
val perhaps_number = try dest_number; 
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset

83 
val is_number = can dest_number; 
23466  84 

32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

85 
val [miconj, midisj, mieq, mineq, milt, mile, migt, mige, midvd, mindvd, miP] = 
23466  86 
map(instantiate' [SOME @{ctyp "int"}] []) @{thms "minf"}; 
87 

32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

88 
val [infDconj, infDdisj, infDdvd,infDndvd,infDP] = 
23466  89 
map(instantiate' [SOME @{ctyp "int"}] []) @{thms "inf_period"}; 
90 

32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

91 
val [piconj, pidisj, pieq,pineq,pilt,pile,pigt,pige,pidvd,pindvd,piP] = 
23466  92 
map (instantiate' [SOME @{ctyp "int"}] []) @{thms "pinf"}; 
93 

94 
val [miP, piP] = map (instantiate' [SOME @{ctyp "bool"}] []) [miP, piP]; 

95 

96 
val infDP = instantiate' (map SOME [@{ctyp "int"}, @{ctyp "bool"}]) [] infDP; 

97 

32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

98 
val [[asetconj, asetdisj, aseteq, asetneq, asetlt, asetle, 
23466  99 
asetgt, asetge, asetdvd, asetndvd,asetP], 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

100 
[bsetconj, bsetdisj, bseteq, bsetneq, bsetlt, bsetle, 
23466  101 
bsetgt, bsetge, bsetdvd, bsetndvd,bsetP]] = [@{thms "aset"}, @{thms "bset"}]; 
102 

36797
cb074cec7a30
dropped unused bindings; avoid open (documents dependency on generated code more explicitly)
haftmann
parents:
36717
diff
changeset

103 
val [cpmi, cppi] = [@{thm "cpmi"}, @{thm "cppi"}]; 
23466  104 

105 
val unity_coeff_ex = instantiate' [SOME @{ctyp "int"}] [] @{thm "unity_coeff_ex"}; 

106 

32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

107 
val [zdvd_mono,simp_from_to,all_not_ex] = 
23466  108 
[@{thm "zdvd_mono"}, @{thm "simp_from_to"}, @{thm "all_not_ex"}]; 
109 

110 
val [dvd_uminus, dvd_uminus'] = @{thms "uminus_dvd_conv"}; 

111 

112 
val eval_ss = presburger_ss addsimps [simp_from_to] delsimps [insert_iff,bex_triv]; 

113 
val eval_conv = Simplifier.rewrite eval_ss; 

114 

23689
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23582
diff
changeset

115 
(* recognising cterm without moving to terms *) 
23466  116 

32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

117 
datatype fm = And of cterm*cterm Or of cterm*cterm Eq of cterm  NEq of cterm 
23466  118 
 Lt of cterm  Le of cterm  Gt of cterm  Ge of cterm 
119 
 Dvd of cterm*cterm  NDvd of cterm*cterm  Nox 

120 

32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

121 
fun whatis x ct = 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

122 
( case (term_of ct) of 
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

123 
Const(@{const_name HOL.conj},_)$_$_ => And (Thm.dest_binop ct) 
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

124 
 Const (@{const_name HOL.disj},_)$_$_ => Or (Thm.dest_binop ct) 
38549
d0385f2764d8
use antiquotations for remaining unqualified constants in HOL
haftmann
parents:
37388
diff
changeset

125 
 Const (@{const_name "op ="},_)$y$_ => if term_of x aconv y then Eq (Thm.dest_arg ct) else Nox 
d0385f2764d8
use antiquotations for remaining unqualified constants in HOL
haftmann
parents:
37388
diff
changeset

126 
 Const (@{const_name Not},_) $ (Const (@{const_name "op ="},_)$y$_) => 
23466  127 
if term_of x aconv y then NEq (funpow 2 Thm.dest_arg ct) else Nox 
35092
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

128 
 Const (@{const_name Orderings.less}, _) $ y$ z => 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

129 
if term_of x aconv y then Lt (Thm.dest_arg ct) 
23466  130 
else if term_of x aconv z then Gt (Thm.dest_arg1 ct) else Nox 
35092
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

131 
 Const (@{const_name Orderings.less_eq}, _) $ y $ z => 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

132 
if term_of x aconv y then Le (Thm.dest_arg ct) 
23466  133 
else if term_of x aconv z then Ge (Thm.dest_arg1 ct) else Nox 
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset

134 
 Const (@{const_name Rings.dvd},_)$_$(Const(@{const_name Groups.plus},_)$y$_) => 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

135 
if term_of x aconv y then Dvd (Thm.dest_binop ct > Thm.dest_arg) else Nox 
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset

136 
 Const (@{const_name Not},_) $ (Const (@{const_name Rings.dvd},_)$_$(Const(@{const_name Groups.plus},_)$y$_)) => 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

137 
if term_of x aconv y then 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

138 
NDvd (Thm.dest_binop (Thm.dest_arg ct) > Thm.dest_arg) else Nox 
23466  139 
 _ => Nox) 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

140 
handle CTERM _ => Nox; 
23466  141 

32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

142 
fun get_pmi_term t = 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

143 
let val (x,eq) = 
23466  144 
(Thm.dest_abs NONE o Thm.dest_arg o snd o Thm.dest_abs NONE o Thm.dest_arg) 
145 
(Thm.dest_arg t) 

146 
in (Thm.cabs x o Thm.dest_arg o Thm.dest_arg) eq end; 

147 

148 
val get_pmi = get_pmi_term o cprop_of; 

149 

32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

150 
val p_v' = @{cpat "?P' :: int => bool"}; 
23466  151 
val q_v' = @{cpat "?Q' :: int => bool"}; 
152 
val p_v = @{cpat "?P:: int => bool"}; 

153 
val q_v = @{cpat "?Q:: int => bool"}; 

154 

32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

155 
fun myfwd (th1, th2, th3) p q 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

156 
[(th_1,th_2,th_3), (th_1',th_2',th_3')] = 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

157 
let 
23466  158 
val (mp', mq') = (get_pmi th_1, get_pmi th_1') 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

159 
val mi_th = FWD (instantiate ([],[(p_v,p),(q_v,q), (p_v',mp'),(q_v',mq')]) th1) 
23466  160 
[th_1, th_1'] 
161 
val infD_th = FWD (instantiate ([],[(p_v,mp'), (q_v, mq')]) th3) [th_3,th_3'] 

162 
val set_th = FWD (instantiate ([],[(p_v,p), (q_v,q)]) th2) [th_2, th_2'] 

163 
in (mi_th, set_th, infD_th) 

164 
end; 

165 

166 
val inst' = fn cts => instantiate' [] (map SOME cts); 

167 
val infDTrue = instantiate' [] [SOME true_tm] infDP; 

168 
val infDFalse = instantiate' [] [SOME false_tm] infDP; 

169 

170 
val cadd = @{cterm "op + :: int => _"} 

171 
val cmulC = @{cterm "op * :: int => _"} 

172 
val cminus = @{cterm "op  :: int => _"} 

23689
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23582
diff
changeset

173 
val cone = @{cterm "1 :: int"} 
36797
cb074cec7a30
dropped unused bindings; avoid open (documents dependency on generated code more explicitly)
haftmann
parents:
36717
diff
changeset

174 
val [addC, mulC, subC] = map term_of [cadd, cmulC, cminus] 
23689
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23582
diff
changeset

175 
val [zero, one] = [@{term "0 :: int"}, @{term "1 :: int"}]; 
23466  176 

36831
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset

177 
fun numeral1 f n = HOLogic.mk_number iT (f (dest_number n)); 
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset

178 
fun numeral2 f m n = HOLogic.mk_number iT (f (dest_number m) (dest_number n)); 
23466  179 

32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

180 
val [minus1,plus1] = 
23466  181 
map (fn c => fn t => Thm.capply (Thm.capply c t) cone) [cminus,cadd]; 
182 

32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

183 
fun decomp_pinf x dvd inS [aseteq, asetneq, asetlt, asetle, 
23466  184 
asetgt, asetge,asetdvd,asetndvd,asetP, 
185 
infDdvd, infDndvd, asetconj, 

186 
asetdisj, infDconj, infDdisj] cp = 

187 
case (whatis x cp) of 

188 
And (p,q) => ([p,q], myfwd (piconj, asetconj, infDconj) (Thm.cabs x p) (Thm.cabs x q)) 

189 
 Or (p,q) => ([p,q], myfwd (pidisj, asetdisj, infDdisj) (Thm.cabs x p) (Thm.cabs x q)) 

190 
 Eq t => ([], K (inst' [t] pieq, FWD (inst' [t] aseteq) [inS (plus1 t)], infDFalse)) 

191 
 NEq t => ([], K (inst' [t] pineq, FWD (inst' [t] asetneq) [inS t], infDTrue)) 

192 
 Lt t => ([], K (inst' [t] pilt, FWD (inst' [t] asetlt) [inS t], infDFalse)) 

193 
 Le t => ([], K (inst' [t] pile, FWD (inst' [t] asetle) [inS (plus1 t)], infDFalse)) 

194 
 Gt t => ([], K (inst' [t] pigt, (inst' [t] asetgt), infDTrue)) 

195 
 Ge t => ([], K (inst' [t] pige, (inst' [t] asetge), infDTrue)) 

32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

196 
 Dvd (d,s) => 
23466  197 
([],let val dd = dvd d 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

198 
in K (inst' [d,s] pidvd, FWD (inst' [d,s] asetdvd) [dd],FWD (inst' [d,s] infDdvd) [dd]) end) 
23466  199 
 NDvd(d,s) => ([],let val dd = dvd d 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

200 
in K (inst' [d,s] pindvd, FWD (inst' [d,s] asetndvd) [dd], FWD (inst' [d,s] infDndvd) [dd]) end) 
23466  201 
 _ => ([], K (inst' [cp] piP, inst' [cp] asetP, inst' [cp] infDP)); 
202 

203 
fun decomp_minf x dvd inS [bseteq,bsetneq,bsetlt, bsetle, bsetgt, 

204 
bsetge,bsetdvd,bsetndvd,bsetP, 

205 
infDdvd, infDndvd, bsetconj, 

206 
bsetdisj, infDconj, infDdisj] cp = 

207 
case (whatis x cp) of 

208 
And (p,q) => ([p,q], myfwd (miconj, bsetconj, infDconj) (Thm.cabs x p) (Thm.cabs x q)) 

209 
 Or (p,q) => ([p,q], myfwd (midisj, bsetdisj, infDdisj) (Thm.cabs x p) (Thm.cabs x q)) 

210 
 Eq t => ([], K (inst' [t] mieq, FWD (inst' [t] bseteq) [inS (minus1 t)], infDFalse)) 

211 
 NEq t => ([], K (inst' [t] mineq, FWD (inst' [t] bsetneq) [inS t], infDTrue)) 

212 
 Lt t => ([], K (inst' [t] milt, (inst' [t] bsetlt), infDTrue)) 

213 
 Le t => ([], K (inst' [t] mile, (inst' [t] bsetle), infDTrue)) 

214 
 Gt t => ([], K (inst' [t] migt, FWD (inst' [t] bsetgt) [inS t], infDFalse)) 

215 
 Ge t => ([], K (inst' [t] mige,FWD (inst' [t] bsetge) [inS (minus1 t)], infDFalse)) 

216 
 Dvd (d,s) => ([],let val dd = dvd d 

32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

217 
in K (inst' [d,s] midvd, FWD (inst' [d,s] bsetdvd) [dd] , FWD (inst' [d,s] infDdvd) [dd]) end) 
23466  218 
 NDvd (d,s) => ([],let val dd = dvd d 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

219 
in K (inst' [d,s] mindvd, FWD (inst' [d,s] bsetndvd) [dd], FWD (inst' [d,s] infDndvd) [dd]) end) 
23466  220 
 _ => ([], K (inst' [cp] miP, inst' [cp] bsetP, inst' [cp] infDP)) 
221 

222 
(* Canonical linear form for terms, formulae etc.. *) 

32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

223 
fun provelin ctxt t = Goal.prove ctxt [] [] t 
31101
26c7bb764a38
qualified names for Lin_Arith tactics and simprocs
haftmann
parents:
30686
diff
changeset

224 
(fn _ => EVERY [simp_tac lin_ss 1, TRY (Lin_Arith.tac ctxt 1)]); 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

225 
fun linear_cmul 0 tm = zero 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

226 
 linear_cmul n tm = case tm of 
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset

227 
Const (@{const_name Groups.plus}, _) $ a $ b => addC $ linear_cmul n a $ linear_cmul n b 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset

228 
 Const (@{const_name Groups.times}, _) $ c $ x => mulC $ numeral1 (fn m => n * m) c $ x 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset

229 
 Const (@{const_name Groups.minus}, _) $ a $ b => subC $ linear_cmul n a $ linear_cmul n b 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset

230 
 (m as Const (@{const_name Groups.uminus}, _)) $ a => m $ linear_cmul n a 
25768  231 
 _ => numeral1 (fn m => n * m) tm; 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

232 
fun earlier [] x y = false 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

233 
 earlier (h::t) x y = 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

234 
if h aconv y then false else if h aconv x then true else earlier t x y; 
23466  235 

32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

236 
fun linear_add vars tm1 tm2 = case (tm1, tm2) of 
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset

237 
(Const (@{const_name Groups.plus}, _) $ (Const (@{const_name Groups.times}, _) $ c1 $ x1) $ r1, 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset

238 
Const (@{const_name Groups.plus}, _) $ (Const (@{const_name Groups.times}, _) $ c2 $ x2) $ r2) => 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

239 
if x1 = x2 then 
33002  240 
let val c = numeral2 Integer.add c1 c2 
25768  241 
in if c = zero then linear_add vars r1 r2 
242 
else addC$(mulC$c$x1)$(linear_add vars r1 r2) 

32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

243 
end 
25768  244 
else if earlier vars x1 x2 then addC $ (mulC $ c1 $ x1) $ linear_add vars r1 tm2 
245 
else addC $ (mulC $ c2 $ x2) $ linear_add vars tm1 r2 

35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset

246 
 (Const (@{const_name Groups.plus}, _) $ (Const (@{const_name Groups.times}, _) $ c1 $ x1) $ r1, _) => 
25768  247 
addC $ (mulC $ c1 $ x1) $ linear_add vars r1 tm2 
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset

248 
 (_, Const (@{const_name Groups.plus}, _) $ (Const (@{const_name Groups.times}, _) $ c2 $ x2) $ r2) => 
25768  249 
addC $ (mulC $ c2 $ x2) $ linear_add vars tm1 r2 
33002  250 
 (_, _) => numeral2 Integer.add tm1 tm2; 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

251 

54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

252 
fun linear_neg tm = linear_cmul ~1 tm; 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

253 
fun linear_sub vars tm1 tm2 = linear_add vars tm1 (linear_neg tm2); 
23466  254 

36806  255 
exception COOPER of string; 
23466  256 

36831
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset

257 
fun lint vars tm = if is_number tm then tm else case tm of 
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset

258 
Const (@{const_name Groups.uminus}, _) $ t => linear_neg (lint vars t) 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset

259 
 Const (@{const_name Groups.plus}, _) $ s $ t => linear_add vars (lint vars s) (lint vars t) 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset

260 
 Const (@{const_name Groups.minus}, _) $ s $ t => linear_sub vars (lint vars s) (lint vars t) 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset

261 
 Const (@{const_name Groups.times}, _) $ s $ t => 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

262 
let val s' = lint vars s 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

263 
val t' = lint vars t 
36831
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset

264 
in case perhaps_number s' of SOME n => linear_cmul n t' 
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset

265 
 NONE => (case perhaps_number t' of SOME n => linear_cmul n s' 
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset

266 
 NONE => raise COOPER "lint: not linear") 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

267 
end 
25768  268 
 _ => addC $ (mulC $ one $ tm) $ zero; 
23466  269 

35092
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

270 
fun lin (vs as x::_) (Const (@{const_name Not}, _) $ (Const (@{const_name Orderings.less}, T) $ s $ t)) = 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

271 
lin vs (Const (@{const_name Orderings.less_eq}, T) $ t $ s) 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

272 
 lin (vs as x::_) (Const (@{const_name Not},_) $ (Const(@{const_name Orderings.less_eq}, T) $ s $ t)) = 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

273 
lin vs (Const (@{const_name Orderings.less}, T) $ t $ s) 
25768  274 
 lin vs (Const (@{const_name Not},T)$t) = Const (@{const_name Not},T)$ (lin vs t) 
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
34974
diff
changeset

275 
 lin (vs as x::_) (Const(@{const_name Rings.dvd},_)$d$t) = 
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
34974
diff
changeset

276 
HOLogic.mk_binrel @{const_name Rings.dvd} (numeral1 abs d, lint vs t) 
38549
d0385f2764d8
use antiquotations for remaining unqualified constants in HOL
haftmann
parents:
37388
diff
changeset

277 
 lin (vs as x::_) ((b as Const(@{const_name "op ="},_))$s$t) = 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

278 
(case lint vs (subC$t$s) of 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

279 
(t as a$(m$c$y)$r) => 
23466  280 
if x <> y then b$zero$t 
36831
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset

281 
else if dest_number c < 0 then b$(m$(numeral1 ~ c)$y)$r 
23466  282 
else b$(m$c$y)$(linear_neg r) 
283 
 t => b$zero$t) 

32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

284 
 lin (vs as x::_) (b$s$t) = 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

285 
(case lint vs (subC$t$s) of 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

286 
(t as a$(m$c$y)$r) => 
23466  287 
if x <> y then b$zero$t 
36831
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset

288 
else if dest_number c < 0 then b$(m$(numeral1 ~ c)$y)$r 
23466  289 
else b$(linear_neg r)$(m$c$y) 
290 
 t => b$zero$t) 

291 
 lin vs fm = fm; 

292 

32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

293 
fun lint_conv ctxt vs ct = 
23466  294 
let val t = term_of ct 
295 
in (provelin ctxt ((HOLogic.eq_const iT)$t$(lint vs t) > HOLogic.mk_Trueprop)) 

296 
RS eq_reflection 

297 
end; 

298 

32398  299 
fun is_intrel_type T = T = @{typ "int => int => bool"}; 
300 

301 
fun is_intrel (b$_$_) = is_intrel_type (fastype_of b) 

302 
 is_intrel (@{term "Not"}$(b$_$_)) = is_intrel_type (fastype_of b) 

23466  303 
 is_intrel _ = false; 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

304 

25768  305 
fun linearize_conv ctxt vs ct = case term_of ct of 
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
34974
diff
changeset

306 
Const(@{const_name Rings.dvd},_)$d$t => 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

307 
let 
36797
cb074cec7a30
dropped unused bindings; avoid open (documents dependency on generated code more explicitly)
haftmann
parents:
36717
diff
changeset

308 
val th = Conv.binop_conv (lint_conv ctxt vs) ct 
23466  309 
val (d',t') = Thm.dest_binop (Thm.rhs_of th) 
310 
val (dt',tt') = (term_of d', term_of t') 

36831
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset

311 
in if is_number dt' andalso is_number tt' 
36797
cb074cec7a30
dropped unused bindings; avoid open (documents dependency on generated code more explicitly)
haftmann
parents:
36717
diff
changeset

312 
then Conv.fconv_rule (Conv.arg_conv (Simplifier.rewrite presburger_ss)) th 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

313 
else 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

314 
let 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

315 
val dth = 
36831
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset

316 
((if dest_number (term_of d') < 0 then 
36797
cb074cec7a30
dropped unused bindings; avoid open (documents dependency on generated code more explicitly)
haftmann
parents:
36717
diff
changeset

317 
Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv (lint_conv ctxt vs))) 
23466  318 
(Thm.transitive th (inst' [d',t'] dvd_uminus)) 
319 
else th) handle TERM _ => th) 

320 
val d'' = Thm.rhs_of dth > Thm.dest_arg1 

321 
in 

32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

322 
case tt' of 
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset

323 
Const(@{const_name Groups.plus},_)$(Const(@{const_name Groups.times},_)$c$_)$_ => 
36831
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset

324 
let val x = dest_number c 
36797
cb074cec7a30
dropped unused bindings; avoid open (documents dependency on generated code more explicitly)
haftmann
parents:
36717
diff
changeset

325 
in if x < 0 then Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv (lint_conv ctxt vs))) 
23466  326 
(Thm.transitive dth (inst' [d'',t'] dvd_uminus')) 
327 
else dth end 

328 
 _ => dth 

329 
end 

330 
end 

36797
cb074cec7a30
dropped unused bindings; avoid open (documents dependency on generated code more explicitly)
haftmann
parents:
36717
diff
changeset

331 
 Const (@{const_name Not},_)$(Const(@{const_name Rings.dvd},_)$_$_) => Conv.arg_conv (linearize_conv ctxt vs) ct 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

332 
 t => if is_intrel t 
23466  333 
then (provelin ctxt ((HOLogic.eq_const bT)$t$(lin vs t) > HOLogic.mk_Trueprop)) 
334 
RS eq_reflection 

36945  335 
else Thm.reflexive ct; 
23466  336 

337 
val dvdc = @{cterm "op dvd :: int => _"}; 

338 

32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

339 
fun unify ctxt q = 
23466  340 
let 
341 
val (e,(cx,p)) = q > Thm.dest_comb > Thm.dest_abs NONE 

32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

342 
val x = term_of cx 
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset

343 
val ins = insert (op = : int * int > bool) 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

344 
fun h (acc,dacc) t = 
23466  345 
case (term_of t) of 
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset

346 
Const(s,_)$(Const(@{const_name Groups.times},_)$c$y)$ _ => 
23881  347 
if x aconv y andalso member (op =) 
35092
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

348 
["op =", @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s 
36831
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset

349 
then (ins (dest_number c) acc,dacc) else (acc,dacc) 
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset

350 
 Const(s,_)$_$(Const(@{const_name Groups.times},_)$c$y) => 
23881  351 
if x aconv y andalso member (op =) 
35092
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

352 
[@{const_name Orderings.less}, @{const_name Orderings.less_eq}] s 
36831
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset

353 
then (ins (dest_number c) acc, dacc) else (acc,dacc) 
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset

354 
 Const(@{const_name Rings.dvd},_)$_$(Const(@{const_name Groups.plus},_)$(Const(@{const_name Groups.times},_)$c$y)$_) => 
36831
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset

355 
if x aconv y then (acc,ins (dest_number c) dacc) else (acc,dacc) 
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

356 
 Const(@{const_name HOL.conj},_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t) 
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

357 
 Const(@{const_name HOL.disj},_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t) 
25768  358 
 Const (@{const_name Not},_)$_ => h (acc,dacc) (Thm.dest_arg t) 
23466  359 
 _ => (acc, dacc) 
360 
val (cs,ds) = h ([],[]) p 

33042  361 
val l = Integer.lcms (union (op =) cs ds) 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

362 
fun cv k ct = 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

363 
let val (tm as b$s$t) = term_of ct 
23466  364 
in ((HOLogic.eq_const bT)$tm$(b$(linear_cmul k s)$(linear_cmul k t)) 
365 
> HOLogic.mk_Trueprop > provelin ctxt) RS eq_reflection end 

32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

366 
fun nzprop x = 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

367 
let 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

368 
val th = 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

369 
Simplifier.rewrite lin_ss 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

370 
(Thm.capply @{cterm Trueprop} (Thm.capply @{cterm "Not"} 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

371 
(Thm.capply (Thm.capply @{cterm "op = :: int => _"} (Numeral.mk_cnumber @{ctyp "int"} x)) 
23689
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23582
diff
changeset

372 
@{cterm "0::int"}))) 
36945  373 
in Thm.equal_elim (Thm.symmetric th) TrueI end; 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

374 
val notz = 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

375 
let val tab = fold Inttab.update 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

376 
(ds ~~ (map (fn x => nzprop (l div x)) ds)) Inttab.empty 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

377 
in 
36831
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset

378 
fn ct => the (Inttab.lookup tab (ct > term_of > dest_number)) 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

379 
handle Option => 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

380 
(writeln ("noz: TheoremsTable contains no entry for " ^ 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

381 
Syntax.string_of_term ctxt (Thm.term_of ct)); raise Option) 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

382 
end 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

383 
fun unit_conv t = 
23466  384 
case (term_of t) of 
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

385 
Const(@{const_name HOL.conj},_)$_$_ => Conv.binop_conv unit_conv t 
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

386 
 Const(@{const_name HOL.disj},_)$_$_ => Conv.binop_conv unit_conv t 
36797
cb074cec7a30
dropped unused bindings; avoid open (documents dependency on generated code more explicitly)
haftmann
parents:
36717
diff
changeset

387 
 Const (@{const_name Not},_)$_ => Conv.arg_conv unit_conv t 
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset

388 
 Const(s,_)$(Const(@{const_name Groups.times},_)$c$y)$ _ => 
23881  389 
if x=y andalso member (op =) 
35092
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

390 
["op =", @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s 
36831
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset

391 
then cv (l div dest_number c) t else Thm.reflexive t 
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset

392 
 Const(s,_)$_$(Const(@{const_name Groups.times},_)$c$y) => 
23881  393 
if x=y andalso member (op =) 
35092
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

394 
[@{const_name Orderings.less}, @{const_name Orderings.less_eq}] s 
36831
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset

395 
then cv (l div dest_number c) t else Thm.reflexive t 
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset

396 
 Const(@{const_name Rings.dvd},_)$d$(r as (Const(@{const_name Groups.plus},_)$(Const(@{const_name Groups.times},_)$c$y)$_)) => 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

397 
if x=y then 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

398 
let 
36831
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset

399 
val k = l div dest_number c 
23466  400 
val kt = HOLogic.mk_number iT k 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

401 
val th1 = inst' [Thm.dest_arg1 t, Thm.dest_arg t] 
23466  402 
((Thm.dest_arg t > funpow 2 Thm.dest_arg1 > notz) RS zdvd_mono) 
403 
val (d',t') = (mulC$kt$d, mulC$kt$r) 

404 
val thc = (provelin ctxt ((HOLogic.eq_const iT)$d'$(lint [] d') > HOLogic.mk_Trueprop)) 

405 
RS eq_reflection 

406 
val tht = (provelin ctxt ((HOLogic.eq_const iT)$t'$(linear_cmul k r) > HOLogic.mk_Trueprop)) 

407 
RS eq_reflection 

32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

408 
in Thm.transitive th1 (Thm.combination (Drule.arg_cong_rule dvdc thc) tht) end 
23466  409 
else Thm.reflexive t 
410 
 _ => Thm.reflexive t 

411 
val uth = unit_conv p 

23689
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23582
diff
changeset

412 
val clt = Numeral.mk_cnumber @{ctyp "int"} l 
23466  413 
val ltx = Thm.capply (Thm.capply cmulC clt) cx 
414 
val th = Drule.arg_cong_rule e (Thm.abstract_rule (fst (dest_Free x )) cx uth) 

415 
val th' = inst' [Thm.cabs ltx (Thm.rhs_of uth), clt] unity_coeff_ex 

36945  416 
val thf = Thm.transitive th 
417 
(Thm.transitive (Thm.symmetric (Thm.beta_conversion true (cprop_of th' > Thm.dest_arg1))) th') 

23466  418 
val (lth,rth) = Thm.dest_comb (cprop_of thf) >> Thm.dest_arg >> Thm.beta_conversion true 
36945  419 
> Thm.beta_conversion true >> Thm.symmetric 
420 
in Thm.transitive (Thm.transitive lth thf) rth end; 

23466  421 

422 

423 
val emptyIS = @{cterm "{}::int set"}; 

424 
val insert_tm = @{cterm "insert :: int => _"}; 

425 
fun mkISet cts = fold_rev (Thm.capply insert_tm #> Thm.capply) cts emptyIS; 

426 
val eqelem_imp_imp = (thm"eqelem_imp_iff") RS iffD1; 

32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

427 
val [A_tm,B_tm] = map (fn th => cprop_of th > funpow 2 Thm.dest_arg > Thm.dest_abs NONE > snd > Thm.dest_arg1 > Thm.dest_arg 
23466  428 
> Thm.dest_abs NONE > snd > Thm.dest_fun > Thm.dest_arg) 
429 
[asetP,bsetP]; 

430 

431 
val D_tm = @{cpat "?D::int"}; 

432 

32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

433 
fun cooperex_conv ctxt vs q = 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

434 
let 
23466  435 

436 
val uth = unify ctxt q 

437 
val (x,p) = Thm.dest_abs NONE (Thm.dest_arg (Thm.rhs_of uth)) 

438 
val ins = insert (op aconvc) 

32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

439 
fun h t (bacc,aacc,dacc) = 
23466  440 
case (whatis x t) of 
441 
And (p,q) => h q (h p (bacc,aacc,dacc)) 

442 
 Or (p,q) => h q (h p (bacc,aacc,dacc)) 

32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

443 
 Eq t => (ins (minus1 t) bacc, 
23466  444 
ins (plus1 t) aacc,dacc) 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

445 
 NEq t => (ins t bacc, 
23466  446 
ins t aacc, dacc) 
447 
 Lt t => (bacc, ins t aacc, dacc) 

448 
 Le t => (bacc, ins (plus1 t) aacc,dacc) 

449 
 Gt t => (ins t bacc, aacc,dacc) 

450 
 Ge t => (ins (minus1 t) bacc, aacc,dacc) 

36831
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset

451 
 Dvd (d,_) => (bacc,aacc,insert (op =) (term_of d > dest_number) dacc) 
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset

452 
 NDvd (d,_) => (bacc,aacc,insert (op =) (term_of d> dest_number) dacc) 
23466  453 
 _ => (bacc, aacc, dacc) 
454 
val (b0,a0,ds) = h p ([],[],[]) 

24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset

455 
val d = Integer.lcms ds 
23582  456 
val cd = Numeral.mk_cnumber @{ctyp "int"} d 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

457 
fun divprop x = 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

458 
let 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

459 
val th = 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

460 
Simplifier.rewrite lin_ss 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

461 
(Thm.capply @{cterm Trueprop} 
23582  462 
(Thm.capply (Thm.capply dvdc (Numeral.mk_cnumber @{ctyp "int"} x)) cd)) 
36945  463 
in Thm.equal_elim (Thm.symmetric th) TrueI end; 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

464 
val dvd = 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

465 
let val tab = fold Inttab.update (ds ~~ (map divprop ds)) Inttab.empty in 
36831
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset

466 
fn ct => the (Inttab.lookup tab (term_of ct > dest_number)) 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

467 
handle Option => 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

468 
(writeln ("dvd: TheoremsTable contains no entry for" ^ 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

469 
Syntax.string_of_term ctxt (Thm.term_of ct)); raise Option) 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

470 
end 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

471 
val dp = 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

472 
let val th = Simplifier.rewrite lin_ss 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

473 
(Thm.capply @{cterm Trueprop} 
23466  474 
(Thm.capply (Thm.capply @{cterm "op < :: int => _"} @{cterm "0::int"}) cd)) 
36945  475 
in Thm.equal_elim (Thm.symmetric th) TrueI end; 
23466  476 
(* A and B set *) 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

477 
local 
23466  478 
val insI1 = instantiate' [SOME @{ctyp "int"}] [] @{thm "insertI1"} 
479 
val insI2 = instantiate' [SOME @{ctyp "int"}] [] @{thm "insertI2"} 

480 
in 

32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

481 
fun provein x S = 
23466  482 
case term_of S of 
32264
0be31453f698
Set.UNIV and Set.empty are mere abbreviations for top and bot
haftmann
parents:
31101
diff
changeset

483 
Const(@{const_name Orderings.bot}, _) => error "Unexpected error in Cooper, please email Amine Chaieb" 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

484 
 Const(@{const_name insert}, _) $ y $ _ => 
23466  485 
let val (cy,S') = Thm.dest_binop S 
486 
in if term_of x aconv y then instantiate' [] [SOME x, SOME S'] insI1 

36945  487 
else Thm.implies_elim (instantiate' [] [SOME x, SOME S', SOME cy] insI2) 
23466  488 
(provein x S') 
489 
end 

490 
end 

32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

491 

23466  492 
val al = map (lint vs o term_of) a0 
493 
val bl = map (lint vs o term_of) b0 

32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

494 
val (sl,s0,f,abths,cpth) = 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

495 
if length (distinct (op aconv) bl) <= length (distinct (op aconv) al) 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

496 
then 
23466  497 
(bl,b0,decomp_minf, 
36945  498 
fn B => (map (fn th => Thm.implies_elim (Thm.instantiate ([],[(B_tm,B), (D_tm,cd)]) th) dp) 
23466  499 
[bseteq,bsetneq,bsetlt, bsetle, bsetgt,bsetge])@ 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

500 
(map (Thm.instantiate ([],[(B_tm,B), (D_tm,cd)])) 
23466  501 
[bsetdvd,bsetndvd,bsetP,infDdvd, infDndvd,bsetconj, 
502 
bsetdisj,infDconj, infDdisj]), 

32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

503 
cpmi) 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

504 
else (al,a0,decomp_pinf,fn A => 
36945  505 
(map (fn th => Thm.implies_elim (Thm.instantiate ([],[(A_tm,A), (D_tm,cd)]) th) dp) 
23466  506 
[aseteq,asetneq,asetlt, asetle, asetgt,asetge])@ 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

507 
(map (Thm.instantiate ([],[(A_tm,A), (D_tm,cd)])) 
23466  508 
[asetdvd,asetndvd, asetP, infDdvd, infDndvd,asetconj, 
509 
asetdisj,infDconj, infDdisj]),cppi) 

32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

510 
val cpth = 
23466  511 
let 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

512 
val sths = map (fn (tl,t0) => 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

513 
if tl = term_of t0 
23466  514 
then instantiate' [SOME @{ctyp "int"}] [SOME t0] refl 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

515 
else provelin ctxt ((HOLogic.eq_const iT)$tl$(term_of t0) 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

516 
> HOLogic.mk_Trueprop)) 
23466  517 
(sl ~~ s0) 
518 
val csl = distinct (op aconvc) (map (cprop_of #> Thm.dest_arg #> Thm.dest_arg1) sths) 

519 
val S = mkISet csl 

32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

520 
val inStab = fold (fn ct => fn tab => Termtab.update (term_of ct, provein ct S) tab) 
23466  521 
csl Termtab.empty 
522 
val eqelem_th = instantiate' [SOME @{ctyp "int"}] [NONE,NONE, SOME S] eqelem_imp_imp 

32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

523 
val inS = 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

524 
let 
23466  525 
val tab = fold Termtab.update 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

526 
(map (fn eq => 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

527 
let val (s,t) = cprop_of eq > Thm.dest_arg > Thm.dest_binop 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

528 
val th = if term_of s = term_of t 
33035  529 
then the (Termtab.lookup inStab (term_of s)) 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

530 
else FWD (instantiate' [] [SOME s, SOME t] eqelem_th) 
33035  531 
[eq, the (Termtab.lookup inStab (term_of s))] 
23466  532 
in (term_of t, th) end) 
533 
sths) Termtab.empty 

32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

534 
in 
33035  535 
fn ct => the (Termtab.lookup tab (term_of ct)) 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

536 
handle Option => 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

537 
(writeln ("inS: No theorem for " ^ Syntax.string_of_term ctxt (Thm.term_of ct)); 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

538 
raise Option) 
23466  539 
end 
540 
val (inf, nb, pd) = divide_and_conquer (f x dvd inS (abths S)) p 

541 
in [dp, inf, nb, pd] MRS cpth 

542 
end 

543 
val cpth' = Thm.transitive uth (cpth RS eq_reflection) 

27018  544 
in Thm.transitive cpth' ((simp_thms_conv ctxt then_conv eval_conv) (Thm.rhs_of cpth')) 
23466  545 
end; 
546 

32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

547 
fun literals_conv bops uops env cv = 
23466  548 
let fun h t = 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

549 
case (term_of t) of 
36797
cb074cec7a30
dropped unused bindings; avoid open (documents dependency on generated code more explicitly)
haftmann
parents:
36717
diff
changeset

550 
b$_$_ => if member (op aconv) bops b then Conv.binop_conv h t else cv env t 
cb074cec7a30
dropped unused bindings; avoid open (documents dependency on generated code more explicitly)
haftmann
parents:
36717
diff
changeset

551 
 u$_ => if member (op aconv) uops u then Conv.arg_conv h t else cv env t 
23466  552 
 _ => cv env t 
553 
in h end; 

554 

555 
fun integer_nnf_conv ctxt env = 

556 
nnf_conv then_conv literals_conv [HOLogic.conj, HOLogic.disj] [] env (linearize_conv ctxt); 

557 

36831
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset

558 
val conv_ss = HOL_basic_ss addsimps 
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset

559 
(@{thms simp_thms} @ take 4 @{thms ex_simps} @ [not_all, all_not_ex, @{thm ex_disj_distrib}]); 
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset

560 

3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset

561 
fun conv ctxt p = 
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset

562 
Qelim.gen_qelim_conv (Simplifier.rewrite conv_ss) (Simplifier.rewrite presburger_ss) (Simplifier.rewrite conv_ss) 
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset

563 
(cons o term_of) (OldTerm.term_frees (term_of p)) (linearize_conv ctxt) (integer_nnf_conv ctxt) 
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset

564 
(cooperex_conv ctxt) p 
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset

565 
handle CTERM s => raise COOPER "bad cterm" 
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset

566 
 THM s => raise COOPER "bad thm" 
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset

567 
 TYPE s => raise COOPER "bad type" 
23466  568 

36831
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset

569 
fun add_bools t = 
36807  570 
let 
36831
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset

571 
val ops = [@{term "op = :: int => _"}, @{term "op < :: int => _"}, @{term "op <= :: int => _"}, 
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

572 
@{term HOL.conj}, @{term HOL.disj}, @{term HOL.implies}, @{term "op = :: bool => _"}, 
36831
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset

573 
@{term "Not"}, @{term "All :: (int => _) => _"}, 
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset

574 
@{term "Ex :: (int => _) => _"}, @{term "True"}, @{term "False"}]; 
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset

575 
val is_op = member (op =) ops; 
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset

576 
val skip = not (fastype_of t = HOLogic.boolT) 
36807  577 
in case t of 
36831
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset

578 
(l as f $ a) $ b => if skip orelse is_op f then add_bools b o add_bools l 
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset

579 
else insert (op aconv) t 
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset

580 
 f $ a => if skip orelse is_op f then add_bools a o add_bools f 
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset

581 
else insert (op aconv) t 
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset

582 
 Abs p => add_bools (snd (variant_abs p)) 
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset

583 
 _ => if skip orelse is_op t then I else insert (op aconv) t 
36807  584 
end; 
585 

36832  586 
fun descend vs (abs as (_, xT, _)) = 
587 
let 

588 
val (xn', p') = variant_abs abs; 

36833
9628f969d843
represent deBruin indices simply by position in list
haftmann
parents:
36832
diff
changeset

589 
in ((xn', xT) :: vs, p') end; 
36832  590 

36831
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset

591 
local structure Proc = Cooper_Procedure in 
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset

592 

36833
9628f969d843
represent deBruin indices simply by position in list
haftmann
parents:
36832
diff
changeset

593 
fun num_of_term vs (Free vT) = Proc.Bound (find_index (fn vT' => vT' = vT) vs) 
36832  594 
 num_of_term vs (Term.Bound i) = Proc.Bound i 
595 
 num_of_term vs @{term "0::int"} = Proc.C 0 

596 
 num_of_term vs @{term "1::int"} = Proc.C 1 

597 
 num_of_term vs (t as Const (@{const_name number_of}, _) $ _) = 

598 
Proc.C (dest_number t) 

599 
 num_of_term vs (Const (@{const_name Groups.uminus}, _) $ t') = 

600 
Proc.Neg (num_of_term vs t') 

601 
 num_of_term vs (Const (@{const_name Groups.plus}, _) $ t1 $ t2) = 

602 
Proc.Add (num_of_term vs t1, num_of_term vs t2) 

603 
 num_of_term vs (Const (@{const_name Groups.minus}, _) $ t1 $ t2) = 

604 
Proc.Sub (num_of_term vs t1, num_of_term vs t2) 

605 
 num_of_term vs (Const (@{const_name Groups.times}, _) $ t1 $ t2) = 

606 
(case perhaps_number t1 

607 
of SOME n => Proc.Mul (n, num_of_term vs t2) 

608 
 NONE => (case perhaps_number t2 

609 
of SOME n => Proc.Mul (n, num_of_term vs t1) 

610 
 NONE => raise COOPER "reification: unsupported kind of multiplication")) 

611 
 num_of_term _ _ = raise COOPER "reification: bad term"; 

23689
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23582
diff
changeset

612 

36832  613 
fun fm_of_term ps vs (Const (@{const_name True}, _)) = Proc.T 
614 
 fm_of_term ps vs (Const (@{const_name False}, _)) = Proc.F 

38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

615 
 fm_of_term ps vs (Const (@{const_name HOL.conj}, _) $ t1 $ t2) = 
36832  616 
Proc.And (fm_of_term ps vs t1, fm_of_term ps vs t2) 
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

617 
 fm_of_term ps vs (Const (@{const_name HOL.disj}, _) $ t1 $ t2) = 
36832  618 
Proc.Or (fm_of_term ps vs t1, fm_of_term ps vs t2) 
38786
e46e7a9cb622
formerly unnamed infix impliciation now named HOL.implies
haftmann
parents:
38558
diff
changeset

619 
 fm_of_term ps vs (Const (@{const_name HOL.implies}, _) $ t1 $ t2) = 
36832  620 
Proc.Imp (fm_of_term ps vs t1, fm_of_term ps vs t2) 
621 
 fm_of_term ps vs (@{term "op = :: bool => _ "} $ t1 $ t2) = 

622 
Proc.Iff (fm_of_term ps vs t1, fm_of_term ps vs t2) 

623 
 fm_of_term ps vs (Const (@{const_name Not}, _) $ t') = 

624 
Proc.Not (fm_of_term ps vs t') 

38558  625 
 fm_of_term ps vs (Const (@{const_name Ex}, _) $ Abs abs) = 
36832  626 
Proc.E (uncurry (fm_of_term ps) (descend vs abs)) 
38558  627 
 fm_of_term ps vs (Const (@{const_name All}, _) $ Abs abs) = 
36832  628 
Proc.A (uncurry (fm_of_term ps) (descend vs abs)) 
629 
 fm_of_term ps vs (@{term "op = :: int => _"} $ t1 $ t2) = 

630 
Proc.Eq (Proc.Sub (num_of_term vs t1, num_of_term vs t2)) 

631 
 fm_of_term ps vs (Const (@{const_name Orderings.less_eq}, _) $ t1 $ t2) = 

632 
Proc.Le (Proc.Sub (num_of_term vs t1, num_of_term vs t2)) 

633 
 fm_of_term ps vs (Const (@{const_name Orderings.less}, _) $ t1 $ t2) = 

634 
Proc.Lt (Proc.Sub (num_of_term vs t1, num_of_term vs t2)) 

635 
 fm_of_term ps vs (Const (@{const_name Rings.dvd}, _) $ t1 $ t2) = 

636 
(case perhaps_number t1 

637 
of SOME n => Proc.Dvd (n, num_of_term vs t2) 

638 
 NONE => raise COOPER "reification: unsupported dvd") 

36833
9628f969d843
represent deBruin indices simply by position in list
haftmann
parents:
36832
diff
changeset

639 
 fm_of_term ps vs t = let val n = find_index (fn t' => t aconv t') ps 
9628f969d843
represent deBruin indices simply by position in list
haftmann
parents:
36832
diff
changeset

640 
in if n > 0 then Proc.Closed n else raise COOPER "reification: unknown term" end; 
23466  641 

36832  642 
fun term_of_num vs (Proc.C i) = HOLogic.mk_number HOLogic.intT i 
36833
9628f969d843
represent deBruin indices simply by position in list
haftmann
parents:
36832
diff
changeset

643 
 term_of_num vs (Proc.Bound n) = Free (nth vs n) 
36832  644 
 term_of_num vs (Proc.Neg t') = 
645 
@{term "uminus :: int => _"} $ term_of_num vs t' 

646 
 term_of_num vs (Proc.Add (t1, t2)) = 

647 
@{term "op + :: int => _"} $ term_of_num vs t1 $ term_of_num vs t2 

648 
 term_of_num vs (Proc.Sub (t1, t2)) = 

649 
@{term "op  :: int => _"} $ term_of_num vs t1 $ term_of_num vs t2 

650 
 term_of_num vs (Proc.Mul (i, t2)) = 

651 
@{term "op * :: int => _"} $ HOLogic.mk_number HOLogic.intT i $ term_of_num vs t2 

652 
 term_of_num vs (Proc.Cn (n, i, t')) = 

653 
term_of_num vs (Proc.Add (Proc.Mul (i, Proc.Bound n), t')); 

23466  654 

36832  655 
fun term_of_fm ps vs Proc.T = HOLogic.true_const 
656 
 term_of_fm ps vs Proc.F = HOLogic.false_const 

657 
 term_of_fm ps vs (Proc.And (t1, t2)) = HOLogic.conj $ term_of_fm ps vs t1 $ term_of_fm ps vs t2 

658 
 term_of_fm ps vs (Proc.Or (t1, t2)) = HOLogic.disj $ term_of_fm ps vs t1 $ term_of_fm ps vs t2 

659 
 term_of_fm ps vs (Proc.Imp (t1, t2)) = HOLogic.imp $ term_of_fm ps vs t1 $ term_of_fm ps vs t2 

660 
 term_of_fm ps vs (Proc.Iff (t1, t2)) = @{term "op = :: bool => _"} $ term_of_fm ps vs t1 $ term_of_fm ps vs t2 

661 
 term_of_fm ps vs (Proc.Not t') = HOLogic.Not $ term_of_fm ps vs t' 

662 
 term_of_fm ps vs (Proc.Eq t') = @{term "op = :: int => _ "} $ term_of_num vs t'$ @{term "0::int"} 

663 
 term_of_fm ps vs (Proc.NEq t') = term_of_fm ps vs (Proc.Not (Proc.Eq t')) 

664 
 term_of_fm ps vs (Proc.Lt t') = @{term "op < :: int => _ "} $ term_of_num vs t' $ @{term "0::int"} 

665 
 term_of_fm ps vs (Proc.Le t') = @{term "op <= :: int => _ "} $ term_of_num vs t' $ @{term "0::int"} 

666 
 term_of_fm ps vs (Proc.Gt t') = @{term "op < :: int => _ "} $ @{term "0::int"} $ term_of_num vs t' 

667 
 term_of_fm ps vs (Proc.Ge t') = @{term "op <= :: int => _ "} $ @{term "0::int"} $ term_of_num vs t' 

668 
 term_of_fm ps vs (Proc.Dvd (i, t')) = @{term "op dvd :: int => _ "} $ 

669 
HOLogic.mk_number HOLogic.intT i $ term_of_num vs t' 

670 
 term_of_fm ps vs (Proc.NDvd (i, t')) = term_of_fm ps vs (Proc.Not (Proc.Dvd (i, t'))) 

36833
9628f969d843
represent deBruin indices simply by position in list
haftmann
parents:
36832
diff
changeset

671 
 term_of_fm ps vs (Proc.Closed n) = nth ps n 
36832  672 
 term_of_fm ps vs (Proc.NClosed n) = term_of_fm ps vs (Proc.Not (Proc.Closed n)); 
23466  673 

36833
9628f969d843
represent deBruin indices simply by position in list
haftmann
parents:
36832
diff
changeset

674 
fun procedure t = 
23713  675 
let 
36833
9628f969d843
represent deBruin indices simply by position in list
haftmann
parents:
36832
diff
changeset

676 
val vs = Term.add_frees t []; 
9628f969d843
represent deBruin indices simply by position in list
haftmann
parents:
36832
diff
changeset

677 
val ps = add_bools t []; 
9628f969d843
represent deBruin indices simply by position in list
haftmann
parents:
36832
diff
changeset

678 
in (term_of_fm ps vs o Proc.pa o fm_of_term ps vs) t end; 
23466  679 

36831
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset

680 
end; 
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset

681 

38808  682 
val (_, oracle) = Context.>>> (Context.map_theory_result 
683 
(Thm.add_oracle (@{binding cooper}, 

684 
(fn (ctxt, t) => 

685 
(Thm.cterm_of (ProofContext.theory_of ctxt) o Logic.mk_equals o pairself HOLogic.mk_Trueprop) 

686 
(t, procedure t))))); 

36802  687 

688 
val comp_ss = HOL_ss addsimps @{thms semiring_norm}; 

689 

690 
fun strip_objimp ct = 

691 
(case Thm.term_of ct of 

38786
e46e7a9cb622
formerly unnamed infix impliciation now named HOL.implies
haftmann
parents:
38558
diff
changeset

692 
Const (@{const_name HOL.implies}, _) $ _ $ _ => 
36802  693 
let val (A, B) = Thm.dest_binop ct 
694 
in A :: strip_objimp B end 

695 
 _ => [ct]); 

696 

697 
fun strip_objall ct = 

698 
case term_of ct of 

38558  699 
Const (@{const_name All}, _) $ Abs (xn,xT,p) => 
36802  700 
let val (a,(v,t')) = (apsnd (Thm.dest_abs (SOME xn)) o Thm.dest_comb) ct 
701 
in apfst (cons (a,v)) (strip_objall t') 

702 
end 

703 
 _ => ([],ct); 

704 

705 
local 

706 
val all_maxscope_ss = 

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

708 
in 

709 
fun thin_prems_tac P = simp_tac all_maxscope_ss THEN' 

710 
CSUBGOAL (fn (p', i) => 

711 
let 

712 
val (qvs, p) = strip_objall (Thm.dest_arg p') 

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

714 
val qs = filter P ps 

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

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

38786
e46e7a9cb622
formerly unnamed infix impliciation now named HOL.implies
haftmann
parents:
38558
diff
changeset

717 
(fold_rev (fn p => fn q => Thm.capply (Thm.capply @{cterm HOL.implies} p) q) qs q) 
36802  718 
val g = Thm.capply (Thm.capply @{cterm "op ==>"} (Thm.capply @{cterm "Trueprop"} ng)) p' 
719 
val ntac = (case qs of [] => q aconvc @{cterm "False"} 

720 
 _ => false) 

721 
in 

722 
if ntac then no_tac 

723 
else rtac (Goal.prove_internal [] g (K (blast_tac HOL_cs 1))) i 

724 
end) 

23466  725 
end; 
36802  726 

727 
local 

728 
fun isnum t = case t of 

729 
Const(@{const_name Groups.zero},_) => true 

730 
 Const(@{const_name Groups.one},_) => true 

37388  731 
 @{term Suc}$s => isnum s 
36802  732 
 @{term "nat"}$s => isnum s 
733 
 @{term "int"}$s => isnum s 

734 
 Const(@{const_name Groups.uminus},_)$s => isnum s 

735 
 Const(@{const_name Groups.plus},_)$l$r => isnum l andalso isnum r 

736 
 Const(@{const_name Groups.times},_)$l$r => isnum l andalso isnum r 

737 
 Const(@{const_name Groups.minus},_)$l$r => isnum l andalso isnum r 

738 
 Const(@{const_name Power.power},_)$l$r => isnum l andalso isnum r 

739 
 Const(@{const_name Divides.mod},_)$l$r => isnum l andalso isnum r 

740 
 Const(@{const_name Divides.div},_)$l$r => isnum l andalso isnum r 

36831
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset

741 
 _ => is_number t orelse can HOLogic.dest_nat t 
36802  742 

743 
fun ty cts t = 

744 
if not (member (op =) [HOLogic.intT, HOLogic.natT, HOLogic.boolT] (typ_of (ctyp_of_term t))) then false 

745 
else case term_of t of 

746 
c$l$r => if member (op =) [@{term"op *::int => _"}, @{term"op *::nat => _"}] c 

747 
then not (isnum l orelse isnum r) 

748 
else not (member (op aconv) cts c) 

749 
 c$_ => not (member (op aconv) cts c) 

750 
 c => not (member (op aconv) cts c) 

751 

752 
val term_constants = 

753 
let fun h acc t = case t of 

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

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

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

757 
 _ => acc 

758 
in h [] end; 

759 
in 

760 
fun is_relevant ctxt ct = 

761 
subset (op aconv) (term_constants (term_of ct) , snd (get ctxt)) 

762 
andalso forall (fn Free (_,T) => member (op =) [@{typ int}, @{typ nat}] T) (OldTerm.term_frees (term_of ct)) 

763 
andalso forall (fn Var (_,T) => member (op =) [@{typ int}, @{typ nat}] T) (OldTerm.term_vars (term_of ct)); 

764 

765 
fun int_nat_terms ctxt ct = 

766 
let 

767 
val cts = snd (get ctxt) 

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

769 
case (term_of t) of 

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

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

772 
 _ => acc 

773 
in h [] ct end 

774 
end; 

775 

776 
fun generalize_tac f = CSUBGOAL (fn (p, i) => PRIMITIVE (fn st => 

777 
let 

778 
fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"} 

779 
fun gen x t = Thm.capply (all (ctyp_of_term x)) (Thm.cabs x t) 

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

781 
val p' = fold_rev gen ts p 

36945  782 
in Thm.implies_intr p' (Thm.implies_elim st (fold Thm.forall_elim ts (Thm.assume p'))) end)); 
36802  783 

784 
local 

785 
val ss1 = comp_ss 

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

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

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

789 
@{thm "zmult_int"}] 

790 
addsplits [@{thm "zdiff_int_split"}] 

791 

792 
val ss2 = HOL_basic_ss 

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

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

795 
@{thm "number_of2"}, @{thm "int_0"}, @{thm "int_1"}, @{thm "Suc_eq_plus1"}] 

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

797 
val div_mod_ss = HOL_basic_ss addsimps @{thms simp_thms} 

36945  798 
@ map (Thm.symmetric o mk_meta_eq) 
36802  799 
[@{thm "dvd_eq_mod_eq_0"}, 
800 
@{thm "mod_add_left_eq"}, @{thm "mod_add_right_eq"}, 

801 
@{thm "mod_add_eq"}, @{thm "div_add1_eq"}, @{thm "zdiv_zadd1_eq"}] 

802 
@ [@{thm "mod_self"}, @{thm "zmod_self"}, @{thm "mod_by_0"}, 

803 
@{thm "div_by_0"}, @{thm "DIVISION_BY_ZERO"} RS conjunct1, 

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

805 
@{thm "div_0"}, @{thm "mod_0"}, @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, 

806 
@{thm "mod_1"}, @{thm "Suc_eq_plus1"}] 

807 
@ @{thms add_ac} 

808 
addsimprocs [cancel_div_mod_nat_proc, cancel_div_mod_int_proc] 

809 
val splits_ss = comp_ss addsimps [@{thm "mod_div_equality'"}] addsplits 

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

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

812 
in 

813 
fun nat_to_int_tac ctxt = 

814 
simp_tac (Simplifier.context ctxt ss1) THEN_ALL_NEW 

815 
simp_tac (Simplifier.context ctxt ss2) THEN_ALL_NEW 

816 
simp_tac (Simplifier.context ctxt comp_ss); 

817 

818 
fun div_mod_tac ctxt i = simp_tac (Simplifier.context ctxt div_mod_ss) i; 

819 
fun splits_tac ctxt i = simp_tac (Simplifier.context ctxt splits_ss) i; 

820 
end; 

821 

36804  822 
fun core_tac ctxt = CSUBGOAL (fn (p, i) => 
36805  823 
let 
36802  824 
val cpth = 
825 
if !quick_and_dirty 

36805  826 
then oracle (ctxt, Envir.beta_norm (Pattern.eta_long [] (term_of (Thm.dest_arg p)))) 
36804  827 
else Conv.arg_conv (conv ctxt) p 
36802  828 
val p' = Thm.rhs_of cpth 
36945  829 
val th = Thm.implies_intr p' (Thm.equal_elim (Thm.symmetric cpth) (Thm.assume p')) 
36802  830 
in rtac th i end 
831 
handle COOPER _ => no_tac); 

832 

833 
fun finish_tac q = SUBGOAL (fn (_, i) => 

834 
(if q then I else TRY) (rtac TrueI i)); 

835 

36804  836 
fun tac elim add_ths del_ths ctxt = 
36802  837 
let val ss = Simplifier.context ctxt (fst (get ctxt)) delsimps del_ths addsimps add_ths 
838 
val aprems = Arith_Data.get_arith_facts ctxt 

839 
in 

840 
Method.insert_tac aprems 

841 
THEN_ALL_NEW Object_Logic.full_atomize_tac 

842 
THEN_ALL_NEW CONVERSION Thm.eta_long_conversion 

843 
THEN_ALL_NEW simp_tac ss 

844 
THEN_ALL_NEW (TRY o generalize_tac (int_nat_terms ctxt)) 

845 
THEN_ALL_NEW Object_Logic.full_atomize_tac 

846 
THEN_ALL_NEW (thin_prems_tac (is_relevant ctxt)) 

847 
THEN_ALL_NEW Object_Logic.full_atomize_tac 

848 
THEN_ALL_NEW div_mod_tac ctxt 

849 
THEN_ALL_NEW splits_tac ctxt 

850 
THEN_ALL_NEW simp_tac ss 

851 
THEN_ALL_NEW CONVERSION Thm.eta_long_conversion 

852 
THEN_ALL_NEW nat_to_int_tac ctxt 

36804  853 
THEN_ALL_NEW (core_tac ctxt) 
36802  854 
THEN_ALL_NEW finish_tac elim 
855 
end; 

856 

36804  857 
val method = 
36802  858 
let 
859 
fun keyword k = Scan.lift (Args.$$$ k  Args.colon) >> K () 

860 
fun simple_keyword k = Scan.lift (Args.$$$ k) >> K () 

861 
val addN = "add" 

862 
val delN = "del" 

863 
val elimN = "elim" 

864 
val any_keyword = keyword addN  keyword delN  simple_keyword elimN 

865 
val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat; 

866 
in 

867 
Scan.optional (simple_keyword elimN >> K false) true  

868 
Scan.optional (keyword addN  thms) []  

869 
Scan.optional (keyword delN  thms) [] >> 

870 
(fn ((elim, add_ths), del_ths) => fn ctxt => 

36804  871 
SIMPLE_METHOD' (tac elim add_ths del_ths ctxt)) 
36802  872 
end; 
873 

874 

875 
(* theory setup *) 

876 

877 
local 

878 

879 
fun keyword k = Scan.lift (Args.$$$ k  Args.colon) >> K (); 

880 

881 
val constsN = "consts"; 

882 
val any_keyword = keyword constsN 

883 
val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat; 

884 
val terms = thms >> map (term_of o Drule.dest_term); 

885 

886 
fun optional scan = Scan.optional scan []; 

887 

888 
in 

889 

890 
val setup = 

891 
Attrib.setup @{binding presburger} 

892 
((Scan.lift (Args.$$$ "del")  optional (keyword constsN  terms)) >> del  

893 
optional (keyword constsN  terms) >> add) "data for Cooper's algorithm" 

36804  894 
#> Arith_Data.add_tactic "Presburger arithmetic" (K (tac true [] [])); 
36802  895 

896 
end; 

897 

898 
end; 