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 *})