src/HOL/arith_data.ML
author wenzelm
Fri Mar 28 19:43:54 2008 +0100 (2008-03-28)
changeset 26462 dac4e2bce00d
parent 26101 a657683e902a
child 28262 aa7ca36d67fd
permissions -rw-r--r--
avoid rebinding of existing facts;
wenzelm@9436
     1
(*  Title:      HOL/arith_data.ML
wenzelm@9436
     2
    ID:         $Id$
wenzelm@24095
     3
    Author:     Markus Wenzel, Stefan Berghofer, and Tobias Nipkow
wenzelm@9436
     4
wenzelm@24095
     5
Basic arithmetic proof tools.
wenzelm@9436
     6
*)
wenzelm@9436
     7
haftmann@26101
     8
signature ARITH_DATA =
haftmann@26101
     9
sig
haftmann@26101
    10
  val prove_conv: tactic -> (MetaSimplifier.simpset -> tactic)
haftmann@26101
    11
    -> MetaSimplifier.simpset -> term * term -> thm
haftmann@26101
    12
  val simp_all_tac: thm list -> MetaSimplifier.simpset -> tactic
haftmann@26101
    13
haftmann@26101
    14
  val mk_sum: term list -> term
haftmann@26101
    15
  val mk_norm_sum: term list -> term
haftmann@26101
    16
  val dest_sum: term -> term list
haftmann@26101
    17
haftmann@26101
    18
  val nat_cancel_sums_add: simproc list
haftmann@26101
    19
  val nat_cancel_sums: simproc list
haftmann@26101
    20
  val setup: Context.generic -> Context.generic
haftmann@26101
    21
end;
wenzelm@9436
    22
haftmann@26101
    23
structure ArithData: ARITH_DATA =
wenzelm@9436
    24
struct
wenzelm@9436
    25
haftmann@26101
    26
(** generic proof tools **)
haftmann@26101
    27
haftmann@26101
    28
(* prove conversions *)
haftmann@26101
    29
haftmann@26101
    30
fun prove_conv expand_tac norm_tac ss tu =  (* FIXME avoid standard *)
haftmann@26101
    31
  mk_meta_eq (standard (Goal.prove (Simplifier.the_context ss) [] []
haftmann@26101
    32
      (HOLogic.mk_Trueprop (HOLogic.mk_eq tu))
haftmann@26101
    33
    (K (EVERY [expand_tac, norm_tac ss]))));
haftmann@26101
    34
haftmann@26101
    35
(* rewriting *)
haftmann@26101
    36
haftmann@26101
    37
fun simp_all_tac rules =
haftmann@26101
    38
  let val ss0 = HOL_ss addsimps rules
haftmann@26101
    39
  in fn ss => ALLGOALS (simp_tac (Simplifier.inherit_context ss ss0)) end;
haftmann@26101
    40
haftmann@26101
    41
wenzelm@9436
    42
(** abstract syntax of structure nat: 0, Suc, + **)
wenzelm@9436
    43
haftmann@26101
    44
local
wenzelm@9436
    45
haftmann@22997
    46
val mk_plus = HOLogic.mk_binop @{const_name HOL.plus};
haftmann@26101
    47
val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} HOLogic.natT;
haftmann@26101
    48
haftmann@26101
    49
in
wenzelm@9436
    50
wenzelm@9436
    51
fun mk_sum [] = HOLogic.zero
wenzelm@9436
    52
  | mk_sum [t] = t
wenzelm@9436
    53
  | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
wenzelm@9436
    54
wenzelm@9436
    55
(*normal form of sums: Suc (... (Suc (a + (b + ...))))*)
wenzelm@9436
    56
fun mk_norm_sum ts =
haftmann@21621
    57
  let val (ones, sums) = List.partition (equal HOLogic.Suc_zero) ts in
wenzelm@9436
    58
    funpow (length ones) HOLogic.mk_Suc (mk_sum sums)
wenzelm@9436
    59
  end;
wenzelm@9436
    60
wenzelm@24095
    61
wenzelm@9436
    62
fun dest_sum tm =
wenzelm@9436
    63
  if HOLogic.is_zero tm then []
wenzelm@9436
    64
  else
wenzelm@9436
    65
    (case try HOLogic.dest_Suc tm of
haftmann@21621
    66
      SOME t => HOLogic.Suc_zero :: dest_sum t
skalberg@15531
    67
    | NONE =>
wenzelm@9436
    68
        (case try dest_plus tm of
skalberg@15531
    69
          SOME (t, u) => dest_sum t @ dest_sum u
skalberg@15531
    70
        | NONE => [tm]));
wenzelm@9436
    71
wenzelm@24095
    72
end;
wenzelm@24095
    73
webertj@20217
    74
wenzelm@9436
    75
(** cancel common summands **)
wenzelm@9436
    76
wenzelm@9436
    77
structure Sum =
wenzelm@9436
    78
struct
wenzelm@9436
    79
  val mk_sum = mk_norm_sum;
wenzelm@9436
    80
  val dest_sum = dest_sum;
wenzelm@9436
    81
  val prove_conv = prove_conv;
haftmann@22838
    82
  val norm_tac1 = simp_all_tac [@{thm "add_Suc"}, @{thm "add_Suc_right"},
haftmann@22838
    83
    @{thm "add_0"}, @{thm "add_0_right"}];
haftmann@22548
    84
  val norm_tac2 = simp_all_tac @{thms add_ac};
wenzelm@18328
    85
  fun norm_tac ss = norm_tac1 ss THEN norm_tac2 ss;
wenzelm@9436
    86
end;
wenzelm@9436
    87
wenzelm@9436
    88
fun gen_uncancel_tac rule ct =
haftmann@22838
    89
  rtac (instantiate' [] [NONE, SOME ct] (rule RS @{thm subst_equals})) 1;
wenzelm@9436
    90
wenzelm@24095
    91
wenzelm@9436
    92
(* nat eq *)
wenzelm@9436
    93
wenzelm@9436
    94
structure EqCancelSums = CancelSumsFun
wenzelm@9436
    95
(struct
wenzelm@9436
    96
  open Sum;
wenzelm@9436
    97
  val mk_bal = HOLogic.mk_eq;
wenzelm@9436
    98
  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
haftmann@22838
    99
  val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel"};
wenzelm@9436
   100
end);
wenzelm@9436
   101
wenzelm@24095
   102
wenzelm@9436
   103
(* nat less *)
wenzelm@9436
   104
wenzelm@9436
   105
structure LessCancelSums = CancelSumsFun
wenzelm@9436
   106
(struct
wenzelm@9436
   107
  open Sum;
haftmann@23881
   108
  val mk_bal = HOLogic.mk_binrel @{const_name HOL.less};
haftmann@23881
   109
  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT;
haftmann@22838
   110
  val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_less"};
wenzelm@9436
   111
end);
wenzelm@9436
   112
wenzelm@24095
   113
wenzelm@9436
   114
(* nat le *)
wenzelm@9436
   115
wenzelm@9436
   116
structure LeCancelSums = CancelSumsFun
wenzelm@9436
   117
(struct
wenzelm@9436
   118
  open Sum;
haftmann@23881
   119
  val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq};
haftmann@23881
   120
  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT;
haftmann@22838
   121
  val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_le"};
wenzelm@9436
   122
end);
wenzelm@9436
   123
wenzelm@24095
   124
wenzelm@9436
   125
(* nat diff *)
wenzelm@9436
   126
wenzelm@9436
   127
structure DiffCancelSums = CancelSumsFun
wenzelm@9436
   128
(struct
wenzelm@9436
   129
  open Sum;
haftmann@22997
   130
  val mk_bal = HOLogic.mk_binop @{const_name HOL.minus};
haftmann@22997
   131
  val dest_bal = HOLogic.dest_bin @{const_name HOL.minus} HOLogic.natT;
haftmann@22838
   132
  val uncancel_tac = gen_uncancel_tac @{thm "diff_cancel"};
wenzelm@9436
   133
end);
wenzelm@9436
   134
wenzelm@24095
   135
wenzelm@24095
   136
(* prepare nat_cancel simprocs *)
wenzelm@9436
   137
haftmann@26101
   138
val nat_cancel_sums_add =
haftmann@26101
   139
  [Simplifier.simproc @{theory} "nateq_cancel_sums"
haftmann@26101
   140
     ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"]
haftmann@26101
   141
     (K EqCancelSums.proc),
haftmann@26101
   142
   Simplifier.simproc @{theory} "natless_cancel_sums"
haftmann@26101
   143
     ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"]
haftmann@26101
   144
     (K LessCancelSums.proc),
haftmann@26101
   145
   Simplifier.simproc @{theory} "natle_cancel_sums"
haftmann@26101
   146
     ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"]
haftmann@26101
   147
     (K LeCancelSums.proc)];
wenzelm@9436
   148
wenzelm@9436
   149
val nat_cancel_sums = nat_cancel_sums_add @
haftmann@26101
   150
  [Simplifier.simproc @{theory} "natdiff_cancel_sums"
haftmann@26101
   151
    ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"]
haftmann@26101
   152
    (K DiffCancelSums.proc)];
wenzelm@9436
   153
haftmann@26101
   154
val setup =
wenzelm@24095
   155
  Simplifier.map_ss (fn ss => ss addsimprocs nat_cancel_sums);
wenzelm@24076
   156
wenzelm@24095
   157
end;