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