src/HOL/ex/Arith_Examples.thy
 changeset 23208 4d8a0976fa1c parent 23198 174b5f2ec7c1 child 23211 4d56ad10b5e8
```     1.1 --- a/src/HOL/ex/Arith_Examples.thy	Sat Jun 02 19:10:04 2007 +0200
1.2 +++ b/src/HOL/ex/Arith_Examples.thy	Sat Jun 02 20:14:38 2007 +0200
1.3 @@ -52,6 +52,12 @@
1.4  lemma "min (i::int) j <= max i j"
1.5    by (tactic {* fast_arith_tac 1 *})
1.6
1.7 +lemma "min (i::nat) j + max i j = i + j"
1.8 +  by (tactic {* fast_arith_tac 1 *})
1.9 +
1.10 +lemma "min (i::int) j + max i j = i + j"
1.11 +  by (tactic {* fast_arith_tac 1 *})
1.12 +
1.13  lemma "(i::nat) < j ==> min i j < max i j"
1.14    by (tactic {* fast_arith_tac 1 *})
1.15
1.16 @@ -142,6 +148,18 @@
1.17  lemma "(x::nat) < y & y < z ==> x < z"
1.18    by (tactic {* simple_arith_tac 1 *})
1.19
1.20 +text {* This example involves no arithmetic at all, but is solved by
1.21 +  preprocessing (i.e. NNF normalization) alone. *}
1.22 +
1.23 +lemma "(P::bool) = Q ==> Q = P"
1.24 +  by (tactic {* simple_arith_tac 1 *})
1.25 +
1.26 +lemma "[| P = (x = 0); (~P) = (y = 0) |] ==> min (x::nat) y = 0"
1.27 +  by (tactic {* simple_arith_tac 1 *})
1.28 +
1.29 +lemma "[| P = (x = 0); (~P) = (y = 0) |] ==> max (x::nat) y = x + y"
1.30 +  by (tactic {* simple_arith_tac 1 *})
1.31 +
1.32  lemma "[| (x::nat) ~= y; a + 2 = b; a < y; y < b; a < x; x < b |] ==> False"
1.33    by (tactic {* fast_arith_tac 1 *})
1.34
1.35 @@ -184,7 +202,8 @@
1.36  oops
1.37
1.38  lemma "2 * (x::nat) ~= 1"
1.39 -(* FIXME: this is beyond the scope of the decision procedure at the moment? *)
1.40 +(* FIXME: this is beyond the scope of the decision procedure at the moment, *)
1.41 +(*        because its negation is satisfiable in the rationals?             *)
1.42  (* by (tactic {* fast_arith_tac 1 *}) *)
1.43  oops
1.44
```