src/ZF/Arith.ML
 author lcp Thu Sep 30 10:10:21 1993 +0100 (1993-09-30) changeset 14 1c0926788772 parent 6 8ce8c4d13d4d child 25 3ac1c0c0016e permissions -rw-r--r--
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext

domrange/image_subset,vimage_subset: deleted needless premise!
misc: This slightly simplifies two proofs in Schroeder-Bernstein Theorem

ind-syntax/rule_concl: recoded to avoid exceptions
intr-elim: now checks conclusions of introduction rules

func/fun_disjoint_Un: now uses ex_ex1I
list-fn/hd,tl,drop: new
simpdata/bquant_simps: new

list/list_case_type: restored!

bool.thy: changed 1 from a "def" to a translation
Removed occurreces of one_def in bool.ML, nat.ML, univ.ML, ex/integ.ML

nat/succ_less_induct: new induction principle
 clasohm@0 ` 1` ```(* Title: ZF/arith.ML ``` clasohm@0 ` 2` ``` ID: \$Id\$ ``` clasohm@0 ` 3` ``` Author: Lawrence C Paulson, Cambridge University Computer Laboratory ``` clasohm@0 ` 4` ``` Copyright 1992 University of Cambridge ``` clasohm@0 ` 5` clasohm@0 ` 6` ```For arith.thy. Arithmetic operators and their definitions ``` clasohm@0 ` 7` clasohm@0 ` 8` ```Proofs about elementary arithmetic: addition, multiplication, etc. ``` clasohm@0 ` 9` clasohm@0 ` 10` ```Could prove def_rec_0, def_rec_succ... ``` clasohm@0 ` 11` ```*) ``` clasohm@0 ` 12` clasohm@0 ` 13` ```open Arith; ``` clasohm@0 ` 14` clasohm@0 ` 15` ```(*"Difference" is subtraction of natural numbers. ``` clasohm@0 ` 16` ``` There are no negative numbers; we have ``` clasohm@0 ` 17` ``` m #- n = 0 iff m<=n and m #- n = succ(k) iff m>n. ``` clasohm@0 ` 18` ``` Also, rec(m, 0, %z w.z) is pred(m). ``` clasohm@0 ` 19` ```*) ``` clasohm@0 ` 20` clasohm@0 ` 21` ```(** rec -- better than nat_rec; the succ case has no type requirement! **) ``` clasohm@0 ` 22` clasohm@0 ` 23` ```val rec_trans = rec_def RS def_transrec RS trans; ``` clasohm@0 ` 24` clasohm@0 ` 25` ```goal Arith.thy "rec(0,a,b) = a"; ``` clasohm@0 ` 26` ```by (rtac rec_trans 1); ``` clasohm@0 ` 27` ```by (rtac nat_case_0 1); ``` clasohm@0 ` 28` ```val rec_0 = result(); ``` clasohm@0 ` 29` clasohm@0 ` 30` ```goal Arith.thy "rec(succ(m),a,b) = b(m, rec(m,a,b))"; ``` clasohm@0 ` 31` ```by (rtac rec_trans 1); ``` lcp@14 ` 32` ```by (simp_tac (ZF_ss addsimps [nat_case_succ, nat_succI]) 1); ``` clasohm@0 ` 33` ```val rec_succ = result(); ``` clasohm@0 ` 34` clasohm@0 ` 35` ```val major::prems = goal Arith.thy ``` clasohm@0 ` 36` ``` "[| n: nat; \ ``` clasohm@0 ` 37` ```\ a: C(0); \ ``` clasohm@0 ` 38` ```\ !!m z. [| m: nat; z: C(m) |] ==> b(m,z): C(succ(m)) \ ``` clasohm@0 ` 39` ```\ |] ==> rec(n,a,b) : C(n)"; ``` clasohm@0 ` 40` ```by (rtac (major RS nat_induct) 1); ``` clasohm@0 ` 41` ```by (ALLGOALS ``` lcp@6 ` 42` ``` (asm_simp_tac (ZF_ss addsimps (prems@[rec_0,rec_succ])))); ``` clasohm@0 ` 43` ```val rec_type = result(); ``` clasohm@0 ` 44` clasohm@0 ` 45` ```val nat_typechecks = [rec_type,nat_0I,nat_1I,nat_succI,Ord_nat]; ``` clasohm@0 ` 46` lcp@6 ` 47` ```val nat_ss = ZF_ss addsimps ([rec_0,rec_succ] @ nat_typechecks); ``` clasohm@0 ` 48` clasohm@0 ` 49` clasohm@0 ` 50` ```(** Addition **) ``` clasohm@0 ` 51` clasohm@0 ` 52` ```val add_type = prove_goalw Arith.thy [add_def] ``` clasohm@0 ` 53` ``` "[| m:nat; n:nat |] ==> m #+ n : nat" ``` clasohm@0 ` 54` ``` (fn prems=> [ (typechk_tac (prems@nat_typechecks@ZF_typechecks)) ]); ``` clasohm@0 ` 55` clasohm@0 ` 56` ```val add_0 = prove_goalw Arith.thy [add_def] ``` clasohm@0 ` 57` ``` "0 #+ n = n" ``` clasohm@0 ` 58` ``` (fn _ => [ (rtac rec_0 1) ]); ``` clasohm@0 ` 59` clasohm@0 ` 60` ```val add_succ = prove_goalw Arith.thy [add_def] ``` clasohm@0 ` 61` ``` "succ(m) #+ n = succ(m #+ n)" ``` clasohm@0 ` 62` ``` (fn _=> [ (rtac rec_succ 1) ]); ``` clasohm@0 ` 63` clasohm@0 ` 64` ```(** Multiplication **) ``` clasohm@0 ` 65` clasohm@0 ` 66` ```val mult_type = prove_goalw Arith.thy [mult_def] ``` clasohm@0 ` 67` ``` "[| m:nat; n:nat |] ==> m #* n : nat" ``` clasohm@0 ` 68` ``` (fn prems=> ``` clasohm@0 ` 69` ``` [ (typechk_tac (prems@[add_type]@nat_typechecks@ZF_typechecks)) ]); ``` clasohm@0 ` 70` clasohm@0 ` 71` ```val mult_0 = prove_goalw Arith.thy [mult_def] ``` clasohm@0 ` 72` ``` "0 #* n = 0" ``` clasohm@0 ` 73` ``` (fn _ => [ (rtac rec_0 1) ]); ``` clasohm@0 ` 74` clasohm@0 ` 75` ```val mult_succ = prove_goalw Arith.thy [mult_def] ``` clasohm@0 ` 76` ``` "succ(m) #* n = n #+ (m #* n)" ``` clasohm@0 ` 77` ``` (fn _ => [ (rtac rec_succ 1) ]); ``` clasohm@0 ` 78` clasohm@0 ` 79` ```(** Difference **) ``` clasohm@0 ` 80` clasohm@0 ` 81` ```val diff_type = prove_goalw Arith.thy [diff_def] ``` clasohm@0 ` 82` ``` "[| m:nat; n:nat |] ==> m #- n : nat" ``` clasohm@0 ` 83` ``` (fn prems=> [ (typechk_tac (prems@nat_typechecks@ZF_typechecks)) ]); ``` clasohm@0 ` 84` clasohm@0 ` 85` ```val diff_0 = prove_goalw Arith.thy [diff_def] ``` clasohm@0 ` 86` ``` "m #- 0 = m" ``` clasohm@0 ` 87` ``` (fn _ => [ (rtac rec_0 1) ]); ``` clasohm@0 ` 88` clasohm@0 ` 89` ```val diff_0_eq_0 = prove_goalw Arith.thy [diff_def] ``` clasohm@0 ` 90` ``` "n:nat ==> 0 #- n = 0" ``` clasohm@0 ` 91` ``` (fn [prem]=> ``` clasohm@0 ` 92` ``` [ (rtac (prem RS nat_induct) 1), ``` lcp@6 ` 93` ``` (ALLGOALS (asm_simp_tac nat_ss)) ]); ``` clasohm@0 ` 94` clasohm@0 ` 95` ```(*Must simplify BEFORE the induction!! (Else we get a critical pair) ``` clasohm@0 ` 96` ``` succ(m) #- succ(n) rewrites to pred(succ(m) #- n) *) ``` clasohm@0 ` 97` ```val diff_succ_succ = prove_goalw Arith.thy [diff_def] ``` clasohm@0 ` 98` ``` "[| m:nat; n:nat |] ==> succ(m) #- succ(n) = m #- n" ``` clasohm@0 ` 99` ``` (fn prems=> ``` lcp@6 ` 100` ``` [ (asm_simp_tac (nat_ss addsimps prems) 1), ``` clasohm@0 ` 101` ``` (nat_ind_tac "n" prems 1), ``` lcp@6 ` 102` ``` (ALLGOALS (asm_simp_tac (nat_ss addsimps prems))) ]); ``` clasohm@0 ` 103` lcp@14 ` 104` ```(*The conclusion is equivalent to m#-n <= m *) ``` clasohm@0 ` 105` ```val prems = goal Arith.thy ``` clasohm@0 ` 106` ``` "[| m:nat; n:nat |] ==> m #- n : succ(m)"; ``` clasohm@0 ` 107` ```by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); ``` clasohm@0 ` 108` ```by (resolve_tac prems 1); ``` clasohm@0 ` 109` ```by (resolve_tac prems 1); ``` clasohm@0 ` 110` ```by (etac succE 3); ``` clasohm@0 ` 111` ```by (ALLGOALS ``` lcp@6 ` 112` ``` (asm_simp_tac ``` lcp@14 ` 113` ``` (nat_ss addsimps (prems @ [succ_iff, diff_0, diff_0_eq_0, ``` lcp@14 ` 114` ``` diff_succ_succ])))); ``` lcp@14 ` 115` ```val diff_less_succ = result(); ``` clasohm@0 ` 116` clasohm@0 ` 117` ```(*** Simplification over add, mult, diff ***) ``` clasohm@0 ` 118` clasohm@0 ` 119` ```val arith_typechecks = [add_type, mult_type, diff_type]; ``` clasohm@0 ` 120` ```val arith_rews = [add_0, add_succ, ``` clasohm@0 ` 121` ``` mult_0, mult_succ, ``` clasohm@0 ` 122` ``` diff_0, diff_0_eq_0, diff_succ_succ]; ``` clasohm@0 ` 123` lcp@6 ` 124` ```val arith_ss = nat_ss addsimps (arith_rews@arith_typechecks); ``` clasohm@0 ` 125` clasohm@0 ` 126` ```(*** Addition ***) ``` clasohm@0 ` 127` clasohm@0 ` 128` ```(*Associative law for addition*) ``` clasohm@0 ` 129` ```val add_assoc = prove_goal Arith.thy ``` clasohm@0 ` 130` ``` "m:nat ==> (m #+ n) #+ k = m #+ (n #+ k)" ``` clasohm@0 ` 131` ``` (fn prems=> ``` clasohm@0 ` 132` ``` [ (nat_ind_tac "m" prems 1), ``` lcp@6 ` 133` ``` (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]); ``` clasohm@0 ` 134` clasohm@0 ` 135` ```(*The following two lemmas are used for add_commute and sometimes ``` clasohm@0 ` 136` ``` elsewhere, since they are safe for rewriting.*) ``` clasohm@0 ` 137` ```val add_0_right = prove_goal Arith.thy ``` clasohm@0 ` 138` ``` "m:nat ==> m #+ 0 = m" ``` clasohm@0 ` 139` ``` (fn prems=> ``` clasohm@0 ` 140` ``` [ (nat_ind_tac "m" prems 1), ``` lcp@6 ` 141` ``` (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]); ``` clasohm@0 ` 142` clasohm@0 ` 143` ```val add_succ_right = prove_goal Arith.thy ``` clasohm@0 ` 144` ``` "m:nat ==> m #+ succ(n) = succ(m #+ n)" ``` clasohm@0 ` 145` ``` (fn prems=> ``` clasohm@0 ` 146` ``` [ (nat_ind_tac "m" prems 1), ``` lcp@6 ` 147` ``` (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]); ``` clasohm@0 ` 148` clasohm@0 ` 149` ```(*Commutative law for addition*) ``` clasohm@0 ` 150` ```val add_commute = prove_goal Arith.thy ``` clasohm@0 ` 151` ``` "[| m:nat; n:nat |] ==> m #+ n = n #+ m" ``` clasohm@0 ` 152` ``` (fn prems=> ``` clasohm@0 ` 153` ``` [ (nat_ind_tac "n" prems 1), ``` clasohm@0 ` 154` ``` (ALLGOALS ``` lcp@6 ` 155` ``` (asm_simp_tac ``` lcp@6 ` 156` ``` (arith_ss addsimps (prems@[add_0_right, add_succ_right])))) ]); ``` clasohm@0 ` 157` clasohm@0 ` 158` ```(*Cancellation law on the left*) ``` clasohm@0 ` 159` ```val [knat,eqn] = goal Arith.thy ``` clasohm@0 ` 160` ``` "[| k:nat; k #+ m = k #+ n |] ==> m=n"; ``` clasohm@0 ` 161` ```by (rtac (eqn RS rev_mp) 1); ``` clasohm@0 ` 162` ```by (nat_ind_tac "k" [knat] 1); ``` lcp@6 ` 163` ```by (ALLGOALS (simp_tac arith_ss)); ``` clasohm@0 ` 164` ```by (fast_tac ZF_cs 1); ``` clasohm@0 ` 165` ```val add_left_cancel = result(); ``` clasohm@0 ` 166` clasohm@0 ` 167` ```(*** Multiplication ***) ``` clasohm@0 ` 168` clasohm@0 ` 169` ```(*right annihilation in product*) ``` clasohm@0 ` 170` ```val mult_0_right = prove_goal Arith.thy ``` clasohm@0 ` 171` ``` "m:nat ==> m #* 0 = 0" ``` clasohm@0 ` 172` ``` (fn prems=> ``` clasohm@0 ` 173` ``` [ (nat_ind_tac "m" prems 1), ``` lcp@6 ` 174` ``` (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]); ``` clasohm@0 ` 175` clasohm@0 ` 176` ```(*right successor law for multiplication*) ``` clasohm@0 ` 177` ```val mult_succ_right = prove_goal Arith.thy ``` lcp@6 ` 178` ``` "!!m n. [| m:nat; n:nat |] ==> m #* succ(n) = m #+ (m #* n)" ``` lcp@6 ` 179` ``` (fn _=> ``` lcp@6 ` 180` ``` [ (nat_ind_tac "m" [] 1), ``` lcp@6 ` 181` ``` (ALLGOALS (asm_simp_tac (arith_ss addsimps [add_assoc RS sym]))), ``` clasohm@0 ` 182` ``` (*The final goal requires the commutative law for addition*) ``` lcp@6 ` 183` ``` (rtac (add_commute RS subst_context) 1), ``` lcp@6 ` 184` ``` (REPEAT (assume_tac 1)) ]); ``` clasohm@0 ` 185` clasohm@0 ` 186` ```(*Commutative law for multiplication*) ``` clasohm@0 ` 187` ```val mult_commute = prove_goal Arith.thy ``` clasohm@0 ` 188` ``` "[| m:nat; n:nat |] ==> m #* n = n #* m" ``` clasohm@0 ` 189` ``` (fn prems=> ``` clasohm@0 ` 190` ``` [ (nat_ind_tac "m" prems 1), ``` lcp@6 ` 191` ``` (ALLGOALS (asm_simp_tac ``` lcp@6 ` 192` ``` (arith_ss addsimps (prems@[mult_0_right, mult_succ_right])))) ]); ``` clasohm@0 ` 193` clasohm@0 ` 194` ```(*addition distributes over multiplication*) ``` clasohm@0 ` 195` ```val add_mult_distrib = prove_goal Arith.thy ``` lcp@14 ` 196` ``` "!!m n. [| m:nat; k:nat |] ==> (m #+ n) #* k = (m #* k) #+ (n #* k)" ``` lcp@14 ` 197` ``` (fn _=> ``` lcp@14 ` 198` ``` [ (etac nat_induct 1), ``` lcp@14 ` 199` ``` (ALLGOALS (asm_simp_tac (arith_ss addsimps [add_assoc RS sym]))) ]); ``` clasohm@0 ` 200` clasohm@0 ` 201` ```(*Distributive law on the left; requires an extra typing premise*) ``` clasohm@0 ` 202` ```val add_mult_distrib_left = prove_goal Arith.thy ``` clasohm@0 ` 203` ``` "[| m:nat; n:nat; k:nat |] ==> k #* (m #+ n) = (k #* m) #+ (k #* n)" ``` clasohm@0 ` 204` ``` (fn prems=> ``` clasohm@0 ` 205` ``` let val mult_commute' = read_instantiate [("m","k")] mult_commute ``` lcp@6 ` 206` ``` val ss = arith_ss addsimps ([mult_commute',add_mult_distrib]@prems) ``` lcp@6 ` 207` ``` in [ (simp_tac ss 1) ] ``` clasohm@0 ` 208` ``` end); ``` clasohm@0 ` 209` clasohm@0 ` 210` ```(*Associative law for multiplication*) ``` clasohm@0 ` 211` ```val mult_assoc = prove_goal Arith.thy ``` lcp@14 ` 212` ``` "!!m n k. [| m:nat; n:nat; k:nat |] ==> (m #* n) #* k = m #* (n #* k)" ``` lcp@14 ` 213` ``` (fn _=> ``` lcp@14 ` 214` ``` [ (etac nat_induct 1), ``` lcp@14 ` 215` ``` (ALLGOALS (asm_simp_tac (arith_ss addsimps [add_mult_distrib]))) ]); ``` clasohm@0 ` 216` clasohm@0 ` 217` clasohm@0 ` 218` ```(*** Difference ***) ``` clasohm@0 ` 219` clasohm@0 ` 220` ```val diff_self_eq_0 = prove_goal Arith.thy ``` clasohm@0 ` 221` ``` "m:nat ==> m #- m = 0" ``` clasohm@0 ` 222` ``` (fn prems=> ``` clasohm@0 ` 223` ``` [ (nat_ind_tac "m" prems 1), ``` lcp@6 ` 224` ``` (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]); ``` clasohm@0 ` 225` clasohm@0 ` 226` ```(*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *) ``` clasohm@0 ` 227` ```val notless::prems = goal Arith.thy ``` clasohm@0 ` 228` ``` "[| ~m:n; m:nat; n:nat |] ==> n #+ (m#-n) = m"; ``` clasohm@0 ` 229` ```by (rtac (notless RS rev_mp) 1); ``` clasohm@0 ` 230` ```by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); ``` clasohm@0 ` 231` ```by (resolve_tac prems 1); ``` clasohm@0 ` 232` ```by (resolve_tac prems 1); ``` lcp@6 ` 233` ```by (ALLGOALS (asm_simp_tac ``` lcp@14 ` 234` ``` (arith_ss addsimps (prems@[succ_mem_succ_iff, nat_0_in_succ, ``` lcp@14 ` 235` ``` naturals_are_ordinals])))); ``` clasohm@0 ` 236` ```val add_diff_inverse = result(); ``` clasohm@0 ` 237` clasohm@0 ` 238` clasohm@0 ` 239` ```(*Subtraction is the inverse of addition. *) ``` clasohm@0 ` 240` ```val [mnat,nnat] = goal Arith.thy ``` clasohm@0 ` 241` ``` "[| m:nat; n:nat |] ==> (n#+m) #-n = m"; ``` clasohm@0 ` 242` ```by (rtac (nnat RS nat_induct) 1); ``` lcp@6 ` 243` ```by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mnat]))); ``` clasohm@0 ` 244` ```val diff_add_inverse = result(); ``` clasohm@0 ` 245` clasohm@0 ` 246` ```val [mnat,nnat] = goal Arith.thy ``` clasohm@0 ` 247` ``` "[| m:nat; n:nat |] ==> n #- (n#+m) = 0"; ``` clasohm@0 ` 248` ```by (rtac (nnat RS nat_induct) 1); ``` lcp@6 ` 249` ```by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mnat]))); ``` clasohm@0 ` 250` ```val diff_add_0 = result(); ``` clasohm@0 ` 251` clasohm@0 ` 252` clasohm@0 ` 253` ```(*** Remainder ***) ``` clasohm@0 ` 254` clasohm@0 ` 255` ```(*In ordinary notation: if 0 m #- n : m"; ``` clasohm@0 ` 257` ```by (etac rev_mp 1); ``` clasohm@0 ` 258` ```by (etac rev_mp 1); ``` clasohm@0 ` 259` ```by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); ``` lcp@14 ` 260` ```by (ALLGOALS (asm_simp_tac (nat_ss addsimps [diff_less_succ,diff_succ_succ]))); ``` clasohm@0 ` 261` ```val div_termination = result(); ``` clasohm@0 ` 262` clasohm@0 ` 263` ```val div_rls = ``` clasohm@0 ` 264` ``` [Ord_transrec_type, apply_type, div_termination, if_type] @ ``` clasohm@0 ` 265` ``` nat_typechecks; ``` clasohm@0 ` 266` clasohm@0 ` 267` ```(*Type checking depends upon termination!*) ``` clasohm@0 ` 268` ```val prems = goalw Arith.thy [mod_def] ``` clasohm@0 ` 269` ``` "[| 0:n; m:nat; n:nat |] ==> m mod n : nat"; ``` clasohm@0 ` 270` ```by (REPEAT (ares_tac (prems @ div_rls) 1 ORELSE etac Ord_trans 1)); ``` clasohm@0 ` 271` ```val mod_type = result(); ``` clasohm@0 ` 272` lcp@6 ` 273` ```val div_ss = ZF_ss addsimps [naturals_are_ordinals,div_termination]; ``` clasohm@0 ` 274` clasohm@0 ` 275` ```val prems = goal Arith.thy "[| 0:n; m:n; m:nat; n:nat |] ==> m mod n = m"; ``` clasohm@0 ` 276` ```by (rtac (mod_def RS def_transrec RS trans) 1); ``` lcp@6 ` 277` ```by (simp_tac (div_ss addsimps prems) 1); ``` clasohm@0 ` 278` ```val mod_less = result(); ``` clasohm@0 ` 279` clasohm@0 ` 280` ```val prems = goal Arith.thy ``` clasohm@0 ` 281` ``` "[| 0:n; ~m:n; m:nat; n:nat |] ==> m mod n = (m#-n) mod n"; ``` clasohm@0 ` 282` ```by (rtac (mod_def RS def_transrec RS trans) 1); ``` lcp@6 ` 283` ```by (simp_tac (div_ss addsimps prems) 1); ``` clasohm@0 ` 284` ```val mod_geq = result(); ``` clasohm@0 ` 285` clasohm@0 ` 286` ```(*** Quotient ***) ``` clasohm@0 ` 287` clasohm@0 ` 288` ```(*Type checking depends upon termination!*) ``` clasohm@0 ` 289` ```val prems = goalw Arith.thy [div_def] ``` clasohm@0 ` 290` ``` "[| 0:n; m:nat; n:nat |] ==> m div n : nat"; ``` clasohm@0 ` 291` ```by (REPEAT (ares_tac (prems @ div_rls) 1 ORELSE etac Ord_trans 1)); ``` clasohm@0 ` 292` ```val div_type = result(); ``` clasohm@0 ` 293` clasohm@0 ` 294` ```val prems = goal Arith.thy ``` clasohm@0 ` 295` ``` "[| 0:n; m:n; m:nat; n:nat |] ==> m div n = 0"; ``` clasohm@0 ` 296` ```by (rtac (div_def RS def_transrec RS trans) 1); ``` lcp@6 ` 297` ```by (simp_tac (div_ss addsimps prems) 1); ``` clasohm@0 ` 298` ```val div_less = result(); ``` clasohm@0 ` 299` clasohm@0 ` 300` ```val prems = goal Arith.thy ``` clasohm@0 ` 301` ``` "[| 0:n; ~m:n; m:nat; n:nat |] ==> m div n = succ((m#-n) div n)"; ``` clasohm@0 ` 302` ```by (rtac (div_def RS def_transrec RS trans) 1); ``` lcp@6 ` 303` ```by (simp_tac (div_ss addsimps prems) 1); ``` clasohm@0 ` 304` ```val div_geq = result(); ``` clasohm@0 ` 305` clasohm@0 ` 306` ```(*Main Result.*) ``` clasohm@0 ` 307` ```val prems = goal Arith.thy ``` clasohm@0 ` 308` ``` "[| 0:n; m:nat; n:nat |] ==> (m div n)#*n #+ m mod n = m"; ``` clasohm@0 ` 309` ```by (res_inst_tac [("i","m")] complete_induct 1); ``` clasohm@0 ` 310` ```by (resolve_tac prems 1); ``` clasohm@0 ` 311` ```by (res_inst_tac [("Q","x:n")] (excluded_middle RS disjE) 1); ``` clasohm@0 ` 312` ```by (ALLGOALS ``` lcp@6 ` 313` ``` (asm_simp_tac ``` lcp@6 ` 314` ``` (arith_ss addsimps ([mod_type,div_type] @ prems @ ``` clasohm@0 ` 315` ``` [mod_less,mod_geq, div_less, div_geq, ``` clasohm@0 ` 316` ``` add_assoc, add_diff_inverse, div_termination])))); ``` clasohm@0 ` 317` ```val mod_div_equality = result(); ``` clasohm@0 ` 318` clasohm@0 ` 319` clasohm@0 ` 320` ```(**** Additional theorems about "less than" ****) ``` clasohm@0 ` 321` clasohm@0 ` 322` ```val [mnat,nnat] = goal Arith.thy ``` clasohm@0 ` 323` ``` "[| m:nat; n:nat |] ==> ~ (m #+ n) : n"; ``` clasohm@0 ` 324` ```by (rtac (mnat RS nat_induct) 1); ``` lcp@6 ` 325` ```by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mem_not_refl]))); ``` clasohm@0 ` 326` ```by (rtac notI 1); ``` clasohm@0 ` 327` ```by (etac notE 1); ``` clasohm@0 ` 328` ```by (etac (succI1 RS Ord_trans) 1); ``` clasohm@0 ` 329` ```by (rtac (nnat RS naturals_are_ordinals) 1); ``` clasohm@0 ` 330` ```val add_not_less_self = result(); ``` clasohm@0 ` 331` clasohm@0 ` 332` ```val [mnat,nnat] = goal Arith.thy ``` clasohm@0 ` 333` ``` "[| m:nat; n:nat |] ==> m : succ(m #+ n)"; ``` clasohm@0 ` 334` ```by (rtac (mnat RS nat_induct) 1); ``` clasohm@0 ` 335` ```(*May not simplify even with ZF_ss because it would expand m:succ(...) *) ``` clasohm@0 ` 336` ```by (rtac (add_0 RS ssubst) 1); ``` clasohm@0 ` 337` ```by (rtac (add_succ RS ssubst) 2); ``` lcp@14 ` 338` ```by (REPEAT (ares_tac [nnat, nat_0_in_succ, succ_mem_succI, ``` clasohm@0 ` 339` ``` naturals_are_ordinals, nat_succI, add_type] 1)); ``` clasohm@0 ` 340` ```val add_less_succ_self = result(); ``` lcp@14 ` 341` lcp@14 ` 342` ```goal Arith.thy "!!m n. [| m:nat; n:nat |] ==> m <= m #+ n"; ``` lcp@14 ` 343` ```by (rtac (add_less_succ_self RS member_succD) 1); ``` lcp@14 ` 344` ```by (REPEAT (ares_tac [naturals_are_ordinals, add_type] 1)); ``` lcp@14 ` 345` ```val add_leq_self = result(); ``` lcp@14 ` 346` lcp@14 ` 347` ```goal Arith.thy "!!m n. [| m:nat; n:nat |] ==> m <= n #+ m"; ``` lcp@14 ` 348` ```by (rtac (add_commute RS ssubst) 1); ``` lcp@14 ` 349` ```by (REPEAT (ares_tac [add_leq_self] 1)); ``` lcp@14 ` 350` ```val add_leq_self2 = result(); ``` lcp@14 ` 351` lcp@14 ` 352` ```(** Monotonicity of addition **) ``` lcp@14 ` 353` lcp@14 ` 354` ```(*strict, in 1st argument*) ``` lcp@14 ` 355` ```goal Arith.thy "!!i j k. [| i:j; j:nat |] ==> i#+k : j#+k"; ``` lcp@14 ` 356` ```by (etac succ_less_induct 1); ``` lcp@14 ` 357` ```by (ALLGOALS (asm_simp_tac (arith_ss addsimps [succ_iff]))); ``` lcp@14 ` 358` ```val add_less_mono1 = result(); ``` lcp@14 ` 359` lcp@14 ` 360` ```(*strict, in both arguments*) ``` lcp@14 ` 361` ```goal Arith.thy "!!i j k l. [| i:j; k:l; j:nat; l:nat |] ==> i#+k : j#+l"; ``` lcp@14 ` 362` ```by (rtac (add_less_mono1 RS Ord_trans) 1); ``` lcp@14 ` 363` ```by (REPEAT_FIRST (ares_tac [add_type, naturals_are_ordinals])); ``` lcp@14 ` 364` ```by (EVERY [rtac (add_commute RS ssubst) 1, ``` lcp@14 ` 365` ``` rtac (add_commute RS ssubst) 3, ``` lcp@14 ` 366` ``` rtac add_less_mono1 5]); ``` lcp@14 ` 367` ```by (REPEAT (ares_tac [Ord_nat RSN (3,Ord_trans)] 1)); ``` lcp@14 ` 368` ```val add_less_mono = result(); ``` lcp@14 ` 369` lcp@14 ` 370` ```(*A [clumsy] way of lifting < monotonictity to <= monotonicity *) ``` lcp@14 ` 371` ```val less_mono::ford::prems = goal Ord.thy ``` lcp@14 ` 372` ``` "[| !!i j. [| i:j; j:k |] ==> f(i) : f(j); \ ``` lcp@14 ` 373` ```\ !!i. i:k ==> f(i):k; \ ``` lcp@14 ` 374` ```\ i<=j; i:k; j:k; Ord(k) \ ``` lcp@14 ` 375` ```\ |] ==> f(i) <= f(j)"; ``` lcp@14 ` 376` ```by (cut_facts_tac prems 1); ``` lcp@14 ` 377` ```by (rtac member_succD 1); ``` lcp@14 ` 378` ```by (dtac member_succI 1); ``` lcp@14 ` 379` ```by (fast_tac (ZF_cs addSIs [less_mono]) 3); ``` lcp@14 ` 380` ```by (REPEAT (ares_tac [ford,Ord_in_Ord] 1)); ``` lcp@14 ` 381` ```val Ord_less_mono_imp_mono = result(); ``` lcp@14 ` 382` lcp@14 ` 383` ```(*<=, in 1st argument*) ``` lcp@14 ` 384` ```goal Arith.thy ``` lcp@14 ` 385` ``` "!!i j k. [| i<=j; i:nat; j:nat; k:nat |] ==> i#+k <= j#+k"; ``` lcp@14 ` 386` ```by (res_inst_tac [("f", "%j.j#+k")] Ord_less_mono_imp_mono 1); ``` lcp@14 ` 387` ```by (REPEAT (ares_tac [add_less_mono1, add_type, Ord_nat] 1)); ``` lcp@14 ` 388` ```val add_mono1 = result(); ``` lcp@14 ` 389` lcp@14 ` 390` ```(*<=, in both arguments*) ``` lcp@14 ` 391` ```goal Arith.thy ``` lcp@14 ` 392` ``` "!!i j k. [| i<=j; k<=l; i:nat; j:nat; k:nat; l:nat |] ==> i#+k <= j#+l"; ``` lcp@14 ` 393` ```by (rtac (add_mono1 RS subset_trans) 1); ``` lcp@14 ` 394` ```by (REPEAT (assume_tac 1)); ``` lcp@14 ` 395` ```by (EVERY [rtac (add_commute RS ssubst) 1, ``` lcp@14 ` 396` ``` rtac (add_commute RS ssubst) 3, ``` lcp@14 ` 397` ``` rtac add_mono1 5]); ``` lcp@14 ` 398` ```by (REPEAT (assume_tac 1)); ``` lcp@14 ` 399` ```val add_mono = result(); ```