src/HOL/Nat.ML
 author oheimb Wed Apr 17 17:59:58 1996 +0200 (1996-04-17) changeset 1660 8cb42cd97579 parent 1618 372880456b5b child 1672 2c109cd2fdd0 permissions -rw-r--r--
*** empty log message ***
 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); ``` 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@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); ``` 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` paulson@1618 ` 126` ```bind_thm ("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@1465 ` 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@1465 ` 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@1475 ` 163` ```(* The unrolling rule for nat_rec *) ``` clasohm@1475 ` 164` ```goal Nat.thy ``` clasohm@1475 ` 165` ``` "(%n. nat_rec n c d) = 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` clasohm@923 ` 177` ```goal Nat.thy "nat_rec 0 c h = 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` clasohm@923 ` 182` ```goal Nat.thy "nat_rec (Suc n) c h = h n (nat_rec n c h)"; ``` 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 ``` clasohm@923 ` 189` ``` "[| !!n. f(n) == nat_rec n c h |] ==> 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 ``` clasohm@923 ` 195` ``` "[| !!n. f(n) == nat_rec n c h |] ==> 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)"; ``` paulson@1552 ` 234` ```by (fast_tac (HOL_cs addIs ([wf_pred_nat, wf_trancl RS wf_asym]@prems))1); ``` clasohm@923 ` 235` ```qed "less_not_sym"; ``` clasohm@923 ` 236` clasohm@972 ` 237` ```(* [| n(m; m(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` clasohm@972 ` 245` ```(* n(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)"; ``` paulson@1618 ` 249` ```by (fast_tac (HOL_cs 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"; ``` nipkow@1301 ` 268` ```Addsimps [not_less0]; ``` clasohm@923 ` 269` clasohm@923 ` 270` ```(* n<0 ==> R *) ``` clasohm@923 ` 271` ```bind_thm ("less_zeroE", (not_less0 RS notE)); ``` clasohm@923 ` 272` clasohm@923 ` 273` ```val [major,less,eq] = goal Nat.thy ``` clasohm@923 ` 274` ``` "[| m < Suc(n); m P; m=n ==> P |] ==> P"; ``` clasohm@923 ` 275` ```by (rtac (major RS lessE) 1); ``` clasohm@923 ` 276` ```by (rtac eq 1); ``` clasohm@923 ` 277` ```by (fast_tac (HOL_cs addSDs [Suc_inject]) 1); ``` clasohm@923 ` 278` ```by (rtac less 1); ``` clasohm@923 ` 279` ```by (fast_tac (HOL_cs addSDs [Suc_inject]) 1); ``` clasohm@923 ` 280` ```qed "less_SucE"; ``` clasohm@923 ` 281` clasohm@923 ` 282` ```goal Nat.thy "(m < Suc(n)) = (m < n | m = n)"; ``` clasohm@923 ` 283` ```by (fast_tac (HOL_cs addSIs [lessI] ``` clasohm@1465 ` 284` ``` addEs [less_trans, less_SucE]) 1); ``` clasohm@923 ` 285` ```qed "less_Suc_eq"; ``` clasohm@923 ` 286` nipkow@1301 ` 287` ```val prems = goal Nat.thy "m n ~= 0"; ``` paulson@1552 ` 288` ```by (res_inst_tac [("n","n")] natE 1); ``` paulson@1552 ` 289` ```by (cut_facts_tac prems 1); ``` paulson@1552 ` 290` ```by (ALLGOALS Asm_full_simp_tac); ``` nipkow@1301 ` 291` ```qed "gr_implies_not0"; ``` nipkow@1301 ` 292` ```Addsimps [gr_implies_not0]; ``` clasohm@923 ` 293` oheimb@1660 ` 294` ```qed_goal "zero_less_eq" Nat.thy "0 < n = (n ~= 0)" (fn _ => [ ``` oheimb@1660 ` 295` ``` rtac iffI 1, ``` oheimb@1660 ` 296` ``` etac gr_implies_not0 1, ``` oheimb@1660 ` 297` ``` rtac natE 1, ``` oheimb@1660 ` 298` ``` contr_tac 1, ``` oheimb@1660 ` 299` ``` etac ssubst 1, ``` oheimb@1660 ` 300` ``` rtac zero_less_Suc 1]); ``` oheimb@1660 ` 301` clasohm@923 ` 302` ```(** Inductive (?) properties **) ``` clasohm@923 ` 303` clasohm@923 ` 304` ```val [prem] = goal Nat.thy "Suc(m) < n ==> m P \ ``` clasohm@923 ` 316` ```\ |] ==> P"; ``` clasohm@923 ` 317` ```by (rtac (major RS lessE) 1); ``` clasohm@923 ` 318` ```by (etac (lessI RS minor) 1); ``` clasohm@923 ` 319` ```by (etac (Suc_lessD RS minor) 1); ``` clasohm@923 ` 320` ```by (assume_tac 1); ``` clasohm@923 ` 321` ```qed "Suc_lessE"; ``` clasohm@923 ` 322` clasohm@923 ` 323` ```val [major] = goal Nat.thy "Suc(m) < Suc(n) ==> m Suc(m) < Suc(n)"; ``` clasohm@923 ` 330` ```by (subgoal_tac "m Suc(m) < Suc(n)" 1); ``` clasohm@923 ` 331` ```by (fast_tac (HOL_cs addIs prems) 1); ``` clasohm@923 ` 332` ```by (nat_ind_tac "n" 1); ``` clasohm@923 ` 333` ```by (rtac impI 1); ``` clasohm@923 ` 334` ```by (etac less_zeroE 1); ``` clasohm@923 ` 335` ```by (fast_tac (HOL_cs addSIs [lessI] ``` clasohm@1465 ` 336` ``` addSDs [Suc_inject] ``` clasohm@1465 ` 337` ``` addEs [less_trans, lessE]) 1); ``` clasohm@923 ` 338` ```qed "Suc_mono"; ``` clasohm@923 ` 339` clasohm@923 ` 340` ```goal Nat.thy "(Suc(m) < Suc(n)) = (m j Suc i < k"; ``` paulson@1552 ` 351` ```by (nat_ind_tac "k" 1); ``` oheimb@1660 ` 352` ```by (ALLGOALS (asm_simp_tac (!simpset))); ``` oheimb@1660 ` 353` ```by (asm_simp_tac (!simpset addsimps [less_Suc_eq]) 1); ``` paulson@1552 ` 354` ```by (fast_tac (HOL_cs addDs [Suc_lessD]) 1); ``` nipkow@1485 ` 355` ```qed_spec_mp "less_trans_Suc"; ``` clasohm@923 ` 356` clasohm@923 ` 357` ```(*"Less than" is a linear ordering*) ``` clasohm@923 ` 358` ```goal Nat.thy "m P n m; m=n ==> P n m; n P n m |] ==> P n m" ``` oheimb@1660 ` 368` ```( fn prems => ``` oheimb@1660 ` 369` ``` [ ``` oheimb@1660 ` 370` ``` (res_inst_tac [("m1","n"),("n1","m")] (less_linear RS disjE) 1), ``` oheimb@1660 ` 371` ``` (etac disjE 2), ``` oheimb@1660 ` 372` ``` (etac (hd (tl (tl prems))) 1), ``` oheimb@1660 ` 373` ``` (etac (sym RS hd (tl prems)) 1), ``` oheimb@1660 ` 374` ``` (etac (hd prems) 1) ``` oheimb@1660 ` 375` ``` ]); ``` oheimb@1660 ` 376` clasohm@923 ` 377` ```(*Can be used with less_Suc_eq to get n=m | n P(m) |] ==> P(n) |] ==> P(n)"; ``` clasohm@923 ` 386` ```by (wf_ind_tac "n" [wf_pred_nat RS wf_trancl] 1); ``` clasohm@923 ` 387` ```by (eresolve_tac prems 1); ``` clasohm@923 ` 388` ```qed "less_induct"; ``` clasohm@923 ` 389` clasohm@923 ` 390` clasohm@923 ` 391` ```(*** Properties of <= ***) ``` clasohm@923 ` 392` clasohm@923 ` 393` ```goalw Nat.thy [le_def] "0 <= n"; ``` clasohm@923 ` 394` ```by (rtac not_less0 1); ``` clasohm@923 ` 395` ```qed "le0"; ``` clasohm@923 ` 396` nipkow@1301 ` 397` ```goalw Nat.thy [le_def] "~ Suc n <= n"; ``` paulson@1552 ` 398` ```by (Simp_tac 1); ``` nipkow@1301 ` 399` ```qed "Suc_n_not_le_n"; ``` nipkow@1301 ` 400` nipkow@1301 ` 401` ```goalw Nat.thy [le_def] "(i <= 0) = (i = 0)"; ``` paulson@1552 ` 402` ```by (nat_ind_tac "i" 1); ``` paulson@1552 ` 403` ```by (ALLGOALS Asm_simp_tac); ``` nipkow@1301 ` 404` ```qed "le_0"; ``` nipkow@1301 ` 405` nipkow@1301 ` 406` ```Addsimps [less_not_refl, ``` oheimb@1660 ` 407` ``` (*less_Suc_eq,*) le0, le_0, ``` nipkow@1301 ` 408` ``` Suc_Suc_eq, Suc_n_not_le_n, ``` clasohm@1264 ` 409` ``` n_not_Suc_n, Suc_n_not_n, ``` clasohm@1264 ` 410` ``` nat_case_0, nat_case_Suc, nat_rec_0, nat_rec_Suc]; ``` clasohm@923 ` 411` clasohm@923 ` 412` ```(*Prevents simplification of f and g: much faster*) ``` clasohm@923 ` 413` ```qed_goal "nat_case_weak_cong" Nat.thy ``` clasohm@923 ` 414` ``` "m=n ==> nat_case a f m = nat_case a f n" ``` clasohm@923 ` 415` ``` (fn [prem] => [rtac (prem RS arg_cong) 1]); ``` clasohm@923 ` 416` clasohm@923 ` 417` ```qed_goal "nat_rec_weak_cong" Nat.thy ``` clasohm@923 ` 418` ``` "m=n ==> nat_rec m a f = nat_rec n a f" ``` clasohm@923 ` 419` ``` (fn [prem] => [rtac (prem RS arg_cong) 1]); ``` clasohm@923 ` 420` paulson@1618 ` 421` ```val prems = goalw Nat.thy [le_def] "~n m<=(n::nat)"; ``` clasohm@923 ` 422` ```by (resolve_tac prems 1); ``` clasohm@923 ` 423` ```qed "leI"; ``` clasohm@923 ` 424` paulson@1618 ` 425` ```val prems = goalw Nat.thy [le_def] "m<=n ==> ~ n < (m::nat)"; ``` clasohm@923 ` 426` ```by (resolve_tac prems 1); ``` clasohm@923 ` 427` ```qed "leD"; ``` clasohm@923 ` 428` clasohm@923 ` 429` ```val leE = make_elim leD; ``` clasohm@923 ` 430` paulson@1618 ` 431` ```goal Nat.thy "(~n n<(m::nat)"; ``` clasohm@923 ` 436` ```by (fast_tac HOL_cs 1); ``` clasohm@923 ` 437` ```qed "not_leE"; ``` clasohm@923 ` 438` clasohm@923 ` 439` ```goalw Nat.thy [le_def] "!!m. m < n ==> Suc(m) <= n"; ``` oheimb@1660 ` 440` ```by (simp_tac (!simpset addsimps [less_Suc_eq]) 1); ``` paulson@1618 ` 441` ```by (fast_tac (HOL_cs addEs [less_irrefl,less_asym]) 1); ``` clasohm@923 ` 442` ```qed "lessD"; ``` clasohm@923 ` 443` clasohm@923 ` 444` ```goalw Nat.thy [le_def] "!!m. Suc(m) <= n ==> m <= n"; ``` oheimb@1660 ` 445` ```by (asm_full_simp_tac (!simpset addsimps [less_Suc_eq]) 1); ``` paulson@1552 ` 446` ```by (fast_tac HOL_cs 1); ``` clasohm@923 ` 447` ```qed "Suc_leD"; ``` clasohm@923 ` 448` nipkow@1327 ` 449` ```goalw Nat.thy [le_def] "!!m. m <= n ==> m <= Suc n"; ``` nipkow@1327 ` 450` ```by (fast_tac (HOL_cs addDs [Suc_lessD]) 1); ``` nipkow@1327 ` 451` ```qed "le_SucI"; ``` nipkow@1327 ` 452` ```Addsimps[le_SucI]; ``` nipkow@1327 ` 453` clasohm@923 ` 454` ```goalw Nat.thy [le_def] "!!m. m < n ==> m <= (n::nat)"; ``` clasohm@923 ` 455` ```by (fast_tac (HOL_cs addEs [less_asym]) 1); ``` clasohm@923 ` 456` ```qed "less_imp_le"; ``` clasohm@923 ` 457` clasohm@923 ` 458` ```goalw Nat.thy [le_def] "!!m. m <= n ==> m < n | m=(n::nat)"; ``` clasohm@923 ` 459` ```by (cut_facts_tac [less_linear] 1); ``` paulson@1618 ` 460` ```by (fast_tac (HOL_cs addEs [less_irrefl,less_asym]) 1); ``` clasohm@923 ` 461` ```qed "le_imp_less_or_eq"; ``` clasohm@923 ` 462` clasohm@923 ` 463` ```goalw Nat.thy [le_def] "!!m. m m <=(n::nat)"; ``` clasohm@923 ` 464` ```by (cut_facts_tac [less_linear] 1); ``` paulson@1618 ` 465` ```by (fast_tac (HOL_cs addEs [less_irrefl,less_asym]) 1); ``` clasohm@923 ` 466` ```by (flexflex_tac); ``` clasohm@923 ` 467` ```qed "less_or_eq_imp_le"; ``` clasohm@923 ` 468` clasohm@923 ` 469` ```goal Nat.thy "(x <= (y::nat)) = (x < y | x=y)"; ``` clasohm@923 ` 470` ```by (REPEAT(ares_tac [iffI,less_or_eq_imp_le,le_imp_less_or_eq] 1)); ``` clasohm@923 ` 471` ```qed "le_eq_less_or_eq"; ``` clasohm@923 ` 472` clasohm@923 ` 473` ```goal Nat.thy "n <= (n::nat)"; ``` paulson@1552 ` 474` ```by (simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1); ``` clasohm@923 ` 475` ```qed "le_refl"; ``` clasohm@923 ` 476` clasohm@923 ` 477` ```val prems = goal Nat.thy "!!i. [| i <= j; j < k |] ==> i < (k::nat)"; ``` clasohm@923 ` 478` ```by (dtac le_imp_less_or_eq 1); ``` clasohm@923 ` 479` ```by (fast_tac (HOL_cs addIs [less_trans]) 1); ``` clasohm@923 ` 480` ```qed "le_less_trans"; ``` clasohm@923 ` 481` clasohm@923 ` 482` ```goal Nat.thy "!!i. [| i < j; j <= k |] ==> i < (k::nat)"; ``` clasohm@923 ` 483` ```by (dtac le_imp_less_or_eq 1); ``` clasohm@923 ` 484` ```by (fast_tac (HOL_cs addIs [less_trans]) 1); ``` clasohm@923 ` 485` ```qed "less_le_trans"; ``` clasohm@923 ` 486` clasohm@923 ` 487` ```goal Nat.thy "!!i. [| i <= j; j <= k |] ==> i <= (k::nat)"; ``` clasohm@923 ` 488` ```by (EVERY1[dtac le_imp_less_or_eq, dtac le_imp_less_or_eq, ``` clasohm@923 ` 489` ``` rtac less_or_eq_imp_le, fast_tac (HOL_cs addIs [less_trans])]); ``` clasohm@923 ` 490` ```qed "le_trans"; ``` clasohm@923 ` 491` clasohm@923 ` 492` ```val prems = goal Nat.thy "!!m. [| m <= n; n <= m |] ==> m = (n::nat)"; ``` clasohm@923 ` 493` ```by (EVERY1[dtac le_imp_less_or_eq, dtac le_imp_less_or_eq, ``` paulson@1618 ` 494` ``` fast_tac (HOL_cs addEs [less_irrefl,less_asym])]); ``` clasohm@923 ` 495` ```qed "le_anti_sym"; ``` clasohm@923 ` 496` clasohm@923 ` 497` ```goal Nat.thy "(Suc(n) <= Suc(m)) = (n <= m)"; ``` clasohm@1264 ` 498` ```by (simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1); ``` clasohm@923 ` 499` ```qed "Suc_le_mono"; ``` clasohm@923 ` 500` clasohm@1264 ` 501` ```Addsimps [le_refl,Suc_le_mono]; ``` nipkow@1531 ` 502` nipkow@1531 ` 503` nipkow@1531 ` 504` ```(** LEAST -- the least number operator **) ``` nipkow@1531 ` 505` nipkow@1531 ` 506` ```val [prem1,prem2] = goalw Nat.thy [Least_def] ``` nipkow@1531 ` 507` ``` "[| P(k); !!x. x ~P(x) |] ==> (LEAST x.P(x)) = k"; ``` nipkow@1531 ` 508` ```by (rtac select_equality 1); ``` nipkow@1531 ` 509` ```by (fast_tac (HOL_cs addSIs [prem1,prem2]) 1); ``` nipkow@1531 ` 510` ```by (cut_facts_tac [less_linear] 1); ``` nipkow@1531 ` 511` ```by (fast_tac (HOL_cs addSIs [prem1] addSDs [prem2]) 1); ``` nipkow@1531 ` 512` ```qed "Least_equality"; ``` nipkow@1531 ` 513` nipkow@1531 ` 514` ```val [prem] = goal Nat.thy "P(k) ==> P(LEAST x.P(x))"; ``` nipkow@1531 ` 515` ```by (rtac (prem RS rev_mp) 1); ``` nipkow@1531 ` 516` ```by (res_inst_tac [("n","k")] less_induct 1); ``` nipkow@1531 ` 517` ```by (rtac impI 1); ``` nipkow@1531 ` 518` ```by (rtac classical 1); ``` nipkow@1531 ` 519` ```by (res_inst_tac [("s","n")] (Least_equality RS ssubst) 1); ``` nipkow@1531 ` 520` ```by (assume_tac 1); ``` nipkow@1531 ` 521` ```by (assume_tac 2); ``` nipkow@1531 ` 522` ```by (fast_tac HOL_cs 1); ``` nipkow@1531 ` 523` ```qed "LeastI"; ``` nipkow@1531 ` 524` nipkow@1531 ` 525` ```(*Proof is almost identical to the one above!*) ``` nipkow@1531 ` 526` ```val [prem] = goal Nat.thy "P(k) ==> (LEAST x.P(x)) <= k"; ``` nipkow@1531 ` 527` ```by (rtac (prem RS rev_mp) 1); ``` nipkow@1531 ` 528` ```by (res_inst_tac [("n","k")] less_induct 1); ``` nipkow@1531 ` 529` ```by (rtac impI 1); ``` nipkow@1531 ` 530` ```by (rtac classical 1); ``` nipkow@1531 ` 531` ```by (res_inst_tac [("s","n")] (Least_equality RS ssubst) 1); ``` nipkow@1531 ` 532` ```by (assume_tac 1); ``` nipkow@1531 ` 533` ```by (rtac le_refl 2); ``` nipkow@1531 ` 534` ```by (fast_tac (HOL_cs addIs [less_imp_le,le_trans]) 1); ``` nipkow@1531 ` 535` ```qed "Least_le"; ``` nipkow@1531 ` 536` nipkow@1531 ` 537` ```val [prem] = goal Nat.thy "k < (LEAST x.P(x)) ==> ~P(k)"; ``` nipkow@1531 ` 538` ```by (rtac notI 1); ``` nipkow@1531 ` 539` ```by (etac (rewrite_rule [le_def] Least_le RS notE) 1); ``` nipkow@1531 ` 540` ```by (rtac prem 1); ``` nipkow@1531 ` 541` ```qed "not_less_Least"; ``` oheimb@1660 ` 542` oheimb@1660 ` 543` ```qed_goalw "Least_Suc" Nat.thy [Least_def] ``` oheimb@1660 ` 544` ``` "[| ? n. P (Suc n); ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P (Suc m))" ``` oheimb@1660 ` 545` ``` (fn prems => [ ``` oheimb@1660 ` 546` ``` cut_facts_tac prems 1, ``` oheimb@1660 ` 547` ``` rtac select_equality 1, ``` oheimb@1660 ` 548` ``` fold_goals_tac [Least_def], ``` oheimb@1660 ` 549` ``` safe_tac (HOL_cs addSEs [LeastI]), ``` oheimb@1660 ` 550` ``` res_inst_tac [("n","j")] natE 1, ``` oheimb@1660 ` 551` ``` fast_tac HOL_cs 1, ``` oheimb@1660 ` 552` ``` fast_tac (HOL_cs addDs [Suc_less_SucD] addDs [not_less_Least]) 1, ``` oheimb@1660 ` 553` ``` res_inst_tac [("n","k")] natE 1, ``` oheimb@1660 ` 554` ``` fast_tac HOL_cs 1, ``` oheimb@1660 ` 555` ``` hyp_subst_tac 1, ``` oheimb@1660 ` 556` ``` rewtac Least_def, ``` oheimb@1660 ` 557` ``` rtac (select_equality RS arg_cong RS sym) 1, ``` oheimb@1660 ` 558` ``` safe_tac HOL_cs, ``` oheimb@1660 ` 559` ``` dtac Suc_mono 1, ``` oheimb@1660 ` 560` ``` fast_tac HOL_cs 1, ``` oheimb@1660 ` 561` ``` cut_facts_tac [less_linear] 1, ``` oheimb@1660 ` 562` ``` safe_tac HOL_cs, ``` oheimb@1660 ` 563` ``` atac 2, ``` oheimb@1660 ` 564` ``` fast_tac HOL_cs 2, ``` oheimb@1660 ` 565` ``` dtac Suc_mono 1, ``` oheimb@1660 ` 566` ``` fast_tac HOL_cs 1]); ```