src/HOL/Tools/nat_arith.ML
author haftmann
Thu, 08 Jul 2010 16:19:24 +0200
changeset 37744 3daaf23b9ab4
parent 35267 8dfd816713c6
child 38715 6513ea67d95d
permissions -rw-r--r--
tuned titles
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
30496
7cdcc9dd95cb vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents: 29302
diff changeset
     1
(* Author: Markus Wenzel, Stefan Berghofer, and Tobias Nipkow
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
     2
30496
7cdcc9dd95cb vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents: 29302
diff changeset
     3
Basic arithmetic for natural numbers.
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
     4
*)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
     5
30496
7cdcc9dd95cb vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents: 29302
diff changeset
     6
signature NAT_ARITH =
26101
a657683e902a tuned structures in arith_data.ML
haftmann
parents: 25484
diff changeset
     7
sig
a657683e902a tuned structures in arith_data.ML
haftmann
parents: 25484
diff changeset
     8
  val mk_sum: term list -> term
a657683e902a tuned structures in arith_data.ML
haftmann
parents: 25484
diff changeset
     9
  val mk_norm_sum: term list -> term
a657683e902a tuned structures in arith_data.ML
haftmann
parents: 25484
diff changeset
    10
  val dest_sum: term -> term list
a657683e902a tuned structures in arith_data.ML
haftmann
parents: 25484
diff changeset
    11
a657683e902a tuned structures in arith_data.ML
haftmann
parents: 25484
diff changeset
    12
  val nat_cancel_sums_add: simproc list
a657683e902a tuned structures in arith_data.ML
haftmann
parents: 25484
diff changeset
    13
  val nat_cancel_sums: simproc list
a657683e902a tuned structures in arith_data.ML
haftmann
parents: 25484
diff changeset
    14
  val setup: Context.generic -> Context.generic
a657683e902a tuned structures in arith_data.ML
haftmann
parents: 25484
diff changeset
    15
end;
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    16
30496
7cdcc9dd95cb vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents: 29302
diff changeset
    17
structure Nat_Arith: NAT_ARITH =
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    18
struct
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    19
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    20
(** abstract syntax of structure nat: 0, Suc, + **)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    21
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
    22
val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
    23
val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT;
26101
a657683e902a tuned structures in arith_data.ML
haftmann
parents: 25484
diff changeset
    24
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    25
fun mk_sum [] = HOLogic.zero
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    26
  | mk_sum [t] = t
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    27
  | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    28
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    29
(*normal form of sums: Suc (... (Suc (a + (b + ...))))*)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    30
fun mk_norm_sum ts =
21621
f9fd69d96c4e slight cleanup in hologic.ML
haftmann
parents: 21415
diff changeset
    31
  let val (ones, sums) = List.partition (equal HOLogic.Suc_zero) ts in
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    32
    funpow (length ones) HOLogic.mk_Suc (mk_sum sums)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    33
  end;
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    34
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    35
fun dest_sum tm =
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    36
  if HOLogic.is_zero tm then []
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    37
  else
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    38
    (case try HOLogic.dest_Suc tm of
21621
f9fd69d96c4e slight cleanup in hologic.ML
haftmann
parents: 21415
diff changeset
    39
      SOME t => HOLogic.Suc_zero :: dest_sum t
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15234
diff changeset
    40
    | NONE =>
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    41
        (case try dest_plus tm of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15234
diff changeset
    42
          SOME (t, u) => dest_sum t @ dest_sum u
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15234
diff changeset
    43
        | NONE => [tm]));
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    44
20217
25b068a99d2b linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents: 20044
diff changeset
    45
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    46
(** cancel common summands **)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    47
30496
7cdcc9dd95cb vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents: 29302
diff changeset
    48
structure CommonCancelSums =
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    49
struct
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    50
  val mk_sum = mk_norm_sum;
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    51
  val dest_sum = dest_sum;
30496
7cdcc9dd95cb vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents: 29302
diff changeset
    52
  val prove_conv = Arith_Data.prove_conv2;
35047
1b2bae06c796 hide fact Nat.add_0_right; make add_0_right from Groups priority
haftmann
parents: 34974
diff changeset
    53
  val norm_tac1 = Arith_Data.simp_all_tac [@{thm add_Suc}, @{thm add_Suc_right},
35064
1bdef0c013d3 hide fact names clashing with fact names from Group.thy
haftmann
parents: 35047
diff changeset
    54
    @{thm Nat.add_0}, @{thm Nat.add_0_right}];
30496
7cdcc9dd95cb vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents: 29302
diff changeset
    55
  val norm_tac2 = Arith_Data.simp_all_tac @{thms add_ac};
18328
841261f303a1 simprocs: static evaluation of simpset;
wenzelm
parents: 17989
diff changeset
    56
  fun norm_tac ss = norm_tac1 ss THEN norm_tac2 ss;
30496
7cdcc9dd95cb vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents: 29302
diff changeset
    57
  fun gen_uncancel_tac rule = let val rule' = rule RS @{thm subst_equals}
7cdcc9dd95cb vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents: 29302
diff changeset
    58
    in fn ct => rtac (instantiate' [] [NONE, SOME ct] rule') 1 end;
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    59
end;
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    60
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    61
structure EqCancelSums = CancelSumsFun
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    62
(struct
30496
7cdcc9dd95cb vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents: 29302
diff changeset
    63
  open CommonCancelSums;
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    64
  val mk_bal = HOLogic.mk_eq;
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    65
  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
22838
haftmann
parents: 22634
diff changeset
    66
  val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel"};
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    67
end);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    68
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    69
structure LessCancelSums = CancelSumsFun
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    70
(struct
30496
7cdcc9dd95cb vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents: 29302
diff changeset
    71
  open CommonCancelSums;
35092
cfe605c54e50 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents: 35064
diff changeset
    72
  val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less};
cfe605c54e50 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents: 35064
diff changeset
    73
  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT;
22838
haftmann
parents: 22634
diff changeset
    74
  val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_less"};
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    75
end);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    76
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    77
structure LeCancelSums = CancelSumsFun
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    78
(struct
30496
7cdcc9dd95cb vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents: 29302
diff changeset
    79
  open CommonCancelSums;
35092
cfe605c54e50 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents: 35064
diff changeset
    80
  val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq};
cfe605c54e50 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents: 35064
diff changeset
    81
  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT;
22838
haftmann
parents: 22634
diff changeset
    82
  val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_le"};
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    83
end);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    84
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    85
structure DiffCancelSums = CancelSumsFun
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    86
(struct
30496
7cdcc9dd95cb vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents: 29302
diff changeset
    87
  open CommonCancelSums;
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
    88
  val mk_bal = HOLogic.mk_binop @{const_name Groups.minus};
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
    89
  val dest_bal = HOLogic.dest_bin @{const_name Groups.minus} HOLogic.natT;
22838
haftmann
parents: 22634
diff changeset
    90
  val uncancel_tac = gen_uncancel_tac @{thm "diff_cancel"};
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    91
end);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    92
26101
a657683e902a tuned structures in arith_data.ML
haftmann
parents: 25484
diff changeset
    93
val nat_cancel_sums_add =
32010
cb1a1c94b4cd more antiquotations;
wenzelm
parents: 30496
diff changeset
    94
  [Simplifier.simproc @{theory} "nateq_cancel_sums"
26101
a657683e902a tuned structures in arith_data.ML
haftmann
parents: 25484
diff changeset
    95
     ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"]
a657683e902a tuned structures in arith_data.ML
haftmann
parents: 25484
diff changeset
    96
     (K EqCancelSums.proc),
32010
cb1a1c94b4cd more antiquotations;
wenzelm
parents: 30496
diff changeset
    97
   Simplifier.simproc @{theory} "natless_cancel_sums"
26101
a657683e902a tuned structures in arith_data.ML
haftmann
parents: 25484
diff changeset
    98
     ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"]
a657683e902a tuned structures in arith_data.ML
haftmann
parents: 25484
diff changeset
    99
     (K LessCancelSums.proc),
32010
cb1a1c94b4cd more antiquotations;
wenzelm
parents: 30496
diff changeset
   100
   Simplifier.simproc @{theory} "natle_cancel_sums"
26101
a657683e902a tuned structures in arith_data.ML
haftmann
parents: 25484
diff changeset
   101
     ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"]
a657683e902a tuned structures in arith_data.ML
haftmann
parents: 25484
diff changeset
   102
     (K LeCancelSums.proc)];
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
   103
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
   104
val nat_cancel_sums = nat_cancel_sums_add @
32010
cb1a1c94b4cd more antiquotations;
wenzelm
parents: 30496
diff changeset
   105
  [Simplifier.simproc @{theory} "natdiff_cancel_sums"
26101
a657683e902a tuned structures in arith_data.ML
haftmann
parents: 25484
diff changeset
   106
    ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"]
a657683e902a tuned structures in arith_data.ML
haftmann
parents: 25484
diff changeset
   107
    (K DiffCancelSums.proc)];
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
   108
26101
a657683e902a tuned structures in arith_data.ML
haftmann
parents: 25484
diff changeset
   109
val setup =
24095
785c3cd7fcb5 moved lin_arith stuff to Tools/lin_arith.ML;
wenzelm
parents: 24076
diff changeset
   110
  Simplifier.map_ss (fn ss => ss addsimprocs nat_cancel_sums);
24076
ae946f751c44 arith method setup: proper context;
wenzelm
parents: 23881
diff changeset
   111
24095
785c3cd7fcb5 moved lin_arith stuff to Tools/lin_arith.ML;
wenzelm
parents: 24076
diff changeset
   112
end;