src/HOL/Tools/Presburger/reflected_cooper.ML
author haftmann
Fri Feb 10 09:09:07 2006 +0100 (2006-02-10)
changeset 19008 14c1b2f5dda4
parent 17521 0f1c48de39f5
child 19233 77ca20b0ed77
permissions -rw-r--r--
improved code generator devarification
     1 (* $Id$ *)
     2 (* The oracle for Presburger arithmetic based on the verified Code *)
     3     (* in HOL/ex/Reflected_Presburger.thy *)
     4 
     5 structure ReflectedCooper =
     6 struct
     7 
     8 open Generated;
     9 (* pseudo reification : term -> intterm *)
    10 
    11 fun i_of_term vs t = 
    12     case t of
    13 	Free(xn,xT) => (case AList.lookup (op =) vs t of 
    14 			   NONE   => error "Variable not found in the list!!"
    15 			 | SOME n => Var n)
    16       | Const("0",iT) => Cst 0
    17       | Const("1",iT) => Cst 1
    18       | Bound i => Var (nat (IntInf.fromInt i))
    19       | Const("uminus",_)$t' => Neg (i_of_term vs t')
    20       | Const ("op +",_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
    21       | Const ("op -",_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
    22       | Const ("op *",_)$t1$t2 => Mult (i_of_term vs t1,i_of_term vs t2)
    23       | Const ("Numeral.number_of",_)$t' => Cst (HOLogic.dest_binum t')
    24       | _ => error "i_of_term: unknown term";
    25 	
    26 
    27 (* pseudo reification : term -> QF *)
    28 fun qf_of_term vs t = 
    29     case t of 
    30 	Const("True",_) => T
    31       | Const("False",_) => F
    32       | Const("op <",_)$t1$t2 => Lt (i_of_term vs t1,i_of_term vs t2)
    33       | Const("op <=",_)$t1$t2 => Le (i_of_term vs t1,i_of_term vs t2)
    34       | Const ("Divides.op dvd",_)$t1$t2 => 
    35 	Divides(i_of_term vs t1,i_of_term vs t2)
    36       | Const("op =",eqT)$t1$t2 => 
    37 	if (domain_type eqT = HOLogic.intT)
    38 	then let val i1 = i_of_term vs t1
    39 		 val i2 = i_of_term vs t2
    40 	     in	Eq (i1,i2)
    41 	     end 
    42 	else Equ(qf_of_term vs t1,qf_of_term vs t2)
    43       | Const("op &",_)$t1$t2 => And(qf_of_term vs t1,qf_of_term vs t2)
    44       | Const("op |",_)$t1$t2 => Or(qf_of_term vs t1,qf_of_term vs t2)
    45       | Const("op -->",_)$t1$t2 => Imp(qf_of_term vs t1,qf_of_term vs t2)
    46       | Const("Not",_)$t' => NOT(qf_of_term vs t')
    47       | Const("Ex",_)$Abs(xn,xT,p) => 
    48 	QEx(qf_of_term (map (fn(v,n) => (v,n + 1)) vs) p)
    49       | Const("All",_)$Abs(xn,xT,p) => 
    50 	QAll(qf_of_term (map (fn(v,n) => (v,n + 1)) vs) p)
    51       | _ => error "qf_of_term : unknown term!";
    52 
    53 (*
    54 fun parse s = term_of (read_cterm (sign_of Main.thy) (s,HOLogic.boolT));
    55 
    56 val t = parse "ALL (i::int) (j::int). i < 8* j --> (i - 1 = j + 3 + 2*j) & (j <= -i + k ) | 4 = i | 5 dvd i";
    57 *)
    58 fun zip [] [] = []
    59   | zip (x::xs) (y::ys) = (x,y)::(zip xs ys);
    60 
    61 
    62 fun start_vs t =
    63     let val fs = term_frees t
    64     in zip fs (map (nat o IntInf.fromInt) (0 upto  (length fs - 1)))
    65     end ;
    66 
    67 (* transform intterm and QF back to terms *)
    68 val iT = HOLogic.intT;
    69 val bT = HOLogic.boolT;
    70 fun myassoc2 l v =
    71     case l of
    72 	[] => NONE
    73       | (x,v')::xs => if v = v' then SOME x
    74 		      else myassoc2 xs v;
    75 
    76 fun term_of_i vs t =
    77     case t of 
    78 	Cst i => CooperDec.mk_numeral i
    79       | Var n => valOf (myassoc2 vs n)
    80       | Neg t' => Const("uminus",iT --> iT)$(term_of_i vs t')
    81       | Add(t1,t2) => Const("op +",[iT,iT] ---> iT)$
    82 			   (term_of_i vs t1)$(term_of_i vs t2)
    83       | Sub(t1,t2) => Const("op -",[iT,iT] ---> iT)$
    84 			   (term_of_i vs t1)$(term_of_i vs t2)
    85       | Mult(t1,t2) => Const("op *",[iT,iT] ---> iT)$
    86 			   (term_of_i vs t1)$(term_of_i vs t2);
    87 
    88 fun term_of_qf vs t = 
    89     case t of 
    90 	T => HOLogic.true_const 
    91       | F => HOLogic.false_const
    92       | Lt(t1,t2) => Const("op <",[iT,iT] ---> bT)$
    93 			   (term_of_i vs t1)$(term_of_i vs t2)
    94       | Le(t1,t2) => Const("op <=",[iT,iT] ---> bT)$
    95 			  (term_of_i vs t1)$(term_of_i vs t2)
    96       | Gt(t1,t2) => Const("op <",[iT,iT] ---> bT)$
    97 			   (term_of_i vs t2)$(term_of_i vs t1)
    98       | Ge(t1,t2) => Const("op <=",[iT,iT] ---> bT)$
    99 			  (term_of_i vs t2)$(term_of_i vs t1)
   100       | Eq(t1,t2) => Const("op =",[iT,iT] ---> bT)$
   101 			   (term_of_i vs t1)$(term_of_i vs t2)
   102       | Divides(t1,t2) => Const("Divides.op dvd",[iT,iT] ---> bT)$
   103 			       (term_of_i vs t1)$(term_of_i vs t2)
   104       | NOT t' => HOLogic.Not$(term_of_qf vs t')
   105       | And(t1,t2) => HOLogic.conj$(term_of_qf vs t1)$(term_of_qf vs t2)
   106       | Or(t1,t2) => HOLogic.disj$(term_of_qf vs t1)$(term_of_qf vs t2)
   107       | Imp(t1,t2) => HOLogic.imp$(term_of_qf vs t1)$(term_of_qf vs t2)
   108       | Equ(t1,t2) => (HOLogic.eq_const bT)$(term_of_qf vs t1)$
   109 					   (term_of_qf vs t2)
   110       | _ => error "If this is raised, Isabelle/HOL or generate_code is inconsistent!";
   111 
   112 (* The oracle *)
   113  exception COOPER; 
   114 
   115 fun presburger_oracle thy t =
   116     let val vs = start_vs t
   117 	val result = lift_un (term_of_qf vs) (pa (qf_of_term vs t))
   118     in 
   119     case result of 
   120 	None => raise COOPER
   121       | Some t' => HOLogic.mk_Trueprop (HOLogic.mk_eq(t,t'))
   122     end ;
   123  
   124 end;