src/HOL/NatDef.ML
 author paulson Thu Mar 12 10:39:19 1998 +0100 (1998-03-12) changeset 4737 4544290d5a6b parent 4686 74a12e86b20b child 4745 b855a7094195 permissions -rw-r--r--
The theorem nat_neqE, and some tidying
 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` nipkow@2608 ` 11` ```goal thy "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*) ``` nipkow@2608 ` 18` ```goal thy "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` nipkow@2608 ` 83` ```goal thy "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` nipkow@2608 ` 88` ```goal thy "inj_onto Abs_Nat Nat"; ``` nipkow@2608 ` 89` ```by (rtac inj_onto_inverseI 1); ``` nipkow@2608 ` 90` ```by (etac Abs_Nat_inverse 1); ``` nipkow@2608 ` 91` ```qed "inj_onto_Abs_Nat"; ``` nipkow@2608 ` 92` nipkow@2608 ` 93` ```(*** Distinctness of constructors ***) ``` nipkow@2608 ` 94` nipkow@2608 ` 95` ```goalw thy [Zero_def,Suc_def] "Suc(m) ~= 0"; ``` nipkow@2608 ` 96` ```by (rtac (inj_onto_Abs_Nat RS inj_onto_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` nipkow@2608 ` 110` ```goalw thy [Suc_def] "inj(Suc)"; ``` nipkow@2608 ` 111` ```by (rtac injI 1); ``` nipkow@2608 ` 112` ```by (dtac (inj_onto_Abs_Nat RS inj_ontoD) 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` nipkow@2608 ` 120` ```goal thy "(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` nipkow@2608 ` 126` ```goal thy "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@3236 ` 133` ```goal thy "!!n. 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` nipkow@2608 ` 141` ```goalw thy [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` nipkow@2608 ` 145` ```goalw thy [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` paulson@3236 ` 149` ```goalw thy [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 *) ``` nipkow@2608 ` 159` ```goal thy ``` nipkow@2608 ` 160` ``` "(%n. nat_rec c d n) = 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` nipkow@2608 ` 172` ```goal thy "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` nipkow@2608 ` 177` ```goal thy "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*) ``` paulson@3378 ` 203` ```goalw thy [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` paulson@3236 ` 215` ```goalw thy [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` nipkow@2608 ` 241` ```goalw thy [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` nipkow@2608 ` 249` ```goal thy "!!m. 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` nipkow@2608 ` 263` ```goal thy "~ 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` nipkow@2608 ` 284` ```goal thy "(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` nipkow@3484 ` 288` ```goal thy "(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` nipkow@4356 ` 299` ```goal thy "(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` nipkow@2608 ` 323` ```(** Inductive (?) properties **) ``` nipkow@2608 ` 324` nipkow@2608 ` 325` ```val [prem] = goal thy "Suc(m) < n ==> m P \ ``` nipkow@2608 ` 334` ```\ |] ==> P"; ``` nipkow@2608 ` 335` ```by (rtac (major RS lessE) 1); ``` nipkow@2608 ` 336` ```by (etac (lessI RS minor) 1); ``` nipkow@2608 ` 337` ```by (etac (Suc_lessD RS minor) 1); ``` nipkow@2608 ` 338` ```by (assume_tac 1); ``` nipkow@2608 ` 339` ```qed "Suc_lessE"; ``` nipkow@2608 ` 340` nipkow@2608 ` 341` ```goal thy "!!m n. Suc(m) < Suc(n) ==> m Suc(m) < Suc(n)"; ``` nipkow@2608 ` 346` ```by (etac rev_mp 1); ``` nipkow@2608 ` 347` ```by (nat_ind_tac "n" 1); ``` wenzelm@4089 ` 348` ```by (ALLGOALS (fast_tac (claset() addEs [less_trans, lessE]))); ``` nipkow@2608 ` 349` ```qed "Suc_mono"; ``` nipkow@2608 ` 350` nipkow@2608 ` 351` nipkow@2608 ` 352` ```goal thy "(Suc(m) < Suc(n)) = (m j Suc i < k"; ``` nipkow@2608 ` 363` ```by (nat_ind_tac "k" 1); ``` wenzelm@4089 ` 364` ```by (ALLGOALS (asm_simp_tac (simpset()))); ``` wenzelm@4089 ` 365` ```by (asm_simp_tac (simpset() addsimps [less_Suc_eq]) 1); ``` wenzelm@4089 ` 366` ```by (blast_tac (claset() addDs [Suc_lessD]) 1); ``` nipkow@2608 ` 367` ```qed_spec_mp "less_trans_Suc"; ``` nipkow@2608 ` 368` nipkow@2608 ` 369` ```(*"Less than" is a linear ordering*) ``` nipkow@2608 ` 370` ```goal thy "m P n m; m=n ==> P n m; n P n m |] ==> P n m" ``` paulson@2935 ` 385` ```( fn [major,eqCase,lessCase] => ``` nipkow@2608 ` 386` ``` [ ``` paulson@2935 ` 387` ``` (rtac (less_linear RS disjE) 1), ``` nipkow@2608 ` 388` ``` (etac disjE 2), ``` paulson@2935 ` 389` ``` (etac lessCase 1), ``` paulson@2935 ` 390` ``` (etac (sym RS eqCase) 1), ``` paulson@2935 ` 391` ``` (etac major 1) ``` nipkow@2608 ` 392` ``` ]); ``` nipkow@2608 ` 393` nipkow@2608 ` 394` ```(*Can be used with less_Suc_eq to get n=m | n P(m) |] ==> P(n) |] ==> P(n)"; ``` nipkow@2608 ` 403` ```by (wf_ind_tac "n" [wf_pred_nat RS wf_trancl] 1); ``` nipkow@2608 ` 404` ```by (eresolve_tac prems 1); ``` nipkow@2608 ` 405` ```qed "less_induct"; ``` nipkow@2608 ` 406` nipkow@2608 ` 407` ```qed_goal "nat_induct2" thy ``` nipkow@2608 ` 408` ```"[| P 0; P 1; !!k. P k ==> P (Suc (Suc k)) |] ==> P n" (fn prems => [ ``` paulson@3023 ` 409` ``` cut_facts_tac prems 1, ``` paulson@3023 ` 410` ``` rtac less_induct 1, ``` paulson@3023 ` 411` ``` res_inst_tac [("n","n")] natE 1, ``` paulson@3023 ` 412` ``` hyp_subst_tac 1, ``` paulson@3023 ` 413` ``` atac 1, ``` paulson@3023 ` 414` ``` hyp_subst_tac 1, ``` paulson@3023 ` 415` ``` res_inst_tac [("n","x")] natE 1, ``` paulson@3023 ` 416` ``` hyp_subst_tac 1, ``` paulson@3023 ` 417` ``` atac 1, ``` paulson@3023 ` 418` ``` hyp_subst_tac 1, ``` paulson@3023 ` 419` ``` resolve_tac prems 1, ``` paulson@3023 ` 420` ``` dtac spec 1, ``` paulson@3023 ` 421` ``` etac mp 1, ``` paulson@3023 ` 422` ``` rtac (lessI RS less_trans) 1, ``` paulson@3023 ` 423` ``` rtac (lessI RS Suc_mono) 1]); ``` nipkow@2608 ` 424` nipkow@2608 ` 425` ```(*** Properties of <= ***) ``` nipkow@2608 ` 426` nipkow@2608 ` 427` ```goalw thy [le_def] "(m <= n) = (m < Suc n)"; ``` nipkow@2608 ` 428` ```by (rtac not_less_eq 1); ``` nipkow@2608 ` 429` ```qed "le_eq_less_Suc"; ``` nipkow@2608 ` 430` paulson@3343 ` 431` ```(* m<=n ==> m < Suc n *) ``` paulson@3343 ` 432` ```bind_thm ("le_imp_less_Suc", le_eq_less_Suc RS iffD1); ``` paulson@3343 ` 433` nipkow@2608 ` 434` ```goalw thy [le_def] "0 <= n"; ``` nipkow@2608 ` 435` ```by (rtac not_less0 1); ``` nipkow@2608 ` 436` ```qed "le0"; ``` nipkow@2608 ` 437` nipkow@2608 ` 438` ```goalw thy [le_def] "~ Suc n <= n"; ``` nipkow@2608 ` 439` ```by (Simp_tac 1); ``` nipkow@2608 ` 440` ```qed "Suc_n_not_le_n"; ``` nipkow@2608 ` 441` nipkow@2608 ` 442` ```goalw thy [le_def] "(i <= 0) = (i = 0)"; ``` nipkow@2608 ` 443` ```by (nat_ind_tac "i" 1); ``` nipkow@2608 ` 444` ```by (ALLGOALS Asm_simp_tac); ``` nipkow@2608 ` 445` ```qed "le_0_eq"; ``` paulson@4614 ` 446` ```AddIffs [le_0_eq]; ``` nipkow@2608 ` 447` nipkow@2608 ` 448` ```Addsimps [(*less_Suc_eq, makes simpset non-confluent*) le0, le_0_eq, ``` nipkow@2608 ` 449` ``` Suc_n_not_le_n, ``` nipkow@2608 ` 450` ``` n_not_Suc_n, Suc_n_not_n, ``` nipkow@2608 ` 451` ``` nat_case_0, nat_case_Suc, nat_rec_0, nat_rec_Suc]; ``` nipkow@2608 ` 452` paulson@3355 ` 453` ```goal thy "!!m. (m <= Suc(n)) = (m<=n | m = Suc n)"; ``` wenzelm@4089 ` 454` ```by (simp_tac (simpset() addsimps [le_eq_less_Suc]) 1); ``` wenzelm@4089 ` 455` ```by (blast_tac (claset() addSEs [less_SucE] addIs [less_SucI]) 1); ``` paulson@3355 ` 456` ```qed "le_Suc_eq"; ``` paulson@3355 ` 457` paulson@4614 ` 458` ```(* [| m <= Suc n; m <= n ==> R; m = Suc n ==> R |] ==> R *) ``` paulson@4614 ` 459` ```bind_thm ("le_SucE", le_Suc_eq RS iffD1 RS disjE); ``` paulson@4614 ` 460` nipkow@2608 ` 461` ```(* ``` nipkow@2608 ` 462` ```goal thy "(Suc m < n | Suc m = n) = (m < n)"; ``` nipkow@2608 ` 463` ```by (stac (less_Suc_eq RS sym) 1); ``` nipkow@2608 ` 464` ```by (rtac Suc_less_eq 1); ``` nipkow@2608 ` 465` ```qed "Suc_le_eq"; ``` nipkow@2608 ` 466` nipkow@2608 ` 467` ```this could make the simpset (with less_Suc_eq added again) more confluent, ``` nipkow@2608 ` 468` ```but less_Suc_eq makes additional problems with terms of the form 0 < Suc (...) ``` nipkow@2608 ` 469` ```*) ``` nipkow@2608 ` 470` nipkow@2608 ` 471` ```(*Prevents simplification of f and g: much faster*) ``` nipkow@2608 ` 472` ```qed_goal "nat_case_weak_cong" thy ``` nipkow@2608 ` 473` ``` "m=n ==> nat_case a f m = nat_case a f n" ``` nipkow@2608 ` 474` ``` (fn [prem] => [rtac (prem RS arg_cong) 1]); ``` nipkow@2608 ` 475` nipkow@2608 ` 476` ```qed_goal "nat_rec_weak_cong" thy ``` nipkow@2608 ` 477` ``` "m=n ==> nat_rec a f m = nat_rec a f n" ``` nipkow@2608 ` 478` ``` (fn [prem] => [rtac (prem RS arg_cong) 1]); ``` nipkow@2608 ` 479` nipkow@2608 ` 480` ```qed_goal "expand_nat_case" thy ``` nipkow@2608 ` 481` ``` "P(nat_case z s n) = ((n=0 --> P z) & (!m. n = Suc m --> P(s m)))" ``` nipkow@2608 ` 482` ``` (fn _ => [nat_ind_tac "n" 1, ALLGOALS Asm_simp_tac]); ``` nipkow@2608 ` 483` nipkow@2608 ` 484` ```val prems = goalw thy [le_def] "~n m<=(n::nat)"; ``` nipkow@2608 ` 485` ```by (resolve_tac prems 1); ``` nipkow@2608 ` 486` ```qed "leI"; ``` nipkow@2608 ` 487` nipkow@2608 ` 488` ```val prems = goalw thy [le_def] "m<=n ==> ~ n < (m::nat)"; ``` nipkow@2608 ` 489` ```by (resolve_tac prems 1); ``` nipkow@2608 ` 490` ```qed "leD"; ``` nipkow@2608 ` 491` nipkow@2608 ` 492` ```val leE = make_elim leD; ``` nipkow@2608 ` 493` nipkow@2608 ` 494` ```goal thy "(~n n<(m::nat)"; ``` paulson@2891 ` 499` ```by (Blast_tac 1); ``` nipkow@2608 ` 500` ```qed "not_leE"; ``` nipkow@2608 ` 501` paulson@4599 ` 502` ```goalw thy [le_def] "(~n<=m) = (m<(n::nat))"; ``` paulson@4599 ` 503` ```by (Simp_tac 1); ``` paulson@4599 ` 504` ```qed "not_le_iff_less"; ``` paulson@4599 ` 505` nipkow@2608 ` 506` ```goalw thy [le_def] "!!m. m < n ==> Suc(m) <= n"; ``` wenzelm@4089 ` 507` ```by (simp_tac (simpset() addsimps [less_Suc_eq]) 1); ``` wenzelm@4089 ` 508` ```by (blast_tac (claset() addSEs [less_irrefl,less_asym]) 1); ``` paulson@3343 ` 509` ```qed "Suc_leI"; (*formerly called lessD*) ``` nipkow@2608 ` 510` nipkow@2608 ` 511` ```goalw thy [le_def] "!!m. Suc(m) <= n ==> m <= n"; ``` wenzelm@4089 ` 512` ```by (asm_full_simp_tac (simpset() addsimps [less_Suc_eq]) 1); ``` nipkow@2608 ` 513` ```qed "Suc_leD"; ``` nipkow@2608 ` 514` nipkow@2608 ` 515` ```(* stronger version of Suc_leD *) ``` nipkow@2608 ` 516` ```goalw thy [le_def] ``` nipkow@2608 ` 517` ``` "!!m. Suc m <= n ==> m < n"; ``` wenzelm@4089 ` 518` ```by (asm_full_simp_tac (simpset() addsimps [less_Suc_eq]) 1); ``` nipkow@2608 ` 519` ```by (cut_facts_tac [less_linear] 1); ``` paulson@2891 ` 520` ```by (Blast_tac 1); ``` nipkow@2608 ` 521` ```qed "Suc_le_lessD"; ``` nipkow@2608 ` 522` nipkow@2608 ` 523` ```goal thy "(Suc m <= n) = (m < n)"; ``` wenzelm@4089 ` 524` ```by (blast_tac (claset() addIs [Suc_leI, Suc_le_lessD]) 1); ``` nipkow@2608 ` 525` ```qed "Suc_le_eq"; ``` nipkow@2608 ` 526` nipkow@2608 ` 527` ```goalw thy [le_def] "!!m. m <= n ==> m <= Suc n"; ``` wenzelm@4089 ` 528` ```by (blast_tac (claset() addDs [Suc_lessD]) 1); ``` nipkow@2608 ` 529` ```qed "le_SucI"; ``` nipkow@2608 ` 530` ```Addsimps[le_SucI]; ``` nipkow@2608 ` 531` nipkow@2608 ` 532` ```bind_thm ("le_Suc", not_Suc_n_less_n RS leI); ``` nipkow@2608 ` 533` nipkow@2608 ` 534` ```goalw thy [le_def] "!!m. m < n ==> m <= (n::nat)"; ``` wenzelm@4089 ` 535` ```by (blast_tac (claset() addEs [less_asym]) 1); ``` nipkow@2608 ` 536` ```qed "less_imp_le"; ``` nipkow@2608 ` 537` paulson@3343 ` 538` ```(** Equivalence of m<=n and m m < n | m=(n::nat)"; ``` nipkow@2608 ` 541` ```by (cut_facts_tac [less_linear] 1); ``` wenzelm@4089 ` 542` ```by (blast_tac (claset() addEs [less_irrefl,less_asym]) 1); ``` nipkow@2608 ` 543` ```qed "le_imp_less_or_eq"; ``` nipkow@2608 ` 544` nipkow@2608 ` 545` ```goalw thy [le_def] "!!m. m m <=(n::nat)"; ``` nipkow@2608 ` 546` ```by (cut_facts_tac [less_linear] 1); ``` wenzelm@4089 ` 547` ```by (blast_tac (claset() addSEs [less_irrefl] addEs [less_asym]) 1); ``` nipkow@2608 ` 548` ```qed "less_or_eq_imp_le"; ``` nipkow@2608 ` 549` paulson@3343 ` 550` ```goal thy "(m <= (n::nat)) = (m < n | m=n)"; ``` nipkow@2608 ` 551` ```by (REPEAT(ares_tac [iffI,less_or_eq_imp_le,le_imp_less_or_eq] 1)); ``` nipkow@2608 ` 552` ```qed "le_eq_less_or_eq"; ``` nipkow@2608 ` 553` paulson@4635 ` 554` ```(*Useful with Blast_tac. m=n ==> m<=n *) ``` paulson@4635 ` 555` ```bind_thm ("eq_imp_le", disjI2 RS less_or_eq_imp_le); ``` paulson@4635 ` 556` nipkow@2608 ` 557` ```goal thy "n <= (n::nat)"; ``` wenzelm@4089 ` 558` ```by (simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1); ``` nipkow@2608 ` 559` ```qed "le_refl"; ``` nipkow@2608 ` 560` paulson@4468 ` 561` ```goal thy "!!i. [| i <= j; j < k |] ==> i < (k::nat)"; ``` paulson@4468 ` 562` ```by (blast_tac (claset() addSDs [le_imp_less_or_eq] ``` paulson@4468 ` 563` ``` addIs [less_trans]) 1); ``` nipkow@2608 ` 564` ```qed "le_less_trans"; ``` nipkow@2608 ` 565` nipkow@2608 ` 566` ```goal thy "!!i. [| i < j; j <= k |] ==> i < (k::nat)"; ``` paulson@4468 ` 567` ```by (blast_tac (claset() addSDs [le_imp_less_or_eq] ``` paulson@4468 ` 568` ``` addIs [less_trans]) 1); ``` nipkow@2608 ` 569` ```qed "less_le_trans"; ``` nipkow@2608 ` 570` nipkow@2608 ` 571` ```goal thy "!!i. [| i <= j; j <= k |] ==> i <= (k::nat)"; ``` paulson@4468 ` 572` ```by (blast_tac (claset() addSDs [le_imp_less_or_eq] ``` paulson@4468 ` 573` ``` addIs [less_or_eq_imp_le, less_trans]) 1); ``` nipkow@2608 ` 574` ```qed "le_trans"; ``` nipkow@2608 ` 575` paulson@2891 ` 576` ```goal thy "!!m. [| m <= n; n <= m |] ==> m = (n::nat)"; ``` paulson@4468 ` 577` ```(*order_less_irrefl could make this proof fail*) ``` paulson@4468 ` 578` ```by (blast_tac (claset() addSDs [le_imp_less_or_eq] ``` paulson@4468 ` 579` ``` addSEs [less_irrefl] addEs [less_asym]) 1); ``` nipkow@2608 ` 580` ```qed "le_anti_sym"; ``` nipkow@2608 ` 581` nipkow@2608 ` 582` ```goal thy "(Suc(n) <= Suc(m)) = (n <= m)"; ``` wenzelm@4089 ` 583` ```by (simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1); ``` nipkow@2608 ` 584` ```qed "Suc_le_mono"; ``` nipkow@2608 ` 585` nipkow@2608 ` 586` ```AddIffs [Suc_le_mono]; ``` nipkow@2608 ` 587` nipkow@2608 ` 588` ```(* Axiom 'order_le_less' of class 'order': *) ``` nipkow@2608 ` 589` ```goal thy "(m::nat) < n = (m <= n & m ~= n)"; ``` paulson@4737 ` 590` ```by (simp_tac (simpset() addsimps [le_def, nat_neq_iff]) 1); ``` paulson@4737 ` 591` ```by (blast_tac (claset() addSEs [less_asym]) 1); ``` nipkow@2608 ` 592` ```qed "nat_less_le"; ``` nipkow@2608 ` 593` nipkow@4640 ` 594` ```(* Axiom 'linorder_linear' of class 'linorder': *) ``` nipkow@4640 ` 595` ```goal thy "(m::nat) <= n | n <= m"; ``` nipkow@4640 ` 596` ```by (simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1); ``` nipkow@4640 ` 597` ```by (cut_facts_tac [less_linear] 1); ``` nipkow@4640 ` 598` ```by(Blast_tac 1); ``` nipkow@4640 ` 599` ```qed "nat_le_linear"; ``` nipkow@4640 ` 600` nipkow@4640 ` 601` nipkow@4640 ` 602` ```(** max ``` paulson@4599 ` 603` paulson@4599 ` 604` ```goalw thy [max_def] "!!z::nat. (z <= max x y) = (z <= x | z <= y)"; ``` nipkow@4686 ` 605` ```by (simp_tac (simpset() addsimps [not_le_iff_less]) 1); ``` paulson@4599 ` 606` ```by (blast_tac (claset() addIs [less_imp_le, le_trans]) 1); ``` paulson@4599 ` 607` ```qed "le_max_iff_disj"; ``` paulson@4599 ` 608` paulson@4599 ` 609` ```goalw thy [max_def] "!!z::nat. (max x y <= z) = (x <= z & y <= z)"; ``` nipkow@4686 ` 610` ```by (simp_tac (simpset() addsimps [not_le_iff_less]) 1); ``` paulson@4599 ` 611` ```by (blast_tac (claset() addIs [less_imp_le, le_trans]) 1); ``` paulson@4599 ` 612` ```qed "max_le_iff_conj"; ``` paulson@4599 ` 613` paulson@4599 ` 614` paulson@4599 ` 615` ```(** min **) ``` paulson@4599 ` 616` paulson@4599 ` 617` ```goalw thy [min_def] "!!z::nat. (z <= min x y) = (z <= x & z <= y)"; ``` nipkow@4686 ` 618` ```by (simp_tac (simpset() addsimps [not_le_iff_less]) 1); ``` paulson@4599 ` 619` ```by (blast_tac (claset() addIs [less_imp_le, le_trans]) 1); ``` paulson@4599 ` 620` ```qed "le_min_iff_conj"; ``` paulson@4599 ` 621` paulson@4599 ` 622` ```goalw thy [min_def] "!!z::nat. (min x y <= z) = (x <= z | y <= z)"; ``` nipkow@4686 ` 623` ```by (simp_tac (simpset() addsimps [not_le_iff_less] addsplits) 1); ``` paulson@4599 ` 624` ```by (blast_tac (claset() addIs [less_imp_le, le_trans]) 1); ``` paulson@4599 ` 625` ```qed "min_le_iff_disj"; ``` nipkow@4640 ` 626` ``` **) ``` paulson@4599 ` 627` nipkow@2608 ` 628` ```(** LEAST -- the least number operator **) ``` nipkow@2608 ` 629` nipkow@3143 ` 630` ```goal thy "(! m::nat. P m --> n <= m) = (! m. m < n --> ~ P m)"; ``` wenzelm@4089 ` 631` ```by (blast_tac (claset() addIs [leI] addEs [leE]) 1); ``` nipkow@3143 ` 632` ```val lemma = result(); ``` nipkow@3143 ` 633` nipkow@3143 ` 634` ```(* This is an old def of Least for nat, which is derived for compatibility *) ``` nipkow@3143 ` 635` ```goalw thy [Least_def] ``` nipkow@3143 ` 636` ``` "(LEAST n::nat. P n) == (@n. P(n) & (ALL m. m < n --> ~P(m)))"; ``` wenzelm@4089 ` 637` ```by (simp_tac (simpset() addsimps [lemma]) 1); ``` nipkow@3143 ` 638` ```qed "Least_nat_def"; ``` nipkow@3143 ` 639` nipkow@3143 ` 640` ```val [prem1,prem2] = goalw thy [Least_nat_def] ``` wenzelm@3842 ` 641` ``` "[| P(k::nat); !!x. x ~P(x) |] ==> (LEAST x. P(x)) = k"; ``` nipkow@2608 ` 642` ```by (rtac select_equality 1); ``` wenzelm@4089 ` 643` ```by (blast_tac (claset() addSIs [prem1,prem2]) 1); ``` nipkow@2608 ` 644` ```by (cut_facts_tac [less_linear] 1); ``` wenzelm@4089 ` 645` ```by (blast_tac (claset() addSIs [prem1] addSDs [prem2]) 1); ``` nipkow@2608 ` 646` ```qed "Least_equality"; ``` nipkow@2608 ` 647` wenzelm@3842 ` 648` ```val [prem] = goal thy "P(k::nat) ==> P(LEAST x. P(x))"; ``` nipkow@2608 ` 649` ```by (rtac (prem RS rev_mp) 1); ``` nipkow@2608 ` 650` ```by (res_inst_tac [("n","k")] less_induct 1); ``` nipkow@2608 ` 651` ```by (rtac impI 1); ``` nipkow@2608 ` 652` ```by (rtac classical 1); ``` nipkow@2608 ` 653` ```by (res_inst_tac [("s","n")] (Least_equality RS ssubst) 1); ``` nipkow@2608 ` 654` ```by (assume_tac 1); ``` nipkow@2608 ` 655` ```by (assume_tac 2); ``` paulson@2891 ` 656` ```by (Blast_tac 1); ``` nipkow@2608 ` 657` ```qed "LeastI"; ``` nipkow@2608 ` 658` nipkow@2608 ` 659` ```(*Proof is almost identical to the one above!*) ``` wenzelm@3842 ` 660` ```val [prem] = goal thy "P(k::nat) ==> (LEAST x. P(x)) <= k"; ``` nipkow@2608 ` 661` ```by (rtac (prem RS rev_mp) 1); ``` nipkow@2608 ` 662` ```by (res_inst_tac [("n","k")] less_induct 1); ``` nipkow@2608 ` 663` ```by (rtac impI 1); ``` nipkow@2608 ` 664` ```by (rtac classical 1); ``` nipkow@2608 ` 665` ```by (res_inst_tac [("s","n")] (Least_equality RS ssubst) 1); ``` nipkow@2608 ` 666` ```by (assume_tac 1); ``` nipkow@2608 ` 667` ```by (rtac le_refl 2); ``` wenzelm@4089 ` 668` ```by (blast_tac (claset() addIs [less_imp_le,le_trans]) 1); ``` nipkow@2608 ` 669` ```qed "Least_le"; ``` nipkow@2608 ` 670` wenzelm@3842 ` 671` ```val [prem] = goal thy "k < (LEAST x. P(x)) ==> ~P(k::nat)"; ``` nipkow@2608 ` 672` ```by (rtac notI 1); ``` nipkow@2608 ` 673` ```by (etac (rewrite_rule [le_def] Least_le RS notE) 1); ``` nipkow@2608 ` 674` ```by (rtac prem 1); ``` nipkow@2608 ` 675` ```qed "not_less_Least"; ``` nipkow@2608 ` 676` nipkow@3143 ` 677` ```qed_goalw "Least_Suc" thy [Least_nat_def] ``` nipkow@2608 ` 678` ``` "!!P. [| ? n. P(Suc n); ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))" ``` nipkow@2608 ` 679` ``` (fn _ => [ ``` nipkow@2608 ` 680` ``` rtac select_equality 1, ``` nipkow@3143 ` 681` ``` fold_goals_tac [Least_nat_def], ``` wenzelm@4089 ` 682` ``` safe_tac (claset() addSEs [LeastI]), ``` nipkow@2608 ` 683` ``` rename_tac "j" 1, ``` nipkow@2608 ` 684` ``` res_inst_tac [("n","j")] natE 1, ``` paulson@2891 ` 685` ``` Blast_tac 1, ``` wenzelm@4089 ` 686` ``` blast_tac (claset() addDs [Suc_less_SucD, not_less_Least]) 1, ``` nipkow@2608 ` 687` ``` rename_tac "k n" 1, ``` nipkow@2608 ` 688` ``` res_inst_tac [("n","k")] natE 1, ``` paulson@2891 ` 689` ``` Blast_tac 1, ``` nipkow@2608 ` 690` ``` hyp_subst_tac 1, ``` nipkow@3143 ` 691` ``` rewtac Least_nat_def, ``` nipkow@2608 ` 692` ``` rtac (select_equality RS arg_cong RS sym) 1, ``` paulson@4153 ` 693` ``` Safe_tac, ``` nipkow@2608 ` 694` ``` dtac Suc_mono 1, ``` paulson@2891 ` 695` ``` Blast_tac 1, ``` nipkow@2608 ` 696` ``` cut_facts_tac [less_linear] 1, ``` paulson@4153 ` 697` ``` Safe_tac, ``` nipkow@2608 ` 698` ``` atac 2, ``` paulson@2891 ` 699` ``` Blast_tac 2, ``` nipkow@2608 ` 700` ``` dtac Suc_mono 1, ``` paulson@2891 ` 701` ``` Blast_tac 1]); ``` nipkow@2608 ` 702` nipkow@2608 ` 703` nipkow@2608 ` 704` ```(*** Instantiation of transitivity prover ***) ``` nipkow@2608 ` 705` nipkow@2608 ` 706` ```structure Less_Arith = ``` nipkow@2608 ` 707` ```struct ``` nipkow@2608 ` 708` ```val nat_leI = leI; ``` nipkow@2608 ` 709` ```val nat_leD = leD; ``` nipkow@2608 ` 710` ```val lessI = lessI; ``` nipkow@2608 ` 711` ```val zero_less_Suc = zero_less_Suc; ``` nipkow@2608 ` 712` ```val less_reflE = less_irrefl; ``` nipkow@2608 ` 713` ```val less_zeroE = less_zeroE; ``` nipkow@2608 ` 714` ```val less_incr = Suc_mono; ``` nipkow@2608 ` 715` ```val less_decr = Suc_less_SucD; ``` nipkow@2608 ` 716` ```val less_incr_rhs = Suc_mono RS Suc_lessD; ``` nipkow@2608 ` 717` ```val less_decr_lhs = Suc_lessD; ``` nipkow@2608 ` 718` ```val less_trans_Suc = less_trans_Suc; ``` paulson@3343 ` 719` ```val leI = Suc_leI RS (Suc_le_mono RS iffD1); ``` nipkow@2608 ` 720` ```val not_lessI = leI RS leD ``` nipkow@2608 ` 721` ```val not_leI = prove_goal thy "!!m::nat. n < m ==> ~ m <= n" ``` nipkow@2608 ` 722` ``` (fn _ => [etac swap2 1, etac leD 1]); ``` nipkow@2608 ` 723` ```val eqI = prove_goal thy "!!m. [| m < Suc n; n < Suc m |] ==> m=n" ``` nipkow@2608 ` 724` ``` (fn _ => [etac less_SucE 1, ``` wenzelm@4089 ` 725` ``` blast_tac (claset() addSDs [Suc_less_SucD] addSEs [less_irrefl] ``` paulson@2891 ` 726` ``` addDs [less_trans_Suc]) 1, ``` paulson@2935 ` 727` ``` assume_tac 1]); ``` nipkow@2608 ` 728` ```val leD = le_eq_less_Suc RS iffD1; ``` nipkow@2608 ` 729` ```val not_lessD = nat_leI RS leD; ``` nipkow@2608 ` 730` ```val not_leD = not_leE ``` nipkow@2608 ` 731` ```val eqD1 = prove_goal thy "!!n. m = n ==> m < Suc n" ``` nipkow@2608 ` 732` ``` (fn _ => [etac subst 1, rtac lessI 1]); ``` nipkow@2608 ` 733` ```val eqD2 = sym RS eqD1; ``` nipkow@2608 ` 734` nipkow@2608 ` 735` ```fun is_zero(t) = t = Const("0",Type("nat",[])); ``` nipkow@2608 ` 736` nipkow@2608 ` 737` ```fun nnb T = T = Type("fun",[Type("nat",[]), ``` nipkow@2608 ` 738` ``` Type("fun",[Type("nat",[]), ``` nipkow@2608 ` 739` ``` Type("bool",[])])]) ``` nipkow@2608 ` 740` nipkow@2608 ` 741` ```fun decomp_Suc(Const("Suc",_)\$t) = let val (a,i) = decomp_Suc t in (a,i+1) end ``` nipkow@2608 ` 742` ``` | decomp_Suc t = (t,0); ``` nipkow@2608 ` 743` nipkow@2608 ` 744` ```fun decomp2(rel,T,lhs,rhs) = ``` nipkow@2608 ` 745` ``` if not(nnb T) then None else ``` nipkow@2608 ` 746` ``` let val (x,i) = decomp_Suc lhs ``` nipkow@2608 ` 747` ``` val (y,j) = decomp_Suc rhs ``` nipkow@2608 ` 748` ``` in case rel of ``` nipkow@2608 ` 749` ``` "op <" => Some(x,i,"<",y,j) ``` nipkow@2608 ` 750` ``` | "op <=" => Some(x,i,"<=",y,j) ``` nipkow@2608 ` 751` ``` | "op =" => Some(x,i,"=",y,j) ``` nipkow@2608 ` 752` ``` | _ => None ``` nipkow@2608 ` 753` ``` end; ``` nipkow@2608 ` 754` nipkow@2608 ` 755` ```fun negate(Some(x,i,rel,y,j)) = Some(x,i,"~"^rel,y,j) ``` nipkow@2608 ` 756` ``` | negate None = None; ``` nipkow@2608 ` 757` nipkow@2608 ` 758` ```fun decomp(_\$(Const(rel,T)\$lhs\$rhs)) = decomp2(rel,T,lhs,rhs) ``` paulson@2718 ` 759` ``` | decomp(_\$(Const("Not",_)\$(Const(rel,T)\$lhs\$rhs))) = ``` nipkow@2608 ` 760` ``` negate(decomp2(rel,T,lhs,rhs)) ``` nipkow@2608 ` 761` ``` | decomp _ = None ``` nipkow@2608 ` 762` nipkow@2608 ` 763` ```end; ``` nipkow@2608 ` 764` nipkow@2608 ` 765` ```structure Trans_Tac = Trans_Tac_Fun(Less_Arith); ``` nipkow@2608 ` 766` nipkow@2608 ` 767` ```open Trans_Tac; ``` nipkow@2608 ` 768` nipkow@2608 ` 769` ```(*** eliminates ~= in premises, which trans_tac cannot deal with ***) ``` paulson@4737 ` 770` ```bind_thm("nat_neqE", nat_neq_iff RS iffD1 RS disjE); ``` pusch@2680 ` 771` pusch@2680 ` 772` pusch@2680 ` 773` ```(* add function nat_add_primrec *) ``` paulson@4737 ` 774` ```val (_, nat_add_primrec, _, _) = ``` paulson@4737 ` 775` ``` Datatype.add_datatype ([], "nat", ``` paulson@4737 ` 776` ``` [("0", [], Mixfix ("0", [], max_pri)), ``` paulson@4737 ` 777` ``` ("Suc", [dtTyp ([], "nat")], NoSyn)]) ``` paulson@4737 ` 778` ``` (Theory.add_name "Arith" HOL.thy); ``` paulson@4737 ` 779` wenzelm@3768 ` 780` ```(*pretend Arith is part of the basic theory to fool package*) ```