src/HOL/Nat.ML
 author paulson Thu Sep 12 10:40:05 1996 +0200 (1996-09-12) changeset 1985 84cf16192e03 parent 1931 c77409a88b75 child 2009 9023e474d22a permissions -rw-r--r--
Tidied many proofs, using AddIffs to let equivalences take
the place of separate Intr and Elim rules. Also deleted most named clasets.
 clasohm@1465 ` 1` ```(* Title: HOL/nat ``` clasohm@923 ` 2` ``` ID: \$Id\$ ``` clasohm@1465 ` 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); ``` berghofe@1760 ` 35` ```by (fast_tac (!claset 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@1465 ` 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); ``` berghofe@1760 ` 69` ```by (fast_tac (!claset addSEs prems) 1); ``` clasohm@923 ` 70` ```by (nat_ind_tac "n" 1); ``` clasohm@923 ` 71` ```by (rtac (refl RS disjI1) 1); ``` berghofe@1760 ` 72` ```by (Fast_tac 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` paulson@1985 ` 98` ```bind_thm ("Zero_not_Suc", Suc_not_Zero RS not_sym); ``` clasohm@923 ` 99` paulson@1985 ` 100` ```AddIffs [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` paulson@1985 ` 121` ```AddIffs [Suc_Suc_eq]; ``` paulson@1985 ` 122` clasohm@923 ` 123` ```goal Nat.thy "n ~= Suc(n)"; ``` clasohm@923 ` 124` ```by (nat_ind_tac "n" 1); ``` paulson@1985 ` 125` ```by (ALLGOALS Asm_simp_tac); ``` clasohm@923 ` 126` ```qed "n_not_Suc_n"; ``` clasohm@923 ` 127` paulson@1618 ` 128` ```bind_thm ("Suc_n_not_n", n_not_Suc_n RS not_sym); ``` clasohm@923 ` 129` clasohm@923 ` 130` ```(*** nat_case -- the selection operator for nat ***) ``` clasohm@923 ` 131` clasohm@923 ` 132` ```goalw Nat.thy [nat_case_def] "nat_case a f 0 = a"; ``` paulson@1985 ` 133` ```by (fast_tac (!claset addIs [select_equality]) 1); ``` clasohm@923 ` 134` ```qed "nat_case_0"; ``` clasohm@923 ` 135` clasohm@923 ` 136` ```goalw Nat.thy [nat_case_def] "nat_case a f (Suc k) = f(k)"; ``` paulson@1985 ` 137` ```by (fast_tac (!claset addIs [select_equality]) 1); ``` clasohm@923 ` 138` ```qed "nat_case_Suc"; ``` clasohm@923 ` 139` clasohm@923 ` 140` ```(** Introduction rules for 'pred_nat' **) ``` clasohm@923 ` 141` clasohm@972 ` 142` ```goalw Nat.thy [pred_nat_def] "(n, Suc(n)) : pred_nat"; ``` berghofe@1760 ` 143` ```by (Fast_tac 1); ``` clasohm@923 ` 144` ```qed "pred_natI"; ``` clasohm@923 ` 145` clasohm@923 ` 146` ```val major::prems = goalw Nat.thy [pred_nat_def] ``` clasohm@972 ` 147` ``` "[| p : pred_nat; !!x n. [| p = (n, Suc(n)) |] ==> R \ ``` clasohm@923 ` 148` ```\ |] ==> R"; ``` clasohm@923 ` 149` ```by (rtac (major RS CollectE) 1); ``` clasohm@923 ` 150` ```by (REPEAT (eresolve_tac ([asm_rl,exE]@prems) 1)); ``` clasohm@923 ` 151` ```qed "pred_natE"; ``` clasohm@923 ` 152` clasohm@923 ` 153` ```goalw Nat.thy [wf_def] "wf(pred_nat)"; ``` clasohm@923 ` 154` ```by (strip_tac 1); ``` clasohm@923 ` 155` ```by (nat_ind_tac "x" 1); ``` paulson@1985 ` 156` ```by (fast_tac (!claset addSEs [mp, pred_natE]) 2); ``` paulson@1985 ` 157` ```by (fast_tac (!claset addSEs [mp, pred_natE]) 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@1475 ` 163` ```(* The unrolling rule for nat_rec *) ``` clasohm@1475 ` 164` ```goal Nat.thy ``` berghofe@1824 ` 165` ``` "(%n. nat_rec c d n) = wfrec pred_nat (%f. nat_case ?c (%m. ?d m (f m)))"; ``` clasohm@1475 ` 166` ``` by (simp_tac (HOL_ss addsimps [nat_rec_def]) 1); ``` clasohm@1475 ` 167` ```bind_thm("nat_rec_unfold", wf_pred_nat RS ``` clasohm@1475 ` 168` ``` ((result() RS eq_reflection) RS def_wfrec)); ``` clasohm@1475 ` 169` clasohm@1475 ` 170` ```(*--------------------------------------------------------------------------- ``` clasohm@1475 ` 171` ``` * Old: ``` clasohm@1475 ` 172` ``` * bind_thm ("nat_rec_unfold", (wf_pred_nat RS (nat_rec_def RS def_wfrec))); ``` clasohm@1475 ` 173` ``` *---------------------------------------------------------------------------*) ``` clasohm@923 ` 174` clasohm@923 ` 175` ```(** conversion rules **) ``` clasohm@923 ` 176` berghofe@1824 ` 177` ```goal Nat.thy "nat_rec c h 0 = c"; ``` clasohm@923 ` 178` ```by (rtac (nat_rec_unfold RS trans) 1); ``` clasohm@1264 ` 179` ```by (simp_tac (!simpset addsimps [nat_case_0]) 1); ``` clasohm@923 ` 180` ```qed "nat_rec_0"; ``` clasohm@923 ` 181` berghofe@1824 ` 182` ```goal Nat.thy "nat_rec c h (Suc n) = h n (nat_rec c h n)"; ``` clasohm@923 ` 183` ```by (rtac (nat_rec_unfold RS trans) 1); ``` clasohm@1264 ` 184` ```by (simp_tac (!simpset addsimps [nat_case_Suc, pred_natI, cut_apply]) 1); ``` clasohm@923 ` 185` ```qed "nat_rec_Suc"; ``` clasohm@923 ` 186` clasohm@923 ` 187` ```(*These 2 rules ease the use of primitive recursion. NOTE USE OF == *) ``` clasohm@923 ` 188` ```val [rew] = goal Nat.thy ``` berghofe@1824 ` 189` ``` "[| !!n. f(n) == nat_rec c h n |] ==> f(0) = c"; ``` clasohm@923 ` 190` ```by (rewtac rew); ``` clasohm@923 ` 191` ```by (rtac nat_rec_0 1); ``` clasohm@923 ` 192` ```qed "def_nat_rec_0"; ``` clasohm@923 ` 193` clasohm@923 ` 194` ```val [rew] = goal Nat.thy ``` berghofe@1824 ` 195` ``` "[| !!n. f(n) == nat_rec c h n |] ==> f(Suc(n)) = h n (f n)"; ``` clasohm@923 ` 196` ```by (rewtac rew); ``` clasohm@923 ` 197` ```by (rtac nat_rec_Suc 1); ``` clasohm@923 ` 198` ```qed "def_nat_rec_Suc"; ``` clasohm@923 ` 199` clasohm@923 ` 200` ```fun nat_recs def = ``` clasohm@923 ` 201` ``` [standard (def RS def_nat_rec_0), ``` clasohm@923 ` 202` ``` standard (def RS def_nat_rec_Suc)]; ``` clasohm@923 ` 203` clasohm@923 ` 204` clasohm@923 ` 205` ```(*** Basic properties of "less than" ***) ``` clasohm@923 ` 206` clasohm@923 ` 207` ```(** Introduction properties **) ``` clasohm@923 ` 208` clasohm@923 ` 209` ```val prems = goalw Nat.thy [less_def] "[| i i<(k::nat)"; ``` clasohm@923 ` 210` ```by (rtac (trans_trancl RS transD) 1); ``` clasohm@923 ` 211` ```by (resolve_tac prems 1); ``` clasohm@923 ` 212` ```by (resolve_tac prems 1); ``` clasohm@923 ` 213` ```qed "less_trans"; ``` clasohm@923 ` 214` clasohm@923 ` 215` ```goalw Nat.thy [less_def] "n < Suc(n)"; ``` clasohm@923 ` 216` ```by (rtac (pred_natI RS r_into_trancl) 1); ``` clasohm@923 ` 217` ```qed "lessI"; ``` nipkow@1301 ` 218` ```Addsimps [lessI]; ``` clasohm@923 ` 219` paulson@1618 ` 220` ```(* i i ~ m<(n::nat)"; ``` berghofe@1760 ` 234` ```by (fast_tac (!claset addIs ([wf_pred_nat, wf_trancl RS wf_asym]@prems))1); ``` clasohm@923 ` 235` ```qed "less_not_sym"; ``` clasohm@923 ` 236` paulson@1931 ` 237` ```(* [| n R *) ``` clasohm@923 ` 238` ```bind_thm ("less_asym", (less_not_sym RS notE)); ``` clasohm@923 ` 239` clasohm@923 ` 240` ```goalw Nat.thy [less_def] "~ n<(n::nat)"; ``` clasohm@923 ` 241` ```by (rtac notI 1); ``` paulson@1618 ` 242` ```by (etac (wf_pred_nat RS wf_trancl RS wf_irrefl) 1); ``` clasohm@923 ` 243` ```qed "less_not_refl"; ``` clasohm@923 ` 244` paulson@1817 ` 245` ```(* n R *) ``` paulson@1618 ` 246` ```bind_thm ("less_irrefl", (less_not_refl RS notE)); ``` clasohm@923 ` 247` clasohm@923 ` 248` ```goal Nat.thy "!!m. n m ~= (n::nat)"; ``` berghofe@1760 ` 249` ```by (fast_tac (!claset addEs [less_irrefl]) 1); ``` clasohm@923 ` 250` ```qed "less_not_refl2"; ``` clasohm@923 ` 251` clasohm@923 ` 252` clasohm@923 ` 253` ```val major::prems = goalw Nat.thy [less_def] ``` clasohm@923 ` 254` ``` "[| i P; !!j. [| i P \ ``` clasohm@923 ` 255` ```\ |] ==> P"; ``` clasohm@923 ` 256` ```by (rtac (major RS tranclE) 1); ``` nipkow@1024 ` 257` ```by (REPEAT_FIRST (bound_hyp_subst_tac ORELSE' ``` clasohm@1465 ` 258` ``` eresolve_tac (prems@[pred_natE, Pair_inject]))); ``` nipkow@1024 ` 259` ```by (rtac refl 1); ``` clasohm@923 ` 260` ```qed "lessE"; ``` clasohm@923 ` 261` clasohm@923 ` 262` ```goal Nat.thy "~ n<0"; ``` clasohm@923 ` 263` ```by (rtac notI 1); ``` clasohm@923 ` 264` ```by (etac lessE 1); ``` clasohm@923 ` 265` ```by (etac Zero_neq_Suc 1); ``` clasohm@923 ` 266` ```by (etac Zero_neq_Suc 1); ``` clasohm@923 ` 267` ```qed "not_less0"; ``` paulson@1985 ` 268` paulson@1985 ` 269` ```AddIffs [not_less0]; ``` clasohm@923 ` 270` clasohm@923 ` 271` ```(* n<0 ==> R *) ``` paulson@1985 ` 272` ```bind_thm ("less_zeroE", not_less0 RS notE); ``` clasohm@923 ` 273` clasohm@923 ` 274` ```val [major,less,eq] = goal Nat.thy ``` clasohm@923 ` 275` ``` "[| m < Suc(n); m P; m=n ==> P |] ==> P"; ``` clasohm@923 ` 276` ```by (rtac (major RS lessE) 1); ``` clasohm@923 ` 277` ```by (rtac eq 1); ``` paulson@1985 ` 278` ```by (Fast_tac 1); ``` clasohm@923 ` 279` ```by (rtac less 1); ``` paulson@1985 ` 280` ```by (Fast_tac 1); ``` clasohm@923 ` 281` ```qed "less_SucE"; ``` clasohm@923 ` 282` clasohm@923 ` 283` ```goal Nat.thy "(m < Suc(n)) = (m < n | m = n)"; ``` berghofe@1760 ` 284` ```by (fast_tac (!claset addSIs [lessI] ``` paulson@1919 ` 285` ``` addEs [less_trans, less_SucE]) 1); ``` clasohm@923 ` 286` ```qed "less_Suc_eq"; ``` clasohm@923 ` 287` nipkow@1301 ` 288` ```val prems = goal Nat.thy "m n ~= 0"; ``` paulson@1552 ` 289` ```by (res_inst_tac [("n","n")] natE 1); ``` paulson@1552 ` 290` ```by (cut_facts_tac prems 1); ``` paulson@1552 ` 291` ```by (ALLGOALS Asm_full_simp_tac); ``` nipkow@1301 ` 292` ```qed "gr_implies_not0"; ``` nipkow@1301 ` 293` ```Addsimps [gr_implies_not0]; ``` clasohm@923 ` 294` oheimb@1660 ` 295` ```qed_goal "zero_less_eq" Nat.thy "0 < n = (n ~= 0)" (fn _ => [ ``` oheimb@1660 ` 296` ``` rtac iffI 1, ``` oheimb@1660 ` 297` ``` etac gr_implies_not0 1, ``` oheimb@1660 ` 298` ``` rtac natE 1, ``` oheimb@1660 ` 299` ``` contr_tac 1, ``` oheimb@1660 ` 300` ``` etac ssubst 1, ``` oheimb@1660 ` 301` ``` rtac zero_less_Suc 1]); ``` oheimb@1660 ` 302` clasohm@923 ` 303` ```(** Inductive (?) properties **) ``` clasohm@923 ` 304` clasohm@923 ` 305` ```val [prem] = goal Nat.thy "Suc(m) < n ==> m P \ ``` clasohm@923 ` 314` ```\ |] ==> P"; ``` clasohm@923 ` 315` ```by (rtac (major RS lessE) 1); ``` clasohm@923 ` 316` ```by (etac (lessI RS minor) 1); ``` clasohm@923 ` 317` ```by (etac (Suc_lessD RS minor) 1); ``` clasohm@923 ` 318` ```by (assume_tac 1); ``` clasohm@923 ` 319` ```qed "Suc_lessE"; ``` clasohm@923 ` 320` paulson@1985 ` 321` ```goal Nat.thy "!!m n. Suc(m) < Suc(n) ==> m Suc(m) < Suc(n)"; ``` paulson@1985 ` 326` ```by (etac rev_mp 1); ``` clasohm@923 ` 327` ```by (nat_ind_tac "n" 1); ``` paulson@1985 ` 328` ```by (ALLGOALS (fast_tac (!claset addSIs [lessI] ``` paulson@1985 ` 329` ``` addEs [less_trans, lessE]))); ``` clasohm@923 ` 330` ```qed "Suc_mono"; ``` clasohm@923 ` 331` oheimb@1672 ` 332` clasohm@923 ` 333` ```goal Nat.thy "(Suc(m) < Suc(n)) = (m j Suc i < k"; ``` paulson@1552 ` 344` ```by (nat_ind_tac "k" 1); ``` oheimb@1660 ` 345` ```by (ALLGOALS (asm_simp_tac (!simpset))); ``` oheimb@1660 ` 346` ```by (asm_simp_tac (!simpset addsimps [less_Suc_eq]) 1); ``` berghofe@1760 ` 347` ```by (fast_tac (!claset addDs [Suc_lessD]) 1); ``` nipkow@1485 ` 348` ```qed_spec_mp "less_trans_Suc"; ``` clasohm@923 ` 349` clasohm@923 ` 350` ```(*"Less than" is a linear ordering*) ``` clasohm@923 ` 351` ```goal Nat.thy "m P n m; m=n ==> P n m; n P n m |] ==> P n m" ``` oheimb@1660 ` 361` ```( fn prems => ``` oheimb@1660 ` 362` ``` [ ``` oheimb@1660 ` 363` ``` (res_inst_tac [("m1","n"),("n1","m")] (less_linear RS disjE) 1), ``` oheimb@1660 ` 364` ``` (etac disjE 2), ``` oheimb@1660 ` 365` ``` (etac (hd (tl (tl prems))) 1), ``` oheimb@1660 ` 366` ``` (etac (sym RS hd (tl prems)) 1), ``` oheimb@1660 ` 367` ``` (etac (hd prems) 1) ``` oheimb@1660 ` 368` ``` ]); ``` oheimb@1660 ` 369` clasohm@923 ` 370` ```(*Can be used with less_Suc_eq to get n=m | n P(m) |] ==> P(n) |] ==> P(n)"; ``` clasohm@923 ` 379` ```by (wf_ind_tac "n" [wf_pred_nat RS wf_trancl] 1); ``` clasohm@923 ` 380` ```by (eresolve_tac prems 1); ``` clasohm@923 ` 381` ```qed "less_induct"; ``` clasohm@923 ` 382` clasohm@923 ` 383` clasohm@923 ` 384` ```(*** Properties of <= ***) ``` clasohm@923 ` 385` paulson@1931 ` 386` ```goalw Nat.thy [le_def] "(m <= n) = (m < Suc n)"; ``` paulson@1931 ` 387` ```by (rtac not_less_eq 1); ``` paulson@1931 ` 388` ```qed "le_eq_less_Suc"; ``` paulson@1931 ` 389` clasohm@923 ` 390` ```goalw Nat.thy [le_def] "0 <= n"; ``` clasohm@923 ` 391` ```by (rtac not_less0 1); ``` clasohm@923 ` 392` ```qed "le0"; ``` clasohm@923 ` 393` nipkow@1301 ` 394` ```goalw Nat.thy [le_def] "~ Suc n <= n"; ``` paulson@1552 ` 395` ```by (Simp_tac 1); ``` nipkow@1301 ` 396` ```qed "Suc_n_not_le_n"; ``` nipkow@1301 ` 397` nipkow@1301 ` 398` ```goalw Nat.thy [le_def] "(i <= 0) = (i = 0)"; ``` paulson@1552 ` 399` ```by (nat_ind_tac "i" 1); ``` paulson@1552 ` 400` ```by (ALLGOALS Asm_simp_tac); ``` oheimb@1777 ` 401` ```qed "le_0_eq"; ``` nipkow@1301 ` 402` nipkow@1301 ` 403` ```Addsimps [less_not_refl, ``` oheimb@1777 ` 404` ``` (*less_Suc_eq, makes simpset non-confluent*) le0, le_0_eq, ``` paulson@1985 ` 405` ``` Suc_n_not_le_n, ``` clasohm@1264 ` 406` ``` n_not_Suc_n, Suc_n_not_n, ``` clasohm@1264 ` 407` ``` nat_case_0, nat_case_Suc, nat_rec_0, nat_rec_Suc]; ``` clasohm@923 ` 408` oheimb@1777 ` 409` ```(* ``` oheimb@1777 ` 410` ```goal Nat.thy "(Suc m < n | Suc m = n) = (m < n)"; ``` oheimb@1777 ` 411` ```by(stac (less_Suc_eq RS sym) 1); ``` oheimb@1777 ` 412` ```by(rtac Suc_less_eq 1); ``` oheimb@1777 ` 413` ```qed "Suc_le_eq"; ``` oheimb@1777 ` 414` oheimb@1777 ` 415` ```this could make the simpset (with less_Suc_eq added again) more confluent, ``` oheimb@1777 ` 416` ```but less_Suc_eq makes additional problems with terms of the form 0 < Suc (...) ``` oheimb@1777 ` 417` ```*) ``` oheimb@1777 ` 418` clasohm@923 ` 419` ```(*Prevents simplification of f and g: much faster*) ``` clasohm@923 ` 420` ```qed_goal "nat_case_weak_cong" Nat.thy ``` clasohm@923 ` 421` ``` "m=n ==> nat_case a f m = nat_case a f n" ``` clasohm@923 ` 422` ``` (fn [prem] => [rtac (prem RS arg_cong) 1]); ``` clasohm@923 ` 423` clasohm@923 ` 424` ```qed_goal "nat_rec_weak_cong" Nat.thy ``` berghofe@1824 ` 425` ``` "m=n ==> nat_rec a f m = nat_rec a f n" ``` clasohm@923 ` 426` ``` (fn [prem] => [rtac (prem RS arg_cong) 1]); ``` clasohm@923 ` 427` paulson@1618 ` 428` ```val prems = goalw Nat.thy [le_def] "~n m<=(n::nat)"; ``` clasohm@923 ` 429` ```by (resolve_tac prems 1); ``` clasohm@923 ` 430` ```qed "leI"; ``` clasohm@923 ` 431` paulson@1618 ` 432` ```val prems = goalw Nat.thy [le_def] "m<=n ==> ~ n < (m::nat)"; ``` clasohm@923 ` 433` ```by (resolve_tac prems 1); ``` clasohm@923 ` 434` ```qed "leD"; ``` clasohm@923 ` 435` clasohm@923 ` 436` ```val leE = make_elim leD; ``` clasohm@923 ` 437` paulson@1618 ` 438` ```goal Nat.thy "(~n n<(m::nat)"; ``` berghofe@1760 ` 443` ```by (Fast_tac 1); ``` clasohm@923 ` 444` ```qed "not_leE"; ``` clasohm@923 ` 445` clasohm@923 ` 446` ```goalw Nat.thy [le_def] "!!m. m < n ==> Suc(m) <= n"; ``` oheimb@1660 ` 447` ```by (simp_tac (!simpset addsimps [less_Suc_eq]) 1); ``` berghofe@1760 ` 448` ```by (fast_tac (!claset addEs [less_irrefl,less_asym]) 1); ``` clasohm@923 ` 449` ```qed "lessD"; ``` clasohm@923 ` 450` clasohm@923 ` 451` ```goalw Nat.thy [le_def] "!!m. Suc(m) <= n ==> m <= n"; ``` oheimb@1660 ` 452` ```by (asm_full_simp_tac (!simpset addsimps [less_Suc_eq]) 1); ``` berghofe@1760 ` 453` ```by (Fast_tac 1); ``` clasohm@923 ` 454` ```qed "Suc_leD"; ``` clasohm@923 ` 455` paulson@1817 ` 456` ```(* stronger version of Suc_leD *) ``` paulson@1817 ` 457` ```goalw Nat.thy [le_def] ``` paulson@1817 ` 458` ``` "!!m. Suc m <= n ==> m < n"; ``` paulson@1817 ` 459` ```by (asm_full_simp_tac (!simpset addsimps [less_Suc_eq]) 1); ``` paulson@1817 ` 460` ```by (cut_facts_tac [less_linear] 1); ``` berghofe@1823 ` 461` ```by (Fast_tac 1); ``` paulson@1817 ` 462` ```qed "Suc_le_lessD"; ``` paulson@1817 ` 463` paulson@1817 ` 464` ```goal Nat.thy "(Suc m <= n) = (m < n)"; ``` paulson@1817 ` 465` ```by (fast_tac (!claset addIs [lessD, Suc_le_lessD]) 1); ``` paulson@1817 ` 466` ```qed "Suc_le_eq"; ``` paulson@1817 ` 467` nipkow@1327 ` 468` ```goalw Nat.thy [le_def] "!!m. m <= n ==> m <= Suc n"; ``` berghofe@1760 ` 469` ```by (fast_tac (!claset addDs [Suc_lessD]) 1); ``` nipkow@1327 ` 470` ```qed "le_SucI"; ``` nipkow@1327 ` 471` ```Addsimps[le_SucI]; ``` nipkow@1327 ` 472` clasohm@923 ` 473` ```goalw Nat.thy [le_def] "!!m. m < n ==> m <= (n::nat)"; ``` berghofe@1760 ` 474` ```by (fast_tac (!claset addEs [less_asym]) 1); ``` clasohm@923 ` 475` ```qed "less_imp_le"; ``` clasohm@923 ` 476` clasohm@923 ` 477` ```goalw Nat.thy [le_def] "!!m. m <= n ==> m < n | m=(n::nat)"; ``` clasohm@923 ` 478` ```by (cut_facts_tac [less_linear] 1); ``` berghofe@1760 ` 479` ```by (fast_tac (!claset addEs [less_irrefl,less_asym]) 1); ``` clasohm@923 ` 480` ```qed "le_imp_less_or_eq"; ``` clasohm@923 ` 481` clasohm@923 ` 482` ```goalw Nat.thy [le_def] "!!m. m m <=(n::nat)"; ``` clasohm@923 ` 483` ```by (cut_facts_tac [less_linear] 1); ``` berghofe@1760 ` 484` ```by (fast_tac (!claset addEs [less_irrefl,less_asym]) 1); ``` clasohm@923 ` 485` ```by (flexflex_tac); ``` clasohm@923 ` 486` ```qed "less_or_eq_imp_le"; ``` clasohm@923 ` 487` clasohm@923 ` 488` ```goal Nat.thy "(x <= (y::nat)) = (x < y | x=y)"; ``` clasohm@923 ` 489` ```by (REPEAT(ares_tac [iffI,less_or_eq_imp_le,le_imp_less_or_eq] 1)); ``` clasohm@923 ` 490` ```qed "le_eq_less_or_eq"; ``` clasohm@923 ` 491` clasohm@923 ` 492` ```goal Nat.thy "n <= (n::nat)"; ``` paulson@1552 ` 493` ```by (simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1); ``` clasohm@923 ` 494` ```qed "le_refl"; ``` clasohm@923 ` 495` clasohm@923 ` 496` ```val prems = goal Nat.thy "!!i. [| i <= j; j < k |] ==> i < (k::nat)"; ``` clasohm@923 ` 497` ```by (dtac le_imp_less_or_eq 1); ``` berghofe@1760 ` 498` ```by (fast_tac (!claset addIs [less_trans]) 1); ``` clasohm@923 ` 499` ```qed "le_less_trans"; ``` clasohm@923 ` 500` clasohm@923 ` 501` ```goal Nat.thy "!!i. [| i < j; j <= k |] ==> i < (k::nat)"; ``` clasohm@923 ` 502` ```by (dtac le_imp_less_or_eq 1); ``` berghofe@1760 ` 503` ```by (fast_tac (!claset addIs [less_trans]) 1); ``` clasohm@923 ` 504` ```qed "less_le_trans"; ``` clasohm@923 ` 505` clasohm@923 ` 506` ```goal Nat.thy "!!i. [| i <= j; j <= k |] ==> i <= (k::nat)"; ``` clasohm@923 ` 507` ```by (EVERY1[dtac le_imp_less_or_eq, dtac le_imp_less_or_eq, ``` berghofe@1760 ` 508` ``` rtac less_or_eq_imp_le, fast_tac (!claset addIs [less_trans])]); ``` clasohm@923 ` 509` ```qed "le_trans"; ``` clasohm@923 ` 510` clasohm@923 ` 511` ```val prems = goal Nat.thy "!!m. [| m <= n; n <= m |] ==> m = (n::nat)"; ``` clasohm@923 ` 512` ```by (EVERY1[dtac le_imp_less_or_eq, dtac le_imp_less_or_eq, ``` berghofe@1760 ` 513` ``` fast_tac (!claset addEs [less_irrefl,less_asym])]); ``` clasohm@923 ` 514` ```qed "le_anti_sym"; ``` clasohm@923 ` 515` clasohm@923 ` 516` ```goal Nat.thy "(Suc(n) <= Suc(m)) = (n <= m)"; ``` clasohm@1264 ` 517` ```by (simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1); ``` clasohm@923 ` 518` ```qed "Suc_le_mono"; ``` clasohm@923 ` 519` clasohm@1264 ` 520` ```Addsimps [le_refl,Suc_le_mono]; ``` nipkow@1531 ` 521` nipkow@1531 ` 522` nipkow@1531 ` 523` ```(** LEAST -- the least number operator **) ``` nipkow@1531 ` 524` nipkow@1531 ` 525` ```val [prem1,prem2] = goalw Nat.thy [Least_def] ``` nipkow@1531 ` 526` ``` "[| P(k); !!x. x ~P(x) |] ==> (LEAST x.P(x)) = k"; ``` nipkow@1531 ` 527` ```by (rtac select_equality 1); ``` berghofe@1760 ` 528` ```by (fast_tac (!claset addSIs [prem1,prem2]) 1); ``` nipkow@1531 ` 529` ```by (cut_facts_tac [less_linear] 1); ``` berghofe@1760 ` 530` ```by (fast_tac (!claset addSIs [prem1] addSDs [prem2]) 1); ``` nipkow@1531 ` 531` ```qed "Least_equality"; ``` nipkow@1531 ` 532` nipkow@1531 ` 533` ```val [prem] = goal Nat.thy "P(k) ==> P(LEAST x.P(x))"; ``` nipkow@1531 ` 534` ```by (rtac (prem RS rev_mp) 1); ``` nipkow@1531 ` 535` ```by (res_inst_tac [("n","k")] less_induct 1); ``` nipkow@1531 ` 536` ```by (rtac impI 1); ``` nipkow@1531 ` 537` ```by (rtac classical 1); ``` nipkow@1531 ` 538` ```by (res_inst_tac [("s","n")] (Least_equality RS ssubst) 1); ``` nipkow@1531 ` 539` ```by (assume_tac 1); ``` nipkow@1531 ` 540` ```by (assume_tac 2); ``` berghofe@1760 ` 541` ```by (Fast_tac 1); ``` nipkow@1531 ` 542` ```qed "LeastI"; ``` nipkow@1531 ` 543` nipkow@1531 ` 544` ```(*Proof is almost identical to the one above!*) ``` nipkow@1531 ` 545` ```val [prem] = goal Nat.thy "P(k) ==> (LEAST x.P(x)) <= k"; ``` nipkow@1531 ` 546` ```by (rtac (prem RS rev_mp) 1); ``` nipkow@1531 ` 547` ```by (res_inst_tac [("n","k")] less_induct 1); ``` nipkow@1531 ` 548` ```by (rtac impI 1); ``` nipkow@1531 ` 549` ```by (rtac classical 1); ``` nipkow@1531 ` 550` ```by (res_inst_tac [("s","n")] (Least_equality RS ssubst) 1); ``` nipkow@1531 ` 551` ```by (assume_tac 1); ``` nipkow@1531 ` 552` ```by (rtac le_refl 2); ``` berghofe@1760 ` 553` ```by (fast_tac (!claset addIs [less_imp_le,le_trans]) 1); ``` nipkow@1531 ` 554` ```qed "Least_le"; ``` nipkow@1531 ` 555` nipkow@1531 ` 556` ```val [prem] = goal Nat.thy "k < (LEAST x.P(x)) ==> ~P(k)"; ``` nipkow@1531 ` 557` ```by (rtac notI 1); ``` nipkow@1531 ` 558` ```by (etac (rewrite_rule [le_def] Least_le RS notE) 1); ``` nipkow@1531 ` 559` ```by (rtac prem 1); ``` nipkow@1531 ` 560` ```qed "not_less_Least"; ``` oheimb@1660 ` 561` oheimb@1660 ` 562` ```qed_goalw "Least_Suc" Nat.thy [Least_def] ``` paulson@1931 ` 563` ``` "!!P. [| ? n. P(Suc n); ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))" ``` paulson@1931 ` 564` ``` (fn _ => [ ``` oheimb@1660 ` 565` ``` rtac select_equality 1, ``` oheimb@1660 ` 566` ``` fold_goals_tac [Least_def], ``` berghofe@1786 ` 567` ``` safe_tac (!claset addSEs [LeastI]), ``` oheimb@1660 ` 568` ``` res_inst_tac [("n","j")] natE 1, ``` berghofe@1760 ` 569` ``` Fast_tac 1, ``` paulson@1931 ` 570` ``` fast_tac (!claset addDs [Suc_less_SucD, not_less_Least]) 1, ``` oheimb@1660 ` 571` ``` res_inst_tac [("n","k")] natE 1, ``` berghofe@1760 ` 572` ``` Fast_tac 1, ``` oheimb@1660 ` 573` ``` hyp_subst_tac 1, ``` oheimb@1660 ` 574` ``` rewtac Least_def, ``` oheimb@1660 ` 575` ``` rtac (select_equality RS arg_cong RS sym) 1, ``` berghofe@1786 ` 576` ``` safe_tac (!claset), ``` oheimb@1660 ` 577` ``` dtac Suc_mono 1, ``` berghofe@1760 ` 578` ``` Fast_tac 1, ``` oheimb@1660 ` 579` ``` cut_facts_tac [less_linear] 1, ``` berghofe@1786 ` 580` ``` safe_tac (!claset), ``` oheimb@1660 ` 581` ``` atac 2, ``` berghofe@1760 ` 582` ``` Fast_tac 2, ``` oheimb@1660 ` 583` ``` dtac Suc_mono 1, ``` berghofe@1760 ` 584` ``` Fast_tac 1]); ```