# HG changeset patch
# User paulson
# Date 1079343979 -3600
# Node ID 6be497cacab58a2af85c0a45f68ecc0bdc0a3799
# Parent  bbfa6b01a55f4e6002611a927fdf6c59b0562252
heavy tidying

diff -r bbfa6b01a55f -r 6be497cacab5 src/HOL/Hyperreal/HLog.thy
--- a/src/HOL/Hyperreal/HLog.thy	Mon Mar 15 10:46:01 2004 +0100
+++ b/src/HOL/Hyperreal/HLog.thy	Mon Mar 15 10:46:19 2004 +0100
@@ -32,22 +32,19 @@
 by (simp add: powhr_def starfun hypreal_mult powr_def)
 
 lemma powhr_one_eq_one [simp]: "1 powhr a = 1"
-apply (rule eq_Abs_hypreal [of a])
+apply (cases a)
 apply (simp add: powhr hypreal_one_num)
 done
 
 lemma powhr_mult:
      "[| 0 < x; 0 < y |] ==> (x * y) powhr a = (x powhr a) * (y powhr a)"
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of y])
-apply (rule eq_Abs_hypreal [of a])
+apply (cases x, cases y, cases a)
 apply (simp add: powhr hypreal_zero_num hypreal_mult hypreal_less, ultra)
 apply (simp add: powr_mult) 
 done
 
 lemma powhr_gt_zero [simp]: "0 < x powhr a"
-apply (rule eq_Abs_hypreal [of a])
-apply (rule eq_Abs_hypreal [of x])
+apply (cases a, cases x)
 apply (simp add: hypreal_zero_def powhr hypreal_less hypreal_zero_num)
 done
 
@@ -61,37 +58,28 @@
 
 lemma powhr_divide:
      "[| 0 < x; 0 < y |] ==> (x / y) powhr a = (x powhr a)/(y powhr a)"
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of y])
-apply (rule eq_Abs_hypreal [of a])
+apply (cases x, cases y, cases a)
 apply (simp add: powhr hypreal_divide hypreal_zero_num hypreal_less, ultra)
 apply (simp add: powr_divide)
 done
 
 lemma powhr_add: "x powhr (a + b) = (x powhr a) * (x powhr b)"
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of b])
-apply (rule eq_Abs_hypreal [of a])
+apply (cases x, cases b, cases a)
 apply (simp add: powhr hypreal_add hypreal_mult powr_add)
 done
 
 lemma powhr_powhr: "(x powhr a) powhr b = x powhr (a * b)"
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of b])
-apply (rule eq_Abs_hypreal [of a])
+apply (cases x, cases b, cases a)
 apply (simp add: powhr hypreal_mult powr_powr)
 done
 
 lemma powhr_powhr_swap: "(x powhr a) powhr b = (x powhr b) powhr a"
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of b])
-apply (rule eq_Abs_hypreal [of a])
+apply (cases x, cases b, cases a)
 apply (simp add: powhr powr_powr_swap)
 done
 
 lemma powhr_minus: "x powhr (-a) = inverse (x powhr a)"
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of a])
+apply (cases x, cases a)
 apply (simp add: powhr hypreal_minus hypreal_inverse hypreal_less powr_minus)
 done
 
@@ -99,16 +87,12 @@
 by (simp add: divide_inverse powhr_minus)
 
 lemma powhr_less_mono: "[| a < b; 1 < x |] ==> x powhr a < x powhr b"
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of a])
-apply (rule eq_Abs_hypreal [of b])
+apply (cases x, cases a, cases b)
 apply (simp add: powhr hypreal_one_num hypreal_less, ultra)
 done
 
 lemma powhr_less_cancel: "[| x powhr a < x powhr b; 1 < x |] ==> a < b"
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of a])
-apply (rule eq_Abs_hypreal [of b])
+apply (cases x, cases a, cases b)
 apply (simp add: powhr hypreal_one_num hypreal_less, ultra)
 done
 
@@ -128,21 +112,19 @@
 done
 
 lemma hlog_starfun_ln: "( *f* ln) x = hlog (( *f* exp) 1) x"
-apply (rule eq_Abs_hypreal [of x])
+apply (cases x)
 apply (simp add: starfun hlog log_ln hypreal_one_num)
 done
 
 lemma powhr_hlog_cancel [simp]:
      "[| 0 < a; a \<noteq> 1; 0 < x |] ==> a powhr (hlog a x) = x"
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of a])
+apply (cases x, cases a)
 apply (simp add: hlog powhr hypreal_zero_num hypreal_less hypreal_one_num, ultra)
 done
 
 lemma hlog_powhr_cancel [simp]:
      "[| 0 < a; a \<noteq> 1 |] ==> hlog a (a powhr y) = y"
-apply (rule eq_Abs_hypreal [of y])
-apply (rule eq_Abs_hypreal [of a])
+apply (cases y, cases a)
 apply (simp add: hlog powhr hypreal_zero_num hypreal_less hypreal_one_num, ultra)
 apply (auto intro: log_powr_cancel) 
 done
@@ -150,33 +132,27 @@
 lemma hlog_mult:
      "[| 0 < a; a \<noteq> 1; 0 < x; 0 < y  |]  
       ==> hlog a (x * y) = hlog a x + hlog a y"
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of y])
-apply (rule eq_Abs_hypreal [of a])
+apply (cases x, cases y, cases a)
 apply (simp add: hlog powhr hypreal_zero_num hypreal_one_num hypreal_less hypreal_add hypreal_mult, ultra)
 apply (simp add: log_mult)
 done
 
 lemma hlog_as_starfun:
      "[| 0 < a; a \<noteq> 1 |] ==> hlog a x = ( *f* ln) x / ( *f* ln) a"
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of a])
+apply (cases x, cases a)
 apply (simp add: hlog starfun hypreal_zero_num hypreal_one_num hypreal_divide log_def)
 done
 
 lemma hlog_eq_div_starfun_ln_mult_hlog:
      "[| 0 < a; a \<noteq> 1; 0 < b; b \<noteq> 1; 0 < x |]  
       ==> hlog a x = (( *f* ln) b/( *f*ln) a) * hlog b x"
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of a])
-apply (rule eq_Abs_hypreal [of b])
+apply (cases x, cases a, cases b)
 apply (simp add: hlog starfun hypreal_zero_num hypreal_one_num hypreal_less hypreal_divide hypreal_mult, ultra)
 apply (auto dest: log_eq_div_ln_mult_log) 
 done
 
 lemma powhr_as_starfun: "x powhr a = ( *f* exp) (a * ( *f* ln) x)"
-apply (rule eq_Abs_hypreal [of a])
-apply (rule eq_Abs_hypreal [of x])
+apply (cases a, cases x)
 apply (simp add: powhr starfun hypreal_mult powr_def)
 done
 
@@ -202,12 +178,12 @@
 by (rule hlog_as_starfun, auto)
 
 lemma hlog_one [simp]: "hlog a 1 = 0"
-apply (rule eq_Abs_hypreal [of a])
+apply (cases a)
 apply (simp add: hypreal_one_num hypreal_zero_num hlog)
 done
 
 lemma hlog_eq_one [simp]: "[| 0 < a; a \<noteq> 1 |] ==> hlog a a = 1"
-apply (rule eq_Abs_hypreal [of a])
+apply (cases a)
 apply (simp add: hypreal_one_num hypreal_zero_num hlog hypreal_less, ultra)
 apply (auto intro: log_eq_one) 
 done
@@ -224,9 +200,7 @@
 
 lemma hlog_less_cancel_iff [simp]:
      "[| 1 < a; 0 < x; 0 < y |] ==> (hlog a x < hlog a y) = (x < y)"
-apply (rule eq_Abs_hypreal [of a])
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of y])
+apply (cases a, cases x, cases y)
 apply (auto simp add: hlog hypreal_less hypreal_zero_num hypreal_one_num, ultra+)
 done
 
diff -r bbfa6b01a55f -r 6be497cacab5 src/HOL/Hyperreal/HSeries.thy
--- a/src/HOL/Hyperreal/HSeries.thy	Mon Mar 15 10:46:01 2004 +0100
+++ b/src/HOL/Hyperreal/HSeries.thy	Mon Mar 15 10:46:19 2004 +0100
@@ -36,7 +36,7 @@
 
 text{*Base case in definition of @{term sumr}*}
 lemma sumhr_zero [simp]: "sumhr (m,0,f) = 0"
-apply (rule eq_Abs_hypnat [of m])
+apply (cases m)
 apply (simp add: hypnat_zero_def sumhr symmetric hypreal_zero_def)
 done
 
@@ -44,48 +44,43 @@
 lemma sumhr_if: 
      "sumhr(m,n+1,f) = 
       (if n + 1 \<le> m then 0 else sumhr(m,n,f) + ( *fNat* f) n)"
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases m, cases n)
 apply (auto simp add: hypnat_one_def sumhr hypnat_add hypnat_le starfunNat
            hypreal_add hypreal_zero_def,   ultra+)
 done
 
 lemma sumhr_Suc_zero [simp]: "sumhr (n + 1, n, f) = 0"
-apply (rule eq_Abs_hypnat [of n])
+apply (cases n)
 apply (simp add: hypnat_one_def sumhr hypnat_add hypreal_zero_def)
 done
 
 lemma sumhr_eq_bounds [simp]: "sumhr (n,n,f) = 0"
-apply (rule eq_Abs_hypnat [of n])
+apply (cases n)
 apply (simp add: sumhr hypreal_zero_def)
 done
 
 lemma sumhr_Suc [simp]: "sumhr (m,m + 1,f) = ( *fNat* f) m"
-apply (rule eq_Abs_hypnat [of m])
+apply (cases m)
 apply (simp add: sumhr hypnat_one_def  hypnat_add starfunNat)
 done
 
 lemma sumhr_add_lbound_zero [simp]: "sumhr(m+k,k,f) = 0"
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypnat [of k])
+apply (cases m, cases k)
 apply (simp add: sumhr hypnat_add hypreal_zero_def)
 done
 
 lemma sumhr_add: "sumhr (m,n,f) + sumhr(m,n,g) = sumhr(m,n,%i. f i + g i)"
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases m, cases n)
 apply (simp add: sumhr hypreal_add sumr_add)
 done
 
 lemma sumhr_mult: "hypreal_of_real r * sumhr(m,n,f) = sumhr(m,n,%n. r * f n)"
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases m, cases n)
 apply (simp add: sumhr hypreal_of_real_def hypreal_mult sumr_mult)
 done
 
 lemma sumhr_split_add: "n < p ==> sumhr(0,n,f) + sumhr(n,p,f) = sumhr(0,p,f)"
-apply (rule eq_Abs_hypnat [of n])
-apply (rule eq_Abs_hypnat [of p])
+apply (cases n, cases p)
 apply (auto elim!: FreeUltrafilterNat_subset simp 
             add: hypnat_zero_def sumhr hypreal_add hypnat_less sumr_split_add)
 done
@@ -94,8 +89,7 @@
 by (drule_tac f1 = f in sumhr_split_add [symmetric], simp)
 
 lemma sumhr_hrabs: "abs(sumhr(m,n,f)) \<le> sumhr(m,n,%i. abs(f i))"
-apply (rule eq_Abs_hypnat [of n])
-apply (rule eq_Abs_hypnat [of m])
+apply (cases n, cases m)
 apply (simp add: sumhr hypreal_le hypreal_hrabs sumr_rabs)
 done
 
@@ -109,35 +103,32 @@
 done
 
 lemma sumhr_const: "sumhr(0,n,%i. r) = hypreal_of_hypnat n*hypreal_of_real r"
-apply (rule eq_Abs_hypnat [of n])
+apply (cases n)
 apply (simp add: sumhr hypnat_zero_def hypreal_of_real_def hypreal_of_hypnat hypreal_mult)
 done
 
 lemma sumhr_add_mult_const: 
      "sumhr(0,n,f) + -(hypreal_of_hypnat n*hypreal_of_real r) =  
       sumhr(0,n,%i. f i + -r)"
-apply (rule eq_Abs_hypnat [of n])
+apply (cases n)
 apply (simp add: sumhr hypnat_zero_def hypreal_of_real_def hypreal_of_hypnat 
                  hypreal_mult hypreal_add hypreal_minus sumr_add [symmetric])
 done
 
 lemma sumhr_less_bounds_zero [simp]: "n < m ==> sumhr(m,n,f) = 0"
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases m, cases n)
 apply (auto elim: FreeUltrafilterNat_subset 
             simp add: sumhr hypnat_less hypreal_zero_def)
 done
 
 lemma sumhr_minus: "sumhr(m, n, %i. - f i) = - sumhr(m, n, f)"
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases m, cases n)
 apply (simp add: sumhr hypreal_minus sumr_minus)
 done
 
 lemma sumhr_shift_bounds:
      "sumhr(m+hypnat_of_nat k,n+hypnat_of_nat k,f) = sumhr(m,n,%i. f(i + k))"
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases m, cases n)
 apply (simp add: sumhr hypnat_add sumr_shift_bounds hypnat_of_nat_eq)
 done
 
@@ -169,7 +160,7 @@
                    hypnat_of_nat_eq hypreal_of_real_def hypreal_mult)
 
 lemma starfunNat_sumr: "( *fNat* (%n. sumr 0 n f)) N = sumhr(0,N,f)"
-apply (rule eq_Abs_hypnat [of N])
+apply (cases N)
 apply (simp add: hypnat_zero_def starfunNat sumhr)
 done
 
diff -r bbfa6b01a55f -r 6be497cacab5 src/HOL/Hyperreal/HTranscendental.thy
--- a/src/HOL/Hyperreal/HTranscendental.thy	Mon Mar 15 10:46:01 2004 +0100
+++ b/src/HOL/Hyperreal/HTranscendental.thy	Mon Mar 15 10:46:19 2004 +0100
@@ -33,14 +33,14 @@
 by (simp add: starfun hypreal_one_num)
 
 lemma hypreal_sqrt_pow2_iff: "(( *f* sqrt)(x) ^ 2 = x) = (0 \<le> x)"
-apply (rule eq_Abs_hypreal [of x])
+apply (cases x)
 apply (auto simp add: hypreal_le hypreal_zero_num starfun hrealpow 
                       real_sqrt_pow2_iff 
             simp del: hpowr_Suc realpow_Suc)
 done
 
 lemma hypreal_sqrt_gt_zero_pow2: "0 < x ==> ( *f* sqrt) (x) ^ 2 = x"
-apply (rule eq_Abs_hypreal [of x])
+apply (cases x)
 apply (auto intro: FreeUltrafilterNat_subset real_sqrt_gt_zero_pow2
             simp add: hypreal_less starfun hrealpow hypreal_zero_num 
             simp del: hpowr_Suc realpow_Suc)
@@ -62,8 +62,7 @@
 
 lemma hypreal_sqrt_mult_distrib: 
     "[|0 < x; 0 <y |] ==> ( *f* sqrt)(x*y) =  ( *f* sqrt)(x) * ( *f* sqrt)(y)"
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of y])
+apply (cases x, cases y)
 apply (simp add: hypreal_zero_def starfun hypreal_mult hypreal_less hypreal_zero_num, ultra)
 apply (auto intro: real_sqrt_mult_distrib) 
 done
@@ -101,7 +100,7 @@
 done
 
 lemma hypreal_sqrt_gt_zero: "0 < x ==> 0 < ( *f* sqrt)(x)"
-apply (rule eq_Abs_hypreal [of x])
+apply (cases x)
 apply (auto simp add: starfun hypreal_zero_def hypreal_less hypreal_zero_num, ultra)
 apply (auto intro: real_sqrt_gt_zero)
 done
@@ -110,7 +109,7 @@
 by (auto intro: hypreal_sqrt_gt_zero simp add: order_le_less)
 
 lemma hypreal_sqrt_hrabs [simp]: "( *f* sqrt)(x ^ 2) = abs(x)"
-apply (rule eq_Abs_hypreal [of x])
+apply (cases x)
 apply (simp add: starfun hypreal_hrabs hypreal_mult numeral_2_eq_2)
 done
 
@@ -122,7 +121,7 @@
 
 lemma hypreal_sqrt_hyperpow_hrabs [simp]:
      "( *f* sqrt)(x pow (hypnat_of_nat 2)) = abs(x)"
-apply (rule eq_Abs_hypreal [of x])
+apply (cases x)
 apply (simp add: starfun hypreal_hrabs hypnat_of_nat_eq hyperpow)
 done
 
@@ -142,8 +141,7 @@
 done
 
 lemma hypreal_sqrt_sum_squares_ge1 [simp]: "x \<le> ( *f* sqrt)(x ^ 2 + y ^ 2)"
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of y])
+apply (cases x, cases y)
 apply (simp add: starfun hypreal_add hrealpow hypreal_le 
             del: hpowr_Suc realpow_Suc)
 done
@@ -274,8 +272,7 @@
 by (auto intro: STAR_exp_Infinitesimal)
 
 lemma STAR_exp_add: "( *f* exp)(x + y) = ( *f* exp) x * ( *f* exp) y"
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of y])
+apply (cases x, cases y)
 apply (simp add: starfun hypreal_add hypreal_mult exp_add)
 done
 
@@ -293,7 +290,7 @@
 done
 
 lemma starfun_exp_ge_add_one_self [simp]: "0 \<le> x ==> (1 + x) \<le> ( *f* exp) x"
-apply (rule eq_Abs_hypreal [of x])
+apply (cases x)
 apply (simp add: starfun hypreal_add hypreal_le hypreal_zero_num hypreal_one_num, ultra)
 done
 
@@ -306,7 +303,7 @@
 done
 
 lemma starfun_exp_minus: "( *f* exp) (-x) = inverse(( *f* exp) x)"
-apply (rule eq_Abs_hypreal [of x])
+apply (cases x)
 apply (simp add: starfun hypreal_inverse hypreal_minus exp_minus)
 done
 
@@ -320,7 +317,7 @@
 done
 
 lemma starfun_exp_gt_one [simp]: "0 < x ==> 1 < ( *f* exp) x"
-apply (rule eq_Abs_hypreal [of x])
+apply (cases x)
 apply (simp add: starfun hypreal_one_num hypreal_zero_num hypreal_less, ultra)
 done
 
@@ -338,12 +335,12 @@
 
 
 lemma starfun_ln_exp [simp]: "( *f* ln) (( *f* exp) x) = x"
-apply (rule eq_Abs_hypreal [of x])
+apply (cases x)
 apply (simp add: starfun)
 done
 
 lemma starfun_exp_ln_iff [simp]: "(( *f* exp)(( *f* ln) x) = x) = (0 < x)"
-apply (rule eq_Abs_hypreal [of x])
+apply (cases x)
 apply (simp add: starfun hypreal_zero_num hypreal_less)
 done
 
@@ -351,22 +348,22 @@
 by (auto simp add: starfun)
 
 lemma starfun_ln_less_self [simp]: "0 < x ==> ( *f* ln) x < x"
-apply (rule eq_Abs_hypreal [of x])
+apply (cases x)
 apply (simp add: starfun hypreal_zero_num hypreal_less, ultra)
 done
 
 lemma starfun_ln_ge_zero [simp]: "1 \<le> x ==> 0 \<le> ( *f* ln) x"
-apply (rule eq_Abs_hypreal [of x])
+apply (cases x)
 apply (simp add: starfun hypreal_zero_num hypreal_le hypreal_one_num, ultra)
 done
 
 lemma starfun_ln_gt_zero [simp]: "1 < x ==> 0 < ( *f* ln) x"
-apply (rule eq_Abs_hypreal [of x])
+apply (cases x)
 apply (simp add: starfun hypreal_zero_num hypreal_less hypreal_one_num, ultra)
 done
 
 lemma starfun_ln_not_eq_zero [simp]: "[| 0 < x; x \<noteq> 1 |] ==> ( *f* ln) x \<noteq> 0"
-apply (rule eq_Abs_hypreal [of x])
+apply (cases x)
 apply (auto simp add: starfun hypreal_zero_num hypreal_less hypreal_one_num, ultra)
 apply (auto dest: ln_not_eq_zero) 
 done
@@ -379,13 +376,13 @@
 done
 
 lemma starfun_ln_inverse: "0 < x ==> ( *f* ln) (inverse x) = -( *f* ln) x"
-apply (rule eq_Abs_hypreal [of x])
+apply (cases x)
 apply (simp add: starfun hypreal_zero_num hypreal_minus hypreal_inverse hypreal_less, ultra)
 apply (simp add: ln_inverse)
 done
 
 lemma starfun_exp_HFinite: "x \<in> HFinite ==> ( *f* exp) x \<in> HFinite"
-apply (rule eq_Abs_hypreal [of x])
+apply (cases x)
 apply (auto simp add: starfun HFinite_FreeUltrafilterNat_iff)
 apply (rule bexI, rule_tac [2] lemma_hyprel_refl, auto)
 apply (rule_tac x = "exp u" in exI)
@@ -433,7 +430,7 @@
 done
 
 lemma starfun_ln_less_zero: "[| 0 < x; x < 1 |] ==> ( *f* ln) x < 0"
-apply (rule eq_Abs_hypreal [of x])
+apply (cases x)
 apply (simp add: hypreal_zero_num hypreal_one_num hypreal_less starfun, ultra)
 apply (auto intro: ln_less_zero) 
 done
diff -r bbfa6b01a55f -r 6be497cacab5 src/HOL/Hyperreal/HyperDef.thy
--- a/src/HOL/Hyperreal/HyperDef.thy	Mon Mar 15 10:46:01 2004 +0100
+++ b/src/HOL/Hyperreal/HyperDef.thy	Mon Mar 15 10:46:19 2004 +0100
@@ -2,9 +2,11 @@
     ID          : $Id$
     Author      : Jacques D. Fleuriot
     Copyright   : 1998  University of Cambridge
-    Description : Construction of hyperreals using ultrafilters
+    Conversion to Isar and new proofs by Lawrence C Paulson, 2004
 *)
 
+header{*Construction of Hyperreals Using Ultrafilters*}
+
 theory HyperDef = Filter + Real
 files ("fuf.ML"):  (*Warning: file fuf.ML refers to the name Hyperdef!*)
 
@@ -233,19 +235,17 @@
 text{*Proving that @{term hyprel} is an equivalence relation*}
 
 lemma hyprel_iff: "((X,Y) \<in> hyprel) = ({n. X n = Y n}: FreeUltrafilterNat)"
-by (unfold hyprel_def, fast)
+by (simp add: hyprel_def)
 
 lemma hyprel_refl: "(x,x) \<in> hyprel"
-apply (unfold hyprel_def)
-apply (auto simp add: FreeUltrafilterNat_Nat_set)
-done
+by (simp add: hyprel_def)
 
 lemma hyprel_sym [rule_format (no_asm)]: "(x,y) \<in> hyprel --> (y,x) \<in> hyprel"
 by (simp add: hyprel_def eq_commute)
 
 lemma hyprel_trans: 
       "[|(x,y) \<in> hyprel; (y,z) \<in> hyprel|] ==> (x,z) \<in> hyprel"
-by (unfold hyprel_def, auto, ultra)
+by (simp add: hyprel_def, ultra)
 
 lemma equiv_hyprel: "equiv UNIV hyprel"
 apply (simp add: equiv_def refl_def sym_def trans_def hyprel_refl)
@@ -257,7 +257,7 @@
     eq_equiv_class_iff [OF equiv_hyprel UNIV_I UNIV_I, simp] 
 
 lemma hyprel_in_hypreal [simp]: "hyprel``{x}:hypreal"
-by (unfold hypreal_def hyprel_def quotient_def, blast)
+by (simp add: hypreal_def hyprel_def quotient_def, blast)
 
 lemma inj_on_Abs_hypreal: "inj_on Abs_hypreal hypreal"
 apply (rule inj_on_inverseI)
@@ -279,12 +279,10 @@
 done
 
 lemma lemma_hyprel_refl [simp]: "x \<in> hyprel `` {x}"
-apply (unfold hyprel_def, safe)
-apply (auto intro!: FreeUltrafilterNat_Nat_set)
-done
+by (simp add: hyprel_def)
 
 lemma hypreal_empty_not_mem [simp]: "{} \<notin> hypreal"
-apply (unfold hypreal_def)
+apply (simp add: hypreal_def)
 apply (auto elim!: quotientE equalityCE)
 done
 
@@ -297,53 +295,47 @@
 
 lemma inj_hypreal_of_real: "inj(hypreal_of_real)"
 apply (rule inj_onI)
-apply (unfold hypreal_of_real_def)
-apply (drule inj_on_Abs_hypreal [THEN inj_onD])
-apply (rule hyprel_in_hypreal)+
-apply (drule eq_equiv_class)
-apply (rule equiv_hyprel)
-apply (simp_all add: split: split_if_asm) 
+apply (simp add: hypreal_of_real_def split: split_if_asm)
 done
 
 lemma eq_Abs_hypreal:
-    "(!!x y. z = Abs_hypreal(hyprel``{x}) ==> P) ==> P"
+    "(!!x. z = Abs_hypreal(hyprel``{x}) ==> P) ==> P"
 apply (rule_tac x1=z in Rep_hypreal [unfolded hypreal_def, THEN quotientE])
 apply (drule_tac f = Abs_hypreal in arg_cong)
 apply (force simp add: Rep_hypreal_inverse)
 done
 
+theorem hypreal_cases [case_names Abs_hypreal, cases type: hypreal]:
+    "(!!x. z = Abs_hypreal(hyprel``{x}) ==> P) ==> P"
+by (rule eq_Abs_hypreal [of z], blast)
+
 
 subsection{*Hyperreal Addition*}
 
 lemma hypreal_add_congruent2: 
     "congruent2 hyprel (%X Y. hyprel``{%n. X n + Y n})"
-apply (unfold congruent2_def, auto, ultra)
+apply (simp add: congruent2_def, auto, ultra)
 done
 
 lemma hypreal_add: 
   "Abs_hypreal(hyprel``{%n. X n}) + Abs_hypreal(hyprel``{%n. Y n}) =  
    Abs_hypreal(hyprel``{%n. X n + Y n})"
-apply (unfold hypreal_add_def)
+apply (simp add: hypreal_add_def)
 apply (simp add: UN_equiv_class2 [OF equiv_hyprel hypreal_add_congruent2])
 done
 
 lemma hypreal_add_commute: "(z::hypreal) + w = w + z"
-apply (rule eq_Abs_hypreal [of z])
-apply (rule eq_Abs_hypreal [of w])
+apply (cases z, cases w)
 apply (simp add: add_ac hypreal_add)
 done
 
 lemma hypreal_add_assoc: "((z1::hypreal) + z2) + z3 = z1 + (z2 + z3)"
-apply (rule eq_Abs_hypreal [of z1])
-apply (rule eq_Abs_hypreal [of z2])
-apply (rule eq_Abs_hypreal [of z3])
+apply (cases z1, cases z2, cases z3)
 apply (simp add: hypreal_add real_add_assoc)
 done
 
 lemma hypreal_add_zero_left: "(0::hypreal) + z = z"
-apply (rule eq_Abs_hypreal [of z])
-apply (simp add: hypreal_zero_def hypreal_add)
-done
+by (cases z, simp add: hypreal_zero_def hypreal_add)
 
 instance hypreal :: plus_ac0
   by (intro_classes,
@@ -362,7 +354,7 @@
 
 lemma hypreal_minus: 
    "- (Abs_hypreal(hyprel``{%n. X n})) = Abs_hypreal(hyprel `` {%n. -(X n)})"
-apply (unfold hypreal_minus_def)
+apply (simp add: hypreal_minus_def)
 apply (rule_tac f = Abs_hypreal in arg_cong)
 apply (simp add: hyprel_in_hypreal [THEN Abs_hypreal_inverse] 
                UN_equiv_class [OF equiv_hyprel hypreal_minus_congruent])
@@ -375,7 +367,7 @@
 done
 
 lemma hypreal_add_minus [simp]: "z + -z = (0::hypreal)"
-apply (unfold hypreal_zero_def)
+apply (simp add: hypreal_zero_def)
 apply (rule_tac z = z in eq_Abs_hypreal)
 apply (simp add: hypreal_minus hypreal_add)
 done
@@ -388,62 +380,55 @@
 
 lemma hypreal_mult_congruent2: 
     "congruent2 hyprel (%X Y. hyprel``{%n. X n * Y n})"
-apply (unfold congruent2_def, auto, ultra)
+apply (simp add: congruent2_def, auto, ultra)
 done
 
 lemma hypreal_mult: 
   "Abs_hypreal(hyprel``{%n. X n}) * Abs_hypreal(hyprel``{%n. Y n}) =  
    Abs_hypreal(hyprel``{%n. X n * Y n})"
-apply (unfold hypreal_mult_def)
+apply (simp add: hypreal_mult_def)
 apply (simp add: UN_equiv_class2 [OF equiv_hyprel hypreal_mult_congruent2])
 done
 
 lemma hypreal_mult_commute: "(z::hypreal) * w = w * z"
-apply (rule eq_Abs_hypreal [of z])
-apply (rule eq_Abs_hypreal [of w])
+apply (cases z, cases w)
 apply (simp add: hypreal_mult mult_ac)
 done
 
 lemma hypreal_mult_assoc: "((z1::hypreal) * z2) * z3 = z1 * (z2 * z3)"
-apply (rule eq_Abs_hypreal [of z1])
-apply (rule eq_Abs_hypreal [of z2])
-apply (rule eq_Abs_hypreal [of z3])
+apply (cases z1, cases z2, cases z3)
 apply (simp add: hypreal_mult mult_assoc)
 done
 
 lemma hypreal_mult_1: "(1::hypreal) * z = z"
-apply (unfold hypreal_one_def)
+apply (simp add: hypreal_one_def)
 apply (rule_tac z = z in eq_Abs_hypreal)
 apply (simp add: hypreal_mult)
 done
 
 lemma hypreal_add_mult_distrib:
      "((z1::hypreal) + z2) * w = (z1 * w) + (z2 * w)"
-apply (rule eq_Abs_hypreal [of z1])
-apply (rule eq_Abs_hypreal [of z2])
-apply (rule eq_Abs_hypreal [of w])
+apply (cases z1, cases z2, cases w)
 apply (simp add: hypreal_mult hypreal_add left_distrib)
 done
 
 text{*one and zero are distinct*}
 lemma hypreal_zero_not_eq_one: "0 \<noteq> (1::hypreal)"
-apply (unfold hypreal_zero_def hypreal_one_def)
-apply (auto simp add: real_zero_not_eq_one)
-done
+by (simp add: hypreal_zero_def hypreal_one_def)
 
 
 subsection{*Multiplicative Inverse on @{typ hypreal} *}
 
 lemma hypreal_inverse_congruent: 
   "congruent hyprel (%X. hyprel``{%n. if X n = 0 then 0 else inverse(X n)})"
-apply (unfold congruent_def)
+apply (simp add: congruent_def)
 apply (auto, ultra)
 done
 
 lemma hypreal_inverse: 
       "inverse (Abs_hypreal(hyprel``{%n. X n})) =  
        Abs_hypreal(hyprel `` {%n. if X n = 0 then 0 else inverse(X n)})"
-apply (unfold hypreal_inverse_def)
+apply (simp add: hypreal_inverse_def)
 apply (rule_tac f = Abs_hypreal in arg_cong)
 apply (simp add: hyprel_in_hypreal [THEN Abs_hypreal_inverse] 
            UN_equiv_class [OF equiv_hyprel hypreal_inverse_congruent])
@@ -451,8 +436,8 @@
 
 lemma hypreal_mult_inverse: 
      "x \<noteq> 0 ==> x*inverse(x) = (1::hypreal)"
-apply (unfold hypreal_one_def hypreal_zero_def)
-apply (rule eq_Abs_hypreal [of x])
+apply (simp add: hypreal_one_def hypreal_zero_def)
+apply (cases x)
 apply (simp add: hypreal_inverse hypreal_mult)
 apply (drule FreeUltrafilterNat_Compl_mem)
 apply (blast intro!: right_inverse FreeUltrafilterNat_subset)
@@ -492,25 +477,22 @@
 lemma hypreal_le: 
       "(Abs_hypreal(hyprel``{%n. X n}) \<le> Abs_hypreal(hyprel``{%n. Y n})) =  
        ({n. X n \<le> Y n} \<in> FreeUltrafilterNat)"
-apply (unfold hypreal_le_def)
+apply (simp add: hypreal_le_def)
 apply (auto intro!: lemma_hyprel_refl, ultra)
 done
 
 lemma hypreal_le_refl: "w \<le> (w::hypreal)"
-apply (rule eq_Abs_hypreal [of w])
+apply (cases w)
 apply (simp add: hypreal_le) 
 done
 
 lemma hypreal_le_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::hypreal)"
-apply (rule eq_Abs_hypreal [of i])
-apply (rule eq_Abs_hypreal [of j])
-apply (rule eq_Abs_hypreal [of k])
+apply (cases i, cases j, cases k)
 apply (simp add: hypreal_le, ultra)
 done
 
 lemma hypreal_le_anti_sym: "[| z \<le> w; w \<le> z |] ==> z = (w::hypreal)"
-apply (rule eq_Abs_hypreal [of z])
-apply (rule eq_Abs_hypreal [of w])
+apply (cases z, cases w)
 apply (simp add: hypreal_le, ultra)
 done
 
@@ -526,8 +508,7 @@
 
 (* Axiom 'linorder_linear' of class 'linorder': *)
 lemma hypreal_le_linear: "(z::hypreal) \<le> w | w \<le> z"
-apply (rule eq_Abs_hypreal [of z])
-apply (rule eq_Abs_hypreal [of w])
+apply (cases z, cases w)
 apply (auto simp add: hypreal_le, ultra)
 done
 
@@ -538,16 +519,12 @@
 by (auto simp add: order_less_irrefl)
 
 lemma hypreal_add_left_mono: "x \<le> y ==> z + x \<le> z + (y::hypreal)"
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of y])
-apply (rule eq_Abs_hypreal [of z])
+apply (cases x, cases y, cases z)
 apply (auto simp add: hypreal_le hypreal_add) 
 done
 
 lemma hypreal_mult_less_mono2: "[| (0::hypreal)<z; x<y |] ==> z*x<z*y"
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of y])
-apply (rule eq_Abs_hypreal [of z])
+apply (cases x, cases y, cases z)
 apply (auto simp add: hypreal_zero_def hypreal_le hypreal_mult 
                       linorder_not_le [symmetric], ultra) 
 done
@@ -630,25 +607,25 @@
 
 lemma hypreal_of_real_add [simp]: 
      "hypreal_of_real (w + z) = hypreal_of_real w + hypreal_of_real z"
-apply (unfold hypreal_of_real_def)
+apply (simp add: hypreal_of_real_def)
 apply (simp add: hypreal_add left_distrib)
 done
 
 lemma hypreal_of_real_mult [simp]: 
      "hypreal_of_real (w * z) = hypreal_of_real w * hypreal_of_real z"
-apply (unfold hypreal_of_real_def)
+apply (simp add: hypreal_of_real_def)
 apply (simp add: hypreal_mult right_distrib)
 done
 
 lemma hypreal_of_real_one [simp]: "hypreal_of_real 1 = (1::hypreal)"
-by (unfold hypreal_of_real_def hypreal_one_def, simp)
+by (simp add: hypreal_of_real_def hypreal_one_def)
 
 lemma hypreal_of_real_zero [simp]: "hypreal_of_real 0 = 0"
-by (unfold hypreal_of_real_def hypreal_zero_def, simp)
+by (simp add: hypreal_of_real_def hypreal_zero_def)
 
 lemma hypreal_of_real_le_iff [simp]: 
      "(hypreal_of_real w \<le> hypreal_of_real z) = (w \<le> z)"
-apply (unfold hypreal_le_def hypreal_of_real_def, auto)
+apply (simp add: hypreal_le_def hypreal_of_real_def, auto)
 apply (rule_tac [2] x = "%n. w" in exI, safe)
 apply (rule_tac [3] x = "%n. z" in exI, auto)
 apply (rule FreeUltrafilterNat_P, ultra)
@@ -713,7 +690,7 @@
 by (simp add: hypreal_one_def [THEN meta_eq_to_obj_eq, symmetric])
 
 lemma hypreal_omega_gt_zero [simp]: "0 < omega"
-apply (unfold omega_def)
+apply (simp add: omega_def)
 apply (auto simp add: hypreal_less hypreal_zero_num)
 done
 
@@ -738,9 +715,7 @@
 subsection{*Existence of Infinite Hyperreal Number*}
 
 lemma Rep_hypreal_omega: "Rep_hypreal(omega) \<in> hypreal"
-apply (unfold omega_def)
-apply (rule Rep_hypreal)
-done
+by (simp add: omega_def)
 
 text{*Existence of infinite number not corresponding to any real number.
 Use assumption that member @{term FreeUltrafilterNat} is not finite.*}
@@ -757,7 +732,7 @@
 
 lemma not_ex_hypreal_of_real_eq_omega: 
       "~ (\<exists>x. hypreal_of_real x = omega)"
-apply (unfold omega_def hypreal_of_real_def)
+apply (simp add: omega_def hypreal_of_real_def)
 apply (auto simp add: real_of_nat_Suc diff_eq_eq [symmetric] 
             lemma_finite_omega_set [THEN FreeUltrafilterNat_finite])
 done
@@ -778,7 +753,7 @@
 
 lemma not_ex_hypreal_of_real_eq_epsilon: 
       "~ (\<exists>x. hypreal_of_real x = epsilon)"
-apply (unfold epsilon_def hypreal_of_real_def)
+apply (simp add: epsilon_def hypreal_of_real_def)
 apply (auto simp add: lemma_finite_epsilon_set [THEN FreeUltrafilterNat_finite])
 done
 
@@ -786,7 +761,7 @@
 by (cut_tac not_ex_hypreal_of_real_eq_epsilon, auto)
 
 lemma hypreal_epsilon_not_zero: "epsilon \<noteq> 0"
-by (unfold epsilon_def hypreal_zero_def, auto)
+by (simp add: epsilon_def hypreal_zero_def)
 
 lemma hypreal_epsilon_inverse_omega: "epsilon = inverse(omega)"
 by (simp add: hypreal_inverse omega_def epsilon_def)
diff -r bbfa6b01a55f -r 6be497cacab5 src/HOL/Hyperreal/HyperNat.thy
--- a/src/HOL/Hyperreal/HyperNat.thy	Mon Mar 15 10:46:01 2004 +0100
+++ b/src/HOL/Hyperreal/HyperNat.thy	Mon Mar 15 10:46:19 2004 +0100
@@ -63,19 +63,18 @@
 
 lemma hypnatrel_iff:
      "((X,Y) \<in> hypnatrel) = ({n. X n = Y n}: FreeUltrafilterNat)"
-apply (unfold hypnatrel_def, fast)
+apply (simp add: hypnatrel_def)
 done
 
 lemma hypnatrel_refl: "(x,x) \<in> hypnatrel"
-by (unfold hypnatrel_def, auto)
+by (simp add: hypnatrel_def)
 
 lemma hypnatrel_sym: "(x,y) \<in> hypnatrel ==> (y,x) \<in> hypnatrel"
 by (auto simp add: hypnatrel_def eq_commute)
 
 lemma hypnatrel_trans [rule_format (no_asm)]:
      "(x,y) \<in> hypnatrel --> (y,z) \<in> hypnatrel --> (x,z) \<in> hypnatrel"
-apply (unfold hypnatrel_def, auto, ultra)
-done
+by (auto simp add: hypnatrel_def, ultra)
 
 lemma equiv_hypnatrel:
      "equiv UNIV hypnatrel"
@@ -88,7 +87,7 @@
     eq_equiv_class_iff [OF equiv_hypnatrel UNIV_I UNIV_I, simp]
 
 lemma hypnatrel_in_hypnat [simp]: "hypnatrel``{x}:hypnat"
-by (unfold hypnat_def hypnatrel_def quotient_def, blast)
+by (simp add: hypnat_def hypnatrel_def quotient_def, blast)
 
 lemma inj_on_Abs_hypnat: "inj_on Abs_hypnat hypnat"
 apply (rule inj_on_inverseI)
@@ -114,7 +113,7 @@
 declare lemma_hypnatrel_refl [simp]
 
 lemma hypnat_empty_not_mem: "{} \<notin> hypnat"
-apply (unfold hypnat_def)
+apply (simp add: hypnat_def)
 apply (auto elim!: quotientE equalityCE)
 done
 
@@ -133,11 +132,15 @@
 apply (force simp add: Rep_hypnat_inverse)
 done
 
+theorem hypnat_cases [case_names Abs_hypnat, cases type: hypnat]:
+    "(!!x. z = Abs_hypnat(hypnatrel``{x}) ==> P) ==> P"
+by (rule eq_Abs_hypnat [of z], blast)
+
 subsection{*Hypernat Addition*}
 
 lemma hypnat_add_congruent2:
      "congruent2 hypnatrel (%X Y. hypnatrel``{%n. X n + Y n})"
-apply (unfold congruent2_def, auto, ultra)
+apply (simp add: congruent2_def, auto, ultra)
 done
 
 lemma hypnat_add:
@@ -146,20 +149,17 @@
 by (simp add: hypnat_add_def UN_equiv_class2 [OF equiv_hypnatrel hypnat_add_congruent2])
 
 lemma hypnat_add_commute: "(z::hypnat) + w = w + z"
-apply (rule eq_Abs_hypnat [of z])
-apply (rule eq_Abs_hypnat [of w])
+apply (cases z, cases w)
 apply (simp add: add_ac hypnat_add)
 done
 
 lemma hypnat_add_assoc: "((z1::hypnat) + z2) + z3 = z1 + (z2 + z3)"
-apply (rule eq_Abs_hypnat [of z1])
-apply (rule eq_Abs_hypnat [of z2])
-apply (rule eq_Abs_hypnat [of z3])
+apply (cases z1, cases z2, cases z3)
 apply (simp add: hypnat_add nat_add_assoc)
 done
 
 lemma hypnat_add_zero_left: "(0::hypnat) + z = z"
-apply (rule eq_Abs_hypnat [of z])
+apply (cases z)
 apply (simp add: hypnat_zero_def hypnat_add)
 done
 
@@ -174,7 +174,7 @@
 
 lemma hypnat_minus_congruent2:
     "congruent2 hypnatrel (%X Y. hypnatrel``{%n. X n - Y n})"
-apply (unfold congruent2_def, auto, ultra)
+apply (simp add: congruent2_def, auto, ultra)
 done
 
 lemma hypnat_minus:
@@ -183,29 +183,26 @@
 by (simp add: hypnat_minus_def UN_equiv_class2 [OF equiv_hypnatrel hypnat_minus_congruent2])
 
 lemma hypnat_minus_zero: "z - z = (0::hypnat)"
-apply (rule eq_Abs_hypnat [of z])
+apply (cases z)
 apply (simp add: hypnat_zero_def hypnat_minus)
 done
 
 lemma hypnat_diff_0_eq_0: "(0::hypnat) - n = 0"
-apply (rule eq_Abs_hypnat [of n])
+apply (cases n)
 apply (simp add: hypnat_minus hypnat_zero_def)
 done
 
 declare hypnat_minus_zero [simp] hypnat_diff_0_eq_0 [simp]
 
 lemma hypnat_add_is_0: "(m+n = (0::hypnat)) = (m=0 & n=0)"
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases m, cases n)
 apply (auto intro: FreeUltrafilterNat_subset dest: FreeUltrafilterNat_Int simp add: hypnat_zero_def hypnat_add)
 done
 
 declare hypnat_add_is_0 [iff]
 
 lemma hypnat_diff_diff_left: "(i::hypnat) - j - k = i - (j+k)"
-apply (rule eq_Abs_hypnat [of i])
-apply (rule eq_Abs_hypnat [of j])
-apply (rule eq_Abs_hypnat [of k])
+apply (cases i, cases j, cases k)
 apply (simp add: hypnat_minus hypnat_add diff_diff_left)
 done
 
@@ -213,23 +210,19 @@
 by (simp add: hypnat_diff_diff_left hypnat_add_commute)
 
 lemma hypnat_diff_add_inverse: "((n::hypnat) + m) - n = m"
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases m, cases n)
 apply (simp add: hypnat_minus hypnat_add)
 done
 declare hypnat_diff_add_inverse [simp]
 
 lemma hypnat_diff_add_inverse2:  "((m::hypnat) + n) - n = m"
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases m, cases n)
 apply (simp add: hypnat_minus hypnat_add)
 done
 declare hypnat_diff_add_inverse2 [simp]
 
 lemma hypnat_diff_cancel: "((k::hypnat) + m) - (k+n) = m - n"
-apply (rule eq_Abs_hypnat [of k])
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases k, cases m, cases n)
 apply (simp add: hypnat_minus hypnat_add)
 done
 declare hypnat_diff_cancel [simp]
@@ -239,8 +232,7 @@
 declare hypnat_diff_cancel2 [simp]
 
 lemma hypnat_diff_add_0: "(n::hypnat) - (n+m) = (0::hypnat)"
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases m, cases n)
 apply (simp add: hypnat_zero_def hypnat_minus hypnat_add)
 done
 declare hypnat_diff_add_0 [simp]
@@ -250,7 +242,7 @@
 
 lemma hypnat_mult_congruent2:
     "congruent2 hypnatrel (%X Y. hypnatrel``{%n. X n * Y n})"
-by (unfold congruent2_def, auto, ultra)
+by (simp add: congruent2_def, auto, ultra)
 
 lemma hypnat_mult:
   "Abs_hypnat(hypnatrel``{%n. X n}) * Abs_hypnat(hypnatrel``{%n. Y n}) =
@@ -258,27 +250,22 @@
 by (simp add: hypnat_mult_def UN_equiv_class2 [OF equiv_hypnatrel hypnat_mult_congruent2])
 
 lemma hypnat_mult_commute: "(z::hypnat) * w = w * z"
-apply (rule eq_Abs_hypnat [of z])
-apply (rule eq_Abs_hypnat [of w])
+apply (cases z, cases w)
 apply (simp add: hypnat_mult mult_ac)
 done
 
 lemma hypnat_mult_assoc: "((z1::hypnat) * z2) * z3 = z1 * (z2 * z3)"
-apply (rule eq_Abs_hypnat [of z1])
-apply (rule eq_Abs_hypnat [of z2])
-apply (rule eq_Abs_hypnat [of z3])
+apply (cases z1, cases z2, cases z3)
 apply (simp add: hypnat_mult mult_assoc)
 done
 
 lemma hypnat_mult_1: "(1::hypnat) * z = z"
-apply (rule eq_Abs_hypnat [of z])
+apply (cases z)
 apply (simp add: hypnat_mult hypnat_one_def)
 done
 
 lemma hypnat_diff_mult_distrib: "((m::hypnat) - n) * k = (m * k) - (n * k)"
-apply (rule eq_Abs_hypnat [of k])
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases k, cases m, cases n)
 apply (simp add: hypnat_mult hypnat_minus diff_mult_distrib)
 done
 
@@ -286,9 +273,7 @@
 by (simp add: hypnat_diff_mult_distrib hypnat_mult_commute [of k])
 
 lemma hypnat_add_mult_distrib: "((z1::hypnat) + z2) * w = (z1 * w) + (z2 * w)"
-apply (rule eq_Abs_hypnat [of z1])
-apply (rule eq_Abs_hypnat [of z2])
-apply (rule eq_Abs_hypnat [of w])
+apply (cases z1, cases z2, cases w)
 apply (simp add: hypnat_mult hypnat_add add_mult_distrib)
 done
 
@@ -324,25 +309,22 @@
 lemma hypnat_le:
       "(Abs_hypnat(hypnatrel``{%n. X n}) \<le> Abs_hypnat(hypnatrel``{%n. Y n})) =
        ({n. X n \<le> Y n} \<in> FreeUltrafilterNat)"
-apply (unfold hypnat_le_def)
+apply (simp add: hypnat_le_def)
 apply (auto intro!: lemma_hypnatrel_refl, ultra)
 done
 
 lemma hypnat_le_refl: "w \<le> (w::hypnat)"
-apply (rule eq_Abs_hypnat [of w])
+apply (cases w)
 apply (simp add: hypnat_le)
 done
 
 lemma hypnat_le_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::hypnat)"
-apply (rule eq_Abs_hypnat [of i])
-apply (rule eq_Abs_hypnat [of j])
-apply (rule eq_Abs_hypnat [of k])
+apply (cases i, cases j, cases k)
 apply (simp add: hypnat_le, ultra)
 done
 
 lemma hypnat_le_anti_sym: "[| z \<le> w; w \<le> z |] ==> z = (w::hypnat)"
-apply (rule eq_Abs_hypnat [of z])
-apply (rule eq_Abs_hypnat [of w])
+apply (cases z, cases w)
 apply (simp add: hypnat_le, ultra)
 done
 
@@ -357,8 +339,7 @@
 
 (* Axiom 'linorder_linear' of class 'linorder': *)
 lemma hypnat_le_linear: "(z::hypnat) \<le> w | w \<le> z"
-apply (rule eq_Abs_hypnat [of z])
-apply (rule eq_Abs_hypnat [of w])
+apply (cases z, cases w)
 apply (auto simp add: hypnat_le, ultra)
 done
 
@@ -366,16 +347,12 @@
   by (intro_classes, rule hypnat_le_linear)
 
 lemma hypnat_add_left_mono: "x \<le> y ==> z + x \<le> z + (y::hypnat)"
-apply (rule eq_Abs_hypnat [of x])
-apply (rule eq_Abs_hypnat [of y])
-apply (rule eq_Abs_hypnat [of z])
+apply (cases x, cases y, cases z)
 apply (auto simp add: hypnat_le hypnat_add)
 done
 
 lemma hypnat_mult_less_mono2: "[| (0::hypnat)<z; x<y |] ==> z*x<z*y"
-apply (rule eq_Abs_hypnat [of x])
-apply (rule eq_Abs_hypnat [of y])
-apply (rule eq_Abs_hypnat [of z])
+apply (cases x, cases y, cases z)
 apply (simp add: hypnat_zero_def  hypnat_mult linorder_not_le [symmetric])
 apply (auto simp add: hypnat_le, ultra)
 done
@@ -396,19 +373,17 @@
 qed
 
 lemma hypnat_le_zero_cancel [iff]: "(n \<le> (0::hypnat)) = (n = 0)"
-apply (rule eq_Abs_hypnat [of n])
+apply (cases n)
 apply (simp add: hypnat_zero_def hypnat_le)
 done
 
 lemma hypnat_mult_is_0 [simp]: "(m*n = (0::hypnat)) = (m=0 | n=0)"
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases m, cases n)
 apply (auto simp add: hypnat_zero_def hypnat_mult, ultra+)
 done
 
 lemma hypnat_diff_is_0_eq [simp]: "((m::hypnat) - n = 0) = (m \<le> n)"
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases m, cases n)
 apply (simp add: hypnat_le hypnat_minus hypnat_zero_def)
 done
 
@@ -424,19 +399,18 @@
 done
 
 lemma hypnat_not_less0 [iff]: "~ n < (0::hypnat)"
-apply (rule eq_Abs_hypnat [of n])
+apply (cases n)
 apply (auto simp add: hypnat_zero_def hypnat_less)
 done
 
 lemma hypnat_less_one [iff]:
       "(n < (1::hypnat)) = (n=0)"
-apply (rule eq_Abs_hypnat [of n])
+apply (cases n)
 apply (auto simp add: hypnat_zero_def hypnat_one_def hypnat_less)
 done
 
 lemma hypnat_add_diff_inverse: "~ m<n ==> n+(m-n) = (m::hypnat)"
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases m, cases n)
 apply (simp add: hypnat_minus hypnat_add hypnat_less split: nat_diff_split, ultra)
 done
 
@@ -484,7 +458,7 @@
 next
   case False
     thus ?thesis
-      by (auto simp add: linorder_not_less dest: order_le_less_trans); 
+      by (auto simp add: linorder_not_less dest: order_le_less_trans) 
 qed
 
 
@@ -563,15 +537,13 @@
 done
 
 lemma Nats_diff [simp]: "[|a \<in> Nats; b \<in> Nats|] ==> (a-b :: hypnat) \<in> Nats"
-apply (auto simp add: of_nat_eq_add Nats_def split: hypnat_diff_split)
-done
+by (auto simp add: of_nat_eq_add Nats_def split: hypnat_diff_split)
 
 lemma lemma_unbounded_set [simp]: "{n::nat. m < n} \<in> FreeUltrafilterNat"
 apply (insert finite_atMost [of m]) 
 apply (simp add: atMost_def) 
 apply (drule FreeUltrafilterNat_finite) 
-apply (drule FreeUltrafilterNat_Compl_mem) 
-apply ultra
+apply (drule FreeUltrafilterNat_Compl_mem, ultra)
 done
 
 lemma Compl_Collect_le: "- {n::nat. N \<le> n} = {n. n < N}"
@@ -581,7 +553,7 @@
 lemma hypnat_of_nat_eq:
      "hypnat_of_nat m  = Abs_hypnat(hypnatrel``{%n::nat. m})"
 apply (induct m) 
-apply (simp_all add: hypnat_zero_def hypnat_one_def hypnat_add); 
+apply (simp_all add: hypnat_zero_def hypnat_one_def hypnat_add) 
 done
 
 lemma SHNat_eq: "Nats = {n. \<exists>N. n = hypnat_of_nat N}"
@@ -599,8 +571,7 @@
 
 (* Infinite hypernatural not in embedded Nats *)
 lemma SHNAT_omega_not_mem [simp]: "whn \<notin> Nats"
-apply (blast dest: hypnat_omega_gt_SHNat) 
-done
+by (blast dest: hypnat_omega_gt_SHNat)
 
 lemma hypnat_of_nat_less_whn [simp]: "hypnat_of_nat n < whn"
 apply (insert hypnat_omega_gt_SHNat [of "hypnat_of_nat n"])
@@ -657,7 +628,7 @@
 lemma HNatInfinite_FreeUltrafilterNat:
      "x \<in> HNatInfinite 
       ==> \<exists>X \<in> Rep_hypnat x. \<forall>u. {n. u < X n}:  FreeUltrafilterNat"
-apply (rule eq_Abs_hypnat [of x])
+apply (cases x)
 apply (auto simp add: HNatInfinite_iff SHNat_eq hypnat_of_nat_eq)
 apply (rule bexI [OF _ lemma_hypnatrel_refl], clarify) 
 apply (auto simp add: hypnat_of_nat_def hypnat_less)
@@ -666,7 +637,7 @@
 lemma FreeUltrafilterNat_HNatInfinite:
      "\<exists>X \<in> Rep_hypnat x. \<forall>u. {n. u < X n}:  FreeUltrafilterNat
       ==> x \<in> HNatInfinite"
-apply (rule eq_Abs_hypnat [of x])
+apply (cases x)
 apply (auto simp add: hypnat_less HNatInfinite_iff SHNat_eq hypnat_of_nat_eq)
 apply (drule spec, ultra, auto) 
 done
@@ -708,8 +679,7 @@
 lemma HNatInfinite_SHNat_add:
      "[| x \<in> HNatInfinite; y \<in> Nats |] ==> x + y \<in> HNatInfinite"
 apply (auto simp add: HNatInfinite_not_Nats_iff) 
-apply (drule_tac a = "x + y" in Nats_diff)
-apply (auto ); 
+apply (drule_tac a = "x + y" in Nats_diff, auto) 
 done
 
 lemma HNatInfinite_Nats_imp_less: "[| x \<in> HNatInfinite; y \<in> Nats |] ==> y < x"
@@ -764,8 +734,7 @@
 
 lemma hypreal_of_hypnat_inject [simp]:
      "(hypreal_of_hypnat m = hypreal_of_hypnat n) = (m=n)"
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases m, cases n)
 apply (auto simp add: hypreal_of_hypnat)
 done
 
@@ -777,22 +746,19 @@
 
 lemma hypreal_of_hypnat_add [simp]:
      "hypreal_of_hypnat (m + n) = hypreal_of_hypnat m + hypreal_of_hypnat n"
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases m, cases n)
 apply (simp add: hypreal_of_hypnat hypreal_add hypnat_add real_of_nat_add)
 done
 
 lemma hypreal_of_hypnat_mult [simp]:
      "hypreal_of_hypnat (m * n) = hypreal_of_hypnat m * hypreal_of_hypnat n"
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases m, cases n)
 apply (simp add: hypreal_of_hypnat hypreal_mult hypnat_mult real_of_nat_mult)
 done
 
 lemma hypreal_of_hypnat_less_iff [simp]:
      "(hypreal_of_hypnat n < hypreal_of_hypnat m) = (n < m)"
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases m, cases n)
 apply (simp add: hypreal_of_hypnat hypreal_less hypnat_less)
 done
 
@@ -801,13 +767,13 @@
 declare hypreal_of_hypnat_eq_zero_iff [simp]
 
 lemma hypreal_of_hypnat_ge_zero [simp]: "0 \<le> hypreal_of_hypnat n"
-apply (rule eq_Abs_hypnat [of n])
+apply (cases n)
 apply (simp add: hypreal_of_hypnat hypreal_zero_num hypreal_le)
 done
 
 lemma HNatInfinite_inverse_Infinitesimal [simp]:
      "n \<in> HNatInfinite ==> inverse (hypreal_of_hypnat n) \<in> Infinitesimal"
-apply (rule eq_Abs_hypnat [of n])
+apply (cases n)
 apply (auto simp add: hypreal_of_hypnat hypreal_inverse 
       HNatInfinite_FreeUltrafilterNat_iff Infinitesimal_FreeUltrafilterNat_iff2)
 apply (rule bexI, rule_tac [2] lemma_hyprel_refl, auto)
diff -r bbfa6b01a55f -r 6be497cacab5 src/HOL/Hyperreal/HyperPow.thy
--- a/src/HOL/Hyperreal/HyperPow.thy	Mon Mar 15 10:46:01 2004 +0100
+++ b/src/HOL/Hyperreal/HyperPow.thy	Mon Mar 15 10:46:19 2004 +0100
@@ -146,78 +146,62 @@
 
 lemma hyperpow_not_zero [rule_format (no_asm)]:
      "r \<noteq> (0::hypreal) --> r pow n \<noteq> 0"
-apply (simp (no_asm) add: hypreal_zero_def)
-apply (rule eq_Abs_hypnat [of n])
-apply (rule eq_Abs_hypreal [of r])
+apply (simp (no_asm) add: hypreal_zero_def, cases n, cases r)
 apply (auto simp add: hyperpow)
 apply (drule FreeUltrafilterNat_Compl_mem, ultra)
 done
 
 lemma hyperpow_inverse:
      "r \<noteq> (0::hypreal) --> inverse(r pow n) = (inverse r) pow n"
-apply (simp (no_asm) add: hypreal_zero_def)
-apply (rule eq_Abs_hypnat [of n])
-apply (rule eq_Abs_hypreal [of r])
+apply (simp (no_asm) add: hypreal_zero_def, cases n, cases r)
 apply (auto dest!: FreeUltrafilterNat_Compl_mem simp add: hypreal_inverse hyperpow)
 apply (rule FreeUltrafilterNat_subset)
 apply (auto dest: realpow_not_zero intro: power_inverse)
 done
 
 lemma hyperpow_hrabs: "abs r pow n = abs (r pow n)"
-apply (rule eq_Abs_hypnat [of n])
-apply (rule eq_Abs_hypreal [of r])
+apply (cases n, cases r)
 apply (auto simp add: hypreal_hrabs hyperpow power_abs [symmetric])
 done
 
 lemma hyperpow_add: "r pow (n + m) = (r pow n) * (r pow m)"
-apply (rule eq_Abs_hypnat [of n])
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypreal [of r])
+apply (cases n, cases m, cases r)
 apply (auto simp add: hyperpow hypnat_add hypreal_mult power_add)
 done
 
 lemma hyperpow_one: "r pow (1::hypnat) = r"
-apply (unfold hypnat_one_def)
-apply (rule eq_Abs_hypreal [of r])
+apply (unfold hypnat_one_def, cases r)
 apply (auto simp add: hyperpow)
 done
 declare hyperpow_one [simp]
 
 lemma hyperpow_two:
      "r pow ((1::hypnat) + (1::hypnat)) = r * r"
-apply (unfold hypnat_one_def)
-apply (rule eq_Abs_hypreal [of r])
+apply (unfold hypnat_one_def, cases r)
 apply (auto simp add: hyperpow hypnat_add hypreal_mult)
 done
 
 lemma hyperpow_gt_zero: "(0::hypreal) < r ==> 0 < r pow n"
-apply (simp add: hypreal_zero_def)
-apply (rule eq_Abs_hypnat [of n])
-apply (rule eq_Abs_hypreal [of r])
+apply (simp add: hypreal_zero_def, cases n, cases r)
 apply (auto elim!: FreeUltrafilterNat_subset zero_less_power
                    simp add: hyperpow hypreal_less hypreal_le)
 done
 
 lemma hyperpow_ge_zero: "(0::hypreal) \<le> r ==> 0 \<le> r pow n"
-apply (simp add: hypreal_zero_def)
-apply (rule eq_Abs_hypnat [of n])
-apply (rule eq_Abs_hypreal [of r])
+apply (simp add: hypreal_zero_def, cases n, cases r)
 apply (auto elim!: FreeUltrafilterNat_subset zero_le_power 
             simp add: hyperpow hypreal_le)
 done
 
 lemma hyperpow_le: "[|(0::hypreal) < x; x \<le> y|] ==> x pow n \<le> y pow n"
-apply (simp add: hypreal_zero_def)
-apply (rule eq_Abs_hypnat [of n])
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of y])
+apply (simp add: hypreal_zero_def, cases n, cases x, cases y)
 apply (auto simp add: hyperpow hypreal_le hypreal_less)
 apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset], assumption)
 apply (auto intro: power_mono)
 done
 
 lemma hyperpow_eq_one: "1 pow n = (1::hypreal)"
-apply (rule eq_Abs_hypnat [of n])
+apply (cases n)
 apply (auto simp add: hypreal_one_def hyperpow)
 done
 declare hyperpow_eq_one [simp]
@@ -225,15 +209,13 @@
 lemma hrabs_hyperpow_minus_one: "abs(-1 pow n) = (1::hypreal)"
 apply (subgoal_tac "abs ((- (1::hypreal)) pow n) = (1::hypreal) ")
 apply simp
-apply (rule eq_Abs_hypnat [of n])
+apply (cases n)
 apply (auto simp add: hypreal_one_def hyperpow hypreal_minus hypreal_hrabs)
 done
 declare hrabs_hyperpow_minus_one [simp]
 
 lemma hyperpow_mult: "(r * s) pow n = (r pow n) * (s pow n)"
-apply (rule eq_Abs_hypnat [of n])
-apply (rule eq_Abs_hypreal [of r])
-apply (rule eq_Abs_hypreal [of s])
+apply (cases n, cases r, cases s)
 apply (auto simp add: hyperpow hypreal_mult power_mult_distrib)
 done
 
@@ -272,8 +254,7 @@
      "-1 pow ((1 + 1)*n) = (1::hypreal)"
 apply (subgoal_tac " (- ((1::hypreal))) pow ((1 + 1)*n) = (1::hypreal) ")
 apply simp
-apply (simp only: hypreal_one_def)
-apply (rule eq_Abs_hypnat [of n])
+apply (simp only: hypreal_one_def, cases n)
 apply (auto simp add: nat_mult_2 [symmetric] hyperpow hypnat_add hypreal_minus
                       left_distrib)
 done
@@ -281,9 +262,7 @@
 
 lemma hyperpow_less_le:
      "[|(0::hypreal) \<le> r; r \<le> 1; n < N|] ==> r pow N \<le> r pow n"
-apply (rule eq_Abs_hypnat [of n])
-apply (rule eq_Abs_hypnat [of N])
-apply (rule eq_Abs_hypreal [of r])
+apply (cases n, cases N, cases r)
 apply (auto simp add: hyperpow hypreal_le hypreal_less hypnat_less 
             hypreal_zero_def hypreal_one_def)
 apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset])
@@ -338,7 +317,7 @@
 
 lemma hrealpow_hyperpow_Infinitesimal_iff:
      "(x ^ n \<in> Infinitesimal) = (x pow (hypnat_of_nat n) \<in> Infinitesimal)"
-apply (rule eq_Abs_hypreal [of x])
+apply (cases x)
 apply (simp add: hrealpow hyperpow hypnat_of_nat_eq)
 done
 
diff -r bbfa6b01a55f -r 6be497cacab5 src/HOL/Hyperreal/NSA.thy
--- a/src/HOL/Hyperreal/NSA.thy	Mon Mar 15 10:46:01 2004 +0100
+++ b/src/HOL/Hyperreal/NSA.thy	Mon Mar 15 10:46:19 2004 +0100
@@ -1848,7 +1848,7 @@
 lemma HFinite_FreeUltrafilterNat:
     "x \<in> HFinite 
      ==> \<exists>X \<in> Rep_hypreal x. \<exists>u. {n. abs (X n) < u} \<in> FreeUltrafilterNat"
-apply (rule eq_Abs_hypreal [of x])
+apply (cases x)
 apply (auto simp add: HFinite_def abs_less_iff minus_less_iff [of x] 
               hypreal_less SReal_iff hypreal_minus hypreal_of_real_def)
 apply (rule_tac x=x in bexI) 
@@ -1859,7 +1859,7 @@
      "\<exists>X \<in> Rep_hypreal x.
        \<exists>u. {n. abs (X n) < u} \<in> FreeUltrafilterNat
        ==>  x \<in> HFinite"
-apply (rule eq_Abs_hypreal [of x])
+apply (cases x)
 apply (auto simp add: HFinite_def abs_less_iff minus_less_iff [of x])
 apply (rule_tac x = "hypreal_of_real u" in bexI)
 apply (auto simp add: hypreal_less SReal_iff hypreal_minus hypreal_of_real_def, ultra+)
@@ -1954,7 +1954,7 @@
            \<forall>u. 0 < u --> {n. abs (X n) < u} \<in> FreeUltrafilterNat"
 apply (simp add: Infinitesimal_def)
 apply (auto simp add: abs_less_iff minus_less_iff [of x])
-apply (rule eq_Abs_hypreal [of x])
+apply (cases x)
 apply (auto, rule bexI [OF _ lemma_hyprel_refl], safe)
 apply (drule hypreal_of_real_less_iff [THEN iffD2])
 apply (drule_tac x = "hypreal_of_real u" in bspec, auto)
@@ -1966,7 +1966,7 @@
             \<forall>u. 0 < u --> {n. abs (X n) < u} \<in> FreeUltrafilterNat
       ==> x \<in> Infinitesimal"
 apply (simp add: Infinitesimal_def)
-apply (rule eq_Abs_hypreal [of x])
+apply (cases x)
 apply (auto simp add: abs_less_iff abs_interval_iff minus_less_iff [of x])
 apply (auto simp add: SReal_iff)
 apply (drule_tac [!] x=y in spec) 
diff -r bbfa6b01a55f -r 6be497cacab5 src/HOL/Hyperreal/NatStar.thy
--- a/src/HOL/Hyperreal/NatStar.thy	Mon Mar 15 10:46:01 2004 +0100
+++ b/src/HOL/Hyperreal/NatStar.thy	Mon Mar 15 10:46:19 2004 +0100
@@ -213,13 +213,13 @@
 
 lemma starfunNat_mult:
      "( *fNat* f) z * ( *fNat* g) z = ( *fNat* (%x. f x * g x)) z"
-apply (rule eq_Abs_hypnat [of z])
+apply (cases z)
 apply (simp add: starfunNat hypreal_mult)
 done
 
 lemma starfunNat2_mult:
      "( *fNat2* f) z * ( *fNat2* g) z = ( *fNat2* (%x. f x * g x)) z"
-apply (rule eq_Abs_hypnat [of z])
+apply (cases z)
 apply (simp add: starfunNat2 hypnat_mult)
 done
 
@@ -227,19 +227,19 @@
 
 lemma starfunNat_add:
      "( *fNat* f) z + ( *fNat* g) z = ( *fNat* (%x. f x + g x)) z"
-apply (rule eq_Abs_hypnat [of z])
+apply (cases z)
 apply (simp add: starfunNat hypreal_add)
 done
 
 lemma starfunNat2_add:
      "( *fNat2* f) z + ( *fNat2* g) z = ( *fNat2* (%x. f x + g x)) z"
-apply (rule eq_Abs_hypnat [of z])
+apply (cases z)
 apply (simp add: starfunNat2 hypnat_add)
 done
 
 lemma starfunNat2_minus:
      "( *fNat2* f) z - ( *fNat2* g) z = ( *fNat2* (%x. f x - g x)) z"
-apply (rule eq_Abs_hypnat [of z])
+apply (cases z)
 apply (simp add: starfunNat2 hypnat_minus)
 done
 
@@ -285,23 +285,23 @@
 text{*NS extension of constant function*}
 
 lemma starfunNat_const_fun [simp]: "( *fNat* (%x. k)) z = hypreal_of_real k"
-apply (rule eq_Abs_hypnat [of z])
+apply (cases z)
 apply (simp add: starfunNat hypreal_of_real_def)
 done
 
 lemma starfunNat2_const_fun [simp]: "( *fNat2* (%x. k)) z = hypnat_of_nat  k"
-apply (rule eq_Abs_hypnat [of z])
+apply (cases z)
 apply (simp add: starfunNat2 hypnat_of_nat_eq)
 done
 
 lemma starfunNat_minus: "- ( *fNat* f) x = ( *fNat* (%x. - f x)) x"
-apply (rule eq_Abs_hypnat [of x])
+apply (cases x)
 apply (simp add: starfunNat hypreal_minus)
 done
 
 lemma starfunNat_inverse:
      "inverse (( *fNat* f) x) = ( *fNat* (%x. inverse (f x))) x"
-apply (rule eq_Abs_hypnat [of x])
+apply (cases x)
 apply (simp add: starfunNat hypreal_inverse)
 done
 
@@ -346,27 +346,27 @@
 
 lemma starfunNat_shift_one:
      "( *fNat* (%n. f (Suc n))) N = ( *fNat* f) (N + (1::hypnat))"
-apply (rule eq_Abs_hypnat [of N])
+apply (cases N)
 apply (simp add: starfunNat hypnat_one_def hypnat_add)
 done
 
 text{*Nonstandard extension with absolute value*}
 
 lemma starfunNat_rabs: "( *fNat* (%n. abs (f n))) N = abs(( *fNat* f) N)"
-apply (rule eq_Abs_hypnat [of N])
+apply (cases N)
 apply (simp add: starfunNat hypreal_hrabs)
 done
 
 text{*The hyperpow function as a nonstandard extension of realpow*}
 
 lemma starfunNat_pow: "( *fNat* (%n. r ^ n)) N = (hypreal_of_real r) pow N"
-apply (rule eq_Abs_hypnat [of N])
+apply (cases N)
 apply (simp add: hyperpow hypreal_of_real_def starfunNat)
 done
 
 lemma starfunNat_pow2:
      "( *fNat* (%n. (X n) ^ m)) N = ( *fNat* X) N pow hypnat_of_nat m"
-apply (rule eq_Abs_hypnat [of N])
+apply (cases N)
 apply (simp add: hyperpow hypnat_of_nat_eq starfunNat)
 done
 
@@ -411,7 +411,7 @@
 
 lemma starfunNat_n_mult:
      "( *fNatn* f) z * ( *fNatn* g) z = ( *fNatn* (% i x. f i x * g i x)) z"
-apply (rule eq_Abs_hypnat [of z])
+apply (cases z)
 apply (simp add: starfunNat_n hypreal_mult)
 done
 
@@ -419,7 +419,7 @@
 
 lemma starfunNat_n_add:
      "( *fNatn* f) z + ( *fNatn* g) z = ( *fNatn* (%i x. f i x + g i x)) z"
-apply (rule eq_Abs_hypnat [of z])
+apply (cases z)
 apply (simp add: starfunNat_n hypreal_add)
 done
 
@@ -427,7 +427,7 @@
 
 lemma starfunNat_n_add_minus:
      "( *fNatn* f) z + -( *fNatn* g) z = ( *fNatn* (%i x. f i x + -g i x)) z"
-apply (rule eq_Abs_hypnat [of z])
+apply (cases z)
 apply (simp add: starfunNat_n hypreal_minus hypreal_add)
 done
 
@@ -436,12 +436,12 @@
 
 lemma starfunNat_n_const_fun [simp]:
      "( *fNatn* (%i x. k)) z = hypreal_of_real  k"
-apply (rule eq_Abs_hypnat [of z])
+apply (cases z)
 apply (simp add: starfunNat_n hypreal_of_real_def)
 done
 
 lemma starfunNat_n_minus: "- ( *fNatn* f) x = ( *fNatn* (%i x. - (f i) x)) x"
-apply (rule eq_Abs_hypnat [of x])
+apply (cases x)
 apply (simp add: starfunNat_n hypreal_minus)
 done
 
diff -r bbfa6b01a55f -r 6be497cacab5 src/HOL/Hyperreal/Star.thy
--- a/src/HOL/Hyperreal/Star.thy	Mon Mar 15 10:46:01 2004 +0100
+++ b/src/HOL/Hyperreal/Star.thy	Mon Mar 15 10:46:19 2004 +0100
@@ -1,8 +1,7 @@
 (*  Title       : Star.thy
     Author      : Jacques D. Fleuriot
     Copyright   : 1998  University of Cambridge
-    Description : defining *-transforms in NSA which extends sets of reals,
-                  and real=>real functions
+    Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4
 *)
 
 header{*Star-Transforms in Non-Standard Analysis*}
@@ -12,30 +11,30 @@
 constdefs
     (* nonstandard extension of sets *)
     starset :: "real set => hypreal set"          ("*s* _" [80] 80)
-    "*s* A  == {x. ALL X: Rep_hypreal(x). {n::nat. X n : A}: FreeUltrafilterNat}"
+    "*s* A  == {x. \<forall>X \<in> Rep_hypreal(x). {n::nat. X n  \<in> A}: FreeUltrafilterNat}"
 
     (* internal sets *)
     starset_n :: "(nat => real set) => hypreal set"        ("*sn* _" [80] 80)
-    "*sn* As  == {x. ALL X: Rep_hypreal(x). {n::nat. X n : (As n)}: FreeUltrafilterNat}"
+    "*sn* As  == {x. \<forall>X \<in> Rep_hypreal(x). {n::nat. X n : (As n)}: FreeUltrafilterNat}"
 
     InternalSets :: "hypreal set set"
-    "InternalSets == {X. EX As. X = *sn* As}"
+    "InternalSets == {X. \<exists>As. X = *sn* As}"
 
     (* nonstandard extension of function *)
     is_starext  :: "[hypreal => hypreal, real => real] => bool"
-    "is_starext F f == (ALL x y. EX X: Rep_hypreal(x). EX Y: Rep_hypreal(y).
+    "is_starext F f == (\<forall>x y. \<exists>X \<in> Rep_hypreal(x). \<exists>Y \<in> Rep_hypreal(y).
                         ((y = (F x)) = ({n. Y n = f(X n)} : FreeUltrafilterNat)))"
 
     starfun :: "(real => real) => hypreal => hypreal"       ("*f* _" [80] 80)
-    "*f* f  == (%x. Abs_hypreal(UN X: Rep_hypreal(x). hyprel``{%n. f(X n)}))"
+    "*f* f  == (%x. Abs_hypreal(\<Union>X \<in> Rep_hypreal(x). hyprel``{%n. f(X n)}))"
 
     (* internal functions *)
     starfun_n :: "(nat => (real => real)) => hypreal => hypreal"
                  ("*fn* _" [80] 80)
-    "*fn* F  == (%x. Abs_hypreal(UN X: Rep_hypreal(x). hyprel``{%n. (F n)(X n)}))"
+    "*fn* F  == (%x. Abs_hypreal(\<Union>X \<in> Rep_hypreal(x). hyprel``{%n. (F n)(X n)}))"
 
     InternalFuns :: "(hypreal => hypreal) set"
-    "InternalFuns == {X. EX F. X = *fn* F}"
+    "InternalFuns == {X. \<exists>F. X = *fn* F}"
 
 
 
@@ -47,7 +46,7 @@
    referee for the JCM Paper: let f(x) be least y such
    that  Q(x,y)
 *)
-lemma no_choice: "ALL x. EX y. Q x y ==> EX (f :: nat => nat). ALL x. Q x (f x)"
+lemma no_choice: "\<forall>x. \<exists>y. Q x y ==> \<exists>(f :: nat => nat). \<forall>x. Q x (f x)"
 apply (rule_tac x = "%x. LEAST y. Q x y" in exI)
 apply (blast intro: LeastI)
 done
@@ -57,20 +56,15 @@
  ------------------------------------------------------------*)
 
 lemma STAR_real_set: "*s*(UNIV::real set) = (UNIV::hypreal set)"
-
-apply (unfold starset_def, auto)
-done
+by (simp add: starset_def)
 declare STAR_real_set [simp]
 
 lemma STAR_empty_set: "*s* {} = {}"
-apply (unfold starset_def, safe)
-apply (rule_tac z = x in eq_Abs_hypreal)
-apply (drule_tac x = "%n. xa n" in bspec, auto)
-done
+by (simp add: starset_def)
 declare STAR_empty_set [simp]
 
 lemma STAR_Un: "*s* (A Un B) = *s* A Un *s* B"
-apply (unfold starset_def, auto)
+apply (auto simp add: starset_def)
   prefer 3 apply (blast intro: FreeUltrafilterNat_subset)
  prefer 2 apply (blast intro: FreeUltrafilterNat_subset)
 apply (drule FreeUltrafilterNat_Compl_mem)
@@ -79,7 +73,7 @@
 done
 
 lemma STAR_Int: "*s* (A Int B) = *s* A Int *s* B"
-apply (unfold starset_def, auto)
+apply (simp add: starset_def, auto)
 prefer 3 apply (blast intro: FreeUltrafilterNat_Int FreeUltrafilterNat_subset)
 apply (blast intro: FreeUltrafilterNat_subset)+
 done
@@ -98,23 +92,23 @@
 by (auto simp add: Diff_eq STAR_Int STAR_Compl)
 
 lemma STAR_subset: "A <= B ==> *s* A <= *s* B"
-apply (unfold starset_def)
+apply (simp add: starset_def)
 apply (blast intro: FreeUltrafilterNat_subset)+
 done
 
-lemma STAR_mem: "a : A ==> hypreal_of_real a : *s* A"
-apply (unfold starset_def hypreal_of_real_def)
+lemma STAR_mem: "a  \<in> A ==> hypreal_of_real a : *s* A"
+apply (simp add: starset_def hypreal_of_real_def)
 apply (auto intro: FreeUltrafilterNat_subset)
 done
 
 lemma STAR_hypreal_of_real_image_subset: "hypreal_of_real ` A <= *s* A"
-apply (unfold starset_def)
+apply (simp add: starset_def)
 apply (auto simp add: hypreal_of_real_def)
 apply (blast intro: FreeUltrafilterNat_subset)
 done
 
 lemma STAR_hypreal_of_real_Int: "*s* X Int Reals = hypreal_of_real ` X"
-apply (unfold starset_def)
+apply (simp add: starset_def)
 apply (auto simp add: hypreal_of_real_def SReal_def)
 apply (simp add: hypreal_of_real_def [symmetric])
 apply (rule imageI, rule ccontr)
@@ -123,21 +117,21 @@
 prefer 2 apply (blast intro: FreeUltrafilterNat_subset, auto)
 done
 
-lemma lemma_not_hyprealA: "x \<notin> hypreal_of_real ` A ==> ALL y: A. x \<noteq> hypreal_of_real y"
+lemma lemma_not_hyprealA: "x \<notin> hypreal_of_real ` A ==> \<forall>y \<in> A. x \<noteq> hypreal_of_real y"
 by auto
 
 lemma lemma_Compl_eq: "- {n. X n = xa} = {n. X n \<noteq> xa}"
 by auto
 
 lemma STAR_real_seq_to_hypreal:
-    "ALL n. (X n) \<notin> M
+    "\<forall>n. (X n) \<notin> M
           ==> Abs_hypreal(hyprel``{X}) \<notin> *s* M"
-apply (unfold starset_def)
-apply (auto, rule bexI, rule_tac [2] lemma_hyprel_refl, auto)
+apply (simp add: starset_def)
+apply (rule bexI, rule_tac [2] lemma_hyprel_refl, auto)
 done
 
 lemma STAR_singleton: "*s* {x} = {hypreal_of_real x}"
-apply (unfold starset_def)
+apply (simp add: starset_def)
 apply (auto simp add: hypreal_of_real_def)
 apply (rule_tac z = xa in eq_Abs_hypreal)
 apply (auto intro: FreeUltrafilterNat_subset)
@@ -157,11 +151,8 @@
    sequence) as a special case of an internal set
  -----------------------------------------------------------------*)
 
-lemma starset_n_starset:
-     "ALL n. (As n = A) ==> *sn* As = *s* A"
-
-apply (unfold starset_n_def starset_def, auto)
-done
+lemma starset_n_starset: "\<forall>n. (As n = A) ==> *sn* As = *s* A"
+by (simp add: starset_n_def starset_def)
 
 
 (*----------------------------------------------------------------*)
@@ -173,11 +164,8 @@
 (* constant sequence) as a special case of an internal function   *)
 (*----------------------------------------------------------------*)
 
-lemma starfun_n_starfun:
-     "ALL n. (F n = f) ==> *fn* F = *f* f"
-
-apply (unfold starfun_n_def starfun_def, auto)
-done
+lemma starfun_n_starfun: "\<forall>n. (F n = f) ==> *fn* F = *f* f"
+by (simp add: starfun_n_def starfun_def)
 
 
 (*
@@ -193,7 +181,7 @@
 
 lemma hrabs_is_starext_rabs: "is_starext abs abs"
 
-apply (unfold is_starext_def, safe)
+apply (simp add: is_starext_def, safe)
 apply (rule_tac z = x in eq_Abs_hypreal)
 apply (rule_tac z = y in eq_Abs_hypreal, auto)
 apply (rule bexI, rule_tac [2] lemma_hyprel_refl)
@@ -202,7 +190,7 @@
 apply (arith | ultra)+
 done
 
-lemma Rep_hypreal_FreeUltrafilterNat: "[| X: Rep_hypreal z; Y: Rep_hypreal z |]
+lemma Rep_hypreal_FreeUltrafilterNat: "[| X \<in> Rep_hypreal z; Y \<in> Rep_hypreal z |]
       ==> {n. X n = Y n} : FreeUltrafilterNat"
 apply (rule_tac z = z in eq_Abs_hypreal)
 apply (auto, ultra)
@@ -213,12 +201,12 @@
  -----------------------------------------------------------------------*)
 
 lemma starfun_congruent: "congruent hyprel (%X. hyprel``{%n. f (X n)})"
-by (unfold congruent_def, auto, ultra)
+by (simp add: congruent_def, auto, ultra)
 
 lemma starfun:
       "( *f* f) (Abs_hypreal(hyprel``{%n. X n})) =
        Abs_hypreal(hyprel `` {%n. f (X n)})"
-apply (unfold starfun_def)
+apply (simp add: starfun_def)
 apply (rule_tac f = Abs_hypreal in arg_cong)
 apply (simp add: hyprel_in_hypreal [THEN Abs_hypreal_inverse] 
                  UN_equiv_class [OF equiv_hyprel starfun_congruent])
@@ -260,8 +248,7 @@
 
 lemma starfun_diff:
   "( *f* f) xa  - ( *f* g) xa = ( *f* (%x. f x - g x)) xa"
-apply (unfold hypreal_diff_def real_diff_def)
-apply (rule starfun_add_minus)
+apply (simp add: diff_minus)
 done
 declare starfun_diff [symmetric, simp]
 
@@ -276,7 +263,7 @@
 done
 
 lemma starfun_o: "( *f* f) o ( *f* g) = ( *f* (f o g))"
-apply (unfold o_def)
+apply (simp add: o_def)
 apply (simp (no_asm) add: starfun_o2)
 done
 
@@ -311,7 +298,7 @@
 
 lemma is_starext_starfun: "is_starext ( *f* f) f"
 
-apply (unfold is_starext_def, auto)
+apply (simp add: is_starext_def, auto)
 apply (rule_tac z = x in eq_Abs_hypreal)
 apply (rule_tac z = y in eq_Abs_hypreal)
 apply (auto intro!: bexI simp add: starfun)
@@ -323,7 +310,7 @@
 
 lemma is_starfun_starext: "is_starext F f ==> F = *f* f"
 
-apply (unfold is_starext_def)
+apply (simp add: is_starext_def)
 apply (rule ext)
 apply (rule_tac z = x in eq_Abs_hypreal)
 apply (drule_tac x = x in spec)
@@ -394,10 +381,8 @@
 done
 declare starfun_inverse [symmetric, simp]
 
-lemma starfun_divide:
-  "( *f* f) xa  / ( *f* g) xa = ( *f* (%x. f x / g x)) xa"
-apply (unfold hypreal_divide_def real_divide_def, auto)
-done
+lemma starfun_divide: "( *f* f) xa  / ( *f* g) xa = ( *f* (%x. f x / g x)) xa"
+by (simp add: divide_inverse)
 declare starfun_divide [symmetric, simp]
 
 lemma starfun_inverse2: "inverse (( *f* f) x) = ( *f* (%x. inverse (f x))) x"
@@ -410,8 +395,8 @@
     topology of the reals
  ------------------------------------------------------------*)
 lemma starfun_mem_starset:
-      "( *f* f) x : *s* A ==> x : *s* {x. f x : A}"
-apply (unfold starset_def)
+      "( *f* f) x : *s* A ==> x : *s* {x. f x  \<in> A}"
+apply (simp add: starset_def)
 apply (rule_tac z = x in eq_Abs_hypreal)
 apply (auto simp add: starfun)
 apply (rename_tac "X")
@@ -438,7 +423,7 @@
 lemma STAR_rabs_add_minus:
    "*s* {x. abs (x + - y) < r} =
      {x. abs(x + -hypreal_of_real y) < hypreal_of_real r}"
-apply (unfold starset_def, safe)
+apply (simp add: starset_def, safe)
 apply (rule_tac [!] z = x in eq_Abs_hypreal)
 apply (auto intro!: exI dest!: bspec simp add: hypreal_minus hypreal_of_real_def hypreal_add hypreal_hrabs hypreal_less, ultra)
 done
@@ -446,7 +431,7 @@
 lemma STAR_starfun_rabs_add_minus:
   "*s* {x. abs (f x + - y) < r} =
        {x. abs(( *f* f) x + -hypreal_of_real y) < hypreal_of_real r}"
-apply (unfold starset_def, safe)
+apply (simp add: starset_def, safe)
 apply (rule_tac [!] z = x in eq_Abs_hypreal)
 apply (auto intro!: exI dest!: bspec simp add: hypreal_minus hypreal_of_real_def hypreal_add hypreal_hrabs hypreal_less starfun, ultra)
 done
@@ -457,10 +442,10 @@
    move both if possible?
  -------------------------------------------------------------------*)
 lemma Infinitesimal_FreeUltrafilterNat_iff2:
-     "(x:Infinitesimal) =
-      (EX X:Rep_hypreal(x).
-        ALL m. {n. abs(X n) < inverse(real(Suc m))}
-               : FreeUltrafilterNat)"
+     "(x \<in> Infinitesimal) =
+      (\<exists>X \<in> Rep_hypreal(x).
+        \<forall>m. {n. abs(X n) < inverse(real(Suc m))}
+                \<in>  FreeUltrafilterNat)"
 apply (rule eq_Abs_hypreal [of x])
 apply (auto intro!: bexI lemma_hyprel_refl 
             simp add: Infinitesimal_hypreal_of_nat_iff hypreal_of_real_def
@@ -469,7 +454,7 @@
 done
 
 lemma approx_FreeUltrafilterNat_iff: "(Abs_hypreal(hyprel``{X}) @= Abs_hypreal(hyprel``{Y})) =
-      (ALL m. {n. abs (X n + - Y n) <
+      (\<forall>m. {n. abs (X n + - Y n) <
                   inverse(real(Suc m))} : FreeUltrafilterNat)"
 apply (subst approx_minus_iff)
 apply (rule mem_infmal_iff [THEN subst])