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