discontinued unused / unmaintained SVC oracle -- current Isabelle tools (e.g. arith, smt) can easily solve the given examples with full proof reconstruction;
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