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