moved SVC stuff to ex;
authorwenzelm
Tue Feb 05 23:18:08 2002 +0100 (2002-02-05)
changeset 12869f362c0323d92
parent 12868 cdf338ef5fad
child 12870 3905bc0e9002
moved SVC stuff to ex;
src/HOL/IsaMakefile
src/HOL/PreList.thy
src/HOL/SVC_Oracle.ML
src/HOL/SVC_Oracle.thy
src/HOL/Tools/svc_funcs.ML
src/HOL/ex/ROOT.ML
src/HOL/ex/SVC_Oracle.ML
src/HOL/ex/SVC_Oracle.thy
src/HOL/ex/svc_funcs.ML
     1.1 --- a/src/HOL/IsaMakefile	Tue Feb 05 15:51:28 2002 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Tue Feb 05 23:18:08 2002 +0100
     1.3 @@ -92,15 +92,13 @@
     1.4    Option.ML Option.thy Power.ML Power.thy PreList.thy \
     1.5    Product_Type.ML Product_Type.thy ROOT.ML Recdef.thy Record.thy \
     1.6    Relation.ML Relation.thy Relation_Power.ML Relation_Power.thy \
     1.7 -  SVC_Oracle.ML SVC_Oracle.thy Set.ML Set.thy SetInterval.ML \
     1.8 -  SetInterval.thy Sum_Type.ML Sum_Type.thy \
     1.9 +  Set.ML Set.thy SetInterval.ML SetInterval.thy Sum_Type.ML Sum_Type.thy \
    1.10    Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML \
    1.11    Tools/datatype_codegen.ML Tools/datatype_package.ML Tools/datatype_prop.ML \
    1.12    Tools/datatype_rep_proofs.ML \
    1.13    Tools/inductive_package.ML Tools/inductive_codegen.ML Tools/meson.ML Tools/numeral_syntax.ML \
    1.14    Tools/primrec_package.ML Tools/recdef_package.ML Tools/recfun_codegen.ML \
    1.15 -  Tools/record_package.ML Tools/split_rule.ML \
    1.16 -  Tools/svc_funcs.ML Tools/typedef_package.ML \
    1.17 +  Tools/record_package.ML Tools/split_rule.ML Tools/typedef_package.ML \
    1.18    Transitive_Closure.thy Transitive_Closure.ML Typedef.thy \
    1.19    Wellfounded_Recursion.ML Wellfounded_Recursion.thy Wellfounded_Relations.ML \
    1.20    Wellfounded_Relations.thy arith_data.ML blastdata.ML cladata.ML \
    1.21 @@ -553,10 +551,10 @@
    1.22    ex/MT.ML ex/MT.thy ex/MonoidGroup.thy ex/Multiquote.thy \
    1.23    ex/NatSum.thy ex/PER.thy ex/Primrec.thy ex/Puzzle.ML ex/Puzzle.thy \
    1.24    ex/Qsort.ML ex/Qsort.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy \
    1.25 -  ex/Ring.ML ex/Ring.thy ex/StringEx.thy ex/Tarski.ML \
    1.26 -  ex/Tarski.thy ex/Tuple.thy ex/cla.ML ex/mesontest.ML ex/mesontest2.ML \
    1.27 -  ex/mesontest2.thy ex/set.ML ex/set.thy ex/svc_test.ML ex/svc_test.thy \
    1.28 -  ex/document/root.bib ex/document/root.tex
    1.29 +  ex/Ring.ML ex/Ring.thy ex/StringEx.thy ex/SVC_Oracle.ML ex/SVC_Oracle.thy \
    1.30 +  ex/Tarski.ML ex/Tarski.thy ex/Tuple.thy ex/cla.ML ex/mesontest.ML \
    1.31 +  ex/mesontest2.ML ex/mesontest2.thy ex/set.ML ex/set.thy ex/svc_funcs.ML \
    1.32 +  ex/svc_test.ML ex/svc_test.thy ex/document/root.bib ex/document/root.tex
    1.33  	@$(ISATOOL) usedir $(OUT)/HOL ex
    1.34  
    1.35  
     2.1 --- a/src/HOL/PreList.thy	Tue Feb 05 15:51:28 2002 +0100
     2.2 +++ b/src/HOL/PreList.thy	Tue Feb 05 23:18:08 2002 +0100
     2.3 @@ -9,7 +9,7 @@
     2.4  
     2.5  theory PreList =
     2.6    Option + Wellfounded_Relations + NatSimprocs + Recdef + Record +
     2.7 -  Relation_Power + SVC_Oracle:
     2.8 +  Relation_Power:
     2.9  
    2.10  (*belongs to theory Divides*)
    2.11  declare dvdI [intro?]  dvdE [elim?]  dvd_trans [trans]
     3.1 --- a/src/HOL/SVC_Oracle.ML	Tue Feb 05 15:51:28 2002 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,113 +0,0 @@
     3.4 -(*  Title:      HOL/SVC_Oracle.ML
     3.5 -    ID:         $Id$
     3.6 -    Author:     Lawrence C Paulson
     3.7 -    Copyright   1999  University of Cambridge
     3.8 -
     3.9 -Installing the oracle for SVC (Stanford Validity Checker)
    3.10 -
    3.11 -The following code merely CALLS the oracle; 
    3.12 -  the soundness-critical functions are at HOL/Tools/svc_funcs.ML
    3.13 -
    3.14 -Based upon the work of Søren T. Heilmann
    3.15 -*)
    3.16 -
    3.17 -
    3.18 -(*Generalize an Isabelle formula, replacing by Vars
    3.19 -  all subterms not intelligible to SVC.*)
    3.20 -fun svc_abstract t =
    3.21 -  let
    3.22 -    (*The oracle's result is given to the subgoal using compose_tac because
    3.23 -      its premises are matched against the assumptions rather than used
    3.24 -      to make subgoals.  Therefore , abstraction must copy the parameters
    3.25 -      precisely and make them available to all generated Vars.*)
    3.26 -    val params = Term.strip_all_vars t
    3.27 -    and body   = Term.strip_all_body t
    3.28 -    val Us = map #2 params
    3.29 -    val nPar = length params
    3.30 -    val vname = ref "V_a"
    3.31 -    val pairs = ref ([] : (term*term) list)
    3.32 -    fun insert t = 
    3.33 -	let val T = fastype_of t
    3.34 -            val v = Unify.combound (Var ((!vname,0), Us--->T),
    3.35 -				    0, nPar)
    3.36 -	in  vname := bump_string (!vname); 
    3.37 -	    pairs := (t, v) :: !pairs;
    3.38 -	    v
    3.39 -	end;
    3.40 -    fun replace t = 
    3.41 -	case t of
    3.42 -	    Free _  => t  (*but not existing Vars, lest the names clash*)
    3.43 -	  | Bound _ => t
    3.44 -	  | _ => (case gen_assoc Pattern.aeconv (!pairs, t) of
    3.45 -		      Some v => v
    3.46 -		    | None   => insert t)
    3.47 -    (*abstraction of a numeric literal*)
    3.48 -    fun lit (t as Const("0", _)) = t
    3.49 -      | lit (t as Const("1", _)) = t
    3.50 -      | lit (t as Const("Numeral.number_of", _) $ w) = t
    3.51 -      | lit t = replace t
    3.52 -    (*abstraction of a real/rational expression*)
    3.53 -    fun rat ((c as Const("op +", _)) $ x $ y) = c $ (rat x) $ (rat y)
    3.54 -      | rat ((c as Const("op -", _)) $ x $ y) = c $ (rat x) $ (rat y)
    3.55 -      | rat ((c as Const("op /", _)) $ x $ y) = c $ (rat x) $ (rat y)
    3.56 -      | rat ((c as Const("op *", _)) $ x $ y) = c $ (rat x) $ (rat y)
    3.57 -      | rat ((c as Const("uminus", _)) $ x) = c $ (rat x)
    3.58 -      | rat t = lit t
    3.59 -    (*abstraction of an integer expression: no div, mod*)
    3.60 -    fun int ((c as Const("op +", _)) $ x $ y) = c $ (int x) $ (int y)
    3.61 -      | int ((c as Const("op -", _)) $ x $ y) = c $ (int x) $ (int y)
    3.62 -      | int ((c as Const("op *", _)) $ x $ y) = c $ (int x) $ (int y)
    3.63 -      | int ((c as Const("uminus", _)) $ x) = c $ (int x)
    3.64 -      | int t = lit t
    3.65 -    (*abstraction of a natural number expression: no minus*)
    3.66 -    fun nat ((c as Const("op +", _)) $ x $ y) = c $ (nat x) $ (nat y)
    3.67 -      | nat ((c as Const("op *", _)) $ x $ y) = c $ (nat x) $ (nat y)
    3.68 -      | nat ((c as Const("Suc", _)) $ x) = c $ (nat x)
    3.69 -      | nat t = lit t
    3.70 -    (*abstraction of a relation: =, <, <=*)
    3.71 -    fun rel (T, c $ x $ y) =
    3.72 -	    if T = HOLogic.realT then c $ (rat x) $ (rat y)
    3.73 -	    else if T = HOLogic.intT then c $ (int x) $ (int y)
    3.74 -	    else if T = HOLogic.natT then c $ (nat x) $ (nat y)
    3.75 -	    else if T = HOLogic.boolT then c $ (fm x) $ (fm y)
    3.76 -	    else replace (c $ x $ y)   (*non-numeric comparison*)
    3.77 -    (*abstraction of a formula*)
    3.78 -    and fm ((c as Const("op &", _)) $ p $ q) = c $ (fm p) $ (fm q)
    3.79 -      | fm ((c as Const("op |", _)) $ p $ q) = c $ (fm p) $ (fm q)
    3.80 -      | fm ((c as Const("op -->", _)) $ p $ q) = c $ (fm p) $ (fm q)
    3.81 -      | fm ((c as Const("Not", _)) $ p) = c $ (fm p)
    3.82 -      | fm ((c as Const("True", _))) = c
    3.83 -      | fm ((c as Const("False", _))) = c
    3.84 -      | fm (t as Const("op =",  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
    3.85 -      | fm (t as Const("op <",  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
    3.86 -      | fm (t as Const("op <=", Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
    3.87 -      | fm t = replace t
    3.88 -    (*entry point, and abstraction of a meta-formula*)
    3.89 -    fun mt ((c as Const("Trueprop", _)) $ p) = c $ (fm p)
    3.90 -      | mt ((c as Const("==>", _)) $ p $ q)  = c $ (mt p) $ (mt q)
    3.91 -      | mt t = fm t  (*it might be a formula*)
    3.92 -  in (list_all (params, mt body), !pairs) end;
    3.93 -
    3.94 -
    3.95 -(*Present the entire subgoal to the oracle, assumptions and all, but possibly
    3.96 -  abstracted.  Use via compose_tac, which performs no lifting but will
    3.97 -  instantiate variables.*)
    3.98 -local val svc_thy = the_context () in
    3.99 -
   3.100 -fun svc_tac i st = 
   3.101 -  let val prem = BasisLibrary.List.nth (prems_of st, i-1)
   3.102 -      val (absPrem, _) = svc_abstract prem
   3.103 -      val th = invoke_oracle svc_thy "svc_oracle"
   3.104 -	             (#sign (rep_thm st), Svc.OracleExn absPrem)
   3.105 -   in 
   3.106 -      compose_tac (false, th, 0) i st
   3.107 -   end 
   3.108 -   handle Svc.OracleExn _ => Seq.empty
   3.109 -	| Subscript       => Seq.empty;
   3.110 -
   3.111 -end;
   3.112 -
   3.113 -
   3.114 -(*check if user has SVC installed*)
   3.115 -fun svc_enabled () = getenv "SVC_HOME" <> "";
   3.116 -fun if_svc_enabled f x = if svc_enabled () then f x else ();
     4.1 --- a/src/HOL/SVC_Oracle.thy	Tue Feb 05 15:51:28 2002 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,22 +0,0 @@
     4.4 -(*  Title:      HOL/SVC_Oracle.thy
     4.5 -    ID:         $Id$
     4.6 -    Author:     Lawrence C Paulson
     4.7 -    Copyright   1999  University of Cambridge
     4.8 -
     4.9 -Installing the oracle for SVC (Stanford Validity Checker)
    4.10 -
    4.11 -Based upon the work of Søren T. Heilmann
    4.12 -*)
    4.13 -
    4.14 -theory SVC_Oracle = NatBin (** + Real??**)
    4.15 -files "Tools/svc_funcs.ML":
    4.16 -
    4.17 -consts
    4.18 -  (*reserved for the oracle*)
    4.19 -  iff_keep :: "[bool, bool] => bool"
    4.20 -  iff_unfold :: "[bool, bool] => bool"
    4.21 -
    4.22 -oracle
    4.23 -  svc_oracle = Svc.oracle
    4.24 -
    4.25 -end
     5.1 --- a/src/HOL/Tools/svc_funcs.ML	Tue Feb 05 15:51:28 2002 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,260 +0,0 @@
     5.4 -(*  Title:      HOL/Tools/svc_funcs.ML
     5.5 -    ID:         $Id$
     5.6 -    Author:     Lawrence C Paulson
     5.7 -    Copyright   1999  University of Cambridge
     5.8 -
     5.9 -Translation functions for the interface to SVC
    5.10 -
    5.11 -Based upon the work of Søren T. Heilmann
    5.12 -
    5.13 -Integers and naturals are translated as follows:
    5.14 -  In a positive context, replace x<y by x+1<=y
    5.15 -  In a negative context, replace x<=y by x<y+1
    5.16 -  In a negative context, replace x=y by x<y+1 & y<x+1
    5.17 -Biconditionals (if-and-only-iff) are expanded if they require such translations
    5.18 -  in either operand.
    5.19 -
    5.20 -For each variable of type nat, an assumption is added that it is non-negative.
    5.21 -*)
    5.22 -
    5.23 -structure Svc =
    5.24 -struct
    5.25 - val trace = ref false;
    5.26 -
    5.27 - datatype expr =
    5.28 -     Buildin of string * expr list
    5.29 -   | Interp of string * expr list
    5.30 -   | UnInterp of string * expr list
    5.31 -   | FalseExpr 
    5.32 -   | TrueExpr
    5.33 -   | Int of int
    5.34 -   | Rat of int * int;
    5.35 -
    5.36 - open BasisLibrary
    5.37 -
    5.38 - fun signedInt i = 
    5.39 -     if i < 0 then "-" ^ Int.toString (~i)
    5.40 -     else Int.toString i;
    5.41 -	 
    5.42 - fun is_intnat T = T = HOLogic.intT orelse T = HOLogic.natT;
    5.43 - 
    5.44 - fun is_numeric T = is_intnat T orelse T = HOLogic.realT;
    5.45 - 
    5.46 - fun is_numeric_op T = is_numeric (domain_type T);
    5.47 -
    5.48 - fun toString t =
    5.49 -     let fun ue (Buildin(s, l)) = 
    5.50 -	     "(" ^ s ^ (foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ ") "
    5.51 -	   | ue (Interp(s, l)) = 
    5.52 -	     "{" ^ s ^ (foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ "} "
    5.53 -	   | ue (UnInterp(s, l)) = 
    5.54 -	     "(" ^ s ^ (foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ ") "
    5.55 -	   | ue (FalseExpr) = "FALSE "
    5.56 -	   | ue (TrueExpr)  = "TRUE "
    5.57 -	   | ue (Int i)     = (signedInt i) ^ " "
    5.58 -	   | ue (Rat(i, j)) = (signedInt i) ^ "|" ^ (signedInt j) ^ " "
    5.59 -     in
    5.60 -	 ue t
    5.61 -     end;
    5.62 -
    5.63 - fun valid e = 
    5.64 -  let val svc_home = getenv "SVC_HOME" 
    5.65 -      val svc_machine = getenv "SVC_MACHINE"
    5.66 -      val check_valid = if svc_home = ""
    5.67 -	                then error "Environment variable SVC_HOME not set"
    5.68 -			else if svc_machine = ""
    5.69 -	                then error "Environment variable SVC_MACHINE not set"
    5.70 -			else svc_home ^ "/" ^ svc_machine ^ "/bin/check_valid"
    5.71 -      val svc_input = toString e
    5.72 -      val _ = if !trace then tracing ("Calling SVC:\n" ^ svc_input) else ()
    5.73 -      val svc_input_file  = File.tmp_path (Path.basic "SVM_in");
    5.74 -      val svc_output_file = File.tmp_path (Path.basic "SVM_out");
    5.75 -      val _ = (File.write svc_input_file svc_input;
    5.76 -	       execute (check_valid ^ " -dump-result " ^ 
    5.77 -			File.sysify_path svc_output_file ^
    5.78 -			" " ^ File.sysify_path svc_input_file ^ 
    5.79 -			"> /dev/null 2>&1"))
    5.80 -      val svc_output =
    5.81 -        (case Library.try File.read svc_output_file of
    5.82 -          Some out => out
    5.83 -        | None => error "SVC returned no output");
    5.84 -  in
    5.85 -      if ! trace then tracing ("SVC Returns:\n" ^ svc_output)
    5.86 -      else (File.rm svc_input_file; File.rm svc_output_file);
    5.87 -      String.isPrefix "VALID" svc_output
    5.88 -  end
    5.89 -
    5.90 - (*New exception constructor for passing arguments to the oracle*)
    5.91 - exception OracleExn of term;
    5.92 -
    5.93 - fun apply c args =
    5.94 -     let val (ts, bs) = ListPair.unzip args
    5.95 -     in  (list_comb(c,ts), exists I bs)  end;
    5.96 -
    5.97 - (*Determining whether the biconditionals must be unfolded: if there are
    5.98 -   int or nat comparisons below*)
    5.99 - val iff_tag =
   5.100 -   let fun tag t =
   5.101 -	 let val (c,ts) = strip_comb t
   5.102 -	 in  case c of
   5.103 -	     Const("op &", _)   => apply c (map tag ts)
   5.104 -	   | Const("op |", _)   => apply c (map tag ts)
   5.105 -	   | Const("op -->", _) => apply c (map tag ts)
   5.106 -	   | Const("Not", _)    => apply c (map tag ts)
   5.107 -	   | Const("True", _)   => (c, false)
   5.108 -	   | Const("False", _)  => (c, false)
   5.109 -	   | Const("op =", Type ("fun", [T,_])) => 
   5.110 -		 if T = HOLogic.boolT then
   5.111 -		     (*biconditional: with int/nat comparisons below?*)
   5.112 -		     let val [t1,t2] = ts
   5.113 -			 val (u1,b1) = tag t1
   5.114 -			 and (u2,b2) = tag t2
   5.115 -			 val cname = if b1 orelse b2 then "unfold" else "keep"
   5.116 -		     in 
   5.117 -			(Const ("SVC_Oracle.iff_" ^ cname, dummyT) $ u1 $ u2,
   5.118 -			 b1 orelse b2)
   5.119 -		     end
   5.120 -		 else (*might be numeric equality*) (t, is_intnat T)
   5.121 -	   | Const("op <", Type ("fun", [T,_]))  => (t, is_intnat T)
   5.122 -	   | Const("op <=", Type ("fun", [T,_])) => (t, is_intnat T)
   5.123 -	   | _ => (t, false)
   5.124 -	 end
   5.125 -   in #1 o tag end;
   5.126 -
   5.127 - (*Map expression e to 0<=a --> e, where "a" is the name of a nat variable*)
   5.128 - fun add_nat_var (a, e) = 
   5.129 -     Buildin("=>", [Buildin("<=", [Int 0, UnInterp (a, [])]),
   5.130 -		    e]);
   5.131 -
   5.132 - fun param_string [] = ""
   5.133 -   | param_string is = "_" ^ space_implode "_" (map string_of_int is)
   5.134 -
   5.135 - (*Translate an Isabelle formula into an SVC expression
   5.136 -   pos ["positive"]: true if an assumption, false if a goal*)
   5.137 - fun expr_of pos t =
   5.138 -  let
   5.139 -    val params = rev (rename_wrt_term t (Term.strip_all_vars t))
   5.140 -    and body   = Term.strip_all_body t
   5.141 -    val nat_vars = ref ([] : string list)
   5.142 -    (*translation of a variable: record all natural numbers*)
   5.143 -    fun trans_var (a,T,is) =
   5.144 -	(if T = HOLogic.natT then nat_vars := (a ins_string (!nat_vars))
   5.145 -	                     else ();
   5.146 -         UnInterp (a ^ param_string is, []))
   5.147 -    (*A variable, perhaps applied to a series of parameters*)
   5.148 -    fun var (Free(a,T), is)      = trans_var ("F_" ^ a, T, is)
   5.149 -      | var (Var((a, 0), T), is) = trans_var (a, T, is)
   5.150 -      | var (Bound i, is)        = 
   5.151 -          let val (a,T) = List.nth (params, i)
   5.152 -	  in  trans_var ("B_" ^ a, T, is)  end
   5.153 -      | var (t $ Bound i, is)    = var(t,i::is)
   5.154 -            (*removing a parameter from a Var: the bound var index will
   5.155 -               become part of the Var's name*)
   5.156 -      | var (t,_) = raise OracleExn t;
   5.157 -    (*translation of a literal*)
   5.158 -    fun lit (Const("Numeral.number_of", _) $ w) =
   5.159 -          (HOLogic.dest_binum w handle TERM _ => raise Match)
   5.160 -      | lit (Const("0", _)) = 0
   5.161 -      | lit (Const("1", _)) = 1
   5.162 -    (*translation of a literal expression [no variables]*)
   5.163 -    fun litExp (Const("op +", T) $ x $ y) = 
   5.164 -	  if is_numeric_op T then (litExp x) + (litExp y)
   5.165 -          else raise OracleExn t
   5.166 -      | litExp (Const("op -", T) $ x $ y) = 
   5.167 -	  if is_numeric_op T then (litExp x) - (litExp y)
   5.168 -          else raise OracleExn t
   5.169 -      | litExp (Const("op *", T) $ x $ y) = 
   5.170 -	  if is_numeric_op T then (litExp x) * (litExp y)
   5.171 -          else raise OracleExn t
   5.172 -      | litExp (Const("uminus", T) $ x)   = 
   5.173 -	  if is_numeric_op T then ~(litExp x)
   5.174 -          else raise OracleExn t
   5.175 -      | litExp t = lit t 
   5.176 -		   handle Match => raise OracleExn t
   5.177 -    (*translation of a real/rational expression*)
   5.178 -    fun suc t = Interp("+", [Int 1, t])
   5.179 -    fun tm (Const("Suc", T) $ x) = suc (tm x)
   5.180 -      | tm (Const("op +", T) $ x $ y) = 
   5.181 -	  if is_numeric_op T then Interp("+", [tm x, tm y])
   5.182 -          else raise OracleExn t
   5.183 -      | tm (Const("op -", T) $ x $ y) = 
   5.184 -	  if is_numeric_op T then 
   5.185 -	      Interp("+", [tm x, Interp("*", [Int ~1, tm y])])
   5.186 -          else raise OracleExn t
   5.187 -      | tm (Const("op *", T) $ x $ y) = 
   5.188 -	  if is_numeric_op T then Interp("*", [tm x, tm y])
   5.189 -          else raise OracleExn t
   5.190 -      | tm (Const("RealDef.rinv", T) $ x) = 
   5.191 -	  if domain_type T = HOLogic.realT then 
   5.192 -	      Rat(1, litExp x)
   5.193 -          else raise OracleExn t
   5.194 -      | tm (Const("uminus", T) $ x) = 
   5.195 -	  if is_numeric_op T then Interp("*", [Int ~1, tm x])
   5.196 -          else raise OracleExn t
   5.197 -      | tm t = Int (lit t) 
   5.198 -	       handle Match => var (t,[])
   5.199 -    (*translation of a formula*)
   5.200 -    and fm pos (Const("op &", _) $ p $ q) =  
   5.201 -	    Buildin("AND", [fm pos p, fm pos q])
   5.202 -      | fm pos (Const("op |", _) $ p $ q) =  
   5.203 -	    Buildin("OR", [fm pos p, fm pos q])
   5.204 -      | fm pos (Const("op -->", _) $ p $ q) =  
   5.205 -	    Buildin("=>", [fm (not pos) p, fm pos q])
   5.206 -      | fm pos (Const("Not", _) $ p) =  
   5.207 -	    Buildin("NOT", [fm (not pos) p])
   5.208 -      | fm pos (Const("True", _)) = TrueExpr
   5.209 -      | fm pos (Const("False", _)) = FalseExpr
   5.210 -      | fm pos (Const("SVC_Oracle.iff_keep", _) $ p $ q) = 
   5.211 -	     (*polarity doesn't matter*)
   5.212 -	    Buildin("=", [fm pos p, fm pos q]) 
   5.213 -      | fm pos (Const("SVC_Oracle.iff_unfold", _) $ p $ q) = 
   5.214 -	    Buildin("AND",   (*unfolding uses both polarities*)
   5.215 -			 [Buildin("=>", [fm (not pos) p, fm pos q]),
   5.216 -			  Buildin("=>", [fm (not pos) q, fm pos p])])
   5.217 -      | fm pos (t as Const("op =", Type ("fun", [T,_])) $ x $ y) = 
   5.218 -	    let val tx = tm x and ty = tm y
   5.219 -		in if pos orelse T = HOLogic.realT then
   5.220 -		       Buildin("=", [tx, ty])
   5.221 -		   else if is_intnat T then
   5.222 -		       Buildin("AND", 
   5.223 -				    [Buildin("<", [tx, suc ty]), 
   5.224 -				     Buildin("<", [ty, suc tx])])
   5.225 -		   else raise OracleExn t
   5.226 -	    end
   5.227 -	(*inequalities: possible types are nat, int, real*)
   5.228 -      | fm pos (t as Const("op <",  Type ("fun", [T,_])) $ x $ y) = 
   5.229 -	    if not pos orelse T = HOLogic.realT then
   5.230 -		Buildin("<", [tm x, tm y])
   5.231 -	    else if is_intnat T then
   5.232 -		Buildin("<=", [suc (tm x), tm y])
   5.233 -	    else raise OracleExn t
   5.234 -      | fm pos (t as Const("op <=",  Type ("fun", [T,_])) $ x $ y) = 
   5.235 -	    if pos orelse T = HOLogic.realT then
   5.236 -		Buildin("<=", [tm x, tm y])
   5.237 -	    else if is_intnat T then
   5.238 -		Buildin("<", [tm x, suc (tm y)])
   5.239 -	    else raise OracleExn t
   5.240 -      | fm pos t = var(t,[]);
   5.241 -      (*entry point, and translation of a meta-formula*)
   5.242 -      fun mt pos ((c as Const("Trueprop", _)) $ p) = fm pos (iff_tag p)
   5.243 -	| mt pos ((c as Const("==>", _)) $ p $ q) = 
   5.244 -	    Buildin("=>", [mt (not pos) p, mt pos q])
   5.245 -	| mt pos t = fm pos (iff_tag t)  (*it might be a formula*)
   5.246 -
   5.247 -      val body_e = mt pos body  (*evaluate now to assign into !nat_vars*)
   5.248 -  in 
   5.249 -     foldr add_nat_var (!nat_vars, body_e) 
   5.250 -  end;
   5.251 -
   5.252 -
   5.253 - (*The oracle proves the given formula t, if possible*)
   5.254 - fun oracle (sign, OracleExn t) = 
   5.255 -   let val dummy = if !trace then tracing ("Subgoal abstracted to\n" ^
   5.256 -					   Sign.string_of_term sign t)
   5.257 -                   else ()
   5.258 -   in
   5.259 -       if valid (expr_of false t) then t
   5.260 -       else raise OracleExn t
   5.261 -   end;
   5.262 -
   5.263 -end;
     6.1 --- a/src/HOL/ex/ROOT.ML	Tue Feb 05 15:51:28 2002 +0100
     6.2 +++ b/src/HOL/ex/ROOT.ML	Tue Feb 05 23:18:08 2002 +0100
     6.3 @@ -35,4 +35,5 @@
     6.4  time_use_thy "MT";
     6.5  time_use_thy "Tarski";
     6.6  
     6.7 +time_use_thy "SVC_Oracle";
     6.8  if_svc_enabled time_use_thy "svc_test";
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/ex/SVC_Oracle.ML	Tue Feb 05 23:18:08 2002 +0100
     7.3 @@ -0,0 +1,113 @@
     7.4 +(*  Title:      HOL/SVC_Oracle.ML
     7.5 +    ID:         $Id$
     7.6 +    Author:     Lawrence C Paulson
     7.7 +    Copyright   1999  University of Cambridge
     7.8 +
     7.9 +Installing the oracle for SVC (Stanford Validity Checker)
    7.10 +
    7.11 +The following code merely CALLS the oracle; 
    7.12 +  the soundness-critical functions are at HOL/Tools/svc_funcs.ML
    7.13 +
    7.14 +Based upon the work of Søren T. Heilmann
    7.15 +*)
    7.16 +
    7.17 +
    7.18 +(*Generalize an Isabelle formula, replacing by Vars
    7.19 +  all subterms not intelligible to SVC.*)
    7.20 +fun svc_abstract t =
    7.21 +  let
    7.22 +    (*The oracle's result is given to the subgoal using compose_tac because
    7.23 +      its premises are matched against the assumptions rather than used
    7.24 +      to make subgoals.  Therefore , abstraction must copy the parameters
    7.25 +      precisely and make them available to all generated Vars.*)
    7.26 +    val params = Term.strip_all_vars t
    7.27 +    and body   = Term.strip_all_body t
    7.28 +    val Us = map #2 params
    7.29 +    val nPar = length params
    7.30 +    val vname = ref "V_a"
    7.31 +    val pairs = ref ([] : (term*term) list)
    7.32 +    fun insert t = 
    7.33 +	let val T = fastype_of t
    7.34 +            val v = Unify.combound (Var ((!vname,0), Us--->T),
    7.35 +				    0, nPar)
    7.36 +	in  vname := bump_string (!vname); 
    7.37 +	    pairs := (t, v) :: !pairs;
    7.38 +	    v
    7.39 +	end;
    7.40 +    fun replace t = 
    7.41 +	case t of
    7.42 +	    Free _  => t  (*but not existing Vars, lest the names clash*)
    7.43 +	  | Bound _ => t
    7.44 +	  | _ => (case gen_assoc Pattern.aeconv (!pairs, t) of
    7.45 +		      Some v => v
    7.46 +		    | None   => insert t)
    7.47 +    (*abstraction of a numeric literal*)
    7.48 +    fun lit (t as Const("0", _)) = t
    7.49 +      | lit (t as Const("1", _)) = t
    7.50 +      | lit (t as Const("Numeral.number_of", _) $ w) = t
    7.51 +      | lit t = replace t
    7.52 +    (*abstraction of a real/rational expression*)
    7.53 +    fun rat ((c as Const("op +", _)) $ x $ y) = c $ (rat x) $ (rat y)
    7.54 +      | rat ((c as Const("op -", _)) $ x $ y) = c $ (rat x) $ (rat y)
    7.55 +      | rat ((c as Const("op /", _)) $ x $ y) = c $ (rat x) $ (rat y)
    7.56 +      | rat ((c as Const("op *", _)) $ x $ y) = c $ (rat x) $ (rat y)
    7.57 +      | rat ((c as Const("uminus", _)) $ x) = c $ (rat x)
    7.58 +      | rat t = lit t
    7.59 +    (*abstraction of an integer expression: no div, mod*)
    7.60 +    fun int ((c as Const("op +", _)) $ x $ y) = c $ (int x) $ (int y)
    7.61 +      | int ((c as Const("op -", _)) $ x $ y) = c $ (int x) $ (int y)
    7.62 +      | int ((c as Const("op *", _)) $ x $ y) = c $ (int x) $ (int y)
    7.63 +      | int ((c as Const("uminus", _)) $ x) = c $ (int x)
    7.64 +      | int t = lit t
    7.65 +    (*abstraction of a natural number expression: no minus*)
    7.66 +    fun nat ((c as Const("op +", _)) $ x $ y) = c $ (nat x) $ (nat y)
    7.67 +      | nat ((c as Const("op *", _)) $ x $ y) = c $ (nat x) $ (nat y)
    7.68 +      | nat ((c as Const("Suc", _)) $ x) = c $ (nat x)
    7.69 +      | nat t = lit t
    7.70 +    (*abstraction of a relation: =, <, <=*)
    7.71 +    fun rel (T, c $ x $ y) =
    7.72 +	    if T = HOLogic.realT then c $ (rat x) $ (rat y)
    7.73 +	    else if T = HOLogic.intT then c $ (int x) $ (int y)
    7.74 +	    else if T = HOLogic.natT then c $ (nat x) $ (nat y)
    7.75 +	    else if T = HOLogic.boolT then c $ (fm x) $ (fm y)
    7.76 +	    else replace (c $ x $ y)   (*non-numeric comparison*)
    7.77 +    (*abstraction of a formula*)
    7.78 +    and fm ((c as Const("op &", _)) $ p $ q) = c $ (fm p) $ (fm q)
    7.79 +      | fm ((c as Const("op |", _)) $ p $ q) = c $ (fm p) $ (fm q)
    7.80 +      | fm ((c as Const("op -->", _)) $ p $ q) = c $ (fm p) $ (fm q)
    7.81 +      | fm ((c as Const("Not", _)) $ p) = c $ (fm p)
    7.82 +      | fm ((c as Const("True", _))) = c
    7.83 +      | fm ((c as Const("False", _))) = c
    7.84 +      | fm (t as Const("op =",  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
    7.85 +      | fm (t as Const("op <",  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
    7.86 +      | fm (t as Const("op <=", Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
    7.87 +      | fm t = replace t
    7.88 +    (*entry point, and abstraction of a meta-formula*)
    7.89 +    fun mt ((c as Const("Trueprop", _)) $ p) = c $ (fm p)
    7.90 +      | mt ((c as Const("==>", _)) $ p $ q)  = c $ (mt p) $ (mt q)
    7.91 +      | mt t = fm t  (*it might be a formula*)
    7.92 +  in (list_all (params, mt body), !pairs) end;
    7.93 +
    7.94 +
    7.95 +(*Present the entire subgoal to the oracle, assumptions and all, but possibly
    7.96 +  abstracted.  Use via compose_tac, which performs no lifting but will
    7.97 +  instantiate variables.*)
    7.98 +local val svc_thy = the_context () in
    7.99 +
   7.100 +fun svc_tac i st = 
   7.101 +  let val prem = BasisLibrary.List.nth (prems_of st, i-1)
   7.102 +      val (absPrem, _) = svc_abstract prem
   7.103 +      val th = invoke_oracle svc_thy "svc_oracle"
   7.104 +	             (#sign (rep_thm st), Svc.OracleExn absPrem)
   7.105 +   in 
   7.106 +      compose_tac (false, th, 0) i st
   7.107 +   end 
   7.108 +   handle Svc.OracleExn _ => Seq.empty
   7.109 +	| Subscript       => Seq.empty;
   7.110 +
   7.111 +end;
   7.112 +
   7.113 +
   7.114 +(*check if user has SVC installed*)
   7.115 +fun svc_enabled () = getenv "SVC_HOME" <> "";
   7.116 +fun if_svc_enabled f x = if svc_enabled () then f x else ();
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/ex/SVC_Oracle.thy	Tue Feb 05 23:18:08 2002 +0100
     8.3 @@ -0,0 +1,22 @@
     8.4 +(*  Title:      HOL/ex/SVC_Oracle.thy
     8.5 +    ID:         $Id$
     8.6 +    Author:     Lawrence C Paulson
     8.7 +    Copyright   1999  University of Cambridge
     8.8 +
     8.9 +Installing the oracle for SVC (Stanford Validity Checker)
    8.10 +
    8.11 +Based upon the work of Søren T. Heilmann
    8.12 +*)
    8.13 +
    8.14 +theory SVC_Oracle = Main (** + Real??**)
    8.15 +files "svc_funcs.ML":
    8.16 +
    8.17 +consts
    8.18 +  (*reserved for the oracle*)
    8.19 +  iff_keep :: "[bool, bool] => bool"
    8.20 +  iff_unfold :: "[bool, bool] => bool"
    8.21 +
    8.22 +oracle
    8.23 +  svc_oracle = Svc.oracle
    8.24 +
    8.25 +end
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/ex/svc_funcs.ML	Tue Feb 05 23:18:08 2002 +0100
     9.3 @@ -0,0 +1,260 @@
     9.4 +(*  Title:      HOL/Tools/svc_funcs.ML
     9.5 +    ID:         $Id$
     9.6 +    Author:     Lawrence C Paulson
     9.7 +    Copyright   1999  University of Cambridge
     9.8 +
     9.9 +Translation functions for the interface to SVC
    9.10 +
    9.11 +Based upon the work of Søren T. Heilmann
    9.12 +
    9.13 +Integers and naturals are translated as follows:
    9.14 +  In a positive context, replace x<y by x+1<=y
    9.15 +  In a negative context, replace x<=y by x<y+1
    9.16 +  In a negative context, replace x=y by x<y+1 & y<x+1
    9.17 +Biconditionals (if-and-only-iff) are expanded if they require such translations
    9.18 +  in either operand.
    9.19 +
    9.20 +For each variable of type nat, an assumption is added that it is non-negative.
    9.21 +*)
    9.22 +
    9.23 +structure Svc =
    9.24 +struct
    9.25 + val trace = ref false;
    9.26 +
    9.27 + datatype expr =
    9.28 +     Buildin of string * expr list
    9.29 +   | Interp of string * expr list
    9.30 +   | UnInterp of string * expr list
    9.31 +   | FalseExpr 
    9.32 +   | TrueExpr
    9.33 +   | Int of int
    9.34 +   | Rat of int * int;
    9.35 +
    9.36 + open BasisLibrary
    9.37 +
    9.38 + fun signedInt i = 
    9.39 +     if i < 0 then "-" ^ Int.toString (~i)
    9.40 +     else Int.toString i;
    9.41 +	 
    9.42 + fun is_intnat T = T = HOLogic.intT orelse T = HOLogic.natT;
    9.43 + 
    9.44 + fun is_numeric T = is_intnat T orelse T = HOLogic.realT;
    9.45 + 
    9.46 + fun is_numeric_op T = is_numeric (domain_type T);
    9.47 +
    9.48 + fun toString t =
    9.49 +     let fun ue (Buildin(s, l)) = 
    9.50 +	     "(" ^ s ^ (foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ ") "
    9.51 +	   | ue (Interp(s, l)) = 
    9.52 +	     "{" ^ s ^ (foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ "} "
    9.53 +	   | ue (UnInterp(s, l)) = 
    9.54 +	     "(" ^ s ^ (foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ ") "
    9.55 +	   | ue (FalseExpr) = "FALSE "
    9.56 +	   | ue (TrueExpr)  = "TRUE "
    9.57 +	   | ue (Int i)     = (signedInt i) ^ " "
    9.58 +	   | ue (Rat(i, j)) = (signedInt i) ^ "|" ^ (signedInt j) ^ " "
    9.59 +     in
    9.60 +	 ue t
    9.61 +     end;
    9.62 +
    9.63 + fun valid e = 
    9.64 +  let val svc_home = getenv "SVC_HOME" 
    9.65 +      val svc_machine = getenv "SVC_MACHINE"
    9.66 +      val check_valid = if svc_home = ""
    9.67 +	                then error "Environment variable SVC_HOME not set"
    9.68 +			else if svc_machine = ""
    9.69 +	                then error "Environment variable SVC_MACHINE not set"
    9.70 +			else svc_home ^ "/" ^ svc_machine ^ "/bin/check_valid"
    9.71 +      val svc_input = toString e
    9.72 +      val _ = if !trace then tracing ("Calling SVC:\n" ^ svc_input) else ()
    9.73 +      val svc_input_file  = File.tmp_path (Path.basic "SVM_in");
    9.74 +      val svc_output_file = File.tmp_path (Path.basic "SVM_out");
    9.75 +      val _ = (File.write svc_input_file svc_input;
    9.76 +	       execute (check_valid ^ " -dump-result " ^ 
    9.77 +			File.sysify_path svc_output_file ^
    9.78 +			" " ^ File.sysify_path svc_input_file ^ 
    9.79 +			"> /dev/null 2>&1"))
    9.80 +      val svc_output =
    9.81 +        (case Library.try File.read svc_output_file of
    9.82 +          Some out => out
    9.83 +        | None => error "SVC returned no output");
    9.84 +  in
    9.85 +      if ! trace then tracing ("SVC Returns:\n" ^ svc_output)
    9.86 +      else (File.rm svc_input_file; File.rm svc_output_file);
    9.87 +      String.isPrefix "VALID" svc_output
    9.88 +  end
    9.89 +
    9.90 + (*New exception constructor for passing arguments to the oracle*)
    9.91 + exception OracleExn of term;
    9.92 +
    9.93 + fun apply c args =
    9.94 +     let val (ts, bs) = ListPair.unzip args
    9.95 +     in  (list_comb(c,ts), exists I bs)  end;
    9.96 +
    9.97 + (*Determining whether the biconditionals must be unfolded: if there are
    9.98 +   int or nat comparisons below*)
    9.99 + val iff_tag =
   9.100 +   let fun tag t =
   9.101 +	 let val (c,ts) = strip_comb t
   9.102 +	 in  case c of
   9.103 +	     Const("op &", _)   => apply c (map tag ts)
   9.104 +	   | Const("op |", _)   => apply c (map tag ts)
   9.105 +	   | Const("op -->", _) => apply c (map tag ts)
   9.106 +	   | Const("Not", _)    => apply c (map tag ts)
   9.107 +	   | Const("True", _)   => (c, false)
   9.108 +	   | Const("False", _)  => (c, false)
   9.109 +	   | Const("op =", Type ("fun", [T,_])) => 
   9.110 +		 if T = HOLogic.boolT then
   9.111 +		     (*biconditional: with int/nat comparisons below?*)
   9.112 +		     let val [t1,t2] = ts
   9.113 +			 val (u1,b1) = tag t1
   9.114 +			 and (u2,b2) = tag t2
   9.115 +			 val cname = if b1 orelse b2 then "unfold" else "keep"
   9.116 +		     in 
   9.117 +			(Const ("SVC_Oracle.iff_" ^ cname, dummyT) $ u1 $ u2,
   9.118 +			 b1 orelse b2)
   9.119 +		     end
   9.120 +		 else (*might be numeric equality*) (t, is_intnat T)
   9.121 +	   | Const("op <", Type ("fun", [T,_]))  => (t, is_intnat T)
   9.122 +	   | Const("op <=", Type ("fun", [T,_])) => (t, is_intnat T)
   9.123 +	   | _ => (t, false)
   9.124 +	 end
   9.125 +   in #1 o tag end;
   9.126 +
   9.127 + (*Map expression e to 0<=a --> e, where "a" is the name of a nat variable*)
   9.128 + fun add_nat_var (a, e) = 
   9.129 +     Buildin("=>", [Buildin("<=", [Int 0, UnInterp (a, [])]),
   9.130 +		    e]);
   9.131 +
   9.132 + fun param_string [] = ""
   9.133 +   | param_string is = "_" ^ space_implode "_" (map string_of_int is)
   9.134 +
   9.135 + (*Translate an Isabelle formula into an SVC expression
   9.136 +   pos ["positive"]: true if an assumption, false if a goal*)
   9.137 + fun expr_of pos t =
   9.138 +  let
   9.139 +    val params = rev (rename_wrt_term t (Term.strip_all_vars t))
   9.140 +    and body   = Term.strip_all_body t
   9.141 +    val nat_vars = ref ([] : string list)
   9.142 +    (*translation of a variable: record all natural numbers*)
   9.143 +    fun trans_var (a,T,is) =
   9.144 +	(if T = HOLogic.natT then nat_vars := (a ins_string (!nat_vars))
   9.145 +	                     else ();
   9.146 +         UnInterp (a ^ param_string is, []))
   9.147 +    (*A variable, perhaps applied to a series of parameters*)
   9.148 +    fun var (Free(a,T), is)      = trans_var ("F_" ^ a, T, is)
   9.149 +      | var (Var((a, 0), T), is) = trans_var (a, T, is)
   9.150 +      | var (Bound i, is)        = 
   9.151 +          let val (a,T) = List.nth (params, i)
   9.152 +	  in  trans_var ("B_" ^ a, T, is)  end
   9.153 +      | var (t $ Bound i, is)    = var(t,i::is)
   9.154 +            (*removing a parameter from a Var: the bound var index will
   9.155 +               become part of the Var's name*)
   9.156 +      | var (t,_) = raise OracleExn t;
   9.157 +    (*translation of a literal*)
   9.158 +    fun lit (Const("Numeral.number_of", _) $ w) =
   9.159 +          (HOLogic.dest_binum w handle TERM _ => raise Match)
   9.160 +      | lit (Const("0", _)) = 0
   9.161 +      | lit (Const("1", _)) = 1
   9.162 +    (*translation of a literal expression [no variables]*)
   9.163 +    fun litExp (Const("op +", T) $ x $ y) = 
   9.164 +	  if is_numeric_op T then (litExp x) + (litExp y)
   9.165 +          else raise OracleExn t
   9.166 +      | litExp (Const("op -", T) $ x $ y) = 
   9.167 +	  if is_numeric_op T then (litExp x) - (litExp y)
   9.168 +          else raise OracleExn t
   9.169 +      | litExp (Const("op *", T) $ x $ y) = 
   9.170 +	  if is_numeric_op T then (litExp x) * (litExp y)
   9.171 +          else raise OracleExn t
   9.172 +      | litExp (Const("uminus", T) $ x)   = 
   9.173 +	  if is_numeric_op T then ~(litExp x)
   9.174 +          else raise OracleExn t
   9.175 +      | litExp t = lit t 
   9.176 +		   handle Match => raise OracleExn t
   9.177 +    (*translation of a real/rational expression*)
   9.178 +    fun suc t = Interp("+", [Int 1, t])
   9.179 +    fun tm (Const("Suc", T) $ x) = suc (tm x)
   9.180 +      | tm (Const("op +", T) $ x $ y) = 
   9.181 +	  if is_numeric_op T then Interp("+", [tm x, tm y])
   9.182 +          else raise OracleExn t
   9.183 +      | tm (Const("op -", T) $ x $ y) = 
   9.184 +	  if is_numeric_op T then 
   9.185 +	      Interp("+", [tm x, Interp("*", [Int ~1, tm y])])
   9.186 +          else raise OracleExn t
   9.187 +      | tm (Const("op *", T) $ x $ y) = 
   9.188 +	  if is_numeric_op T then Interp("*", [tm x, tm y])
   9.189 +          else raise OracleExn t
   9.190 +      | tm (Const("RealDef.rinv", T) $ x) = 
   9.191 +	  if domain_type T = HOLogic.realT then 
   9.192 +	      Rat(1, litExp x)
   9.193 +          else raise OracleExn t
   9.194 +      | tm (Const("uminus", T) $ x) = 
   9.195 +	  if is_numeric_op T then Interp("*", [Int ~1, tm x])
   9.196 +          else raise OracleExn t
   9.197 +      | tm t = Int (lit t) 
   9.198 +	       handle Match => var (t,[])
   9.199 +    (*translation of a formula*)
   9.200 +    and fm pos (Const("op &", _) $ p $ q) =  
   9.201 +	    Buildin("AND", [fm pos p, fm pos q])
   9.202 +      | fm pos (Const("op |", _) $ p $ q) =  
   9.203 +	    Buildin("OR", [fm pos p, fm pos q])
   9.204 +      | fm pos (Const("op -->", _) $ p $ q) =  
   9.205 +	    Buildin("=>", [fm (not pos) p, fm pos q])
   9.206 +      | fm pos (Const("Not", _) $ p) =  
   9.207 +	    Buildin("NOT", [fm (not pos) p])
   9.208 +      | fm pos (Const("True", _)) = TrueExpr
   9.209 +      | fm pos (Const("False", _)) = FalseExpr
   9.210 +      | fm pos (Const("SVC_Oracle.iff_keep", _) $ p $ q) = 
   9.211 +	     (*polarity doesn't matter*)
   9.212 +	    Buildin("=", [fm pos p, fm pos q]) 
   9.213 +      | fm pos (Const("SVC_Oracle.iff_unfold", _) $ p $ q) = 
   9.214 +	    Buildin("AND",   (*unfolding uses both polarities*)
   9.215 +			 [Buildin("=>", [fm (not pos) p, fm pos q]),
   9.216 +			  Buildin("=>", [fm (not pos) q, fm pos p])])
   9.217 +      | fm pos (t as Const("op =", Type ("fun", [T,_])) $ x $ y) = 
   9.218 +	    let val tx = tm x and ty = tm y
   9.219 +		in if pos orelse T = HOLogic.realT then
   9.220 +		       Buildin("=", [tx, ty])
   9.221 +		   else if is_intnat T then
   9.222 +		       Buildin("AND", 
   9.223 +				    [Buildin("<", [tx, suc ty]), 
   9.224 +				     Buildin("<", [ty, suc tx])])
   9.225 +		   else raise OracleExn t
   9.226 +	    end
   9.227 +	(*inequalities: possible types are nat, int, real*)
   9.228 +      | fm pos (t as Const("op <",  Type ("fun", [T,_])) $ x $ y) = 
   9.229 +	    if not pos orelse T = HOLogic.realT then
   9.230 +		Buildin("<", [tm x, tm y])
   9.231 +	    else if is_intnat T then
   9.232 +		Buildin("<=", [suc (tm x), tm y])
   9.233 +	    else raise OracleExn t
   9.234 +      | fm pos (t as Const("op <=",  Type ("fun", [T,_])) $ x $ y) = 
   9.235 +	    if pos orelse T = HOLogic.realT then
   9.236 +		Buildin("<=", [tm x, tm y])
   9.237 +	    else if is_intnat T then
   9.238 +		Buildin("<", [tm x, suc (tm y)])
   9.239 +	    else raise OracleExn t
   9.240 +      | fm pos t = var(t,[]);
   9.241 +      (*entry point, and translation of a meta-formula*)
   9.242 +      fun mt pos ((c as Const("Trueprop", _)) $ p) = fm pos (iff_tag p)
   9.243 +	| mt pos ((c as Const("==>", _)) $ p $ q) = 
   9.244 +	    Buildin("=>", [mt (not pos) p, mt pos q])
   9.245 +	| mt pos t = fm pos (iff_tag t)  (*it might be a formula*)
   9.246 +
   9.247 +      val body_e = mt pos body  (*evaluate now to assign into !nat_vars*)
   9.248 +  in 
   9.249 +     foldr add_nat_var (!nat_vars, body_e) 
   9.250 +  end;
   9.251 +
   9.252 +
   9.253 + (*The oracle proves the given formula t, if possible*)
   9.254 + fun oracle (sign, OracleExn t) = 
   9.255 +   let val dummy = if !trace then tracing ("Subgoal abstracted to\n" ^
   9.256 +					   Sign.string_of_term sign t)
   9.257 +                   else ()
   9.258 +   in
   9.259 +       if valid (expr_of false t) then t
   9.260 +       else raise OracleExn t
   9.261 +   end;
   9.262 +
   9.263 +end;