author webertj Sat, 02 Jun 2007 20:14:38 +0200 changeset 23208 4d8a0976fa1c parent 23207 769f7762f531 child 23209 098a23702aba
extended
```--- a/src/HOL/ex/Arith_Examples.thy	Sat Jun 02 19:10:04 2007 +0200
+++ b/src/HOL/ex/Arith_Examples.thy	Sat Jun 02 20:14:38 2007 +0200
@@ -52,6 +52,12 @@
lemma "min (i::int) j <= max i j"
by (tactic {* fast_arith_tac 1 *})

+lemma "min (i::nat) j + max i j = i + j"
+  by (tactic {* fast_arith_tac 1 *})
+
+lemma "min (i::int) j + max i j = i + j"
+  by (tactic {* fast_arith_tac 1 *})
+
lemma "(i::nat) < j ==> min i j < max i j"
by (tactic {* fast_arith_tac 1 *})

@@ -142,6 +148,18 @@
lemma "(x::nat) < y & y < z ==> x < z"
by (tactic {* simple_arith_tac 1 *})

+text {* This example involves no arithmetic at all, but is solved by
+  preprocessing (i.e. NNF normalization) alone. *}
+
+lemma "(P::bool) = Q ==> Q = P"
+  by (tactic {* simple_arith_tac 1 *})
+
+lemma "[| P = (x = 0); (~P) = (y = 0) |] ==> min (x::nat) y = 0"
+  by (tactic {* simple_arith_tac 1 *})
+
+lemma "[| P = (x = 0); (~P) = (y = 0) |] ==> max (x::nat) y = x + y"
+  by (tactic {* simple_arith_tac 1 *})
+
lemma "[| (x::nat) ~= y; a + 2 = b; a < y; y < b; a < x; x < b |] ==> False"
by (tactic {* fast_arith_tac 1 *})

@@ -184,7 +202,8 @@
oops

lemma "2 * (x::nat) ~= 1"
-(* FIXME: this is beyond the scope of the decision procedure at the moment? *)
+(* FIXME: this is beyond the scope of the decision procedure at the moment, *)
+(*        because its negation is satisfiable in the rationals?             *)
(* by (tactic {* fast_arith_tac 1 *}) *)
oops
```