src/HOL/arith_data.ML
author wenzelm
Tue, 31 Jul 2007 19:40:26 +0200
changeset 24095 785c3cd7fcb5
parent 24076 ae946f751c44
child 25484 4c98517601ce
permissions -rw-r--r--
moved lin_arith stuff to Tools/lin_arith.ML;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
     1
(*  Title:      HOL/arith_data.ML
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
24095
785c3cd7fcb5 moved lin_arith stuff to Tools/lin_arith.ML;
wenzelm
parents: 24076
diff changeset
     3
    Author:     Markus Wenzel, Stefan Berghofer, and Tobias Nipkow
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
     4
24095
785c3cd7fcb5 moved lin_arith stuff to Tools/lin_arith.ML;
wenzelm
parents: 24076
diff changeset
     5
Basic arithmetic proof tools.
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
     6
*)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
     7
24095
785c3cd7fcb5 moved lin_arith stuff to Tools/lin_arith.ML;
wenzelm
parents: 24076
diff changeset
     8
(*** cancellation of common terms ***)
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
     9
13517
42efec18f5b2 Added div+mod cancelling simproc
nipkow
parents: 13499
diff changeset
    10
structure NatArithUtils =
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    11
struct
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    12
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    13
(** abstract syntax of structure nat: 0, Suc, + **)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    14
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    15
(* mk_sum, mk_norm_sum *)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    16
22997
d4f3b015b50b canonical prefixing of class constants
haftmann
parents: 22947
diff changeset
    17
val mk_plus = HOLogic.mk_binop @{const_name HOL.plus};
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    18
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    19
fun mk_sum [] = HOLogic.zero
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    20
  | mk_sum [t] = t
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    21
  | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    22
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    23
(*normal form of sums: Suc (... (Suc (a + (b + ...))))*)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    24
fun mk_norm_sum ts =
21621
f9fd69d96c4e slight cleanup in hologic.ML
haftmann
parents: 21415
diff changeset
    25
  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
    26
    funpow (length ones) HOLogic.mk_Suc (mk_sum sums)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    27
  end;
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    28
24095
785c3cd7fcb5 moved lin_arith stuff to Tools/lin_arith.ML;
wenzelm
parents: 24076
diff changeset
    29
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    30
(* dest_sum *)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    31
22997
d4f3b015b50b canonical prefixing of class constants
haftmann
parents: 22947
diff changeset
    32
val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} HOLogic.natT;
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    33
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    34
fun dest_sum tm =
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    35
  if HOLogic.is_zero tm then []
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    36
  else
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    37
    (case try HOLogic.dest_Suc tm of
21621
f9fd69d96c4e slight cleanup in hologic.ML
haftmann
parents: 21415
diff changeset
    38
      SOME t => HOLogic.Suc_zero :: dest_sum t
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15234
diff changeset
    39
    | NONE =>
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    40
        (case try dest_plus tm of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15234
diff changeset
    41
          SOME (t, u) => dest_sum t @ dest_sum u
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15234
diff changeset
    42
        | NONE => [tm]));
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    43
24095
785c3cd7fcb5 moved lin_arith stuff to Tools/lin_arith.ML;
wenzelm
parents: 24076
diff changeset
    44
785c3cd7fcb5 moved lin_arith stuff to Tools/lin_arith.ML;
wenzelm
parents: 24076
diff changeset
    45
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    46
(** generic proof tools **)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    47
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    48
(* prove conversions *)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    49
20044
92cc2f4c7335 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 19823
diff changeset
    50
fun prove_conv expand_tac norm_tac ss tu =  (* FIXME avoid standard *)
92cc2f4c7335 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 19823
diff changeset
    51
  mk_meta_eq (standard (Goal.prove (Simplifier.the_context ss) [] []
92cc2f4c7335 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 19823
diff changeset
    52
      (HOLogic.mk_Trueprop (HOLogic.mk_eq tu))
17989
wenzelm
parents: 17985
diff changeset
    53
    (K (EVERY [expand_tac, norm_tac ss]))));
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    54
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    55
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    56
(* rewriting *)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    57
18328
841261f303a1 simprocs: static evaluation of simpset;
wenzelm
parents: 17989
diff changeset
    58
fun simp_all_tac rules =
841261f303a1 simprocs: static evaluation of simpset;
wenzelm
parents: 17989
diff changeset
    59
  let val ss0 = HOL_ss addsimps rules
841261f303a1 simprocs: static evaluation of simpset;
wenzelm
parents: 17989
diff changeset
    60
  in fn ss => ALLGOALS (simp_tac (Simplifier.inherit_context ss ss0)) end;
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    61
13517
42efec18f5b2 Added div+mod cancelling simproc
nipkow
parents: 13499
diff changeset
    62
fun prep_simproc (name, pats, proc) =
16834
71d87aeebb57 HOL.Not;
wenzelm
parents: 16733
diff changeset
    63
  Simplifier.simproc (the_context ()) name pats proc;
13517
42efec18f5b2 Added div+mod cancelling simproc
nipkow
parents: 13499
diff changeset
    64
24095
785c3cd7fcb5 moved lin_arith stuff to Tools/lin_arith.ML;
wenzelm
parents: 24076
diff changeset
    65
end;
785c3cd7fcb5 moved lin_arith stuff to Tools/lin_arith.ML;
wenzelm
parents: 24076
diff changeset
    66
20217
25b068a99d2b linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents: 20044
diff changeset
    67
13517
42efec18f5b2 Added div+mod cancelling simproc
nipkow
parents: 13499
diff changeset
    68
24095
785c3cd7fcb5 moved lin_arith stuff to Tools/lin_arith.ML;
wenzelm
parents: 24076
diff changeset
    69
(** ArithData **)
785c3cd7fcb5 moved lin_arith stuff to Tools/lin_arith.ML;
wenzelm
parents: 24076
diff changeset
    70
13517
42efec18f5b2 Added div+mod cancelling simproc
nipkow
parents: 13499
diff changeset
    71
signature ARITH_DATA =
42efec18f5b2 Added div+mod cancelling simproc
nipkow
parents: 13499
diff changeset
    72
sig
42efec18f5b2 Added div+mod cancelling simproc
nipkow
parents: 13499
diff changeset
    73
  val nat_cancel_sums_add: simproc list
42efec18f5b2 Added div+mod cancelling simproc
nipkow
parents: 13499
diff changeset
    74
  val nat_cancel_sums: simproc list
24095
785c3cd7fcb5 moved lin_arith stuff to Tools/lin_arith.ML;
wenzelm
parents: 24076
diff changeset
    75
  val arith_data_setup: Context.generic -> Context.generic
13517
42efec18f5b2 Added div+mod cancelling simproc
nipkow
parents: 13499
diff changeset
    76
end;
42efec18f5b2 Added div+mod cancelling simproc
nipkow
parents: 13499
diff changeset
    77
42efec18f5b2 Added div+mod cancelling simproc
nipkow
parents: 13499
diff changeset
    78
structure ArithData: ARITH_DATA =
42efec18f5b2 Added div+mod cancelling simproc
nipkow
parents: 13499
diff changeset
    79
struct
42efec18f5b2 Added div+mod cancelling simproc
nipkow
parents: 13499
diff changeset
    80
42efec18f5b2 Added div+mod cancelling simproc
nipkow
parents: 13499
diff changeset
    81
open NatArithUtils;
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    82
24095
785c3cd7fcb5 moved lin_arith stuff to Tools/lin_arith.ML;
wenzelm
parents: 24076
diff changeset
    83
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    84
(** cancel common summands **)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    85
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    86
structure Sum =
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    87
struct
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    88
  val mk_sum = mk_norm_sum;
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    89
  val dest_sum = dest_sum;
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    90
  val prove_conv = prove_conv;
22838
haftmann
parents: 22634
diff changeset
    91
  val norm_tac1 = simp_all_tac [@{thm "add_Suc"}, @{thm "add_Suc_right"},
haftmann
parents: 22634
diff changeset
    92
    @{thm "add_0"}, @{thm "add_0_right"}];
22548
6ce4bddf3bcb dropped legacy ML bindings
haftmann
parents: 21879
diff changeset
    93
  val norm_tac2 = simp_all_tac @{thms add_ac};
18328
841261f303a1 simprocs: static evaluation of simpset;
wenzelm
parents: 17989
diff changeset
    94
  fun norm_tac ss = norm_tac1 ss THEN norm_tac2 ss;
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    95
end;
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    96
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    97
fun gen_uncancel_tac rule ct =
22838
haftmann
parents: 22634
diff changeset
    98
  rtac (instantiate' [] [NONE, SOME ct] (rule RS @{thm subst_equals})) 1;
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    99
24095
785c3cd7fcb5 moved lin_arith stuff to Tools/lin_arith.ML;
wenzelm
parents: 24076
diff changeset
   100
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
   101
(* nat eq *)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
   102
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
   103
structure EqCancelSums = CancelSumsFun
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
   104
(struct
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
   105
  open Sum;
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
   106
  val mk_bal = HOLogic.mk_eq;
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
   107
  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
22838
haftmann
parents: 22634
diff changeset
   108
  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
   109
end);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
   110
24095
785c3cd7fcb5 moved lin_arith stuff to Tools/lin_arith.ML;
wenzelm
parents: 24076
diff changeset
   111
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
   112
(* nat less *)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
   113
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
   114
structure LessCancelSums = CancelSumsFun
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
   115
(struct
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
   116
  open Sum;
23881
851c74f1bb69 moved class ord from Orderings.thy to HOL.thy
haftmann
parents: 23530
diff changeset
   117
  val mk_bal = HOLogic.mk_binrel @{const_name HOL.less};
851c74f1bb69 moved class ord from Orderings.thy to HOL.thy
haftmann
parents: 23530
diff changeset
   118
  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT;
22838
haftmann
parents: 22634
diff changeset
   119
  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
   120
end);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
   121
24095
785c3cd7fcb5 moved lin_arith stuff to Tools/lin_arith.ML;
wenzelm
parents: 24076
diff changeset
   122
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
   123
(* nat le *)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
   124
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
   125
structure LeCancelSums = CancelSumsFun
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
   126
(struct
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
   127
  open Sum;
23881
851c74f1bb69 moved class ord from Orderings.thy to HOL.thy
haftmann
parents: 23530
diff changeset
   128
  val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq};
851c74f1bb69 moved class ord from Orderings.thy to HOL.thy
haftmann
parents: 23530
diff changeset
   129
  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT;
22838
haftmann
parents: 22634
diff changeset
   130
  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
   131
end);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
   132
24095
785c3cd7fcb5 moved lin_arith stuff to Tools/lin_arith.ML;
wenzelm
parents: 24076
diff changeset
   133
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
   134
(* nat diff *)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
   135
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
   136
structure DiffCancelSums = CancelSumsFun
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
   137
(struct
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
   138
  open Sum;
22997
d4f3b015b50b canonical prefixing of class constants
haftmann
parents: 22947
diff changeset
   139
  val mk_bal = HOLogic.mk_binop @{const_name HOL.minus};
d4f3b015b50b canonical prefixing of class constants
haftmann
parents: 22947
diff changeset
   140
  val dest_bal = HOLogic.dest_bin @{const_name HOL.minus} HOLogic.natT;
22838
haftmann
parents: 22634
diff changeset
   141
  val uncancel_tac = gen_uncancel_tac @{thm "diff_cancel"};
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
   142
end);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
   143
24095
785c3cd7fcb5 moved lin_arith stuff to Tools/lin_arith.ML;
wenzelm
parents: 24076
diff changeset
   144
785c3cd7fcb5 moved lin_arith stuff to Tools/lin_arith.ML;
wenzelm
parents: 24076
diff changeset
   145
(* prepare nat_cancel simprocs *)
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
   146
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
   147
val nat_cancel_sums_add = map prep_simproc
13462
56610e2ba220 sane interface for simprocs;
wenzelm
parents: 12949
diff changeset
   148
  [("nateq_cancel_sums",
20268
1fe9aed8fcac code reformatted
webertj
parents: 20254
diff changeset
   149
     ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"],
1fe9aed8fcac code reformatted
webertj
parents: 20254
diff changeset
   150
     K EqCancelSums.proc),
13462
56610e2ba220 sane interface for simprocs;
wenzelm
parents: 12949
diff changeset
   151
   ("natless_cancel_sums",
20268
1fe9aed8fcac code reformatted
webertj
parents: 20254
diff changeset
   152
     ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"],
1fe9aed8fcac code reformatted
webertj
parents: 20254
diff changeset
   153
     K LessCancelSums.proc),
13462
56610e2ba220 sane interface for simprocs;
wenzelm
parents: 12949
diff changeset
   154
   ("natle_cancel_sums",
20268
1fe9aed8fcac code reformatted
webertj
parents: 20254
diff changeset
   155
     ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"],
1fe9aed8fcac code reformatted
webertj
parents: 20254
diff changeset
   156
     K LeCancelSums.proc)];
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
   157
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
   158
val nat_cancel_sums = nat_cancel_sums_add @
13462
56610e2ba220 sane interface for simprocs;
wenzelm
parents: 12949
diff changeset
   159
  [prep_simproc ("natdiff_cancel_sums",
20268
1fe9aed8fcac code reformatted
webertj
parents: 20254
diff changeset
   160
    ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"],
1fe9aed8fcac code reformatted
webertj
parents: 20254
diff changeset
   161
    K DiffCancelSums.proc)];
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
   162
24095
785c3cd7fcb5 moved lin_arith stuff to Tools/lin_arith.ML;
wenzelm
parents: 24076
diff changeset
   163
val arith_data_setup =
785c3cd7fcb5 moved lin_arith stuff to Tools/lin_arith.ML;
wenzelm
parents: 24076
diff changeset
   164
  Simplifier.map_ss (fn ss => ss addsimprocs nat_cancel_sums);
24076
ae946f751c44 arith method setup: proper context;
wenzelm
parents: 23881
diff changeset
   165
ae946f751c44 arith method setup: proper context;
wenzelm
parents: 23881
diff changeset
   166
24095
785c3cd7fcb5 moved lin_arith stuff to Tools/lin_arith.ML;
wenzelm
parents: 24076
diff changeset
   167
(* FIXME dead code *)
15195
197e00ce3f20 new forward deduction capability for simplifier
nipkow
parents: 15185
diff changeset
   168
(* antisymmetry:
15197
19e735596e51 Added antisymmetry simproc
nipkow
parents: 15195
diff changeset
   169
   combines x <= y (or ~(y < x)) and y <= x (or ~(x < y)) into x = y
15195
197e00ce3f20 new forward deduction capability for simplifier
nipkow
parents: 15185
diff changeset
   170
197e00ce3f20 new forward deduction capability for simplifier
nipkow
parents: 15185
diff changeset
   171
local
197e00ce3f20 new forward deduction capability for simplifier
nipkow
parents: 15185
diff changeset
   172
val antisym = mk_meta_eq order_antisym
22548
6ce4bddf3bcb dropped legacy ML bindings
haftmann
parents: 21879
diff changeset
   173
val not_lessD = @{thm linorder_not_less} RS iffD1
15195
197e00ce3f20 new forward deduction capability for simplifier
nipkow
parents: 15185
diff changeset
   174
fun prp t thm = (#prop(rep_thm thm) = t)
197e00ce3f20 new forward deduction capability for simplifier
nipkow
parents: 15185
diff changeset
   175
in
197e00ce3f20 new forward deduction capability for simplifier
nipkow
parents: 15185
diff changeset
   176
fun antisym_eq prems thm =
197e00ce3f20 new forward deduction capability for simplifier
nipkow
parents: 15185
diff changeset
   177
  let
197e00ce3f20 new forward deduction capability for simplifier
nipkow
parents: 15185
diff changeset
   178
    val r = #prop(rep_thm thm);
197e00ce3f20 new forward deduction capability for simplifier
nipkow
parents: 15185
diff changeset
   179
  in
197e00ce3f20 new forward deduction capability for simplifier
nipkow
parents: 15185
diff changeset
   180
    case r of
23881
851c74f1bb69 moved class ord from Orderings.thy to HOL.thy
haftmann
parents: 23530
diff changeset
   181
      Tr $ ((c as Const(@{const_name HOL.less_eq},T)) $ s $ t) =>
15195
197e00ce3f20 new forward deduction capability for simplifier
nipkow
parents: 15185
diff changeset
   182
        let val r' = Tr $ (c $ t $ s)
197e00ce3f20 new forward deduction capability for simplifier
nipkow
parents: 15185
diff changeset
   183
        in
197e00ce3f20 new forward deduction capability for simplifier
nipkow
parents: 15185
diff changeset
   184
          case Library.find_first (prp r') prems of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15234
diff changeset
   185
            NONE =>
23881
851c74f1bb69 moved class ord from Orderings.thy to HOL.thy
haftmann
parents: 23530
diff changeset
   186
              let val r' = Tr $ (HOLogic.Not $ (Const(@{const_name HOL.less},T) $ s $ t))
15195
197e00ce3f20 new forward deduction capability for simplifier
nipkow
parents: 15185
diff changeset
   187
              in case Library.find_first (prp r') prems of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15234
diff changeset
   188
                   NONE => []
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15234
diff changeset
   189
                 | SOME thm' => [(thm' RS not_lessD) RS (thm RS antisym)]
15195
197e00ce3f20 new forward deduction capability for simplifier
nipkow
parents: 15185
diff changeset
   190
              end
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15234
diff changeset
   191
          | SOME thm' => [thm' RS (thm RS antisym)]
15195
197e00ce3f20 new forward deduction capability for simplifier
nipkow
parents: 15185
diff changeset
   192
        end
23881
851c74f1bb69 moved class ord from Orderings.thy to HOL.thy
haftmann
parents: 23530
diff changeset
   193
    | Tr $ (Const("Not",_) $ (Const(@{const_name HOL.less},T) $ s $ t)) =>
851c74f1bb69 moved class ord from Orderings.thy to HOL.thy
haftmann
parents: 23530
diff changeset
   194
        let val r' = Tr $ (Const(@{const_name HOL.less_eq},T) $ s $ t)
15195
197e00ce3f20 new forward deduction capability for simplifier
nipkow
parents: 15185
diff changeset
   195
        in
197e00ce3f20 new forward deduction capability for simplifier
nipkow
parents: 15185
diff changeset
   196
          case Library.find_first (prp r') prems of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15234
diff changeset
   197
            NONE =>
23881
851c74f1bb69 moved class ord from Orderings.thy to HOL.thy
haftmann
parents: 23530
diff changeset
   198
              let val r' = Tr $ (HOLogic.Not $ (Const(@{const_name HOL.less},T) $ t $ s))
15195
197e00ce3f20 new forward deduction capability for simplifier
nipkow
parents: 15185
diff changeset
   199
              in case Library.find_first (prp r') prems of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15234
diff changeset
   200
                   NONE => []
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15234
diff changeset
   201
                 | SOME thm' =>
15195
197e00ce3f20 new forward deduction capability for simplifier
nipkow
parents: 15185
diff changeset
   202
                     [(thm' RS not_lessD) RS ((thm RS not_lessD) RS antisym)]
197e00ce3f20 new forward deduction capability for simplifier
nipkow
parents: 15185
diff changeset
   203
              end
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15234
diff changeset
   204
          | SOME thm' => [thm' RS ((thm RS not_lessD) RS antisym)]
15195
197e00ce3f20 new forward deduction capability for simplifier
nipkow
parents: 15185
diff changeset
   205
        end
197e00ce3f20 new forward deduction capability for simplifier
nipkow
parents: 15185
diff changeset
   206
    | _ => []
197e00ce3f20 new forward deduction capability for simplifier
nipkow
parents: 15185
diff changeset
   207
  end
197e00ce3f20 new forward deduction capability for simplifier
nipkow
parents: 15185
diff changeset
   208
  handle THM _ => []
197e00ce3f20 new forward deduction capability for simplifier
nipkow
parents: 15185
diff changeset
   209
end;
15197
19e735596e51 Added antisymmetry simproc
nipkow
parents: 15195
diff changeset
   210
*)
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
   211
24095
785c3cd7fcb5 moved lin_arith stuff to Tools/lin_arith.ML;
wenzelm
parents: 24076
diff changeset
   212
end;
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
   213
24095
785c3cd7fcb5 moved lin_arith stuff to Tools/lin_arith.ML;
wenzelm
parents: 24076
diff changeset
   214
open ArithData;