src/ZF/IntArith.thy
author wenzelm
Tue Sep 25 22:36:06 2012 +0200 (2012-09-25 ago)
changeset 49566 66cbf8bb4693
parent 48891 c0eafbd55de3
permissions -rw-r--r--
basic integration of graphview into document model;
added Graph_Dockable;
updated Isabelle/jEdit authors and dependencies etc.;
     1 
     2 theory IntArith imports Bin
     3 begin
     4 
     5 
     6 (** To simplify inequalities involving integer negation and literals,
     7     such as -x = #3
     8 **)
     9 
    10 lemmas [simp] =
    11   zminus_equation [where y = "integ_of(w)"]
    12   equation_zminus [where x = "integ_of(w)"]
    13   for w
    14 
    15 lemmas [iff] =
    16   zminus_zless [where y = "integ_of(w)"]
    17   zless_zminus [where x = "integ_of(w)"]
    18   for w
    19 
    20 lemmas [iff] =
    21   zminus_zle [where y = "integ_of(w)"]
    22   zle_zminus [where x = "integ_of(w)"]
    23   for w
    24 
    25 lemmas [simp] =
    26   Let_def [where s = "integ_of(w)"] for w
    27 
    28 
    29 (*** Simprocs for numeric literals ***)
    30 
    31 (** Combining of literal coefficients in sums of products **)
    32 
    33 lemma zless_iff_zdiff_zless_0: "(x $< y) \<longleftrightarrow> (x$-y $< #0)"
    34   by (simp add: zcompare_rls)
    35 
    36 lemma eq_iff_zdiff_eq_0: "[| x \<in> int; y \<in> int |] ==> (x = y) \<longleftrightarrow> (x$-y = #0)"
    37   by (simp add: zcompare_rls)
    38 
    39 lemma zle_iff_zdiff_zle_0: "(x $<= y) \<longleftrightarrow> (x$-y $<= #0)"
    40   by (simp add: zcompare_rls)
    41 
    42 
    43 (** For combine_numerals **)
    44 
    45 lemma left_zadd_zmult_distrib: "i$*u $+ (j$*u $+ k) = (i$+j)$*u $+ k"
    46   by (simp add: zadd_zmult_distrib zadd_ac)
    47 
    48 
    49 (** For cancel_numerals **)
    50 
    51 lemmas rel_iff_rel_0_rls =
    52   zless_iff_zdiff_zless_0 [where y = "u $+ v"]
    53   eq_iff_zdiff_eq_0 [where y = "u $+ v"]
    54   zle_iff_zdiff_zle_0 [where y = "u $+ v"]
    55   zless_iff_zdiff_zless_0 [where y = n]
    56   eq_iff_zdiff_eq_0 [where y = n]
    57   zle_iff_zdiff_zle_0 [where y = n]
    58   for u v (* FIXME n (!?) *)
    59 
    60 lemma eq_add_iff1: "(i$*u $+ m = j$*u $+ n) \<longleftrightarrow> ((i$-j)$*u $+ m = intify(n))"
    61   apply (simp add: zdiff_def zadd_zmult_distrib)
    62   apply (simp add: zcompare_rls)
    63   apply (simp add: zadd_ac)
    64   done
    65 
    66 lemma eq_add_iff2: "(i$*u $+ m = j$*u $+ n) \<longleftrightarrow> (intify(m) = (j$-i)$*u $+ n)"
    67   apply (simp add: zdiff_def zadd_zmult_distrib)
    68   apply (simp add: zcompare_rls)
    69   apply (simp add: zadd_ac)
    70   done
    71 
    72 lemma less_add_iff1: "(i$*u $+ m $< j$*u $+ n) \<longleftrightarrow> ((i$-j)$*u $+ m $< n)"
    73   apply (simp add: zdiff_def zadd_zmult_distrib zadd_ac rel_iff_rel_0_rls)
    74   done
    75 
    76 lemma less_add_iff2: "(i$*u $+ m $< j$*u $+ n) \<longleftrightarrow> (m $< (j$-i)$*u $+ n)"
    77   apply (simp add: zdiff_def zadd_zmult_distrib zadd_ac rel_iff_rel_0_rls)
    78   done
    79 
    80 lemma le_add_iff1: "(i$*u $+ m $<= j$*u $+ n) \<longleftrightarrow> ((i$-j)$*u $+ m $<= n)"
    81   apply (simp add: zdiff_def zadd_zmult_distrib)
    82   apply (simp add: zcompare_rls)
    83   apply (simp add: zadd_ac)
    84   done
    85 
    86 lemma le_add_iff2: "(i$*u $+ m $<= j$*u $+ n) \<longleftrightarrow> (m $<= (j$-i)$*u $+ n)"
    87   apply (simp add: zdiff_def zadd_zmult_distrib)
    88   apply (simp add: zcompare_rls)
    89   apply (simp add: zadd_ac)
    90   done
    91 
    92 ML_file "int_arith.ML"
    93 
    94 end