src/HOL/Integ/Bin.ML
author paulson
Tue, 13 Jul 1999 10:43:31 +0200
changeset 6989 dd3e8bd86cc6
parent 6973 52f70b76a8b5
child 6997 1833bdd83ebf
permissions -rw-r--r--
new theorem zmult_eq_0_iff
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2224
4fc4b465be5b New material from Norbert Voelker for efficient binary comparisons
paulson
parents: 1894
diff changeset
     1
(*  Title:      HOL/Integ/Bin.ML
4fc4b465be5b New material from Norbert Voelker for efficient binary comparisons
paulson
parents: 1894
diff changeset
     2
    Authors:    Lawrence C Paulson, Cambridge University Computer Laboratory
4fc4b465be5b New material from Norbert Voelker for efficient binary comparisons
paulson
parents: 1894
diff changeset
     3
                David Spelt, University of Twente 
6060
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
     4
                Tobias Nipkow, Technical University Munich
1632
39e146ac224c Binary integers and their numeric syntax
paulson
parents:
diff changeset
     5
    Copyright   1994  University of Cambridge
6060
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
     6
    Copyright   1996  University of Twente
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
     7
    Copyright   1999  TU Munich
1632
39e146ac224c Binary integers and their numeric syntax
paulson
parents:
diff changeset
     8
6060
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
     9
Arithmetic on binary integers;
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
    10
decision procedure for linear arithmetic.
1632
39e146ac224c Binary integers and their numeric syntax
paulson
parents:
diff changeset
    11
*)
39e146ac224c Binary integers and their numeric syntax
paulson
parents:
diff changeset
    12
39e146ac224c Binary integers and their numeric syntax
paulson
parents:
diff changeset
    13
(** extra rules for bin_succ, bin_pred, bin_add, bin_mult **)
39e146ac224c Binary integers and their numeric syntax
paulson
parents:
diff changeset
    14
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
    15
qed_goal "NCons_Pls_0" thy
5512
4327eec06849 much renaming and tidying
paulson
parents: 5510
diff changeset
    16
    "NCons Pls False = Pls"
2224
4fc4b465be5b New material from Norbert Voelker for efficient binary comparisons
paulson
parents: 1894
diff changeset
    17
 (fn _ => [(Simp_tac 1)]);
1632
39e146ac224c Binary integers and their numeric syntax
paulson
parents:
diff changeset
    18
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
    19
qed_goal "NCons_Pls_1" thy
5512
4327eec06849 much renaming and tidying
paulson
parents: 5510
diff changeset
    20
    "NCons Pls True = Pls BIT True"
2224
4fc4b465be5b New material from Norbert Voelker for efficient binary comparisons
paulson
parents: 1894
diff changeset
    21
 (fn _ => [(Simp_tac 1)]);
1632
39e146ac224c Binary integers and their numeric syntax
paulson
parents:
diff changeset
    22
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
    23
qed_goal "NCons_Min_0" thy
5512
4327eec06849 much renaming and tidying
paulson
parents: 5510
diff changeset
    24
    "NCons Min False = Min BIT False"
2224
4fc4b465be5b New material from Norbert Voelker for efficient binary comparisons
paulson
parents: 1894
diff changeset
    25
 (fn _ => [(Simp_tac 1)]);
1632
39e146ac224c Binary integers and their numeric syntax
paulson
parents:
diff changeset
    26
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
    27
qed_goal "NCons_Min_1" thy
5512
4327eec06849 much renaming and tidying
paulson
parents: 5510
diff changeset
    28
    "NCons Min True = Min"
2224
4fc4b465be5b New material from Norbert Voelker for efficient binary comparisons
paulson
parents: 1894
diff changeset
    29
 (fn _ => [(Simp_tac 1)]);
1632
39e146ac224c Binary integers and their numeric syntax
paulson
parents:
diff changeset
    30
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
    31
qed_goal "bin_succ_1" thy
5512
4327eec06849 much renaming and tidying
paulson
parents: 5510
diff changeset
    32
    "bin_succ(w BIT True) = (bin_succ w) BIT False"
2224
4fc4b465be5b New material from Norbert Voelker for efficient binary comparisons
paulson
parents: 1894
diff changeset
    33
 (fn _ => [(Simp_tac 1)]);
1632
39e146ac224c Binary integers and their numeric syntax
paulson
parents:
diff changeset
    34
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
    35
qed_goal "bin_succ_0" thy
5512
4327eec06849 much renaming and tidying
paulson
parents: 5510
diff changeset
    36
    "bin_succ(w BIT False) =  NCons w True"
2224
4fc4b465be5b New material from Norbert Voelker for efficient binary comparisons
paulson
parents: 1894
diff changeset
    37
 (fn _ => [(Simp_tac 1)]);
1632
39e146ac224c Binary integers and their numeric syntax
paulson
parents:
diff changeset
    38
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
    39
qed_goal "bin_pred_1" thy
5512
4327eec06849 much renaming and tidying
paulson
parents: 5510
diff changeset
    40
    "bin_pred(w BIT True) = NCons w False"
2224
4fc4b465be5b New material from Norbert Voelker for efficient binary comparisons
paulson
parents: 1894
diff changeset
    41
 (fn _ => [(Simp_tac 1)]);
1632
39e146ac224c Binary integers and their numeric syntax
paulson
parents:
diff changeset
    42
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
    43
qed_goal "bin_pred_0" thy
5512
4327eec06849 much renaming and tidying
paulson
parents: 5510
diff changeset
    44
    "bin_pred(w BIT False) = (bin_pred w) BIT True"
2224
4fc4b465be5b New material from Norbert Voelker for efficient binary comparisons
paulson
parents: 1894
diff changeset
    45
 (fn _ => [(Simp_tac 1)]);
1632
39e146ac224c Binary integers and their numeric syntax
paulson
parents:
diff changeset
    46
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
    47
qed_goal "bin_minus_1" thy
5512
4327eec06849 much renaming and tidying
paulson
parents: 5510
diff changeset
    48
    "bin_minus(w BIT True) = bin_pred (NCons (bin_minus w) False)"
2224
4fc4b465be5b New material from Norbert Voelker for efficient binary comparisons
paulson
parents: 1894
diff changeset
    49
 (fn _ => [(Simp_tac 1)]);
1632
39e146ac224c Binary integers and their numeric syntax
paulson
parents:
diff changeset
    50
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
    51
qed_goal "bin_minus_0" thy
5512
4327eec06849 much renaming and tidying
paulson
parents: 5510
diff changeset
    52
    "bin_minus(w BIT False) = (bin_minus w) BIT False"
2224
4fc4b465be5b New material from Norbert Voelker for efficient binary comparisons
paulson
parents: 1894
diff changeset
    53
 (fn _ => [(Simp_tac 1)]);
1632
39e146ac224c Binary integers and their numeric syntax
paulson
parents:
diff changeset
    54
5491
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
    55
1632
39e146ac224c Binary integers and their numeric syntax
paulson
parents:
diff changeset
    56
(*** bin_add: binary addition ***)
39e146ac224c Binary integers and their numeric syntax
paulson
parents:
diff changeset
    57
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
    58
qed_goal "bin_add_BIT_11" thy
5512
4327eec06849 much renaming and tidying
paulson
parents: 5510
diff changeset
    59
    "bin_add (v BIT True) (w BIT True) = \
4327eec06849 much renaming and tidying
paulson
parents: 5510
diff changeset
    60
\    NCons (bin_add v (bin_succ w)) False"
2224
4fc4b465be5b New material from Norbert Voelker for efficient binary comparisons
paulson
parents: 1894
diff changeset
    61
 (fn _ => [(Simp_tac 1)]);
1632
39e146ac224c Binary integers and their numeric syntax
paulson
parents:
diff changeset
    62
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
    63
qed_goal "bin_add_BIT_10" thy
5512
4327eec06849 much renaming and tidying
paulson
parents: 5510
diff changeset
    64
    "bin_add (v BIT True) (w BIT False) = NCons (bin_add v w) True"
2224
4fc4b465be5b New material from Norbert Voelker for efficient binary comparisons
paulson
parents: 1894
diff changeset
    65
 (fn _ => [(Simp_tac 1)]);
1632
39e146ac224c Binary integers and their numeric syntax
paulson
parents:
diff changeset
    66
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
    67
qed_goal "bin_add_BIT_0" thy
5512
4327eec06849 much renaming and tidying
paulson
parents: 5510
diff changeset
    68
    "bin_add (v BIT False) (w BIT y) = NCons (bin_add v w) y"
5491
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
    69
 (fn _ => [Auto_tac]);
1632
39e146ac224c Binary integers and their numeric syntax
paulson
parents:
diff changeset
    70
5551
ed5e19bc7e32 renamed some axioms; some new theorems
paulson
parents: 5540
diff changeset
    71
Goal "bin_add w Pls = w";
ed5e19bc7e32 renamed some axioms; some new theorems
paulson
parents: 5540
diff changeset
    72
by (induct_tac "w" 1);
ed5e19bc7e32 renamed some axioms; some new theorems
paulson
parents: 5540
diff changeset
    73
by Auto_tac;
ed5e19bc7e32 renamed some axioms; some new theorems
paulson
parents: 5540
diff changeset
    74
qed "bin_add_Pls_right";
1632
39e146ac224c Binary integers and their numeric syntax
paulson
parents:
diff changeset
    75
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
    76
qed_goal "bin_add_BIT_Min" thy
5512
4327eec06849 much renaming and tidying
paulson
parents: 5510
diff changeset
    77
    "bin_add (v BIT x) Min = bin_pred (v BIT x)"
2224
4fc4b465be5b New material from Norbert Voelker for efficient binary comparisons
paulson
parents: 1894
diff changeset
    78
 (fn _ => [(Simp_tac 1)]);
1632
39e146ac224c Binary integers and their numeric syntax
paulson
parents:
diff changeset
    79
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
    80
qed_goal "bin_add_BIT_BIT" thy
5512
4327eec06849 much renaming and tidying
paulson
parents: 5510
diff changeset
    81
    "bin_add (v BIT x) (w BIT y) = \
4327eec06849 much renaming and tidying
paulson
parents: 5510
diff changeset
    82
\    NCons(bin_add v (if x & y then (bin_succ w) else w)) (x~= y)"
2224
4fc4b465be5b New material from Norbert Voelker for efficient binary comparisons
paulson
parents: 1894
diff changeset
    83
 (fn _ => [(Simp_tac 1)]);
1632
39e146ac224c Binary integers and their numeric syntax
paulson
parents:
diff changeset
    84
39e146ac224c Binary integers and their numeric syntax
paulson
parents:
diff changeset
    85
6036
1512f4b7d2e8 fixed comments
paulson
parents: 5779
diff changeset
    86
(*** bin_mult: binary multiplication ***)
1632
39e146ac224c Binary integers and their numeric syntax
paulson
parents:
diff changeset
    87
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
    88
qed_goal "bin_mult_1" thy
5512
4327eec06849 much renaming and tidying
paulson
parents: 5510
diff changeset
    89
    "bin_mult (v BIT True) w = bin_add (NCons (bin_mult v w) False) w"
2224
4fc4b465be5b New material from Norbert Voelker for efficient binary comparisons
paulson
parents: 1894
diff changeset
    90
 (fn _ => [(Simp_tac 1)]);
1632
39e146ac224c Binary integers and their numeric syntax
paulson
parents:
diff changeset
    91
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
    92
qed_goal "bin_mult_0" thy
5512
4327eec06849 much renaming and tidying
paulson
parents: 5510
diff changeset
    93
    "bin_mult (v BIT False) w = NCons (bin_mult v w) False"
2224
4fc4b465be5b New material from Norbert Voelker for efficient binary comparisons
paulson
parents: 1894
diff changeset
    94
 (fn _ => [(Simp_tac 1)]);
1632
39e146ac224c Binary integers and their numeric syntax
paulson
parents:
diff changeset
    95
39e146ac224c Binary integers and their numeric syntax
paulson
parents:
diff changeset
    96
39e146ac224c Binary integers and their numeric syntax
paulson
parents:
diff changeset
    97
(**** The carry/borrow functions, bin_succ and bin_pred ****)
39e146ac224c Binary integers and their numeric syntax
paulson
parents:
diff changeset
    98
39e146ac224c Binary integers and their numeric syntax
paulson
parents:
diff changeset
    99
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   100
(**** number_of ****)
1632
39e146ac224c Binary integers and their numeric syntax
paulson
parents:
diff changeset
   101
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   102
qed_goal "number_of_NCons" thy
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   103
    "number_of(NCons w b) = (number_of(w BIT b)::int)"
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5069
diff changeset
   104
 (fn _ =>[(induct_tac "w" 1),
5510
ad120f7c52ad improved (but still flawed) treatment of binary arithmetic
paulson
parents: 5491
diff changeset
   105
          (ALLGOALS Asm_simp_tac) ]);
1632
39e146ac224c Binary integers and their numeric syntax
paulson
parents:
diff changeset
   106
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   107
Addsimps [number_of_NCons];
1632
39e146ac224c Binary integers and their numeric syntax
paulson
parents:
diff changeset
   108
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   109
qed_goal "number_of_succ" thy
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   110
    "number_of(bin_succ w) = int 1 + number_of w"
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   111
 (fn _ =>[induct_tac "w" 1,
5510
ad120f7c52ad improved (but still flawed) treatment of binary arithmetic
paulson
parents: 5491
diff changeset
   112
          (ALLGOALS(asm_simp_tac (simpset() addsimps zadd_ac))) ]);
5491
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   113
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   114
qed_goal "number_of_pred" thy
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   115
    "number_of(bin_pred w) = - (int 1) + number_of w"
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   116
 (fn _ =>[induct_tac "w" 1,
5510
ad120f7c52ad improved (but still flawed) treatment of binary arithmetic
paulson
parents: 5491
diff changeset
   117
          (ALLGOALS(asm_simp_tac (simpset() addsimps zadd_ac))) ]);
1632
39e146ac224c Binary integers and their numeric syntax
paulson
parents:
diff changeset
   118
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   119
Goal "number_of(bin_minus w) = (- (number_of w)::int)";
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   120
by (induct_tac "w" 1);
5491
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   121
by (Simp_tac 1);
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   122
by (Simp_tac 1);
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   123
by (asm_simp_tac (simpset()
5551
ed5e19bc7e32 renamed some axioms; some new theorems
paulson
parents: 5540
diff changeset
   124
		  delsimps [bin_pred_Pls, bin_pred_Min, bin_pred_BIT]
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   125
		  addsimps [number_of_succ,number_of_pred,
5491
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   126
			    zadd_assoc]) 1);
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   127
qed "number_of_minus";
1632
39e146ac224c Binary integers and their numeric syntax
paulson
parents:
diff changeset
   128
39e146ac224c Binary integers and their numeric syntax
paulson
parents:
diff changeset
   129
 
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   130
val bin_add_simps = [bin_add_BIT_BIT, number_of_succ, number_of_pred];
1632
39e146ac224c Binary integers and their numeric syntax
paulson
parents:
diff changeset
   131
6036
1512f4b7d2e8 fixed comments
paulson
parents: 5779
diff changeset
   132
(*This proof is complicated by the mutual recursion*)
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   133
Goal "! w. number_of(bin_add v w) = (number_of v + number_of w::int)";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5069
diff changeset
   134
by (induct_tac "v" 1);
4686
74a12e86b20b Removed `addsplits [expand_if]'
nipkow
parents: 4641
diff changeset
   135
by (simp_tac (simpset() addsimps bin_add_simps) 1);
74a12e86b20b Removed `addsplits [expand_if]'
nipkow
parents: 4641
diff changeset
   136
by (simp_tac (simpset() addsimps bin_add_simps) 1);
1632
39e146ac224c Binary integers and their numeric syntax
paulson
parents:
diff changeset
   137
by (rtac allI 1);
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5069
diff changeset
   138
by (induct_tac "w" 1);
5540
0f16c3b66ab4 much renaming and reorganization
paulson
parents: 5512
diff changeset
   139
by (ALLGOALS (asm_simp_tac (simpset() addsimps bin_add_simps @ zadd_ac)));
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   140
qed_spec_mp "number_of_add";
1632
39e146ac224c Binary integers and their numeric syntax
paulson
parents:
diff changeset
   141
5779
5c74f003a68e Explicit (and improved) simprules for binary arithmetic.
paulson
parents: 5747
diff changeset
   142
5c74f003a68e Explicit (and improved) simprules for binary arithmetic.
paulson
parents: 5747
diff changeset
   143
(*Subtraction*)
5c74f003a68e Explicit (and improved) simprules for binary arithmetic.
paulson
parents: 5747
diff changeset
   144
Goalw [zdiff_def]
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   145
     "number_of v - number_of w = (number_of(bin_add v (bin_minus w))::int)";
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   146
by (simp_tac (simpset() addsimps [number_of_add, number_of_minus]) 1);
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   147
qed "diff_number_of_eq";
5779
5c74f003a68e Explicit (and improved) simprules for binary arithmetic.
paulson
parents: 5747
diff changeset
   148
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   149
val bin_mult_simps = [zmult_zminus, number_of_minus, number_of_add];
1632
39e146ac224c Binary integers and their numeric syntax
paulson
parents:
diff changeset
   150
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   151
Goal "number_of(bin_mult v w) = (number_of v * number_of w::int)";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5069
diff changeset
   152
by (induct_tac "v" 1);
4686
74a12e86b20b Removed `addsplits [expand_if]'
nipkow
parents: 4641
diff changeset
   153
by (simp_tac (simpset() addsimps bin_mult_simps) 1);
74a12e86b20b Removed `addsplits [expand_if]'
nipkow
parents: 4641
diff changeset
   154
by (simp_tac (simpset() addsimps bin_mult_simps) 1);
5491
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   155
by (asm_simp_tac
5540
0f16c3b66ab4 much renaming and reorganization
paulson
parents: 5512
diff changeset
   156
    (simpset() addsimps bin_mult_simps @ [zadd_zmult_distrib] @ zadd_ac) 1);
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   157
qed "number_of_mult";
5491
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   158
1632
39e146ac224c Binary integers and their numeric syntax
paulson
parents:
diff changeset
   159
6941
f52c70a449fb products of signs as equivalences
paulson
parents: 6917
diff changeset
   160
(*The correctness of shifting.  But it doesn't seem to give a measurable
f52c70a449fb products of signs as equivalences
paulson
parents: 6917
diff changeset
   161
  speed-up.*)
f52c70a449fb products of signs as equivalences
paulson
parents: 6917
diff changeset
   162
Goal "(#2::int) * number_of w = number_of (w BIT False)";
f52c70a449fb products of signs as equivalences
paulson
parents: 6917
diff changeset
   163
by (induct_tac "w" 1);
f52c70a449fb products of signs as equivalences
paulson
parents: 6917
diff changeset
   164
by (ALLGOALS (asm_simp_tac
f52c70a449fb products of signs as equivalences
paulson
parents: 6917
diff changeset
   165
    (simpset() addsimps bin_mult_simps @ [zadd_zmult_distrib] @ zadd_ac)));
f52c70a449fb products of signs as equivalences
paulson
parents: 6917
diff changeset
   166
qed "double_number_of_BIT";
f52c70a449fb products of signs as equivalences
paulson
parents: 6917
diff changeset
   167
f52c70a449fb products of signs as equivalences
paulson
parents: 6917
diff changeset
   168
5491
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   169
(** Simplification rules with integer constants **)
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   170
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   171
Goal "#0 + z = (z::int)";
5491
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   172
by (Simp_tac 1);
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   173
qed "zadd_0";
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   174
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   175
Goal "z + #0 = (z::int)";
5491
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   176
by (Simp_tac 1);
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   177
qed "zadd_0_right";
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   178
5592
64697e426048 better handling of literals
paulson
parents: 5582
diff changeset
   179
Addsimps [zadd_0, zadd_0_right];
64697e426048 better handling of literals
paulson
parents: 5582
diff changeset
   180
64697e426048 better handling of literals
paulson
parents: 5582
diff changeset
   181
64697e426048 better handling of literals
paulson
parents: 5582
diff changeset
   182
(** Converting simple cases of (int n) to numerals **)
5491
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   183
5592
64697e426048 better handling of literals
paulson
parents: 5582
diff changeset
   184
(*int 0 = #0 *)
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   185
bind_thm ("int_0", number_of_Pls RS sym);
5491
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   186
5592
64697e426048 better handling of literals
paulson
parents: 5582
diff changeset
   187
Goal "int (Suc n) = #1 + int n";
64697e426048 better handling of literals
paulson
parents: 5582
diff changeset
   188
by (simp_tac (simpset() addsimps [zadd_int]) 1);
64697e426048 better handling of literals
paulson
parents: 5582
diff changeset
   189
qed "int_Suc";
5510
ad120f7c52ad improved (but still flawed) treatment of binary arithmetic
paulson
parents: 5491
diff changeset
   190
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   191
Goal "- (#0) = (#0::int)";
5491
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   192
by (Simp_tac 1);
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   193
qed "zminus_0";
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   194
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   195
Addsimps [zminus_0];
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   196
5582
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   197
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   198
Goal "(#0::int) - x = -x";
5582
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   199
by (simp_tac (simpset() addsimps [zdiff_def]) 1);
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   200
qed "zdiff0";
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   201
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   202
Goal "x - (#0::int) = x";
5582
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   203
by (simp_tac (simpset() addsimps [zdiff_def]) 1);
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   204
qed "zdiff0_right";
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   205
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   206
Goal "x - x = (#0::int)";
5582
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   207
by (simp_tac (simpset() addsimps [zdiff_def]) 1);
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   208
qed "zdiff_self";
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   209
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   210
Addsimps [zdiff0, zdiff0_right, zdiff_self];
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   211
6917
eba301caceea Introduction of integer division algorithm
paulson
parents: 6910
diff changeset
   212
eba301caceea Introduction of integer division algorithm
paulson
parents: 6910
diff changeset
   213
(** Special simplification, for constants only **)
6838
941c4f70db91 rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents: 6716
diff changeset
   214
6917
eba301caceea Introduction of integer division algorithm
paulson
parents: 6910
diff changeset
   215
fun inst x t = read_instantiate_sg (sign_of Bin.thy) [(x,t)];
eba301caceea Introduction of integer division algorithm
paulson
parents: 6910
diff changeset
   216
eba301caceea Introduction of integer division algorithm
paulson
parents: 6910
diff changeset
   217
(*Distributive laws*)
eba301caceea Introduction of integer division algorithm
paulson
parents: 6910
diff changeset
   218
Addsimps (map (inst "w" "number_of ?v")
6838
941c4f70db91 rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents: 6716
diff changeset
   219
	  [zadd_zmult_distrib, zadd_zmult_distrib2,
941c4f70db91 rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents: 6716
diff changeset
   220
	   zdiff_zmult_distrib, zdiff_zmult_distrib2]);
941c4f70db91 rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents: 6716
diff changeset
   221
6917
eba301caceea Introduction of integer division algorithm
paulson
parents: 6910
diff changeset
   222
Addsimps (map (inst "x" "number_of ?v") 
eba301caceea Introduction of integer division algorithm
paulson
parents: 6910
diff changeset
   223
	  [zless_zminus, zle_zminus, equation_zminus]);
eba301caceea Introduction of integer division algorithm
paulson
parents: 6910
diff changeset
   224
Addsimps (map (inst "y" "number_of ?v") 
eba301caceea Introduction of integer division algorithm
paulson
parents: 6910
diff changeset
   225
	  [zminus_zless, zminus_zle, zminus_equation]);
eba301caceea Introduction of integer division algorithm
paulson
parents: 6910
diff changeset
   226
eba301caceea Introduction of integer division algorithm
paulson
parents: 6910
diff changeset
   227
6838
941c4f70db91 rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents: 6716
diff changeset
   228
(** Special-case simplification for small constants **)
941c4f70db91 rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents: 6716
diff changeset
   229
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   230
Goal "#0 * z = (#0::int)";
5491
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   231
by (Simp_tac 1);
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   232
qed "zmult_0";
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   233
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   234
Goal "z * #0 = (#0::int)";
6838
941c4f70db91 rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents: 6716
diff changeset
   235
by (Simp_tac 1);
941c4f70db91 rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents: 6716
diff changeset
   236
qed "zmult_0_right";
941c4f70db91 rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents: 6716
diff changeset
   237
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   238
Goal "#1 * z = (z::int)";
5491
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   239
by (Simp_tac 1);
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   240
qed "zmult_1";
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   241
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   242
Goal "z * #1 = (z::int)";
6838
941c4f70db91 rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents: 6716
diff changeset
   243
by (Simp_tac 1);
941c4f70db91 rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents: 6716
diff changeset
   244
qed "zmult_1_right";
941c4f70db91 rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents: 6716
diff changeset
   245
6917
eba301caceea Introduction of integer division algorithm
paulson
parents: 6910
diff changeset
   246
Goal "#-1 * z = -(z::int)";
eba301caceea Introduction of integer division algorithm
paulson
parents: 6910
diff changeset
   247
by (simp_tac (simpset() addsimps zcompare_rls@[zmult_zminus]) 1);
eba301caceea Introduction of integer division algorithm
paulson
parents: 6910
diff changeset
   248
qed "zmult_minus1";
eba301caceea Introduction of integer division algorithm
paulson
parents: 6910
diff changeset
   249
eba301caceea Introduction of integer division algorithm
paulson
parents: 6910
diff changeset
   250
Goal "z * #-1 = -(z::int)";
eba301caceea Introduction of integer division algorithm
paulson
parents: 6910
diff changeset
   251
by (simp_tac (simpset() addsimps zcompare_rls@[zmult_zminus_right]) 1);
eba301caceea Introduction of integer division algorithm
paulson
parents: 6910
diff changeset
   252
qed "zmult_minus1_right";
eba301caceea Introduction of integer division algorithm
paulson
parents: 6910
diff changeset
   253
eba301caceea Introduction of integer division algorithm
paulson
parents: 6910
diff changeset
   254
Addsimps [zmult_0, zmult_0_right, 
eba301caceea Introduction of integer division algorithm
paulson
parents: 6910
diff changeset
   255
	  zmult_1, zmult_1_right,
eba301caceea Introduction of integer division algorithm
paulson
parents: 6910
diff changeset
   256
	  zmult_minus1, zmult_minus1_right];
eba301caceea Introduction of integer division algorithm
paulson
parents: 6910
diff changeset
   257
eba301caceea Introduction of integer division algorithm
paulson
parents: 6910
diff changeset
   258
(*For specialist use: NOT as default simprules*)
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   259
Goal "#2 * z = (z+z::int)";
5491
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   260
by (simp_tac (simpset() addsimps [zadd_zmult_distrib]) 1);
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   261
qed "zmult_2";
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   262
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   263
Goal "z * #2 = (z+z::int)";
5491
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   264
by (simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 1);
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   265
qed "zmult_2_right";
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   266
6917
eba301caceea Introduction of integer division algorithm
paulson
parents: 6910
diff changeset
   267
eba301caceea Introduction of integer division algorithm
paulson
parents: 6910
diff changeset
   268
(** Inequality reasoning **)
5491
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   269
6989
dd3e8bd86cc6 new theorem zmult_eq_0_iff
paulson
parents: 6973
diff changeset
   270
Goal "(m*n = (#0::int)) = (m = #0 | n = #0)";
dd3e8bd86cc6 new theorem zmult_eq_0_iff
paulson
parents: 6973
diff changeset
   271
by (stac (int_0 RS sym) 1 THEN rtac zmult_eq_int0_iff 1);
dd3e8bd86cc6 new theorem zmult_eq_0_iff
paulson
parents: 6973
diff changeset
   272
qed "zmult_eq_0_iff";
dd3e8bd86cc6 new theorem zmult_eq_0_iff
paulson
parents: 6973
diff changeset
   273
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   274
Goal "(w < z + (#1::int)) = (w<z | w=z)";
5592
64697e426048 better handling of literals
paulson
parents: 5582
diff changeset
   275
by (simp_tac (simpset() addsimps [zless_add_int_Suc_eq]) 1);
5491
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   276
qed "zless_add1_eq";
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   277
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   278
Goal "(w + (#1::int) <= z) = (w<z)";
5592
64697e426048 better handling of literals
paulson
parents: 5582
diff changeset
   279
by (simp_tac (simpset() addsimps [add_int_Suc_zle_eq]) 1);
5491
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   280
qed "add1_zle_eq";
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   281
Addsimps [add1_zle_eq];
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   282
5540
0f16c3b66ab4 much renaming and reorganization
paulson
parents: 5512
diff changeset
   283
Goal "neg x = (x < #0)";
6917
eba301caceea Introduction of integer division algorithm
paulson
parents: 6910
diff changeset
   284
by (simp_tac (simpset() addsimps [neg_eq_less_int0]) 1); 
5540
0f16c3b66ab4 much renaming and reorganization
paulson
parents: 5512
diff changeset
   285
qed "neg_eq_less_0"; 
5510
ad120f7c52ad improved (but still flawed) treatment of binary arithmetic
paulson
parents: 5491
diff changeset
   286
6989
dd3e8bd86cc6 new theorem zmult_eq_0_iff
paulson
parents: 6973
diff changeset
   287
Goal "(~neg x) = (#0 <= x)";
6917
eba301caceea Introduction of integer division algorithm
paulson
parents: 6910
diff changeset
   288
by (simp_tac (simpset() addsimps [not_neg_eq_ge_int0]) 1); 
5540
0f16c3b66ab4 much renaming and reorganization
paulson
parents: 5512
diff changeset
   289
qed "not_neg_eq_ge_0"; 
5510
ad120f7c52ad improved (but still flawed) treatment of binary arithmetic
paulson
parents: 5491
diff changeset
   290
5582
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   291
Goal "#0 <= int m";
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   292
by (Simp_tac 1);
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   293
qed "zero_zle_int";
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   294
AddIffs [zero_zle_int];
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   295
5510
ad120f7c52ad improved (but still flawed) treatment of binary arithmetic
paulson
parents: 5491
diff changeset
   296
5747
387b5bf9326a Now users will never see (int 0)
paulson
parents: 5592
diff changeset
   297
(** Needed because (int 0) rewrites to #0.
387b5bf9326a Now users will never see (int 0)
paulson
parents: 5592
diff changeset
   298
    Can these be generalized without evaluating large numbers?**)
387b5bf9326a Now users will never see (int 0)
paulson
parents: 5592
diff changeset
   299
387b5bf9326a Now users will never see (int 0)
paulson
parents: 5592
diff changeset
   300
Goal "~ (int k < #0)";
387b5bf9326a Now users will never see (int 0)
paulson
parents: 5592
diff changeset
   301
by (Simp_tac 1);
387b5bf9326a Now users will never see (int 0)
paulson
parents: 5592
diff changeset
   302
qed "int_less_0_conv";
387b5bf9326a Now users will never see (int 0)
paulson
parents: 5592
diff changeset
   303
387b5bf9326a Now users will never see (int 0)
paulson
parents: 5592
diff changeset
   304
Goal "(int k <= #0) = (k=0)";
387b5bf9326a Now users will never see (int 0)
paulson
parents: 5592
diff changeset
   305
by (Simp_tac 1);
387b5bf9326a Now users will never see (int 0)
paulson
parents: 5592
diff changeset
   306
qed "int_le_0_conv";
387b5bf9326a Now users will never see (int 0)
paulson
parents: 5592
diff changeset
   307
387b5bf9326a Now users will never see (int 0)
paulson
parents: 5592
diff changeset
   308
Goal "(int k = #0) = (k=0)";
387b5bf9326a Now users will never see (int 0)
paulson
parents: 5592
diff changeset
   309
by (Simp_tac 1);
387b5bf9326a Now users will never see (int 0)
paulson
parents: 5592
diff changeset
   310
qed "int_eq_0_conv";
387b5bf9326a Now users will never see (int 0)
paulson
parents: 5592
diff changeset
   311
387b5bf9326a Now users will never see (int 0)
paulson
parents: 5592
diff changeset
   312
Goal "(#0 = int k) = (k=0)";
387b5bf9326a Now users will never see (int 0)
paulson
parents: 5592
diff changeset
   313
by Auto_tac;
387b5bf9326a Now users will never see (int 0)
paulson
parents: 5592
diff changeset
   314
qed "int_eq_0_conv'";
387b5bf9326a Now users will never see (int 0)
paulson
parents: 5592
diff changeset
   315
387b5bf9326a Now users will never see (int 0)
paulson
parents: 5592
diff changeset
   316
Addsimps [int_less_0_conv, int_le_0_conv, int_eq_0_conv, int_eq_0_conv'];
387b5bf9326a Now users will never see (int 0)
paulson
parents: 5592
diff changeset
   317
387b5bf9326a Now users will never see (int 0)
paulson
parents: 5592
diff changeset
   318
5491
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   319
(** Simplification rules for comparison of binary numbers (Norbert Voelker) **)
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   320
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   321
(** Equals (=) **)
1632
39e146ac224c Binary integers and their numeric syntax
paulson
parents:
diff changeset
   322
5491
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   323
Goalw [iszero_def]
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   324
  "((number_of x::int) = number_of y) = iszero(number_of (bin_add x (bin_minus y)))"; 
5491
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   325
by (simp_tac (simpset() addsimps
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   326
              (zcompare_rls @ [number_of_add, number_of_minus])) 1); 
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   327
qed "eq_number_of_eq"; 
5491
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   328
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   329
Goalw [iszero_def] "iszero ((number_of Pls)::int)"; 
5491
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   330
by (Simp_tac 1); 
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   331
qed "iszero_number_of_Pls"; 
5491
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   332
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   333
Goalw [iszero_def] "~ iszero ((number_of Min)::int)"; 
5491
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   334
by (Simp_tac 1);
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   335
qed "nonzero_number_of_Min"; 
5491
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   336
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   337
Goalw [iszero_def]
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   338
     "iszero (number_of (w BIT x)) = (~x & iszero (number_of w::int))"; 
5491
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   339
by (Simp_tac 1);
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   340
by (int_case_tac "number_of w" 1); 
5491
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   341
by (ALLGOALS (asm_simp_tac 
5540
0f16c3b66ab4 much renaming and reorganization
paulson
parents: 5512
diff changeset
   342
	      (simpset() addsimps zcompare_rls @ 
0f16c3b66ab4 much renaming and reorganization
paulson
parents: 5512
diff changeset
   343
				  [zminus_zadd_distrib RS sym, 
5582
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   344
				   zadd_int]))); 
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   345
qed "iszero_number_of_BIT"; 
5491
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   346
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   347
Goal "iszero (number_of (w BIT False)) = iszero (number_of w::int)"; 
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   348
by (simp_tac (HOL_ss addsimps [iszero_number_of_BIT]) 1); 
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   349
qed "iszero_number_of_0"; 
5779
5c74f003a68e Explicit (and improved) simprules for binary arithmetic.
paulson
parents: 5747
diff changeset
   350
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   351
Goal "~ iszero (number_of (w BIT True)::int)"; 
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   352
by (simp_tac (HOL_ss addsimps [iszero_number_of_BIT]) 1); 
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   353
qed "iszero_number_of_1"; 
5779
5c74f003a68e Explicit (and improved) simprules for binary arithmetic.
paulson
parents: 5747
diff changeset
   354
5c74f003a68e Explicit (and improved) simprules for binary arithmetic.
paulson
parents: 5747
diff changeset
   355
5491
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   356
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   357
(** Less-than (<) **)
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   358
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   359
Goalw [zless_def,zdiff_def] 
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   360
    "(number_of x::int) < number_of y \
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   361
\    = neg (number_of (bin_add x (bin_minus y)))";
5491
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   362
by (simp_tac (simpset() addsimps bin_mult_simps) 1);
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   363
qed "less_number_of_eq_neg"; 
5491
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   364
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   365
Goal "~ neg (number_of Pls)"; 
5491
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   366
by (Simp_tac 1); 
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   367
qed "not_neg_number_of_Pls"; 
5491
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   368
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   369
Goal "neg (number_of Min)"; 
5491
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   370
by (Simp_tac 1);
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   371
qed "neg_number_of_Min"; 
5491
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   372
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   373
Goal "neg (number_of (w BIT x)) = neg (number_of w)"; 
5491
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   374
by (Asm_simp_tac 1); 
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   375
by (int_case_tac "number_of w" 1); 
5491
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   376
by (ALLGOALS (asm_simp_tac 
6917
eba301caceea Introduction of integer division algorithm
paulson
parents: 6910
diff changeset
   377
	      (simpset() addsimps [zadd_int, neg_eq_less_int0, 
5540
0f16c3b66ab4 much renaming and reorganization
paulson
parents: 5512
diff changeset
   378
				   symmetric zdiff_def] @ zcompare_rls))); 
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   379
qed "neg_number_of_BIT"; 
5491
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   380
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   381
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   382
(** Less-than-or-equals (<=) **)
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   383
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   384
Goal "(number_of x <= (number_of y::int)) = (~ number_of y < (number_of x::int))";
5491
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   385
by (simp_tac (simpset() addsimps [zle_def]) 1);
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   386
qed "le_number_of_eq_not_less"; 
5491
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   387
5540
0f16c3b66ab4 much renaming and reorganization
paulson
parents: 5512
diff changeset
   388
(*Delete the original rewrites, with their clumsy conditional expressions*)
5551
ed5e19bc7e32 renamed some axioms; some new theorems
paulson
parents: 5540
diff changeset
   389
Delsimps [bin_succ_BIT, bin_pred_BIT, bin_minus_BIT, 
ed5e19bc7e32 renamed some axioms; some new theorems
paulson
parents: 5540
diff changeset
   390
          NCons_Pls, NCons_Min, bin_add_BIT, bin_mult_BIT];
5491
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   391
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   392
(*Hide the binary representation of integer constants*)
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   393
Delsimps [number_of_Pls, number_of_Min, number_of_BIT];
5491
22f8331cdf47 revised treatment of integers
paulson
parents: 5224
diff changeset
   394
5779
5c74f003a68e Explicit (and improved) simprules for binary arithmetic.
paulson
parents: 5747
diff changeset
   395
(*simplification of arithmetic operations on integer constants*)
5c74f003a68e Explicit (and improved) simprules for binary arithmetic.
paulson
parents: 5747
diff changeset
   396
val bin_arith_extra_simps =
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   397
    [number_of_add RS sym,
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   398
     number_of_minus RS sym,
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   399
     number_of_mult RS sym,
5779
5c74f003a68e Explicit (and improved) simprules for binary arithmetic.
paulson
parents: 5747
diff changeset
   400
     bin_succ_1, bin_succ_0, 
5c74f003a68e Explicit (and improved) simprules for binary arithmetic.
paulson
parents: 5747
diff changeset
   401
     bin_pred_1, bin_pred_0, 
5c74f003a68e Explicit (and improved) simprules for binary arithmetic.
paulson
parents: 5747
diff changeset
   402
     bin_minus_1, bin_minus_0,  
5c74f003a68e Explicit (and improved) simprules for binary arithmetic.
paulson
parents: 5747
diff changeset
   403
     bin_add_Pls_right, bin_add_BIT_Min,
5c74f003a68e Explicit (and improved) simprules for binary arithmetic.
paulson
parents: 5747
diff changeset
   404
     bin_add_BIT_0, bin_add_BIT_10, bin_add_BIT_11,
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   405
     diff_number_of_eq, 
5779
5c74f003a68e Explicit (and improved) simprules for binary arithmetic.
paulson
parents: 5747
diff changeset
   406
     bin_mult_1, bin_mult_0, 
5c74f003a68e Explicit (and improved) simprules for binary arithmetic.
paulson
parents: 5747
diff changeset
   407
     NCons_Pls_0, NCons_Pls_1, 
5c74f003a68e Explicit (and improved) simprules for binary arithmetic.
paulson
parents: 5747
diff changeset
   408
     NCons_Min_0, NCons_Min_1, NCons_BIT];
2224
4fc4b465be5b New material from Norbert Voelker for efficient binary comparisons
paulson
parents: 1894
diff changeset
   409
5779
5c74f003a68e Explicit (and improved) simprules for binary arithmetic.
paulson
parents: 5747
diff changeset
   410
(*For making a minimal simpset, one must include these default simprules
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   411
  of thy.  Also include simp_thms, or at least (~False)=True*)
5779
5c74f003a68e Explicit (and improved) simprules for binary arithmetic.
paulson
parents: 5747
diff changeset
   412
val bin_arith_simps =
5c74f003a68e Explicit (and improved) simprules for binary arithmetic.
paulson
parents: 5747
diff changeset
   413
    [bin_pred_Pls, bin_pred_Min,
5c74f003a68e Explicit (and improved) simprules for binary arithmetic.
paulson
parents: 5747
diff changeset
   414
     bin_succ_Pls, bin_succ_Min,
5c74f003a68e Explicit (and improved) simprules for binary arithmetic.
paulson
parents: 5747
diff changeset
   415
     bin_add_Pls, bin_add_Min,
5c74f003a68e Explicit (and improved) simprules for binary arithmetic.
paulson
parents: 5747
diff changeset
   416
     bin_minus_Pls, bin_minus_Min,
5c74f003a68e Explicit (and improved) simprules for binary arithmetic.
paulson
parents: 5747
diff changeset
   417
     bin_mult_Pls, bin_mult_Min] @ bin_arith_extra_simps;
2224
4fc4b465be5b New material from Norbert Voelker for efficient binary comparisons
paulson
parents: 1894
diff changeset
   418
5779
5c74f003a68e Explicit (and improved) simprules for binary arithmetic.
paulson
parents: 5747
diff changeset
   419
(*Simplification of relational operations*)
5c74f003a68e Explicit (and improved) simprules for binary arithmetic.
paulson
parents: 5747
diff changeset
   420
val bin_rel_simps =
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   421
    [eq_number_of_eq, iszero_number_of_Pls, nonzero_number_of_Min,
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   422
     iszero_number_of_0, iszero_number_of_1,
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   423
     less_number_of_eq_neg,
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   424
     not_neg_number_of_Pls, neg_number_of_Min, neg_number_of_BIT,
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   425
     le_number_of_eq_not_less];
2224
4fc4b465be5b New material from Norbert Voelker for efficient binary comparisons
paulson
parents: 1894
diff changeset
   426
5779
5c74f003a68e Explicit (and improved) simprules for binary arithmetic.
paulson
parents: 5747
diff changeset
   427
Addsimps bin_arith_extra_simps;
5c74f003a68e Explicit (and improved) simprules for binary arithmetic.
paulson
parents: 5747
diff changeset
   428
Addsimps bin_rel_simps;
5510
ad120f7c52ad improved (but still flawed) treatment of binary arithmetic
paulson
parents: 5491
diff changeset
   429
6060
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   430
(*---------------------------------------------------------------------------*)
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   431
(* Linear arithmetic                                                         *)
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   432
(*---------------------------------------------------------------------------*)
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   433
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   434
(*
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   435
Instantiation of the generic linear arithmetic package for int.
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   436
FIXME: multiplication with constants (eg #2 * i) does not work yet.
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   437
Solution: the cancellation simprocs in Int_Cancel should be able to deal with
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   438
it (eg simplify #3 * i <= 2 * i to i <= #0) or `add_rules' below should
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   439
include rules for turning multiplication with constants into addition.
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   440
(The latter option is very inefficient!)
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   441
*)
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   442
6128
2acc5d36610c More arith refinements.
nipkow
parents: 6109
diff changeset
   443
structure Int_LA_Data(*: LIN_ARITH_DATA*) =
6060
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   444
struct
6101
dde00dc06f0d Restructured Arithmatic
nipkow
parents: 6079
diff changeset
   445
6128
2acc5d36610c More arith refinements.
nipkow
parents: 6109
diff changeset
   446
val lessD = Nat_LA_Data.lessD @ [add1_zle_eq RS iffD2];
6060
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   447
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   448
fun add_atom(t,m,(p,i)) = (case assoc(p,t) of None => ((t,m)::p,i)
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   449
                           | Some n => (overwrite(p,(t,n+m:int)), i));
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   450
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   451
(* Turn term into list of summand * multiplicity plus a constant *)
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   452
fun poly(Const("op +",_) $ s $ t, m, pi) = poly(s,m,poly(t,m,pi))
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   453
  | poly(Const("op -",_) $ s $ t, m, pi) = poly(s,m,poly(t,~1*m,pi))
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   454
  | poly(Const("uminus",_) $ t, m, pi) =   poly(t,~1*m,pi)
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   455
  | poly(all as Const("op *",_) $ (Const("Numeral.number_of",_)$c) $ t, m, pi) =
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   456
      (poly(t,m*NumeralSyntax.dest_bin c,pi) handle Match => add_atom(all,m,pi))
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   457
  | poly(all as Const("Numeral.number_of",_)$t,m,(p,i)) =
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   458
     ((p,i + m*NumeralSyntax.dest_bin t) handle Match => add_atom(all,m,(p,i)))
6060
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   459
  | poly x  = add_atom x;
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   460
6128
2acc5d36610c More arith refinements.
nipkow
parents: 6109
diff changeset
   461
fun decomp2(rel,lhs,rhs) =
6060
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   462
  let val (p,i) = poly(lhs,1,([],0)) and (q,j) = poly(rhs,1,([],0))
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   463
  in case rel of
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   464
       "op <"  => Some(p,i,"<",q,j)
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   465
     | "op <=" => Some(p,i,"<=",q,j)
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   466
     | "op ="  => Some(p,i,"=",q,j)
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   467
     | _       => None
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   468
  end;
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   469
6128
2acc5d36610c More arith refinements.
nipkow
parents: 6109
diff changeset
   470
val intT = Type("IntDef.int",[]);
2acc5d36610c More arith refinements.
nipkow
parents: 6109
diff changeset
   471
fun iib T = T = ([intT,intT] ---> HOLogic.boolT);
6060
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   472
6128
2acc5d36610c More arith refinements.
nipkow
parents: 6109
diff changeset
   473
fun decomp1(T,xxx) =
2acc5d36610c More arith refinements.
nipkow
parents: 6109
diff changeset
   474
  if iib T then decomp2 xxx else Nat_LA_Data.decomp1(T,xxx);
2acc5d36610c More arith refinements.
nipkow
parents: 6109
diff changeset
   475
2acc5d36610c More arith refinements.
nipkow
parents: 6109
diff changeset
   476
fun decomp(_$(Const(rel,T)$lhs$rhs)) = decomp1(T,(rel,lhs,rhs))
6060
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   477
  | decomp(_$(Const("Not",_)$(Const(rel,T)$lhs$rhs))) =
6128
2acc5d36610c More arith refinements.
nipkow
parents: 6109
diff changeset
   478
      Nat_LA_Data.negate(decomp1(T,(rel,lhs,rhs)))
6060
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   479
  | decomp _ = None
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   480
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   481
(* reduce contradictory <= to False *)
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   482
val add_rules = simp_thms@bin_arith_simps@bin_rel_simps@[int_0];
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   483
6128
2acc5d36610c More arith refinements.
nipkow
parents: 6109
diff changeset
   484
val cancel_sums_ss = Nat_LA_Data.cancel_sums_ss addsimps add_rules
6060
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   485
          addsimprocs [Int_Cancel.sum_conv, Int_Cancel.rel_conv];
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   486
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   487
val simp = simplify cancel_sums_ss;
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   488
6128
2acc5d36610c More arith refinements.
nipkow
parents: 6109
diff changeset
   489
val add_mono_thms = Nat_LA_Data.add_mono_thms @
2acc5d36610c More arith refinements.
nipkow
parents: 6109
diff changeset
   490
  map (fn s => prove_goal Int.thy s
2acc5d36610c More arith refinements.
nipkow
parents: 6109
diff changeset
   491
                 (fn prems => [cut_facts_tac prems 1,
2acc5d36610c More arith refinements.
nipkow
parents: 6109
diff changeset
   492
                      asm_simp_tac (simpset() addsimps [zadd_zle_mono]) 1]))
2acc5d36610c More arith refinements.
nipkow
parents: 6109
diff changeset
   493
    ["(i <= j) & (k <= l) ==> i + k <= j + (l::int)",
2acc5d36610c More arith refinements.
nipkow
parents: 6109
diff changeset
   494
     "(i  = j) & (k <= l) ==> i + k <= j + (l::int)",
2acc5d36610c More arith refinements.
nipkow
parents: 6109
diff changeset
   495
     "(i <= j) & (k  = l) ==> i + k <= j + (l::int)",
2acc5d36610c More arith refinements.
nipkow
parents: 6109
diff changeset
   496
     "(i  = j) & (k  = l) ==> i + k  = j + (l::int)"
2acc5d36610c More arith refinements.
nipkow
parents: 6109
diff changeset
   497
    ];
6060
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   498
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   499
end;
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   500
6128
2acc5d36610c More arith refinements.
nipkow
parents: 6109
diff changeset
   501
(* Update parameters of arithmetic prover *)
2acc5d36610c More arith refinements.
nipkow
parents: 6109
diff changeset
   502
LA_Data_Ref.add_mono_thms := Int_LA_Data.add_mono_thms;
2acc5d36610c More arith refinements.
nipkow
parents: 6109
diff changeset
   503
LA_Data_Ref.lessD :=         Int_LA_Data.lessD;
2acc5d36610c More arith refinements.
nipkow
parents: 6109
diff changeset
   504
LA_Data_Ref.decomp :=        Int_LA_Data.decomp;
2acc5d36610c More arith refinements.
nipkow
parents: 6109
diff changeset
   505
LA_Data_Ref.simp :=          Int_LA_Data.simp;
2acc5d36610c More arith refinements.
nipkow
parents: 6109
diff changeset
   506
6060
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   507
6128
2acc5d36610c More arith refinements.
nipkow
parents: 6109
diff changeset
   508
val int_arith_simproc_pats =
6394
3d9fd50fcc43 Theory.sign_of;
wenzelm
parents: 6301
diff changeset
   509
  map (fn s => Thm.read_cterm (Theory.sign_of Int.thy) (s, HOLogic.boolT))
6128
2acc5d36610c More arith refinements.
nipkow
parents: 6109
diff changeset
   510
      ["(m::int) < n","(m::int) <= n", "(m::int) = n"];
6060
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   511
6128
2acc5d36610c More arith refinements.
nipkow
parents: 6109
diff changeset
   512
val fast_int_arith_simproc = mk_simproc "fast_int_arith" int_arith_simproc_pats
2acc5d36610c More arith refinements.
nipkow
parents: 6109
diff changeset
   513
                                        Fast_Arith.lin_arith_prover;
2acc5d36610c More arith refinements.
nipkow
parents: 6109
diff changeset
   514
2acc5d36610c More arith refinements.
nipkow
parents: 6109
diff changeset
   515
Addsimprocs [fast_int_arith_simproc];
6060
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   516
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   517
(* FIXME: K true should be replaced by a sensible test to speed things up
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   518
   in case there are lots of irrelevant terms involved.
6157
29942d3a1818 arith_tac for min/max
nipkow
parents: 6128
diff changeset
   519
6128
2acc5d36610c More arith refinements.
nipkow
parents: 6109
diff changeset
   520
val arith_tac =
2acc5d36610c More arith refinements.
nipkow
parents: 6109
diff changeset
   521
  refute_tac (K true) (REPEAT o split_tac[nat_diff_split])
2acc5d36610c More arith refinements.
nipkow
parents: 6109
diff changeset
   522
             ((REPEAT_DETERM o etac linorder_neqE) THEN' fast_arith_tac);
6157
29942d3a1818 arith_tac for min/max
nipkow
parents: 6128
diff changeset
   523
*)
6060
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   524
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   525
(* Some test data
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   526
Goal "!!a::int. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d";
6301
08245f5a436d expandshort
paulson
parents: 6157
diff changeset
   527
by (fast_arith_tac 1);
6060
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   528
Goal "!!a::int. [| a < b; c < d |] ==> a-d+ #2 <= b+(-c)";
6301
08245f5a436d expandshort
paulson
parents: 6157
diff changeset
   529
by (fast_arith_tac 1);
6060
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   530
Goal "!!a::int. [| a < b; c < d |] ==> a+c+ #1 < b+d";
6301
08245f5a436d expandshort
paulson
parents: 6157
diff changeset
   531
by (fast_arith_tac 1);
6060
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   532
Goal "!!a::int. [| a <= b; b+b <= c |] ==> a+a <= c";
6301
08245f5a436d expandshort
paulson
parents: 6157
diff changeset
   533
by (fast_arith_tac 1);
6060
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   534
Goal "!!a::int. [| a+b <= i+j; a<=b; i<=j |] \
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   535
\     ==> a+a <= j+j";
6301
08245f5a436d expandshort
paulson
parents: 6157
diff changeset
   536
by (fast_arith_tac 1);
6060
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   537
Goal "!!a::int. [| a+b < i+j; a<b; i<j |] \
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   538
\     ==> a+a - - #-1 < j+j - #3";
6301
08245f5a436d expandshort
paulson
parents: 6157
diff changeset
   539
by (fast_arith_tac 1);
6060
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   540
Goal "!!a::int. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k";
6301
08245f5a436d expandshort
paulson
parents: 6157
diff changeset
   541
by (arith_tac 1);
6060
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   542
Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   543
\     ==> a <= l";
6301
08245f5a436d expandshort
paulson
parents: 6157
diff changeset
   544
by (fast_arith_tac 1);
6060
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   545
Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   546
\     ==> a+a+a+a <= l+l+l+l";
6301
08245f5a436d expandshort
paulson
parents: 6157
diff changeset
   547
by (fast_arith_tac 1);
6060
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   548
Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   549
\     ==> a+a+a+a+a <= l+l+l+l+i";
6301
08245f5a436d expandshort
paulson
parents: 6157
diff changeset
   550
by (fast_arith_tac 1);
6060
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   551
Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   552
\     ==> a+a+a+a+a+a <= l+l+l+l+i+l";
6301
08245f5a436d expandshort
paulson
parents: 6157
diff changeset
   553
by (fast_arith_tac 1);
6060
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   554
*)
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   555
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   556
(*---------------------------------------------------------------------------*)
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   557
(* End of linear arithmetic                                                  *)
d30d1dd2082d Instantiated lin.arith.
nipkow
parents: 6036
diff changeset
   558
(*---------------------------------------------------------------------------*)
5510
ad120f7c52ad improved (but still flawed) treatment of binary arithmetic
paulson
parents: 5491
diff changeset
   559
5592
64697e426048 better handling of literals
paulson
parents: 5582
diff changeset
   560
(** Simplification of arithmetic when nested to the right **)
64697e426048 better handling of literals
paulson
parents: 5582
diff changeset
   561
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   562
Goal "number_of v + (number_of w + z) = (number_of(bin_add v w) + z::int)";
5592
64697e426048 better handling of literals
paulson
parents: 5582
diff changeset
   563
by (simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   564
qed "add_number_of_left";
5592
64697e426048 better handling of literals
paulson
parents: 5582
diff changeset
   565
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   566
Goal "number_of v * (number_of w * z) = (number_of(bin_mult v w) * z::int)";
5592
64697e426048 better handling of literals
paulson
parents: 5582
diff changeset
   567
by (simp_tac (simpset() addsimps [zmult_assoc RS sym]) 1);
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   568
qed "mult_number_of_left";
5592
64697e426048 better handling of literals
paulson
parents: 5582
diff changeset
   569
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   570
Addsimps [add_number_of_left, mult_number_of_left];
5592
64697e426048 better handling of literals
paulson
parents: 5582
diff changeset
   571
5510
ad120f7c52ad improved (but still flawed) treatment of binary arithmetic
paulson
parents: 5491
diff changeset
   572
(** Simplification of inequalities involving numerical constants **)
ad120f7c52ad improved (but still flawed) treatment of binary arithmetic
paulson
parents: 5491
diff changeset
   573
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   574
Goal "(w <= z + (#1::int)) = (w<=z | w = z + (#1::int))";
6301
08245f5a436d expandshort
paulson
parents: 6157
diff changeset
   575
by (arith_tac 1);
5510
ad120f7c52ad improved (but still flawed) treatment of binary arithmetic
paulson
parents: 5491
diff changeset
   576
qed "zle_add1_eq";
ad120f7c52ad improved (but still flawed) treatment of binary arithmetic
paulson
parents: 5491
diff changeset
   577
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   578
Goal "(w <= z - (#1::int)) = (w<(z::int))";
6301
08245f5a436d expandshort
paulson
parents: 6157
diff changeset
   579
by (arith_tac 1);
5510
ad120f7c52ad improved (but still flawed) treatment of binary arithmetic
paulson
parents: 5491
diff changeset
   580
qed "zle_diff1_eq";
ad120f7c52ad improved (but still flawed) treatment of binary arithmetic
paulson
parents: 5491
diff changeset
   581
Addsimps [zle_diff1_eq];
ad120f7c52ad improved (but still flawed) treatment of binary arithmetic
paulson
parents: 5491
diff changeset
   582
ad120f7c52ad improved (but still flawed) treatment of binary arithmetic
paulson
parents: 5491
diff changeset
   583
(*2nd premise can be proved automatically if v is a literal*)
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   584
Goal "[| w <= z; #0 <= v |] ==> w <= z + (v::int)";
6301
08245f5a436d expandshort
paulson
parents: 6157
diff changeset
   585
by (fast_arith_tac 1);
5510
ad120f7c52ad improved (but still flawed) treatment of binary arithmetic
paulson
parents: 5491
diff changeset
   586
qed "zle_imp_zle_zadd";
ad120f7c52ad improved (but still flawed) treatment of binary arithmetic
paulson
parents: 5491
diff changeset
   587
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   588
Goal "w <= z ==> w <= z + (#1::int)";
6301
08245f5a436d expandshort
paulson
parents: 6157
diff changeset
   589
by (fast_arith_tac 1);
5510
ad120f7c52ad improved (but still flawed) treatment of binary arithmetic
paulson
parents: 5491
diff changeset
   590
qed "zle_imp_zle_zadd1";
ad120f7c52ad improved (but still flawed) treatment of binary arithmetic
paulson
parents: 5491
diff changeset
   591
ad120f7c52ad improved (but still flawed) treatment of binary arithmetic
paulson
parents: 5491
diff changeset
   592
(*2nd premise can be proved automatically if v is a literal*)
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   593
Goal "[| w < z; #0 <= v |] ==> w < z + (v::int)";
6301
08245f5a436d expandshort
paulson
parents: 6157
diff changeset
   594
by (fast_arith_tac 1);
5510
ad120f7c52ad improved (but still flawed) treatment of binary arithmetic
paulson
parents: 5491
diff changeset
   595
qed "zless_imp_zless_zadd";
ad120f7c52ad improved (but still flawed) treatment of binary arithmetic
paulson
parents: 5491
diff changeset
   596
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   597
Goal "w < z ==> w < z + (#1::int)";
6301
08245f5a436d expandshort
paulson
parents: 6157
diff changeset
   598
by (fast_arith_tac 1);
5510
ad120f7c52ad improved (but still flawed) treatment of binary arithmetic
paulson
parents: 5491
diff changeset
   599
qed "zless_imp_zless_zadd1";
ad120f7c52ad improved (but still flawed) treatment of binary arithmetic
paulson
parents: 5491
diff changeset
   600
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   601
Goal "(w < z + #1) = (w<=(z::int))";
6301
08245f5a436d expandshort
paulson
parents: 6157
diff changeset
   602
by (arith_tac 1);
5510
ad120f7c52ad improved (but still flawed) treatment of binary arithmetic
paulson
parents: 5491
diff changeset
   603
qed "zle_add1_eq_le";
ad120f7c52ad improved (but still flawed) treatment of binary arithmetic
paulson
parents: 5491
diff changeset
   604
Addsimps [zle_add1_eq_le];
ad120f7c52ad improved (but still flawed) treatment of binary arithmetic
paulson
parents: 5491
diff changeset
   605
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   606
Goal "(z = z + w) = (w = (#0::int))";
6301
08245f5a436d expandshort
paulson
parents: 6157
diff changeset
   607
by (arith_tac 1);
5510
ad120f7c52ad improved (but still flawed) treatment of binary arithmetic
paulson
parents: 5491
diff changeset
   608
qed "zadd_left_cancel0";
ad120f7c52ad improved (but still flawed) treatment of binary arithmetic
paulson
parents: 5491
diff changeset
   609
Addsimps [zadd_left_cancel0];
ad120f7c52ad improved (but still flawed) treatment of binary arithmetic
paulson
parents: 5491
diff changeset
   610
ad120f7c52ad improved (but still flawed) treatment of binary arithmetic
paulson
parents: 5491
diff changeset
   611
(*LOOPS as a simprule!*)
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   612
Goal "[| w + v < z; #0 <= v |] ==> w < (z::int)";
6301
08245f5a436d expandshort
paulson
parents: 6157
diff changeset
   613
by (fast_arith_tac 1);
5510
ad120f7c52ad improved (but still flawed) treatment of binary arithmetic
paulson
parents: 5491
diff changeset
   614
qed "zless_zadd_imp_zless";
ad120f7c52ad improved (but still flawed) treatment of binary arithmetic
paulson
parents: 5491
diff changeset
   615
5540
0f16c3b66ab4 much renaming and reorganization
paulson
parents: 5512
diff changeset
   616
(*LOOPS as a simprule!  Analogous to Suc_lessD*)
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   617
Goal "w + #1 < z ==> w < (z::int)";
6301
08245f5a436d expandshort
paulson
parents: 6157
diff changeset
   618
by (fast_arith_tac 1);
5510
ad120f7c52ad improved (but still flawed) treatment of binary arithmetic
paulson
parents: 5491
diff changeset
   619
qed "zless_zadd1_imp_zless";
ad120f7c52ad improved (but still flawed) treatment of binary arithmetic
paulson
parents: 5491
diff changeset
   620
6910
7c3503ae3d78 use generic numeral encoding and syntax;
wenzelm
parents: 6838
diff changeset
   621
Goal "w + #-1 = w - (#1::int)";
5582
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   622
by (Simp_tac 1);
5551
ed5e19bc7e32 renamed some axioms; some new theorems
paulson
parents: 5540
diff changeset
   623
qed "zplus_minus1_conv";
5510
ad120f7c52ad improved (but still flawed) treatment of binary arithmetic
paulson
parents: 5491
diff changeset
   624
5551
ed5e19bc7e32 renamed some axioms; some new theorems
paulson
parents: 5540
diff changeset
   625
5562
02261e6880d1 Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents: 5551
diff changeset
   626
(*** nat ***)
5551
ed5e19bc7e32 renamed some axioms; some new theorems
paulson
parents: 5540
diff changeset
   627
5582
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   628
Goal "#0 <= z ==> int (nat z) = z"; 
5551
ed5e19bc7e32 renamed some axioms; some new theorems
paulson
parents: 5540
diff changeset
   629
by (asm_full_simp_tac
5562
02261e6880d1 Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents: 5551
diff changeset
   630
    (simpset() addsimps [neg_eq_less_0, zle_def, not_neg_nat]) 1); 
02261e6880d1 Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents: 5551
diff changeset
   631
qed "nat_0_le"; 
5551
ed5e19bc7e32 renamed some axioms; some new theorems
paulson
parents: 5540
diff changeset
   632
5562
02261e6880d1 Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents: 5551
diff changeset
   633
Goal "z < #0 ==> nat z = 0"; 
5551
ed5e19bc7e32 renamed some axioms; some new theorems
paulson
parents: 5540
diff changeset
   634
by (asm_full_simp_tac
5562
02261e6880d1 Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents: 5551
diff changeset
   635
    (simpset() addsimps [neg_eq_less_0, zle_def, neg_nat]) 1); 
02261e6880d1 Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents: 5551
diff changeset
   636
qed "nat_less_0"; 
5551
ed5e19bc7e32 renamed some axioms; some new theorems
paulson
parents: 5540
diff changeset
   637
5562
02261e6880d1 Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents: 5551
diff changeset
   638
Addsimps [nat_0_le, nat_less_0];
5551
ed5e19bc7e32 renamed some axioms; some new theorems
paulson
parents: 5540
diff changeset
   639
5582
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   640
Goal "#0 <= w ==> (nat w = m) = (w = int m)";
5551
ed5e19bc7e32 renamed some axioms; some new theorems
paulson
parents: 5540
diff changeset
   641
by Auto_tac;
5562
02261e6880d1 Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents: 5551
diff changeset
   642
qed "nat_eq_iff";
5551
ed5e19bc7e32 renamed some axioms; some new theorems
paulson
parents: 5540
diff changeset
   643
5582
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   644
Goal "#0 <= w ==> (nat w < m) = (w < int m)";
5551
ed5e19bc7e32 renamed some axioms; some new theorems
paulson
parents: 5540
diff changeset
   645
by (rtac iffI 1);
ed5e19bc7e32 renamed some axioms; some new theorems
paulson
parents: 5540
diff changeset
   646
by (asm_full_simp_tac 
5582
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   647
    (simpset() delsimps [zless_int] addsimps [zless_int RS sym]) 2);
5562
02261e6880d1 Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents: 5551
diff changeset
   648
by (etac (nat_0_le RS subst) 1);
5551
ed5e19bc7e32 renamed some axioms; some new theorems
paulson
parents: 5540
diff changeset
   649
by (Simp_tac 1);
5562
02261e6880d1 Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents: 5551
diff changeset
   650
qed "nat_less_iff";
5551
ed5e19bc7e32 renamed some axioms; some new theorems
paulson
parents: 5540
diff changeset
   651
5747
387b5bf9326a Now users will never see (int 0)
paulson
parents: 5592
diff changeset
   652
6716
87c750df8888 Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents: 6394
diff changeset
   653
(*Users don't want to see (int 0), int(Suc 0) or w + - z*)
87c750df8888 Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents: 6394
diff changeset
   654
Addsimps [int_0, int_Suc, symmetric zdiff_def];
87c750df8888 Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents: 6394
diff changeset
   655
87c750df8888 Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents: 6394
diff changeset
   656
Goal "nat #0 = 0";
87c750df8888 Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents: 6394
diff changeset
   657
by (simp_tac (simpset() addsimps [nat_eq_iff]) 1);
87c750df8888 Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents: 6394
diff changeset
   658
qed "nat_0";
87c750df8888 Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents: 6394
diff changeset
   659
87c750df8888 Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents: 6394
diff changeset
   660
Goal "nat #1 = 1";
87c750df8888 Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents: 6394
diff changeset
   661
by (simp_tac (simpset() addsimps [nat_eq_iff]) 1);
87c750df8888 Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents: 6394
diff changeset
   662
qed "nat_1";
87c750df8888 Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents: 6394
diff changeset
   663
87c750df8888 Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents: 6394
diff changeset
   664
Goal "nat #2 = 2";
87c750df8888 Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents: 6394
diff changeset
   665
by (simp_tac (simpset() addsimps [nat_eq_iff]) 1);
87c750df8888 Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents: 6394
diff changeset
   666
qed "nat_2";
87c750df8888 Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents: 6394
diff changeset
   667
87c750df8888 Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents: 6394
diff changeset
   668
Goal "nat #3 = Suc 2";
87c750df8888 Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents: 6394
diff changeset
   669
by (simp_tac (simpset() addsimps [nat_eq_iff]) 1);
87c750df8888 Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents: 6394
diff changeset
   670
qed "nat_3";
87c750df8888 Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents: 6394
diff changeset
   671
87c750df8888 Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents: 6394
diff changeset
   672
Goal "nat #4 = Suc (Suc 2)";
87c750df8888 Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents: 6394
diff changeset
   673
by (simp_tac (simpset() addsimps [nat_eq_iff]) 1);
87c750df8888 Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents: 6394
diff changeset
   674
qed "nat_4";
87c750df8888 Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents: 6394
diff changeset
   675
87c750df8888 Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents: 6394
diff changeset
   676
Goal "nat #5 = Suc (Suc (Suc 2))";
87c750df8888 Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents: 6394
diff changeset
   677
by (simp_tac (simpset() addsimps [nat_eq_iff]) 1);
87c750df8888 Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents: 6394
diff changeset
   678
qed "nat_5";
87c750df8888 Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents: 6394
diff changeset
   679
87c750df8888 Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents: 6394
diff changeset
   680
Goal "nat #6 = Suc (Suc (Suc (Suc 2)))";
87c750df8888 Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents: 6394
diff changeset
   681
by (simp_tac (simpset() addsimps [nat_eq_iff]) 1);
87c750df8888 Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents: 6394
diff changeset
   682
qed "nat_6";
87c750df8888 Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents: 6394
diff changeset
   683
87c750df8888 Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents: 6394
diff changeset
   684
Goal "nat #7 = Suc (Suc (Suc (Suc (Suc 2))))";
87c750df8888 Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents: 6394
diff changeset
   685
by (simp_tac (simpset() addsimps [nat_eq_iff]) 1);
87c750df8888 Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents: 6394
diff changeset
   686
qed "nat_7";
87c750df8888 Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents: 6394
diff changeset
   687
87c750df8888 Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents: 6394
diff changeset
   688
Goal "nat #8 = Suc (Suc (Suc (Suc (Suc (Suc 2)))))";
87c750df8888 Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents: 6394
diff changeset
   689
by (simp_tac (simpset() addsimps [nat_eq_iff]) 1);
87c750df8888 Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents: 6394
diff changeset
   690
qed "nat_8";
87c750df8888 Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents: 6394
diff changeset
   691
87c750df8888 Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents: 6394
diff changeset
   692
Goal "nat #9 = Suc (Suc (Suc (Suc (Suc (Suc (Suc 2))))))";
87c750df8888 Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents: 6394
diff changeset
   693
by (simp_tac (simpset() addsimps [nat_eq_iff]) 1);
87c750df8888 Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents: 6394
diff changeset
   694
qed "nat_9";
87c750df8888 Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents: 6394
diff changeset
   695
87c750df8888 Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents: 6394
diff changeset
   696
(*Users also don't want to see (nat 0), (nat 1), ...*)
87c750df8888 Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents: 6394
diff changeset
   697
Addsimps [nat_0, nat_1, nat_2, nat_3, nat_4, 
87c750df8888 Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents: 6394
diff changeset
   698
	  nat_5, nat_6, nat_7, nat_8, nat_9];
87c750df8888 Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents: 6394
diff changeset
   699
5747
387b5bf9326a Now users will never see (int 0)
paulson
parents: 5592
diff changeset
   700
5562
02261e6880d1 Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents: 5551
diff changeset
   701
Goal "#0 <= w ==> (nat w < nat z) = (w<z)";
5551
ed5e19bc7e32 renamed some axioms; some new theorems
paulson
parents: 5540
diff changeset
   702
by (case_tac "neg z" 1);
5562
02261e6880d1 Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents: 5551
diff changeset
   703
by (auto_tac (claset(), simpset() addsimps [nat_less_iff]));
5551
ed5e19bc7e32 renamed some axioms; some new theorems
paulson
parents: 5540
diff changeset
   704
by (auto_tac (claset() addIs [zless_trans], 
5747
387b5bf9326a Now users will never see (int 0)
paulson
parents: 5592
diff changeset
   705
	      simpset() addsimps [neg_eq_less_0, zle_def]));
5562
02261e6880d1 Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents: 5551
diff changeset
   706
qed "nat_less_eq_zless";
5747
387b5bf9326a Now users will never see (int 0)
paulson
parents: 5592
diff changeset
   707
6838
941c4f70db91 rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents: 6716
diff changeset
   708
6917
eba301caceea Introduction of integer division algorithm
paulson
parents: 6910
diff changeset
   709
(*Towards canonical simplification*)
6838
941c4f70db91 rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents: 6716
diff changeset
   710
Addsimps zadd_ac;
941c4f70db91 rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents: 6716
diff changeset
   711
Addsimps zmult_ac;
6917
eba301caceea Introduction of integer division algorithm
paulson
parents: 6910
diff changeset
   712
Addsimps [zmult_zminus, zmult_zminus_right];
6941
f52c70a449fb products of signs as equivalences
paulson
parents: 6917
diff changeset
   713
f52c70a449fb products of signs as equivalences
paulson
parents: 6917
diff changeset
   714
f52c70a449fb products of signs as equivalences
paulson
parents: 6917
diff changeset
   715
f52c70a449fb products of signs as equivalences
paulson
parents: 6917
diff changeset
   716
(** Products of signs **)
f52c70a449fb products of signs as equivalences
paulson
parents: 6917
diff changeset
   717
f52c70a449fb products of signs as equivalences
paulson
parents: 6917
diff changeset
   718
Goal "(m::int) < #0 ==> (#0 < m*n) = (n < #0)";
f52c70a449fb products of signs as equivalences
paulson
parents: 6917
diff changeset
   719
by Auto_tac;
f52c70a449fb products of signs as equivalences
paulson
parents: 6917
diff changeset
   720
by (force_tac (claset() addDs [zmult_zless_mono1_neg], simpset()) 2);
f52c70a449fb products of signs as equivalences
paulson
parents: 6917
diff changeset
   721
by (eres_inst_tac [("P", "#0 < m * n")] rev_mp 1);
f52c70a449fb products of signs as equivalences
paulson
parents: 6917
diff changeset
   722
by (simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1);
f52c70a449fb products of signs as equivalences
paulson
parents: 6917
diff changeset
   723
by (force_tac (claset() addDs [zmult_zless_mono1_neg], 
f52c70a449fb products of signs as equivalences
paulson
parents: 6917
diff changeset
   724
	       simpset() addsimps [order_le_less]) 1);
f52c70a449fb products of signs as equivalences
paulson
parents: 6917
diff changeset
   725
qed "neg_imp_zmult_pos_iff";
f52c70a449fb products of signs as equivalences
paulson
parents: 6917
diff changeset
   726
f52c70a449fb products of signs as equivalences
paulson
parents: 6917
diff changeset
   727
Goal "(m::int) < #0 ==> (m*n < #0) = (#0 < n)";
f52c70a449fb products of signs as equivalences
paulson
parents: 6917
diff changeset
   728
by Auto_tac;
f52c70a449fb products of signs as equivalences
paulson
parents: 6917
diff changeset
   729
by (force_tac (claset() addDs [zmult_zless_mono1], simpset()) 2);
f52c70a449fb products of signs as equivalences
paulson
parents: 6917
diff changeset
   730
by (eres_inst_tac [("P", "m * n < #0")] rev_mp 1);
f52c70a449fb products of signs as equivalences
paulson
parents: 6917
diff changeset
   731
by (simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1);
f52c70a449fb products of signs as equivalences
paulson
parents: 6917
diff changeset
   732
by (force_tac (claset() addDs [zmult_zless_mono1_neg], 
f52c70a449fb products of signs as equivalences
paulson
parents: 6917
diff changeset
   733
	       simpset() addsimps [order_le_less]) 1);
f52c70a449fb products of signs as equivalences
paulson
parents: 6917
diff changeset
   734
qed "neg_imp_zmult_neg_iff";
f52c70a449fb products of signs as equivalences
paulson
parents: 6917
diff changeset
   735
f52c70a449fb products of signs as equivalences
paulson
parents: 6917
diff changeset
   736
Goal "#0 < (m::int) ==> (m*n < #0) = (n < #0)";
f52c70a449fb products of signs as equivalences
paulson
parents: 6917
diff changeset
   737
by Auto_tac;
f52c70a449fb products of signs as equivalences
paulson
parents: 6917
diff changeset
   738
by (force_tac (claset() addDs [zmult_zless_mono1_neg], simpset()) 2);
f52c70a449fb products of signs as equivalences
paulson
parents: 6917
diff changeset
   739
by (eres_inst_tac [("P", "m * n < #0")] rev_mp 1);
f52c70a449fb products of signs as equivalences
paulson
parents: 6917
diff changeset
   740
by (simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1);
f52c70a449fb products of signs as equivalences
paulson
parents: 6917
diff changeset
   741
by (force_tac (claset() addDs [zmult_zless_mono1], 
f52c70a449fb products of signs as equivalences
paulson
parents: 6917
diff changeset
   742
	       simpset() addsimps [order_le_less]) 1);
f52c70a449fb products of signs as equivalences
paulson
parents: 6917
diff changeset
   743
qed "pos_imp_zmult_neg_iff";
f52c70a449fb products of signs as equivalences
paulson
parents: 6917
diff changeset
   744
f52c70a449fb products of signs as equivalences
paulson
parents: 6917
diff changeset
   745
Goal "#0 < (m::int) ==> (#0 < m*n) = (#0 < n)";
f52c70a449fb products of signs as equivalences
paulson
parents: 6917
diff changeset
   746
by Auto_tac;
f52c70a449fb products of signs as equivalences
paulson
parents: 6917
diff changeset
   747
by (force_tac (claset() addDs [zmult_zless_mono1], simpset()) 2);
f52c70a449fb products of signs as equivalences
paulson
parents: 6917
diff changeset
   748
by (eres_inst_tac [("P", "#0 < m * n")] rev_mp 1);
f52c70a449fb products of signs as equivalences
paulson
parents: 6917
diff changeset
   749
by (simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1);
f52c70a449fb products of signs as equivalences
paulson
parents: 6917
diff changeset
   750
by (force_tac (claset() addDs [zmult_zless_mono1], 
f52c70a449fb products of signs as equivalences
paulson
parents: 6917
diff changeset
   751
	       simpset() addsimps [order_le_less]) 1);
f52c70a449fb products of signs as equivalences
paulson
parents: 6917
diff changeset
   752
qed "pos_imp_zmult_pos_iff";
6973
52f70b76a8b5 new theorems for the "at most" relation
paulson
parents: 6941
diff changeset
   753
52f70b76a8b5 new theorems for the "at most" relation
paulson
parents: 6941
diff changeset
   754
(** <= versions of the theorems above **)
52f70b76a8b5 new theorems for the "at most" relation
paulson
parents: 6941
diff changeset
   755
52f70b76a8b5 new theorems for the "at most" relation
paulson
parents: 6941
diff changeset
   756
Goal "(m::int) < #0 ==> (m*n <= #0) = (#0 <= n)";
52f70b76a8b5 new theorems for the "at most" relation
paulson
parents: 6941
diff changeset
   757
by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym,
52f70b76a8b5 new theorems for the "at most" relation
paulson
parents: 6941
diff changeset
   758
				      neg_imp_zmult_pos_iff]) 1);
52f70b76a8b5 new theorems for the "at most" relation
paulson
parents: 6941
diff changeset
   759
qed "neg_imp_zmult_nonpos_iff";
52f70b76a8b5 new theorems for the "at most" relation
paulson
parents: 6941
diff changeset
   760
52f70b76a8b5 new theorems for the "at most" relation
paulson
parents: 6941
diff changeset
   761
Goal "(m::int) < #0 ==> (#0 <= m*n) = (n <= #0)";
52f70b76a8b5 new theorems for the "at most" relation
paulson
parents: 6941
diff changeset
   762
by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym,
52f70b76a8b5 new theorems for the "at most" relation
paulson
parents: 6941
diff changeset
   763
				      neg_imp_zmult_neg_iff]) 1);
52f70b76a8b5 new theorems for the "at most" relation
paulson
parents: 6941
diff changeset
   764
qed "neg_imp_zmult_nonneg_iff";
52f70b76a8b5 new theorems for the "at most" relation
paulson
parents: 6941
diff changeset
   765
52f70b76a8b5 new theorems for the "at most" relation
paulson
parents: 6941
diff changeset
   766
Goal "#0 < (m::int) ==> (m*n <= #0) = (n <= #0)";
52f70b76a8b5 new theorems for the "at most" relation
paulson
parents: 6941
diff changeset
   767
by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym,
52f70b76a8b5 new theorems for the "at most" relation
paulson
parents: 6941
diff changeset
   768
				      pos_imp_zmult_pos_iff]) 1);
52f70b76a8b5 new theorems for the "at most" relation
paulson
parents: 6941
diff changeset
   769
qed "pos_imp_zmult_nonpos_iff";
52f70b76a8b5 new theorems for the "at most" relation
paulson
parents: 6941
diff changeset
   770
52f70b76a8b5 new theorems for the "at most" relation
paulson
parents: 6941
diff changeset
   771
Goal "#0 < (m::int) ==> (#0 <= m*n) = (#0 <= n)";
52f70b76a8b5 new theorems for the "at most" relation
paulson
parents: 6941
diff changeset
   772
by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym,
52f70b76a8b5 new theorems for the "at most" relation
paulson
parents: 6941
diff changeset
   773
				      pos_imp_zmult_neg_iff]) 1);
52f70b76a8b5 new theorems for the "at most" relation
paulson
parents: 6941
diff changeset
   774
qed "pos_imp_zmult_nonneg_iff";