author | clasohm |
Tue, 30 Jan 1996 15:24:36 +0100 | |
changeset 1465 | 5d7a7e439cec |
parent 1266 | 3ae9fe3c0f68 |
child 1619 | cb62d89b7adb |
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$ |
1465 | 3 |
Authors: Riccardo Mattolini, Dip. Sistemi e Informatica |
4 |
Lawrence C Paulson, Cambridge University Computer Laboratory |
|
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
5 |
Copyright 1994 Universita' di Firenze |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
6 |
Copyright 1993 University of Cambridge |
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 |
The integers as equivalence classes over nat*nat. |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
9 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
10 |
Could also prove... |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
11 |
"znegative(z) ==> $# zmagnitude(z) = $~ z" |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
12 |
"~ znegative(z) ==> $# zmagnitude(z) = z" |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
13 |
< is a linear ordering |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
14 |
+ and * are monotonic wrt < |
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 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
17 |
open Integ; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
18 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
19 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
20 |
(*** Proving that intrel is an equivalence relation ***) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
21 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
22 |
val eqa::eqb::prems = goal Arith.thy |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
23 |
"[| (x1::nat) + y2 = x2 + y1; x2 + y3 = x3 + y2 |] ==> \ |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
24 |
\ x1 + y3 = x3 + y1"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
25 |
by (res_inst_tac [("k2","x2")] (add_left_cancel RS iffD1) 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
26 |
by (rtac (add_left_commute RS trans) 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
27 |
by (rtac (eqb RS ssubst) 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
28 |
by (rtac (add_left_commute RS trans) 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
29 |
by (rtac (eqa RS ssubst) 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
30 |
by (rtac (add_left_commute) 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
31 |
qed "integ_trans_lemma"; |
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 |
(** Natural deduction for intrel **) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
34 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
35 |
val prems = goalw Integ.thy [intrel_def] |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
36 |
"[| x1+y2 = x2+y1|] ==> \ |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset
|
37 |
\ ((x1,y1),(x2,y2)): intrel"; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
38 |
by (fast_tac (rel_cs addIs prems) 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
39 |
qed "intrelI"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
40 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
41 |
(*intrelE is hard to derive because fast_tac tries hyp_subst_tac so soon*) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
42 |
goalw Integ.thy [intrel_def] |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
43 |
"p: intrel --> (EX x1 y1 x2 y2. \ |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset
|
44 |
\ p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1)"; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
45 |
by (fast_tac rel_cs 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
46 |
qed "intrelE_lemma"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
47 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
48 |
val [major,minor] = goal Integ.thy |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
49 |
"[| p: intrel; \ |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset
|
50 |
\ !!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
|
51 |
\ ==> Q"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
52 |
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
|
53 |
by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1)); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
54 |
qed "intrelE"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
55 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
56 |
val intrel_cs = rel_cs addSIs [intrelI] addSEs [intrelE]; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
57 |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset
|
58 |
goal Integ.thy "((x1,y1),(x2,y2)): intrel = (x1+y2 = x2+y1)"; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
59 |
by (fast_tac intrel_cs 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
60 |
qed "intrel_iff"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
61 |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset
|
62 |
goal Integ.thy "(x,x): intrel"; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
63 |
by (rtac (surjective_pairing RS ssubst) 1 THEN rtac (refl RS intrelI) 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
64 |
qed "intrel_refl"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
65 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
66 |
goalw Integ.thy [equiv_def, refl_def, sym_def, trans_def] |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
67 |
"equiv {x::(nat*nat).True} intrel"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
68 |
by (fast_tac (intrel_cs addSIs [intrel_refl] |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
69 |
addSEs [sym, integ_trans_lemma]) 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
70 |
qed "equiv_intrel"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
71 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
72 |
val equiv_intrel_iff = |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
73 |
[TrueI, TrueI] MRS |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
74 |
([CollectI, CollectI] MRS |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
75 |
(equiv_intrel RS eq_equiv_class_iff)); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
76 |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset
|
77 |
goalw Integ.thy [Integ_def,intrel_def,quotient_def] "intrel^^{(x,y)}:Integ"; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
78 |
by (fast_tac set_cs 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
79 |
qed "intrel_in_integ"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
80 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
81 |
goal Integ.thy "inj_onto Abs_Integ Integ"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
82 |
by (rtac inj_onto_inverseI 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
83 |
by (etac Abs_Integ_inverse 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
84 |
qed "inj_onto_Abs_Integ"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
85 |
|
1266 | 86 |
Addsimps [equiv_intrel_iff, inj_onto_Abs_Integ RS inj_onto_iff, |
1465 | 87 |
intrel_iff, intrel_in_integ, Abs_Integ_inverse]; |
925
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 |
goal Integ.thy "inj(Rep_Integ)"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
90 |
by (rtac inj_inverseI 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
91 |
by (rtac Rep_Integ_inverse 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
92 |
qed "inj_Rep_Integ"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
93 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
94 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
95 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
96 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
97 |
(** znat: the injection from nat to Integ **) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
98 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
99 |
goal Integ.thy "inj(znat)"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
100 |
by (rtac injI 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
101 |
by (rewtac znat_def); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
102 |
by (dtac (inj_onto_Abs_Integ RS inj_ontoD) 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
103 |
by (REPEAT (rtac intrel_in_integ 1)); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
104 |
by (dtac eq_equiv_class 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
105 |
by (rtac equiv_intrel 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
106 |
by (fast_tac set_cs 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
107 |
by (safe_tac intrel_cs); |
1266 | 108 |
by (Asm_full_simp_tac 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
109 |
qed "inj_znat"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
110 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
111 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
112 |
(**** zminus: unary negation on Integ ****) |
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 |
goalw Integ.thy [congruent_def] |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset
|
115 |
"congruent intrel (%p. split (%x y. intrel^^{(y,x)}) p)"; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
116 |
by (safe_tac intrel_cs); |
1266 | 117 |
by (asm_simp_tac (!simpset addsimps add_ac) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
118 |
qed "zminus_congruent"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
119 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
120 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
121 |
(*Resolve th against the corresponding facts for zminus*) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
122 |
val zminus_ize = RSLIST [equiv_intrel, zminus_congruent]; |
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 |
goalw Integ.thy [zminus_def] |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset
|
125 |
"$~ 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
|
126 |
by (res_inst_tac [("f","Abs_Integ")] arg_cong 1); |
1266 | 127 |
by (simp_tac (!simpset addsimps |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
128 |
[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
|
129 |
qed "zminus"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
130 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
131 |
(*by lcp*) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
132 |
val [prem] = goal Integ.thy |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset
|
133 |
"(!!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
|
134 |
by (res_inst_tac [("x1","z")] |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
135 |
(rewrite_rule [Integ_def] Rep_Integ RS quotientE) 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
136 |
by (dres_inst_tac [("f","Abs_Integ")] arg_cong 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
137 |
by (res_inst_tac [("p","x")] PairE 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
138 |
by (rtac prem 1); |
1266 | 139 |
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
|
140 |
qed "eq_Abs_Integ"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
141 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
142 |
goal Integ.thy "$~ ($~ z) = z"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
143 |
by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
1266 | 144 |
by (asm_simp_tac (!simpset addsimps [zminus]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
145 |
qed "zminus_zminus"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
146 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
147 |
goal Integ.thy "inj(zminus)"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
148 |
by (rtac injI 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
149 |
by (dres_inst_tac [("f","zminus")] arg_cong 1); |
1266 | 150 |
by (asm_full_simp_tac (!simpset addsimps [zminus_zminus]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
151 |
qed "inj_zminus"; |
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 |
goalw Integ.thy [znat_def] "$~ ($#0) = $#0"; |
1266 | 154 |
by (simp_tac (!simpset addsimps [zminus]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
155 |
qed "zminus_0"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
156 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
157 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
158 |
(**** znegative: the test for negative integers ****) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
159 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
160 |
goal Arith.thy "!!m x n::nat. n+m=x ==> m<=x"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
161 |
by (dtac (disjI2 RS less_or_eq_imp_le) 1); |
1266 | 162 |
by (asm_full_simp_tac (!simpset addsimps add_ac) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
163 |
by (dtac add_leD1 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
164 |
by (assume_tac 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
165 |
qed "not_znegative_znat_lemma"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
166 |
|
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 |
goalw Integ.thy [znegative_def, znat_def] |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
169 |
"~ znegative($# n)"; |
1266 | 170 |
by (Simp_tac 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
171 |
by (safe_tac intrel_cs); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
172 |
by (rtac ccontr 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
173 |
by (etac notE 1); |
1266 | 174 |
by (Asm_full_simp_tac 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
175 |
by (dtac not_znegative_znat_lemma 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
176 |
by (fast_tac (HOL_cs addDs [leD]) 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
177 |
qed "not_znegative_znat"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
178 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
179 |
goalw Integ.thy [znegative_def, znat_def] "znegative($~ $# Suc(n))"; |
1266 | 180 |
by (simp_tac (!simpset addsimps [zminus]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
181 |
by (REPEAT (ares_tac [exI, conjI] 1)); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
182 |
by (rtac (intrelI RS ImageI) 2); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
183 |
by (rtac singletonI 3); |
1266 | 184 |
by (Simp_tac 2); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
185 |
by (rtac less_add_Suc1 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
186 |
qed "znegative_zminus_znat"; |
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 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
189 |
(**** zmagnitude: magnitide of an integer, as a natural number ****) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
190 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
191 |
goal Arith.thy "!!n::nat. n - Suc(n+m)=0"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
192 |
by (nat_ind_tac "n" 1); |
1266 | 193 |
by (ALLGOALS Asm_simp_tac); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
194 |
qed "diff_Suc_add_0"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
195 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
196 |
goal Arith.thy "Suc((n::nat)+m)-n=Suc(m)"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
197 |
by (nat_ind_tac "n" 1); |
1266 | 198 |
by (ALLGOALS Asm_simp_tac); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
199 |
qed "diff_Suc_add_inverse"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
200 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
201 |
goalw Integ.thy [congruent_def] |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset
|
202 |
"congruent intrel (split (%x y. intrel^^{((y-x) + (x-(y::nat)),0)}))"; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
203 |
by (safe_tac intrel_cs); |
1266 | 204 |
by (Asm_simp_tac 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
205 |
by (etac rev_mp 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
206 |
by (res_inst_tac [("m","x1"),("n","y1")] diff_induct 1); |
1266 | 207 |
by (asm_simp_tac (!simpset addsimps [inj_Suc RS inj_eq]) 3); |
208 |
by (asm_simp_tac (!simpset addsimps [diff_add_inverse,diff_add_0]) 2); |
|
209 |
by (Asm_simp_tac 1); |
|
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
210 |
by (rtac impI 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
211 |
by (etac subst 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
212 |
by (res_inst_tac [("m1","x")] (add_commute RS ssubst) 1); |
1266 | 213 |
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
|
214 |
by (rtac impI 1); |
1266 | 215 |
by (asm_simp_tac (!simpset addsimps |
1465 | 216 |
[diff_add_inverse, diff_add_0, diff_Suc_add_0, |
217 |
diff_Suc_add_inverse]) 1); |
|
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
218 |
qed "zmagnitude_congruent"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
219 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
220 |
(*Resolve th against the corresponding facts for zmagnitude*) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
221 |
val zmagnitude_ize = RSLIST [equiv_intrel, zmagnitude_congruent]; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
222 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
223 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
224 |
goalw Integ.thy [zmagnitude_def] |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset
|
225 |
"zmagnitude (Abs_Integ(intrel^^{(x,y)})) = \ |
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset
|
226 |
\ Abs_Integ(intrel^^{((y - x) + (x - y),0)})"; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
227 |
by (res_inst_tac [("f","Abs_Integ")] arg_cong 1); |
1266 | 228 |
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
|
229 |
qed "zmagnitude"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
230 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
231 |
goalw Integ.thy [znat_def] "zmagnitude($# n) = $#n"; |
1266 | 232 |
by (asm_simp_tac (!simpset addsimps [zmagnitude]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
233 |
qed "zmagnitude_znat"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
234 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
235 |
goalw Integ.thy [znat_def] "zmagnitude($~ $# n) = $#n"; |
1266 | 236 |
by (asm_simp_tac (!simpset addsimps [zmagnitude, zminus]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
237 |
qed "zmagnitude_zminus_znat"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
238 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
239 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
240 |
(**** zadd: addition on Integ ****) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
241 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
242 |
(** Congruence property for addition **) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
243 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
244 |
goalw Integ.thy [congruent2_def] |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
245 |
"congruent2 intrel (%p1 p2. \ |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset
|
246 |
\ 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
|
247 |
(*Proof via congruent2_commuteI seems longer*) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
248 |
by (safe_tac intrel_cs); |
1266 | 249 |
by (asm_simp_tac (!simpset addsimps [add_assoc]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
250 |
(*The rest should be trivial, but rearranging terms is hard*) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
251 |
by (res_inst_tac [("x1","x1a")] (add_left_commute RS ssubst) 1); |
1266 | 252 |
by (asm_simp_tac (!simpset addsimps [add_assoc RS sym]) 1); |
253 |
by (asm_simp_tac (!simpset addsimps add_ac) 1); |
|
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
254 |
qed "zadd_congruent2"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
255 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
256 |
(*Resolve th against the corresponding facts for zadd*) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
257 |
val zadd_ize = RSLIST [equiv_intrel, zadd_congruent2]; |
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 |
goalw Integ.thy [zadd_def] |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset
|
260 |
"Abs_Integ(intrel^^{(x1,y1)}) + Abs_Integ(intrel^^{(x2,y2)}) = \ |
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset
|
261 |
\ Abs_Integ(intrel^^{(x1+x2, y1+y2)})"; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
262 |
by (asm_simp_tac |
1266 | 263 |
(!simpset addsimps [zadd_ize UN_equiv_class2]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
264 |
qed "zadd"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
265 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
266 |
goalw Integ.thy [znat_def] "$#0 + z = z"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
267 |
by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
1266 | 268 |
by (asm_simp_tac (!simpset addsimps [zadd]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
269 |
qed "zadd_0"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
270 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
271 |
goal Integ.thy "$~ (z + w) = $~ z + $~ w"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
272 |
by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
273 |
by (res_inst_tac [("z","w")] eq_Abs_Integ 1); |
1266 | 274 |
by (asm_simp_tac (!simpset addsimps [zminus,zadd]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
275 |
qed "zminus_zadd_distrib"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
276 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
277 |
goal Integ.thy "(z::int) + w = w + z"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
278 |
by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
279 |
by (res_inst_tac [("z","w")] eq_Abs_Integ 1); |
1266 | 280 |
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
|
281 |
qed "zadd_commute"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
282 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
283 |
goal Integ.thy "((z1::int) + z2) + z3 = z1 + (z2 + z3)"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
284 |
by (res_inst_tac [("z","z1")] eq_Abs_Integ 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
285 |
by (res_inst_tac [("z","z2")] eq_Abs_Integ 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
286 |
by (res_inst_tac [("z","z3")] eq_Abs_Integ 1); |
1266 | 287 |
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
|
288 |
qed "zadd_assoc"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
289 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
290 |
(*For AC rewriting*) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
291 |
goal Integ.thy "(x::int)+(y+z)=y+(x+z)"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
292 |
by (rtac (zadd_commute RS trans) 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
293 |
by (rtac (zadd_assoc RS trans) 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
294 |
by (rtac (zadd_commute RS arg_cong) 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
295 |
qed "zadd_left_commute"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
296 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
297 |
(*Integer addition is an AC operator*) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
298 |
val zadd_ac = [zadd_assoc,zadd_commute,zadd_left_commute]; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
299 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
300 |
goalw Integ.thy [znat_def] "$# (m + n) = ($#m) + ($#n)"; |
1266 | 301 |
by (asm_simp_tac (!simpset addsimps [zadd]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
302 |
qed "znat_add"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
303 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
304 |
goalw Integ.thy [znat_def] "z + ($~ z) = $#0"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
305 |
by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
1266 | 306 |
by (asm_simp_tac (!simpset addsimps [zminus, zadd, add_commute]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
307 |
qed "zadd_zminus_inverse"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
308 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
309 |
goal Integ.thy "($~ z) + z = $#0"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
310 |
by (rtac (zadd_commute RS trans) 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
311 |
by (rtac zadd_zminus_inverse 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
312 |
qed "zadd_zminus_inverse2"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
313 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
314 |
goal Integ.thy "z + $#0 = z"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
315 |
by (rtac (zadd_commute RS trans) 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
316 |
by (rtac zadd_0 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
317 |
qed "zadd_0_right"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
318 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
319 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
320 |
(*Need properties of subtraction? Or use $- just as an abbreviation!*) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
321 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
322 |
(**** zmult: multiplication on Integ ****) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
323 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
324 |
(** Congruence property for multiplication **) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
325 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
326 |
goal Integ.thy "((k::nat) + l) + (m + n) = (k + m) + (n + l)"; |
1266 | 327 |
by (simp_tac (!simpset addsimps add_ac) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
328 |
qed "zmult_congruent_lemma"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
329 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
330 |
goal Integ.thy |
1465 | 331 |
"congruent2 intrel (%p1 p2. \ |
332 |
\ split (%x1 y1. split (%x2 y2. \ |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset
|
333 |
\ 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
|
334 |
by (rtac (equiv_intrel RS congruent2_commuteI) 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
335 |
by (safe_tac intrel_cs); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
336 |
by (rewtac split_def); |
1266 | 337 |
by (simp_tac (!simpset addsimps add_ac@mult_ac) 1); |
338 |
by (asm_simp_tac (!simpset delsimps [equiv_intrel_iff] |
|
339 |
addsimps add_ac@mult_ac) 1); |
|
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
340 |
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
|
341 |
by (rtac (zmult_congruent_lemma RS trans) 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
342 |
by (rtac (zmult_congruent_lemma RS trans RS sym) 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
343 |
by (rtac (zmult_congruent_lemma RS trans RS sym) 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
344 |
by (rtac (zmult_congruent_lemma RS trans RS sym) 1); |
1266 | 345 |
by (asm_simp_tac (!simpset delsimps [add_mult_distrib] |
346 |
addsimps [add_mult_distrib RS sym]) 1); |
|
347 |
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
|
348 |
qed "zmult_congruent2"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
349 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
350 |
(*Resolve th against the corresponding facts for zmult*) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
351 |
val zmult_ize = RSLIST [equiv_intrel, zmult_congruent2]; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
352 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
353 |
goalw Integ.thy [zmult_def] |
1465 | 354 |
"Abs_Integ((intrel^^{(x1,y1)})) * Abs_Integ((intrel^^{(x2,y2)})) = \ |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset
|
355 |
\ Abs_Integ(intrel ^^ {(x1*x2 + y1*y2, x1*y2 + y1*x2)})"; |
1266 | 356 |
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
|
357 |
qed "zmult"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
358 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
359 |
goalw Integ.thy [znat_def] "$#0 * z = $#0"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
360 |
by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
1266 | 361 |
by (asm_simp_tac (!simpset addsimps [zmult]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
362 |
qed "zmult_0"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
363 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
364 |
goalw Integ.thy [znat_def] "$#Suc(0) * z = z"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
365 |
by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
1266 | 366 |
by (asm_simp_tac (!simpset addsimps [zmult]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
367 |
qed "zmult_1"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
368 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
369 |
goal Integ.thy "($~ z) * w = $~ (z * w)"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
370 |
by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
371 |
by (res_inst_tac [("z","w")] eq_Abs_Integ 1); |
1266 | 372 |
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
|
373 |
qed "zmult_zminus"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
374 |
|
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 |
goal Integ.thy "($~ z) * ($~ w) = (z * w)"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
377 |
by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
378 |
by (res_inst_tac [("z","w")] eq_Abs_Integ 1); |
1266 | 379 |
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
|
380 |
qed "zmult_zminus_zminus"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
381 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
382 |
goal Integ.thy "(z::int) * w = w * z"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
383 |
by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
384 |
by (res_inst_tac [("z","w")] eq_Abs_Integ 1); |
1266 | 385 |
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
|
386 |
qed "zmult_commute"; |
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 |
goal Integ.thy "z * $# 0 = $#0"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
389 |
by (rtac ([zmult_commute, zmult_0] MRS trans) 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
390 |
qed "zmult_0_right"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
391 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
392 |
goal Integ.thy "z * $#Suc(0) = z"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
393 |
by (rtac ([zmult_commute, zmult_1] MRS trans) 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
394 |
qed "zmult_1_right"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
395 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
396 |
goal Integ.thy "((z1::int) * z2) * z3 = z1 * (z2 * z3)"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
397 |
by (res_inst_tac [("z","z1")] eq_Abs_Integ 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
398 |
by (res_inst_tac [("z","z2")] eq_Abs_Integ 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
399 |
by (res_inst_tac [("z","z3")] eq_Abs_Integ 1); |
1266 | 400 |
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
|
401 |
qed "zmult_assoc"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
402 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
403 |
(*For AC rewriting*) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
404 |
qed_goal "zmult_left_commute" Integ.thy |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
405 |
"(z1::int)*(z2*z3) = z2*(z1*z3)" |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
406 |
(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
|
407 |
rtac (zmult_commute RS arg_cong) 1]); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
408 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
409 |
(*Integer multiplication is an AC operator*) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
410 |
val zmult_ac = [zmult_assoc, zmult_commute, zmult_left_commute]; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
411 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
412 |
goal Integ.thy "((z1::int) + z2) * w = (z1 * w) + (z2 * w)"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
413 |
by (res_inst_tac [("z","z1")] eq_Abs_Integ 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
414 |
by (res_inst_tac [("z","z2")] eq_Abs_Integ 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
415 |
by (res_inst_tac [("z","w")] eq_Abs_Integ 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
416 |
by (asm_simp_tac |
1266 | 417 |
(!simpset addsimps ([zadd, zmult] @ add_ac @ mult_ac)) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
418 |
qed "zadd_zmult_distrib"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
419 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
420 |
val zmult_commute'= read_instantiate [("z","w")] zmult_commute; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
421 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
422 |
goal Integ.thy "w * ($~ z) = $~ (w * z)"; |
1266 | 423 |
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
|
424 |
qed "zmult_zminus_right"; |
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 |
goal Integ.thy "(w::int) * (z1 + z2) = (w * z1) + (w * z2)"; |
1266 | 427 |
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
|
428 |
qed "zadd_zmult_distrib2"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
429 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
430 |
val zadd_simps = |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
431 |
[zadd_0, zadd_0_right, zadd_zminus_inverse, zadd_zminus_inverse2]; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
432 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
433 |
val zminus_simps = [zminus_zminus, zminus_0, zminus_zadd_distrib]; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
434 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
435 |
val zmult_simps = [zmult_0, zmult_1, zmult_0_right, zmult_1_right, |
1465 | 436 |
zmult_zminus, zmult_zminus_right]; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
437 |
|
1266 | 438 |
Addsimps (zadd_simps @ zminus_simps @ zmult_simps @ |
439 |
[zmagnitude_znat, zmagnitude_zminus_znat]); |
|
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
440 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
441 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
442 |
(**** Additional Theorems (by Mattolini; proofs mainly by lcp) ****) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
443 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
444 |
(* Some Theorems about zsuc and zpred *) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
445 |
goalw Integ.thy [zsuc_def] "$#(Suc(n)) = zsuc($# n)"; |
1266 | 446 |
by (simp_tac (!simpset addsimps [znat_add RS sym]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
447 |
qed "znat_Suc"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
448 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
449 |
goalw Integ.thy [zpred_def,zsuc_def,zdiff_def] "$~ zsuc(z) = zpred($~ z)"; |
1266 | 450 |
by (Simp_tac 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
451 |
qed "zminus_zsuc"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
452 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
453 |
goalw Integ.thy [zpred_def,zsuc_def,zdiff_def] "$~ zpred(z) = zsuc($~ z)"; |
1266 | 454 |
by (Simp_tac 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
455 |
qed "zminus_zpred"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
456 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
457 |
goalw Integ.thy [zsuc_def,zpred_def,zdiff_def] |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
458 |
"zpred(zsuc(z)) = z"; |
1266 | 459 |
by (simp_tac (!simpset addsimps [zadd_assoc]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
460 |
qed "zpred_zsuc"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
461 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
462 |
goalw Integ.thy [zsuc_def,zpred_def,zdiff_def] |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
463 |
"zsuc(zpred(z)) = z"; |
1266 | 464 |
by (simp_tac (!simpset addsimps [zadd_assoc]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
465 |
qed "zsuc_zpred"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
466 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
467 |
goal Integ.thy "(zpred(z)=w) = (z=zsuc(w))"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
468 |
by (safe_tac HOL_cs); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
469 |
by (rtac (zsuc_zpred RS sym) 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
470 |
by (rtac zpred_zsuc 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
471 |
qed "zpred_to_zsuc"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
472 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
473 |
goal Integ.thy "(zsuc(z)=w)=(z=zpred(w))"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
474 |
by (safe_tac HOL_cs); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
475 |
by (rtac (zpred_zsuc RS sym) 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
476 |
by (rtac zsuc_zpred 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
477 |
qed "zsuc_to_zpred"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
478 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
479 |
goal Integ.thy "($~ z = w) = (z = $~ w)"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
480 |
by (safe_tac HOL_cs); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
481 |
by (rtac (zminus_zminus RS sym) 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
482 |
by (rtac zminus_zminus 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
483 |
qed "zminus_exchange"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
484 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
485 |
goal Integ.thy"(zsuc(z)=zsuc(w)) = (z=w)"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
486 |
by (safe_tac intrel_cs); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
487 |
by (dres_inst_tac [("f","zpred")] arg_cong 1); |
1266 | 488 |
by (asm_full_simp_tac (!simpset addsimps [zpred_zsuc]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
489 |
qed "bijective_zsuc"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
490 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
491 |
goal Integ.thy"(zpred(z)=zpred(w)) = (z=w)"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
492 |
by (safe_tac intrel_cs); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
493 |
by (dres_inst_tac [("f","zsuc")] arg_cong 1); |
1266 | 494 |
by (asm_full_simp_tac (!simpset addsimps [zsuc_zpred]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
495 |
qed "bijective_zpred"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
496 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
497 |
(* Additional Theorems about zadd *) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
498 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
499 |
goalw Integ.thy [zsuc_def] "zsuc(z) + w = zsuc(z+w)"; |
1266 | 500 |
by (simp_tac (!simpset addsimps zadd_ac) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
501 |
qed "zadd_zsuc"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
502 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
503 |
goalw Integ.thy [zsuc_def] "w + zsuc(z) = zsuc(w+z)"; |
1266 | 504 |
by (simp_tac (!simpset addsimps zadd_ac) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
505 |
qed "zadd_zsuc_right"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
506 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
507 |
goalw Integ.thy [zpred_def,zdiff_def] "zpred(z) + w = zpred(z+w)"; |
1266 | 508 |
by (simp_tac (!simpset addsimps zadd_ac) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
509 |
qed "zadd_zpred"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
510 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
511 |
goalw Integ.thy [zpred_def,zdiff_def] "w + zpred(z) = zpred(w+z)"; |
1266 | 512 |
by (simp_tac (!simpset addsimps zadd_ac) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
513 |
qed "zadd_zpred_right"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
514 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
515 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
516 |
(* Additional Theorems about zmult *) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
517 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
518 |
goalw Integ.thy [zsuc_def] "zsuc(w) * z = z + w * z"; |
1266 | 519 |
by (simp_tac (!simpset addsimps [zadd_zmult_distrib, zadd_commute]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
520 |
qed "zmult_zsuc"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
521 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
522 |
goalw Integ.thy [zsuc_def] "z * zsuc(w) = z + w * z"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
523 |
by (simp_tac |
1266 | 524 |
(!simpset addsimps [zadd_zmult_distrib2, zadd_commute, zmult_commute]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
525 |
qed "zmult_zsuc_right"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
526 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
527 |
goalw Integ.thy [zpred_def, zdiff_def] "zpred(w) * z = w * z - z"; |
1266 | 528 |
by (simp_tac (!simpset addsimps [zadd_zmult_distrib]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
529 |
qed "zmult_zpred"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
530 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
531 |
goalw Integ.thy [zpred_def, zdiff_def] "z * zpred(w) = w * z - z"; |
1266 | 532 |
by (simp_tac (!simpset addsimps [zadd_zmult_distrib2, zmult_commute]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
533 |
qed "zmult_zpred_right"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
534 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
535 |
(* Further Theorems about zsuc and zpred *) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
536 |
goal Integ.thy "$#Suc(m) ~= $#0"; |
1266 | 537 |
by (simp_tac (!simpset addsimps [inj_znat RS inj_eq]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
538 |
qed "znat_Suc_not_znat_Zero"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
539 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
540 |
bind_thm ("znat_Zero_not_znat_Suc", (znat_Suc_not_znat_Zero RS not_sym)); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
541 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
542 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
543 |
goalw Integ.thy [zsuc_def,znat_def] "w ~= zsuc(w)"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
544 |
by (res_inst_tac [("z","w")] eq_Abs_Integ 1); |
1266 | 545 |
by (asm_full_simp_tac (!simpset addsimps [zadd]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
546 |
qed "n_not_zsuc_n"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
547 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
548 |
val zsuc_n_not_n = n_not_zsuc_n RS not_sym; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
549 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
550 |
goal Integ.thy "w ~= zpred(w)"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
551 |
by (safe_tac HOL_cs); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
552 |
by (dres_inst_tac [("x","w"),("f","zsuc")] arg_cong 1); |
1266 | 553 |
by (asm_full_simp_tac (!simpset addsimps [zsuc_zpred,zsuc_n_not_n]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
554 |
qed "n_not_zpred_n"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
555 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
556 |
val zpred_n_not_n = n_not_zpred_n RS not_sym; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
557 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
558 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
559 |
(* Theorems about less and less_equal *) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
560 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
561 |
goalw Integ.thy [zless_def, znegative_def, zdiff_def, znat_def] |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
562 |
"!!w. w<z ==> ? n. z = w + $#(Suc(n))"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
563 |
by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
564 |
by (res_inst_tac [("z","w")] eq_Abs_Integ 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
565 |
by (safe_tac intrel_cs); |
1266 | 566 |
by (asm_full_simp_tac (!simpset addsimps [zadd, zminus]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
567 |
by (safe_tac (intrel_cs addSDs [less_eq_Suc_add])); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
568 |
by (res_inst_tac [("x","k")] exI 1); |
1266 | 569 |
by (asm_full_simp_tac (!simpset delsimps [add_Suc, add_Suc_right] |
570 |
addsimps ([add_Suc RS sym] @ add_ac)) 1); |
|
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
571 |
(*To cancel x2, rename it to be first!*) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
572 |
by (rename_tac "a b c" 1); |
1266 | 573 |
by (asm_full_simp_tac (!simpset delsimps [add_Suc_right] |
574 |
addsimps (add_left_cancel::add_ac)) 1); |
|
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
575 |
qed "zless_eq_zadd_Suc"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
576 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
577 |
goalw Integ.thy [zless_def, znegative_def, zdiff_def, znat_def] |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
578 |
"z < z + $#(Suc(n))"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
579 |
by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
580 |
by (safe_tac intrel_cs); |
1266 | 581 |
by (simp_tac (!simpset addsimps [zadd, zminus]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
582 |
by (REPEAT_SOME (ares_tac [refl, exI, singletonI, ImageI, conjI, intrelI])); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
583 |
by (rtac le_less_trans 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
584 |
by (rtac lessI 2); |
1266 | 585 |
by (asm_simp_tac (!simpset addsimps ([le_add1,add_left_cancel_le]@add_ac)) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
586 |
qed "zless_zadd_Suc"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
587 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
588 |
goal Integ.thy "!!z1 z2 z3. [| z1<z2; z2<z3 |] ==> z1 < (z3::int)"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
589 |
by (safe_tac (HOL_cs addSDs [zless_eq_zadd_Suc])); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
590 |
by (simp_tac |
1266 | 591 |
(!simpset addsimps [zadd_assoc, zless_zadd_Suc, znat_add RS sym]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
592 |
qed "zless_trans"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
593 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
594 |
goalw Integ.thy [zsuc_def] "z<zsuc(z)"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
595 |
by (rtac zless_zadd_Suc 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
596 |
qed "zlessI"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
597 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
598 |
val zless_zsucI = zlessI RSN (2,zless_trans); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
599 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
600 |
goal Integ.thy "!!z w::int. z<w ==> ~w<z"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
601 |
by (safe_tac (HOL_cs addSDs [zless_eq_zadd_Suc])); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
602 |
by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
603 |
by (safe_tac intrel_cs); |
1266 | 604 |
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
|
605 |
by (asm_full_simp_tac |
1266 | 606 |
(!simpset delsimps [add_Suc_right] addsimps [add_left_cancel, add_assoc, add_Suc_right RS sym]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
607 |
by (resolve_tac [less_not_refl2 RS notE] 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
608 |
by (etac sym 2); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
609 |
by (REPEAT (resolve_tac [lessI, trans_less_add2, less_SucI] 1)); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
610 |
qed "zless_not_sym"; |
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 |
(* [| n<m; m<n |] ==> R *) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
613 |
bind_thm ("zless_asym", (zless_not_sym RS notE)); |
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 |
goal Integ.thy "!!z::int. ~ z<z"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
616 |
by (resolve_tac [zless_asym RS notI] 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
617 |
by (REPEAT (assume_tac 1)); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
618 |
qed "zless_not_refl"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
619 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
620 |
(* z<z ==> R *) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
621 |
bind_thm ("zless_anti_refl", (zless_not_refl RS notE)); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
622 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
623 |
goal Integ.thy "!!w. z<w ==> w ~= (z::int)"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
624 |
by(fast_tac (HOL_cs addEs [zless_anti_refl]) 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
625 |
qed "zless_not_refl2"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
626 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
627 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
628 |
(*"Less than" is a linear ordering*) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
629 |
goalw Integ.thy [zless_def, znegative_def, zdiff_def] |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
630 |
"z<w | z=w | w<(z::int)"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
631 |
by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
632 |
by (res_inst_tac [("z","w")] eq_Abs_Integ 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
633 |
by (safe_tac intrel_cs); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
634 |
by (asm_full_simp_tac |
1266 | 635 |
(!simpset addsimps [zadd, zminus, Image_iff, Bex_def]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
636 |
by (res_inst_tac [("m1", "x+ya"), ("n1", "xa+y")] (less_linear RS disjE) 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
637 |
by (etac disjE 2); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
638 |
by (assume_tac 2); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
639 |
by (DEPTH_SOLVE |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
640 |
(swap_res_tac [exI] 1 THEN |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
641 |
swap_res_tac [exI] 1 THEN |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
642 |
etac conjI 1 THEN |
1266 | 643 |
simp_tac (!simpset addsimps add_ac) 1)); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
644 |
qed "zless_linear"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
645 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
646 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
647 |
(*** Properties of <= ***) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
648 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
649 |
goalw Integ.thy [zless_def, znegative_def, zdiff_def, znat_def] |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
650 |
"($#m < $#n) = (m<n)"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
651 |
by (simp_tac |
1266 | 652 |
(!simpset addsimps [zadd, zminus, Image_iff, Bex_def]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
653 |
by (fast_tac (HOL_cs addIs [add_commute] addSEs [less_add_eq_less]) 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
654 |
qed "zless_eq_less"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
655 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
656 |
goalw Integ.thy [zle_def, le_def] "($#m <= $#n) = (m<=n)"; |
1266 | 657 |
by (simp_tac (!simpset addsimps [zless_eq_less]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
658 |
qed "zle_eq_le"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
659 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
660 |
goalw Integ.thy [zle_def] "!!w. ~(w<z) ==> z<=(w::int)"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
661 |
by (assume_tac 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
662 |
qed "zleI"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
663 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
664 |
goalw Integ.thy [zle_def] "!!w. z<=w ==> ~(w<(z::int))"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
665 |
by (assume_tac 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
666 |
qed "zleD"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
667 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
668 |
val zleE = make_elim zleD; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
669 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
670 |
goalw Integ.thy [zle_def] "!!z. ~ z <= w ==> w<(z::int)"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
671 |
by (fast_tac HOL_cs 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
672 |
qed "not_zleE"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
673 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
674 |
goalw Integ.thy [zle_def] "!!z. z < w ==> z <= (w::int)"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
675 |
by (fast_tac (HOL_cs addEs [zless_asym]) 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
676 |
qed "zless_imp_zle"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
677 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
678 |
goalw Integ.thy [zle_def] "!!z. z <= w ==> z < w | z=(w::int)"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
679 |
by (cut_facts_tac [zless_linear] 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
680 |
by (fast_tac (HOL_cs addEs [zless_anti_refl,zless_asym]) 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
681 |
qed "zle_imp_zless_or_eq"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
682 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
683 |
goalw Integ.thy [zle_def] "!!z. z<w | z=w ==> z <=(w::int)"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
684 |
by (cut_facts_tac [zless_linear] 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
685 |
by (fast_tac (HOL_cs addEs [zless_anti_refl,zless_asym]) 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
686 |
qed "zless_or_eq_imp_zle"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
687 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
688 |
goal Integ.thy "(x <= (y::int)) = (x < y | x=y)"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
689 |
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
|
690 |
qed "zle_eq_zless_or_eq"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
691 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
692 |
goal Integ.thy "w <= (w::int)"; |
1266 | 693 |
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
|
694 |
qed "zle_refl"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
695 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
696 |
val prems = goal Integ.thy "!!i. [| i <= j; j < k |] ==> i < (k::int)"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
697 |
by (dtac zle_imp_zless_or_eq 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
698 |
by (fast_tac (HOL_cs addIs [zless_trans]) 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
699 |
qed "zle_zless_trans"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
700 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
701 |
goal Integ.thy "!!i. [| i <= j; j <= k |] ==> i <= (k::int)"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
702 |
by (EVERY1 [dtac zle_imp_zless_or_eq, dtac zle_imp_zless_or_eq, |
1465 | 703 |
rtac zless_or_eq_imp_zle, fast_tac (HOL_cs addIs [zless_trans])]); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
704 |
qed "zle_trans"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
705 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
706 |
goal Integ.thy "!!z. [| z <= w; w <= z |] ==> z = (w::int)"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
707 |
by (EVERY1 [dtac zle_imp_zless_or_eq, dtac zle_imp_zless_or_eq, |
1465 | 708 |
fast_tac (HOL_cs addEs [zless_anti_refl,zless_asym])]); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
709 |
qed "zle_anti_sym"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
710 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
711 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
712 |
goal Integ.thy "!!w w' z::int. z + w' = z + w ==> w' = w"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
713 |
by (dres_inst_tac [("f", "%x. x + $~z")] arg_cong 1); |
1266 | 714 |
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
|
715 |
qed "zadd_left_cancel"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
716 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
717 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
718 |
(*** Monotonicity results ***) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
719 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
720 |
goal Integ.thy "!!v w z::int. v < w ==> v + z < w + z"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
721 |
by (safe_tac (HOL_cs addSDs [zless_eq_zadd_Suc])); |
1266 | 722 |
by (simp_tac (!simpset addsimps zadd_ac) 1); |
723 |
by (simp_tac (!simpset addsimps [zadd_assoc RS sym, zless_zadd_Suc]) 1); |
|
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
724 |
qed "zadd_zless_mono1"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
725 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
726 |
goal Integ.thy "!!v w z::int. (v+z < w+z) = (v < w)"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
727 |
by (safe_tac (HOL_cs addSEs [zadd_zless_mono1])); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
728 |
by (dres_inst_tac [("z", "$~z")] zadd_zless_mono1 1); |
1266 | 729 |
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
|
730 |
qed "zadd_left_cancel_zless"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
731 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
732 |
goal Integ.thy "!!v w z::int. (v+z <= w+z) = (v <= w)"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
733 |
by (asm_full_simp_tac |
1266 | 734 |
(!simpset addsimps [zle_def, zadd_left_cancel_zless]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
735 |
qed "zadd_left_cancel_zle"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
736 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
737 |
(*"v<=w ==> v+z <= w+z"*) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
738 |
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
|
739 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
740 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
741 |
goal Integ.thy "!!z' z::int. [| w'<=w; z'<=z |] ==> w' + z' <= w + z"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
742 |
by (etac (zadd_zle_mono1 RS zle_trans) 1); |
1266 | 743 |
by (simp_tac (!simpset addsimps [zadd_commute]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
744 |
(*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
|
745 |
by (etac zadd_zle_mono1 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
746 |
qed "zadd_zle_mono"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
747 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
748 |
goal Integ.thy "!!w z::int. z<=$#0 ==> w+z <= w"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
749 |
by (dres_inst_tac [("z", "w")] zadd_zle_mono1 1); |
1266 | 750 |
by (asm_full_simp_tac (!simpset addsimps [zadd_commute]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
751 |
qed "zadd_zle_self"; |