# HG changeset patch # User wenzelm # Date 1433165993 -7200 # Node ID 7676bcaa1f95df2b82e7b932b5455ac0051c6d7a # Parent f215fd466e30be4d26f60e96f56b8566471bd1bb discontinued unused / unmaintained SVC oracle -- current Isabelle tools (e.g. arith, smt) can easily solve the given examples with full proof reconstruction; diff -r f215fd466e30 -r 7676bcaa1f95 src/HOL/ROOT --- a/src/HOL/ROOT Mon Jun 01 15:06:09 2015 +0200 +++ b/src/HOL/ROOT Mon Jun 01 15:39:53 2015 +0200 @@ -588,7 +588,6 @@ Set_Comprehension_Pointfree_Examples Parallel_Example IArray_Examples - SVC_Oracle Simps_Case_Conv_Examples ML Rewrite_Examples @@ -597,8 +596,6 @@ SOS_Cert theories [skip_proofs = false] Meson_Test - theories [condition = SVC_HOME] - svc_test theories [condition = ISABELLE_FULL_TEST] Sudoku document_files "root.bib" "root.tex" diff -r f215fd466e30 -r 7676bcaa1f95 src/HOL/ex/SVC_Oracle.thy --- a/src/HOL/ex/SVC_Oracle.thy Mon Jun 01 15:06:09 2015 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,122 +0,0 @@ -(* Title: HOL/ex/SVC_Oracle.thy - Author: Lawrence C Paulson - Copyright 1999 University of Cambridge - -Based upon the work of Søren T. Heilmann. -*) - -section {* Installing an oracle for SVC (Stanford Validity Checker) *} - -theory SVC_Oracle -imports Main -begin - -consts - iff_keep :: "[bool, bool] => bool" - iff_unfold :: "[bool, bool] => bool" - -ML_file "svc_funcs.ML" - -hide_const iff_keep iff_unfold - -oracle svc_oracle = Svc.oracle - -ML {* -(* -Installing the oracle for SVC (Stanford Validity Checker) - -The following code merely CALLS the oracle; - the soundness-critical functions are at svc_funcs.ML - -Based upon the work of Søren T. Heilmann -*) - - -(*Generalize an Isabelle formula, replacing by Vars - all subterms not intelligible to SVC.*) -fun svc_abstract t = - let - (*The oracle's result is given to the subgoal using compose_tac because - its premises are matched against the assumptions rather than used - to make subgoals. Therefore , abstraction must copy the parameters - precisely and make them available to all generated Vars.*) - val params = Term.strip_all_vars t - and body = Term.strip_all_body t - val Us = map #2 params - val nPar = length params - val vname = Unsynchronized.ref "V_a" - val pairs = Unsynchronized.ref ([] : (term*term) list) - fun insert t = - let val T = fastype_of t - val v = Logic.combound (Var ((!vname,0), Us--->T), 0, nPar) - in vname := Symbol.bump_string (!vname); - pairs := (t, v) :: !pairs; - v - end; - fun replace t = - case t of - Free _ => t (*but not existing Vars, lest the names clash*) - | Bound _ => t - | _ => (case AList.lookup Envir.aeconv (!pairs) t of - SOME v => v - | NONE => insert t) - (*abstraction of a numeric literal*) - fun lit t = if can HOLogic.dest_number t then t else replace t; - (*abstraction of a real/rational expression*) - fun rat ((c as Const(@{const_name Groups.plus}, _)) $ x $ y) = c $ (rat x) $ (rat y) - | rat ((c as Const(@{const_name Groups.minus}, _)) $ x $ y) = c $ (rat x) $ (rat y) - | rat ((c as Const(@{const_name Fields.divide}, _)) $ x $ y) = c $ (rat x) $ (rat y) - | rat ((c as Const(@{const_name Groups.times}, _)) $ x $ y) = c $ (rat x) $ (rat y) - | rat ((c as Const(@{const_name Groups.uminus}, _)) $ x) = c $ (rat x) - | rat t = lit t - (*abstraction of an integer expression: no div, mod*) - fun int ((c as Const(@{const_name Groups.plus}, _)) $ x $ y) = c $ (int x) $ (int y) - | int ((c as Const(@{const_name Groups.minus}, _)) $ x $ y) = c $ (int x) $ (int y) - | int ((c as Const(@{const_name Groups.times}, _)) $ x $ y) = c $ (int x) $ (int y) - | int ((c as Const(@{const_name Groups.uminus}, _)) $ x) = c $ (int x) - | int t = lit t - (*abstraction of a natural number expression: no minus*) - fun nat ((c as Const(@{const_name Groups.plus}, _)) $ x $ y) = c $ (nat x) $ (nat y) - | nat ((c as Const(@{const_name Groups.times}, _)) $ x $ y) = c $ (nat x) $ (nat y) - | nat ((c as Const(@{const_name Suc}, _)) $ x) = c $ (nat x) - | nat t = lit t - (*abstraction of a relation: =, <, <=*) - fun rel (T, c $ x $ y) = - if T = HOLogic.realT then c $ (rat x) $ (rat y) - else if T = HOLogic.intT then c $ (int x) $ (int y) - else if T = HOLogic.natT then c $ (nat x) $ (nat y) - else if T = HOLogic.boolT then c $ (fm x) $ (fm y) - else replace (c $ x $ y) (*non-numeric comparison*) - (*abstraction of a formula*) - and fm ((c as Const(@{const_name HOL.conj}, _)) $ p $ q) = c $ (fm p) $ (fm q) - | fm ((c as Const(@{const_name HOL.disj}, _)) $ p $ q) = c $ (fm p) $ (fm q) - | fm ((c as Const(@{const_name HOL.implies}, _)) $ p $ q) = c $ (fm p) $ (fm q) - | fm ((c as Const(@{const_name Not}, _)) $ p) = c $ (fm p) - | fm ((c as Const(@{const_name True}, _))) = c - | fm ((c as Const(@{const_name False}, _))) = c - | fm (t as Const(@{const_name HOL.eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t) - | fm (t as Const(@{const_name Orderings.less}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t) - | fm (t as Const(@{const_name Orderings.less_eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t) - | fm t = replace t - (*entry point, and abstraction of a meta-formula*) - fun mt ((c as Const(@{const_name Trueprop}, _)) $ p) = c $ (fm p) - | mt ((c as Const(@{const_name Pure.imp}, _)) $ p $ q) = c $ (mt p) $ (mt q) - | mt t = fm t (*it might be a formula*) - in (Logic.list_all (params, mt body), !pairs) end; - - -(*Present the entire subgoal to the oracle, assumptions and all, but possibly - abstracted. Use via compose_tac, which performs no lifting but will - instantiate variables.*) - -fun svc_tac ctxt = CSUBGOAL (fn (ct, i) => - let - val (abs_goal, _) = svc_abstract (Thm.term_of ct); - val th = svc_oracle (Thm.cterm_of ctxt abs_goal); - in compose_tac ctxt (false, th, 0) i end - handle TERM _ => no_tac); -*} - -method_setup svc = {* Scan.succeed (SIMPLE_METHOD' o svc_tac) *} - -end diff -r f215fd466e30 -r 7676bcaa1f95 src/HOL/ex/svc_funcs.ML --- a/src/HOL/ex/svc_funcs.ML Mon Jun 01 15:06:09 2015 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,255 +0,0 @@ -(* Title: HOL/ex/svc_funcs.ML - Author: Lawrence C Paulson - Copyright 1999 University of Cambridge - -Translation functions for the interface to SVC. - -Based upon the work of Soren T. Heilmann - -Integers and naturals are translated as follows: - In a positive context, replace x a ^ " " ^ (ue b)) ("", l)) ^ ") " - | ue (Interp(s, l)) = - "{" ^ s ^ (Library.foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ "} " - | ue (UnInterp(s, l)) = - "(" ^ s ^ (Library.foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ ") " - | ue (FalseExpr) = "FALSE " - | ue (TrueExpr) = "TRUE " - | ue (Int i) = signed_string_of_int i ^ " " - | ue (Rat(i, j)) = signed_string_of_int i ^ "|" ^ signed_string_of_int j ^ " " - in - ue t - end; - - fun valid e = - let val svc_home = getenv "SVC_HOME" - val svc_machine = getenv "SVC_MACHINE" - val check_valid = if svc_home = "" - then error "Environment variable SVC_HOME not set" - else if svc_machine = "" - then error "Environment variable SVC_MACHINE not set" - else svc_home ^ "/" ^ svc_machine ^ "/bin/check_valid" - val svc_input = toString e - val _ = if !trace then tracing ("Calling SVC:\n" ^ svc_input) else () - val svc_input_file = File.tmp_path (Path.basic "SVM_in"); - val svc_output_file = File.tmp_path (Path.basic "SVM_out"); - val _ = File.write svc_input_file svc_input; - val _ = - Isabelle_System.bash_output (check_valid ^ " -dump-result " ^ - File.shell_path svc_output_file ^ " " ^ File.shell_path svc_input_file ^ - ">/dev/null 2>&1") - val svc_output = - (case try File.read svc_output_file of - SOME out => out - | NONE => error "SVC returned no output"); - in - if ! trace then tracing ("SVC Returns:\n" ^ svc_output) - else (File.rm svc_input_file; File.rm svc_output_file); - String.isPrefix "VALID" svc_output - end - - fun fail t = raise TERM ("SVC oracle", [t]); - - fun apply c args = - let val (ts, bs) = ListPair.unzip args - in (list_comb(c,ts), exists I bs) end; - - (*Determining whether the biconditionals must be unfolded: if there are - int or nat comparisons below*) - val iff_tag = - let fun tag t = - let val (c,ts) = strip_comb t - in case c of - Const(@{const_name HOL.conj}, _) => apply c (map tag ts) - | Const(@{const_name HOL.disj}, _) => apply c (map tag ts) - | Const(@{const_name HOL.implies}, _) => apply c (map tag ts) - | Const(@{const_name Not}, _) => apply c (map tag ts) - | Const(@{const_name True}, _) => (c, false) - | Const(@{const_name False}, _) => (c, false) - | Const(@{const_name HOL.eq}, Type ("fun", [T,_])) => - if T = HOLogic.boolT then - (*biconditional: with int/nat comparisons below?*) - let val [t1,t2] = ts - val (u1,b1) = tag t1 - and (u2,b2) = tag t2 - val cname = if b1 orelse b2 then "unfold" else "keep" - in - (Const ("SVC_Oracle.iff_" ^ cname, dummyT) $ u1 $ u2, - b1 orelse b2) - end - else (*might be numeric equality*) (t, is_intnat T) - | Const(@{const_name Orderings.less}, Type ("fun", [T,_])) => (t, is_intnat T) - | Const(@{const_name Orderings.less_eq}, Type ("fun", [T,_])) => (t, is_intnat T) - | _ => (t, false) - end - in #1 o tag end; - - (*Map expression e to 0<=a --> e, where "a" is the name of a nat variable*) - fun add_nat_var a e = - Buildin("=>", [Buildin("<=", [Int 0, UnInterp (a, [])]), - e]); - - fun param_string [] = "" - | param_string is = "_" ^ space_implode "_" (map string_of_int is) - - (*Translate an Isabelle formula into an SVC expression - pos ["positive"]: true if an assumption, false if a goal*) - fun expr_of pos t = - let - val params = rev (Term.rename_wrt_term t (Term.strip_all_vars t)) - and body = Term.strip_all_body t - val nat_vars = Unsynchronized.ref ([] : string list) - (*translation of a variable: record all natural numbers*) - fun trans_var (a,T,is) = - (if T = HOLogic.natT then nat_vars := (insert (op =) a (!nat_vars)) - else (); - UnInterp (a ^ param_string is, [])) - (*A variable, perhaps applied to a series of parameters*) - fun var (Free(a,T), is) = trans_var ("F_" ^ a, T, is) - | var (Var((a, 0), T), is) = trans_var (a, T, is) - | var (Bound i, is) = - let val (a,T) = nth params i - in trans_var ("B_" ^ a, T, is) end - | var (t $ Bound i, is) = var(t,i::is) - (*removing a parameter from a Var: the bound var index will - become part of the Var's name*) - | var (t,_) = fail t; - (*translation of a literal*) - val lit = snd o HOLogic.dest_number; - (*translation of a literal expression [no variables]*) - fun litExp (Const(@{const_name Groups.plus}, T) $ x $ y) = - if is_numeric_op T then (litExp x) + (litExp y) - else fail t - | litExp (Const(@{const_name Groups.minus}, T) $ x $ y) = - if is_numeric_op T then (litExp x) - (litExp y) - else fail t - | litExp (Const(@{const_name Groups.times}, T) $ x $ y) = - if is_numeric_op T then (litExp x) * (litExp y) - else fail t - | litExp (Const(@{const_name Groups.uminus}, T) $ x) = - if is_numeric_op T then ~(litExp x) - else fail t - | litExp t = lit t - handle Match => fail t - (*translation of a real/rational expression*) - fun suc t = Interp("+", [Int 1, t]) - fun tm (Const(@{const_name Suc}, T) $ x) = suc (tm x) - | tm (Const(@{const_name Groups.plus}, T) $ x $ y) = - if is_numeric_op T then Interp("+", [tm x, tm y]) - else fail t - | tm (Const(@{const_name Groups.minus}, T) $ x $ y) = - if is_numeric_op T then - Interp("+", [tm x, Interp("*", [Int ~1, tm y])]) - else fail t - | tm (Const(@{const_name Groups.times}, T) $ x $ y) = - if is_numeric_op T then Interp("*", [tm x, tm y]) - else fail t - | tm (Const(@{const_name Fields.inverse}, T) $ x) = - if domain_type T = HOLogic.realT then - Rat(1, litExp x) - else fail t - | tm (Const(@{const_name Groups.uminus}, T) $ x) = - if is_numeric_op T then Interp("*", [Int ~1, tm x]) - else fail t - | tm t = Int (lit t) - handle Match => var (t,[]) - (*translation of a formula*) - and fm pos (Const(@{const_name HOL.conj}, _) $ p $ q) = - Buildin("AND", [fm pos p, fm pos q]) - | fm pos (Const(@{const_name HOL.disj}, _) $ p $ q) = - Buildin("OR", [fm pos p, fm pos q]) - | fm pos (Const(@{const_name HOL.implies}, _) $ p $ q) = - Buildin("=>", [fm (not pos) p, fm pos q]) - | fm pos (Const(@{const_name Not}, _) $ p) = - Buildin("NOT", [fm (not pos) p]) - | fm pos (Const(@{const_name True}, _)) = TrueExpr - | fm pos (Const(@{const_name False}, _)) = FalseExpr - | fm pos (Const(@{const_name iff_keep}, _) $ p $ q) = - (*polarity doesn't matter*) - Buildin("=", [fm pos p, fm pos q]) - | fm pos (Const(@{const_name iff_unfold}, _) $ p $ q) = - Buildin("AND", (*unfolding uses both polarities*) - [Buildin("=>", [fm (not pos) p, fm pos q]), - Buildin("=>", [fm (not pos) q, fm pos p])]) - | fm pos (t as Const(@{const_name HOL.eq}, Type ("fun", [T,_])) $ x $ y) = - let val tx = tm x and ty = tm y - in if pos orelse T = HOLogic.realT then - Buildin("=", [tx, ty]) - else if is_intnat T then - Buildin("AND", - [Buildin("<", [tx, suc ty]), - Buildin("<", [ty, suc tx])]) - else fail t - end - (*inequalities: possible types are nat, int, real*) - | fm pos (t as Const(@{const_name Orderings.less}, Type ("fun", [T,_])) $ x $ y) = - if not pos orelse T = HOLogic.realT then - Buildin("<", [tm x, tm y]) - else if is_intnat T then - Buildin("<=", [suc (tm x), tm y]) - else fail t - | fm pos (t as Const(@{const_name Orderings.less_eq}, Type ("fun", [T,_])) $ x $ y) = - if pos orelse T = HOLogic.realT then - Buildin("<=", [tm x, tm y]) - else if is_intnat T then - Buildin("<", [tm x, suc (tm y)]) - else fail t - | fm pos t = var(t,[]); - (*entry point, and translation of a meta-formula*) - fun mt pos ((c as Const(@{const_name Trueprop}, _)) $ p) = fm pos (iff_tag p) - | mt pos ((c as Const(@{const_name Pure.imp}, _)) $ p $ q) = - Buildin("=>", [mt (not pos) p, mt pos q]) - | mt pos t = fm pos (iff_tag t) (*it might be a formula*) - - val body_e = mt pos body (*evaluate now to assign into !nat_vars*) - in - fold_rev add_nat_var (!nat_vars) body_e - end; - - - (*The oracle proves the given formula, if possible*) - fun oracle ct = - let - val thy = Thm.theory_of_cterm ct; - val t = Thm.term_of ct; - val _ = - if ! trace then tracing ("SVC oracle: problem is\n" ^ Syntax.string_of_term_global thy t) - else (); - in if valid (expr_of false t) then ct else fail t end; - -end; diff -r f215fd466e30 -r 7676bcaa1f95 src/HOL/ex/svc_test.thy --- a/src/HOL/ex/svc_test.thy Mon Jun 01 15:06:09 2015 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,248 +0,0 @@ -section {* Demonstrating the interface SVC *} - -theory svc_test -imports SVC_Oracle -begin - -subsubsection {* Propositional Logic *} - -text {* - @{text "blast"}'s runtime for this type of problem appears to be exponential - in its length, though @{text "fast"} manages. -*} -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" - by svc - - -subsection {* Some big tautologies supplied by John Harrison *} - -text {* - @{text "auto"} manages; @{text "blast"} and @{text "fast"} take a minute or more. -*} -lemma puz013_1: "~(~v12 & - v0 & - v10 & - (v4 | v5) & - (v9 | v2) & - (v8 | v1) & - (v7 | v0) & - (v3 | v12) & - (v11 | v10) & - (~v12 | ~v6 | v7) & - (~v10 | ~v3 | v1) & - (~v10 | ~v0 | ~v4 | v11) & - (~v5 | ~v2 | ~v8) & - (~v12 | ~v9 | ~v7) & - (~v0 | ~v1 | v4) & - (~v4 | v7 | v2) & - (~v12 | ~v3 | v8) & - (~v4 | v5 | v6) & - (~v7 | ~v8 | v9) & - (~v10 | ~v11 | v12))" - by svc - -lemma dk17_be: - "(GE17 <-> ~IN4 & ~IN3 & ~IN2 & ~IN1) & - (GE0 <-> GE17 & ~IN5) & - (GE22 <-> ~IN9 & ~IN7 & ~IN6 & IN0) & - (GE19 <-> ~IN5 & ~IN4 & ~IN3 & ~IN0) & - (GE20 <-> ~IN7 & ~IN6) & - (GE18 <-> ~IN6 & ~IN2 & ~IN1 & ~IN0) & - (GE21 <-> IN9 & ~IN7 & IN6 & ~IN0) & - (GE23 <-> GE22 & GE0) & - (GE25 <-> ~IN9 & ~IN7 & IN6 & ~IN0) & - (GE26 <-> IN9 & ~IN7 & ~IN6 & IN0) & - (GE2 <-> GE20 & GE19) & - (GE1 <-> GE18 & ~IN7) & - (GE24 <-> GE23 | GE21 & GE0) & - (GE5 <-> ~IN5 & IN4 | IN5 & ~IN4) & - (GE6 <-> GE0 & IN7 & ~IN6 & ~IN0) & - (GE12 <-> GE26 & GE0 | GE25 & GE0) & - (GE14 <-> GE2 & IN8 & ~IN2 & IN1) & - (GE27 <-> ~IN8 & IN5 & ~IN4 & ~IN3) & - (GE9 <-> GE1 & ~IN5 & ~IN4 & IN3) & - (GE7 <-> GE24 | GE2 & IN2 & ~IN1) & - (GE10 <-> GE6 | GE5 & GE1 & ~IN3) & - (GE15 <-> ~IN8 | IN9) & - (GE16 <-> GE12 | GE14 & ~IN9) & - (GE4 <-> - GE5 & GE1 & IN8 & ~IN3 | - GE0 & ~IN7 & IN6 & ~IN0 | - GE2 & IN2 & ~IN1) & - (GE13 <-> GE27 & GE1) & - (GE11 <-> GE9 | GE6 & ~IN8) & - (GE8 <-> GE1 & ~IN5 & IN4 & ~IN3 | GE2 & ~IN2 & IN1) & - (OUT0 <-> GE7 & ~IN8) & - (OUT1 <-> GE7 & IN8) & - (OUT2 <-> GE8 & ~IN9 | GE10 & IN8) & - (OUT3 <-> GE8 & IN9 & ~IN8 | GE11 & ~IN9 | GE12 & ~IN8) & - (OUT4 <-> GE11 & IN9 | GE12 & IN8) & - (OUT5 <-> GE14 & IN9) & - (OUT6 <-> GE13 & ~IN9) & - (OUT7 <-> GE13 & IN9) & - (OUT8 <-> GE9 & ~IN8 | GE15 & GE6 | GE4 & IN9) & - (OUT9 <-> GE9 & IN8 | ~GE15 & GE10 | GE16) & - (OUT10 <-> GE7) & - (WRES0 <-> ~IN5 & ~IN4 & ~IN3 & ~IN2 & ~IN1) & - (WRES1 <-> ~IN7 & ~IN6 & ~IN2 & ~IN1 & ~IN0) & - (WRES2 <-> ~IN7 & ~IN6 & ~IN5 & ~IN4 & ~IN3 & ~IN0) & - (WRES5 <-> ~IN5 & IN4 | IN5 & ~IN4) & - (WRES6 <-> WRES0 & IN7 & ~IN6 & ~IN0) & - (WRES9 <-> WRES1 & ~IN5 & ~IN4 & IN3) & - (WRES7 <-> - WRES0 & ~IN9 & ~IN7 & ~IN6 & IN0 | - WRES0 & IN9 & ~IN7 & IN6 & ~IN0 | - WRES2 & IN2 & ~IN1) & - (WRES10 <-> WRES6 | WRES5 & WRES1 & ~IN3) & - (WRES12 <-> - WRES0 & IN9 & ~IN7 & ~IN6 & IN0 | - WRES0 & ~IN9 & ~IN7 & IN6 & ~IN0) & - (WRES14 <-> WRES2 & IN8 & ~IN2 & IN1) & - (WRES15 <-> ~IN8 | IN9) & - (WRES4 <-> - WRES5 & WRES1 & IN8 & ~IN3 | - WRES2 & IN2 & ~IN1 | - WRES0 & ~IN7 & IN6 & ~IN0) & - (WRES13 <-> WRES1 & ~IN8 & IN5 & ~IN4 & ~IN3) & - (WRES11 <-> WRES9 | WRES6 & ~IN8) & - (WRES8 <-> WRES1 & ~IN5 & IN4 & ~IN3 | WRES2 & ~IN2 & IN1) - --> (OUT10 <-> WRES7) & - (OUT9 <-> WRES9 & IN8 | WRES12 | WRES14 & ~IN9 | ~WRES15 & WRES10) & - (OUT8 <-> WRES9 & ~IN8 | WRES15 & WRES6 | WRES4 & IN9) & - (OUT7 <-> WRES13 & IN9) & - (OUT6 <-> WRES13 & ~IN9) & - (OUT5 <-> WRES14 & IN9) & - (OUT4 <-> WRES11 & IN9 | WRES12 & IN8) & - (OUT3 <-> WRES8 & IN9 & ~IN8 | WRES11 & ~IN9 | WRES12 & ~IN8) & - (OUT2 <-> WRES8 & ~IN9 | WRES10 & IN8) & - (OUT1 <-> WRES7 & IN8) & - (OUT0 <-> WRES7 & ~IN8)" - by svc - -text {* @{text "fast"} only takes a couple of seconds. *} - -lemma sqn_be: "(GE0 <-> IN6 & IN1 | ~IN6 & ~IN1) & - (GE8 <-> ~IN3 & ~IN1) & - (GE5 <-> IN6 | IN5) & - (GE9 <-> ~GE0 | IN2 | ~IN5) & - (GE1 <-> IN3 | ~IN0) & - (GE11 <-> GE8 & IN4) & - (GE3 <-> ~IN4 | ~IN2) & - (GE34 <-> ~GE5 & IN4 | ~GE9) & - (GE2 <-> ~IN4 & IN1) & - (GE14 <-> ~GE1 & ~IN4) & - (GE19 <-> GE11 & ~GE5) & - (GE13 <-> GE8 & ~GE3 & ~IN0) & - (GE20 <-> ~IN5 & IN2 | GE34) & - (GE12 <-> GE2 & ~IN3) & - (GE27 <-> GE14 & IN6 | GE19) & - (GE10 <-> ~IN6 | IN5) & - (GE28 <-> GE13 | GE20 & ~GE1) & - (GE6 <-> ~IN5 | IN6) & - (GE15 <-> GE2 & IN2) & - (GE29 <-> GE27 | GE12 & GE5) & - (GE4 <-> IN3 & ~IN0) & - (GE21 <-> ~GE10 & ~IN1 | ~IN5 & ~IN2) & - (GE30 <-> GE28 | GE14 & IN2) & - (GE31 <-> GE29 | GE15 & ~GE6) & - (GE7 <-> ~IN6 | ~IN5) & - (GE17 <-> ~GE3 & ~IN1) & - (GE18 <-> GE4 & IN2) & - (GE16 <-> GE2 & IN0) & - (GE23 <-> GE19 | GE9 & ~GE1) & - (GE32 <-> GE15 & ~IN6 & ~IN0 | GE21 & GE4 & ~IN4 | GE30 | GE31) & - (GE33 <-> - GE18 & ~GE6 & ~IN4 | - GE17 & ~GE7 & IN3 | - ~GE7 & GE4 & ~GE3 | - GE11 & IN5 & ~IN0) & - (GE25 <-> GE14 & ~GE6 | GE13 & ~GE5 | GE16 & ~IN5 | GE15 & GE1) & - (GE26 <-> - GE12 & IN5 & ~IN2 | - GE10 & GE4 & IN1 | - GE17 & ~GE6 & IN0 | - GE2 & ~IN6) & - (GE24 <-> GE23 | GE16 & GE7) & - (OUT0 <-> - GE6 & IN4 & ~IN1 & IN0 | GE18 & GE0 & ~IN5 | GE12 & ~GE10 | GE24) & - (OUT1 <-> GE26 | GE25 | ~GE5 & GE4 & GE3 | GE7 & ~GE1 & IN1) & - (OUT2 <-> GE33 | GE32) & - (WRES8 <-> ~IN3 & ~IN1) & - (WRES0 <-> IN6 & IN1 | ~IN6 & ~IN1) & - (WRES2 <-> ~IN4 & IN1) & - (WRES3 <-> ~IN4 | ~IN2) & - (WRES1 <-> IN3 | ~IN0) & - (WRES4 <-> IN3 & ~IN0) & - (WRES5 <-> IN6 | IN5) & - (WRES11 <-> WRES8 & IN4) & - (WRES9 <-> ~WRES0 | IN2 | ~IN5) & - (WRES10 <-> ~IN6 | IN5) & - (WRES6 <-> ~IN5 | IN6) & - (WRES7 <-> ~IN6 | ~IN5) & - (WRES12 <-> WRES2 & ~IN3) & - (WRES13 <-> WRES8 & ~WRES3 & ~IN0) & - (WRES14 <-> ~WRES1 & ~IN4) & - (WRES15 <-> WRES2 & IN2) & - (WRES17 <-> ~WRES3 & ~IN1) & - (WRES18 <-> WRES4 & IN2) & - (WRES19 <-> WRES11 & ~WRES5) & - (WRES20 <-> ~IN5 & IN2 | ~WRES5 & IN4 | ~WRES9) & - (WRES21 <-> ~WRES10 & ~IN1 | ~IN5 & ~IN2) & - (WRES16 <-> WRES2 & IN0) - --> (OUT2 <-> - WRES11 & IN5 & ~IN0 | - ~WRES7 & WRES4 & ~WRES3 | - WRES12 & WRES5 | - WRES13 | - WRES14 & IN2 | - WRES14 & IN6 | - WRES15 & ~WRES6 | - WRES15 & ~IN6 & ~IN0 | - WRES17 & ~WRES7 & IN3 | - WRES18 & ~WRES6 & ~IN4 | - WRES20 & ~WRES1 | - WRES21 & WRES4 & ~IN4 | - WRES19) & - (OUT1 <-> - ~WRES5 & WRES4 & WRES3 | - WRES7 & ~WRES1 & IN1 | - WRES2 & ~IN6 | - WRES10 & WRES4 & IN1 | - WRES12 & IN5 & ~IN2 | - WRES13 & ~WRES5 | - WRES14 & ~WRES6 | - WRES15 & WRES1 | - WRES16 & ~IN5 | - WRES17 & ~WRES6 & IN0) & - (OUT0 <-> - WRES6 & IN4 & ~IN1 & IN0 | - WRES9 & ~WRES1 | - WRES12 & ~WRES10 | - WRES16 & WRES7 | - WRES18 & WRES0 & ~IN5 | - WRES19)" - by svc - - -subsection {* Linear arithmetic *} - -lemma "x ~= 14 & x ~= 13 & x ~= 12 & x ~= 11 & x ~= 10 & x ~= 9 & - x ~= 8 & x ~= 7 & x ~= 6 & x ~= 5 & x ~= 4 & x ~= 3 & - x ~= 2 & x ~= 1 & 0 < x & x < 16 --> 15 = (x::int)" - by svc - -text {*merely to test polarity handling in the presence of biconditionals*} -lemma "(x < (y::int)) = (x+1 <= y)" - by svc - - -subsection {* Natural number examples requiring implicit "non-negative" assumptions *} - -lemma "(3::nat)*a <= 2 + 4*b + 6*c & 11 <= 2*a + b + 2*c & - a + 3*b <= 5 + 2*c --> 2 + 3*b <= 2*a + 6*c" - by svc - -lemma "(n::nat) < 2 ==> (n = 0) | (n = 1)" - by svc - -end