src/HOL/Real/PNat.ML
author wenzelm
Thu Jun 22 23:04:34 2000 +0200 (2000-06-22)
changeset 9108 9fff97d29837
parent 9043 ca761fe227d8
child 9422 4b6bc2b347e5
permissions -rw-r--r--
bind_thm(s);
     1 (*  Title       : PNat.ML
     2     ID          : $Id$
     3     Author      : Jacques D. Fleuriot
     4     Copyright   : 1998  University of Cambridge
     5     Description : The positive naturals -- proofs 
     6                 : mainly as in Nat.thy
     7 *)
     8 
     9 Goal "mono(%X. {1} Un (Suc``X))";
    10 by (REPEAT (ares_tac [monoI, subset_refl, image_mono, Un_mono] 1));
    11 qed "pnat_fun_mono";
    12 
    13 bind_thm ("pnat_unfold", pnat_fun_mono RS (pnat_def RS def_lfp_Tarski));
    14 
    15 Goal "1 : pnat";
    16 by (stac pnat_unfold 1);
    17 by (rtac (singletonI RS UnI1) 1);
    18 qed "one_RepI";
    19 
    20 Addsimps [one_RepI];
    21 
    22 Goal "i: pnat ==> Suc(i) : pnat";
    23 by (stac pnat_unfold 1);
    24 by (etac (imageI RS UnI2) 1);
    25 qed "pnat_Suc_RepI";
    26 
    27 Goal "2 : pnat";
    28 by (rtac (one_RepI RS pnat_Suc_RepI) 1);
    29 qed "two_RepI";
    30 
    31 (*** Induction ***)
    32 
    33 val major::prems = goal thy
    34     "[| i: pnat;  P(1);   \
    35 \       !!j. [| j: pnat; P(j) |] ==> P(Suc(j)) |]  ==> P(i)";
    36 by (rtac ([pnat_def, pnat_fun_mono, major] MRS def_induct) 1);
    37 by (blast_tac (claset() addIs prems) 1);
    38 qed "PNat_induct";
    39 
    40 val prems = goalw thy [pnat_one_def,pnat_Suc_def]
    41     "[| P(1p);   \
    42 \       !!n. P(n) ==> P(pSuc n) |]  ==> P(n)";
    43 by (rtac (Rep_pnat_inverse RS subst) 1);   
    44 by (rtac (Rep_pnat RS PNat_induct) 1);
    45 by (REPEAT (ares_tac prems 1
    46      ORELSE eresolve_tac [Abs_pnat_inverse RS subst] 1));
    47 qed "pnat_induct";
    48 
    49 (*Perform induction on n. *)
    50 fun pnat_ind_tac a i = 
    51   res_inst_tac [("n",a)] pnat_induct i  THEN  rename_last_tac a [""] (i+1);
    52 
    53 val prems = goal thy
    54     "[| !!x. P x 1p;  \
    55 \       !!y. P 1p (pSuc y);  \
    56 \       !!x y. [| P x y |] ==> P (pSuc x) (pSuc y)  \
    57 \    |] ==> P m n";
    58 by (res_inst_tac [("x","m")] spec 1);
    59 by (pnat_ind_tac "n" 1);
    60 by (rtac allI 2);
    61 by (pnat_ind_tac "x" 2);
    62 by (REPEAT (ares_tac (prems@[allI]) 1 ORELSE etac spec 1));
    63 qed "pnat_diff_induct";
    64 
    65 (*Case analysis on the natural numbers*)
    66 val prems = goal thy 
    67     "[| n=1p ==> P;  !!x. n = pSuc(x) ==> P |] ==> P";
    68 by (subgoal_tac "n=1p | (EX x. n = pSuc(x))" 1);
    69 by (fast_tac (claset() addSEs prems) 1);
    70 by (pnat_ind_tac "n" 1);
    71 by (rtac (refl RS disjI1) 1);
    72 by (Blast_tac 1);
    73 qed "pnatE";
    74 
    75 (*** Isomorphisms: Abs_Nat and Rep_Nat ***)
    76 
    77 Goal "inj_on Abs_pnat pnat";
    78 by (rtac inj_on_inverseI 1);
    79 by (etac Abs_pnat_inverse 1);
    80 qed "inj_on_Abs_pnat";
    81 
    82 Addsimps [inj_on_Abs_pnat RS inj_on_iff];
    83 
    84 Goal "inj(Rep_pnat)";
    85 by (rtac inj_inverseI 1);
    86 by (rtac Rep_pnat_inverse 1);
    87 qed "inj_Rep_pnat";
    88 
    89 Goal "0 ~: pnat";
    90 by (stac pnat_unfold 1);
    91 by Auto_tac;
    92 qed "zero_not_mem_pnat";
    93 
    94 (* 0 : pnat ==> P *)
    95 bind_thm ("zero_not_mem_pnatE", zero_not_mem_pnat RS notE);
    96 
    97 Addsimps [zero_not_mem_pnat];
    98 
    99 Goal "x : pnat ==> 0 < x";
   100 by (dtac (pnat_unfold RS subst) 1);
   101 by Auto_tac;
   102 qed "mem_pnat_gt_zero";
   103 
   104 Goal "0 < x ==> x: pnat";
   105 by (stac pnat_unfold 1);
   106 by (dtac (gr_implies_not0 RS not0_implies_Suc) 1); 
   107 by (etac exE 1 THEN Asm_simp_tac 1);
   108 by (induct_tac "m" 1);
   109 by (auto_tac (claset(),simpset() 
   110     addsimps [one_RepI]) THEN dtac pnat_Suc_RepI 1);
   111 by (Blast_tac 1);
   112 qed "gt_0_mem_pnat";
   113 
   114 Goal "(x: pnat) = (0 < x)";
   115 by (blast_tac (claset() addDs [mem_pnat_gt_zero,gt_0_mem_pnat]) 1);
   116 qed "mem_pnat_gt_0_iff";
   117 
   118 Goal "0 < Rep_pnat x";
   119 by (rtac (Rep_pnat RS mem_pnat_gt_zero) 1);
   120 qed "Rep_pnat_gt_zero";
   121 
   122 Goalw [pnat_add_def] "(x::pnat) + y = y + x";
   123 by (simp_tac (simpset() addsimps [add_commute]) 1);
   124 qed "pnat_add_commute";
   125 
   126 (** alternative definition for pnat **)
   127 (** order isomorphism **)
   128 Goal "pnat = {x::nat. 0 < x}";
   129 by (rtac set_ext 1);
   130 by (simp_tac (simpset() addsimps 
   131     [mem_pnat_gt_0_iff]) 1);
   132 qed "Collect_pnat_gt_0";
   133 
   134 (*** Distinctness of constructors ***)
   135 
   136 Goalw [pnat_one_def,pnat_Suc_def] "pSuc(m) ~= 1p";
   137 by (rtac (inj_on_Abs_pnat RS inj_on_contraD) 1);
   138 by (rtac (Rep_pnat_gt_zero RS Suc_mono RS less_not_refl2) 1);
   139 by (REPEAT (resolve_tac [Rep_pnat RS  pnat_Suc_RepI, one_RepI] 1));
   140 qed "pSuc_not_one";
   141 
   142 bind_thm ("one_not_pSuc", pSuc_not_one RS not_sym);
   143 
   144 AddIffs [pSuc_not_one,one_not_pSuc];
   145 
   146 bind_thm ("pSuc_neq_one", (pSuc_not_one RS notE));
   147 bind_thm ("one_neq_pSuc", pSuc_neq_one RS pSuc_neq_one);
   148 
   149 (** Injectiveness of pSuc **)
   150 
   151 Goalw [pnat_Suc_def] "inj(pSuc)";
   152 by (rtac injI 1);
   153 by (dtac (inj_on_Abs_pnat RS inj_onD) 1);
   154 by (REPEAT (resolve_tac [Rep_pnat, pnat_Suc_RepI] 1));
   155 by (dtac (inj_Suc RS injD) 1);
   156 by (etac (inj_Rep_pnat RS injD) 1);
   157 qed "inj_pSuc"; 
   158 
   159 bind_thm ("pSuc_inject", inj_pSuc RS injD);
   160 
   161 Goal "(pSuc(m)=pSuc(n)) = (m=n)";
   162 by (EVERY1 [rtac iffI, etac pSuc_inject, etac arg_cong]); 
   163 qed "pSuc_pSuc_eq";
   164 
   165 AddIffs [pSuc_pSuc_eq];
   166 
   167 Goal "n ~= pSuc(n)";
   168 by (pnat_ind_tac "n" 1);
   169 by (ALLGOALS Asm_simp_tac);
   170 qed "n_not_pSuc_n";
   171 
   172 bind_thm ("pSuc_n_not_n", n_not_pSuc_n RS not_sym);
   173 
   174 Goal "n ~= 1p ==> EX m. n = pSuc m";
   175 by (rtac pnatE 1);
   176 by (REPEAT (Blast_tac 1));
   177 qed "not1p_implies_pSuc";
   178 
   179 Goal "pSuc m = m + 1p";
   180 by (auto_tac (claset(),simpset() addsimps [pnat_Suc_def,
   181     pnat_one_def,Abs_pnat_inverse,pnat_add_def]));
   182 qed "pSuc_is_plus_one";
   183 
   184 Goal
   185       "(Rep_pnat x + Rep_pnat y): pnat";
   186 by (cut_facts_tac [[Rep_pnat_gt_zero,
   187     Rep_pnat_gt_zero] MRS add_less_mono,Collect_pnat_gt_0] 1);
   188 by (etac ssubst 1);
   189 by Auto_tac;
   190 qed "sum_Rep_pnat";
   191 
   192 Goalw [pnat_add_def] 
   193       "Rep_pnat x + Rep_pnat y = Rep_pnat (x + y)";
   194 by (simp_tac (simpset() addsimps [sum_Rep_pnat RS 
   195                           Abs_pnat_inverse]) 1);
   196 qed "sum_Rep_pnat_sum";
   197 
   198 Goalw [pnat_add_def] 
   199       "(x + y) + z = x + (y + (z::pnat))";
   200 by (res_inst_tac [("f","Abs_pnat")] arg_cong 1);
   201 by (simp_tac (simpset() addsimps [sum_Rep_pnat RS 
   202                 Abs_pnat_inverse,add_assoc]) 1);
   203 qed "pnat_add_assoc";
   204 
   205 Goalw [pnat_add_def] "x + (y + z) = y + (x + (z::pnat))";
   206 by (res_inst_tac [("f","Abs_pnat")] arg_cong 1);
   207 by (simp_tac (simpset() addsimps [sum_Rep_pnat RS 
   208           Abs_pnat_inverse,add_left_commute]) 1);
   209 qed "pnat_add_left_commute";
   210 
   211 (*Addition is an AC-operator*)
   212 bind_thms ("pnat_add_ac", [pnat_add_assoc, pnat_add_commute, pnat_add_left_commute]);
   213 
   214 Goalw [pnat_add_def] "((x::pnat) + y = x + z) = (y = z)";
   215 by (auto_tac (claset() addDs [inj_on_Abs_pnat RS inj_onD,
   216      inj_Rep_pnat RS injD],simpset() addsimps [sum_Rep_pnat]));
   217 qed "pnat_add_left_cancel";
   218 
   219 Goalw [pnat_add_def] "(y + (x::pnat) = z + x) = (y = z)";
   220 by (auto_tac (claset() addDs [inj_on_Abs_pnat RS inj_onD,
   221      inj_Rep_pnat RS injD],simpset() addsimps [sum_Rep_pnat]));
   222 qed "pnat_add_right_cancel";
   223 
   224 Goalw [pnat_add_def] "!(y::pnat). x + y ~= x";
   225 by (rtac (Rep_pnat_inverse RS subst) 1);
   226 by (auto_tac (claset() addDs [inj_on_Abs_pnat RS inj_onD] 
   227   	               addSDs [add_eq_self_zero],
   228 	      simpset() addsimps [sum_Rep_pnat, Rep_pnat,Abs_pnat_inverse,
   229 				  Rep_pnat_gt_zero RS less_not_refl2]));
   230 qed "pnat_no_add_ident";
   231 
   232 
   233 (***) (***) (***) (***) (***) (***) (***) (***) (***)
   234 
   235   (*** pnat_less ***)
   236 
   237 Goalw [pnat_less_def] 
   238       "[| x < (y::pnat); y < z |] ==> x < z";
   239 by ((etac less_trans 1) THEN assume_tac 1);
   240 qed "pnat_less_trans";
   241 
   242 Goalw [pnat_less_def] "x < (y::pnat) ==> ~ y < x";
   243 by (etac less_not_sym 1);
   244 qed "pnat_less_not_sym";
   245 
   246 (* [| x < y;  ~P ==> y < x |] ==> P *)
   247 bind_thm ("pnat_less_asym", pnat_less_not_sym RS swap);
   248 
   249 Goalw [pnat_less_def] "~ y < (y::pnat)";
   250 by Auto_tac;
   251 qed "pnat_less_not_refl";
   252 
   253 bind_thm ("pnat_less_irrefl",pnat_less_not_refl RS notE);
   254 
   255 Goalw [pnat_less_def] 
   256      "x < (y::pnat) ==> x ~= y";
   257 by Auto_tac;
   258 qed "pnat_less_not_refl2";
   259 
   260 Goal "~ Rep_pnat y < 0";
   261 by Auto_tac;
   262 qed "Rep_pnat_not_less0";
   263 
   264 (*** Rep_pnat < 0 ==> P ***)
   265 bind_thm ("Rep_pnat_less_zeroE",Rep_pnat_not_less0 RS notE);
   266 
   267 Goal "~ Rep_pnat y < 1";
   268 by (auto_tac (claset(),simpset() addsimps [less_Suc_eq,
   269                   Rep_pnat_gt_zero,less_not_refl2]));
   270 qed "Rep_pnat_not_less_one";
   271 
   272 (*** Rep_pnat < 1 ==> P ***)
   273 bind_thm ("Rep_pnat_less_oneE",Rep_pnat_not_less_one RS notE);
   274 
   275 Goalw [pnat_less_def] 
   276      "x < (y::pnat) ==> Rep_pnat y ~= 1";
   277 by (auto_tac (claset(),simpset() 
   278     addsimps [Rep_pnat_not_less_one] delsimps [less_one]));
   279 qed "Rep_pnat_gt_implies_not0";
   280 
   281 Goalw [pnat_less_def] 
   282       "(x::pnat) < y | x = y | y < x";
   283 by (cut_facts_tac [less_linear] 1);
   284 by (fast_tac (claset() addIs [inj_Rep_pnat RS injD]) 1);
   285 qed "pnat_less_linear";
   286 
   287 Goalw [le_def] "1 <= Rep_pnat x";
   288 by (rtac Rep_pnat_not_less_one 1);
   289 qed "Rep_pnat_le_one";
   290 
   291 Goalw [pnat_less_def]
   292      "!! (z1::nat). z1 < z2  ==> EX z3. z1 + Rep_pnat z3 = z2";
   293 by (dtac less_imp_add_positive 1);
   294 by (force_tac (claset() addSIs [Abs_pnat_inverse],
   295 	       simpset() addsimps [Collect_pnat_gt_0]) 1);
   296 qed "lemma_less_ex_sum_Rep_pnat";
   297 
   298 
   299    (*** pnat_le ***)
   300 
   301 Goalw [pnat_le_def] "~ (x::pnat) < y ==> y <= x";
   302 by (assume_tac 1);
   303 qed "pnat_leI";
   304 
   305 Goalw [pnat_le_def] "(x::pnat) <= y ==> ~ y < x";
   306 by (assume_tac 1);
   307 qed "pnat_leD";
   308 
   309 bind_thm ("pnat_leE", make_elim pnat_leD);
   310 
   311 Goal "(~ (x::pnat) < y) = (y <= x)";
   312 by (blast_tac (claset() addIs [pnat_leI] addEs [pnat_leE]) 1);
   313 qed "pnat_not_less_iff_le";
   314 
   315 Goalw [pnat_le_def] "~(x::pnat) <= y ==> y < x";
   316 by (Blast_tac 1);
   317 qed "pnat_not_leE";
   318 
   319 Goalw [pnat_le_def] "(x::pnat) < y ==> x <= y";
   320 by (blast_tac (claset() addEs [pnat_less_asym]) 1);
   321 qed "pnat_less_imp_le";
   322 
   323 (** Equivalence of m<=n and  m<n | m=n **)
   324 
   325 Goalw [pnat_le_def] "m <= n ==> m < n | m=(n::pnat)";
   326 by (cut_facts_tac [pnat_less_linear] 1);
   327 by (blast_tac (claset() addEs [pnat_less_irrefl,pnat_less_asym]) 1);
   328 qed "pnat_le_imp_less_or_eq";
   329 
   330 Goalw [pnat_le_def] "m<n | m=n ==> m <=(n::pnat)";
   331 by (cut_facts_tac [pnat_less_linear] 1);
   332 by (blast_tac (claset() addSEs [pnat_less_irrefl] addEs [pnat_less_asym]) 1);
   333 qed "pnat_less_or_eq_imp_le";
   334 
   335 Goal "(m <= (n::pnat)) = (m < n | m=n)";
   336 by (REPEAT(ares_tac [iffI,pnat_less_or_eq_imp_le,pnat_le_imp_less_or_eq] 1));
   337 qed "pnat_le_eq_less_or_eq";
   338 
   339 Goal "n <= (n::pnat)";
   340 by (simp_tac (simpset() addsimps [pnat_le_eq_less_or_eq]) 1);
   341 qed "pnat_le_refl";
   342 
   343 val prems = goal thy "!!i. [| i <= j; j < k |] ==> i < (k::pnat)";
   344 by (dtac pnat_le_imp_less_or_eq 1);
   345 by (blast_tac (claset() addIs [pnat_less_trans]) 1);
   346 qed "pnat_le_less_trans";
   347 
   348 Goal "[| i < j; j <= k |] ==> i < (k::pnat)";
   349 by (dtac pnat_le_imp_less_or_eq 1);
   350 by (blast_tac (claset() addIs [pnat_less_trans]) 1);
   351 qed "pnat_less_le_trans";
   352 
   353 Goal "[| i <= j; j <= k |] ==> i <= (k::pnat)";
   354 by (EVERY1[dtac pnat_le_imp_less_or_eq, 
   355            dtac pnat_le_imp_less_or_eq,
   356            rtac pnat_less_or_eq_imp_le, 
   357            blast_tac (claset() addIs [pnat_less_trans])]);
   358 qed "pnat_le_trans";
   359 
   360 Goal "[| m <= n; n <= m |] ==> m = (n::pnat)";
   361 by (EVERY1[dtac pnat_le_imp_less_or_eq, 
   362            dtac pnat_le_imp_less_or_eq,
   363            blast_tac (claset() addIs [pnat_less_asym])]);
   364 qed "pnat_le_anti_sym";
   365 
   366 Goal "(m::pnat) < n = (m <= n & m ~= n)";
   367 by (rtac iffI 1);
   368 by (rtac conjI 1);
   369 by (etac pnat_less_imp_le 1);
   370 by (etac pnat_less_not_refl2 1);
   371 by (blast_tac (claset() addSDs [pnat_le_imp_less_or_eq]) 1);
   372 qed "pnat_less_le";
   373 
   374 (** LEAST -- the least number operator **)
   375 
   376 Goal "(! m::pnat. P m --> n <= m) = (! m. m < n --> ~ P m)";
   377 by (blast_tac (claset() addIs [pnat_leI] addEs [pnat_leE]) 1);
   378 val lemma = result();
   379 
   380 (* Comment below from NatDef.ML where Least_nat_def is proved*)
   381 (* This is an old def of Least for nat, which is derived for compatibility *)
   382 Goalw [Least_def]
   383   "(LEAST n::pnat. P n) == (@n. P(n) & (ALL m. m < n --> ~P(m)))";
   384 by (simp_tac (simpset() addsimps [lemma]) 1);
   385 qed "Least_pnat_def";
   386 
   387 val [prem1,prem2] = goalw thy [Least_pnat_def]
   388     "[| P(k::pnat);  !!x. x<k ==> ~P(x) |] ==> (LEAST x. P(x)) = k";
   389 by (rtac select_equality 1);
   390 by (blast_tac (claset() addSIs [prem1,prem2]) 1);
   391 by (cut_facts_tac [pnat_less_linear] 1);
   392 by (blast_tac (claset() addSIs [prem1] addSDs [prem2]) 1);
   393 qed "pnat_Least_equality";
   394 
   395 (***) (***) (***) (***) (***) (***) (***) (***)
   396 
   397 (*** alternative definition for pnat_le ***)
   398 Goalw [pnat_le_def,pnat_less_def] 
   399       "((m::pnat) <= n) = (Rep_pnat m <= Rep_pnat n)";
   400 by (auto_tac (claset() addSIs [leI] addSEs [leD],simpset()));
   401 qed "pnat_le_iff_Rep_pnat_le";
   402 
   403 Goal "!!k::pnat. (k + m <= k + n) = (m<=n)";
   404 by (simp_tac (simpset() addsimps [pnat_le_iff_Rep_pnat_le,
   405                            sum_Rep_pnat_sum RS sym]) 1);
   406 qed "pnat_add_left_cancel_le";
   407 
   408 Goalw [pnat_less_def] "!!k::pnat. (k + m < k + n) = (m<n)";
   409 by (simp_tac (simpset() addsimps [sum_Rep_pnat_sum RS sym]) 1);
   410 qed "pnat_add_left_cancel_less";
   411 
   412 Addsimps [pnat_add_left_cancel, pnat_add_right_cancel,
   413   pnat_add_left_cancel_le, pnat_add_left_cancel_less];
   414 
   415 Goal "n <= ((m + n)::pnat)";
   416 by (simp_tac (simpset() addsimps [pnat_le_iff_Rep_pnat_le,
   417                     sum_Rep_pnat_sum RS sym,le_add2]) 1);
   418 qed "pnat_le_add2";
   419 
   420 Goal "n <= ((n + m)::pnat)";
   421 by (simp_tac (simpset() addsimps pnat_add_ac) 1);
   422 by (rtac pnat_le_add2 1);
   423 qed "pnat_le_add1";
   424 
   425 (*** "i <= j ==> i <= j + m" ***)
   426 bind_thm ("pnat_trans_le_add1", pnat_le_add1 RSN (2,pnat_le_trans));
   427 
   428 (*** "i <= j ==> i <= m + j" ***)
   429 bind_thm ("pnat_trans_le_add2", pnat_le_add2 RSN (2,pnat_le_trans));
   430 
   431 (*"i < j ==> i < j + m"*)
   432 bind_thm ("pnat_trans_less_add1", pnat_le_add1 RSN (2,pnat_less_le_trans));
   433 
   434 (*"i < j ==> i < m + j"*)
   435 bind_thm ("pnat_trans_less_add2", pnat_le_add2 RSN (2,pnat_less_le_trans));
   436 
   437 Goalw [pnat_less_def] "i+j < (k::pnat) ==> i<k";
   438 by (auto_tac (claset() addEs [add_lessD1],
   439     simpset() addsimps [sum_Rep_pnat_sum RS sym]));
   440 qed "pnat_add_lessD1";
   441 
   442 Goal "!!i::pnat. ~ (i+j < i)";
   443 by (rtac  notI 1);
   444 by (etac (pnat_add_lessD1 RS pnat_less_irrefl) 1);
   445 qed "pnat_not_add_less1";
   446 
   447 Goal "!!i::pnat. ~ (j+i < i)";
   448 by (simp_tac (simpset() addsimps [pnat_add_commute, pnat_not_add_less1]) 1);
   449 qed "pnat_not_add_less2";
   450 
   451 AddIffs [pnat_not_add_less1, pnat_not_add_less2];
   452 
   453 Goal "m + k <= n --> m <= (n::pnat)";
   454 by (simp_tac (simpset() addsimps [pnat_le_iff_Rep_pnat_le,
   455     sum_Rep_pnat_sum RS sym]) 1);
   456 qed_spec_mp "pnat_add_leD1";
   457 
   458 Goal "!!n::pnat. m + k <= n ==> k <= n";
   459 by (full_simp_tac (simpset() addsimps [pnat_add_commute]) 1);
   460 by (etac pnat_add_leD1 1);
   461 qed_spec_mp "pnat_add_leD2";
   462 
   463 Goal "!!n::pnat. m + k <= n ==> m <= n & k <= n";
   464 by (blast_tac (claset() addDs [pnat_add_leD1, pnat_add_leD2]) 1);
   465 bind_thm ("pnat_add_leE", result() RS conjE);
   466 
   467 Goalw [pnat_less_def] 
   468       "!!k l::pnat. [| k < l; m + l = k + n |] ==> m < n";
   469 by (rtac less_add_eq_less 1 THEN assume_tac 1);
   470 by (auto_tac (claset(),simpset() addsimps [sum_Rep_pnat_sum]));
   471 qed "pnat_less_add_eq_less";
   472 
   473 (* ordering on positive naturals in terms of existence of sum *)
   474 (* could provide alternative definition -- Gleason *)
   475 Goalw [pnat_less_def,pnat_add_def] 
   476       "(z1::pnat) < z2 = (EX z3. z1 + z3 = z2)";
   477 by (rtac iffI 1);
   478 by (res_inst_tac [("t","z2")] (Rep_pnat_inverse RS subst) 1);
   479 by (dtac lemma_less_ex_sum_Rep_pnat 1);
   480 by (etac exE 1 THEN res_inst_tac [("x","z3")] exI 1);
   481 by (auto_tac (claset(),simpset() addsimps [sum_Rep_pnat_sum,Rep_pnat_inverse]));
   482 by (res_inst_tac [("t","Rep_pnat z1")] (add_0_right RS subst) 1);
   483 by (auto_tac (claset(),simpset() addsimps [sum_Rep_pnat_sum RS sym,
   484                Rep_pnat_gt_zero] delsimps [add_0_right]));
   485 qed "pnat_less_iff";
   486 
   487 Goal "(EX (x::pnat). z1 + x = z2) | z1 = z2 \
   488 \          |(EX x. z2 + x = z1)";
   489 by (cut_facts_tac [pnat_less_linear] 1);
   490 by (asm_full_simp_tac (simpset() addsimps [pnat_less_iff]) 1);
   491 qed "pnat_linear_Ex_eq";
   492 
   493 Goal "!!(x::pnat). x + y = z ==> x < z";
   494 by (rtac (pnat_less_iff RS iffD2) 1);
   495 by (Blast_tac 1);
   496 qed "pnat_eq_lessI";
   497 
   498 (*** Monotonicity of Addition ***)
   499 
   500 (*strict, in 1st argument*)
   501 Goalw [pnat_less_def] "!!i j k::pnat. i < j ==> i + k < j + k";
   502 by (auto_tac (claset() addIs [add_less_mono1],
   503        simpset() addsimps [sum_Rep_pnat_sum RS sym]));
   504 qed "pnat_add_less_mono1";
   505 
   506 Goalw [pnat_less_def] "!!i j k::pnat. [|i < j; k < l|] ==> i + k < j + l";
   507 by (auto_tac (claset() addIs [add_less_mono],
   508        simpset() addsimps [sum_Rep_pnat_sum RS sym]));
   509 qed "pnat_add_less_mono";
   510 
   511 Goalw [pnat_less_def]
   512 "!!f. [| !!i j::pnat. i<j ==> f(i) < f(j);       \
   513 \        i <= j                                 \
   514 \     |] ==> f(i) <= (f(j)::pnat)";
   515 by (auto_tac (claset() addSDs [inj_Rep_pnat RS injD],
   516              simpset() addsimps [pnat_le_iff_Rep_pnat_le,
   517 				 order_le_less]));
   518 qed "pnat_less_mono_imp_le_mono";
   519 
   520 Goal "!!i j k::pnat. i<=j ==> i + k <= j + k";
   521 by (res_inst_tac [("f", "%j. j+k")] pnat_less_mono_imp_le_mono 1);
   522 by (etac pnat_add_less_mono1 1);
   523 by (assume_tac 1);
   524 qed "pnat_add_le_mono1";
   525 
   526 Goal "!!k l::pnat. [|i<=j;  k<=l |] ==> i + k <= j + l";
   527 by (etac (pnat_add_le_mono1 RS pnat_le_trans) 1);
   528 by (simp_tac (simpset() addsimps [pnat_add_commute]) 1);
   529 (*j moves to the end because it is free while k, l are bound*)
   530 by (etac pnat_add_le_mono1 1);
   531 qed "pnad_add_le_mono";
   532 
   533 Goal "1 * Rep_pnat n = Rep_pnat n";
   534 by (Asm_simp_tac 1);
   535 qed "Rep_pnat_mult_1";
   536 
   537 Goal "Rep_pnat n * 1 = Rep_pnat n";
   538 by (Asm_simp_tac 1);
   539 qed "Rep_pnat_mult_1_right";
   540 
   541 Goal
   542       "(Rep_pnat x * Rep_pnat y): pnat";
   543 by (cut_facts_tac [[Rep_pnat_gt_zero,
   544     Rep_pnat_gt_zero] MRS mult_less_mono1,Collect_pnat_gt_0] 1);
   545 by (etac ssubst 1);
   546 by Auto_tac;
   547 qed "mult_Rep_pnat";
   548 
   549 Goalw [pnat_mult_def] 
   550       "Rep_pnat x * Rep_pnat y = Rep_pnat (x * y)";
   551 by (simp_tac (simpset() addsimps [mult_Rep_pnat RS 
   552                           Abs_pnat_inverse]) 1);
   553 qed "mult_Rep_pnat_mult";
   554 
   555 Goalw [pnat_mult_def] "m * n = n * (m::pnat)";
   556 by (full_simp_tac (simpset() addsimps [mult_commute]) 1);
   557 qed "pnat_mult_commute";
   558 
   559 Goalw [pnat_mult_def,pnat_add_def] "(m + n)*k = (m*k) + ((n*k)::pnat)";
   560 by (res_inst_tac [("f","Abs_pnat")] arg_cong 1);
   561 by (simp_tac (simpset() addsimps [mult_Rep_pnat RS 
   562                 Abs_pnat_inverse,sum_Rep_pnat RS 
   563              Abs_pnat_inverse, add_mult_distrib]) 1);
   564 qed "pnat_add_mult_distrib";
   565 
   566 Goalw [pnat_mult_def,pnat_add_def] "k*(m + n) = (k*m) + ((k*n)::pnat)";
   567 by (res_inst_tac [("f","Abs_pnat")] arg_cong 1);
   568 by (simp_tac (simpset() addsimps [mult_Rep_pnat RS 
   569                 Abs_pnat_inverse,sum_Rep_pnat RS 
   570              Abs_pnat_inverse, add_mult_distrib2]) 1);
   571 qed "pnat_add_mult_distrib2";
   572 
   573 Goalw [pnat_mult_def] 
   574       "(x * y) * z = x * (y * (z::pnat))";
   575 by (res_inst_tac [("f","Abs_pnat")] arg_cong 1);
   576 by (simp_tac (simpset() addsimps [mult_Rep_pnat RS 
   577                 Abs_pnat_inverse,mult_assoc]) 1);
   578 qed "pnat_mult_assoc";
   579 
   580 Goalw [pnat_mult_def] "x * (y * z) = y * (x * (z::pnat))";
   581 by (res_inst_tac [("f","Abs_pnat")] arg_cong 1);
   582 by (simp_tac (simpset() addsimps [mult_Rep_pnat RS 
   583           Abs_pnat_inverse,mult_left_commute]) 1);
   584 qed "pnat_mult_left_commute";
   585 
   586 Goalw [pnat_mult_def] "x * (Abs_pnat 1) = x";
   587 by (full_simp_tac (simpset() addsimps [one_RepI RS Abs_pnat_inverse,
   588                    Rep_pnat_inverse]) 1);
   589 qed "pnat_mult_1";
   590 
   591 Goal "Abs_pnat 1 * x = x";
   592 by (full_simp_tac (simpset() addsimps [pnat_mult_1,
   593                    pnat_mult_commute]) 1);
   594 qed "pnat_mult_1_left";
   595 
   596 (*Multiplication is an AC-operator*)
   597 bind_thms ("pnat_mult_ac", [pnat_mult_assoc, pnat_mult_commute, pnat_mult_left_commute]);
   598 
   599 Goal "!!i j k::pnat. i<=j ==> i * k <= j * k";
   600 by (asm_full_simp_tac (simpset() addsimps [pnat_le_iff_Rep_pnat_le,
   601                      mult_Rep_pnat_mult RS sym,mult_le_mono1]) 1);
   602 qed "pnat_mult_le_mono1";
   603 
   604 Goal "!!i::pnat. [| i<=j; k<=l |] ==> i*k<=j*l";
   605 by (asm_full_simp_tac (simpset() addsimps [pnat_le_iff_Rep_pnat_le,
   606                      mult_Rep_pnat_mult RS sym,mult_le_mono]) 1);
   607 qed "pnat_mult_le_mono";
   608 
   609 Goal "!!i::pnat. i<j ==> k*i < k*j";
   610 by (asm_full_simp_tac (simpset() addsimps [pnat_less_def,
   611     mult_Rep_pnat_mult RS sym,Rep_pnat_gt_zero,mult_less_mono2]) 1);
   612 qed "pnat_mult_less_mono2";
   613 
   614 Goal "!!i::pnat. i<j ==> i*k < j*k";
   615 by (dtac pnat_mult_less_mono2 1);
   616 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [pnat_mult_commute])));
   617 qed "pnat_mult_less_mono1";
   618 
   619 Goalw [pnat_less_def] "(m*(k::pnat) < n*k) = (m<n)";
   620 by (asm_full_simp_tac (simpset() addsimps [mult_Rep_pnat_mult 
   621               RS sym,Rep_pnat_gt_zero]) 1);
   622 qed "pnat_mult_less_cancel2";
   623 
   624 Goalw [pnat_less_def] "((k::pnat)*m < k*n) = (m<n)";
   625 by (asm_full_simp_tac (simpset() addsimps [mult_Rep_pnat_mult 
   626               RS sym,Rep_pnat_gt_zero]) 1);
   627 qed "pnat_mult_less_cancel1";
   628 
   629 Addsimps [pnat_mult_less_cancel1, pnat_mult_less_cancel2];
   630 
   631 Goalw [pnat_mult_def]  "(m*(k::pnat) = n*k) = (m=n)";
   632 by (auto_tac (claset() addSDs [inj_on_Abs_pnat RS inj_onD, 
   633     inj_Rep_pnat RS injD] addIs [mult_Rep_pnat], 
   634     simpset() addsimps [Rep_pnat_gt_zero RS mult_cancel2]));
   635 qed "pnat_mult_cancel2";
   636 
   637 Goal "((k::pnat)*m = k*n) = (m=n)";
   638 by (rtac (pnat_mult_cancel2 RS subst) 1);
   639 by (auto_tac (claset () addIs [pnat_mult_commute RS subst],simpset()));
   640 qed "pnat_mult_cancel1";
   641 
   642 Addsimps [pnat_mult_cancel1, pnat_mult_cancel2];
   643 
   644 Goal
   645      "!!(z1::pnat). z2*z3 = z4*z5  ==> z2*(z1*z3) = z4*(z1*z5)";
   646 by (auto_tac (claset() addIs [pnat_mult_cancel1 RS iffD2],
   647     simpset() addsimps [pnat_mult_left_commute]));
   648 qed "pnat_same_multI2";
   649 
   650 val [prem] = goal thy
   651     "(!!u. z = Abs_pnat(u) ==> P) ==> P";
   652 by (cut_inst_tac [("x1","z")] 
   653     (rewrite_rule [pnat_def] (Rep_pnat RS Abs_pnat_inverse)) 1);
   654 by (res_inst_tac [("u","Rep_pnat z")] prem 1);
   655 by (dtac (inj_Rep_pnat RS injD) 1);
   656 by (Asm_simp_tac 1);
   657 qed "eq_Abs_pnat";
   658 
   659 (** embedding of naturals in positive naturals **)
   660 
   661 (* pnat_one_eq! *)
   662 Goalw [pnat_of_nat_def,pnat_one_def]"1p = pnat_of_nat 0";
   663 by (Full_simp_tac 1);
   664 qed "pnat_one_iff";
   665 
   666 Goalw [pnat_of_nat_def,pnat_one_def,
   667        pnat_add_def] "1p + 1p = pnat_of_nat 1";
   668 by (res_inst_tac [("f","Abs_pnat")] arg_cong 1);
   669 by (auto_tac (claset() addIs [(gt_0_mem_pnat RS Abs_pnat_inverse RS ssubst)],
   670     simpset()));
   671 qed "pnat_two_eq";
   672 
   673 Goal "inj(pnat_of_nat)";
   674 by (rtac injI 1);
   675 by (rewtac pnat_of_nat_def);
   676 by (dtac (inj_on_Abs_pnat RS inj_onD) 1);
   677 by (auto_tac (claset() addSIs [gt_0_mem_pnat],simpset()));
   678 qed "inj_pnat_of_nat";
   679 
   680 Goal "0 < n + 1";
   681 by Auto_tac;
   682 qed "nat_add_one_less";
   683 
   684 Goal "0 < n1 + n2 + 1";
   685 by Auto_tac;
   686 qed "nat_add_one_less1";
   687 
   688 (* this worked with one call to auto_tac before! *)
   689 Goalw [pnat_add_def,pnat_of_nat_def,pnat_one_def] 
   690       "pnat_of_nat n1 + pnat_of_nat n2 = \
   691 \      pnat_of_nat (n1 + n2) + 1p";
   692 by (res_inst_tac [("f","Abs_pnat")] arg_cong 1);
   693 by (rtac (gt_0_mem_pnat RS Abs_pnat_inverse RS ssubst) 1);
   694 by (rtac (gt_0_mem_pnat RS Abs_pnat_inverse RS ssubst) 2);
   695 by (rtac (gt_0_mem_pnat RS Abs_pnat_inverse RS ssubst) 3);
   696 by (rtac (gt_0_mem_pnat RS Abs_pnat_inverse RS ssubst) 4);
   697 by (auto_tac (claset(),
   698 	      simpset() addsimps [sum_Rep_pnat_sum,
   699 				  nat_add_one_less,nat_add_one_less1]));
   700 qed "pnat_of_nat_add";
   701 
   702 Goalw [pnat_of_nat_def,pnat_less_def] 
   703        "(n < m) = (pnat_of_nat n < pnat_of_nat m)";
   704 by (auto_tac (claset(),simpset() 
   705     addsimps [Abs_pnat_inverse,Collect_pnat_gt_0]));
   706 qed "pnat_of_nat_less_iff";
   707 Addsimps [pnat_of_nat_less_iff RS sym];
   708 
   709 goalw PNat.thy [pnat_mult_def,pnat_of_nat_def] 
   710       "pnat_of_nat n1 * pnat_of_nat n2 = \
   711 \      pnat_of_nat (n1 * n2 + n1 + n2)";
   712 by (auto_tac (claset(),simpset() addsimps [mult_Rep_pnat_mult,
   713     pnat_add_def,Abs_pnat_inverse,gt_0_mem_pnat]));
   714 qed "pnat_of_nat_mult";