--- a/NEWS Sun Oct 01 12:07:57 2006 +0200
+++ b/NEWS Sun Oct 01 18:29:23 2006 +0200
@@ -1,7 +1,7 @@
Isabelle NEWS -- history user-relevant changes
==============================================
-New in this Isabelle release
+New in this Isabelle version
----------------------------
*** General ***
@@ -15,8 +15,8 @@
with Isar theories; migration is usually quite simple with the ML
function use_legacy_bindings. INCOMPATIBILITY.
-* Theory syntax: some popular names (e.g. "class", "if") are now
-keywords. INCOMPATIBILITY, use double quotes.
+* Theory syntax: some popular names (e.g. "class", "if", "fun") are
+now keywords. INCOMPATIBILITY, use double quotes.
* Legacy goal package: reduced interface to the bare minimum required
to keep existing proof scripts running. Most other user-level
@@ -44,11 +44,12 @@
*** Pure ***
-* class_package.ML offers a combination of axclasses and locales to achieve
-Haskell-like type classes in Isabelle. See HOL/ex/Classpackage.thy for examples.
-
-* Yet another code generator framework allows to generate executable code
-for ML and Haskell (including "class"es). A short usage sketch:
+* class_package.ML offers a combination of axclasses and locales to
+achieve Haskell-like type classes in Isabelle. See
+HOL/ex/Classpackage.thy for examples.
+
+* Yet another code generator framework allows to generate executable
+code for ML and Haskell (including "class"es). A short usage sketch:
internal compilation:
code_gen <list of constants (term syntax)> (SML -)
@@ -564,6 +565,8 @@
* inductive and datatype: provide projections of mutual rules, bundled
as foo_bar.inducts;
+* Library: theory Infinite_Set has been moved to the library.
+
* Library: theory Accessible_Part has been move to main HOL.
* Library: added theory Coinductive_List of potentially infinite lists
@@ -572,30 +575,36 @@
* Library: added theory AssocList which implements (finite) maps as
association lists.
-* New proof method "evaluation" for efficiently solving a goal
- (i.e. a boolean expression) by compiling it to ML. The goal is
- "proved" (via the oracle "Evaluation") if it evaluates to True.
-
-* Linear arithmetic now splits certain operators (e.g. min, max, abs) also
-when invoked by the simplifier. This results in the simplifier being more
-powerful on arithmetic goals.
-INCOMPATIBILTY: rewrite proofs. Set fast_arith_split_limit to 0 to obtain
-the old behavior.
+* New proof method "evaluation" for efficiently solving a goal (i.e. a
+boolean expression) by compiling it to ML. The goal is "proved" (via
+the oracle "Evaluation") if it evaluates to True.
+
+* Linear arithmetic now splits certain operators (e.g. min, max, abs)
+also when invoked by the simplifier. This results in the simplifier
+being more powerful on arithmetic goals. INCOMPATIBILTY. Set
+fast_arith_split_limit to 0 to obtain the old behavior.
* Support for hex (0x20) and binary (0b1001) numerals.
-* New method:
- reify eqs (t), where eqs are equations for an interpretation
- I :: 'a list => 'b => 'c and t::'c is an optional parameter,
- computes a term s::'b and a list xs::'a list and proves the theorem
- I xs s = t. This is also known as reification or quoting. The resulting theorem is applied to the subgoal to substitute t with I xs s.
-If t is omitted, the subgoal itself is reified.
-
-* New method:
- reflection corr_thm eqs (t). The parameters eqs and (t) are as explained above. corr_thm is a theorem for
-I vs (f t) = I vs t, where f is supposed to be a computable function (in the sense of code generattion). The method uses reify to compute s and xs as above then applies corr_thm and uses normalization by evaluation to "prove" f s = r and finally gets the theorem t = r, which is again applied to the subgoal. An Example is available in HOL/ex/ReflectionEx.thy.
-
-* Reflection: Automatic refification now handels binding, an example is available in HOL/ex/ReflectionEx.thy
+* New method: reify eqs (t), where eqs are equations for an
+interpretation I :: 'a list => 'b => 'c and t::'c is an optional
+parameter, computes a term s::'b and a list xs::'a list and proves the
+theorem I xs s = t. This is also known as reification or quoting. The
+resulting theorem is applied to the subgoal to substitute t with I xs
+s. If t is omitted, the subgoal itself is reified.
+
+* New method: reflection corr_thm eqs (t). The parameters eqs and (t)
+are as explained above. corr_thm is a theorem for I vs (f t) = I vs t,
+where f is supposed to be a computable function (in the sense of code
+generattion). The method uses reify to compute s and xs as above then
+applies corr_thm and uses normalization by evaluation to "prove" f s =
+r and finally gets the theorem t = r, which is again applied to the
+subgoal. An Example is available in HOL/ex/ReflectionEx.thy.
+
+* Reflection: Automatic refification now handels binding, an example
+is available in HOL/ex/ReflectionEx.thy
+
+
*** HOL-Algebra ***
* Method algebra is now set up via an attribute. For examples see CRing.thy.
@@ -607,6 +616,7 @@
* Renamed `CRing.thy' to `Ring.thy'. INCOMPATIBILITY.
+
*** HOL-Complex ***
* Theory Real: new method ferrack implements quantifier elimination
--- a/src/HOL/Library/Library/ROOT.ML Sun Oct 01 12:07:57 2006 +0200
+++ b/src/HOL/Library/Library/ROOT.ML Sun Oct 01 18:29:23 2006 +0200
@@ -1,3 +1,5 @@
+(* $Id$ *)
+
use_thy "Library";
use_thy "List_Prefix";
use_thy "List_lexord";
--- a/src/HOL/Library/While_Combinator.thy Sun Oct 01 12:07:57 2006 +0200
+++ b/src/HOL/Library/While_Combinator.thy Sun Oct 01 18:29:23 2006 +0200
@@ -37,7 +37,7 @@
definition
while :: "('a => bool) => ('a => 'a) => 'a => 'a"
- "while b c s == while_aux (b, c, s)"
+ "while b c s = while_aux (b, c, s)"
lemma while_aux_unfold:
"while_aux (b, c, s) =
--- a/src/HOL/ex/BinEx.thy Sun Oct 01 12:07:57 2006 +0200
+++ b/src/HOL/ex/BinEx.thy Sun Oct 01 18:29:23 2006 +0200
@@ -10,9 +10,6 @@
subsection {* Regression Testing for Cancellation Simprocs *}
-(*taken from HOL/Integ/int_arith1.ML *)
-
-
lemma "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)"
apply simp oops
@@ -283,7 +280,7 @@
lemma "Suc 99999 = 100000"
by (simp add: Suc_nat_number_of)
- -- {* not a default rewrite since sometimes we want to have @{text "Suc #nnn"} *}
+ -- {* not a default rewrite since sometimes we want to have @{text "Suc nnn"} *}
text {* \medskip Addition *}
@@ -390,8 +387,4 @@
lemma "x + y - x + z - x - y - z + x < (1::int)"
by simp
-
-text{*The proofs about arithmetic yielding normal forms have been deleted:
- they are irrelevant with the new treatment of numerals.*}
-
end
--- a/src/HOL/ex/CTL.thy Sun Oct 01 12:07:57 2006 +0200
+++ b/src/HOL/ex/CTL.thy Sun Oct 01 18:29:23 2006 +0200
@@ -23,12 +23,13 @@
lemmas [intro!] = Int_greatest Un_upper2 Un_upper1 Int_lower1 Int_lower2
types 'a ctl = "'a set"
-constdefs
+
+definition
imp :: "'a ctl \<Rightarrow> 'a ctl \<Rightarrow> 'a ctl" (infixr "\<rightarrow>" 75)
- "p \<rightarrow> q \<equiv> - p \<union> q"
+ "p \<rightarrow> q = - p \<union> q"
-lemma [intro!]: "p \<inter> p \<rightarrow> q \<subseteq> q" by (unfold imp_def) auto
-lemma [intro!]: "p \<subseteq> (q \<rightarrow> p)" by (unfold imp_def) rule
+lemma [intro!]: "p \<inter> p \<rightarrow> q \<subseteq> q" unfolding imp_def by auto
+lemma [intro!]: "p \<subseteq> (q \<rightarrow> p)" unfolding imp_def by rule
text {*
@@ -37,7 +38,7 @@
a transition relation over states @{typ "'a"}.
*}
-consts model :: "('a \<times> 'a) set" ("\<M>")
+axiomatization \<M> :: "('a \<times> 'a) set"
text {*
The operators @{text \<EX>}, @{text \<EF>}, @{text \<EG>} are taken
@@ -56,10 +57,10 @@
\cite{McMillan-PhDThesis}.
*}
-constdefs
- EX :: "'a ctl \<Rightarrow> 'a ctl" ("\<EX> _" [80] 90) "\<EX> p \<equiv> {s. \<exists>s'. (s, s') \<in> \<M> \<and> s' \<in> p}"
- EF :: "'a ctl \<Rightarrow> 'a ctl" ("\<EF> _" [80] 90) "\<EF> p \<equiv> lfp (\<lambda>s. p \<union> \<EX> s)"
- EG :: "'a ctl \<Rightarrow> 'a ctl" ("\<EG> _" [80] 90) "\<EG> p \<equiv> gfp (\<lambda>s. p \<inter> \<EX> s)"
+definition
+ EX :: "'a ctl \<Rightarrow> 'a ctl" ("\<EX> _" [80] 90) "\<EX> p = {s. \<exists>s'. (s, s') \<in> \<M> \<and> s' \<in> p}"
+ EF :: "'a ctl \<Rightarrow> 'a ctl" ("\<EF> _" [80] 90) "\<EF> p = lfp (\<lambda>s. p \<union> \<EX> s)"
+ EG :: "'a ctl \<Rightarrow> 'a ctl" ("\<EG> _" [80] 90) "\<EG> p = gfp (\<lambda>s. p \<inter> \<EX> s)"
text {*
@{text "\<AX>"}, @{text "\<AF>"} and @{text "\<AG>"} are now defined
@@ -67,10 +68,10 @@
"\<EG>"}.
*}
-constdefs
- AX :: "'a ctl \<Rightarrow> 'a ctl" ("\<AX> _" [80] 90) "\<AX> p \<equiv> - \<EX> - p"
- AF :: "'a ctl \<Rightarrow> 'a ctl" ("\<AF> _" [80] 90) "\<AF> p \<equiv> - \<EG> - p"
- AG :: "'a ctl \<Rightarrow> 'a ctl" ("\<AG> _" [80] 90) "\<AG> p \<equiv> - \<EF> - p"
+definition
+ AX :: "'a ctl \<Rightarrow> 'a ctl" ("\<AX> _" [80] 90) "\<AX> p = - \<EX> - p"
+ AF :: "'a ctl \<Rightarrow> 'a ctl" ("\<AF> _" [80] 90) "\<AF> p = - \<EG> - p"
+ AG :: "'a ctl \<Rightarrow> 'a ctl" ("\<AG> _" [80] 90) "\<AG> p = - \<EF> - p"
lemmas [simp] = EX_def EG_def AX_def EF_def AF_def AG_def
@@ -163,8 +164,6 @@
finally show ?thesis .
qed
-text {**}
-
lemma AG_fp_2: "\<AG> p \<subseteq> \<AX> \<AG> p"
proof -
note AG_fp also have "p \<inter> \<AX> \<AG> p \<subseteq> \<AX> \<AG> p" by auto
--- a/src/HOL/ex/Codegenerator.thy Sun Oct 01 12:07:57 2006 +0200
+++ b/src/HOL/ex/Codegenerator.thy Sun Oct 01 18:29:23 2006 +0200
@@ -5,7 +5,7 @@
header {* Test and Examples for code generator *}
theory Codegenerator
-imports Main "~~/src/HOL/ex/Records"
+imports Main Records
begin
subsection {* booleans *}
--- a/src/HOL/ex/Lagrange.thy Sun Oct 01 12:07:57 2006 +0200
+++ b/src/HOL/ex/Lagrange.thy Sun Oct 01 18:29:23 2006 +0200
@@ -25,34 +25,38 @@
However, this is an abstract theorem about commutative rings. It has,
a priori, nothing to do with nat. *}
-ML"Delsimprocs[ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]"
+ML_setup {*
+ Delsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]
+*}
lemma Lagrange_lemma:
- "!!x1::'a::comm_ring.
- (sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) =
- sq(x1*y1 - x2*y2 - x3*y3 - x4*y4) +
- sq(x1*y2 + x2*y1 + x3*y4 - x4*y3) +
- sq(x1*y3 - x2*y4 + x3*y1 + x4*y2) +
- sq(x1*y4 + x2*y3 - x3*y2 + x4*y1)"
-by(simp add: sq_def ring_eq_simps)
+ fixes x1 :: "'a::comm_ring"
+ shows
+ "(sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) =
+ sq (x1*y1 - x2*y2 - x3*y3 - x4*y4) +
+ sq (x1*y2 + x2*y1 + x3*y4 - x4*y3) +
+ sq (x1*y3 - x2*y4 + x3*y1 + x4*y2) +
+ sq (x1*y4 + x2*y3 - x3*y2 + x4*y1)"
+ by (simp add: sq_def ring_eq_simps)
-text{*A challenge by John Harrison. Takes about 74s on a 2.5GHz Apple G5.*}
+text {*
+ A challenge by John Harrison. Takes about 22s on a 1.6GHz machine.
+*}
-lemma "!!p1::'a::comm_ring.
- (sq p1 + sq q1 + sq r1 + sq s1 + sq t1 + sq u1 + sq v1 + sq w1) *
- (sq p2 + sq q2 + sq r2 + sq s2 + sq t2 + sq u2 + sq v2 + sq w2)
- = sq (p1*p2 - q1*q2 - r1*r2 - s1*s2 - t1*t2 - u1*u2 - v1*v2 - w1*w2) +
- sq (p1*q2 + q1*p2 + r1*s2 - s1*r2 + t1*u2 - u1*t2 - v1*w2 + w1*v2) +
- sq (p1*r2 - q1*s2 + r1*p2 + s1*q2 + t1*v2 + u1*w2 - v1*t2 - w1*u2) +
- sq (p1*s2 + q1*r2 - r1*q2 + s1*p2 + t1*w2 - u1*v2 + v1*u2 - w1*t2) +
- sq (p1*t2 - q1*u2 - r1*v2 - s1*w2 + t1*p2 + u1*q2 + v1*r2 + w1*s2) +
- sq (p1*u2 + q1*t2 - r1*w2 + s1*v2 - t1*q2 + u1*p2 - v1*s2 + w1*r2) +
- sq (p1*v2 + q1*w2 + r1*t2 - s1*u2 - t1*r2 + u1*s2 + v1*p2 - w1*q2) +
- sq (p1*w2 - q1*v2 + r1*u2 + s1*t2 - t1*s2 - u1*r2 + v1*q2 + w1*p2)"
-oops
-(*
-by(simp add: sq_def ring_eq_simps)
-*)
+lemma
+ fixes p1 :: "'a::comm_ring"
+ shows
+ "(sq p1 + sq q1 + sq r1 + sq s1 + sq t1 + sq u1 + sq v1 + sq w1) *
+ (sq p2 + sq q2 + sq r2 + sq s2 + sq t2 + sq u2 + sq v2 + sq w2)
+ = sq (p1*p2 - q1*q2 - r1*r2 - s1*s2 - t1*t2 - u1*u2 - v1*v2 - w1*w2) +
+ sq (p1*q2 + q1*p2 + r1*s2 - s1*r2 + t1*u2 - u1*t2 - v1*w2 + w1*v2) +
+ sq (p1*r2 - q1*s2 + r1*p2 + s1*q2 + t1*v2 + u1*w2 - v1*t2 - w1*u2) +
+ sq (p1*s2 + q1*r2 - r1*q2 + s1*p2 + t1*w2 - u1*v2 + v1*u2 - w1*t2) +
+ sq (p1*t2 - q1*u2 - r1*v2 - s1*w2 + t1*p2 + u1*q2 + v1*r2 + w1*s2) +
+ sq (p1*u2 + q1*t2 - r1*w2 + s1*v2 - t1*q2 + u1*p2 - v1*s2 + w1*r2) +
+ sq (p1*v2 + q1*w2 + r1*t2 - s1*u2 - t1*r2 + u1*s2 + v1*p2 - w1*q2) +
+ sq (p1*w2 - q1*v2 + r1*u2 + s1*t2 - t1*s2 - u1*r2 + v1*q2 + w1*p2)"
+ by (simp add: sq_def ring_eq_simps)
end
--- a/src/HOL/ex/NormalForm.thy Sun Oct 01 12:07:57 2006 +0200
+++ b/src/HOL/ex/NormalForm.thy Sun Oct 01 18:29:23 2006 +0200
@@ -1,8 +1,8 @@
(* ID: $Id$
Authors: Klaus Aehlig, Tobias Nipkow
+*)
-Test of normalization function
-*)
+header "Test of normalization function"
theory NormalForm
imports Main
@@ -32,11 +32,11 @@
"add2 (S m) n = S(add2 m n)"
lemma [code]: "add2 (add2 n m) k = add2 n (add2 m k)"
-by(induct n, auto)
+by(induct n) auto
lemma [code]: "add2 n (S m) = S(add2 n m)"
-by(induct n, auto)
+by(induct n) auto
lemma [code]: "add2 n Z = n"
-by(induct n, auto)
+by(induct n) auto
lemma "add2 (add2 n m) k = add2 n (add2 m k)" by normalization
lemma "add2 (add2 (S n) (S m)) (S k) = S(S(S(add2 n (add2 m k))))" by normalization
--- a/src/HOL/ex/svc_test.thy Sun Oct 01 12:07:57 2006 +0200
+++ b/src/HOL/ex/svc_test.thy Sun Oct 01 18:29:23 2006 +0200
@@ -7,10 +7,245 @@
imports SVC_Oracle
begin
-syntax
- "<->" :: "[bool, bool] => bool" (infixr 25)
+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 (tactic {* svc_tac 1 *})
+
+
+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 (tactic {* svc_tac 1 *})
+
+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 (tactic {* svc_tac 1 *})
+
+text {* @{text "fast"} only takes a couple of seconds. *}
-translations
- "x <-> y" => "x = y"
+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 (tactic {* svc_tac 1 *})
+
+
+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 (tactic {* svc_tac 1 *})
+
+text {*merely to test polarity handling in the presence of biconditionals*}
+lemma "(x < (y::int)) = (x+1 <= y)"
+ by (tactic {* svc_tac 1 *})
+
+
+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 (tactic {* svc_tac 1 *})
+
+lemma "(n::nat) < 2 ==> (n = 0) | (n = 1)"
+ by (tactic {* svc_tac 1 *})
end