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