src/HOL/ex/coopereif.ML
author haftmann
Fri Aug 24 14:14:20 2007 +0200 (2007-08-24)
changeset 24423 ae9cd0e92423
parent 24000 467e77e4e276
child 24630 351a308ab58d
permissions -rw-r--r--
overloaded definitions accompanied by explicit constants
     1 (*  ID:         $Id$
     2     Author:     Amine Chaieb, TU Muenchen
     3 
     4 Reification for the automatically generated oracle for Presburger arithmetic
     5 in HOL/ex/Reflected_Presburger.thy.
     6 *)
     7 
     8 structure Coopereif =
     9 struct
    10 
    11 open GeneratedCooper;
    12 
    13 val nat = GeneratedCooper.nat o Integer.int;
    14 
    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
    21     | Term.Bound i => Bound (nat i)
    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)
    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"))
    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
    34       | Const("False",_) => F
    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))
    37       | Const(@{const_name "Divides.dvd"},_)$t1$t2 => 
    38           (Dvd(HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle _ => error "qf_of_term: unsupported dvd")
    39       | @{term "op = :: int => _"}$t1$t2 => Eq (Sub (i_of_term vs t1,i_of_term vs t2))
    40       | @{term "op = :: bool => _ "}$t1$t2 => Iff(qf_of_term ps vs t1,qf_of_term ps vs t2)
    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)
    43       | Const("op -->",_)$t1$t2 => Imp(qf_of_term ps vs t1,qf_of_term ps vs t2)
    44       | Const("Not",_)$t' => Not(qf_of_term ps vs t')
    45       | Const("Ex",_)$Abs(xn,xT,p) => 
    46          let val (xn',p') = variant_abs (xn,xT,p)
    47              val vs' = (Free (xn',xT), nat 0) :: (map (fn(v,n) => (v,1 + n)) vs)
    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)
    52              val vs' = (Free (xn',xT), nat 0) :: (map (fn(v,n) => (v,1 + n)) vs)
    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
    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)
    65 in
    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
    70   | f $ a => if ty t orelse f mem ops then term_bools (term_bools acc f) a  
    71       else insert (op aconv) t acc
    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
    74 
    75 end;
    76 
    77 fun start_vs t =
    78   let
    79     val fs = term_frees t
    80     val ps = term_bools [] t
    81   in
    82     (fs ~~ (map nat (0 upto  (length fs - 1))),
    83       ps ~~ (map nat (0 upto  (length ps - 1))))
    84   end;
    85 
    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
    95   | Cn (n,i, t') => term_of_i vs (Add (Mul (i, Bound n), t'));
    96 
    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 (Not(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 (Not(Dvd(i,t')))
   109   | Not 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   | Imp(t1,t2) => HOLogic.imp$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
   113   | Iff(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 (Not (Closed n))
   116   | _ => error "If this is raised, Isabelle/HOL or generate_code is inconsistent!";
   117 
   118 (* The oracle *)
   119 fun cooper_oracle thy t = 
   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;
   123 
   124 end;