(* Title : PRat.ML
Author : Jacques D. Fleuriot
Copyright : 1998 University of Cambridge
Description : The positive rationals
*)
open PRat;
Delrules [equalityI];
(*** Many theorems similar to those in Integ.thy ***)
(*** Proving that ratrel is an equivalence relation ***)
Goal
"!! x1. [| (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 x2. [| 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 thy
"[| 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 (stac surjective_pairing 1 THEN rtac (refl RS ratrelI) 1);
qed "ratrel_refl";
Goalw [equiv_def, refl_def, sym_def, trans_def]
"equiv {x::(pnat*pnat).True} ratrel";
by (fast_tac (claset() addSIs [ratrel_refl]
addSEs [sym, prat_trans_lemma]) 1);
qed "equiv_ratrel";
val equiv_ratrel_iff =
[TrueI, TrueI] MRS
([CollectI, CollectI] MRS
(equiv_ratrel RS 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];
val 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_pnat: the injection from pnat to prat **)
Goal "inj(prat_pnat)";
by (rtac injI 1);
by (rewtac prat_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_pnat";
(* lcp's original eq_Abs_Integ *)
val [prem] = goal thy
"(!!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 (%p. split (%x y. ratrel^^{(y,x)}) p)";
by Safe_tac;
by (asm_full_simp_tac (simpset() addsimps [pnat_mult_commute]) 1);
qed "qinv_congruent";
(*Resolve th against the corresponding facts for qinv*)
val qinv_ize = RSLIST [equiv_ratrel, qinv_congruent];
Goalw [qinv_def]
"qinv (Abs_prat(ratrel^^{(x,y)})) = Abs_prat(ratrel ^^ {(y,x)})";
by (res_inst_tac [("f","Abs_prat")] arg_cong 1);
by (simp_tac (simpset() addsimps
[ratrel_in_prat RS Abs_prat_inverse,qinv_ize UN_equiv_class]) 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_pnat_def] "qinv($# (Abs_pnat 1)) = $#(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. \
\ split (%x1 y1. split (%x2 y2. ratrel^^{(x1*y2 + x2*y1, y1*y2)}) p2) p1)";
by (rtac (equiv_ratrel RS congruent2_commuteI) 1);
by Safe_tac;
by (rewtac split_def);
by (asm_simp_tac (simpset() addsimps [pnat_mult_commute,pnat_add_commute]) 1);
by (auto_tac (claset(),simpset() addsimps [prat_add_congruent2_lemma]));
qed "prat_add_congruent2";
(*Resolve th against the corresponding facts for prat_add*)
val prat_add_ize = RSLIST [equiv_ratrel, 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 [prat_add_ize 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";
qed_goal "prat_add_left_commute" thy
"(z1::prat) + (z2 + z3) = z2 + (z1 + z3)"
(fn _ => [rtac (prat_add_commute RS trans) 1, rtac (prat_add_assoc RS trans) 1,
rtac (prat_add_commute RS arg_cong) 1]);
(* Positive Rational addition is an AC operator *)
val prat_add_ac = [prat_add_assoc, prat_add_commute, prat_add_left_commute];
(*** Congruence property for multiplication ***)
Goalw [congruent2_def]
"congruent2 ratrel (%p1 p2. \
\ split (%x1 y1. split (%x2 y2. ratrel^^{(x1*x2, y1*y2)}) p2) p1)";
(*Proof via congruent2_commuteI seems longer*)
by Safe_tac;
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";
(*Resolve th against the corresponding facts for pnat_mult*)
val prat_mult_ize = RSLIST [equiv_ratrel, 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 [prat_mult_ize 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*)
val prat_mult_ac = [prat_mult_assoc,prat_mult_commute,prat_mult_left_commute];
Goalw [prat_pnat_def] "($#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_pnat_def] "z * ($#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_pnat_def]
"$#((z1::pnat) + z2) = $#z1 + $#z2";
by (asm_simp_tac (simpset() addsimps [prat_add,
pnat_add_mult_distrib,pnat_mult_1]) 1);
qed "prat_pnat_add";
Goalw [prat_pnat_def]
"$#((z1::pnat) * z2) = $#z1 * $#z2";
by (asm_simp_tac (simpset() addsimps [prat_mult,
pnat_mult_1]) 1);
qed "prat_pnat_mult";
(*** prat_mult and qinv ***)
Goalw [prat_def,prat_pnat_def] "qinv (q) * q = $# (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) = $# (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 "? y. (x::prat) * y = $# Abs_pnat 1";
by (fast_tac (claset() addIs [prat_mult_qinv_right]) 1);
qed "prat_qinv_ex";
Goal "?! y. (x::prat) * y = $# 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 "?! y. y * (x::prat) = $# 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 = $# 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 "? 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 **)
qed_goal "prat_add_assoc_cong" thy
"!!z. (z::prat) + v = z' + v' ==> z + (v + w) = z' + (v' + w)"
(fn _ => [(asm_simp_tac (simpset() addsimps [prat_add_assoc RS sym]) 1)]);
qed_goal "prat_add_assoc_swap" thy "(z::prat) + (v + w) = v + (z + w)"
(fn _ => [(REPEAT (ares_tac [prat_add_commute RS prat_add_assoc_cong] 1))]);
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";
val prat_mult_simps = [prat_mult_1, prat_mult_1_right,
prat_mult_qinv, prat_mult_qinv_right];
Addsimps prat_mult_simps;
(*** 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
"!! Q1. [| 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 |] ==> P";
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_asym";
Goal "!! (q1::prat). q1 < q2 ==> ~ q2 < q1";
by (auto_tac (claset() addSDs [prat_less_asym],simpset()));
qed "prat_less_not_sym";
(* half of positive fraction exists- Gleason p. 120- Proposition 9-2.6(i)*)
Goal "!(q::prat). ? 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 "? (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 ==> ? 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";
(* there is no smallest positive fraction *)
Goalw [prat_less_def] "? (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::prat). [| 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::prat). [| 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","$#Abs_pnat 1")] prat_less_trans 1);
by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl]));
qed "lemma2_qinv_prat_less";
Goal
"!!(q1::prat). 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). q1 < $#Abs_pnat 1 ==> $#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). q1 < $#1p ==> $#1p < qinv(q1)";
by (etac prat_qinv_gt_1 1);
qed "prat_qinv_is_gt_1";
Goalw [prat_less_def] "$#Abs_pnat 1 < $#Abs_pnat 1 + $#Abs_pnat 1";
by (Fast_tac 1);
qed "prat_less_1_2";
Goal "qinv($#Abs_pnat 1 + $#Abs_pnat 1) < $#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) < $#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] "$#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";
val 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";
val prems = goal thy "!!i. [| 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::prat). [| i < j; j <= k |] ==> i < k";
by (dtac prat_le_imp_less_or_eq 1);
by (fast_tac (claset() addIs [prat_less_trans]) 1);
qed "prat_less_le_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 "[| z <= w; w <= z |] ==> z = (w::prat)";
by (EVERY1 [dtac prat_le_imp_less_or_eq, dtac prat_le_imp_less_or_eq,
fast_tac (claset() addEs [prat_less_irrefl,prat_less_asym])]);
qed "prat_le_anti_sym";
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]
"!!x. [| 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]
"!!x. [| 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::prat). 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_pnat_def] "Abs_prat(ratrel^^{(x,y)}) = $#x*qinv($#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","$#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_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","$#x")] prat_add_le2_mono1 2);
by (cut_inst_tac [("z","$#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_pnat_add,prat_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 "($#n < $#m) = (n < m)";
by (auto_tac (claset(),simpset() addsimps [prat_less_def,
pnat_less_iff,prat_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_pnat_def,pnat_less_iff RS sym]));
qed "prat_pnat_less_iff";
Addsimps [prat_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 "? q. q: {x::prat. x < $#Abs_pnat 1}";
by (fast_tac (claset() addIs [prat_less_qinv_2_1]) 1);
qed "lemma_prat_less_1_memEx";
Goal "{x::prat. x < $#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 < $#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 --- $#Abs_pnat 1 itself ***)
Goal "? q. q ~: {x::prat. x < $#Abs_pnat 1}";
by (res_inst_tac [("x","$#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 < $#Abs_pnat 1} ~= {q::prat. True}";
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 < $#Abs_pnat 1} < {q::prat. True}";
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 < $#Abs_pnat 1} : {A. {} < A & A < {q::prat. True} & \
\ (!y: A. ((!z. z < y --> z: A) & \
\ (? 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";