src/HOL/NatDef.ML
 author paulson Wed Jul 15 10:15:13 1998 +0200 (1998-07-15) changeset 5143 b94cd208f073 parent 5132 24f992a25adc child 5148 74919e8f221c permissions -rw-r--r--
Removal of leading "\!\!..." from most Goal commands
 nipkow@2608 ` 1` ```(* Title: HOL/NatDef.ML ``` nipkow@2608 ` 2` ``` ID: \$Id\$ ``` nipkow@2608 ` 3` ``` Author: Tobias Nipkow, Cambridge University Computer Laboratory ``` nipkow@2608 ` 4` ``` Copyright 1991 University of Cambridge ``` paulson@4737 ` 5` paulson@4737 ` 6` ```Blast_tac proofs here can get PROOF FAILED of Ord theorems like order_refl ``` paulson@4737 ` 7` ```and order_less_irrefl. We do not add the "nat" versions to the basic claset ``` paulson@4737 ` 8` ```because the type will be promoted to type class "order". ``` nipkow@2608 ` 9` ```*) ``` nipkow@2608 ` 10` wenzelm@5069 ` 11` ```Goal "mono(%X. {Zero_Rep} Un (Suc_Rep``X))"; ``` nipkow@2608 ` 12` ```by (REPEAT (ares_tac [monoI, subset_refl, image_mono, Un_mono] 1)); ``` nipkow@2608 ` 13` ```qed "Nat_fun_mono"; ``` nipkow@2608 ` 14` nipkow@2608 ` 15` ```val Nat_unfold = Nat_fun_mono RS (Nat_def RS def_lfp_Tarski); ``` nipkow@2608 ` 16` nipkow@2608 ` 17` ```(* Zero is a natural number -- this also justifies the type definition*) ``` wenzelm@5069 ` 18` ```Goal "Zero_Rep: Nat"; ``` nipkow@2608 ` 19` ```by (stac Nat_unfold 1); ``` nipkow@2608 ` 20` ```by (rtac (singletonI RS UnI1) 1); ``` nipkow@2608 ` 21` ```qed "Zero_RepI"; ``` nipkow@2608 ` 22` nipkow@2608 ` 23` ```val prems = goal thy "i: Nat ==> Suc_Rep(i) : Nat"; ``` nipkow@2608 ` 24` ```by (stac Nat_unfold 1); ``` nipkow@2608 ` 25` ```by (rtac (imageI RS UnI2) 1); ``` nipkow@2608 ` 26` ```by (resolve_tac prems 1); ``` nipkow@2608 ` 27` ```qed "Suc_RepI"; ``` nipkow@2608 ` 28` nipkow@2608 ` 29` ```(*** Induction ***) ``` nipkow@2608 ` 30` nipkow@2608 ` 31` ```val major::prems = goal thy ``` nipkow@2608 ` 32` ``` "[| i: Nat; P(Zero_Rep); \ ``` nipkow@2608 ` 33` ```\ !!j. [| j: Nat; P(j) |] ==> P(Suc_Rep(j)) |] ==> P(i)"; ``` nipkow@2608 ` 34` ```by (rtac ([Nat_def, Nat_fun_mono, major] MRS def_induct) 1); ``` wenzelm@4089 ` 35` ```by (blast_tac (claset() addIs prems) 1); ``` nipkow@2608 ` 36` ```qed "Nat_induct"; ``` nipkow@2608 ` 37` nipkow@2608 ` 38` ```val prems = goalw thy [Zero_def,Suc_def] ``` nipkow@2608 ` 39` ``` "[| P(0); \ ``` nipkow@3040 ` 40` ```\ !!n. P(n) ==> P(Suc(n)) |] ==> P(n)"; ``` nipkow@2608 ` 41` ```by (rtac (Rep_Nat_inverse RS subst) 1); (*types force good instantiation*) ``` nipkow@2608 ` 42` ```by (rtac (Rep_Nat RS Nat_induct) 1); ``` nipkow@2608 ` 43` ```by (REPEAT (ares_tac prems 1 ``` nipkow@2608 ` 44` ``` ORELSE eresolve_tac [Abs_Nat_inverse RS subst] 1)); ``` nipkow@2608 ` 45` ```qed "nat_induct"; ``` nipkow@2608 ` 46` nipkow@2608 ` 47` ```(*Perform induction on n. *) ``` paulson@3563 ` 48` ```local fun raw_nat_ind_tac a i = ``` paulson@3563 ` 49` ``` res_inst_tac [("n",a)] nat_induct i THEN rename_last_tac a [""] (i+1) ``` paulson@3563 ` 50` ```in ``` paulson@3563 ` 51` ```val nat_ind_tac = Datatype.occs_in_prems raw_nat_ind_tac ``` paulson@3563 ` 52` ```end; ``` nipkow@3040 ` 53` nipkow@2608 ` 54` ```(*A special form of induction for reasoning about m P (Suc x) (Suc y) \ ``` nipkow@2608 ` 59` ```\ |] ==> P m n"; ``` nipkow@2608 ` 60` ```by (res_inst_tac [("x","m")] spec 1); ``` nipkow@2608 ` 61` ```by (nat_ind_tac "n" 1); ``` nipkow@2608 ` 62` ```by (rtac allI 2); ``` nipkow@2608 ` 63` ```by (nat_ind_tac "x" 2); ``` nipkow@2608 ` 64` ```by (REPEAT (ares_tac (prems@[allI]) 1 ORELSE etac spec 1)); ``` nipkow@2608 ` 65` ```qed "diff_induct"; ``` nipkow@2608 ` 66` nipkow@2608 ` 67` ```(*Case analysis on the natural numbers*) ``` nipkow@2608 ` 68` ```val prems = goal thy ``` nipkow@2608 ` 69` ``` "[| n=0 ==> P; !!x. n = Suc(x) ==> P |] ==> P"; ``` nipkow@2608 ` 70` ```by (subgoal_tac "n=0 | (EX x. n = Suc(x))" 1); ``` wenzelm@4089 ` 71` ```by (fast_tac (claset() addSEs prems) 1); ``` nipkow@2608 ` 72` ```by (nat_ind_tac "n" 1); ``` nipkow@2608 ` 73` ```by (rtac (refl RS disjI1) 1); ``` paulson@2891 ` 74` ```by (Blast_tac 1); ``` nipkow@2608 ` 75` ```qed "natE"; ``` nipkow@2608 ` 76` nipkow@3282 ` 77` nipkow@2608 ` 78` ```(*** Isomorphisms: Abs_Nat and Rep_Nat ***) ``` nipkow@2608 ` 79` nipkow@2608 ` 80` ```(*We can't take these properties as axioms, or take Abs_Nat==Inv(Rep_Nat), ``` nipkow@2608 ` 81` ``` since we assume the isomorphism equations will one day be given by Isabelle*) ``` nipkow@2608 ` 82` wenzelm@5069 ` 83` ```Goal "inj(Rep_Nat)"; ``` nipkow@2608 ` 84` ```by (rtac inj_inverseI 1); ``` nipkow@2608 ` 85` ```by (rtac Rep_Nat_inverse 1); ``` nipkow@2608 ` 86` ```qed "inj_Rep_Nat"; ``` nipkow@2608 ` 87` wenzelm@5069 ` 88` ```Goal "inj_on Abs_Nat Nat"; ``` nipkow@4830 ` 89` ```by (rtac inj_on_inverseI 1); ``` nipkow@2608 ` 90` ```by (etac Abs_Nat_inverse 1); ``` nipkow@4830 ` 91` ```qed "inj_on_Abs_Nat"; ``` nipkow@2608 ` 92` nipkow@2608 ` 93` ```(*** Distinctness of constructors ***) ``` nipkow@2608 ` 94` wenzelm@5069 ` 95` ```Goalw [Zero_def,Suc_def] "Suc(m) ~= 0"; ``` nipkow@4830 ` 96` ```by (rtac (inj_on_Abs_Nat RS inj_on_contraD) 1); ``` nipkow@2608 ` 97` ```by (rtac Suc_Rep_not_Zero_Rep 1); ``` nipkow@2608 ` 98` ```by (REPEAT (resolve_tac [Rep_Nat, Suc_RepI, Zero_RepI] 1)); ``` nipkow@2608 ` 99` ```qed "Suc_not_Zero"; ``` nipkow@2608 ` 100` nipkow@2608 ` 101` ```bind_thm ("Zero_not_Suc", Suc_not_Zero RS not_sym); ``` nipkow@2608 ` 102` nipkow@2608 ` 103` ```AddIffs [Suc_not_Zero,Zero_not_Suc]; ``` nipkow@2608 ` 104` nipkow@2608 ` 105` ```bind_thm ("Suc_neq_Zero", (Suc_not_Zero RS notE)); ``` nipkow@2608 ` 106` ```val Zero_neq_Suc = sym RS Suc_neq_Zero; ``` nipkow@2608 ` 107` nipkow@2608 ` 108` ```(** Injectiveness of Suc **) ``` nipkow@2608 ` 109` wenzelm@5069 ` 110` ```Goalw [Suc_def] "inj(Suc)"; ``` nipkow@2608 ` 111` ```by (rtac injI 1); ``` nipkow@4830 ` 112` ```by (dtac (inj_on_Abs_Nat RS inj_onD) 1); ``` nipkow@2608 ` 113` ```by (REPEAT (resolve_tac [Rep_Nat, Suc_RepI] 1)); ``` nipkow@2608 ` 114` ```by (dtac (inj_Suc_Rep RS injD) 1); ``` nipkow@2608 ` 115` ```by (etac (inj_Rep_Nat RS injD) 1); ``` nipkow@2608 ` 116` ```qed "inj_Suc"; ``` nipkow@2608 ` 117` nipkow@2608 ` 118` ```val Suc_inject = inj_Suc RS injD; ``` nipkow@2608 ` 119` wenzelm@5069 ` 120` ```Goal "(Suc(m)=Suc(n)) = (m=n)"; ``` nipkow@2608 ` 121` ```by (EVERY1 [rtac iffI, etac Suc_inject, etac arg_cong]); ``` nipkow@2608 ` 122` ```qed "Suc_Suc_eq"; ``` nipkow@2608 ` 123` nipkow@2608 ` 124` ```AddIffs [Suc_Suc_eq]; ``` nipkow@2608 ` 125` wenzelm@5069 ` 126` ```Goal "n ~= Suc(n)"; ``` nipkow@2608 ` 127` ```by (nat_ind_tac "n" 1); ``` nipkow@2608 ` 128` ```by (ALLGOALS Asm_simp_tac); ``` nipkow@2608 ` 129` ```qed "n_not_Suc_n"; ``` nipkow@2608 ` 130` nipkow@2608 ` 131` ```bind_thm ("Suc_n_not_n", n_not_Suc_n RS not_sym); ``` nipkow@2608 ` 132` paulson@5143 ` 133` ```Goal "n ~= 0 ==> EX m. n = Suc m"; ``` paulson@3457 ` 134` ```by (rtac natE 1); ``` paulson@3236 ` 135` ```by (REPEAT (Blast_tac 1)); ``` paulson@3236 ` 136` ```qed "not0_implies_Suc"; ``` paulson@3236 ` 137` paulson@3236 ` 138` nipkow@2608 ` 139` ```(*** nat_case -- the selection operator for nat ***) ``` nipkow@2608 ` 140` wenzelm@5069 ` 141` ```Goalw [nat_case_def] "nat_case a f 0 = a"; ``` oheimb@4535 ` 142` ```by (Blast_tac 1); ``` nipkow@2608 ` 143` ```qed "nat_case_0"; ``` nipkow@2608 ` 144` wenzelm@5069 ` 145` ```Goalw [nat_case_def] "nat_case a f (Suc k) = f(k)"; ``` oheimb@4535 ` 146` ```by (Blast_tac 1); ``` nipkow@2608 ` 147` ```qed "nat_case_Suc"; ``` nipkow@2608 ` 148` wenzelm@5069 ` 149` ```Goalw [wf_def, pred_nat_def] "wf(pred_nat)"; ``` paulson@3718 ` 150` ```by (Clarify_tac 1); ``` nipkow@2608 ` 151` ```by (nat_ind_tac "x" 1); ``` paulson@3236 ` 152` ```by (ALLGOALS Blast_tac); ``` nipkow@2608 ` 153` ```qed "wf_pred_nat"; ``` nipkow@2608 ` 154` nipkow@2608 ` 155` nipkow@2608 ` 156` ```(*** nat_rec -- by wf recursion on pred_nat ***) ``` nipkow@2608 ` 157` nipkow@2608 ` 158` ```(* The unrolling rule for nat_rec *) ``` wenzelm@5069 ` 159` ```Goal ``` nipkow@4821 ` 160` ``` "nat_rec c d = wfrec pred_nat (%f. nat_case c (%m. d m (f m)))"; ``` nipkow@2608 ` 161` ``` by (simp_tac (HOL_ss addsimps [nat_rec_def]) 1); ``` nipkow@2608 ` 162` ```bind_thm("nat_rec_unfold", wf_pred_nat RS ``` nipkow@2608 ` 163` ``` ((result() RS eq_reflection) RS def_wfrec)); ``` nipkow@2608 ` 164` nipkow@2608 ` 165` ```(*--------------------------------------------------------------------------- ``` nipkow@2608 ` 166` ``` * Old: ``` nipkow@2608 ` 167` ``` * bind_thm ("nat_rec_unfold", (wf_pred_nat RS (nat_rec_def RS def_wfrec))); ``` nipkow@2608 ` 168` ``` *---------------------------------------------------------------------------*) ``` nipkow@2608 ` 169` nipkow@2608 ` 170` ```(** conversion rules **) ``` nipkow@2608 ` 171` wenzelm@5069 ` 172` ```Goal "nat_rec c h 0 = c"; ``` nipkow@2608 ` 173` ```by (rtac (nat_rec_unfold RS trans) 1); ``` wenzelm@4089 ` 174` ```by (simp_tac (simpset() addsimps [nat_case_0]) 1); ``` nipkow@2608 ` 175` ```qed "nat_rec_0"; ``` nipkow@2608 ` 176` wenzelm@5069 ` 177` ```Goal "nat_rec c h (Suc n) = h n (nat_rec c h n)"; ``` nipkow@2608 ` 178` ```by (rtac (nat_rec_unfold RS trans) 1); ``` wenzelm@4089 ` 179` ```by (simp_tac (simpset() addsimps [nat_case_Suc, pred_nat_def, cut_apply]) 1); ``` nipkow@2608 ` 180` ```qed "nat_rec_Suc"; ``` nipkow@2608 ` 181` nipkow@2608 ` 182` ```(*These 2 rules ease the use of primitive recursion. NOTE USE OF == *) ``` nipkow@2608 ` 183` ```val [rew] = goal thy ``` nipkow@2608 ` 184` ``` "[| !!n. f(n) == nat_rec c h n |] ==> f(0) = c"; ``` nipkow@2608 ` 185` ```by (rewtac rew); ``` nipkow@2608 ` 186` ```by (rtac nat_rec_0 1); ``` nipkow@2608 ` 187` ```qed "def_nat_rec_0"; ``` nipkow@2608 ` 188` nipkow@2608 ` 189` ```val [rew] = goal thy ``` nipkow@2608 ` 190` ``` "[| !!n. f(n) == nat_rec c h n |] ==> f(Suc(n)) = h n (f n)"; ``` nipkow@2608 ` 191` ```by (rewtac rew); ``` nipkow@2608 ` 192` ```by (rtac nat_rec_Suc 1); ``` nipkow@2608 ` 193` ```qed "def_nat_rec_Suc"; ``` nipkow@2608 ` 194` nipkow@2608 ` 195` ```fun nat_recs def = ``` nipkow@2608 ` 196` ``` [standard (def RS def_nat_rec_0), ``` nipkow@2608 ` 197` ``` standard (def RS def_nat_rec_Suc)]; ``` nipkow@2608 ` 198` nipkow@2608 ` 199` nipkow@2608 ` 200` ```(*** Basic properties of "less than" ***) ``` nipkow@2608 ` 201` paulson@3378 ` 202` ```(*Used in TFL/post.sml*) ``` wenzelm@5069 ` 203` ```Goalw [less_def] "(m,n) : pred_nat^+ = (m i<(k::nat)"; ``` nipkow@2608 ` 210` ```by (rtac (trans_trancl RS transD) 1); ``` nipkow@2608 ` 211` ```by (resolve_tac prems 1); ``` nipkow@2608 ` 212` ```by (resolve_tac prems 1); ``` nipkow@2608 ` 213` ```qed "less_trans"; ``` nipkow@2608 ` 214` wenzelm@5069 ` 215` ```Goalw [less_def, pred_nat_def] "n < Suc(n)"; ``` wenzelm@4089 ` 216` ```by (simp_tac (simpset() addsimps [r_into_trancl]) 1); ``` nipkow@2608 ` 217` ```qed "lessI"; ``` nipkow@2608 ` 218` ```AddIffs [lessI]; ``` nipkow@2608 ` 219` nipkow@2608 ` 220` ```(* i i ~ m<(n::nat)"; ``` wenzelm@4089 ` 235` ```by (blast_tac (claset() addIs ([wf_pred_nat, wf_trancl RS wf_asym]@prems))1); ``` nipkow@2608 ` 236` ```qed "less_not_sym"; ``` nipkow@2608 ` 237` nipkow@2608 ` 238` ```(* [| n R *) ``` nipkow@2608 ` 239` ```bind_thm ("less_asym", (less_not_sym RS notE)); ``` nipkow@2608 ` 240` wenzelm@5069 ` 241` ```Goalw [less_def] "~ n<(n::nat)"; ``` nipkow@2608 ` 242` ```by (rtac notI 1); ``` nipkow@2608 ` 243` ```by (etac (wf_pred_nat RS wf_trancl RS wf_irrefl) 1); ``` nipkow@2608 ` 244` ```qed "less_not_refl"; ``` nipkow@2608 ` 245` nipkow@2608 ` 246` ```(* n R *) ``` nipkow@2608 ` 247` ```bind_thm ("less_irrefl", (less_not_refl RS notE)); ``` nipkow@2608 ` 248` paulson@5143 ` 249` ```Goal "n m ~= (n::nat)"; ``` wenzelm@4089 ` 250` ```by (blast_tac (claset() addSEs [less_irrefl]) 1); ``` nipkow@2608 ` 251` ```qed "less_not_refl2"; ``` nipkow@2608 ` 252` nipkow@2608 ` 253` paulson@3236 ` 254` ```val major::prems = goalw thy [less_def, pred_nat_def] ``` nipkow@2608 ` 255` ``` "[| i P; !!j. [| i P \ ``` nipkow@2608 ` 256` ```\ |] ==> P"; ``` nipkow@2608 ` 257` ```by (rtac (major RS tranclE) 1); ``` paulson@3236 ` 258` ```by (ALLGOALS Full_simp_tac); ``` nipkow@2608 ` 259` ```by (REPEAT_FIRST (bound_hyp_subst_tac ORELSE' ``` paulson@3236 ` 260` ``` eresolve_tac (prems@[asm_rl, Pair_inject]))); ``` nipkow@2608 ` 261` ```qed "lessE"; ``` nipkow@2608 ` 262` wenzelm@5069 ` 263` ```Goal "~ n<0"; ``` nipkow@2608 ` 264` ```by (rtac notI 1); ``` nipkow@2608 ` 265` ```by (etac lessE 1); ``` nipkow@2608 ` 266` ```by (etac Zero_neq_Suc 1); ``` nipkow@2608 ` 267` ```by (etac Zero_neq_Suc 1); ``` nipkow@2608 ` 268` ```qed "not_less0"; ``` nipkow@2608 ` 269` nipkow@2608 ` 270` ```AddIffs [not_less0]; ``` nipkow@2608 ` 271` nipkow@2608 ` 272` ```(* n<0 ==> R *) ``` nipkow@2608 ` 273` ```bind_thm ("less_zeroE", not_less0 RS notE); ``` nipkow@2608 ` 274` nipkow@2608 ` 275` ```val [major,less,eq] = goal thy ``` nipkow@2608 ` 276` ``` "[| m < Suc(n); m P; m=n ==> P |] ==> P"; ``` nipkow@2608 ` 277` ```by (rtac (major RS lessE) 1); ``` nipkow@2608 ` 278` ```by (rtac eq 1); ``` paulson@2891 ` 279` ```by (Blast_tac 1); ``` nipkow@2608 ` 280` ```by (rtac less 1); ``` paulson@2891 ` 281` ```by (Blast_tac 1); ``` nipkow@2608 ` 282` ```qed "less_SucE"; ``` nipkow@2608 ` 283` wenzelm@5069 ` 284` ```Goal "(m < Suc(n)) = (m < n | m = n)"; ``` wenzelm@4089 ` 285` ```by (blast_tac (claset() addSEs [less_SucE] addIs [less_trans]) 1); ``` nipkow@2608 ` 286` ```qed "less_Suc_eq"; ``` nipkow@2608 ` 287` wenzelm@5069 ` 288` ```Goal "(n<1) = (n=0)"; ``` wenzelm@4089 ` 289` ```by (simp_tac (simpset() addsimps [less_Suc_eq]) 1); ``` nipkow@3484 ` 290` ```qed "less_one"; ``` nipkow@3484 ` 291` ```AddIffs [less_one]; ``` nipkow@3484 ` 292` nipkow@2608 ` 293` ```val prems = goal thy "m n ~= 0"; ``` nipkow@2608 ` 294` ```by (res_inst_tac [("n","n")] natE 1); ``` nipkow@2608 ` 295` ```by (cut_facts_tac prems 1); ``` nipkow@2608 ` 296` ```by (ALLGOALS Asm_full_simp_tac); ``` nipkow@2608 ` 297` ```qed "gr_implies_not0"; ``` nipkow@4356 ` 298` wenzelm@5069 ` 299` ```Goal "(n ~= 0) = (0 < n)"; ``` wenzelm@4423 ` 300` ```by (rtac natE 1); ``` paulson@4737 ` 301` ```by (Blast_tac 1); ``` paulson@4737 ` 302` ```by (Blast_tac 1); ``` nipkow@4356 ` 303` ```qed "neq0_conv"; ``` paulson@4614 ` 304` ```AddIffs [neq0_conv]; ``` paulson@4614 ` 305` paulson@4635 ` 306` ```(*This theorem is useful with blast_tac: (n=0 ==> False) ==> 0 0 < n"; ``` nipkow@4356 ` 317` ```by (dtac gr_implies_not0 1); ``` nipkow@4356 ` 318` ```by (Asm_full_simp_tac 1); ``` nipkow@4356 ` 319` ```qed "gr_implies_gr0"; ``` nipkow@4356 ` 320` ```Addsimps [gr_implies_gr0]; ``` nipkow@4356 ` 321` nipkow@2608 ` 322` paulson@5143 ` 323` ```Goal "m Suc(m) < Suc(n)"; ``` nipkow@2608 ` 324` ```by (etac rev_mp 1); ``` nipkow@2608 ` 325` ```by (nat_ind_tac "n" 1); ``` wenzelm@4089 ` 326` ```by (ALLGOALS (fast_tac (claset() addEs [less_trans, lessE]))); ``` nipkow@2608 ` 327` ```qed "Suc_mono"; ``` nipkow@2608 ` 328` nipkow@2608 ` 329` ```(*"Less than" is a linear ordering*) ``` wenzelm@5069 ` 330` ```Goal "m P n m; m=n ==> P n m; n P n m |] ==> P n m" ``` paulson@2935 ` 345` ```( fn [major,eqCase,lessCase] => ``` nipkow@2608 ` 346` ``` [ ``` paulson@2935 ` 347` ``` (rtac (less_linear RS disjE) 1), ``` nipkow@2608 ` 348` ``` (etac disjE 2), ``` paulson@2935 ` 349` ``` (etac lessCase 1), ``` paulson@2935 ` 350` ``` (etac (sym RS eqCase) 1), ``` paulson@2935 ` 351` ``` (etac major 1) ``` nipkow@2608 ` 352` ``` ]); ``` nipkow@2608 ` 353` paulson@4745 ` 354` paulson@4745 ` 355` ```(** Inductive (?) properties **) ``` paulson@4745 ` 356` paulson@5143 ` 357` ```Goal "[| m Suc(m) < n"; ``` paulson@4745 ` 358` ```by (full_simp_tac (simpset() addsimps [nat_neq_iff]) 1); ``` paulson@4745 ` 359` ```by (blast_tac (claset() addSEs [less_irrefl, less_SucE] addEs [less_asym]) 1); ``` paulson@4745 ` 360` ```qed "Suc_lessI"; ``` paulson@4745 ` 361` paulson@4745 ` 362` ```val [prem] = goal thy "Suc(m) < n ==> m P \ ``` paulson@4745 ` 371` ```\ |] ==> P"; ``` paulson@4745 ` 372` ```by (rtac (major RS lessE) 1); ``` paulson@4745 ` 373` ```by (etac (lessI RS minor) 1); ``` paulson@4745 ` 374` ```by (etac (Suc_lessD RS minor) 1); ``` paulson@4745 ` 375` ```by (assume_tac 1); ``` paulson@4745 ` 376` ```qed "Suc_lessE"; ``` paulson@4745 ` 377` paulson@5143 ` 378` ```Goal "Suc(m) < Suc(n) ==> m j Suc i < k"; ``` paulson@4745 ` 394` ```by (nat_ind_tac "k" 1); ``` paulson@4745 ` 395` ```by (ALLGOALS (asm_simp_tac (simpset()))); ``` paulson@4745 ` 396` ```by (asm_simp_tac (simpset() addsimps [less_Suc_eq]) 1); ``` paulson@4745 ` 397` ```by (blast_tac (claset() addDs [Suc_lessD]) 1); ``` paulson@4745 ` 398` ```qed_spec_mp "less_trans_Suc"; ``` paulson@4745 ` 399` nipkow@2608 ` 400` ```(*Can be used with less_Suc_eq to get n=m | n P(m) |] ==> P(n) |] ==> P(n)"; ``` nipkow@2608 ` 409` ```by (wf_ind_tac "n" [wf_pred_nat RS wf_trancl] 1); ``` nipkow@2608 ` 410` ```by (eresolve_tac prems 1); ``` nipkow@2608 ` 411` ```qed "less_induct"; ``` nipkow@2608 ` 412` nipkow@2608 ` 413` ```qed_goal "nat_induct2" thy ``` nipkow@2608 ` 414` ```"[| P 0; P 1; !!k. P k ==> P (Suc (Suc k)) |] ==> P n" (fn prems => [ ``` paulson@3023 ` 415` ``` cut_facts_tac prems 1, ``` paulson@3023 ` 416` ``` rtac less_induct 1, ``` paulson@3023 ` 417` ``` res_inst_tac [("n","n")] natE 1, ``` paulson@3023 ` 418` ``` hyp_subst_tac 1, ``` paulson@3023 ` 419` ``` atac 1, ``` paulson@3023 ` 420` ``` hyp_subst_tac 1, ``` paulson@3023 ` 421` ``` res_inst_tac [("n","x")] natE 1, ``` paulson@3023 ` 422` ``` hyp_subst_tac 1, ``` paulson@3023 ` 423` ``` atac 1, ``` paulson@3023 ` 424` ``` hyp_subst_tac 1, ``` paulson@3023 ` 425` ``` resolve_tac prems 1, ``` paulson@3023 ` 426` ``` dtac spec 1, ``` paulson@3023 ` 427` ``` etac mp 1, ``` paulson@3023 ` 428` ``` rtac (lessI RS less_trans) 1, ``` paulson@3023 ` 429` ``` rtac (lessI RS Suc_mono) 1]); ``` nipkow@2608 ` 430` nipkow@2608 ` 431` ```(*** Properties of <= ***) ``` nipkow@2608 ` 432` wenzelm@5069 ` 433` ```Goalw [le_def] "(m <= n) = (m < Suc n)"; ``` nipkow@2608 ` 434` ```by (rtac not_less_eq 1); ``` nipkow@2608 ` 435` ```qed "le_eq_less_Suc"; ``` nipkow@2608 ` 436` paulson@3343 ` 437` ```(* m<=n ==> m < Suc n *) ``` paulson@3343 ` 438` ```bind_thm ("le_imp_less_Suc", le_eq_less_Suc RS iffD1); ``` paulson@3343 ` 439` wenzelm@5069 ` 440` ```Goalw [le_def] "0 <= n"; ``` nipkow@2608 ` 441` ```by (rtac not_less0 1); ``` nipkow@2608 ` 442` ```qed "le0"; ``` nipkow@2608 ` 443` wenzelm@5069 ` 444` ```Goalw [le_def] "~ Suc n <= n"; ``` nipkow@2608 ` 445` ```by (Simp_tac 1); ``` nipkow@2608 ` 446` ```qed "Suc_n_not_le_n"; ``` nipkow@2608 ` 447` wenzelm@5069 ` 448` ```Goalw [le_def] "(i <= 0) = (i = 0)"; ``` nipkow@2608 ` 449` ```by (nat_ind_tac "i" 1); ``` nipkow@2608 ` 450` ```by (ALLGOALS Asm_simp_tac); ``` nipkow@2608 ` 451` ```qed "le_0_eq"; ``` paulson@4614 ` 452` ```AddIffs [le_0_eq]; ``` nipkow@2608 ` 453` nipkow@2608 ` 454` ```Addsimps [(*less_Suc_eq, makes simpset non-confluent*) le0, le_0_eq, ``` nipkow@2608 ` 455` ``` Suc_n_not_le_n, ``` nipkow@2608 ` 456` ``` n_not_Suc_n, Suc_n_not_n, ``` nipkow@2608 ` 457` ``` nat_case_0, nat_case_Suc, nat_rec_0, nat_rec_Suc]; ``` nipkow@2608 ` 458` paulson@5143 ` 459` ```Goal "(m <= Suc(n)) = (m<=n | m = Suc n)"; ``` wenzelm@4089 ` 460` ```by (simp_tac (simpset() addsimps [le_eq_less_Suc]) 1); ``` wenzelm@4089 ` 461` ```by (blast_tac (claset() addSEs [less_SucE] addIs [less_SucI]) 1); ``` paulson@3355 ` 462` ```qed "le_Suc_eq"; ``` paulson@3355 ` 463` paulson@4614 ` 464` ```(* [| m <= Suc n; m <= n ==> R; m = Suc n ==> R |] ==> R *) ``` paulson@4614 ` 465` ```bind_thm ("le_SucE", le_Suc_eq RS iffD1 RS disjE); ``` paulson@4614 ` 466` nipkow@2608 ` 467` ```(* ``` wenzelm@5069 ` 468` ```Goal "(Suc m < n | Suc m = n) = (m < n)"; ``` nipkow@2608 ` 469` ```by (stac (less_Suc_eq RS sym) 1); ``` nipkow@2608 ` 470` ```by (rtac Suc_less_eq 1); ``` nipkow@2608 ` 471` ```qed "Suc_le_eq"; ``` nipkow@2608 ` 472` nipkow@2608 ` 473` ```this could make the simpset (with less_Suc_eq added again) more confluent, ``` nipkow@2608 ` 474` ```but less_Suc_eq makes additional problems with terms of the form 0 < Suc (...) ``` nipkow@2608 ` 475` ```*) ``` nipkow@2608 ` 476` nipkow@2608 ` 477` ```(*Prevents simplification of f and g: much faster*) ``` nipkow@2608 ` 478` ```qed_goal "nat_case_weak_cong" thy ``` nipkow@2608 ` 479` ``` "m=n ==> nat_case a f m = nat_case a f n" ``` nipkow@2608 ` 480` ``` (fn [prem] => [rtac (prem RS arg_cong) 1]); ``` nipkow@2608 ` 481` nipkow@2608 ` 482` ```qed_goal "nat_rec_weak_cong" thy ``` nipkow@2608 ` 483` ``` "m=n ==> nat_rec a f m = nat_rec a f n" ``` nipkow@2608 ` 484` ``` (fn [prem] => [rtac (prem RS arg_cong) 1]); ``` nipkow@2608 ` 485` nipkow@4830 ` 486` ```qed_goal "split_nat_case" thy ``` nipkow@2608 ` 487` ``` "P(nat_case z s n) = ((n=0 --> P z) & (!m. n = Suc m --> P(s m)))" ``` nipkow@2608 ` 488` ``` (fn _ => [nat_ind_tac "n" 1, ALLGOALS Asm_simp_tac]); ``` nipkow@2608 ` 489` nipkow@2608 ` 490` ```val prems = goalw thy [le_def] "~n m<=(n::nat)"; ``` nipkow@2608 ` 491` ```by (resolve_tac prems 1); ``` nipkow@2608 ` 492` ```qed "leI"; ``` nipkow@2608 ` 493` nipkow@2608 ` 494` ```val prems = goalw thy [le_def] "m<=n ==> ~ n < (m::nat)"; ``` nipkow@2608 ` 495` ```by (resolve_tac prems 1); ``` nipkow@2608 ` 496` ```qed "leD"; ``` nipkow@2608 ` 497` nipkow@2608 ` 498` ```val leE = make_elim leD; ``` nipkow@2608 ` 499` wenzelm@5069 ` 500` ```Goal "(~n n<(m::nat)"; ``` paulson@2891 ` 505` ```by (Blast_tac 1); ``` nipkow@2608 ` 506` ```qed "not_leE"; ``` nipkow@2608 ` 507` wenzelm@5069 ` 508` ```Goalw [le_def] "(~n<=m) = (m<(n::nat))"; ``` paulson@4599 ` 509` ```by (Simp_tac 1); ``` paulson@4599 ` 510` ```qed "not_le_iff_less"; ``` paulson@4599 ` 511` paulson@5143 ` 512` ```Goalw [le_def] "m < n ==> Suc(m) <= n"; ``` wenzelm@4089 ` 513` ```by (simp_tac (simpset() addsimps [less_Suc_eq]) 1); ``` wenzelm@4089 ` 514` ```by (blast_tac (claset() addSEs [less_irrefl,less_asym]) 1); ``` paulson@3343 ` 515` ```qed "Suc_leI"; (*formerly called lessD*) ``` nipkow@2608 ` 516` paulson@5143 ` 517` ```Goalw [le_def] "Suc(m) <= n ==> m <= n"; ``` wenzelm@4089 ` 518` ```by (asm_full_simp_tac (simpset() addsimps [less_Suc_eq]) 1); ``` nipkow@2608 ` 519` ```qed "Suc_leD"; ``` nipkow@2608 ` 520` nipkow@2608 ` 521` ```(* stronger version of Suc_leD *) ``` wenzelm@5069 ` 522` ```Goalw [le_def] ``` nipkow@2608 ` 523` ``` "!!m. Suc m <= n ==> m < n"; ``` wenzelm@4089 ` 524` ```by (asm_full_simp_tac (simpset() addsimps [less_Suc_eq]) 1); ``` nipkow@2608 ` 525` ```by (cut_facts_tac [less_linear] 1); ``` paulson@2891 ` 526` ```by (Blast_tac 1); ``` nipkow@2608 ` 527` ```qed "Suc_le_lessD"; ``` nipkow@2608 ` 528` wenzelm@5069 ` 529` ```Goal "(Suc m <= n) = (m < n)"; ``` wenzelm@4089 ` 530` ```by (blast_tac (claset() addIs [Suc_leI, Suc_le_lessD]) 1); ``` nipkow@2608 ` 531` ```qed "Suc_le_eq"; ``` nipkow@2608 ` 532` paulson@5143 ` 533` ```Goalw [le_def] "m <= n ==> m <= Suc n"; ``` wenzelm@4089 ` 534` ```by (blast_tac (claset() addDs [Suc_lessD]) 1); ``` nipkow@2608 ` 535` ```qed "le_SucI"; ``` nipkow@2608 ` 536` ```Addsimps[le_SucI]; ``` nipkow@2608 ` 537` nipkow@2608 ` 538` ```bind_thm ("le_Suc", not_Suc_n_less_n RS leI); ``` nipkow@2608 ` 539` paulson@5143 ` 540` ```Goalw [le_def] "m < n ==> m <= (n::nat)"; ``` wenzelm@4089 ` 541` ```by (blast_tac (claset() addEs [less_asym]) 1); ``` nipkow@2608 ` 542` ```qed "less_imp_le"; ``` nipkow@2608 ` 543` paulson@3343 ` 544` ```(** Equivalence of m<=n and m m < n | m=(n::nat)"; ``` nipkow@2608 ` 547` ```by (cut_facts_tac [less_linear] 1); ``` wenzelm@4089 ` 548` ```by (blast_tac (claset() addEs [less_irrefl,less_asym]) 1); ``` nipkow@2608 ` 549` ```qed "le_imp_less_or_eq"; ``` nipkow@2608 ` 550` paulson@5143 ` 551` ```Goalw [le_def] "m m <=(n::nat)"; ``` nipkow@2608 ` 552` ```by (cut_facts_tac [less_linear] 1); ``` wenzelm@4089 ` 553` ```by (blast_tac (claset() addSEs [less_irrefl] addEs [less_asym]) 1); ``` nipkow@2608 ` 554` ```qed "less_or_eq_imp_le"; ``` nipkow@2608 ` 555` wenzelm@5069 ` 556` ```Goal "(m <= (n::nat)) = (m < n | m=n)"; ``` nipkow@2608 ` 557` ```by (REPEAT(ares_tac [iffI,less_or_eq_imp_le,le_imp_less_or_eq] 1)); ``` nipkow@2608 ` 558` ```qed "le_eq_less_or_eq"; ``` nipkow@2608 ` 559` paulson@4635 ` 560` ```(*Useful with Blast_tac. m=n ==> m<=n *) ``` paulson@4635 ` 561` ```bind_thm ("eq_imp_le", disjI2 RS less_or_eq_imp_le); ``` paulson@4635 ` 562` wenzelm@5069 ` 563` ```Goal "n <= (n::nat)"; ``` wenzelm@4089 ` 564` ```by (simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1); ``` nipkow@2608 ` 565` ```qed "le_refl"; ``` nipkow@2608 ` 566` paulson@5143 ` 567` ```Goal "[| i <= j; j < k |] ==> i < (k::nat)"; ``` paulson@4468 ` 568` ```by (blast_tac (claset() addSDs [le_imp_less_or_eq] ``` paulson@4468 ` 569` ``` addIs [less_trans]) 1); ``` nipkow@2608 ` 570` ```qed "le_less_trans"; ``` nipkow@2608 ` 571` paulson@5143 ` 572` ```Goal "[| i < j; j <= k |] ==> i < (k::nat)"; ``` paulson@4468 ` 573` ```by (blast_tac (claset() addSDs [le_imp_less_or_eq] ``` paulson@4468 ` 574` ``` addIs [less_trans]) 1); ``` nipkow@2608 ` 575` ```qed "less_le_trans"; ``` nipkow@2608 ` 576` paulson@5143 ` 577` ```Goal "[| i <= j; j <= k |] ==> i <= (k::nat)"; ``` paulson@4468 ` 578` ```by (blast_tac (claset() addSDs [le_imp_less_or_eq] ``` paulson@4468 ` 579` ``` addIs [less_or_eq_imp_le, less_trans]) 1); ``` nipkow@2608 ` 580` ```qed "le_trans"; ``` nipkow@2608 ` 581` paulson@5143 ` 582` ```Goal "[| m <= n; n <= m |] ==> m = (n::nat)"; ``` paulson@4468 ` 583` ```(*order_less_irrefl could make this proof fail*) ``` paulson@4468 ` 584` ```by (blast_tac (claset() addSDs [le_imp_less_or_eq] ``` paulson@4468 ` 585` ``` addSEs [less_irrefl] addEs [less_asym]) 1); ``` nipkow@2608 ` 586` ```qed "le_anti_sym"; ``` nipkow@2608 ` 587` wenzelm@5069 ` 588` ```Goal "(Suc(n) <= Suc(m)) = (n <= m)"; ``` wenzelm@4089 ` 589` ```by (simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1); ``` nipkow@2608 ` 590` ```qed "Suc_le_mono"; ``` nipkow@2608 ` 591` nipkow@2608 ` 592` ```AddIffs [Suc_le_mono]; ``` nipkow@2608 ` 593` nipkow@2608 ` 594` ```(* Axiom 'order_le_less' of class 'order': *) ``` wenzelm@5069 ` 595` ```Goal "(m::nat) < n = (m <= n & m ~= n)"; ``` paulson@4737 ` 596` ```by (simp_tac (simpset() addsimps [le_def, nat_neq_iff]) 1); ``` paulson@4737 ` 597` ```by (blast_tac (claset() addSEs [less_asym]) 1); ``` nipkow@2608 ` 598` ```qed "nat_less_le"; ``` nipkow@2608 ` 599` nipkow@4640 ` 600` ```(* Axiom 'linorder_linear' of class 'linorder': *) ``` wenzelm@5069 ` 601` ```Goal "(m::nat) <= n | n <= m"; ``` nipkow@4640 ` 602` ```by (simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1); ``` nipkow@4640 ` 603` ```by (cut_facts_tac [less_linear] 1); ``` wenzelm@5132 ` 604` ```by (Blast_tac 1); ``` nipkow@4640 ` 605` ```qed "nat_le_linear"; ``` nipkow@4640 ` 606` nipkow@4640 ` 607` nipkow@4640 ` 608` ```(** max ``` paulson@4599 ` 609` wenzelm@5069 ` 610` ```Goalw [max_def] "!!z::nat. (z <= max x y) = (z <= x | z <= y)"; ``` nipkow@4686 ` 611` ```by (simp_tac (simpset() addsimps [not_le_iff_less]) 1); ``` paulson@4599 ` 612` ```by (blast_tac (claset() addIs [less_imp_le, le_trans]) 1); ``` paulson@4599 ` 613` ```qed "le_max_iff_disj"; ``` paulson@4599 ` 614` wenzelm@5069 ` 615` ```Goalw [max_def] "!!z::nat. (max x y <= z) = (x <= z & y <= z)"; ``` nipkow@4686 ` 616` ```by (simp_tac (simpset() addsimps [not_le_iff_less]) 1); ``` paulson@4599 ` 617` ```by (blast_tac (claset() addIs [less_imp_le, le_trans]) 1); ``` paulson@4599 ` 618` ```qed "max_le_iff_conj"; ``` paulson@4599 ` 619` paulson@4599 ` 620` paulson@4599 ` 621` ```(** min **) ``` paulson@4599 ` 622` wenzelm@5069 ` 623` ```Goalw [min_def] "!!z::nat. (z <= min x y) = (z <= x & z <= y)"; ``` nipkow@4686 ` 624` ```by (simp_tac (simpset() addsimps [not_le_iff_less]) 1); ``` paulson@4599 ` 625` ```by (blast_tac (claset() addIs [less_imp_le, le_trans]) 1); ``` paulson@4599 ` 626` ```qed "le_min_iff_conj"; ``` paulson@4599 ` 627` wenzelm@5069 ` 628` ```Goalw [min_def] "!!z::nat. (min x y <= z) = (x <= z | y <= z)"; ``` nipkow@4686 ` 629` ```by (simp_tac (simpset() addsimps [not_le_iff_less] addsplits) 1); ``` paulson@4599 ` 630` ```by (blast_tac (claset() addIs [less_imp_le, le_trans]) 1); ``` paulson@4599 ` 631` ```qed "min_le_iff_disj"; ``` nipkow@4640 ` 632` ``` **) ``` paulson@4599 ` 633` nipkow@2608 ` 634` ```(** LEAST -- the least number operator **) ``` nipkow@2608 ` 635` wenzelm@5069 ` 636` ```Goal "(! m::nat. P m --> n <= m) = (! m. m < n --> ~ P m)"; ``` wenzelm@4089 ` 637` ```by (blast_tac (claset() addIs [leI] addEs [leE]) 1); ``` nipkow@3143 ` 638` ```val lemma = result(); ``` nipkow@3143 ` 639` nipkow@3143 ` 640` ```(* This is an old def of Least for nat, which is derived for compatibility *) ``` wenzelm@5069 ` 641` ```Goalw [Least_def] ``` nipkow@3143 ` 642` ``` "(LEAST n::nat. P n) == (@n. P(n) & (ALL m. m < n --> ~P(m)))"; ``` wenzelm@4089 ` 643` ```by (simp_tac (simpset() addsimps [lemma]) 1); ``` nipkow@3143 ` 644` ```qed "Least_nat_def"; ``` nipkow@3143 ` 645` nipkow@3143 ` 646` ```val [prem1,prem2] = goalw thy [Least_nat_def] ``` wenzelm@3842 ` 647` ``` "[| P(k::nat); !!x. x ~P(x) |] ==> (LEAST x. P(x)) = k"; ``` nipkow@2608 ` 648` ```by (rtac select_equality 1); ``` wenzelm@4089 ` 649` ```by (blast_tac (claset() addSIs [prem1,prem2]) 1); ``` nipkow@2608 ` 650` ```by (cut_facts_tac [less_linear] 1); ``` wenzelm@4089 ` 651` ```by (blast_tac (claset() addSIs [prem1] addSDs [prem2]) 1); ``` nipkow@2608 ` 652` ```qed "Least_equality"; ``` nipkow@2608 ` 653` wenzelm@3842 ` 654` ```val [prem] = goal thy "P(k::nat) ==> P(LEAST x. P(x))"; ``` nipkow@2608 ` 655` ```by (rtac (prem RS rev_mp) 1); ``` nipkow@2608 ` 656` ```by (res_inst_tac [("n","k")] less_induct 1); ``` nipkow@2608 ` 657` ```by (rtac impI 1); ``` nipkow@2608 ` 658` ```by (rtac classical 1); ``` nipkow@2608 ` 659` ```by (res_inst_tac [("s","n")] (Least_equality RS ssubst) 1); ``` nipkow@2608 ` 660` ```by (assume_tac 1); ``` nipkow@2608 ` 661` ```by (assume_tac 2); ``` paulson@2891 ` 662` ```by (Blast_tac 1); ``` nipkow@2608 ` 663` ```qed "LeastI"; ``` nipkow@2608 ` 664` nipkow@2608 ` 665` ```(*Proof is almost identical to the one above!*) ``` wenzelm@3842 ` 666` ```val [prem] = goal thy "P(k::nat) ==> (LEAST x. P(x)) <= k"; ``` nipkow@2608 ` 667` ```by (rtac (prem RS rev_mp) 1); ``` nipkow@2608 ` 668` ```by (res_inst_tac [("n","k")] less_induct 1); ``` nipkow@2608 ` 669` ```by (rtac impI 1); ``` nipkow@2608 ` 670` ```by (rtac classical 1); ``` nipkow@2608 ` 671` ```by (res_inst_tac [("s","n")] (Least_equality RS ssubst) 1); ``` nipkow@2608 ` 672` ```by (assume_tac 1); ``` nipkow@2608 ` 673` ```by (rtac le_refl 2); ``` wenzelm@4089 ` 674` ```by (blast_tac (claset() addIs [less_imp_le,le_trans]) 1); ``` nipkow@2608 ` 675` ```qed "Least_le"; ``` nipkow@2608 ` 676` wenzelm@3842 ` 677` ```val [prem] = goal thy "k < (LEAST x. P(x)) ==> ~P(k::nat)"; ``` nipkow@2608 ` 678` ```by (rtac notI 1); ``` nipkow@2608 ` 679` ```by (etac (rewrite_rule [le_def] Least_le RS notE) 1); ``` nipkow@2608 ` 680` ```by (rtac prem 1); ``` nipkow@2608 ` 681` ```qed "not_less_Least"; ``` nipkow@2608 ` 682` nipkow@3143 ` 683` ```qed_goalw "Least_Suc" thy [Least_nat_def] ``` nipkow@2608 ` 684` ``` "!!P. [| ? n. P(Suc n); ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))" ``` nipkow@2608 ` 685` ``` (fn _ => [ ``` nipkow@2608 ` 686` ``` rtac select_equality 1, ``` nipkow@3143 ` 687` ``` fold_goals_tac [Least_nat_def], ``` wenzelm@4089 ` 688` ``` safe_tac (claset() addSEs [LeastI]), ``` nipkow@2608 ` 689` ``` rename_tac "j" 1, ``` nipkow@2608 ` 690` ``` res_inst_tac [("n","j")] natE 1, ``` paulson@2891 ` 691` ``` Blast_tac 1, ``` wenzelm@4089 ` 692` ``` blast_tac (claset() addDs [Suc_less_SucD, not_less_Least]) 1, ``` nipkow@2608 ` 693` ``` rename_tac "k n" 1, ``` nipkow@2608 ` 694` ``` res_inst_tac [("n","k")] natE 1, ``` paulson@2891 ` 695` ``` Blast_tac 1, ``` nipkow@2608 ` 696` ``` hyp_subst_tac 1, ``` nipkow@3143 ` 697` ``` rewtac Least_nat_def, ``` nipkow@2608 ` 698` ``` rtac (select_equality RS arg_cong RS sym) 1, ``` paulson@4153 ` 699` ``` Safe_tac, ``` nipkow@2608 ` 700` ``` dtac Suc_mono 1, ``` paulson@2891 ` 701` ``` Blast_tac 1, ``` nipkow@2608 ` 702` ``` cut_facts_tac [less_linear] 1, ``` paulson@4153 ` 703` ``` Safe_tac, ``` nipkow@2608 ` 704` ``` atac 2, ``` paulson@2891 ` 705` ``` Blast_tac 2, ``` nipkow@2608 ` 706` ``` dtac Suc_mono 1, ``` paulson@2891 ` 707` ``` Blast_tac 1]); ``` nipkow@2608 ` 708` nipkow@2608 ` 709` nipkow@2608 ` 710` ```(*** Instantiation of transitivity prover ***) ``` nipkow@2608 ` 711` nipkow@2608 ` 712` ```structure Less_Arith = ``` nipkow@2608 ` 713` ```struct ``` nipkow@2608 ` 714` ```val nat_leI = leI; ``` nipkow@2608 ` 715` ```val nat_leD = leD; ``` nipkow@2608 ` 716` ```val lessI = lessI; ``` nipkow@2608 ` 717` ```val zero_less_Suc = zero_less_Suc; ``` nipkow@2608 ` 718` ```val less_reflE = less_irrefl; ``` nipkow@2608 ` 719` ```val less_zeroE = less_zeroE; ``` nipkow@2608 ` 720` ```val less_incr = Suc_mono; ``` nipkow@2608 ` 721` ```val less_decr = Suc_less_SucD; ``` nipkow@2608 ` 722` ```val less_incr_rhs = Suc_mono RS Suc_lessD; ``` nipkow@2608 ` 723` ```val less_decr_lhs = Suc_lessD; ``` nipkow@2608 ` 724` ```val less_trans_Suc = less_trans_Suc; ``` paulson@3343 ` 725` ```val leI = Suc_leI RS (Suc_le_mono RS iffD1); ``` nipkow@2608 ` 726` ```val not_lessI = leI RS leD ``` nipkow@2608 ` 727` ```val not_leI = prove_goal thy "!!m::nat. n < m ==> ~ m <= n" ``` nipkow@2608 ` 728` ``` (fn _ => [etac swap2 1, etac leD 1]); ``` nipkow@2608 ` 729` ```val eqI = prove_goal thy "!!m. [| m < Suc n; n < Suc m |] ==> m=n" ``` nipkow@2608 ` 730` ``` (fn _ => [etac less_SucE 1, ``` wenzelm@4089 ` 731` ``` blast_tac (claset() addSDs [Suc_less_SucD] addSEs [less_irrefl] ``` paulson@2891 ` 732` ``` addDs [less_trans_Suc]) 1, ``` paulson@2935 ` 733` ``` assume_tac 1]); ``` nipkow@2608 ` 734` ```val leD = le_eq_less_Suc RS iffD1; ``` nipkow@2608 ` 735` ```val not_lessD = nat_leI RS leD; ``` nipkow@2608 ` 736` ```val not_leD = not_leE ``` nipkow@2608 ` 737` ```val eqD1 = prove_goal thy "!!n. m = n ==> m < Suc n" ``` nipkow@2608 ` 738` ``` (fn _ => [etac subst 1, rtac lessI 1]); ``` nipkow@2608 ` 739` ```val eqD2 = sym RS eqD1; ``` nipkow@2608 ` 740` nipkow@2608 ` 741` ```fun is_zero(t) = t = Const("0",Type("nat",[])); ``` nipkow@2608 ` 742` nipkow@2608 ` 743` ```fun nnb T = T = Type("fun",[Type("nat",[]), ``` nipkow@2608 ` 744` ``` Type("fun",[Type("nat",[]), ``` nipkow@2608 ` 745` ``` Type("bool",[])])]) ``` nipkow@2608 ` 746` nipkow@2608 ` 747` ```fun decomp_Suc(Const("Suc",_)\$t) = let val (a,i) = decomp_Suc t in (a,i+1) end ``` nipkow@2608 ` 748` ``` | decomp_Suc t = (t,0); ``` nipkow@2608 ` 749` nipkow@2608 ` 750` ```fun decomp2(rel,T,lhs,rhs) = ``` nipkow@2608 ` 751` ``` if not(nnb T) then None else ``` nipkow@2608 ` 752` ``` let val (x,i) = decomp_Suc lhs ``` nipkow@2608 ` 753` ``` val (y,j) = decomp_Suc rhs ``` nipkow@2608 ` 754` ``` in case rel of ``` nipkow@2608 ` 755` ``` "op <" => Some(x,i,"<",y,j) ``` nipkow@2608 ` 756` ``` | "op <=" => Some(x,i,"<=",y,j) ``` nipkow@2608 ` 757` ``` | "op =" => Some(x,i,"=",y,j) ``` nipkow@2608 ` 758` ``` | _ => None ``` nipkow@2608 ` 759` ``` end; ``` nipkow@2608 ` 760` nipkow@2608 ` 761` ```fun negate(Some(x,i,rel,y,j)) = Some(x,i,"~"^rel,y,j) ``` nipkow@2608 ` 762` ``` | negate None = None; ``` nipkow@2608 ` 763` nipkow@2608 ` 764` ```fun decomp(_\$(Const(rel,T)\$lhs\$rhs)) = decomp2(rel,T,lhs,rhs) ``` paulson@2718 ` 765` ``` | decomp(_\$(Const("Not",_)\$(Const(rel,T)\$lhs\$rhs))) = ``` nipkow@2608 ` 766` ``` negate(decomp2(rel,T,lhs,rhs)) ``` nipkow@2608 ` 767` ``` | decomp _ = None ``` nipkow@2608 ` 768` nipkow@2608 ` 769` ```end; ``` nipkow@2608 ` 770` nipkow@2608 ` 771` ```structure Trans_Tac = Trans_Tac_Fun(Less_Arith); ``` nipkow@2608 ` 772` nipkow@2608 ` 773` ```open Trans_Tac; ``` nipkow@2608 ` 774` nipkow@2608 ` 775` ```(*** eliminates ~= in premises, which trans_tac cannot deal with ***) ``` paulson@4737 ` 776` ```bind_thm("nat_neqE", nat_neq_iff RS iffD1 RS disjE); ``` pusch@2680 ` 777` pusch@2680 ` 778` pusch@2680 ` 779` ```(* add function nat_add_primrec *) ``` paulson@4737 ` 780` ```val (_, nat_add_primrec, _, _) = ``` paulson@4737 ` 781` ``` Datatype.add_datatype ([], "nat", ``` paulson@4737 ` 782` ``` [("0", [], Mixfix ("0", [], max_pri)), ``` paulson@4737 ` 783` ``` ("Suc", [dtTyp ([], "nat")], NoSyn)]) ``` paulson@4737 ` 784` ``` (Theory.add_name "Arith" HOL.thy); ``` paulson@4737 ` 785` wenzelm@3768 ` 786` ```(*pretend Arith is part of the basic theory to fool package*) ```