568
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1 |
theory IntEx2
|
790
|
2 |
imports "../QuotMain" "../QuotProd" Nat
|
604
|
3 |
(*uses
|
568
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
4 |
("Tools/numeral.ML")
|
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
5 |
("Tools/numeral_syntax.ML")
|
604
|
6 |
("Tools/int_arith.ML")*)
|
568
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
7 |
begin
|
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
8 |
|
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
9 |
fun
|
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
10 |
intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50)
|
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
11 |
where
|
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
12 |
"intrel (x, y) (u, v) = (x + v = u + y)"
|
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
13 |
|
766
df053507edba
renamed "quotient" command to "quotient_type"; needs new keyword file to be installed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
14 |
quotient_type int = "nat \<times> nat" / intrel
|
677
35fbace8d48d
naming in this file cannot be made to agree to the original (PROBLEM?)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
15 |
unfolding equivp_def
|
35fbace8d48d
naming in this file cannot be made to agree to the original (PROBLEM?)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
16 |
by (auto simp add: mem_def expand_fun_eq)
|
568
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
17 |
|
715
|
18 |
instantiation int :: "{zero, one, plus, uminus, minus, times, ord, abs, sgn}"
|
568
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
19 |
begin
|
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
20 |
|
711
|
21 |
ML {* @{term "0 \<Colon> int"} *}
|
568
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
22 |
|
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
23 |
quotient_definition
|
711
|
24 |
"0 \<Colon> int" as "(0\<Colon>nat, 0\<Colon>nat)"
|
705
|
25 |
|
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
26 |
quotient_definition
|
711
|
27 |
"1 \<Colon> int" as "(1\<Colon>nat, 0\<Colon>nat)"
|
568
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
28 |
|
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
29 |
fun
|
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
30 |
plus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
|
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
31 |
where
|
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
32 |
"plus_raw (x, y) (u, v) = (x + u, y + v)"
|
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
33 |
|
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
34 |
quotient_definition
|
711
|
35 |
"(op +) \<Colon> (int \<Rightarrow> int \<Rightarrow> int)" as "plus_raw"
|
568
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
36 |
|
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
37 |
fun
|
677
35fbace8d48d
naming in this file cannot be made to agree to the original (PROBLEM?)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
38 |
uminus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
|
568
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
39 |
where
|
677
35fbace8d48d
naming in this file cannot be made to agree to the original (PROBLEM?)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
40 |
"uminus_raw (x, y) = (y, x)"
|
568
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
41 |
|
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
42 |
quotient_definition
|
711
|
43 |
"(uminus \<Colon> (int \<Rightarrow> int))" as "uminus_raw"
|
568
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
44 |
|
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
45 |
definition
|
711
|
46 |
minus_int_def [code del]: "z - w = z + (-w\<Colon>int)"
|
568
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
47 |
|
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
48 |
fun
|
710
|
49 |
mult_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
|
568
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
50 |
where
|
710
|
51 |
"mult_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
|
568
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
52 |
|
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
53 |
quotient_definition
|
710
|
54 |
mult_int_def: "(op *) :: (int \<Rightarrow> int \<Rightarrow> int)" as "mult_raw"
|
568
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
55 |
|
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
56 |
fun
|
710
|
57 |
le_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
|
568
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
58 |
where
|
710
|
59 |
"le_raw (x, y) (u, v) = (x+v \<le> u+y)"
|
568
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
60 |
|
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
61 |
quotient_definition
|
710
|
62 |
le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" as "le_raw"
|
568
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
63 |
|
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
64 |
definition
|
570
|
65 |
less_int_def [code del]: "(z\<Colon>int) < w = (z \<le> w \<and> z \<noteq> w)"
|
568
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
66 |
|
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
67 |
definition
|
711
|
68 |
zabs_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"
|
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
69 |
|
568
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
70 |
definition
|
711
|
71 |
zsgn_def: "sgn (i\<Colon>int) = (if i = 0 then 0 else if 0 < i then 1 else - 1)"
|
568
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
72 |
|
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
73 |
instance ..
|
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
74 |
|
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
75 |
end
|
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
76 |
|
636
|
77 |
lemma plus_raw_rsp[quot_respect]:
|
568
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
78 |
shows "(op \<approx> ===> op \<approx> ===> op \<approx>) plus_raw plus_raw"
|
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
79 |
by auto
|
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
80 |
|
691
cc3c55f56116
Removed 'Presburger' as it introduces int & other minor cleaning in Int2.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
81 |
lemma uminus_raw_rsp[quot_respect]:
|
677
35fbace8d48d
naming in this file cannot be made to agree to the original (PROBLEM?)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
82 |
shows "(op \<approx> ===> op \<approx>) uminus_raw uminus_raw"
|
579
|
83 |
by auto
|
|
84 |
|
710
|
85 |
lemma mult_raw_fst:
|
672
|
86 |
assumes a: "x \<approx> z"
|
710
|
87 |
shows "mult_raw x y \<approx> mult_raw z y"
|
672
|
88 |
using a
|
|
89 |
apply(cases x, cases y, cases z)
|
710
|
90 |
apply(auto simp add: mult_raw.simps intrel.simps)
|
672
|
91 |
apply(rename_tac u v w x y z)
|
|
92 |
apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x")
|
|
93 |
apply(simp add: mult_ac)
|
|
94 |
apply(simp add: add_mult_distrib [symmetric])
|
|
95 |
done
|
|
96 |
|
710
|
97 |
lemma mult_raw_snd:
|
672
|
98 |
assumes a: "x \<approx> z"
|
710
|
99 |
shows "mult_raw y x \<approx> mult_raw y z"
|
672
|
100 |
using a
|
|
101 |
apply(cases x, cases y, cases z)
|
710
|
102 |
apply(auto simp add: mult_raw.simps intrel.simps)
|
672
|
103 |
apply(rename_tac u v w x y z)
|
|
104 |
apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x")
|
|
105 |
apply(simp add: mult_ac)
|
|
106 |
apply(simp add: add_mult_distrib [symmetric])
|
|
107 |
done
|
|
108 |
|
710
|
109 |
lemma mult_raw_rsp[quot_respect]:
|
|
110 |
shows "(op \<approx> ===> op \<approx> ===> op \<approx>) mult_raw mult_raw"
|
672
|
111 |
apply(simp only: fun_rel.simps)
|
|
112 |
apply(rule allI | rule impI)+
|
|
113 |
apply(rule equivp_transp[OF int_equivp])
|
710
|
114 |
apply(rule mult_raw_fst)
|
672
|
115 |
apply(assumption)
|
710
|
116 |
apply(rule mult_raw_snd)
|
672
|
117 |
apply(assumption)
|
|
118 |
done
|
568
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
119 |
|
710
|
120 |
lemma le_raw_rsp[quot_respect]:
|
|
121 |
shows "(op \<approx> ===> op \<approx> ===> op =) le_raw le_raw"
|
570
|
122 |
by auto
|
|
123 |
|
568
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
124 |
lemma plus_assoc_raw:
|
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
125 |
shows "plus_raw (plus_raw i j) k \<approx> plus_raw i (plus_raw j k)"
|
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
126 |
by (cases i, cases j, cases k) (simp)
|
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
127 |
|
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
128 |
lemma plus_sym_raw:
|
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
129 |
shows "plus_raw i j \<approx> plus_raw j i"
|
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
130 |
by (cases i, cases j) (simp)
|
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
131 |
|
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
132 |
lemma plus_zero_raw:
|
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
133 |
shows "plus_raw (0, 0) i \<approx> i"
|
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
134 |
by (cases i) (simp)
|
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
135 |
|
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
136 |
lemma plus_minus_zero_raw:
|
677
35fbace8d48d
naming in this file cannot be made to agree to the original (PROBLEM?)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
137 |
shows "plus_raw (uminus_raw i) i \<approx> (0, 0)"
|
568
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
138 |
by (cases i) (simp)
|
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
139 |
|
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
140 |
lemma times_assoc_raw:
|
710
|
141 |
shows "mult_raw (mult_raw i j) k \<approx> mult_raw i (mult_raw j k)"
|
568
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
142 |
by (cases i, cases j, cases k)
|
600
|
143 |
(simp add: algebra_simps)
|
568
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
144 |
|
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
145 |
lemma times_sym_raw:
|
710
|
146 |
shows "mult_raw i j \<approx> mult_raw j i"
|
600
|
147 |
by (cases i, cases j) (simp add: algebra_simps)
|
568
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
148 |
|
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
149 |
lemma times_one_raw:
|
710
|
150 |
shows "mult_raw (1, 0) i \<approx> i"
|
568
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
151 |
by (cases i) (simp)
|
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
152 |
|
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
153 |
lemma times_plus_comm_raw:
|
710
|
154 |
shows "mult_raw (plus_raw i j) k \<approx> plus_raw (mult_raw i k) (mult_raw j k)"
|
568
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
155 |
by (cases i, cases j, cases k)
|
600
|
156 |
(simp add: algebra_simps)
|
568
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
157 |
|
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
158 |
lemma one_zero_distinct:
|
579
|
159 |
shows "\<not> (0, 0) \<approx> ((1::nat), (0::nat))"
|
568
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
160 |
by simp
|
579
|
161 |
|
673
|
162 |
text{* The integers form a @{text comm_ring_1}*}
|
568
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
163 |
|
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
164 |
instance int :: comm_ring_1
|
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
165 |
proof
|
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
166 |
fix i j k :: int
|
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
167 |
show "(i + j) + k = i + (j + k)"
|
675
|
168 |
by (lifting plus_assoc_raw)
|
568
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
169 |
show "i + j = j + i"
|
654
02fd9de9d45e
tuned the examples and flagged the problematic cleaning lemmas in FSet
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
170 |
by (lifting plus_sym_raw)
|
568
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
171 |
show "0 + i = (i::int)"
|
654
02fd9de9d45e
tuned the examples and flagged the problematic cleaning lemmas in FSet
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
172 |
by (lifting plus_zero_raw)
|
568
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
173 |
show "- i + i = 0"
|
654
02fd9de9d45e
tuned the examples and flagged the problematic cleaning lemmas in FSet
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
174 |
by (lifting plus_minus_zero_raw)
|
568
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
175 |
show "i - j = i + - j"
|
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
176 |
by (simp add: minus_int_def)
|
568
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
177 |
show "(i * j) * k = i * (j * k)"
|
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
178 |
by (lifting times_assoc_raw)
|
568
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
179 |
show "i * j = j * i"
|
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
180 |
by (lifting times_sym_raw)
|
568
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
181 |
show "1 * i = i"
|
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
182 |
by (lifting times_one_raw)
|
568
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
183 |
show "(i + j) * k = i * k + j * k"
|
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
184 |
by (lifting times_plus_comm_raw)
|
568
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
185 |
show "0 \<noteq> (1::int)"
|
654
02fd9de9d45e
tuned the examples and flagged the problematic cleaning lemmas in FSet
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
186 |
by (lifting one_zero_distinct)
|
568
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
187 |
qed
|
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
188 |
|
675
|
189 |
lemma plus_raw_rsp_aux:
|
|
190 |
assumes a: "a \<approx> b" "c \<approx> d"
|
|
191 |
shows "plus_raw a c \<approx> plus_raw b d"
|
|
192 |
using a
|
|
193 |
by (cases a, cases b, cases c, cases d)
|
|
194 |
(simp)
|
674
|
195 |
|
673
|
196 |
lemma add:
|
719
|
197 |
"(abs_int (x,y)) + (abs_int (u,v)) =
|
|
198 |
(abs_int (x + u, y + v))"
|
790
|
199 |
apply(simp add: plus_int_def id_simps)
|
674
|
200 |
apply(fold plus_raw.simps)
|
|
201 |
apply(rule Quotient_rel_abs[OF Quotient_int])
|
675
|
202 |
apply(rule plus_raw_rsp_aux)
|
674
|
203 |
apply(simp_all add: rep_abs_rsp_left[OF Quotient_int])
|
|
204 |
done
|
570
|
205 |
|
682
|
206 |
definition int_of_nat_raw:
|
|
207 |
"int_of_nat_raw m = (m :: nat, 0 :: nat)"
|
679
fe64784b38c3
With int_of_nat as a quotient_def, lemmas about it can be easily lifted.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
208 |
|
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
209 |
quotient_definition
|
705
|
210 |
"int_of_nat :: nat \<Rightarrow> int" as "int_of_nat_raw"
|
679
fe64784b38c3
With int_of_nat as a quotient_def, lemmas about it can be easily lifted.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
211 |
|
682
|
212 |
lemma[quot_respect]:
|
|
213 |
shows "(op = ===> op \<approx>) int_of_nat_raw int_of_nat_raw"
|
679
fe64784b38c3
With int_of_nat as a quotient_def, lemmas about it can be easily lifted.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
214 |
by (simp add: equivp_reflp[OF int_equivp])
|
fe64784b38c3
With int_of_nat as a quotient_def, lemmas about it can be easily lifted.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
215 |
|
692
c9231c2903bc
Moved 'int_induct' to IntEx to keep IntEx2 being just theory of integers in order.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
216 |
lemma int_of_nat:
|
679
fe64784b38c3
With int_of_nat as a quotient_def, lemmas about it can be easily lifted.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
217 |
shows "of_nat m = int_of_nat m"
|
fe64784b38c3
With int_of_nat as a quotient_def, lemmas about it can be easily lifted.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
218 |
apply (induct m)
|
fe64784b38c3
With int_of_nat as a quotient_def, lemmas about it can be easily lifted.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
219 |
apply (simp_all add: zero_int_def one_int_def int_of_nat_def int_of_nat_raw add)
|
fe64784b38c3
With int_of_nat as a quotient_def, lemmas about it can be easily lifted.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
220 |
done
|
570
|
221 |
|
|
222 |
lemma le_antisym_raw:
|
710
|
223 |
shows "le_raw i j \<Longrightarrow> le_raw j i \<Longrightarrow> i \<approx> j"
|
570
|
224 |
by (cases i, cases j) (simp)
|
|
225 |
|
|
226 |
lemma le_refl_raw:
|
710
|
227 |
shows "le_raw i i"
|
570
|
228 |
by (cases i) (simp)
|
|
229 |
|
|
230 |
lemma le_trans_raw:
|
710
|
231 |
shows "le_raw i j \<Longrightarrow> le_raw j k \<Longrightarrow> le_raw i k"
|
570
|
232 |
by (cases i, cases j, cases k) (simp)
|
|
233 |
|
|
234 |
lemma le_cases_raw:
|
710
|
235 |
shows "le_raw i j \<or> le_raw j i"
|
570
|
236 |
by (cases i, cases j)
|
|
237 |
(simp add: linorder_linear)
|
|
238 |
|
|
239 |
instance int :: linorder
|
|
240 |
proof
|
|
241 |
fix i j k :: int
|
|
242 |
show antisym: "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j"
|
654
02fd9de9d45e
tuned the examples and flagged the problematic cleaning lemmas in FSet
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
243 |
by (lifting le_antisym_raw)
|
570
|
244 |
show "(i < j) = (i \<le> j \<and> \<not> j \<le> i)"
|
|
245 |
by (auto simp add: less_int_def dest: antisym)
|
|
246 |
show "i \<le> i"
|
654
02fd9de9d45e
tuned the examples and flagged the problematic cleaning lemmas in FSet
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
247 |
by (lifting le_refl_raw)
|
570
|
248 |
show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k"
|
654
02fd9de9d45e
tuned the examples and flagged the problematic cleaning lemmas in FSet
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
249 |
by (lifting le_trans_raw)
|
570
|
250 |
show "i \<le> j \<or> j \<le> i"
|
654
02fd9de9d45e
tuned the examples and flagged the problematic cleaning lemmas in FSet
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
251 |
by (lifting le_cases_raw)
|
570
|
252 |
qed
|
|
253 |
|
|
254 |
instantiation int :: distrib_lattice
|
|
255 |
begin
|
|
256 |
|
|
257 |
definition
|
|
258 |
"(inf \<Colon> int \<Rightarrow> int \<Rightarrow> int) = min"
|
|
259 |
|
|
260 |
definition
|
|
261 |
"(sup \<Colon> int \<Rightarrow> int \<Rightarrow> int) = max"
|
|
262 |
|
|
263 |
instance
|
|
264 |
by intro_classes
|
|
265 |
(auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1)
|
|
266 |
|
|
267 |
end
|
|
268 |
|
|
269 |
lemma le_plus_raw:
|
710
|
270 |
shows "le_raw i j \<Longrightarrow> le_raw (plus_raw k i) (plus_raw k j)"
|
570
|
271 |
by (cases i, cases j, cases k) (simp)
|
|
272 |
|
|
273 |
|
|
274 |
instance int :: pordered_cancel_ab_semigroup_add
|
|
275 |
proof
|
|
276 |
fix i j k :: int
|
|
277 |
show "i \<le> j \<Longrightarrow> k + i \<le> k + j"
|
654
02fd9de9d45e
tuned the examples and flagged the problematic cleaning lemmas in FSet
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
278 |
by (lifting le_plus_raw)
|
570
|
279 |
qed
|
|
280 |
|
673
|
281 |
abbreviation
|
710
|
282 |
"less_raw i j \<equiv> le_raw i j \<and> \<not>(i \<approx> j)"
|
673
|
283 |
|
675
|
284 |
lemma zmult_zless_mono2_lemma:
|
|
285 |
fixes i j::int
|
|
286 |
and k::nat
|
|
287 |
shows "i < j \<Longrightarrow> 0 < k \<Longrightarrow> of_nat k * i < of_nat k * j"
|
|
288 |
apply(induct "k")
|
|
289 |
apply(simp)
|
|
290 |
apply(case_tac "k = 0")
|
|
291 |
apply(simp_all add: left_distrib add_strict_mono)
|
|
292 |
done
|
673
|
293 |
|
679
fe64784b38c3
With int_of_nat as a quotient_def, lemmas about it can be easily lifted.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
294 |
lemma zero_le_imp_eq_int_raw:
|
fe64784b38c3
With int_of_nat as a quotient_def, lemmas about it can be easily lifted.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
295 |
fixes k::"(nat \<times> nat)"
|
682
|
296 |
shows "less_raw (0, 0) k \<Longrightarrow> (\<exists>n > 0. k \<approx> int_of_nat_raw n)"
|
679
fe64784b38c3
With int_of_nat as a quotient_def, lemmas about it can be easily lifted.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
297 |
apply(cases k)
|
fe64784b38c3
With int_of_nat as a quotient_def, lemmas about it can be easily lifted.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
298 |
apply(simp add:int_of_nat_raw)
|
fe64784b38c3
With int_of_nat as a quotient_def, lemmas about it can be easily lifted.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
299 |
apply(auto)
|
fe64784b38c3
With int_of_nat as a quotient_def, lemmas about it can be easily lifted.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
300 |
apply(rule_tac i="b" and j="a" in less_Suc_induct)
|
fe64784b38c3
With int_of_nat as a quotient_def, lemmas about it can be easily lifted.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
301 |
apply(auto)
|
fe64784b38c3
With int_of_nat as a quotient_def, lemmas about it can be easily lifted.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
302 |
done
|
fe64784b38c3
With int_of_nat as a quotient_def, lemmas about it can be easily lifted.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
303 |
|
fe64784b38c3
With int_of_nat as a quotient_def, lemmas about it can be easily lifted.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
304 |
lemma zero_le_imp_eq_int:
|
675
|
305 |
fixes k::int
|
692
c9231c2903bc
Moved 'int_induct' to IntEx to keep IntEx2 being just theory of integers in order.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
306 |
shows "0 < k \<Longrightarrow> \<exists>n > 0. k = of_nat n"
|
c9231c2903bc
Moved 'int_induct' to IntEx to keep IntEx2 being just theory of integers in order.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
307 |
unfolding less_int_def int_of_nat
|
682
|
308 |
by (lifting zero_le_imp_eq_int_raw)
|
570
|
309 |
|
675
|
310 |
lemma zmult_zless_mono2:
|
|
311 |
fixes i j k::int
|
|
312 |
assumes a: "i < j" "0 < k"
|
|
313 |
shows "k * i < k * j"
|
|
314 |
using a
|
682
|
315 |
using a
|
675
|
316 |
apply(drule_tac zero_le_imp_eq_int)
|
|
317 |
apply(auto simp add: zmult_zless_mono2_lemma)
|
|
318 |
done
|
570
|
319 |
|
|
320 |
text{*The integers form an ordered integral domain*}
|
|
321 |
instance int :: ordered_idom
|
|
322 |
proof
|
|
323 |
fix i j k :: int
|
|
324 |
show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"
|
675
|
325 |
by (rule zmult_zless_mono2)
|
570
|
326 |
show "\<bar>i\<bar> = (if i < 0 then -i else i)"
|
711
|
327 |
by (simp only: zabs_def)
|
570
|
328 |
show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
|
711
|
329 |
by (simp only: zsgn_def)
|
570
|
330 |
qed
|
|
331 |
|
|
332 |
instance int :: lordered_ring
|
|
333 |
proof
|
|
334 |
fix k :: int
|
|
335 |
show "abs k = sup k (- k)"
|
711
|
336 |
by (auto simp add: sup_int_def zabs_def less_minus_self_iff [symmetric])
|
570
|
337 |
qed
|
|
338 |
|
|
339 |
lemmas int_distrib =
|
|
340 |
left_distrib [of "z1::int" "z2" "w", standard]
|
|
341 |
right_distrib [of "w::int" "z1" "z2", standard]
|
|
342 |
left_diff_distrib [of "z1::int" "z2" "w", standard]
|
|
343 |
right_diff_distrib [of "w::int" "z1" "z2", standard]
|
|
344 |
|
|
345 |
|
|
346 |
subsection {* Embedding of the Integers into any @{text ring_1}: @{text of_int}*}
|
|
347 |
|
|
348 |
(*
|
|
349 |
context ring_1
|
|
350 |
begin
|
|
351 |
|
|
352 |
|
|
353 |
definition
|
|
354 |
of_int :: "int \<Rightarrow> 'a"
|
|
355 |
where
|
|
356 |
"of_int
|
|
357 |
*)
|
|
358 |
|
|
359 |
|
|
360 |
subsection {* Binary representation *}
|
|
361 |
|
|
362 |
text {*
|
|
363 |
This formalization defines binary arithmetic in terms of the integers
|
|
364 |
rather than using a datatype. This avoids multiple representations (leading
|
|
365 |
zeroes, etc.) See @{text "ZF/Tools/twos-compl.ML"}, function @{text
|
|
366 |
int_of_binary}, for the numerical interpretation.
|
|
367 |
|
|
368 |
The representation expects that @{text "(m mod 2)"} is 0 or 1,
|
|
369 |
even if m is negative;
|
|
370 |
For instance, @{text "-5 div 2 = -3"} and @{text "-5 mod 2 = 1"}; thus
|
|
371 |
@{text "-5 = (-3)*2 + 1"}.
|
|
372 |
|
|
373 |
This two's complement binary representation derives from the paper
|
|
374 |
"An Efficient Representation of Arithmetic for Term Rewriting" by
|
|
375 |
Dave Cohen and Phil Watson, Rewriting Techniques and Applications,
|
|
376 |
Springer LNCS 488 (240-251), 1991.
|
|
377 |
*}
|
|
378 |
|
|
379 |
subsubsection {* The constructors @{term Bit0}, @{term Bit1}, @{term Pls} and @{term Min} *}
|
|
380 |
|
|
381 |
definition
|
|
382 |
Pls :: int where
|
|
383 |
[code del]: "Pls = 0"
|
|
384 |
|
|
385 |
definition
|
|
386 |
Min :: int where
|
|
387 |
[code del]: "Min = - 1"
|
|
388 |
|
|
389 |
definition
|
|
390 |
Bit0 :: "int \<Rightarrow> int" where
|
|
391 |
[code del]: "Bit0 k = k + k"
|
|
392 |
|
|
393 |
definition
|
|
394 |
Bit1 :: "int \<Rightarrow> int" where
|
|
395 |
[code del]: "Bit1 k = 1 + k + k"
|
|
396 |
|
|
397 |
class number = -- {* for numeric types: nat, int, real, \dots *}
|
|
398 |
fixes number_of :: "int \<Rightarrow> 'a"
|
|
399 |
|
600
|
400 |
(*use "~~/src/HOL/Tools/numeral.ML"
|
570
|
401 |
|
|
402 |
syntax
|
|
403 |
"_Numeral" :: "num_const \<Rightarrow> 'a" ("_")
|
|
404 |
|
|
405 |
use "~~/src/HOL/Tools/numeral_syntax.ML"
|
600
|
406 |
|
570
|
407 |
setup NumeralSyntax.setup
|
|
408 |
|
|
409 |
abbreviation
|
|
410 |
"Numeral0 \<equiv> number_of Pls"
|
|
411 |
|
|
412 |
abbreviation
|
|
413 |
"Numeral1 \<equiv> number_of (Bit1 Pls)"
|
|
414 |
|
|
415 |
lemma Let_number_of [simp]: "Let (number_of v) f = f (number_of v)"
|
|
416 |
-- {* Unfold all @{text let}s involving constants *}
|
|
417 |
unfolding Let_def ..
|
|
418 |
|
|
419 |
definition
|
|
420 |
succ :: "int \<Rightarrow> int" where
|
|
421 |
[code del]: "succ k = k + 1"
|
|
422 |
|
|
423 |
definition
|
|
424 |
pred :: "int \<Rightarrow> int" where
|
|
425 |
[code del]: "pred k = k - 1"
|
|
426 |
|
|
427 |
lemmas
|
|
428 |
max_number_of [simp] = max_def
|
|
429 |
[of "number_of u" "number_of v", standard, simp]
|
|
430 |
and
|
|
431 |
min_number_of [simp] = min_def
|
|
432 |
[of "number_of u" "number_of v", standard, simp]
|
|
433 |
-- {* unfolding @{text minx} and @{text max} on numerals *}
|
|
434 |
|
|
435 |
lemmas numeral_simps =
|
|
436 |
succ_def pred_def Pls_def Min_def Bit0_def Bit1_def
|
|
437 |
|
|
438 |
text {* Removal of leading zeroes *}
|
|
439 |
|
|
440 |
lemma Bit0_Pls [simp, code_post]:
|
|
441 |
"Bit0 Pls = Pls"
|
|
442 |
unfolding numeral_simps by simp
|
|
443 |
|
|
444 |
lemma Bit1_Min [simp, code_post]:
|
|
445 |
"Bit1 Min = Min"
|
|
446 |
unfolding numeral_simps by simp
|
|
447 |
|
|
448 |
lemmas normalize_bin_simps =
|
|
449 |
Bit0_Pls Bit1_Min
|
600
|
450 |
*)
|
601
|
451 |
|
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
452 |
end
|