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