src/HOL/arith_data.ML
author haftmann
Wed Sep 26 20:27:55 2007 +0200 (2007-09-26)
changeset 24728 e2b3a1065676
parent 24095 785c3cd7fcb5
child 25484 4c98517601ce
permissions -rw-r--r--
moved Finite_Set before Datatype
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
wenzelm@24095
     8
(*** cancellation of common terms ***)
wenzelm@9436
     9
nipkow@13517
    10
structure NatArithUtils =
wenzelm@9436
    11
struct
wenzelm@9436
    12
wenzelm@9436
    13
(** abstract syntax of structure nat: 0, Suc, + **)
wenzelm@9436
    14
wenzelm@9436
    15
(* mk_sum, mk_norm_sum *)
wenzelm@9436
    16
haftmann@22997
    17
val mk_plus = HOLogic.mk_binop @{const_name HOL.plus};
wenzelm@9436
    18
wenzelm@9436
    19
fun mk_sum [] = HOLogic.zero
wenzelm@9436
    20
  | mk_sum [t] = t
wenzelm@9436
    21
  | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
wenzelm@9436
    22
wenzelm@9436
    23
(*normal form of sums: Suc (... (Suc (a + (b + ...))))*)
wenzelm@9436
    24
fun mk_norm_sum ts =
haftmann@21621
    25
  let val (ones, sums) = List.partition (equal HOLogic.Suc_zero) ts in
wenzelm@9436
    26
    funpow (length ones) HOLogic.mk_Suc (mk_sum sums)
wenzelm@9436
    27
  end;
wenzelm@9436
    28
wenzelm@24095
    29
wenzelm@9436
    30
(* dest_sum *)
wenzelm@9436
    31
haftmann@22997
    32
val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} HOLogic.natT;
wenzelm@9436
    33
wenzelm@9436
    34
fun dest_sum tm =
wenzelm@9436
    35
  if HOLogic.is_zero tm then []
wenzelm@9436
    36
  else
wenzelm@9436
    37
    (case try HOLogic.dest_Suc tm of
haftmann@21621
    38
      SOME t => HOLogic.Suc_zero :: dest_sum t
skalberg@15531
    39
    | NONE =>
wenzelm@9436
    40
        (case try dest_plus tm of
skalberg@15531
    41
          SOME (t, u) => dest_sum t @ dest_sum u
skalberg@15531
    42
        | NONE => [tm]));
wenzelm@9436
    43
wenzelm@24095
    44
wenzelm@24095
    45
wenzelm@9436
    46
(** generic proof tools **)
wenzelm@9436
    47
wenzelm@9436
    48
(* prove conversions *)
wenzelm@9436
    49
wenzelm@20044
    50
fun prove_conv expand_tac norm_tac ss tu =  (* FIXME avoid standard *)
wenzelm@20044
    51
  mk_meta_eq (standard (Goal.prove (Simplifier.the_context ss) [] []
wenzelm@20044
    52
      (HOLogic.mk_Trueprop (HOLogic.mk_eq tu))
wenzelm@17989
    53
    (K (EVERY [expand_tac, norm_tac ss]))));
wenzelm@9436
    54
wenzelm@9436
    55
wenzelm@9436
    56
(* rewriting *)
wenzelm@9436
    57
wenzelm@18328
    58
fun simp_all_tac rules =
wenzelm@18328
    59
  let val ss0 = HOL_ss addsimps rules
wenzelm@18328
    60
  in fn ss => ALLGOALS (simp_tac (Simplifier.inherit_context ss ss0)) end;
wenzelm@9436
    61
nipkow@13517
    62
fun prep_simproc (name, pats, proc) =
wenzelm@16834
    63
  Simplifier.simproc (the_context ()) name pats proc;
nipkow@13517
    64
wenzelm@24095
    65
end;
wenzelm@24095
    66
webertj@20217
    67
nipkow@13517
    68
wenzelm@24095
    69
(** ArithData **)
wenzelm@24095
    70
nipkow@13517
    71
signature ARITH_DATA =
nipkow@13517
    72
sig
nipkow@13517
    73
  val nat_cancel_sums_add: simproc list
nipkow@13517
    74
  val nat_cancel_sums: simproc list
wenzelm@24095
    75
  val arith_data_setup: Context.generic -> Context.generic
nipkow@13517
    76
end;
nipkow@13517
    77
nipkow@13517
    78
structure ArithData: ARITH_DATA =
nipkow@13517
    79
struct
nipkow@13517
    80
nipkow@13517
    81
open NatArithUtils;
wenzelm@9436
    82
wenzelm@24095
    83
wenzelm@9436
    84
(** cancel common summands **)
wenzelm@9436
    85
wenzelm@9436
    86
structure Sum =
wenzelm@9436
    87
struct
wenzelm@9436
    88
  val mk_sum = mk_norm_sum;
wenzelm@9436
    89
  val dest_sum = dest_sum;
wenzelm@9436
    90
  val prove_conv = prove_conv;
haftmann@22838
    91
  val norm_tac1 = simp_all_tac [@{thm "add_Suc"}, @{thm "add_Suc_right"},
haftmann@22838
    92
    @{thm "add_0"}, @{thm "add_0_right"}];
haftmann@22548
    93
  val norm_tac2 = simp_all_tac @{thms add_ac};
wenzelm@18328
    94
  fun norm_tac ss = norm_tac1 ss THEN norm_tac2 ss;
wenzelm@9436
    95
end;
wenzelm@9436
    96
wenzelm@9436
    97
fun gen_uncancel_tac rule ct =
haftmann@22838
    98
  rtac (instantiate' [] [NONE, SOME ct] (rule RS @{thm subst_equals})) 1;
wenzelm@9436
    99
wenzelm@24095
   100
wenzelm@9436
   101
(* nat eq *)
wenzelm@9436
   102
wenzelm@9436
   103
structure EqCancelSums = CancelSumsFun
wenzelm@9436
   104
(struct
wenzelm@9436
   105
  open Sum;
wenzelm@9436
   106
  val mk_bal = HOLogic.mk_eq;
wenzelm@9436
   107
  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
haftmann@22838
   108
  val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel"};
wenzelm@9436
   109
end);
wenzelm@9436
   110
wenzelm@24095
   111
wenzelm@9436
   112
(* nat less *)
wenzelm@9436
   113
wenzelm@9436
   114
structure LessCancelSums = CancelSumsFun
wenzelm@9436
   115
(struct
wenzelm@9436
   116
  open Sum;
haftmann@23881
   117
  val mk_bal = HOLogic.mk_binrel @{const_name HOL.less};
haftmann@23881
   118
  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT;
haftmann@22838
   119
  val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_less"};
wenzelm@9436
   120
end);
wenzelm@9436
   121
wenzelm@24095
   122
wenzelm@9436
   123
(* nat le *)
wenzelm@9436
   124
wenzelm@9436
   125
structure LeCancelSums = CancelSumsFun
wenzelm@9436
   126
(struct
wenzelm@9436
   127
  open Sum;
haftmann@23881
   128
  val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq};
haftmann@23881
   129
  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT;
haftmann@22838
   130
  val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_le"};
wenzelm@9436
   131
end);
wenzelm@9436
   132
wenzelm@24095
   133
wenzelm@9436
   134
(* nat diff *)
wenzelm@9436
   135
wenzelm@9436
   136
structure DiffCancelSums = CancelSumsFun
wenzelm@9436
   137
(struct
wenzelm@9436
   138
  open Sum;
haftmann@22997
   139
  val mk_bal = HOLogic.mk_binop @{const_name HOL.minus};
haftmann@22997
   140
  val dest_bal = HOLogic.dest_bin @{const_name HOL.minus} HOLogic.natT;
haftmann@22838
   141
  val uncancel_tac = gen_uncancel_tac @{thm "diff_cancel"};
wenzelm@9436
   142
end);
wenzelm@9436
   143
wenzelm@24095
   144
wenzelm@24095
   145
(* prepare nat_cancel simprocs *)
wenzelm@9436
   146
wenzelm@9436
   147
val nat_cancel_sums_add = map prep_simproc
wenzelm@13462
   148
  [("nateq_cancel_sums",
webertj@20268
   149
     ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"],
webertj@20268
   150
     K EqCancelSums.proc),
wenzelm@13462
   151
   ("natless_cancel_sums",
webertj@20268
   152
     ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"],
webertj@20268
   153
     K LessCancelSums.proc),
wenzelm@13462
   154
   ("natle_cancel_sums",
webertj@20268
   155
     ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"],
webertj@20268
   156
     K LeCancelSums.proc)];
wenzelm@9436
   157
wenzelm@9436
   158
val nat_cancel_sums = nat_cancel_sums_add @
wenzelm@13462
   159
  [prep_simproc ("natdiff_cancel_sums",
webertj@20268
   160
    ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"],
webertj@20268
   161
    K DiffCancelSums.proc)];
wenzelm@9436
   162
wenzelm@24095
   163
val arith_data_setup =
wenzelm@24095
   164
  Simplifier.map_ss (fn ss => ss addsimprocs nat_cancel_sums);
wenzelm@24076
   165
wenzelm@24076
   166
wenzelm@24095
   167
(* FIXME dead code *)
nipkow@15195
   168
(* antisymmetry:
nipkow@15197
   169
   combines x <= y (or ~(y < x)) and y <= x (or ~(x < y)) into x = y
nipkow@15195
   170
nipkow@15195
   171
local
nipkow@15195
   172
val antisym = mk_meta_eq order_antisym
haftmann@22548
   173
val not_lessD = @{thm linorder_not_less} RS iffD1
nipkow@15195
   174
fun prp t thm = (#prop(rep_thm thm) = t)
nipkow@15195
   175
in
nipkow@15195
   176
fun antisym_eq prems thm =
nipkow@15195
   177
  let
nipkow@15195
   178
    val r = #prop(rep_thm thm);
nipkow@15195
   179
  in
nipkow@15195
   180
    case r of
haftmann@23881
   181
      Tr $ ((c as Const(@{const_name HOL.less_eq},T)) $ s $ t) =>
nipkow@15195
   182
        let val r' = Tr $ (c $ t $ s)
nipkow@15195
   183
        in
nipkow@15195
   184
          case Library.find_first (prp r') prems of
skalberg@15531
   185
            NONE =>
haftmann@23881
   186
              let val r' = Tr $ (HOLogic.Not $ (Const(@{const_name HOL.less},T) $ s $ t))
nipkow@15195
   187
              in case Library.find_first (prp r') prems of
skalberg@15531
   188
                   NONE => []
skalberg@15531
   189
                 | SOME thm' => [(thm' RS not_lessD) RS (thm RS antisym)]
nipkow@15195
   190
              end
skalberg@15531
   191
          | SOME thm' => [thm' RS (thm RS antisym)]
nipkow@15195
   192
        end
haftmann@23881
   193
    | Tr $ (Const("Not",_) $ (Const(@{const_name HOL.less},T) $ s $ t)) =>
haftmann@23881
   194
        let val r' = Tr $ (Const(@{const_name HOL.less_eq},T) $ s $ t)
nipkow@15195
   195
        in
nipkow@15195
   196
          case Library.find_first (prp r') prems of
skalberg@15531
   197
            NONE =>
haftmann@23881
   198
              let val r' = Tr $ (HOLogic.Not $ (Const(@{const_name HOL.less},T) $ t $ s))
nipkow@15195
   199
              in case Library.find_first (prp r') prems of
skalberg@15531
   200
                   NONE => []
skalberg@15531
   201
                 | SOME thm' =>
nipkow@15195
   202
                     [(thm' RS not_lessD) RS ((thm RS not_lessD) RS antisym)]
nipkow@15195
   203
              end
skalberg@15531
   204
          | SOME thm' => [thm' RS ((thm RS not_lessD) RS antisym)]
nipkow@15195
   205
        end
nipkow@15195
   206
    | _ => []
nipkow@15195
   207
  end
nipkow@15195
   208
  handle THM _ => []
nipkow@15195
   209
end;
nipkow@15197
   210
*)
wenzelm@9436
   211
wenzelm@24095
   212
end;
wenzelm@9436
   213
wenzelm@24095
   214
open ArithData;