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