src/ZF/int_arith.ML
author wenzelm
Thu, 31 May 2007 12:06:31 +0200
changeset 23146 0bc590051d95
child 24630 351a308ab58d
permissions -rw-r--r--
moved Integ files to canonical place;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
23146
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
     1
(*  Title:      ZF/int_arith.ML
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
     3
    Author:     Larry Paulson
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
     4
    Copyright   2000  University of Cambridge
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
     5
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
     6
Simprocs for linear arithmetic.
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
     7
*)
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
     8
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
     9
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    10
(** To simplify inequalities involving integer negation and literals,
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    11
    such as -x = #3
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    12
**)
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    13
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    14
Addsimps [inst "y" "integ_of(?w)" zminus_equation,
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    15
          inst "x" "integ_of(?w)" equation_zminus];
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    16
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    17
AddIffs [inst "y" "integ_of(?w)" zminus_zless,
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    18
         inst "x" "integ_of(?w)" zless_zminus];
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    19
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    20
AddIffs [inst "y" "integ_of(?w)" zminus_zle,
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    21
         inst "x" "integ_of(?w)" zle_zminus];
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    22
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    23
Addsimps [inst "s" "integ_of(?w)" (thm "Let_def")];
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    24
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    25
(*** Simprocs for numeric literals ***)
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    26
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    27
(** Combining of literal coefficients in sums of products **)
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    28
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    29
Goal "(x $< y) <-> (x$-y $< #0)";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    30
by (simp_tac (simpset() addsimps zcompare_rls) 1);
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    31
qed "zless_iff_zdiff_zless_0";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    32
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    33
Goal "[| x: int; y: int |] ==> (x = y) <-> (x$-y = #0)";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    34
by (asm_simp_tac (simpset() addsimps zcompare_rls) 1);
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    35
qed "eq_iff_zdiff_eq_0";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    36
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    37
Goal "(x $<= y) <-> (x$-y $<= #0)";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    38
by (asm_simp_tac (simpset() addsimps zcompare_rls) 1);
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    39
qed "zle_iff_zdiff_zle_0";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    40
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    41
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    42
(** For combine_numerals **)
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    43
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    44
Goal "i$*u $+ (j$*u $+ k) = (i$+j)$*u $+ k";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    45
by (simp_tac (simpset() addsimps [zadd_zmult_distrib]@zadd_ac) 1);
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    46
qed "left_zadd_zmult_distrib";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    47
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    48
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    49
(** For cancel_numerals **)
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    50
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    51
val rel_iff_rel_0_rls = map (inst "y" "?u$+?v")
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    52
                          [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0,
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    53
                           zle_iff_zdiff_zle_0] @
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    54
                        map (inst "y" "n")
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    55
                          [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0,
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    56
                           zle_iff_zdiff_zle_0];
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    57
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    58
Goal "(i$*u $+ m = j$*u $+ n) <-> ((i$-j)$*u $+ m = intify(n))";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    59
by (simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]) 1);
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    60
by (simp_tac (simpset() addsimps zcompare_rls) 1);
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    61
by (simp_tac (simpset() addsimps zadd_ac) 1);
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    62
qed "eq_add_iff1";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    63
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    64
Goal "(i$*u $+ m = j$*u $+ n) <-> (intify(m) = (j$-i)$*u $+ n)";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    65
by (simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]) 1);
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    66
by (simp_tac (simpset() addsimps zcompare_rls) 1);
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    67
by (simp_tac (simpset() addsimps zadd_ac) 1);
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    68
qed "eq_add_iff2";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    69
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    70
Goal "(i$*u $+ m $< j$*u $+ n) <-> ((i$-j)$*u $+ m $< n)";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    71
by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    72
                                     zadd_ac@rel_iff_rel_0_rls) 1);
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    73
qed "less_add_iff1";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    74
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    75
Goal "(i$*u $+ m $< j$*u $+ n) <-> (m $< (j$-i)$*u $+ n)";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    76
by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    77
                                     zadd_ac@rel_iff_rel_0_rls) 1);
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    78
qed "less_add_iff2";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    79
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    80
Goal "(i$*u $+ m $<= j$*u $+ n) <-> ((i$-j)$*u $+ m $<= n)";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    81
by (simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]) 1);
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    82
by (simp_tac (simpset() addsimps zcompare_rls) 1);
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    83
by (simp_tac (simpset() addsimps zadd_ac) 1);
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    84
qed "le_add_iff1";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    85
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    86
Goal "(i$*u $+ m $<= j$*u $+ n) <-> (m $<= (j$-i)$*u $+ n)";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    87
by (simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]) 1);
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    88
by (simp_tac (simpset() addsimps zcompare_rls) 1);
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    89
by (simp_tac (simpset() addsimps zadd_ac) 1);
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    90
qed "le_add_iff2";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    91
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    92
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    93
structure Int_Numeral_Simprocs =
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    94
struct
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    95
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    96
(*Utilities*)
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    97
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    98
val integ_of_const = Const ("Bin.integ_of", iT --> iT);
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    99
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   100
fun mk_numeral n = integ_of_const $ NumeralSyntax.mk_bin n;
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   101
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   102
(*Decodes a binary INTEGER*)
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   103
fun dest_numeral (Const("Bin.integ_of", _) $ w) =
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   104
     (NumeralSyntax.dest_bin w
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   105
      handle Match => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w]))
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   106
  | dest_numeral t =  raise TERM("Int_Numeral_Simprocs.dest_numeral:2", [t]);
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   107
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   108
fun find_first_numeral past (t::terms) =
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   109
        ((dest_numeral t, rev past @ terms)
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   110
         handle TERM _ => find_first_numeral (t::past) terms)
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   111
  | find_first_numeral past [] = raise TERM("find_first_numeral", []);
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   112
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   113
val zero = mk_numeral 0;
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   114
val mk_plus = FOLogic.mk_binop "Int.zadd";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   115
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   116
val iT = Ind_Syntax.iT;
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   117
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   118
val zminus_const = Const ("Int.zminus", iT --> iT);
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   119
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   120
(*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*)
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   121
fun mk_sum []        = zero
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   122
  | mk_sum [t,u]     = mk_plus (t, u)
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   123
  | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   124
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   125
(*this version ALWAYS includes a trailing zero*)
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   126
fun long_mk_sum []        = zero
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   127
  | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   128
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   129
val dest_plus = FOLogic.dest_bin "Int.zadd" iT;
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   130
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   131
(*decompose additions AND subtractions as a sum*)
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   132
fun dest_summing (pos, Const ("Int.zadd", _) $ t $ u, ts) =
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   133
        dest_summing (pos, t, dest_summing (pos, u, ts))
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   134
  | dest_summing (pos, Const ("Int.zdiff", _) $ t $ u, ts) =
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   135
        dest_summing (pos, t, dest_summing (not pos, u, ts))
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   136
  | dest_summing (pos, t, ts) =
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   137
        if pos then t::ts else zminus_const$t :: ts;
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   138
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   139
fun dest_sum t = dest_summing (true, t, []);
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   140
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   141
val mk_diff = FOLogic.mk_binop "Int.zdiff";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   142
val dest_diff = FOLogic.dest_bin "Int.zdiff" iT;
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   143
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   144
val one = mk_numeral 1;
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   145
val mk_times = FOLogic.mk_binop "Int.zmult";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   146
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   147
fun mk_prod [] = one
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   148
  | mk_prod [t] = t
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   149
  | mk_prod (t :: ts) = if t = one then mk_prod ts
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   150
                        else mk_times (t, mk_prod ts);
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   151
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   152
val dest_times = FOLogic.dest_bin "Int.zmult" iT;
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   153
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   154
fun dest_prod t =
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   155
      let val (t,u) = dest_times t
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   156
      in  dest_prod t @ dest_prod u  end
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   157
      handle TERM _ => [t];
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   158
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   159
(*DON'T do the obvious simplifications; that would create special cases*)
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   160
fun mk_coeff (k, t) = mk_times (mk_numeral k, t);
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   161
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   162
(*Express t as a product of (possibly) a numeral with other sorted terms*)
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   163
fun dest_coeff sign (Const ("Int.zminus", _) $ t) = dest_coeff (~sign) t
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   164
  | dest_coeff sign t =
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   165
    let val ts = sort Term.term_ord (dest_prod t)
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   166
        val (n, ts') = find_first_numeral [] ts
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   167
                          handle TERM _ => (1, ts)
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   168
    in (sign*n, mk_prod ts') end;
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   169
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   170
(*Find first coefficient-term THAT MATCHES u*)
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   171
fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   172
  | find_first_coeff past u (t::terms) =
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   173
        let val (n,u') = dest_coeff 1 t
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   174
        in  if u aconv u' then (n, rev past @ terms)
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   175
                          else find_first_coeff (t::past) u terms
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   176
        end
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   177
        handle TERM _ => find_first_coeff (t::past) u terms;
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   178
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   179
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   180
(*Simplify #1*n and n*#1 to n*)
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   181
val add_0s = [zadd_0_intify, zadd_0_right_intify];
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   182
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   183
val mult_1s = [zmult_1_intify, zmult_1_right_intify,
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   184
               zmult_minus1, zmult_minus1_right];
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   185
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   186
val tc_rules = [integ_of_type, intify_in_int,
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   187
                int_of_type, zadd_type, zdiff_type, zmult_type] @ 
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   188
               thms "bin.intros";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   189
val intifys = [intify_ident, zadd_intify1, zadd_intify2,
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   190
               zdiff_intify1, zdiff_intify2, zmult_intify1, zmult_intify2,
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   191
               zless_intify1, zless_intify2, zle_intify1, zle_intify2];
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   192
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   193
(*To perform binary arithmetic*)
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   194
val bin_simps = [add_integ_of_left] @ bin_arith_simps @ bin_rel_simps;
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   195
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   196
(*To evaluate binary negations of coefficients*)
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   197
val zminus_simps = NCons_simps @
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   198
                   [integ_of_minus RS sym,
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   199
                    bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min,
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   200
                    bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min];
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   201
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   202
(*To let us treat subtraction as addition*)
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   203
val diff_simps = [zdiff_def, zminus_zadd_distrib, zminus_zminus];
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   204
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   205
(*push the unary minus down: - x * y = x * - y *)
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   206
val int_minus_mult_eq_1_to_2 =
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   207
    [zmult_zminus, zmult_zminus_right RS sym] MRS trans |> standard;
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   208
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   209
(*to extract again any uncancelled minuses*)
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   210
val int_minus_from_mult_simps =
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   211
    [zminus_zminus, zmult_zminus, zmult_zminus_right];
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   212
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   213
(*combine unary minus with numeric literals, however nested within a product*)
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   214
val int_mult_minus_simps =
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   215
    [zmult_assoc, zmult_zminus RS sym, int_minus_mult_eq_1_to_2];
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   216
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   217
fun prep_simproc (name, pats, proc) =
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   218
  Simplifier.simproc (the_context ()) name pats proc;
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   219
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   220
structure CancelNumeralsCommon =
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   221
  struct
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   222
  val mk_sum            = (fn T:typ => mk_sum)
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   223
  val dest_sum          = dest_sum
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   224
  val mk_coeff          = mk_coeff
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   225
  val dest_coeff        = dest_coeff 1
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   226
  val find_first_coeff  = find_first_coeff []
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   227
  fun trans_tac _       = ArithData.gen_trans_tac iff_trans
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   228
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   229
  val norm_ss1 = ZF_ss addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ zadd_ac
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   230
  val norm_ss2 = ZF_ss addsimps bin_simps @ int_mult_minus_simps @ intifys
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   231
  val norm_ss3 = ZF_ss addsimps int_minus_from_mult_simps @ zadd_ac @ zmult_ac @ tc_rules @ intifys
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   232
  fun norm_tac ss =
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   233
    ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss1))
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   234
    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss2))
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   235
    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss3))
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   236
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   237
  val numeral_simp_ss = ZF_ss addsimps add_0s @ bin_simps @ tc_rules @ intifys
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   238
  fun numeral_simp_tac ss =
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   239
    ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   240
    THEN ALLGOALS (SIMPSET' (fn simpset => asm_simp_tac (Simplifier.inherit_context ss simpset)))
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   241
  val simplify_meta_eq  = ArithData.simplify_meta_eq (add_0s @ mult_1s)
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   242
  end;
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   243
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   244
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   245
structure EqCancelNumerals = CancelNumeralsFun
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   246
 (open CancelNumeralsCommon
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   247
  val prove_conv = ArithData.prove_conv "inteq_cancel_numerals"
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   248
  val mk_bal   = FOLogic.mk_eq
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   249
  val dest_bal = FOLogic.dest_eq
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   250
  val bal_add1 = eq_add_iff1 RS iff_trans
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   251
  val bal_add2 = eq_add_iff2 RS iff_trans
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   252
);
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   253
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   254
structure LessCancelNumerals = CancelNumeralsFun
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   255
 (open CancelNumeralsCommon
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   256
  val prove_conv = ArithData.prove_conv "intless_cancel_numerals"
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   257
  val mk_bal   = FOLogic.mk_binrel "Int.zless"
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   258
  val dest_bal = FOLogic.dest_bin "Int.zless" iT
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   259
  val bal_add1 = less_add_iff1 RS iff_trans
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   260
  val bal_add2 = less_add_iff2 RS iff_trans
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   261
);
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   262
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   263
structure LeCancelNumerals = CancelNumeralsFun
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   264
 (open CancelNumeralsCommon
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   265
  val prove_conv = ArithData.prove_conv "intle_cancel_numerals"
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   266
  val mk_bal   = FOLogic.mk_binrel "Int.zle"
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   267
  val dest_bal = FOLogic.dest_bin "Int.zle" iT
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   268
  val bal_add1 = le_add_iff1 RS iff_trans
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   269
  val bal_add2 = le_add_iff2 RS iff_trans
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   270
);
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   271
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   272
val cancel_numerals =
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   273
  map prep_simproc
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   274
   [("inteq_cancel_numerals",
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   275
     ["l $+ m = n", "l = m $+ n",
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   276
      "l $- m = n", "l = m $- n",
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   277
      "l $* m = n", "l = m $* n"],
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   278
     K EqCancelNumerals.proc),
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   279
    ("intless_cancel_numerals",
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   280
     ["l $+ m $< n", "l $< m $+ n",
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   281
      "l $- m $< n", "l $< m $- n",
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   282
      "l $* m $< n", "l $< m $* n"],
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   283
     K LessCancelNumerals.proc),
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   284
    ("intle_cancel_numerals",
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   285
     ["l $+ m $<= n", "l $<= m $+ n",
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   286
      "l $- m $<= n", "l $<= m $- n",
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   287
      "l $* m $<= n", "l $<= m $* n"],
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   288
     K LeCancelNumerals.proc)];
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   289
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   290
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   291
(*version without the hyps argument*)
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   292
fun prove_conv_nohyps name tacs sg = ArithData.prove_conv name tacs sg [];
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   293
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   294
structure CombineNumeralsData =
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   295
  struct
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   296
  type coeff            = IntInf.int
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   297
  val iszero            = (fn x : IntInf.int => x = 0)
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   298
  val add               = IntInf.+ 
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   299
  val mk_sum            = (fn T:typ => long_mk_sum) (*to work for #2*x $+ #3*x *)
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   300
  val dest_sum          = dest_sum
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   301
  val mk_coeff          = mk_coeff
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   302
  val dest_coeff        = dest_coeff 1
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   303
  val left_distrib      = left_zadd_zmult_distrib RS trans
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   304
  val prove_conv        = prove_conv_nohyps "int_combine_numerals"
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   305
  fun trans_tac _       = ArithData.gen_trans_tac trans
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   306
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   307
  val norm_ss1 = ZF_ss addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ zadd_ac @ intifys
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   308
  val norm_ss2 = ZF_ss addsimps bin_simps @ int_mult_minus_simps @ intifys
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   309
  val norm_ss3 = ZF_ss addsimps int_minus_from_mult_simps @ zadd_ac @ zmult_ac @ tc_rules @ intifys
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   310
  fun norm_tac ss =
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   311
    ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss1))
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   312
    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss2))
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   313
    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss3))
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   314
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   315
  val numeral_simp_ss = ZF_ss addsimps add_0s @ bin_simps @ tc_rules @ intifys
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   316
  fun numeral_simp_tac ss =
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   317
    ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   318
  val simplify_meta_eq  = ArithData.simplify_meta_eq (add_0s @ mult_1s)
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   319
  end;
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   320
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   321
structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   322
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   323
val combine_numerals =
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   324
  prep_simproc ("int_combine_numerals", ["i $+ j", "i $- j"], K CombineNumerals.proc);
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   325
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   326
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   327
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   328
(** Constant folding for integer multiplication **)
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   329
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   330
(*The trick is to regard products as sums, e.g. #3 $* x $* #4 as
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   331
  the "sum" of #3, x, #4; the literals are then multiplied*)
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   332
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   333
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   334
structure CombineNumeralsProdData =
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   335
  struct
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   336
  type coeff            = IntInf.int
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   337
  val iszero            = (fn x : IntInf.int => x = 0)
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   338
  val add               = IntInf.*
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   339
  val mk_sum            = (fn T:typ => mk_prod)
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   340
  val dest_sum          = dest_prod
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   341
  fun mk_coeff(k,t) = if t=one then mk_numeral k
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   342
                      else raise TERM("mk_coeff", [])
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   343
  fun dest_coeff t = (dest_numeral t, one)  (*We ONLY want pure numerals.*)
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   344
  val left_distrib      = zmult_assoc RS sym RS trans
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   345
  val prove_conv        = prove_conv_nohyps "int_combine_numerals_prod"
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   346
  fun trans_tac _       = ArithData.gen_trans_tac trans
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   347
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   348
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   349
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   350
val norm_ss1 = ZF_ss addsimps mult_1s @ diff_simps @ zminus_simps
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   351
  val norm_ss2 = ZF_ss addsimps [zmult_zminus_right RS sym] @
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   352
    bin_simps @ zmult_ac @ tc_rules @ intifys
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   353
  fun norm_tac ss =
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   354
    ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss1))
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   355
    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss2))
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   356
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   357
  val numeral_simp_ss = ZF_ss addsimps bin_simps @ tc_rules @ intifys
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   358
  fun numeral_simp_tac ss =
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   359
    ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   360
  val simplify_meta_eq  = ArithData.simplify_meta_eq (mult_1s);
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   361
  end;
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   362
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   363
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   364
structure CombineNumeralsProd = CombineNumeralsFun(CombineNumeralsProdData);
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   365
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   366
val combine_numerals_prod =
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   367
  prep_simproc ("int_combine_numerals_prod", ["i $* j"], K CombineNumeralsProd.proc);
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   368
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   369
end;
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   370
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   371
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   372
Addsimprocs Int_Numeral_Simprocs.cancel_numerals;
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   373
Addsimprocs [Int_Numeral_Simprocs.combine_numerals,
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   374
             Int_Numeral_Simprocs.combine_numerals_prod];
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   375
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   376
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   377
(*examples:*)
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   378
(*
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   379
print_depth 22;
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   380
set timing;
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   381
set trace_simp;
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   382
fun test s = (Goal s; by (Asm_simp_tac 1));
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   383
val sg = #sign (rep_thm (topthm()));
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   384
val t = FOLogic.dest_Trueprop (Logic.strip_assums_concl(getgoal 1));
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   385
val (t,_) = FOLogic.dest_eq t;
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   386
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   387
(*combine_numerals_prod (products of separate literals) *)
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   388
test "#5 $* x $* #3 = y";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   389
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   390
test "y2 $+ ?x42 = y $+ y2";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   391
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   392
test "oo : int ==> l $+ (l $+ #2) $+ oo = oo";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   393
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   394
test "#9$*x $+ y = x$*#23 $+ z";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   395
test "y $+ x = x $+ z";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   396
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   397
test "x : int ==> x $+ y $+ z = x $+ z";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   398
test "x : int ==> y $+ (z $+ x) = z $+ x";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   399
test "z : int ==> x $+ y $+ z = (z $+ y) $+ (x $+ w)";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   400
test "z : int ==> x$*y $+ z = (z $+ y) $+ (y$*x $+ w)";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   401
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   402
test "#-3 $* x $+ y $<= x $* #2 $+ z";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   403
test "y $+ x $<= x $+ z";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   404
test "x $+ y $+ z $<= x $+ z";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   405
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   406
test "y $+ (z $+ x) $< z $+ x";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   407
test "x $+ y $+ z $< (z $+ y) $+ (x $+ w)";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   408
test "x$*y $+ z $< (z $+ y) $+ (y$*x $+ w)";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   409
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   410
test "l $+ #2 $+ #2 $+ #2 $+ (l $+ #2) $+ (oo $+ #2) = uu";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   411
test "u : int ==> #2 $* u = u";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   412
test "(i $+ j $+ #12 $+ k) $- #15 = y";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   413
test "(i $+ j $+ #12 $+ k) $- #5 = y";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   414
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   415
test "y $- b $< b";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   416
test "y $- (#3 $* b $+ c) $< b $- #2 $* c";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   417
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   418
test "(#2 $* x $- (u $* v) $+ y) $- v $* #3 $* u = w";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   419
test "(#2 $* x $* u $* v $+ (u $* v) $* #4 $+ y) $- v $* u $* #4 = w";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   420
test "(#2 $* x $* u $* v $+ (u $* v) $* #4 $+ y) $- v $* u = w";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   421
test "u $* v $- (x $* u $* v $+ (u $* v) $* #4 $+ y) = w";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   422
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   423
test "(i $+ j $+ #12 $+ k) = u $+ #15 $+ y";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   424
test "(i $+ j $* #2 $+ #12 $+ k) = j $+ #5 $+ y";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   425
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   426
test "#2 $* y $+ #3 $* z $+ #6 $* w $+ #2 $* y $+ #3 $* z $+ #2 $* u = #2 $* y' $+ #3 $* z' $+ #6 $* w' $+ #2 $* y' $+ #3 $* z' $+ u $+ vv";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   427
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   428
test "a $+ $-(b$+c) $+ b = d";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   429
test "a $+ $-(b$+c) $- b = d";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   430
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   431
(*negative numerals*)
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   432
test "(i $+ j $+ #-2 $+ k) $- (u $+ #5 $+ y) = zz";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   433
test "(i $+ j $+ #-3 $+ k) $< u $+ #5 $+ y";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   434
test "(i $+ j $+ #3 $+ k) $< u $+ #-6 $+ y";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   435
test "(i $+ j $+ #-12 $+ k) $- #15 = y";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   436
test "(i $+ j $+ #12 $+ k) $- #-15 = y";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   437
test "(i $+ j $+ #-12 $+ k) $- #-15 = y";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   438
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   439
(*Multiplying separated numerals*)
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   440
Goal "#6 $* ($# x $* #2) =  uu";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   441
Goal "#4 $* ($# x $* $# x) $* (#2 $* $# x) =  uu";
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   442
*)
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   443