src/HOL/ex/svc_funcs.ML
changeset 16836 45a3dc4688bc
parent 16258 f3d913abf7e5
child 17465 93fc1211603f
     1.1 --- a/src/HOL/ex/svc_funcs.ML	Thu Jul 14 19:28:17 2005 +0200
     1.2 +++ b/src/HOL/ex/svc_funcs.ML	Thu Jul 14 19:28:18 2005 +0200
     1.3 @@ -25,55 +25,55 @@
     1.4       Buildin of string * expr list
     1.5     | Interp of string * expr list
     1.6     | UnInterp of string * expr list
     1.7 -   | FalseExpr 
     1.8 +   | FalseExpr
     1.9     | TrueExpr
    1.10     | Int of IntInf.int
    1.11     | Rat of IntInf.int * IntInf.int;
    1.12  
    1.13   open BasisLibrary
    1.14  
    1.15 - fun signedInt i = 
    1.16 + fun signedInt i =
    1.17       if i < 0 then "-" ^ IntInf.toString (~i)
    1.18       else IntInf.toString i;
    1.19 -	 
    1.20 +
    1.21   fun is_intnat T = T = HOLogic.intT orelse T = HOLogic.natT;
    1.22 - 
    1.23 +
    1.24   fun is_numeric T = is_intnat T orelse T = HOLogic.realT;
    1.25 - 
    1.26 +
    1.27   fun is_numeric_op T = is_numeric (domain_type T);
    1.28  
    1.29   fun toString t =
    1.30 -     let fun ue (Buildin(s, l)) = 
    1.31 -	     "(" ^ s ^ (Library.foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ ") "
    1.32 -	   | ue (Interp(s, l)) = 
    1.33 -	     "{" ^ s ^ (Library.foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ "} "
    1.34 -	   | ue (UnInterp(s, l)) = 
    1.35 -	     "(" ^ s ^ (Library.foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ ") "
    1.36 -	   | ue (FalseExpr) = "FALSE "
    1.37 -	   | ue (TrueExpr)  = "TRUE "
    1.38 -	   | ue (Int i)     = (signedInt i) ^ " "
    1.39 -	   | ue (Rat(i, j)) = (signedInt i) ^ "|" ^ (signedInt j) ^ " "
    1.40 +     let fun ue (Buildin(s, l)) =
    1.41 +             "(" ^ s ^ (Library.foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ ") "
    1.42 +           | ue (Interp(s, l)) =
    1.43 +             "{" ^ s ^ (Library.foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ "} "
    1.44 +           | ue (UnInterp(s, l)) =
    1.45 +             "(" ^ s ^ (Library.foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ ") "
    1.46 +           | ue (FalseExpr) = "FALSE "
    1.47 +           | ue (TrueExpr)  = "TRUE "
    1.48 +           | ue (Int i)     = (signedInt i) ^ " "
    1.49 +           | ue (Rat(i, j)) = (signedInt i) ^ "|" ^ (signedInt j) ^ " "
    1.50       in
    1.51 -	 ue t
    1.52 +         ue t
    1.53       end;
    1.54  
    1.55 - fun valid e = 
    1.56 -  let val svc_home = getenv "SVC_HOME" 
    1.57 + fun valid e =
    1.58 +  let val svc_home = getenv "SVC_HOME"
    1.59        val svc_machine = getenv "SVC_MACHINE"
    1.60        val check_valid = if svc_home = ""
    1.61 -	                then error "Environment variable SVC_HOME not set"
    1.62 -			else if svc_machine = ""
    1.63 -	                then error "Environment variable SVC_MACHINE not set"
    1.64 -			else svc_home ^ "/" ^ svc_machine ^ "/bin/check_valid"
    1.65 +                        then error "Environment variable SVC_HOME not set"
    1.66 +                        else if svc_machine = ""
    1.67 +                        then error "Environment variable SVC_MACHINE not set"
    1.68 +                        else svc_home ^ "/" ^ svc_machine ^ "/bin/check_valid"
    1.69        val svc_input = toString e
    1.70        val _ = if !trace then tracing ("Calling SVC:\n" ^ svc_input) else ()
    1.71        val svc_input_file  = File.tmp_path (Path.basic "SVM_in");
    1.72        val svc_output_file = File.tmp_path (Path.basic "SVM_out");
    1.73        val _ = (File.write svc_input_file svc_input;
    1.74 -	       execute (check_valid ^ " -dump-result " ^ 
    1.75 -			File.shell_path svc_output_file ^
    1.76 -			" " ^ File.shell_path svc_input_file ^ 
    1.77 -			">/dev/null 2>&1"))
    1.78 +               execute (check_valid ^ " -dump-result " ^
    1.79 +                        File.shell_path svc_output_file ^
    1.80 +                        " " ^ File.shell_path svc_input_file ^
    1.81 +                        ">/dev/null 2>&1"))
    1.82        val svc_output =
    1.83          (case Library.try File.read svc_output_file of
    1.84            SOME out => out
    1.85 @@ -84,8 +84,7 @@
    1.86        String.isPrefix "VALID" svc_output
    1.87    end
    1.88  
    1.89 - (*New exception constructor for passing arguments to the oracle*)
    1.90 - exception OracleExn of term;
    1.91 + fun fail t = raise TERM ("SVC oracle", [t]);
    1.92  
    1.93   fun apply c args =
    1.94       let val (ts, bs) = ListPair.unzip args
    1.95 @@ -95,36 +94,36 @@
    1.96     int or nat comparisons below*)
    1.97   val iff_tag =
    1.98     let fun tag t =
    1.99 -	 let val (c,ts) = strip_comb t
   1.100 -	 in  case c of
   1.101 -	     Const("op &", _)   => apply c (map tag ts)
   1.102 -	   | Const("op |", _)   => apply c (map tag ts)
   1.103 -	   | Const("op -->", _) => apply c (map tag ts)
   1.104 -	   | Const("Not", _)    => apply c (map tag ts)
   1.105 -	   | Const("True", _)   => (c, false)
   1.106 -	   | Const("False", _)  => (c, false)
   1.107 -	   | Const("op =", Type ("fun", [T,_])) => 
   1.108 -		 if T = HOLogic.boolT then
   1.109 -		     (*biconditional: with int/nat comparisons below?*)
   1.110 -		     let val [t1,t2] = ts
   1.111 -			 val (u1,b1) = tag t1
   1.112 -			 and (u2,b2) = tag t2
   1.113 -			 val cname = if b1 orelse b2 then "unfold" else "keep"
   1.114 -		     in 
   1.115 -			(Const ("SVC_Oracle.iff_" ^ cname, dummyT) $ u1 $ u2,
   1.116 -			 b1 orelse b2)
   1.117 -		     end
   1.118 -		 else (*might be numeric equality*) (t, is_intnat T)
   1.119 -	   | Const("op <", Type ("fun", [T,_]))  => (t, is_intnat T)
   1.120 -	   | Const("op <=", Type ("fun", [T,_])) => (t, is_intnat T)
   1.121 -	   | _ => (t, false)
   1.122 -	 end
   1.123 +         let val (c,ts) = strip_comb t
   1.124 +         in  case c of
   1.125 +             Const("op &", _)   => apply c (map tag ts)
   1.126 +           | Const("op |", _)   => apply c (map tag ts)
   1.127 +           | Const("op -->", _) => apply c (map tag ts)
   1.128 +           | Const("Not", _)    => apply c (map tag ts)
   1.129 +           | Const("True", _)   => (c, false)
   1.130 +           | Const("False", _)  => (c, false)
   1.131 +           | Const("op =", Type ("fun", [T,_])) =>
   1.132 +                 if T = HOLogic.boolT then
   1.133 +                     (*biconditional: with int/nat comparisons below?*)
   1.134 +                     let val [t1,t2] = ts
   1.135 +                         val (u1,b1) = tag t1
   1.136 +                         and (u2,b2) = tag t2
   1.137 +                         val cname = if b1 orelse b2 then "unfold" else "keep"
   1.138 +                     in
   1.139 +                        (Const ("SVC_Oracle.iff_" ^ cname, dummyT) $ u1 $ u2,
   1.140 +                         b1 orelse b2)
   1.141 +                     end
   1.142 +                 else (*might be numeric equality*) (t, is_intnat T)
   1.143 +           | Const("op <", Type ("fun", [T,_]))  => (t, is_intnat T)
   1.144 +           | Const("op <=", Type ("fun", [T,_])) => (t, is_intnat T)
   1.145 +           | _ => (t, false)
   1.146 +         end
   1.147     in #1 o tag end;
   1.148  
   1.149   (*Map expression e to 0<=a --> e, where "a" is the name of a nat variable*)
   1.150 - fun add_nat_var (a, e) = 
   1.151 + fun add_nat_var (a, e) =
   1.152       Buildin("=>", [Buildin("<=", [Int 0, UnInterp (a, [])]),
   1.153 -		    e]);
   1.154 +                    e]);
   1.155  
   1.156   fun param_string [] = ""
   1.157     | param_string is = "_" ^ space_implode "_" (map string_of_int is)
   1.158 @@ -138,123 +137,119 @@
   1.159      val nat_vars = ref ([] : string list)
   1.160      (*translation of a variable: record all natural numbers*)
   1.161      fun trans_var (a,T,is) =
   1.162 -	(if T = HOLogic.natT then nat_vars := (a ins_string (!nat_vars))
   1.163 -	                     else ();
   1.164 +        (if T = HOLogic.natT then nat_vars := (a ins_string (!nat_vars))
   1.165 +                             else ();
   1.166           UnInterp (a ^ param_string is, []))
   1.167      (*A variable, perhaps applied to a series of parameters*)
   1.168      fun var (Free(a,T), is)      = trans_var ("F_" ^ a, T, is)
   1.169        | var (Var((a, 0), T), is) = trans_var (a, T, is)
   1.170 -      | var (Bound i, is)        = 
   1.171 +      | var (Bound i, is)        =
   1.172            let val (a,T) = List.nth (params, i)
   1.173 -	  in  trans_var ("B_" ^ a, T, is)  end
   1.174 +          in  trans_var ("B_" ^ a, T, is)  end
   1.175        | var (t $ Bound i, is)    = var(t,i::is)
   1.176              (*removing a parameter from a Var: the bound var index will
   1.177                 become part of the Var's name*)
   1.178 -      | var (t,_) = raise OracleExn t;
   1.179 +      | var (t,_) = fail t;
   1.180      (*translation of a literal*)
   1.181      fun lit (Const("Numeral.number_of", _) $ w) =
   1.182            (HOLogic.dest_binum w handle TERM _ => raise Match)
   1.183        | lit (Const("0", _)) = 0
   1.184        | lit (Const("1", _)) = 1
   1.185      (*translation of a literal expression [no variables]*)
   1.186 -    fun litExp (Const("op +", T) $ x $ y) = 
   1.187 -	  if is_numeric_op T then (litExp x) + (litExp y)
   1.188 -          else raise OracleExn t
   1.189 -      | litExp (Const("op -", T) $ x $ y) = 
   1.190 -	  if is_numeric_op T then (litExp x) - (litExp y)
   1.191 -          else raise OracleExn t
   1.192 -      | litExp (Const("op *", T) $ x $ y) = 
   1.193 -	  if is_numeric_op T then (litExp x) * (litExp y)
   1.194 -          else raise OracleExn t
   1.195 -      | litExp (Const("uminus", T) $ x)   = 
   1.196 -	  if is_numeric_op T then ~(litExp x)
   1.197 -          else raise OracleExn t
   1.198 -      | litExp t = lit t 
   1.199 -		   handle Match => raise OracleExn t
   1.200 +    fun litExp (Const("op +", T) $ x $ y) =
   1.201 +          if is_numeric_op T then (litExp x) + (litExp y)
   1.202 +          else fail t
   1.203 +      | litExp (Const("op -", T) $ x $ y) =
   1.204 +          if is_numeric_op T then (litExp x) - (litExp y)
   1.205 +          else fail t
   1.206 +      | litExp (Const("op *", T) $ x $ y) =
   1.207 +          if is_numeric_op T then (litExp x) * (litExp y)
   1.208 +          else fail t
   1.209 +      | litExp (Const("uminus", T) $ x)   =
   1.210 +          if is_numeric_op T then ~(litExp x)
   1.211 +          else fail t
   1.212 +      | litExp t = lit t
   1.213 +                   handle Match => fail t
   1.214      (*translation of a real/rational expression*)
   1.215      fun suc t = Interp("+", [Int 1, t])
   1.216      fun tm (Const("Suc", T) $ x) = suc (tm x)
   1.217 -      | tm (Const("op +", T) $ x $ y) = 
   1.218 -	  if is_numeric_op T then Interp("+", [tm x, tm y])
   1.219 -          else raise OracleExn t
   1.220 -      | tm (Const("op -", T) $ x $ y) = 
   1.221 -	  if is_numeric_op T then 
   1.222 -	      Interp("+", [tm x, Interp("*", [Int ~1, tm y])])
   1.223 -          else raise OracleExn t
   1.224 -      | tm (Const("op *", T) $ x $ y) = 
   1.225 -	  if is_numeric_op T then Interp("*", [tm x, tm y])
   1.226 -          else raise OracleExn t
   1.227 -      | tm (Const("RealDef.rinv", T) $ x) = 
   1.228 -	  if domain_type T = HOLogic.realT then 
   1.229 -	      Rat(1, litExp x)
   1.230 -          else raise OracleExn t
   1.231 -      | tm (Const("uminus", T) $ x) = 
   1.232 -	  if is_numeric_op T then Interp("*", [Int ~1, tm x])
   1.233 -          else raise OracleExn t
   1.234 -      | tm t = Int (lit t) 
   1.235 -	       handle Match => var (t,[])
   1.236 +      | tm (Const("op +", T) $ x $ y) =
   1.237 +          if is_numeric_op T then Interp("+", [tm x, tm y])
   1.238 +          else fail t
   1.239 +      | tm (Const("op -", T) $ x $ y) =
   1.240 +          if is_numeric_op T then
   1.241 +              Interp("+", [tm x, Interp("*", [Int ~1, tm y])])
   1.242 +          else fail t
   1.243 +      | tm (Const("op *", T) $ x $ y) =
   1.244 +          if is_numeric_op T then Interp("*", [tm x, tm y])
   1.245 +          else fail t
   1.246 +      | tm (Const("RealDef.rinv", T) $ x) =
   1.247 +          if domain_type T = HOLogic.realT then
   1.248 +              Rat(1, litExp x)
   1.249 +          else fail t
   1.250 +      | tm (Const("uminus", T) $ x) =
   1.251 +          if is_numeric_op T then Interp("*", [Int ~1, tm x])
   1.252 +          else fail t
   1.253 +      | tm t = Int (lit t)
   1.254 +               handle Match => var (t,[])
   1.255      (*translation of a formula*)
   1.256 -    and fm pos (Const("op &", _) $ p $ q) =  
   1.257 -	    Buildin("AND", [fm pos p, fm pos q])
   1.258 -      | fm pos (Const("op |", _) $ p $ q) =  
   1.259 -	    Buildin("OR", [fm pos p, fm pos q])
   1.260 -      | fm pos (Const("op -->", _) $ p $ q) =  
   1.261 -	    Buildin("=>", [fm (not pos) p, fm pos q])
   1.262 -      | fm pos (Const("Not", _) $ p) =  
   1.263 -	    Buildin("NOT", [fm (not pos) p])
   1.264 +    and fm pos (Const("op &", _) $ p $ q) =
   1.265 +            Buildin("AND", [fm pos p, fm pos q])
   1.266 +      | fm pos (Const("op |", _) $ p $ q) =
   1.267 +            Buildin("OR", [fm pos p, fm pos q])
   1.268 +      | fm pos (Const("op -->", _) $ p $ q) =
   1.269 +            Buildin("=>", [fm (not pos) p, fm pos q])
   1.270 +      | fm pos (Const("Not", _) $ p) =
   1.271 +            Buildin("NOT", [fm (not pos) p])
   1.272        | fm pos (Const("True", _)) = TrueExpr
   1.273        | fm pos (Const("False", _)) = FalseExpr
   1.274 -      | fm pos (Const("SVC_Oracle.iff_keep", _) $ p $ q) = 
   1.275 -	     (*polarity doesn't matter*)
   1.276 -	    Buildin("=", [fm pos p, fm pos q]) 
   1.277 -      | fm pos (Const("SVC_Oracle.iff_unfold", _) $ p $ q) = 
   1.278 -	    Buildin("AND",   (*unfolding uses both polarities*)
   1.279 -			 [Buildin("=>", [fm (not pos) p, fm pos q]),
   1.280 -			  Buildin("=>", [fm (not pos) q, fm pos p])])
   1.281 -      | fm pos (t as Const("op =", Type ("fun", [T,_])) $ x $ y) = 
   1.282 -	    let val tx = tm x and ty = tm y
   1.283 -		in if pos orelse T = HOLogic.realT then
   1.284 -		       Buildin("=", [tx, ty])
   1.285 -		   else if is_intnat T then
   1.286 -		       Buildin("AND", 
   1.287 -				    [Buildin("<", [tx, suc ty]), 
   1.288 -				     Buildin("<", [ty, suc tx])])
   1.289 -		   else raise OracleExn t
   1.290 -	    end
   1.291 -	(*inequalities: possible types are nat, int, real*)
   1.292 -      | fm pos (t as Const("op <",  Type ("fun", [T,_])) $ x $ y) = 
   1.293 -	    if not pos orelse T = HOLogic.realT then
   1.294 -		Buildin("<", [tm x, tm y])
   1.295 -	    else if is_intnat T then
   1.296 -		Buildin("<=", [suc (tm x), tm y])
   1.297 -	    else raise OracleExn t
   1.298 -      | fm pos (t as Const("op <=",  Type ("fun", [T,_])) $ x $ y) = 
   1.299 -	    if pos orelse T = HOLogic.realT then
   1.300 -		Buildin("<=", [tm x, tm y])
   1.301 -	    else if is_intnat T then
   1.302 -		Buildin("<", [tm x, suc (tm y)])
   1.303 -	    else raise OracleExn t
   1.304 +      | fm pos (Const("SVC_Oracle.iff_keep", _) $ p $ q) =
   1.305 +             (*polarity doesn't matter*)
   1.306 +            Buildin("=", [fm pos p, fm pos q])
   1.307 +      | fm pos (Const("SVC_Oracle.iff_unfold", _) $ p $ q) =
   1.308 +            Buildin("AND",   (*unfolding uses both polarities*)
   1.309 +                         [Buildin("=>", [fm (not pos) p, fm pos q]),
   1.310 +                          Buildin("=>", [fm (not pos) q, fm pos p])])
   1.311 +      | fm pos (t as Const("op =", Type ("fun", [T,_])) $ x $ y) =
   1.312 +            let val tx = tm x and ty = tm y
   1.313 +                in if pos orelse T = HOLogic.realT then
   1.314 +                       Buildin("=", [tx, ty])
   1.315 +                   else if is_intnat T then
   1.316 +                       Buildin("AND",
   1.317 +                                    [Buildin("<", [tx, suc ty]),
   1.318 +                                     Buildin("<", [ty, suc tx])])
   1.319 +                   else fail t
   1.320 +            end
   1.321 +        (*inequalities: possible types are nat, int, real*)
   1.322 +      | fm pos (t as Const("op <",  Type ("fun", [T,_])) $ x $ y) =
   1.323 +            if not pos orelse T = HOLogic.realT then
   1.324 +                Buildin("<", [tm x, tm y])
   1.325 +            else if is_intnat T then
   1.326 +                Buildin("<=", [suc (tm x), tm y])
   1.327 +            else fail t
   1.328 +      | fm pos (t as Const("op <=",  Type ("fun", [T,_])) $ x $ y) =
   1.329 +            if pos orelse T = HOLogic.realT then
   1.330 +                Buildin("<=", [tm x, tm y])
   1.331 +            else if is_intnat T then
   1.332 +                Buildin("<", [tm x, suc (tm y)])
   1.333 +            else fail t
   1.334        | fm pos t = var(t,[]);
   1.335        (*entry point, and translation of a meta-formula*)
   1.336        fun mt pos ((c as Const("Trueprop", _)) $ p) = fm pos (iff_tag p)
   1.337 -	| mt pos ((c as Const("==>", _)) $ p $ q) = 
   1.338 -	    Buildin("=>", [mt (not pos) p, mt pos q])
   1.339 -	| mt pos t = fm pos (iff_tag t)  (*it might be a formula*)
   1.340 +        | mt pos ((c as Const("==>", _)) $ p $ q) =
   1.341 +            Buildin("=>", [mt (not pos) p, mt pos q])
   1.342 +        | mt pos t = fm pos (iff_tag t)  (*it might be a formula*)
   1.343  
   1.344        val body_e = mt pos body  (*evaluate now to assign into !nat_vars*)
   1.345 -  in 
   1.346 -     foldr add_nat_var body_e (!nat_vars) 
   1.347 +  in
   1.348 +     foldr add_nat_var body_e (!nat_vars)
   1.349    end;
   1.350  
   1.351  
   1.352   (*The oracle proves the given formula t, if possible*)
   1.353 - fun oracle (sign, OracleExn t) = 
   1.354 -   let val dummy = if !trace then tracing ("Subgoal abstracted to\n" ^
   1.355 -					   Sign.string_of_term sign t)
   1.356 -                   else ()
   1.357 -   in
   1.358 -       if valid (expr_of false t) then t
   1.359 -       else raise OracleExn t
   1.360 -   end;
   1.361 + fun oracle thy t =
   1.362 +  (conditional (! trace) (fn () =>
   1.363 +    tracing ("SVC oracle: problem is\n" ^ Sign.string_of_term thy t));
   1.364 +  if valid (expr_of false t) then t else fail t);
   1.365  
   1.366  end;