src/HOL/Real/PRat.ML
author wenzelm
Thu Jun 22 23:04:34 2000 +0200 (2000-06-22)
changeset 9108 9fff97d29837
parent 9043 ca761fe227d8
child 9369 139fde7af7bd
permissions -rw-r--r--
bind_thm(s);
paulson@5078
     1
(*  Title       : PRat.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 rationals
paulson@5078
     6
*) 
paulson@5078
     7
paulson@5078
     8
Delrules [equalityI];
paulson@5078
     9
paulson@5078
    10
(*** Many theorems similar to those in Integ.thy ***)
paulson@5078
    11
(*** Proving that ratrel is an equivalence relation ***)
paulson@5078
    12
paulson@7219
    13
Goal "[| (x1::pnat) * y2 = x2 * y1; x2 * y3 = x3 * y2 |] \
paulson@5078
    14
\            ==> x1 * y3 = x3 * y1";        
paulson@5078
    15
by (res_inst_tac [("k1","y2")] (pnat_mult_cancel1 RS iffD1) 1);
paulson@5078
    16
by (auto_tac (claset(), simpset() addsimps [pnat_mult_assoc RS sym]));
paulson@5078
    17
by (auto_tac (claset(),simpset() addsimps [pnat_mult_commute]));
paulson@5078
    18
by (dres_inst_tac [("s","x2 * y3")] sym 1);
paulson@5078
    19
by (asm_simp_tac (simpset() addsimps [pnat_mult_left_commute,
paulson@5078
    20
    pnat_mult_commute]) 1);
paulson@5078
    21
qed "prat_trans_lemma";
paulson@5078
    22
paulson@5078
    23
(** Natural deduction for ratrel **)
paulson@5078
    24
paulson@5078
    25
Goalw [ratrel_def]
paulson@5078
    26
    "(((x1,y1),(x2,y2)): ratrel) = (x1 * y2 = x2 * y1)";
paulson@5078
    27
by (Fast_tac 1);
paulson@5078
    28
qed "ratrel_iff";
paulson@5078
    29
paulson@5078
    30
Goalw [ratrel_def]
paulson@5148
    31
    "[| x1 * y2 = x2 * y1 |] ==> ((x1,y1),(x2,y2)): ratrel";
paulson@5078
    32
by (Fast_tac  1);
paulson@5078
    33
qed "ratrelI";
paulson@5078
    34
paulson@5078
    35
Goalw [ratrel_def]
paulson@5078
    36
  "p: ratrel --> (EX x1 y1 x2 y2. \
paulson@5078
    37
\                  p = ((x1,y1),(x2,y2)) & x1 *y2 = x2 *y1)";
paulson@5078
    38
by (Fast_tac 1);
paulson@5078
    39
qed "ratrelE_lemma";
paulson@5078
    40
paulson@5078
    41
val [major,minor] = goal thy
paulson@5078
    42
  "[| p: ratrel;  \
paulson@5078
    43
\     !!x1 y1 x2 y2. [| p = ((x1,y1),(x2,y2));  x1*y2 = x2*y1 \
paulson@5078
    44
\                    |] ==> Q |] ==> Q";
paulson@5078
    45
by (cut_facts_tac [major RS (ratrelE_lemma RS mp)] 1);
paulson@5078
    46
by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1));
paulson@5078
    47
qed "ratrelE";
paulson@5078
    48
paulson@5078
    49
AddSIs [ratrelI];
paulson@5078
    50
AddSEs [ratrelE];
paulson@5078
    51
paulson@5078
    52
Goal "(x,x): ratrel";
paulson@5078
    53
by (stac surjective_pairing 1 THEN rtac (refl RS ratrelI) 1);
paulson@5078
    54
qed "ratrel_refl";
paulson@5078
    55
paulson@5078
    56
Goalw [equiv_def, refl_def, sym_def, trans_def]
paulson@7376
    57
    "equiv UNIV ratrel";
paulson@5078
    58
by (fast_tac (claset() addSIs [ratrel_refl] 
paulson@7376
    59
                       addSEs [sym, prat_trans_lemma]) 1);
paulson@5078
    60
qed "equiv_ratrel";
paulson@5078
    61
wenzelm@9108
    62
bind_thm ("equiv_ratrel_iff", [equiv_ratrel, UNIV_I, UNIV_I] MRS eq_equiv_class_iff);
paulson@5078
    63
paulson@5078
    64
Goalw  [prat_def,ratrel_def,quotient_def] "ratrel^^{(x,y)}:prat";
paulson@5078
    65
by (Blast_tac 1);
paulson@5078
    66
qed "ratrel_in_prat";
paulson@5078
    67
paulson@5078
    68
Goal "inj_on Abs_prat prat";
paulson@5078
    69
by (rtac inj_on_inverseI 1);
paulson@5078
    70
by (etac Abs_prat_inverse 1);
paulson@5078
    71
qed "inj_on_Abs_prat";
paulson@5078
    72
paulson@5078
    73
Addsimps [equiv_ratrel_iff,inj_on_Abs_prat RS inj_on_iff,
paulson@5078
    74
          ratrel_iff, ratrel_in_prat, Abs_prat_inverse];
paulson@5078
    75
paulson@5078
    76
Addsimps [equiv_ratrel RS eq_equiv_class_iff];
wenzelm@9108
    77
bind_thm ("eq_ratrelD", equiv_ratrel RSN (2,eq_equiv_class));
paulson@5078
    78
paulson@5078
    79
Goal "inj(Rep_prat)";
paulson@5078
    80
by (rtac inj_inverseI 1);
paulson@5078
    81
by (rtac Rep_prat_inverse 1);
paulson@5078
    82
qed "inj_Rep_prat";
paulson@5078
    83
paulson@7077
    84
(** prat_of_pnat: the injection from pnat to prat **)
paulson@7077
    85
Goal "inj(prat_of_pnat)";
paulson@5078
    86
by (rtac injI 1);
paulson@7077
    87
by (rewtac prat_of_pnat_def);
paulson@5078
    88
by (dtac (inj_on_Abs_prat RS inj_onD) 1);
paulson@5078
    89
by (REPEAT (rtac ratrel_in_prat 1));
paulson@5078
    90
by (dtac eq_equiv_class 1);
paulson@5078
    91
by (rtac equiv_ratrel 1);
paulson@5078
    92
by (Fast_tac 1);
paulson@5078
    93
by Safe_tac;
paulson@5078
    94
by (Asm_full_simp_tac 1);
paulson@7077
    95
qed "inj_prat_of_pnat";
paulson@5078
    96
paulson@5078
    97
val [prem] = goal thy
paulson@5078
    98
    "(!!x y. z = Abs_prat(ratrel^^{(x,y)}) ==> P) ==> P";
paulson@5078
    99
by (res_inst_tac [("x1","z")] 
paulson@5078
   100
    (rewrite_rule [prat_def] Rep_prat RS quotientE) 1);
paulson@5078
   101
by (dres_inst_tac [("f","Abs_prat")] arg_cong 1);
paulson@5078
   102
by (res_inst_tac [("p","x")] PairE 1);
paulson@5078
   103
by (rtac prem 1);
paulson@5078
   104
by (asm_full_simp_tac (simpset() addsimps [Rep_prat_inverse]) 1);
paulson@5078
   105
qed "eq_Abs_prat";
paulson@5078
   106
paulson@5078
   107
(**** qinv: inverse on prat ****)
paulson@5078
   108
paulson@7376
   109
Goalw [congruent_def] "congruent ratrel (%(x,y). ratrel^^{(y,x)})";
paulson@5078
   110
by Safe_tac;
paulson@5078
   111
by (asm_full_simp_tac (simpset() addsimps [pnat_mult_commute]) 1);
paulson@5078
   112
qed "qinv_congruent";
paulson@5078
   113
paulson@5078
   114
Goalw [qinv_def]
paulson@5078
   115
      "qinv (Abs_prat(ratrel^^{(x,y)})) = Abs_prat(ratrel ^^ {(y,x)})";
paulson@5078
   116
by (simp_tac (simpset() addsimps 
paulson@7376
   117
	      [equiv_ratrel RS UN_equiv_class, qinv_congruent]) 1);
paulson@5078
   118
qed "qinv";
paulson@5078
   119
paulson@5078
   120
Goal "qinv (qinv z) = z";
paulson@5078
   121
by (res_inst_tac [("z","z")] eq_Abs_prat 1);
paulson@5078
   122
by (asm_simp_tac (simpset() addsimps [qinv]) 1);
paulson@5078
   123
qed "qinv_qinv";
paulson@5078
   124
paulson@5078
   125
Goal "inj(qinv)";
paulson@5078
   126
by (rtac injI 1);
paulson@5078
   127
by (dres_inst_tac [("f","qinv")] arg_cong 1);
paulson@5078
   128
by (asm_full_simp_tac (simpset() addsimps [qinv_qinv]) 1);
paulson@5078
   129
qed "inj_qinv";
paulson@5078
   130
paulson@7077
   131
Goalw [prat_of_pnat_def] 
paulson@7077
   132
      "qinv(prat_of_pnat  (Abs_pnat 1)) = prat_of_pnat (Abs_pnat 1)";
paulson@5078
   133
by (simp_tac (simpset() addsimps [qinv]) 1);
paulson@5078
   134
qed "qinv_1";
paulson@5078
   135
paulson@5148
   136
Goal "!!(x1::pnat). [| x1 * y2 = x2 * y1 |] ==> \
paulson@5078
   137
\     (x * y1 + x1 * ya) * (ya * y2) = (x * y2 + x2 * ya) * (ya * y1)";
paulson@5078
   138
by (auto_tac (claset() addSIs [pnat_same_multI2],
paulson@5078
   139
       simpset() addsimps [pnat_add_mult_distrib,
paulson@5078
   140
       pnat_mult_assoc]));
paulson@5078
   141
by (res_inst_tac [("n1","y2")] (pnat_mult_commute RS subst) 1);
paulson@5078
   142
by (auto_tac (claset() addIs [pnat_add_left_cancel RS iffD2],simpset() addsimps pnat_mult_ac));
paulson@5078
   143
by (res_inst_tac [("y1","x1")] (pnat_mult_left_commute RS subst) 1);
paulson@5078
   144
by (res_inst_tac [("y1","x1")] (pnat_mult_left_commute RS ssubst) 1);
paulson@5078
   145
by (auto_tac (claset(),simpset() addsimps [pnat_mult_assoc RS sym]));
paulson@5078
   146
qed "prat_add_congruent2_lemma";
paulson@5078
   147
paulson@7219
   148
Goal "congruent2 ratrel (%p1 p2.                  \
paulson@7376
   149
\        (%(x1,y1). (%(x2,y2). ratrel^^{(x1*y2 + x2*y1, y1*y2)}) p2) p1)";
paulson@5078
   150
by (rtac (equiv_ratrel RS congruent2_commuteI) 1);
paulson@7376
   151
by (auto_tac (claset(),simpset() addsimps [prat_add_congruent2_lemma]));
paulson@5078
   152
by (asm_simp_tac (simpset() addsimps [pnat_mult_commute,pnat_add_commute]) 1);
paulson@5078
   153
qed "prat_add_congruent2";
paulson@5078
   154
paulson@5078
   155
Goalw [prat_add_def]
paulson@5078
   156
   "Abs_prat((ratrel^^{(x1,y1)})) + Abs_prat((ratrel^^{(x2,y2)})) =   \
paulson@5078
   157
\   Abs_prat(ratrel ^^ {(x1*y2 + x2*y1, y1*y2)})";
paulson@7376
   158
by (simp_tac (simpset() addsimps [UN_UN_split_split_eq, prat_add_congruent2, 
paulson@7376
   159
				  equiv_ratrel RS UN_equiv_class2]) 1);
paulson@5078
   160
qed "prat_add";
paulson@5078
   161
paulson@5078
   162
Goal "(z::prat) + w = w + z";
paulson@5078
   163
by (res_inst_tac [("z","z")] eq_Abs_prat 1);
paulson@5078
   164
by (res_inst_tac [("z","w")] eq_Abs_prat 1);
paulson@5535
   165
by (asm_simp_tac
paulson@5535
   166
    (simpset() addsimps [prat_add] @ pnat_add_ac @ pnat_mult_ac) 1);
paulson@5078
   167
qed "prat_add_commute";
paulson@5078
   168
paulson@5078
   169
Goal "((z1::prat) + z2) + z3 = z1 + (z2 + z3)";
paulson@5078
   170
by (res_inst_tac [("z","z1")] eq_Abs_prat 1);
paulson@5078
   171
by (res_inst_tac [("z","z2")] eq_Abs_prat 1);
paulson@5078
   172
by (res_inst_tac [("z","z3")] eq_Abs_prat 1);
paulson@5535
   173
by (asm_simp_tac (simpset() addsimps [pnat_add_mult_distrib2,prat_add] @ 
paulson@7376
   174
		                     pnat_add_ac @ pnat_mult_ac) 1);
paulson@5078
   175
qed "prat_add_assoc";
paulson@5078
   176
paulson@7376
   177
(*For AC rewriting*)
paulson@7376
   178
Goal "(z1::prat) + (z2 + z3) = z2 + (z1 + z3)";
paulson@7376
   179
by (rtac (prat_add_commute RS trans) 1);
paulson@7376
   180
by (rtac (prat_add_assoc RS trans) 1);
paulson@7376
   181
by (rtac (prat_add_commute RS arg_cong) 1);
paulson@7376
   182
qed "prat_add_left_commute";
paulson@5078
   183
paulson@5078
   184
(* Positive Rational addition is an AC operator *)
wenzelm@9108
   185
bind_thms ("prat_add_ac", [prat_add_assoc, prat_add_commute, prat_add_left_commute]);
paulson@5078
   186
paulson@5078
   187
paulson@5078
   188
(*** Congruence property for multiplication ***)
paulson@5078
   189
paulson@5078
   190
Goalw [congruent2_def]
paulson@5078
   191
    "congruent2 ratrel (%p1 p2.                  \
paulson@5078
   192
\         split (%x1 y1. split (%x2 y2. ratrel^^{(x1*x2, y1*y2)}) p2) p1)";
paulson@5078
   193
(*Proof via congruent2_commuteI seems longer*)
paulson@5078
   194
by Safe_tac;
paulson@5078
   195
by (asm_simp_tac (simpset() addsimps [pnat_mult_assoc]) 1);
paulson@5078
   196
(*The rest should be trivial, but rearranging terms is hard*)
paulson@5078
   197
by (res_inst_tac [("x1","x1a")] (pnat_mult_left_commute RS ssubst) 1);
paulson@5078
   198
by (asm_simp_tac (simpset() addsimps [pnat_mult_assoc RS sym]) 1);
paulson@5078
   199
by (asm_simp_tac (simpset() addsimps pnat_mult_ac) 1);
paulson@5078
   200
qed "pnat_mult_congruent2";
paulson@5078
   201
paulson@5078
   202
Goalw [prat_mult_def]
paulson@5078
   203
  "Abs_prat(ratrel^^{(x1,y1)}) * Abs_prat(ratrel^^{(x2,y2)}) = \
paulson@5078
   204
\  Abs_prat(ratrel^^{(x1*x2, y1*y2)})";
paulson@7376
   205
by (asm_simp_tac 
paulson@7376
   206
    (simpset() addsimps [UN_UN_split_split_eq, pnat_mult_congruent2,
paulson@7376
   207
			 equiv_ratrel RS UN_equiv_class2]) 1);
paulson@5078
   208
qed "prat_mult";
paulson@5078
   209
paulson@5078
   210
Goal "(z::prat) * w = w * z";
paulson@5078
   211
by (res_inst_tac [("z","z")] eq_Abs_prat 1);
paulson@5078
   212
by (res_inst_tac [("z","w")] eq_Abs_prat 1);
paulson@5535
   213
by (asm_simp_tac (simpset() addsimps pnat_mult_ac @ [prat_mult]) 1);
paulson@5078
   214
qed "prat_mult_commute";
paulson@5078
   215
paulson@5078
   216
Goal "((z1::prat) * z2) * z3 = z1 * (z2 * z3)";
paulson@5078
   217
by (res_inst_tac [("z","z1")] eq_Abs_prat 1);
paulson@5078
   218
by (res_inst_tac [("z","z2")] eq_Abs_prat 1);
paulson@5078
   219
by (res_inst_tac [("z","z3")] eq_Abs_prat 1);
paulson@5078
   220
by (asm_simp_tac (simpset() addsimps [prat_mult, pnat_mult_assoc]) 1);
paulson@5078
   221
qed "prat_mult_assoc";
paulson@5078
   222
paulson@5078
   223
(*For AC rewriting*)
paulson@5078
   224
Goal "(x::prat)*(y*z)=y*(x*z)";
paulson@5078
   225
by (rtac (prat_mult_commute RS trans) 1);
paulson@5078
   226
by (rtac (prat_mult_assoc RS trans) 1);
paulson@5078
   227
by (rtac (prat_mult_commute RS arg_cong) 1);
paulson@5078
   228
qed "prat_mult_left_commute";
paulson@5078
   229
paulson@5078
   230
(*Positive Rational multiplication is an AC operator*)
wenzelm@9108
   231
bind_thms ("prat_mult_ac", [prat_mult_assoc,
wenzelm@9108
   232
                    prat_mult_commute,prat_mult_left_commute]);
paulson@5078
   233
paulson@7077
   234
Goalw [prat_of_pnat_def] 
paulson@7077
   235
      "(prat_of_pnat (Abs_pnat 1)) * z = z";
paulson@5078
   236
by (res_inst_tac [("z","z")] eq_Abs_prat 1);
paulson@7376
   237
by (asm_full_simp_tac (simpset() addsimps [prat_mult] @ pnat_mult_ac) 1);
paulson@5078
   238
qed "prat_mult_1";
paulson@5078
   239
paulson@7077
   240
Goalw [prat_of_pnat_def] 
paulson@7077
   241
      "z * (prat_of_pnat (Abs_pnat 1)) = z";
paulson@5078
   242
by (res_inst_tac [("z","z")] eq_Abs_prat 1);
paulson@7376
   243
by (asm_full_simp_tac (simpset() addsimps [prat_mult] @ pnat_mult_ac) 1);
paulson@5078
   244
qed "prat_mult_1_right";
paulson@5078
   245
paulson@7077
   246
Goalw [prat_of_pnat_def] 
paulson@7077
   247
      "prat_of_pnat ((z1::pnat) + z2) = \
paulson@7077
   248
\      prat_of_pnat z1 + prat_of_pnat z2";
paulson@5078
   249
by (asm_simp_tac (simpset() addsimps [prat_add,
paulson@7376
   250
				      pnat_add_mult_distrib,pnat_mult_1]) 1);
paulson@7077
   251
qed "prat_of_pnat_add";
paulson@5078
   252
paulson@7077
   253
Goalw [prat_of_pnat_def] 
paulson@7077
   254
      "prat_of_pnat ((z1::pnat) * z2) = \
paulson@7077
   255
\      prat_of_pnat z1 * prat_of_pnat z2";
paulson@7376
   256
by (asm_simp_tac (simpset() addsimps [prat_mult, pnat_mult_1]) 1);
paulson@7077
   257
qed "prat_of_pnat_mult";
paulson@5078
   258
paulson@5078
   259
(*** prat_mult and qinv ***)
paulson@5078
   260
paulson@7077
   261
Goalw [prat_def,prat_of_pnat_def] 
paulson@7077
   262
      "qinv (q) * q = prat_of_pnat (Abs_pnat 1)";
paulson@5078
   263
by (res_inst_tac [("z","q")] eq_Abs_prat 1);
paulson@5078
   264
by (asm_full_simp_tac (simpset() addsimps [qinv,
paulson@7376
   265
        prat_mult,pnat_mult_1,pnat_mult_1_left, pnat_mult_commute]) 1);
paulson@5078
   266
qed "prat_mult_qinv";
paulson@5078
   267
paulson@7077
   268
Goal "q * qinv (q) = prat_of_pnat (Abs_pnat 1)";
paulson@5078
   269
by (rtac (prat_mult_commute RS subst) 1);
paulson@5078
   270
by (simp_tac (simpset() addsimps [prat_mult_qinv]) 1);
paulson@5078
   271
qed "prat_mult_qinv_right";
paulson@5078
   272
paulson@9043
   273
Goal "EX y. (x::prat) * y = prat_of_pnat (Abs_pnat 1)";
paulson@5078
   274
by (fast_tac (claset() addIs [prat_mult_qinv_right]) 1);
paulson@5078
   275
qed "prat_qinv_ex";
paulson@5078
   276
paulson@9043
   277
Goal "EX! y. (x::prat) * y = prat_of_pnat (Abs_pnat 1)";
paulson@5078
   278
by (auto_tac (claset() addIs [prat_mult_qinv_right],simpset()));
paulson@5078
   279
by (dres_inst_tac [("f","%x. ya*x")] arg_cong 1);
paulson@5078
   280
by (asm_full_simp_tac (simpset() addsimps [prat_mult_assoc RS sym]) 1);
paulson@5078
   281
by (asm_full_simp_tac (simpset() addsimps [prat_mult_commute,
paulson@5078
   282
    prat_mult_1,prat_mult_1_right]) 1);
paulson@5078
   283
qed "prat_qinv_ex1";
paulson@5078
   284
paulson@9043
   285
Goal "EX! y. y * (x::prat) = prat_of_pnat (Abs_pnat 1)";
paulson@5078
   286
by (auto_tac (claset() addIs [prat_mult_qinv],simpset()));
paulson@5078
   287
by (dres_inst_tac [("f","%x. x*ya")] arg_cong 1);
paulson@5078
   288
by (asm_full_simp_tac (simpset() addsimps [prat_mult_assoc]) 1);
paulson@5078
   289
by (asm_full_simp_tac (simpset() addsimps [prat_mult_commute,
paulson@5078
   290
    prat_mult_1,prat_mult_1_right]) 1);
paulson@5078
   291
qed "prat_qinv_left_ex1";
paulson@5078
   292
paulson@7077
   293
Goal "x * y = prat_of_pnat (Abs_pnat 1) ==> x = qinv y";
paulson@5078
   294
by (cut_inst_tac [("q","y")] prat_mult_qinv 1);
paulson@5078
   295
by (res_inst_tac [("x1","y")] (prat_qinv_left_ex1 RS ex1E) 1);
paulson@5078
   296
by (Blast_tac 1);
paulson@5078
   297
qed "prat_mult_inv_qinv";
paulson@5078
   298
paulson@9043
   299
Goal "EX y. x = qinv y";
paulson@5078
   300
by (cut_inst_tac [("x","x")] prat_qinv_ex 1);
paulson@5078
   301
by (etac exE 1 THEN dtac prat_mult_inv_qinv 1);
paulson@5078
   302
by (Fast_tac 1);
paulson@5078
   303
qed "prat_as_inverse_ex";
paulson@5078
   304
paulson@5078
   305
Goal "qinv(x*y) = qinv(x)*qinv(y)";
paulson@5078
   306
by (res_inst_tac [("z","x")] eq_Abs_prat 1);
paulson@5078
   307
by (res_inst_tac [("z","y")] eq_Abs_prat 1);
paulson@5078
   308
by (auto_tac (claset(),simpset() addsimps [qinv,prat_mult]));
paulson@5078
   309
qed "qinv_mult_eq";
paulson@5078
   310
paulson@5078
   311
(** Lemmas **)
paulson@5078
   312
paulson@5078
   313
Goal "((z1::prat) + z2) * w = (z1 * w) + (z2 * w)";
paulson@5078
   314
by (res_inst_tac [("z","z1")] eq_Abs_prat 1);
paulson@5078
   315
by (res_inst_tac [("z","z2")] eq_Abs_prat 1);
paulson@5078
   316
by (res_inst_tac [("z","w")] eq_Abs_prat 1);
paulson@5078
   317
by (asm_simp_tac 
paulson@5535
   318
    (simpset() addsimps [pnat_add_mult_distrib2, prat_add, prat_mult] @ 
paulson@5535
   319
                        pnat_add_ac @ pnat_mult_ac) 1);
paulson@5078
   320
qed "prat_add_mult_distrib";
paulson@5078
   321
paulson@5078
   322
val prat_mult_commute'= read_instantiate [("z","w")] prat_mult_commute;
paulson@5078
   323
paulson@5078
   324
Goal "(w::prat) * (z1 + z2) = (w * z1) + (w * z2)";
paulson@5078
   325
by (simp_tac (simpset() addsimps [prat_mult_commute',prat_add_mult_distrib]) 1);
paulson@5078
   326
qed "prat_add_mult_distrib2";
paulson@5078
   327
paulson@7376
   328
Addsimps [prat_mult_1, prat_mult_1_right, 
paulson@7376
   329
	  prat_mult_qinv, prat_mult_qinv_right];
paulson@5078
   330
paulson@5078
   331
      (*** theorems for ordering ***)
paulson@5078
   332
(* prove introduction and elimination rules for prat_less *)
paulson@5078
   333
paulson@5078
   334
Goalw [prat_less_def]
paulson@5078
   335
    "Q1 < (Q2::prat) = (EX Q3. Q1 + Q3 = Q2)";
paulson@5078
   336
by (Fast_tac 1);
paulson@5078
   337
qed "prat_less_iff";
paulson@5078
   338
paulson@5078
   339
Goalw [prat_less_def]
paulson@5078
   340
      "!!(Q1::prat). Q1 + Q3 = Q2 ==> Q1 < Q2";
paulson@5078
   341
by (Fast_tac  1);
paulson@5078
   342
qed "prat_lessI";
paulson@5078
   343
paulson@5078
   344
(* ordering on positive fractions in terms of existence of sum *)
paulson@5078
   345
Goalw [prat_less_def]
paulson@5078
   346
      "Q1 < (Q2::prat) --> (EX Q3. Q1 + Q3 = Q2)";
paulson@5078
   347
by (Fast_tac 1);
paulson@5078
   348
qed "prat_lessE_lemma";
paulson@5078
   349
paulson@5148
   350
Goal "!!P. [| Q1 < (Q2::prat); \
paulson@5148
   351
\             !! (Q3::prat). Q1 + Q3 = Q2 ==> P |] \
paulson@5148
   352
\          ==> P";
paulson@5078
   353
by (dtac (prat_lessE_lemma RS mp) 1);
paulson@5078
   354
by Auto_tac;
paulson@5078
   355
qed "prat_lessE";
paulson@5078
   356
paulson@5078
   357
(* qless is a strong order i.e nonreflexive and transitive *)
paulson@5148
   358
Goal "!!(q1::prat). [| q1 < q2; q2 < q3 |] ==> q1 < q3";
paulson@5078
   359
by (REPEAT(dtac (prat_lessE_lemma RS mp) 1));
paulson@5078
   360
by (REPEAT(etac exE 1));
paulson@5078
   361
by (hyp_subst_tac 1);
paulson@5078
   362
by (res_inst_tac [("Q3.0","Q3 + Q3a")] prat_lessI 1);
paulson@5078
   363
by (auto_tac (claset(),simpset() addsimps [prat_add_assoc]));
paulson@5078
   364
qed "prat_less_trans";
paulson@5078
   365
paulson@5078
   366
Goal "~q < (q::prat)";
paulson@5078
   367
by (EVERY1[rtac notI, dtac (prat_lessE_lemma RS mp)]);
paulson@5078
   368
by (res_inst_tac [("z","q")] eq_Abs_prat 1);
paulson@5078
   369
by (res_inst_tac [("z","Q3")] eq_Abs_prat 1);
paulson@5078
   370
by (etac exE 1 THEN res_inst_tac [("z","Q3a")] eq_Abs_prat 1);
paulson@5078
   371
by (REPEAT(hyp_subst_tac 1));
paulson@5078
   372
by (asm_full_simp_tac (simpset() addsimps [prat_add,
paulson@5078
   373
    pnat_no_add_ident,pnat_add_mult_distrib2] @ pnat_mult_ac) 1);
paulson@5078
   374
qed "prat_less_not_refl";
paulson@5078
   375
paulson@5078
   376
(*** y < y ==> P ***)
paulson@5078
   377
bind_thm("prat_less_irrefl",prat_less_not_refl RS notE);
paulson@5078
   378
paulson@5459
   379
Goal "!! (q1::prat). q1 < q2 ==> ~ q2 < q1";
paulson@5459
   380
by (rtac notI 1);
paulson@5078
   381
by (dtac prat_less_trans 1 THEN assume_tac 1);
paulson@5078
   382
by (asm_full_simp_tac (simpset() addsimps [prat_less_not_refl]) 1);
paulson@5459
   383
qed "prat_less_not_sym";
paulson@5078
   384
paulson@5459
   385
(* [| x < y;  ~P ==> y < x |] ==> P *)
paulson@5459
   386
bind_thm ("prat_less_asym", prat_less_not_sym RS swap);
paulson@5078
   387
paulson@5078
   388
(* half of positive fraction exists- Gleason p. 120- Proposition 9-2.6(i)*)
paulson@9043
   389
Goal "!(q::prat). EX x. x + x = q";
paulson@5078
   390
by (rtac allI 1);
paulson@5078
   391
by (res_inst_tac [("z","q")] eq_Abs_prat 1);
paulson@5078
   392
by (res_inst_tac [("x","Abs_prat (ratrel ^^ {(x, y+y)})")] exI 1);
paulson@7376
   393
by (auto_tac (claset(),
paulson@7376
   394
	      simpset() addsimps 
paulson@5078
   395
              [prat_add,pnat_mult_assoc RS sym,pnat_add_mult_distrib,
paulson@5078
   396
               pnat_add_mult_distrib2]));
paulson@5078
   397
qed "lemma_prat_dense";
paulson@5078
   398
paulson@9043
   399
Goal "EX (x::prat). x + x = q";
paulson@5078
   400
by (res_inst_tac [("z","q")] eq_Abs_prat 1);
paulson@5078
   401
by (res_inst_tac [("x","Abs_prat (ratrel ^^ {(x, y+y)})")] exI 1);
paulson@5078
   402
by (auto_tac (claset(),simpset() addsimps 
paulson@5078
   403
              [prat_add,pnat_mult_assoc RS sym,pnat_add_mult_distrib,
paulson@5078
   404
               pnat_add_mult_distrib2]));
paulson@5078
   405
qed "prat_lemma_dense";
paulson@5078
   406
paulson@5078
   407
(* there exists a number between any two positive fractions *)
paulson@5078
   408
(* Gleason p. 120- Proposition 9-2.6(iv) *)
paulson@5078
   409
Goalw [prat_less_def] 
paulson@9043
   410
      "!! (q1::prat). q1 < q2 ==> EX x. q1 < x & x < q2";
paulson@5078
   411
by (auto_tac (claset() addIs [lemma_prat_dense],simpset()));
paulson@5078
   412
by (res_inst_tac [("x","T")] (lemma_prat_dense RS allE) 1);
paulson@5078
   413
by (etac exE 1);
paulson@5078
   414
by (res_inst_tac [("x","q1 + x")] exI 1);
paulson@5078
   415
by (auto_tac (claset() addIs [prat_lemma_dense],
paulson@7376
   416
	      simpset() addsimps [prat_add_assoc]));
paulson@5078
   417
qed "prat_dense";
paulson@5078
   418
paulson@5078
   419
(* ordering of addition for positive fractions *)
paulson@7376
   420
Goalw [prat_less_def] "!!(q1::prat). q1 < q2 ==> q1 + x < q2 + x";
paulson@5078
   421
by (Step_tac 1);
paulson@5078
   422
by (res_inst_tac [("x","T")] exI 1);
paulson@5078
   423
by (auto_tac (claset(),simpset() addsimps prat_add_ac));
paulson@5078
   424
qed "prat_add_less2_mono1";
paulson@5078
   425
paulson@7219
   426
Goal "!!(q1::prat). q1 < q2 ==> x + q1 < x + q2";
paulson@5078
   427
by (auto_tac (claset() addIs [prat_add_less2_mono1],
paulson@5078
   428
    simpset() addsimps [prat_add_commute]));
paulson@5078
   429
qed "prat_add_less2_mono2";
paulson@5078
   430
paulson@5078
   431
(* ordering of multiplication for positive fractions *)
paulson@5078
   432
Goalw [prat_less_def] 
paulson@5078
   433
      "!!(q1::prat). q1 < q2 ==> q1 * x < q2 * x";
paulson@5078
   434
by (Step_tac 1);
paulson@5078
   435
by (res_inst_tac [("x","T*x")] exI 1);
paulson@5078
   436
by (auto_tac (claset(),simpset() addsimps [prat_add_mult_distrib]));
paulson@5078
   437
qed "prat_mult_less2_mono1";
paulson@5078
   438
paulson@5078
   439
Goal "!!(q1::prat). q1 < q2  ==> x * q1 < x * q2";
paulson@5078
   440
by (auto_tac (claset() addDs [prat_mult_less2_mono1],
paulson@5078
   441
    simpset() addsimps [prat_mult_commute]));
paulson@5078
   442
qed "prat_mult_left_less2_mono1";
paulson@5078
   443
paulson@5078
   444
(* there is no smallest positive fraction *)
paulson@9043
   445
Goalw [prat_less_def] "EX (x::prat). x < y";
paulson@5078
   446
by (cut_facts_tac [lemma_prat_dense] 1);
paulson@5078
   447
by (Fast_tac 1);
paulson@5078
   448
qed "qless_Ex";
paulson@5078
   449
paulson@5078
   450
(* lemma for proving $< is linear *)
paulson@5078
   451
Goalw [prat_def,prat_less_def] 
paulson@5078
   452
      "ratrel ^^ {(x, y * ya)} : {p::(pnat*pnat).True}/ratrel";
paulson@5078
   453
by (asm_full_simp_tac (simpset() addsimps [ratrel_def,quotient_def]) 1);
paulson@5078
   454
by (Blast_tac 1);
paulson@5078
   455
qed "lemma_prat_less_linear";
paulson@5078
   456
paulson@5078
   457
(* linearity of < -- Gleason p. 120 - Proposition 9-2.6 *)
paulson@5078
   458
(*** FIXME Proof long ***)
paulson@5078
   459
Goalw [prat_less_def] 
paulson@5078
   460
      "(q1::prat) < q2 | q1 = q2 | q2 < q1";
paulson@5078
   461
by (res_inst_tac [("z","q1")] eq_Abs_prat 1);
paulson@5078
   462
by (res_inst_tac [("z","q2")] eq_Abs_prat 1);
paulson@5078
   463
by (Step_tac 1 THEN REPEAT(dtac (not_ex RS iffD1) 1) 
paulson@5078
   464
               THEN Auto_tac);
paulson@7376
   465
by (cut_inst_tac  [("z1.0","x*ya"), ("z2.0","xa*y")] pnat_linear_Ex_eq 1);
paulson@5078
   466
by (EVERY1[etac disjE,etac exE]);
paulson@5078
   467
by (eres_inst_tac 
paulson@5078
   468
    [("x","Abs_prat(ratrel^^{(xb,ya*y)})")] allE 1);
paulson@5078
   469
by (asm_full_simp_tac 
paulson@5078
   470
    (simpset() addsimps [prat_add, pnat_mult_assoc 
paulson@5078
   471
     RS sym,pnat_add_mult_distrib RS sym]) 1);
paulson@5078
   472
by (EVERY1[asm_full_simp_tac (simpset() addsimps pnat_mult_ac),
paulson@5078
   473
    etac disjE, assume_tac, etac exE]);
paulson@5078
   474
by (thin_tac "!T. Abs_prat (ratrel ^^ {(x, y)}) + T ~= \
paulson@5078
   475
\     Abs_prat (ratrel ^^ {(xa, ya)})" 1);
paulson@5078
   476
by (eres_inst_tac [("x","Abs_prat(ratrel^^{(xb,y*ya)})")] allE 1);
paulson@5078
   477
by (asm_full_simp_tac (simpset() addsimps [prat_add,
paulson@5078
   478
      pnat_mult_assoc RS sym,pnat_add_mult_distrib RS sym]) 1);
paulson@5078
   479
by (asm_full_simp_tac (simpset() addsimps pnat_mult_ac) 1);
paulson@5078
   480
qed "prat_linear";
paulson@5078
   481
paulson@7219
   482
Goal "!!(q1::prat). [| q1 < q2 ==> P;  q1 = q2 ==> P; \
paulson@5078
   483
\          q2 < q1 ==> P |] ==> P";
paulson@5078
   484
by (cut_inst_tac [("q1.0","q1"),("q2.0","q2")] prat_linear 1);
paulson@5078
   485
by Auto_tac;
paulson@5078
   486
qed "prat_linear_less2";
paulson@5078
   487
paulson@5078
   488
(* Gleason p. 120 -- 9-2.6 (iv) *)
paulson@7376
   489
Goal "[| q1 < q2; qinv(q1) = qinv(q2) |] ==> P";
paulson@7376
   490
by (cut_inst_tac [("x","qinv (q2)"),("q1.0","q1"), ("q2.0","q2")] 
paulson@7376
   491
    prat_mult_less2_mono1 1);
paulson@5078
   492
by (assume_tac 1);
paulson@5078
   493
by (Asm_full_simp_tac 1 THEN dtac sym 1);
paulson@5078
   494
by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl]));
paulson@5078
   495
qed "lemma1_qinv_prat_less";
paulson@5078
   496
paulson@7376
   497
Goal "[| q1 < q2; qinv(q1) < qinv(q2) |] ==> P";
paulson@7376
   498
by (cut_inst_tac [("x","qinv (q2)"),("q1.0","q1"), ("q2.0","q2")] 
paulson@7376
   499
    prat_mult_less2_mono1 1);
paulson@5078
   500
by (assume_tac 1);
paulson@7376
   501
by (cut_inst_tac [("x","q1"),("q1.0","qinv (q1)"), ("q2.0","qinv (q2)")] 
paulson@7376
   502
    prat_mult_left_less2_mono1 1);
paulson@5078
   503
by Auto_tac;
paulson@7077
   504
by (dres_inst_tac [("q2.0","prat_of_pnat (Abs_pnat 1)")] prat_less_trans 1);
paulson@7077
   505
by (auto_tac (claset(),simpset() addsimps 
paulson@7077
   506
    [prat_less_not_refl]));
paulson@5078
   507
qed "lemma2_qinv_prat_less";
paulson@5078
   508
paulson@7376
   509
Goal "q1 < q2  ==> qinv (q2) < qinv (q1)";
paulson@7376
   510
by (res_inst_tac [("q2.0","qinv q1"), ("q1.0","qinv q2")] prat_linear_less2 1);
paulson@5078
   511
by (auto_tac (claset() addEs [lemma1_qinv_prat_less,
paulson@5078
   512
                 lemma2_qinv_prat_less],simpset()));
paulson@5078
   513
qed "qinv_prat_less";
paulson@5078
   514
paulson@7376
   515
Goal "q1 < prat_of_pnat (Abs_pnat 1) \
paulson@7077
   516
\     ==> prat_of_pnat (Abs_pnat 1) < qinv(q1)";
paulson@5078
   517
by (dtac qinv_prat_less 1);
paulson@5078
   518
by (full_simp_tac (simpset() addsimps [qinv_1]) 1);
paulson@5078
   519
qed "prat_qinv_gt_1";
paulson@5078
   520
paulson@7077
   521
Goalw [pnat_one_def] 
paulson@7376
   522
     "q1 < prat_of_pnat 1p ==> prat_of_pnat 1p < qinv(q1)";
paulson@5078
   523
by (etac prat_qinv_gt_1 1);
paulson@5078
   524
qed "prat_qinv_is_gt_1";
paulson@5078
   525
paulson@7077
   526
Goalw [prat_less_def] 
paulson@7077
   527
      "prat_of_pnat (Abs_pnat 1) < prat_of_pnat (Abs_pnat 1) \
paulson@7077
   528
\                   + prat_of_pnat (Abs_pnat 1)";
paulson@5078
   529
by (Fast_tac 1); 
paulson@5078
   530
qed "prat_less_1_2";
paulson@5078
   531
paulson@7077
   532
Goal "qinv(prat_of_pnat (Abs_pnat 1) + \
paulson@7077
   533
\     prat_of_pnat (Abs_pnat 1)) < prat_of_pnat (Abs_pnat 1)";
paulson@5078
   534
by (cut_facts_tac [prat_less_1_2 RS qinv_prat_less] 1);
paulson@5078
   535
by (asm_full_simp_tac (simpset() addsimps [qinv_1]) 1);
paulson@5078
   536
qed "prat_less_qinv_2_1";
paulson@5078
   537
paulson@7077
   538
Goal "!!(x::prat). x < y ==> x*qinv(y) < prat_of_pnat (Abs_pnat 1)";
paulson@5078
   539
by (dres_inst_tac [("x","qinv(y)")] prat_mult_less2_mono1 1);
paulson@5078
   540
by (Asm_full_simp_tac 1);
paulson@5078
   541
qed "prat_mult_qinv_less_1";
paulson@5078
   542
paulson@5078
   543
Goal "(x::prat) < x + x";
paulson@5078
   544
by (cut_inst_tac [("x","x")] 
paulson@5078
   545
    (prat_less_1_2 RS prat_mult_left_less2_mono1) 1);
paulson@5078
   546
by (asm_full_simp_tac (simpset() addsimps 
paulson@5078
   547
    [prat_add_mult_distrib2]) 1);
paulson@5078
   548
qed "prat_self_less_add_self";
paulson@5078
   549
paulson@5078
   550
Goalw [prat_less_def] "(x::prat) < y + x";
paulson@5078
   551
by (res_inst_tac [("x","y")] exI 1);
paulson@5078
   552
by (simp_tac (simpset() addsimps [prat_add_commute]) 1);
paulson@5078
   553
qed "prat_self_less_add_right";
paulson@5078
   554
paulson@5078
   555
Goal "(x::prat) < x + y";
paulson@5078
   556
by (rtac (prat_add_commute RS subst) 1);
paulson@5078
   557
by (simp_tac (simpset() addsimps [prat_self_less_add_right]) 1);
paulson@5078
   558
qed "prat_self_less_add_left";
paulson@5078
   559
paulson@7077
   560
Goalw [prat_less_def] "prat_of_pnat 1p < y ==> (x::prat) < x * y";
paulson@5078
   561
by (auto_tac (claset(),simpset() addsimps [pnat_one_def,
paulson@5078
   562
    prat_add_mult_distrib2]));
paulson@5078
   563
qed "prat_self_less_mult_right";
paulson@5078
   564
paulson@5078
   565
(*** Properties of <= ***)
paulson@5078
   566
paulson@5143
   567
Goalw [prat_le_def] "~(w < z) ==> z <= (w::prat)";
paulson@5078
   568
by (assume_tac 1);
paulson@5078
   569
qed "prat_leI";
paulson@5078
   570
paulson@5143
   571
Goalw [prat_le_def] "z<=w ==> ~(w<(z::prat))";
paulson@5078
   572
by (assume_tac 1);
paulson@5078
   573
qed "prat_leD";
paulson@5078
   574
wenzelm@9108
   575
bind_thm ("prat_leE", make_elim prat_leD);
paulson@5078
   576
paulson@5143
   577
Goal "(~(w < z)) = (z <= (w::prat))";
paulson@5078
   578
by (fast_tac (claset() addSIs [prat_leI,prat_leD]) 1);
paulson@5078
   579
qed "prat_less_le_iff";
paulson@5078
   580
paulson@5143
   581
Goalw [prat_le_def] "~ z <= w ==> w<(z::prat)";
paulson@5078
   582
by (Fast_tac 1);
paulson@5078
   583
qed "not_prat_leE";
paulson@5078
   584
paulson@5143
   585
Goalw [prat_le_def] "z < w ==> z <= (w::prat)";
paulson@5078
   586
by (fast_tac (claset() addEs [prat_less_asym]) 1);
paulson@5078
   587
qed "prat_less_imp_le";
paulson@5078
   588
paulson@5078
   589
Goalw [prat_le_def] "!!(x::prat). x <= y ==> x < y | x = y";
paulson@5078
   590
by (cut_facts_tac [prat_linear] 1);
paulson@5078
   591
by (fast_tac (claset() addEs [prat_less_irrefl,prat_less_asym]) 1);
paulson@5078
   592
qed "prat_le_imp_less_or_eq";
paulson@5078
   593
paulson@5143
   594
Goalw [prat_le_def] "z<w | z=w ==> z <=(w::prat)";
paulson@5078
   595
by (cut_facts_tac [prat_linear] 1);
paulson@5078
   596
by (fast_tac (claset() addEs [prat_less_irrefl,prat_less_asym]) 1);
paulson@5078
   597
qed "prat_less_or_eq_imp_le";
paulson@5078
   598
paulson@5078
   599
Goal "(x <= (y::prat)) = (x < y | x=y)";
paulson@5078
   600
by (REPEAT(ares_tac [iffI, prat_less_or_eq_imp_le, prat_le_imp_less_or_eq] 1));
paulson@5078
   601
qed "prat_le_eq_less_or_eq";
paulson@5078
   602
paulson@5078
   603
Goal "w <= (w::prat)";
paulson@5078
   604
by (simp_tac (simpset() addsimps [prat_le_eq_less_or_eq]) 1);
paulson@5078
   605
qed "prat_le_refl";
paulson@5078
   606
paulson@5078
   607
val prems = goal thy "!!i. [| i <= j; j < k |] ==> i < (k::prat)";
paulson@5078
   608
by (dtac prat_le_imp_less_or_eq 1);
paulson@5078
   609
by (fast_tac (claset() addIs [prat_less_trans]) 1);
paulson@5078
   610
qed "prat_le_less_trans";
paulson@5078
   611
paulson@5078
   612
Goal "!! (i::prat). [| i < j; j <= k |] ==> i < k";
paulson@5078
   613
by (dtac prat_le_imp_less_or_eq 1);
paulson@5078
   614
by (fast_tac (claset() addIs [prat_less_trans]) 1);
paulson@5078
   615
qed "prat_less_le_trans";
paulson@5078
   616
paulson@5143
   617
Goal "[| i <= j; j <= k |] ==> i <= (k::prat)";
paulson@5078
   618
by (EVERY1 [dtac prat_le_imp_less_or_eq, dtac prat_le_imp_less_or_eq,
paulson@5078
   619
            rtac prat_less_or_eq_imp_le, fast_tac (claset() addIs [prat_less_trans])]);
paulson@5078
   620
qed "prat_le_trans";
paulson@5078
   621
paulson@5143
   622
Goal "[| z <= w; w <= z |] ==> z = (w::prat)";
paulson@5078
   623
by (EVERY1 [dtac prat_le_imp_less_or_eq, dtac prat_le_imp_less_or_eq,
paulson@5078
   624
            fast_tac (claset() addEs [prat_less_irrefl,prat_less_asym])]);
paulson@5078
   625
qed "prat_le_anti_sym";
paulson@5078
   626
paulson@5143
   627
Goal "[| ~ y < x; y ~= x |] ==> x < (y::prat)";
paulson@5078
   628
by (rtac not_prat_leE 1);
paulson@5078
   629
by (fast_tac (claset() addDs [prat_le_imp_less_or_eq]) 1);
paulson@5078
   630
qed "not_less_not_eq_prat_less";
paulson@5078
   631
paulson@5078
   632
Goalw [prat_less_def] 
paulson@5148
   633
      "[| x1 < y1; x2 < y2 |] ==> x1 + x2 < y1 + (y2::prat)";
paulson@5078
   634
by (REPEAT(etac exE 1));
paulson@5078
   635
by (res_inst_tac [("x","T+Ta")] exI 1);
paulson@5078
   636
by (auto_tac (claset(),simpset() addsimps prat_add_ac));
paulson@5078
   637
qed "prat_add_less_mono";
paulson@5078
   638
paulson@5078
   639
Goalw [prat_less_def] 
paulson@5148
   640
      "[| x1 < y1; x2 < y2 |] ==> x1 * x2 < y1 * (y2::prat)";
paulson@5078
   641
by (REPEAT(etac exE 1));
paulson@5078
   642
by (res_inst_tac [("x","T*Ta+T*x2+x1*Ta")] exI 1);
paulson@7376
   643
by (auto_tac (claset(),
paulson@7376
   644
	      simpset() addsimps prat_add_ac @ 
paulson@7376
   645
	                      [prat_add_mult_distrib,prat_add_mult_distrib2]));
paulson@5078
   646
qed "prat_mult_less_mono";
paulson@5078
   647
paulson@5078
   648
(* more prat_le *)
paulson@5078
   649
Goal "!!(q1::prat). q1 <= q2  ==> x * q1 <= x * q2";
paulson@5078
   650
by (dtac prat_le_imp_less_or_eq 1);
paulson@5078
   651
by (Step_tac 1);
paulson@7376
   652
by (auto_tac (claset() addSIs [prat_le_refl, prat_less_imp_le,
paulson@7376
   653
			       prat_mult_left_less2_mono1],
paulson@7376
   654
	      simpset()));
paulson@5078
   655
qed "prat_mult_left_le2_mono1";
paulson@5078
   656
paulson@5078
   657
Goal "!!(q1::prat). q1 <= q2  ==> q1 * x <= q2 * x";
paulson@5078
   658
by (auto_tac (claset() addDs [prat_mult_left_le2_mono1],
paulson@7376
   659
	      simpset() addsimps [prat_mult_commute]));
paulson@5078
   660
qed "prat_mult_le2_mono1";
paulson@5078
   661
paulson@7376
   662
Goal "q1 <= q2  ==> qinv (q2) <= qinv (q1)";
paulson@5078
   663
by (dtac prat_le_imp_less_or_eq 1);
paulson@5078
   664
by (Step_tac 1);
paulson@7376
   665
by (auto_tac (claset() addSIs [prat_le_refl, prat_less_imp_le,qinv_prat_less],
paulson@7376
   666
	      simpset()));
paulson@5078
   667
qed "qinv_prat_le";
paulson@5078
   668
paulson@5078
   669
Goal "!!(q1::prat). q1 <= q2  ==> x + q1 <= x + q2";
paulson@5078
   670
by (dtac prat_le_imp_less_or_eq 1);
paulson@5078
   671
by (Step_tac 1);
paulson@5078
   672
by (auto_tac (claset() addSIs [prat_le_refl,
paulson@7376
   673
			       prat_less_imp_le,prat_add_less2_mono1],
paulson@7376
   674
	      simpset() addsimps [prat_add_commute]));
paulson@5078
   675
qed "prat_add_left_le2_mono1";
paulson@5078
   676
paulson@5078
   677
Goal "!!(q1::prat). q1 <= q2  ==> q1 + x <= q2 + x";
paulson@5078
   678
by (auto_tac (claset() addDs [prat_add_left_le2_mono1],
paulson@7376
   679
	      simpset() addsimps [prat_add_commute]));
paulson@5078
   680
qed "prat_add_le2_mono1";
paulson@5078
   681
paulson@5078
   682
Goal "!!k l::prat. [|i<=j;  k<=l |] ==> i + k <= j + l";
paulson@5078
   683
by (etac (prat_add_le2_mono1 RS prat_le_trans) 1);
paulson@5078
   684
by (simp_tac (simpset() addsimps [prat_add_commute]) 1);
paulson@5078
   685
(*j moves to the end because it is free while k, l are bound*)
paulson@5078
   686
by (etac prat_add_le2_mono1 1);
paulson@5078
   687
qed "prat_add_le_mono";
paulson@5078
   688
paulson@5078
   689
Goal "!!(x::prat). x + y < z + y ==> x < z";
paulson@5078
   690
by (rtac ccontr 1);
paulson@5078
   691
by (etac (prat_leI RS prat_le_imp_less_or_eq RS disjE) 1);
paulson@5078
   692
by (dres_inst_tac [("x","y"),("q1.0","z")] prat_add_less2_mono1 1);
paulson@5078
   693
by (auto_tac (claset() addIs [prat_less_asym],
paulson@5078
   694
    simpset() addsimps [prat_less_not_refl]));
paulson@5078
   695
qed "prat_add_right_less_cancel";
paulson@5078
   696
paulson@5078
   697
Goal "!!(x::prat). y + x < y + z ==> x < z";
paulson@5078
   698
by (res_inst_tac [("y","y")] prat_add_right_less_cancel 1);
paulson@5078
   699
by (asm_full_simp_tac (simpset() addsimps [prat_add_commute]) 1);
paulson@5078
   700
qed "prat_add_left_less_cancel";
paulson@5078
   701
paulson@5078
   702
(*** lemmas required for lemma_gleason9_34 in PReal : w*y > y/z ***)
paulson@7077
   703
Goalw [prat_of_pnat_def] 
paulson@7077
   704
      "Abs_prat(ratrel^^{(x,y)}) = (prat_of_pnat x)*qinv(prat_of_pnat y)";
paulson@5078
   705
by (auto_tac (claset(),simpset() addsimps [prat_mult,qinv,pnat_mult_1_left,
paulson@5078
   706
    pnat_mult_1]));
paulson@5078
   707
qed "Abs_prat_mult_qinv";
paulson@5078
   708
paulson@5078
   709
Goal "Abs_prat(ratrel^^{(x,y)}) <= Abs_prat(ratrel^^{(x,Abs_pnat 1)})";
paulson@5078
   710
by (simp_tac (simpset() addsimps [Abs_prat_mult_qinv]) 1);
paulson@5078
   711
by (rtac prat_mult_left_le2_mono1 1);
paulson@5078
   712
by (rtac qinv_prat_le 1);
paulson@5078
   713
by (pnat_ind_tac "y" 1);
paulson@7077
   714
by (dres_inst_tac [("x","prat_of_pnat (Abs_pnat 1)")] prat_add_le2_mono1 2);
paulson@5078
   715
by (cut_facts_tac [prat_less_1_2 RS prat_less_imp_le] 2);
paulson@5078
   716
by (auto_tac (claset() addIs [prat_le_trans],
paulson@5078
   717
    simpset() addsimps [prat_le_refl,
paulson@7077
   718
    pSuc_is_plus_one,pnat_one_def,prat_of_pnat_add]));
paulson@5078
   719
qed "lemma_Abs_prat_le1";
paulson@5078
   720
paulson@5078
   721
Goal "Abs_prat(ratrel^^{(x,Abs_pnat 1)}) <= Abs_prat(ratrel^^{(x*y,Abs_pnat 1)})";
paulson@5078
   722
by (simp_tac (simpset() addsimps [Abs_prat_mult_qinv]) 1);
paulson@5078
   723
by (rtac prat_mult_le2_mono1 1);
paulson@5078
   724
by (pnat_ind_tac "y" 1);
paulson@7077
   725
by (dres_inst_tac [("x","prat_of_pnat x")] prat_add_le2_mono1 2);
paulson@7077
   726
by (cut_inst_tac [("z","prat_of_pnat x")] (prat_self_less_add_self 
paulson@5078
   727
    RS prat_less_imp_le) 2);
paulson@5078
   728
by (auto_tac (claset() addIs [prat_le_trans],
paulson@5078
   729
    simpset() addsimps [prat_le_refl,
paulson@7376
   730
			pSuc_is_plus_one,pnat_one_def,prat_add_mult_distrib2,
paulson@7376
   731
			prat_of_pnat_add,prat_of_pnat_mult]));
paulson@5078
   732
qed "lemma_Abs_prat_le2";
paulson@5078
   733
paulson@5078
   734
Goal "Abs_prat(ratrel^^{(x,z)}) <= Abs_prat(ratrel^^{(x*y,Abs_pnat 1)})";
paulson@7077
   735
by (fast_tac (claset() addIs [prat_le_trans,
paulson@7376
   736
			      lemma_Abs_prat_le1,lemma_Abs_prat_le2]) 1);
paulson@5078
   737
qed "lemma_Abs_prat_le3";
paulson@5078
   738
paulson@5078
   739
Goal "Abs_prat(ratrel^^{(x*y,Abs_pnat 1)}) * Abs_prat(ratrel^^{(w,x)}) = \
paulson@5078
   740
\         Abs_prat(ratrel^^{(w*y,Abs_pnat 1)})";
paulson@5078
   741
by (full_simp_tac (simpset() addsimps [prat_mult,
paulson@5078
   742
    pnat_mult_1,pnat_mult_1_left] @ pnat_mult_ac) 1);
paulson@5078
   743
qed "pre_lemma_gleason9_34";
paulson@5078
   744
paulson@5078
   745
Goal "Abs_prat(ratrel^^{(y*x,Abs_pnat 1*y)}) = \
paulson@5078
   746
\         Abs_prat(ratrel^^{(x,Abs_pnat 1)})";
paulson@7376
   747
by (auto_tac (claset(),
paulson@7376
   748
	      simpset() addsimps [pnat_mult_1,pnat_mult_1_left] @ pnat_mult_ac));
paulson@5078
   749
qed "pre_lemma_gleason9_34b";
paulson@5078
   750
paulson@7077
   751
Goal "(prat_of_pnat n < prat_of_pnat m) = (n < m)";
paulson@5078
   752
by (auto_tac (claset(),simpset() addsimps [prat_less_def,
paulson@7077
   753
    pnat_less_iff,prat_of_pnat_add]));
paulson@5078
   754
by (res_inst_tac [("z","T")] eq_Abs_prat 1);
paulson@5078
   755
by (auto_tac (claset() addDs [pnat_eq_lessI],
paulson@5078
   756
    simpset() addsimps [prat_add,pnat_mult_1,
paulson@7077
   757
    pnat_mult_1_left,prat_of_pnat_def,pnat_less_iff RS sym]));
paulson@7077
   758
qed "prat_of_pnat_less_iff";
paulson@5078
   759
paulson@7077
   760
Addsimps [prat_of_pnat_less_iff];
paulson@5078
   761
paulson@7077
   762
(*------------------------------------------------------------------*)
paulson@5078
   763
paulson@5078
   764
(*** prove witness that will be required to prove non-emptiness ***)
paulson@7077
   765
(*** of preal type as defined using Dedekind Sections in PReal  ***)
paulson@5078
   766
(*** Show that exists positive real `one' ***)
paulson@5078
   767
paulson@9043
   768
Goal "EX q. q: {x::prat. x < prat_of_pnat (Abs_pnat 1)}";
paulson@5078
   769
by (fast_tac (claset() addIs [prat_less_qinv_2_1]) 1);
paulson@5078
   770
qed "lemma_prat_less_1_memEx";
paulson@5078
   771
paulson@7077
   772
Goal "{x::prat. x < prat_of_pnat (Abs_pnat 1)} ~= {}";
paulson@5078
   773
by (rtac notI 1);
paulson@5078
   774
by (cut_facts_tac [lemma_prat_less_1_memEx] 1);
paulson@5078
   775
by (Asm_full_simp_tac 1);
paulson@5078
   776
qed "lemma_prat_less_1_set_non_empty";
paulson@5078
   777
paulson@7077
   778
Goalw [psubset_def] "{} < {x::prat. x < prat_of_pnat (Abs_pnat 1)}";
paulson@5078
   779
by (asm_full_simp_tac (simpset() addsimps 
paulson@5078
   780
         [lemma_prat_less_1_set_non_empty RS not_sym]) 1);
paulson@5078
   781
qed "empty_set_psubset_lemma_prat_less_1_set";
paulson@5078
   782
paulson@7077
   783
(*** exists rational not in set --- prat_of_pnat (Abs_pnat 1) itself ***)
paulson@9043
   784
Goal "EX q. q ~: {x::prat. x < prat_of_pnat (Abs_pnat 1)}";
paulson@7077
   785
by (res_inst_tac [("x","prat_of_pnat (Abs_pnat 1)")] exI 1);
paulson@5078
   786
by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl]));
paulson@5078
   787
qed "lemma_prat_less_1_not_memEx";
paulson@5078
   788
paulson@7825
   789
Goal "{x::prat. x < prat_of_pnat (Abs_pnat 1)} ~= UNIV";
paulson@5078
   790
by (rtac notI 1);
paulson@5078
   791
by (cut_facts_tac [lemma_prat_less_1_not_memEx] 1);
paulson@5078
   792
by (Asm_full_simp_tac 1);
paulson@5078
   793
qed "lemma_prat_less_1_set_not_rat_set";
paulson@5078
   794
paulson@5078
   795
Goalw [psubset_def,subset_def] 
paulson@7825
   796
      "{x::prat. x < prat_of_pnat (Abs_pnat 1)} < UNIV";
paulson@7825
   797
by (asm_full_simp_tac
paulson@7825
   798
    (simpset() addsimps [lemma_prat_less_1_set_not_rat_set,
paulson@7825
   799
			 lemma_prat_less_1_not_memEx]) 1);
paulson@5078
   800
qed "lemma_prat_less_1_set_psubset_rat_set";
paulson@5078
   801
paulson@5078
   802
(*** prove non_emptiness of type ***)
paulson@7077
   803
Goal "{x::prat. x < prat_of_pnat (Abs_pnat 1)} : {A. {} < A & \
paulson@7825
   804
\               A < UNIV & \
paulson@7077
   805
\               (!y: A. ((!z. z < y --> z: A) & \
paulson@9043
   806
\               (EX u: A. y < u)))}";
paulson@5078
   807
by (auto_tac (claset() addDs [prat_less_trans],
paulson@5078
   808
    simpset() addsimps [empty_set_psubset_lemma_prat_less_1_set,
paulson@5078
   809
                       lemma_prat_less_1_set_psubset_rat_set]));
paulson@5078
   810
by (dtac prat_dense 1);
paulson@5078
   811
by (Fast_tac 1);
paulson@5078
   812
qed "preal_1";