--- a/src/HOL/Hyperreal/SEQ.ML Fri Mar 05 11:43:55 2004 +0100
+++ b/src/HOL/Hyperreal/SEQ.ML Fri Mar 05 15:18:59 2004 +0100
@@ -76,18 +76,18 @@
by (dres_inst_tac [("x","xa")] spec 1);
by (dres_inst_tac [("x","x")] spec 2);
by (Auto_tac);
-val lemma_NSLIMSEQ1 = result();
+qed "lemma_NSLIMSEQ1";
Goal "{n. f n <= Suc u} = {n. f n <= u} Un {n. f n = Suc u}";
by (auto_tac (claset(),simpset() addsimps [le_Suc_eq]));
-val lemma_NSLIMSEQ2 = result();
+qed "lemma_NSLIMSEQ2";
Goal "!!(f::nat=>nat). ALL n. n <= f n \
\ ==> {n. f n = Suc u} <= {n. n <= Suc u}";
by (Auto_tac);
by (dres_inst_tac [("x","x")] spec 1);
by (Auto_tac);
-val lemma_NSLIMSEQ3 = result();
+qed "lemma_NSLIMSEQ3";
Goal "!!(f::nat=>nat). ALL n. n <= f n \
\ ==> finite {n. f n <= u}";
@@ -127,7 +127,7 @@
Goal "{n. abs (X (f n) + - L) < r} Int {n. r <= abs (X (f n) + - (L::real))} \
\ = {}";
by Auto_tac;
-val lemmaLIM2 = result();
+qed "lemmaLIM2";
Goal "[| 0 < r; ALL n. r <= abs (X (f n) + - L); \
\ ( *fNat* X) (Abs_hypnat (hypnatrel `` {f})) + \
@@ -145,7 +145,7 @@
by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1);
by (asm_full_simp_tac (simpset() addsimps [lemmaLIM2,
FreeUltrafilterNat_empty]) 1);
-val lemmaLIM3 = result();
+qed "lemmaLIM3";
Goalw [LIMSEQ_def,NSLIMSEQ_def]
"X ----NS> L ==> X ----> L";
@@ -445,7 +445,7 @@
(* a few lemmas *)
Goal "ALL n. abs(X n) <= K ==> ALL n. abs(X((f::nat=>nat) n)) <= K";
by (Auto_tac);
-val lemma_Bseq = result();
+qed "lemma_Bseq";
Goalw [Bseq_def,NSBseq_def] "Bseq X ==> NSBseq X";
by (Step_tac 1);
@@ -477,14 +477,14 @@
by (Step_tac 1);
by (cut_inst_tac [("n","N")] real_of_nat_Suc_gt_zero 1);
by (Blast_tac 1);
-val lemmaNSBseq = result();
+qed "lemmaNSBseq";
Goal "ALL K. 0 < K --> (EX n. K < abs (X n)) \
\ ==> EX f. ALL N. real(Suc N) < abs (X (f N))";
by (dtac lemmaNSBseq 1);
by (dtac choice 1);
by (Blast_tac 1);
-val lemmaNSBseq2 = result();
+qed "lemmaNSBseq2";
Goal "ALL N. real(Suc N) < abs (X (f N)) \
\ ==> Abs_hypreal(hyprel``{X o f}) : HInfinite";
@@ -506,7 +506,7 @@
\ {n. f n <= u & real(Suc n) < abs (X (f n))} \
\ Un {n. real(Suc n) < abs (X (Suc u))}";
by (auto_tac (claset() addSDs [le_imp_less_or_eq], simpset()));
-val lemma_finite_NSBseq = result();
+qed "lemma_finite_NSBseq";
Goal "finite {n. f n <= (u::nat) & real(Suc n) < abs(X(f n))}";
by (induct_tac "u" 1);
@@ -515,7 +515,7 @@
by (rtac (lemma_finite_NSBseq RS finite_subset) 2);
by (auto_tac (claset() addIs [finite_real_of_nat_less_real],
simpset() addsimps [real_of_nat_Suc, less_diff_eq RS sym]));
-val lemma_finite_NSBseq2 = result();
+qed "lemma_finite_NSBseq2";
Goal "ALL N. real(Suc N) < abs (X (f N)) \
\ ==> Abs_hypnat(hypnatrel``{f}) : HNatInfinite";
@@ -619,7 +619,7 @@
by (Step_tac 1);
by (dres_inst_tac [("y","X n")] isLubD2 1);
by (ALLGOALS(blast_tac (claset() addDs [real_le_anti_sym])));
-val lemma_converg1 = result();
+qed "lemma_converg1";
(*-------------------------------------------------------------------
The best of both world: Easier to prove this result as a standard
@@ -651,13 +651,13 @@
by (dres_inst_tac [("y","X m")] isLubD2 1);
by (auto_tac (claset() addSDs [order_le_imp_less_or_eq],
simpset()));
-val lemma_converg2 = result();
+qed "lemma_converg2";
Goal "!!(X ::nat=>real). ALL m. X m <= U ==> \
\ isUb UNIV {x. EX n. X n = x} U";
by (rtac (setleI RS isUbI) 1);
by (Auto_tac);
-val lemma_converg3 = result();
+qed "lemma_converg3";
(* FIXME: U - T < U redundant *)
Goal "!!(X::nat=> real). \
@@ -673,7 +673,7 @@
by (dtac isLub_le_isUb 1 THEN assume_tac 1);
by (auto_tac (claset() addDs [order_less_le_trans],
simpset()));
-val lemma_converg4 = result();
+qed "lemma_converg4";
(*-------------------------------------------------------------------
A standard proof of the theorem for monotone increasing sequence
@@ -777,13 +777,13 @@
simpset() addsimps [HNatInfinite_FreeUltrafilterNat_iff]));
by (dres_inst_tac [("x","M")] spec 1);
by (ultra_tac (claset(), simpset() addsimps [less_imp_le]) 1);
-val lemmaCauchy1 = result();
+qed "lemmaCauchy1";
Goal "{n. ALL m n. M <= m & M <= (n::nat) --> abs (X m + - X n) < u} Int \
\ {n. M <= xa n} Int {n. M <= x n} <= \
\ {n. abs (X (xa n) + - X (x n)) < u}";
by (Blast_tac 1);
-val lemmaCauchy2 = result();
+qed "lemmaCauchy2";
Goalw [Cauchy_def,NSCauchy_def]
"Cauchy X ==> NSCauchy X";
@@ -858,7 +858,7 @@
by (Step_tac 1);
by (dtac spec 1 THEN Auto_tac);
by (arith_tac 1);
-val lemmaCauchy = result();
+qed "lemmaCauchy";
Goal "(n < Suc M) = (n <= M)";
by Auto_tac;
@@ -894,29 +894,29 @@
by (REPEAT(dres_inst_tac [("x","m")] spec 1));
by (auto_tac (claset() addEs [less_asym],
simpset() addsimps [le_def]));
-val lemma_Nat_covered = result();
+qed "lemma_Nat_covered";
Goal "[| ALL n. n <= M --> abs ((X::nat=>real) n) <= a; a < b |] \
\ ==> ALL n. n <= M --> abs(X n) <= b";
by (blast_tac (claset() addIs [order_le_less_trans RS order_less_imp_le]) 1);
-val lemma_trans1 = result();
+qed "lemma_trans1";
Goal "[| ALL n. M <= n --> abs ((X::nat=>real) n) < a; \
\ a < b |] \
\ ==> ALL n. M <= n --> abs(X n)<= b";
by (blast_tac (claset() addIs [order_less_trans RS order_less_imp_le]) 1);
-val lemma_trans2 = result();
+qed "lemma_trans2";
Goal "[| ALL n. n <= M --> abs (X n) <= a; \
\ a = b |] \
\ ==> ALL n. n <= M --> abs(X n) <= b";
by (Auto_tac);
-val lemma_trans3 = result();
+qed "lemma_trans3";
Goal "ALL n. M <= n --> abs ((X::nat=>real) n) < a \
\ ==> ALL n. M <= n --> abs (X n) <= a";
by (blast_tac (claset() addIs [order_less_imp_le]) 1);
-val lemma_trans4 = result();
+qed "lemma_trans4";
(*----------------------------------------------------------
Trickier than expected --- proof is more involved than