author  haftmann 
Wed, 05 May 2010 18:25:34 +0200  
changeset 36692  54b64d4ad524 
parent 36527  68a837d1a754 
child 36717  2a72455be88b 
permissions  rwrr 
24584  1 
(* Title: HOL/Tools/Qelim/cooper.ML 
23466  2 
Author: Amine Chaieb, TU Muenchen 
3 
*) 

4 

5 
signature COOPER = 

6 
sig 

23484  7 
val cooper_conv : Proof.context > conv 
23466  8 
exception COOPER of string * exn 
9 
end; 

10 

11 
structure Cooper: COOPER = 

12 
struct 

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

13 

23466  14 
open Conv; 
23689
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23582
diff
changeset

15 
open Normalizer; 
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23582
diff
changeset

16 

23466  17 
exception COOPER of string * exn; 
27018  18 
fun simp_thms_conv ctxt = 
35410  19 
Simplifier.rewrite (Simplifier.context ctxt HOL_basic_ss addsimps @{thms simp_thms}); 
23484  20 
val FWD = Drule.implies_elim_list; 
23466  21 

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

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

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

25 
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

26 
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

27 

23466  28 
val iT = HOLogic.intT 
29 
val bT = HOLogic.boolT; 

30 
val dest_numeral = HOLogic.dest_number #> snd; 

31 

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

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

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

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

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

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

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

42 

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

44 

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

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

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

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

50 
val [miex, cpmi, piex, cppi] = [@{thm "minusinfinity"}, @{thm "cpmi"}, 
23466  51 
@{thm "plusinfinity"}, @{thm "cppi"}]; 
52 

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

54 

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

55 
val [zdvd_mono,simp_from_to,all_not_ex] = 
23466  56 
[@{thm "zdvd_mono"}, @{thm "simp_from_to"}, @{thm "all_not_ex"}]; 
57 

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

59 

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

61 
val eval_conv = Simplifier.rewrite eval_ss; 

62 

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

63 
(* recognising cterm without moving to terms *) 
23466  64 

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

65 
datatype fm = And of cterm*cterm Or of cterm*cterm Eq of cterm  NEq of cterm 
23466  66 
 Lt of cterm  Le of cterm  Gt of cterm  Ge of cterm 
67 
 Dvd of cterm*cterm  NDvd of cterm*cterm  Nox 

68 

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

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

70 
( case (term_of ct) of 
23466  71 
Const("op &",_)$_$_ => And (Thm.dest_binop ct) 
72 
 Const ("op ",_)$_$_ => Or (Thm.dest_binop ct) 

73 
 Const ("op =",ty)$y$_ => if term_of x aconv y then Eq (Thm.dest_arg ct) else Nox 

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

74 
 Const (@{const_name Not},_) $ (Const ("op =",_)$y$_) => 
23466  75 
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

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

77 
if term_of x aconv y then Lt (Thm.dest_arg ct) 
23466  78 
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

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

80 
if term_of x aconv y then Le (Thm.dest_arg ct) 
23466  81 
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

82 
 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

83 
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

84 
 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

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

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

88 
handle CTERM _ => Nox; 
23466  89 

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

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

91 
let val (x,eq) = 
23466  92 
(Thm.dest_abs NONE o Thm.dest_arg o snd o Thm.dest_abs NONE o Thm.dest_arg) 
93 
(Thm.dest_arg t) 

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

95 

96 
val get_pmi = get_pmi_term o cprop_of; 

97 

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

98 
val p_v' = @{cpat "?P' :: int => bool"}; 
23466  99 
val q_v' = @{cpat "?Q' :: int => bool"}; 
100 
val p_v = @{cpat "?P:: int => bool"}; 

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

102 

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

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

104 
[(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

105 
let 
23466  106 
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

107 
val mi_th = FWD (instantiate ([],[(p_v,p),(q_v,q), (p_v',mp'),(q_v',mq')]) th1) 
23466  108 
[th_1, th_1'] 
109 
val infD_th = FWD (instantiate ([],[(p_v,mp'), (q_v, mq')]) th3) [th_3,th_3'] 

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

111 
in (mi_th, set_th, infD_th) 

112 
end; 

113 

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

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

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

117 

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

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

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

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

121 
val cone = @{cterm "1 :: int"} 
23466  122 
val cneg = @{cterm "uminus :: int => _"} 
123 
val [addC, mulC, subC, negC] = map term_of [cadd, cmulC, cminus, cneg] 

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

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

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

126 
val is_numeral = can dest_numeral; 
23466  127 

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

128 
fun numeral1 f n = HOLogic.mk_number iT (f (dest_numeral n)); 
23466  129 
fun numeral2 f m n = HOLogic.mk_number iT (f (dest_numeral m) (dest_numeral n)); 
130 

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

131 
val [minus1,plus1] = 
23466  132 
map (fn c => fn t => Thm.capply (Thm.capply c t) cone) [cminus,cadd]; 
133 

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

134 
fun decomp_pinf x dvd inS [aseteq, asetneq, asetlt, asetle, 
23466  135 
asetgt, asetge,asetdvd,asetndvd,asetP, 
136 
infDdvd, infDndvd, asetconj, 

137 
asetdisj, infDconj, infDdisj] cp = 

138 
case (whatis x cp) of 

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

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

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

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

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

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

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

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

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

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

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

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

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

155 
bsetge,bsetdvd,bsetndvd,bsetP, 

156 
infDdvd, infDndvd, bsetconj, 

157 
bsetdisj, infDconj, infDdisj] cp = 

158 
case (whatis x cp) of 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

175 
(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

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

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

178 
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

179 
 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

180 
 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

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

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

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

185 
if h aconv y then false else if h aconv x then true else earlier t x y; 
23466  186 

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

187 
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

188 
(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

189 
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

190 
if x1 = x2 then 
33002  191 
let val c = numeral2 Integer.add c1 c2 
25768  192 
in if c = zero then linear_add vars r1 r2 
193 
else addC$(mulC$c$x1)$(linear_add vars r1 r2) 

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

194 
end 
25768  195 
else if earlier vars x1 x2 then addC $ (mulC $ c1 $ x1) $ linear_add vars r1 tm2 
196 
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

197 
 (Const (@{const_name Groups.plus}, _) $ (Const (@{const_name Groups.times}, _) $ c1 $ x1) $ r1, _) => 
25768  198 
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

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

202 

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

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

204 
fun linear_sub vars tm1 tm2 = linear_add vars tm1 (linear_neg tm2); 
23466  205 

206 

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

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

208 
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

209 
 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

210 
 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

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

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

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

214 
in if is_numeral s' then (linear_cmul (dest_numeral s') t') 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

215 
else if is_numeral t' then (linear_cmul (dest_numeral t') s') 
23466  216 
else raise COOPER ("Cooper Failed", TERM ("lint: not linear",[tm])) 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

217 
end 
25768  218 
 _ => addC $ (mulC $ one $ tm) $ zero; 
23466  219 

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

220 
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

221 
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

222 
 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

223 
lin vs (Const (@{const_name Orderings.less}, T) $ t $ s) 
25768  224 
 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

225 
 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

226 
HOLogic.mk_binrel @{const_name Rings.dvd} (numeral1 abs d, lint vs t) 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

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

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

229 
(t as a$(m$c$y)$r) => 
23466  230 
if x <> y then b$zero$t 
231 
else if dest_numeral c < 0 then b$(m$(numeral1 ~ c)$y)$r 

232 
else b$(m$c$y)$(linear_neg r) 

233 
 t => b$zero$t) 

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

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

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

236 
(t as a$(m$c$y)$r) => 
23466  237 
if x <> y then b$zero$t 
238 
else if dest_numeral c < 0 then b$(m$(numeral1 ~ c)$y)$r 

239 
else b$(linear_neg r)$(m$c$y) 

240 
 t => b$zero$t) 

241 
 lin vs fm = fm; 

242 

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

243 
fun lint_conv ctxt vs ct = 
23466  244 
let val t = term_of ct 
245 
in (provelin ctxt ((HOLogic.eq_const iT)$t$(lint vs t) > HOLogic.mk_Trueprop)) 

246 
RS eq_reflection 

247 
end; 

248 

32398  249 
fun is_intrel_type T = T = @{typ "int => int => bool"}; 
250 

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

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

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

254 

25768  255 
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

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

257 
let 
23466  258 
val th = binop_conv (lint_conv ctxt vs) ct 
259 
val (d',t') = Thm.dest_binop (Thm.rhs_of th) 

260 
val (dt',tt') = (term_of d', term_of t') 

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

261 
in if is_numeral dt' andalso is_numeral tt' 
23466  262 
then Conv.fconv_rule (arg_conv (Simplifier.rewrite presburger_ss)) th 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

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

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

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

266 
((if dest_numeral (term_of d') < 0 then 
23466  267 
Conv.fconv_rule (arg_conv (arg1_conv (lint_conv ctxt vs))) 
268 
(Thm.transitive th (inst' [d',t'] dvd_uminus)) 

269 
else th) handle TERM _ => th) 

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

271 
in 

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

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

273 
Const(@{const_name Groups.plus},_)$(Const(@{const_name Groups.times},_)$c$_)$_ => 
23466  274 
let val x = dest_numeral c 
275 
in if x < 0 then Conv.fconv_rule (arg_conv (arg_conv (lint_conv ctxt vs))) 

276 
(Thm.transitive dth (inst' [d'',t'] dvd_uminus')) 

277 
else dth end 

278 
 _ => dth 

279 
end 

280 
end 

35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
34974
diff
changeset

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

282 
 t => if is_intrel t 
23466  283 
then (provelin ctxt ((HOLogic.eq_const bT)$t$(lin vs t) > HOLogic.mk_Trueprop)) 
284 
RS eq_reflection 

285 
else reflexive ct; 

286 

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

288 

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

289 
fun unify ctxt q = 
23466  290 
let 
291 
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

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

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

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

296 
Const(s,_)$(Const(@{const_name Groups.times},_)$c$y)$ _ => 
23881  297 
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

298 
["op =", @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s 
23466  299 
then (ins (dest_numeral c) acc,dacc) else (acc,dacc) 
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset

300 
 Const(s,_)$_$(Const(@{const_name Groups.times},_)$c$y) => 
23881  301 
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

302 
[@{const_name Orderings.less}, @{const_name Orderings.less_eq}] s 
23466  303 
then (ins (dest_numeral c) acc, dacc) else (acc,dacc) 
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset

304 
 Const(@{const_name Rings.dvd},_)$_$(Const(@{const_name Groups.plus},_)$(Const(@{const_name Groups.times},_)$c$y)$_) => 
23466  305 
if x aconv y then (acc,ins (dest_numeral c) dacc) else (acc,dacc) 
306 
 Const("op &",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t) 

307 
 Const("op ",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t) 

25768  308 
 Const (@{const_name Not},_)$_ => h (acc,dacc) (Thm.dest_arg t) 
23466  309 
 _ => (acc, dacc) 
310 
val (cs,ds) = h ([],[]) p 

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

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

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

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

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

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

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

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

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

321 
(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

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

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

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

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

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

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

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

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

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

333 
fun unit_conv t = 
23466  334 
case (term_of t) of 
335 
Const("op &",_)$_$_ => binop_conv unit_conv t 

336 
 Const("op ",_)$_$_ => binop_conv unit_conv t 

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

338 
 Const(s,_)$(Const(@{const_name Groups.times},_)$c$y)$ _ => 
23881  339 
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

340 
["op =", @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s 
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset

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

342 
 Const(s,_)$_$(Const(@{const_name Groups.times},_)$c$y) => 
23881  343 
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

344 
[@{const_name Orderings.less}, @{const_name Orderings.less_eq}] s 
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset

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

346 
 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

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

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

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

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

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

355 
RS eq_reflection 

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

357 
RS eq_reflection 

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

358 
in Thm.transitive th1 (Thm.combination (Drule.arg_cong_rule dvdc thc) tht) end 
23466  359 
else Thm.reflexive t 
360 
 _ => Thm.reflexive t 

361 
val uth = unit_conv p 

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

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

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

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

366 
val thf = transitive th 
23466  367 
(transitive (symmetric (beta_conversion true (cprop_of th' > Thm.dest_arg1))) th') 
368 
val (lth,rth) = Thm.dest_comb (cprop_of thf) >> Thm.dest_arg >> Thm.beta_conversion true 

369 
> beta_conversion true >> Thm.symmetric 

370 
in transitive (transitive lth thf) rth end; 

371 

372 

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

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

375 
val mem_tm = Const("op :",[iT , HOLogic.mk_setT iT] > bT); 

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

377 
val cTrp = @{cterm "Trueprop"}; 

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

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

379 
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  380 
> Thm.dest_abs NONE > snd > Thm.dest_fun > Thm.dest_arg) 
381 
[asetP,bsetP]; 

382 

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

384 

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

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

386 
let 
23466  387 

388 
val uth = unify ctxt q 

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

390 
val ins = insert (op aconvc) 

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

391 
fun h t (bacc,aacc,dacc) = 
23466  392 
case (whatis x t) of 
393 
And (p,q) => h q (h p (bacc,aacc,dacc)) 

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

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

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

397 
 NEq t => (ins t bacc, 
23466  398 
ins t aacc, dacc) 
399 
 Lt t => (bacc, ins t aacc, dacc) 

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

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

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

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

403 
 Dvd (d,s) => (bacc,aacc,insert (op =) (term_of d > dest_numeral) dacc) 
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset

404 
 NDvd (d,s) => (bacc,aacc,insert (op =) (term_of d> dest_numeral) dacc) 
23466  405 
 _ => (bacc, aacc, dacc) 
406 
val (b0,a0,ds) = h p ([],[],[]) 

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

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

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

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

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

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

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

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

418 
let val tab = fold Inttab.update (ds ~~ (map divprop ds)) Inttab.empty in 
33035  419 
fn ct => the (Inttab.lookup tab (term_of ct > dest_numeral)) 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

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

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

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

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

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

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

426 
(Thm.capply @{cterm Trueprop} 
23466  427 
(Thm.capply (Thm.capply @{cterm "op < :: int => _"} @{cterm "0::int"}) cd)) 
428 
in equal_elim (Thm.symmetric th) TrueI end; 

429 
(* A and B set *) 

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

430 
local 
23466  431 
val insI1 = instantiate' [SOME @{ctyp "int"}] [] @{thm "insertI1"} 
432 
val insI2 = instantiate' [SOME @{ctyp "int"}] [] @{thm "insertI2"} 

433 
in 

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

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

436 
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

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

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

440 
else implies_elim (instantiate' [] [SOME x, SOME S', SOME cy] insI2) 
23466  441 
(provein x S') 
442 
end 

443 
end 

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

444 

23466  445 
val al = map (lint vs o term_of) a0 
446 
val bl = map (lint vs o term_of) b0 

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

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

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

449 
then 
23466  450 
(bl,b0,decomp_minf, 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

451 
fn B => (map (fn th => implies_elim (Thm.instantiate ([],[(B_tm,B), (D_tm,cd)]) th) dp) 
23466  452 
[bseteq,bsetneq,bsetlt, bsetle, bsetgt,bsetge])@ 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

453 
(map (Thm.instantiate ([],[(B_tm,B), (D_tm,cd)])) 
23466  454 
[bsetdvd,bsetndvd,bsetP,infDdvd, infDndvd,bsetconj, 
455 
bsetdisj,infDconj, infDdisj]), 

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

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

457 
else (al,a0,decomp_pinf,fn A => 
23466  458 
(map (fn th => implies_elim (Thm.instantiate ([],[(A_tm,A), (D_tm,cd)]) th) dp) 
459 
[aseteq,asetneq,asetlt, asetle, asetgt,asetge])@ 

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

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

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

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

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

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

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

469 
> HOLogic.mk_Trueprop)) 
23466  470 
(sl ~~ s0) 
471 
val csl = distinct (op aconvc) (map (cprop_of #> Thm.dest_arg #> Thm.dest_arg1) sths) 

472 
val S = mkISet csl 

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

473 
val inStab = fold (fn ct => fn tab => Termtab.update (term_of ct, provein ct S) tab) 
23466  474 
csl Termtab.empty 
475 
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

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

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

478 
fun transmem th0 th1 = 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

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

480 
(Drule.arg_cong_rule cTrp (Drule.fun_cong_rule (Drule.arg_cong_rule 
23466  481 
((Thm.dest_fun o Thm.dest_fun o Thm.dest_arg o cprop_of) th1) th0) S)) th1 
482 
val tab = fold Termtab.update 

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

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

484 
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

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

487 
else FWD (instantiate' [] [SOME s, SOME t] eqelem_th) 
33035  488 
[eq, the (Termtab.lookup inStab (term_of s))] 
23466  489 
in (term_of t, th) end) 
490 
sths) Termtab.empty 

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

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

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

494 
(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

495 
raise Option) 
23466  496 
end 
497 
val (inf, nb, pd) = divide_and_conquer (f x dvd inS (abths S)) p 

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

499 
end 

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

27018  501 
in Thm.transitive cpth' ((simp_thms_conv ctxt then_conv eval_conv) (Thm.rhs_of cpth')) 
23466  502 
end; 
503 

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

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

506 
case (term_of t) of 
23466  507 
b$_$_ => if member (op aconv) bops b then binop_conv h t else cv env t 
508 
 u$_ => if member (op aconv) uops u then arg_conv h t else cv env t 

509 
 _ => cv env t 

510 
in h end; 

511 

512 
fun integer_nnf_conv ctxt env = 

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

514 

515 
local 

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

516 
val pcv = Simplifier.rewrite 
35410  517 
(HOL_basic_ss addsimps (@{thms simp_thms} @ List.take(@{thms ex_simps}, 4) 
518 
@ [not_all, all_not_ex, @{thm ex_disj_distrib}])) 

23466  519 
val postcv = Simplifier.rewrite presburger_ss 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

520 
fun conv ctxt p = 
24298  521 
let val _ = () 
23466  522 
in 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

523 
Qelim.gen_qelim_conv pcv postcv pcv (cons o term_of) 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

524 
(OldTerm.term_frees (term_of p)) (linearize_conv ctxt) (integer_nnf_conv ctxt) 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

525 
(cooperex_conv ctxt) p 
23466  526 
end 
527 
handle CTERM s => raise COOPER ("Cooper Failed", CTERM s) 

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

528 
 THM s => raise COOPER ("Cooper Failed", THM s) 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

529 
 TYPE s => raise COOPER ("Cooper Failed", TYPE s) 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

530 
in val cooper_conv = conv 
23466  531 
end; 
532 
end; 

533 

534 

535 

536 
structure Coopereif = 

537 
struct 

538 

36527  539 
open Generated_Cooper; 
23713  540 

36692
54b64d4ad524
farewell to oldstyle mem infixes  type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
36527
diff
changeset

541 
fun member eq = Library.member eq; 
54b64d4ad524
farewell to oldstyle mem infixes  type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
36527
diff
changeset

542 

23713  543 
fun cooper s = raise Cooper.COOPER ("Cooper oracle failed", ERROR s); 
544 
fun i_of_term vs t = case t 

545 
of Free (xn, xT) => (case AList.lookup (op aconv) vs t 

546 
of NONE => cooper "Variable not found in the list!" 

547 
 SOME n => Bound n) 

548 
 @{term "0::int"} => C 0 

549 
 @{term "1::int"} => C 1 

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

550 
 Term.Bound i => Bound i 
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset

551 
 Const(@{const_name Groups.uminus},_)$t' => Neg (i_of_term vs t') 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset

552 
 Const(@{const_name Groups.plus},_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2) 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset

553 
 Const(@{const_name Groups.minus},_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2) 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset

554 
 Const(@{const_name Groups.times},_)$t1$t2 => 
23713  555 
(Mul (HOLogic.dest_number t1 > snd, i_of_term vs t2) 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

556 
handle TERM _ => 
23713  557 
(Mul (HOLogic.dest_number t2 > snd, i_of_term vs t1) 
558 
handle TERM _ => cooper "Reification: Unsupported kind of multiplication")) 

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

559 
 _ => (C (HOLogic.dest_number t > snd) 
23713  560 
handle TERM _ => cooper "Reification: unknown term"); 
23689
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23582
diff
changeset

561 

23713  562 
fun qf_of_term ps vs t = case t 
563 
of Const("True",_) => T 

564 
 Const("False",_) => F 

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

565 
 Const(@{const_name Orderings.less},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2)) 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

566 
 Const(@{const_name Orderings.less_eq},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2)) 
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
34974
diff
changeset

567 
 Const(@{const_name Rings.dvd},_)$t1$t2 => 
28397
389c5e494605
handle _ should be avoided (spurious Interrupt will spoil the game);
wenzelm
parents:
28290
diff
changeset

568 
(Dvd(HOLogic.dest_number t1 > snd, i_of_term vs t2) handle _ => cooper "Reification: unsupported dvd") (* FIXME avoid handle _ *) 
23713  569 
 @{term "op = :: int => _"}$t1$t2 => Eq (Sub (i_of_term vs t1,i_of_term vs t2)) 
29787  570 
 @{term "op = :: bool => _ "}$t1$t2 => Iff(qf_of_term ps vs t1,qf_of_term ps vs t2) 
23713  571 
 Const("op &",_)$t1$t2 => And(qf_of_term ps vs t1,qf_of_term ps vs t2) 
572 
 Const("op ",_)$t1$t2 => Or(qf_of_term ps vs t1,qf_of_term ps vs t2) 

29787  573 
 Const("op >",_)$t1$t2 => Imp(qf_of_term ps vs t1,qf_of_term ps vs t2) 
574 
 Const (@{const_name Not},_)$t' => Not(qf_of_term ps vs t') 

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

575 
 Const("Ex",_)$Abs(xn,xT,p) => 
23713  576 
let val (xn',p') = variant_abs (xn,xT,p) 
577 
val vs' = (Free (xn',xT), 0) :: (map (fn(v,n) => (v,1+ n)) vs) 

578 
in E (qf_of_term ps vs' p') 

579 
end 

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

580 
 Const("All",_)$Abs(xn,xT,p) => 
23713  581 
let val (xn',p') = variant_abs (xn,xT,p) 
582 
val vs' = (Free (xn',xT), 0) :: (map (fn(v,n) => (v,1+ n)) vs) 

583 
in A (qf_of_term ps vs' p') 

584 
end 

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

585 
 _ =>(case AList.lookup (op aconv) ps t of 
23713  586 
NONE => cooper "Reification: unknown term!" 
587 
 SOME n => Closed n); 

23466  588 

589 
local 

590 
val ops = [@{term "op &"}, @{term "op "}, @{term "op >"}, @{term "op = :: bool => _"}, 

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

591 
@{term "op = :: int => _"}, @{term "op < :: int => _"}, 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

592 
@{term "op <= :: int => _"}, @{term "Not"}, @{term "All:: (int => _) => _"}, 
23466  593 
@{term "Ex:: (int => _) => _"}, @{term "True"}, @{term "False"}] 
594 
fun ty t = Bool.not (fastype_of t = HOLogic.boolT) 

595 
in 

596 
fun term_bools acc t = 

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

597 
case t of 
36692
54b64d4ad524
farewell to oldstyle mem infixes  type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
36527
diff
changeset

598 
(l as f $ a) $ b => if ty t orelse member (op =) ops f then term_bools (term_bools acc l)b 
23466  599 
else insert (op aconv) t acc 
36692
54b64d4ad524
farewell to oldstyle mem infixes  type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
36527
diff
changeset

600 
 f $ a => if ty t orelse member (op =) ops f then term_bools (term_bools acc f) a 
23466  601 
else insert (op aconv) t acc 
602 
 Abs p => term_bools acc (snd (variant_abs p)) 

36692
54b64d4ad524
farewell to oldstyle mem infixes  type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
36527
diff
changeset

603 
 _ => if ty t orelse member (op =) ops t then acc else insert (op aconv) t acc 
23466  604 
end; 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

605 

23466  606 
fun myassoc2 l v = 
607 
case l of 

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

608 
[] => NONE 
23689
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23582
diff
changeset

609 
 (x,v')::xs => if v = v' then SOME x 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

610 
else myassoc2 xs v; 
23466  611 

23713  612 
fun term_of_i vs t = case t 
613 
of C i => HOLogic.mk_number HOLogic.intT i 

614 
 Bound n => the (myassoc2 vs n) 

615 
 Neg t' => @{term "uminus :: int => _"} $ term_of_i vs t' 

616 
 Add (t1, t2) => @{term "op + :: int => _"} $ term_of_i vs t1 $ term_of_i vs t2 

617 
 Sub (t1, t2) => @{term "op  :: int => _"} $ term_of_i vs t1 $ term_of_i vs t2 

618 
 Mul (i, t2) => @{term "op * :: int => _"} $ 

619 
HOLogic.mk_number HOLogic.intT i $ term_of_i vs t2 

29787  620 
 Cn (n, i, t') => term_of_i vs (Add (Mul (i, Bound n), t')); 
23466  621 

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

622 
fun term_of_qf ps vs t = 
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

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

624 
T => HOLogic.true_const 
23466  625 
 F => HOLogic.false_const 
626 
 Lt t' => @{term "op < :: int => _ "}$ term_of_i vs t'$ @{term "0::int"} 

627 
 Le t' => @{term "op <= :: int => _ "}$ term_of_i vs t' $ @{term "0::int"} 

628 
 Gt t' => @{term "op < :: int => _ "}$ @{term "0::int"}$ term_of_i vs t' 

629 
 Ge t' => @{term "op <= :: int => _ "}$ @{term "0::int"}$ term_of_i vs t' 

630 
 Eq t' => @{term "op = :: int => _ "}$ term_of_i vs t'$ @{term "0::int"} 

29787  631 
 NEq t' => term_of_qf ps vs (Not (Eq t')) 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset

632 
 Dvd(i,t') => @{term "op dvd :: int => _ "} $ 
23713  633 
HOLogic.mk_number HOLogic.intT i $ term_of_i vs t' 
29787  634 
 NDvd(i,t')=> term_of_qf ps vs (Not(Dvd(i,t'))) 
635 
 Not t' => HOLogic.Not$(term_of_qf ps vs t') 

23466  636 
 And(t1,t2) => HOLogic.conj$(term_of_qf ps vs t1)$(term_of_qf ps vs t2) 
637 
 Or(t1,t2) => HOLogic.disj$(term_of_qf ps vs t1)$(term_of_qf ps vs t2) 

29787  638 
 Imp(t1,t2) => HOLogic.imp$(term_of_qf ps vs t1)$(term_of_qf ps vs t2) 
639 
 Iff(t1,t2) => @{term "op = :: bool => _"} $ term_of_qf ps vs t1 $ term_of_qf ps vs t2 

23713  640 
 Closed n => the (myassoc2 ps n) 
29787  641 
 NClosed n => term_of_qf ps vs (Not (Closed n)) 
642 
 _ => cooper "If this is raised, Isabelle/HOL or code generator is inconsistent!"; 

23466  643 

28290  644 
fun cooper_oracle ct = 
23713  645 
let 
28290  646 
val thy = Thm.theory_of_cterm ct; 
647 
val t = Thm.term_of ct; 

29265
5b4247055bd7
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents:
28397
diff
changeset

648 
val (vs, ps) = pairself (map_index swap) (OldTerm.term_frees t, term_bools [] t); 
23713  649 
in 
28290  650 
Thm.cterm_of thy (Logic.mk_equals (HOLogic.mk_Trueprop t, 
651 
HOLogic.mk_Trueprop (term_of_qf ps vs (pa (qf_of_term ps vs t))))) 

23713  652 
end; 
23466  653 

654 
end; 