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