author | wenzelm |
Sun, 03 Dec 2017 18:53:49 +0100 | |
changeset 67120 | 491fd7f0b5df |
parent 66886 | 960509bfd47e |
child 67408 | 4a4c14b24800 |
permissions | -rw-r--r-- |
65363 | 1 |
(* Title: HOL/Word/Word_Miscellaneous.thy *) |
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
2 |
|
61799 | 3 |
section \<open>Miscellaneous lemmas, of at least doubtful value\<close> |
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
4 |
|
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
5 |
theory Word_Miscellaneous |
66453
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
65363
diff
changeset
|
6 |
imports "HOL-Library.Bit" Misc_Numeric |
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
7 |
begin |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
8 |
|
65363 | 9 |
lemma power_minus_simp: "0 < n \<Longrightarrow> a ^ n = a * a ^ (n - 1)" |
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
10 |
by (auto dest: gr0_implies_Suc) |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
11 |
|
65363 | 12 |
lemma funpow_minus_simp: "0 < n \<Longrightarrow> f ^^ n = f \<circ> f ^^ (n - 1)" |
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
13 |
by (auto dest: gr0_implies_Suc) |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
14 |
|
65363 | 15 |
lemma power_numeral: "a ^ numeral k = a * a ^ (pred_numeral k)" |
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
16 |
by (simp add: numeral_eq_Suc) |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
17 |
|
65363 | 18 |
lemma funpow_numeral [simp]: "f ^^ numeral k = f \<circ> f ^^ (pred_numeral k)" |
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
19 |
by (simp add: numeral_eq_Suc) |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
20 |
|
65363 | 21 |
lemma replicate_numeral [simp]: "replicate (numeral k) x = x # replicate (pred_numeral k) x" |
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
22 |
by (simp add: numeral_eq_Suc) |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
23 |
|
65363 | 24 |
lemma rco_alt: "(f \<circ> g) ^^ n \<circ> f = f \<circ> (g \<circ> f) ^^ n" |
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
25 |
apply (rule ext) |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
26 |
apply (induct n) |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
27 |
apply (simp_all add: o_def) |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
28 |
done |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
29 |
|
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
30 |
lemma list_exhaust_size_gt0: |
67120 | 31 |
assumes "\<And>a list. y = a # list \<Longrightarrow> P" |
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
32 |
shows "0 < length y \<Longrightarrow> P" |
65363 | 33 |
apply (cases y) |
34 |
apply simp |
|
67120 | 35 |
apply (rule assms) |
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
36 |
apply fastforce |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
37 |
done |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
38 |
|
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
39 |
lemma list_exhaust_size_eq0: |
67120 | 40 |
assumes "y = [] \<Longrightarrow> P" |
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
41 |
shows "length y = 0 \<Longrightarrow> P" |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
42 |
apply (cases y) |
67120 | 43 |
apply (rule assms) |
65363 | 44 |
apply simp |
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
45 |
apply simp |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
46 |
done |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
47 |
|
65363 | 48 |
lemma size_Cons_lem_eq: "y = xa # list \<Longrightarrow> size y = Suc k \<Longrightarrow> size list = k" |
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
49 |
by auto |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
50 |
|
62390 | 51 |
lemmas ls_splits = prod.split prod.split_asm if_split_asm |
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
52 |
|
65363 | 53 |
lemma not_B1_is_B0: "y \<noteq> 1 \<Longrightarrow> y = 0" |
54 |
for y :: bit |
|
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
55 |
by (cases y) auto |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
56 |
|
65363 | 57 |
lemma B1_ass_B0: |
58 |
fixes y :: bit |
|
59 |
assumes y: "y = 0 \<Longrightarrow> y = 1" |
|
60 |
shows "y = 1" |
|
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
61 |
apply (rule classical) |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
62 |
apply (drule not_B1_is_B0) |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
63 |
apply (erule y) |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
64 |
done |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
65 |
|
61799 | 66 |
\<comment> "simplifications for specific word lengths" |
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
67 |
lemmas n2s_ths [THEN eq_reflection] = add_2_eq_Suc add_2_eq_Suc' |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
68 |
|
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
69 |
lemmas s2n_ths = n2s_ths [symmetric] |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
70 |
|
65363 | 71 |
lemma and_len: "xs = ys \<Longrightarrow> xs = ys \<and> length xs = length ys" |
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
72 |
by auto |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
73 |
|
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
74 |
lemma size_if: "size (if p then xs else ys) = (if p then size xs else size ys)" |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
75 |
by auto |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
76 |
|
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
77 |
lemma tl_if: "tl (if p then xs else ys) = (if p then tl xs else tl ys)" |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
78 |
by auto |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
79 |
|
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
80 |
lemma hd_if: "hd (if p then xs else ys) = (if p then hd xs else hd ys)" |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
81 |
by auto |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
82 |
|
65363 | 83 |
lemma if_Not_x: "(if p then \<not> x else x) = (p = (\<not> x))" |
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
84 |
by auto |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
85 |
|
65363 | 86 |
lemma if_x_Not: "(if p then x else \<not> x) = (p = x)" |
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
87 |
by auto |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
88 |
|
65363 | 89 |
lemma if_same_and: "(If p x y \<and> If p u v) = (if p then x \<and> u else y \<and> v)" |
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
90 |
by auto |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
91 |
|
65363 | 92 |
lemma if_same_eq: "(If p x y = (If p u v)) = (if p then x = u else y = v)" |
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
93 |
by auto |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
94 |
|
65363 | 95 |
lemma if_same_eq_not: "(If p x y = (\<not> If p u v)) = (if p then x = (\<not> u) else y = (\<not> v))" |
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
96 |
by auto |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
97 |
|
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
98 |
(* note - if_Cons can cause blowup in the size, if p is complex, |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
99 |
so make a simproc *) |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
100 |
lemma if_Cons: "(if p then x # xs else y # ys) = If p x y # If p xs ys" |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
101 |
by auto |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
102 |
|
65363 | 103 |
lemma if_single: "(if xc then [xab] else [an]) = [if xc then xab else an]" |
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
104 |
by auto |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
105 |
|
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
106 |
lemma if_bool_simps: |
65363 | 107 |
"If p True y = (p \<or> y) \<and> If p False y = (\<not> p \<and> y) \<and> |
108 |
If p y True = (p \<longrightarrow> y) \<and> If p y False = (p \<and> y)" |
|
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
109 |
by auto |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
110 |
|
65363 | 111 |
lemmas if_simps = |
112 |
if_x_Not if_Not_x if_cancel if_True if_False if_bool_simps |
|
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
113 |
|
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
114 |
lemmas seqr = eq_reflection [where x = "size w"] for w (* FIXME: delete *) |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
115 |
|
65363 | 116 |
lemma the_elemI: "y = {x} \<Longrightarrow> the_elem y = x" |
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
117 |
by simp |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
118 |
|
65363 | 119 |
lemma nonemptyE: "S \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> S \<Longrightarrow> R) \<Longrightarrow> R" |
120 |
by auto |
|
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
121 |
|
65363 | 122 |
lemma gt_or_eq_0: "0 < y \<or> 0 = y" |
123 |
for y :: nat |
|
124 |
by arith |
|
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
125 |
|
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
126 |
lemmas xtr1 = xtrans(1) |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
127 |
lemmas xtr2 = xtrans(2) |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
128 |
lemmas xtr3 = xtrans(3) |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
129 |
lemmas xtr4 = xtrans(4) |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
130 |
lemmas xtr5 = xtrans(5) |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
131 |
lemmas xtr6 = xtrans(6) |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
132 |
lemmas xtr7 = xtrans(7) |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
133 |
lemmas xtr8 = xtrans(8) |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
134 |
|
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
135 |
lemmas nat_simps = diff_add_inverse2 diff_add_inverse |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
136 |
lemmas nat_iffs = le_add1 le_add2 |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
137 |
|
65363 | 138 |
lemma sum_imp_diff: "j = k + i \<Longrightarrow> j - i = k" |
139 |
for k :: nat |
|
140 |
by arith |
|
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
141 |
|
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
142 |
lemmas pos_mod_sign2 = zless2 [THEN pos_mod_sign [where b = "2::int"]] |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
143 |
lemmas pos_mod_bound2 = zless2 [THEN pos_mod_bound [where b = "2::int"]] |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
144 |
|
65363 | 145 |
lemma nmod2: "n mod 2 = 0 \<or> n mod 2 = 1" |
146 |
for n :: int |
|
58681 | 147 |
by arith |
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
148 |
|
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
55816
diff
changeset
|
149 |
lemmas eme1p = emep1 [simplified add.commute] |
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
150 |
|
65363 | 151 |
lemma le_diff_eq': "a \<le> c - b \<longleftrightarrow> b + a \<le> c" |
152 |
for a b c :: int |
|
153 |
by arith |
|
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
154 |
|
65363 | 155 |
lemma less_diff_eq': "a < c - b \<longleftrightarrow> b + a < c" |
156 |
for a b c :: int |
|
157 |
by arith |
|
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
158 |
|
65363 | 159 |
lemma diff_less_eq': "a - b < c \<longleftrightarrow> a < b + c" |
160 |
for a b c :: int |
|
161 |
by arith |
|
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
162 |
|
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
163 |
lemmas m1mod22k = mult_pos_pos [OF zless2 zless2p, THEN zmod_minus1] |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
164 |
|
65363 | 165 |
lemma z1pdiv2: "(2 * b + 1) div 2 = b" |
166 |
for b :: int |
|
167 |
by arith |
|
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
168 |
|
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
169 |
lemmas zdiv_le_dividend = xtr3 [OF div_by_1 [symmetric] zdiv_mono2, |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
170 |
simplified int_one_le_iff_zero_less, simplified] |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
171 |
|
65363 | 172 |
lemma axxbyy: "a + m + m = b + n + n \<Longrightarrow> a = 0 \<or> a = 1 \<Longrightarrow> b = 0 \<or> b = 1 \<Longrightarrow> a = b \<and> m = n" |
173 |
for a b m n :: int |
|
174 |
by arith |
|
175 |
||
176 |
lemma axxmod2: "(1 + x + x) mod 2 = 1 \<and> (0 + x + x) mod 2 = 0" |
|
177 |
for x :: int |
|
178 |
by arith |
|
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
179 |
|
65363 | 180 |
lemma axxdiv2: "(1 + x + x) div 2 = x \<and> (0 + x + x) div 2 = x" |
181 |
for x :: int |
|
182 |
by arith |
|
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
183 |
|
65363 | 184 |
lemmas iszero_minus = |
185 |
trans [THEN trans, OF iszero_def neg_equal_0_iff_equal iszero_def [symmetric]] |
|
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
186 |
|
65363 | 187 |
lemmas zadd_diff_inverse = |
188 |
trans [OF diff_add_cancel [symmetric] add.commute] |
|
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
189 |
|
65363 | 190 |
lemmas add_diff_cancel2 = |
191 |
add.commute [THEN diff_eq_eq [THEN iffD2]] |
|
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
192 |
|
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
193 |
lemmas rdmods [symmetric] = mod_minus_eq |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
194 |
mod_diff_left_eq mod_diff_right_eq mod_add_left_eq |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
195 |
mod_add_right_eq mod_mult_right_eq mod_mult_left_eq |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
196 |
|
65363 | 197 |
lemma mod_plus_right: "(a + x) mod m = (b + x) mod m \<longleftrightarrow> a mod m = b mod m" |
198 |
for a b m x :: nat |
|
199 |
by (induct x) (simp_all add: mod_Suc, arith) |
|
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
200 |
|
65363 | 201 |
lemma nat_minus_mod: "(n - n mod m) mod m = 0" |
202 |
for m n :: nat |
|
203 |
by (induct n) (simp_all add: mod_Suc) |
|
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
204 |
|
65363 | 205 |
lemmas nat_minus_mod_plus_right = |
206 |
trans [OF nat_minus_mod mod_0 [symmetric], |
|
207 |
THEN mod_plus_right [THEN iffD2], simplified] |
|
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
208 |
|
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
209 |
lemmas push_mods' = mod_add_eq |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
210 |
mod_mult_eq mod_diff_eq |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
211 |
mod_minus_eq |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
212 |
|
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
213 |
lemmas push_mods = push_mods' [THEN eq_reflection] |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
214 |
lemmas pull_mods = push_mods [symmetric] rdmods [THEN eq_reflection] |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
215 |
|
65363 | 216 |
lemma nat_mod_eq: "b < n \<Longrightarrow> a mod n = b mod n \<Longrightarrow> a mod n = b" |
217 |
for a b n :: nat |
|
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
218 |
by (induct a) auto |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
219 |
|
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
220 |
lemmas nat_mod_eq' = refl [THEN [2] nat_mod_eq] |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
221 |
|
65363 | 222 |
lemma nat_mod_lem: "0 < n \<Longrightarrow> b < n \<longleftrightarrow> b mod n = b" |
223 |
for b n :: nat |
|
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
224 |
apply safe |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
225 |
apply (erule nat_mod_eq') |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
226 |
apply (erule subst) |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
227 |
apply (erule mod_less_divisor) |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
228 |
done |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
229 |
|
65363 | 230 |
lemma mod_nat_add: "x < z \<Longrightarrow> y < z \<Longrightarrow> (x + y) mod z = (if x + y < z then x + y else x + y - z)" |
231 |
for x y z :: nat |
|
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
232 |
apply (rule nat_mod_eq) |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
233 |
apply auto |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
234 |
apply (rule trans) |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
235 |
apply (rule le_mod_geq) |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
236 |
apply simp |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
237 |
apply (rule nat_mod_eq') |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
238 |
apply arith |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
239 |
done |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
240 |
|
65363 | 241 |
lemma mod_nat_sub: "x < z \<Longrightarrow> (x - y) mod z = x - y" |
242 |
for x y :: nat |
|
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
243 |
by (rule nat_mod_eq') arith |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
244 |
|
65363 | 245 |
lemma int_mod_eq: "0 \<le> b \<Longrightarrow> b < n \<Longrightarrow> a mod n = b mod n \<Longrightarrow> a mod n = b" |
246 |
for a b n :: int |
|
55816
e8dd03241e86
cursory polishing: tuned proofs, tuned symbols, tuned headings
haftmann
parents:
55417
diff
changeset
|
247 |
by (metis mod_pos_pos_trivial) |
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
248 |
|
55816
e8dd03241e86
cursory polishing: tuned proofs, tuned symbols, tuned headings
haftmann
parents:
55417
diff
changeset
|
249 |
lemmas int_mod_eq' = mod_pos_pos_trivial (* FIXME delete *) |
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
250 |
|
66801 | 251 |
lemmas int_mod_le = zmod_le_nonneg_dividend (* FIXME: delete *) |
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
252 |
|
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
253 |
lemma mod_add_if_z: |
65363 | 254 |
"x < z \<Longrightarrow> y < z \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> z \<Longrightarrow> |
255 |
(x + y) mod z = (if x + y < z then x + y else x + y - z)" |
|
256 |
for x y z :: int |
|
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
257 |
by (auto intro: int_mod_eq) |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
258 |
|
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
259 |
lemma mod_sub_if_z: |
65363 | 260 |
"x < z \<Longrightarrow> y < z \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> z \<Longrightarrow> |
261 |
(x - y) mod z = (if y \<le> x then x - y else x - y + z)" |
|
262 |
for x y z :: int |
|
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
263 |
by (auto intro: int_mod_eq) |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
264 |
|
64246 | 265 |
lemmas zmde = mult_div_mod_eq [symmetric, THEN diff_eq_eq [THEN iffD2], symmetric] |
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
266 |
lemmas mcl = mult_cancel_left [THEN iffD1, THEN make_pos_rule] |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
267 |
|
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
268 |
(* already have this for naturals, div_mult_self1/2, but not for ints *) |
65363 | 269 |
lemma zdiv_mult_self: "m \<noteq> 0 \<Longrightarrow> (a + m * n) div m = a div m + n" |
270 |
for a m n :: int |
|
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
271 |
apply (rule mcl) |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
272 |
prefer 2 |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
273 |
apply (erule asm_rl) |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
274 |
apply (simp add: zmde ring_distribs) |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
275 |
done |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
276 |
|
65363 | 277 |
lemma mod_power_lem: "a > 1 \<Longrightarrow> a ^ n mod a ^ m = (if m \<le> n then 0 else a ^ n)" |
278 |
for a :: int |
|
66886 | 279 |
by (simp add: mod_eq_0_iff le_imp_power_dvd) |
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
280 |
|
65363 | 281 |
lemma pl_pl_rels: "a + b = c + d \<Longrightarrow> a \<ge> c \<and> b \<le> d \<or> a \<le> c \<and> b \<ge> d" |
282 |
for a b c d :: nat |
|
283 |
by arith |
|
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
284 |
|
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
55816
diff
changeset
|
285 |
lemmas pl_pl_rels' = add.commute [THEN [2] trans, THEN pl_pl_rels] |
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
286 |
|
65363 | 287 |
lemma minus_eq: "m - k = m \<longleftrightarrow> k = 0 \<or> m = 0" |
288 |
for k m :: nat |
|
289 |
by arith |
|
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
290 |
|
65363 | 291 |
lemma pl_pl_mm: "a + b = c + d \<Longrightarrow> a - c = d - b" |
292 |
for a b c d :: nat |
|
293 |
by arith |
|
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
294 |
|
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
55816
diff
changeset
|
295 |
lemmas pl_pl_mm' = add.commute [THEN [2] trans, THEN pl_pl_mm] |
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
296 |
|
64245
3d00821444fc
avoid references to lemmas designed for prover tools
haftmann
parents:
62390
diff
changeset
|
297 |
lemmas dme = div_mult_mod_eq |
66808
1907167b6038
elementary definition of division on natural numbers
haftmann
parents:
66801
diff
changeset
|
298 |
lemmas dtle = div_times_less_eq_dividend |
1907167b6038
elementary definition of division on natural numbers
haftmann
parents:
66801
diff
changeset
|
299 |
lemmas th2 = order_trans [OF order_refl [THEN [2] mult_le_mono] div_times_less_eq_dividend] |
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
300 |
|
65363 | 301 |
lemma td_gal: "0 < c \<Longrightarrow> a \<ge> b * c \<longleftrightarrow> a div c \<ge> b" |
302 |
for a b c :: nat |
|
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
303 |
apply safe |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
304 |
apply (erule (1) xtr4 [OF div_le_mono div_mult_self_is_m]) |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
305 |
apply (erule th2) |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
306 |
done |
65363 | 307 |
|
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
308 |
lemmas td_gal_lt = td_gal [simplified not_less [symmetric], simplified] |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
309 |
|
67120 | 310 |
lemmas div_mult_le = div_times_less_eq_dividend |
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
311 |
|
66808
1907167b6038
elementary definition of division on natural numbers
haftmann
parents:
66801
diff
changeset
|
312 |
lemmas sdl = div_nat_eqI |
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
313 |
|
65363 | 314 |
lemma given_quot: "f > 0 \<Longrightarrow> (f * l + (f - 1)) div f = l" |
315 |
for f l :: nat |
|
66808
1907167b6038
elementary definition of division on natural numbers
haftmann
parents:
66801
diff
changeset
|
316 |
by (rule div_nat_eqI) (simp_all) |
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
317 |
|
65363 | 318 |
lemma given_quot_alt: "f > 0 \<Longrightarrow> (l * f + f - Suc 0) div f = l" |
319 |
for f l :: nat |
|
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
320 |
apply (frule given_quot) |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
321 |
apply (rule trans) |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
322 |
prefer 2 |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
323 |
apply (erule asm_rl) |
65363 | 324 |
apply (rule_tac f="\<lambda>n. n div f" in arg_cong) |
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset
|
325 |
apply (simp add : ac_simps) |
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
326 |
done |
65363 | 327 |
|
328 |
lemma diff_mod_le: "a < d \<Longrightarrow> b dvd d \<Longrightarrow> a - a mod b \<le> d - b" |
|
329 |
for a b d :: nat |
|
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
330 |
apply (unfold dvd_def) |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
331 |
apply clarify |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
332 |
apply (case_tac k) |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
333 |
apply clarsimp |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
334 |
apply clarify |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
335 |
apply (cases "b > 0") |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
55816
diff
changeset
|
336 |
apply (drule mult.commute [THEN xtr1]) |
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
337 |
apply (frule (1) td_gal_lt [THEN iffD1]) |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
338 |
apply (clarsimp simp: le_simps) |
64246 | 339 |
apply (rule minus_mod_eq_mult_div [symmetric, THEN [2] xtr4]) |
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
340 |
apply (rule mult_mono) |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
341 |
apply auto |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
342 |
done |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
343 |
|
65363 | 344 |
lemma less_le_mult': "w * c < b * c \<Longrightarrow> 0 \<le> c \<Longrightarrow> (w + 1) * c \<le> b * c" |
345 |
for b c w :: int |
|
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
346 |
apply (rule mult_right_mono) |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
347 |
apply (rule zless_imp_add1_zle) |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
348 |
apply (erule (1) mult_right_less_imp_less) |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
349 |
apply assumption |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
350 |
done |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
351 |
|
65363 | 352 |
lemma less_le_mult: "w * c < b * c \<Longrightarrow> 0 \<le> c \<Longrightarrow> w * c + c \<le> b * c" |
353 |
for b c w :: int |
|
55816
e8dd03241e86
cursory polishing: tuned proofs, tuned symbols, tuned headings
haftmann
parents:
55417
diff
changeset
|
354 |
using less_le_mult' [of w c b] by (simp add: algebra_simps) |
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
355 |
|
65363 | 356 |
lemmas less_le_mult_minus = iffD2 [OF le_diff_eq less_le_mult, |
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
357 |
simplified left_diff_distrib] |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
358 |
|
65363 | 359 |
lemma gen_minus: "0 < n \<Longrightarrow> f n = f (Suc (n - 1))" |
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
360 |
by auto |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
361 |
|
65363 | 362 |
lemma mpl_lem: "j \<le> i \<Longrightarrow> k < j \<Longrightarrow> i - j + k < i" |
363 |
for i j k :: nat |
|
364 |
by arith |
|
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
365 |
|
65363 | 366 |
lemma nonneg_mod_div: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> (a mod b) \<and> 0 \<le> a div b" |
367 |
for a b :: int |
|
368 |
by (cases "b = 0") (auto intro: pos_imp_zdiv_nonneg_iff [THEN iffD2]) |
|
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
369 |
|
54872 | 370 |
declare iszero_0 [intro] |
371 |
||
65363 | 372 |
lemma min_pm [simp]: "min a b + (a - b) = a" |
373 |
for a b :: nat |
|
54872 | 374 |
by arith |
65363 | 375 |
|
376 |
lemma min_pm1 [simp]: "a - b + min a b = a" |
|
377 |
for a b :: nat |
|
54872 | 378 |
by arith |
379 |
||
65363 | 380 |
lemma rev_min_pm [simp]: "min b a + (a - b) = a" |
381 |
for a b :: nat |
|
54872 | 382 |
by arith |
383 |
||
65363 | 384 |
lemma rev_min_pm1 [simp]: "a - b + min b a = a" |
385 |
for a b :: nat |
|
54872 | 386 |
by arith |
387 |
||
65363 | 388 |
lemma min_minus [simp]: "min m (m - k) = m - k" |
389 |
for m k :: nat |
|
54872 | 390 |
by arith |
65363 | 391 |
|
392 |
lemma min_minus' [simp]: "min (m - k) m = m - k" |
|
393 |
for m k :: nat |
|
54872 | 394 |
by arith |
395 |
||
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
diff
changeset
|
396 |
end |