# HG changeset patch
# User paulson
# Date 1083840180 -7200
# Node ID 14b2c22a7e402f9e19629d89b826a4fc1b7da20c
# Parent  ef1a47a4996be235a4438edfd913fee4d8331ea7
tidied

diff -r ef1a47a4996b -r 14b2c22a7e40 src/HOL/Hyperreal/HyperDef.thy
--- a/src/HOL/Hyperreal/HyperDef.thy	Thu May 06 12:42:20 2004 +0200
+++ b/src/HOL/Hyperreal/HyperDef.thy	Thu May 06 12:43:00 2004 +0200
@@ -18,7 +18,7 @@
 
   hyprel :: "((nat=>real)*(nat=>real)) set"
     "hyprel == {p. \<exists>X Y. p = ((X::nat=>real),Y) &
-                   {n::nat. X(n) = Y(n)}: FreeUltrafilterNat}"
+                   {n::nat. X(n) = Y(n)} \<in> FreeUltrafilterNat}"
 
 typedef hypreal = "UNIV//hyprel" 
     by (auto simp add: quotient_def) 
@@ -28,13 +28,13 @@
 defs (overloaded)
 
   hypreal_zero_def:
-  "0 == Abs_hypreal(hyprel``{%n::nat. (0::real)})"
+  "0 == Abs_hypreal(hyprel``{%n. 0})"
 
   hypreal_one_def:
-  "1 == Abs_hypreal(hyprel``{%n::nat. (1::real)})"
+  "1 == Abs_hypreal(hyprel``{%n. 1})"
 
   hypreal_minus_def:
-  "- P == Abs_hypreal(\<Union>X \<in> Rep_hypreal(P). hyprel``{%n::nat. - (X n)})"
+  "- P == Abs_hypreal(\<Union>X \<in> Rep_hypreal(P). hyprel``{%n. - (X n)})"
 
   hypreal_diff_def:
   "x - y == x + -(y::hypreal)"
@@ -49,13 +49,13 @@
 constdefs
 
   hypreal_of_real  :: "real => hypreal"
-  "hypreal_of_real r         == Abs_hypreal(hyprel``{%n::nat. r})"
+  "hypreal_of_real r         == Abs_hypreal(hyprel``{%n. r})"
 
   omega   :: hypreal   -- {*an infinite number @{text "= [<1,2,3,...>]"} *}
-  "omega == Abs_hypreal(hyprel``{%n::nat. real (Suc n)})"
+  "omega == Abs_hypreal(hyprel``{%n. real (Suc n)})"
 
   epsilon :: hypreal   -- {*an infinitesimal number @{text "= [<1,1/2,1/3,...>]"} *}
-  "epsilon == Abs_hypreal(hyprel``{%n::nat. inverse (real (Suc n))})"
+  "epsilon == Abs_hypreal(hyprel``{%n. inverse (real (Suc n))})"
 
 syntax (xsymbols)
   omega   :: hypreal   ("\<omega>")
@@ -70,16 +70,16 @@
 
   hypreal_add_def:
   "P + Q == Abs_hypreal(\<Union>X \<in> Rep_hypreal(P). \<Union>Y \<in> Rep_hypreal(Q).
-                hyprel``{%n::nat. X n + Y n})"
+                hyprel``{%n. X n + Y n})"
 
   hypreal_mult_def:
   "P * Q == Abs_hypreal(\<Union>X \<in> Rep_hypreal(P). \<Union>Y \<in> Rep_hypreal(Q).
-                hyprel``{%n::nat. X n * Y n})"
+                hyprel``{%n. X n * Y n})"
 
   hypreal_le_def:
   "P \<le> (Q::hypreal) == \<exists>X Y. X \<in> Rep_hypreal(P) &
                                Y \<in> Rep_hypreal(Q) &
-                               {n::nat. X n \<le> Y n} \<in> FreeUltrafilterNat"
+                               {n. X n \<le> Y n} \<in> FreeUltrafilterNat"
 
   hypreal_less_def: "(x < (y::hypreal)) == (x \<le> y & x \<noteq> y)"
 
@@ -112,11 +112,11 @@
 text{*Also, proof of various properties of @{term FreeUltrafilterNat}: 
 an arbitrary free ultrafilter*}
 
-lemma FreeUltrafilterNat_Ex: "\<exists>U. U: FreeUltrafilter (UNIV::nat set)"
+lemma FreeUltrafilterNat_Ex: "\<exists>U. U \<in> FreeUltrafilter (UNIV::nat set)"
 by (rule not_finite_nat [THEN FreeUltrafilter_Ex])
 
 lemma FreeUltrafilterNat_mem [simp]: 
-     "FreeUltrafilterNat: FreeUltrafilter(UNIV:: nat set)"
+     "FreeUltrafilterNat \<in> FreeUltrafilter(UNIV:: nat set)"
 apply (unfold FreeUltrafilterNat_def)
 apply (rule FreeUltrafilterNat_Ex [THEN exE])
 apply (rule someI2, assumption+)
@@ -129,7 +129,7 @@
 apply (blast dest: mem_FreeUltrafiltersetD1)
 done
 
-lemma FreeUltrafilterNat_not_finite: "x: FreeUltrafilterNat ==> ~ finite x"
+lemma FreeUltrafilterNat_not_finite: "x \<in> FreeUltrafilterNat ==> ~ finite x"
 by (blast dest: FreeUltrafilterNat_finite)
 
 lemma FreeUltrafilterNat_empty [simp]: "{} \<notin> FreeUltrafilterNat"
@@ -141,24 +141,26 @@
 done
 
 lemma FreeUltrafilterNat_Int:
-     "[| X: FreeUltrafilterNat;  Y: FreeUltrafilterNat |]   
+     "[| X \<in> FreeUltrafilterNat;  Y \<in> FreeUltrafilterNat |]   
       ==> X Int Y \<in> FreeUltrafilterNat"
-apply (cut_tac FreeUltrafilterNat_mem)
+apply (insert FreeUltrafilterNat_mem)
 apply (blast dest: FreeUltrafilter_Ultrafilter Ultrafilter_Filter mem_FiltersetD1)
 done
 
 lemma FreeUltrafilterNat_subset:
-     "[| X: FreeUltrafilterNat;  X \<subseteq> Y |]  
+     "[| X \<in> FreeUltrafilterNat;  X \<subseteq> Y |]  
       ==> Y \<in> FreeUltrafilterNat"
-apply (cut_tac FreeUltrafilterNat_mem)
+apply (insert FreeUltrafilterNat_mem)
 apply (blast dest: FreeUltrafilter_Ultrafilter Ultrafilter_Filter mem_FiltersetD2)
 done
 
 lemma FreeUltrafilterNat_Compl:
-     "X: FreeUltrafilterNat ==> -X \<notin> FreeUltrafilterNat"
-apply safe
-apply (drule FreeUltrafilterNat_Int, assumption, auto)
-done
+     "X \<in> FreeUltrafilterNat ==> -X \<notin> FreeUltrafilterNat"
+proof
+  assume "X \<in> \<U>" and "- X \<in> \<U>"
+  hence "X Int - X \<in> \<U>" by (rule FreeUltrafilterNat_Int) 
+  thus False by force
+qed
 
 lemma FreeUltrafilterNat_Compl_mem:
      "X\<notin> FreeUltrafilterNat ==> -X \<in> FreeUltrafilterNat"
@@ -168,11 +170,11 @@
 done
 
 lemma FreeUltrafilterNat_Compl_iff1:
-     "(X \<notin> FreeUltrafilterNat) = (-X: FreeUltrafilterNat)"
+     "(X \<notin> FreeUltrafilterNat) = (-X \<in> FreeUltrafilterNat)"
 by (blast dest: FreeUltrafilterNat_Compl FreeUltrafilterNat_Compl_mem)
 
 lemma FreeUltrafilterNat_Compl_iff2:
-     "(X: FreeUltrafilterNat) = (-X \<notin> FreeUltrafilterNat)"
+     "(X \<in> FreeUltrafilterNat) = (-X \<notin> FreeUltrafilterNat)"
 by (auto simp add: FreeUltrafilterNat_Compl_iff1 [symmetric])
 
 lemma cofinite_mem_FreeUltrafilterNat: "finite (-X) ==> X \<in> FreeUltrafilterNat"
@@ -220,18 +222,16 @@
 
 text{*One further property of our free ultrafilter*}
 lemma FreeUltrafilterNat_Un:
-     "X Un Y: FreeUltrafilterNat  
-      ==> X: FreeUltrafilterNat | Y: FreeUltrafilterNat"
-apply auto
-apply ultra
-done
+     "X Un Y \<in> FreeUltrafilterNat  
+      ==> X \<in> FreeUltrafilterNat | Y \<in> FreeUltrafilterNat"
+by (auto, ultra)
 
 
 subsection{*Properties of @{term hyprel}*}
 
 text{*Proving that @{term hyprel} is an equivalence relation*}
 
-lemma hyprel_iff: "((X,Y) \<in> hyprel) = ({n. X n = Y n}: FreeUltrafilterNat)"
+lemma hyprel_iff: "((X,Y) \<in> hyprel) = ({n. X n = Y n} \<in> FreeUltrafilterNat)"
 by (simp add: hyprel_def)
 
 lemma hyprel_refl: "(x,x) \<in> hyprel"
@@ -284,7 +284,7 @@
 done
 
 lemma Rep_hypreal_nonempty [simp]: "Rep_hypreal x \<noteq> {}"
-by (cut_tac x = x in Rep_hypreal, auto)
+by (insert Rep_hypreal [of x], auto)
 
 
 subsection{*@{term hypreal_of_real}: 
@@ -311,8 +311,7 @@
 
 lemma hypreal_add_congruent2: 
     "congruent2 hyprel hyprel (%X Y. hyprel``{%n. X n + Y n})"
-apply (simp add: congruent2_def, auto, ultra)
-done
+by (simp add: congruent2_def, auto, ultra)
 
 lemma hypreal_add: 
   "Abs_hypreal(hyprel``{%n. X n}) + Abs_hypreal(hyprel``{%n. Y n}) =  
@@ -350,23 +349,17 @@
 
 lemma hypreal_minus: 
    "- (Abs_hypreal(hyprel``{%n. X n})) = Abs_hypreal(hyprel `` {%n. -(X n)})"
-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])
-done
+by (simp add: hypreal_minus_def Abs_hypreal_inject 
+              hyprel_in_hypreal [THEN Abs_hypreal_inverse] 
+              UN_equiv_class [OF equiv_hyprel hypreal_minus_congruent])
 
 lemma hypreal_diff:
      "Abs_hypreal(hyprel``{%n. X n}) - Abs_hypreal(hyprel``{%n. Y n}) =  
       Abs_hypreal(hyprel``{%n. X n - Y n})"
-apply (simp add: hypreal_diff_def hypreal_minus hypreal_add)
-done
+by (simp add: hypreal_diff_def hypreal_minus hypreal_add)
 
 lemma hypreal_add_minus [simp]: "z + -z = (0::hypreal)"
-apply (simp add: hypreal_zero_def)
-apply (rule_tac z = z in eq_Abs_hypreal)
-apply (simp add: hypreal_minus hypreal_add)
-done
+by (cases z, simp add: hypreal_zero_def hypreal_minus hypreal_add)
 
 lemma hypreal_add_minus_left: "-z + z = (0::hypreal)"
 by (simp add: hypreal_add_commute hypreal_add_minus)
@@ -385,26 +378,17 @@
         UN_equiv_class2 [OF equiv_hyprel equiv_hyprel hypreal_mult_congruent2])
 
 lemma hypreal_mult_commute: "(z::hypreal) * w = w * z"
-apply (cases z, cases w)
-apply (simp add: hypreal_mult mult_ac)
-done
+by (cases z, cases w, simp add: hypreal_mult mult_ac)
 
 lemma hypreal_mult_assoc: "((z1::hypreal) * z2) * z3 = z1 * (z2 * z3)"
-apply (cases z1, cases z2, cases z3)
-apply (simp add: hypreal_mult mult_assoc)
-done
+by (cases z1, cases z2, cases z3, simp add: hypreal_mult mult_assoc)
 
 lemma hypreal_mult_1: "(1::hypreal) * z = z"
-apply (simp add: hypreal_one_def)
-apply (rule_tac z = z in eq_Abs_hypreal)
-apply (simp add: hypreal_mult)
-done
+by (cases z, simp add: hypreal_one_def hypreal_mult)
 
 lemma hypreal_add_mult_distrib:
      "((z1::hypreal) + z2) * w = (z1 * w) + (z2 * w)"
-apply (cases z1, cases z2, cases w)
-apply (simp add: hypreal_mult hypreal_add left_distrib)
-done
+by (cases z1, cases z2, cases w, simp add: hypreal_mult hypreal_add left_distrib)
 
 text{*one and zero are distinct*}
 lemma hypreal_zero_not_eq_one: "0 \<noteq> (1::hypreal)"
@@ -415,24 +399,19 @@
 
 lemma hypreal_inverse_congruent: 
   "congruent hyprel (%X. hyprel``{%n. if X n = 0 then 0 else inverse(X n)})"
-apply (simp add: congruent_def)
-apply (auto, ultra)
-done
+by (auto simp add: congruent_def, ultra)
 
 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 (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])
-done
+by (simp add: hypreal_inverse_def Abs_hypreal_inject 
+              hyprel_in_hypreal [THEN Abs_hypreal_inverse] 
+              UN_equiv_class [OF equiv_hyprel hypreal_inverse_congruent])
 
 lemma hypreal_mult_inverse: 
      "x \<noteq> 0 ==> x*inverse(x) = (1::hypreal)"
-apply (simp add: hypreal_one_def hypreal_zero_def)
 apply (cases x)
-apply (simp add: hypreal_inverse hypreal_mult)
+apply (simp add: hypreal_one_def hypreal_zero_def hypreal_inverse hypreal_mult)
 apply (drule FreeUltrafilterNat_Compl_mem)
 apply (blast intro!: right_inverse FreeUltrafilterNat_subset)
 done
@@ -476,19 +455,13 @@
 done
 
 lemma hypreal_le_refl: "w \<le> (w::hypreal)"
-apply (cases w)
-apply (simp add: hypreal_le) 
-done
+by (cases w, simp add: hypreal_le)
 
 lemma hypreal_le_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::hypreal)"
-apply (cases i, cases j, cases k)
-apply (simp add: hypreal_le, ultra)
-done
+by (cases i, cases j, cases k, simp add: hypreal_le, ultra)
 
 lemma hypreal_le_anti_sym: "[| z \<le> w; w \<le> z |] ==> z = (w::hypreal)"
-apply (cases z, cases w)
-apply (simp add: hypreal_le, ultra)
-done
+by (cases z, cases w, simp add: hypreal_le, ultra)
 
 (* Axiom 'order_less_le' of class 'order': *)
 lemma hypreal_less_le: "((w::hypreal) < z) = (w \<le> z & w \<noteq> z)"
@@ -554,15 +527,11 @@
 
 lemma hypreal_of_real_add [simp]: 
      "hypreal_of_real (w + z) = hypreal_of_real w + hypreal_of_real z"
-apply (simp add: hypreal_of_real_def)
-apply (simp add: hypreal_add left_distrib)
-done
+by (simp add: hypreal_of_real_def, simp add: hypreal_add left_distrib)
 
 lemma hypreal_of_real_mult [simp]: 
      "hypreal_of_real (w * z) = hypreal_of_real w * hypreal_of_real z"
-apply (simp add: hypreal_of_real_def)
-apply (simp add: hypreal_mult right_distrib)
-done
+by (simp add: hypreal_of_real_def, simp add: hypreal_mult right_distrib)
 
 lemma hypreal_of_real_one [simp]: "hypreal_of_real 1 = (1::hypreal)"
 by (simp add: hypreal_of_real_def hypreal_one_def)
@@ -627,8 +596,7 @@
 lemma hypreal_less: 
       "(Abs_hypreal(hyprel``{%n. X n}) < Abs_hypreal(hyprel``{%n. Y n})) =  
        ({n. X n < Y n} \<in> FreeUltrafilterNat)"
-apply (auto simp add: hypreal_le linorder_not_le [symmetric], ultra+)
-done
+by (auto simp add: hypreal_le linorder_not_le [symmetric], ultra+)
 
 lemma hypreal_zero_num: "0 = Abs_hypreal (hyprel `` {%n. 0})"
 by (simp add: hypreal_zero_def [THEN meta_eq_to_obj_eq, symmetric])
@@ -637,9 +605,7 @@
 by (simp add: hypreal_one_def [THEN meta_eq_to_obj_eq, symmetric])
 
 lemma hypreal_omega_gt_zero [simp]: "0 < omega"
-apply (simp add: omega_def)
-apply (auto simp add: hypreal_less hypreal_zero_num)
-done
+by (auto simp add: omega_def hypreal_less hypreal_zero_num)
 
 lemma hypreal_hrabs:
      "abs (Abs_hypreal (hyprel `` {X})) = 
@@ -685,7 +651,7 @@
 done
 
 lemma hypreal_of_real_not_eq_omega: "hypreal_of_real x \<noteq> omega"
-by (cut_tac not_ex_hypreal_of_real_eq_omega, auto)
+by (insert not_ex_hypreal_of_real_eq_omega, auto)
 
 text{*Existence of infinitesimal number also not corresponding to any
  real number*}
@@ -698,14 +664,12 @@
 lemma lemma_finite_epsilon_set: "finite {n. x = inverse(real(Suc n))}"
 by (cut_tac x = x in lemma_epsilon_empty_singleton_disj, auto)
 
-lemma not_ex_hypreal_of_real_eq_epsilon: 
-      "~ (\<exists>x. hypreal_of_real x = epsilon)"
-apply (simp add: epsilon_def hypreal_of_real_def)
-apply (auto simp add: lemma_finite_epsilon_set [THEN FreeUltrafilterNat_finite])
-done
+lemma not_ex_hypreal_of_real_eq_epsilon: "~ (\<exists>x. hypreal_of_real x = epsilon)"
+by (auto simp add: epsilon_def hypreal_of_real_def 
+                   lemma_finite_epsilon_set [THEN FreeUltrafilterNat_finite])
 
 lemma hypreal_of_real_not_eq_epsilon: "hypreal_of_real x \<noteq> epsilon"
-by (cut_tac not_ex_hypreal_of_real_eq_epsilon, auto)
+by (insert not_ex_hypreal_of_real_eq_epsilon, auto)
 
 lemma hypreal_epsilon_not_zero: "epsilon \<noteq> 0"
 by (simp add: epsilon_def hypreal_zero_def)
diff -r ef1a47a4996b -r 14b2c22a7e40 src/HOL/Integ/Bin.thy
--- a/src/HOL/Integ/Bin.thy	Thu May 06 12:42:20 2004 +0200
+++ b/src/HOL/Integ/Bin.thy	Thu May 06 12:43:00 2004 +0200
@@ -1,9 +1,9 @@
 (*  Title:	HOL/Integ/Bin.thy
     ID:         $Id$
     Authors:	Lawrence C Paulson, Cambridge University Computer Laboratory
-		David Spelt, University of Twente
     Copyright	1994  University of Cambridge
-    Copyright   1996 University of Twente
+
+Ported from ZF to HOL by David Spelt.
 *)
 
 header{*Arithmetic on Binary Integers*}