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