src/HOL/ex/svc_funcs.ML
author wenzelm
Thu Jul 14 19:28:18 2005 +0200 (2005-07-14)
changeset 16836 45a3dc4688bc
parent 16258 f3d913abf7e5
child 17465 93fc1211603f
permissions -rw-r--r--
improved oracle setup;
wenzelm@12869
     1
(*  Title:      HOL/Tools/svc_funcs.ML
wenzelm@12869
     2
    ID:         $Id$
wenzelm@12869
     3
    Author:     Lawrence C Paulson
wenzelm@12869
     4
    Copyright   1999  University of Cambridge
wenzelm@12869
     5
wenzelm@12869
     6
Translation functions for the interface to SVC
wenzelm@12869
     7
wenzelm@12869
     8
Based upon the work of Søren T. Heilmann
wenzelm@12869
     9
wenzelm@12869
    10
Integers and naturals are translated as follows:
wenzelm@12869
    11
  In a positive context, replace x<y by x+1<=y
wenzelm@12869
    12
  In a negative context, replace x<=y by x<y+1
wenzelm@12869
    13
  In a negative context, replace x=y by x<y+1 & y<x+1
wenzelm@12869
    14
Biconditionals (if-and-only-iff) are expanded if they require such translations
wenzelm@12869
    15
  in either operand.
wenzelm@12869
    16
wenzelm@12869
    17
For each variable of type nat, an assumption is added that it is non-negative.
wenzelm@12869
    18
*)
wenzelm@12869
    19
wenzelm@12869
    20
structure Svc =
wenzelm@12869
    21
struct
wenzelm@12869
    22
 val trace = ref false;
wenzelm@12869
    23
wenzelm@12869
    24
 datatype expr =
wenzelm@12869
    25
     Buildin of string * expr list
wenzelm@12869
    26
   | Interp of string * expr list
wenzelm@12869
    27
   | UnInterp of string * expr list
wenzelm@16836
    28
   | FalseExpr
wenzelm@12869
    29
   | TrueExpr
paulson@15965
    30
   | Int of IntInf.int
paulson@15965
    31
   | Rat of IntInf.int * IntInf.int;
wenzelm@12869
    32
wenzelm@12869
    33
 open BasisLibrary
wenzelm@12869
    34
wenzelm@16836
    35
 fun signedInt i =
paulson@15965
    36
     if i < 0 then "-" ^ IntInf.toString (~i)
paulson@15965
    37
     else IntInf.toString i;
wenzelm@16836
    38
wenzelm@12869
    39
 fun is_intnat T = T = HOLogic.intT orelse T = HOLogic.natT;
wenzelm@16836
    40
wenzelm@12869
    41
 fun is_numeric T = is_intnat T orelse T = HOLogic.realT;
wenzelm@16836
    42
wenzelm@12869
    43
 fun is_numeric_op T = is_numeric (domain_type T);
wenzelm@12869
    44
wenzelm@12869
    45
 fun toString t =
wenzelm@16836
    46
     let fun ue (Buildin(s, l)) =
wenzelm@16836
    47
             "(" ^ s ^ (Library.foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ ") "
wenzelm@16836
    48
           | ue (Interp(s, l)) =
wenzelm@16836
    49
             "{" ^ s ^ (Library.foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ "} "
wenzelm@16836
    50
           | ue (UnInterp(s, l)) =
wenzelm@16836
    51
             "(" ^ s ^ (Library.foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ ") "
wenzelm@16836
    52
           | ue (FalseExpr) = "FALSE "
wenzelm@16836
    53
           | ue (TrueExpr)  = "TRUE "
wenzelm@16836
    54
           | ue (Int i)     = (signedInt i) ^ " "
wenzelm@16836
    55
           | ue (Rat(i, j)) = (signedInt i) ^ "|" ^ (signedInt j) ^ " "
wenzelm@12869
    56
     in
wenzelm@16836
    57
         ue t
wenzelm@12869
    58
     end;
wenzelm@12869
    59
wenzelm@16836
    60
 fun valid e =
wenzelm@16836
    61
  let val svc_home = getenv "SVC_HOME"
wenzelm@12869
    62
      val svc_machine = getenv "SVC_MACHINE"
wenzelm@12869
    63
      val check_valid = if svc_home = ""
wenzelm@16836
    64
                        then error "Environment variable SVC_HOME not set"
wenzelm@16836
    65
                        else if svc_machine = ""
wenzelm@16836
    66
                        then error "Environment variable SVC_MACHINE not set"
wenzelm@16836
    67
                        else svc_home ^ "/" ^ svc_machine ^ "/bin/check_valid"
wenzelm@12869
    68
      val svc_input = toString e
wenzelm@12869
    69
      val _ = if !trace then tracing ("Calling SVC:\n" ^ svc_input) else ()
wenzelm@12869
    70
      val svc_input_file  = File.tmp_path (Path.basic "SVM_in");
wenzelm@12869
    71
      val svc_output_file = File.tmp_path (Path.basic "SVM_out");
wenzelm@12869
    72
      val _ = (File.write svc_input_file svc_input;
wenzelm@16836
    73
               execute (check_valid ^ " -dump-result " ^
wenzelm@16836
    74
                        File.shell_path svc_output_file ^
wenzelm@16836
    75
                        " " ^ File.shell_path svc_input_file ^
wenzelm@16836
    76
                        ">/dev/null 2>&1"))
wenzelm@12869
    77
      val svc_output =
wenzelm@12869
    78
        (case Library.try File.read svc_output_file of
skalberg@15531
    79
          SOME out => out
skalberg@15531
    80
        | NONE => error "SVC returned no output");
wenzelm@12869
    81
  in
wenzelm@12869
    82
      if ! trace then tracing ("SVC Returns:\n" ^ svc_output)
wenzelm@12869
    83
      else (File.rm svc_input_file; File.rm svc_output_file);
wenzelm@12869
    84
      String.isPrefix "VALID" svc_output
wenzelm@12869
    85
  end
wenzelm@12869
    86
wenzelm@16836
    87
 fun fail t = raise TERM ("SVC oracle", [t]);
wenzelm@12869
    88
wenzelm@12869
    89
 fun apply c args =
wenzelm@12869
    90
     let val (ts, bs) = ListPair.unzip args
wenzelm@12869
    91
     in  (list_comb(c,ts), exists I bs)  end;
wenzelm@12869
    92
wenzelm@12869
    93
 (*Determining whether the biconditionals must be unfolded: if there are
wenzelm@12869
    94
   int or nat comparisons below*)
wenzelm@12869
    95
 val iff_tag =
wenzelm@12869
    96
   let fun tag t =
wenzelm@16836
    97
         let val (c,ts) = strip_comb t
wenzelm@16836
    98
         in  case c of
wenzelm@16836
    99
             Const("op &", _)   => apply c (map tag ts)
wenzelm@16836
   100
           | Const("op |", _)   => apply c (map tag ts)
wenzelm@16836
   101
           | Const("op -->", _) => apply c (map tag ts)
wenzelm@16836
   102
           | Const("Not", _)    => apply c (map tag ts)
wenzelm@16836
   103
           | Const("True", _)   => (c, false)
wenzelm@16836
   104
           | Const("False", _)  => (c, false)
wenzelm@16836
   105
           | Const("op =", Type ("fun", [T,_])) =>
wenzelm@16836
   106
                 if T = HOLogic.boolT then
wenzelm@16836
   107
                     (*biconditional: with int/nat comparisons below?*)
wenzelm@16836
   108
                     let val [t1,t2] = ts
wenzelm@16836
   109
                         val (u1,b1) = tag t1
wenzelm@16836
   110
                         and (u2,b2) = tag t2
wenzelm@16836
   111
                         val cname = if b1 orelse b2 then "unfold" else "keep"
wenzelm@16836
   112
                     in
wenzelm@16836
   113
                        (Const ("SVC_Oracle.iff_" ^ cname, dummyT) $ u1 $ u2,
wenzelm@16836
   114
                         b1 orelse b2)
wenzelm@16836
   115
                     end
wenzelm@16836
   116
                 else (*might be numeric equality*) (t, is_intnat T)
wenzelm@16836
   117
           | Const("op <", Type ("fun", [T,_]))  => (t, is_intnat T)
wenzelm@16836
   118
           | Const("op <=", Type ("fun", [T,_])) => (t, is_intnat T)
wenzelm@16836
   119
           | _ => (t, false)
wenzelm@16836
   120
         end
wenzelm@12869
   121
   in #1 o tag end;
wenzelm@12869
   122
wenzelm@12869
   123
 (*Map expression e to 0<=a --> e, where "a" is the name of a nat variable*)
wenzelm@16836
   124
 fun add_nat_var (a, e) =
wenzelm@12869
   125
     Buildin("=>", [Buildin("<=", [Int 0, UnInterp (a, [])]),
wenzelm@16836
   126
                    e]);
wenzelm@12869
   127
wenzelm@12869
   128
 fun param_string [] = ""
wenzelm@12869
   129
   | param_string is = "_" ^ space_implode "_" (map string_of_int is)
wenzelm@12869
   130
wenzelm@12869
   131
 (*Translate an Isabelle formula into an SVC expression
wenzelm@12869
   132
   pos ["positive"]: true if an assumption, false if a goal*)
wenzelm@12869
   133
 fun expr_of pos t =
wenzelm@12869
   134
  let
wenzelm@12869
   135
    val params = rev (rename_wrt_term t (Term.strip_all_vars t))
wenzelm@12869
   136
    and body   = Term.strip_all_body t
wenzelm@12869
   137
    val nat_vars = ref ([] : string list)
wenzelm@12869
   138
    (*translation of a variable: record all natural numbers*)
wenzelm@12869
   139
    fun trans_var (a,T,is) =
wenzelm@16836
   140
        (if T = HOLogic.natT then nat_vars := (a ins_string (!nat_vars))
wenzelm@16836
   141
                             else ();
wenzelm@12869
   142
         UnInterp (a ^ param_string is, []))
wenzelm@12869
   143
    (*A variable, perhaps applied to a series of parameters*)
wenzelm@12869
   144
    fun var (Free(a,T), is)      = trans_var ("F_" ^ a, T, is)
wenzelm@12869
   145
      | var (Var((a, 0), T), is) = trans_var (a, T, is)
wenzelm@16836
   146
      | var (Bound i, is)        =
wenzelm@12869
   147
          let val (a,T) = List.nth (params, i)
wenzelm@16836
   148
          in  trans_var ("B_" ^ a, T, is)  end
wenzelm@12869
   149
      | var (t $ Bound i, is)    = var(t,i::is)
wenzelm@12869
   150
            (*removing a parameter from a Var: the bound var index will
wenzelm@12869
   151
               become part of the Var's name*)
wenzelm@16836
   152
      | var (t,_) = fail t;
wenzelm@12869
   153
    (*translation of a literal*)
wenzelm@12869
   154
    fun lit (Const("Numeral.number_of", _) $ w) =
wenzelm@12869
   155
          (HOLogic.dest_binum w handle TERM _ => raise Match)
wenzelm@12869
   156
      | lit (Const("0", _)) = 0
wenzelm@12869
   157
      | lit (Const("1", _)) = 1
wenzelm@12869
   158
    (*translation of a literal expression [no variables]*)
wenzelm@16836
   159
    fun litExp (Const("op +", T) $ x $ y) =
wenzelm@16836
   160
          if is_numeric_op T then (litExp x) + (litExp y)
wenzelm@16836
   161
          else fail t
wenzelm@16836
   162
      | litExp (Const("op -", T) $ x $ y) =
wenzelm@16836
   163
          if is_numeric_op T then (litExp x) - (litExp y)
wenzelm@16836
   164
          else fail t
wenzelm@16836
   165
      | litExp (Const("op *", T) $ x $ y) =
wenzelm@16836
   166
          if is_numeric_op T then (litExp x) * (litExp y)
wenzelm@16836
   167
          else fail t
wenzelm@16836
   168
      | litExp (Const("uminus", T) $ x)   =
wenzelm@16836
   169
          if is_numeric_op T then ~(litExp x)
wenzelm@16836
   170
          else fail t
wenzelm@16836
   171
      | litExp t = lit t
wenzelm@16836
   172
                   handle Match => fail t
wenzelm@12869
   173
    (*translation of a real/rational expression*)
wenzelm@12869
   174
    fun suc t = Interp("+", [Int 1, t])
wenzelm@12869
   175
    fun tm (Const("Suc", T) $ x) = suc (tm x)
wenzelm@16836
   176
      | tm (Const("op +", T) $ x $ y) =
wenzelm@16836
   177
          if is_numeric_op T then Interp("+", [tm x, tm y])
wenzelm@16836
   178
          else fail t
wenzelm@16836
   179
      | tm (Const("op -", T) $ x $ y) =
wenzelm@16836
   180
          if is_numeric_op T then
wenzelm@16836
   181
              Interp("+", [tm x, Interp("*", [Int ~1, tm y])])
wenzelm@16836
   182
          else fail t
wenzelm@16836
   183
      | tm (Const("op *", T) $ x $ y) =
wenzelm@16836
   184
          if is_numeric_op T then Interp("*", [tm x, tm y])
wenzelm@16836
   185
          else fail t
wenzelm@16836
   186
      | tm (Const("RealDef.rinv", T) $ x) =
wenzelm@16836
   187
          if domain_type T = HOLogic.realT then
wenzelm@16836
   188
              Rat(1, litExp x)
wenzelm@16836
   189
          else fail t
wenzelm@16836
   190
      | tm (Const("uminus", T) $ x) =
wenzelm@16836
   191
          if is_numeric_op T then Interp("*", [Int ~1, tm x])
wenzelm@16836
   192
          else fail t
wenzelm@16836
   193
      | tm t = Int (lit t)
wenzelm@16836
   194
               handle Match => var (t,[])
wenzelm@12869
   195
    (*translation of a formula*)
wenzelm@16836
   196
    and fm pos (Const("op &", _) $ p $ q) =
wenzelm@16836
   197
            Buildin("AND", [fm pos p, fm pos q])
wenzelm@16836
   198
      | fm pos (Const("op |", _) $ p $ q) =
wenzelm@16836
   199
            Buildin("OR", [fm pos p, fm pos q])
wenzelm@16836
   200
      | fm pos (Const("op -->", _) $ p $ q) =
wenzelm@16836
   201
            Buildin("=>", [fm (not pos) p, fm pos q])
wenzelm@16836
   202
      | fm pos (Const("Not", _) $ p) =
wenzelm@16836
   203
            Buildin("NOT", [fm (not pos) p])
wenzelm@12869
   204
      | fm pos (Const("True", _)) = TrueExpr
wenzelm@12869
   205
      | fm pos (Const("False", _)) = FalseExpr
wenzelm@16836
   206
      | fm pos (Const("SVC_Oracle.iff_keep", _) $ p $ q) =
wenzelm@16836
   207
             (*polarity doesn't matter*)
wenzelm@16836
   208
            Buildin("=", [fm pos p, fm pos q])
wenzelm@16836
   209
      | fm pos (Const("SVC_Oracle.iff_unfold", _) $ p $ q) =
wenzelm@16836
   210
            Buildin("AND",   (*unfolding uses both polarities*)
wenzelm@16836
   211
                         [Buildin("=>", [fm (not pos) p, fm pos q]),
wenzelm@16836
   212
                          Buildin("=>", [fm (not pos) q, fm pos p])])
wenzelm@16836
   213
      | fm pos (t as Const("op =", Type ("fun", [T,_])) $ x $ y) =
wenzelm@16836
   214
            let val tx = tm x and ty = tm y
wenzelm@16836
   215
                in if pos orelse T = HOLogic.realT then
wenzelm@16836
   216
                       Buildin("=", [tx, ty])
wenzelm@16836
   217
                   else if is_intnat T then
wenzelm@16836
   218
                       Buildin("AND",
wenzelm@16836
   219
                                    [Buildin("<", [tx, suc ty]),
wenzelm@16836
   220
                                     Buildin("<", [ty, suc tx])])
wenzelm@16836
   221
                   else fail t
wenzelm@16836
   222
            end
wenzelm@16836
   223
        (*inequalities: possible types are nat, int, real*)
wenzelm@16836
   224
      | fm pos (t as Const("op <",  Type ("fun", [T,_])) $ x $ y) =
wenzelm@16836
   225
            if not pos orelse T = HOLogic.realT then
wenzelm@16836
   226
                Buildin("<", [tm x, tm y])
wenzelm@16836
   227
            else if is_intnat T then
wenzelm@16836
   228
                Buildin("<=", [suc (tm x), tm y])
wenzelm@16836
   229
            else fail t
wenzelm@16836
   230
      | fm pos (t as Const("op <=",  Type ("fun", [T,_])) $ x $ y) =
wenzelm@16836
   231
            if pos orelse T = HOLogic.realT then
wenzelm@16836
   232
                Buildin("<=", [tm x, tm y])
wenzelm@16836
   233
            else if is_intnat T then
wenzelm@16836
   234
                Buildin("<", [tm x, suc (tm y)])
wenzelm@16836
   235
            else fail t
wenzelm@12869
   236
      | fm pos t = var(t,[]);
wenzelm@12869
   237
      (*entry point, and translation of a meta-formula*)
wenzelm@12869
   238
      fun mt pos ((c as Const("Trueprop", _)) $ p) = fm pos (iff_tag p)
wenzelm@16836
   239
        | mt pos ((c as Const("==>", _)) $ p $ q) =
wenzelm@16836
   240
            Buildin("=>", [mt (not pos) p, mt pos q])
wenzelm@16836
   241
        | mt pos t = fm pos (iff_tag t)  (*it might be a formula*)
wenzelm@12869
   242
wenzelm@12869
   243
      val body_e = mt pos body  (*evaluate now to assign into !nat_vars*)
wenzelm@16836
   244
  in
wenzelm@16836
   245
     foldr add_nat_var body_e (!nat_vars)
wenzelm@12869
   246
  end;
wenzelm@12869
   247
wenzelm@12869
   248
wenzelm@12869
   249
 (*The oracle proves the given formula t, if possible*)
wenzelm@16836
   250
 fun oracle thy t =
wenzelm@16836
   251
  (conditional (! trace) (fn () =>
wenzelm@16836
   252
    tracing ("SVC oracle: problem is\n" ^ Sign.string_of_term thy t));
wenzelm@16836
   253
  if valid (expr_of false t) then t else fail t);
wenzelm@12869
   254
wenzelm@12869
   255
end;