src/ZF/IntArith.thy
author wenzelm
Thu Sep 02 00:48:07 2010 +0200 (2010-09-02)
changeset 38980 af73cf0dc31f
parent 27237 c94eefffc3a5
child 45602 2a858377c3d2
permissions -rw-r--r--
turned show_question_marks into proper configuration option;
show_question_marks only affects regular type/term pretty printing, not raw Term.string_of_vname;
tuned;
     1 
     2 theory IntArith imports Bin
     3 uses ("int_arith.ML")
     4 begin
     5 
     6 
     7 (** To simplify inequalities involving integer negation and literals,
     8     such as -x = #3
     9 **)
    10 
    11 lemmas [simp] =
    12   zminus_equation [where y = "integ_of(w)", standard]
    13   equation_zminus [where x = "integ_of(w)", standard]
    14 
    15 lemmas [iff] =
    16   zminus_zless [where y = "integ_of(w)", standard]
    17   zless_zminus [where x = "integ_of(w)", standard]
    18 
    19 lemmas [iff] =
    20   zminus_zle [where y = "integ_of(w)", standard]
    21   zle_zminus [where x = "integ_of(w)", standard]
    22 
    23 lemmas [simp] =
    24   Let_def [where s = "integ_of(w)", standard]
    25 
    26 
    27 (*** Simprocs for numeric literals ***)
    28 
    29 (** Combining of literal coefficients in sums of products **)
    30 
    31 lemma zless_iff_zdiff_zless_0: "(x $< y) <-> (x$-y $< #0)"
    32   by (simp add: zcompare_rls)
    33 
    34 lemma eq_iff_zdiff_eq_0: "[| x: int; y: int |] ==> (x = y) <-> (x$-y = #0)"
    35   by (simp add: zcompare_rls)
    36 
    37 lemma zle_iff_zdiff_zle_0: "(x $<= y) <-> (x$-y $<= #0)"
    38   by (simp add: zcompare_rls)
    39 
    40 
    41 (** For combine_numerals **)
    42 
    43 lemma left_zadd_zmult_distrib: "i$*u $+ (j$*u $+ k) = (i$+j)$*u $+ k"
    44   by (simp add: zadd_zmult_distrib zadd_ac)
    45 
    46 
    47 (** For cancel_numerals **)
    48 
    49 lemmas rel_iff_rel_0_rls =
    50   zless_iff_zdiff_zless_0 [where y = "u $+ v", standard]
    51   eq_iff_zdiff_eq_0 [where y = "u $+ v", standard]
    52   zle_iff_zdiff_zle_0 [where y = "u $+ v", standard]
    53   zless_iff_zdiff_zless_0 [where y = n]
    54   eq_iff_zdiff_eq_0 [where y = n]
    55   zle_iff_zdiff_zle_0 [where y = n]
    56 
    57 lemma eq_add_iff1: "(i$*u $+ m = j$*u $+ n) <-> ((i$-j)$*u $+ m = intify(n))"
    58   apply (simp add: zdiff_def zadd_zmult_distrib)
    59   apply (simp add: zcompare_rls)
    60   apply (simp add: zadd_ac)
    61   done
    62 
    63 lemma eq_add_iff2: "(i$*u $+ m = j$*u $+ n) <-> (intify(m) = (j$-i)$*u $+ n)"
    64   apply (simp add: zdiff_def zadd_zmult_distrib)
    65   apply (simp add: zcompare_rls)
    66   apply (simp add: zadd_ac)
    67   done
    68 
    69 lemma less_add_iff1: "(i$*u $+ m $< j$*u $+ n) <-> ((i$-j)$*u $+ m $< n)"
    70   apply (simp add: zdiff_def zadd_zmult_distrib zadd_ac rel_iff_rel_0_rls)
    71   done
    72 
    73 lemma less_add_iff2: "(i$*u $+ m $< j$*u $+ n) <-> (m $< (j$-i)$*u $+ n)"
    74   apply (simp add: zdiff_def zadd_zmult_distrib zadd_ac rel_iff_rel_0_rls)
    75   done
    76 
    77 lemma le_add_iff1: "(i$*u $+ m $<= j$*u $+ n) <-> ((i$-j)$*u $+ m $<= n)"
    78   apply (simp add: zdiff_def zadd_zmult_distrib)
    79   apply (simp add: zcompare_rls)
    80   apply (simp add: zadd_ac)
    81   done
    82 
    83 lemma le_add_iff2: "(i$*u $+ m $<= j$*u $+ n) <-> (m $<= (j$-i)$*u $+ n)"
    84   apply (simp add: zdiff_def zadd_zmult_distrib)
    85   apply (simp add: zcompare_rls)
    86   apply (simp add: zadd_ac)
    87   done
    88 
    89 use "int_arith.ML"
    90 
    91 end