src/HOL/Nat.ML
 author nipkow Sun Nov 12 16:29:12 1995 +0100 (1995-11-12) changeset 1327 6c29cfab679c parent 1301 42782316d510 child 1465 5d7a7e439cec permissions -rw-r--r--
added new arithmetic lemmas and the functions take and drop.
 clasohm@923 ` 1` ```(* Title: HOL/nat ``` clasohm@923 ` 2` ``` ID: \$Id\$ ``` clasohm@923 ` 3` ``` Author: Tobias Nipkow, Cambridge University Computer Laboratory ``` clasohm@923 ` 4` ``` Copyright 1991 University of Cambridge ``` clasohm@923 ` 5` clasohm@923 ` 6` ```For nat.thy. Type nat is defined as a set (Nat) over the type ind. ``` clasohm@923 ` 7` ```*) ``` clasohm@923 ` 8` clasohm@923 ` 9` ```open Nat; ``` clasohm@923 ` 10` clasohm@923 ` 11` ```goal Nat.thy "mono(%X. {Zero_Rep} Un (Suc_Rep``X))"; ``` clasohm@923 ` 12` ```by (REPEAT (ares_tac [monoI, subset_refl, image_mono, Un_mono] 1)); ``` clasohm@923 ` 13` ```qed "Nat_fun_mono"; ``` clasohm@923 ` 14` clasohm@923 ` 15` ```val Nat_unfold = Nat_fun_mono RS (Nat_def RS def_lfp_Tarski); ``` clasohm@923 ` 16` clasohm@923 ` 17` ```(* Zero is a natural number -- this also justifies the type definition*) ``` clasohm@923 ` 18` ```goal Nat.thy "Zero_Rep: Nat"; ``` clasohm@923 ` 19` ```by (rtac (Nat_unfold RS ssubst) 1); ``` clasohm@923 ` 20` ```by (rtac (singletonI RS UnI1) 1); ``` clasohm@923 ` 21` ```qed "Zero_RepI"; ``` clasohm@923 ` 22` clasohm@923 ` 23` ```val prems = goal Nat.thy "i: Nat ==> Suc_Rep(i) : Nat"; ``` clasohm@923 ` 24` ```by (rtac (Nat_unfold RS ssubst) 1); ``` clasohm@923 ` 25` ```by (rtac (imageI RS UnI2) 1); ``` clasohm@923 ` 26` ```by (resolve_tac prems 1); ``` clasohm@923 ` 27` ```qed "Suc_RepI"; ``` clasohm@923 ` 28` clasohm@923 ` 29` ```(*** Induction ***) ``` clasohm@923 ` 30` clasohm@923 ` 31` ```val major::prems = goal Nat.thy ``` clasohm@923 ` 32` ``` "[| i: Nat; P(Zero_Rep); \ ``` clasohm@923 ` 33` ```\ !!j. [| j: Nat; P(j) |] ==> P(Suc_Rep(j)) |] ==> P(i)"; ``` clasohm@923 ` 34` ```by (rtac ([Nat_def, Nat_fun_mono, major] MRS def_induct) 1); ``` clasohm@923 ` 35` ```by (fast_tac (set_cs addIs prems) 1); ``` clasohm@923 ` 36` ```qed "Nat_induct"; ``` clasohm@923 ` 37` clasohm@923 ` 38` ```val prems = goalw Nat.thy [Zero_def,Suc_def] ``` clasohm@923 ` 39` ``` "[| P(0); \ ``` clasohm@923 ` 40` ```\ !!k. P(k) ==> P(Suc(k)) |] ==> P(n)"; ``` clasohm@923 ` 41` ```by (rtac (Rep_Nat_inverse RS subst) 1); (*types force good instantiation*) ``` clasohm@923 ` 42` ```by (rtac (Rep_Nat RS Nat_induct) 1); ``` clasohm@923 ` 43` ```by (REPEAT (ares_tac prems 1 ``` clasohm@923 ` 44` ``` ORELSE eresolve_tac [Abs_Nat_inverse RS subst] 1)); ``` clasohm@923 ` 45` ```qed "nat_induct"; ``` clasohm@923 ` 46` clasohm@923 ` 47` ```(*Perform induction on n. *) ``` clasohm@923 ` 48` ```fun nat_ind_tac a i = ``` clasohm@923 ` 49` ``` EVERY [res_inst_tac [("n",a)] nat_induct i, ``` clasohm@923 ` 50` ``` rename_last_tac a ["1"] (i+1)]; ``` clasohm@923 ` 51` clasohm@923 ` 52` ```(*A special form of induction for reasoning about m P (Suc x) (Suc y) \ ``` clasohm@923 ` 57` ```\ |] ==> P m n"; ``` clasohm@923 ` 58` ```by (res_inst_tac [("x","m")] spec 1); ``` clasohm@923 ` 59` ```by (nat_ind_tac "n" 1); ``` clasohm@923 ` 60` ```by (rtac allI 2); ``` clasohm@923 ` 61` ```by (nat_ind_tac "x" 2); ``` clasohm@923 ` 62` ```by (REPEAT (ares_tac (prems@[allI]) 1 ORELSE etac spec 1)); ``` clasohm@923 ` 63` ```qed "diff_induct"; ``` clasohm@923 ` 64` clasohm@923 ` 65` ```(*Case analysis on the natural numbers*) ``` clasohm@923 ` 66` ```val prems = goal Nat.thy ``` clasohm@923 ` 67` ``` "[| n=0 ==> P; !!x. n = Suc(x) ==> P |] ==> P"; ``` clasohm@923 ` 68` ```by (subgoal_tac "n=0 | (EX x. n = Suc(x))" 1); ``` clasohm@923 ` 69` ```by (fast_tac (HOL_cs addSEs prems) 1); ``` clasohm@923 ` 70` ```by (nat_ind_tac "n" 1); ``` clasohm@923 ` 71` ```by (rtac (refl RS disjI1) 1); ``` clasohm@923 ` 72` ```by (fast_tac HOL_cs 1); ``` clasohm@923 ` 73` ```qed "natE"; ``` clasohm@923 ` 74` clasohm@923 ` 75` ```(*** Isomorphisms: Abs_Nat and Rep_Nat ***) ``` clasohm@923 ` 76` clasohm@923 ` 77` ```(*We can't take these properties as axioms, or take Abs_Nat==Inv(Rep_Nat), ``` clasohm@923 ` 78` ``` since we assume the isomorphism equations will one day be given by Isabelle*) ``` clasohm@923 ` 79` clasohm@923 ` 80` ```goal Nat.thy "inj(Rep_Nat)"; ``` clasohm@923 ` 81` ```by (rtac inj_inverseI 1); ``` clasohm@923 ` 82` ```by (rtac Rep_Nat_inverse 1); ``` clasohm@923 ` 83` ```qed "inj_Rep_Nat"; ``` clasohm@923 ` 84` clasohm@923 ` 85` ```goal Nat.thy "inj_onto Abs_Nat Nat"; ``` clasohm@923 ` 86` ```by (rtac inj_onto_inverseI 1); ``` clasohm@923 ` 87` ```by (etac Abs_Nat_inverse 1); ``` clasohm@923 ` 88` ```qed "inj_onto_Abs_Nat"; ``` clasohm@923 ` 89` clasohm@923 ` 90` ```(*** Distinctness of constructors ***) ``` clasohm@923 ` 91` clasohm@923 ` 92` ```goalw Nat.thy [Zero_def,Suc_def] "Suc(m) ~= 0"; ``` clasohm@923 ` 93` ```by (rtac (inj_onto_Abs_Nat RS inj_onto_contraD) 1); ``` clasohm@923 ` 94` ```by (rtac Suc_Rep_not_Zero_Rep 1); ``` clasohm@923 ` 95` ```by (REPEAT (resolve_tac [Rep_Nat, Suc_RepI, Zero_RepI] 1)); ``` clasohm@923 ` 96` ```qed "Suc_not_Zero"; ``` clasohm@923 ` 97` clasohm@923 ` 98` ```bind_thm ("Zero_not_Suc", (Suc_not_Zero RS not_sym)); ``` clasohm@923 ` 99` nipkow@1301 ` 100` ```Addsimps [Suc_not_Zero,Zero_not_Suc]; ``` nipkow@1301 ` 101` clasohm@923 ` 102` ```bind_thm ("Suc_neq_Zero", (Suc_not_Zero RS notE)); ``` clasohm@923 ` 103` ```val Zero_neq_Suc = sym RS Suc_neq_Zero; ``` clasohm@923 ` 104` clasohm@923 ` 105` ```(** Injectiveness of Suc **) ``` clasohm@923 ` 106` clasohm@923 ` 107` ```goalw Nat.thy [Suc_def] "inj(Suc)"; ``` clasohm@923 ` 108` ```by (rtac injI 1); ``` clasohm@923 ` 109` ```by (dtac (inj_onto_Abs_Nat RS inj_ontoD) 1); ``` clasohm@923 ` 110` ```by (REPEAT (resolve_tac [Rep_Nat, Suc_RepI] 1)); ``` clasohm@923 ` 111` ```by (dtac (inj_Suc_Rep RS injD) 1); ``` clasohm@923 ` 112` ```by (etac (inj_Rep_Nat RS injD) 1); ``` clasohm@923 ` 113` ```qed "inj_Suc"; ``` clasohm@923 ` 114` clasohm@1264 ` 115` ```val Suc_inject = inj_Suc RS injD; ``` clasohm@923 ` 116` clasohm@923 ` 117` ```goal Nat.thy "(Suc(m)=Suc(n)) = (m=n)"; ``` clasohm@923 ` 118` ```by (EVERY1 [rtac iffI, etac Suc_inject, etac arg_cong]); ``` clasohm@923 ` 119` ```qed "Suc_Suc_eq"; ``` clasohm@923 ` 120` clasohm@923 ` 121` ```goal Nat.thy "n ~= Suc(n)"; ``` clasohm@923 ` 122` ```by (nat_ind_tac "n" 1); ``` nipkow@1301 ` 123` ```by (ALLGOALS(asm_simp_tac (!simpset addsimps [Suc_Suc_eq]))); ``` clasohm@923 ` 124` ```qed "n_not_Suc_n"; ``` clasohm@923 ` 125` clasohm@923 ` 126` ```val Suc_n_not_n = n_not_Suc_n RS not_sym; ``` clasohm@923 ` 127` clasohm@923 ` 128` ```(*** nat_case -- the selection operator for nat ***) ``` clasohm@923 ` 129` clasohm@923 ` 130` ```goalw Nat.thy [nat_case_def] "nat_case a f 0 = a"; ``` clasohm@923 ` 131` ```by (fast_tac (set_cs addIs [select_equality] addEs [Zero_neq_Suc]) 1); ``` clasohm@923 ` 132` ```qed "nat_case_0"; ``` clasohm@923 ` 133` clasohm@923 ` 134` ```goalw Nat.thy [nat_case_def] "nat_case a f (Suc k) = f(k)"; ``` clasohm@923 ` 135` ```by (fast_tac (set_cs addIs [select_equality] ``` clasohm@923 ` 136` ``` addEs [make_elim Suc_inject, Suc_neq_Zero]) 1); ``` clasohm@923 ` 137` ```qed "nat_case_Suc"; ``` clasohm@923 ` 138` clasohm@923 ` 139` ```(** Introduction rules for 'pred_nat' **) ``` clasohm@923 ` 140` clasohm@972 ` 141` ```goalw Nat.thy [pred_nat_def] "(n, Suc(n)) : pred_nat"; ``` clasohm@923 ` 142` ```by (fast_tac set_cs 1); ``` clasohm@923 ` 143` ```qed "pred_natI"; ``` clasohm@923 ` 144` clasohm@923 ` 145` ```val major::prems = goalw Nat.thy [pred_nat_def] ``` clasohm@972 ` 146` ``` "[| p : pred_nat; !!x n. [| p = (n, Suc(n)) |] ==> R \ ``` clasohm@923 ` 147` ```\ |] ==> R"; ``` clasohm@923 ` 148` ```by (rtac (major RS CollectE) 1); ``` clasohm@923 ` 149` ```by (REPEAT (eresolve_tac ([asm_rl,exE]@prems) 1)); ``` clasohm@923 ` 150` ```qed "pred_natE"; ``` clasohm@923 ` 151` clasohm@923 ` 152` ```goalw Nat.thy [wf_def] "wf(pred_nat)"; ``` clasohm@923 ` 153` ```by (strip_tac 1); ``` clasohm@923 ` 154` ```by (nat_ind_tac "x" 1); ``` clasohm@923 ` 155` ```by (fast_tac (HOL_cs addSEs [mp, pred_natE, Pair_inject, ``` clasohm@923 ` 156` ``` make_elim Suc_inject]) 2); ``` clasohm@923 ` 157` ```by (fast_tac (HOL_cs addSEs [mp, pred_natE, Pair_inject, Zero_neq_Suc]) 1); ``` clasohm@923 ` 158` ```qed "wf_pred_nat"; ``` clasohm@923 ` 159` clasohm@923 ` 160` clasohm@923 ` 161` ```(*** nat_rec -- by wf recursion on pred_nat ***) ``` clasohm@923 ` 162` clasohm@923 ` 163` ```bind_thm ("nat_rec_unfold", (wf_pred_nat RS (nat_rec_def RS def_wfrec))); ``` clasohm@923 ` 164` clasohm@923 ` 165` ```(** conversion rules **) ``` clasohm@923 ` 166` clasohm@923 ` 167` ```goal Nat.thy "nat_rec 0 c h = c"; ``` clasohm@923 ` 168` ```by (rtac (nat_rec_unfold RS trans) 1); ``` clasohm@1264 ` 169` ```by (simp_tac (!simpset addsimps [nat_case_0]) 1); ``` clasohm@923 ` 170` ```qed "nat_rec_0"; ``` clasohm@923 ` 171` clasohm@923 ` 172` ```goal Nat.thy "nat_rec (Suc n) c h = h n (nat_rec n c h)"; ``` clasohm@923 ` 173` ```by (rtac (nat_rec_unfold RS trans) 1); ``` clasohm@1264 ` 174` ```by (simp_tac (!simpset addsimps [nat_case_Suc, pred_natI, cut_apply]) 1); ``` clasohm@923 ` 175` ```qed "nat_rec_Suc"; ``` clasohm@923 ` 176` clasohm@923 ` 177` ```(*These 2 rules ease the use of primitive recursion. NOTE USE OF == *) ``` clasohm@923 ` 178` ```val [rew] = goal Nat.thy ``` clasohm@923 ` 179` ``` "[| !!n. f(n) == nat_rec n c h |] ==> f(0) = c"; ``` clasohm@923 ` 180` ```by (rewtac rew); ``` clasohm@923 ` 181` ```by (rtac nat_rec_0 1); ``` clasohm@923 ` 182` ```qed "def_nat_rec_0"; ``` clasohm@923 ` 183` clasohm@923 ` 184` ```val [rew] = goal Nat.thy ``` clasohm@923 ` 185` ``` "[| !!n. f(n) == nat_rec n c h |] ==> f(Suc(n)) = h n (f n)"; ``` clasohm@923 ` 186` ```by (rewtac rew); ``` clasohm@923 ` 187` ```by (rtac nat_rec_Suc 1); ``` clasohm@923 ` 188` ```qed "def_nat_rec_Suc"; ``` clasohm@923 ` 189` clasohm@923 ` 190` ```fun nat_recs def = ``` clasohm@923 ` 191` ``` [standard (def RS def_nat_rec_0), ``` clasohm@923 ` 192` ``` standard (def RS def_nat_rec_Suc)]; ``` clasohm@923 ` 193` clasohm@923 ` 194` clasohm@923 ` 195` ```(*** Basic properties of "less than" ***) ``` clasohm@923 ` 196` clasohm@923 ` 197` ```(** Introduction properties **) ``` clasohm@923 ` 198` clasohm@923 ` 199` ```val prems = goalw Nat.thy [less_def] "[| i i<(k::nat)"; ``` clasohm@923 ` 200` ```by (rtac (trans_trancl RS transD) 1); ``` clasohm@923 ` 201` ```by (resolve_tac prems 1); ``` clasohm@923 ` 202` ```by (resolve_tac prems 1); ``` clasohm@923 ` 203` ```qed "less_trans"; ``` clasohm@923 ` 204` clasohm@923 ` 205` ```goalw Nat.thy [less_def] "n < Suc(n)"; ``` clasohm@923 ` 206` ```by (rtac (pred_natI RS r_into_trancl) 1); ``` clasohm@923 ` 207` ```qed "lessI"; ``` nipkow@1301 ` 208` ```Addsimps [lessI]; ``` clasohm@923 ` 209` clasohm@972 ` 210` ```(* i(j ==> i(Suc(j) *) ``` clasohm@923 ` 211` ```val less_SucI = lessI RSN (2, less_trans); ``` clasohm@923 ` 212` clasohm@923 ` 213` ```goal Nat.thy "0 < Suc(n)"; ``` clasohm@923 ` 214` ```by (nat_ind_tac "n" 1); ``` clasohm@923 ` 215` ```by (rtac lessI 1); ``` clasohm@923 ` 216` ```by (etac less_trans 1); ``` clasohm@923 ` 217` ```by (rtac lessI 1); ``` clasohm@923 ` 218` ```qed "zero_less_Suc"; ``` nipkow@1301 ` 219` ```Addsimps [zero_less_Suc]; ``` clasohm@923 ` 220` clasohm@923 ` 221` ```(** Elimination properties **) ``` clasohm@923 ` 222` clasohm@923 ` 223` ```val prems = goalw Nat.thy [less_def] "n ~ m<(n::nat)"; ``` clasohm@923 ` 224` ```by(fast_tac (HOL_cs addIs ([wf_pred_nat, wf_trancl RS wf_asym]@prems))1); ``` clasohm@923 ` 225` ```qed "less_not_sym"; ``` clasohm@923 ` 226` clasohm@972 ` 227` ```(* [| n(m; m(n |] ==> R *) ``` clasohm@923 ` 228` ```bind_thm ("less_asym", (less_not_sym RS notE)); ``` clasohm@923 ` 229` clasohm@923 ` 230` ```goalw Nat.thy [less_def] "~ n<(n::nat)"; ``` clasohm@923 ` 231` ```by (rtac notI 1); ``` clasohm@923 ` 232` ```by (etac (wf_pred_nat RS wf_trancl RS wf_anti_refl) 1); ``` clasohm@923 ` 233` ```qed "less_not_refl"; ``` clasohm@923 ` 234` clasohm@972 ` 235` ```(* n(n ==> R *) ``` clasohm@923 ` 236` ```bind_thm ("less_anti_refl", (less_not_refl RS notE)); ``` clasohm@923 ` 237` clasohm@923 ` 238` ```goal Nat.thy "!!m. n m ~= (n::nat)"; ``` clasohm@923 ` 239` ```by(fast_tac (HOL_cs addEs [less_anti_refl]) 1); ``` clasohm@923 ` 240` ```qed "less_not_refl2"; ``` clasohm@923 ` 241` clasohm@923 ` 242` clasohm@923 ` 243` ```val major::prems = goalw Nat.thy [less_def] ``` clasohm@923 ` 244` ``` "[| i P; !!j. [| i P \ ``` clasohm@923 ` 245` ```\ |] ==> P"; ``` clasohm@923 ` 246` ```by (rtac (major RS tranclE) 1); ``` nipkow@1024 ` 247` ```by (REPEAT_FIRST (bound_hyp_subst_tac ORELSE' ``` nipkow@1024 ` 248` ``` eresolve_tac (prems@[pred_natE, Pair_inject]))); ``` nipkow@1024 ` 249` ```by (rtac refl 1); ``` clasohm@923 ` 250` ```qed "lessE"; ``` clasohm@923 ` 251` clasohm@923 ` 252` ```goal Nat.thy "~ n<0"; ``` clasohm@923 ` 253` ```by (rtac notI 1); ``` clasohm@923 ` 254` ```by (etac lessE 1); ``` clasohm@923 ` 255` ```by (etac Zero_neq_Suc 1); ``` clasohm@923 ` 256` ```by (etac Zero_neq_Suc 1); ``` clasohm@923 ` 257` ```qed "not_less0"; ``` nipkow@1301 ` 258` ```Addsimps [not_less0]; ``` clasohm@923 ` 259` clasohm@923 ` 260` ```(* n<0 ==> R *) ``` clasohm@923 ` 261` ```bind_thm ("less_zeroE", (not_less0 RS notE)); ``` clasohm@923 ` 262` clasohm@923 ` 263` ```val [major,less,eq] = goal Nat.thy ``` clasohm@923 ` 264` ``` "[| m < Suc(n); m P; m=n ==> P |] ==> P"; ``` clasohm@923 ` 265` ```by (rtac (major RS lessE) 1); ``` clasohm@923 ` 266` ```by (rtac eq 1); ``` clasohm@923 ` 267` ```by (fast_tac (HOL_cs addSDs [Suc_inject]) 1); ``` clasohm@923 ` 268` ```by (rtac less 1); ``` clasohm@923 ` 269` ```by (fast_tac (HOL_cs addSDs [Suc_inject]) 1); ``` clasohm@923 ` 270` ```qed "less_SucE"; ``` clasohm@923 ` 271` clasohm@923 ` 272` ```goal Nat.thy "(m < Suc(n)) = (m < n | m = n)"; ``` clasohm@923 ` 273` ```by (fast_tac (HOL_cs addSIs [lessI] ``` clasohm@923 ` 274` ``` addEs [less_trans, less_SucE]) 1); ``` clasohm@923 ` 275` ```qed "less_Suc_eq"; ``` clasohm@923 ` 276` nipkow@1301 ` 277` ```val prems = goal Nat.thy "m n ~= 0"; ``` nipkow@1301 ` 278` ```by(res_inst_tac [("n","n")] natE 1); ``` nipkow@1301 ` 279` ```by(cut_facts_tac prems 1); ``` nipkow@1301 ` 280` ```by(ALLGOALS Asm_full_simp_tac); ``` nipkow@1301 ` 281` ```qed "gr_implies_not0"; ``` nipkow@1301 ` 282` ```Addsimps [gr_implies_not0]; ``` clasohm@923 ` 283` clasohm@923 ` 284` ```(** Inductive (?) properties **) ``` clasohm@923 ` 285` clasohm@923 ` 286` ```val [prem] = goal Nat.thy "Suc(m) < n ==> m P \ ``` clasohm@923 ` 298` ```\ |] ==> P"; ``` clasohm@923 ` 299` ```by (rtac (major RS lessE) 1); ``` clasohm@923 ` 300` ```by (etac (lessI RS minor) 1); ``` clasohm@923 ` 301` ```by (etac (Suc_lessD RS minor) 1); ``` clasohm@923 ` 302` ```by (assume_tac 1); ``` clasohm@923 ` 303` ```qed "Suc_lessE"; ``` clasohm@923 ` 304` clasohm@923 ` 305` ```val [major] = goal Nat.thy "Suc(m) < Suc(n) ==> m Suc(m) < Suc(n)"; ``` clasohm@923 ` 312` ```by (subgoal_tac "m Suc(m) < Suc(n)" 1); ``` clasohm@923 ` 313` ```by (fast_tac (HOL_cs addIs prems) 1); ``` clasohm@923 ` 314` ```by (nat_ind_tac "n" 1); ``` clasohm@923 ` 315` ```by (rtac impI 1); ``` clasohm@923 ` 316` ```by (etac less_zeroE 1); ``` clasohm@923 ` 317` ```by (fast_tac (HOL_cs addSIs [lessI] ``` clasohm@923 ` 318` ``` addSDs [Suc_inject] ``` clasohm@923 ` 319` ``` addEs [less_trans, lessE]) 1); ``` clasohm@923 ` 320` ```qed "Suc_mono"; ``` clasohm@923 ` 321` clasohm@923 ` 322` ```goal Nat.thy "(Suc(m) < Suc(n)) = (m j Suc i < k"; ``` nipkow@1301 ` 333` ```by(nat_ind_tac "k" 1); ``` nipkow@1301 ` 334` ```by(ALLGOALS (asm_simp_tac (!simpset addsimps [less_Suc_eq]))); ``` nipkow@1301 ` 335` ```by(fast_tac (HOL_cs addDs [Suc_lessD]) 1); ``` nipkow@1301 ` 336` ```bind_thm("less_trans_Suc",result() RS mp); ``` clasohm@923 ` 337` clasohm@923 ` 338` ```(*"Less than" is a linear ordering*) ``` clasohm@923 ` 339` ```goal Nat.thy "m P(m) |] ==> P(n) |] ==> P(n)"; ``` clasohm@923 ` 356` ```by (wf_ind_tac "n" [wf_pred_nat RS wf_trancl] 1); ``` clasohm@923 ` 357` ```by (eresolve_tac prems 1); ``` clasohm@923 ` 358` ```qed "less_induct"; ``` clasohm@923 ` 359` clasohm@923 ` 360` clasohm@923 ` 361` ```(*** Properties of <= ***) ``` clasohm@923 ` 362` clasohm@923 ` 363` ```goalw Nat.thy [le_def] "0 <= n"; ``` clasohm@923 ` 364` ```by (rtac not_less0 1); ``` clasohm@923 ` 365` ```qed "le0"; ``` clasohm@923 ` 366` nipkow@1301 ` 367` ```goalw Nat.thy [le_def] "~ Suc n <= n"; ``` nipkow@1301 ` 368` ```by(Simp_tac 1); ``` nipkow@1301 ` 369` ```qed "Suc_n_not_le_n"; ``` nipkow@1301 ` 370` nipkow@1301 ` 371` ```goalw Nat.thy [le_def] "(i <= 0) = (i = 0)"; ``` nipkow@1301 ` 372` ```by(nat_ind_tac "i" 1); ``` nipkow@1301 ` 373` ```by(ALLGOALS Asm_simp_tac); ``` nipkow@1301 ` 374` ```qed "le_0"; ``` nipkow@1301 ` 375` nipkow@1301 ` 376` ```Addsimps [less_not_refl, ``` nipkow@1301 ` 377` ``` less_Suc_eq, le0, le_0, ``` nipkow@1301 ` 378` ``` Suc_Suc_eq, Suc_n_not_le_n, ``` clasohm@1264 ` 379` ``` n_not_Suc_n, Suc_n_not_n, ``` clasohm@1264 ` 380` ``` nat_case_0, nat_case_Suc, nat_rec_0, nat_rec_Suc]; ``` clasohm@923 ` 381` clasohm@923 ` 382` ```(*Prevents simplification of f and g: much faster*) ``` clasohm@923 ` 383` ```qed_goal "nat_case_weak_cong" Nat.thy ``` clasohm@923 ` 384` ``` "m=n ==> nat_case a f m = nat_case a f n" ``` clasohm@923 ` 385` ``` (fn [prem] => [rtac (prem RS arg_cong) 1]); ``` clasohm@923 ` 386` clasohm@923 ` 387` ```qed_goal "nat_rec_weak_cong" Nat.thy ``` clasohm@923 ` 388` ``` "m=n ==> nat_rec m a f = nat_rec n a f" ``` clasohm@923 ` 389` ``` (fn [prem] => [rtac (prem RS arg_cong) 1]); ``` clasohm@923 ` 390` clasohm@923 ` 391` ```val prems = goalw Nat.thy [le_def] "~(n m<=(n::nat)"; ``` clasohm@923 ` 392` ```by (resolve_tac prems 1); ``` clasohm@923 ` 393` ```qed "leI"; ``` clasohm@923 ` 394` clasohm@923 ` 395` ```val prems = goalw Nat.thy [le_def] "m<=n ==> ~(n<(m::nat))"; ``` clasohm@923 ` 396` ```by (resolve_tac prems 1); ``` clasohm@923 ` 397` ```qed "leD"; ``` clasohm@923 ` 398` clasohm@923 ` 399` ```val leE = make_elim leD; ``` clasohm@923 ` 400` clasohm@923 ` 401` ```goalw Nat.thy [le_def] "!!m. ~ m <= n ==> n<(m::nat)"; ``` clasohm@923 ` 402` ```by (fast_tac HOL_cs 1); ``` clasohm@923 ` 403` ```qed "not_leE"; ``` clasohm@923 ` 404` clasohm@923 ` 405` ```goalw Nat.thy [le_def] "!!m. m < n ==> Suc(m) <= n"; ``` clasohm@1264 ` 406` ```by(Simp_tac 1); ``` clasohm@923 ` 407` ```by (fast_tac (HOL_cs addEs [less_anti_refl,less_asym]) 1); ``` clasohm@923 ` 408` ```qed "lessD"; ``` clasohm@923 ` 409` clasohm@923 ` 410` ```goalw Nat.thy [le_def] "!!m. Suc(m) <= n ==> m <= n"; ``` clasohm@1264 ` 411` ```by(Asm_full_simp_tac 1); ``` clasohm@923 ` 412` ```by(fast_tac HOL_cs 1); ``` clasohm@923 ` 413` ```qed "Suc_leD"; ``` clasohm@923 ` 414` nipkow@1327 ` 415` ```goalw Nat.thy [le_def] "!!m. m <= n ==> m <= Suc n"; ``` nipkow@1327 ` 416` ```by (fast_tac (HOL_cs addDs [Suc_lessD]) 1); ``` nipkow@1327 ` 417` ```qed "le_SucI"; ``` nipkow@1327 ` 418` ```Addsimps[le_SucI]; ``` nipkow@1327 ` 419` clasohm@923 ` 420` ```goalw Nat.thy [le_def] "!!m. m < n ==> m <= (n::nat)"; ``` clasohm@923 ` 421` ```by (fast_tac (HOL_cs addEs [less_asym]) 1); ``` clasohm@923 ` 422` ```qed "less_imp_le"; ``` clasohm@923 ` 423` clasohm@923 ` 424` ```goalw Nat.thy [le_def] "!!m. m <= n ==> m < n | m=(n::nat)"; ``` clasohm@923 ` 425` ```by (cut_facts_tac [less_linear] 1); ``` clasohm@923 ` 426` ```by (fast_tac (HOL_cs addEs [less_anti_refl,less_asym]) 1); ``` clasohm@923 ` 427` ```qed "le_imp_less_or_eq"; ``` clasohm@923 ` 428` clasohm@923 ` 429` ```goalw Nat.thy [le_def] "!!m. m m <=(n::nat)"; ``` clasohm@923 ` 430` ```by (cut_facts_tac [less_linear] 1); ``` clasohm@923 ` 431` ```by (fast_tac (HOL_cs addEs [less_anti_refl,less_asym]) 1); ``` clasohm@923 ` 432` ```by (flexflex_tac); ``` clasohm@923 ` 433` ```qed "less_or_eq_imp_le"; ``` clasohm@923 ` 434` clasohm@923 ` 435` ```goal Nat.thy "(x <= (y::nat)) = (x < y | x=y)"; ``` clasohm@923 ` 436` ```by (REPEAT(ares_tac [iffI,less_or_eq_imp_le,le_imp_less_or_eq] 1)); ``` clasohm@923 ` 437` ```qed "le_eq_less_or_eq"; ``` clasohm@923 ` 438` clasohm@923 ` 439` ```goal Nat.thy "n <= (n::nat)"; ``` clasohm@1264 ` 440` ```by(simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1); ``` clasohm@923 ` 441` ```qed "le_refl"; ``` clasohm@923 ` 442` clasohm@923 ` 443` ```val prems = goal Nat.thy "!!i. [| i <= j; j < k |] ==> i < (k::nat)"; ``` clasohm@923 ` 444` ```by (dtac le_imp_less_or_eq 1); ``` clasohm@923 ` 445` ```by (fast_tac (HOL_cs addIs [less_trans]) 1); ``` clasohm@923 ` 446` ```qed "le_less_trans"; ``` clasohm@923 ` 447` clasohm@923 ` 448` ```goal Nat.thy "!!i. [| i < j; j <= k |] ==> i < (k::nat)"; ``` clasohm@923 ` 449` ```by (dtac le_imp_less_or_eq 1); ``` clasohm@923 ` 450` ```by (fast_tac (HOL_cs addIs [less_trans]) 1); ``` clasohm@923 ` 451` ```qed "less_le_trans"; ``` clasohm@923 ` 452` clasohm@923 ` 453` ```goal Nat.thy "!!i. [| i <= j; j <= k |] ==> i <= (k::nat)"; ``` clasohm@923 ` 454` ```by (EVERY1[dtac le_imp_less_or_eq, dtac le_imp_less_or_eq, ``` clasohm@923 ` 455` ``` rtac less_or_eq_imp_le, fast_tac (HOL_cs addIs [less_trans])]); ``` clasohm@923 ` 456` ```qed "le_trans"; ``` clasohm@923 ` 457` clasohm@923 ` 458` ```val prems = goal Nat.thy "!!m. [| m <= n; n <= m |] ==> m = (n::nat)"; ``` clasohm@923 ` 459` ```by (EVERY1[dtac le_imp_less_or_eq, dtac le_imp_less_or_eq, ``` clasohm@923 ` 460` ``` fast_tac (HOL_cs addEs [less_anti_refl,less_asym])]); ``` clasohm@923 ` 461` ```qed "le_anti_sym"; ``` clasohm@923 ` 462` clasohm@923 ` 463` ```goal Nat.thy "(Suc(n) <= Suc(m)) = (n <= m)"; ``` clasohm@1264 ` 464` ```by (simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1); ``` clasohm@923 ` 465` ```qed "Suc_le_mono"; ``` clasohm@923 ` 466` clasohm@1264 ` 467` ```Addsimps [le_refl,Suc_le_mono]; ```