src/ZF/IntArith.thy
author wenzelm
Wed, 27 Mar 2013 16:38:25 +0100
changeset 51553 63327f679cff
parent 48891 c0eafbd55de3
permissions -rw-r--r--
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
23146
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
     1
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
     2
theory IntArith imports Bin
27237
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
     3
begin
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
     4
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
     5
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
     6
(** To simplify inequalities involving integer negation and literals,
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
     7
    such as -x = #3
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
     8
**)
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
     9
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    10
lemmas [simp] =
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 27237
diff changeset
    11
  zminus_equation [where y = "integ_of(w)"]
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 27237
diff changeset
    12
  equation_zminus [where x = "integ_of(w)"]
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 27237
diff changeset
    13
  for w
27237
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    14
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    15
lemmas [iff] =
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 27237
diff changeset
    16
  zminus_zless [where y = "integ_of(w)"]
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 27237
diff changeset
    17
  zless_zminus [where x = "integ_of(w)"]
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 27237
diff changeset
    18
  for w
27237
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    19
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    20
lemmas [iff] =
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 27237
diff changeset
    21
  zminus_zle [where y = "integ_of(w)"]
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 27237
diff changeset
    22
  zle_zminus [where x = "integ_of(w)"]
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 27237
diff changeset
    23
  for w
27237
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    24
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    25
lemmas [simp] =
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 27237
diff changeset
    26
  Let_def [where s = "integ_of(w)"] for w
27237
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    27
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    28
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    29
(*** Simprocs for numeric literals ***)
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    30
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    31
(** Combining of literal coefficients in sums of products **)
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    32
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 45602
diff changeset
    33
lemma zless_iff_zdiff_zless_0: "(x $< y) \<longleftrightarrow> (x$-y $< #0)"
27237
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    34
  by (simp add: zcompare_rls)
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    35
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
    36
lemma eq_iff_zdiff_eq_0: "[| x \<in> int; y \<in> int |] ==> (x = y) \<longleftrightarrow> (x$-y = #0)"
27237
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    37
  by (simp add: zcompare_rls)
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    38
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 45602
diff changeset
    39
lemma zle_iff_zdiff_zle_0: "(x $<= y) \<longleftrightarrow> (x$-y $<= #0)"
27237
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    40
  by (simp add: zcompare_rls)
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    41
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    42
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    43
(** For combine_numerals **)
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    44
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    45
lemma left_zadd_zmult_distrib: "i$*u $+ (j$*u $+ k) = (i$+j)$*u $+ k"
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    46
  by (simp add: zadd_zmult_distrib zadd_ac)
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    47
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    48
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    49
(** For cancel_numerals **)
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    50
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    51
lemmas rel_iff_rel_0_rls =
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 27237
diff changeset
    52
  zless_iff_zdiff_zless_0 [where y = "u $+ v"]
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 27237
diff changeset
    53
  eq_iff_zdiff_eq_0 [where y = "u $+ v"]
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 27237
diff changeset
    54
  zle_iff_zdiff_zle_0 [where y = "u $+ v"]
27237
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    55
  zless_iff_zdiff_zless_0 [where y = n]
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    56
  eq_iff_zdiff_eq_0 [where y = n]
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    57
  zle_iff_zdiff_zle_0 [where y = n]
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 27237
diff changeset
    58
  for u v (* FIXME n (!?) *)
27237
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    59
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 45602
diff changeset
    60
lemma eq_add_iff1: "(i$*u $+ m = j$*u $+ n) \<longleftrightarrow> ((i$-j)$*u $+ m = intify(n))"
27237
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    61
  apply (simp add: zdiff_def zadd_zmult_distrib)
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    62
  apply (simp add: zcompare_rls)
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    63
  apply (simp add: zadd_ac)
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    64
  done
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    65
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 45602
diff changeset
    66
lemma eq_add_iff2: "(i$*u $+ m = j$*u $+ n) \<longleftrightarrow> (intify(m) = (j$-i)$*u $+ n)"
27237
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    67
  apply (simp add: zdiff_def zadd_zmult_distrib)
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    68
  apply (simp add: zcompare_rls)
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    69
  apply (simp add: zadd_ac)
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    70
  done
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    71
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 45602
diff changeset
    72
lemma less_add_iff1: "(i$*u $+ m $< j$*u $+ n) \<longleftrightarrow> ((i$-j)$*u $+ m $< n)"
27237
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    73
  apply (simp add: zdiff_def zadd_zmult_distrib zadd_ac rel_iff_rel_0_rls)
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    74
  done
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    75
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 45602
diff changeset
    76
lemma less_add_iff2: "(i$*u $+ m $< j$*u $+ n) \<longleftrightarrow> (m $< (j$-i)$*u $+ n)"
27237
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    77
  apply (simp add: zdiff_def zadd_zmult_distrib zadd_ac rel_iff_rel_0_rls)
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    78
  done
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    79
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 45602
diff changeset
    80
lemma le_add_iff1: "(i$*u $+ m $<= j$*u $+ n) \<longleftrightarrow> ((i$-j)$*u $+ m $<= n)"
27237
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    81
  apply (simp add: zdiff_def zadd_zmult_distrib)
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    82
  apply (simp add: zcompare_rls)
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    83
  apply (simp add: zadd_ac)
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    84
  done
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    85
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 45602
diff changeset
    86
lemma le_add_iff2: "(i$*u $+ m $<= j$*u $+ n) \<longleftrightarrow> (m $<= (j$-i)$*u $+ n)"
27237
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    87
  apply (simp add: zdiff_def zadd_zmult_distrib)
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    88
  apply (simp add: zcompare_rls)
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    89
  apply (simp add: zadd_ac)
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    90
  done
c94eefffc3a5 converted ML proofs;
wenzelm
parents: 23146
diff changeset
    91
48891
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 46953
diff changeset
    92
ML_file "int_arith.ML"
23146
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    93
0bc590051d95 moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    94
end