src/HOL/ex/Arith_Examples.thy
 changeset 23198 174b5f2ec7c1 parent 23196 fabf2e8a7ba4 child 23208 4d8a0976fa1c
```     1.1 --- a/src/HOL/ex/Arith_Examples.thy	Sat Jun 02 03:15:35 2007 +0200
1.2 +++ b/src/HOL/ex/Arith_Examples.thy	Sat Jun 02 03:17:44 2007 +0200
1.3 @@ -94,15 +94,33 @@
1.4    by (tactic {* fast_arith_tac 1 *})
1.5
1.6  lemma "(i::nat) mod 0 = i"
1.7 -oops
1.8 +  (* FIXME: need to replace 0 by its numeral representation *)
1.9 +  apply (subst nat_numeral_0_eq_0 [symmetric])
1.10 +  by (tactic {* fast_arith_tac 1 *})
1.11 +
1.12 +lemma "(i::nat) mod 1 = 0"
1.13 +  (* FIXME: need to replace 1 by its numeral representation *)
1.14 +  apply (subst nat_numeral_1_eq_1 [symmetric])
1.15 +  by (tactic {* fast_arith_tac 1 *})
1.16
1.17 -lemma "(i::nat) mod (Suc 0) = 0"
1.18 +lemma "(i::nat) mod 42 <= 41"
1.19 +  by (tactic {* fast_arith_tac 1 *})
1.20 +
1.21 +lemma "(i::int) mod 0 = i"
1.22 +  (* FIXME: need to replace 0 by its numeral representation *)
1.23 +  apply (subst numeral_0_eq_0 [symmetric])
1.24 +  by (tactic {* fast_arith_tac 1 *})
1.25 +
1.26 +lemma "(i::int) mod 1 = 0"
1.27 +  (* FIXME: need to replace 1 by its numeral representation *)
1.28 +  apply (subst numeral_1_eq_1 [symmetric])
1.29 +  (* FIXME: arith does not know about iszero *)
1.30 +  apply (tactic {* LA_Data_Ref.pre_tac 1 *})
1.31  oops
1.32
1.33 -lemma "(i::nat) div 0 = 0"
1.34 -oops
1.35 -
1.36 -lemma "(i::nat) mod (number_of (1::int)) = 0"
1.37 +lemma "(i::int) mod 42 <= 41"
1.38 +  (* FIXME: arith does not know about iszero *)
1.39 +  apply (tactic {* LA_Data_Ref.pre_tac 1 *})
1.40  oops
1.41
1.42  section {* Meta-Logic *}
1.43 @@ -115,6 +133,9 @@
1.44
1.45  section {* Various Other Examples *}
1.46
1.47 +lemma "(x < Suc y) = (x <= y)"
1.48 +  by (tactic {* simple_arith_tac 1 *})
1.49 +
1.50  lemma "[| (x::nat) < y; y < z |] ==> x < z"
1.51    by (tactic {* fast_arith_tac 1 *})
1.52
1.53 @@ -148,12 +169,47 @@
1.54  lemma "((a::nat) - (b - (c - (d - e)))) = (a - (b - (c - (d - e))))"
1.55    by (tactic {* fast_arith_tac 1 *})
1.56
1.57 +lemma "(n < m & m < n') | (n < m & m = n') | (n < n' & n' < m) |
1.58 +  (n = n' & n' < m) | (n = m & m < n') |
1.59 +  (n' < m & m < n) | (n' < m & m = n) |
1.60 +  (n' < n & n < m) | (n' = n & n < m) | (n' = m & m < n) |
1.61 +  (m < n & n < n') | (m < n & n' = n) | (m < n' & n' < n) |
1.62 +  (m = n & n < n') | (m = n' & n' < n) |
1.63 +  (n' = m & m = (n::nat))"
1.64 +(* FIXME: this should work in principle, but is extremely slow because     *)
1.65 +(*        preprocessing negates the goal and tries to compute its negation *)
1.66 +(*        normal form, which creates lots of separate cases for this       *)
1.67 +(*        disjunction of conjunctions                                      *)
1.68 +(* by (tactic {* simple_arith_tac 1 *}) *)
1.69 +oops
1.70 +
1.71 +lemma "2 * (x::nat) ~= 1"
1.72 +(* FIXME: this is beyond the scope of the decision procedure at the moment? *)
1.73 +(* by (tactic {* fast_arith_tac 1 *}) *)
1.74 +oops
1.75 +
1.76 +text {* Constants. *}
1.77 +
1.78 +lemma "(0::nat) < 1"
1.79 +  by (tactic {* fast_arith_tac 1 *})
1.80 +
1.81 +lemma "(0::int) < 1"
1.82 +  by (tactic {* fast_arith_tac 1 *})
1.83 +
1.84 +lemma "(47::nat) + 11 < 08 * 15"
1.85 +  by (tactic {* fast_arith_tac 1 *})
1.86 +
1.87 +lemma "(47::int) + 11 < 08 * 15"
1.88 +  by (tactic {* fast_arith_tac 1 *})
1.89 +
1.90  text {* Splitting of inequalities of different type. *}
1.91
1.92  lemma "[| (a::nat) ~= b; (i::int) ~= j; a < 2; b < 2 |] ==>
1.93    a + b <= nat (max (abs i) (abs j))"
1.94    by (tactic {* fast_arith_tac 1 *})
1.95
1.96 +text {* Again, but different order. *}
1.97 +
1.98  lemma "[| (i::int) ~= j; (a::nat) ~= b; a < 2; b < 2 |] ==>
1.99    a + b <= nat (max (abs i) (abs j))"
1.100    by (tactic {* fast_arith_tac 1 *})
```