src/HOL/Real/PNat.ML
author wenzelm
Wed, 23 Jan 2002 17:13:54 +0100
changeset 12842 32c9c881dec8
parent 12018 ec054019c910
permissions -rw-r--r--
delsimps [less_Suc0];
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
9422
4b6bc2b347e5 avoid referencing thy value;
wenzelm
parents: 9108
diff changeset
     1
(*  Title       : HOL/Real/PNat.ML
7219
4e3f386c2e37 inserted Id: lines
paulson
parents: 7077
diff changeset
     2
    ID          : $Id$
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     3
    Author      : Jacques D. Fleuriot
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     4
    Copyright   : 1998  University of Cambridge
9422
4b6bc2b347e5 avoid referencing thy value;
wenzelm
parents: 9108
diff changeset
     5
4b6bc2b347e5 avoid referencing thy value;
wenzelm
parents: 9108
diff changeset
     6
The positive naturals -- proofs mainly as in theory Nat.
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     7
*)
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     8
11701
3d51fbf81c17 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents: 11655
diff changeset
     9
Goal "mono(%X. {Suc 0} Un Suc`X)";
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    10
by (REPEAT (ares_tac [monoI, subset_refl, image_mono, Un_mono] 1));
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    11
qed "pnat_fun_mono";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    12
10186
499637e8f2c6 *** empty log message ***
nipkow
parents: 9747
diff changeset
    13
bind_thm ("pnat_unfold", pnat_fun_mono RS (pnat_def RS def_lfp_unfold));
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    14
11701
3d51fbf81c17 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents: 11655
diff changeset
    15
Goal "Suc 0 : pnat";
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    16
by (stac pnat_unfold 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    17
by (rtac (singletonI RS UnI1) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    18
qed "one_RepI";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    19
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    20
Addsimps [one_RepI];
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    21
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    22
Goal "i: pnat ==> Suc(i) : pnat";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    23
by (stac pnat_unfold 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    24
by (etac (imageI RS UnI2) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    25
qed "pnat_Suc_RepI";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    26
11701
3d51fbf81c17 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents: 11655
diff changeset
    27
Goal "Suc (Suc 0) : pnat";
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    28
by (rtac (one_RepI RS pnat_Suc_RepI) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    29
qed "two_RepI";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    30
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    31
(*** Induction ***)
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    32
9635
c9ebf0a1d712 tidied & updated proofs, deleting some unused ones
paulson
parents: 9422
diff changeset
    33
val major::prems = Goal
11701
3d51fbf81c17 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents: 11655
diff changeset
    34
    "[| i: pnat;  P(Suc 0);   \
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    35
\       !!j. [| j: pnat; P(j) |] ==> P(Suc(j)) |]  ==> P(i)";
10202
9e8b4bebc940 induct -> lfp_induct
nipkow
parents: 10186
diff changeset
    36
by (rtac ([pnat_def, pnat_fun_mono, major] MRS def_lfp_induct) 1);
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    37
by (blast_tac (claset() addIs prems) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    38
qed "PNat_induct";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    39
9635
c9ebf0a1d712 tidied & updated proofs, deleting some unused ones
paulson
parents: 9422
diff changeset
    40
val prems = Goalw [pnat_one_def,pnat_Suc_def]
12018
ec054019c910 Numerals and simprocs for types real and hypreal. The abstract
paulson
parents: 11701
diff changeset
    41
    "[| P(1);   \
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    42
\       !!n. P(n) ==> P(pSuc n) |]  ==> P(n)";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    43
by (rtac (Rep_pnat_inverse RS subst) 1);   
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    44
by (rtac (Rep_pnat RS PNat_induct) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    45
by (REPEAT (ares_tac prems 1
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    46
     ORELSE eresolve_tac [Abs_pnat_inverse RS subst] 1));
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    47
qed "pnat_induct";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    48
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    49
(*Perform induction on n. *)
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5148
diff changeset
    50
fun pnat_ind_tac a i = 
9747
043098ba5098 introduced induct_thm_tac
nipkow
parents: 9635
diff changeset
    51
  induct_thm_tac pnat_induct a i  THEN  rename_last_tac a [""] (i+1);
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    52
9635
c9ebf0a1d712 tidied & updated proofs, deleting some unused ones
paulson
parents: 9422
diff changeset
    53
val prems = Goal
12018
ec054019c910 Numerals and simprocs for types real and hypreal. The abstract
paulson
parents: 11701
diff changeset
    54
    "[| !!x. P x 1;  \
ec054019c910 Numerals and simprocs for types real and hypreal. The abstract
paulson
parents: 11701
diff changeset
    55
\       !!y. P 1 (pSuc y);  \
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    56
\       !!x y. [| P x y |] ==> P (pSuc x) (pSuc y)  \
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    57
\    |] ==> P m n";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    58
by (res_inst_tac [("x","m")] spec 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    59
by (pnat_ind_tac "n" 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    60
by (rtac allI 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    61
by (pnat_ind_tac "x" 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    62
by (REPEAT (ares_tac (prems@[allI]) 1 ORELSE etac spec 1));
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    63
qed "pnat_diff_induct";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    64
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    65
(*Case analysis on the natural numbers*)
9635
c9ebf0a1d712 tidied & updated proofs, deleting some unused ones
paulson
parents: 9422
diff changeset
    66
val prems = Goal
12018
ec054019c910 Numerals and simprocs for types real and hypreal. The abstract
paulson
parents: 11701
diff changeset
    67
    "[| n=1 ==> P;  !!x. n = pSuc(x) ==> P |] ==> P";
ec054019c910 Numerals and simprocs for types real and hypreal. The abstract
paulson
parents: 11701
diff changeset
    68
by (subgoal_tac "n=1 | (EX x. n = pSuc(x))" 1);
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    69
by (fast_tac (claset() addSEs prems) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    70
by (pnat_ind_tac "n" 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    71
by (rtac (refl RS disjI1) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    72
by (Blast_tac 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    73
qed "pnatE";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    74
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    75
(*** Isomorphisms: Abs_Nat and Rep_Nat ***)
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    76
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    77
Goal "inj_on Abs_pnat pnat";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    78
by (rtac inj_on_inverseI 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    79
by (etac Abs_pnat_inverse 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    80
qed "inj_on_Abs_pnat";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    81
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    82
Addsimps [inj_on_Abs_pnat RS inj_on_iff];
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    83
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    84
Goal "inj(Rep_pnat)";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    85
by (rtac inj_inverseI 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    86
by (rtac Rep_pnat_inverse 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    87
qed "inj_Rep_pnat";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    88
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    89
Goal "0 ~: pnat";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    90
by (stac pnat_unfold 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    91
by Auto_tac;
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    92
qed "zero_not_mem_pnat";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    93
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    94
(* 0 : pnat ==> P *)
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    95
bind_thm ("zero_not_mem_pnatE", zero_not_mem_pnat RS notE);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    96
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    97
Addsimps [zero_not_mem_pnat];
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    98
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5078
diff changeset
    99
Goal "x : pnat ==> 0 < x";
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   100
by (dtac (pnat_unfold RS subst) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   101
by Auto_tac;
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   102
qed "mem_pnat_gt_zero";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   103
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5078
diff changeset
   104
Goal "0 < x ==> x: pnat";
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   105
by (stac pnat_unfold 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   106
by (dtac (gr_implies_not0 RS not0_implies_Suc) 1); 
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   107
by (etac exE 1 THEN Asm_simp_tac 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   108
by (induct_tac "m" 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   109
by (auto_tac (claset(),simpset() 
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   110
    addsimps [one_RepI]) THEN dtac pnat_Suc_RepI 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   111
by (Blast_tac 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   112
qed "gt_0_mem_pnat";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   113
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   114
Goal "(x: pnat) = (0 < x)";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   115
by (blast_tac (claset() addDs [mem_pnat_gt_zero,gt_0_mem_pnat]) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   116
qed "mem_pnat_gt_0_iff";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   117
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   118
Goal "0 < Rep_pnat x";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   119
by (rtac (Rep_pnat RS mem_pnat_gt_zero) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   120
qed "Rep_pnat_gt_zero";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   121
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   122
Goalw [pnat_add_def] "(x::pnat) + y = y + x";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   123
by (simp_tac (simpset() addsimps [add_commute]) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   124
qed "pnat_add_commute";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   125
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   126
(** alternative definition for pnat **)
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   127
(** order isomorphism **)
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   128
Goal "pnat = {x::nat. 0 < x}";
10292
paulson
parents: 10231
diff changeset
   129
by (auto_tac (claset(), simpset() addsimps [mem_pnat_gt_0_iff]));  
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   130
qed "Collect_pnat_gt_0";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   131
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   132
(*** Distinctness of constructors ***)
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   133
12018
ec054019c910 Numerals and simprocs for types real and hypreal. The abstract
paulson
parents: 11701
diff changeset
   134
Goalw [pnat_one_def,pnat_Suc_def] "pSuc(m) ~= 1";
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   135
by (rtac (inj_on_Abs_pnat RS inj_on_contraD) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   136
by (rtac (Rep_pnat_gt_zero RS Suc_mono RS less_not_refl2) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   137
by (REPEAT (resolve_tac [Rep_pnat RS  pnat_Suc_RepI, one_RepI] 1));
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   138
qed "pSuc_not_one";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   139
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   140
bind_thm ("one_not_pSuc", pSuc_not_one RS not_sym);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   141
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   142
AddIffs [pSuc_not_one,one_not_pSuc];
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   143
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   144
bind_thm ("pSuc_neq_one", (pSuc_not_one RS notE));
9108
9fff97d29837 bind_thm(s);
wenzelm
parents: 9043
diff changeset
   145
bind_thm ("one_neq_pSuc", pSuc_neq_one RS pSuc_neq_one);
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   146
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   147
(** Injectiveness of pSuc **)
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   148
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   149
Goalw [pnat_Suc_def] "inj(pSuc)";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   150
by (rtac injI 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   151
by (dtac (inj_on_Abs_pnat RS inj_onD) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   152
by (REPEAT (resolve_tac [Rep_pnat, pnat_Suc_RepI] 1));
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   153
by (dtac (inj_Suc RS injD) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   154
by (etac (inj_Rep_pnat RS injD) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   155
qed "inj_pSuc"; 
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   156
9108
9fff97d29837 bind_thm(s);
wenzelm
parents: 9043
diff changeset
   157
bind_thm ("pSuc_inject", inj_pSuc RS injD);
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   158
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   159
Goal "(pSuc(m)=pSuc(n)) = (m=n)";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   160
by (EVERY1 [rtac iffI, etac pSuc_inject, etac arg_cong]); 
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   161
qed "pSuc_pSuc_eq";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   162
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   163
AddIffs [pSuc_pSuc_eq];
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   164
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   165
Goal "n ~= pSuc(n)";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   166
by (pnat_ind_tac "n" 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   167
by (ALLGOALS Asm_simp_tac);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   168
qed "n_not_pSuc_n";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   169
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   170
bind_thm ("pSuc_n_not_n", n_not_pSuc_n RS not_sym);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   171
12018
ec054019c910 Numerals and simprocs for types real and hypreal. The abstract
paulson
parents: 11701
diff changeset
   172
Goal "n ~= 1 ==> EX m. n = pSuc m";
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   173
by (rtac pnatE 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   174
by (REPEAT (Blast_tac 1));
12018
ec054019c910 Numerals and simprocs for types real and hypreal. The abstract
paulson
parents: 11701
diff changeset
   175
qed "not1_implies_pSuc";
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   176
12018
ec054019c910 Numerals and simprocs for types real and hypreal. The abstract
paulson
parents: 11701
diff changeset
   177
Goal "pSuc m = m + 1";
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   178
by (auto_tac (claset(),simpset() addsimps [pnat_Suc_def,
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   179
    pnat_one_def,Abs_pnat_inverse,pnat_add_def]));
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   180
qed "pSuc_is_plus_one";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   181
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   182
Goal
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   183
      "(Rep_pnat x + Rep_pnat y): pnat";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   184
by (cut_facts_tac [[Rep_pnat_gt_zero,
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   185
    Rep_pnat_gt_zero] MRS add_less_mono,Collect_pnat_gt_0] 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   186
by (etac ssubst 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   187
by Auto_tac;
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   188
qed "sum_Rep_pnat";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   189
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   190
Goalw [pnat_add_def] 
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   191
      "Rep_pnat x + Rep_pnat y = Rep_pnat (x + y)";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   192
by (simp_tac (simpset() addsimps [sum_Rep_pnat RS 
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   193
                          Abs_pnat_inverse]) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   194
qed "sum_Rep_pnat_sum";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   195
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   196
Goalw [pnat_add_def] 
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   197
      "(x + y) + z = x + (y + (z::pnat))";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   198
by (res_inst_tac [("f","Abs_pnat")] arg_cong 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   199
by (simp_tac (simpset() addsimps [sum_Rep_pnat RS 
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   200
                Abs_pnat_inverse,add_assoc]) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   201
qed "pnat_add_assoc";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   202
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   203
Goalw [pnat_add_def] "x + (y + z) = y + (x + (z::pnat))";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   204
by (res_inst_tac [("f","Abs_pnat")] arg_cong 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   205
by (simp_tac (simpset() addsimps [sum_Rep_pnat RS 
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   206
          Abs_pnat_inverse,add_left_commute]) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   207
qed "pnat_add_left_commute";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   208
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   209
(*Addition is an AC-operator*)
9108
9fff97d29837 bind_thm(s);
wenzelm
parents: 9043
diff changeset
   210
bind_thms ("pnat_add_ac", [pnat_add_assoc, pnat_add_commute, pnat_add_left_commute]);
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   211
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   212
Goalw [pnat_add_def] "((x::pnat) + y = x + z) = (y = z)";
8866
paulson
parents: 8856
diff changeset
   213
by (auto_tac (claset() addDs [inj_on_Abs_pnat RS inj_onD,
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   214
     inj_Rep_pnat RS injD],simpset() addsimps [sum_Rep_pnat]));
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   215
qed "pnat_add_left_cancel";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   216
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   217
Goalw [pnat_add_def] "(y + (x::pnat) = z + x) = (y = z)";
8866
paulson
parents: 8856
diff changeset
   218
by (auto_tac (claset() addDs [inj_on_Abs_pnat RS inj_onD,
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   219
     inj_Rep_pnat RS injD],simpset() addsimps [sum_Rep_pnat]));
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   220
qed "pnat_add_right_cancel";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   221
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   222
Goalw [pnat_add_def] "!(y::pnat). x + y ~= x";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   223
by (rtac (Rep_pnat_inverse RS subst) 1);
8866
paulson
parents: 8856
diff changeset
   224
by (auto_tac (claset() addDs [inj_on_Abs_pnat RS inj_onD] 
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   225
  	               addSDs [add_eq_self_zero],
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   226
	      simpset() addsimps [sum_Rep_pnat, Rep_pnat,Abs_pnat_inverse,
8866
paulson
parents: 8856
diff changeset
   227
				  Rep_pnat_gt_zero RS less_not_refl2]));
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   228
qed "pnat_no_add_ident";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   229
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   230
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   231
(***) (***) (***) (***) (***) (***) (***) (***) (***)
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   232
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   233
  (*** pnat_less ***)
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   234
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5078
diff changeset
   235
Goalw [pnat_less_def] "~ y < (y::pnat)";
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   236
by Auto_tac;
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   237
qed "pnat_less_not_refl";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   238
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   239
bind_thm ("pnat_less_irrefl",pnat_less_not_refl RS notE);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   240
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   241
Goalw [pnat_less_def] 
5148
74919e8f221c More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5143
diff changeset
   242
     "x < (y::pnat) ==> x ~= y";
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   243
by Auto_tac;
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   244
qed "pnat_less_not_refl2";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   245
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   246
Goal "~ Rep_pnat y < 0";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   247
by Auto_tac;
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   248
qed "Rep_pnat_not_less0";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   249
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   250
(*** Rep_pnat < 0 ==> P ***)
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   251
bind_thm ("Rep_pnat_less_zeroE",Rep_pnat_not_less0 RS notE);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   252
11701
3d51fbf81c17 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents: 11655
diff changeset
   253
Goal "~ Rep_pnat y < Suc 0";
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   254
by (auto_tac (claset(),simpset() addsimps [less_Suc_eq,
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   255
                  Rep_pnat_gt_zero,less_not_refl2]));
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   256
qed "Rep_pnat_not_less_one";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   257
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   258
(*** Rep_pnat < 1 ==> P ***)
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   259
bind_thm ("Rep_pnat_less_oneE",Rep_pnat_not_less_one RS notE);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   260
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   261
Goalw [pnat_less_def] 
11701
3d51fbf81c17 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents: 11655
diff changeset
   262
     "x < (y::pnat) ==> Rep_pnat y ~= Suc 0";
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   263
by (auto_tac (claset(),simpset() 
12842
32c9c881dec8 delsimps [less_Suc0];
wenzelm
parents: 12018
diff changeset
   264
    addsimps [Rep_pnat_not_less_one] delsimps [less_Suc0]));
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   265
qed "Rep_pnat_gt_implies_not0";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   266
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   267
Goalw [pnat_less_def] 
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   268
      "(x::pnat) < y | x = y | y < x";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   269
by (cut_facts_tac [less_linear] 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   270
by (fast_tac (claset() addIs [inj_Rep_pnat RS injD]) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   271
qed "pnat_less_linear";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   272
11701
3d51fbf81c17 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents: 11655
diff changeset
   273
Goalw [le_def] "Suc 0 <= Rep_pnat x";
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   274
by (rtac Rep_pnat_not_less_one 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   275
qed "Rep_pnat_le_one";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   276
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   277
Goalw [pnat_less_def]
9043
ca761fe227d8 First round of changes, towards installation of simprocs
paulson
parents: 8866
diff changeset
   278
     "!! (z1::nat). z1 < z2  ==> EX z3. z1 + Rep_pnat z3 = z2";
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   279
by (dtac less_imp_add_positive 1);
5758
27a2b36efd95 corrected auto_tac (applications of unsafe wrappers)
oheimb
parents: 5588
diff changeset
   280
by (force_tac (claset() addSIs [Abs_pnat_inverse],
27a2b36efd95 corrected auto_tac (applications of unsafe wrappers)
oheimb
parents: 5588
diff changeset
   281
	       simpset() addsimps [Collect_pnat_gt_0]) 1);
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   282
qed "lemma_less_ex_sum_Rep_pnat";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   283
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   284
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   285
   (*** pnat_le ***)
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   286
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   287
(*** alternative definition for pnat_le ***)
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   288
Goalw [pnat_le_def,pnat_less_def] 
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   289
      "((m::pnat) <= n) = (Rep_pnat m <= Rep_pnat n)";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   290
by (auto_tac (claset() addSIs [leI] addSEs [leD],simpset()));
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   291
qed "pnat_le_iff_Rep_pnat_le";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   292
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   293
Goal "!!k::pnat. (k + m <= k + n) = (m<=n)";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   294
by (simp_tac (simpset() addsimps [pnat_le_iff_Rep_pnat_le,
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   295
                           sum_Rep_pnat_sum RS sym]) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   296
qed "pnat_add_left_cancel_le";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   297
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   298
Goalw [pnat_less_def] "!!k::pnat. (k + m < k + n) = (m<n)";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   299
by (simp_tac (simpset() addsimps [sum_Rep_pnat_sum RS sym]) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   300
qed "pnat_add_left_cancel_less";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   301
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   302
Addsimps [pnat_add_left_cancel, pnat_add_right_cancel,
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   303
  pnat_add_left_cancel_le, pnat_add_left_cancel_less];
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   304
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5078
diff changeset
   305
Goalw [pnat_less_def] "i+j < (k::pnat) ==> i<k";
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   306
by (auto_tac (claset() addEs [add_lessD1],
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   307
    simpset() addsimps [sum_Rep_pnat_sum RS sym]));
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   308
qed "pnat_add_lessD1";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   309
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   310
Goal "!!i::pnat. ~ (i+j < i)";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   311
by (rtac  notI 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   312
by (etac (pnat_add_lessD1 RS pnat_less_irrefl) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   313
qed "pnat_not_add_less1";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   314
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   315
Goal "!!i::pnat. ~ (j+i < i)";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   316
by (simp_tac (simpset() addsimps [pnat_add_commute, pnat_not_add_less1]) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   317
qed "pnat_not_add_less2";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   318
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   319
AddIffs [pnat_not_add_less1, pnat_not_add_less2];
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   320
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   321
Goal "m + k <= n --> m <= (n::pnat)";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   322
by (simp_tac (simpset() addsimps [pnat_le_iff_Rep_pnat_le,
10752
c4f1bf2acf4c tidying, and separation of HOL-Hyperreal from HOL-Real
paulson
parents: 10292
diff changeset
   323
                                  sum_Rep_pnat_sum RS sym]) 1);
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   324
qed_spec_mp "pnat_add_leD1";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   325
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   326
Goal "!!n::pnat. m + k <= n ==> k <= n";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   327
by (full_simp_tac (simpset() addsimps [pnat_add_commute]) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   328
by (etac pnat_add_leD1 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   329
qed_spec_mp "pnat_add_leD2";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   330
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   331
Goal "!!n::pnat. m + k <= n ==> m <= n & k <= n";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   332
by (blast_tac (claset() addDs [pnat_add_leD1, pnat_add_leD2]) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   333
bind_thm ("pnat_add_leE", result() RS conjE);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   334
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   335
Goalw [pnat_less_def] 
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   336
      "!!k l::pnat. [| k < l; m + l = k + n |] ==> m < n";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   337
by (rtac less_add_eq_less 1 THEN assume_tac 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   338
by (auto_tac (claset(),simpset() addsimps [sum_Rep_pnat_sum]));
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   339
qed "pnat_less_add_eq_less";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   340
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   341
(* ordering on positive naturals in terms of existence of sum *)
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   342
(* could provide alternative definition -- Gleason *)
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   343
Goalw [pnat_less_def,pnat_add_def] 
11655
923e4d0d36d5 tuned parentheses in relational expressions;
wenzelm
parents: 11464
diff changeset
   344
      "((z1::pnat) < z2) = (EX z3. z1 + z3 = z2)";
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   345
by (rtac iffI 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   346
by (res_inst_tac [("t","z2")] (Rep_pnat_inverse RS subst) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   347
by (dtac lemma_less_ex_sum_Rep_pnat 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   348
by (etac exE 1 THEN res_inst_tac [("x","z3")] exI 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   349
by (auto_tac (claset(),simpset() addsimps [sum_Rep_pnat_sum,Rep_pnat_inverse]));
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   350
by (res_inst_tac [("t","Rep_pnat z1")] (add_0_right RS subst) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   351
by (auto_tac (claset(),simpset() addsimps [sum_Rep_pnat_sum RS sym,
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   352
               Rep_pnat_gt_zero] delsimps [add_0_right]));
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   353
qed "pnat_less_iff";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   354
9043
ca761fe227d8 First round of changes, towards installation of simprocs
paulson
parents: 8866
diff changeset
   355
Goal "(EX (x::pnat). z1 + x = z2) | z1 = z2 \
ca761fe227d8 First round of changes, towards installation of simprocs
paulson
parents: 8866
diff changeset
   356
\          |(EX x. z2 + x = z1)";
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   357
by (cut_facts_tac [pnat_less_linear] 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   358
by (asm_full_simp_tac (simpset() addsimps [pnat_less_iff]) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   359
qed "pnat_linear_Ex_eq";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   360
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   361
Goal "!!(x::pnat). x + y = z ==> x < z";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   362
by (rtac (pnat_less_iff RS iffD2) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   363
by (Blast_tac 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   364
qed "pnat_eq_lessI";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   365
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   366
(*** Monotonicity of Addition ***)
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   367
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   368
Goal "1 * Rep_pnat n = Rep_pnat n";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   369
by (Asm_simp_tac 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   370
qed "Rep_pnat_mult_1";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   371
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   372
Goal "Rep_pnat n * 1 = Rep_pnat n";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   373
by (Asm_simp_tac 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   374
qed "Rep_pnat_mult_1_right";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   375
10752
c4f1bf2acf4c tidying, and separation of HOL-Hyperreal from HOL-Real
paulson
parents: 10292
diff changeset
   376
Goal "(Rep_pnat x * Rep_pnat y): pnat";
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   377
by (cut_facts_tac [[Rep_pnat_gt_zero,
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   378
    Rep_pnat_gt_zero] MRS mult_less_mono1,Collect_pnat_gt_0] 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   379
by (etac ssubst 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   380
by Auto_tac;
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   381
qed "mult_Rep_pnat";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   382
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   383
Goalw [pnat_mult_def] 
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   384
      "Rep_pnat x * Rep_pnat y = Rep_pnat (x * y)";
10752
c4f1bf2acf4c tidying, and separation of HOL-Hyperreal from HOL-Real
paulson
parents: 10292
diff changeset
   385
by (simp_tac (simpset() addsimps [mult_Rep_pnat RS Abs_pnat_inverse]) 1);
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   386
qed "mult_Rep_pnat_mult";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   387
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   388
Goalw [pnat_mult_def] "m * n = n * (m::pnat)";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   389
by (full_simp_tac (simpset() addsimps [mult_commute]) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   390
qed "pnat_mult_commute";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   391
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   392
Goalw [pnat_mult_def,pnat_add_def] "(m + n)*k = (m*k) + ((n*k)::pnat)";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   393
by (res_inst_tac [("f","Abs_pnat")] arg_cong 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   394
by (simp_tac (simpset() addsimps [mult_Rep_pnat RS 
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   395
                Abs_pnat_inverse,sum_Rep_pnat RS 
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   396
             Abs_pnat_inverse, add_mult_distrib]) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   397
qed "pnat_add_mult_distrib";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   398
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   399
Goalw [pnat_mult_def,pnat_add_def] "k*(m + n) = (k*m) + ((k*n)::pnat)";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   400
by (res_inst_tac [("f","Abs_pnat")] arg_cong 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   401
by (simp_tac (simpset() addsimps [mult_Rep_pnat RS 
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   402
                Abs_pnat_inverse,sum_Rep_pnat RS 
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   403
             Abs_pnat_inverse, add_mult_distrib2]) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   404
qed "pnat_add_mult_distrib2";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   405
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   406
Goalw [pnat_mult_def] 
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   407
      "(x * y) * z = x * (y * (z::pnat))";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   408
by (res_inst_tac [("f","Abs_pnat")] arg_cong 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   409
by (simp_tac (simpset() addsimps [mult_Rep_pnat RS 
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   410
                Abs_pnat_inverse,mult_assoc]) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   411
qed "pnat_mult_assoc";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   412
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   413
Goalw [pnat_mult_def] "x * (y * z) = y * (x * (z::pnat))";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   414
by (res_inst_tac [("f","Abs_pnat")] arg_cong 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   415
by (simp_tac (simpset() addsimps [mult_Rep_pnat RS 
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   416
          Abs_pnat_inverse,mult_left_commute]) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   417
qed "pnat_mult_left_commute";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   418
11701
3d51fbf81c17 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents: 11655
diff changeset
   419
Goalw [pnat_mult_def] "x * (Abs_pnat (Suc 0)) = x";
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   420
by (full_simp_tac (simpset() addsimps [one_RepI RS Abs_pnat_inverse,
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   421
                   Rep_pnat_inverse]) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   422
qed "pnat_mult_1";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   423
11701
3d51fbf81c17 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents: 11655
diff changeset
   424
Goal "Abs_pnat (Suc 0) * x = x";
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   425
by (full_simp_tac (simpset() addsimps [pnat_mult_1,
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   426
                   pnat_mult_commute]) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   427
qed "pnat_mult_1_left";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   428
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   429
(*Multiplication is an AC-operator*)
9635
c9ebf0a1d712 tidied & updated proofs, deleting some unused ones
paulson
parents: 9422
diff changeset
   430
bind_thms ("pnat_mult_ac", 
c9ebf0a1d712 tidied & updated proofs, deleting some unused ones
paulson
parents: 9422
diff changeset
   431
	   [pnat_mult_assoc, pnat_mult_commute, pnat_mult_left_commute]);
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   432
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   433
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   434
Goal "!!i::pnat. i<j ==> k*i < k*j";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   435
by (asm_full_simp_tac (simpset() addsimps [pnat_less_def,
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   436
    mult_Rep_pnat_mult RS sym,Rep_pnat_gt_zero,mult_less_mono2]) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   437
qed "pnat_mult_less_mono2";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   438
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   439
Goal "!!i::pnat. i<j ==> i*k < j*k";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   440
by (dtac pnat_mult_less_mono2 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   441
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [pnat_mult_commute])));
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   442
qed "pnat_mult_less_mono1";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   443
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   444
Goalw [pnat_less_def] "(m*(k::pnat) < n*k) = (m<n)";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   445
by (asm_full_simp_tac (simpset() addsimps [mult_Rep_pnat_mult 
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   446
              RS sym,Rep_pnat_gt_zero]) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   447
qed "pnat_mult_less_cancel2";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   448
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   449
Goalw [pnat_less_def] "((k::pnat)*m < k*n) = (m<n)";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   450
by (asm_full_simp_tac (simpset() addsimps [mult_Rep_pnat_mult 
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   451
              RS sym,Rep_pnat_gt_zero]) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   452
qed "pnat_mult_less_cancel1";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   453
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   454
Addsimps [pnat_mult_less_cancel1, pnat_mult_less_cancel2];
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   455
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   456
Goalw [pnat_mult_def]  "(m*(k::pnat) = n*k) = (m=n)";
9635
c9ebf0a1d712 tidied & updated proofs, deleting some unused ones
paulson
parents: 9422
diff changeset
   457
by (cut_inst_tac [("x","k")] Rep_pnat_gt_zero 1);
c9ebf0a1d712 tidied & updated proofs, deleting some unused ones
paulson
parents: 9422
diff changeset
   458
by (auto_tac (claset() addSDs [inj_on_Abs_pnat RS inj_onD,
c9ebf0a1d712 tidied & updated proofs, deleting some unused ones
paulson
parents: 9422
diff changeset
   459
                               inj_Rep_pnat RS injD] 
c9ebf0a1d712 tidied & updated proofs, deleting some unused ones
paulson
parents: 9422
diff changeset
   460
                       addIs [mult_Rep_pnat], 
c9ebf0a1d712 tidied & updated proofs, deleting some unused ones
paulson
parents: 9422
diff changeset
   461
    simpset() addsimps [mult_cancel2]));
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   462
qed "pnat_mult_cancel2";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   463
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   464
Goal "((k::pnat)*m = k*n) = (m=n)";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   465
by (rtac (pnat_mult_cancel2 RS subst) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   466
by (auto_tac (claset () addIs [pnat_mult_commute RS subst],simpset()));
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   467
qed "pnat_mult_cancel1";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   468
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   469
Addsimps [pnat_mult_cancel1, pnat_mult_cancel2];
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   470
9635
c9ebf0a1d712 tidied & updated proofs, deleting some unused ones
paulson
parents: 9422
diff changeset
   471
Goal "!!(z1::pnat). z2*z3 = z4*z5  ==> z2*(z1*z3) = z4*(z1*z5)";
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   472
by (auto_tac (claset() addIs [pnat_mult_cancel1 RS iffD2],
9635
c9ebf0a1d712 tidied & updated proofs, deleting some unused ones
paulson
parents: 9422
diff changeset
   473
              simpset() addsimps [pnat_mult_left_commute]));
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   474
qed "pnat_same_multI2";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   475
9635
c9ebf0a1d712 tidied & updated proofs, deleting some unused ones
paulson
parents: 9422
diff changeset
   476
val [prem] = Goal
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   477
    "(!!u. z = Abs_pnat(u) ==> P) ==> P";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   478
by (cut_inst_tac [("x1","z")] 
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   479
    (rewrite_rule [pnat_def] (Rep_pnat RS Abs_pnat_inverse)) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   480
by (res_inst_tac [("u","Rep_pnat z")] prem 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   481
by (dtac (inj_Rep_pnat RS injD) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   482
by (Asm_simp_tac 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   483
qed "eq_Abs_pnat";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   484
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   485
(** embedding of naturals in positive naturals **)
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   486
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   487
(* pnat_one_eq! *)
12018
ec054019c910 Numerals and simprocs for types real and hypreal. The abstract
paulson
parents: 11701
diff changeset
   488
Goalw [pnat_of_nat_def,pnat_one_def]"1 = pnat_of_nat 0";
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   489
by (Full_simp_tac 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   490
qed "pnat_one_iff";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   491
7077
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names;
paulson
parents: 6073
diff changeset
   492
Goalw [pnat_of_nat_def,pnat_one_def,
12018
ec054019c910 Numerals and simprocs for types real and hypreal. The abstract
paulson
parents: 11701
diff changeset
   493
       pnat_add_def] "1 + 1 = pnat_of_nat 1";
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   494
by (res_inst_tac [("f","Abs_pnat")] arg_cong 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   495
by (auto_tac (claset() addIs [(gt_0_mem_pnat RS Abs_pnat_inverse RS ssubst)],
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   496
    simpset()));
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   497
qed "pnat_two_eq";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   498
7077
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names;
paulson
parents: 6073
diff changeset
   499
Goal "inj(pnat_of_nat)";
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   500
by (rtac injI 1);
7077
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names;
paulson
parents: 6073
diff changeset
   501
by (rewtac pnat_of_nat_def);
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   502
by (dtac (inj_on_Abs_pnat RS inj_onD) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   503
by (auto_tac (claset() addSIs [gt_0_mem_pnat],simpset()));
7077
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names;
paulson
parents: 6073
diff changeset
   504
qed "inj_pnat_of_nat";
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   505
11701
3d51fbf81c17 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents: 11655
diff changeset
   506
Goal "0 < n + (1::nat)";
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   507
by Auto_tac;
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   508
qed "nat_add_one_less";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   509
11701
3d51fbf81c17 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents: 11655
diff changeset
   510
Goal "0 < n1 + n2 + (1::nat)";
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   511
by Auto_tac;
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   512
qed "nat_add_one_less1";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   513
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   514
(* this worked with one call to auto_tac before! *)
7077
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names;
paulson
parents: 6073
diff changeset
   515
Goalw [pnat_add_def,pnat_of_nat_def,pnat_one_def] 
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names;
paulson
parents: 6073
diff changeset
   516
      "pnat_of_nat n1 + pnat_of_nat n2 = \
12018
ec054019c910 Numerals and simprocs for types real and hypreal. The abstract
paulson
parents: 11701
diff changeset
   517
\      pnat_of_nat (n1 + n2) + 1";
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   518
by (res_inst_tac [("f","Abs_pnat")] arg_cong 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   519
by (rtac (gt_0_mem_pnat RS Abs_pnat_inverse RS ssubst) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   520
by (rtac (gt_0_mem_pnat RS Abs_pnat_inverse RS ssubst) 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   521
by (rtac (gt_0_mem_pnat RS Abs_pnat_inverse RS ssubst) 3);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   522
by (rtac (gt_0_mem_pnat RS Abs_pnat_inverse RS ssubst) 4);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   523
by (auto_tac (claset(),
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   524
	      simpset() addsimps [sum_Rep_pnat_sum,
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   525
				  nat_add_one_less,nat_add_one_less1]));
7077
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names;
paulson
parents: 6073
diff changeset
   526
qed "pnat_of_nat_add";
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   527
7077
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names;
paulson
parents: 6073
diff changeset
   528
Goalw [pnat_of_nat_def,pnat_less_def] 
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names;
paulson
parents: 6073
diff changeset
   529
       "(n < m) = (pnat_of_nat n < pnat_of_nat m)";
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   530
by (auto_tac (claset(),simpset() 
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   531
    addsimps [Abs_pnat_inverse,Collect_pnat_gt_0]));
7077
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names;
paulson
parents: 6073
diff changeset
   532
qed "pnat_of_nat_less_iff";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names;
paulson
parents: 6073
diff changeset
   533
Addsimps [pnat_of_nat_less_iff RS sym];
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   534
9422
4b6bc2b347e5 avoid referencing thy value;
wenzelm
parents: 9108
diff changeset
   535
Goalw [pnat_mult_def,pnat_of_nat_def] 
7292
dff3470c5c62 real literals using binary arithmetic
paulson
parents: 7219
diff changeset
   536
      "pnat_of_nat n1 * pnat_of_nat n2 = \
dff3470c5c62 real literals using binary arithmetic
paulson
parents: 7219
diff changeset
   537
\      pnat_of_nat (n1 * n2 + n1 + n2)";
dff3470c5c62 real literals using binary arithmetic
paulson
parents: 7219
diff changeset
   538
by (auto_tac (claset(),simpset() addsimps [mult_Rep_pnat_mult,
dff3470c5c62 real literals using binary arithmetic
paulson
parents: 7219
diff changeset
   539
    pnat_add_def,Abs_pnat_inverse,gt_0_mem_pnat]));
dff3470c5c62 real literals using binary arithmetic
paulson
parents: 7219
diff changeset
   540
qed "pnat_of_nat_mult";