improved oracle setup;
authorwenzelm
Thu Jul 14 19:28:18 2005 +0200 (2005-07-14)
changeset 1683645a3dc4688bc
parent 16835 2e7d7ec7a268
child 16837 416e86088931
improved oracle setup;
src/HOL/Integ/Presburger.thy
src/HOL/Integ/presburger.ML
src/HOL/Presburger.thy
src/HOL/Tools/Presburger/presburger.ML
src/HOL/ex/SVC_Oracle.ML
src/HOL/ex/SVC_Oracle.thy
src/HOL/ex/svc_funcs.ML
     1.1 --- a/src/HOL/Integ/Presburger.thy	Thu Jul 14 19:28:17 2005 +0200
     1.2 +++ b/src/HOL/Integ/Presburger.thy	Thu Jul 14 19:28:18 2005 +0200
     1.3 @@ -983,7 +983,7 @@
     1.4  
     1.5  use "cooper_dec.ML"
     1.6  oracle
     1.7 -  presburger_oracle = CooperDec.mk_presburger_oracle
     1.8 +  presburger_oracle ("term") = CooperDec.presburger_oracle
     1.9  
    1.10  use "cooper_proof.ML"
    1.11  use "qelim.ML"
     2.1 --- a/src/HOL/Integ/presburger.ML	Thu Jul 14 19:28:17 2005 +0200
     2.2 +++ b/src/HOL/Integ/presburger.ML	Thu Jul 14 19:28:18 2005 +0200
     2.3 @@ -28,12 +28,6 @@
     2.4  (*-----------------------------------------------------------------*)
     2.5  
     2.6  
     2.7 -(* Invoking the oracle *)
     2.8 -
     2.9 -fun pres_oracle sg t = 
    2.10 -  invoke_oracle (theory "Presburger") "presburger_oracle" 
    2.11 -     (sg, CooperDec.COOPER_ORACLE t) ;
    2.12 -
    2.13  val presburger_ss = simpset_of (theory "Presburger");
    2.14  
    2.15  fun cooper_pp sg (fm as e$Abs(xn,xT,p)) = 
    2.16 @@ -279,7 +273,7 @@
    2.17      let val pth = 
    2.18            (* If quick_and_dirty then run without proof generation as oracle*)
    2.19               if !quick_and_dirty 
    2.20 -             then pres_oracle sg (Pattern.eta_long [] t1)
    2.21 +             then presburger_oracle sg (Pattern.eta_long [] t1)
    2.22  (*
    2.23  assume (cterm_of sg 
    2.24  	       (HOLogic.mk_Trueprop(HOLogic.mk_eq(t1,CooperDec.integer_qelim (Pattern.eta_long [] t1)))))
     3.1 --- a/src/HOL/Presburger.thy	Thu Jul 14 19:28:17 2005 +0200
     3.2 +++ b/src/HOL/Presburger.thy	Thu Jul 14 19:28:18 2005 +0200
     3.3 @@ -983,7 +983,7 @@
     3.4  
     3.5  use "cooper_dec.ML"
     3.6  oracle
     3.7 -  presburger_oracle = CooperDec.mk_presburger_oracle
     3.8 +  presburger_oracle ("term") = CooperDec.presburger_oracle
     3.9  
    3.10  use "cooper_proof.ML"
    3.11  use "qelim.ML"
     4.1 --- a/src/HOL/Tools/Presburger/presburger.ML	Thu Jul 14 19:28:17 2005 +0200
     4.2 +++ b/src/HOL/Tools/Presburger/presburger.ML	Thu Jul 14 19:28:18 2005 +0200
     4.3 @@ -28,12 +28,6 @@
     4.4  (*-----------------------------------------------------------------*)
     4.5  
     4.6  
     4.7 -(* Invoking the oracle *)
     4.8 -
     4.9 -fun pres_oracle sg t = 
    4.10 -  invoke_oracle (theory "Presburger") "presburger_oracle" 
    4.11 -     (sg, CooperDec.COOPER_ORACLE t) ;
    4.12 -
    4.13  val presburger_ss = simpset_of (theory "Presburger");
    4.14  
    4.15  fun cooper_pp sg (fm as e$Abs(xn,xT,p)) = 
    4.16 @@ -279,7 +273,7 @@
    4.17      let val pth = 
    4.18            (* If quick_and_dirty then run without proof generation as oracle*)
    4.19               if !quick_and_dirty 
    4.20 -             then pres_oracle sg (Pattern.eta_long [] t1)
    4.21 +             then presburger_oracle sg (Pattern.eta_long [] t1)
    4.22  (*
    4.23  assume (cterm_of sg 
    4.24  	       (HOLogic.mk_Trueprop(HOLogic.mk_eq(t1,CooperDec.integer_qelim (Pattern.eta_long [] t1)))))
     5.1 --- a/src/HOL/ex/SVC_Oracle.ML	Thu Jul 14 19:28:17 2005 +0200
     5.2 +++ b/src/HOL/ex/SVC_Oracle.ML	Thu Jul 14 19:28:18 2005 +0200
     5.3 @@ -5,7 +5,7 @@
     5.4  
     5.5  Installing the oracle for SVC (Stanford Validity Checker)
     5.6  
     5.7 -The following code merely CALLS the oracle; 
     5.8 +The following code merely CALLS the oracle;
     5.9    the soundness-critical functions are at HOL/Tools/svc_funcs.ML
    5.10  
    5.11  Based upon the work of Søren T. Heilmann
    5.12 @@ -26,21 +26,21 @@
    5.13      val nPar = length params
    5.14      val vname = ref "V_a"
    5.15      val pairs = ref ([] : (term*term) list)
    5.16 -    fun insert t = 
    5.17 -	let val T = fastype_of t
    5.18 +    fun insert t =
    5.19 +        let val T = fastype_of t
    5.20              val v = Unify.combound (Var ((!vname,0), Us--->T),
    5.21 -				    0, nPar)
    5.22 -	in  vname := Symbol.bump_string (!vname); 
    5.23 -	    pairs := (t, v) :: !pairs;
    5.24 -	    v
    5.25 -	end;
    5.26 -    fun replace t = 
    5.27 -	case t of
    5.28 -	    Free _  => t  (*but not existing Vars, lest the names clash*)
    5.29 -	  | Bound _ => t
    5.30 -	  | _ => (case gen_assoc Pattern.aeconv (!pairs, t) of
    5.31 -		      SOME v => v
    5.32 -		    | NONE   => insert t)
    5.33 +                                    0, nPar)
    5.34 +        in  vname := Symbol.bump_string (!vname);
    5.35 +            pairs := (t, v) :: !pairs;
    5.36 +            v
    5.37 +        end;
    5.38 +    fun replace t =
    5.39 +        case t of
    5.40 +            Free _  => t  (*but not existing Vars, lest the names clash*)
    5.41 +          | Bound _ => t
    5.42 +          | _ => (case gen_assoc Pattern.aeconv (!pairs, t) of
    5.43 +                      SOME v => v
    5.44 +                    | NONE   => insert t)
    5.45      (*abstraction of a numeric literal*)
    5.46      fun lit (t as Const("0", _)) = t
    5.47        | lit (t as Const("1", _)) = t
    5.48 @@ -66,11 +66,11 @@
    5.49        | nat t = lit t
    5.50      (*abstraction of a relation: =, <, <=*)
    5.51      fun rel (T, c $ x $ y) =
    5.52 -	    if T = HOLogic.realT then c $ (rat x) $ (rat y)
    5.53 -	    else if T = HOLogic.intT then c $ (int x) $ (int y)
    5.54 -	    else if T = HOLogic.natT then c $ (nat x) $ (nat y)
    5.55 -	    else if T = HOLogic.boolT then c $ (fm x) $ (fm y)
    5.56 -	    else replace (c $ x $ y)   (*non-numeric comparison*)
    5.57 +            if T = HOLogic.realT then c $ (rat x) $ (rat y)
    5.58 +            else if T = HOLogic.intT then c $ (int x) $ (int y)
    5.59 +            else if T = HOLogic.natT then c $ (nat x) $ (nat y)
    5.60 +            else if T = HOLogic.boolT then c $ (fm x) $ (fm y)
    5.61 +            else replace (c $ x $ y)   (*non-numeric comparison*)
    5.62      (*abstraction of a formula*)
    5.63      and fm ((c as Const("op &", _)) $ p $ q) = c $ (fm p) $ (fm q)
    5.64        | fm ((c as Const("op |", _)) $ p $ q) = c $ (fm p) $ (fm q)
    5.65 @@ -92,20 +92,13 @@
    5.66  (*Present the entire subgoal to the oracle, assumptions and all, but possibly
    5.67    abstracted.  Use via compose_tac, which performs no lifting but will
    5.68    instantiate variables.*)
    5.69 -local val svc_thy = the_context () in
    5.70  
    5.71 -fun svc_tac i st = 
    5.72 -  let val prem = BasisLibrary.List.nth (prems_of st, i-1)
    5.73 -      val (absPrem, _) = svc_abstract prem
    5.74 -      val th = invoke_oracle svc_thy "svc_oracle"
    5.75 -	             (#sign (rep_thm st), Svc.OracleExn absPrem)
    5.76 -   in 
    5.77 -      compose_tac (false, th, 0) i st
    5.78 -   end 
    5.79 -   handle Svc.OracleExn _ => Seq.empty
    5.80 -	| Subscript       => Seq.empty;
    5.81 -
    5.82 -end;
    5.83 +fun svc_tac i st =
    5.84 +  let
    5.85 +    val (abs_goal, _) = svc_abstract (Logic.get_goal (Thm.prop_of st) i)
    5.86 +    val th = svc_oracle (Thm.theory_of_thm st) abs_goal
    5.87 +   in compose_tac (false, th, 0) i end
    5.88 +   handle TERM _ => no_tac;
    5.89  
    5.90  
    5.91  (*check if user has SVC installed*)
     6.1 --- a/src/HOL/ex/SVC_Oracle.thy	Thu Jul 14 19:28:17 2005 +0200
     6.2 +++ b/src/HOL/ex/SVC_Oracle.thy	Thu Jul 14 19:28:18 2005 +0200
     6.3 @@ -8,15 +8,18 @@
     6.4  Based upon the work of Søren T. Heilmann
     6.5  *)
     6.6  
     6.7 -theory SVC_Oracle imports Main (** + Real??**)
     6.8 -uses "svc_funcs.ML" begin
     6.9 +theory SVC_Oracle
    6.10 +imports Main
    6.11 +uses "svc_funcs.ML"
    6.12 +begin
    6.13  
    6.14  consts
    6.15 -  (*reserved for the oracle*)
    6.16    iff_keep :: "[bool, bool] => bool"
    6.17    iff_unfold :: "[bool, bool] => bool"
    6.18  
    6.19 +hide const iff_keep iff_unfold
    6.20 +
    6.21  oracle
    6.22 -  svc_oracle = Svc.oracle
    6.23 +  svc_oracle ("term") = Svc.oracle
    6.24  
    6.25  end
     7.1 --- a/src/HOL/ex/svc_funcs.ML	Thu Jul 14 19:28:17 2005 +0200
     7.2 +++ b/src/HOL/ex/svc_funcs.ML	Thu Jul 14 19:28:18 2005 +0200
     7.3 @@ -25,55 +25,55 @@
     7.4       Buildin of string * expr list
     7.5     | Interp of string * expr list
     7.6     | UnInterp of string * expr list
     7.7 -   | FalseExpr 
     7.8 +   | FalseExpr
     7.9     | TrueExpr
    7.10     | Int of IntInf.int
    7.11     | Rat of IntInf.int * IntInf.int;
    7.12  
    7.13   open BasisLibrary
    7.14  
    7.15 - fun signedInt i = 
    7.16 + fun signedInt i =
    7.17       if i < 0 then "-" ^ IntInf.toString (~i)
    7.18       else IntInf.toString i;
    7.19 -	 
    7.20 +
    7.21   fun is_intnat T = T = HOLogic.intT orelse T = HOLogic.natT;
    7.22 - 
    7.23 +
    7.24   fun is_numeric T = is_intnat T orelse T = HOLogic.realT;
    7.25 - 
    7.26 +
    7.27   fun is_numeric_op T = is_numeric (domain_type T);
    7.28  
    7.29   fun toString t =
    7.30 -     let fun ue (Buildin(s, l)) = 
    7.31 -	     "(" ^ s ^ (Library.foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ ") "
    7.32 -	   | ue (Interp(s, l)) = 
    7.33 -	     "{" ^ s ^ (Library.foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ "} "
    7.34 -	   | ue (UnInterp(s, l)) = 
    7.35 -	     "(" ^ s ^ (Library.foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ ") "
    7.36 -	   | ue (FalseExpr) = "FALSE "
    7.37 -	   | ue (TrueExpr)  = "TRUE "
    7.38 -	   | ue (Int i)     = (signedInt i) ^ " "
    7.39 -	   | ue (Rat(i, j)) = (signedInt i) ^ "|" ^ (signedInt j) ^ " "
    7.40 +     let fun ue (Buildin(s, l)) =
    7.41 +             "(" ^ s ^ (Library.foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ ") "
    7.42 +           | ue (Interp(s, l)) =
    7.43 +             "{" ^ s ^ (Library.foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ "} "
    7.44 +           | ue (UnInterp(s, l)) =
    7.45 +             "(" ^ s ^ (Library.foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ ") "
    7.46 +           | ue (FalseExpr) = "FALSE "
    7.47 +           | ue (TrueExpr)  = "TRUE "
    7.48 +           | ue (Int i)     = (signedInt i) ^ " "
    7.49 +           | ue (Rat(i, j)) = (signedInt i) ^ "|" ^ (signedInt j) ^ " "
    7.50       in
    7.51 -	 ue t
    7.52 +         ue t
    7.53       end;
    7.54  
    7.55 - fun valid e = 
    7.56 -  let val svc_home = getenv "SVC_HOME" 
    7.57 + fun valid e =
    7.58 +  let val svc_home = getenv "SVC_HOME"
    7.59        val svc_machine = getenv "SVC_MACHINE"
    7.60        val check_valid = if svc_home = ""
    7.61 -	                then error "Environment variable SVC_HOME not set"
    7.62 -			else if svc_machine = ""
    7.63 -	                then error "Environment variable SVC_MACHINE not set"
    7.64 -			else svc_home ^ "/" ^ svc_machine ^ "/bin/check_valid"
    7.65 +                        then error "Environment variable SVC_HOME not set"
    7.66 +                        else if svc_machine = ""
    7.67 +                        then error "Environment variable SVC_MACHINE not set"
    7.68 +                        else svc_home ^ "/" ^ svc_machine ^ "/bin/check_valid"
    7.69        val svc_input = toString e
    7.70        val _ = if !trace then tracing ("Calling SVC:\n" ^ svc_input) else ()
    7.71        val svc_input_file  = File.tmp_path (Path.basic "SVM_in");
    7.72        val svc_output_file = File.tmp_path (Path.basic "SVM_out");
    7.73        val _ = (File.write svc_input_file svc_input;
    7.74 -	       execute (check_valid ^ " -dump-result " ^ 
    7.75 -			File.shell_path svc_output_file ^
    7.76 -			" " ^ File.shell_path svc_input_file ^ 
    7.77 -			">/dev/null 2>&1"))
    7.78 +               execute (check_valid ^ " -dump-result " ^
    7.79 +                        File.shell_path svc_output_file ^
    7.80 +                        " " ^ File.shell_path svc_input_file ^
    7.81 +                        ">/dev/null 2>&1"))
    7.82        val svc_output =
    7.83          (case Library.try File.read svc_output_file of
    7.84            SOME out => out
    7.85 @@ -84,8 +84,7 @@
    7.86        String.isPrefix "VALID" svc_output
    7.87    end
    7.88  
    7.89 - (*New exception constructor for passing arguments to the oracle*)
    7.90 - exception OracleExn of term;
    7.91 + fun fail t = raise TERM ("SVC oracle", [t]);
    7.92  
    7.93   fun apply c args =
    7.94       let val (ts, bs) = ListPair.unzip args
    7.95 @@ -95,36 +94,36 @@
    7.96     int or nat comparisons below*)
    7.97   val iff_tag =
    7.98     let fun tag t =
    7.99 -	 let val (c,ts) = strip_comb t
   7.100 -	 in  case c of
   7.101 -	     Const("op &", _)   => apply c (map tag ts)
   7.102 -	   | Const("op |", _)   => apply c (map tag ts)
   7.103 -	   | Const("op -->", _) => apply c (map tag ts)
   7.104 -	   | Const("Not", _)    => apply c (map tag ts)
   7.105 -	   | Const("True", _)   => (c, false)
   7.106 -	   | Const("False", _)  => (c, false)
   7.107 -	   | Const("op =", Type ("fun", [T,_])) => 
   7.108 -		 if T = HOLogic.boolT then
   7.109 -		     (*biconditional: with int/nat comparisons below?*)
   7.110 -		     let val [t1,t2] = ts
   7.111 -			 val (u1,b1) = tag t1
   7.112 -			 and (u2,b2) = tag t2
   7.113 -			 val cname = if b1 orelse b2 then "unfold" else "keep"
   7.114 -		     in 
   7.115 -			(Const ("SVC_Oracle.iff_" ^ cname, dummyT) $ u1 $ u2,
   7.116 -			 b1 orelse b2)
   7.117 -		     end
   7.118 -		 else (*might be numeric equality*) (t, is_intnat T)
   7.119 -	   | Const("op <", Type ("fun", [T,_]))  => (t, is_intnat T)
   7.120 -	   | Const("op <=", Type ("fun", [T,_])) => (t, is_intnat T)
   7.121 -	   | _ => (t, false)
   7.122 -	 end
   7.123 +         let val (c,ts) = strip_comb t
   7.124 +         in  case c of
   7.125 +             Const("op &", _)   => apply c (map tag ts)
   7.126 +           | Const("op |", _)   => apply c (map tag ts)
   7.127 +           | Const("op -->", _) => apply c (map tag ts)
   7.128 +           | Const("Not", _)    => apply c (map tag ts)
   7.129 +           | Const("True", _)   => (c, false)
   7.130 +           | Const("False", _)  => (c, false)
   7.131 +           | Const("op =", Type ("fun", [T,_])) =>
   7.132 +                 if T = HOLogic.boolT then
   7.133 +                     (*biconditional: with int/nat comparisons below?*)
   7.134 +                     let val [t1,t2] = ts
   7.135 +                         val (u1,b1) = tag t1
   7.136 +                         and (u2,b2) = tag t2
   7.137 +                         val cname = if b1 orelse b2 then "unfold" else "keep"
   7.138 +                     in
   7.139 +                        (Const ("SVC_Oracle.iff_" ^ cname, dummyT) $ u1 $ u2,
   7.140 +                         b1 orelse b2)
   7.141 +                     end
   7.142 +                 else (*might be numeric equality*) (t, is_intnat T)
   7.143 +           | Const("op <", Type ("fun", [T,_]))  => (t, is_intnat T)
   7.144 +           | Const("op <=", Type ("fun", [T,_])) => (t, is_intnat T)
   7.145 +           | _ => (t, false)
   7.146 +         end
   7.147     in #1 o tag end;
   7.148  
   7.149   (*Map expression e to 0<=a --> e, where "a" is the name of a nat variable*)
   7.150 - fun add_nat_var (a, e) = 
   7.151 + fun add_nat_var (a, e) =
   7.152       Buildin("=>", [Buildin("<=", [Int 0, UnInterp (a, [])]),
   7.153 -		    e]);
   7.154 +                    e]);
   7.155  
   7.156   fun param_string [] = ""
   7.157     | param_string is = "_" ^ space_implode "_" (map string_of_int is)
   7.158 @@ -138,123 +137,119 @@
   7.159      val nat_vars = ref ([] : string list)
   7.160      (*translation of a variable: record all natural numbers*)
   7.161      fun trans_var (a,T,is) =
   7.162 -	(if T = HOLogic.natT then nat_vars := (a ins_string (!nat_vars))
   7.163 -	                     else ();
   7.164 +        (if T = HOLogic.natT then nat_vars := (a ins_string (!nat_vars))
   7.165 +                             else ();
   7.166           UnInterp (a ^ param_string is, []))
   7.167      (*A variable, perhaps applied to a series of parameters*)
   7.168      fun var (Free(a,T), is)      = trans_var ("F_" ^ a, T, is)
   7.169        | var (Var((a, 0), T), is) = trans_var (a, T, is)
   7.170 -      | var (Bound i, is)        = 
   7.171 +      | var (Bound i, is)        =
   7.172            let val (a,T) = List.nth (params, i)
   7.173 -	  in  trans_var ("B_" ^ a, T, is)  end
   7.174 +          in  trans_var ("B_" ^ a, T, is)  end
   7.175        | var (t $ Bound i, is)    = var(t,i::is)
   7.176              (*removing a parameter from a Var: the bound var index will
   7.177                 become part of the Var's name*)
   7.178 -      | var (t,_) = raise OracleExn t;
   7.179 +      | var (t,_) = fail t;
   7.180      (*translation of a literal*)
   7.181      fun lit (Const("Numeral.number_of", _) $ w) =
   7.182            (HOLogic.dest_binum w handle TERM _ => raise Match)
   7.183        | lit (Const("0", _)) = 0
   7.184        | lit (Const("1", _)) = 1
   7.185      (*translation of a literal expression [no variables]*)
   7.186 -    fun litExp (Const("op +", T) $ x $ y) = 
   7.187 -	  if is_numeric_op T then (litExp x) + (litExp y)
   7.188 -          else raise OracleExn t
   7.189 -      | litExp (Const("op -", T) $ x $ y) = 
   7.190 -	  if is_numeric_op T then (litExp x) - (litExp y)
   7.191 -          else raise OracleExn t
   7.192 -      | litExp (Const("op *", T) $ x $ y) = 
   7.193 -	  if is_numeric_op T then (litExp x) * (litExp y)
   7.194 -          else raise OracleExn t
   7.195 -      | litExp (Const("uminus", T) $ x)   = 
   7.196 -	  if is_numeric_op T then ~(litExp x)
   7.197 -          else raise OracleExn t
   7.198 -      | litExp t = lit t 
   7.199 -		   handle Match => raise OracleExn t
   7.200 +    fun litExp (Const("op +", T) $ x $ y) =
   7.201 +          if is_numeric_op T then (litExp x) + (litExp y)
   7.202 +          else fail t
   7.203 +      | litExp (Const("op -", T) $ x $ y) =
   7.204 +          if is_numeric_op T then (litExp x) - (litExp y)
   7.205 +          else fail t
   7.206 +      | litExp (Const("op *", T) $ x $ y) =
   7.207 +          if is_numeric_op T then (litExp x) * (litExp y)
   7.208 +          else fail t
   7.209 +      | litExp (Const("uminus", T) $ x)   =
   7.210 +          if is_numeric_op T then ~(litExp x)
   7.211 +          else fail t
   7.212 +      | litExp t = lit t
   7.213 +                   handle Match => fail t
   7.214      (*translation of a real/rational expression*)
   7.215      fun suc t = Interp("+", [Int 1, t])
   7.216      fun tm (Const("Suc", T) $ x) = suc (tm x)
   7.217 -      | tm (Const("op +", T) $ x $ y) = 
   7.218 -	  if is_numeric_op T then Interp("+", [tm x, tm y])
   7.219 -          else raise OracleExn t
   7.220 -      | tm (Const("op -", T) $ x $ y) = 
   7.221 -	  if is_numeric_op T then 
   7.222 -	      Interp("+", [tm x, Interp("*", [Int ~1, tm y])])
   7.223 -          else raise OracleExn t
   7.224 -      | tm (Const("op *", T) $ x $ y) = 
   7.225 -	  if is_numeric_op T then Interp("*", [tm x, tm y])
   7.226 -          else raise OracleExn t
   7.227 -      | tm (Const("RealDef.rinv", T) $ x) = 
   7.228 -	  if domain_type T = HOLogic.realT then 
   7.229 -	      Rat(1, litExp x)
   7.230 -          else raise OracleExn t
   7.231 -      | tm (Const("uminus", T) $ x) = 
   7.232 -	  if is_numeric_op T then Interp("*", [Int ~1, tm x])
   7.233 -          else raise OracleExn t
   7.234 -      | tm t = Int (lit t) 
   7.235 -	       handle Match => var (t,[])
   7.236 +      | tm (Const("op +", T) $ x $ y) =
   7.237 +          if is_numeric_op T then Interp("+", [tm x, tm y])
   7.238 +          else fail t
   7.239 +      | tm (Const("op -", T) $ x $ y) =
   7.240 +          if is_numeric_op T then
   7.241 +              Interp("+", [tm x, Interp("*", [Int ~1, tm y])])
   7.242 +          else fail t
   7.243 +      | tm (Const("op *", T) $ x $ y) =
   7.244 +          if is_numeric_op T then Interp("*", [tm x, tm y])
   7.245 +          else fail t
   7.246 +      | tm (Const("RealDef.rinv", T) $ x) =
   7.247 +          if domain_type T = HOLogic.realT then
   7.248 +              Rat(1, litExp x)
   7.249 +          else fail t
   7.250 +      | tm (Const("uminus", T) $ x) =
   7.251 +          if is_numeric_op T then Interp("*", [Int ~1, tm x])
   7.252 +          else fail t
   7.253 +      | tm t = Int (lit t)
   7.254 +               handle Match => var (t,[])
   7.255      (*translation of a formula*)
   7.256 -    and fm pos (Const("op &", _) $ p $ q) =  
   7.257 -	    Buildin("AND", [fm pos p, fm pos q])
   7.258 -      | fm pos (Const("op |", _) $ p $ q) =  
   7.259 -	    Buildin("OR", [fm pos p, fm pos q])
   7.260 -      | fm pos (Const("op -->", _) $ p $ q) =  
   7.261 -	    Buildin("=>", [fm (not pos) p, fm pos q])
   7.262 -      | fm pos (Const("Not", _) $ p) =  
   7.263 -	    Buildin("NOT", [fm (not pos) p])
   7.264 +    and fm pos (Const("op &", _) $ p $ q) =
   7.265 +            Buildin("AND", [fm pos p, fm pos q])
   7.266 +      | fm pos (Const("op |", _) $ p $ q) =
   7.267 +            Buildin("OR", [fm pos p, fm pos q])
   7.268 +      | fm pos (Const("op -->", _) $ p $ q) =
   7.269 +            Buildin("=>", [fm (not pos) p, fm pos q])
   7.270 +      | fm pos (Const("Not", _) $ p) =
   7.271 +            Buildin("NOT", [fm (not pos) p])
   7.272        | fm pos (Const("True", _)) = TrueExpr
   7.273        | fm pos (Const("False", _)) = FalseExpr
   7.274 -      | fm pos (Const("SVC_Oracle.iff_keep", _) $ p $ q) = 
   7.275 -	     (*polarity doesn't matter*)
   7.276 -	    Buildin("=", [fm pos p, fm pos q]) 
   7.277 -      | fm pos (Const("SVC_Oracle.iff_unfold", _) $ p $ q) = 
   7.278 -	    Buildin("AND",   (*unfolding uses both polarities*)
   7.279 -			 [Buildin("=>", [fm (not pos) p, fm pos q]),
   7.280 -			  Buildin("=>", [fm (not pos) q, fm pos p])])
   7.281 -      | fm pos (t as Const("op =", Type ("fun", [T,_])) $ x $ y) = 
   7.282 -	    let val tx = tm x and ty = tm y
   7.283 -		in if pos orelse T = HOLogic.realT then
   7.284 -		       Buildin("=", [tx, ty])
   7.285 -		   else if is_intnat T then
   7.286 -		       Buildin("AND", 
   7.287 -				    [Buildin("<", [tx, suc ty]), 
   7.288 -				     Buildin("<", [ty, suc tx])])
   7.289 -		   else raise OracleExn t
   7.290 -	    end
   7.291 -	(*inequalities: possible types are nat, int, real*)
   7.292 -      | fm pos (t as Const("op <",  Type ("fun", [T,_])) $ x $ y) = 
   7.293 -	    if not pos orelse T = HOLogic.realT then
   7.294 -		Buildin("<", [tm x, tm y])
   7.295 -	    else if is_intnat T then
   7.296 -		Buildin("<=", [suc (tm x), tm y])
   7.297 -	    else raise OracleExn t
   7.298 -      | fm pos (t as Const("op <=",  Type ("fun", [T,_])) $ x $ y) = 
   7.299 -	    if pos orelse T = HOLogic.realT then
   7.300 -		Buildin("<=", [tm x, tm y])
   7.301 -	    else if is_intnat T then
   7.302 -		Buildin("<", [tm x, suc (tm y)])
   7.303 -	    else raise OracleExn t
   7.304 +      | fm pos (Const("SVC_Oracle.iff_keep", _) $ p $ q) =
   7.305 +             (*polarity doesn't matter*)
   7.306 +            Buildin("=", [fm pos p, fm pos q])
   7.307 +      | fm pos (Const("SVC_Oracle.iff_unfold", _) $ p $ q) =
   7.308 +            Buildin("AND",   (*unfolding uses both polarities*)
   7.309 +                         [Buildin("=>", [fm (not pos) p, fm pos q]),
   7.310 +                          Buildin("=>", [fm (not pos) q, fm pos p])])
   7.311 +      | fm pos (t as Const("op =", Type ("fun", [T,_])) $ x $ y) =
   7.312 +            let val tx = tm x and ty = tm y
   7.313 +                in if pos orelse T = HOLogic.realT then
   7.314 +                       Buildin("=", [tx, ty])
   7.315 +                   else if is_intnat T then
   7.316 +                       Buildin("AND",
   7.317 +                                    [Buildin("<", [tx, suc ty]),
   7.318 +                                     Buildin("<", [ty, suc tx])])
   7.319 +                   else fail t
   7.320 +            end
   7.321 +        (*inequalities: possible types are nat, int, real*)
   7.322 +      | fm pos (t as Const("op <",  Type ("fun", [T,_])) $ x $ y) =
   7.323 +            if not pos orelse T = HOLogic.realT then
   7.324 +                Buildin("<", [tm x, tm y])
   7.325 +            else if is_intnat T then
   7.326 +                Buildin("<=", [suc (tm x), tm y])
   7.327 +            else fail t
   7.328 +      | fm pos (t as Const("op <=",  Type ("fun", [T,_])) $ x $ y) =
   7.329 +            if pos orelse T = HOLogic.realT then
   7.330 +                Buildin("<=", [tm x, tm y])
   7.331 +            else if is_intnat T then
   7.332 +                Buildin("<", [tm x, suc (tm y)])
   7.333 +            else fail t
   7.334        | fm pos t = var(t,[]);
   7.335        (*entry point, and translation of a meta-formula*)
   7.336        fun mt pos ((c as Const("Trueprop", _)) $ p) = fm pos (iff_tag p)
   7.337 -	| mt pos ((c as Const("==>", _)) $ p $ q) = 
   7.338 -	    Buildin("=>", [mt (not pos) p, mt pos q])
   7.339 -	| mt pos t = fm pos (iff_tag t)  (*it might be a formula*)
   7.340 +        | mt pos ((c as Const("==>", _)) $ p $ q) =
   7.341 +            Buildin("=>", [mt (not pos) p, mt pos q])
   7.342 +        | mt pos t = fm pos (iff_tag t)  (*it might be a formula*)
   7.343  
   7.344        val body_e = mt pos body  (*evaluate now to assign into !nat_vars*)
   7.345 -  in 
   7.346 -     foldr add_nat_var body_e (!nat_vars) 
   7.347 +  in
   7.348 +     foldr add_nat_var body_e (!nat_vars)
   7.349    end;
   7.350  
   7.351  
   7.352   (*The oracle proves the given formula t, if possible*)
   7.353 - fun oracle (sign, OracleExn t) = 
   7.354 -   let val dummy = if !trace then tracing ("Subgoal abstracted to\n" ^
   7.355 -					   Sign.string_of_term sign t)
   7.356 -                   else ()
   7.357 -   in
   7.358 -       if valid (expr_of false t) then t
   7.359 -       else raise OracleExn t
   7.360 -   end;
   7.361 + fun oracle thy t =
   7.362 +  (conditional (! trace) (fn () =>
   7.363 +    tracing ("SVC oracle: problem is\n" ^ Sign.string_of_term thy t));
   7.364 +  if valid (expr_of false t) then t else fail t);
   7.365  
   7.366  end;