tuned;
authorwenzelm
Sun Oct 01 18:29:23 2006 +0200 (2006-10-01)
changeset 20807bd3b60f9a343
parent 20806 3728dba101f1
child 20808 96d413f78870
tuned;
NEWS
src/HOL/Library/Library/ROOT.ML
src/HOL/Library/While_Combinator.thy
src/HOL/ex/BinEx.thy
src/HOL/ex/CTL.thy
src/HOL/ex/Codegenerator.thy
src/HOL/ex/Lagrange.thy
src/HOL/ex/NormalForm.thy
src/HOL/ex/svc_test.thy
     1.1 --- a/NEWS	Sun Oct 01 12:07:57 2006 +0200
     1.2 +++ b/NEWS	Sun Oct 01 18:29:23 2006 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4  Isabelle NEWS -- history user-relevant changes
     1.5  ==============================================
     1.6  
     1.7 -New in this Isabelle release
     1.8 +New in this Isabelle version
     1.9  ----------------------------
    1.10  
    1.11  *** General ***
    1.12 @@ -15,8 +15,8 @@
    1.13  with Isar theories; migration is usually quite simple with the ML
    1.14  function use_legacy_bindings.  INCOMPATIBILITY.
    1.15  
    1.16 -* Theory syntax: some popular names (e.g. "class", "if") are now
    1.17 -keywords.  INCOMPATIBILITY, use double quotes.
    1.18 +* Theory syntax: some popular names (e.g. "class", "if", "fun") are
    1.19 +now keywords.  INCOMPATIBILITY, use double quotes.
    1.20  
    1.21  * Legacy goal package: reduced interface to the bare minimum required
    1.22  to keep existing proof scripts running.  Most other user-level
    1.23 @@ -44,11 +44,12 @@
    1.24  
    1.25  *** Pure ***
    1.26  
    1.27 -* class_package.ML offers a combination of axclasses and locales to achieve
    1.28 -Haskell-like type classes in Isabelle. See HOL/ex/Classpackage.thy for examples.
    1.29 -
    1.30 -* Yet another code generator framework allows to generate executable code
    1.31 -for ML and Haskell (including "class"es). A short usage sketch:
    1.32 +* class_package.ML offers a combination of axclasses and locales to
    1.33 +achieve Haskell-like type classes in Isabelle. See
    1.34 +HOL/ex/Classpackage.thy for examples.
    1.35 +
    1.36 +* Yet another code generator framework allows to generate executable
    1.37 +code for ML and Haskell (including "class"es). A short usage sketch:
    1.38  
    1.39      internal compilation:
    1.40          code_gen <list of constants (term syntax)> (SML -)
    1.41 @@ -564,6 +565,8 @@
    1.42  * inductive and datatype: provide projections of mutual rules, bundled
    1.43  as foo_bar.inducts;
    1.44  
    1.45 +* Library: theory Infinite_Set has been moved to the library.
    1.46 +
    1.47  * Library: theory Accessible_Part has been move to main HOL.
    1.48  
    1.49  * Library: added theory Coinductive_List of potentially infinite lists
    1.50 @@ -572,30 +575,36 @@
    1.51  * Library: added theory AssocList which implements (finite) maps as
    1.52  association lists.
    1.53  
    1.54 -* New proof method "evaluation" for efficiently solving a goal
    1.55 -  (i.e. a boolean expression) by compiling it to ML. The goal is
    1.56 -  "proved" (via the oracle "Evaluation") if it evaluates to True.
    1.57 -
    1.58 -* Linear arithmetic now splits certain operators (e.g. min, max, abs) also
    1.59 -when invoked by the simplifier.  This results in the simplifier being more
    1.60 -powerful on arithmetic goals.
    1.61 -INCOMPATIBILTY: rewrite proofs.  Set fast_arith_split_limit to 0 to obtain
    1.62 -the old behavior.
    1.63 +* New proof method "evaluation" for efficiently solving a goal (i.e. a
    1.64 +boolean expression) by compiling it to ML. The goal is "proved" (via
    1.65 +the oracle "Evaluation") if it evaluates to True.
    1.66 +
    1.67 +* Linear arithmetic now splits certain operators (e.g. min, max, abs)
    1.68 +also when invoked by the simplifier.  This results in the simplifier
    1.69 +being more powerful on arithmetic goals.  INCOMPATIBILTY.  Set
    1.70 +fast_arith_split_limit to 0 to obtain the old behavior.
    1.71  
    1.72  * Support for hex (0x20) and binary (0b1001) numerals. 
    1.73  
    1.74 -* New method:
    1.75 -  reify eqs (t), where eqs are equations for an interpretation 
    1.76 - I :: 'a list => 'b => 'c and t::'c is an optional parameter,
    1.77 - computes a term s::'b and a list xs::'a list and proves the theorem
    1.78 -  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.
    1.79 -If t is omitted, the subgoal itself is reified.
    1.80 -
    1.81 -* New method:
    1.82 - reflection corr_thm eqs (t). The parameters eqs and (t) are as explained above. corr_thm is a theorem for 
    1.83 -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.
    1.84 -
    1.85 -* Reflection: Automatic refification now handels binding, an example is available in HOL/ex/ReflectionEx.thy
    1.86 +* New method: reify eqs (t), where eqs are equations for an
    1.87 +interpretation I :: 'a list => 'b => 'c and t::'c is an optional
    1.88 +parameter, computes a term s::'b and a list xs::'a list and proves the
    1.89 +theorem I xs s = t. This is also known as reification or quoting. The
    1.90 +resulting theorem is applied to the subgoal to substitute t with I xs
    1.91 +s.  If t is omitted, the subgoal itself is reified.
    1.92 +
    1.93 +* New method: reflection corr_thm eqs (t). The parameters eqs and (t)
    1.94 +are as explained above. corr_thm is a theorem for I vs (f t) = I vs t,
    1.95 +where f is supposed to be a computable function (in the sense of code
    1.96 +generattion). The method uses reify to compute s and xs as above then
    1.97 +applies corr_thm and uses normalization by evaluation to "prove" f s =
    1.98 +r and finally gets the theorem t = r, which is again applied to the
    1.99 +subgoal. An Example is available in HOL/ex/ReflectionEx.thy.
   1.100 +
   1.101 +* Reflection: Automatic refification now handels binding, an example
   1.102 +is available in HOL/ex/ReflectionEx.thy
   1.103 +
   1.104 +
   1.105  *** HOL-Algebra ***
   1.106  
   1.107  * Method algebra is now set up via an attribute.  For examples see CRing.thy.
   1.108 @@ -607,6 +616,7 @@
   1.109  
   1.110  * Renamed `CRing.thy' to `Ring.thy'.  INCOMPATIBILITY.
   1.111  
   1.112 +
   1.113  *** HOL-Complex ***
   1.114  
   1.115  * Theory Real: new method ferrack implements quantifier elimination
     2.1 --- a/src/HOL/Library/Library/ROOT.ML	Sun Oct 01 12:07:57 2006 +0200
     2.2 +++ b/src/HOL/Library/Library/ROOT.ML	Sun Oct 01 18:29:23 2006 +0200
     2.3 @@ -1,3 +1,5 @@
     2.4 +(* $Id$ *)
     2.5 +
     2.6  use_thy "Library";
     2.7  use_thy "List_Prefix";
     2.8  use_thy "List_lexord";
     3.1 --- a/src/HOL/Library/While_Combinator.thy	Sun Oct 01 12:07:57 2006 +0200
     3.2 +++ b/src/HOL/Library/While_Combinator.thy	Sun Oct 01 18:29:23 2006 +0200
     3.3 @@ -37,7 +37,7 @@
     3.4  
     3.5  definition
     3.6    while :: "('a => bool) => ('a => 'a) => 'a => 'a"
     3.7 -  "while b c s == while_aux (b, c, s)"
     3.8 +  "while b c s = while_aux (b, c, s)"
     3.9  
    3.10  lemma while_aux_unfold:
    3.11    "while_aux (b, c, s) =
     4.1 --- a/src/HOL/ex/BinEx.thy	Sun Oct 01 12:07:57 2006 +0200
     4.2 +++ b/src/HOL/ex/BinEx.thy	Sun Oct 01 18:29:23 2006 +0200
     4.3 @@ -10,9 +10,6 @@
     4.4  
     4.5  subsection {* Regression Testing for Cancellation Simprocs *}
     4.6  
     4.7 -(*taken from HOL/Integ/int_arith1.ML *)
     4.8 -
     4.9 -
    4.10  lemma "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)"
    4.11  apply simp  oops
    4.12  
    4.13 @@ -283,7 +280,7 @@
    4.14  
    4.15  lemma "Suc 99999 = 100000"
    4.16    by (simp add: Suc_nat_number_of)
    4.17 -    -- {* not a default rewrite since sometimes we want to have @{text "Suc #nnn"} *}
    4.18 +    -- {* not a default rewrite since sometimes we want to have @{text "Suc nnn"} *}
    4.19  
    4.20  
    4.21  text {* \medskip Addition *}
    4.22 @@ -390,8 +387,4 @@
    4.23  lemma "x + y - x + z - x - y - z + x < (1::int)"
    4.24    by simp
    4.25  
    4.26 -
    4.27 -text{*The proofs about arithmetic yielding normal forms have been deleted:
    4.28 - they are irrelevant with the new treatment of numerals.*}
    4.29 -
    4.30  end
     5.1 --- a/src/HOL/ex/CTL.thy	Sun Oct 01 12:07:57 2006 +0200
     5.2 +++ b/src/HOL/ex/CTL.thy	Sun Oct 01 18:29:23 2006 +0200
     5.3 @@ -23,12 +23,13 @@
     5.4  lemmas [intro!] = Int_greatest Un_upper2 Un_upper1 Int_lower1 Int_lower2
     5.5  
     5.6  types 'a ctl = "'a set"
     5.7 -constdefs
     5.8 +
     5.9 +definition
    5.10    imp :: "'a ctl \<Rightarrow> 'a ctl \<Rightarrow> 'a ctl"    (infixr "\<rightarrow>" 75)
    5.11 -  "p \<rightarrow> q \<equiv> - p \<union> q"
    5.12 +  "p \<rightarrow> q = - p \<union> q"
    5.13  
    5.14 -lemma [intro!]: "p \<inter> p \<rightarrow> q \<subseteq> q" by (unfold imp_def) auto
    5.15 -lemma [intro!]: "p \<subseteq> (q \<rightarrow> p)" by (unfold imp_def) rule
    5.16 +lemma [intro!]: "p \<inter> p \<rightarrow> q \<subseteq> q" unfolding imp_def by auto
    5.17 +lemma [intro!]: "p \<subseteq> (q \<rightarrow> p)" unfolding imp_def by rule
    5.18  
    5.19  
    5.20  text {*
    5.21 @@ -37,7 +38,7 @@
    5.22    a transition relation over states @{typ "'a"}.
    5.23  *}
    5.24  
    5.25 -consts model :: "('a \<times> 'a) set"    ("\<M>")
    5.26 +axiomatization \<M> :: "('a \<times> 'a) set"
    5.27  
    5.28  text {*
    5.29    The operators @{text \<EX>}, @{text \<EF>}, @{text \<EG>} are taken
    5.30 @@ -56,10 +57,10 @@
    5.31    \cite{McMillan-PhDThesis}.
    5.32  *}
    5.33  
    5.34 -constdefs
    5.35 -  EX :: "'a ctl \<Rightarrow> 'a ctl"    ("\<EX> _" [80] 90)    "\<EX> p \<equiv> {s. \<exists>s'. (s, s') \<in> \<M> \<and> s' \<in> p}"
    5.36 -  EF :: "'a ctl \<Rightarrow> 'a ctl"    ("\<EF> _" [80] 90)    "\<EF> p \<equiv> lfp (\<lambda>s. p \<union> \<EX> s)"
    5.37 -  EG :: "'a ctl \<Rightarrow> 'a ctl"    ("\<EG> _" [80] 90)    "\<EG> p \<equiv> gfp (\<lambda>s. p \<inter> \<EX> s)"
    5.38 +definition
    5.39 +  EX :: "'a ctl \<Rightarrow> 'a ctl"    ("\<EX> _" [80] 90)    "\<EX> p = {s. \<exists>s'. (s, s') \<in> \<M> \<and> s' \<in> p}"
    5.40 +  EF :: "'a ctl \<Rightarrow> 'a ctl"    ("\<EF> _" [80] 90)    "\<EF> p = lfp (\<lambda>s. p \<union> \<EX> s)"
    5.41 +  EG :: "'a ctl \<Rightarrow> 'a ctl"    ("\<EG> _" [80] 90)    "\<EG> p = gfp (\<lambda>s. p \<inter> \<EX> s)"
    5.42  
    5.43  text {*
    5.44    @{text "\<AX>"}, @{text "\<AF>"} and @{text "\<AG>"} are now defined
    5.45 @@ -67,10 +68,10 @@
    5.46    "\<EG>"}.
    5.47  *}
    5.48  
    5.49 -constdefs
    5.50 -  AX :: "'a ctl \<Rightarrow> 'a ctl"    ("\<AX> _" [80] 90)    "\<AX> p \<equiv> - \<EX> - p"
    5.51 -  AF :: "'a ctl \<Rightarrow> 'a ctl"    ("\<AF> _" [80] 90)    "\<AF> p \<equiv> - \<EG> - p"
    5.52 -  AG :: "'a ctl \<Rightarrow> 'a ctl"    ("\<AG> _" [80] 90)    "\<AG> p \<equiv> - \<EF> - p"
    5.53 +definition
    5.54 +  AX :: "'a ctl \<Rightarrow> 'a ctl"    ("\<AX> _" [80] 90)    "\<AX> p = - \<EX> - p"
    5.55 +  AF :: "'a ctl \<Rightarrow> 'a ctl"    ("\<AF> _" [80] 90)    "\<AF> p = - \<EG> - p"
    5.56 +  AG :: "'a ctl \<Rightarrow> 'a ctl"    ("\<AG> _" [80] 90)    "\<AG> p = - \<EF> - p"
    5.57  
    5.58  lemmas [simp] = EX_def EG_def AX_def EF_def AF_def AG_def
    5.59  
    5.60 @@ -163,8 +164,6 @@
    5.61    finally show ?thesis .
    5.62  qed
    5.63  
    5.64 -text {**}
    5.65 -
    5.66  lemma AG_fp_2: "\<AG> p \<subseteq> \<AX> \<AG> p"
    5.67  proof -
    5.68    note AG_fp also have "p \<inter> \<AX> \<AG> p \<subseteq> \<AX> \<AG> p" by auto
     6.1 --- a/src/HOL/ex/Codegenerator.thy	Sun Oct 01 12:07:57 2006 +0200
     6.2 +++ b/src/HOL/ex/Codegenerator.thy	Sun Oct 01 18:29:23 2006 +0200
     6.3 @@ -5,7 +5,7 @@
     6.4  header {* Test and Examples for code generator *}
     6.5  
     6.6  theory Codegenerator
     6.7 -imports Main "~~/src/HOL/ex/Records"
     6.8 +imports Main Records
     6.9  begin
    6.10  
    6.11  subsection {* booleans *}
     7.1 --- a/src/HOL/ex/Lagrange.thy	Sun Oct 01 12:07:57 2006 +0200
     7.2 +++ b/src/HOL/ex/Lagrange.thy	Sun Oct 01 18:29:23 2006 +0200
     7.3 @@ -25,34 +25,38 @@
     7.4  However, this is an abstract theorem about commutative rings.  It has,
     7.5  a priori, nothing to do with nat. *}
     7.6  
     7.7 -ML"Delsimprocs[ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]"
     7.8 +ML_setup {*
     7.9 +  Delsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]
    7.10 +*}
    7.11  
    7.12  lemma Lagrange_lemma:
    7.13 - "!!x1::'a::comm_ring.
    7.14 -  (sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) =
    7.15 -  sq(x1*y1 - x2*y2 - x3*y3 - x4*y4)  +
    7.16 -  sq(x1*y2 + x2*y1 + x3*y4 - x4*y3)  +
    7.17 -  sq(x1*y3 - x2*y4 + x3*y1 + x4*y2)  +
    7.18 -  sq(x1*y4 + x2*y3 - x3*y2 + x4*y1)"
    7.19 -by(simp add: sq_def ring_eq_simps)
    7.20 +  fixes x1 :: "'a::comm_ring"
    7.21 +  shows
    7.22 +  "(sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) =
    7.23 +    sq (x1*y1 - x2*y2 - x3*y3 - x4*y4)  +
    7.24 +    sq (x1*y2 + x2*y1 + x3*y4 - x4*y3)  +
    7.25 +    sq (x1*y3 - x2*y4 + x3*y1 + x4*y2)  +
    7.26 +    sq (x1*y4 + x2*y3 - x3*y2 + x4*y1)"
    7.27 +  by (simp add: sq_def ring_eq_simps)
    7.28  
    7.29  
    7.30 -text{*A challenge by John Harrison. Takes about 74s on a 2.5GHz Apple G5.*}
    7.31 +text {*
    7.32 +  A challenge by John Harrison. Takes about 22s on a 1.6GHz machine.
    7.33 +*}
    7.34  
    7.35 -lemma "!!p1::'a::comm_ring.
    7.36 - (sq p1 + sq q1 + sq r1 + sq s1 + sq t1 + sq u1 + sq v1 + sq w1) * 
    7.37 - (sq p2 + sq q2 + sq r2 + sq s2 + sq t2 + sq u2 + sq v2 + sq w2) 
    7.38 -  = sq (p1*p2 - q1*q2 - r1*r2 - s1*s2 - t1*t2 - u1*u2 - v1*v2 - w1*w2) + 
    7.39 -    sq (p1*q2 + q1*p2 + r1*s2 - s1*r2 + t1*u2 - u1*t2 - v1*w2 + w1*v2) +
    7.40 -    sq (p1*r2 - q1*s2 + r1*p2 + s1*q2 + t1*v2 + u1*w2 - v1*t2 - w1*u2) +
    7.41 -    sq (p1*s2 + q1*r2 - r1*q2 + s1*p2 + t1*w2 - u1*v2 + v1*u2 - w1*t2) +
    7.42 -    sq (p1*t2 - q1*u2 - r1*v2 - s1*w2 + t1*p2 + u1*q2 + v1*r2 + w1*s2) +
    7.43 -    sq (p1*u2 + q1*t2 - r1*w2 + s1*v2 - t1*q2 + u1*p2 - v1*s2 + w1*r2) +
    7.44 -    sq (p1*v2 + q1*w2 + r1*t2 - s1*u2 - t1*r2 + u1*s2 + v1*p2 - w1*q2) +
    7.45 -    sq (p1*w2 - q1*v2 + r1*u2 + s1*t2 - t1*s2 - u1*r2 + v1*q2 + w1*p2)"
    7.46 -oops
    7.47 -(*
    7.48 -by(simp add: sq_def ring_eq_simps)
    7.49 -*)
    7.50 +lemma
    7.51 +  fixes p1 :: "'a::comm_ring"
    7.52 +  shows
    7.53 +  "(sq p1 + sq q1 + sq r1 + sq s1 + sq t1 + sq u1 + sq v1 + sq w1) * 
    7.54 +   (sq p2 + sq q2 + sq r2 + sq s2 + sq t2 + sq u2 + sq v2 + sq w2) 
    7.55 +    = sq (p1*p2 - q1*q2 - r1*r2 - s1*s2 - t1*t2 - u1*u2 - v1*v2 - w1*w2) + 
    7.56 +      sq (p1*q2 + q1*p2 + r1*s2 - s1*r2 + t1*u2 - u1*t2 - v1*w2 + w1*v2) +
    7.57 +      sq (p1*r2 - q1*s2 + r1*p2 + s1*q2 + t1*v2 + u1*w2 - v1*t2 - w1*u2) +
    7.58 +      sq (p1*s2 + q1*r2 - r1*q2 + s1*p2 + t1*w2 - u1*v2 + v1*u2 - w1*t2) +
    7.59 +      sq (p1*t2 - q1*u2 - r1*v2 - s1*w2 + t1*p2 + u1*q2 + v1*r2 + w1*s2) +
    7.60 +      sq (p1*u2 + q1*t2 - r1*w2 + s1*v2 - t1*q2 + u1*p2 - v1*s2 + w1*r2) +
    7.61 +      sq (p1*v2 + q1*w2 + r1*t2 - s1*u2 - t1*r2 + u1*s2 + v1*p2 - w1*q2) +
    7.62 +      sq (p1*w2 - q1*v2 + r1*u2 + s1*t2 - t1*s2 - u1*r2 + v1*q2 + w1*p2)"
    7.63 +  by (simp add: sq_def ring_eq_simps)
    7.64  
    7.65  end
     8.1 --- a/src/HOL/ex/NormalForm.thy	Sun Oct 01 12:07:57 2006 +0200
     8.2 +++ b/src/HOL/ex/NormalForm.thy	Sun Oct 01 18:29:23 2006 +0200
     8.3 @@ -1,8 +1,8 @@
     8.4  (*  ID:         $Id$
     8.5      Authors:    Klaus Aehlig, Tobias Nipkow
     8.6 +*)
     8.7  
     8.8 -Test of normalization function
     8.9 -*)
    8.10 +header "Test of normalization function"
    8.11  
    8.12  theory NormalForm
    8.13  imports Main
    8.14 @@ -32,11 +32,11 @@
    8.15  "add2 (S m) n = S(add2 m n)"
    8.16  
    8.17  lemma [code]: "add2 (add2 n m) k = add2 n (add2 m k)"
    8.18 -by(induct n, auto)
    8.19 +by(induct n) auto
    8.20  lemma [code]: "add2 n (S m) =  S(add2 n m)"
    8.21 -by(induct n, auto)
    8.22 +by(induct n) auto
    8.23  lemma [code]: "add2 n Z = n"
    8.24 -by(induct n, auto)
    8.25 +by(induct n) auto
    8.26  
    8.27  lemma "add2 (add2 n m) k = add2 n (add2 m k)" by normalization
    8.28  lemma "add2 (add2 (S n) (S m)) (S k) = S(S(S(add2 n (add2 m k))))" by normalization
     9.1 --- a/src/HOL/ex/svc_test.thy	Sun Oct 01 12:07:57 2006 +0200
     9.2 +++ b/src/HOL/ex/svc_test.thy	Sun Oct 01 18:29:23 2006 +0200
     9.3 @@ -7,10 +7,245 @@
     9.4  imports SVC_Oracle
     9.5  begin
     9.6  
     9.7 -syntax
     9.8 -  "<->" :: "[bool, bool] => bool"    (infixr 25)
     9.9 +subsubsection {* Propositional Logic *}
    9.10 +
    9.11 +text {*
    9.12 +  @{text "blast"}'s runtime for this type of problem appears to be exponential
    9.13 +  in its length, though @{text "fast"} manages.
    9.14 +*}
    9.15 +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"
    9.16 +  by (tactic {* svc_tac 1 *})
    9.17 +
    9.18 +
    9.19 +subsection {* Some big tautologies supplied by John Harrison *}
    9.20 +
    9.21 +text {*
    9.22 +  @{text "auto"} manages; @{text "blast"} and @{text "fast"} take a minute or more.
    9.23 +*}
    9.24 +lemma puz013_1: "~(~v12 &
    9.25 +   v0 &
    9.26 +   v10 &
    9.27 +   (v4 | v5) &
    9.28 +   (v9 | v2) &
    9.29 +   (v8 | v1) &
    9.30 +   (v7 | v0) &
    9.31 +   (v3 | v12) &
    9.32 +   (v11 | v10) &
    9.33 +   (~v12 | ~v6 | v7) &
    9.34 +   (~v10 | ~v3 | v1) &
    9.35 +   (~v10 | ~v0 | ~v4 | v11) &
    9.36 +   (~v5 | ~v2 | ~v8) &
    9.37 +   (~v12 | ~v9 | ~v7) &
    9.38 +   (~v0 | ~v1 | v4) &
    9.39 +   (~v4 | v7 | v2) &
    9.40 +   (~v12 | ~v3 | v8) &
    9.41 +   (~v4 | v5 | v6) &
    9.42 +   (~v7 | ~v8 | v9) &
    9.43 +   (~v10 | ~v11 | v12))"
    9.44 +  by (tactic {* svc_tac 1 *})
    9.45 +
    9.46 +lemma dk17_be:
    9.47 +  "(GE17 <-> ~IN4 & ~IN3 & ~IN2 & ~IN1) &
    9.48 +    (GE0 <-> GE17 & ~IN5) &
    9.49 +    (GE22 <-> ~IN9 & ~IN7 & ~IN6 & IN0) &
    9.50 +    (GE19 <-> ~IN5 & ~IN4 & ~IN3 & ~IN0) &
    9.51 +    (GE20 <-> ~IN7 & ~IN6) &
    9.52 +    (GE18 <-> ~IN6 & ~IN2 & ~IN1 & ~IN0) &
    9.53 +    (GE21 <-> IN9 & ~IN7 & IN6 & ~IN0) &
    9.54 +    (GE23 <-> GE22 & GE0) &
    9.55 +    (GE25 <-> ~IN9 & ~IN7 & IN6 & ~IN0) &
    9.56 +    (GE26 <-> IN9 & ~IN7 & ~IN6 & IN0) &
    9.57 +    (GE2 <-> GE20 & GE19) &
    9.58 +    (GE1 <-> GE18 & ~IN7) &
    9.59 +    (GE24 <-> GE23 | GE21 & GE0) &
    9.60 +    (GE5 <-> ~IN5 & IN4 | IN5 & ~IN4) &
    9.61 +    (GE6 <-> GE0 & IN7 & ~IN6 & ~IN0) &
    9.62 +    (GE12 <-> GE26 & GE0 | GE25 & GE0) &
    9.63 +    (GE14 <-> GE2 & IN8 & ~IN2 & IN1) &
    9.64 +    (GE27 <-> ~IN8 & IN5 & ~IN4 & ~IN3) &
    9.65 +    (GE9 <-> GE1 & ~IN5 & ~IN4 & IN3) &
    9.66 +    (GE7 <-> GE24 | GE2 & IN2 & ~IN1) &
    9.67 +    (GE10 <-> GE6 | GE5 & GE1 & ~IN3) &
    9.68 +    (GE15 <-> ~IN8 | IN9) &
    9.69 +    (GE16 <-> GE12 | GE14 & ~IN9) &
    9.70 +    (GE4 <->
    9.71 +     GE5 & GE1 & IN8 & ~IN3 |
    9.72 +     GE0 & ~IN7 & IN6 & ~IN0 |
    9.73 +     GE2 & IN2 & ~IN1) &
    9.74 +    (GE13 <-> GE27 & GE1) &
    9.75 +    (GE11 <-> GE9 | GE6 & ~IN8) &
    9.76 +    (GE8 <-> GE1 & ~IN5 & IN4 & ~IN3 | GE2 & ~IN2 & IN1) &
    9.77 +    (OUT0 <-> GE7 & ~IN8) &
    9.78 +    (OUT1 <-> GE7 & IN8) &
    9.79 +    (OUT2 <-> GE8 & ~IN9 | GE10 & IN8) &
    9.80 +    (OUT3 <-> GE8 & IN9 & ~IN8 | GE11 & ~IN9 | GE12 & ~IN8) &
    9.81 +    (OUT4 <-> GE11 & IN9 | GE12 & IN8) &
    9.82 +    (OUT5 <-> GE14 & IN9) &
    9.83 +    (OUT6 <-> GE13 & ~IN9) &
    9.84 +    (OUT7 <-> GE13 & IN9) &
    9.85 +    (OUT8 <-> GE9 & ~IN8 | GE15 & GE6 | GE4 & IN9) &
    9.86 +    (OUT9 <-> GE9 & IN8 | ~GE15 & GE10 | GE16) &
    9.87 +    (OUT10 <-> GE7) &
    9.88 +    (WRES0 <-> ~IN5 & ~IN4 & ~IN3 & ~IN2 & ~IN1) &
    9.89 +    (WRES1 <-> ~IN7 & ~IN6 & ~IN2 & ~IN1 & ~IN0) &
    9.90 +    (WRES2 <-> ~IN7 & ~IN6 & ~IN5 & ~IN4 & ~IN3 & ~IN0) &
    9.91 +    (WRES5 <-> ~IN5 & IN4 | IN5 & ~IN4) &
    9.92 +    (WRES6 <-> WRES0 & IN7 & ~IN6 & ~IN0) &
    9.93 +    (WRES9 <-> WRES1 & ~IN5 & ~IN4 & IN3) &
    9.94 +    (WRES7 <->
    9.95 +     WRES0 & ~IN9 & ~IN7 & ~IN6 & IN0 |
    9.96 +     WRES0 & IN9 & ~IN7 & IN6 & ~IN0 |
    9.97 +     WRES2 & IN2 & ~IN1) &
    9.98 +    (WRES10 <-> WRES6 | WRES5 & WRES1 & ~IN3) &
    9.99 +    (WRES12 <->
   9.100 +     WRES0 & IN9 & ~IN7 & ~IN6 & IN0 |
   9.101 +     WRES0 & ~IN9 & ~IN7 & IN6 & ~IN0) &
   9.102 +    (WRES14 <-> WRES2 & IN8 & ~IN2 & IN1) &
   9.103 +    (WRES15 <-> ~IN8 | IN9) &
   9.104 +    (WRES4 <->
   9.105 +     WRES5 & WRES1 & IN8 & ~IN3 |
   9.106 +     WRES2 & IN2 & ~IN1 |
   9.107 +     WRES0 & ~IN7 & IN6 & ~IN0) &
   9.108 +    (WRES13 <-> WRES1 & ~IN8 & IN5 & ~IN4 & ~IN3) &
   9.109 +    (WRES11 <-> WRES9 | WRES6 & ~IN8) &
   9.110 +    (WRES8 <-> WRES1 & ~IN5 & IN4 & ~IN3 | WRES2 & ~IN2 & IN1)
   9.111 +    --> (OUT10 <-> WRES7) &
   9.112 +        (OUT9 <-> WRES9 & IN8 | WRES12 | WRES14 & ~IN9 | ~WRES15 & WRES10) &
   9.113 +        (OUT8 <-> WRES9 & ~IN8 | WRES15 & WRES6 | WRES4 & IN9) &
   9.114 +        (OUT7 <-> WRES13 & IN9) &
   9.115 +        (OUT6 <-> WRES13 & ~IN9) &
   9.116 +        (OUT5 <-> WRES14 & IN9) &
   9.117 +        (OUT4 <-> WRES11 & IN9 | WRES12 & IN8) &
   9.118 +        (OUT3 <-> WRES8 & IN9 & ~IN8 | WRES11 & ~IN9 | WRES12 & ~IN8) &
   9.119 +        (OUT2 <-> WRES8 & ~IN9 | WRES10 & IN8) &
   9.120 +        (OUT1 <-> WRES7 & IN8) &
   9.121 +        (OUT0 <-> WRES7 & ~IN8)"
   9.122 +  by (tactic {* svc_tac 1 *})
   9.123 +
   9.124 +text {* @{text "fast"} only takes a couple of seconds. *}
   9.125  
   9.126 -translations
   9.127 -  "x <-> y" => "x = y"
   9.128 +lemma sqn_be: "(GE0 <-> IN6 & IN1 | ~IN6 & ~IN1) &
   9.129 +   (GE8 <-> ~IN3 & ~IN1) &
   9.130 +   (GE5 <-> IN6 | IN5) &
   9.131 +   (GE9 <-> ~GE0 | IN2 | ~IN5) &
   9.132 +   (GE1 <-> IN3 | ~IN0) &
   9.133 +   (GE11 <-> GE8 & IN4) &
   9.134 +   (GE3 <-> ~IN4 | ~IN2) &
   9.135 +   (GE34 <-> ~GE5 & IN4 | ~GE9) &
   9.136 +   (GE2 <-> ~IN4 & IN1) &
   9.137 +   (GE14 <-> ~GE1 & ~IN4) &
   9.138 +   (GE19 <-> GE11 & ~GE5) &
   9.139 +   (GE13 <-> GE8 & ~GE3 & ~IN0) &
   9.140 +   (GE20 <-> ~IN5 & IN2 | GE34) &
   9.141 +   (GE12 <-> GE2 & ~IN3) &
   9.142 +   (GE27 <-> GE14 & IN6 | GE19) &
   9.143 +   (GE10 <-> ~IN6 | IN5) &
   9.144 +   (GE28 <-> GE13 | GE20 & ~GE1) &
   9.145 +   (GE6 <-> ~IN5 | IN6) &
   9.146 +   (GE15 <-> GE2 & IN2) &
   9.147 +   (GE29 <-> GE27 | GE12 & GE5) &
   9.148 +   (GE4 <-> IN3 & ~IN0) &
   9.149 +   (GE21 <-> ~GE10 & ~IN1 | ~IN5 & ~IN2) &
   9.150 +   (GE30 <-> GE28 | GE14 & IN2) &
   9.151 +   (GE31 <-> GE29 | GE15 & ~GE6) &
   9.152 +   (GE7 <-> ~IN6 | ~IN5) &
   9.153 +   (GE17 <-> ~GE3 & ~IN1) &
   9.154 +   (GE18 <-> GE4 & IN2) &
   9.155 +   (GE16 <-> GE2 & IN0) &
   9.156 +   (GE23 <-> GE19 | GE9 & ~GE1) &
   9.157 +   (GE32 <-> GE15 & ~IN6 & ~IN0 | GE21 & GE4 & ~IN4 | GE30 | GE31) &
   9.158 +   (GE33 <->
   9.159 +    GE18 & ~GE6 & ~IN4 |
   9.160 +    GE17 & ~GE7 & IN3 |
   9.161 +    ~GE7 & GE4 & ~GE3 |
   9.162 +    GE11 & IN5 & ~IN0) &
   9.163 +   (GE25 <-> GE14 & ~GE6 | GE13 & ~GE5 | GE16 & ~IN5 | GE15 & GE1) &
   9.164 +   (GE26 <->
   9.165 +    GE12 & IN5 & ~IN2 |
   9.166 +    GE10 & GE4 & IN1 |
   9.167 +    GE17 & ~GE6 & IN0 |
   9.168 +    GE2 & ~IN6) &
   9.169 +   (GE24 <-> GE23 | GE16 & GE7) &
   9.170 +   (OUT0 <->
   9.171 +    GE6 & IN4 & ~IN1 & IN0 | GE18 & GE0 & ~IN5 | GE12 & ~GE10 | GE24) &
   9.172 +   (OUT1 <-> GE26 | GE25 | ~GE5 & GE4 & GE3 | GE7 & ~GE1 & IN1) &
   9.173 +   (OUT2 <-> GE33 | GE32) &
   9.174 +   (WRES8 <-> ~IN3 & ~IN1) &
   9.175 +   (WRES0 <-> IN6 & IN1 | ~IN6 & ~IN1) &
   9.176 +   (WRES2 <-> ~IN4 & IN1) &
   9.177 +   (WRES3 <-> ~IN4 | ~IN2) &
   9.178 +   (WRES1 <-> IN3 | ~IN0) &
   9.179 +   (WRES4 <-> IN3 & ~IN0) &
   9.180 +   (WRES5 <-> IN6 | IN5) &
   9.181 +   (WRES11 <-> WRES8 & IN4) &
   9.182 +   (WRES9 <-> ~WRES0 | IN2 | ~IN5) &
   9.183 +   (WRES10 <-> ~IN6 | IN5) &
   9.184 +   (WRES6 <-> ~IN5 | IN6) &
   9.185 +   (WRES7 <-> ~IN6 | ~IN5) &
   9.186 +   (WRES12 <-> WRES2 & ~IN3) &
   9.187 +   (WRES13 <-> WRES8 & ~WRES3 & ~IN0) &
   9.188 +   (WRES14 <-> ~WRES1 & ~IN4) &
   9.189 +   (WRES15 <-> WRES2 & IN2) &
   9.190 +   (WRES17 <-> ~WRES3 & ~IN1) &
   9.191 +   (WRES18 <-> WRES4 & IN2) &
   9.192 +   (WRES19 <-> WRES11 & ~WRES5) &
   9.193 +   (WRES20 <-> ~IN5 & IN2 | ~WRES5 & IN4 | ~WRES9) &
   9.194 +   (WRES21 <-> ~WRES10 & ~IN1 | ~IN5 & ~IN2) &
   9.195 +   (WRES16 <-> WRES2 & IN0)
   9.196 +   --> (OUT2 <->
   9.197 +        WRES11 & IN5 & ~IN0 |
   9.198 +        ~WRES7 & WRES4 & ~WRES3 |
   9.199 +        WRES12 & WRES5 |
   9.200 +        WRES13 |
   9.201 +        WRES14 & IN2 |
   9.202 +        WRES14 & IN6 |
   9.203 +        WRES15 & ~WRES6 |
   9.204 +        WRES15 & ~IN6 & ~IN0 |
   9.205 +        WRES17 & ~WRES7 & IN3 |
   9.206 +        WRES18 & ~WRES6 & ~IN4 |
   9.207 +        WRES20 & ~WRES1 |
   9.208 +        WRES21 & WRES4 & ~IN4 |
   9.209 +        WRES19) &
   9.210 +       (OUT1 <->
   9.211 +        ~WRES5 & WRES4 & WRES3 |
   9.212 +        WRES7 & ~WRES1 & IN1 |
   9.213 +        WRES2 & ~IN6 |
   9.214 +        WRES10 & WRES4 & IN1 |
   9.215 +        WRES12 & IN5 & ~IN2 |
   9.216 +        WRES13 & ~WRES5 |
   9.217 +        WRES14 & ~WRES6 |
   9.218 +        WRES15 & WRES1 |
   9.219 +        WRES16 & ~IN5 |
   9.220 +        WRES17 & ~WRES6 & IN0) &
   9.221 +       (OUT0 <->
   9.222 +        WRES6 & IN4 & ~IN1 & IN0 |
   9.223 +        WRES9 & ~WRES1 |
   9.224 +        WRES12 & ~WRES10 |
   9.225 +        WRES16 & WRES7 |
   9.226 +        WRES18 & WRES0 & ~IN5 |
   9.227 +        WRES19)"
   9.228 +  by (tactic {* svc_tac 1 *})
   9.229 +
   9.230 +
   9.231 +subsection {* Linear arithmetic *}
   9.232 +
   9.233 +lemma "x ~= 14 & x ~= 13 & x ~= 12 & x ~= 11 & x ~= 10 & x ~= 9 &
   9.234 +      x ~= 8 & x ~= 7 & x ~= 6 & x ~= 5 & x ~= 4 & x ~= 3 &
   9.235 +      x ~= 2 & x ~= 1 & 0 < x & x < 16 --> 15 = (x::int)"
   9.236 +  by (tactic {* svc_tac 1 *})
   9.237 +
   9.238 +text {*merely to test polarity handling in the presence of biconditionals*}
   9.239 +lemma "(x < (y::int)) = (x+1 <= y)"
   9.240 +  by (tactic {* svc_tac 1 *})
   9.241 +
   9.242 +
   9.243 +subsection {* Natural number examples requiring implicit "non-negative" assumptions *}
   9.244 +
   9.245 +lemma "(3::nat)*a <= 2 + 4*b + 6*c  & 11 <= 2*a + b + 2*c &
   9.246 +      a + 3*b <= 5 + 2*c  --> 2 + 3*b <= 2*a + 6*c"
   9.247 +  by (tactic {* svc_tac 1 *})
   9.248 +
   9.249 +lemma "(n::nat) < 2 ==> (n = 0) | (n = 1)"
   9.250 +  by (tactic {* svc_tac 1 *})
   9.251  
   9.252  end