some tests for arith added
authorwebertj
Fri Jun 01 23:21:40 2007 +0200 (2007-06-01)
changeset 231931f2d94b6a8ef
parent 23192 ec73b9707d48
child 23194 085fa3def13b
some tests for arith added
src/HOL/IsaMakefile
src/HOL/ex/Arith_Examples.thy
src/HOL/ex/ROOT.ML
     1.1 --- a/src/HOL/IsaMakefile	Fri Jun 01 22:09:16 2007 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri Jun 01 23:21:40 2007 +0200
     1.3 @@ -618,7 +618,8 @@
     1.4  HOL-ex: HOL $(LOG)/HOL-ex.gz
     1.5  
     1.6  $(LOG)/HOL-ex.gz: $(OUT)/HOL Library/Commutative_Ring.thy                       \
     1.7 -  ex/Abstract_NAT.thy ex/Antiquote.thy ex/BT.thy ex/BinEx.thy                   \
     1.8 +  ex/Abstract_NAT.thy ex/Antiquote.thy ex/Arith_Examples.thy                    \
     1.9 +  ex/BT.thy ex/BinEx.thy                                                        \
    1.10    ex/Chinese.thy ex/Classical.thy ex/Classpackage.thy                           \
    1.11    ex/Eval_examples.thy ex/Random.thy                                            \
    1.12    ex/Codegenerator.thy ex/Codegenerator_Rat.thy                                 \
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/ex/Arith_Examples.thy	Fri Jun 01 23:21:40 2007 +0200
     2.3 @@ -0,0 +1,163 @@
     2.4 +(*  Title:  HOL/ex/Arith_Examples.thy
     2.5 +    ID:     $Id$
     2.6 +    Author: Tjark Weber
     2.7 +*)
     2.8 +
     2.9 +header {* {\tt arith} *}
    2.10 +
    2.11 +theory Arith_Examples imports Main begin
    2.12 +
    2.13 +text {*
    2.14 +  The {\tt arith} tactic is used frequently throughout the Isabelle
    2.15 +  distribution.  This file merely contains some additional tests and special
    2.16 +  corner cases.  Some rather technical remarks:
    2.17 +
    2.18 +  {\tt fast_arith_tac} is a very basic version of the tactic.  It performs no
    2.19 +  meta-to-object-logic conversion, and only some splitting of operators.
    2.20 +  {\tt simple_arith_tac} performs meta-to-object-logic conversion, full
    2.21 +  splitting of operators, and NNF normalization of the goal.  The {\tt arith}
    2.22 +  tactic combines them both, and tries other tactics (e.g.~{\tt presburger})
    2.23 +  as well.  This is the one that you should use in your proofs!
    2.24 +
    2.25 +  An {\tt arith}-based simproc is available as well (see {\tt
    2.26 +  Fast_Arith.lin_arith_prover}), which---for performance reasons---however
    2.27 +  does even less splitting than {\tt fast_arith_tac} at the moment (namely
    2.28 +  inequalities only).  (On the other hand, it does take apart conjunctions,
    2.29 +  which {\tt fast_arith_tac} currently does not do.)
    2.30 +*}
    2.31 +
    2.32 +ML {* set trace_arith; *}
    2.33 +
    2.34 +section {* Splitting of Operators: @{term max}, @{term min}, @{term abs},
    2.35 +           @{term HOL.minus}, @{term nat}, @{term Divides.mod},
    2.36 +           @{term Divides.div} *}
    2.37 +
    2.38 +lemma "(i::nat) <= max i j"
    2.39 +  by (tactic {* fast_arith_tac 1 *})
    2.40 +
    2.41 +lemma "(i::int) <= max i j"
    2.42 +  by (tactic {* fast_arith_tac 1 *})
    2.43 +
    2.44 +lemma "min i j <= (i::nat)"
    2.45 +  by (tactic {* fast_arith_tac 1 *})
    2.46 +
    2.47 +lemma "min i j <= (i::int)"
    2.48 +  by (tactic {* fast_arith_tac 1 *})
    2.49 +
    2.50 +lemma "min (i::nat) j <= max i j"
    2.51 +  by (tactic {* fast_arith_tac 1 *})
    2.52 +
    2.53 +lemma "min (i::int) j <= max i j"
    2.54 +  by (tactic {* fast_arith_tac 1 *})
    2.55 +
    2.56 +lemma "(i::nat) < j ==> min i j < max i j"
    2.57 +  by (tactic {* fast_arith_tac 1 *})
    2.58 +
    2.59 +lemma "(i::int) < j ==> min i j < max i j"
    2.60 +  by (tactic {* fast_arith_tac 1 *})
    2.61 +
    2.62 +lemma "(0::int) <= abs i"
    2.63 +  by (tactic {* fast_arith_tac 1 *})
    2.64 +
    2.65 +lemma "(i::int) <= abs i"
    2.66 +  by (tactic {* fast_arith_tac 1 *})
    2.67 +
    2.68 +lemma "abs (abs (i::int)) = abs i"
    2.69 +  by (tactic {* fast_arith_tac 1 *})
    2.70 +
    2.71 +text {* Also testing subgoals with bound variables. *}
    2.72 +
    2.73 +lemma "!!x. (x::nat) <= y ==> x - y = 0"
    2.74 +  by (tactic {* fast_arith_tac 1 *})
    2.75 +
    2.76 +lemma "!!x. (x::nat) - y = 0 ==> x <= y"
    2.77 +  by (tactic {* fast_arith_tac 1 *})
    2.78 +
    2.79 +lemma "!!x. ((x::nat) <= y) = (x - y = 0)"
    2.80 +  by (tactic {* simple_arith_tac 1 *})
    2.81 +
    2.82 +lemma "[| (x::nat) < y; d < 1 |] ==> x - y = d"
    2.83 +  by (tactic {* fast_arith_tac 1 *})
    2.84 +
    2.85 +lemma "[| (x::nat) < y; d < 1 |] ==> x - y - x = d - x"
    2.86 +  by (tactic {* fast_arith_tac 1 *})
    2.87 +
    2.88 +lemma "(x::int) < y ==> x - y < 0"
    2.89 +  by (tactic {* fast_arith_tac 1 *})
    2.90 +
    2.91 +lemma "nat (i + j) <= nat i + nat j"
    2.92 +  by (tactic {* fast_arith_tac 1 *})
    2.93 +
    2.94 +lemma "i < j ==> nat (i - j) = 0"
    2.95 +  by (tactic {* fast_arith_tac 1 *})
    2.96 +
    2.97 +lemma "(i::nat) mod 0 = i"
    2.98 +oops
    2.99 +
   2.100 +lemma "(i::nat) mod (Suc 0) = 0"
   2.101 +oops
   2.102 +
   2.103 +lemma "(i::nat) div 0 = 0"
   2.104 +oops
   2.105 +
   2.106 +ML {* (#splits (ArithTheoryData.get (the_context ()))); *}
   2.107 +
   2.108 +lemma "(i::nat) mod (number_of (1::int)) = 0"
   2.109 +oops
   2.110 +
   2.111 +section {* Meta-Logic *}
   2.112 +
   2.113 +lemma "x < Suc y == x <= y"
   2.114 +  by (tactic {* simple_arith_tac 1 *})
   2.115 +
   2.116 +lemma "((x::nat) == z ==> x ~= y) ==> x ~= y | z ~= y"
   2.117 +  by (tactic {* simple_arith_tac 1 *})
   2.118 +
   2.119 +section {* Other Examples *}
   2.120 +
   2.121 +lemma "[| (x::nat) < y; y < z |] ==> x < z"
   2.122 +  by (tactic {* fast_arith_tac 1 *})
   2.123 +
   2.124 +lemma "(x::nat) < y & y < z ==> x < z"
   2.125 +  by (tactic {* simple_arith_tac 1 *})
   2.126 +
   2.127 +lemma "[| (x::nat) ~= y; a + 2 = b; a < y; y < b; a < x; x < b |] ==> False"
   2.128 +  by (tactic {* fast_arith_tac 1 *})
   2.129 +
   2.130 +lemma "[| (x::nat) > y; y > z; z > x |] ==> False"
   2.131 +  by (tactic {* fast_arith_tac 1 *})
   2.132 +
   2.133 +lemma "(x::nat) - 5 > y ==> y < x"
   2.134 +  by (tactic {* fast_arith_tac 1 *})
   2.135 +
   2.136 +lemma "(x::nat) ~= 0 ==> 0 < x"
   2.137 +  by (tactic {* fast_arith_tac 1 *})
   2.138 +
   2.139 +lemma "[| (x::nat) ~= y; x <= y |] ==> x < y"
   2.140 +  by (tactic {* fast_arith_tac 1 *})
   2.141 +
   2.142 +lemma "(x::nat) < y \<longrightarrow> P (x - y) \<longrightarrow> P 0"
   2.143 +  by (tactic {* simple_arith_tac 1 *})
   2.144 +
   2.145 +lemma "(x - y) - (x::nat) = (x - x) - y"
   2.146 +  by (tactic {* fast_arith_tac 1 *})
   2.147 +
   2.148 +lemma "[| (a::nat) < b; c < d |] ==> (a - b) = (c - d)"
   2.149 +  by (tactic {* fast_arith_tac 1 *})
   2.150 +
   2.151 +lemma "((a::nat) - (b - (c - (d - e)))) = (a - (b - (c - (d - e))))"
   2.152 +  by (tactic {* fast_arith_tac 1 *})
   2.153 +
   2.154 +text {* Splitting of inequalities of different type. *}
   2.155 +
   2.156 +lemma "[| (a::nat) ~= b; (i::int) ~= j; a < 2; b < 2 |] ==>
   2.157 +  a + b <= nat (max (abs i) (abs j))"
   2.158 +  by (tactic {* fast_arith_tac 1 *})
   2.159 +
   2.160 +lemma "[| (i::int) ~= j; (a::nat) ~= b; a < 2; b < 2 |] ==>
   2.161 +  a + b <= nat (max (abs i) (abs j))"
   2.162 +  by (tactic {* fast_arith_tac 1 *})
   2.163 +
   2.164 +ML {* reset trace_arith; *}
   2.165 +
   2.166 +end
     3.1 --- a/src/HOL/ex/ROOT.ML	Fri Jun 01 22:09:16 2007 +0200
     3.2 +++ b/src/HOL/ex/ROOT.ML	Fri Jun 01 23:21:40 2007 +0200
     3.3 @@ -39,6 +39,7 @@
     3.4  time_use_thy "Classical";
     3.5  time_use_thy "CTL";
     3.6  time_use_thy "mesontest2";
     3.7 +time_use_thy "Arith_Examples";
     3.8  time_use_thy "PresburgerEx";
     3.9  time_use_thy "Reflected_Presburger";
    3.10  time_use_thy "BT";