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