turned translation for 1::nat into def.
introduced 1' and replaced most occurrences of 1 by 1'.
(* Title : PRat.ML
ID : $Id$
Author : Jacques D. Fleuriot
Copyright : 1998 University of Cambridge
Description : The positive rationals
*)
(*** Many theorems similar to those in theory Integ ***)
(*** Proving that ratrel is an equivalence relation ***)
Goal "[| (x1::pnat) * y2 = x2 * y1; x2 * y3 = x3 * y2 |] \
\ ==> x1 * y3 = x3 * y1";
by (res_inst_tac [("k1","y2")] (pnat_mult_cancel1 RS iffD1) 1);
by (auto_tac (claset(), simpset() addsimps [pnat_mult_assoc RS sym]));
by (auto_tac (claset(),simpset() addsimps [pnat_mult_commute]));
by (dres_inst_tac [("s","x2 * y3")] sym 1);
by (asm_simp_tac (simpset() addsimps [pnat_mult_left_commute,
pnat_mult_commute]) 1);
qed "prat_trans_lemma";
(** Natural deduction for ratrel **)
Goalw [ratrel_def]
"(((x1,y1),(x2,y2)): ratrel) = (x1 * y2 = x2 * y1)";
by (Fast_tac 1);
qed "ratrel_iff";
Goalw [ratrel_def]
"[| x1 * y2 = x2 * y1 |] ==> ((x1,y1),(x2,y2)): ratrel";
by (Fast_tac 1);
qed "ratrelI";
Goalw [ratrel_def]
"p: ratrel --> (EX x1 y1 x2 y2. \
\ p = ((x1,y1),(x2,y2)) & x1 *y2 = x2 *y1)";
by (Fast_tac 1);
qed "ratrelE_lemma";
val [major,minor] = Goal
"[| p: ratrel; \
\ !!x1 y1 x2 y2. [| p = ((x1,y1),(x2,y2)); x1*y2 = x2*y1 \
\ |] ==> Q |] ==> Q";
by (cut_facts_tac [major RS (ratrelE_lemma RS mp)] 1);
by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1));
qed "ratrelE";
AddSIs [ratrelI];
AddSEs [ratrelE];
Goal "(x,x): ratrel";
by (pair_tac "x" 1);
by (rtac ratrelI 1);
by (rtac refl 1);
qed "ratrel_refl";
Goalw [equiv_def, refl_def, sym_def, trans_def]
"equiv UNIV ratrel";
by (fast_tac (claset() addSIs [ratrel_refl]
addSEs [sym, prat_trans_lemma]) 1);
qed "equiv_ratrel";
bind_thm ("equiv_ratrel_iff", [equiv_ratrel, UNIV_I, UNIV_I] MRS eq_equiv_class_iff);
Goalw [prat_def,ratrel_def,quotient_def] "ratrel``{(x,y)}:prat";
by (Blast_tac 1);
qed "ratrel_in_prat";
Goal "inj_on Abs_prat prat";
by (rtac inj_on_inverseI 1);
by (etac Abs_prat_inverse 1);
qed "inj_on_Abs_prat";
Addsimps [equiv_ratrel_iff,inj_on_Abs_prat RS inj_on_iff,
ratrel_iff, ratrel_in_prat, Abs_prat_inverse];
Addsimps [equiv_ratrel RS eq_equiv_class_iff];
bind_thm ("eq_ratrelD", equiv_ratrel RSN (2,eq_equiv_class));
Goal "inj(Rep_prat)";
by (rtac inj_inverseI 1);
by (rtac Rep_prat_inverse 1);
qed "inj_Rep_prat";
(** prat_of_pnat: the injection from pnat to prat **)
Goal "inj(prat_of_pnat)";
by (rtac injI 1);
by (rewtac prat_of_pnat_def);
by (dtac (inj_on_Abs_prat RS inj_onD) 1);
by (REPEAT (rtac ratrel_in_prat 1));
by (dtac eq_equiv_class 1);
by (rtac equiv_ratrel 1);
by (Fast_tac 1);
by Safe_tac;
by (Asm_full_simp_tac 1);
qed "inj_prat_of_pnat";
val [prem] = Goal
"(!!x y. z = Abs_prat(ratrel``{(x,y)}) ==> P) ==> P";
by (res_inst_tac [("x1","z")]
(rewrite_rule [prat_def] Rep_prat RS quotientE) 1);
by (dres_inst_tac [("f","Abs_prat")] arg_cong 1);
by (res_inst_tac [("p","x")] PairE 1);
by (rtac prem 1);
by (asm_full_simp_tac (simpset() addsimps [Rep_prat_inverse]) 1);
qed "eq_Abs_prat";
(**** qinv: inverse on prat ****)
Goalw [congruent_def] "congruent ratrel (%(x,y). ratrel``{(y,x)})";
by (auto_tac (claset(), simpset() addsimps [pnat_mult_commute]));
qed "qinv_congruent";
Goalw [qinv_def]
"qinv (Abs_prat(ratrel``{(x,y)})) = Abs_prat(ratrel `` {(y,x)})";
by (simp_tac (simpset() addsimps
[equiv_ratrel RS UN_equiv_class, qinv_congruent]) 1);
qed "qinv";
Goal "qinv (qinv z) = z";
by (res_inst_tac [("z","z")] eq_Abs_prat 1);
by (asm_simp_tac (simpset() addsimps [qinv]) 1);
qed "qinv_qinv";
Goal "inj(qinv)";
by (rtac injI 1);
by (dres_inst_tac [("f","qinv")] arg_cong 1);
by (asm_full_simp_tac (simpset() addsimps [qinv_qinv]) 1);
qed "inj_qinv";
Goalw [prat_of_pnat_def]
"qinv(prat_of_pnat (Abs_pnat 1')) = prat_of_pnat (Abs_pnat 1')";
by (simp_tac (simpset() addsimps [qinv]) 1);
qed "qinv_1";
Goal "!!(x1::pnat). [| x1 * y2 = x2 * y1 |] ==> \
\ (x * y1 + x1 * ya) * (ya * y2) = (x * y2 + x2 * ya) * (ya * y1)";
by (auto_tac (claset() addSIs [pnat_same_multI2],
simpset() addsimps [pnat_add_mult_distrib,
pnat_mult_assoc]));
by (res_inst_tac [("n1","y2")] (pnat_mult_commute RS subst) 1);
by (auto_tac (claset() addIs [pnat_add_left_cancel RS iffD2],simpset() addsimps pnat_mult_ac));
by (res_inst_tac [("y1","x1")] (pnat_mult_left_commute RS subst) 1);
by (res_inst_tac [("y1","x1")] (pnat_mult_left_commute RS ssubst) 1);
by (auto_tac (claset(),simpset() addsimps [pnat_mult_assoc RS sym]));
qed "prat_add_congruent2_lemma";
Goal "congruent2 ratrel (%p1 p2. \
\ (%(x1,y1). (%(x2,y2). ratrel``{(x1*y2 + x2*y1, y1*y2)}) p2) p1)";
by (rtac (equiv_ratrel RS congruent2_commuteI) 1);
by (auto_tac (claset() delrules [equalityI],
simpset() addsimps [prat_add_congruent2_lemma]));
by (asm_simp_tac (simpset() addsimps [pnat_mult_commute,pnat_add_commute]) 1);
qed "prat_add_congruent2";
Goalw [prat_add_def]
"Abs_prat((ratrel``{(x1,y1)})) + Abs_prat((ratrel``{(x2,y2)})) = \
\ Abs_prat(ratrel `` {(x1*y2 + x2*y1, y1*y2)})";
by (simp_tac (simpset() addsimps [UN_UN_split_split_eq, prat_add_congruent2,
equiv_ratrel RS UN_equiv_class2]) 1);
qed "prat_add";
Goal "(z::prat) + w = w + z";
by (res_inst_tac [("z","z")] eq_Abs_prat 1);
by (res_inst_tac [("z","w")] eq_Abs_prat 1);
by (asm_simp_tac
(simpset() addsimps [prat_add] @ pnat_add_ac @ pnat_mult_ac) 1);
qed "prat_add_commute";
Goal "((z1::prat) + z2) + z3 = z1 + (z2 + z3)";
by (res_inst_tac [("z","z1")] eq_Abs_prat 1);
by (res_inst_tac [("z","z2")] eq_Abs_prat 1);
by (res_inst_tac [("z","z3")] eq_Abs_prat 1);
by (asm_simp_tac (simpset() addsimps [pnat_add_mult_distrib2,prat_add] @
pnat_add_ac @ pnat_mult_ac) 1);
qed "prat_add_assoc";
(*For AC rewriting*)
Goal "(z1::prat) + (z2 + z3) = z2 + (z1 + z3)";
by (rtac (prat_add_commute RS trans) 1);
by (rtac (prat_add_assoc RS trans) 1);
by (rtac (prat_add_commute RS arg_cong) 1);
qed "prat_add_left_commute";
(* Positive Rational addition is an AC operator *)
bind_thms ("prat_add_ac", [prat_add_assoc, prat_add_commute, prat_add_left_commute]);
(*** Congruence property for multiplication ***)
Goalw [congruent2_def]
"congruent2 ratrel (%p1 p2. \
\ (%(x1,y1). (%(x2,y2). ratrel``{(x1*x2, y1*y2)}) p2) p1)";
(*Proof via congruent2_commuteI seems longer*)
by (Clarify_tac 1);
by (asm_simp_tac (simpset() addsimps [pnat_mult_assoc]) 1);
(*The rest should be trivial, but rearranging terms is hard*)
by (res_inst_tac [("x1","x1a")] (pnat_mult_left_commute RS ssubst) 1);
by (asm_simp_tac (simpset() addsimps [pnat_mult_assoc RS sym]) 1);
by (asm_simp_tac (simpset() addsimps pnat_mult_ac) 1);
qed "pnat_mult_congruent2";
Goalw [prat_mult_def]
"Abs_prat(ratrel``{(x1,y1)}) * Abs_prat(ratrel``{(x2,y2)}) = \
\ Abs_prat(ratrel``{(x1*x2, y1*y2)})";
by (asm_simp_tac
(simpset() addsimps [UN_UN_split_split_eq, pnat_mult_congruent2,
equiv_ratrel RS UN_equiv_class2]) 1);
qed "prat_mult";
Goal "(z::prat) * w = w * z";
by (res_inst_tac [("z","z")] eq_Abs_prat 1);
by (res_inst_tac [("z","w")] eq_Abs_prat 1);
by (asm_simp_tac (simpset() addsimps pnat_mult_ac @ [prat_mult]) 1);
qed "prat_mult_commute";
Goal "((z1::prat) * z2) * z3 = z1 * (z2 * z3)";
by (res_inst_tac [("z","z1")] eq_Abs_prat 1);
by (res_inst_tac [("z","z2")] eq_Abs_prat 1);
by (res_inst_tac [("z","z3")] eq_Abs_prat 1);
by (asm_simp_tac (simpset() addsimps [prat_mult, pnat_mult_assoc]) 1);
qed "prat_mult_assoc";
(*For AC rewriting*)
Goal "(x::prat)*(y*z)=y*(x*z)";
by (rtac (prat_mult_commute RS trans) 1);
by (rtac (prat_mult_assoc RS trans) 1);
by (rtac (prat_mult_commute RS arg_cong) 1);
qed "prat_mult_left_commute";
(*Positive Rational multiplication is an AC operator*)
bind_thms ("prat_mult_ac", [prat_mult_assoc,
prat_mult_commute,prat_mult_left_commute]);
Goalw [prat_of_pnat_def]
"(prat_of_pnat (Abs_pnat 1')) * z = z";
by (res_inst_tac [("z","z")] eq_Abs_prat 1);
by (asm_full_simp_tac (simpset() addsimps [prat_mult] @ pnat_mult_ac) 1);
qed "prat_mult_1";
Goalw [prat_of_pnat_def]
"z * (prat_of_pnat (Abs_pnat 1')) = z";
by (res_inst_tac [("z","z")] eq_Abs_prat 1);
by (asm_full_simp_tac (simpset() addsimps [prat_mult] @ pnat_mult_ac) 1);
qed "prat_mult_1_right";
Goalw [prat_of_pnat_def]
"prat_of_pnat ((z1::pnat) + z2) = \
\ prat_of_pnat z1 + prat_of_pnat z2";
by (asm_simp_tac (simpset() addsimps [prat_add,
pnat_add_mult_distrib,pnat_mult_1]) 1);
qed "prat_of_pnat_add";
Goalw [prat_of_pnat_def]
"prat_of_pnat ((z1::pnat) * z2) = \
\ prat_of_pnat z1 * prat_of_pnat z2";
by (asm_simp_tac (simpset() addsimps [prat_mult, pnat_mult_1]) 1);
qed "prat_of_pnat_mult";
(*** prat_mult and qinv ***)
Goalw [prat_def,prat_of_pnat_def]
"qinv (q) * q = prat_of_pnat (Abs_pnat 1')";
by (res_inst_tac [("z","q")] eq_Abs_prat 1);
by (asm_full_simp_tac (simpset() addsimps [qinv,
prat_mult,pnat_mult_1,pnat_mult_1_left, pnat_mult_commute]) 1);
qed "prat_mult_qinv";
Goal "q * qinv (q) = prat_of_pnat (Abs_pnat 1')";
by (rtac (prat_mult_commute RS subst) 1);
by (simp_tac (simpset() addsimps [prat_mult_qinv]) 1);
qed "prat_mult_qinv_right";
Goal "EX y. (x::prat) * y = prat_of_pnat (Abs_pnat 1')";
by (fast_tac (claset() addIs [prat_mult_qinv_right]) 1);
qed "prat_qinv_ex";
Goal "EX! y. (x::prat) * y = prat_of_pnat (Abs_pnat 1')";
by (auto_tac (claset() addIs [prat_mult_qinv_right],simpset()));
by (dres_inst_tac [("f","%x. ya*x")] arg_cong 1);
by (asm_full_simp_tac (simpset() addsimps [prat_mult_assoc RS sym]) 1);
by (asm_full_simp_tac (simpset() addsimps [prat_mult_commute,
prat_mult_1,prat_mult_1_right]) 1);
qed "prat_qinv_ex1";
Goal "EX! y. y * (x::prat) = prat_of_pnat (Abs_pnat 1')";
by (auto_tac (claset() addIs [prat_mult_qinv],simpset()));
by (dres_inst_tac [("f","%x. x*ya")] arg_cong 1);
by (asm_full_simp_tac (simpset() addsimps [prat_mult_assoc]) 1);
by (asm_full_simp_tac (simpset() addsimps [prat_mult_commute,
prat_mult_1,prat_mult_1_right]) 1);
qed "prat_qinv_left_ex1";
Goal "x * y = prat_of_pnat (Abs_pnat 1') ==> x = qinv y";
by (cut_inst_tac [("q","y")] prat_mult_qinv 1);
by (res_inst_tac [("x1","y")] (prat_qinv_left_ex1 RS ex1E) 1);
by (Blast_tac 1);
qed "prat_mult_inv_qinv";
Goal "EX y. x = qinv y";
by (cut_inst_tac [("x","x")] prat_qinv_ex 1);
by (etac exE 1 THEN dtac prat_mult_inv_qinv 1);
by (Fast_tac 1);
qed "prat_as_inverse_ex";
Goal "qinv(x*y) = qinv(x)*qinv(y)";
by (res_inst_tac [("z","x")] eq_Abs_prat 1);
by (res_inst_tac [("z","y")] eq_Abs_prat 1);
by (auto_tac (claset(),simpset() addsimps [qinv,prat_mult]));
qed "qinv_mult_eq";
(** Lemmas **)
Goal "((z1::prat) + z2) * w = (z1 * w) + (z2 * w)";
by (res_inst_tac [("z","z1")] eq_Abs_prat 1);
by (res_inst_tac [("z","z2")] eq_Abs_prat 1);
by (res_inst_tac [("z","w")] eq_Abs_prat 1);
by (asm_simp_tac
(simpset() addsimps [pnat_add_mult_distrib2, prat_add, prat_mult] @
pnat_add_ac @ pnat_mult_ac) 1);
qed "prat_add_mult_distrib";
val prat_mult_commute'= read_instantiate [("z","w")] prat_mult_commute;
Goal "(w::prat) * (z1 + z2) = (w * z1) + (w * z2)";
by (simp_tac (simpset() addsimps [prat_mult_commute',prat_add_mult_distrib]) 1);
qed "prat_add_mult_distrib2";
Addsimps [prat_mult_1, prat_mult_1_right,
prat_mult_qinv, prat_mult_qinv_right];
(*** theorems for ordering ***)
(* prove introduction and elimination rules for prat_less *)
Goalw [prat_less_def]
"Q1 < (Q2::prat) = (EX Q3. Q1 + Q3 = Q2)";
by (Fast_tac 1);
qed "prat_less_iff";
Goalw [prat_less_def]
"!!(Q1::prat). Q1 + Q3 = Q2 ==> Q1 < Q2";
by (Fast_tac 1);
qed "prat_lessI";
(* ordering on positive fractions in terms of existence of sum *)
Goalw [prat_less_def]
"Q1 < (Q2::prat) --> (EX Q3. Q1 + Q3 = Q2)";
by (Fast_tac 1);
qed "prat_lessE_lemma";
Goal "!!P. [| Q1 < (Q2::prat); \
\ !! (Q3::prat). Q1 + Q3 = Q2 ==> P |] \
\ ==> P";
by (dtac (prat_lessE_lemma RS mp) 1);
by Auto_tac;
qed "prat_lessE";
(* qless is a strong order i.e nonreflexive and transitive *)
Goal "!!(q1::prat). [| q1 < q2; q2 < q3 |] ==> q1 < q3";
by (REPEAT(dtac (prat_lessE_lemma RS mp) 1));
by (REPEAT(etac exE 1));
by (hyp_subst_tac 1);
by (res_inst_tac [("Q3.0","Q3 + Q3a")] prat_lessI 1);
by (auto_tac (claset(),simpset() addsimps [prat_add_assoc]));
qed "prat_less_trans";
Goal "~q < (q::prat)";
by (EVERY1[rtac notI, dtac (prat_lessE_lemma RS mp)]);
by (res_inst_tac [("z","q")] eq_Abs_prat 1);
by (res_inst_tac [("z","Q3")] eq_Abs_prat 1);
by (etac exE 1 THEN res_inst_tac [("z","Q3a")] eq_Abs_prat 1);
by (REPEAT(hyp_subst_tac 1));
by (asm_full_simp_tac (simpset() addsimps [prat_add,
pnat_no_add_ident,pnat_add_mult_distrib2] @ pnat_mult_ac) 1);
qed "prat_less_not_refl";
(*** y < y ==> P ***)
bind_thm("prat_less_irrefl",prat_less_not_refl RS notE);
Goal "!! (q1::prat). q1 < q2 ==> ~ q2 < q1";
by (rtac notI 1);
by (dtac prat_less_trans 1 THEN assume_tac 1);
by (asm_full_simp_tac (simpset() addsimps [prat_less_not_refl]) 1);
qed "prat_less_not_sym";
(* [| x < y; ~P ==> y < x |] ==> P *)
bind_thm ("prat_less_asym", prat_less_not_sym RS contrapos_np);
(* half of positive fraction exists- Gleason p. 120- Proposition 9-2.6(i)*)
Goal "!(q::prat). EX x. x + x = q";
by (rtac allI 1);
by (res_inst_tac [("z","q")] eq_Abs_prat 1);
by (res_inst_tac [("x","Abs_prat (ratrel `` {(x, y+y)})")] exI 1);
by (auto_tac (claset(),
simpset() addsimps
[prat_add,pnat_mult_assoc RS sym,pnat_add_mult_distrib,
pnat_add_mult_distrib2]));
qed "lemma_prat_dense";
Goal "EX (x::prat). x + x = q";
by (res_inst_tac [("z","q")] eq_Abs_prat 1);
by (res_inst_tac [("x","Abs_prat (ratrel `` {(x, y+y)})")] exI 1);
by (auto_tac (claset(),simpset() addsimps
[prat_add,pnat_mult_assoc RS sym,pnat_add_mult_distrib,
pnat_add_mult_distrib2]));
qed "prat_lemma_dense";
(* there exists a number between any two positive fractions *)
(* Gleason p. 120- Proposition 9-2.6(iv) *)
Goalw [prat_less_def]
"!! (q1::prat). q1 < q2 ==> EX x. q1 < x & x < q2";
by (auto_tac (claset() addIs [lemma_prat_dense],simpset()));
by (res_inst_tac [("x","T")] (lemma_prat_dense RS allE) 1);
by (etac exE 1);
by (res_inst_tac [("x","q1 + x")] exI 1);
by (auto_tac (claset() addIs [prat_lemma_dense],
simpset() addsimps [prat_add_assoc]));
qed "prat_dense";
(* ordering of addition for positive fractions *)
Goalw [prat_less_def] "!!(q1::prat). q1 < q2 ==> q1 + x < q2 + x";
by (Step_tac 1);
by (res_inst_tac [("x","T")] exI 1);
by (auto_tac (claset(),simpset() addsimps prat_add_ac));
qed "prat_add_less2_mono1";
Goal "!!(q1::prat). q1 < q2 ==> x + q1 < x + q2";
by (auto_tac (claset() addIs [prat_add_less2_mono1],
simpset() addsimps [prat_add_commute]));
qed "prat_add_less2_mono2";
(* ordering of multiplication for positive fractions *)
Goalw [prat_less_def]
"!!(q1::prat). q1 < q2 ==> q1 * x < q2 * x";
by (Step_tac 1);
by (res_inst_tac [("x","T*x")] exI 1);
by (auto_tac (claset(),simpset() addsimps [prat_add_mult_distrib]));
qed "prat_mult_less2_mono1";
Goal "!!(q1::prat). q1 < q2 ==> x * q1 < x * q2";
by (auto_tac (claset() addDs [prat_mult_less2_mono1],
simpset() addsimps [prat_mult_commute]));
qed "prat_mult_left_less2_mono1";
Goal "!!(a1::prat). a1 < a2 ==> a1 * b + a2 * c < a2 * (b + c)";
by (auto_tac (claset() addSIs [prat_add_less2_mono1,prat_mult_less2_mono1],
simpset() addsimps [prat_add_mult_distrib2]));
qed "lemma_prat_add_mult_mono";
(* there is no smallest positive fraction *)
Goalw [prat_less_def] "EX (x::prat). x < y";
by (cut_facts_tac [lemma_prat_dense] 1);
by (Fast_tac 1);
qed "qless_Ex";
(* lemma for proving $< is linear *)
Goalw [prat_def,prat_less_def]
"ratrel `` {(x, y * ya)} : {p::(pnat*pnat).True}//ratrel";
by (asm_full_simp_tac (simpset() addsimps [ratrel_def,quotient_def]) 1);
by (Blast_tac 1);
qed "lemma_prat_less_linear";
(* linearity of < -- Gleason p. 120 - Proposition 9-2.6 *)
(*** FIXME Proof long ***)
Goalw [prat_less_def]
"(q1::prat) < q2 | q1 = q2 | q2 < q1";
by (res_inst_tac [("z","q1")] eq_Abs_prat 1);
by (res_inst_tac [("z","q2")] eq_Abs_prat 1);
by (Step_tac 1 THEN REPEAT(dtac (not_ex RS iffD1) 1)
THEN Auto_tac);
by (cut_inst_tac [("z1.0","x*ya"), ("z2.0","xa*y")] pnat_linear_Ex_eq 1);
by (EVERY1[etac disjE,etac exE]);
by (eres_inst_tac
[("x","Abs_prat(ratrel``{(xb,ya*y)})")] allE 1);
by (asm_full_simp_tac
(simpset() addsimps [prat_add, pnat_mult_assoc
RS sym,pnat_add_mult_distrib RS sym]) 1);
by (EVERY1[asm_full_simp_tac (simpset() addsimps pnat_mult_ac),
etac disjE, assume_tac, etac exE]);
by (thin_tac "!T. Abs_prat (ratrel `` {(x, y)}) + T ~= \
\ Abs_prat (ratrel `` {(xa, ya)})" 1);
by (eres_inst_tac [("x","Abs_prat(ratrel``{(xb,y*ya)})")] allE 1);
by (asm_full_simp_tac (simpset() addsimps [prat_add,
pnat_mult_assoc RS sym,pnat_add_mult_distrib RS sym]) 1);
by (asm_full_simp_tac (simpset() addsimps pnat_mult_ac) 1);
qed "prat_linear";
Goal "!!(q1::prat). [| q1 < q2 ==> P; q1 = q2 ==> P; \
\ q2 < q1 ==> P |] ==> P";
by (cut_inst_tac [("q1.0","q1"),("q2.0","q2")] prat_linear 1);
by Auto_tac;
qed "prat_linear_less2";
(* Gleason p. 120 -- 9-2.6 (iv) *)
Goal "[| q1 < q2; qinv(q1) = qinv(q2) |] ==> P";
by (cut_inst_tac [("x","qinv (q2)"),("q1.0","q1"), ("q2.0","q2")]
prat_mult_less2_mono1 1);
by (assume_tac 1);
by (Asm_full_simp_tac 1 THEN dtac sym 1);
by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl]));
qed "lemma1_qinv_prat_less";
Goal "[| q1 < q2; qinv(q1) < qinv(q2) |] ==> P";
by (cut_inst_tac [("x","qinv (q2)"),("q1.0","q1"), ("q2.0","q2")]
prat_mult_less2_mono1 1);
by (assume_tac 1);
by (cut_inst_tac [("x","q1"),("q1.0","qinv (q1)"), ("q2.0","qinv (q2)")]
prat_mult_left_less2_mono1 1);
by Auto_tac;
by (dres_inst_tac [("q2.0","prat_of_pnat (Abs_pnat 1')")] prat_less_trans 1);
by (auto_tac (claset(),simpset() addsimps
[prat_less_not_refl]));
qed "lemma2_qinv_prat_less";
Goal "q1 < q2 ==> qinv (q2) < qinv (q1)";
by (res_inst_tac [("q2.0","qinv q1"), ("q1.0","qinv q2")] prat_linear_less2 1);
by (auto_tac (claset() addEs [lemma1_qinv_prat_less,
lemma2_qinv_prat_less],simpset()));
qed "qinv_prat_less";
Goal "q1 < prat_of_pnat (Abs_pnat 1') \
\ ==> prat_of_pnat (Abs_pnat 1') < qinv(q1)";
by (dtac qinv_prat_less 1);
by (full_simp_tac (simpset() addsimps [qinv_1]) 1);
qed "prat_qinv_gt_1";
Goalw [pnat_one_def]
"q1 < prat_of_pnat 1p ==> prat_of_pnat 1p < qinv(q1)";
by (etac prat_qinv_gt_1 1);
qed "prat_qinv_is_gt_1";
Goalw [prat_less_def]
"prat_of_pnat (Abs_pnat 1') < prat_of_pnat (Abs_pnat 1') \
\ + prat_of_pnat (Abs_pnat 1')";
by (Fast_tac 1);
qed "prat_less_1_2";
Goal "qinv(prat_of_pnat (Abs_pnat 1') + \
\ prat_of_pnat (Abs_pnat 1')) < prat_of_pnat (Abs_pnat 1')";
by (cut_facts_tac [prat_less_1_2 RS qinv_prat_less] 1);
by (asm_full_simp_tac (simpset() addsimps [qinv_1]) 1);
qed "prat_less_qinv_2_1";
Goal "!!(x::prat). x < y ==> x*qinv(y) < prat_of_pnat (Abs_pnat 1')";
by (dres_inst_tac [("x","qinv(y)")] prat_mult_less2_mono1 1);
by (Asm_full_simp_tac 1);
qed "prat_mult_qinv_less_1";
Goal "(x::prat) < x + x";
by (cut_inst_tac [("x","x")]
(prat_less_1_2 RS prat_mult_left_less2_mono1) 1);
by (asm_full_simp_tac (simpset() addsimps
[prat_add_mult_distrib2]) 1);
qed "prat_self_less_add_self";
Goalw [prat_less_def] "(x::prat) < y + x";
by (res_inst_tac [("x","y")] exI 1);
by (simp_tac (simpset() addsimps [prat_add_commute]) 1);
qed "prat_self_less_add_right";
Goal "(x::prat) < x + y";
by (rtac (prat_add_commute RS subst) 1);
by (simp_tac (simpset() addsimps [prat_self_less_add_right]) 1);
qed "prat_self_less_add_left";
Goalw [prat_less_def] "prat_of_pnat 1p < y ==> (x::prat) < x * y";
by (auto_tac (claset(),simpset() addsimps [pnat_one_def,
prat_add_mult_distrib2]));
qed "prat_self_less_mult_right";
(*** Properties of <= ***)
Goalw [prat_le_def] "~(w < z) ==> z <= (w::prat)";
by (assume_tac 1);
qed "prat_leI";
Goalw [prat_le_def] "z<=w ==> ~(w<(z::prat))";
by (assume_tac 1);
qed "prat_leD";
bind_thm ("prat_leE", make_elim prat_leD);
Goal "(~(w < z)) = (z <= (w::prat))";
by (fast_tac (claset() addSIs [prat_leI,prat_leD]) 1);
qed "prat_less_le_iff";
Goalw [prat_le_def] "~ z <= w ==> w<(z::prat)";
by (Fast_tac 1);
qed "not_prat_leE";
Goalw [prat_le_def] "z < w ==> z <= (w::prat)";
by (fast_tac (claset() addEs [prat_less_asym]) 1);
qed "prat_less_imp_le";
Goalw [prat_le_def] "!!(x::prat). x <= y ==> x < y | x = y";
by (cut_facts_tac [prat_linear] 1);
by (fast_tac (claset() addEs [prat_less_irrefl,prat_less_asym]) 1);
qed "prat_le_imp_less_or_eq";
Goalw [prat_le_def] "z<w | z=w ==> z <=(w::prat)";
by (cut_facts_tac [prat_linear] 1);
by (fast_tac (claset() addEs [prat_less_irrefl,prat_less_asym]) 1);
qed "prat_less_or_eq_imp_le";
Goal "(x <= (y::prat)) = (x < y | x=y)";
by (REPEAT(ares_tac [iffI, prat_less_or_eq_imp_le, prat_le_imp_less_or_eq] 1));
qed "prat_le_eq_less_or_eq";
Goal "w <= (w::prat)";
by (simp_tac (simpset() addsimps [prat_le_eq_less_or_eq]) 1);
qed "prat_le_refl";
Goal "[| i <= j; j < k |] ==> i < (k::prat)";
by (dtac prat_le_imp_less_or_eq 1);
by (fast_tac (claset() addIs [prat_less_trans]) 1);
qed "prat_le_less_trans";
Goal "[| i <= j; j <= k |] ==> i <= (k::prat)";
by (EVERY1 [dtac prat_le_imp_less_or_eq, dtac prat_le_imp_less_or_eq,
rtac prat_less_or_eq_imp_le, fast_tac (claset() addIs [prat_less_trans])]);
qed "prat_le_trans";
Goal "[| ~ y < x; y ~= x |] ==> x < (y::prat)";
by (rtac not_prat_leE 1);
by (fast_tac (claset() addDs [prat_le_imp_less_or_eq]) 1);
qed "not_less_not_eq_prat_less";
Goalw [prat_less_def]
"[| x1 < y1; x2 < y2 |] ==> x1 + x2 < y1 + (y2::prat)";
by (REPEAT(etac exE 1));
by (res_inst_tac [("x","T+Ta")] exI 1);
by (auto_tac (claset(),simpset() addsimps prat_add_ac));
qed "prat_add_less_mono";
Goalw [prat_less_def]
"[| x1 < y1; x2 < y2 |] ==> x1 * x2 < y1 * (y2::prat)";
by (REPEAT(etac exE 1));
by (res_inst_tac [("x","T*Ta+T*x2+x1*Ta")] exI 1);
by (auto_tac (claset(),
simpset() addsimps prat_add_ac @
[prat_add_mult_distrib,prat_add_mult_distrib2]));
qed "prat_mult_less_mono";
(* more prat_le *)
Goal "!!(q1::prat). q1 <= q2 ==> x * q1 <= x * q2";
by (dtac prat_le_imp_less_or_eq 1);
by (Step_tac 1);
by (auto_tac (claset() addSIs [prat_le_refl, prat_less_imp_le,
prat_mult_left_less2_mono1],
simpset()));
qed "prat_mult_left_le2_mono1";
Goal "!!(q1::prat). q1 <= q2 ==> q1 * x <= q2 * x";
by (auto_tac (claset() addDs [prat_mult_left_le2_mono1],
simpset() addsimps [prat_mult_commute]));
qed "prat_mult_le2_mono1";
Goal "q1 <= q2 ==> qinv (q2) <= qinv (q1)";
by (dtac prat_le_imp_less_or_eq 1);
by (Step_tac 1);
by (auto_tac (claset() addSIs [prat_le_refl, prat_less_imp_le,qinv_prat_less],
simpset()));
qed "qinv_prat_le";
Goal "!!(q1::prat). q1 <= q2 ==> x + q1 <= x + q2";
by (dtac prat_le_imp_less_or_eq 1);
by (Step_tac 1);
by (auto_tac (claset() addSIs [prat_le_refl,
prat_less_imp_le,prat_add_less2_mono1],
simpset() addsimps [prat_add_commute]));
qed "prat_add_left_le2_mono1";
Goal "!!(q1::prat). q1 <= q2 ==> q1 + x <= q2 + x";
by (auto_tac (claset() addDs [prat_add_left_le2_mono1],
simpset() addsimps [prat_add_commute]));
qed "prat_add_le2_mono1";
Goal "!!k l::prat. [|i<=j; k<=l |] ==> i + k <= j + l";
by (etac (prat_add_le2_mono1 RS prat_le_trans) 1);
by (simp_tac (simpset() addsimps [prat_add_commute]) 1);
(*j moves to the end because it is free while k, l are bound*)
by (etac prat_add_le2_mono1 1);
qed "prat_add_le_mono";
Goal "!!(x::prat). x + y < z + y ==> x < z";
by (rtac ccontr 1);
by (etac (prat_leI RS prat_le_imp_less_or_eq RS disjE) 1);
by (dres_inst_tac [("x","y"),("q1.0","z")] prat_add_less2_mono1 1);
by (auto_tac (claset() addIs [prat_less_asym],
simpset() addsimps [prat_less_not_refl]));
qed "prat_add_right_less_cancel";
Goal "!!(x::prat). y + x < y + z ==> x < z";
by (res_inst_tac [("y","y")] prat_add_right_less_cancel 1);
by (asm_full_simp_tac (simpset() addsimps [prat_add_commute]) 1);
qed "prat_add_left_less_cancel";
(*** lemmas required for lemma_gleason9_34 in PReal : w*y > y/z ***)
Goalw [prat_of_pnat_def]
"Abs_prat(ratrel``{(x,y)}) = (prat_of_pnat x)*qinv(prat_of_pnat y)";
by (auto_tac (claset(),simpset() addsimps [prat_mult,qinv,pnat_mult_1_left,
pnat_mult_1]));
qed "Abs_prat_mult_qinv";
Goal "Abs_prat(ratrel``{(x,y)}) <= Abs_prat(ratrel``{(x,Abs_pnat 1')})";
by (simp_tac (simpset() addsimps [Abs_prat_mult_qinv]) 1);
by (rtac prat_mult_left_le2_mono1 1);
by (rtac qinv_prat_le 1);
by (pnat_ind_tac "y" 1);
by (dres_inst_tac [("x","prat_of_pnat (Abs_pnat 1')")] prat_add_le2_mono1 2);
by (cut_facts_tac [prat_less_1_2 RS prat_less_imp_le] 2);
by (auto_tac (claset() addIs [prat_le_trans],
simpset() addsimps [prat_le_refl,
pSuc_is_plus_one,pnat_one_def,prat_of_pnat_add]));
qed "lemma_Abs_prat_le1";
Goal "Abs_prat(ratrel``{(x,Abs_pnat 1')}) <= Abs_prat(ratrel``{(x*y,Abs_pnat 1')})";
by (simp_tac (simpset() addsimps [Abs_prat_mult_qinv]) 1);
by (rtac prat_mult_le2_mono1 1);
by (pnat_ind_tac "y" 1);
by (dres_inst_tac [("x","prat_of_pnat x")] prat_add_le2_mono1 2);
by (cut_inst_tac [("z","prat_of_pnat x")] (prat_self_less_add_self
RS prat_less_imp_le) 2);
by (auto_tac (claset() addIs [prat_le_trans],
simpset() addsimps [prat_le_refl,
pSuc_is_plus_one,pnat_one_def,prat_add_mult_distrib2,
prat_of_pnat_add,prat_of_pnat_mult]));
qed "lemma_Abs_prat_le2";
Goal "Abs_prat(ratrel``{(x,z)}) <= Abs_prat(ratrel``{(x*y,Abs_pnat 1')})";
by (fast_tac (claset() addIs [prat_le_trans,
lemma_Abs_prat_le1,lemma_Abs_prat_le2]) 1);
qed "lemma_Abs_prat_le3";
Goal "Abs_prat(ratrel``{(x*y,Abs_pnat 1')}) * Abs_prat(ratrel``{(w,x)}) = \
\ Abs_prat(ratrel``{(w*y,Abs_pnat 1')})";
by (full_simp_tac (simpset() addsimps [prat_mult,
pnat_mult_1,pnat_mult_1_left] @ pnat_mult_ac) 1);
qed "pre_lemma_gleason9_34";
Goal "Abs_prat(ratrel``{(y*x,Abs_pnat 1'*y)}) = \
\ Abs_prat(ratrel``{(x,Abs_pnat 1')})";
by (auto_tac (claset(),
simpset() addsimps [pnat_mult_1,pnat_mult_1_left] @ pnat_mult_ac));
qed "pre_lemma_gleason9_34b";
Goal "(prat_of_pnat n < prat_of_pnat m) = (n < m)";
by (auto_tac (claset(),simpset() addsimps [prat_less_def,
pnat_less_iff,prat_of_pnat_add]));
by (res_inst_tac [("z","T")] eq_Abs_prat 1);
by (auto_tac (claset() addDs [pnat_eq_lessI],
simpset() addsimps [prat_add,pnat_mult_1,
pnat_mult_1_left,prat_of_pnat_def,pnat_less_iff RS sym]));
qed "prat_of_pnat_less_iff";
Addsimps [prat_of_pnat_less_iff];
(*------------------------------------------------------------------*)
(*** prove witness that will be required to prove non-emptiness ***)
(*** of preal type as defined using Dedekind Sections in PReal ***)
(*** Show that exists positive real `one' ***)
Goal "EX q. q: {x::prat. x < prat_of_pnat (Abs_pnat 1')}";
by (fast_tac (claset() addIs [prat_less_qinv_2_1]) 1);
qed "lemma_prat_less_1_memEx";
Goal "{x::prat. x < prat_of_pnat (Abs_pnat 1')} ~= {}";
by (rtac notI 1);
by (cut_facts_tac [lemma_prat_less_1_memEx] 1);
by (Asm_full_simp_tac 1);
qed "lemma_prat_less_1_set_non_empty";
Goalw [psubset_def] "{} < {x::prat. x < prat_of_pnat (Abs_pnat 1')}";
by (asm_full_simp_tac (simpset() addsimps
[lemma_prat_less_1_set_non_empty RS not_sym]) 1);
qed "empty_set_psubset_lemma_prat_less_1_set";
(*** exists rational not in set --- prat_of_pnat (Abs_pnat 1) itself ***)
Goal "EX q. q ~: {x::prat. x < prat_of_pnat (Abs_pnat 1')}";
by (res_inst_tac [("x","prat_of_pnat (Abs_pnat 1')")] exI 1);
by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl]));
qed "lemma_prat_less_1_not_memEx";
Goal "{x::prat. x < prat_of_pnat (Abs_pnat 1')} ~= UNIV";
by (rtac notI 1);
by (cut_facts_tac [lemma_prat_less_1_not_memEx] 1);
by (Asm_full_simp_tac 1);
qed "lemma_prat_less_1_set_not_rat_set";
Goalw [psubset_def,subset_def]
"{x::prat. x < prat_of_pnat (Abs_pnat 1')} < UNIV";
by (asm_full_simp_tac
(simpset() addsimps [lemma_prat_less_1_set_not_rat_set,
lemma_prat_less_1_not_memEx]) 1);
qed "lemma_prat_less_1_set_psubset_rat_set";
(*** prove non_emptiness of type ***)
Goal "{x::prat. x < prat_of_pnat (Abs_pnat 1')} : {A. {} < A & \
\ A < UNIV & \
\ (!y: A. ((!z. z < y --> z: A) & \
\ (EX u: A. y < u)))}";
by (auto_tac (claset() addDs [prat_less_trans],
simpset() addsimps [empty_set_psubset_lemma_prat_less_1_set,
lemma_prat_less_1_set_psubset_rat_set]));
by (dtac prat_dense 1);
by (Fast_tac 1);
qed "preal_1";