discontinued unused / unmaintained SVC oracle -- current Isabelle tools (e.g. arith, smt) can easily solve the given examples with full proof reconstruction;
authorwenzelm
Mon Jun 01 15:39:53 2015 +0200 (2015-06-01)
changeset 603327676bcaa1f95
parent 60331 f215fd466e30
child 60333 fd54c15231d3
discontinued unused / unmaintained SVC oracle -- current Isabelle tools (e.g. arith, smt) can easily solve the given examples with full proof reconstruction;
src/HOL/ROOT
src/HOL/ex/SVC_Oracle.thy
src/HOL/ex/svc_funcs.ML
src/HOL/ex/svc_test.thy
     1.1 --- a/src/HOL/ROOT	Mon Jun 01 15:06:09 2015 +0200
     1.2 +++ b/src/HOL/ROOT	Mon Jun 01 15:39:53 2015 +0200
     1.3 @@ -588,7 +588,6 @@
     1.4      Set_Comprehension_Pointfree_Examples
     1.5      Parallel_Example
     1.6      IArray_Examples
     1.7 -    SVC_Oracle
     1.8      Simps_Case_Conv_Examples
     1.9      ML
    1.10      Rewrite_Examples
    1.11 @@ -597,8 +596,6 @@
    1.12      SOS_Cert
    1.13    theories [skip_proofs = false]
    1.14      Meson_Test
    1.15 -  theories [condition = SVC_HOME]
    1.16 -    svc_test
    1.17    theories [condition = ISABELLE_FULL_TEST]
    1.18      Sudoku
    1.19    document_files "root.bib" "root.tex"
     2.1 --- a/src/HOL/ex/SVC_Oracle.thy	Mon Jun 01 15:06:09 2015 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,122 +0,0 @@
     2.4 -(*  Title:      HOL/ex/SVC_Oracle.thy
     2.5 -    Author:     Lawrence C Paulson
     2.6 -    Copyright   1999  University of Cambridge
     2.7 -
     2.8 -Based upon the work of Søren T. Heilmann.
     2.9 -*)
    2.10 -
    2.11 -section {* Installing an oracle for SVC (Stanford Validity Checker) *}
    2.12 -
    2.13 -theory SVC_Oracle
    2.14 -imports Main
    2.15 -begin
    2.16 -
    2.17 -consts
    2.18 -  iff_keep :: "[bool, bool] => bool"
    2.19 -  iff_unfold :: "[bool, bool] => bool"
    2.20 -
    2.21 -ML_file "svc_funcs.ML"
    2.22 -
    2.23 -hide_const iff_keep iff_unfold
    2.24 -
    2.25 -oracle svc_oracle = Svc.oracle
    2.26 -
    2.27 -ML {*
    2.28 -(*
    2.29 -Installing the oracle for SVC (Stanford Validity Checker)
    2.30 -
    2.31 -The following code merely CALLS the oracle;
    2.32 -  the soundness-critical functions are at svc_funcs.ML
    2.33 -
    2.34 -Based upon the work of Søren T. Heilmann
    2.35 -*)
    2.36 -
    2.37 -
    2.38 -(*Generalize an Isabelle formula, replacing by Vars
    2.39 -  all subterms not intelligible to SVC.*)
    2.40 -fun svc_abstract t =
    2.41 -  let
    2.42 -    (*The oracle's result is given to the subgoal using compose_tac because
    2.43 -      its premises are matched against the assumptions rather than used
    2.44 -      to make subgoals.  Therefore , abstraction must copy the parameters
    2.45 -      precisely and make them available to all generated Vars.*)
    2.46 -    val params = Term.strip_all_vars t
    2.47 -    and body   = Term.strip_all_body t
    2.48 -    val Us = map #2 params
    2.49 -    val nPar = length params
    2.50 -    val vname = Unsynchronized.ref "V_a"
    2.51 -    val pairs = Unsynchronized.ref ([] : (term*term) list)
    2.52 -    fun insert t =
    2.53 -        let val T = fastype_of t
    2.54 -            val v = Logic.combound (Var ((!vname,0), Us--->T), 0, nPar)
    2.55 -        in  vname := Symbol.bump_string (!vname);
    2.56 -            pairs := (t, v) :: !pairs;
    2.57 -            v
    2.58 -        end;
    2.59 -    fun replace t =
    2.60 -        case t of
    2.61 -            Free _  => t  (*but not existing Vars, lest the names clash*)
    2.62 -          | Bound _ => t
    2.63 -          | _ => (case AList.lookup Envir.aeconv (!pairs) t of
    2.64 -                      SOME v => v
    2.65 -                    | NONE   => insert t)
    2.66 -    (*abstraction of a numeric literal*)
    2.67 -    fun lit t = if can HOLogic.dest_number t then t else replace t;
    2.68 -    (*abstraction of a real/rational expression*)
    2.69 -    fun rat ((c as Const(@{const_name Groups.plus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
    2.70 -      | rat ((c as Const(@{const_name Groups.minus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
    2.71 -      | rat ((c as Const(@{const_name Fields.divide}, _)) $ x $ y) = c $ (rat x) $ (rat y)
    2.72 -      | rat ((c as Const(@{const_name Groups.times}, _)) $ x $ y) = c $ (rat x) $ (rat y)
    2.73 -      | rat ((c as Const(@{const_name Groups.uminus}, _)) $ x) = c $ (rat x)
    2.74 -      | rat t = lit t
    2.75 -    (*abstraction of an integer expression: no div, mod*)
    2.76 -    fun int ((c as Const(@{const_name Groups.plus}, _)) $ x $ y) = c $ (int x) $ (int y)
    2.77 -      | int ((c as Const(@{const_name Groups.minus}, _)) $ x $ y) = c $ (int x) $ (int y)
    2.78 -      | int ((c as Const(@{const_name Groups.times}, _)) $ x $ y) = c $ (int x) $ (int y)
    2.79 -      | int ((c as Const(@{const_name Groups.uminus}, _)) $ x) = c $ (int x)
    2.80 -      | int t = lit t
    2.81 -    (*abstraction of a natural number expression: no minus*)
    2.82 -    fun nat ((c as Const(@{const_name Groups.plus}, _)) $ x $ y) = c $ (nat x) $ (nat y)
    2.83 -      | nat ((c as Const(@{const_name Groups.times}, _)) $ x $ y) = c $ (nat x) $ (nat y)
    2.84 -      | nat ((c as Const(@{const_name Suc}, _)) $ x) = c $ (nat x)
    2.85 -      | nat t = lit t
    2.86 -    (*abstraction of a relation: =, <, <=*)
    2.87 -    fun rel (T, c $ x $ y) =
    2.88 -            if T = HOLogic.realT then c $ (rat x) $ (rat y)
    2.89 -            else if T = HOLogic.intT then c $ (int x) $ (int y)
    2.90 -            else if T = HOLogic.natT then c $ (nat x) $ (nat y)
    2.91 -            else if T = HOLogic.boolT then c $ (fm x) $ (fm y)
    2.92 -            else replace (c $ x $ y)   (*non-numeric comparison*)
    2.93 -    (*abstraction of a formula*)
    2.94 -    and fm ((c as Const(@{const_name HOL.conj}, _)) $ p $ q) = c $ (fm p) $ (fm q)
    2.95 -      | fm ((c as Const(@{const_name HOL.disj}, _)) $ p $ q) = c $ (fm p) $ (fm q)
    2.96 -      | fm ((c as Const(@{const_name HOL.implies}, _)) $ p $ q) = c $ (fm p) $ (fm q)
    2.97 -      | fm ((c as Const(@{const_name Not}, _)) $ p) = c $ (fm p)
    2.98 -      | fm ((c as Const(@{const_name True}, _))) = c
    2.99 -      | fm ((c as Const(@{const_name False}, _))) = c
   2.100 -      | fm (t as Const(@{const_name HOL.eq},  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
   2.101 -      | fm (t as Const(@{const_name Orderings.less},  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
   2.102 -      | fm (t as Const(@{const_name Orderings.less_eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
   2.103 -      | fm t = replace t
   2.104 -    (*entry point, and abstraction of a meta-formula*)
   2.105 -    fun mt ((c as Const(@{const_name Trueprop}, _)) $ p) = c $ (fm p)
   2.106 -      | mt ((c as Const(@{const_name Pure.imp}, _)) $ p $ q)  = c $ (mt p) $ (mt q)
   2.107 -      | mt t = fm t  (*it might be a formula*)
   2.108 -  in (Logic.list_all (params, mt body), !pairs) end;
   2.109 -
   2.110 -
   2.111 -(*Present the entire subgoal to the oracle, assumptions and all, but possibly
   2.112 -  abstracted.  Use via compose_tac, which performs no lifting but will
   2.113 -  instantiate variables.*)
   2.114 -
   2.115 -fun svc_tac ctxt = CSUBGOAL (fn (ct, i) =>
   2.116 -  let
   2.117 -    val (abs_goal, _) = svc_abstract (Thm.term_of ct);
   2.118 -    val th = svc_oracle (Thm.cterm_of ctxt abs_goal);
   2.119 -   in compose_tac ctxt (false, th, 0) i end
   2.120 -   handle TERM _ => no_tac);
   2.121 -*}
   2.122 -
   2.123 -method_setup svc = {* Scan.succeed (SIMPLE_METHOD' o svc_tac) *}
   2.124 -
   2.125 -end
     3.1 --- a/src/HOL/ex/svc_funcs.ML	Mon Jun 01 15:06:09 2015 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,255 +0,0 @@
     3.4 -(*  Title:      HOL/ex/svc_funcs.ML
     3.5 -    Author:     Lawrence C Paulson
     3.6 -    Copyright   1999  University of Cambridge
     3.7 -
     3.8 -Translation functions for the interface to SVC.
     3.9 -
    3.10 -Based upon the work of Soren T. Heilmann
    3.11 -
    3.12 -Integers and naturals are translated as follows:
    3.13 -  In a positive context, replace x<y by x+1<=y
    3.14 -  In a negative context, replace x<=y by x<y+1
    3.15 -  In a negative context, replace x=y by x<y+1 & y<x+1
    3.16 -Biconditionals (if-and-only-iff) are expanded if they require such translations
    3.17 -  in either operand.
    3.18 -
    3.19 -For each variable of type nat, an assumption is added that it is non-negative.
    3.20 -
    3.21 -Relevant Isabelle environment settings:
    3.22 -
    3.23 -  #SVC_HOME=
    3.24 -  #SVC_MACHINE=i386-redhat-linux
    3.25 -  #SVC_MACHINE=sparc-sun-solaris
    3.26 -*)
    3.27 -
    3.28 -structure Svc =
    3.29 -struct
    3.30 - val trace = Unsynchronized.ref false;
    3.31 -
    3.32 - datatype expr =
    3.33 -     Buildin of string * expr list
    3.34 -   | Interp of string * expr list
    3.35 -   | UnInterp of string * expr list
    3.36 -   | FalseExpr
    3.37 -   | TrueExpr
    3.38 -   | Int of int
    3.39 -   | Rat of int * int;
    3.40 -
    3.41 - fun is_intnat T = T = HOLogic.intT orelse T = HOLogic.natT;
    3.42 -
    3.43 - fun is_numeric T = is_intnat T orelse T = HOLogic.realT;
    3.44 -
    3.45 - fun is_numeric_op T = is_numeric (domain_type T);
    3.46 -
    3.47 - fun toString t =
    3.48 -     let fun ue (Buildin(s, l)) =
    3.49 -             "(" ^ s ^ (Library.foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ ") "
    3.50 -           | ue (Interp(s, l)) =
    3.51 -             "{" ^ s ^ (Library.foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ "} "
    3.52 -           | ue (UnInterp(s, l)) =
    3.53 -             "(" ^ s ^ (Library.foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ ") "
    3.54 -           | ue (FalseExpr) = "FALSE "
    3.55 -           | ue (TrueExpr)  = "TRUE "
    3.56 -           | ue (Int i)     = signed_string_of_int i ^ " "
    3.57 -           | ue (Rat(i, j)) = signed_string_of_int i ^ "|" ^ signed_string_of_int j ^ " "
    3.58 -     in
    3.59 -         ue t
    3.60 -     end;
    3.61 -
    3.62 - fun valid e =
    3.63 -  let val svc_home = getenv "SVC_HOME"
    3.64 -      val svc_machine = getenv "SVC_MACHINE"
    3.65 -      val check_valid = if svc_home = ""
    3.66 -                        then error "Environment variable SVC_HOME not set"
    3.67 -                        else if svc_machine = ""
    3.68 -                        then error "Environment variable SVC_MACHINE not set"
    3.69 -                        else svc_home ^ "/" ^ svc_machine ^ "/bin/check_valid"
    3.70 -      val svc_input = toString e
    3.71 -      val _ = if !trace then tracing ("Calling SVC:\n" ^ svc_input) else ()
    3.72 -      val svc_input_file  = File.tmp_path (Path.basic "SVM_in");
    3.73 -      val svc_output_file = File.tmp_path (Path.basic "SVM_out");
    3.74 -      val _ = File.write svc_input_file svc_input;
    3.75 -      val _ =
    3.76 -        Isabelle_System.bash_output (check_valid ^ " -dump-result " ^
    3.77 -          File.shell_path svc_output_file ^ " " ^ File.shell_path svc_input_file ^
    3.78 -          ">/dev/null 2>&1")
    3.79 -      val svc_output =
    3.80 -        (case try File.read svc_output_file of
    3.81 -          SOME out => out
    3.82 -        | NONE => error "SVC returned no output");
    3.83 -  in
    3.84 -      if ! trace then tracing ("SVC Returns:\n" ^ svc_output)
    3.85 -      else (File.rm svc_input_file; File.rm svc_output_file);
    3.86 -      String.isPrefix "VALID" svc_output
    3.87 -  end
    3.88 -
    3.89 - fun fail t = raise TERM ("SVC oracle", [t]);
    3.90 -
    3.91 - fun apply c args =
    3.92 -     let val (ts, bs) = ListPair.unzip args
    3.93 -     in  (list_comb(c,ts), exists I bs)  end;
    3.94 -
    3.95 - (*Determining whether the biconditionals must be unfolded: if there are
    3.96 -   int or nat comparisons below*)
    3.97 - val iff_tag =
    3.98 -   let fun tag t =
    3.99 -         let val (c,ts) = strip_comb t
   3.100 -         in  case c of
   3.101 -             Const(@{const_name HOL.conj}, _)   => apply c (map tag ts)
   3.102 -           | Const(@{const_name HOL.disj}, _)   => apply c (map tag ts)
   3.103 -           | Const(@{const_name HOL.implies}, _) => apply c (map tag ts)
   3.104 -           | Const(@{const_name Not}, _)    => apply c (map tag ts)
   3.105 -           | Const(@{const_name True}, _)   => (c, false)
   3.106 -           | Const(@{const_name False}, _)  => (c, false)
   3.107 -           | Const(@{const_name HOL.eq}, Type ("fun", [T,_])) =>
   3.108 -                 if T = HOLogic.boolT then
   3.109 -                     (*biconditional: with int/nat comparisons below?*)
   3.110 -                     let val [t1,t2] = ts
   3.111 -                         val (u1,b1) = tag t1
   3.112 -                         and (u2,b2) = tag t2
   3.113 -                         val cname = if b1 orelse b2 then "unfold" else "keep"
   3.114 -                     in
   3.115 -                        (Const ("SVC_Oracle.iff_" ^ cname, dummyT) $ u1 $ u2,
   3.116 -                         b1 orelse b2)
   3.117 -                     end
   3.118 -                 else (*might be numeric equality*) (t, is_intnat T)
   3.119 -           | Const(@{const_name Orderings.less}, Type ("fun", [T,_]))  => (t, is_intnat T)
   3.120 -           | Const(@{const_name Orderings.less_eq}, Type ("fun", [T,_])) => (t, is_intnat T)
   3.121 -           | _ => (t, false)
   3.122 -         end
   3.123 -   in #1 o tag end;
   3.124 -
   3.125 - (*Map expression e to 0<=a --> e, where "a" is the name of a nat variable*)
   3.126 - fun add_nat_var a e =
   3.127 -     Buildin("=>", [Buildin("<=", [Int 0, UnInterp (a, [])]),
   3.128 -                    e]);
   3.129 -
   3.130 - fun param_string [] = ""
   3.131 -   | param_string is = "_" ^ space_implode "_" (map string_of_int is)
   3.132 -
   3.133 - (*Translate an Isabelle formula into an SVC expression
   3.134 -   pos ["positive"]: true if an assumption, false if a goal*)
   3.135 - fun expr_of pos t =
   3.136 -  let
   3.137 -    val params = rev (Term.rename_wrt_term t (Term.strip_all_vars t))
   3.138 -    and body   = Term.strip_all_body t
   3.139 -    val nat_vars = Unsynchronized.ref ([] : string list)
   3.140 -    (*translation of a variable: record all natural numbers*)
   3.141 -    fun trans_var (a,T,is) =
   3.142 -        (if T = HOLogic.natT then nat_vars := (insert (op =) a (!nat_vars))
   3.143 -                             else ();
   3.144 -         UnInterp (a ^ param_string is, []))
   3.145 -    (*A variable, perhaps applied to a series of parameters*)
   3.146 -    fun var (Free(a,T), is)      = trans_var ("F_" ^ a, T, is)
   3.147 -      | var (Var((a, 0), T), is) = trans_var (a, T, is)
   3.148 -      | var (Bound i, is)        =
   3.149 -          let val (a,T) = nth params i
   3.150 -          in  trans_var ("B_" ^ a, T, is)  end
   3.151 -      | var (t $ Bound i, is)    = var(t,i::is)
   3.152 -            (*removing a parameter from a Var: the bound var index will
   3.153 -               become part of the Var's name*)
   3.154 -      | var (t,_) = fail t;
   3.155 -    (*translation of a literal*)
   3.156 -    val lit = snd o HOLogic.dest_number;
   3.157 -    (*translation of a literal expression [no variables]*)
   3.158 -    fun litExp (Const(@{const_name Groups.plus}, T) $ x $ y) =
   3.159 -          if is_numeric_op T then (litExp x) + (litExp y)
   3.160 -          else fail t
   3.161 -      | litExp (Const(@{const_name Groups.minus}, T) $ x $ y) =
   3.162 -          if is_numeric_op T then (litExp x) - (litExp y)
   3.163 -          else fail t
   3.164 -      | litExp (Const(@{const_name Groups.times}, T) $ x $ y) =
   3.165 -          if is_numeric_op T then (litExp x) * (litExp y)
   3.166 -          else fail t
   3.167 -      | litExp (Const(@{const_name Groups.uminus}, T) $ x)   =
   3.168 -          if is_numeric_op T then ~(litExp x)
   3.169 -          else fail t
   3.170 -      | litExp t = lit t
   3.171 -                   handle Match => fail t
   3.172 -    (*translation of a real/rational expression*)
   3.173 -    fun suc t = Interp("+", [Int 1, t])
   3.174 -    fun tm (Const(@{const_name Suc}, T) $ x) = suc (tm x)
   3.175 -      | tm (Const(@{const_name Groups.plus}, T) $ x $ y) =
   3.176 -          if is_numeric_op T then Interp("+", [tm x, tm y])
   3.177 -          else fail t
   3.178 -      | tm (Const(@{const_name Groups.minus}, T) $ x $ y) =
   3.179 -          if is_numeric_op T then
   3.180 -              Interp("+", [tm x, Interp("*", [Int ~1, tm y])])
   3.181 -          else fail t
   3.182 -      | tm (Const(@{const_name Groups.times}, T) $ x $ y) =
   3.183 -          if is_numeric_op T then Interp("*", [tm x, tm y])
   3.184 -          else fail t
   3.185 -      | tm (Const(@{const_name Fields.inverse}, T) $ x) =
   3.186 -          if domain_type T = HOLogic.realT then
   3.187 -              Rat(1, litExp x)
   3.188 -          else fail t
   3.189 -      | tm (Const(@{const_name Groups.uminus}, T) $ x) =
   3.190 -          if is_numeric_op T then Interp("*", [Int ~1, tm x])
   3.191 -          else fail t
   3.192 -      | tm t = Int (lit t)
   3.193 -               handle Match => var (t,[])
   3.194 -    (*translation of a formula*)
   3.195 -    and fm pos (Const(@{const_name HOL.conj}, _) $ p $ q) =
   3.196 -            Buildin("AND", [fm pos p, fm pos q])
   3.197 -      | fm pos (Const(@{const_name HOL.disj}, _) $ p $ q) =
   3.198 -            Buildin("OR", [fm pos p, fm pos q])
   3.199 -      | fm pos (Const(@{const_name HOL.implies}, _) $ p $ q) =
   3.200 -            Buildin("=>", [fm (not pos) p, fm pos q])
   3.201 -      | fm pos (Const(@{const_name Not}, _) $ p) =
   3.202 -            Buildin("NOT", [fm (not pos) p])
   3.203 -      | fm pos (Const(@{const_name True}, _)) = TrueExpr
   3.204 -      | fm pos (Const(@{const_name False}, _)) = FalseExpr
   3.205 -      | fm pos (Const(@{const_name iff_keep}, _) $ p $ q) =
   3.206 -             (*polarity doesn't matter*)
   3.207 -            Buildin("=", [fm pos p, fm pos q])
   3.208 -      | fm pos (Const(@{const_name iff_unfold}, _) $ p $ q) =
   3.209 -            Buildin("AND",   (*unfolding uses both polarities*)
   3.210 -                         [Buildin("=>", [fm (not pos) p, fm pos q]),
   3.211 -                          Buildin("=>", [fm (not pos) q, fm pos p])])
   3.212 -      | fm pos (t as Const(@{const_name HOL.eq}, Type ("fun", [T,_])) $ x $ y) =
   3.213 -            let val tx = tm x and ty = tm y
   3.214 -                in if pos orelse T = HOLogic.realT then
   3.215 -                       Buildin("=", [tx, ty])
   3.216 -                   else if is_intnat T then
   3.217 -                       Buildin("AND",
   3.218 -                                    [Buildin("<", [tx, suc ty]),
   3.219 -                                     Buildin("<", [ty, suc tx])])
   3.220 -                   else fail t
   3.221 -            end
   3.222 -        (*inequalities: possible types are nat, int, real*)
   3.223 -      | fm pos (t as Const(@{const_name Orderings.less},  Type ("fun", [T,_])) $ x $ y) =
   3.224 -            if not pos orelse T = HOLogic.realT then
   3.225 -                Buildin("<", [tm x, tm y])
   3.226 -            else if is_intnat T then
   3.227 -                Buildin("<=", [suc (tm x), tm y])
   3.228 -            else fail t
   3.229 -      | fm pos (t as Const(@{const_name Orderings.less_eq},  Type ("fun", [T,_])) $ x $ y) =
   3.230 -            if pos orelse T = HOLogic.realT then
   3.231 -                Buildin("<=", [tm x, tm y])
   3.232 -            else if is_intnat T then
   3.233 -                Buildin("<", [tm x, suc (tm y)])
   3.234 -            else fail t
   3.235 -      | fm pos t = var(t,[]);
   3.236 -      (*entry point, and translation of a meta-formula*)
   3.237 -      fun mt pos ((c as Const(@{const_name Trueprop}, _)) $ p) = fm pos (iff_tag p)
   3.238 -        | mt pos ((c as Const(@{const_name Pure.imp}, _)) $ p $ q) =
   3.239 -            Buildin("=>", [mt (not pos) p, mt pos q])
   3.240 -        | mt pos t = fm pos (iff_tag t)  (*it might be a formula*)
   3.241 -
   3.242 -      val body_e = mt pos body  (*evaluate now to assign into !nat_vars*)
   3.243 -  in
   3.244 -     fold_rev add_nat_var (!nat_vars) body_e
   3.245 -  end;
   3.246 -
   3.247 -
   3.248 - (*The oracle proves the given formula, if possible*)
   3.249 -  fun oracle ct =
   3.250 -    let
   3.251 -      val thy = Thm.theory_of_cterm ct;
   3.252 -      val t = Thm.term_of ct;
   3.253 -      val _ =
   3.254 -        if ! trace then tracing ("SVC oracle: problem is\n" ^ Syntax.string_of_term_global thy t)
   3.255 -       else ();
   3.256 -    in if valid (expr_of false t) then ct else fail t end;
   3.257 -
   3.258 -end;
     4.1 --- a/src/HOL/ex/svc_test.thy	Mon Jun 01 15:06:09 2015 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,248 +0,0 @@
     4.4 -section {* Demonstrating the interface SVC *}
     4.5 -
     4.6 -theory svc_test
     4.7 -imports SVC_Oracle
     4.8 -begin
     4.9 -
    4.10 -subsubsection {* Propositional Logic *}
    4.11 -
    4.12 -text {*
    4.13 -  @{text "blast"}'s runtime for this type of problem appears to be exponential
    4.14 -  in its length, though @{text "fast"} manages.
    4.15 -*}
    4.16 -lemma "P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P"
    4.17 -  by svc
    4.18 -
    4.19 -
    4.20 -subsection {* Some big tautologies supplied by John Harrison *}
    4.21 -
    4.22 -text {*
    4.23 -  @{text "auto"} manages; @{text "blast"} and @{text "fast"} take a minute or more.
    4.24 -*}
    4.25 -lemma puz013_1: "~(~v12 &
    4.26 -   v0 &
    4.27 -   v10 &
    4.28 -   (v4 | v5) &
    4.29 -   (v9 | v2) &
    4.30 -   (v8 | v1) &
    4.31 -   (v7 | v0) &
    4.32 -   (v3 | v12) &
    4.33 -   (v11 | v10) &
    4.34 -   (~v12 | ~v6 | v7) &
    4.35 -   (~v10 | ~v3 | v1) &
    4.36 -   (~v10 | ~v0 | ~v4 | v11) &
    4.37 -   (~v5 | ~v2 | ~v8) &
    4.38 -   (~v12 | ~v9 | ~v7) &
    4.39 -   (~v0 | ~v1 | v4) &
    4.40 -   (~v4 | v7 | v2) &
    4.41 -   (~v12 | ~v3 | v8) &
    4.42 -   (~v4 | v5 | v6) &
    4.43 -   (~v7 | ~v8 | v9) &
    4.44 -   (~v10 | ~v11 | v12))"
    4.45 -  by svc
    4.46 -
    4.47 -lemma dk17_be:
    4.48 -  "(GE17 <-> ~IN4 & ~IN3 & ~IN2 & ~IN1) &
    4.49 -    (GE0 <-> GE17 & ~IN5) &
    4.50 -    (GE22 <-> ~IN9 & ~IN7 & ~IN6 & IN0) &
    4.51 -    (GE19 <-> ~IN5 & ~IN4 & ~IN3 & ~IN0) &
    4.52 -    (GE20 <-> ~IN7 & ~IN6) &
    4.53 -    (GE18 <-> ~IN6 & ~IN2 & ~IN1 & ~IN0) &
    4.54 -    (GE21 <-> IN9 & ~IN7 & IN6 & ~IN0) &
    4.55 -    (GE23 <-> GE22 & GE0) &
    4.56 -    (GE25 <-> ~IN9 & ~IN7 & IN6 & ~IN0) &
    4.57 -    (GE26 <-> IN9 & ~IN7 & ~IN6 & IN0) &
    4.58 -    (GE2 <-> GE20 & GE19) &
    4.59 -    (GE1 <-> GE18 & ~IN7) &
    4.60 -    (GE24 <-> GE23 | GE21 & GE0) &
    4.61 -    (GE5 <-> ~IN5 & IN4 | IN5 & ~IN4) &
    4.62 -    (GE6 <-> GE0 & IN7 & ~IN6 & ~IN0) &
    4.63 -    (GE12 <-> GE26 & GE0 | GE25 & GE0) &
    4.64 -    (GE14 <-> GE2 & IN8 & ~IN2 & IN1) &
    4.65 -    (GE27 <-> ~IN8 & IN5 & ~IN4 & ~IN3) &
    4.66 -    (GE9 <-> GE1 & ~IN5 & ~IN4 & IN3) &
    4.67 -    (GE7 <-> GE24 | GE2 & IN2 & ~IN1) &
    4.68 -    (GE10 <-> GE6 | GE5 & GE1 & ~IN3) &
    4.69 -    (GE15 <-> ~IN8 | IN9) &
    4.70 -    (GE16 <-> GE12 | GE14 & ~IN9) &
    4.71 -    (GE4 <->
    4.72 -     GE5 & GE1 & IN8 & ~IN3 |
    4.73 -     GE0 & ~IN7 & IN6 & ~IN0 |
    4.74 -     GE2 & IN2 & ~IN1) &
    4.75 -    (GE13 <-> GE27 & GE1) &
    4.76 -    (GE11 <-> GE9 | GE6 & ~IN8) &
    4.77 -    (GE8 <-> GE1 & ~IN5 & IN4 & ~IN3 | GE2 & ~IN2 & IN1) &
    4.78 -    (OUT0 <-> GE7 & ~IN8) &
    4.79 -    (OUT1 <-> GE7 & IN8) &
    4.80 -    (OUT2 <-> GE8 & ~IN9 | GE10 & IN8) &
    4.81 -    (OUT3 <-> GE8 & IN9 & ~IN8 | GE11 & ~IN9 | GE12 & ~IN8) &
    4.82 -    (OUT4 <-> GE11 & IN9 | GE12 & IN8) &
    4.83 -    (OUT5 <-> GE14 & IN9) &
    4.84 -    (OUT6 <-> GE13 & ~IN9) &
    4.85 -    (OUT7 <-> GE13 & IN9) &
    4.86 -    (OUT8 <-> GE9 & ~IN8 | GE15 & GE6 | GE4 & IN9) &
    4.87 -    (OUT9 <-> GE9 & IN8 | ~GE15 & GE10 | GE16) &
    4.88 -    (OUT10 <-> GE7) &
    4.89 -    (WRES0 <-> ~IN5 & ~IN4 & ~IN3 & ~IN2 & ~IN1) &
    4.90 -    (WRES1 <-> ~IN7 & ~IN6 & ~IN2 & ~IN1 & ~IN0) &
    4.91 -    (WRES2 <-> ~IN7 & ~IN6 & ~IN5 & ~IN4 & ~IN3 & ~IN0) &
    4.92 -    (WRES5 <-> ~IN5 & IN4 | IN5 & ~IN4) &
    4.93 -    (WRES6 <-> WRES0 & IN7 & ~IN6 & ~IN0) &
    4.94 -    (WRES9 <-> WRES1 & ~IN5 & ~IN4 & IN3) &
    4.95 -    (WRES7 <->
    4.96 -     WRES0 & ~IN9 & ~IN7 & ~IN6 & IN0 |
    4.97 -     WRES0 & IN9 & ~IN7 & IN6 & ~IN0 |
    4.98 -     WRES2 & IN2 & ~IN1) &
    4.99 -    (WRES10 <-> WRES6 | WRES5 & WRES1 & ~IN3) &
   4.100 -    (WRES12 <->
   4.101 -     WRES0 & IN9 & ~IN7 & ~IN6 & IN0 |
   4.102 -     WRES0 & ~IN9 & ~IN7 & IN6 & ~IN0) &
   4.103 -    (WRES14 <-> WRES2 & IN8 & ~IN2 & IN1) &
   4.104 -    (WRES15 <-> ~IN8 | IN9) &
   4.105 -    (WRES4 <->
   4.106 -     WRES5 & WRES1 & IN8 & ~IN3 |
   4.107 -     WRES2 & IN2 & ~IN1 |
   4.108 -     WRES0 & ~IN7 & IN6 & ~IN0) &
   4.109 -    (WRES13 <-> WRES1 & ~IN8 & IN5 & ~IN4 & ~IN3) &
   4.110 -    (WRES11 <-> WRES9 | WRES6 & ~IN8) &
   4.111 -    (WRES8 <-> WRES1 & ~IN5 & IN4 & ~IN3 | WRES2 & ~IN2 & IN1)
   4.112 -    --> (OUT10 <-> WRES7) &
   4.113 -        (OUT9 <-> WRES9 & IN8 | WRES12 | WRES14 & ~IN9 | ~WRES15 & WRES10) &
   4.114 -        (OUT8 <-> WRES9 & ~IN8 | WRES15 & WRES6 | WRES4 & IN9) &
   4.115 -        (OUT7 <-> WRES13 & IN9) &
   4.116 -        (OUT6 <-> WRES13 & ~IN9) &
   4.117 -        (OUT5 <-> WRES14 & IN9) &
   4.118 -        (OUT4 <-> WRES11 & IN9 | WRES12 & IN8) &
   4.119 -        (OUT3 <-> WRES8 & IN9 & ~IN8 | WRES11 & ~IN9 | WRES12 & ~IN8) &
   4.120 -        (OUT2 <-> WRES8 & ~IN9 | WRES10 & IN8) &
   4.121 -        (OUT1 <-> WRES7 & IN8) &
   4.122 -        (OUT0 <-> WRES7 & ~IN8)"
   4.123 -  by svc
   4.124 -
   4.125 -text {* @{text "fast"} only takes a couple of seconds. *}
   4.126 -
   4.127 -lemma sqn_be: "(GE0 <-> IN6 & IN1 | ~IN6 & ~IN1) &
   4.128 -   (GE8 <-> ~IN3 & ~IN1) &
   4.129 -   (GE5 <-> IN6 | IN5) &
   4.130 -   (GE9 <-> ~GE0 | IN2 | ~IN5) &
   4.131 -   (GE1 <-> IN3 | ~IN0) &
   4.132 -   (GE11 <-> GE8 & IN4) &
   4.133 -   (GE3 <-> ~IN4 | ~IN2) &
   4.134 -   (GE34 <-> ~GE5 & IN4 | ~GE9) &
   4.135 -   (GE2 <-> ~IN4 & IN1) &
   4.136 -   (GE14 <-> ~GE1 & ~IN4) &
   4.137 -   (GE19 <-> GE11 & ~GE5) &
   4.138 -   (GE13 <-> GE8 & ~GE3 & ~IN0) &
   4.139 -   (GE20 <-> ~IN5 & IN2 | GE34) &
   4.140 -   (GE12 <-> GE2 & ~IN3) &
   4.141 -   (GE27 <-> GE14 & IN6 | GE19) &
   4.142 -   (GE10 <-> ~IN6 | IN5) &
   4.143 -   (GE28 <-> GE13 | GE20 & ~GE1) &
   4.144 -   (GE6 <-> ~IN5 | IN6) &
   4.145 -   (GE15 <-> GE2 & IN2) &
   4.146 -   (GE29 <-> GE27 | GE12 & GE5) &
   4.147 -   (GE4 <-> IN3 & ~IN0) &
   4.148 -   (GE21 <-> ~GE10 & ~IN1 | ~IN5 & ~IN2) &
   4.149 -   (GE30 <-> GE28 | GE14 & IN2) &
   4.150 -   (GE31 <-> GE29 | GE15 & ~GE6) &
   4.151 -   (GE7 <-> ~IN6 | ~IN5) &
   4.152 -   (GE17 <-> ~GE3 & ~IN1) &
   4.153 -   (GE18 <-> GE4 & IN2) &
   4.154 -   (GE16 <-> GE2 & IN0) &
   4.155 -   (GE23 <-> GE19 | GE9 & ~GE1) &
   4.156 -   (GE32 <-> GE15 & ~IN6 & ~IN0 | GE21 & GE4 & ~IN4 | GE30 | GE31) &
   4.157 -   (GE33 <->
   4.158 -    GE18 & ~GE6 & ~IN4 |
   4.159 -    GE17 & ~GE7 & IN3 |
   4.160 -    ~GE7 & GE4 & ~GE3 |
   4.161 -    GE11 & IN5 & ~IN0) &
   4.162 -   (GE25 <-> GE14 & ~GE6 | GE13 & ~GE5 | GE16 & ~IN5 | GE15 & GE1) &
   4.163 -   (GE26 <->
   4.164 -    GE12 & IN5 & ~IN2 |
   4.165 -    GE10 & GE4 & IN1 |
   4.166 -    GE17 & ~GE6 & IN0 |
   4.167 -    GE2 & ~IN6) &
   4.168 -   (GE24 <-> GE23 | GE16 & GE7) &
   4.169 -   (OUT0 <->
   4.170 -    GE6 & IN4 & ~IN1 & IN0 | GE18 & GE0 & ~IN5 | GE12 & ~GE10 | GE24) &
   4.171 -   (OUT1 <-> GE26 | GE25 | ~GE5 & GE4 & GE3 | GE7 & ~GE1 & IN1) &
   4.172 -   (OUT2 <-> GE33 | GE32) &
   4.173 -   (WRES8 <-> ~IN3 & ~IN1) &
   4.174 -   (WRES0 <-> IN6 & IN1 | ~IN6 & ~IN1) &
   4.175 -   (WRES2 <-> ~IN4 & IN1) &
   4.176 -   (WRES3 <-> ~IN4 | ~IN2) &
   4.177 -   (WRES1 <-> IN3 | ~IN0) &
   4.178 -   (WRES4 <-> IN3 & ~IN0) &
   4.179 -   (WRES5 <-> IN6 | IN5) &
   4.180 -   (WRES11 <-> WRES8 & IN4) &
   4.181 -   (WRES9 <-> ~WRES0 | IN2 | ~IN5) &
   4.182 -   (WRES10 <-> ~IN6 | IN5) &
   4.183 -   (WRES6 <-> ~IN5 | IN6) &
   4.184 -   (WRES7 <-> ~IN6 | ~IN5) &
   4.185 -   (WRES12 <-> WRES2 & ~IN3) &
   4.186 -   (WRES13 <-> WRES8 & ~WRES3 & ~IN0) &
   4.187 -   (WRES14 <-> ~WRES1 & ~IN4) &
   4.188 -   (WRES15 <-> WRES2 & IN2) &
   4.189 -   (WRES17 <-> ~WRES3 & ~IN1) &
   4.190 -   (WRES18 <-> WRES4 & IN2) &
   4.191 -   (WRES19 <-> WRES11 & ~WRES5) &
   4.192 -   (WRES20 <-> ~IN5 & IN2 | ~WRES5 & IN4 | ~WRES9) &
   4.193 -   (WRES21 <-> ~WRES10 & ~IN1 | ~IN5 & ~IN2) &
   4.194 -   (WRES16 <-> WRES2 & IN0)
   4.195 -   --> (OUT2 <->
   4.196 -        WRES11 & IN5 & ~IN0 |
   4.197 -        ~WRES7 & WRES4 & ~WRES3 |
   4.198 -        WRES12 & WRES5 |
   4.199 -        WRES13 |
   4.200 -        WRES14 & IN2 |
   4.201 -        WRES14 & IN6 |
   4.202 -        WRES15 & ~WRES6 |
   4.203 -        WRES15 & ~IN6 & ~IN0 |
   4.204 -        WRES17 & ~WRES7 & IN3 |
   4.205 -        WRES18 & ~WRES6 & ~IN4 |
   4.206 -        WRES20 & ~WRES1 |
   4.207 -        WRES21 & WRES4 & ~IN4 |
   4.208 -        WRES19) &
   4.209 -       (OUT1 <->
   4.210 -        ~WRES5 & WRES4 & WRES3 |
   4.211 -        WRES7 & ~WRES1 & IN1 |
   4.212 -        WRES2 & ~IN6 |
   4.213 -        WRES10 & WRES4 & IN1 |
   4.214 -        WRES12 & IN5 & ~IN2 |
   4.215 -        WRES13 & ~WRES5 |
   4.216 -        WRES14 & ~WRES6 |
   4.217 -        WRES15 & WRES1 |
   4.218 -        WRES16 & ~IN5 |
   4.219 -        WRES17 & ~WRES6 & IN0) &
   4.220 -       (OUT0 <->
   4.221 -        WRES6 & IN4 & ~IN1 & IN0 |
   4.222 -        WRES9 & ~WRES1 |
   4.223 -        WRES12 & ~WRES10 |
   4.224 -        WRES16 & WRES7 |
   4.225 -        WRES18 & WRES0 & ~IN5 |
   4.226 -        WRES19)"
   4.227 -  by svc
   4.228 -
   4.229 -
   4.230 -subsection {* Linear arithmetic *}
   4.231 -
   4.232 -lemma "x ~= 14 & x ~= 13 & x ~= 12 & x ~= 11 & x ~= 10 & x ~= 9 &
   4.233 -      x ~= 8 & x ~= 7 & x ~= 6 & x ~= 5 & x ~= 4 & x ~= 3 &
   4.234 -      x ~= 2 & x ~= 1 & 0 < x & x < 16 --> 15 = (x::int)"
   4.235 -  by svc
   4.236 -
   4.237 -text {*merely to test polarity handling in the presence of biconditionals*}
   4.238 -lemma "(x < (y::int)) = (x+1 <= y)"
   4.239 -  by svc
   4.240 -
   4.241 -
   4.242 -subsection {* Natural number examples requiring implicit "non-negative" assumptions *}
   4.243 -
   4.244 -lemma "(3::nat)*a <= 2 + 4*b + 6*c  & 11 <= 2*a + b + 2*c &
   4.245 -      a + 3*b <= 5 + 2*c  --> 2 + 3*b <= 2*a + 6*c"
   4.246 -  by svc
   4.247 -
   4.248 -lemma "(n::nat) < 2 ==> (n = 0) | (n = 1)"
   4.249 -  by svc
   4.250 -
   4.251 -end