author | paulson |
Tue, 15 Sep 1998 15:06:29 +0200 | |
changeset 5491 | 22f8331cdf47 |
parent 5454 | a0b16470c502 |
child 5509 | c38cc427976c |
permissions | -rw-r--r-- |
1465 | 1 |
(* Title: Integ.ML |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
2 |
ID: $Id$ |
2215 | 3 |
Authors: Lawrence C Paulson, Cambridge University Computer Laboratory |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
4 |
Copyright 1993 University of Cambridge |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
5 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
6 |
The integers as equivalence classes over nat*nat. |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
7 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
8 |
Could also prove... |
5491 | 9 |
"znegative(z) ==> $# zmagnitude(z) = - z" |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
10 |
"~ znegative(z) ==> $# zmagnitude(z) = z" |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
11 |
*) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
12 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
13 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
14 |
(*** Proving that intrel is an equivalence relation ***) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
15 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
16 |
val eqa::eqb::prems = goal Arith.thy |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
17 |
"[| (x1::nat) + y2 = x2 + y1; x2 + y3 = x3 + y2 |] ==> \ |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
18 |
\ x1 + y3 = x3 + y1"; |
4473 | 19 |
by (res_inst_tac [("k1","x2")] (add_left_cancel RS iffD1) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
20 |
by (rtac (add_left_commute RS trans) 1); |
2036 | 21 |
by (stac eqb 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
22 |
by (rtac (add_left_commute RS trans) 1); |
2036 | 23 |
by (stac eqa 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
24 |
by (rtac (add_left_commute) 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
25 |
qed "integ_trans_lemma"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
26 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
27 |
(** Natural deduction for intrel **) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
28 |
|
5316 | 29 |
Goalw [intrel_def] "[| x1+y2 = x2+y1|] ==> ((x1,y1),(x2,y2)): intrel"; |
30 |
by (Fast_tac 1); |
|
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
31 |
qed "intrelI"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
32 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
33 |
(*intrelE is hard to derive because fast_tac tries hyp_subst_tac so soon*) |
5069 | 34 |
Goalw [intrel_def] |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
35 |
"p: intrel --> (EX x1 y1 x2 y2. \ |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset
|
36 |
\ p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1)"; |
1894 | 37 |
by (Fast_tac 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
38 |
qed "intrelE_lemma"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
39 |
|
5316 | 40 |
val [major,minor] = Goal |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
41 |
"[| p: intrel; \ |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset
|
42 |
\ !!x1 y1 x2 y2. [| p = ((x1,y1),(x2,y2)); x1+y2 = x2+y1|] ==> Q |] \ |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
43 |
\ ==> Q"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
44 |
by (cut_facts_tac [major RS (intrelE_lemma RS mp)] 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
45 |
by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1)); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
46 |
qed "intrelE"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
47 |
|
1894 | 48 |
AddSIs [intrelI]; |
49 |
AddSEs [intrelE]; |
|
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
50 |
|
5069 | 51 |
Goal "((x1,y1),(x2,y2)): intrel = (x1+y2 = x2+y1)"; |
1894 | 52 |
by (Fast_tac 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
53 |
qed "intrel_iff"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
54 |
|
5069 | 55 |
Goal "(x,x): intrel"; |
2036 | 56 |
by (stac surjective_pairing 1 THEN rtac (refl RS intrelI) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
57 |
qed "intrel_refl"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
58 |
|
5069 | 59 |
Goalw [equiv_def, refl_def, sym_def, trans_def] |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
60 |
"equiv {x::(nat*nat).True} intrel"; |
4089 | 61 |
by (fast_tac (claset() addSIs [intrel_refl] |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
62 |
addSEs [sym, integ_trans_lemma]) 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
63 |
qed "equiv_intrel"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
64 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
65 |
val equiv_intrel_iff = |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
66 |
[TrueI, TrueI] MRS |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
67 |
([CollectI, CollectI] MRS |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
68 |
(equiv_intrel RS eq_equiv_class_iff)); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
69 |
|
5069 | 70 |
Goalw [Integ_def,intrel_def,quotient_def] "intrel^^{(x,y)}:Integ"; |
1894 | 71 |
by (Fast_tac 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
72 |
qed "intrel_in_integ"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
73 |
|
5069 | 74 |
Goal "inj_on Abs_Integ Integ"; |
4831 | 75 |
by (rtac inj_on_inverseI 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
76 |
by (etac Abs_Integ_inverse 1); |
4831 | 77 |
qed "inj_on_Abs_Integ"; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
78 |
|
4831 | 79 |
Addsimps [equiv_intrel_iff, inj_on_Abs_Integ RS inj_on_iff, |
1465 | 80 |
intrel_iff, intrel_in_integ, Abs_Integ_inverse]; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
81 |
|
5069 | 82 |
Goal "inj(Rep_Integ)"; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
83 |
by (rtac inj_inverseI 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
84 |
by (rtac Rep_Integ_inverse 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
85 |
qed "inj_Rep_Integ"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
86 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
87 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
88 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
89 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
90 |
(** znat: the injection from nat to Integ **) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
91 |
|
5069 | 92 |
Goal "inj(znat)"; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
93 |
by (rtac injI 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
94 |
by (rewtac znat_def); |
4831 | 95 |
by (dtac (inj_on_Abs_Integ RS inj_onD) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
96 |
by (REPEAT (rtac intrel_in_integ 1)); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
97 |
by (dtac eq_equiv_class 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
98 |
by (rtac equiv_intrel 1); |
1894 | 99 |
by (Fast_tac 1); |
4162 | 100 |
by Safe_tac; |
1266 | 101 |
by (Asm_full_simp_tac 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
102 |
qed "inj_znat"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
103 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
104 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
105 |
(**** zminus: unary negation on Integ ****) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
106 |
|
5069 | 107 |
Goalw [congruent_def] |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset
|
108 |
"congruent intrel (%p. split (%x y. intrel^^{(y,x)}) p)"; |
4162 | 109 |
by Safe_tac; |
4089 | 110 |
by (asm_simp_tac (simpset() addsimps add_ac) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
111 |
qed "zminus_congruent"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
112 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
113 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
114 |
(*Resolve th against the corresponding facts for zminus*) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
115 |
val zminus_ize = RSLIST [equiv_intrel, zminus_congruent]; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
116 |
|
5069 | 117 |
Goalw [zminus_def] |
5491 | 118 |
"- Abs_Integ(intrel^^{(x,y)}) = Abs_Integ(intrel ^^ {(y,x)})"; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
119 |
by (res_inst_tac [("f","Abs_Integ")] arg_cong 1); |
4089 | 120 |
by (simp_tac (simpset() addsimps |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
121 |
[intrel_in_integ RS Abs_Integ_inverse,zminus_ize UN_equiv_class]) 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
122 |
qed "zminus"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
123 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
124 |
(*by lcp*) |
5316 | 125 |
val [prem] = Goal "(!!x y. z = Abs_Integ(intrel^^{(x,y)}) ==> P) ==> P"; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
126 |
by (res_inst_tac [("x1","z")] |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
127 |
(rewrite_rule [Integ_def] Rep_Integ RS quotientE) 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
128 |
by (dres_inst_tac [("f","Abs_Integ")] arg_cong 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
129 |
by (res_inst_tac [("p","x")] PairE 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
130 |
by (rtac prem 1); |
4089 | 131 |
by (asm_full_simp_tac (simpset() addsimps [Rep_Integ_inverse]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
132 |
qed "eq_Abs_Integ"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
133 |
|
5491 | 134 |
Goal "- (- z) = (z::int)"; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
135 |
by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
4089 | 136 |
by (asm_simp_tac (simpset() addsimps [zminus]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
137 |
qed "zminus_zminus"; |
5491 | 138 |
Addsimps [zminus_zminus]; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
139 |
|
5491 | 140 |
Goal "inj(uminus::int=>int)"; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
141 |
by (rtac injI 1); |
5491 | 142 |
by (dres_inst_tac [("f","uminus")] arg_cong 1); |
143 |
by (Asm_full_simp_tac 1); |
|
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
144 |
qed "inj_zminus"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
145 |
|
5491 | 146 |
Goalw [znat_def] "- ($# 0) = $# 0"; |
4089 | 147 |
by (simp_tac (simpset() addsimps [zminus]) 1); |
5491 | 148 |
qed "zminus_nat0"; |
149 |
||
150 |
Addsimps [zminus_nat0]; |
|
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
151 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
152 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
153 |
(**** znegative: the test for negative integers ****) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
154 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
155 |
|
5316 | 156 |
Goalw [znegative_def, znat_def] "~ znegative($# n)"; |
1266 | 157 |
by (Simp_tac 1); |
4162 | 158 |
by Safe_tac; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
159 |
qed "not_znegative_znat"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
160 |
|
5491 | 161 |
Goalw [znegative_def, znat_def] "znegative(- $# Suc(n))"; |
4089 | 162 |
by (simp_tac (simpset() addsimps [zminus]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
163 |
qed "znegative_zminus_znat"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
164 |
|
5491 | 165 |
Addsimps [znegative_zminus_znat, not_znegative_znat]; |
166 |
||
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
167 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
168 |
(**** zmagnitude: magnitide of an integer, as a natural number ****) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
169 |
|
5069 | 170 |
Goalw [congruent_def] |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset
|
171 |
"congruent intrel (split (%x y. intrel^^{((y-x) + (x-(y::nat)),0)}))"; |
4162 | 172 |
by Safe_tac; |
1266 | 173 |
by (Asm_simp_tac 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
174 |
by (etac rev_mp 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
175 |
by (res_inst_tac [("m","x1"),("n","y1")] diff_induct 1); |
4089 | 176 |
by (asm_simp_tac (simpset() addsimps [inj_Suc RS inj_eq]) 3); |
177 |
by (asm_simp_tac (simpset() addsimps [diff_add_inverse,diff_add_0]) 2); |
|
1266 | 178 |
by (Asm_simp_tac 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
179 |
by (rtac impI 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
180 |
by (etac subst 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
181 |
by (res_inst_tac [("m1","x")] (add_commute RS ssubst) 1); |
4089 | 182 |
by (asm_simp_tac (simpset() addsimps [diff_add_inverse,diff_add_0]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
183 |
qed "zmagnitude_congruent"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
184 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
185 |
(*Resolve th against the corresponding facts for zmagnitude*) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
186 |
val zmagnitude_ize = RSLIST [equiv_intrel, zmagnitude_congruent]; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
187 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
188 |
|
5069 | 189 |
Goalw [zmagnitude_def] |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset
|
190 |
"zmagnitude (Abs_Integ(intrel^^{(x,y)})) = \ |
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset
|
191 |
\ Abs_Integ(intrel^^{((y - x) + (x - y),0)})"; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
192 |
by (res_inst_tac [("f","Abs_Integ")] arg_cong 1); |
4089 | 193 |
by (asm_simp_tac (simpset() addsimps [zmagnitude_ize UN_equiv_class]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
194 |
qed "zmagnitude"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
195 |
|
5069 | 196 |
Goalw [znat_def] "zmagnitude($# n) = $#n"; |
4089 | 197 |
by (asm_simp_tac (simpset() addsimps [zmagnitude]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
198 |
qed "zmagnitude_znat"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
199 |
|
5491 | 200 |
Goalw [znat_def] "zmagnitude(- $# n) = $#n"; |
4089 | 201 |
by (asm_simp_tac (simpset() addsimps [zmagnitude, zminus]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
202 |
qed "zmagnitude_zminus_znat"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
203 |
|
5491 | 204 |
Addsimps [zmagnitude_znat, zmagnitude_zminus_znat]; |
205 |
||
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
206 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
207 |
(**** zadd: addition on Integ ****) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
208 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
209 |
(** Congruence property for addition **) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
210 |
|
5069 | 211 |
Goalw [congruent2_def] |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
212 |
"congruent2 intrel (%p1 p2. \ |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset
|
213 |
\ split (%x1 y1. split (%x2 y2. intrel^^{(x1+x2, y1+y2)}) p2) p1)"; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
214 |
(*Proof via congruent2_commuteI seems longer*) |
4162 | 215 |
by Safe_tac; |
4089 | 216 |
by (asm_simp_tac (simpset() addsimps [add_assoc]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
217 |
(*The rest should be trivial, but rearranging terms is hard*) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
218 |
by (res_inst_tac [("x1","x1a")] (add_left_commute RS ssubst) 1); |
4089 | 219 |
by (asm_simp_tac (simpset() addsimps [add_assoc RS sym]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
220 |
qed "zadd_congruent2"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
221 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
222 |
(*Resolve th against the corresponding facts for zadd*) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
223 |
val zadd_ize = RSLIST [equiv_intrel, zadd_congruent2]; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
224 |
|
5069 | 225 |
Goalw [zadd_def] |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset
|
226 |
"Abs_Integ(intrel^^{(x1,y1)}) + Abs_Integ(intrel^^{(x2,y2)}) = \ |
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset
|
227 |
\ Abs_Integ(intrel^^{(x1+x2, y1+y2)})"; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
228 |
by (asm_simp_tac |
4089 | 229 |
(simpset() addsimps [zadd_ize UN_equiv_class2]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
230 |
qed "zadd"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
231 |
|
5491 | 232 |
Goal "- (z + w) = - z + - (w::int)"; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
233 |
by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
234 |
by (res_inst_tac [("z","w")] eq_Abs_Integ 1); |
4089 | 235 |
by (asm_simp_tac (simpset() addsimps [zminus,zadd]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
236 |
qed "zminus_zadd_distrib"; |
5491 | 237 |
Addsimps [zminus_zadd_distrib]; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
238 |
|
5069 | 239 |
Goal "(z::int) + w = w + z"; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
240 |
by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
241 |
by (res_inst_tac [("z","w")] eq_Abs_Integ 1); |
4089 | 242 |
by (asm_simp_tac (simpset() addsimps (add_ac @ [zadd])) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
243 |
qed "zadd_commute"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
244 |
|
5069 | 245 |
Goal "((z1::int) + z2) + z3 = z1 + (z2 + z3)"; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
246 |
by (res_inst_tac [("z","z1")] eq_Abs_Integ 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
247 |
by (res_inst_tac [("z","z2")] eq_Abs_Integ 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
248 |
by (res_inst_tac [("z","z3")] eq_Abs_Integ 1); |
4089 | 249 |
by (asm_simp_tac (simpset() addsimps [zadd, add_assoc]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
250 |
qed "zadd_assoc"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
251 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
252 |
(*For AC rewriting*) |
5069 | 253 |
Goal "(x::int)+(y+z)=y+(x+z)"; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
254 |
by (rtac (zadd_commute RS trans) 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
255 |
by (rtac (zadd_assoc RS trans) 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
256 |
by (rtac (zadd_commute RS arg_cong) 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
257 |
qed "zadd_left_commute"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
258 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
259 |
(*Integer addition is an AC operator*) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
260 |
val zadd_ac = [zadd_assoc,zadd_commute,zadd_left_commute]; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
261 |
|
5491 | 262 |
Goalw [znat_def] "($#m) + ($#n) = $# (m + n)"; |
263 |
by (simp_tac (simpset() addsimps [zadd]) 1); |
|
264 |
qed "add_znat"; |
|
265 |
||
266 |
Goal "$# (Suc m) = $# 1 + ($# m)"; |
|
267 |
by (simp_tac (simpset() addsimps [add_znat]) 1); |
|
268 |
qed "znat_Suc"; |
|
269 |
||
270 |
Goalw [znat_def] "$# 0 + z = z"; |
|
271 |
by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
|
4089 | 272 |
by (asm_simp_tac (simpset() addsimps [zadd]) 1); |
5491 | 273 |
qed "zadd_nat0"; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
274 |
|
5491 | 275 |
Goal "z + $# 0 = z"; |
276 |
by (rtac (zadd_commute RS trans) 1); |
|
277 |
by (rtac zadd_nat0 1); |
|
278 |
qed "zadd_nat0_right"; |
|
279 |
||
280 |
Goalw [znat_def] "z + (- z) = $# 0"; |
|
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
281 |
by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
4089 | 282 |
by (asm_simp_tac (simpset() addsimps [zminus, zadd, add_commute]) 1); |
5491 | 283 |
qed "zadd_zminus_inverse_nat"; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
284 |
|
5491 | 285 |
Goal "(- z) + z = $# 0"; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
286 |
by (rtac (zadd_commute RS trans) 1); |
5491 | 287 |
by (rtac zadd_zminus_inverse_nat 1); |
288 |
qed "zadd_zminus_inverse_nat2"; |
|
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
289 |
|
5491 | 290 |
Addsimps [zadd_nat0, zadd_nat0_right, |
291 |
zadd_zminus_inverse_nat, zadd_zminus_inverse_nat2]; |
|
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
292 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
293 |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
294 |
(** Lemmas **) |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
295 |
|
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
296 |
qed_goal "zadd_assoc_cong" Integ.thy |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
297 |
"!!z. (z::int) + v = z' + v' ==> z + (v + w) = z' + (v' + w)" |
4089 | 298 |
(fn _ => [(asm_simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1)]); |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
299 |
|
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
300 |
qed_goal "zadd_assoc_swap" Integ.thy "(z::int) + (v + w) = v + (z + w)" |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
301 |
(fn _ => [(REPEAT (ares_tac [zadd_commute RS zadd_assoc_cong] 1))]); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
302 |
|
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
303 |
|
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
304 |
(*Need properties of subtraction? Or use $- just as an abbreviation!*) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
305 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
306 |
(**** zmult: multiplication on Integ ****) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
307 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
308 |
(** Congruence property for multiplication **) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
309 |
|
5069 | 310 |
Goal "((k::nat) + l) + (m + n) = (k + m) + (n + l)"; |
4089 | 311 |
by (simp_tac (simpset() addsimps add_ac) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
312 |
qed "zmult_congruent_lemma"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
313 |
|
5278 | 314 |
Goal "congruent2 intrel (%p1 p2. \ |
1465 | 315 |
\ split (%x1 y1. split (%x2 y2. \ |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset
|
316 |
\ intrel^^{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)"; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
317 |
by (rtac (equiv_intrel RS congruent2_commuteI) 1); |
5491 | 318 |
by (pair_tac "w" 2); |
319 |
by (rename_tac "z1 z2" 2); |
|
320 |
by Safe_tac; |
|
321 |
by (rewtac split_def); |
|
322 |
by (simp_tac (simpset() addsimps add_ac@mult_ac) 1); |
|
4089 | 323 |
by (asm_simp_tac (simpset() delsimps [equiv_intrel_iff] |
1266 | 324 |
addsimps add_ac@mult_ac) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
325 |
by (rtac (intrelI RS(equiv_intrel RS equiv_class_eq)) 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
326 |
by (rtac (zmult_congruent_lemma RS trans) 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
327 |
by (rtac (zmult_congruent_lemma RS trans RS sym) 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
328 |
by (rtac (zmult_congruent_lemma RS trans RS sym) 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
329 |
by (rtac (zmult_congruent_lemma RS trans RS sym) 1); |
4089 | 330 |
by (asm_simp_tac (simpset() addsimps [add_mult_distrib RS sym]) 1); |
331 |
by (asm_simp_tac (simpset() addsimps add_ac@mult_ac) 1); |
|
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
332 |
qed "zmult_congruent2"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
333 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
334 |
(*Resolve th against the corresponding facts for zmult*) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
335 |
val zmult_ize = RSLIST [equiv_intrel, zmult_congruent2]; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
336 |
|
5069 | 337 |
Goalw [zmult_def] |
1465 | 338 |
"Abs_Integ((intrel^^{(x1,y1)})) * Abs_Integ((intrel^^{(x2,y2)})) = \ |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset
|
339 |
\ Abs_Integ(intrel ^^ {(x1*x2 + y1*y2, x1*y2 + y1*x2)})"; |
4089 | 340 |
by (simp_tac (simpset() addsimps [zmult_ize UN_equiv_class2]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
341 |
qed "zmult"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
342 |
|
5491 | 343 |
Goal "(- z) * w = - (z * (w::int))"; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
344 |
by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
345 |
by (res_inst_tac [("z","w")] eq_Abs_Integ 1); |
4089 | 346 |
by (asm_simp_tac (simpset() addsimps ([zminus, zmult] @ add_ac)) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
347 |
qed "zmult_zminus"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
348 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
349 |
|
5491 | 350 |
Goal "(- z) * (- w) = (z * (w::int))"; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
351 |
by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
352 |
by (res_inst_tac [("z","w")] eq_Abs_Integ 1); |
4089 | 353 |
by (asm_simp_tac (simpset() addsimps ([zminus, zmult] @ add_ac)) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
354 |
qed "zmult_zminus_zminus"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
355 |
|
5069 | 356 |
Goal "(z::int) * w = w * z"; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
357 |
by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
358 |
by (res_inst_tac [("z","w")] eq_Abs_Integ 1); |
4089 | 359 |
by (asm_simp_tac (simpset() addsimps ([zmult] @ add_ac @ mult_ac)) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
360 |
qed "zmult_commute"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
361 |
|
5069 | 362 |
Goal "((z1::int) * z2) * z3 = z1 * (z2 * z3)"; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
363 |
by (res_inst_tac [("z","z1")] eq_Abs_Integ 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
364 |
by (res_inst_tac [("z","z2")] eq_Abs_Integ 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
365 |
by (res_inst_tac [("z","z3")] eq_Abs_Integ 1); |
4089 | 366 |
by (asm_simp_tac (simpset() addsimps ([add_mult_distrib2,zmult] @ |
2036 | 367 |
add_ac @ mult_ac)) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
368 |
qed "zmult_assoc"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
369 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
370 |
(*For AC rewriting*) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
371 |
qed_goal "zmult_left_commute" Integ.thy |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
372 |
"(z1::int)*(z2*z3) = z2*(z1*z3)" |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
373 |
(fn _ => [rtac (zmult_commute RS trans) 1, rtac (zmult_assoc RS trans) 1, |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
374 |
rtac (zmult_commute RS arg_cong) 1]); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
375 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
376 |
(*Integer multiplication is an AC operator*) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
377 |
val zmult_ac = [zmult_assoc, zmult_commute, zmult_left_commute]; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
378 |
|
5069 | 379 |
Goal "((z1::int) + z2) * w = (z1 * w) + (z2 * w)"; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
380 |
by (res_inst_tac [("z","z1")] eq_Abs_Integ 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
381 |
by (res_inst_tac [("z","z2")] eq_Abs_Integ 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
382 |
by (res_inst_tac [("z","w")] eq_Abs_Integ 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
383 |
by (asm_simp_tac |
4089 | 384 |
(simpset() addsimps ([add_mult_distrib2, zadd, zmult] @ |
2036 | 385 |
add_ac @ mult_ac)) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
386 |
qed "zadd_zmult_distrib"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
387 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
388 |
val zmult_commute'= read_instantiate [("z","w")] zmult_commute; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
389 |
|
5491 | 390 |
Goal "w * (- z) = - (w * (z::int))"; |
4089 | 391 |
by (simp_tac (simpset() addsimps [zmult_commute', zmult_zminus]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
392 |
qed "zmult_zminus_right"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
393 |
|
5069 | 394 |
Goal "(w::int) * (z1 + z2) = (w * z1) + (w * z2)"; |
4089 | 395 |
by (simp_tac (simpset() addsimps [zmult_commute',zadd_zmult_distrib]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
396 |
qed "zadd_zmult_distrib2"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
397 |
|
5491 | 398 |
Goalw [znat_def] "$# 0 * z = $# 0"; |
399 |
by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
|
400 |
by (asm_simp_tac (simpset() addsimps [zmult]) 1); |
|
401 |
qed "zmult_nat0"; |
|
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
402 |
|
5491 | 403 |
Goalw [znat_def] "$# 1 * z = z"; |
404 |
by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
|
405 |
by (asm_simp_tac (simpset() addsimps [zmult]) 1); |
|
406 |
qed "zmult_nat1"; |
|
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
407 |
|
5491 | 408 |
Goal "z * $# 0 = $# 0"; |
409 |
by (rtac ([zmult_commute, zmult_nat0] MRS trans) 1); |
|
410 |
qed "zmult_nat0_right"; |
|
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
411 |
|
5491 | 412 |
Goal "z * $# 1 = z"; |
413 |
by (rtac ([zmult_commute, zmult_nat1] MRS trans) 1); |
|
414 |
qed "zmult_nat1_right"; |
|
415 |
||
416 |
Addsimps [zmult_nat0, zmult_nat0_right, zmult_nat1, zmult_nat1_right]; |
|
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
417 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
418 |
|
5491 | 419 |
Goal "(- z = w) = (z = - (w::int))"; |
4162 | 420 |
by Safe_tac; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
421 |
by (rtac (zminus_zminus RS sym) 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
422 |
by (rtac zminus_zminus 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
423 |
qed "zminus_exchange"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
424 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
425 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
426 |
(* Theorems about less and less_equal *) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
427 |
|
5491 | 428 |
(*This lemma allows direct proofs of other <-properties*) |
5069 | 429 |
Goalw [zless_def, znegative_def, zdiff_def, znat_def] |
5491 | 430 |
"(w < z) = (EX n. z = w + $#(Suc n))"; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
431 |
by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
432 |
by (res_inst_tac [("z","w")] eq_Abs_Integ 1); |
5491 | 433 |
by (Clarify_tac 1); |
4089 | 434 |
by (asm_full_simp_tac (simpset() addsimps [zadd, zminus]) 1); |
435 |
by (safe_tac (claset() addSDs [less_eq_Suc_add])); |
|
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
436 |
by (res_inst_tac [("x","k")] exI 1); |
5491 | 437 |
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps add_ac))); |
438 |
qed "zless_iff_Suc_zadd"; |
|
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
439 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
440 |
Goal "[| z1<z2; z2<z3 |] ==> z1 < (z3::int)"; |
5491 | 441 |
by (auto_tac (claset(), |
442 |
simpset() addsimps [zless_iff_Suc_zadd, zadd_assoc, |
|
443 |
add_znat])); |
|
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
444 |
qed "zless_trans"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
445 |
|
5316 | 446 |
Goal "!!w::int. z<w ==> ~w<z"; |
5491 | 447 |
by (safe_tac (claset() addSDs [zless_iff_Suc_zadd RS iffD1])); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
448 |
by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
4162 | 449 |
by Safe_tac; |
4089 | 450 |
by (asm_full_simp_tac (simpset() addsimps ([znat_def, zadd])) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
451 |
qed "zless_not_sym"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
452 |
|
5454 | 453 |
(* [| n<m; ~P ==> m<n |] ==> P *) |
454 |
bind_thm ("zless_asym", (zless_not_sym RS swap)); |
|
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
455 |
|
5069 | 456 |
Goal "!!z::int. ~ z<z"; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
457 |
by (resolve_tac [zless_asym RS notI] 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
458 |
by (REPEAT (assume_tac 1)); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
459 |
qed "zless_not_refl"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
460 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
461 |
(* z<z ==> R *) |
1619 | 462 |
bind_thm ("zless_irrefl", (zless_not_refl RS notE)); |
5491 | 463 |
AddSEs [zless_irrefl]; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
464 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
465 |
Goal "z<w ==> w ~= (z::int)"; |
5491 | 466 |
by (Blast_tac 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
467 |
qed "zless_not_refl2"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
468 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
469 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
470 |
(*"Less than" is a linear ordering*) |
5069 | 471 |
Goalw [zless_def, znegative_def, zdiff_def] |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
472 |
"z<w | z=w | w<(z::int)"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
473 |
by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
474 |
by (res_inst_tac [("z","w")] eq_Abs_Integ 1); |
4162 | 475 |
by Safe_tac; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
476 |
by (asm_full_simp_tac |
4089 | 477 |
(simpset() addsimps [zadd, zminus, Image_iff, Bex_def]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
478 |
by (res_inst_tac [("m1", "x+ya"), ("n1", "xa+y")] (less_linear RS disjE) 1); |
5316 | 479 |
by (auto_tac (claset(), simpset() addsimps add_ac)); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
480 |
qed "zless_linear"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
481 |
|
5491 | 482 |
Goal "($# m = $# n) = (m = n)"; |
483 |
by (fast_tac (claset() addSEs [inj_znat RS injD]) 1); |
|
484 |
qed "znat_znat_eq"; |
|
485 |
AddIffs [znat_znat_eq]; |
|
486 |
||
487 |
Goal "($#m < $#n) = (m<n)"; |
|
488 |
by (simp_tac (simpset() addsimps [less_iff_Suc_add, zless_iff_Suc_zadd, |
|
489 |
add_znat]) 1); |
|
490 |
qed "zless_eq_less"; |
|
491 |
Addsimps [zless_eq_less]; |
|
492 |
||
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
493 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
494 |
(*** Properties of <= ***) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
495 |
|
5069 | 496 |
Goalw [zle_def, le_def] "($#m <= $#n) = (m<=n)"; |
5491 | 497 |
by (Simp_tac 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
498 |
qed "zle_eq_le"; |
5491 | 499 |
Addsimps [zle_eq_le]; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
500 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
501 |
Goalw [zle_def] "~(w<z) ==> z<=(w::int)"; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
502 |
by (assume_tac 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
503 |
qed "zleI"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
504 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
505 |
Goalw [zle_def] "z<=w ==> ~(w<(z::int))"; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
506 |
by (assume_tac 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
507 |
qed "zleD"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
508 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
509 |
val zleE = make_elim zleD; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
510 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
511 |
Goalw [zle_def] "~ z <= w ==> w<(z::int)"; |
1894 | 512 |
by (Fast_tac 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
513 |
qed "not_zleE"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
514 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
515 |
Goalw [zle_def] "z <= w ==> z < w | z=(w::int)"; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
516 |
by (cut_facts_tac [zless_linear] 1); |
5491 | 517 |
by (blast_tac (claset() addEs [zless_asym]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
518 |
qed "zle_imp_zless_or_eq"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
519 |
|
5491 | 520 |
Goalw [zle_def] "z<w | z=w ==> z <= (w::int)"; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
521 |
by (cut_facts_tac [zless_linear] 1); |
5491 | 522 |
by (blast_tac (claset() addEs [zless_asym]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
523 |
qed "zless_or_eq_imp_zle"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
524 |
|
5069 | 525 |
Goal "(x <= (y::int)) = (x < y | x=y)"; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
526 |
by (REPEAT(ares_tac [iffI, zless_or_eq_imp_zle, zle_imp_zless_or_eq] 1)); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
527 |
qed "zle_eq_zless_or_eq"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
528 |
|
5069 | 529 |
Goal "w <= (w::int)"; |
4089 | 530 |
by (simp_tac (simpset() addsimps [zle_eq_zless_or_eq]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
531 |
qed "zle_refl"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
532 |
|
5491 | 533 |
Goalw [zle_def] "z < w ==> z <= (w::int)"; |
534 |
by (blast_tac (claset() addEs [zless_asym]) 1); |
|
535 |
qed "zless_imp_zle"; |
|
536 |
||
537 |
Addsimps [zle_refl, zless_imp_zle]; |
|
538 |
||
5316 | 539 |
Goal "[| i <= j; j < k |] ==> i < (k::int)"; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
540 |
by (dtac zle_imp_zless_or_eq 1); |
5454 | 541 |
by (blast_tac (claset() addIs [zless_trans]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
542 |
qed "zle_zless_trans"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
543 |
|
5491 | 544 |
Goal "[| i < j; j <= k |] ==> i < (k::int)"; |
545 |
by (dtac zle_imp_zless_or_eq 1); |
|
546 |
by (blast_tac (claset() addIs [zless_trans]) 1); |
|
547 |
qed "zless_zle_trans"; |
|
548 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
549 |
Goal "[| i <= j; j <= k |] ==> i <= (k::int)"; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
550 |
by (EVERY1 [dtac zle_imp_zless_or_eq, dtac zle_imp_zless_or_eq, |
5316 | 551 |
rtac zless_or_eq_imp_zle, |
5454 | 552 |
blast_tac (claset() addIs [zless_trans])]); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
553 |
qed "zle_trans"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
554 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
555 |
Goal "[| z <= w; w <= z |] ==> z = (w::int)"; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
556 |
by (EVERY1 [dtac zle_imp_zless_or_eq, dtac zle_imp_zless_or_eq, |
5491 | 557 |
blast_tac (claset() addEs [zless_asym])]); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
558 |
qed "zle_anti_sym"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
559 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
560 |
|
5491 | 561 |
Goal "!!w::int. (z + w' = z + w) = (w' = w)"; |
562 |
by Safe_tac; |
|
563 |
by (dres_inst_tac [("f", "%x. x + -z")] arg_cong 1); |
|
4089 | 564 |
by (asm_full_simp_tac (simpset() addsimps zadd_ac) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
565 |
qed "zadd_left_cancel"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
566 |
|
5491 | 567 |
Addsimps [zadd_left_cancel]; |
568 |
||
569 |
Goal "!!z::int. (w' + z = w + z) = (w' = w)"; |
|
570 |
by (asm_full_simp_tac (simpset() addsimps zadd_ac) 1); |
|
571 |
qed "zadd_right_cancel"; |
|
572 |
||
573 |
Addsimps [zadd_right_cancel]; |
|
574 |
||
575 |
||
576 |
Goal "(w < z + $# 1) = (w<z | w=z)"; |
|
577 |
by (auto_tac (claset(), |
|
578 |
simpset() addsimps [zless_iff_Suc_zadd, zadd_assoc, |
|
579 |
add_znat])); |
|
580 |
by (cut_inst_tac [("m","n")] znat_Suc 1); |
|
581 |
by (exhaust_tac "n" 1); |
|
582 |
auto(); |
|
583 |
by (full_simp_tac (simpset() addsimps zadd_ac) 1); |
|
584 |
by (asm_full_simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1); |
|
585 |
qed "zless_add_nat1_eq"; |
|
586 |
||
587 |
||
588 |
Goal "(w + $# 1 <= z) = (w<z)"; |
|
589 |
by (simp_tac (simpset() addsimps [zle_def, zless_add_nat1_eq]) 1); |
|
590 |
by (auto_tac (claset() addIs [zle_anti_sym] addEs [zless_asym], |
|
591 |
simpset() addsimps [symmetric zle_def])); |
|
592 |
qed "add_nat1_zle_eq"; |
|
593 |
||
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
594 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
595 |
(*** Monotonicity results ***) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
596 |
|
5316 | 597 |
Goal "!!z::int. v < w ==> v + z < w + z"; |
5491 | 598 |
by (full_simp_tac (simpset() addsimps (zless_iff_Suc_zadd::zadd_ac)) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
599 |
qed "zadd_zless_mono1"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
600 |
|
5316 | 601 |
Goal "!!z::int. (v+z < w+z) = (v < w)"; |
4089 | 602 |
by (safe_tac (claset() addSEs [zadd_zless_mono1])); |
5491 | 603 |
by (dres_inst_tac [("z", "-z")] zadd_zless_mono1 1); |
4089 | 604 |
by (asm_full_simp_tac (simpset() addsimps [zadd_assoc]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
605 |
qed "zadd_left_cancel_zless"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
606 |
|
5316 | 607 |
Goal "!!z::int. (v+z <= w+z) = (v <= w)"; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
608 |
by (asm_full_simp_tac |
4089 | 609 |
(simpset() addsimps [zle_def, zadd_left_cancel_zless]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
610 |
qed "zadd_left_cancel_zle"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
611 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
612 |
(*"v<=w ==> v+z <= w+z"*) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
613 |
bind_thm ("zadd_zle_mono1", zadd_left_cancel_zle RS iffD2); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
614 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
615 |
|
5316 | 616 |
Goal "!!z z'::int. [| w'<=w; z'<=z |] ==> w' + z' <= w + z"; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
617 |
by (etac (zadd_zle_mono1 RS zle_trans) 1); |
4089 | 618 |
by (simp_tac (simpset() addsimps [zadd_commute]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
619 |
(*w moves to the end because it is free while z', z are bound*) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
620 |
by (etac zadd_zle_mono1 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
621 |
qed "zadd_zle_mono"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
622 |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
623 |
|
4195 | 624 |
(**** Comparisons: lemmas and proofs by Norbert Voelker ****) |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
625 |
|
5491 | 626 |
Goal "(- x < - y) = (y < (x::int))"; |
627 |
by (rewrite_goals_tac [zless_def,zdiff_def]); |
|
628 |
by (simp_tac (simpset() addsimps zadd_ac) 1); |
|
629 |
qed "zminus_zless_zminus"; |
|
630 |
Addsimps [zminus_zless_zminus]; |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
631 |
|
5491 | 632 |
Goal "(- x <= - y) = (y <= (x::int))"; |
633 |
by (simp_tac (simpset() addsimps [zle_def, zminus_zless_zminus]) 1); |
|
634 |
qed "zminus_zle_zminus"; |
|
635 |
Addsimps [zminus_zle_zminus]; |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
636 |
|
5491 | 637 |
(** The next several equations can make the simplifier loop! **) |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
638 |
|
5491 | 639 |
Goal "(x < - y) = (y < - (x::int))"; |
640 |
by (rewrite_goals_tac [zless_def,zdiff_def]); |
|
641 |
by (simp_tac (simpset() addsimps zadd_ac ) 1); |
|
3725 | 642 |
qed "zless_zminus"; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
643 |
|
5491 | 644 |
Goal "(- x < y) = (- y < (x::int))"; |
645 |
by (rewrite_goals_tac [zless_def,zdiff_def]); |
|
646 |
by (simp_tac (simpset() addsimps zadd_ac) 1); |
|
3725 | 647 |
qed "zminus_zless"; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
648 |
|
5491 | 649 |
Goal "(x <= - y) = (y <= - (x::int))"; |
650 |
by (simp_tac (simpset() addsimps [zle_def, zminus_zless]) 1); |
|
3725 | 651 |
qed "zle_zminus"; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
652 |
|
5491 | 653 |
Goal "(- x <= y) = (- y <= (x::int))"; |
654 |
by (simp_tac (simpset() addsimps [zle_def, zless_zminus]) 1); |
|
3725 | 655 |
qed "zminus_zle"; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
656 |
|
5491 | 657 |
Goal "- $# Suc n < $# 0"; |
658 |
by (stac (zminus_nat0 RS sym) 1); |
|
659 |
by (stac zminus_zless_zminus 1); |
|
660 |
by (Simp_tac 1); |
|
661 |
qed "negative_zless_0"; |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
662 |
|
5491 | 663 |
Goal "- $# Suc n < $# m"; |
664 |
by (rtac (negative_zless_0 RS zless_zle_trans) 1); |
|
665 |
by (Simp_tac 1); |
|
666 |
qed "negative_zless"; |
|
667 |
AddIffs [negative_zless]; |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
668 |
|
5491 | 669 |
Goal "- $# n <= $#0"; |
670 |
by (simp_tac (simpset() addsimps [zminus_zle]) 1); |
|
671 |
qed "negative_zle_0"; |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
672 |
|
5491 | 673 |
Goal "- $# n <= $# m"; |
674 |
by (rtac (negative_zle_0 RS zle_trans) 1); |
|
675 |
by (Simp_tac 1); |
|
676 |
qed "negative_zle"; |
|
677 |
AddIffs [negative_zle]; |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
678 |
|
5491 | 679 |
Goal "~($# 0 <= - $# Suc n)"; |
680 |
by (stac zle_zminus 1); |
|
681 |
by (Simp_tac 1); |
|
3725 | 682 |
qed "not_zle_0_negative"; |
5491 | 683 |
Addsimps [not_zle_0_negative]; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
684 |
|
5491 | 685 |
Goal "($# n <= - $# m) = (n = 0 & m = 0)"; |
686 |
by Safe_tac; |
|
687 |
by (Simp_tac 3); |
|
688 |
by (dtac (zle_zminus RS iffD1) 2); |
|
689 |
by (ALLGOALS (dtac (negative_zle_0 RSN(2,zle_trans)))); |
|
690 |
by (ALLGOALS Asm_full_simp_tac); |
|
3725 | 691 |
qed "znat_zle_znegative"; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
692 |
|
5491 | 693 |
Goal "~($# n < - $# m)"; |
694 |
by (simp_tac (simpset() addsimps [symmetric zle_def]) 1); |
|
3725 | 695 |
qed "not_znat_zless_negative"; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
696 |
|
5491 | 697 |
Goal "(- $# n = $# m) = (n = 0 & m = 0)"; |
698 |
by (rtac iffI 1); |
|
699 |
by (rtac (znat_zle_znegative RS iffD1) 1); |
|
700 |
by (dtac sym 1); |
|
701 |
by (ALLGOALS Asm_simp_tac); |
|
3725 | 702 |
qed "negative_eq_positive"; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
703 |
|
5491 | 704 |
Addsimps [negative_eq_positive, not_znat_zless_negative]; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
705 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
706 |
Goalw [zdiff_def,zless_def] "znegative x = (x < $# 0)"; |
5491 | 707 |
by Auto_tac; |
708 |
qed "znegative_eq_less_0"; |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
709 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
710 |
Goalw [zdiff_def,zless_def] "(~znegative x) = ($# 0 <= x)"; |
5491 | 711 |
by (stac znegative_eq_less_0 1); |
712 |
by (safe_tac (claset() addSDs [zleD,not_zleE,zleI]) ); |
|
713 |
qed "not_znegative_eq_ge_0"; |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
714 |
|
5491 | 715 |
Goal "znegative x ==> ? n. x = - $# Suc n"; |
716 |
by (full_simp_tac (simpset() addsimps [znegative_eq_less_0, |
|
717 |
zless_iff_Suc_zadd]) 1); |
|
718 |
by (etac exE 1); |
|
719 |
by (rtac exI 1); |
|
720 |
by (dres_inst_tac [("f","(% z. z + - $# Suc n )")] arg_cong 1); |
|
721 |
by (auto_tac(claset(), simpset() addsimps [zadd_assoc])); |
|
3725 | 722 |
qed "znegativeD"; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
723 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
724 |
Goal "~znegative x ==> ? n. x = $# n"; |
5491 | 725 |
by (dtac (not_znegative_eq_ge_0 RS iffD1) 1); |
726 |
by (dtac zle_imp_zless_or_eq 1); |
|
727 |
by (etac disjE 1); |
|
728 |
by (dtac (zless_iff_Suc_zadd RS iffD1) 1); |
|
729 |
by Auto_tac; |
|
3725 | 730 |
qed "not_znegativeD"; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
731 |
|
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
732 |
(* a case theorem distinguishing positive and negative int *) |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
733 |
|
5491 | 734 |
val prems = Goal "[|!! n. P ($# n); !! n. P (- $# Suc n) |] ==> P z"; |
735 |
by (cut_inst_tac [("P","znegative z")] excluded_middle 1); |
|
736 |
by (fast_tac (claset() addSDs [znegativeD,not_znegativeD] addSIs prems) 1); |
|
3725 | 737 |
qed "int_cases"; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
738 |
|
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
739 |
fun int_case_tac x = res_inst_tac [("z",x)] int_cases; |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
740 |
|
5491 | 741 |
|
742 |
(*** Subtraction laws ***) |
|
743 |
||
744 |
Goal "x + (y - z) = (x + y) - (z::int)"; |
|
745 |
by (simp_tac (simpset() addsimps (zdiff_def::zadd_ac)) 1); |
|
746 |
qed "zadd_zdiff_eq"; |
|
747 |
||
748 |
Goal "(x - y) + z = (x + z) - (y::int)"; |
|
749 |
by (simp_tac (simpset() addsimps (zdiff_def::zadd_ac)) 1); |
|
750 |
qed "zdiff_zadd_eq"; |
|
751 |
||
752 |
Goal "(x - y) - z = x - (y + (z::int))"; |
|
753 |
by (simp_tac (simpset() addsimps (zdiff_def::zadd_ac)) 1); |
|
754 |
qed "zdiff_zdiff_eq"; |
|
755 |
||
756 |
Goal "x - (y - z) = (x + z) - (y::int)"; |
|
757 |
by (simp_tac (simpset() addsimps (zdiff_def::zadd_ac)) 1); |
|
758 |
qed "zdiff_zdiff_eq2"; |
|
759 |
||
760 |
Goalw [zless_def, zdiff_def] "(x-y < z) = (x < z + (y::int))"; |
|
761 |
by (simp_tac (simpset() addsimps zadd_ac) 1); |
|
762 |
qed "zdiff_zless_eq"; |
|
763 |
||
764 |
Goalw [zless_def, zdiff_def] "(x < z-y) = (x + (y::int) < z)"; |
|
765 |
by (simp_tac (simpset() addsimps zadd_ac) 1); |
|
766 |
qed "zless_zdiff_eq"; |
|
767 |
||
768 |
Goalw [zle_def] "(x-y <= z) = (x <= z + (y::int))"; |
|
769 |
by (simp_tac (simpset() addsimps [zless_zdiff_eq]) 1); |
|
770 |
qed "zdiff_zle_eq"; |
|
771 |
||
772 |
Goalw [zle_def] "(x <= z-y) = (x + (y::int) <= z)"; |
|
773 |
by (simp_tac (simpset() addsimps [zdiff_zless_eq]) 1); |
|
774 |
qed "zle_zdiff_eq"; |
|
775 |
||
776 |
Goalw [zdiff_def] "(x-y = z) = (x = z + (y::int))"; |
|
777 |
by (auto_tac (claset(), simpset() addsimps [zadd_assoc])); |
|
778 |
qed "zdiff_eq_eq"; |
|
779 |
||
780 |
Goalw [zdiff_def] "(x = z-y) = (x + (y::int) = z)"; |
|
781 |
by (auto_tac (claset(), simpset() addsimps [zadd_assoc])); |
|
782 |
qed "eq_zdiff_eq"; |
|
783 |
||
784 |
(*Use with zadd_ac*) |
|
785 |
val zcompare_rls = |
|
786 |
[symmetric zdiff_def, |
|
787 |
zadd_zdiff_eq, zdiff_zadd_eq, zdiff_zdiff_eq, zdiff_zdiff_eq2, |
|
788 |
zdiff_zless_eq, zless_zdiff_eq, zdiff_zle_eq, zle_zdiff_eq, |
|
789 |
zdiff_eq_eq, eq_zdiff_eq]; |
|
790 |
||
791 |
||
792 |
(*These rewrite to $# 0, while from Bin onwards we should rewrite to #0 *) |
|
793 |
Delsimps [zadd_zminus_inverse_nat, zadd_zminus_inverse_nat2]; |
|
794 |
||
795 |