23515

1 
(* ID: $Id$


2 
Author: Amine Chaieb, TU Muenchen

23274

3 

23515

4 
Reification for the automatically generated oracle for Presburger arithmetic


5 
in HOL/ex/Reflected_Presburger.thy.

23274

6 
*)


7 


8 
structure Coopereif =


9 
struct


10 


11 
open GeneratedCooper;


12 

23808

13 
val nat = GeneratedCooper.nat o Integer.int;


14 

23515

15 
fun i_of_term vs t = case t


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


17 
of NONE => error "Variable not found in the list!"


18 
 SOME n => Bound n)


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


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

23693

21 
 Term.Bound i => Bound (nat i)

23515

22 
 Const(@{const_name "HOL.uminus"},_)$t' => Neg (i_of_term vs t')


23 
 Const(@{const_name "HOL.plus"},_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)


24 
 Const(@{const_name "HOL.minus"},_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)


25 
 Const(@{const_name "HOL.times"},_)$t1$t2 => (Mul (HOLogic.dest_number t1 > snd,i_of_term vs t2)

23274

26 
handle TERM _ =>


27 
(Mul (HOLogic.dest_number t2 > snd,i_of_term vs t1)


28 
handle TERM _ => error "i_of_term: Unsupported kind of multiplication"))

23515

29 
 _ => (C (HOLogic.dest_number t > snd)


30 
handle TERM _ => error "i_of_term: unknown term");


31 


32 
fun qf_of_term ps vs t = case t


33 
of Const("True",_) => T

23274

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

23881

35 
 Const(@{const_name HOL.less},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2))


36 
 Const(@{const_name HOL.less_eq},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2))

23274

37 
 Const(@{const_name "Divides.dvd"},_)$t1$t2 =>

23515

38 
(Dvd(HOLogic.dest_number t1 > snd, i_of_term vs t2) handle _ => error "qf_of_term: unsupported dvd")

23274

39 
 @{term "op = :: int => _"}$t1$t2 => Eq (Sub (i_of_term vs t1,i_of_term vs t2))

23515

40 
 @{term "op = :: bool => _ "}$t1$t2 => Iffa(qf_of_term ps vs t1,qf_of_term ps vs t2)

23274

41 
 Const("op &",_)$t1$t2 => And(qf_of_term ps vs t1,qf_of_term ps vs t2)


42 
 Const("op ",_)$t1$t2 => Or(qf_of_term ps vs t1,qf_of_term ps vs t2)

23515

43 
 Const("op >",_)$t1$t2 => Impa(qf_of_term ps vs t1,qf_of_term ps vs t2)


44 
 Const("Not",_)$t' => Nota(qf_of_term ps vs t')

23274

45 
 Const("Ex",_)$Abs(xn,xT,p) =>


46 
let val (xn',p') = variant_abs (xn,xT,p)

23693

47 
val vs' = (Free (xn',xT), nat 0) :: (map (fn(v,n) => (v,1 + n)) vs)

23274

48 
in E (qf_of_term ps vs' p')


49 
end


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


51 
let val (xn',p') = variant_abs (xn,xT,p)

23693

52 
val vs' = (Free (xn',xT), nat 0) :: (map (fn(v,n) => (v,1 + n)) vs)

23274

53 
in A (qf_of_term ps vs' p')


54 
end


55 
 _ =>(case AList.lookup (op aconv) ps t of


56 
NONE => error "qf_of_term ps : unknown term!"


57 
 SOME n => Closed n);


58 


59 
local

23515

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


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


62 
@{term "op <= :: int => _"}, @{term "Not"}, @{term "All:: (int => _) => _"},


63 
@{term "Ex:: (int => _) => _"}, @{term "True"}, @{term "False"}]


64 
fun ty t = Bool.not (fastype_of t = HOLogic.boolT)

23274

65 
in

23515

66 


67 
fun term_bools acc t = case t


68 
of (l as f $ a) $ b => if ty t orelse f mem ops then term_bools (term_bools acc l)b


69 
else insert (op aconv) t acc

23274

70 
 f $ a => if ty t orelse f mem ops then term_bools (term_bools acc f) a

23515

71 
else insert (op aconv) t acc

23274

72 
 Abs p => term_bools acc (snd (variant_abs p))


73 
 _ => if ty t orelse t mem ops then acc else insert (op aconv) t acc

23515

74 

23274

75 
end;


76 


77 
fun start_vs t =

23515

78 
let


79 
val fs = term_frees t


80 
val ps = term_bools [] t


81 
in

23693

82 
(fs ~~ (map nat (0 upto (length fs  1))),


83 
ps ~~ (map nat (0 upto (length ps  1))))

23515

84 
end;

23274

85 

23515

86 
fun term_of_i vs t = case t


87 
of C i => HOLogic.mk_number HOLogic.intT i


88 
 Bound n => (fst o the) (find_first (fn (_, m) => m = n) vs)


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


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


91 
 Sub (t1, t2) => Const (@{const_name "HOL.minus"}, HOLogic.intT > HOLogic.intT > HOLogic.intT) $


92 
term_of_i vs t1 $ term_of_i vs t2


93 
 Mul (i, t2) => Const (@{const_name "HOL.times"}, HOLogic.intT > HOLogic.intT > HOLogic.intT) $


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

23996

95 
 Cn (n,i, t') => term_of_i vs (Add (Mul (i, Bound (nat n)), t'));

23274

96 

23515

97 
fun term_of_qf ps vs t = case t


98 
of T => HOLogic.true_const


99 
 F => HOLogic.false_const


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


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


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


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


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


105 
 NEq t' => term_of_qf ps vs (Nota(Eq t'))


106 
 Dvd(i,t') => @{term "op dvd :: int => _ "}$


107 
(HOLogic.mk_number HOLogic.intT i)$(term_of_i vs t')


108 
 NDvd(i,t')=> term_of_qf ps vs (Nota(Dvd(i,t')))


109 
 Nota t' => HOLogic.Not$(term_of_qf ps vs t')


110 
 And(t1,t2) => HOLogic.conj$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)


111 
 Or(t1,t2) => HOLogic.disj$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)


112 
 Impa(t1,t2) => HOLogic.imp$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)


113 
 Iffa(t1,t2) => HOLogic.eq_const HOLogic.boolT $ term_of_qf ps vs t1 $ term_of_qf ps vs t2


114 
 Closed n => (fst o the) (find_first (fn (_, m) => m = n) ps)


115 
 NClosed n => term_of_qf ps vs (Nota (Closed n))


116 
 _ => error "If this is raised, Isabelle/HOL or generate_code is inconsistent!";

23274

117 


118 
(* The oracle *)


119 
fun cooper_oracle thy t =

23515

120 
let


121 
val (vs, ps) = start_vs t;


122 
in HOLogic.mk_Trueprop (HOLogic.mk_eq (t, term_of_qf ps vs (pa (qf_of_term ps vs t)))) end;

23274

123 


124 
end; 