src/ZF/ex/integ.ML
 author lcp Tue Aug 16 18:58:42 1994 +0200 (1994-08-16) changeset 532 851df239ac8b parent 29 4ec9b266ccd1 permissions -rw-r--r--
ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
 clasohm@0 ` 1` ```(* Title: ZF/ex/integ.ML ``` clasohm@0 ` 2` ``` ID: \$Id\$ ``` clasohm@0 ` 3` ``` Author: Lawrence C Paulson, Cambridge University Computer Laboratory ``` clasohm@0 ` 4` ``` Copyright 1993 University of Cambridge ``` clasohm@0 ` 5` clasohm@0 ` 6` ```For integ.thy. The integers as equivalence classes over nat*nat. ``` clasohm@0 ` 7` clasohm@0 ` 8` ```Could also prove... ``` clasohm@0 ` 9` ```"znegative(z) ==> \$# zmagnitude(z) = \$~ z" ``` clasohm@0 ` 10` ```"~ znegative(z) ==> \$# zmagnitude(z) = z" ``` clasohm@0 ` 11` ```\$< is a linear ordering ``` clasohm@0 ` 12` ```\$+ and \$* are monotonic wrt \$< ``` clasohm@0 ` 13` ```*) ``` clasohm@0 ` 14` lcp@7 ` 15` ```val add_cong = ``` lcp@7 ` 16` ``` read_instantiate_sg (sign_of Arith.thy) [("t","op #+")] subst_context2; ``` clasohm@0 ` 17` lcp@7 ` 18` lcp@7 ` 19` ```open Integ; ``` clasohm@0 ` 20` clasohm@0 ` 21` ```(*** Proving that intrel is an equivalence relation ***) ``` clasohm@0 ` 22` clasohm@0 ` 23` ```val prems = goal Arith.thy ``` clasohm@0 ` 24` ``` "[| m #+ n = m' #+ n'; m: nat; m': nat |] \ ``` clasohm@0 ` 25` ```\ ==> m #+ (n #+ k) = m' #+ (n' #+ k)"; ``` lcp@7 ` 26` ```by (asm_simp_tac (arith_ss addsimps ([add_assoc RS sym] @ prems)) 1); ``` clasohm@0 ` 27` ```val add_assoc_cong = result(); ``` clasohm@0 ` 28` clasohm@0 ` 29` ```val prems = goal Arith.thy ``` clasohm@0 ` 30` ``` "[| m: nat; n: nat |] \ ``` clasohm@0 ` 31` ```\ ==> m #+ (n #+ k) = n #+ (m #+ k)"; ``` clasohm@0 ` 32` ```by (REPEAT (resolve_tac ([add_commute RS add_assoc_cong] @ prems) 1)); ``` clasohm@0 ` 33` ```val add_assoc_swap = result(); ``` clasohm@0 ` 34` clasohm@0 ` 35` ```val add_kill = (refl RS add_cong); ``` lcp@7 ` 36` clasohm@0 ` 37` ```val add_assoc_swap_kill = add_kill RSN (3, add_assoc_swap RS trans); ``` clasohm@0 ` 38` clasohm@0 ` 39` ```(*By luck, requires no typing premises for y1, y2,y3*) ``` clasohm@0 ` 40` ```val eqa::eqb::prems = goal Arith.thy ``` clasohm@0 ` 41` ``` "[| x1 #+ y2 = x2 #+ y1; x2 #+ y3 = x3 #+ y2; \ ``` clasohm@0 ` 42` ```\ x1: nat; x2: nat; x3: nat |] ==> x1 #+ y3 = x3 #+ y1"; ``` clasohm@0 ` 43` ```by (res_inst_tac [("k","x2")] add_left_cancel 1); ``` clasohm@0 ` 44` ```by (resolve_tac prems 1); ``` clasohm@0 ` 45` ```by (rtac (add_assoc_swap RS trans) 1 THEN typechk_tac prems); ``` clasohm@0 ` 46` ```by (rtac (eqb RS ssubst) 1); ``` clasohm@0 ` 47` ```by (rtac (add_assoc_swap RS trans) 1 THEN typechk_tac prems); ``` clasohm@0 ` 48` ```by (rtac (eqa RS ssubst) 1); ``` clasohm@0 ` 49` ```by (rtac (add_assoc_swap) 1 THEN typechk_tac prems); ``` clasohm@0 ` 50` ```val integ_trans_lemma = result(); ``` clasohm@0 ` 51` clasohm@0 ` 52` ```(** Natural deduction for intrel **) ``` clasohm@0 ` 53` clasohm@0 ` 54` ```val prems = goalw Integ.thy [intrel_def] ``` clasohm@0 ` 55` ``` "[| x1#+y2 = x2#+y1; x1: nat; y1: nat; x2: nat; y2: nat |] ==> \ ``` clasohm@0 ` 56` ```\ <,>: intrel"; ``` clasohm@0 ` 57` ```by (fast_tac (ZF_cs addIs prems) 1); ``` clasohm@0 ` 58` ```val intrelI = result(); ``` clasohm@0 ` 59` clasohm@0 ` 60` ```(*intrelE is hard to derive because fast_tac tries hyp_subst_tac so soon*) ``` clasohm@0 ` 61` ```goalw Integ.thy [intrel_def] ``` clasohm@0 ` 62` ``` "p: intrel --> (EX x1 y1 x2 y2. \ ``` clasohm@0 ` 63` ```\ p = <,> & x1#+y2 = x2#+y1 & \ ``` clasohm@0 ` 64` ```\ x1: nat & y1: nat & x2: nat & y2: nat)"; ``` clasohm@0 ` 65` ```by (fast_tac ZF_cs 1); ``` clasohm@0 ` 66` ```val intrelE_lemma = result(); ``` clasohm@0 ` 67` clasohm@0 ` 68` ```val [major,minor] = goal Integ.thy ``` clasohm@0 ` 69` ``` "[| p: intrel; \ ``` clasohm@0 ` 70` ```\ !!x1 y1 x2 y2. [| p = <,>; x1#+y2 = x2#+y1; \ ``` clasohm@0 ` 71` ```\ x1: nat; y1: nat; x2: nat; y2: nat |] ==> Q |] \ ``` clasohm@0 ` 72` ```\ ==> Q"; ``` clasohm@0 ` 73` ```by (cut_facts_tac [major RS (intrelE_lemma RS mp)] 1); ``` clasohm@0 ` 74` ```by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1)); ``` clasohm@0 ` 75` ```val intrelE = result(); ``` clasohm@0 ` 76` clasohm@0 ` 77` ```val intrel_cs = ZF_cs addSIs [intrelI] addSEs [intrelE]; ``` clasohm@0 ` 78` clasohm@0 ` 79` ```goal Integ.thy ``` clasohm@0 ` 80` ``` "<,>: intrel <-> \ ``` clasohm@0 ` 81` ```\ x1#+y2 = x2#+y1 & x1: nat & y1: nat & x2: nat & y2: nat"; ``` clasohm@0 ` 82` ```by (fast_tac intrel_cs 1); ``` clasohm@0 ` 83` ```val intrel_iff = result(); ``` clasohm@0 ` 84` clasohm@0 ` 85` ```val prems = goalw Integ.thy [equiv_def] "equiv(nat*nat, intrel)"; ``` clasohm@0 ` 86` ```by (safe_tac intrel_cs); ``` clasohm@0 ` 87` ```by (rewtac refl_def); ``` clasohm@0 ` 88` ```by (fast_tac intrel_cs 1); ``` clasohm@0 ` 89` ```by (rewtac sym_def); ``` clasohm@0 ` 90` ```by (fast_tac (intrel_cs addSEs [sym]) 1); ``` clasohm@0 ` 91` ```by (rewtac trans_def); ``` clasohm@0 ` 92` ```by (fast_tac (intrel_cs addSEs [integ_trans_lemma]) 1); ``` clasohm@0 ` 93` ```val equiv_intrel = result(); ``` clasohm@0 ` 94` clasohm@0 ` 95` lcp@7 ` 96` ```val intrel_ss = ``` lcp@7 ` 97` ``` arith_ss addsimps [equiv_intrel RS eq_equiv_class_iff, intrel_iff]; ``` clasohm@0 ` 98` lcp@7 ` 99` ```(*Roughly twice as fast as simplifying with intrel_ss*) ``` clasohm@0 ` 100` ```fun INTEG_SIMP_TAC ths = ``` lcp@7 ` 101` ``` let val ss = arith_ss addsimps ths ``` clasohm@0 ` 102` ``` in fn i => ``` lcp@7 ` 103` ``` EVERY [asm_simp_tac ss i, ``` clasohm@0 ` 104` ``` rtac (intrelI RS (equiv_intrel RS equiv_class_eq)) i, ``` clasohm@0 ` 105` ``` typechk_tac (ZF_typechecks@nat_typechecks@arith_typechecks), ``` lcp@7 ` 106` ``` asm_simp_tac ss i] ``` clasohm@0 ` 107` ``` end; ``` clasohm@0 ` 108` clasohm@0 ` 109` clasohm@0 ` 110` ```(** znat: the injection from nat to integ **) ``` clasohm@0 ` 111` clasohm@0 ` 112` ```val prems = goalw Integ.thy [integ_def,quotient_def,znat_def] ``` clasohm@0 ` 113` ``` "m : nat ==> \$#m : integ"; ``` clasohm@0 ` 114` ```by (fast_tac (ZF_cs addSIs (nat_0I::prems)) 1); ``` clasohm@0 ` 115` ```val znat_type = result(); ``` clasohm@0 ` 116` clasohm@0 ` 117` ```val [major,nnat] = goalw Integ.thy [znat_def] ``` clasohm@0 ` 118` ``` "[| \$#m = \$#n; n: nat |] ==> m=n"; ``` clasohm@0 ` 119` ```by (rtac (make_elim (major RS eq_equiv_class)) 1); ``` clasohm@0 ` 120` ```by (rtac equiv_intrel 1); ``` clasohm@0 ` 121` ```by (typechk_tac [nat_0I,nnat,SigmaI]); ``` clasohm@0 ` 122` ```by (safe_tac (intrel_cs addSEs [box_equals,add_0_right])); ``` clasohm@0 ` 123` ```val znat_inject = result(); ``` clasohm@0 ` 124` clasohm@0 ` 125` clasohm@0 ` 126` ```(**** zminus: unary negation on integ ****) ``` clasohm@0 ` 127` clasohm@0 ` 128` ```goalw Integ.thy [congruent_def] ``` clasohm@0 ` 129` ``` "congruent(intrel, split(%x y. intrel``{}))"; ``` clasohm@0 ` 130` ```by (safe_tac intrel_cs); ``` lcp@7 ` 131` ```by (ALLGOALS (asm_simp_tac intrel_ss)); ``` clasohm@0 ` 132` ```by (etac (box_equals RS sym) 1); ``` clasohm@0 ` 133` ```by (REPEAT (ares_tac [add_commute] 1)); ``` clasohm@0 ` 134` ```val zminus_congruent = result(); ``` clasohm@0 ` 135` clasohm@0 ` 136` ```(*Resolve th against the corresponding facts for zminus*) ``` clasohm@0 ` 137` ```val zminus_ize = RSLIST [equiv_intrel, zminus_congruent]; ``` clasohm@0 ` 138` clasohm@0 ` 139` ```val [prem] = goalw Integ.thy [integ_def,zminus_def] ``` clasohm@0 ` 140` ``` "z : integ ==> \$~z : integ"; ``` clasohm@0 ` 141` ```by (typechk_tac [split_type, SigmaI, prem, zminus_ize UN_equiv_class_type, ``` clasohm@0 ` 142` ``` quotientI]); ``` clasohm@0 ` 143` ```val zminus_type = result(); ``` clasohm@0 ` 144` clasohm@0 ` 145` ```val major::prems = goalw Integ.thy [integ_def,zminus_def] ``` clasohm@0 ` 146` ``` "[| \$~z = \$~w; z: integ; w: integ |] ==> z=w"; ``` clasohm@0 ` 147` ```by (rtac (major RS zminus_ize UN_equiv_class_inject) 1); ``` clasohm@0 ` 148` ```by (REPEAT (ares_tac prems 1)); ``` clasohm@0 ` 149` ```by (REPEAT (etac SigmaE 1)); ``` clasohm@0 ` 150` ```by (etac rev_mp 1); ``` lcp@7 ` 151` ```by (asm_simp_tac ZF_ss 1); ``` clasohm@0 ` 152` ```by (fast_tac (intrel_cs addSIs [SigmaI, equiv_intrel] ``` clasohm@0 ` 153` ``` addSEs [box_equals RS sym, add_commute, ``` clasohm@0 ` 154` ``` make_elim eq_equiv_class]) 1); ``` clasohm@0 ` 155` ```val zminus_inject = result(); ``` clasohm@0 ` 156` clasohm@0 ` 157` ```val prems = goalw Integ.thy [zminus_def] ``` clasohm@0 ` 158` ``` "[| x: nat; y: nat |] ==> \$~ (intrel``{}) = intrel `` {}"; ``` lcp@7 ` 159` ```by (asm_simp_tac ``` lcp@7 ` 160` ``` (ZF_ss addsimps (prems@[zminus_ize UN_equiv_class, SigmaI])) 1); ``` clasohm@0 ` 161` ```val zminus = result(); ``` clasohm@0 ` 162` clasohm@0 ` 163` ```goalw Integ.thy [integ_def] "!!z. z : integ ==> \$~ (\$~ z) = z"; ``` clasohm@0 ` 164` ```by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1)); ``` lcp@7 ` 165` ```by (asm_simp_tac (ZF_ss addsimps [zminus]) 1); ``` clasohm@0 ` 166` ```val zminus_zminus = result(); ``` clasohm@0 ` 167` clasohm@0 ` 168` ```goalw Integ.thy [integ_def, znat_def] "\$~ (\$#0) = \$#0"; ``` lcp@7 ` 169` ```by (simp_tac (arith_ss addsimps [zminus]) 1); ``` clasohm@0 ` 170` ```val zminus_0 = result(); ``` clasohm@0 ` 171` clasohm@0 ` 172` clasohm@0 ` 173` ```(**** znegative: the test for negative integers ****) ``` clasohm@0 ` 174` clasohm@0 ` 175` ```goalw Integ.thy [znegative_def, znat_def] ``` clasohm@0 ` 176` ``` "~ znegative(\$# n)"; ``` clasohm@0 ` 177` ```by (safe_tac intrel_cs); ``` lcp@29 ` 178` ```by (rtac (add_le_self2 RS le_imp_not_lt RS notE) 1); ``` clasohm@0 ` 179` ```by (etac ssubst 3); ``` lcp@7 ` 180` ```by (asm_simp_tac (arith_ss addsimps [add_0_right]) 3); ``` clasohm@0 ` 181` ```by (REPEAT (assume_tac 1)); ``` clasohm@0 ` 182` ```val not_znegative_znat = result(); ``` clasohm@0 ` 183` lcp@29 ` 184` ```goalw Integ.thy [znegative_def, znat_def] ``` lcp@29 ` 185` ``` "!!n. n: nat ==> znegative(\$~ \$# succ(n))"; ``` lcp@29 ` 186` ```by (asm_simp_tac (intrel_ss addsimps [zminus]) 1); ``` clasohm@0 ` 187` ```by (REPEAT ``` lcp@29 ` 188` ``` (ares_tac [refl, exI, conjI, nat_0_le, ``` lcp@29 ` 189` ``` refl RS intrelI RS imageI, consI1, nat_0I, nat_succI] 1)); ``` clasohm@0 ` 190` ```val znegative_zminus_znat = result(); ``` clasohm@0 ` 191` clasohm@0 ` 192` clasohm@0 ` 193` ```(**** zmagnitude: magnitide of an integer, as a natural number ****) ``` clasohm@0 ` 194` clasohm@0 ` 195` ```goalw Integ.thy [congruent_def] ``` clasohm@0 ` 196` ``` "congruent(intrel, split(%x y. (y#-x) #+ (x#-y)))"; ``` clasohm@0 ` 197` ```by (safe_tac intrel_cs); ``` lcp@7 ` 198` ```by (ALLGOALS (asm_simp_tac intrel_ss)); ``` clasohm@0 ` 199` ```by (etac rev_mp 1); ``` clasohm@0 ` 200` ```by (res_inst_tac [("m","x1"),("n","y1")] diff_induct 1); ``` clasohm@0 ` 201` ```by (REPEAT (assume_tac 1)); ``` lcp@7 ` 202` ```by (asm_simp_tac (arith_ss addsimps [add_succ_right,succ_inject_iff]) 3); ``` lcp@7 ` 203` ```by (asm_simp_tac ``` lcp@7 ` 204` ``` (arith_ss addsimps [diff_add_inverse,diff_add_0,add_0_right]) 2); ``` lcp@7 ` 205` ```by (asm_simp_tac (arith_ss addsimps [add_0_right]) 1); ``` clasohm@0 ` 206` ```by (rtac impI 1); ``` clasohm@0 ` 207` ```by (etac subst 1); ``` clasohm@0 ` 208` ```by (res_inst_tac [("m1","x")] (add_commute RS ssubst) 1); ``` clasohm@0 ` 209` ```by (REPEAT (assume_tac 1)); ``` lcp@7 ` 210` ```by (asm_simp_tac (arith_ss addsimps [diff_add_inverse,diff_add_0]) 1); ``` clasohm@0 ` 211` ```val zmagnitude_congruent = result(); ``` clasohm@0 ` 212` clasohm@0 ` 213` ```(*Resolve th against the corresponding facts for zmagnitude*) ``` clasohm@0 ` 214` ```val zmagnitude_ize = RSLIST [equiv_intrel, zmagnitude_congruent]; ``` clasohm@0 ` 215` clasohm@0 ` 216` ```val [prem] = goalw Integ.thy [integ_def,zmagnitude_def] ``` clasohm@0 ` 217` ``` "z : integ ==> zmagnitude(z) : nat"; ``` clasohm@0 ` 218` ```by (typechk_tac [split_type, prem, zmagnitude_ize UN_equiv_class_type, ``` clasohm@0 ` 219` ``` add_type, diff_type]); ``` clasohm@0 ` 220` ```val zmagnitude_type = result(); ``` clasohm@0 ` 221` clasohm@0 ` 222` ```val prems = goalw Integ.thy [zmagnitude_def] ``` clasohm@0 ` 223` ``` "[| x: nat; y: nat |] ==> \ ``` clasohm@0 ` 224` ```\ zmagnitude (intrel``{}) = (y #- x) #+ (x #- y)"; ``` lcp@7 ` 225` ```by (asm_simp_tac ``` lcp@7 ` 226` ``` (ZF_ss addsimps (prems@[zmagnitude_ize UN_equiv_class, SigmaI])) 1); ``` clasohm@0 ` 227` ```val zmagnitude = result(); ``` clasohm@0 ` 228` lcp@29 ` 229` ```goalw Integ.thy [znat_def] ``` lcp@29 ` 230` ``` "!!n. n: nat ==> zmagnitude(\$# n) = n"; ``` lcp@29 ` 231` ```by (asm_simp_tac (intrel_ss addsimps [zmagnitude]) 1); ``` clasohm@0 ` 232` ```val zmagnitude_znat = result(); ``` clasohm@0 ` 233` lcp@29 ` 234` ```goalw Integ.thy [znat_def] ``` lcp@29 ` 235` ``` "!!n. n: nat ==> zmagnitude(\$~ \$# n) = n"; ``` lcp@29 ` 236` ```by (asm_simp_tac (intrel_ss addsimps [zmagnitude, zminus ,add_0_right]) 1); ``` clasohm@0 ` 237` ```val zmagnitude_zminus_znat = result(); ``` clasohm@0 ` 238` clasohm@0 ` 239` clasohm@0 ` 240` ```(**** zadd: addition on integ ****) ``` clasohm@0 ` 241` clasohm@0 ` 242` ```(** Congruence property for addition **) ``` clasohm@0 ` 243` clasohm@0 ` 244` ```goalw Integ.thy [congruent2_def] ``` clasohm@0 ` 245` ``` "congruent2(intrel, %p1 p2. \ ``` clasohm@0 ` 246` ```\ split(%x1 y1. split(%x2 y2. intrel `` {}, p2), p1))"; ``` clasohm@0 ` 247` ```(*Proof via congruent2_commuteI seems longer*) ``` clasohm@0 ` 248` ```by (safe_tac intrel_cs); ``` clasohm@0 ` 249` ```by (INTEG_SIMP_TAC [add_assoc] 1); ``` clasohm@0 ` 250` ```(*The rest should be trivial, but rearranging terms is hard*) ``` clasohm@0 ` 251` ```by (res_inst_tac [("m1","x1a")] (add_assoc_swap RS ssubst) 1); ``` clasohm@0 ` 252` ```by (res_inst_tac [("m1","x2a")] (add_assoc_swap RS ssubst) 3); ``` clasohm@0 ` 253` ```by (typechk_tac [add_type]); ``` lcp@7 ` 254` ```by (asm_simp_tac (arith_ss addsimps [add_assoc RS sym]) 1); ``` clasohm@0 ` 255` ```val zadd_congruent2 = result(); ``` clasohm@0 ` 256` clasohm@0 ` 257` ```(*Resolve th against the corresponding facts for zadd*) ``` clasohm@0 ` 258` ```val zadd_ize = RSLIST [equiv_intrel, zadd_congruent2]; ``` clasohm@0 ` 259` clasohm@0 ` 260` ```val prems = goalw Integ.thy [integ_def,zadd_def] ``` clasohm@0 ` 261` ``` "[| z: integ; w: integ |] ==> z \$+ w : integ"; ``` clasohm@0 ` 262` ```by (REPEAT (ares_tac (prems@[zadd_ize UN_equiv_class_type2, ``` clasohm@0 ` 263` ``` split_type, add_type, quotientI, SigmaI]) 1)); ``` clasohm@0 ` 264` ```val zadd_type = result(); ``` clasohm@0 ` 265` clasohm@0 ` 266` ```val prems = goalw Integ.thy [zadd_def] ``` clasohm@0 ` 267` ``` "[| x1: nat; y1: nat; x2: nat; y2: nat |] ==> \ ``` clasohm@0 ` 268` ```\ (intrel``{}) \$+ (intrel``{}) = intrel `` {}"; ``` lcp@7 ` 269` ```by (asm_simp_tac (ZF_ss addsimps ``` clasohm@0 ` 270` ``` (prems @ [zadd_ize UN_equiv_class2, SigmaI])) 1); ``` clasohm@0 ` 271` ```val zadd = result(); ``` clasohm@0 ` 272` clasohm@0 ` 273` ```goalw Integ.thy [integ_def,znat_def] "!!z. z : integ ==> \$#0 \$+ z = z"; ``` clasohm@0 ` 274` ```by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1)); ``` lcp@7 ` 275` ```by (asm_simp_tac (arith_ss addsimps [zadd]) 1); ``` clasohm@0 ` 276` ```val zadd_0 = result(); ``` clasohm@0 ` 277` clasohm@0 ` 278` ```goalw Integ.thy [integ_def] ``` clasohm@0 ` 279` ``` "!!z w. [| z: integ; w: integ |] ==> \$~ (z \$+ w) = \$~ z \$+ \$~ w"; ``` clasohm@0 ` 280` ```by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1)); ``` lcp@7 ` 281` ```by (asm_simp_tac (arith_ss addsimps [zminus,zadd]) 1); ``` clasohm@0 ` 282` ```val zminus_zadd_distrib = result(); ``` clasohm@0 ` 283` clasohm@0 ` 284` ```goalw Integ.thy [integ_def] ``` clasohm@0 ` 285` ``` "!!z w. [| z: integ; w: integ |] ==> z \$+ w = w \$+ z"; ``` clasohm@0 ` 286` ```by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1)); ``` clasohm@0 ` 287` ```by (INTEG_SIMP_TAC [zadd] 1); ``` clasohm@0 ` 288` ```by (REPEAT (ares_tac [add_commute,add_cong] 1)); ``` clasohm@0 ` 289` ```val zadd_commute = result(); ``` clasohm@0 ` 290` clasohm@0 ` 291` ```goalw Integ.thy [integ_def] ``` clasohm@0 ` 292` ``` "!!z1 z2 z3. [| z1: integ; z2: integ; z3: integ |] ==> \ ``` clasohm@0 ` 293` ```\ (z1 \$+ z2) \$+ z3 = z1 \$+ (z2 \$+ z3)"; ``` clasohm@0 ` 294` ```by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1)); ``` clasohm@0 ` 295` ```(*rewriting is much faster without intrel_iff, etc.*) ``` lcp@7 ` 296` ```by (asm_simp_tac (arith_ss addsimps [zadd,add_assoc]) 1); ``` clasohm@0 ` 297` ```val zadd_assoc = result(); ``` clasohm@0 ` 298` clasohm@0 ` 299` ```val prems = goalw Integ.thy [znat_def] ``` clasohm@0 ` 300` ``` "[| m: nat; n: nat |] ==> \$# (m #+ n) = (\$#m) \$+ (\$#n)"; ``` lcp@7 ` 301` ```by (asm_simp_tac (arith_ss addsimps (zadd::prems)) 1); ``` clasohm@0 ` 302` ```val znat_add = result(); ``` clasohm@0 ` 303` clasohm@0 ` 304` ```goalw Integ.thy [integ_def,znat_def] "!!z. z : integ ==> z \$+ (\$~ z) = \$#0"; ``` clasohm@0 ` 305` ```by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1)); ``` lcp@7 ` 306` ```by (asm_simp_tac (intrel_ss addsimps [zminus,zadd,add_0_right]) 1); ``` clasohm@0 ` 307` ```by (REPEAT (ares_tac [add_commute] 1)); ``` clasohm@0 ` 308` ```val zadd_zminus_inverse = result(); ``` clasohm@0 ` 309` clasohm@0 ` 310` ```val prems = goal Integ.thy ``` clasohm@0 ` 311` ``` "z : integ ==> (\$~ z) \$+ z = \$#0"; ``` clasohm@0 ` 312` ```by (rtac (zadd_commute RS trans) 1); ``` clasohm@0 ` 313` ```by (REPEAT (resolve_tac (prems@[zminus_type, zadd_zminus_inverse]) 1)); ``` clasohm@0 ` 314` ```val zadd_zminus_inverse2 = result(); ``` clasohm@0 ` 315` clasohm@0 ` 316` ```val prems = goal Integ.thy "z:integ ==> z \$+ \$#0 = z"; ``` clasohm@0 ` 317` ```by (rtac (zadd_commute RS trans) 1); ``` clasohm@0 ` 318` ```by (REPEAT (resolve_tac (prems@[znat_type,nat_0I,zadd_0]) 1)); ``` clasohm@0 ` 319` ```val zadd_0_right = result(); ``` clasohm@0 ` 320` clasohm@0 ` 321` clasohm@0 ` 322` ```(*Need properties of \$- ??? Or use \$- just as an abbreviation? ``` clasohm@0 ` 323` ``` [| m: nat; n: nat; m>=n |] ==> \$# (m #- n) = (\$#m) \$- (\$#n) ``` clasohm@0 ` 324` ```*) ``` clasohm@0 ` 325` clasohm@0 ` 326` ```(**** zmult: multiplication on integ ****) ``` clasohm@0 ` 327` clasohm@0 ` 328` ```(** Congruence property for multiplication **) ``` clasohm@0 ` 329` clasohm@0 ` 330` ```val prems = goalw Integ.thy [znat_def] ``` clasohm@0 ` 331` ``` "[| k: nat; l: nat; m: nat; n: nat |] ==> \ ``` clasohm@0 ` 332` ```\ (k #+ l) #+ (m #+ n) = (k #+ m) #+ (n #+ l)"; ``` clasohm@0 ` 333` ```val add_commute' = read_instantiate [("m","l")] add_commute; ``` lcp@7 ` 334` ```by (simp_tac (arith_ss addsimps ([add_commute',add_assoc]@prems)) 1); ``` clasohm@0 ` 335` ```val zmult_congruent_lemma = result(); ``` clasohm@0 ` 336` clasohm@0 ` 337` ```goal Integ.thy ``` clasohm@0 ` 338` ``` "congruent2(intrel, %p1 p2. \ ``` clasohm@0 ` 339` ```\ split(%x1 y1. split(%x2 y2. \ ``` clasohm@0 ` 340` ```\ intrel``{}, p2), p1))"; ``` clasohm@0 ` 341` ```by (rtac (equiv_intrel RS congruent2_commuteI) 1); ``` clasohm@0 ` 342` ```by (safe_tac intrel_cs); ``` clasohm@0 ` 343` ```by (ALLGOALS (INTEG_SIMP_TAC [])); ``` clasohm@0 ` 344` ```(*Proof that zmult is congruent in one argument*) ``` clasohm@0 ` 345` ```by (rtac (zmult_congruent_lemma RS trans) 2); ``` clasohm@0 ` 346` ```by (rtac (zmult_congruent_lemma RS trans RS sym) 6); ``` clasohm@0 ` 347` ```by (typechk_tac [mult_type]); ``` lcp@7 ` 348` ```by (asm_simp_tac (arith_ss addsimps [add_mult_distrib_left RS sym]) 2); ``` clasohm@0 ` 349` ```(*Proof that zmult is commutative on representatives*) ``` clasohm@0 ` 350` ```by (rtac add_cong 1); ``` clasohm@0 ` 351` ```by (rtac (add_commute RS trans) 2); ``` clasohm@0 ` 352` ```by (REPEAT (ares_tac [mult_commute,add_type,mult_type,add_cong] 1)); ``` clasohm@0 ` 353` ```val zmult_congruent2 = result(); ``` clasohm@0 ` 354` clasohm@0 ` 355` ```(*Resolve th against the corresponding facts for zmult*) ``` clasohm@0 ` 356` ```val zmult_ize = RSLIST [equiv_intrel, zmult_congruent2]; ``` clasohm@0 ` 357` clasohm@0 ` 358` ```val prems = goalw Integ.thy [integ_def,zmult_def] ``` clasohm@0 ` 359` ``` "[| z: integ; w: integ |] ==> z \$* w : integ"; ``` clasohm@0 ` 360` ```by (REPEAT (ares_tac (prems@[zmult_ize UN_equiv_class_type2, ``` clasohm@0 ` 361` ``` split_type, add_type, mult_type, ``` clasohm@0 ` 362` ``` quotientI, SigmaI]) 1)); ``` clasohm@0 ` 363` ```val zmult_type = result(); ``` clasohm@0 ` 364` clasohm@0 ` 365` clasohm@0 ` 366` ```val prems = goalw Integ.thy [zmult_def] ``` clasohm@0 ` 367` ``` "[| x1: nat; y1: nat; x2: nat; y2: nat |] ==> \ ``` clasohm@0 ` 368` ```\ (intrel``{}) \$* (intrel``{}) = \ ``` clasohm@0 ` 369` ```\ intrel `` {}"; ``` lcp@7 ` 370` ```by (asm_simp_tac (ZF_ss addsimps ``` clasohm@0 ` 371` ``` (prems @ [zmult_ize UN_equiv_class2, SigmaI])) 1); ``` clasohm@0 ` 372` ```val zmult = result(); ``` clasohm@0 ` 373` clasohm@0 ` 374` ```goalw Integ.thy [integ_def,znat_def] "!!z. z : integ ==> \$#0 \$* z = \$#0"; ``` clasohm@0 ` 375` ```by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1)); ``` lcp@7 ` 376` ```by (asm_simp_tac (arith_ss addsimps [zmult]) 1); ``` clasohm@0 ` 377` ```val zmult_0 = result(); ``` clasohm@0 ` 378` lcp@16 ` 379` ```goalw Integ.thy [integ_def,znat_def] ``` clasohm@0 ` 380` ``` "!!z. z : integ ==> \$#1 \$* z = z"; ``` clasohm@0 ` 381` ```by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1)); ``` lcp@7 ` 382` ```by (asm_simp_tac (arith_ss addsimps [zmult,add_0_right]) 1); ``` clasohm@0 ` 383` ```val zmult_1 = result(); ``` clasohm@0 ` 384` clasohm@0 ` 385` ```goalw Integ.thy [integ_def] ``` clasohm@0 ` 386` ``` "!!z w. [| z: integ; w: integ |] ==> (\$~ z) \$* w = \$~ (z \$* w)"; ``` clasohm@0 ` 387` ```by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1)); ``` clasohm@0 ` 388` ```by (INTEG_SIMP_TAC [zminus,zmult] 1); ``` clasohm@0 ` 389` ```by (REPEAT (ares_tac [mult_type,add_commute,add_cong] 1)); ``` clasohm@0 ` 390` ```val zmult_zminus = result(); ``` clasohm@0 ` 391` clasohm@0 ` 392` ```goalw Integ.thy [integ_def] ``` clasohm@0 ` 393` ``` "!!z w. [| z: integ; w: integ |] ==> (\$~ z) \$* (\$~ w) = (z \$* w)"; ``` clasohm@0 ` 394` ```by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1)); ``` clasohm@0 ` 395` ```by (INTEG_SIMP_TAC [zminus,zmult] 1); ``` clasohm@0 ` 396` ```by (REPEAT (ares_tac [mult_type,add_commute,add_cong] 1)); ``` clasohm@0 ` 397` ```val zmult_zminus_zminus = result(); ``` clasohm@0 ` 398` clasohm@0 ` 399` ```goalw Integ.thy [integ_def] ``` clasohm@0 ` 400` ``` "!!z w. [| z: integ; w: integ |] ==> z \$* w = w \$* z"; ``` clasohm@0 ` 401` ```by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1)); ``` clasohm@0 ` 402` ```by (INTEG_SIMP_TAC [zmult] 1); ``` clasohm@0 ` 403` ```by (res_inst_tac [("m1","xc #* y")] (add_commute RS ssubst) 1); ``` clasohm@0 ` 404` ```by (REPEAT (ares_tac [mult_type,mult_commute,add_cong] 1)); ``` clasohm@0 ` 405` ```val zmult_commute = result(); ``` clasohm@0 ` 406` clasohm@0 ` 407` ```goalw Integ.thy [integ_def] ``` clasohm@0 ` 408` ``` "!!z1 z2 z3. [| z1: integ; z2: integ; z3: integ |] ==> \ ``` clasohm@0 ` 409` ```\ (z1 \$* z2) \$* z3 = z1 \$* (z2 \$* z3)"; ``` clasohm@0 ` 410` ```by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1)); ``` clasohm@0 ` 411` ```by (INTEG_SIMP_TAC [zmult, add_mult_distrib_left, ``` clasohm@0 ` 412` ``` add_mult_distrib, add_assoc, mult_assoc] 1); ``` clasohm@0 ` 413` ```(*takes 54 seconds due to wasteful type-checking*) ``` clasohm@0 ` 414` ```by (REPEAT (ares_tac [add_type, mult_type, add_commute, add_kill, ``` clasohm@0 ` 415` ``` add_assoc_swap_kill, add_assoc_swap_kill RS sym] 1)); ``` clasohm@0 ` 416` ```val zmult_assoc = result(); ``` clasohm@0 ` 417` clasohm@0 ` 418` ```goalw Integ.thy [integ_def] ``` clasohm@0 ` 419` ``` "!!z1 z2 z3. [| z1: integ; z2: integ; w: integ |] ==> \ ``` clasohm@0 ` 420` ```\ (z1 \$+ z2) \$* w = (z1 \$* w) \$+ (z2 \$* w)"; ``` clasohm@0 ` 421` ```by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1)); ``` clasohm@0 ` 422` ```by (INTEG_SIMP_TAC [zadd, zmult, add_mult_distrib, add_assoc] 1); ``` clasohm@0 ` 423` ```(*takes 30 seconds due to wasteful type-checking*) ``` clasohm@0 ` 424` ```by (REPEAT (ares_tac [add_type, mult_type, refl, add_commute, add_kill, ``` clasohm@0 ` 425` ``` add_assoc_swap_kill, add_assoc_swap_kill RS sym] 1)); ``` clasohm@0 ` 426` ```val zadd_zmult_distrib = result(); ``` clasohm@0 ` 427` clasohm@0 ` 428` ```val integ_typechecks = ``` clasohm@0 ` 429` ``` [znat_type, zminus_type, zmagnitude_type, zadd_type, zmult_type]; ``` clasohm@0 ` 430` clasohm@0 ` 431` ```val integ_ss = ``` lcp@7 ` 432` ``` arith_ss addsimps ([zminus_zminus, zmagnitude_znat, ``` lcp@7 ` 433` ``` zmagnitude_zminus_znat, zadd_0] @ integ_typechecks); ```