# HG changeset patch # User paulson # Date 933245097 -7200 # Node ID 48e235179ffbc5848afe4ee33516bc9aa731cf8f # Parent fdb397af4cabf947f9cf5178a38d03dfb820fae7 added parentheses to cope with a possible reduction of the precedence of unary minus diff -r fdb397af4cab -r 48e235179ffb src/HOL/HOL.thy --- a/src/HOL/HOL.thy Wed Jul 28 22:01:58 1999 +0200 +++ b/src/HOL/HOL.thy Thu Jul 29 12:44:57 1999 +0200 @@ -70,7 +70,7 @@ consts "+" :: ['a::plus, 'a] => 'a (infixl 65) "-" :: ['a::minus, 'a] => 'a (infixl 65) - uminus :: ['a::minus] => 'a ("- _" [100] 100) + uminus :: ['a::minus] => 'a ("- _" [71] 70) "*" :: ['a::times, 'a] => 'a (infixl 70) (*See Nat.thy for "^"*) diff -r fdb397af4cab -r 48e235179ffb src/HOL/Hoare/Arith2.ML --- a/src/HOL/Hoare/Arith2.ML Wed Jul 28 22:01:58 1999 +0200 +++ b/src/HOL/Hoare/Arith2.ML Thu Jul 29 12:44:57 1999 +0200 @@ -9,40 +9,26 @@ open Arith2; -(*** HOL lemmas ***) - - -val [prem1,prem2]=goal HOL.thy "[|~P ==> ~Q; Q|] ==> P"; -by (cut_facts_tac [prem1 COMP impI,prem2] 1); -by (Fast_tac 1); -val not_imp_swap=result(); - - - (*** cd ***) -val prems=goalw thy [cd_def] "0 cd n n n"; -by (cut_facts_tac prems 1); +Goalw [cd_def] "0 cd n n n"; by (Asm_simp_tac 1); qed "cd_nnn"; -val prems=goalw thy [cd_def] "[| cd x m n; 0 x<=m & x<=n"; -by (cut_facts_tac prems 1); +Goalw [cd_def] "[| cd x m n; 0 x<=m & x<=n"; by (blast_tac (claset() addIs [dvd_imp_le]) 1); qed "cd_le"; -val prems=goalw thy [cd_def] "cd x m n = cd x n m"; +Goalw [cd_def] "cd x m n = cd x n m"; by (Fast_tac 1); qed "cd_swap"; -val prems=goalw thy [cd_def] "n<=m ==> cd x m n = cd x (m-n) n"; -by (cut_facts_tac prems 1); +Goalw [cd_def] "n<=m ==> cd x m n = cd x (m-n) n"; by (blast_tac (claset() addIs [dvd_diff] addDs [dvd_diffD]) 1); qed "cd_diff_l"; -val prems=goalw thy [cd_def] "m<=n ==> cd x m n = cd x m (n-m)"; -by (cut_facts_tac prems 1); +Goalw [cd_def] "m<=n ==> cd x m n = cd x m (n-m)"; by (blast_tac (claset() addIs [dvd_diff] addDs [dvd_diffD]) 1); qed "cd_diff_r"; @@ -60,16 +46,14 @@ by (simp_tac (simpset() addsimps [cd_swap]) 1); qed "gcd_swap"; -val prems=goalw thy [gcd_def] "n<=m ==> gcd m n = gcd (m-n) n"; -by (cut_facts_tac prems 1); +Goalw [gcd_def] "n<=m ==> gcd m n = gcd (m-n) n"; by (subgoal_tac "n<=m ==> !x. cd x m n = cd x (m-n) n" 1); by (Asm_simp_tac 1); by (rtac allI 1); by (etac cd_diff_l 1); qed "gcd_diff_l"; -val prems=goalw thy [gcd_def] "m<=n ==> gcd m n = gcd m (n-m)"; -by (cut_facts_tac prems 1); +Goalw [gcd_def] "m<=n ==> gcd m n = gcd m (n-m)"; by (subgoal_tac "m<=n ==> !x. cd x m n = cd x m (n-m)" 1); by (Asm_simp_tac 1); by (rtac allI 1); @@ -79,11 +63,10 @@ (*** pow ***) -val prems = goal Power.thy "m mod 2 = 0 ==> ((n::nat)*n)^(m div 2) = n^m"; +Goal "m mod 2 = 0 ==> ((n::nat)*n)^(m div 2) = n^m"; by (subgoal_tac "n*n=n^2" 1); -by (etac ssubst 1); -by (stac (power_mult RS sym) 1); +by (etac ssubst 1 THEN stac (power_mult RS sym) 1); by (stac mult_div_cancel 1); -by (ALLGOALS(simp_tac (simpset() addsimps prems))); +by (ALLGOALS Asm_simp_tac); qed "sq_pow_div2"; Addsimps [sq_pow_div2]; diff -r fdb397af4cab -r 48e235179ffb src/HOL/Hoare/Hoare.ML --- a/src/HOL/Hoare/Hoare.ML Wed Jul 28 22:01:58 1999 +0200 +++ b/src/HOL/Hoare/Hoare.ML Thu Jul 29 12:44:57 1999 +0200 @@ -38,7 +38,7 @@ val lemma = result() RS spec RS spec RS mp RS mp; Goalw [Valid_def] - "[| p <= i; Valid (i Int b) c i; (i Int -b) <= q |] \ + "[| p <= i; Valid (i Int b) c i; i Int (-b) <= q |] \ \ ==> Valid p (WHILE b INV {i} DO c OD) q"; by (Asm_simp_tac 1); by (Clarify_tac 1); diff -r fdb397af4cab -r 48e235179ffb src/HOL/Integ/IntDef.ML --- a/src/HOL/Integ/IntDef.ML Wed Jul 28 22:01:58 1999 +0200 +++ b/src/HOL/Integ/IntDef.ML Thu Jul 29 12:44:57 1999 +0200 @@ -180,7 +180,7 @@ (simpset() addsimps [zadd_ize UN_equiv_class2]) 1); qed "zadd"; -Goal "- (z + w) = - z + - (w::int)"; +Goal "- (z + w) = (- z) + (- w::int)"; by (res_inst_tac [("z","z")] eq_Abs_Integ 1); by (res_inst_tac [("z","w")] eq_Abs_Integ 1); by (asm_simp_tac (simpset() addsimps [zminus,zadd]) 1); @@ -612,7 +612,7 @@ Goal "!!w::int. (z + w' = z + w) = (w' = w)"; by Safe_tac; -by (dres_inst_tac [("f", "%x. x + -z")] arg_cong 1); +by (dres_inst_tac [("f", "%x. x + (-z)")] arg_cong 1); by (asm_full_simp_tac (simpset() addsimps zadd_ac) 1); qed "zadd_left_cancel"; diff -r fdb397af4cab -r 48e235179ffb src/HOL/Integ/IntDef.thy --- a/src/HOL/Integ/IntDef.thy Wed Jul 28 22:01:58 1999 +0200 +++ b/src/HOL/Integ/IntDef.thy Thu Jul 29 12:44:57 1999 +0200 @@ -39,7 +39,7 @@ Abs_Integ(UN p1:Rep_Integ(z). UN p2:Rep_Integ(w). split (%x1 y1. split (%x2 y2. intrel^^{(x1+x2, y1+y2)}) p2) p1)" - zdiff_def "z - w == z + -(w::int)" + zdiff_def "z - (w::int) == z + (-w)" zless_def "z (c*a) div (c*b) = a div b"; -by (subgoal_tac "(c * -a) div (c * -b) = -a div -b" 1); +by (subgoal_tac "(c * (-a)) div (c * (-b)) = (-a) div (-b)" 1); by (rtac lemma1 2); by (auto_tac (claset(), simpset() addsimps [zmult_zminus_right])); val lemma2 = result(); @@ -789,7 +789,7 @@ val lemma1 = result(); Goal "[| b < (#0::int); c ~= #0 |] ==> (c*a) mod (c*b) = c * (a mod b)"; -by (subgoal_tac "(c * -a) mod (c * -b) = c * (-a mod -b)" 1); +by (subgoal_tac "(c * (-a)) mod (c * (-b)) = c * ((-a) mod (-b))" 1); by (rtac lemma1 2); by (auto_tac (claset(), simpset() addsimps [zmult_zminus_right, zmod_zminus_zminus])); @@ -838,12 +838,11 @@ Goal "a <= (#0::int) ==> (#1 + #2*b) div (#2*a) = (b+#1) div a"; -by (subgoal_tac "(#1 + #2*(-b-#1)) div (#2 * -a) = (-b-#1) div (-a)" 1); +by (subgoal_tac "(#1 + #2*(-b-#1)) div (#2 * (-a)) = (-b-#1) div (-a)" 1); by (rtac pos_zdiv_times_2 2); by (auto_tac (claset(), simpset() addsimps [zmult_zminus_right])); -by Auto_tac; -by (subgoal_tac "(#-1 + - (#2 * b)) = - (#1 + (#2 * b))" 1); +by (subgoal_tac "(#-1 - (#2 * b)) = - (#1 + (#2 * b))" 1); by (Simp_tac 2); by (asm_full_simp_tac (HOL_ss addsimps [zdiv_zminus_zminus, zdiff_def, @@ -899,11 +898,11 @@ Goal "a <= (#0::int) ==> (#1 + #2*b) mod (#2*a) = #2 * ((b+#1) mod a) - #1"; by (subgoal_tac - "(#1 + #2*(-b-#1)) mod (#2*-a) = #1 + #2*((-b-#1) mod (-a))" 1); + "(#1 + #2*(-b-#1)) mod (#2*(-a)) = #1 + #2*((-b-#1) mod (-a))" 1); by (rtac pos_zmod_times_2 2); by (auto_tac (claset(), simpset() addsimps [zmult_zminus_right])); -by (subgoal_tac "(#-1 + - (#2 * b)) = - (#1 + (#2 * b))" 1); +by (subgoal_tac "(#-1 - (#2 * b)) = - (#1 + (#2 * b))" 1); by (Simp_tac 2); by (asm_full_simp_tac (HOL_ss addsimps [zmod_zminus_zminus, zdiff_def, @@ -938,19 +937,19 @@ by (rtac order_trans 1); by (res_inst_tac [("a'","#-1")] zdiv_mono1 1); by (auto_tac (claset(), simpset() addsimps [zdiv_minus1])); -qed "div_neg_pos"; +qed "div_neg_pos_less0"; Goal "[| (#0::int) <= a; b < #0 |] ==> a div b <= #0"; by (dtac zdiv_mono1_neg 1); by Auto_tac; -qed "div_nonneg_neg"; +qed "div_nonneg_neg_le0"; Goal "(#0::int) < b ==> (#0 <= a div b) = (#0 <= a)"; by Auto_tac; by (dtac zdiv_mono1 2); by (auto_tac (claset(), simpset() addsimps [linorder_neq_iff])); by (full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1); -by (blast_tac (claset() addIs [div_neg_pos]) 1); +by (blast_tac (claset() addIs [div_neg_pos_less0]) 1); qed "pos_imp_zdiv_nonneg_iff"; Goal "b < (#0::int) ==> (#0 <= a div b) = (a <= (#0::int))"; diff -r fdb397af4cab -r 48e235179ffb src/HOL/Integ/NatBin.ML --- a/src/HOL/Integ/NatBin.ML Wed Jul 28 22:01:58 1999 +0200 +++ b/src/HOL/Integ/NatBin.ML Thu Jul 29 12:44:57 1999 +0200 @@ -146,7 +146,7 @@ Goal "(#0::int) <= z ==> nat z div nat z' = nat (z div z')"; by (case_tac "#0 <= z'" 1); by (auto_tac (claset(), - simpset() addsimps [div_nonneg_neg, DIVISION_BY_ZERO_DIV])); + simpset() addsimps [div_nonneg_neg_le0, DIVISION_BY_ZERO_DIV])); by (zdiv_undefined_case_tac "z' = #0" 1); by (simp_tac (simpset() addsimps [numeral_0_eq_0, DIVISION_BY_ZERO_DIV]) 1); by (auto_tac (claset() addSEs [nonneg_eq_int], simpset())); diff -r fdb397af4cab -r 48e235179ffb src/HOL/Real/Hyperreal/Filter.ML --- a/src/HOL/Real/Hyperreal/Filter.ML Wed Jul 28 22:01:58 1999 +0200 +++ b/src/HOL/Real/Hyperreal/Filter.ML Thu Jul 29 12:44:57 1999 +0200 @@ -4,9 +4,6 @@ Description : Filters and Ultrafilter *) -open Filter; - - (*------------------------------------------------------------------ Properties of Filters and Freefilters - rules for intro, destruction etc. @@ -290,7 +287,7 @@ A few properties of freefilters -------------------------------------------------------------------*) -Goal "F1 Int F2 = ((F1 Int Y) Int F2) Un ((F2 Int - Y) Int F1)"; +Goal "F1 Int F2 = ((F1 Int Y) Int F2) Un ((F2 Int (- Y)) Int F1)"; by (Auto_tac); qed "lemma_Compl_cancel_eq"; @@ -303,7 +300,7 @@ qed "finite_IntI2"; Goal "[| finite (F1 Int Y); \ -\ finite (F2 Int - Y) \ +\ finite (F2 Int (- Y)) \ \ |] ==> finite (F1 Int F2)"; by (res_inst_tac [("Y1","Y")] (lemma_Compl_cancel_eq RS ssubst) 1); by (rtac finite_UnI 1); @@ -403,7 +400,7 @@ We prove: 1. Existence of maximal filter i.e. ultrafilter 2. Freeness property i.e ultrafilter is free Use a locale to prove various lemmas and then - export main result- The Ultrafilter Theorem + export main result: The Ultrafilter Theorem -------------------------------------------------------------------*) Open_locale "UFT"; @@ -516,8 +513,9 @@ by (res_inst_tac [("x","Union c")] bexI 1 THEN Blast_tac 1); by (rtac Un_chain_mem_cofinite_Filter_set 1 THEN REPEAT(assume_tac 1)); by (res_inst_tac [("x","frechet (UNIV)")] bexI 1 THEN Blast_tac 1); -by (auto_tac (claset(),simpset() addsimps - [thm "superfrechet_def", thm "frechet_def"])); +by (auto_tac (claset(), + simpset() addsimps + [thm "superfrechet_def", thm "frechet_def"])); qed "max_cofinite_Filter_Ex"; Goal "EX U: superfrechet UNIV. (\ diff -r fdb397af4cab -r 48e235179ffb src/HOL/Real/RComplete.ML --- a/src/HOL/Real/RComplete.ML Wed Jul 28 22:01:58 1999 +0200 +++ b/src/HOL/Real/RComplete.ML Thu Jul 29 12:44:57 1999 +0200 @@ -5,9 +5,6 @@ reals and reals *) - -open RComplete; - claset_ref() := claset() delWrapper "bspec"; (*--------------------------------------------------------- @@ -20,15 +17,14 @@ \ ((? x:P. y < x) = (? X. real_of_preal X : P & \ \ y < real_of_preal X))"; by (blast_tac (claset() addSDs [bspec, - real_gt_zero_preal_Ex RS iffD1]) 1); + real_gt_zero_preal_Ex RS iffD1]) 1); qed "real_sup_lemma1"; Goal "[| ! x:P. 0r < x; ? x. x: P; ? y. !x: P. x < y |] \ \ ==> (? X. X: {w. real_of_preal w : P}) & \ \ (? Y. !X: {w. real_of_preal w : P}. X < Y)"; by (rtac conjI 1); -by (blast_tac (claset() addDs [bspec, - real_gt_zero_preal_Ex RS iffD1]) 1); +by (blast_tac (claset() addDs [bspec, real_gt_zero_preal_Ex RS iffD1]) 1); by Auto_tac; by (dtac bspec 1 THEN assume_tac 1); by (forward_tac [bspec] 1 THEN assume_tac 1); @@ -65,7 +61,7 @@ by (rtac (real_sup_lemma1 RS iffD2) 1 THEN assume_tac 1); by (case_tac "0r < ya" 1); by (auto_tac (claset() addSDs [real_less_all_real2, - real_gt_zero_preal_Ex RS iffD1],simpset())); + real_gt_zero_preal_Ex RS iffD1],simpset())); by (forward_tac [real_sup_lemma2] 2 THEN Auto_tac); by (forward_tac [real_sup_lemma2] 1 THEN Auto_tac); by (rtac (preal_complete RS spec RS iffD2 RS bexE) 1); @@ -79,15 +75,14 @@ Completeness properties using isUb, isLub etc. -------------------------------------------------------*) -Goal "!!(x::real). [| isLub R S x; isLub R S y |] ==> x = y"; +Goal "[| isLub R S x; isLub R S y |] ==> x = (y::real)"; by (forward_tac [isLub_isUb] 1); by (forw_inst_tac [("x","y")] isLub_isUb 1); by (blast_tac (claset() addSIs [real_le_anti_sym] - addSDs [isLub_le_isUb]) 1); + addSDs [isLub_le_isUb]) 1); qed "real_isLub_unique"; -Goalw [setle_def,setge_def] - "!!x::real. [| x <=* S'; S <= S' |] ==> x <=* S"; +Goalw [setle_def,setge_def] "[| (x::real) <=* S'; S <= S' |] ==> x <=* S"; by (Blast_tac 1); qed "real_order_restrict"; @@ -96,13 +91,14 @@ ----------------------------------------------------------------*) Goal "[| ALL x: S. 0r < x; \ -\ EX x. x: S; \ -\ EX u. isUb (UNIV::real set) S u \ -\ |] ==> EX t. isLub (UNIV::real set) S t"; +\ EX x. x: S; \ +\ EX u. isUb (UNIV::real set) S u \ +\ |] ==> EX t. isLub (UNIV::real set) S t"; by (res_inst_tac [("x","real_of_preal(psup({w. real_of_preal w : S}))")] exI 1); by (auto_tac (claset(), simpset() addsimps [isLub_def,leastP_def,isUb_def])); by (auto_tac (claset() addSIs [setleI,setgeI] - addSDs [real_gt_zero_preal_Ex RS iffD1],simpset())); + addSDs [real_gt_zero_preal_Ex RS iffD1], + simpset())); by (forw_inst_tac [("x","y")] bspec 1 THEN assume_tac 1); by (dtac (real_gt_zero_preal_Ex RS iffD1) 1); by (auto_tac (claset(), simpset() addsimps [real_of_preal_le_iff])); @@ -125,38 +121,39 @@ (*------------------------------- Lemmas -------------------------------*) -Goal "! y : {z. ? x: P. z = x + -xa + 1r} Int {x. 0r < x}. 0r < y"; +Goal "! y : {z. ? x: P. z = x + (-xa) + 1r} Int {x. 0r < x}. 0r < y"; by Auto_tac; qed "real_sup_lemma3"; -Goal "(xa <= S + X + -Z) = (xa + -X + Z <= (S::real))"; +Goal "(xa <= S + X + (-Z)) = (xa + (-X) + Z <= (S::real))"; by (simp_tac (simpset() addsimps [real_diff_def, real_diff_le_eq RS sym] @ real_add_ac) 1); qed "lemma_le_swap2"; -Goal "[| 0r < x + -X + 1r; x < xa |] ==> 0r < xa + -X + 1r"; +Goal "[| 0r < x + (-X) + 1r; x < xa |] ==> 0r < xa + (-X) + 1r"; by (dtac real_add_less_mono 1); by (assume_tac 1); by (dres_inst_tac [("C","-x"),("A","0r + x")] real_add_less_mono2 1); -by (asm_full_simp_tac (simpset() addsimps [real_add_zero_right, - real_add_assoc RS sym,real_add_minus_left,real_add_zero_left]) 1); +by (asm_full_simp_tac + (simpset() addsimps [real_add_zero_right, real_add_assoc RS sym, + real_add_minus_left,real_add_zero_left]) 1); by (asm_full_simp_tac (simpset() addsimps real_add_ac) 1); qed "lemma_real_complete1"; -Goal "!!x. [| x + -X + 1r <= S; xa < x |] ==> xa + -X + 1r <= S"; +Goal "[| x + (-X) + 1r <= S; xa < x |] ==> xa + (-X) + 1r <= S"; by (dtac real_less_imp_le 1); by (dtac real_add_le_mono 1); by (assume_tac 1); by (asm_full_simp_tac (simpset() addsimps real_add_ac) 1); qed "lemma_real_complete2"; -Goal "[| x + -X + 1r <= S; xa < x |] ==> xa <= S + X + -1r"; (**) +Goal "[| x + (-X) + 1r <= S; xa < x |] ==> xa <= S + X + (-1r)"; (**) by (rtac (lemma_le_swap2 RS iffD2) 1); by (etac lemma_real_complete2 1); by (assume_tac 1); qed "lemma_real_complete2a"; -Goal "[| x + -X + 1r <= S; xa <= x |] ==> xa <= S + X + -1r"; +Goal "[| x + (-X) + 1r <= S; xa <= x |] ==> xa <= S + X + (-1r)"; by (rotate_tac 1 1); by (etac (real_le_imp_less_or_eq RS disjE) 1); by (blast_tac (claset() addIs [lemma_real_complete2a]) 1); @@ -166,22 +163,22 @@ (*------------------------------------ reals Completeness (again!) ------------------------------------*) -Goal "!!(S::real set). [| EX X. X: S; \ -\ EX Y. isUb (UNIV::real set) S Y \ -\ |] ==> EX t. isLub (UNIV :: real set) S t"; +Goal "[| EX X. X: S; EX Y. isUb (UNIV::real set) S Y |] \ +\ ==> EX t. isLub (UNIV :: real set) S t"; by (Step_tac 1); -by (subgoal_tac "? u. u: {z. ? x: S. z = x + -X + 1r} \ +by (subgoal_tac "? u. u: {z. ? x: S. z = x + (-X) + 1r} \ \ Int {x. 0r < x}" 1); -by (subgoal_tac "isUb (UNIV::real set) ({z. ? x: S. z = x + -X + 1r} \ -\ Int {x. 0r < x}) (Y + -X + 1r)" 1); +by (subgoal_tac "isUb (UNIV::real set) ({z. ? x: S. z = x + (-X) + 1r} \ +\ Int {x. 0r < x}) (Y + (-X) + 1r)" 1); by (cut_inst_tac [("P","S"),("xa","X")] real_sup_lemma3 1); -by (EVERY1[forward_tac [exI RSN (3,posreals_complete)], Blast_tac, Blast_tac, Step_tac]); -by (res_inst_tac [("x","t + X + -1r")] exI 1); +by (EVERY1[forward_tac [exI RSN (3,posreals_complete)], Blast_tac, Blast_tac, + Step_tac]); +by (res_inst_tac [("x","t + X + (-1r)")] exI 1); by (rtac isLubI2 1); by (rtac setgeI 2 THEN Step_tac 2); -by (subgoal_tac "isUb (UNIV:: real set) ({z. ? x: S. z = x + -X + 1r} \ -\ Int {x. 0r < x}) (y + -X + 1r)" 2); -by (dres_inst_tac [("y","(y + - X + 1r)")] isLub_le_isUb 2 +by (subgoal_tac "isUb (UNIV:: real set) ({z. ? x: S. z = x + (-X) + 1r} \ +\ Int {x. 0r < x}) (y + (-X) + 1r)" 2); +by (dres_inst_tac [("y","(y + (- X) + 1r)")] isLub_le_isUb 2 THEN assume_tac 2); by (full_simp_tac (simpset() addsimps [real_diff_def, real_diff_le_eq RS sym] @ @@ -230,9 +227,9 @@ by (asm_full_simp_tac (simpset() addsimps [real_le_diff_eq RS sym, real_diff_def]) 1); by (subgoal_tac "isUb (UNIV::real set) \ -\ {z. EX n. z = x*(real_of_posnat n)} (t + -x)" 1); +\ {z. EX n. z = x*(real_of_posnat n)} (t + (-x))" 1); by (blast_tac (claset() addSIs [isUbI,setleI]) 2); -by (dres_inst_tac [("y","t+-x")] isLub_le_isUb 1); +by (dres_inst_tac [("y","t+(-x)")] isLub_le_isUb 1); by (dres_inst_tac [("x","-t")] real_add_left_le_mono1 2); by (auto_tac (claset() addDs [real_le_less_trans, (real_minus_zero_less_iff2 RS iffD2)], diff -r fdb397af4cab -r 48e235179ffb src/HOL/Real/Real.ML --- a/src/HOL/Real/Real.ML Wed Jul 28 22:01:58 1999 +0200 +++ b/src/HOL/Real/Real.ML Thu Jul 29 12:44:57 1999 +0200 @@ -6,10 +6,10 @@ *) Goal "(0r < x) = (? y. x = real_of_preal y)"; -by (auto_tac (claset(),simpset() addsimps [real_of_preal_zero_less])); +by (auto_tac (claset(), simpset() addsimps [real_of_preal_zero_less])); by (cut_inst_tac [("x","x")] real_of_preal_trichotomy 1); by (blast_tac (claset() addSEs [real_less_irrefl, - real_of_preal_not_minus_gt_zero RS notE]) 1); + real_of_preal_not_minus_gt_zero RS notE]) 1); qed "real_gt_zero_preal_Ex"; Goal "real_of_preal z < x ==> ? y. x = real_of_preal y"; @@ -19,12 +19,12 @@ Goal "real_of_preal z <= x ==> ? y. x = real_of_preal y"; by (blast_tac (claset() addDs [real_le_imp_less_or_eq, - real_gt_preal_preal_Ex]) 1); + real_gt_preal_preal_Ex]) 1); qed "real_ge_preal_preal_Ex"; Goal "y <= 0r ==> !x. y < real_of_preal x"; by (auto_tac (claset() addEs [real_le_imp_less_or_eq RS disjE] - addIs [real_of_preal_zero_less RSN(2,real_less_trans)], + addIs [real_of_preal_zero_less RSN(2,real_less_trans)], simpset() addsimps [real_of_preal_zero_less])); qed "real_less_all_preal"; @@ -43,12 +43,12 @@ by (auto_tac (claset(), simpset() addsimps real_add_ac)); qed "real_lemma_add_positive_imp_less"; -Goal "!!(R::real). ? T. 0r < T & R + T = S ==> R < S"; +Goal "? T. 0r < T & R + T = S ==> R < S"; by (blast_tac (claset() addIs [real_lemma_add_positive_imp_less]) 1); qed "real_ex_add_positive_left_less"; (*Alternative definition for real_less. NOT for rewriting*) -Goal "!!(R::real). (R < S) = (? T. 0r < T & R + T = S)"; +Goal "(R < S) = (? T. 0r < T & R + T = S)"; by (blast_tac (claset() addSIs [real_less_add_positive_left_Ex, real_ex_add_positive_left_less]) 1); qed "real_less_iff_add"; @@ -62,7 +62,7 @@ by (blast_tac (claset() addIs [real_less_trans]) 2); by (auto_tac (claset(), simpset() addsimps - [real_gt_zero_preal_Ex,real_of_preal_minus_less_self])); + [real_gt_zero_preal_Ex,real_of_preal_minus_less_self])); qed "real_gt_zero_iff"; Goal "(x < 0r) = (x < -x)"; @@ -72,11 +72,11 @@ qed "real_lt_zero_iff"; Goalw [real_le_def] "(0r <= x) = (-x <= x)"; -by (auto_tac (claset(),simpset() addsimps [real_lt_zero_iff RS sym])); +by (auto_tac (claset(), simpset() addsimps [real_lt_zero_iff RS sym])); qed "real_ge_zero_iff"; Goalw [real_le_def] "(x <= 0r) = (x <= -x)"; -by (auto_tac (claset(),simpset() addsimps [real_gt_zero_iff RS sym])); +by (auto_tac (claset(), simpset() addsimps [real_gt_zero_iff RS sym])); qed "real_le_zero_iff"; Goal "(real_of_preal m1 <= real_of_preal m2) = (m1 <= m2)"; @@ -86,31 +86,31 @@ by (etac preal_less_irrefl 1); qed "real_of_preal_le_iff"; -Goal "!!(x::real). [| 0r < x; 0r < y |] ==> 0r < x * y"; -by (auto_tac (claset(),simpset() addsimps [real_gt_zero_preal_Ex])); +Goal "[| 0r < x; 0r < y |] ==> 0r < x * y"; +by (auto_tac (claset(), simpset() addsimps [real_gt_zero_preal_Ex])); by (res_inst_tac [("x","y*ya")] exI 1); by (full_simp_tac (simpset() addsimps [real_of_preal_mult]) 1); qed "real_mult_order"; -Goal "!!(x::real). [| x < 0r; y < 0r |] ==> 0r < x * y"; +Goal "[| x < 0r; y < 0r |] ==> 0r < x * y"; by (REPEAT(dtac (real_minus_zero_less_iff RS iffD2) 1)); by (dtac real_mult_order 1 THEN assume_tac 1); by (Asm_full_simp_tac 1); qed "real_mult_less_zero1"; -Goal "!!(x::real). [| 0r <= x; 0r <= y |] ==> 0r <= x * y"; +Goal "[| 0r <= x; 0r <= y |] ==> 0r <= x * y"; by (REPEAT(dtac real_le_imp_less_or_eq 1)); by (auto_tac (claset() addIs [real_mult_order, real_less_imp_le], simpset())); qed "real_le_mult_order"; -Goal "!!(x::real). [| 0r < x; 0r <= y |] ==> 0r <= x * y"; +Goal "[| 0r < x; 0r <= y |] ==> 0r <= x * y"; by (dtac real_le_imp_less_or_eq 1); by (auto_tac (claset() addIs [real_mult_order, - real_less_imp_le],simpset())); + real_less_imp_le],simpset())); qed "real_less_le_mult_order"; -Goal "!!(x::real). [| x <= 0r; y <= 0r |] ==> 0r <= x * y"; +Goal "[| x <= 0r; y <= 0r |] ==> 0r <= x * y"; by (rtac real_less_or_eq_imp_le 1); by (dtac real_le_imp_less_or_eq 1 THEN etac disjE 1); by Auto_tac; @@ -118,17 +118,17 @@ by (auto_tac (claset() addDs [real_mult_less_zero1],simpset())); qed "real_mult_le_zero1"; -Goal "!!(x::real). [| 0r <= x; y < 0r |] ==> x * y <= 0r"; +Goal "[| 0r <= x; y < 0r |] ==> x * y <= 0r"; by (rtac real_less_or_eq_imp_le 1); by (dtac real_le_imp_less_or_eq 1 THEN etac disjE 1); by Auto_tac; by (dtac (real_minus_zero_less_iff RS iffD2) 1); by (rtac (real_minus_zero_less_iff RS subst) 1); by (blast_tac (claset() addDs [real_mult_order] - addIs [real_minus_mult_eq2 RS ssubst]) 1); + addIs [real_minus_mult_eq2 RS ssubst]) 1); qed "real_mult_le_zero"; -Goal "!!(x::real). [| 0r < x; y < 0r |] ==> x*y < 0r"; +Goal "[| 0r < x; y < 0r |] ==> x*y < 0r"; by (dtac (real_minus_zero_less_iff RS iffD2) 1); by (dtac real_mult_order 1 THEN assume_tac 1); by (rtac (real_minus_zero_less_iff RS iffD1) 1); @@ -137,7 +137,7 @@ Goalw [real_one_def] "0r < 1r"; by (auto_tac (claset() addIs [real_gt_zero_preal_Ex RS iffD2], - simpset() addsimps [real_of_preal_def])); + simpset() addsimps [real_of_preal_def])); qed "real_zero_less_one"; (*** Monotonicity results ***) @@ -204,7 +204,7 @@ by (Full_simp_tac 1); qed "real_add_order"; -Goal "!!(x::real). [| 0r <= x; 0r <= y |] ==> 0r <= x + y"; +Goal "[| 0r <= x; 0r <= y |] ==> 0r <= x + y"; by (REPEAT(dtac real_le_imp_less_or_eq 1)); by (auto_tac (claset() addIs [real_add_order, real_less_imp_le], simpset())); @@ -228,12 +228,12 @@ Goal "EX (x::real). x < y"; by (rtac (real_add_zero_right RS subst) 1); -by (res_inst_tac [("x","y + -1r")] exI 1); +by (res_inst_tac [("x","y + (-1r)")] exI 1); by (auto_tac (claset() addSIs [real_add_less_mono2], simpset() addsimps [real_minus_zero_less_iff2, real_zero_less_one])); qed "real_less_Ex"; -Goal "!!(u::real). 0r < r ==> u + -r < u"; +Goal "0r < r ==> u + (-r) < u"; by (res_inst_tac [("C","r")] real_less_add_right_cancel 1); by (simp_tac (simpset() addsimps [real_add_assoc]) 1); qed "real_add_minus_positive_less_self"; @@ -242,10 +242,10 @@ by (Step_tac 1); by (dres_inst_tac [("x","-s")] real_add_left_le_mono1 1); by (dres_inst_tac [("x","r")] real_add_left_le_mono1 2); -by (Auto_tac); +by Auto_tac; by (dres_inst_tac [("z","-r")] real_add_le_mono1 1); by (dres_inst_tac [("z","s")] real_add_le_mono1 2); -by (auto_tac (claset(),simpset() addsimps [real_add_assoc])); +by (auto_tac (claset(), simpset() addsimps [real_add_assoc])); qed "real_le_minus_iff"; Addsimps [real_le_minus_iff RS sym]; @@ -257,14 +257,14 @@ Goal "0r <= x*x"; by (res_inst_tac [("R2.0","0r"),("R1.0","x")] real_linear_less2 1); by (auto_tac (claset() addIs [real_mult_order, - real_mult_less_zero1,real_less_imp_le], - simpset())); + real_mult_less_zero1,real_less_imp_le], + simpset())); qed "real_le_square"; Addsimps [real_le_square]; -(*--------------------------------------------------------------------------------- +(*---------------------------------------------------------------------------- An embedding of the naturals in the reals - ---------------------------------------------------------------------------------*) + ----------------------------------------------------------------------------*) Goalw [real_of_posnat_def] "real_of_posnat 0 = 1r"; by (full_simp_tac (simpset() addsimps [pnat_one_iff RS sym,real_of_preal_def]) 1); @@ -324,7 +324,7 @@ by (induct_tac "n" 1); by (auto_tac (claset(), simpset () addsimps [real_of_posnat_Suc,real_of_posnat_one, - real_of_posnat_less_zero, real_less_imp_le])); + real_of_posnat_less_zero, real_less_imp_le])); qed "real_of_posnat_less_one"; Addsimps [real_of_posnat_less_one]; @@ -352,7 +352,7 @@ by (EVERY1[dtac real_le_imp_less_or_eq, Step_tac]); by (dtac real_mult_less_zero1 1 THEN assume_tac 1); by (auto_tac (claset() addIs [real_zero_less_one RS real_less_asym], - simpset() addsimps [real_minus_mult_eq1 RS sym])); + simpset() addsimps [real_minus_mult_eq1 RS sym])); qed "real_rinv_gt_zero"; Goal "x < 0r ==> rinv x < 0r"; @@ -360,8 +360,7 @@ by (dtac (real_minus_zero_less_iff RS iffD2) 1); by (rtac (real_minus_zero_less_iff RS iffD1) 1); by (dtac (real_minus_rinv RS sym) 1); -by (auto_tac (claset() addIs [real_rinv_gt_zero], - simpset())); +by (auto_tac (claset() addIs [real_rinv_gt_zero], simpset())); qed "real_rinv_less_zero"; Goal "0r < rinv(real_of_posnat n)"; @@ -400,7 +399,7 @@ by (full_simp_tac (simpset() addsimps [real_mult_assoc]) 1); qed "real_sum_of_halves"; -Goal "!!(x::real). [| 0r x*z x*z z*x z*x x x x x x*z<=y*z"; +Goal "[| 0r<=z; x x*z<=y*z"; by (EVERY1 [rtac real_less_or_eq_imp_le, dtac real_le_imp_less_or_eq]); by (auto_tac (claset() addIs [real_mult_less_mono1],simpset())); qed "real_mult_le_less_mono1"; -Goal "!!(x::real). [| 0r<=z; x z*x<=z*y"; +Goal "[| 0r<=z; x z*x<=z*y"; by (asm_simp_tac (simpset() addsimps [real_mult_commute,real_mult_le_less_mono1]) 1); qed "real_mult_le_less_mono2"; -Goal "!!x y (z::real). [| 0r<=z; x<=y |] ==> z*x<=z*y"; +Goal "[| 0r<=z; x<=y |] ==> z*x<=z*y"; by (dres_inst_tac [("x","x")] real_le_imp_less_or_eq 1); by (auto_tac (claset() addIs [real_mult_le_less_mono2], simpset())); qed "real_mult_le_le_mono1"; -Goal "!!(x::real). [| 0r < r1; r1 r1 * x < r2 * y"; by (dres_inst_tac [("x","x")] real_mult_less_mono2 1); by (dres_inst_tac [("R1.0","0r")] real_less_trans 2); by (dres_inst_tac [("x","r1")] real_mult_less_mono1 3); -by (Auto_tac); +by Auto_tac; by (blast_tac (claset() addIs [real_less_trans]) 1); qed "real_mult_less_mono"; -Goal "!!(x::real). [| 0r < r1; r1 0r < r2 * y"; by (dres_inst_tac [("R1.0","0r")] real_less_trans 1); by (assume_tac 1); by (blast_tac (claset() addIs [real_mult_order]) 1); qed "real_mult_order_trans"; -Goal "!!(x::real). [| 0r < r1; r1 r1 * x < r2 * y"; -by (auto_tac (claset() addSDs [real_le_imp_less_or_eq] addIs - [real_mult_less_mono,real_mult_order_trans], +by (auto_tac (claset() addSDs [real_le_imp_less_or_eq] + addIs [real_mult_less_mono,real_mult_order_trans], simpset())); qed "real_mult_less_mono3"; -Goal "!!(x::real). [| 0r <= r1; r1 r1 * x < r2 * y"; -by (auto_tac (claset() addSDs [real_le_imp_less_or_eq] addIs - [real_mult_less_mono,real_mult_order_trans, - real_mult_order],simpset())); +by (auto_tac (claset() addSDs [real_le_imp_less_or_eq] + addIs [real_mult_less_mono,real_mult_order_trans, + real_mult_order], + simpset())); by (dres_inst_tac [("R2.0","x")] real_less_trans 1); by (assume_tac 1); by (blast_tac (claset() addIs [real_mult_order]) 1); qed "real_mult_less_mono4"; -Goal "!!(x::real). [| 0r < r1; r1 <= r2; 0r <= x; x <= y |] \ -\ ==> r1 * x <= r2 * y"; -by (rtac real_less_or_eq_imp_le 1); -by (REPEAT(dtac real_le_imp_less_or_eq 1)); -by (auto_tac (claset() addIs [real_mult_less_mono, - real_mult_order_trans,real_mult_order],simpset())); -qed "real_mult_le_mono"; - -Goal "!!(x::real). [| 0r < r1; r1 < r2; 0r <= x; x <= y |] \ +Goal "[| 0r < r1; r1 <= r2; 0r <= x; x <= y |] \ \ ==> r1 * x <= r2 * y"; by (rtac real_less_or_eq_imp_le 1); by (REPEAT(dtac real_le_imp_less_or_eq 1)); by (auto_tac (claset() addIs [real_mult_less_mono, - real_mult_order_trans,real_mult_order],simpset())); + real_mult_order_trans,real_mult_order], + simpset())); +qed "real_mult_le_mono"; + +Goal "[| 0r < r1; r1 < r2; 0r <= x; x <= y |] \ +\ ==> r1 * x <= r2 * y"; +by (rtac real_less_or_eq_imp_le 1); +by (REPEAT(dtac real_le_imp_less_or_eq 1)); +by (auto_tac (claset() addIs [real_mult_less_mono, real_mult_order_trans, + real_mult_order], + simpset())); qed "real_mult_le_mono2"; -Goal "!!(x::real). [| 0r <= r1; r1 < r2; 0r <= x; x <= y |] \ +Goal "[| 0r <= r1; r1 < r2; 0r <= x; x <= y |] \ \ ==> r1 * x <= r2 * y"; by (dtac real_le_imp_less_or_eq 1); by (auto_tac (claset() addIs [real_mult_le_mono2],simpset())); by (dtac real_le_trans 1 THEN assume_tac 1); -by (auto_tac (claset() addIs [real_less_le_mult_order],simpset())); +by (auto_tac (claset() addIs [real_less_le_mult_order], simpset())); qed "real_mult_le_mono3"; -Goal "!!(x::real). [| 0r <= r1; r1 <= r2; 0r <= x; x <= y |] \ +Goal "[| 0r <= r1; r1 <= r2; 0r <= x; x <= y |] \ \ ==> r1 * x <= r2 * y"; by (dres_inst_tac [("x","r1")] real_le_imp_less_or_eq 1); -by (auto_tac (claset() addIs [real_mult_le_mono3, - real_mult_le_le_mono1],simpset())); +by (auto_tac (claset() addIs [real_mult_le_mono3, real_mult_le_le_mono1], + simpset())); qed "real_mult_le_mono4"; -Goal "!!x. 1r <= x ==> 0r < x"; +Goal "1r <= x ==> 0r < x"; by (rtac ccontr 1 THEN dtac real_leI 1); by (dtac real_le_trans 1 THEN assume_tac 1); -by (auto_tac (claset() addDs [real_zero_less_one - RSN (2,real_le_less_trans)],simpset() addsimps - [real_less_not_refl])); +by (auto_tac (claset() addDs [real_zero_less_one RSN (2,real_le_less_trans)], + simpset() addsimps [real_less_not_refl])); qed "real_gt_zero"; -Goal "!!r. [| 1r < r; 1r <= x |] ==> x <= r * x"; +Goal "[| 1r < r; 1r <= x |] ==> x <= r * x"; by (dtac (real_gt_zero RS real_less_imp_le) 1); by (auto_tac (claset() addSDs [real_mult_le_less_mono1], simpset())); qed "real_mult_self_le"; -Goal "!!r. [| 1r <= r; 1r <= x |] ==> x <= r * x"; +Goal "[| 1r <= r; 1r <= x |] ==> x <= r * x"; by (dtac real_le_imp_less_or_eq 1); by (auto_tac (claset() addIs [real_mult_self_le], - simpset() addsimps [real_le_refl])); + simpset() addsimps [real_le_refl])); qed "real_mult_self_le2"; -Goal "!!(x::real). x < y ==> x < (x + y)*rinv(1r + 1r)"; +Goal "x < y ==> x < (x + y)*rinv(1r + 1r)"; by (dres_inst_tac [("C","x")] real_add_less_mono2 1); by (dtac (real_add_self RS subst) 1); by (dtac (real_zero_less_two RS real_rinv_gt_zero RS @@ -544,7 +545,7 @@ by (asm_full_simp_tac (simpset() addsimps [real_mult_assoc]) 1); qed "real_less_half_sum"; -Goal "!!(x::real). x < y ==> (x + y)*rinv(1r + 1r) < y"; +Goal "x < y ==> (x + y)*rinv(1r + 1r) < y"; by (dtac real_add_less_mono1 1); by (dtac (real_add_self RS subst) 1); by (dtac (real_zero_less_two RS real_rinv_gt_zero RS @@ -552,20 +553,21 @@ by (asm_full_simp_tac (simpset() addsimps [real_mult_assoc]) 1); qed "real_gt_half_sum"; -Goal "!!(x::real). x < y ==> EX r. x < r & r < y"; +Goal "x < y ==> EX r::real. x < r & r < y"; by (blast_tac (claset() addSIs [real_less_half_sum, - real_gt_half_sum]) 1); + real_gt_half_sum]) 1); qed "real_dense"; Goal "(EX n. rinv(real_of_posnat n) < r) = (EX n. 1r < r * real_of_posnat n)"; by (Step_tac 1); by (dres_inst_tac [("n1","n")] (real_of_posnat_less_zero - RS real_mult_less_mono1) 1); + RS real_mult_less_mono1) 1); by (dres_inst_tac [("n2","n")] (real_of_posnat_less_zero RS - real_rinv_gt_zero RS real_mult_less_mono1) 2); + real_rinv_gt_zero RS real_mult_less_mono1) 2); by (auto_tac (claset(), simpset() addsimps [(real_of_posnat_less_zero RS - real_not_refl2 RS not_sym),real_mult_assoc])); + real_not_refl2 RS not_sym), + real_mult_assoc])); qed "real_of_posnat_rinv_Ex_iff"; Goal "(rinv(real_of_posnat n) < r) = (1r < r * real_of_posnat n)"; @@ -573,8 +575,8 @@ by (dres_inst_tac [("n1","n")] (real_of_posnat_less_zero RS real_mult_less_mono1) 1); by (dres_inst_tac [("n2","n")] (real_of_posnat_less_zero RS - real_rinv_gt_zero RS real_mult_less_mono1) 2); -by (auto_tac (claset(),simpset() addsimps [real_mult_assoc])); + real_rinv_gt_zero RS real_mult_less_mono1) 2); +by (auto_tac (claset(), simpset() addsimps [real_mult_assoc])); qed "real_of_posnat_rinv_iff"; Goal "(rinv(real_of_posnat n) <= r) = (1r <= r * real_of_posnat n)"; @@ -584,7 +586,7 @@ by (dres_inst_tac [("n3","n")] (real_of_posnat_less_zero RS real_rinv_gt_zero RS real_less_imp_le RS real_mult_le_le_mono1) 2); -by (auto_tac (claset(),simpset() addsimps real_mult_ac)); +by (auto_tac (claset(), simpset() addsimps real_mult_ac)); qed "real_of_posnat_rinv_le_iff"; Goalw [real_of_posnat_def] "(real_of_posnat n < real_of_posnat m) = (n < m)"; @@ -616,14 +618,14 @@ real_of_posnat_less_zero,real_not_refl2 RS not_sym])); qed "real_of_posnat_rinv_eq_iff"; -Goal "!!x. [| 0r < r; r < x |] ==> rinv x < rinv r"; +Goal "[| 0r < r; r < x |] ==> rinv x < rinv r"; by (forward_tac [real_less_trans] 1 THEN assume_tac 1); by (forward_tac [real_rinv_gt_zero] 1); by (forw_inst_tac [("x","x")] real_rinv_gt_zero 1); by (forw_inst_tac [("x","r"),("z","rinv r")] real_mult_less_mono1 1); by (assume_tac 1); by (asm_full_simp_tac (simpset() addsimps [real_not_refl2 RS - not_sym RS real_mult_inv_right]) 1); + not_sym RS real_mult_inv_right]) 1); by (forward_tac [real_rinv_gt_zero] 1); by (forw_inst_tac [("x","1r"),("z","rinv x")] real_mult_less_mono2 1); by (assume_tac 1); @@ -631,14 +633,14 @@ not_sym RS real_mult_inv_left,real_mult_assoc RS sym]) 1); qed "real_rinv_less_swap"; -Goal "!!x. [| 0r < r; 0r < x|] ==> (r < x) = (rinv x < rinv r)"; +Goal "[| 0r < r; 0r < x|] ==> (r < x) = (rinv x < rinv r)"; by (auto_tac (claset() addIs [real_rinv_less_swap],simpset())); by (res_inst_tac [("t","r")] (real_rinv_rinv RS subst) 1); by (etac (real_not_refl2 RS not_sym) 1); by (res_inst_tac [("t","x")] (real_rinv_rinv RS subst) 1); by (etac (real_not_refl2 RS not_sym) 1); by (auto_tac (claset() addIs [real_rinv_less_swap], - simpset() addsimps [real_rinv_gt_zero])); + simpset() addsimps [real_rinv_gt_zero])); qed "real_rinv_less_iff"; Goal "r < r + rinv(real_of_posnat n)"; @@ -653,87 +655,85 @@ qed "real_add_rinv_real_of_posnat_le"; Addsimps [real_add_rinv_real_of_posnat_le]; -Goal "r + -rinv(real_of_posnat n) < r"; +Goal "r + (-rinv(real_of_posnat n)) < r"; by (res_inst_tac [("C","-r")] real_less_add_left_cancel 1); by (full_simp_tac (simpset() addsimps [real_add_assoc RS sym, - real_minus_zero_less_iff2]) 1); + real_minus_zero_less_iff2]) 1); qed "real_add_minus_rinv_real_of_posnat_less"; Addsimps [real_add_minus_rinv_real_of_posnat_less]; -Goal "r + -rinv(real_of_posnat n) <= r"; +Goal "r + (-rinv(real_of_posnat n)) <= r"; by (rtac real_less_imp_le 1); by (Simp_tac 1); qed "real_add_minus_rinv_real_of_posnat_le"; Addsimps [real_add_minus_rinv_real_of_posnat_le]; -Goal "!!r. 0r < r ==> r*(1r + -rinv(real_of_posnat n)) < r"; +Goal "0r < r ==> r*(1r + (-rinv(real_of_posnat n))) < r"; by (simp_tac (simpset() addsimps [real_add_mult_distrib2]) 1); by (res_inst_tac [("C","-r")] real_less_add_left_cancel 1); -by (auto_tac (claset() addIs [real_mult_order],simpset() - addsimps [real_add_assoc RS sym,real_minus_mult_eq2 RS sym, - real_minus_zero_less_iff2])); +by (auto_tac (claset() addIs [real_mult_order], + simpset() addsimps [real_add_assoc RS sym, + real_minus_mult_eq2 RS sym, + real_minus_zero_less_iff2])); qed "real_mult_less_self"; -Goal "0r <= 1r + -rinv(real_of_posnat n)"; +Goal "0r <= 1r + (-rinv(real_of_posnat n))"; by (res_inst_tac [("C","rinv(real_of_posnat n)")] real_le_add_right_cancel 1); by (simp_tac (simpset() addsimps [real_add_assoc, - real_of_posnat_rinv_le_iff]) 1); + real_of_posnat_rinv_le_iff]) 1); qed "real_add_one_minus_rinv_ge_zero"; -Goal "!!r. 0r < r ==> 0r <= r*(1r + -rinv(real_of_posnat n))"; -by (dtac (real_add_one_minus_rinv_ge_zero RS - real_mult_le_less_mono1) 1); -by (Auto_tac); +Goal "0r < r ==> 0r <= r*(1r + (-rinv(real_of_posnat n)))"; +by (dtac (real_add_one_minus_rinv_ge_zero RS real_mult_le_less_mono1) 1); +by Auto_tac; qed "real_mult_add_one_minus_ge_zero"; -Goal "!!x. x*y = 0r ==> x = 0r | y = 0r"; -by (auto_tac (claset() addIs [ccontr] addDs - [real_mult_not_zero],simpset())); +Goal "x*y = 0r ==> x = 0r | y = 0r"; +by (auto_tac (claset() addIs [ccontr] addDs [real_mult_not_zero], + simpset())); qed "real_mult_zero_disj"; Goal "x + x*y = x*(1r + y)"; by (simp_tac (simpset() addsimps [real_add_mult_distrib2]) 1); qed "real_add_mult_distrib_one"; -Goal "!!x. [| x ~= 1r; y * x = y |] ==> y = 0r"; +Goal "[| x ~= 1r; y * x = y |] ==> y = 0r"; by (dtac (sym RS (real_eq_minus_iff RS iffD1)) 1); by (dtac sym 1); by (asm_full_simp_tac (simpset() addsimps [real_minus_mult_eq2, real_add_mult_distrib_one]) 1); by (dtac real_mult_zero_disj 1); -by (auto_tac (claset(),simpset() - addsimps [real_eq_minus_iff2 RS sym])); +by (auto_tac (claset(), + simpset() addsimps [real_eq_minus_iff2 RS sym])); qed "real_mult_eq_self_zero"; Addsimps [real_mult_eq_self_zero]; -Goal "!!x. [| x ~= 1r; y = y * x |] ==> y = 0r"; +Goal "[| x ~= 1r; y = y * x |] ==> y = 0r"; by (dtac sym 1); by (Asm_full_simp_tac 1); qed "real_mult_eq_self_zero2"; Addsimps [real_mult_eq_self_zero2]; -Goal "!!x. [| 0r <= x*y; 0r < x |] ==> 0r <= y"; +Goal "[| 0r <= x*y; 0r < x |] ==> 0r <= y"; by (forward_tac [real_rinv_gt_zero] 1); by (dres_inst_tac [("x","rinv x")] real_less_le_mult_order 1); by (dtac (real_not_refl2 RS not_sym RS real_mult_inv_left) 2); -by (auto_tac (claset(),simpset() addsimps - [real_mult_assoc RS sym])); +by (auto_tac (claset(), + simpset() addsimps [real_mult_assoc RS sym])); qed "real_mult_ge_zero_cancel"; -Goal "!!x. [|x ~= 0r; y ~= 0r |] ==> \ -\ rinv(x) + rinv(y) = (x + y)*rinv(x*y)"; +Goal "[|x ~= 0r; y ~= 0r |] ==> rinv(x) + rinv(y) = (x + y)*rinv(x*y)"; by (asm_full_simp_tac (simpset() addsimps - [real_rinv_distrib,real_add_mult_distrib, - real_mult_assoc RS sym]) 1); + [real_rinv_distrib,real_add_mult_distrib, + real_mult_assoc RS sym]) 1); by (rtac (real_mult_assoc RS ssubst) 1); by (rtac (real_mult_left_commute RS subst) 1); -by (asm_full_simp_tac (simpset() addsimps - [real_add_commute]) 1); +by (asm_full_simp_tac (simpset() addsimps [real_add_commute]) 1); qed "real_rinv_add"; -(*--------------------------------------------------------------------------------- +(*---------------------------------------------------------------------------- Another embedding of the naturals in the reals (see real_of_posnat) - ---------------------------------------------------------------------------------*) + ----------------------------------------------------------------------------*) Goalw [real_of_nat_def] "real_of_nat 0 = 0r"; by (full_simp_tac (simpset() addsimps [real_of_posnat_one]) 1); qed "real_of_nat_zero"; @@ -754,7 +754,7 @@ qed "real_of_nat_Suc"; Goalw [real_of_nat_def] "(n < m) = (real_of_nat n < real_of_nat m)"; -by (Auto_tac); +by Auto_tac; qed "real_of_nat_less_iff"; Addsimps [real_of_nat_less_iff RS sym]; @@ -762,22 +762,22 @@ Goal "inj real_of_nat"; by (rtac injI 1); by (auto_tac (claset() addSIs [inj_real_of_posnat RS injD], - simpset() addsimps [real_of_nat_def,real_add_right_cancel])); + simpset() addsimps [real_of_nat_def,real_add_right_cancel])); qed "inj_real_of_nat"; Goalw [real_of_nat_def] "0r <= real_of_nat n"; by (res_inst_tac [("C","1r")] real_le_add_right_cancel 1); -by (asm_full_simp_tac (simpset() addsimps - [real_add_assoc]) 1); +by (asm_full_simp_tac (simpset() addsimps [real_add_assoc]) 1); qed "real_of_nat_ge_zero"; Addsimps [real_of_nat_ge_zero]; Goal "real_of_nat n1 * real_of_nat n2 = real_of_nat (n1 * n2)"; by (induct_tac "n1" 1); by (dtac sym 2); -by (auto_tac (claset(),simpset() addsimps [real_of_nat_zero, - real_of_nat_add RS sym,real_of_nat_Suc,real_add_mult_distrib, - real_add_commute])); +by (auto_tac (claset(), + simpset() addsimps [real_of_nat_zero, + real_of_nat_add RS sym,real_of_nat_Suc, + real_add_mult_distrib, real_add_commute])); qed "real_of_nat_mult"; Goal "(real_of_nat n = real_of_nat m) = (n = m)"; @@ -788,21 +788,20 @@ (*------- lemmas -------*) goal NatDef.thy "!!m. [| m < Suc n; n <= m |] ==> m = n"; by (auto_tac (claset() addSDs [le_imp_less_or_eq] addIs [less_asym], - simpset() addsimps [less_Suc_eq])); + simpset() addsimps [less_Suc_eq])); qed "lemma_nat_not_dense"; goal NatDef.thy "!!m. [| m <= Suc n; n < m |] ==> m = Suc n"; by (auto_tac (claset() addSDs [le_imp_less_or_eq] addIs [less_asym], - simpset() addsimps [le_Suc_eq])); + simpset() addsimps [le_Suc_eq])); qed "lemma_nat_not_dense2"; goal NatDef.thy "!!m. m < Suc n ==> ~ Suc n <= m"; -by (blast_tac (claset() addDs - [less_le_trans] addIs [less_asym]) 1); +by (blast_tac (claset() addDs [less_le_trans] addIs [less_asym]) 1); qed "lemma_not_leI"; goalw NatDef.thy [le_def] "!!m. ~ Suc n <= m ==> ~ Suc (Suc n) <= m"; -by (Auto_tac); +by Auto_tac; qed "lemma_not_leI2"; (*------- lemmas -------*) @@ -815,14 +814,15 @@ (* Goalw [real_of_nat_def] "real_of_nat (n1 - n2) = real_of_nat n1 + -real_of_nat n2";*) -Goal "n2 < n1 --> real_of_nat (n1 - n2) = real_of_nat n1 + -real_of_nat n2"; +Goal "n2 < n1 --> real_of_nat (n1 - n2) = real_of_nat n1 + (-real_of_nat n2)"; by (induct_tac "n1" 1); by (Step_tac 1 THEN dtac leI 1 THEN dtac sym 2); by (dtac lemma_nat_not_dense 1); -by (auto_tac (claset(),simpset() addsimps [real_of_nat_Suc, - real_of_nat_zero] @ real_add_ac)); +by (auto_tac (claset(), + simpset() addsimps [real_of_nat_Suc, real_of_nat_zero] @ + real_add_ac)); by (asm_full_simp_tac (simpset() addsimps [real_of_nat_one RS sym, - real_of_nat_add,Suc_diff_n]) 1); + real_of_nat_add,Suc_diff_n]) 1); qed "real_of_nat_minus"; diff -r fdb397af4cab -r 48e235179ffb src/HOL/Real/RealAbs.ML --- a/src/HOL/Real/RealAbs.ML Wed Jul 28 22:01:58 1999 +0200 +++ b/src/HOL/Real/RealAbs.ML Thu Jul 29 12:44:57 1999 +0200 @@ -31,8 +31,8 @@ by (simp_tac (simpset() addsimps [(prem RS real_less_imp_le),rabs_eqI1]) 1); qed "rabs_eqI2"; -val [prem] = goalw thy [rabs_def,real_le_def] "x<0r ==> rabs x = -x"; -by (simp_tac (simpset() addsimps [prem,if_not_P]) 1); +Goalw [rabs_def,real_le_def] "x<0r ==> rabs x = -x"; +by (Asm_simp_tac 1); qed "rabs_minus_eqI2"; Goal "x<=0r ==> rabs x = -x"; @@ -71,39 +71,38 @@ (* case splits nightmare *) Goalw [rabs_def] "rabs(x*y) = (rabs x)*(rabs y)"; -by (auto_tac (claset(),simpset() addsimps [real_minus_mult_eq1, - real_minus_mult_commute,real_minus_mult_eq2])); +by (auto_tac (claset(), + simpset() addsimps [real_minus_mult_eq1, real_minus_mult_commute, + real_minus_mult_eq2])); by (blast_tac (claset() addDs [real_le_mult_order]) 1); by (auto_tac (claset() addSDs [not_real_leE],simpset())); by (EVERY1[dtac real_mult_le_zero, assume_tac, dtac real_le_anti_sym]); by (EVERY[dtac real_mult_le_zero 3, assume_tac 3, dtac real_le_anti_sym 3]); by (dtac real_mult_less_zero1 5 THEN assume_tac 5); by (auto_tac (claset() addDs [real_less_asym,sym], - simpset() addsimps [real_minus_mult_eq2 RS sym] @real_mult_ac)); + simpset() addsimps [real_minus_mult_eq2 RS sym] @real_mult_ac)); qed "rabs_mult"; Goalw [rabs_def] "x~= 0r ==> rabs(rinv(x)) = rinv(rabs(x))"; -by (auto_tac (claset(),simpset() addsimps [real_minus_rinv] - )); +by (auto_tac (claset(), simpset() addsimps [real_minus_rinv])); by (ALLGOALS(dtac not_real_leE)); by (etac real_less_asym 1); -by (blast_tac (claset() addDs [real_le_imp_less_or_eq, - real_rinv_gt_zero]) 1); +by (blast_tac (claset() addDs [real_le_imp_less_or_eq, real_rinv_gt_zero]) 1); by (dtac (rinv_not_zero RS not_sym) 1); by (rtac (real_rinv_less_zero RSN (2,real_less_asym)) 1); by (assume_tac 2); by (blast_tac (claset() addSDs [real_le_imp_less_or_eq]) 1); qed "rabs_rinv"; -val [prem] = goal thy "y ~= 0r ==> rabs(x*rinv(y)) = rabs(x)*rinv(rabs(y))"; +Goal "y ~= 0r ==> rabs(x*rinv(y)) = rabs(x)*rinv(rabs(y))"; by (res_inst_tac [("c1","rabs y")] (real_mult_left_cancel RS subst) 1); -by (simp_tac (simpset() addsimps [(rabs_not_zero_iff RS sym), prem]) 1); -by (simp_tac (simpset() addsimps [(rabs_mult RS sym) ,real_mult_inv_right, - prem,rabs_not_zero_iff RS sym] @ real_mult_ac) 1); +by (asm_simp_tac (simpset() addsimps [rabs_not_zero_iff RS sym]) 1); +by (asm_simp_tac (simpset() addsimps [rabs_mult RS sym, real_mult_inv_right, + rabs_not_zero_iff RS sym] @ real_mult_ac) 1); qed "rabs_mult_rinv"; Goal "rabs(x+y) <= rabs x + rabs y"; -by (EVERY1 [res_inst_tac [("Q1","0r<=x+y")] (expand_if RS ssubst), rtac conjI]); +by (case_tac "0r<=x+y" 1); by (asm_simp_tac (simpset() addsimps [rabs_eqI1,real_add_le_mono,rabs_ge_self]) 1); by (asm_simp_tac @@ -113,38 +112,38 @@ Goal "rabs(w + x + y + z) <= rabs(w) + rabs(x) + rabs(y) + rabs(z)"; by (full_simp_tac (simpset() addsimps [real_add_assoc]) 1); -by (blast_tac (claset() addSIs [(rabs_triangle_ineq RS real_le_trans), +by (blast_tac (claset() addSIs [rabs_triangle_ineq RS real_le_trans, real_add_left_le_mono1]) 1); qed "rabs_triangle_ineq_four"; Goalw [rabs_def] "rabs(-x)=rabs(x)"; -by (auto_tac (claset() addSDs [not_real_leE,real_less_asym] addIs [real_le_anti_sym], - simpset() addsimps [real_ge_zero_iff])); +by (auto_tac (claset() addSDs [not_real_leE,real_less_asym] + addIs [real_le_anti_sym], + simpset() addsimps [real_ge_zero_iff])); qed "rabs_minus_cancel"; -Goal "rabs(x + -y) = rabs (y + -x)"; +Goal "rabs(x + (-y)) = rabs (y + (-x))"; by (rtac (rabs_minus_cancel RS subst) 1); -by (simp_tac (simpset() addsimps - [real_add_commute]) 1); +by (simp_tac (simpset() addsimps [real_add_commute]) 1); qed "rabs_minus_add_cancel"; -Goal "rabs(x + -y) <= rabs x + rabs y"; +Goal "rabs(x + (-y)) <= rabs x + rabs y"; by (res_inst_tac [("x1","y")] (rabs_minus_cancel RS subst) 1); by (rtac rabs_triangle_ineq 1); qed "rabs_triangle_minus_ineq"; -Goal "rabs (x + y + (-l + -m)) <= rabs(x + -l) + rabs(y + -m)"; +Goal "rabs (x + y + ((-l) + (-m))) <= rabs(x + (-l)) + rabs(y + (-m))"; by (full_simp_tac (simpset() addsimps [real_add_assoc]) 1); by (res_inst_tac [("x1","y")] (real_add_left_commute RS ssubst) 1); by (rtac (real_add_assoc RS subst) 1); by (rtac rabs_triangle_ineq 1); qed "rabs_sum_triangle_ineq"; -Goal "rabs(x) <= rabs(x + -y) + rabs(y)"; -by (res_inst_tac [("j","rabs(x + -y + y)")] real_le_trans 1); +Goal "rabs(x) <= rabs(x + (-y)) + rabs(y)"; +by (res_inst_tac [("j","rabs(x + (-y) + y)")] real_le_trans 1); by (simp_tac (simpset() addsimps [real_add_assoc]) 1); by (simp_tac (simpset() addsimps [real_add_assoc RS sym, - rabs_triangle_ineq]) 1); + rabs_triangle_ineq]) 1); qed "rabs_triangle_ineq_minus_cancel"; Goal "[| rabs x < r; rabs y < s |] ==> rabs(x+y) < r+s"; @@ -153,7 +152,7 @@ by (REPEAT (ares_tac [real_add_less_mono] 1)); qed "rabs_add_less"; -Goal "[| rabs x < r; rabs y < s |] ==> rabs(x+ -y) < r+s"; +Goal "[| rabs x < r; rabs y < s |] ==> rabs(x+ (-y)) < r+s"; by (rotate_tac 1 1); by (dtac (rabs_minus_cancel RS ssubst) 1); by (asm_simp_tac (simpset() addsimps [rabs_add_less]) 1); @@ -169,7 +168,7 @@ addIs [real_less_trans]) 1); qed "real_mult_less_trans"; -Goal "!!(x::real) y.[| 0r<=y; x y*x y*x rabs x < r"; @@ -225,7 +224,7 @@ Goal "rabs x =x | rabs x = -x"; by (cut_inst_tac [("R1.0","0r"),("R2.0","x")] real_linear 1); by (blast_tac (claset() addIs [rabs_eqI2,rabs_minus_eqI2, - rabs_zero,rabs_minus_zero]) 1); + rabs_zero,rabs_minus_zero]) 1); qed "rabs_disj"; Goal "rabs x = y ==> x = y | -x = y"; @@ -239,9 +238,8 @@ by Safe_tac; by (rtac (real_less_swap_iff RS iffD2) 1); by (asm_simp_tac (simpset() addsimps [(rabs_ge_minus_self - RS real_le_less_trans)]) 1); -by (asm_simp_tac (simpset() addsimps [(rabs_ge_self - RS real_le_less_trans)]) 1); + RS real_le_less_trans)]) 1); +by (asm_simp_tac (simpset() addsimps [rabs_ge_self RS real_le_less_trans]) 1); by (EVERY1 [dtac (real_less_swap_iff RS iffD1), rotate_tac 1, dtac (real_minus_minus RS subst), cut_inst_tac [("x","x")] rabs_disj, dtac disjE ]); @@ -252,57 +250,57 @@ by (auto_tac (claset(),simpset() addsimps [rabs_interval_iff])); by (dtac (real_less_swap_iff RS iffD1) 1); by (dtac (real_less_swap_iff RS iffD1) 2); -by (Auto_tac); +by Auto_tac; qed "rabs_interval_iff2"; -Goal "!!x. rabs x <= r ==> -r<=x & x<=r"; +Goal "rabs x <= r ==> -r<=x & x<=r"; by (dtac real_le_imp_less_or_eq 1); by (auto_tac (claset() addSDs [real_less_imp_le], - simpset() addsimps [rabs_interval_iff,rabs_ge_self])); + simpset() addsimps [rabs_interval_iff,rabs_ge_self])); by (auto_tac (claset(),simpset() addsimps [real_le_def])); by (dtac (real_less_swap_iff RS iffD1) 1); -by (auto_tac (claset() addSDs [rabs_ge_minus_self - RS real_le_less_trans],simpset() addsimps [real_less_not_refl])); +by (auto_tac (claset() addSDs [rabs_ge_minus_self RS real_le_less_trans], + simpset() addsimps [real_less_not_refl])); qed "rabs_leD"; -Goal "!!x. [| -r rabs x <= r"; +Goal "[| -r rabs x <= r"; by (dtac real_le_imp_less_or_eq 1); by (Step_tac 1); by (blast_tac (claset() addIs - [rabs_interval_iff RS iffD2 RS real_less_imp_le]) 1); -by (auto_tac (claset() addSDs [rabs_eqI2],simpset() addsimps - [real_le_def,real_gt_zero_iff RS sym,real_less_not_refl])); + [rabs_interval_iff RS iffD2 RS real_less_imp_le]) 1); +by (auto_tac (claset() addSDs [rabs_eqI2], + simpset() addsimps + [real_le_def,real_gt_zero_iff RS sym,real_less_not_refl])); qed "rabs_leI1"; -Goal "!!x. [| -r<=x; x<=r |] ==> rabs x <= r"; +Goal "[| -r<=x; x<=r |] ==> rabs x <= r"; by (REPEAT(dtac real_le_imp_less_or_eq 1)); by (Step_tac 1); -by (blast_tac (claset() addIs - [rabs_interval_iff RS iffD2 RS real_less_imp_le]) 1); -by (auto_tac (claset() addSDs [rabs_eqI2],simpset() addsimps - [real_le_def,real_gt_zero_iff RS sym,real_less_not_refl, - rabs_minus_cancel])); +by (blast_tac (claset() + addIs [rabs_interval_iff RS iffD2 RS real_less_imp_le]) 1); +by (auto_tac (claset() addSDs [rabs_eqI2], + simpset() addsimps + [real_le_def,real_gt_zero_iff RS sym,real_less_not_refl, + rabs_minus_cancel])); by (cut_inst_tac [("x","r")] rabs_disj 1); by (rotate_tac 1 1); -by (auto_tac (claset(),simpset() addsimps [real_less_not_refl])); +by (auto_tac (claset(), simpset() addsimps [real_less_not_refl])); qed "rabs_leI"; Goal "(rabs x <= r) = (-r<=x & x<=r)"; by (blast_tac (claset() addSIs [rabs_leD,rabs_leI]) 1); qed "rabs_le_interval_iff"; -Goal - "(rabs (x + -y) < r) = (y + -r < x & x < y + r)"; -by (auto_tac (claset(),simpset() addsimps - [rabs_interval_iff])); +Goal "(rabs (x + (-y)) < r) = (y + (-r) < x & x < y + r)"; +by (auto_tac (claset(), simpset() addsimps [rabs_interval_iff])); by (ALLGOALS(dtac real_less_sum_gt_zero)); by (ALLGOALS(dtac real_less_sum_gt_zero)); by (ALLGOALS(rtac real_sum_gt_zero_less)); -by (auto_tac (claset(),simpset() addsimps - [real_minus_add_distrib] addsimps real_add_ac)); +by (auto_tac (claset(), + simpset() addsimps [real_minus_add_distrib] @ real_add_ac)); qed "rabs_add_minus_interval_iff"; -Goal "!!k. 0r < k ==> 0r < k + rabs(x)"; +Goal "0r < k ==> 0r < k + rabs(x)"; by (res_inst_tac [("t","0r")] (real_add_zero_right RS subst) 1); by (etac (rabs_ge_zero RSN (2,real_add_less_le_mono)) 1); qed "rabs_add_pos_gt_zero"; diff -r fdb397af4cab -r 48e235179ffb src/HOL/Real/RealDef.ML --- a/src/HOL/Real/RealDef.ML Wed Jul 28 22:01:58 1999 +0200 +++ b/src/HOL/Real/RealDef.ML Thu Jul 29 12:44:57 1999 +0200 @@ -206,20 +206,20 @@ qed "real_add_zero_right"; Addsimps [real_add_zero_right]; -Goalw [real_zero_def] "z + -z = 0r"; +Goalw [real_zero_def] "z + (-z) = 0r"; by (res_inst_tac [("z","z")] eq_Abs_real 1); by (asm_full_simp_tac (simpset() addsimps [real_minus, real_add, preal_add_commute]) 1); qed "real_add_minus"; Addsimps [real_add_minus]; -Goal "-z + z = 0r"; +Goal "(-z) + z = 0r"; by (simp_tac (simpset() addsimps [real_add_commute]) 1); qed "real_add_minus_left"; Addsimps [real_add_minus_left]; -Goal "z + (- z + w) = (w::real)"; +Goal "z + ((- z) + w) = (w::real)"; by (simp_tac (simpset() addsimps [real_add_assoc RS sym]) 1); qed "real_add_minus_cancel"; @@ -259,7 +259,7 @@ by (Fast_tac 1); qed "real_as_add_inverse_ex"; -Goal "-(x + y) = -x + -(y::real)"; +Goal "-(x + y) = (-x) + (- y :: real)"; by (res_inst_tac [("z","x")] eq_Abs_real 1); by (res_inst_tac [("z","y")] eq_Abs_real 1); by (auto_tac (claset(),simpset() addsimps [real_minus,real_add])); @@ -269,7 +269,7 @@ Goal "((x::real) + y = x + z) = (y = z)"; by (Step_tac 1); -by (dres_inst_tac [("f","%t.-x + t")] arg_cong 1); +by (dres_inst_tac [("f","%t. (-x) + t")] arg_cong 1); by (asm_full_simp_tac (simpset() addsimps [real_add_assoc RS sym]) 1); qed "real_add_left_cancel"; @@ -277,18 +277,18 @@ by (simp_tac (simpset() addsimps [real_add_commute,real_add_left_cancel]) 1); qed "real_add_right_cancel"; -Goal "((x::real) = y) = (0r = x + - y)"; +Goal "((x::real) = y) = (0r = x + (- y))"; by (Step_tac 1); by (res_inst_tac [("x1","-y")] (real_add_right_cancel RS iffD1) 2); -by (Auto_tac); +by Auto_tac; qed "real_eq_minus_iff"; -Goal "((x::real) = y) = (x + - y = 0r)"; +Goal "((x::real) = y) = (x + (- y) = 0r)"; by (Step_tac 1); by (res_inst_tac [("x1","-y")] (real_add_right_cancel RS iffD1) 2); -by (Auto_tac); +by Auto_tac; qed "real_eq_minus_iff2"; Goal "0r - x = -x"; @@ -391,7 +391,7 @@ Addsimps [real_mult_0_right, real_mult_0]; -Goal "-(x * y) = -x * (y::real)"; +Goal "-(x * y) = (-x) * (y::real)"; by (res_inst_tac [("z","x")] eq_Abs_real 1); by (res_inst_tac [("z","y")] eq_Abs_real 1); by (auto_tac (claset(), @@ -399,7 +399,7 @@ @ preal_mult_ac @ preal_add_ac)); qed "real_minus_mult_eq1"; -Goal "-(x * y) = x * -(y::real)"; +Goal "-(x * y) = x * (- y :: real)"; by (res_inst_tac [("z","x")] eq_Abs_real 1); by (res_inst_tac [("z","y")] eq_Abs_real 1); by (auto_tac (claset(), @@ -407,34 +407,34 @@ @ preal_mult_ac @ preal_add_ac)); qed "real_minus_mult_eq2"; -Goal "- 1r * z = -z"; +Goal "(- 1r) * z = -z"; by (simp_tac (simpset() addsimps [real_minus_mult_eq1 RS sym]) 1); qed "real_mult_minus_1"; Addsimps [real_mult_minus_1]; -Goal "z * - 1r = -z"; +Goal "z * (- 1r) = -z"; by (stac real_mult_commute 1); by (Simp_tac 1); qed "real_mult_minus_1_right"; Addsimps [real_mult_minus_1_right]; -Goal "-x * -y = x * (y::real)"; +Goal "(-x) * (-y) = x * (y::real)"; by (full_simp_tac (simpset() addsimps [real_minus_mult_eq2 RS sym, - real_minus_mult_eq1 RS sym]) 1); + real_minus_mult_eq1 RS sym]) 1); qed "real_minus_mult_cancel"; Addsimps [real_minus_mult_cancel]; -Goal "-x * y = x * -(y::real)"; +Goal "(-x) * y = x * (- y :: real)"; by (full_simp_tac (simpset() addsimps [real_minus_mult_eq2 RS sym, - real_minus_mult_eq1 RS sym]) 1); + real_minus_mult_eq1 RS sym]) 1); qed "real_minus_mult_commute"; (*----------------------------------------------------------------------------- - -----------------------------------------------------------------------------*) + ----------------------------------------------------------------------------*) (** Lemmas **) @@ -493,17 +493,17 @@ Goal "!!(x::real). x ~= 0r ==> ? y. y*x = 1r"; by (asm_simp_tac (simpset() addsimps [real_mult_commute, - real_mult_inv_right_ex]) 1); + real_mult_inv_right_ex]) 1); qed "real_mult_inv_left_ex"; -Goalw [rinv_def] "!!(x::real). x ~= 0r ==> rinv(x)*x = 1r"; +Goalw [rinv_def] "x ~= 0r ==> rinv(x)*x = 1r"; by (forward_tac [real_mult_inv_left_ex] 1); by (Step_tac 1); by (rtac selectI2 1); by Auto_tac; qed "real_mult_inv_left"; -Goal "!!(x::real). x ~= 0r ==> x*rinv(x) = 1r"; +Goal "x ~= 0r ==> x*rinv(x) = 1r"; by (auto_tac (claset() addIs [real_mult_commute RS subst], simpset() addsimps [real_mult_inv_left])); qed "real_mult_inv_right"; @@ -517,15 +517,16 @@ Goal "(c::real) ~= 0r ==> (a*c=b*c) = (a=b)"; by (Step_tac 1); by (dres_inst_tac [("f","%x. x*rinv c")] arg_cong 1); -by (asm_full_simp_tac (simpset() addsimps [real_mult_inv_right] @ real_mult_ac) 1); +by (asm_full_simp_tac + (simpset() addsimps [real_mult_inv_right] @ real_mult_ac) 1); qed "real_mult_right_cancel"; -Goal "!!a. c*a ~= c*b ==> a ~= b"; -by (Auto_tac); +Goal "c*a ~= c*b ==> a ~= b"; +by Auto_tac; qed "real_mult_left_cancel_ccontr"; -Goal "!!a. a*c ~= b*c ==> a ~= b"; -by (Auto_tac); +Goal "a*c ~= b*c ==> a ~= b"; +by Auto_tac; qed "real_mult_right_cancel_ccontr"; Goalw [rinv_def] "x ~= 0r ==> rinv(x) ~= 0r"; @@ -539,7 +540,7 @@ Addsimps [real_mult_inv_left,real_mult_inv_right]; -Goal "!!x. [| x ~= 0r; y ~= 0r |] ==> x * y ~= 0r"; +Goal "[| x ~= 0r; y ~= 0r |] ==> x * y ~= 0r"; by (Step_tac 1); by (dres_inst_tac [("f","%z. rinv x*z")] arg_cong 1); by (asm_full_simp_tac (simpset() addsimps [real_mult_assoc RS sym]) 1); @@ -569,8 +570,7 @@ by Auto_tac; qed "real_minus_rinv"; -Goal "!!x y. [| x ~= 0r; y ~= 0r |] \ -\ ==> rinv(x*y) = rinv(x)*rinv(y)"; +Goal "[| x ~= 0r; y ~= 0r |] ==> rinv(x*y) = rinv(x)*rinv(y)"; by (forw_inst_tac [("y","y")] real_mult_not_zero 1 THEN assume_tac 1); by (res_inst_tac [("c1","x")] (real_mult_left_cancel RS iffD1) 1); by (auto_tac (claset(),simpset() addsimps [real_mult_assoc RS sym])); @@ -778,7 +778,7 @@ addEs [real_less_irrefl]) 1); qed "real_of_preal_not_less_zero"; -Goal "0r < - - real_of_preal m"; +Goal "0r < - (- real_of_preal m)"; by (simp_tac (simpset() addsimps [real_of_preal_zero_less]) 1); qed "real_minus_minus_zero_less"; @@ -970,7 +970,7 @@ qed "real_minus_zero_less_iff2"; (*Alternative definition for real_less*) -Goal "!!(R::real). R < S ==> ? T. 0r < T & R + T = S"; +Goal "R < S ==> ? T. 0r < T & R + T = S"; by (res_inst_tac [("x","R")] real_of_preal_trichotomyE 1); by (ALLGOALS(res_inst_tac [("x","S")] real_of_preal_trichotomyE)); by (auto_tac (claset() addSDs [preal_less_add_left_Ex], @@ -988,19 +988,19 @@ qed "real_less_add_positive_left_Ex"; (** change naff name(s)! **) -Goal "(W < S) ==> (0r < S + -W)"; +Goal "(W < S) ==> (0r < S + (-W))"; by (dtac real_less_add_positive_left_Ex 1); by (auto_tac (claset(), simpset() addsimps [real_add_minus, real_add_zero_right] @ real_add_ac)); qed "real_less_sum_gt_zero"; -Goal "!!S::real. T = S + W ==> S = T + -W"; +Goal "!!S::real. T = S + W ==> S = T + (-W)"; by (asm_simp_tac (simpset() addsimps real_add_ac) 1); qed "real_lemma_change_eq_subj"; (* FIXME: long! *) -Goal "(0r < S + -W) ==> (W < S)"; +Goal "(0r < S + (-W)) ==> (W < S)"; by (rtac ccontr 1); by (dtac (real_leI RS real_le_imp_less_or_eq) 1); by (auto_tac (claset(), @@ -1015,7 +1015,7 @@ by (auto_tac (claset() addEs [real_less_asym], simpset())); qed "real_sum_gt_zero_less"; -Goal "(0r < S + -W) = (W < S)"; +Goal "(0r < S + (-W)) = (W < S)"; by (blast_tac (claset() addIs [real_less_sum_gt_zero, real_sum_gt_zero_less]) 1); qed "real_less_sum_gt_0_iff"; diff -r fdb397af4cab -r 48e235179ffb src/HOL/Real/RealDef.thy --- a/src/HOL/Real/RealDef.thy Wed Jul 28 22:01:58 1999 +0200 +++ b/src/HOL/Real/RealDef.thy Thu Jul 29 12:44:57 1999 +0200 @@ -33,7 +33,7 @@ real_minus_def "- R == Abs_real(UN (x,y):Rep_real(R). realrel^^{(y,x)})" - real_diff_def "x - y == x + -(y::real)" + real_diff_def "x - y == x + (- y :: real)" constdefs @@ -49,7 +49,7 @@ "real_of_posnat n == real_of_preal(preal_of_prat(prat_of_pnat(pnat_of_nat n)))" real_of_nat :: nat => real - "real_of_nat n == real_of_posnat n + -1r" + "real_of_nat n == real_of_posnat n + (-1r)" defs diff -r fdb397af4cab -r 48e235179ffb src/HOL/UNITY/Deadlock.ML --- a/src/HOL/UNITY/Deadlock.ML Wed Jul 28 22:01:58 1999 +0200 +++ b/src/HOL/UNITY/Deadlock.ML Thu Jul 29 12:44:57 1999 +0200 @@ -9,15 +9,13 @@ (*Trivial, two-process case*) Goalw [constrains_def, stable_def] - "[| F : (A Int B) co A; F : (B Int A) co B |] \ -\ ==> F : stable (A Int B)"; + "[| F : (A Int B) co A; F : (B Int A) co B |] ==> F : stable (A Int B)"; by (Blast_tac 1); result(); (*a simplification step*) -Goal "(INT i: atMost n. A(Suc i) Int A i) = \ -\ (INT i: atMost (Suc n). A i)"; +Goal "(INT i: atMost n. A(Suc i) Int A i) = (INT i: atMost (Suc n). A i)"; by (induct_tac "n" 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps [atMost_Suc]))); by (blast_tac (claset() addEs [le_SucE] addSEs [equalityE]) 1); @@ -25,8 +23,8 @@ (*Dual of the required property. Converse inclusion fails.*) -Goal "(UN i: lessThan n. A i) Int -(A n) <= \ -\ (UN i: lessThan n. (A i) Int -(A(Suc i)))"; +Goal "(UN i: lessThan n. A i) Int (- A n) <= \ +\ (UN i: lessThan n. (A i) Int (- A (Suc i)))"; by (induct_tac "n" 1); by (Asm_simp_tac 1); by (simp_tac (simpset() addsimps [lessThan_Suc]) 1); @@ -56,13 +54,12 @@ by (induct_tac "n" 1); by (Asm_simp_tac 1); by (asm_simp_tac - (simpset() addsimps Int_ac @ - [Int_Un_distrib, Int_Un_distrib2, lemma, - lessThan_Suc, atMost_Suc]) 1); + (simpset() addsimps Int_ac @ [Int_Un_distrib, Int_Un_distrib2, lemma, + lessThan_Suc, atMost_Suc]) 1); qed "INT_le_equals_Int"; Goal "(INT i: atMost (Suc n). A i) = \ -\ A 0 Int (INT i: atMost n. -A i Un A(Suc i))"; +\ A 0 Int (INT i: atMost n. -A i Un A(Suc i))"; by (simp_tac (simpset() addsimps [lessThan_Suc_atMost, INT_le_equals_Int]) 1); qed "INT_le_Suc_equals_Int"; @@ -73,9 +70,8 @@ \ ALL i: atMost n. F : (A(Suc i) Int A i) co \ \ (-A i Un A(Suc i)) |] \ \ ==> F : stable (INT i: atMost (Suc n). A i)"; - by (rtac ([zeroprem, allprem RS ball_constrains_INT] MRS - constrains_Int RS constrains_weaken) 1); + constrains_Int RS constrains_weaken) 1); by (simp_tac (simpset() addsimps [Collect_le_Int_equals, Int_assoc, INT_absorb]) 1); by (simp_tac (simpset() addsimps [INT_le_Suc_equals_Int]) 1); diff -r fdb397af4cab -r 48e235179ffb src/HOL/equalities.ML --- a/src/HOL/equalities.ML Wed Jul 28 22:01:58 1999 +0200 +++ b/src/HOL/equalities.ML Thu Jul 29 12:44:57 1999 +0200 @@ -338,25 +338,25 @@ section "Set complement"; -Goal "A Int -A = {}"; +Goal "A Int (-A) = {}"; by (Blast_tac 1); qed "Compl_disjoint"; Addsimps[Compl_disjoint]; -Goal "A Un -A = UNIV"; +Goal "A Un (-A) = UNIV"; by (Blast_tac 1); qed "Compl_partition"; -Goal "- -A = (A:: 'a set)"; +Goal "- (-A) = (A:: 'a set)"; by (Blast_tac 1); qed "double_complement"; Addsimps[double_complement]; -Goal "-(A Un B) = -A Int -B"; +Goal "-(A Un B) = (-A) Int (-B)"; by (Blast_tac 1); qed "Compl_Un"; -Goal "-(A Int B) = -A Un -B"; +Goal "-(A Int B) = (-A) Un (-B)"; by (Blast_tac 1); qed "Compl_Int"; @@ -615,7 +615,7 @@ section "-"; -Goal "A-B = A Int -B"; +Goal "A-B = A Int (-B)"; by (Blast_tac 1); qed "Diff_eq"; @@ -719,7 +719,7 @@ by (Blast_tac 1); qed "Diff_Int_distrib2"; -Goal "A - - B = A Int B"; +Goal "A - (- B) = A Int B"; by Auto_tac; qed "Diff_Compl"; Addsimps [Diff_Compl]; diff -r fdb397af4cab -r 48e235179ffb src/HOL/simpdata.ML --- a/src/HOL/simpdata.ML Wed Jul 28 22:01:58 1999 +0200 +++ b/src/HOL/simpdata.ML Thu Jul 29 12:44:57 1999 +0200 @@ -285,11 +285,11 @@ by (Blast_tac 1); qed "if_False"; -Goalw [if_def] "!!P. P ==> (if P then x else y) = x"; +Goalw [if_def] "P ==> (if P then x else y) = x"; by (Blast_tac 1); qed "if_P"; -Goalw [if_def] "!!P. ~P ==> (if P then x else y) = y"; +Goalw [if_def] "~P ==> (if P then x else y) = y"; by (Blast_tac 1); qed "if_not_P"; @@ -319,8 +319,7 @@ qed "if_eq_cancel"; (*This form is useful for expanding IFs on the RIGHT of the ==> symbol*) -Goal - "(if P then Q else R) = ((P-->Q) & (~P-->R))"; +Goal "(if P then Q else R) = ((P-->Q) & (~P-->R))"; by (rtac split_if 1); qed "if_bool_eq_conj"; @@ -398,8 +397,6 @@ val Addsplits = Splitter.Addsplits; val Delsplits = Splitter.Delsplits; -(** 'if' congruence rules: neither included by default! *) - (*In general it seems wrong to add distributive laws by default: they might cause exponential blow-up. But imp_disjL has been in for a while and cannot be removed without affecting existing proofs. Moreover, @@ -464,7 +461,8 @@ by (asm_simp_tac (HOL_ss addsimps prems) 1); qed "if_cong"; -(*Prevents simplification of x and y: much faster*) +(*Prevents simplification of x and y: faster and allows the execution + of functional programs. NOW THE DEFAULT.*) Goal "b=c ==> (if b then x else y) = (if c then x else y)"; by (etac arg_cong 1); qed "if_weak_cong";