--- a/src/HOL/Hyperreal/NatStar.ML Fri Feb 07 15:36:54 2003 +0100
+++ b/src/HOL/Hyperreal/NatStar.ML Fri Feb 07 16:40:23 2003 +0100
@@ -70,7 +70,7 @@
simpset() addsimps [starsetNat_n_Int RS sym]));
qed "InternalNatSets_Int";
-Goalw [starsetNat_def] "*sNat* (-A) = -(*sNat* A)";
+Goalw [starsetNat_def] "*sNat* (-A) = -( *sNat* A)";
by (Auto_tac);
by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
by (res_inst_tac [("z","x")] eq_Abs_hypnat 2);
@@ -78,7 +78,7 @@
by (TRYALL(Ultra_tac));
qed "NatStar_Compl";
-Goalw [starsetNat_n_def] "*sNatn* ((%n. - A n)) = -(*sNatn* A)";
+Goalw [starsetNat_n_def] "*sNatn* ((%n. - A n)) = -( *sNatn* A)";
by (Auto_tac);
by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
by (res_inst_tac [("z","x")] eq_Abs_hypnat 2);
@@ -148,7 +148,7 @@
by Auto_tac;
qed "starsetNat_starsetNat_n_eq";
-Goalw [InternalNatSets_def] "(*sNat* X) : InternalNatSets";
+Goalw [InternalNatSets_def] "( *sNat* X) : InternalNatSets";
by (auto_tac (claset(),
simpset() addsimps [starsetNat_starsetNat_n_eq]));
qed "InternalNatSets_starsetNat_n";
@@ -195,7 +195,7 @@
(* f::nat=>real *)
Goalw [starfunNat_def]
- "(*fNat* f) (Abs_hypnat(hypnatrel``{%n. X n})) = \
+ "( *fNat* f) (Abs_hypnat(hypnatrel``{%n. X n})) = \
\ Abs_hypreal(hyprel `` {%n. f (X n)})";
by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
by (simp_tac (simpset() addsimps
@@ -205,7 +205,7 @@
(* f::nat=>nat *)
Goalw [starfunNat2_def]
- "(*fNat2* f) (Abs_hypnat(hypnatrel``{%n. X n})) = \
+ "( *fNat2* f) (Abs_hypnat(hypnatrel``{%n. X n})) = \
\ Abs_hypnat(hypnatrel `` {%n. f (X n)})";
by (res_inst_tac [("f","Abs_hypnat")] arg_cong 1);
by (simp_tac (simpset() addsimps
@@ -216,12 +216,12 @@
(*---------------------------------------------
multiplication: ( *f ) x ( *g ) = *(f x g)
---------------------------------------------*)
-Goal "(*fNat* f) z * (*fNat* g) z = (*fNat* (%x. f x * g x)) z";
+Goal "( *fNat* f) z * ( *fNat* g) z = ( *fNat* (%x. f x * g x)) z";
by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
by (auto_tac (claset(), simpset() addsimps [starfunNat,hypreal_mult]));
qed "starfunNat_mult";
-Goal "(*fNat2* f) z * (*fNat2* g) z = (*fNat2* (%x. f x * g x)) z";
+Goal "( *fNat2* f) z * ( *fNat2* g) z = ( *fNat2* (%x. f x * g x)) z";
by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
by (auto_tac (claset(), simpset() addsimps [starfunNat2,hypnat_mult]));
qed "starfunNat2_mult";
@@ -229,17 +229,17 @@
(*---------------------------------------
addition: ( *f ) + ( *g ) = *(f + g)
---------------------------------------*)
-Goal "(*fNat* f) z + (*fNat* g) z = (*fNat* (%x. f x + g x)) z";
+Goal "( *fNat* f) z + ( *fNat* g) z = ( *fNat* (%x. f x + g x)) z";
by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
by (auto_tac (claset(), simpset() addsimps [starfunNat,hypreal_add]));
qed "starfunNat_add";
-Goal "(*fNat2* f) z + (*fNat2* g) z = (*fNat2* (%x. f x + g x)) z";
+Goal "( *fNat2* f) z + ( *fNat2* g) z = ( *fNat2* (%x. f x + g x)) z";
by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
by (auto_tac (claset(), simpset() addsimps [starfunNat2,hypnat_add]));
qed "starfunNat2_add";
-Goal "(*fNat2* f) z - (*fNat2* g) z = (*fNat2* (%x. f x - g x)) z";
+Goal "( *fNat2* f) z - ( *fNat2* g) z = ( *fNat2* (%x. f x - g x)) z";
by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
by (auto_tac (claset(), simpset() addsimps [starfunNat2, hypnat_minus]));
qed "starfunNat2_minus";
@@ -249,18 +249,18 @@
---------------------------------------*)
(***** ( *f::nat=>real ) o ( *g::nat=>nat ) = *(f o g) *****)
-Goal "(*fNat* f) o (*fNat2* g) = (*fNat* (f o g))";
+Goal "( *fNat* f) o ( *fNat2* g) = ( *fNat* (f o g))";
by (rtac ext 1);
by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
by (auto_tac (claset(), simpset() addsimps [starfunNat2, starfunNat]));
qed "starfunNatNat2_o";
-Goal "(%x. (*fNat* f) ((*fNat2* g) x)) = (*fNat* (%x. f(g x)))";
+Goal "(%x. ( *fNat* f) (( *fNat2* g) x)) = ( *fNat* (%x. f(g x)))";
by (rtac ( simplify (simpset() addsimps [o_def]) starfunNatNat2_o) 1);
qed "starfunNatNat2_o2";
(***** ( *f::nat=>nat ) o ( *g::nat=>nat ) = *(f o g) *****)
-Goal "(*fNat2* f) o (*fNat2* g) = (*fNat2* (f o g))";
+Goal "( *fNat2* f) o ( *fNat2* g) = ( *fNat2* (f o g))";
by (rtac ext 1);
by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
by (auto_tac (claset(), simpset() addsimps [starfunNat2]));
@@ -268,38 +268,38 @@
(***** ( *f::real=>real ) o ( *g::nat=>real ) = *(f o g) *****)
-Goal "(*f* f) o (*fNat* g) = (*fNat* (f o g))";
+Goal "( *f* f) o ( *fNat* g) = ( *fNat* (f o g))";
by (rtac ext 1);
by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
by (auto_tac (claset(), simpset() addsimps [starfunNat,starfun]));
qed "starfun_stafunNat_o";
-Goal "(%x. (*f* f) ((*fNat* g) x)) = (*fNat* (%x. f (g x)))";
+Goal "(%x. ( *f* f) (( *fNat* g) x)) = ( *fNat* (%x. f (g x)))";
by (rtac ( simplify (simpset() addsimps [o_def]) starfun_stafunNat_o) 1);
qed "starfun_stafunNat_o2";
(*--------------------------------------
NS extension of constant function
--------------------------------------*)
-Goal "(*fNat* (%x. k)) z = hypreal_of_real k";
+Goal "( *fNat* (%x. k)) z = hypreal_of_real k";
by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
by (auto_tac (claset(), simpset() addsimps [starfunNat, hypreal_of_real_def]));
qed "starfunNat_const_fun";
Addsimps [starfunNat_const_fun];
-Goal "(*fNat2* (%x. k)) z = hypnat_of_nat k";
+Goal "( *fNat2* (%x. k)) z = hypnat_of_nat k";
by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
by (auto_tac (claset(), simpset() addsimps [starfunNat2, hypnat_of_nat_def]));
qed "starfunNat2_const_fun";
Addsimps [starfunNat2_const_fun];
-Goal "- (*fNat* f) x = (*fNat* (%x. - f x)) x";
+Goal "- ( *fNat* f) x = ( *fNat* (%x. - f x)) x";
by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
by (auto_tac (claset(), simpset() addsimps [starfunNat, hypreal_minus]));
qed "starfunNat_minus";
-Goal "inverse ((*fNat* f) x) = (*fNat* (%x. inverse (f x))) x";
+Goal "inverse (( *fNat* f) x) = ( *fNat* (%x. inverse (f x))) x";
by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
by (auto_tac (claset(), simpset() addsimps [starfunNat, hypreal_inverse]));
qed "starfunNat_inverse";
@@ -310,20 +310,20 @@
for all natural arguments (c.f. Hoskins pg. 107- SEQ)
-------------------------------------------------------*)
-Goal "(*fNat* f) (hypnat_of_nat a) = hypreal_of_real (f a)";
+Goal "( *fNat* f) (hypnat_of_nat a) = hypreal_of_real (f a)";
by (auto_tac (claset(),
simpset() addsimps [starfunNat,hypnat_of_nat_def,hypreal_of_real_def]));
qed "starfunNat_eq";
Addsimps [starfunNat_eq];
-Goal "(*fNat2* f) (hypnat_of_nat a) = hypnat_of_nat (f a)";
+Goal "( *fNat2* f) (hypnat_of_nat a) = hypnat_of_nat (f a)";
by (auto_tac (claset(), simpset() addsimps [starfunNat2,hypnat_of_nat_def]));
qed "starfunNat2_eq";
Addsimps [starfunNat2_eq];
-Goal "(*fNat* f) (hypnat_of_nat a) @= hypreal_of_real (f a)";
+Goal "( *fNat* f) (hypnat_of_nat a) @= hypreal_of_real (f a)";
by (Auto_tac);
qed "starfunNat_approx";
@@ -333,7 +333,7 @@
--- used for limit comparison of sequences
----------------------------------------------------------------*)
Goal "ALL n. N <= n --> f n <= g n \
-\ ==> ALL n. hypnat_of_nat N <= n --> (*fNat* f) n <= (*fNat* g) n";
+\ ==> ALL n. hypnat_of_nat N <= n --> ( *fNat* f) n <= ( *fNat* g) n";
by (Step_tac 1);
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
by (auto_tac (claset(),
@@ -345,7 +345,7 @@
(*****----- and another -----*****)
Goal "ALL n. N <= n --> f n < g n \
-\ ==> ALL n. hypnat_of_nat N <= n --> (*fNat* f) n < (*fNat* g) n";
+\ ==> ALL n. hypnat_of_nat N <= n --> ( *fNat* f) n < ( *fNat* g) n";
by (Step_tac 1);
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
by (auto_tac (claset(),
@@ -358,7 +358,7 @@
(*----------------------------------------------------------------
NS extension when we displace argument by one
---------------------------------------------------------------*)
-Goal "(*fNat* (%n. f (Suc n))) N = (*fNat* f) (N + (1::hypnat))";
+Goal "( *fNat* (%n. f (Suc n))) N = ( *fNat* f) (N + (1::hypnat))";
by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
by (auto_tac (claset(),
simpset() addsimps [starfunNat, hypnat_one_def,hypnat_add]));
@@ -367,7 +367,7 @@
(*----------------------------------------------------------------
NS extension with rabs
---------------------------------------------------------------*)
-Goal "(*fNat* (%n. abs (f n))) N = abs((*fNat* f) N)";
+Goal "( *fNat* (%n. abs (f n))) N = abs(( *fNat* f) N)";
by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
by (auto_tac (claset(), simpset() addsimps [starfunNat, hypreal_hrabs]));
qed "starfunNat_rabs";
@@ -375,19 +375,19 @@
(*----------------------------------------------------------------
The hyperpow function as a NS extension of realpow
----------------------------------------------------------------*)
-Goal "(*fNat* (%n. r ^ n)) N = (hypreal_of_real r) pow N";
+Goal "( *fNat* (%n. r ^ n)) N = (hypreal_of_real r) pow N";
by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
by (auto_tac (claset(),
simpset() addsimps [hyperpow, hypreal_of_real_def,starfunNat]));
qed "starfunNat_pow";
-Goal "(*fNat* (%n. (X n) ^ m)) N = (*fNat* X) N pow hypnat_of_nat m";
+Goal "( *fNat* (%n. (X n) ^ m)) N = ( *fNat* X) N pow hypnat_of_nat m";
by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
by (auto_tac (claset(),
simpset() addsimps [hyperpow, hypnat_of_nat_def,starfunNat]));
qed "starfunNat_pow2";
-Goalw [hypnat_of_nat_def] "(*f* (%r. r ^ n)) R = (R) pow hypnat_of_nat n";
+Goalw [hypnat_of_nat_def] "( *f* (%r. r ^ n)) R = (R) pow hypnat_of_nat n";
by (res_inst_tac [("z","R")] eq_Abs_hypreal 1);
by (auto_tac (claset(), simpset() addsimps [hyperpow,starfun]));
qed "starfun_pow";
@@ -395,14 +395,14 @@
(*-----------------------------------------------------
hypreal_of_hypnat as NS extension of real (from "nat")!
-------------------------------------------------------*)
-Goal "(*fNat* real) = hypreal_of_hypnat";
+Goal "( *fNat* real) = hypreal_of_hypnat";
by (rtac ext 1);
by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
by (auto_tac (claset(), simpset() addsimps [hypreal_of_hypnat,starfunNat]));
qed "starfunNat_real_of_nat";
Goal "N : HNatInfinite \
-\ ==> (*fNat* (%x::nat. inverse(real x))) N = inverse(hypreal_of_hypnat N)";
+\ ==> ( *fNat* (%x::nat. inverse(real x))) N = inverse(hypreal_of_hypnat N)";
by (res_inst_tac [("f1","inverse")] (starfun_stafunNat_o2 RS subst) 1);
by (subgoal_tac "hypreal_of_hypnat N ~= 0" 1);
by (auto_tac (claset(),
@@ -419,7 +419,7 @@
qed "starfunNat_n_congruent";
Goalw [starfunNat_n_def]
- "(*fNatn* f) (Abs_hypnat(hypnatrel``{%n. X n})) = \
+ "( *fNatn* f) (Abs_hypnat(hypnatrel``{%n. X n})) = \
\ Abs_hypreal(hyprel `` {%n. f n (X n)})";
by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
by Auto_tac;
@@ -429,7 +429,7 @@
(*-------------------------------------------------
multiplication: ( *fn ) x ( *gn ) = *(fn x gn)
-------------------------------------------------*)
-Goal "(*fNatn* f) z * (*fNatn* g) z = (*fNatn* (% i x. f i x * g i x)) z";
+Goal "( *fNatn* f) z * ( *fNatn* g) z = ( *fNatn* (% i x. f i x * g i x)) z";
by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
by (auto_tac (claset(), simpset() addsimps [starfunNat_n,hypreal_mult]));
qed "starfunNat_n_mult";
@@ -437,7 +437,7 @@
(*-----------------------------------------------
addition: ( *fn ) + ( *gn ) = *(fn + gn)
-----------------------------------------------*)
-Goal "(*fNatn* f) z + (*fNatn* g) z = (*fNatn* (%i x. f i x + g i x)) z";
+Goal "( *fNatn* f) z + ( *fNatn* g) z = ( *fNatn* (%i x. f i x + g i x)) z";
by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
by (auto_tac (claset(), simpset() addsimps [starfunNat_n,hypreal_add]));
qed "starfunNat_n_add";
@@ -445,7 +445,7 @@
(*-------------------------------------------------
subtraction: ( *fn ) + -( *gn ) = *(fn + -gn)
-------------------------------------------------*)
-Goal "(*fNatn* f) z + -(*fNatn* g) z = (*fNatn* (%i x. f i x + -g i x)) z";
+Goal "( *fNatn* f) z + -( *fNatn* g) z = ( *fNatn* (%i x. f i x + -g i x)) z";
by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
by (auto_tac (claset(),
simpset() addsimps [starfunNat_n, hypreal_minus,hypreal_add]));
@@ -455,7 +455,7 @@
composition: ( *fn ) o ( *gn ) = *(fn o gn)
-------------------------------------------------*)
-Goal "(*fNatn* (%i x. k)) z = hypreal_of_real k";
+Goal "( *fNatn* (%i x. k)) z = hypreal_of_real k";
by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
by (auto_tac (claset(),
simpset() addsimps [starfunNat_n, hypreal_of_real_def]));
@@ -463,17 +463,17 @@
Addsimps [starfunNat_n_const_fun];
-Goal "- (*fNatn* f) x = (*fNatn* (%i x. - (f i) x)) x";
+Goal "- ( *fNatn* f) x = ( *fNatn* (%i x. - (f i) x)) x";
by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
by (auto_tac (claset(), simpset() addsimps [starfunNat_n, hypreal_minus]));
qed "starfunNat_n_minus";
-Goal "(*fNatn* f) (hypnat_of_nat n) = Abs_hypreal(hyprel `` {%i. f i n})";
+Goal "( *fNatn* f) (hypnat_of_nat n) = Abs_hypreal(hyprel `` {%i. f i n})";
by (auto_tac (claset(), simpset() addsimps [starfunNat_n,hypnat_of_nat_def]));
qed "starfunNat_n_eq";
Addsimps [starfunNat_n_eq];
-Goal "((*fNat* f) = (*fNat* g)) = (f = g)";
+Goal "(( *fNat* f) = ( *fNat* g)) = (f = g)";
by Auto_tac;
by (rtac ext 1 THEN rtac ccontr 1);
by (dres_inst_tac [("x","hypnat_of_nat(x)")] fun_cong 1);