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
haftmann@23515
     1
(*  ID:         $Id$
haftmann@23515
     2
    Author:     Amine Chaieb, TU Muenchen
chaieb@23274
     3
haftmann@23515
     4
Reification for the automatically generated oracle for Presburger arithmetic
haftmann@23515
     5
in HOL/ex/Reflected_Presburger.thy.
chaieb@23274
     6
*)
chaieb@23274
     7
chaieb@23274
     8
structure Coopereif =
chaieb@23274
     9
struct
chaieb@23274
    10
chaieb@23274
    11
open GeneratedCooper;
chaieb@23274
    12
haftmann@23808
    13
val nat = GeneratedCooper.nat o Integer.int;
haftmann@23808
    14
haftmann@23515
    15
fun i_of_term vs t = case t
haftmann@23515
    16
 of Free(xn,xT) => (case AList.lookup (op aconv) vs t
haftmann@23515
    17
   of NONE   => error "Variable not found in the list!"
haftmann@23515
    18
    | SOME n => Bound n)
haftmann@23515
    19
    | @{term "0::int"} => C 0
haftmann@23515
    20
    | @{term "1::int"} => C 1
haftmann@23693
    21
    | Term.Bound i => Bound (nat i)
haftmann@23515
    22
    | Const(@{const_name "HOL.uminus"},_)$t' => Neg (i_of_term vs t')
haftmann@23515
    23
    | Const(@{const_name "HOL.plus"},_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
haftmann@23515
    24
    | Const(@{const_name "HOL.minus"},_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
haftmann@23515
    25
    | Const(@{const_name "HOL.times"},_)$t1$t2 => (Mul (HOLogic.dest_number t1 |> snd,i_of_term vs t2)
chaieb@23274
    26
        handle TERM _ => 
chaieb@23274
    27
           (Mul (HOLogic.dest_number t2 |> snd,i_of_term vs t1)
chaieb@23274
    28
            handle TERM _ => error "i_of_term: Unsupported kind of multiplication"))
haftmann@23515
    29
    | _ => (C (HOLogic.dest_number t |> snd) 
haftmann@23515
    30
             handle TERM _ => error "i_of_term: unknown term");
haftmann@23515
    31
haftmann@23515
    32
fun qf_of_term ps vs t = case t
haftmann@23515
    33
     of Const("True",_) => T
chaieb@23274
    34
      | Const("False",_) => F
haftmann@23881
    35
      | Const(@{const_name HOL.less},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2))
haftmann@23881
    36
      | Const(@{const_name HOL.less_eq},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2))
chaieb@23274
    37
      | Const(@{const_name "Divides.dvd"},_)$t1$t2 => 
haftmann@23515
    38
          (Dvd(HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle _ => error "qf_of_term: unsupported dvd")
chaieb@23274
    39
      | @{term "op = :: int => _"}$t1$t2 => Eq (Sub (i_of_term vs t1,i_of_term vs t2))
haftmann@24423
    40
      | @{term "op = :: bool => _ "}$t1$t2 => Iff(qf_of_term ps vs t1,qf_of_term ps vs t2)
chaieb@23274
    41
      | Const("op &",_)$t1$t2 => And(qf_of_term ps vs t1,qf_of_term ps vs t2)
chaieb@23274
    42
      | Const("op |",_)$t1$t2 => Or(qf_of_term ps vs t1,qf_of_term ps vs t2)
haftmann@24423
    43
      | Const("op -->",_)$t1$t2 => Imp(qf_of_term ps vs t1,qf_of_term ps vs t2)
haftmann@24423
    44
      | Const("Not",_)$t' => Not(qf_of_term ps vs t')
chaieb@23274
    45
      | Const("Ex",_)$Abs(xn,xT,p) => 
chaieb@23274
    46
         let val (xn',p') = variant_abs (xn,xT,p)
haftmann@23693
    47
             val vs' = (Free (xn',xT), nat 0) :: (map (fn(v,n) => (v,1 + n)) vs)
chaieb@23274
    48
         in E (qf_of_term ps vs' p')
chaieb@23274
    49
         end
chaieb@23274
    50
      | Const("All",_)$Abs(xn,xT,p) => 
chaieb@23274
    51
         let val (xn',p') = variant_abs (xn,xT,p)
haftmann@23693
    52
             val vs' = (Free (xn',xT), nat 0) :: (map (fn(v,n) => (v,1 + n)) vs)
chaieb@23274
    53
         in A (qf_of_term ps vs' p')
chaieb@23274
    54
         end
chaieb@23274
    55
      | _ =>(case AList.lookup (op aconv) ps t of 
chaieb@23274
    56
               NONE => error "qf_of_term ps : unknown term!"
chaieb@23274
    57
             | SOME n => Closed n);
chaieb@23274
    58
chaieb@23274
    59
local
haftmann@23515
    60
  val ops = [@{term "op &"}, @{term "op |"}, @{term "op -->"}, @{term "op = :: bool => _"},
haftmann@23515
    61
    @{term "op = :: int => _"}, @{term "op < :: int => _"},
haftmann@23515
    62
    @{term "op <= :: int => _"}, @{term "Not"}, @{term "All:: (int => _) => _"},
haftmann@23515
    63
    @{term "Ex:: (int => _) => _"}, @{term "True"}, @{term "False"}]
haftmann@23515
    64
  fun ty t = Bool.not (fastype_of t = HOLogic.boolT)
chaieb@23274
    65
in
haftmann@23515
    66
haftmann@23515
    67
fun term_bools acc t = case t
haftmann@23515
    68
 of (l as f $ a) $ b => if ty t orelse f mem ops then term_bools (term_bools acc l)b 
haftmann@23515
    69
      else insert (op aconv) t acc
chaieb@23274
    70
  | f $ a => if ty t orelse f mem ops then term_bools (term_bools acc f) a  
haftmann@23515
    71
      else insert (op aconv) t acc
chaieb@23274
    72
  | Abs p => term_bools acc (snd (variant_abs p))
chaieb@23274
    73
  | _ => if ty t orelse t mem ops then acc else insert (op aconv) t acc
haftmann@23515
    74
chaieb@23274
    75
end;
chaieb@23274
    76
chaieb@23274
    77
fun start_vs t =
haftmann@23515
    78
  let
haftmann@23515
    79
    val fs = term_frees t
haftmann@23515
    80
    val ps = term_bools [] t
haftmann@23515
    81
  in
haftmann@23693
    82
    (fs ~~ (map nat (0 upto  (length fs - 1))),
haftmann@23693
    83
      ps ~~ (map nat (0 upto  (length ps - 1))))
haftmann@23515
    84
  end;
chaieb@23274
    85
haftmann@23515
    86
fun term_of_i vs t = case t
haftmann@23515
    87
 of C i => HOLogic.mk_number HOLogic.intT i
haftmann@23515
    88
  | Bound n => (fst o the) (find_first (fn (_, m) => m = n) vs)
haftmann@23515
    89
  | Neg t' => @{term "uminus :: int => _"} $ term_of_i vs t'
haftmann@23515
    90
  | Add (t1, t2) => @{term "op +:: int => _"} $ term_of_i vs t1 $ term_of_i vs t2
haftmann@23515
    91
  | Sub (t1, t2) => Const (@{const_name "HOL.minus"}, HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $
haftmann@23515
    92
      term_of_i vs t1 $ term_of_i vs t2
haftmann@23515
    93
  | Mul (i, t2) => Const (@{const_name "HOL.times"}, HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $
haftmann@23515
    94
      HOLogic.mk_number HOLogic.intT i $ term_of_i vs t2
chaieb@24000
    95
  | Cn (n,i, t') => term_of_i vs (Add (Mul (i, Bound n), t'));
chaieb@23274
    96
haftmann@23515
    97
fun term_of_qf ps vs t = case t
haftmann@23515
    98
 of T => HOLogic.true_const 
haftmann@23515
    99
  | F => HOLogic.false_const
haftmann@23515
   100
  | Lt t' => @{term "op < :: int => _ "}$ term_of_i vs t'$ @{term "0::int"}
haftmann@23515
   101
  | Le t' => @{term "op <= :: int => _ "}$ term_of_i vs t' $ @{term "0::int"}
haftmann@23515
   102
  | Gt t' => @{term "op < :: int => _ "}$ @{term "0::int"}$ term_of_i vs t'
haftmann@23515
   103
  | Ge t' => @{term "op <= :: int => _ "}$ @{term "0::int"}$ term_of_i vs t'
haftmann@23515
   104
  | Eq t' => @{term "op = :: int => _ "}$ term_of_i vs t'$ @{term "0::int"}
haftmann@24423
   105
  | NEq t' => term_of_qf ps vs (Not(Eq t'))
haftmann@23515
   106
  | Dvd(i,t') => @{term "op dvd :: int => _ "}$ 
haftmann@23515
   107
      (HOLogic.mk_number HOLogic.intT i)$(term_of_i vs t')
haftmann@24423
   108
  | NDvd(i,t')=> term_of_qf ps vs (Not(Dvd(i,t')))
haftmann@24423
   109
  | Not t' => HOLogic.Not$(term_of_qf ps vs t')
haftmann@23515
   110
  | And(t1,t2) => HOLogic.conj$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
haftmann@23515
   111
  | Or(t1,t2) => HOLogic.disj$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
haftmann@24423
   112
  | Imp(t1,t2) => HOLogic.imp$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
haftmann@24423
   113
  | Iff(t1,t2) => HOLogic.eq_const HOLogic.boolT $ term_of_qf ps vs t1 $ term_of_qf ps vs t2
haftmann@23515
   114
  | Closed n => (fst o the) (find_first (fn (_, m) => m = n) ps)
haftmann@24423
   115
  | NClosed n => term_of_qf ps vs (Not (Closed n))
haftmann@23515
   116
  | _ => error "If this is raised, Isabelle/HOL or generate_code is inconsistent!";
chaieb@23274
   117
chaieb@23274
   118
(* The oracle *)
chaieb@23274
   119
fun cooper_oracle thy t = 
haftmann@23515
   120
  let
haftmann@23515
   121
    val (vs, ps) = start_vs t;
haftmann@23515
   122
  in HOLogic.mk_Trueprop (HOLogic.mk_eq (t, term_of_qf ps vs (pa (qf_of_term ps vs t)))) end;
chaieb@23274
   123
chaieb@23274
   124
end;